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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/10/13 14:27, Abdallah Saffidine wrote:
> 
> 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?

A explained by Stefan, abstract types coming from other modules cannot be proved distinct.
Only predefined types such as string or array are handled specially.

The simplest solution is to add a constructor to your type:

	type never = Never

Better to do it when in the same module too.

Jacques Garrigue