Change to disallow rec type aliases

For example,

    rec {type t} => {type t = t}

is no longer allowed.

The check is overly restrictive.

elab.ml

@@ -563,10 +563,16 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
       let t2, zs2 = elab_pathexp env1 exp1 l in
 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 (varTs aks1) with Sub e -> error typ.at
+        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

regression.1ml

@@ -298,6 +298,12 @@ Hungry = {
   do eater <+ 1 <+ 2
 }
 
+type_error rec {type t _, type u _} => {
+  type t x = u x
+  type u x = int
+}
+type_error type rec t => t
+
 PolyRec = {
   type l a = rec (type t) => a | t
   ...rec {type t a} => {type t a = a | t (a, a)}

types.ml

@@ -335,7 +335,14 @@ let rec norm_typ = function
   | FunT(aks, t, s, f) -> FunT(aks, norm_typ t, norm_extyp s, f)
   | TypT(s) -> TypT(norm_extyp s)
   | WrapT(s) -> WrapT(norm_extyp s)
-  | LamT(aks, t) -> LamT(aks, norm_typ t)
+  | LamT(aks, t) ->
+    (match norm_typ t with
+    | AppT(f, ts)
+         when List.for_all2 (fun (a, k) t -> t = VarT (a, k)) aks ts &&
+              List.for_all (fun (a, k) -> not (contains_typ a f)) aks ->
+      f
+    | t -> LamT(aks, t)
+    )
   | AppT(t, ts) ->
     (match norm_typ t with
     | LamT(aks, t') -> norm_typ (subst_typ (subst aks ts) t')