From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 2EE1C7ED1D for ; Tue, 13 Oct 2015 08:16:10 +0200 (CEST) IronPort-PHdr: 9a23:OekvqhQc2bTH7XfqMbf+36nEQdpsv+yvbD5Q0YIujvd0So/mwa64bByN2/xhgRfzUJnB7Loc0qyN4/ymCTZLu8ja+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8GVM18D3mTmKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayV+0CQLdZFDUrNXwurI2u7EGbDFjH2nxJamUXlhtQGwWN0hzwU4255jP6t+58wDGXe9P7R70ucTun5qZvDhTvjXFUGSQ+9TT9h8o4qaNfpA2moBA3l4TRYYWRK/15covfdNUXXnZbU8tNESdGB9XvPMM0E+MdMLMA/MHGrFwUoE77XFH0CQ== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bmillwood@janestreet.com; spf=Pass smtp.mailfrom=bmillwood@janestreet.com; spf=None smtp.helo=postmaster@mxout4.mail.janestreet.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of bmillwood@janestreet.com) identity=pra; client-ip=38.105.200.233; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of bmillwood@janestreet.com designates 38.105.200.233 as permitted sender) identity=mailfrom; client-ip=38.105.200.233; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mxout4.mail.janestreet.com) identity=helo; client-ip=38.105.200.233; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout4.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0B9AgCBoBxWnOnIaSZdg3puBq0BknElgm6CCn8CgTQHOxEBAQEBAQEBARABAQEBAQYWCU+CH4IIAQEDARIRBBkBASkDCwEECwsLNwICIQESAQUBHAYTIod3AwoIAwqeeoExPjGKWHGEZQEFiUoNhRkBAQEBAQEBAQEBAQEBAQEBAQEBAQERBgqGa4R+glCCPQeCaYFFjRN1iBKFGYYNgXSCIJIchX0SI4EXESaCMA0WBxaBS2SGcQEBAQ X-IPAS-Result: A0B9AgCBoBxWnOnIaSZdg3puBq0BknElgm6CCn8CgTQHOxEBAQEBAQEBARABAQEBAQYWCU+CH4IIAQEDARIRBBkBASkDCwEECwsLNwICIQESAQUBHAYTIod3AwoIAwqeeoExPjGKWHGEZQEFiUoNhRkBAQEBAQEBAQEBAQEBAQEBAQEBAQERBgqGa4R+glCCPQeCaYFFjRN1iBKFGYYNgXSCIJIchX0SI4EXESaCMA0WBxaBS2SGcQEBAQ X-IronPort-AV: E=Sophos;i="5.17,676,1437429600"; d="scan'208";a="182464276" Received: from mxout4.mail.janestreet.com ([38.105.200.233]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 13 Oct 2015 08:16:09 +0200 Received: from tot-qpr-mailcore2.delacy.com ([172.27.56.106] helo=tot-qpr-mailcore2) by mxout4.mail.janestreet.com with esmtps (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.82) (envelope-from ) id 1ZlssZ-0003Vn-W5 for caml-list@inria.fr; Tue, 13 Oct 2015 02:16:08 -0400 X-JS-Flow: external Received: by tot-qpr-mailcore2 with JS-mailcore (0.1) (envelope-from ) id BWHKGn-AAABXA-d1; 2015-10-13 02:16:07.955635-04:00 Received: from mail-lb0-f182.google.com ([209.85.217.182]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1ZlssZ-0003S7-Ll for caml-list@inria.fr; Tue, 13 Oct 2015 02:16:07 -0400 Received: by lbbk10 with SMTP id k10so7631031lbb.0 for ; Mon, 12 Oct 2015 23:16:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=A8XUayz7IVR5r8w4FLNnBVsy/HP2Xqpi9Rq2b5bP0f8=; b=CKLd3L/3bmwlcJNeZuLfmUMUpklCzy17AbG49a7/4g6UCHa6GmkgLG7uFq/dVzzMSL dGdO3zz/h17324eWCwg5d08Dae7w0y4rtxBEwDVmyWTDH7FAXjfajZfRMt7qU9lhNy2K VedBDQs/fMqGhtND3VNEiK7e4hKNxPn7NUYHY= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-type; bh=A8XUayz7IVR5r8w4FLNnBVsy/HP2Xqpi9Rq2b5bP0f8=; b=cGuMjHWpcwMmxgMcg2TcAFW37dFquYFa6fipLqLIGPPv2wJwyqy6/qYVv0K3TXHxHO ZfzzFIpRmmDtGiO81tYfy5Qb582cGgWOfBlahOCp4bJp/UVzRsFkLfj54DhH5nmJyyQq n05TYK+1CoqaxGTDCK4EOzXbmDmo4/upjrZlzqie2UrhSfLnN7QUQ/CgSiWXDclV75PY IeE2IUFRlPMqv3a5XcDN3hXOGJGAj582k2jVVQ2SBRpa6IL6Txt6nQNPIvYhK1yWQ5U2 rTP3snGLAuegs+lw/8wbEJdEQR87IiNdPonIkn7pRJlbGMzLJBCVjoXMiW8KvKAOjk8I YWjw== X-Gm-Message-State: ALoCoQkBS805oRU5FDz28qSeNBtpmLH9wnaLHiH1kvrHrpjpH4djOdEnjGscSDI2YrlRPhYnAGh4sDWB2bH9BI/O1RPiTK8jE9AwnhsvEnRK3pTr0Od/r+DriHrqgu9i7+tTvwyHyfIZ X-Received: by 10.25.22.146 with SMTP id 18mr9376000lfw.8.1444716966653; Mon, 12 Oct 2015 23:16:06 -0700 (PDT) X-Received: by 10.25.22.146 with SMTP id 18mr9375995lfw.8.1444716966422; Mon, 12 Oct 2015 23:16:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.137.137 with HTTP; Mon, 12 Oct 2015 23:15:46 -0700 (PDT) In-Reply-To: References: From:Ben Millwood Date: Tue, 13 Oct 2015 14:15:46 +0800 Message-ID: To:Philippe Veber Cc:Abdallah Saffidine , caml users Content-Type: multipart/alternative; boundary=001a114068d295cc2b0521f66185 X-JS-Processed-by: mailcore X-Sender-Copy: hkg-copy Subject: Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings? --001a114068d295cc2b0521f66185 Content-Type: text/plain; charset=UTF-8 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 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 >: > >> 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 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? >> >> > --001a114068d295cc2b0521f66185 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I answered the SO question, with broadly the same answer a= s everyone else gave. This issue has come at least twice before on this mai= ling list -- I feel like there really is a missing feature here in terms of= proper support for empty types.

I'll advance on oth= ers' advice by pointing out that if you say:

t= ype never =3D private [`never]

then you neither &q= uot;use up" a constructor name nor is it possible to write an expressi= on with type never. Unfortunately, the compiler still doesn't realise t= hat, 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= ,

=C2=A0 I came across the very same observation a few days ag= o. I'm not an expert on typing but here's how I understand it: in <= a href=3D"http://gadt1.ml" target=3D"_blank">gadt1.ml the declaration o= f never makes it clear it is an empty type, which in particular is differen= t from bool. Now the signature of Gadt1 as seen by Gadt2 is:

<= span style=3D"font-family:monospace,monospace">module Gadt1 : sig
=C2= =A0 type never
=C2=A0 type _ t1 = =3D A1 : never t1 | B1 : bool t1
= =C2=A0 [...]
end

This implies that Gadt2= doesn't see Gadt1.never as an empty type, but rather as an abstract ty= pe, and so has no indication that it is different from bool. The signature = could as well be hiding a definition like type never =3D bool. So in Gadt2,= the exhaustiveness checker has no way to do its job, hence the puzzling be= havior you observe.

In my case I ch= anged the definition of my phantom types from empty to polymorphic variant = types and made them explicit in the signature of the module.

<= div class=3D"gmail_extra">module Gadt1 := sig
=C2=A0 type never =3D [`never]
=C2=A0 [...]
end

I hope this intuitive explanation is no= t too far from the truth :o)!

Cheers,
=C2= =A0 Philippe.


2015-10-13 7:27 GMT+02:00 A= bdallah Saffidine <abdallah.saffidine@gmail.com>:=
Hi all,
I am reposting this SO question. I suspect there might be a bug in the implemen= tation of Warning 8.

Thanks,
Abdallah

I have two files: gadt1.= ml and gadt2.ml and t= he second depends on the first.

gadt1.ml:

type never
type _ t1 =3D A1 : never  t1 | B1 : bool t1
type _ t2 =3D A2 : string t2 | B2 : bool t2
let get1 : bool t1 -> bool =3D function B1 -> true=

let get2 : bool t2 -> bool =3D function B2 -> true=

gadt2.ml:

let get1 : bool Gad=
t1.t1 -> bool =3D function Gadt.B1 -> true<=
span>
let get2 : bool Gadt1.t2 -> bool =3D 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 a= m quite puzzled that Gadt2.get1 raises a warning while G= adt1.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 behavio= ur or a bug? What did I miss?




--001a114068d295cc2b0521f66185--