Well, in the model, there is no such thing as effective type of objects loosing their power at TU boundaries, and otherwise no relationship defined between effe

Well, in the model, there is no such thing as effective type of objects loosing their power at TU boundaries, and otherwise no relationship defined between effective types and linkage. An implementation that tags all accesses to dynamically check/enforce the effective type rules (by killing a faulty program or doing otherwise nasty stuffs) would not loose its conformance because of that. The default behavior of an implementation used under a particular and completely unspecified build-system is irrelevant to the fact that aliasing analysis is allowed across TU boundaries in the model, and the fact that it does not happen in some cases is just an implementation detail - that if not guaranteed by other means can always be changed without even a warning by compiler vendors. Now that is the situation, in regard with the standard. Should we be happy with it or not is another story.