From ff7547dca05ea8a7066209ef2a053bf6a06918b1 Mon Sep 17 00:00:00 2001
From: Jacques Garrigue <garrigue at math.nagoya-u.ac.jp>
Date: Fri, 12 Apr 2013 10:20:14 +0000
Subject: [PATCH] Fix PR#5981

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@13514 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
---
 Changes                                       |  1 +
 testsuite/tests/typing-gadts/pr5981.ml        | 22 +++++++++++++++
 .../tests/typing-gadts/pr5981.ml.reference    | 28 +++++++++++++++++++
 typing/ctype.ml                               | 11 ++++++--
 4 files changed, 60 insertions(+), 2 deletions(-)
 create mode 100644 testsuite/tests/typing-gadts/pr5981.ml
 create mode 100644 testsuite/tests/typing-gadts/pr5981.ml.reference

diff --git a/Changes b/Changes
index 9e8408bb3..b18b5cc22 100644
--- a/Changes
+++ b/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:
 -------------
diff --git a/testsuite/tests/typing-gadts/pr5981.ml b/testsuite/tests/typing-gadts/pr5981.ml
new file mode 100644
index 000000000..f93b4e36f
--- /dev/null
+++ b/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;;
diff --git a/testsuite/tests/typing-gadts/pr5981.ml.reference b/testsuite/tests/typing-gadts/pr5981.ml.reference
new file mode 100644
index 000000000..3a2d7b162
--- /dev/null
+++ b/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
+# 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 006b93151..df9261327 100644
--- a/typing/ctype.ml
+++ b/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] *)