Add support for mutually recursive types with type parameters

elab.ml

@@ -122,6 +122,27 @@ and paths_row ta ps = function
     ts1 @ ts2
 
 
+let rec_from_extyp typ label s =
+  match s with
+  | ExT([], t) ->
+    let rec find_rec = function
+      | AppT(t, ts) ->
+        let rec_t, unroll_t, roll_t, ak = find_rec t in
+        rec_t, AppT(unroll_t, ts), AppT(roll_t, ts), ak
+      | RecT(ak, unroll_t) as rec_t ->
+        rec_t, unroll_t, rec_t, ak
+      | DotT(t, lab) ->
+        let rec_t, unroll_t, roll_t, ak = find_rec t in
+        rec_t, DotT(unroll_t, lab), DotT(roll_t, lab), ak
+      | _ ->
+        error typ.at ("non-recursive type for " ^ label ^ ":"
+                      ^ " " ^ Types.string_of_extyp s) in
+    find_rec t
+  | _ ->
+    error typ.at ("non-recursive type for " ^ label ^ ":"
+                  ^ " " ^ Types.string_of_extyp s)
+
+
 (* Instantiation *)
 
 let rec instantiate env t e =
@@ -386,15 +407,18 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
 
   | EL.RollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let t, ak, t' =
-      match s with
-      | ExT([], (RecT(ak, t') as t)) -> t, ak, t'
-      | _ -> error typ.at "non-recursive type for rolling" in
+    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "rolling" s in
+    let var_t = lookup_var env var in
+    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
     let _, zs2, f =
-      try sub_typ env (lookup_var env var) (subst_typ (subst [ak] [t]) t') []
-      with Sub e -> error var.at ("rolled value does not match annotation") in
-    ExT([], t), Pure, zs1 @ zs2,
-    IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ t)
+      try sub_typ env var_t unroll_t []
+      with Sub e ->
+        error var.at ("rolled value does not match annotation:"
+                      ^ " " ^ Types.string_of_typ var_t ^ " "
+                      ^ "<"
+                      ^ " " ^ Types.string_of_typ unroll_t) in
+    ExT([], roll_t), Pure, zs1 @ zs2,
+    IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ roll_t)
 
   | EL.IfE(var, exp1, exp2, typ) ->
     let t0, zs0, ex = elab_instvar env var in
@@ -489,13 +513,15 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
 
   | EL.UnrollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let t, ak, t' =
-      match s with
-      | ExT([], (RecT(ak, t') as t)) -> t, ak, t'
-      | _ -> error typ.at "non-recursive type for rolling" in
-    let _, zs2, f = try sub_typ env (lookup_var env var) t [] with Sub e ->
-      error var.at ("unrolled value does not match annotation") in
-    ExT([], subst_typ (subst [ak] [t]) t'), Pure, zs1 @ zs2,
+    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "unrolling" s in
+    let var_t = lookup_var env var in
+    let _, zs2, f = try sub_typ env var_t roll_t [] with Sub e ->
+      error var.at ("unrolled value does not match annotation:"
+                    ^ "  " ^ Types.string_of_typ var_t ^ " "
+                    ^ "<"
+                    ^ "  " ^ Types.string_of_typ roll_t) in
+    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
+    ExT([], unroll_t), Pure, zs1 @ zs2,
     IL.UnrollE(IL.AppE(f, IL.VarE(var.it)))
 
   | EL.RecE(var, typ, exp1) ->

regression.1ml

@@ -35,3 +35,117 @@ type_error {
   Impure : () => {type t; existentials: t} = fun () =>
     {type t = bool; existentials = true} :> {type t = bool; existentials: t};
 };
+
+;;
+
+Mutually = {
+  T = rec (R: {
+    Even: {type t _};
+    Odd: {type t _};
+  }) => {
+    Even = {
+      type t x = {head: x; tail: R.Odd.t x};
+    };
+    Odd = {
+      type t x = opt (R.Even.t x);
+    };
+  };
+
+  V = rec (R: {
+    Even: {
+      make 'x: x => T.Odd.t x => T.Even.t x;
+      size 'x: T.Even.t x -> int;
+    };
+    Odd: {
+      make 'x: opt (T.Even.t x) => T.Odd.t x;
+      size 'x: T.Odd.t x -> int;
+    };
+  }) => {
+    Even = {
+      make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x =
+        @(T.Even.t x) {head; tail};
+      size 'x (v: T.Even.t x) = 1 + R.Odd.size v.@(T.Even.t _).tail;
+    };
+    Odd = {
+      make 'x (v: opt (T.Even.t x)) : T.Odd.t x = @(T.Odd.t x) v;
+      size 'x (v: T.Odd.t x) =
+        caseopt v.@(T.Odd.t x)
+          (fun () => 0)
+          (fun e => R.Even.size e);
+    };
+  };
+};
+
+Mutually = {
+  Even = {...Mutually.T.Even; ...Mutually.V.Even};
+  Odd = {...Mutually.T.Odd; ...Mutually.V.Odd};
+
+  one = Odd.size (Odd.make (some (Even.make true (Odd.make none))));
+};
+
+;;
+
+Hungry = {
+  type eat a = rec eat_a => a -> eat_a;
+
+  eater 'a: eat a = rec (eater: eat a) => @(eat a) (fun a => eater);
+
+  (<+) eater x = eater.@(eat _) x;
+
+  do eater <+ 1 <+ 2;
+};
+
+PolyRec = {
+  type l a = rec (type t) => alt a t;
+  ...rec {type t a} => {type t a = alt a (t (type (a, a)))};
+
+  t_int = t int;
+
+  hmm (x: t int) = casealt (x.@(t int));
+
+  t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
+};
+
+N :> {
+  type Z;
+  type S _;
+} = {
+  type Z   = {};
+  type S _ = {};
+};
+
+ListN = let
+  type I (type x) (type p _) (type t _ _) = {
+    nil     :               p N.Z;
+    (::) 'n : x -> t x n -> p (N.S n);
+  };
+  type T x n (type t _ _) = (type p _) => I x p t -> p n;
+in {
+  ...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;
+
+  local
+    mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
+  in
+    nil  'x                       = mk (fun (type p _) (r: I x p t) => r.nil);
+    (::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs);
+  end;
+} :> {
+  type t _ _;
+
+  case 'x 'n: (type p _) => I x p t => t x n -> p n;
+
+  nil  'x    :               t x N.Z;
+  (::) 'x 'n : x => t x n => t x (N.S n);
+};
+
+ListN = {
+  ...ListN;
+  map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
+    case (t y) {
+      nil = nil;
+      (::) x xs = xy x :: map xs;
+    };
+};

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
@@ -176,6 +180,17 @@ let rec sub_typ env t1 t2 ps =
         raise (Sub (Mismatch(t1, t2))) in
       [], zs, e1
 
+    | LamT(aks1, t1'), LamT(aks2, t2') ->
+      if List.length aks1 <> List.length aks2 ||
+         List.exists2 (fun ak1 ak2 -> snd ak1 <> snd ak2) aks1 aks2 then
+        raise (Sub (Mismatch(t1, t2)));
+      let zs = try
+          equal_typ (add_typs aks2 env)
+            (subst_typ (subst aks1 (varTs aks2)) t1') t2'
+        with Sub e ->
+          raise (Sub (Mismatch(t1, t2)))
+      in [], lift env zs, e1
+
     | RecT(ak1, t1'), RecT(ak2, t2') ->
       if snd ak1 <> snd ak2 then
         raise (Sub (Mismatch(t1, t2)));
@@ -309,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