Fix continuation subtyping

dhil · Jul 31, 2024 · b5d5ae2 · b5d5ae2
1 parent fe20aaf
commit b5d5ae2
Showing 1 changed file with 6 additions and 11 deletions.
diff --git a/interpreter/valid/valid.ml b/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