Merge pull request #9612 from garrigue/pr6744ex

fix number and add examples for #6744

testsuite/tests/typing-poly/poly.ml

@@ -1486,7 +1486,7 @@ match fun x -> x with x -> x, x;;
 - : ('a -> 'a) * ('b -> 'b) = (<fun>, <fun>)
 |}];;
 
-(* PR#6747 *)
+(* PR#6744 *)
 (* ok *)
 let n = object
   method m : 'x 'o. ([< `Foo of 'x] as 'o) -> 'x = fun x -> assert false
@@ -1524,6 +1524,39 @@ Error: This expression has type < m : 'x. [< `Foo of 'x ] -> 'x >
          < m : 'a. [< `Foo of int ] -> 'a >
        The universal variable 'x would escape its scope
 |}];;
+(* ok *)
+let f (n : < m : 'a 'r. [< `Foo of 'a & int | `Bar] as 'r >) =
+  (n : < m : 'b 'r. [< `Foo of 'b & int | `Bar] as 'r >)
+[%%expect{|
+val f :
+  < m : 'a 'c. [< `Bar | `Foo of 'a & int ] as 'c > ->
+  < m : 'b 'd. [< `Bar | `Foo of 'b & int ] as 'd > = <fun>
+|}]
+(* fail? *)
+let f (n : < m : 'a 'r. [< `Foo of 'a & int | `Bar] as 'r >) =
+  (n : < m : 'b 'r. [< `Foo of int & 'b | `Bar] as 'r >)
+[%%expect{|
+Line 2, characters 3-4:
+2 |   (n : < m : 'b 'r. [< `Foo of int & 'b | `Bar] as 'r >)
+       ^
+Error: This expression has type
+         < m : 'a 'c. [< `Bar | `Foo of 'a & int ] as 'c >
+       but an expression was expected of type
+         < m : 'b 'd. [< `Bar | `Foo of int & 'b ] as 'd >
+       Types for tag `Foo are incompatible
+|}]
+(* fail? *)
+let f (n : < m : 'a. [< `Foo of 'a & int | `Bar] >) =
+  (n : < m : 'b. [< `Foo of 'b & int | `Bar] >)
+[%%expect{|
+Line 1:
+Error: Values do not match:
+         val f :
+           < m : 'a. [< `Bar | `Foo of 'a & int ] as 'c > -> < m : 'b. 'c >
+       is not included in
+         val f :
+           < m : 'a. [< `Bar | `Foo of 'b & int ] as 'c > -> < m : 'b. 'c >
+|}]
 
 (* PR#6171 *)
 let f b (x: 'x) =