The meaning of "module M" in export lists is rather subtle, and the above reformulation (or the one-word change) seems to make a subtle change to it. It is not just a clarification. Is that what you intend?!

It depends, I guess, on your interpretation of the report as it stands. It wasn't clear to me whether it is legal to export an entity, using the 'module M' syntax, whose qualified name is ambiguous. Admittedly, if I'd checked your specification I'd have noticed that your interpretation differed from mine, sorry about that. Nevertheless, since there are two interpretations, the report should clarify which one is meant.

A nice aspect of our formal semantics is that the computation of the exports and inscope relations, which includes fixpoint iteration to give meaning to recursive modules, and the error checking can be kept separate. The change proposed above means that the error checking has to be integrated with the fixpoint iteration (or that the fixpoint iteration has to return more than the resulting inscope/export relations), and thus complicates the specification.

Ok, that sounds like a good reason to prefer your current interpretation. Cheers, Simon