diff --git a/design/mvp/Binary.md b/design/mvp/Binary.md
index 04a10dcd..550b9c43 100644
--- a/design/mvp/Binary.md
+++ b/design/mvp/Binary.md
@@ -48,7 +48,10 @@ Notes:
   WebAssembly 1.0 spec.)
 * The `layer` field is meant to distinguish modules from components early in
   the binary format. (Core WebAssembly modules already implicitly have a
-  `layer` field of `0x0` in their 4 byte [`core:version`] field.)
+  `layer` field of `0x0` if the existing 4-byte [`core:version`] field is
+  reinterpreted as two 2-byte fields. This implies that the Core WebAssembly
+  spec needs to make a backwards-compatible spec change to split `core:version`
+  and fix `layer` to forever be `0x0`.)
 
 
 ## Instance Definitions
@@ -72,8 +75,8 @@ core:inlineexport   ::= n:<core:name> si:<core:sortidx>                    => (e
 instance            ::= ie:<instanceexpr>                                  => (instance ie)
 instanceexpr        ::= 0x00 c:<componentidx> arg*:vec(<instantiatearg>)   => (instantiate c arg*)
                       | 0x01 e*:vec(<inlineexport>)                        => e*
-instantiatearg      ::= n:<string>  si:<sortidx>                           => (with n si)
-string              ::= s:<core:name>                                      => s
+instantiatearg      ::= n:<name>  si:<sortidx>                             => (with n si)
+name                ::= n:<core:name>                                      => n
 sortidx             ::= sort:<sort> idx:<u32>                              => (sort idx)
 sort                ::= 0x00 cs:<core:sort>                                => core cs
                       | 0x01                                               => func
@@ -96,7 +99,7 @@ Notes:
 * Validation of `core:instantiatearg` initially only allows the `instance`
   sort, but would be extended to accept other sorts as core wasm is extended.
 * Validation of `instantiate` requires each `<importname>` in `c` to match a
-  `string` in a `with` argument (compared as strings) and for the types to
+  `name` in a `with` argument (compared as strings) and for the types to
   match.
 * When validating `instantiate`, after each individual type-import is supplied
   via `with`, the actual type supplied is immediately substituted for all uses
@@ -111,7 +114,7 @@ Notes:
 (See [Alias Definitions](Explainer.md#alias-definitions) in the explainer.)
 ```ebnf
 alias       ::= s:<sort> t:<aliastarget>                => (alias t (s))
-aliastarget ::= 0x00 i:<instanceidx> n:<string>         => export i n
+aliastarget ::= 0x00 i:<instanceidx> n:<name>           => export i n
               | 0x01 i:<core:instanceidx> n:<core:name> => core export i n
               | 0x02 ct:<u32> idx:<u32>                 => outer ct idx
 ```
diff --git a/design/mvp/CanonicalABI.md b/design/mvp/CanonicalABI.md
index 0223486f..f1ecf285 100644
--- a/design/mvp/CanonicalABI.md
+++ b/design/mvp/CanonicalABI.md
@@ -7,7 +7,7 @@ of modules in Core WebAssembly.
 * [Supporting definitions](#supporting-definitions)
   * [Despecialization](#despecialization)
   * [Alignment](#alignment)
-  * [Size](#size)
+  * [Element Size](#element-size)
   * [Runtime State](#runtime-state)
   * [Loading](#loading)
   * [Storing](#storing)
@@ -156,13 +156,17 @@ Handle types are passed as `i32` indices into the `Table[HandleElem]`
 introduced below.
 
 
-### Size
+### Element Size
 
-Each value type is also assigned a `size`, measured in bytes, which corresponds
-the `sizeof` operator in C. Empty types, such as records with no fields, are
-not permitted, to avoid complications in source languages.
+Each value type is also assigned an `elem_size` which is the number of bytes
+used when values of the type are stored as elements of a `list`. Having this
+byte size be a static property of the type instead of attempting to use a
+variable-length element-encoding scheme both simplifies the implementation and
+maps well to languages which represent `list`s as random-access arrays. Empty
+types, such as records with no fields, are not permitted, to avoid
+complications in source languages.
 ```python
-def size(t):
+def elem_size(t):
   match despecialize(t):
     case Bool()             : return 1
     case S8() | U8()        : return 1
@@ -173,33 +177,33 @@ def size(t):
     case F64()              : return 8
     case Char()             : return 4
     case String() | List(_) : return 8
-    case Record(fields)     : return size_record(fields)
-    case Variant(cases)     : return size_variant(cases)
-    case Flags(labels)      : return size_flags(labels)
+    case Record(fields)     : return elem_size_record(fields)
+    case Variant(cases)     : return elem_size_variant(cases)
+    case Flags(labels)      : return elem_size_flags(labels)
     case Own(_) | Borrow(_) : return 4
 
-def size_record(fields):
+def elem_size_record(fields):
   s = 0
   for f in fields:
     s = align_to(s, alignment(f.t))
-    s += size(f.t)
+    s += elem_size(f.t)
   assert(s > 0)
   return align_to(s, alignment_record(fields))
 
 def align_to(ptr, alignment):
   return math.ceil(ptr / alignment) * alignment
 
-def size_variant(cases):
-  s = size(discriminant_type(cases))
+def elem_size_variant(cases):
+  s = elem_size(discriminant_type(cases))
   s = align_to(s, max_case_alignment(cases))
   cs = 0
   for c in cases:
     if c.t is not None:
-      cs = max(cs, size(c.t))
+      cs = max(cs, elem_size(c.t))
   s += cs
   return align_to(s, alignment_variant(cases))
 
-def size_flags(labels):
+def elem_size_flags(labels):
   n = len(labels)
   assert(n > 0)
   if n <= 8: return 1
@@ -430,7 +434,7 @@ the top-level case analysis:
 ```python
 def load(cx, ptr, t):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : return convert_int_to_bool(load_int(cx, ptr, 1))
     case U8()           : return load_int(cx, ptr, 1)
@@ -511,6 +515,7 @@ testing that its unsigned integral value is in the valid [Unicode Code Point]
 range and not a [Surrogate]:
 ```python
 def convert_i32_to_char(cx, i):
+  assert(i >= 0)
   trap_if(i >= 0x110000)
   trap_if(0xD800 <= i <= 0xDFFF)
   return chr(i)
@@ -571,10 +576,10 @@ def load_list(cx, ptr, elem_type):
 
 def load_list_from_range(cx, ptr, length, elem_type):
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
-  trap_if(ptr + length * size(elem_type) > len(cx.opts.memory))
+  trap_if(ptr + length * elem_size(elem_type) > len(cx.opts.memory))
   a = []
   for i in range(length):
-    a.append(load(cx, ptr + i * size(elem_type), elem_type))
+    a.append(load(cx, ptr + i * elem_size(elem_type), elem_type))
   return a
 
 def load_record(cx, ptr, fields):
@@ -582,7 +587,7 @@ def load_record(cx, ptr, fields):
   for field in fields:
     ptr = align_to(ptr, alignment(field.t))
     record[field.label] = load(cx, ptr, field.t)
-    ptr += size(field.t)
+    ptr += elem_size(field.t)
   return record
 ```
 As a technical detail: the `align_to` in the loop in `load_record` is
@@ -599,7 +604,7 @@ implementation can build the appropriate index tables at compile-time so that
 variant-passing is always O(1) and not involving string operations.
 ```python
 def load_variant(cx, ptr, cases):
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   case_index = load_int(cx, ptr, disc_size)
   ptr += disc_size
   trap_if(case_index >= len(cases))
@@ -630,7 +635,7 @@ derived from the ordered labels of the `flags` type. The code here takes
 advantage of Python's support for integers of arbitrary width.
 ```python
 def load_flags(cx, ptr, labels):
-  i = load_int(cx, ptr, size_flags(labels))
+  i = load_int(cx, ptr, elem_size_flags(labels))
   return unpack_flags_from_int(i, labels)
 
 def unpack_flags_from_int(i, labels):
@@ -670,8 +675,13 @@ def lift_borrow(cx, i, t):
     cx.track_owning_lend(h)
   return h.rep
 ```
-The `track_owning_lend` call to `CallContext` participates in the enforcement of
-the dynamic borrow rules.
+The `track_owning_lend` call to `CallContext` participates in the enforcement
+of the dynamic borrow rules, which keep the source `own` handle alive until the
+end of the call (as an intentionally-conservative upper bound on how long the
+`borrow` handle can be held). This tracking is only required when `h` is an
+`own` handle because, when `h` is a `borrow` handle, this tracking has already
+happened (when the originating `own` handle was lifted) for a strictly longer
+call scope than the current call.
 
 
 ### Storing
@@ -682,7 +692,7 @@ The `store` function defines how to write a value `v` of a given value type
 ```python
 def store(cx, v, t, ptr):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : store_int(cx, int(bool(v)), ptr, 1)
     case U8()           : store_int(cx, v, ptr, 1)
@@ -990,20 +1000,20 @@ def store_list(cx, v, ptr, elem_type):
   store_int(cx, length, ptr + 4, 4)
 
 def store_list_into_range(cx, v, elem_type):
-  byte_length = len(v) * size(elem_type)
+  byte_length = len(v) * elem_size(elem_type)
   trap_if(byte_length >= (1 << 32))
   ptr = cx.opts.realloc(0, 0, alignment(elem_type), byte_length)
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
   trap_if(ptr + byte_length > len(cx.opts.memory))
   for i,e in enumerate(v):
-    store(cx, e, elem_type, ptr + i * size(elem_type))
+    store(cx, e, elem_type, ptr + i * elem_size(elem_type))
   return (ptr, len(v))
 
 def store_record(cx, v, ptr, fields):
   for f in fields:
     ptr = align_to(ptr, alignment(f.t))
     store(cx, v[f.label], f.t, ptr)
-    ptr += size(f.t)
+    ptr += elem_size(f.t)
 ```
 
 Variants are stored using the `|`-separated list of `refines` cases built
@@ -1015,7 +1025,7 @@ case indices to the consumer's case indices.
 ```python
 def store_variant(cx, v, ptr, cases):
   case_index, case_value = match_case(v, cases)
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   store_int(cx, case_index, ptr, disc_size)
   ptr += disc_size
   ptr = align_to(ptr, max_case_alignment(cases))
@@ -1042,7 +1052,7 @@ to variants.
 ```python
 def store_flags(cx, v, ptr, labels):
   i = pack_flags_into_int(v, labels)
-  store_int(cx, i, ptr, size_flags(labels))
+  store_int(cx, i, ptr, elem_size_flags(labels))
 
 def pack_flags_into_int(v, labels):
   i = 0
@@ -1296,7 +1306,7 @@ def lift_flat_variant(cx, vi, cases):
         case ('i64', 'i32') : return wrap_i64_to_i32(x)
         case ('i64', 'f32') : return decode_i32_as_float(wrap_i64_to_i32(x))
         case ('i64', 'f64') : return decode_i64_as_float(x)
-        case _              : return x
+        case _              : assert(have == want); return x
   c = cases[case_index]
   if c.t is None:
     v = None
@@ -1407,7 +1417,7 @@ def lower_flat_variant(cx, v, cases):
         case ('i32', 'i64') : payload[i] = fv
         case ('f32', 'i64') : payload[i] = encode_float_as_i32(fv)
         case ('f64', 'i64') : payload[i] = encode_float_as_i64(fv)
-        case _              : pass
+        case _              : assert(have == want)
   for _ in flat_types:
     payload.append(0)
   return [case_index] + payload
@@ -1437,7 +1447,7 @@ def lift_values(cx, max_flat, vi, ts):
     ptr = vi.next('i32')
     tuple_type = Tuple(ts)
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     return list(load(cx, ptr, tuple_type).values())
   else:
     return [ lift_flat(cx, vi, t) for t in ts ]
@@ -1455,11 +1465,11 @@ def lower_values(cx, max_flat, vs, ts, out_param = None):
     tuple_type = Tuple(ts)
     tuple_value = {str(i): v for i,v in enumerate(vs)}
     if out_param is None:
-      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), size(tuple_type))
+      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), elem_size(tuple_type))
     else:
       ptr = out_param.next('i32')
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     store(cx, tuple_value, tuple_type, ptr)
     return [ptr]
   else:
diff --git a/design/mvp/Explainer.md b/design/mvp/Explainer.md
index 212d6f54..d7b6f2a6 100644
--- a/design/mvp/Explainer.md
+++ b/design/mvp/Explainer.md
@@ -269,9 +269,9 @@ instances, but with an expanded component-level definition of `sort`:
 instance       ::= (instance <id>? <instanceexpr>)
 instanceexpr   ::= (instantiate <componentidx> <instantiatearg>*)
                  | <inlineexport>*
-instantiatearg ::= (with <string> <sortidx>)
-                 | (with <string> (instance <inlineexport>*))
-string         ::= <core:name>
+instantiatearg ::= (with <name> <sortidx>)
+                 | (with <name> (instance <inlineexport>*))
+name           ::= <core:name>
 sortidx        ::= (<sort> <u32>)
 sort           ::= core <core:sort>
                  | func
@@ -290,7 +290,7 @@ future include `data`). Thus, component-level `sort` injects the full set
 of `core:sort`, so that they may be referenced (leaving it up to validation
 rules to throw out the core sorts that aren't allowed in various contexts).
 
-The `string` production reuses the `core:name` quoted-string-literal syntax of
+The `name` production reuses the `core:name` quoted-string-literal syntax of
 Core WebAssembly (which appears in core module imports and exports and can
 contain any valid UTF-8 string).
 
@@ -312,14 +312,14 @@ instance, the `core export` of a core module instance and a definition of an
 `outer` component (containing the current component):
 ```ebnf
 alias            ::= (alias <aliastarget> (<sort> <id>?))
-aliastarget      ::= export <instanceidx> <string>
+aliastarget      ::= export <instanceidx> <name>
                    | core export <core:instanceidx> <core:name>
                    | outer <u32> <u32>
 ```
 If present, the `id` of the alias is bound to the new index added by the alias
 and can be used anywhere a normal `id` can be used.
 
-In the case of `export` aliases, validation ensures `string` is an export in the
+In the case of `export` aliases, validation ensures `name` is an export in the
 target instance and has a matching sort.
 
 In the case of `outer` aliases, the `u32` pair serves as a [de Bruijn
@@ -347,7 +347,7 @@ sortidx     ::= (<sort> <u32>)          ;; as above
               | <inlinealias>
 Xidx        ::= <u32>                   ;; as above
               | <inlinealias>
-inlinealias ::= (<sort> <u32> <string>+)
+inlinealias ::= (<sort> <u32> <name>+)
 ```
 If `<sort>` refers to a `<core:sort>`, then the `<u32>` of `inlinealias` is a
 `<core:instanceidx>`; otherwise it's an `<instanceidx>`. For example, the
@@ -433,10 +433,10 @@ type and function definitions which are introduced in the next two sections.
 The syntax for defining core types extends the existing core type definition
 syntax, adding a `module` type constructor:
 ```ebnf
-core:type        ::= (type <id>? <core:deftype>)              (GC proposal)
-core:deftype     ::= <core:functype>                          (WebAssembly 1.0)
-                   | <core:structtype>                        (GC proposal)
-                   | <core:arraytype>                         (GC proposal)
+core:rectype     ::= ... from the Core WebAssembly spec
+core:typedef     ::= ... from the Core WebAssembly spec
+core:subtype     ::= ... from the Core WebAssembly spec
+core:comptype    ::= ... from the Core WebAssembly spec
                    | <core:moduletype>
 core:moduletype  ::= (module <core:moduledecl>*)
 core:moduledecl  ::= <core:importdecl>
@@ -452,12 +452,16 @@ core:exportdesc  ::= strip-id(<core:importdesc>)
 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
-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 `core:moduletype` defining or aliasing other
-`core:moduletype`s, since, before module-linking, core modules cannot
+Here, `core:comptype` (short for "composite type") as defined in the [GC]
+proposal is extended with a `module` type constructor. The GC proposal also
+adds recursion and explicit subtyping between core wasm types. Owing to
+their different requirements and intended modes of usage, module types
+support implicit subtyping and are not recursive. Thus, the existing core
+validation rules would require the declared supertypes of module types to be
+empty and disallow recursive use of module types.
+
+In the MVP, validation will also 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"
@@ -571,6 +575,8 @@ typebound     ::= (eq <typeidx>)
 
 where bind-id(X) parses '(' sort <id>? Y ')' when X parses '(' sort Y ')'
 ```
+Because there is nothing in this type grammar analogous to the [gc] proposal's
+[`rectype`], none of these types are recursive.
 
 #### Fundamental value types
 
@@ -626,14 +632,20 @@ contain the opaque address of a resource and avoid copying the resource when
 passed across component boundaries. By way of metaphor to operating systems,
 handles are analogous to file descriptors, which are stored in a table and may
 only be used indirectly by untrusted user-mode processes via their integer
-index in the table. In the Component Model, handles are lifted-from and
-lowered-into `i32` values that index an encapsulated per-component-instance
-*handle table* that is maintained by the canonical function definitions
-described [below](#canonical-definitions). The uniqueness and dropping
-conditions mentioned above are enforced at runtime by the Component Model
-through these canonical definitions. The `typeidx` immediate of a handle type
-must refer to a `resource` type (described below) that statically classifies
-the particular kinds of resources the handle can point to.
+index in the table.
+
+In the Component Model, handles are lifted-from and lowered-into `i32` values
+that index an encapsulated per-component-instance *handle table* that is
+maintained by the canonical function definitions described
+[below](#canonical-definitions). In the future, handles could be
+backwards-compatibly lifted and lowered from [reference types]  (via the
+addition of a new `canonopt`, as introduced [below](#canonical-abi)).
+
+The uniqueness and dropping conditions mentioned above are enforced at runtime
+by the Component Model through these canonical definitions. The `typeidx`
+immediate of a handle type must refer to a `resource` type (described below)
+that statically classifies the particular kinds of resources the handle can
+point to.
 
 #### Specialized value types
 
@@ -769,8 +781,10 @@ declarators to be used by subsequent declarators in the type:
 ```
 
 The `type` declarator is restricted by validation to disallow `resource` type
-definitions. Thus, the only resource types possible in an `instancetype` or
-`componenttype` are introduced by `importdecl` or `exportdecl`.
+definitions, thereby preventing "private" resource type definitions from
+appearing in component types and avoiding the [avoidance problem]. Thus, the
+only resource types possible in an `instancetype` or `componenttype` are
+introduced by `importdecl` or `exportdecl`.
 
 With what's defined so far, we can define component types using a mix of type
 definitions:
@@ -788,8 +802,8 @@ definitions:
     (export "h" (func (result $U)))
     (import "T" (type $T (sub resource)))
     (import "i" (func (param "x" (list (own $T)))))
-    (export $T' "T2" (type (eq $T)))
-    (export $U' "U" (type (sub resource)))
+    (export "T2" (type $T' (eq $T)))
+    (export "U" (type $U' (sub resource)))
     (export "j" (func (param "x" (borrow $T')) (result (own $U'))))
   ))
 )
@@ -960,7 +974,7 @@ as well. For example, in this component:
 (component
   (import "C" (component $C
     (export "T1" (type (sub resource)))
-    (export $T2 "T2" (type (sub resource)))
+    (export "T2" (type $T2 (sub resource)))
     (export "T3" (type (eq $T2)))
   ))
   (instance $c (instantiate $C))
@@ -1028,7 +1042,7 @@ following component:
 is assigned the following `componenttype`:
 ```wasm
 (component
-  (export $r1 "r1" (type (sub resource)))
+  (export "r1" (type $r1 (sub resource)))
   (export "r2" (type (eq $r1)))
 )
 ```
@@ -1039,7 +1053,7 @@ If a component wants to hide this fact and force clients to assume `r1` and
 `r2` are distinct types (thereby allowing the implementation to actually use
 separate types in the future without breaking clients), an explicit type can be
 ascribed to the export that replaces the `eq` bound with a less-precise `sub`
-bound.
+bound (using syntax introduced [below](#import-and-export-definitions)).
 ```wasm
 (component
   (type $r (resource (rep i32)))
@@ -2001,6 +2015,7 @@ and will be added over the coming months to complete the MVP proposal:
 [stack-switching]: https://github.com/WebAssembly/stack-switching/blob/main/proposals/stack-switching/Overview.md
 [esm-integration]: https://github.com/WebAssembly/esm-integration/tree/main/proposals/esm-integration
 [gc]: https://github.com/WebAssembly/gc/blob/main/proposals/gc/MVP.md
+[`rectype`]: https://webassembly.github.io/gc/core/text/types.html#text-rectype
 [shared-everything-threads]: https://github.com/WebAssembly/shared-everything-threads
 [WASI Preview 2]: https://github.com/WebAssembly/WASI/tree/main/preview2
 
diff --git a/design/mvp/WIT.md b/design/mvp/WIT.md
index 87bb8a68..85c47275 100644
--- a/design/mvp/WIT.md
+++ b/design/mvp/WIT.md
@@ -16,8 +16,9 @@ The Wasm Interface Type (WIT) format is an [IDL] to provide tooling for the
 A WIT package is a collection of WIT [`interface`s][interfaces] and
 [`world`s][worlds] defined in files in the same directory that all use the
 file extension `wit`, for example `foo.wit`. Files are encoded as valid utf-8
-bytes. Types can be imported between interfaces within a package and
-additionally from other packages through IDs.
+bytes. Types can be imported between interfaces within a package using
+unqualified names and additionally from other packages through namespace-
+and-package-qualified names.
 
 This document will go through the purpose of the syntactic constructs of a WIT
 document, a pseudo-formal [grammar specification][lexical-structure], and
@@ -223,10 +224,10 @@ interface my-interface {
 }
 
 world command {
-  // generates an import of the ID `local:demo/my-interface`
+  // generates an import of the name `local:demo/my-interface`
   import my-interface;
 
-  // generates an import of the ID `wasi:filesystem/types`
+  // generates an import of the name `wasi:filesystem/types`
   import wasi:filesystem/types;
 
   // generates an import of the plain name `foo`
@@ -290,37 +291,12 @@ world union-my-world {
 }
 ```
 
-The `include` statement also works with [WIT package](#wit-packages-and-use) defined below with the same semantics. For example, the following World `union-my-world-a` is equivalent to `union-my-world-b`:
+### De-duplication of interfaces
 
-```wit
-package local:demo;
-
-interface b { ... }
-interface a { ... }
-
-world my-world-a {
-    import a;
-    import b;
-    import wasi:io/c;
-    export d: interface { ... }
-}
-
-world union-my-world-a {
-    include my-world-a;
-}
-
-world union-my-world-b {
-    import a;
-    import b;
-    import wasi:io/c;
-
-    export d: interface { ... }
-}
-```
-
-### De-duplication of IDs
-
-If two worlds shared the same set of import and export IDs, then the union of the two worlds will only contain one copy of this set. For example, the following two worlds `union-my-world-a` and `union-my-world-b` are equivalent:
+If two worlds share an imported or exported [interface name], then the union of
+the two worlds will only contain one copy of that imported or exported name.
+For example, the following two worlds `union-my-world-a` and `union-my-world-b`
+are equivalent:
 
 ```wit
 package local:demo;
@@ -348,9 +324,14 @@ world union-my-world-b {
 
 ### Name Conflicts and `with`
 
-When two or more included Worlds have the same name for an import or export that does *not* have an ID, automatic de-duplication cannot be used (because the two same-named imports/exports might have different meanings in the different worlds) and thus the conflict has to be resolved manually using the `with` keyword:
-The following example shows how to resolve name conflicts where `union-my-world-a` and `union-my-world-b` are equivalent:
+When two or more included Worlds have the same name for an import or export
+with a *plain* name, automatic de-duplication cannot be used (because the two
+same-named imports/exports might have different meanings in the different
+worlds) and thus the conflict has to be resolved manually using the `with`
+keyword.
 
+The following example shows how to resolve name conflicts where
+`union-my-world-a` and `union-my-world-b` are equivalent:
 ```wit
 package local:demo;
 
@@ -368,8 +349,8 @@ world union-my-world-b {
 }
 ```
 
-`with` cannot be used to rename IDs, however, so the following world would be invalid:
-
+`with` cannot be used to rename interface names, however, so the following
+world would be invalid:
 ```wit
 package local:demo;
 
@@ -382,7 +363,7 @@ world world-using-a {
 }
 
 world invalid-union-world {
-    include my-using-a with { a as b }  // invalid: 'a', which is short for 'local:demo/a', is an ID
+    include my-using-a with { a as b }  // invalid: 'a', which is short for 'local:demo/a', is an interface name
 }
 
 ```
@@ -465,7 +446,11 @@ interface my-host-functions {
 ```
 
 Here the `types` interface is not defined in `host.wit` but lookup will find it
-as it's defined in the same package, just instead in a different file.
+as it's defined in the same package, just instead in a different file. Since
+files are not ordered, but type definitions in the Component Model are ordered
+and acyclic, the WIT parser will perform an implicit topological sort of all
+parsed WIT definitions to find an acyclic definition order (or produce an error
+if there is none).
 
 When importing or exporting an [interface][interfaces] in a [world][worlds]
 the same syntax is used in `import` and `export` directives:
@@ -490,9 +475,8 @@ interface another-interface {
 }
 ```
 
-When referring to an interface an ID form can additionally be used to refer to
-dependencies. For example above it was seen:
-
+When referring to an interface, a fully-qualified [interface name] can be used.
+For example, in this WIT document:
 ```wit
 package local:demo;
 
@@ -500,11 +484,8 @@ world my-world {
   import wasi:clocks/monotonic-clock;
 }
 ```
-
-Here the interface being referred to is the ID `wasi:clocks/monotonic-clock`.
-This is the package identified by `wasi:clocks` and the interface
-`monotonic-clock` within that package. This same syntax can be used in `use` as
-well:
+The `monotonic-clock` interface of the `wasi:clocks` package is being imported.
+This same syntax can be used in `use` as well:
 
 ```wit
 package local:demo;
@@ -577,7 +558,7 @@ use wasi:http/handler as http-handler;
 ```
 
 Note that these can all be combined to additionally import packages with
-multiple versions and renaming as different identifiers.
+multiple versions and renaming as different WIT identifiers.
 
 ```wit
 package local:demo;
@@ -638,10 +619,28 @@ to the fact that the `use shared.{ ... }` implicitly requires that `shared` is
 imported into the component as well.
 
 Note that the name `"local:demo/shared"` here is derived from the name of the
-`interface` plus the package ID `local:demo`.
+`interface` plus the package name `local:demo`.
 
-For `export`ed interfaces any transitively `use`d interface is assumed to be an
-import unless it's explicitly listed as an export.
+For `export`ed interfaces, any transitively `use`d interface is assumed to be an
+import unless it's explicitly listed as an export. For example, here `w1` is
+equivalent to `w2`:
+```wit
+interface a {
+  resource r;
+}
+interface b {
+  use a.{r}; 
+  foo: func() -> r;
+}
+
+world w1 {
+  export b;
+}
+world w2 {
+  import a;
+  export b;
+}
+```
 
 > **Note**: It's planned in the future to have "power user syntax" to configure
 > this on a more fine-grained basis for exports, for example being able to
@@ -754,8 +753,32 @@ defined within each language as well.
 ## WIT Identifiers
 [identifiers]: #wit-identifiers
 
-Identifiers in WIT documents are required to be valid plain or interface
-names, as defined by the [component model text format](Explainer.md#import-and-export-definitions).
+Identifiers in WIT can be defined with two different forms. The first is the
+[kebab-case] [`label`](Explainer.md#import-and-export-names) production in the
+Component Model text format.
+
+```wit
+foo: func(bar: u32);
+
+red-green-blue: func(r: u32, g: u32, b: u32);
+
+resource XML { ... }
+parse-XML-document: func(s: string) -> XML;
+```
+
+This form can't lexically represent WIT keywords, so the second form is the
+same syntax with the same restrictions as the first, but prefixed with '%':
+
+```wit
+%foo: func(%bar: u32);
+
+%red-green-blue: func(%r: u32, %g: u32, %b: u32);
+
+// This form also supports identifiers that would otherwise be keywords.
+%variant: func(%enum: s32);
+```
+
+[kebab-case]: https://en.wikipedia.org/wiki/Letter_case#Kebab_case
 
 # Lexical structure
 [lexical-structure]: #lexical-structure
@@ -814,7 +837,7 @@ operator ::= '=' | ',' | ':' | ';' | '(' | ')' | '{' | '}' | '<' | '>' | '*' | '
 
 ### Keywords
 
-Certain identifiers are reserved for use in `wit` documents and cannot be used
+Certain identifiers are reserved for use in WIT documents and cannot be used
 bare as an identifier. These are used to help parse the format, and the list of
 keywords is still in flux at this time but the current set is:
 
@@ -860,7 +883,7 @@ wit-file ::= package-decl? (toplevel-use-item | interface-item | world-item)*
 ## Package declaration
 [package declaration]: #package-declaration
 
-WIT files optionally start with a package declaration which defines the ID of
+WIT files optionally start with a package declaration which defines the name of
 the package.
 
 ```ebnf
@@ -884,7 +907,7 @@ use-path ::= id
            | ( id ':' )+ id ( '/' id )+ ('@' valid-semver)? 🪺
 ```
 
-Here `use-path` is the ID used to refer to interfaces. The bare form `id`
+Here `use-path` is an [interface name]. The bare form `id`
 refers to interfaces defined within the current package, and the full form
 refers to interfaces in package dependencies.
 
@@ -895,6 +918,8 @@ As a future extension, WIT, components and component registries may allow
 nesting both namespaces and packages, which would then generalize the syntax of
 `use-path` as suggested by the 🪺 suffixed rule.
 
+[Interface Name]: Explainer.md#import-and-export-definitions
+
 ## Item: `world`
 
 Worlds define a [componenttype](https://github.com/WebAssembly/component-model/blob/main/design/mvp/Explainer.md#type-definitions) as a collection of imports and exports.
@@ -1302,33 +1327,6 @@ where `%[method]file.read` is the desugared name of a method according to the
 Component Model's definition of [`name`](Explainer.md).
 
 
-## Identifiers
-
-Identifiers in `wit` can be defined with two different forms. The first is a
-[kebab-case] [`label`](Explainer.md#import-and-export-names) production in the
-Component Model text format.
-
-```wit
-foo: func(bar: u32);
-
-red-green-blue: func(r: u32, g: u32, b: u32);
-```
-
-This form can't name identifiers which have the same name as wit keywords, so
-the second form is the same syntax with the same restrictions as the first, but
-prefixed with '%':
-
-```wit
-%foo: func(%bar: u32);
-
-%red-green-blue: func(%r: u32, %g: u32, %b: u32);
-
-// This form also supports identifiers that would otherwise be keywords.
-%variant: func(%enum: s32);
-```
-
-[kebab-case]: https://en.wikipedia.org/wiki/Letter_case#Kebab_case
-
 ## Name resolution
 
 A `wit` document is resolved after parsing to ensure that all names resolve
@@ -1447,7 +1445,7 @@ This example illustrates the basic structure of interfaces:
 * Each top-level WIT definition (in this example: `types` and `namespace`)
   turns into a type export of the same kebab-name.
 * Each WIT interface is mapped to a component-type that exports an
-  instance with a fully-qualified interface name (in this example:
+  instance with a fully-qualified [interface name]  (in this example:
   `local:demo/types` and `local:demo/namespace`). Note that this nested
   scheme allows a single component to both define and implement a WIT interface
   without name conflict.
diff --git a/design/mvp/canonical-abi/definitions.py b/design/mvp/canonical-abi/definitions.py
index 97ae9115..62145e2e 100644
--- a/design/mvp/canonical-abi/definitions.py
+++ b/design/mvp/canonical-abi/definitions.py
@@ -220,9 +220,9 @@ def alignment_flags(labels):
   if n <= 16: return 2
   return 4
 
-### Size
+### Element Size
 
-def size(t):
+def elem_size(t):
   match despecialize(t):
     case Bool()             : return 1
     case S8() | U8()        : return 1
@@ -233,33 +233,33 @@ def size(t):
     case F64()              : return 8
     case Char()             : return 4
     case String() | List(_) : return 8
-    case Record(fields)     : return size_record(fields)
-    case Variant(cases)     : return size_variant(cases)
-    case Flags(labels)      : return size_flags(labels)
+    case Record(fields)     : return elem_size_record(fields)
+    case Variant(cases)     : return elem_size_variant(cases)
+    case Flags(labels)      : return elem_size_flags(labels)
     case Own(_) | Borrow(_) : return 4
 
-def size_record(fields):
+def elem_size_record(fields):
   s = 0
   for f in fields:
     s = align_to(s, alignment(f.t))
-    s += size(f.t)
+    s += elem_size(f.t)
   assert(s > 0)
   return align_to(s, alignment_record(fields))
 
 def align_to(ptr, alignment):
   return math.ceil(ptr / alignment) * alignment
 
-def size_variant(cases):
-  s = size(discriminant_type(cases))
+def elem_size_variant(cases):
+  s = elem_size(discriminant_type(cases))
   s = align_to(s, max_case_alignment(cases))
   cs = 0
   for c in cases:
     if c.t is not None:
-      cs = max(cs, size(c.t))
+      cs = max(cs, elem_size(c.t))
   s += cs
   return align_to(s, alignment_variant(cases))
 
-def size_flags(labels):
+def elem_size_flags(labels):
   n = len(labels)
   assert(n > 0)
   if n <= 8: return 1
@@ -382,7 +382,7 @@ def __init__(self, rep, own, scope = None):
 
 def load(cx, ptr, t):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : return convert_int_to_bool(load_int(cx, ptr, 1))
     case U8()           : return load_int(cx, ptr, 1)
@@ -440,6 +440,7 @@ def core_f64_reinterpret_i64(i):
   return struct.unpack('<d', struct.pack('<Q', i))[0] # f64.reinterpret_i64
 
 def convert_i32_to_char(cx, i):
+  assert(i >= 0)
   trap_if(i >= 0x110000)
   trap_if(0xD800 <= i <= 0xDFFF)
   return chr(i)
@@ -486,10 +487,10 @@ def load_list(cx, ptr, elem_type):
 
 def load_list_from_range(cx, ptr, length, elem_type):
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
-  trap_if(ptr + length * size(elem_type) > len(cx.opts.memory))
+  trap_if(ptr + length * elem_size(elem_type) > len(cx.opts.memory))
   a = []
   for i in range(length):
-    a.append(load(cx, ptr + i * size(elem_type), elem_type))
+    a.append(load(cx, ptr + i * elem_size(elem_type), elem_type))
   return a
 
 def load_record(cx, ptr, fields):
@@ -497,11 +498,11 @@ def load_record(cx, ptr, fields):
   for field in fields:
     ptr = align_to(ptr, alignment(field.t))
     record[field.label] = load(cx, ptr, field.t)
-    ptr += size(field.t)
+    ptr += elem_size(field.t)
   return record
 
 def load_variant(cx, ptr, cases):
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   case_index = load_int(cx, ptr, disc_size)
   ptr += disc_size
   trap_if(case_index >= len(cases))
@@ -527,7 +528,7 @@ def find_case(label, cases):
   return -1
 
 def load_flags(cx, ptr, labels):
-  i = load_int(cx, ptr, size_flags(labels))
+  i = load_int(cx, ptr, elem_size_flags(labels))
   return unpack_flags_from_int(i, labels)
 
 def unpack_flags_from_int(i, labels):
@@ -553,7 +554,7 @@ def lift_borrow(cx, i, t):
 
 def store(cx, v, t, ptr):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : store_int(cx, int(bool(v)), ptr, 1)
     case U8()           : store_int(cx, v, ptr, 1)
@@ -769,24 +770,24 @@ def store_list(cx, v, ptr, elem_type):
   store_int(cx, length, ptr + 4, 4)
 
 def store_list_into_range(cx, v, elem_type):
-  byte_length = len(v) * size(elem_type)
+  byte_length = len(v) * elem_size(elem_type)
   trap_if(byte_length >= (1 << 32))
   ptr = cx.opts.realloc(0, 0, alignment(elem_type), byte_length)
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
   trap_if(ptr + byte_length > len(cx.opts.memory))
   for i,e in enumerate(v):
-    store(cx, e, elem_type, ptr + i * size(elem_type))
+    store(cx, e, elem_type, ptr + i * elem_size(elem_type))
   return (ptr, len(v))
 
 def store_record(cx, v, ptr, fields):
   for f in fields:
     ptr = align_to(ptr, alignment(f.t))
     store(cx, v[f.label], f.t, ptr)
-    ptr += size(f.t)
+    ptr += elem_size(f.t)
 
 def store_variant(cx, v, ptr, cases):
   case_index, case_value = match_case(v, cases)
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   store_int(cx, case_index, ptr, disc_size)
   ptr += disc_size
   ptr = align_to(ptr, max_case_alignment(cases))
@@ -805,7 +806,7 @@ def match_case(v, cases):
 
 def store_flags(cx, v, ptr, labels):
   i = pack_flags_into_int(v, labels)
-  store_int(cx, i, ptr, size_flags(labels))
+  store_int(cx, i, ptr, elem_size_flags(labels))
 
 def pack_flags_into_int(v, labels):
   i = 0
@@ -969,7 +970,7 @@ def next(self, want):
         case ('i64', 'i32') : return wrap_i64_to_i32(x)
         case ('i64', 'f32') : return decode_i32_as_float(wrap_i64_to_i32(x))
         case ('i64', 'f64') : return decode_i64_as_float(x)
-        case _              : return x
+        case _              : assert(have == want); return x
   c = cases[case_index]
   if c.t is None:
     v = None
@@ -1050,7 +1051,7 @@ def lower_flat_variant(cx, v, cases):
         case ('i32', 'i64') : payload[i] = fv
         case ('f32', 'i64') : payload[i] = encode_float_as_i32(fv)
         case ('f64', 'i64') : payload[i] = encode_float_as_i64(fv)
-        case _              : pass
+        case _              : assert(have == want)
   for _ in flat_types:
     payload.append(0)
   return [case_index] + payload
@@ -1072,7 +1073,7 @@ def lift_values(cx, max_flat, vi, ts):
     ptr = vi.next('i32')
     tuple_type = Tuple(ts)
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     return list(load(cx, ptr, tuple_type).values())
   else:
     return [ lift_flat(cx, vi, t) for t in ts ]
@@ -1083,11 +1084,11 @@ def lower_values(cx, max_flat, vs, ts, out_param = None):
     tuple_type = Tuple(ts)
     tuple_value = {str(i): v for i,v in enumerate(vs)}
     if out_param is None:
-      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), size(tuple_type))
+      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), elem_size(tuple_type))
     else:
       ptr = out_param.next('i32')
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     store(cx, tuple_value, tuple_type, ptr)
     return [ptr]
   else: