Disallow outer aliases of core module type from inside core module types

design/mvp/Binary.md

@@ -168,8 +168,10 @@ core:exportdecl  ::= n:<core:name> d:<core:importdesc>  => (export n d)
 ```
 Notes:
 * Reused Core binary rules: [`core:import`], [`core:importdesc`], [`core:functype`]
-* Validation of `core:moduledecl` (currently) rejects `core:moduletype` definitions
-  inside `type` declarators (i.e., nested core module types).
+* Validation of `core:moduledecl` rejects `core:moduletype` definitions
+  and `outer` aliases of `core:moduletype` definitions inside `type`
+  declarators. Thus, as an invariant, when validating a `core:moduletype`, the
+  core type index space will not contain any core module types.
 * As described in the explainer, each module type is validated with an
   initially-empty type index space.
 * `alias` declarators currently only allow `outer` `type` aliases but

design/mvp/Explainer.md

@@ -477,11 +477,12 @@ where strip-id(X) parses '(' sort Y ')' when X parses '(' sort <id>? Y ')'
 ```
 
 Here, `core:deftype` (short for "defined type") is inherited from the [gc]
-proposal and extended with a `module` type constructor. If module-linking is
+proposal and extended with a `module` type constructor. If [module-linking] is
 added to Core WebAssembly, an `instance` type constructor would be added as
 well but, for now, it's left out since it's unnecessary. Also, in the MVP,
-validation will reject nested `core:moduletype`, since, before module-linking,
-core modules cannot themselves import or export other core modules.
+validation will reject `core:moduletype` defining or aliasing other
+`core:moduletype`s, since, before module-linking, core modules cannot
+themselves import or export other core modules.
 
 The body of a module type contains an ordered list of "module declarators"
 which describe, at a type level, the imports and exports of the module. In a