From b66c48d10277e3f93d6f08dbfa3319c1f0c9250b Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Mon, 20 Jul 2020 03:06:50 +0300
Subject: [PATCH] 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        | 8 +++++++-
 regression.1ml | 6 ++++++
 types.ml       | 9 ++++++++-
 3 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/elab.ml b/elab.ml
index 660ab5b9..37dce93a 100644
--- a/elab.ml
+++ b/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
diff --git a/regression.1ml b/regression.1ml
index 14906782..a3731e47 100644
--- a/regression.1ml
+++ b/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)}
diff --git a/types.ml b/types.ml
index 7dfc3c9b..9c271049 100644
--- a/types.ml
+++ b/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')