type nevermodule Gadt1 : sigHi 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:type _ t1 = A1 : never t1 | B1 : bool t1
[...]endThis 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 : sigtype never = [`never]
[...]endI 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>:AbdallahHi all,Thanks,
I am reposting this SO question. I suspect there might be a bug in the implementation of Warning 8.I have two files: gadt1.ml and gadt2.ml and the second depends on the first.
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
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 thatGadt2.get1
raises a warning whileGadt1.get1
andGadt2.get2
don't.My assumption was that the empty type
never
cannot be equal tobool
soGadt2.get1
should not raise a warning. On the other hand, if I callGadt2.get1
with argumentA1
, I get a type error (as desired). Is the warning expected behaviour or a bug? What did I miss?