Fix PR#7222

Changes

@@ -816,6 +816,9 @@ Bug fixes:
 - PR#7220: fix a memory leak when using both threads and exception backtraces
   (Gabriel Scherer, review by François Bobot, report by Rob Hoes)
 
+- PR#7222: Escaped existential type
+  (Jacques Garrigue, report by Florian Angeletti)
+
 - GPR#205: Clear caml_backtrace_last_exn before registering as root
   (report and fix by Frederic Bour)
 

testsuite/tests/typing-gadts/pr6158.ml.reference

@@ -9,7 +9,11 @@ Error: This pattern matches values of type (int s, int s) eq
        but a pattern was expected which matches values of type
          (int s, int t) eq
        Type int s is not compatible with type int t 
-#     module M :
-  functor (S : sig type 'a t = T of 'a type 'a s = T of 'a end) ->
-    sig val f : ($'a S.s, $'a S.t) eq -> unit end
+#     Characters 120-124:
+  struct let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> () end;;
+                                                        ^^^^
+Error: This pattern matches values of type ($'a S.s, $'a S.s) eq
+       but a pattern was expected which matches values of type
+         ($'a S.s, $'a S.t) eq
+       The type constructor $'a would escape its scope
 # 

testsuite/tests/typing-gadts/pr6690.ml.reference

@@ -5,21 +5,21 @@ type 'a local_visit_action
 type ('a, 'result, 'visit_action) context =
     Local : ('a, 'a * insert, 'a local_visit_action) context
   | Global : ('a, 'a, 'a visit_action) context
-#             Characters 35-166:
-  ....: (_, _, visit_action) context -> _ -> visit_action =
-    function
+#             Characters 104-109:
     | Local -> fun _ -> raise Exit
-    | Global -> fun _ -> raise Exit
-Error: This expression has type ($0, $0 * insert, 'a) context -> 'b -> 'a
-       but an expression was expected of type 'c
+      ^^^^^
+Error: This pattern matches values of type
+         ($0, $0 * insert, $0 local_visit_action) context
+       but a pattern was expected which matches values of type
+         ($0, $0 * insert, visit_action) context
        The type constructor $0 would escape its scope
-#             Characters 35-174:
-  ....: ('a, 'result, visit_action) context -> 'a -> visit_action =
-    function
+#             Characters 112-117:
     | Local -> fun _ -> raise Exit
-    | Global -> fun _ -> raise Exit
-Error: This expression has type ($'a, $'a * insert, 'a) context -> $'a -> 'a
-       but an expression was expected of type 'b
+      ^^^^^
+Error: This pattern matches values of type
+         ($'a, $'a * insert, $'a local_visit_action) context
+       but a pattern was expected which matches values of type
+         ($'a, $'a * insert, visit_action) context
        The type constructor $'a would escape its scope
 #             val vexpr : (unit, 'a, 'b) context -> unit -> 'b = <fun>
 # 

testsuite/tests/typing-gadts/pr7222.ml

@@ -0,0 +1,10 @@
+type +'a n = private int 
+type nil = private Nil_type
+type (_,_) elt =
+  | Elt_fine: 'nat n -> ('l,'nat * 'l) elt
+  | Elt: 'nat n -> ('l,'nat -> 'l) elt
+type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t;;
+
+let undetected: ('a -> 'b -> nil) t -> 'a n -> 'b n -> unit = fun sh i j ->
+  let Cons(Elt dim, _) = sh in ()
+;;

testsuite/tests/typing-gadts/pr7222.ml.principal.reference

@@ -0,0 +1,15 @@
+
+#           type +'a n = private int
+type nil = private Nil_type
+type (_, _) elt =
+    Elt_fine : 'nat n -> ('l, 'nat * 'l) elt
+  | Elt : 'nat n -> ('l, 'nat -> 'l) elt
+type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t
+#       Characters 83-99:
+    let Cons(Elt dim, _) = sh in ()
+        ^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type ('a -> $0 -> nil) t
+       but a pattern was expected which matches values of type
+         ('a -> 'b -> nil) t
+       The type constructor $0 would escape its scope
+# 

testsuite/tests/typing-gadts/pr7222.ml.reference

@@ -0,0 +1,15 @@
+
+#           type +'a n = private int
+type nil = private Nil_type
+type (_, _) elt =
+    Elt_fine : 'nat n -> ('l, 'nat * 'l) elt
+  | Elt : 'nat n -> ('l, 'nat -> 'l) elt
+type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t
+#       Characters 88-95:
+    let Cons(Elt dim, _) = sh in ()
+             ^^^^^^^
+Error: This pattern matches values of type ($Cons_'x, 'a -> $Cons_'x) elt
+       but a pattern was expected which matches values of type
+         ($Cons_'x, 'a -> $'b -> nil) elt
+       The type constructor $'b would escape its scope
+# 

typing/ctype.ml

@@ -1898,7 +1898,9 @@ let reify env t =
       match ty.desc with
         Tvar o ->
           let t = create_fresh_constr ty.level o in
-          link_type ty t
+          link_type ty t;
+          if ty.level < newtype_level then
+            raise (Unify [t, newvar2 ty.level])
       | Tvariant r ->
           let r = row_repr r in
           if not (static_row r) then begin
@@ -1909,7 +1911,9 @@ let reify env t =
                 let t = create_fresh_constr m.level o in
                 let row =
                   {r with row_fields=[]; row_fixed=true; row_more = t} in
-                link_type m (newty2 m.level (Tvariant row))
+                link_type m (newty2 m.level (Tvariant row));
+                if m.level < newtype_level then
+                  raise (Unify [t, newvar2 m.level])
             | _ -> assert false
           end;
           iter_row iterator r