(* TEST
   * expect
*)

type 'a t = T of 'a
type 'a s = S of 'a

type (_, _) eq = Refl : ('a, 'a) eq;;

let f : (int s, int t) eq -> unit = function Refl -> ();;

module M (S : sig type 'a t = T of 'a type 'a s = T of 'a end) =
struct let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> () end;;
[%%expect{|
type 'a t = T of 'a
type 'a s = S of 'a
type (_, _) eq = Refl : ('a, 'a) eq
Line 6, characters 45-49:
6 | let f : (int s, int t) eq -> unit = function Refl -> ();;
                                                 ^^^^
Error: This pattern matches values of type (int s, int s) eq
       but a pattern was expected which matches values of type
         (int s, int t) eq
       Type int s is not compatible with type int t
|}];;