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

[Ben Millwood <bmillwood@janestreet.com>]

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

I answered the SO question, with broadly the same answer as everyone else
gave. This issue has come at least twice before on this mailing list -- I
feel like there really is a missing feature here in terms of proper support
for empty types.

I'll advance on others' advice by pointing out that if you say:

type never = private [`never]

then you neither "use up" a constructor name nor is it possible to write an
expression with type never. Unfortunately, the compiler still doesn't
realise that, so it doesn't help you for pattern-matching.

On 13 October 2015 at 14:09, Philippe Veber <philippe.veber@gmail.com>
wrote:

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

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