Add recursively dependent signatures

elab.ml

@@ -585,30 +585,52 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
       IL.RecE(var.it, erase_typ t2, e)
     | _ ->
       let t2, zs2 = elab_pathexp env1 exp1 l in
+      let recT () =
 Trace.debug (lazy ("[RecT] s1 = " ^ string_of_norm_extyp s1));
 Trace.debug (lazy ("[RecT] t2 = " ^ string_of_norm_typ t2));
-      let vts1 = varTs aks1 in
-      let ts, zs3, e =
-        try sub_typ env1 t2 t1 vts1 with Sub e -> error typ.at
-          ("recursive type does not match annotation: " ^ Sub.string_of_error e)
-      in
-      ts
-       |> List.iter (fun t ->
-          let t = norm_typ t in
-          if List.exists (fun t' -> t' = t) vts1 then
-            error typ.at "illegal recursive type alias");
+        let vts1 = varTs aks1 in
+        let ts, zs3, e =
+          try sub_typ env1 t2 t1 vts1 with Sub e -> error typ.at
+            ("recursive type does not match annotation: " ^ Sub.string_of_error e)
+        in
+        ts
+         |> List.iter (fun t ->
+            let t = norm_typ t in
+            if List.exists (fun t' -> t' = t) vts1 then
+              error typ.at "illegal recursive type alias");
 Trace.debug (lazy ("[RecT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
-      let t3, k3 = try make_rec_typ t1 with Recursive ->
-        error typ.at "illegal type for recursive expression" in
-      let a = freshen_var env var.it in
-      let tas1 = paths_typ (VarT(a, k3)) (varTs aks1) t1 in
-      let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst aks1 ts) t3) in
-      let t4 = RecT((a, k3), t3') in
+        let t3, k3 = try make_rec_typ t1 with Recursive ->
+          error typ.at "illegal type for recursive expression" in
+        let a = freshen_var env var.it in
+        let tas1 = paths_typ (VarT(a, k3)) (varTs aks1) t1 in
+        let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst aks1 ts) t3) in
+        let t4 = RecT((a, k3), t3') in
 Trace.debug (lazy ("[RecT] t4 = " ^ string_of_norm_typ t4));
-      let t = subst_typ (subst aks1 (List.map (subst_typ [a, t4]) tas1)) t1 in
+        let t = subst_typ (subst aks1 (List.map (subst_typ [a, t4]) tas1)) t1 in
 Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
-      ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
-      IL.LetE(e, "_", materialize_typ t)
+        ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
+        IL.LetE(e, "_", materialize_typ t) in
+      let depT aks2 t2 =
+        let ts, zs3, e =
+          try sub_typ env1 t2 t1 (varTs aks1) with Sub e -> error typ.at
+            ("recursive type does not match annotation: " ^ Sub.string_of_error e)
+        in
+        let aks = aks1 @ aks2 in
+        let aks' = freshen_vars env aks in
+        let t3 = subst_typ (subst aks (varTs aks')) t2 in
+        let t3' = TypT(ExT(aks', t3)) in
+        ExT([], t3'), Pure, lift_warn typ.at t3 env (zs1 @ zs2 @ zs3),
+        IL.LetE(e, "_", materialize_typ t3') in
+      (match t1 with
+      | TypT(_) -> recT ()
+      | StrT(_) ->
+        (match t2 with
+        | TypT(ExT(aks2, t2)) -> depT aks2 t2
+        | _ -> recT ()
+        )
+      | _ ->
+        error typ.at "pattern does not denote a type"
+      )
     )
   | EL.ImportE(path) ->
     (match Import.resolve (Source.at_file path) path.it with

regression.1ml

@@ -33,6 +33,30 @@ type DEC_PUNNING = {int, list}
 
 ;;
 
+type RDS = rec (R: let type T'1 = {type t _} in {A: T'1, B: T'1}) => let
+  type ONE (type this _) (type that _) = {
+    t = this
+    aThis 'a: this a
+    ofThat 'a: that a -> this a
+  }
+in {
+  A: ONE R.A.t R.B.t
+  B: ONE R.B.t R.A.t
+}
+
+Rds :> RDS = let
+  One = {
+    type t _ = ()
+    aThis = ()
+    ofThat _ = ()
+  }
+in {
+  A = One
+  B = One
+}
+
+;;
+
 Equivalence: {
   type t a b
 
@@ -230,7 +254,21 @@ Kaboom = rec (R: rec R => {kaboom: () ~> R}) : (= R) => {kaboom () = R}
 
 ;;
 
-Mutually = let
+Mutually :> rec (R: {
+  Even: {type t _}
+  Odd: {type t _}
+}) => {
+  Even: {
+    t = R.Even.t
+    make 'x: x -> R.Odd.t x -> R.Even.t x
+    size 'x: R.Even.t x ~> int
+  }
+  Odd: {
+    t = R.Odd.t
+    make 'x: opt (R.Even.t x) -> R.Odd.t x
+    size 'x: R.Odd.t x ~> int
+  }
+} = let
   T = rec (R: {
     Even: {type t _}
     Odd: {type t _}
@@ -290,9 +328,9 @@ type (a `>>` b) c = c
 
 ;;
 
-AnnotRecType = {
-  t = type rec (type t x) : type -> type => fun x => (x, t x)
-}
+;;AnnotRecType = {
+;;  t = type rec (type t x) : type -> type => fun x => (x, t x)
+;;}
 
 Hungry = {
   type eat a = rec eat_a => a ~> eat_a

sub.ml

@@ -157,6 +157,24 @@ let extract_bind oneway env tr1 l t2 =
     | None -> raise (Sub (Struct(l, Missing)))
     | Some (t, zs, e) -> t, zs, fun f _ _ -> IL.AppE(f, e)
 
+let rec has_typs_typ ps = function
+  | StrT(tr) -> List.exists (fun (_, t) -> has_typs_typ ps t) tr
+  | FunT(aks, td, ExT(_, tr), e) ->
+    (match e with
+     | Implicit | Explicit Pure ->
+       has_typs_typ (List.map (fun p -> AppT(p, varTs aks)) ps) tr
+     | Explicit Impure -> false)
+  | TypT(ExT(_, p)) -> List.mem p ps
+  | VarT(_)
+  | PrimT(_)
+  | WrapT(_)
+  | LamT(_)
+  | AppT(_)
+  | TupT(_)
+  | DotT(_)
+  | RecT(_)
+  | InferT(_) -> false
+
 let resolve_typ z t =
   Trace.sub (lazy ("[resolve_typ] z = " ^ string_of_norm_typ (InferT(z))));
   Trace.sub (lazy ("[resolve_typ] t = " ^ string_of_norm_typ t));
@@ -179,6 +197,24 @@ let rec sub_typ oneway env t1 t2 ps =
   Trace.sub (lazy ("[sub_typ] t2 = " ^ string_of_norm_typ t2));
   Trace.sub (lazy ("[sub_typ] ps = " ^
     String.concat ", " (List.map string_of_norm_typ ps)));
+  let ts', zs', t2, ps =
+    if ps <> [] then
+      let su, zs' = match_typ oneway env t1 t2 ps in
+      Trace.sub (lazy ("[sub_typ] su = " ^
+        String.concat ", " (List.map (fun (p, t) -> Printf.sprintf "[= %s] - [= %s]\n" (string_of_typ p) (string_of_typ t)) su)));
+      let t2 = subst_typ (List.map (fun (p, t) -> psubst p t) su) t2 in
+      let ps' = List.filter (fun p -> List.mem_assoc p su) ps in
+      let ts' = List.map (fun p -> List.assoc p su) ps' in
+      let ps = List.filter (fun p -> not (List.mem_assoc p su)) ps in
+      if ps <> [] then begin
+        Trace.sub (lazy ("[sub_typ] unmatched ps = " ^
+          String.concat ", " (List.map string_of_norm_typ ps)));
+        raise Not_found
+      end;
+      ts', zs', t2, ps
+    else
+      [], [], t2, ps
+  in
   let e1 = IL.VarE("x") in
   let t1' = norm_typ t1 in
   let t2' = freshen_typ env (norm_typ t2) in
@@ -363,7 +399,7 @@ let rec sub_typ oneway env t1 t2 ps =
   Trace.sub (lazy ("[sub_typ] done ts = " ^
     String.concat ", " (List.map string_of_norm_typ ts)));
   Trace.sub (lazy ("[sub_typ] done x -> " ^ IL.string_of_exp e));
-  ts, zs, IL.LamE("x", erase_typ t1, e)
+  ts' @ ts, zs' @ zs, IL.LamE("x", erase_typ t1, e)
 
 and sub_extyp oneway env s1 s2 ps =
   Trace.sub (lazy ("[sub_extyp] s1 = " ^ string_of_norm_extyp s1));
@@ -423,5 +459,81 @@ and equal_row env tr1 tr2 ps =
     try sub_row false env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in
   zs1 @ zs2
 
+and match_typ oneway env t1 t2 ps =
+  let lift = lift (level ()) t1 in
+  let t2 = norm_typ t2 in
+  Trace.sub (lazy ("[match_typ] t1 = " ^ string_of_norm_typ t1));
+  Trace.sub (lazy ("[match_typ] t2 = " ^ string_of_typ t2));
+  Trace.sub (lazy ("[match_typ] ps = " ^
+    String.concat ", " (List.map string_of_norm_typ ps)));
+  if not (has_typs_typ ps t2) then [], [] else
+  match norm_typ t1, freshen_typ env t2 with
+  | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) ->
+    assert (aks22 = []);
+    let su, zs = match_typ oneway (add_typs aks21 env) t1 t22 ps in
+    List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs
+
+  | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 ->
+    assert (aks12 = []);
+    let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in
+    let t1' = subst_typ (subst aks11 ts1) t12 in
+    let su, zs2 = match_typ oneway env t1' t2 ps in
+    su, zs1 @ zs2
+
+  | TypT(s1), TypT(s2) ->
+    (match s1, s2 with
+    | ExT(aks1, t), ExT([], p) when List.mem p ps ->
+      if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then
+         raise (Sub (Mismatch (t1, t2)));
+      [(p, t)], []
+    | _ ->
+      [], [])
+
+  | StrT(tr1), StrT(tr2) ->
+    match_row oneway env tr1 tr2 ps
+
+  | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) ->
+    if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2)));
+    if p1 <> Pure || p2 <> Pure then
+      [], []
+    else
+      let env' = add_typs aks2 env in
+      let ts1, zs1, f1 =
+        try sub_typ oneway env' t21 t11 (varTs aks1) with Sub e ->
+          raise (Sub (FunParam e)) in
+      let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in
+      let su, zs2 =
+        try match_extyp
+              oneway env' (subst_extyp (subst aks1 ts1) s1) s2 ps'
+        with Sub e -> raise (Sub (FunResult e)) in
+      List.map (function (AppT(p, _), t) -> (p, LamT(aks2, t))
+                       | _ -> assert false) su, lift env (zs1 @ zs2)
+
+  | _ ->
+    raise (Sub (Mismatch (t1, t2)))
+
+and match_extyp oneway env s1 s2 ps =
+  let ExT(aks2, t2) = freshen_extyp env s2 in
+  let ExT(aks1, t1) = freshen_extyp (add_typs aks2 env) s1 in
+  match aks1, aks2 with
+  | [], [] ->
+    match_typ oneway env t1 t2 ps
+  | _ ->
+    [], []
+
+and match_row oneway env tr1 tr2 ps =
+  match tr2 with
+  | [] ->
+    [], []
+  | (l, t2)::tr2' ->
+    let t1, zs, app = extract_bind oneway env tr1 l t2 in
+    let su1, zs1 =
+      try match_typ oneway env t1 t2 ps with
+      | Sub e -> raise (Sub (Struct(l, e))) in
+    let su2, zs2 =
+      match_row oneway env tr1
+        (subst_row (List.map (fun (p, t) -> psubst p t) su1) tr2') ps in
+    su1 @ su2, zs @ zs1 @ zs2
+
 let sub_typ = sub_typ true
 let sub_extyp = sub_extyp true