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
```