Fix PR#6241

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

Changes

@@ -65,6 +65,7 @@ Bug fixes:
 - PR#6216: inlining of GADT matches generates invalid assembly
 - PR#6235: Issue with type information flowing through a variant pattern
 - PR#6240: Fail to expand module type abbreviation during substyping
+- PR#6241: Assumed inequality between paths involving functor arguments
 
 OCaml 4.01.0:
 -------------

testsuite/tests/typing-gadts/pr6241.ml

@@ -0,0 +1,16 @@
+type (_, _) t =
+ A : ('a, 'a) t
+| B : string -> ('a, 'b) t
+;;
+
+module M (A : sig module type T end) (B : sig module type T end) =
+struct
+ let f : ((module A.T), (module B.T)) t -> string = function
+   | B s -> s
+end;;
+
+module A = struct module type T = sig end end;;
+
+module N = M(A)(A);;
+
+let x = N.f A;;

testsuite/tests/typing-gadts/pr6241.ml.principal.reference

@@ -0,0 +1,16 @@
+
+#       type (_, _) t = A : ('a, 'a) t | B : string -> ('a, 'b) t
+#           Characters 127-149:
+  ....................................................function
+     | B s -> s
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+A
+module M :
+  functor (A : sig module type T end) ->
+    functor (B : sig module type T end) ->
+      sig val f : ((module A.T), (module B.T)) t -> string end
+#   module A : sig module type T = sig  end end
+#   module N : sig val f : ((module A.T), (module A.T)) t -> string end
+#   Exception: Match_failure ("//toplevel//", 7, 52).
+# 

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

@@ -0,0 +1,16 @@
+
+#       type (_, _) t = A : ('a, 'a) t | B : string -> ('a, 'b) t
+#           Characters 127-149:
+  ....................................................function
+     | B s -> s
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+A
+module M :
+  functor (A : sig module type T end) ->
+    functor (B : sig module type T end) ->
+      sig val f : ((module A.T), (module B.T)) t -> string end
+#   module A : sig module type T = sig  end end
+#   module N : sig val f : ((module A.T), (module A.T)) t -> string end
+#   Exception: Match_failure ("//toplevel//", 7, 52).
+# 

typing/ctype.ml

@@ -1991,8 +1991,7 @@ let rec mcomp type_pairs env t1 t2 =
         | (Tconstr (p, _, _), _) | (_, Tconstr (p, _, _)) ->
             let decl = Env.find_type p env in
             if non_aliasable p decl then raise (Unify [])
-        | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
-          when Path.same p1 p2 && n1 = n2 ->
+        | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when n1 = n2 ->
             mcomp_list type_pairs env tl1 tl2
         | (Tvariant row1, Tvariant row2) ->
             mcomp_row type_pairs env row1 row2
@@ -2398,9 +2397,12 @@ and unify3 env t1 t1' t2 t2' =
           unify env t1 t2
       | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
           enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env)
-      | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
-        when Path.same p1 p2 && n1 = n2 ->
-          unify_list env tl1 tl2
+      | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when n1 = n2 ->
+          if Path.same p1 p2 then unify_list env tl1 tl2 else
+          if !umode = Expression then raise (Unify []) else begin
+            List.iter (reify env) (tl1 @ tl2);
+            if !generate_equations then List.iter2 (mcomp !env) tl1 tl2
+          end
       | (_, _) ->
           raise (Unify [])
       end;