Fix PR#5981

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

Changes

@@ -116,6 +116,7 @@ Bug fixes:
 - PR#5907: Undetected cycle during typecheck causes exceptions
 - PR#5911: Signature substitutions fail in submodules
 - PR#5948: GADT with polymorphic variants bug
+- PR#5982: Incompatibility check assumes abstracted types are injective
 
 OCaml 4.00.1:
 -------------

testsuite/tests/typing-gadts/pr5981.ml

@@ -0,0 +1,22 @@
+module F(S : sig type 'a t end) = struct
+  type _ ab =
+      A : int S.t ab
+    | B : float S.t ab
+
+  let f : int S.t ab -> float S.t ab -> string =
+    fun (l : int S.t ab) (r : float S.t ab) -> match l, r with
+    | A, B -> "f A B"
+end;;
+
+module F(S : sig type 'a t end) = struct
+  type a = int * int
+  type b = int -> int
+
+  type _ ab =
+      A : a S.t ab
+    | B : b S.t ab
+
+  let f : a S.t ab -> b S.t ab -> string =
+    fun l r -> match l, r with
+    | A, B -> "f A B"
+end;;

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

@@ -0,0 +1,28 @@
+
+#                 Characters 196-233:
+  ...............................................match l, r with
+      | A, B -> "f A B"
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+(A, A)
+module F :
+  functor (S : sig type 'a t end) ->
+    sig
+      type _ ab = A : int S.t ab | B : float S.t ab
+      val f : int S.t ab -> float S.t ab -> string
+    end
+#                         Characters 197-234:
+  ...............match l, r with
+      | A, B -> "f A B"
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+(A, A)
+module F :
+  functor (S : sig type 'a t end) ->
+    sig
+      type a = int * int
+      type b = int -> int
+      type _ ab = A : a S.t ab | B : b S.t ab
+      val f : a S.t ab -> b S.t ab -> string
+    end
+# 

typing/ctype.ml

@@ -2244,7 +2244,14 @@ and unify3 env t1 t1' t2 t2' =
           then
             unify_list env tl1 tl2
           else
-            set_mode Pattern ~generate:false (fun () -> unify_list env tl1 tl2)
+            set_mode Pattern ~generate:false
+              begin fun () ->
+                let snap = snapshot () in
+                try unify_list env tl1 tl2 with Unify _ ->
+                  backtrack snap;
+                  List.iter (reify env) (tl1 @ tl2)
+              end
+        (*set_mode Pattern ~generate:false (fun () -> unify_list env tl1 tl2)*)
       | (Tconstr ((Path.Pident p) as path,[],_),
          Tconstr ((Path.Pident p') as path',[],_))
         when is_abstract_newtype !env path && is_abstract_newtype !env path'
@@ -2267,7 +2274,7 @@ and unify3 env t1 t1' t2 t2' =
       | (Tconstr (_,[],_), _) | (_, Tconstr (_,[],_)) when !umode = Pattern ->
           reify env t1';
           reify env t2';
-          mcomp !env t1' t2'
+          if !generate_equations then mcomp !env t1' t2'
       | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
           unify_fields env fi1 fi2;
           (* Type [t2'] may have been instantiated by [unify_fields] *)