GADTs, phantom variables and type aliases

Learning
1

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
2

Are you on 4.10 ? Looks related to https://github.com/ocaml/ocaml/pull/9040.

Best,
Nicolás

3

Thank you, @nojb, for the reference. I am using OCaml version 4.11.0+rc1 (but I observed the same limitation in previous versions of OCaml).

4

Equations (M.x = _ M.y) can only be added on abstract types and M.x is not abstract. Using a cast function is the elegant solution as far as I can see.

5

Thank you, @octachron! I forgot this rule!