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