(* TEST
 expect;
*)

type i = <m : 'c. 'c -> 'c >
type ('a, 'b) j = <m : 'c. 'a -> 'b >
type _ t = A : i t;;
[%%expect{|
type i = < m : 'c. 'c -> 'c >
type ('a, 'b) j = < m : 'a -> 'b >
type _ t = A : i t
|}]

let f (type a b) (y : (a, b) j t) : a -> b =
  let A = y in fun x -> x;;
[%%expect{|
Line 2, characters 6-7:
2 |   let A = y in fun x -> x;;
          ^
Error: This pattern matches values of type "i t"
       but a pattern was expected which matches values of type "(a, b) j t"
       Type "i" = "< m : 'c. 'c -> 'c >" is not compatible with type
         "(a, b) j" = "< m : a -> b >"
       The method "m" has type "'c. 'c -> 'c", but the expected method type was
       "a -> b"
       The universal variable "'c" would escape its scope
|}]

let g (type a b) (y : (a,b) j t option) =
  let None = y in () ;;
[%%expect{|
val g : ('a, 'b) j t option -> unit = <fun>
|}]

module M = struct
  type 'a d = D
  type j = <m : 'c. 'c -> 'c d >
end ;;
let g (y : M.j t option) =
  let None = y in () ;;
[%%expect{|
module M : sig type 'a d = D type j = < m : 'c. 'c -> 'c d > end
val g : M.j t option -> unit = <fun>
|}]

module M = struct
  type 'a d
  type j = <m : 'c. 'c -> 'c d >
end ;;
let g (y : M.j t option) =
  let None = y in () ;;
[%%expect{|
module M : sig type 'a d type j = < m : 'c. 'c -> 'c d > end
Line 6, characters 2-20:
6 |   let None = y in () ;;
      ^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: "Some A"

val g : M.j t option -> unit = <fun>
|}]

module M = struct
  type e
  type 'a d
  type i = <m : 'c. 'c -> 'c d >
  type j = <m : 'c. 'c -> e >
end ;;
type _ t = A : M.i t
let g (y : M.j t option) =
  let None = y in () ;;
[%%expect{|
module M :
  sig
    type e
    type 'a d
    type i = < m : 'c. 'c -> 'c d >
    type j = < m : 'c. 'c -> e >
  end
type _ t = A : M.i t
Line 9, characters 2-20:
9 |   let None = y in () ;;
      ^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: "Some A"

val g : M.j t option -> unit = <fun>
|}]

module M = struct
  type 'a d
  type i = <m : 'c. 'c -> 'c d >
  type 'a j = <m : 'c. 'c -> 'a >
end ;;
type _ t = A : M.i t
(* Should warn *)
let g (y : 'a M.j t option) =
  let None = y in () ;;
[%%expect{|
module M :
  sig
    type 'a d
    type i = < m : 'c. 'c -> 'c d >
    type 'a j = < m : 'c. 'c -> 'a >
  end
type _ t = A : M.i t
Line 9, characters 2-20:
9 |   let None = y in () ;;
      ^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: "Some A"

val g : 'a M.j t option -> unit = <fun>
|}]

(* more examples by @lpw25 *)
module M = struct
  type a
  type i = C of <m : 'c. 'c -> 'c >
  type j = C of <m : 'c. 'c -> a >
end
type _ t = A : M.i t;;
let f (y : M.j t) = match y with _ -> .;;
[%%expect{|
module M :
  sig
    type a
    type i = C of < m : 'c. 'c -> 'c >
    type j = C of < m : 'c. 'c -> a >
  end
type _ t = A : M.i t
val f : M.j t -> 'a = <fun>
|}]

module M = struct
  type a
  type i = C of <m : 'c. 'c -> 'c -> 'c >
  type j = C of <m : 'c. 'c -> a >
end
type _ t = A : M.i t;;
let f (y : M.j t) = match y with _ -> .;;
[%%expect{|
module M :
  sig
    type a
    type i = C of < m : 'c. 'c -> 'c -> 'c >
    type j = C of < m : 'c. 'c -> a >
  end
type _ t = A : M.i t
val f : M.j t -> 'a = <fun>
|}]

module M = struct
  type 'a a
  type i = C of <m : 'c. 'c -> 'c -> 'c >
  type j = C of <m : 'c. 'c -> 'c a >
end
type _ t = A : M.i t;;
let f (y : M.j t) = match y with _ -> .;;
[%%expect{|
module M :
  sig
    type 'a a
    type i = C of < m : 'c. 'c -> 'c -> 'c >
    type j = C of < m : 'c. 'c -> 'c a >
  end
type _ t = A : M.i t
Line 7, characters 33-34:
7 | let f (y : M.j t) = match y with _ -> .;;
                                     ^
Error: This match case could not be refuted.
       Here is an example of a value that would reach it: "A"
|}]

module rec M: sig
  type x
  type 'a t = A constraint 'a = <x: 'a. 'a -> x >
end = struct
  type x
  type 'a t = A constraint 'a = <x:'a. 'a -> 'a >
end
[%%expect {|
Lines 4-7, characters 6-3:
4 | ......struct
5 |   type x
6 |   type 'a t = A constraint 'a = <x:'a. 'a -> 'a >
7 | end
Error: Signature mismatch:
       Modules do not match:
         sig
           type x = M.x
           type 'b t = 'b M.t = A constraint 'b = < x : 'a. 'a -> 'a >
         end
       is not included in
         sig type x type 'b t = A constraint 'b = < x : 'a. 'a -> x > end
       Type declarations do not match:
         type 'b t = 'b M.t = A constraint 'b = < x : 'a. 'a -> 'a >
       is not included in
         type 'b t = A constraint 'b = < x : 'a. 'a -> x >
       Their parameters differ
       The type "< x : 'a. 'a -> 'a >" is not equal to the type
         "< x : 'a. 'a -> x >"
       Type "'a" is not equal to type "x" = "M.x"
       The method "x" has type "'a. 'a -> 'a", but the expected method type was
       "'a. 'a -> x"
|}]
