How to use GADTs across modules in OCaml without raising warnings?

Question

I have two files: gadt1.ml and gadt2.ml and the second depends on the first.

gadt1.ml:

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
let get1 : bool t1 -> bool = function B1 -> true
let get2 : bool t2 -> bool = function B2 -> true

gadt2.ml:

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true

when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a warning 8 about the function Gadt2.get1 not being exhaustive. I am quite puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2 don't.

My assumption was that the empty type never cannot be equal to bool so Gadt2.get1 should not raise a warning. On the other hand, if I call Gadt2.get1 with argument A1, I get a type error (as desired). Is the warning expected behaviour or a bug? What did I miss?

By the way, adding -principal to the compile flags does not change anything.

Answer 1

Gadt2 can only see the interface of Gadt1, not its implementation. The interface looks something like this:

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
val get1 : bool t1 -> bool
val get2 : bool t2 -> bool

Note that type never is abstract -- there's nothing to stop an implementation giving it a RHS. In particular, you could, inside gadt1.ml, write type never = bool, at which point it becomes reasonable to pass A1 to get1, and so get1 needs to be prepared for that possibility.

By contrast, string is a non-abstract type: it has a known representation, so it can't possibly be equal to bool, and so A2 could never be passed to get2.

What you seem to be trying to do with never is declare a type which is not abstract but empty, exposing its representation as having no constructors at all. Unfortunately that just isn't well-supported by OCaml; the ability to define a type that locally the compiler can tell is empty is a bit of a quirk, and not really mentioned in the manual. There's no way to express "this type is empty" in a module signature.

update: my belief is that this has since changed, and you can now write:

type never = |

to indicate that never really is an empty type, and not an abstract one.

Answer 2

As Ben says, the problem is that in a signature type t is abstract rather than empty. One alternative is to define a type that is uninhabited:

module One = struct
  type never = { impossible : 'a . 'a }
  type _ t1 = A1 : never  t1 | B1 : bool t1
  type _ t2 = A2 : string t2 | B2 : bool t2
  let get1 : bool t1 -> bool = function B1 -> true
  let get2 : bool t2 -> bool = function B2 -> true
end

module Two = struct
  let get1 : bool One.t1 -> bool = function One.B1 -> true
  let get2 : bool One.t2 -> bool = function One.B2 -> true
end

This doesn't give any exhaustiveness warnings.