WIP Recursively dependent signatures

elab.ml

@@ -270,6 +270,18 @@ Trace.debug (lazy ("[WithT] aks12 = " ^ string_of_norm_extyp (ExT(aks12, StrT []
     ExT(aks11, subst_typ (subst aks12 ts) t1),
     lift_warn typ.at t1 (add_typs aks11 env) (zs1 @ zs2 @ zs3)
 
+  | EL.RecT(var, typ1, typ2) ->
+    let ExT(aks1, t1), zs1 = elab_typ env typ1 l in
+    let env1 = add_val var.it t1 (add_typs aks1 env) in
+    let ExT(aks2, t2), zs2 = elab_typ env1 typ2 l in
+    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' = freshen_vars env aks1 in
+    let t3 = subst_typ (subst aks1 (varTs aks')) t2 in
+    ExT(aks', t3), lift_warn typ.at t3 env (zs1 @ zs2 @ zs3)
+
 and elab_dec env dec l =
   Trace.elab (lazy ("[elab_dec] " ^ EL.label_of_dec dec));
   (fun (s, zs) -> dec.at, env, s, zs, None, EL.label_of_dec dec) <<<

sub.ml

@@ -91,6 +91,23 @@ let lift_warn at t env zs =
 
 (* Subtyping *)
 
+let rec is_tycon_typ = function
+  | VarT(_) -> false
+  | PrimT(_) -> false
+  | StrT(_) -> false
+  | FunT(_, _, s, Explicit e) -> e = Pure && is_tycon_extyp s
+  | FunT(_, _, _, Implicit) -> false
+  | TypT(_) -> true
+  | WrapT(_) -> false
+  | LamT(_) -> false
+  | AppT(_) -> false
+  | TupT(_) -> false
+  | DotT(_) -> false
+  | RecT(_) -> false
+  | InferT(_) -> false
+
+and is_tycon_extyp (ExT(_, t)) = is_tycon_typ t
+
 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));
@@ -290,7 +307,8 @@ and sub_row env tr1 tr2 ps =
   | [] ->
     [], [], []
   | (l, t2)::tr2' ->
-    Trace.sub (lazy ("[sub_row] l = " ^ l));
+    Trace.sub (lazy (let k = if is_tycon_typ t2 then "type" else "val" in
+                     "[sub_row] l = " ^ l ^ " [" ^ k ^ "]"));
     let ts1, zs1, f =
       try sub_typ env (List.assoc l tr1) t2 ps with
       | Not_found -> raise (Sub (Struct(l, Missing)))

syntax.ml

@@ -28,6 +28,7 @@ and typ' =
   | EqT of exp
   | AsT of typ * typ
   | WithT of typ * var list * exp
+  | RecT of var * typ * typ
 
 and dec = (dec', unit) phrase
 and dec' =
@@ -210,13 +211,10 @@ let dotopE(x) =
 
 let recT(p, t2) =
   let b, t1 = p.it in
-  let e = TypE(t2)@@t2.at in
-  let e' =
-    match b.it with
-    | VarB(x, _) -> RecE(x, t1, e)
-    | EmptyB -> RecE("_"@@b.at, t1, e)
-    | _ -> RecE("$"@@b.at, t1, letE(b, e)@@span[b.at; e.at])
-  in PathT(e'@@span[p.at; t2.at])
+  match b.it with
+  | VarB(x, _) -> RecT(x, t1, t2)
+  | EmptyB -> RecT("_"@@b.at, t1, t2)
+  | _ -> RecT("$"@@b.at, t1, letT(b, t2)@@span[b.at; t2.at])
 
 let recE(p, e) =
   let b, t = p.it in
@@ -344,6 +342,7 @@ let label_of_typ t =
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
   | WithT _ -> "WithT"
+  | RecT _ -> "RecT"
 
 let label_of_dec d =
   match d.it with
@@ -398,6 +397,8 @@ let rec string_of_typ t =
   | AsT(t1, t2) -> node' [string_of_typ t1; string_of_typ t2]
   | WithT(t, xs, e) ->
     node' ([string_of_typ t] @ List.map string_of_var xs @ [string_of_exp e])
+  | RecT(x, b, t) ->
+    node' [string_of_var x; string_of_typ b; string_of_typ t]
 
 and string_of_dec d =
   let node' = node (label_of_dec d) in