Fix PR#5997

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

4 files changed, 58 insertions, 7 deletions

diff --git a/Changes b/Changes
index 438fb6677..41ccfcddc 100644
--- a/Changes
+++ b/Changes
@@ -126,6 +126,7 @@ Bug fixes:
 - PR#5948: GADT with polymorphic variants bug
 - PR#5989: Assumed inequalities involving private rows
 - PR#5993: Variance of private type abbreviations not checked for modules
+- PR#5997: Non-compatibility assumed for concrete types with same constructor
 
 OCaml 4.00.1:
 -------------
diff --git a/testsuite/tests/typing-gadts/pr5997.ml b/testsuite/tests/typing-gadts/pr5997.ml
new file mode 100644
index 000000000..81eec1374
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr5997.ml
@@ -0,0 +1,28 @@
+type (_, _) comp =
+  | Eq : ('a, 'a) comp
+  | Diff : ('a, 'b) comp
+;;
+
+module U = struct type t = T end;;
+
+module M : sig
+  type t = T
+  val comp : (U.t, t) comp
+end = struct
+  include U
+  let comp = Eq
+end;;
+
+match M.comp with | Diff -> false;;
+
+module U = struct type t = {x : int} end;;
+
+module M : sig
+  type t = {x : int}
+  val comp : (U.t, t) comp
+end = struct
+  include U
+  let comp = Eq
+end;;
+
+match M.comp with | Diff -> false;;
diff --git a/testsuite/tests/typing-gadts/pr5997.ml.reference b/testsuite/tests/typing-gadts/pr5997.ml.reference
new file mode 100644
index 000000000..65af9f3b1
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr5997.ml.reference
@@ -0,0 +1,21 @@
+
+#       type (_, _) comp = Eq : ('a, 'a) comp | Diff : ('a, 'b) comp
+#   module U : sig type t = T end
+#               module M : sig type t = T val comp : (U.t, t) comp end
+#   Characters 1-34:
+  match M.comp with | Diff -> false;;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+Eq
+Exception: Match_failure ("//toplevel//", 13, 0).
+#   module U : sig type t = { x : int; } end
+#               module M : sig type t = { x : int; } val comp : (U.t, t) comp end
+#   Characters 1-34:
+  match M.comp with | Diff -> false;;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+Eq
+Exception: Match_failure ("//toplevel//", 22, 0).
+# 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 2bbba4d1f..3d96ef019 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -2040,25 +2040,26 @@ and mcomp_type_option type_pairs subst env t t' =
   | Some t, Some t' -> mcomp type_pairs subst env t t'
   | _ -> raise (Unify [])
 
-and mcomp_variant_description type_pairs subst env =
+and mcomp_variant_description type_pairs subst env xs ys =
   let rec iter = fun x y ->
     match x, y with
-    (name,mflag,t) :: xs, (name', mflag', t') :: ys   ->
+    (id, tl, t) :: xs, (id', tl', t') :: ys   ->
       mcomp_type_option type_pairs subst env t t';
-      if name = name' && mflag = mflag'
+      mcomp_list type_pairs subst env tl tl';
+      if Ident.name id = Ident.name id'
       then iter xs ys
       else raise (Unify [])
     | [],[] -> ()
     | _ -> raise (Unify [])
   in
-  iter
+  iter xs ys
 
 and mcomp_record_description type_pairs subst env =
   let rec iter = fun x y ->
     match x, y with
-      (name, mutable_flag, t) :: xs, (name', mutable_flag', t') :: ys ->
+      (id, mutable_flag, t) :: xs, (id', mutable_flag', t') :: ys ->
         mcomp type_pairs subst env t t';
-        if name = name' && mutable_flag = mutable_flag'
+        if Ident.name id = Ident.name id' && mutable_flag = mutable_flag'
         then iter xs ys
         else raise (Unify [])
     | [], [] -> ()
@@ -2271,7 +2272,7 @@ and unify3 env t1 t1' t2 t2' =
           reify env t1' ;
           local_non_recursive_abbrev !env (Path.Pident p) t1';
           add_gadt_equation env p t1'
-      | (Tconstr (_,[],_), _) | (_, Tconstr (_,[],_)) when !umode = Pattern ->
+      | (Tconstr (_,_,_), _) | (_, Tconstr (_,_,_)) when !umode = Pattern ->
           reify env t1';
           reify env t2';
           if !generate_equations then mcomp !env t1' t2'