# type ('a, 'b) eq = Refl : ('a, 'a) eq;;
type ('a, 'b) eq = Refl : ('a, 'a) eq

# module M : sig type 'a t val eq : ('a t, 'b t) eq val v : string t end = struct type 'a t = int let eq = Refl let v = 2 end;;
module M : sig type 'a t val eq : ('a t, 'b t) eq val v : string t end

# let f (type a b) (Refl : (a M.t, b M.t) eq) (x: a M.t) : b M.t = x;;
Line 1, characters 65-66:
Error: This expression has type a M.t but an expression was expected of type
         b M.t
       Type a is not compatible with type b

# let f2 (type b) (Refl : (string M.t, b) eq) : b = M.v;;
val f2 : (string M.t, 'b) eq -> 'b = <fun>

# let f3 (Refl : (string M.t, int M.t) eq) : int M.t = M.v;;
Line 1, characters 53-56:
Error: This expression has type string M.t
       but an expression was expected of type int M.t
       Type string is not compatible with type int