I said appending when changing the union is immutable. Thus your example code above won't typecheck as it requires a mutable reference but the method signature is:
Isn't a collection you cannot change a bit useless? How can I do anything with it?
Afaics that isn't sound, because this requires the linker to be a compiler. In short, you need to compile all the linked modules at the same time. There can't be any more modularity in code. I could write some new code that breaks code that used to compile in another module.
No, its fine, it just needs the header files to list the types that implement each trait. The compiler automatically generates a header/interface for each file it compiles. This contains encoded versions of the type signatures of the public functions in a module (otherwise it could not type check when you import a module without repassing the source code). If we extend the interface generated with trait information, which types implement which traits, and which traits are bounds on which other traits, then the compiler can complete these checks in the link phase.
Edit: If you think about it, some, if not all, of this information must be there, so that when you use a module it knows which types inside that module implement which traits (whether defined in that module or another). This is done without recompiling the used modules (unless it has changed since the last compile).
In any case this is no less sound than your own suggestion which would be required to build the 'union' of types across all source modules. In effect the trait represents the union of types that implement that trait.
Remember soundness is the property of a type system to prevent programs that go wrong at runtime from passing the type checker. So with the unions, if you have to check whether a type in the collection implements the trait at runtime, your static type system is unsound.