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

[Stefan Holdermans <stefan@vectorfabrics.com>]

Abdallah,

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

I suppose that, from the perspective of ‘Gadt2', ‘Gadt1.never’ is an abstract datatype that *could* have been implemented by ‘Gadt1’ as

  type never = bool

Perhaps there’s a design priciple emerging here? Concrete GADTs do not mix well with abstract type arguments.

Cheers,

  Stefan