do not fail when injectivity not proved in Pattern mode, use mcomp

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

8 files changed, 66 insertions, 29 deletions

diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference
index dda0a0fa7..39102239a 100644
--- a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference
@@ -148,7 +148,7 @@ val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
                                            ^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type a * a vlist
        but a pattern was expected which matches values of type
-         ex#42 = ex#43 * ex#44
+         ex#46 = ex#47 * ex#48
 #                                                         type ('a, 'b) ty =
     Int : (int, 'd) ty
   | String : (string, 'f) ty
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference
index dda0a0fa7..39102239a 100644
--- a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference
+++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference
@@ -148,7 +148,7 @@ val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
                                            ^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type a * a vlist
        but a pattern was expected which matches values of type
-         ex#42 = ex#43 * ex#44
+         ex#46 = ex#47 * ex#48
 #                                                         type ('a, 'b) ty =
     Int : (int, 'd) ty
   | String : (string, 'f) ty
diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml
index 1ae0c9748..29afce430 100644
--- a/testsuite/tests/typing-gadts/test.ml
+++ b/testsuite/tests/typing-gadts/test.ml
@@ -436,3 +436,21 @@ let f : type a. a ty -> a t -> int = fun x y ->
   | {left=TA; right=D 0} -> -1
   | {left=TA; right=D z} -> z
 ;; (* ok *)
+
+(* Injectivity *)
+
+module M : sig type 'a t val eq : ('a t, 'b t) eq end =
+  struct type 'a t = int let eq = Eq end
+;;
+
+let f : type a b. (a M.t, b M.t) eq -> (a, b) eq =
+  function Eq -> Eq (* fail *)
+;;
+
+let f : type a b. (a M.t * a, b M.t * b) eq -> (a, b) eq =
+  function Eq -> Eq (* ok *)
+;;
+
+let f : type a b. (a * a M.t, b * b M.t) eq -> (a, b) eq =
+  function Eq -> Eq (* ok *)
+;;
diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference
index b770efb90..f2ef431b7 100644
--- a/testsuite/tests/typing-gadts/test.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/test.ml.principal.reference
@@ -50,9 +50,9 @@ module Nonexhaustive :
 #               Characters 119-120:
       let eval (D x) = x
                        ^
-Error: This expression has type ex#12 t
-       but an expression was expected of type ex#12 t
-       The type constructor ex#12 would escape its scope
+Error: This expression has type ex#16 t
+       but an expression was expected of type ex#16 t
+       The type constructor ex#16 would escape its scope
 #                       Characters 157-158:
   	  C ->
      ^
@@ -268,4 +268,12 @@ Here is an example of a value that is not matched:
 {left=TE TC; right=D [|  |]}
 type ('a, 'b) pair = { left : 'a; right : 'b; }
 val f : 'a ty -> 'a t -> int = <fun>
+#           module M : sig type 'a t val eq : ('a t, 'b t) eq end
+#       Characters 69-71:
+    function Eq -> Eq (* fail *)
+                   ^^
+Error: This expression has type (a, a) eq
+       but an expression was expected of type (a, b) eq
+#       val f : ('a M.t * 'a, 'b M.t * 'b) eq -> ('a, 'b) eq = <fun>
+#       val f : ('a * 'a M.t, 'b * 'b M.t) eq -> ('a, 'b) eq = <fun>
 # 
diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference
index bb44dce52..2e76a55ae 100644
--- a/testsuite/tests/typing-gadts/test.ml.reference
+++ b/testsuite/tests/typing-gadts/test.ml.reference
@@ -50,9 +50,9 @@ module Nonexhaustive :
 #               Characters 119-120:
       let eval (D x) = x
                        ^
-Error: This expression has type ex#12 t
-       but an expression was expected of type ex#12 t
-       The type constructor ex#12 would escape its scope
+Error: This expression has type ex#16 t
+       but an expression was expected of type ex#16 t
+       The type constructor ex#16 would escape its scope
 #                       Characters 157-158:
   	  C ->
      ^
@@ -255,4 +255,12 @@ Here is an example of a value that is not matched:
 {left=TE TC; right=D [|  |]}
 type ('a, 'b) pair = { left : 'a; right : 'b; }
 val f : 'a ty -> 'a t -> int = <fun>
+#           module M : sig type 'a t val eq : ('a t, 'b t) eq end
+#       Characters 69-71:
+    function Eq -> Eq (* fail *)
+                   ^^
+Error: This expression has type (a, a) eq
+       but an expression was expected of type (a, b) eq
+#       val f : ('a M.t * 'a, 'b M.t * 'b) eq -> ('a, 'b) eq = <fun>
+#       val f : ('a * 'a M.t, 'b * 'b M.t) eq -> ('a, 'b) eq = <fun>
 # 
diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
index 527649649..5b1016c97 100644
--- a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
@@ -1,10 +1,8 @@
 
-#                           Characters 212-216:
+#                           Characters 240-248:
            let f (Refl : (a T.t, b T.t) eq) = (x :> b)
-                  ^^^^
-Error: This pattern matches values of type (a T.t, a T.t) eq
-       but a pattern was expected which matches values of type
-         (a T.t, b T.t) eq
+                                              ^^^^^^^^
+Error: Type a is not a subtype of b 
 #                         Characters 36-67:
   type (_, +_) eq = Refl : ('a, 'a) eq
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference
index 527649649..5b1016c97 100644
--- a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference
+++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference
@@ -1,10 +1,8 @@
 
-#                           Characters 212-216:
+#                           Characters 240-248:
            let f (Refl : (a T.t, b T.t) eq) = (x :> b)
-                  ^^^^
-Error: This pattern matches values of type (a T.t, a T.t) eq
-       but a pattern was expected which matches values of type
-         (a T.t, b T.t) eq
+                                              ^^^^^^^^
+Error: Type a is not a subtype of b 
 #                         Characters 36-67:
   type (_, +_) eq = Refl : ('a, 'a) eq
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 319bec1c3..3c44985c4 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -193,16 +193,21 @@ type unification_mode =
   | Pattern (* unification in pattern which may add local constraints *)
 
 let umode = ref Expression
+let generate_equations = ref false
 
-let set_mode mode f = 
-  let old_unification_mode = !umode in
+let set_mode mode ?(generate = (mode = Pattern)) f = 
+  let old_unification_mode = !umode
+  and old_gen = !generate_equations in
   try
     umode := mode;
+    generate_equations := generate;
     let ret = f () in
     umode := old_unification_mode;
+    generate_equations := old_gen;
     ret
   with e ->
     umode := old_unification_mode;
+    generate_equations := old_gen;
     raise e
 
                   (**********************************************)
@@ -2120,8 +2125,7 @@ and unify3 env t1 t1' t2 t2' =
       occur_univar !env t1;
       link_type t2' t1;
   | _ ->
-      let umode = !umode in
-      begin match umode with
+      begin match !umode with
       | Expression ->
           occur !env t1' t2';
           link_type t1' t2
@@ -2140,30 +2144,33 @@ and unify3 env t1 t1' t2 t2' =
       | (Ttuple tl1, Ttuple tl2) ->
           unify_list env tl1 tl2
       | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
-          if umode = Expression || in_current_module p1 || in_pervasives p1
+          if !umode = Expression || not !generate_equations
+          || in_current_module p1 || in_pervasives p1
           || is_datatype (Env.find_type p1 !env)
-          then unify_list env tl1 tl2
-          else set_mode Expression (fun () -> unify_list env tl1 tl2)
+          then
+            unify_list env tl1 tl2
+          else
+            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'
-        && umode = Pattern -> 
+        && !generate_equations -> 
           let source,destination = 
             if find_newtype_level !env path > find_newtype_level !env path'
             then  p,t2'
             else  p',t1'
           in add_gadt_equation env source destination
       | (Tconstr ((Path.Pident p) as path,[],_), _)
-        when is_abstract_newtype !env path && umode = Pattern -> 
+        when is_abstract_newtype !env path && !generate_equations -> 
           reify env t2';
           local_non_recursive_abbrev !env (Path.Pident p) t2';
           add_gadt_equation env p t2'
       | (_, Tconstr ((Path.Pident p) as path,[],_))
-        when is_abstract_newtype !env path && umode = Pattern -> 
+        when is_abstract_newtype !env path && !generate_equations -> 
           reify env t1' ;
           local_non_recursive_abbrev !env (Path.Pident p) t1';
           add_gadt_equation env p t1'
-      | (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern ->
+      | (Tconstr (_,[],_), _) | (_, Tconstr (_,[],_)) when !umode = Pattern ->
           reify env t1';
           reify env t2';
           mcomp !env t1' t2'