Subtyping of recursive types inside modules

regression.1ml

@@ -97,7 +97,7 @@ Hungry = {
 
 PolyRec = {
   type l a = rec (type t) => alt a t;
-  t = rec (type t a) => fun (type a) => alt a (t (type (a, a)));
+  ...rec {type t a} => {type t a = alt a (t (type (a, a)))};
 
   t_int = t int;
 
@@ -121,7 +121,7 @@ ListN = let
   };
   type T x n (type t _ _) = (type p _) => I x p t -> p n;
 in {
-  t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
+  ...rec {type t _ _} => {type t x n = wrap T x n t};
 
   case 'x 'n (type p _) (cs: I x p t) e =
     (unwrap e.@(t _ _): wrap T x n t) p cs;

sub.ml

@@ -141,6 +141,10 @@ let rec sub_typ env t1 t2 ps =
       ts, zs,
       IL.TupE(List.map2 (fun (l, _) f -> l, IL.AppE(f, IL.DotE(e1, l))) tr2 fs)
 
+    | TupT(tr1), TupT(tr2) ->
+      let zs = equal_row env tr1 tr2 ps in
+      [], zs, e1
+
     | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) ->
       if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2)));
       let env' = add_typs aks2 env in
@@ -320,3 +324,10 @@ and equal_extyp env s1 s2 =
   let _, zs2, _ =
     try sub_extyp env s2 s1 [] with Sub e -> raise (Sub (Right e)) in
   zs1 @ zs2
+
+and equal_row env tr1 tr2 ps =
+  let _, zs1, _ =
+    try sub_row env tr1 tr2 ps with Sub e -> raise (Sub (Left e)) in
+  let _, zs2, _ =
+    try sub_row env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in
+  zs1 @ zs2