Hi Abdallah,

  I came across the very same observation a few days ago. I'm not an expert on typing but here's how I understand it: in gadt1.ml the declaration of never makes it clear it is an empty type, which in particular is different from bool. Now the signature of Gadt1 as seen by Gadt2 is:

module Gadt1 : sig
  type never
  type _ t1 = A1 : never t1 | B1 : bool t1
  [...]
end

This implies that Gadt2 doesn't see Gadt1.never as an empty type, but rather as an abstract type, and so has no indication that it is different from bool. The signature could as well be hiding a definition like type never = bool. So in Gadt2, the exhaustiveness checker has no way to do its job, hence the puzzling behavior you observe.

In my case I changed the definition of my phantom types from empty to polymorphic variant types and made them explicit in the signature of the module.

module Gadt1 : sig
  type never = [`never]
  [...]
end

I hope this intuitive explanation is not too far from the truth :o)!

Cheers,
  Philippe.


2015-10-13 7:27 GMT+02:00 Abdallah Saffidine <abdallah.saffidine@gmail.com>:
Hi all,

I am reposting this SO question. 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 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?