Require matching finality

interpreter/valid/valid.ml

@@ -195,22 +195,26 @@ let check_desctype_sub (c : context) (dt : desctype) (dt' : desctype) x x' at =
 let check_descriptors (dts : deftype list) at =
   List.iter (fun dt ->
     let DefT ((RecT dts), x) = dt in
-    let SubT (_, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in
+    let SubT (fin, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in
     Option.iter (fun ut ->
       match ut with
       | Rec x' ->
-        let SubT (_, _, DescT (_, ut', _)) = Lib.List32.nth dts x' in
+        let SubT (fin', _, DescT (_, ut', _)) = Lib.List32.nth dts x' in
         require (ut' = Some (Rec x)) at
             "described type is not described by descriptor";
-        require (x' < x) at "forward use of described type"
+        require (x' < x) at "forward use of described type";
+        require (fin = fin') at
+            "descriptor and described types have mismatched finality"
       | _ -> error at "described type is outside rec group"
     ) ut1;
     Option.iter (fun ut ->
       match ut with
       | Rec x' ->
-        let SubT (_, _, DescT (ut', _, _)) = Lib.List32.nth dts x' in
+        let SubT (fin', _, DescT (ut', _, _)) = Lib.List32.nth dts x' in
         require (ut' = Some (Rec x)) at
             "type is not described by its descriptor";
+        require (fin = fin') at
+            "descriptor and described types have mismatched finality"
       | _ -> error at "descriptor type is outside rec group"
     ) ut2
   ) dts

proposals/custom-descriptors/Overview.md

@@ -124,6 +124,29 @@ This is the same strategy we use for ensuring supertype chains do not have cycle
 )
 ```
 
+Descriptor and described types must also have matching finality,
+i.e. both must be final or both must be open (non-final).
+If a described type were final and its descriptor open,
+the descriptor could never have any subtypes because those subtypes would have to describe
+subtypes of the described type, which cannot exist.
+Conversely, if a described type were open and its descriptor final,
+the described type could never have any subtypes because those subtypes would have to have
+descriptors that are subtypes of the descriptor, which cannot exist.
+
+```wasm
+(rec
+  ;; Invalid: $a is final, but $b is open.
+  (type $a (sub final (descriptor $b) (struct)))
+  (type $b (sub (describes $a) (struct)))
+)
+
+(rec
+  ;; Invalid: $x is open, but $y is final.
+  (type $x (sub (descriptor $y) (struct)))
+  (type $y (sub final (describes $x) (struct)))
+)
+```
+
 Just like any other struct types,
 struct types with `describes` or `descriptor` clauses support width and depth subtyping.
 However, the following new subtyping rules are introduced:
@@ -142,6 +165,9 @@ However, the following new subtyping rules are introduced:
  - A declared supertype of a type without a `describes` clause must also
    not have a `describes` clause.
 
+ - A described type and its descriptor type must have matching finality,
+   i.e. both must be final or both must be open (non-final).
+
  - With shared-everything-threads,
    a shared described type must have a shared descriptor type and vice versa,
    and an unshared described type must have an unshared descriptor type and vice versa.

test/core/custom-descriptors/descriptors.wast

@@ -32,17 +32,6 @@
   )
 )
 
-;; Descriptor and described types can have mismatched finality.
-(module
-  (rec
-    (type $a (sub final (descriptor $b) (struct)))
-    (type $b (sub (describes $a) (struct)))
-  )
-  (rec
-    (type $x (sub (descriptor $y) (struct)))
-    (type $y (sub final (describes $x) (struct)))
-  )
-)
 
 ;; Describes clause must precede descriptor clause.
 (assert_malformed
@@ -231,6 +220,44 @@
   "descriptor type must be a struct"
 )
 
+;; Descriptor and described types must have matching finality.
+(assert_invalid
+  (module
+    (rec
+      (type $a (sub final (descriptor $b) (struct)))
+      (type $b (sub (describes $a) (struct)))
+    )
+  )
+  "descriptor and described types have mismatched finality"
+)
+(assert_invalid
+  (module
+    (rec
+      (type $x (sub (descriptor $y) (struct)))
+      (type $y (sub final (describes $x) (struct)))
+    )
+  )
+  "descriptor and described types have mismatched finality"
+)
+(assert_invalid
+  (module
+    (rec
+      (type $a (descriptor $b) (struct))
+      (type $b (sub (describes $a) (struct)))
+    )
+  )
+  "descriptor and described types have mismatched finality"
+)
+(assert_invalid
+  (module
+    (rec
+      (type $x (sub (descriptor $y) (struct)))
+      (type $y (describes $x) (struct))
+    )
+  )
+  "descriptor and described types have mismatched finality"
+)
+
 ;; Subtyping
 
 (module
@@ -533,7 +560,7 @@
     (rec
       (type $A (sub (struct (field i32))))
       (type $B (sub $A (descriptor $B.desc) (struct (field i64))))
-      (type $B.desc (describes $B) (struct))
+      (type $B.desc (sub (describes $B) (struct)))
     )
   )
   "sub type 1 does not match super type 0"
@@ -545,7 +572,7 @@
     )
     (rec
       (type $B (sub $A (descriptor $B.desc) (struct (field i64))))
-      (type $B.desc (describes $B) (struct))
+      (type $B.desc (sub (describes $B) (struct)))
     )
   )
   "sub type 1 does not match super type 0"