[Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Abdallah Saffidine <abdallah.saffidine@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1135 bytes --]

Hi all,

I am reposting this SO question
<http://stackoverflow.com/questions/33093807/how-to-use-gadts-across-modules-in-ocaml-without-raising-warnings>.
I suspect there might be a bug in the implementation of Warning 8.

Thanks,
Abdallah

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

gadt1.ml:

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

gadt2.ml:

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> truelet 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?

[-- Attachment #2: Type: text/html, Size: 3492 bytes --]