The following program fails to type-check:
type ('a, 'b) eq = | Eq : ('a, 'a) eq module M : sig type x = unit type 'a y val eq : (x, 'a y) eq end = struct type x = unit type 'a y = unit let eq = Eq end let f (x : M.x) : unit M.y = let Eq = (M.eq : (M.x, unit M.y) eq) in x (* This expression has type M.x = unit but an expression was expected of type unit M.y *)
However, removing either the manifest of type
x from the signature (making
type x abstract) or the phantom variable
'a from type
y makes the program type-check again.
Currently, I am circumventing this limitation by calling an explicit
cast function, but I wonder why there is a type error here and if there would be a more elegant solution.
let cast : type a b . (a, b) eq -> a -> b = fun Eq -> Fun.id let f (x : M.x) : unit M.y = cast M.eq x