It is difficult to explain where it is unsound because afaics you have not specified all the details such a design will require, e.g. how can the compiler convey to the linker that adding a data type to a collection was dependent on a change to the collection's element type at a particular scope. Essentially you have just converted the linker into a compiler, which was my point before. Afaics there simply isn't any way to remove the invariant that the data types that were already in the collection have been erased from the compiler's AST by the time you need to add the new trait to conjunction which is the element type. I am 99.9% confident when you work through the details, you will discover it is unsound and can't be fixed.