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

Changes

@@ -11,6 +11,7 @@ Language features:
 - Separation between read-only strings (type string) and read-write byte
   sequences (type bytes). Activated by command-line option -safe-string.
 - Exception cases in pattern matching (patch by Jeremy Yallop).
+- Extensible open datatypes (patch by Leo White).
 
 Build system for the OCaml distribution:
 - Use -bin-annot when building.
@@ -33,7 +34,7 @@ Type system:
 - PR#6331: Slight change in the criterion to distinguish private
   abbreviations and private row types: create a private abbreviation for
   closed objects and fixed polymorphic variants.
-- PR#6333: Compare first class module types structurally rather than
+* PR#6333: Compare first class module types structurally rather than
   nominally. Value subtyping allows module subtyping as long as the internal
   representation is unchanged.
 
@@ -131,6 +132,7 @@ Bug fixes:
 - PR#6384: Uncaught Not_found exception with a hidden .cmi file
 - PR#6385: wrong allocation of large closures by the bytecode interpreter
 - PR#6394: Assertion failed in Typecore.expand_path
+- PR#6405: unsound interaction of -rectypes and GADTs
 - fix -dsource printing of "external _pipe = ..."
   (Gabriel Scherer)
 - bound-checking bug in caml_string_{get,set}{16,32,64}

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
 # 

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
 # 

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
 ;;
 

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 _) -> ()
              ^^^^^^^^

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 _) -> ()
              ^^^^^^^^

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
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^

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
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^

typing/ctype.ml

@@ -1694,7 +1694,8 @@ let occur env ty0 ty =
 let occur_in env ty0 t =
   try occur env ty0 t; false with Unify _ -> true
 
-(* checks that a local constraint is non recursive *)
+(* Check that a local constraint is well-founded *)
+(* PR#6405: always assume -rectypes mode here *)
 let rec local_non_recursive_abbrev visited env p ty =
   let ty = repr ty in
   if not (List.memq ty !visited) then begin
@@ -1704,15 +1705,9 @@ let rec local_non_recursive_abbrev visited env p ty =
         if Path.same p p' then raise Recursive_abbrev;
         begin try
           local_non_recursive_abbrev visited env p (try_expand_once_opt env ty)
-        with Cannot_expand ->
-          if !Clflags.recursive_types then () else
-          iter_type_expr (local_non_recursive_abbrev visited env p) ty
+        with Cannot_expand -> ()
         end
-    | Tobject _ | Tvariant _ ->
-        ()
-    | _ ->
-        if !Clflags.recursive_types then () else
-        iter_type_expr (local_non_recursive_abbrev visited env p) ty
+    | _ -> ()
   end
 
 let local_non_recursive_abbrev env p =