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

module M1 : sig
  type t
  val is_int : t -> (t, int) eq
end = struct
  type t = int
  let is_int (x: t) = (Eq: (t, int) eq)
end

let foo' (type t) (x: t) (e: (t, int) eq) =
  let Eq = e in x + 1

let foo (x: M1.t) =
  foo' x (M1.is_int x)

(*let bar' (x: M1.t) (e: (M1.t, int) eq) =
  let Eq = e in x + 1*)
(*Error: This expression has type M1.t but an expression was expected of type
         int
*)