Section 5.2 (Export lists) doesn't anticipate this question; note the separation between items (5) and (6), whose wording I reproduce below.
Thus provoked, I have come up with another formulation that simplifies the specification, and evades both this problem and others. Here it is:
Replace (5) and (6) by:
(5') The form 'module M' abbreviates the set of all entities whose unqualified name, 'e', is in scope, and for which the qualified name 'M.e' is also in scope. This set may be empty.
It is an error to use module M in an export list unless M is the module bearing the export list, or M is imported by at least one import declaration (qualified or unqualified).
Am I the only one that thinks it's strange that module M ( module A ) where import B as A exports the contents of module B? A isn't even a module! The old definition claims that 'module M where' is the same as 'module M (module M) where' which is a nice property. Perhaps we can clarify the definition so that this is the case. One way to do this is to make 'module M' exports refer to the actual module M, not including any modules renamed to M. Since module names are unique, this is a much simpler formulation and doesn't end up exporting entities from several different modules. I suggest just changing the phrase "or `import A as M [impspec]'" to "or `import M as A [impspec]'" in point (5). Note that this change is slightly strange in a different way - exporting 'module M' doesn't necessarily export the entities which can be referred to by 'M.foo'. Anyway, I thought I'd throw this out as an alternative. Cheers, Simon