Fix PR#6405: unsound interaction of -rectypes and GADTs

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14769 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

7 files changed, 24 insertions, 34 deletions

diff --git a/testsuite/tests/typing-gadts/pr6174.ml.principal.reference b/testsuite/tests/typing-gadts/pr6174.ml.principal.reference
index 647015c367..8f2be5252c 100644
--- a/testsuite/tests/typing-gadts/pr6174.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/pr6174.ml.principal.reference
@@ -1,8 +1,7 @@
 
-#     Characters 118-119:
+#     Characters 137-138:
    fun C k -> k (fun x -> x);;
-       ^
-Error: Recursive local constraint when unifying
-         (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
-       with ((a -> o) -> o) t
+                          ^
+Error: This expression has type ex#0 but an expression was expected of type
+         ex#1 = (ex#2 -> ex#1) -> ex#1
 # 
diff --git a/testsuite/tests/typing-gadts/pr6174.ml.reference b/testsuite/tests/typing-gadts/pr6174.ml.reference
index 647015c367..8f2be5252c 100644
--- a/testsuite/tests/typing-gadts/pr6174.ml.reference
+++ b/testsuite/tests/typing-gadts/pr6174.ml.reference
@@ -1,8 +1,7 @@
 
-#     Characters 118-119:
+#     Characters 137-138:
    fun C k -> k (fun x -> x);;
-       ^
-Error: Recursive local constraint when unifying
-         (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
-       with ((a -> o) -> o) t
+                          ^
+Error: This expression has type ex#0 but an expression was expected of type
+         ex#1 = (ex#2 -> ex#1) -> ex#1
 # 
diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml
index a8215290ad..2f0bb91962 100644
--- a/testsuite/tests/typing-gadts/test.ml
+++ b/testsuite/tests/typing-gadts/test.ml
@@ -102,12 +102,8 @@ module Existential_escape =
 module Rectype =
   struct
     type (_,_) t = C : ('a,'a) t
-    let _ =
-      fun (type s) ->
-        let a : (s, s * s) t = failwith "foo" in
-        match a with
-          C ->
-            ()
+    let f : type s. (s, s*s) t -> unit =
+      fun C -> () (* here s = s*s! *)
   end
 ;;
 
diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference
index 0d40f674a5..fd9fb3501c 100644
--- a/testsuite/tests/typing-gadts/test.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/test.ml.principal.reference
@@ -53,10 +53,8 @@ module Nonexhaustive :
 Error: This expression has type a#2 t but an expression was expected of type
          a#2 t
        The type constructor a#2 would escape its scope
-#                       Characters 174-175:
-            C ->
-            ^
-Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
+#               module Rectype :
+  sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
 #                         Characters 178-186:
           | (IntLit _ | BoolLit _) -> ()
              ^^^^^^^^
diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference
index e6aa47b415..a5faa02c01 100644
--- a/testsuite/tests/typing-gadts/test.ml.reference
+++ b/testsuite/tests/typing-gadts/test.ml.reference
@@ -53,10 +53,8 @@ module Nonexhaustive :
 Error: This expression has type a#2 t but an expression was expected of type
          a#2 t
        The type constructor a#2 would escape its scope
-#                       Characters 174-175:
-            C ->
-            ^
-Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
+#               module Rectype :
+  sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
 #                         Characters 178-186:
           | (IntLit _ | BoolLit _) -> ()
              ^^^^^^^^
diff --git a/testsuite/tests/typing-objects/Tests.ml.principal.reference b/testsuite/tests/typing-objects/Tests.ml.principal.reference
index 97e3c16359..1a01585e01 100644
--- a/testsuite/tests/typing-objects/Tests.ml.principal.reference
+++ b/testsuite/tests/typing-objects/Tests.ml.principal.reference
@@ -295,12 +295,12 @@ Warning 10: this expression should have type unit.
   unit -> object method private m : int method n : int method o : int end
 #   - : int * int = (1, 1)
 #   class c : unit -> object method m : int end
-#       - : int = 98
-# - : int = 99
+#       - : int = 99
 # - : int = 100
-#         - : int * int * int = (101, 102, 103)
-#           - : int * int * int * int * int = (104, 105, 106, 33, 33)
-#           - : int * int * int * int * int = (107, 108, 109, 33, 33)
+# - : int = 101
+#         - : int * int * int = (102, 103, 104)
+#           - : int * int * int * int * int = (105, 106, 107, 33, 33)
+#           - : int * int * int * int * int = (108, 109, 110, 33, 33)
 #         Characters 42-69:
   class a = let _ = new b in object end
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/testsuite/tests/typing-objects/Tests.ml.reference b/testsuite/tests/typing-objects/Tests.ml.reference
index 2a3fc30428..70c05115fd 100644
--- a/testsuite/tests/typing-objects/Tests.ml.reference
+++ b/testsuite/tests/typing-objects/Tests.ml.reference
@@ -294,12 +294,12 @@ Warning 10: this expression should have type unit.
   unit -> object method private m : int method n : int method o : int end
 #   - : int * int = (1, 1)
 #   class c : unit -> object method m : int end
-#       - : int = 98
-# - : int = 99
+#       - : int = 99
 # - : int = 100
-#         - : int * int * int = (101, 102, 103)
-#           - : int * int * int * int * int = (104, 105, 106, 33, 33)
-#           - : int * int * int * int * int = (107, 108, 109, 33, 33)
+# - : int = 101
+#         - : int * int * int = (102, 103, 104)
+#           - : int * int * int * int * int = (105, 106, 107, 33, 33)
+#           - : int * int * int * int * int = (108, 109, 110, 33, 33)
 #         Characters 42-69:
   class a = let _ = new b in object end
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^