From 07b1f8a6b4fabf2f9bd88ece2e0a045670dd11c3 Mon Sep 17 00:00:00 2001
From: Luke Wagner <mail@lukewagner.name>
Date: Thu, 21 Sep 2023 15:50:49 -0500
Subject: [PATCH] Always require type exports to ascribe a type

---
 design/mvp/Binary.md    |  8 +++++---
 design/mvp/Explainer.md | 42 ++++++++++++-----------------------------
 2 files changed, 17 insertions(+), 33 deletions(-)

diff --git a/design/mvp/Binary.md b/design/mvp/Binary.md
index b98fe987..ec98967f 100644
--- a/design/mvp/Binary.md
+++ b/design/mvp/Binary.md
@@ -347,9 +347,11 @@ Notes:
 * Validation requires that all resource types transitively used in the type of an
   export are introduced by a preceding `importdecl` or `exportdecl`.
 * Validation requires any exported `sortidx` to have a valid `externdesc`
-  (which disallows core sorts other than `core module`). When the optional
-  `externdesc` immediate is present, validation requires it to be a supertype
-  of the inferred `externdesc` of the `sortidx`.
+  (which disallows core sorts other than `core module`).
+* When an export's optional `externdesc` immediate is present, validation
+  requires it to be a supertype of the inferred `externdesc` of the `sortidx`.
+* Resource type exports must have an explicit ascribed `externdesc` (indicating
+  `(sub resource)` or `(eq <typeidx>)`).
 * The `name` fields of `exportname` and `importname` must be unique among all
   imports and exports in the containing component definition, component type or
   instance type. (An import and export cannot use the same `name`.)
diff --git a/design/mvp/Explainer.md b/design/mvp/Explainer.md
index 95bbf22d..b6567806 100644
--- a/design/mvp/Explainer.md
+++ b/design/mvp/Explainer.md
@@ -931,46 +931,28 @@ bind a fresh abstract type. For example, in the following component:
 all four types aliases in the outer component are unequal, reflecting the fact
 that each instance of `$C` generates two fresh resource types.
 
-If a single resource type definition is exported more than once, the exports
-after the first are equality-bound to the first export. For example, the
-following component:
+When a component exports a type, the component must explicitly specify how the
+type should appear to the outside world by explicitly ascribing a `typebound`.
+For example, in the following component:
 ```wasm
 (component
   (type $r (resource (rep i32)))
-  (export "r1" (type $r))
-  (export "r2" (type $r))
+  (export $r1 "r1" (type $r) (type (sub resource)))
+  (export     "r2" (type $r) (type (eq $r1)))
+  (export     "r3" (type $r) (type (sub resource)))
 )
 ```
-is assigned the following `componenttype`:
+the inferred `componenttype` is:
 ```wasm
 (component
   (export $r1 "r1" (type (sub resource)))
-  (export "r2" (type (eq $r1)))
-)
-```
-Thus, from an external perspective, `r1` and `r2` are two labels for the same
-type.
-
-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.
-```wasm
-(component
-  (type $r (resource (rep i32)))
-  (export "r1" (type $r)
-  (export "r2" (type $r) (type (sub resource)))
-)
-```
-This component is assigned the following `componenttype`:
-```wasm
-(component
-  (export "r1" (type (sub resource)))
-  (export "r2" (type (sub resource)))
+  (export     "r2" (type (eq $r1)))
+  (export     "r3" (type (sub resource)))
 )
 ```
-The assignment of this type to the above component mirrors the *introduction*
+This type exposes to clients of this component only that `r1` and `r2` are
+equal even though all three exports are of the same internal type definition.
+The assignment of these types to the above component mirrors the *introduction*
 rule of [existential types]  (∃T).
 
 When supplying a resource type (imported *or* defined) to a type import via