Fix continuation subtyping (#38)

This patch fixes the continuation subtyping issue. Resolves #35.

Author: dhil

interpreter/valid/valid.ml

@@ -114,10 +114,6 @@ let func_type_of_tag_type (c : context) (TagT dt) at : func_type =
   | DefFuncT ft -> ft
   | _ -> error at "non-function type"
 
-let heap_type_of_str_type (_c : context) (st : str_type) : heap_type =
-  DefHT (DefT (RecT [SubT (Final, [], st)], Int32.of_int 0))
-
-
 (* Types *)
 
 let check_limits {min; max} range at msg =
@@ -600,9 +596,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (ts1 @ [NumT I32T]) -->... [], []
 
   | ContNew x ->
-    let ct = cont_type c x in
-    let ft = func_type_of_cont_type c ct x.at in
-    [RefT (Null, heap_type_of_str_type c (DefFuncT ft))] -->
+    let ContT ht = cont_type c x in
+    [RefT (Null, ht)] -->
     [RefT (NoNull, DefHT (type_ c x))], []
 
   | ContBind (x, y) ->
@@ -615,8 +610,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     let ts11, ts12 = Lib.List.split (List.length ts1 - List.length ts1') ts1 in
     require (match_func_type c.types (FuncT (ts12, ts2)) ft') e.at
       "type mismatch in continuation types";
-    (ts11 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) -->
-      [RefT (NoNull, heap_type_of_str_type c (DefContT ct'))], []
+    (ts11 @ [RefT (Null, VarHT (StatX x.it))]) -->
+      [RefT (NoNull, VarHT (StatX y.it))], []
 
   | Suspend x ->
     let tag = tag c x in
@@ -627,15 +622,15 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     let ct = cont_type c x in
     let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in
     check_resume_table c ts2 xys e.at;
-    (ts1 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) --> ts2, []
+    (ts1 @ [RefT (Null, VarHT (StatX x.it))]) --> ts2, []
 
   | ResumeThrow (x, y, xys) ->
     let ct = cont_type c x in
     let FuncT (ts1, ts2) = func_type_of_cont_type c ct x.at in
     let tag = tag c y in
     let FuncT (ts0, _) = func_type_of_tag_type c tag y.at in
     check_resume_table c ts2 xys e.at;
-    (ts0 @ [RefT (Null, heap_type_of_str_type c (DefContT ct))]) --> ts2, []
+    (ts0 @ [RefT (Null, VarHT (StatX x.it))]) --> ts2, []
 
   | Barrier (bt, es) ->
     let InstrT (ts1, ts2, xs) as ft = check_block_type c bt e.at in

test/core/cont.wast

@@ -638,3 +638,19 @@
   (i32.const 0) (i32.const 1) (i32.const 2) (i32.const 3)
   (i32.const 4) (i32.const 5) (i32.const 6)
 )
+
+;; Subtyping
+(module
+  (type $ft1 (func (param i32)))
+  (type $ct1 (sub (cont $ft1)))
+
+  (type $ft0 (func))
+  (type $ct0 (sub (cont $ft0)))
+
+  (func $test (param $x (ref $ct1))
+    (i32.const 123)
+    (local.get $x)
+    (cont.bind $ct1 $ct0)
+    (drop)
+  )
+)