Fix MPR#7668

Changes

@@ -61,6 +61,9 @@ be mentioned in the 4.06 section below instead of here.)
   non-regular files, like other Unix variants do.
   (Xavier Leroy)
 
+- MPR#7668: -principal is broken with polymorphic variants
+  (Jacques Garrigue, report by Jun Furuse)
+
 Release branch for 4.06:
 ------------------------
 

testsuite/tests/typing-gadts/test.ml

@@ -736,6 +736,11 @@ Error: This expression has type [> `A of a ]
        Type a is not compatible with type b = a
        This instance of a is ambiguous:
        it would escape the scope of its equation
+|}, Principal{|
+Line _, characters 9-15:
+Error: This expression has type ([> `A of b ] as 'a) -> 'a
+       but an expression was expected of type [> `A of a ] -> [> `A of b ]
+       Types for tag `A are incompatible
 |}];;
 
 let f (type a b) (eq : (a,b) eq) (v : [> `A of a]) : [> `A of b] =

testsuite/tests/typing-misc/pr7668_bad.ml

@@ -0,0 +1,23 @@
+let partition_map f xs =
+ let rec part left right = function
+   | [] -> List.rev left, List.rev right
+   | x::xs ->
+       match f x with
+       | `Left v -> part (v::left) right xs
+       | `Right v -> part left (v::right) xs
+ in
+ part [] [] xs
+;;
+
+let f xs : (int list * int list) = partition_map (fun x -> if x then `Left ()
+else `Right ()) xs
+;;
+[%%expect{|
+val partition_map :
+  ('a -> [< `Left of 'b | `Right of 'c ]) -> 'a list -> 'b list * 'c list =
+  <fun>
+Line _, characters 35-96:
+Error: This expression has type unit list * unit list
+       but an expression was expected of type int list * int list
+       Type unit is not compatible with type int
+|}]

testsuite/tests/typing-poly/poly.ml

@@ -1376,15 +1376,11 @@ end;;
 [%%expect {|
 val n : < m : 'x 'a. ([< `Foo of 'x ] as 'a) -> 'x > = <obj>
 |}];;
-(* ok, but not with -principal *)
+(* ok *)
 let n =
   object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
 [%%expect {|
 val n : < m : 'x. [< `Foo of 'x ] -> 'x > = <obj>
-|}, Principal{|
-Line _, characters 47-68:
-Error: This method has type ([< `Foo of 'b ] as 'a) -> 'b
-       which is less general than 'x. 'a -> 'x
 |}];;
 (* fail *)
 let (n : < m : 'a. [< `Foo of int] -> 'a >) =
@@ -1395,10 +1391,6 @@ Error: This expression has type < m : 'x. [< `Foo of 'x ] -> 'x >
        but an expression was expected of type
          < m : 'a. [< `Foo of int ] -> 'a >
        The universal variable 'x would escape its scope
-|}, Principal{|
-Line _, characters 47-68:
-Error: This method has type ([< `Foo of 'b ] as 'a) -> 'b
-       which is less general than 'x. 'a -> 'x
 |}];;
 (* fail *)
 let (n : 'b -> < m : 'a . ([< `Foo of int] as 'b) -> 'a >) = fun x ->
@@ -1409,10 +1401,6 @@ Error: This expression has type < m : 'x. [< `Foo of 'x ] -> 'x >
        but an expression was expected of type
          < m : 'a. [< `Foo of int ] -> 'a >
        The universal variable 'x would escape its scope
-|}, Principal{|
-Line _, characters 47-68:
-Error: This method has type ([< `Foo of 'b ] as 'a) -> 'b
-       which is less general than 'x. 'a -> 'x
 |}];;
 
 (* PR#6171 *)

typing/ctype.ml

@@ -995,7 +995,7 @@ let rec copy ?env ?partial ?keep_names ty =
               Tlink ty2
           | _ ->
               (* If the row variable is not generic, we must keep it *)
-              let keep = more.level <> generic_level in
+              let keep = more.level <> generic_level && partial = None in
               let more' =
                 match more.desc with
                   Tsubst ty -> ty