From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 AB0057ED99 for ; Wed, 27 May 2015 17:43:41 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of aalekseyev@janestreet.com) identity=pra; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="aalekseyev@janestreet.com"; x-sender="aalekseyev@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of aalekseyev@janestreet.com designates 38.105.200.112 as permitted sender) identity=mailfrom; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="aalekseyev@janestreet.com"; x-sender="aalekseyev@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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="aalekseyev@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CrAQBs5WVVnHDIaSZcg2ReBoMZr2KOOIICAQmFdwKBNgc8EAEBAQEBAQERAQEBAQEGFglPhCIBAQEDARIRBBkBAR4OCwEECwsLAwoNHQICIhIBBQEKEgYTEhCHdgMKCAMKoFw+MYpOcIRkAQWaNgOEewEBAQEBAQQBAQEBAQEBAQETBgqLMIUBBAeCLTsSgTOFTwqRaYZagSk+kW+CDxIjgRWBBIMYboJHAQEB X-IPAS-Result: A0CrAQBs5WVVnHDIaSZcg2ReBoMZr2KOOIICAQmFdwKBNgc8EAEBAQEBAQERAQEBAQEGFglPhCIBAQEDARIRBBkBAR4OCwEECwsLAwoNHQICIhIBBQEKEgYTEhCHdgMKCAMKoFw+MYpOcIRkAQWaNgOEewEBAQEBAQQBAQEBAQEBAQETBgqLMIUBBAeCLTsSgTOFTwqRaYZagSk+kW+CDxIjgRWBBIMYboJHAQEB X-IronPort-AV: E=Sophos;i="5.13,506,1427752800"; d="scan'208";a="155539306" Received: from mxout1.mail.janestreet.com ([38.105.200.112]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 27 May 2015 17:43:40 +0200 Received: from tot-qpr-mailcore1.delacy.com ([172.27.56.68] helo=tot-qpr-mailcore1) by mxout1.mail.janestreet.com with smtp (Exim 4.82) (envelope-from ) id 1YxdUa-00042A-4X for caml-list@inria.fr; Wed, 27 May 2015 11:43:40 -0400 X-JS-Flow: external Received: by tot-qpr-mailcore1 with JS-mailcore (0.1) (envelope-from ) id BVZeYs-AAADHe-D8; 2015-05-27 11:43:40.127170-04:00 Received: from mail-wg0-f50.google.com ([74.125.82.50]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1YxdUZ-0007UG-TD for caml-list@inria.fr; Wed, 27 May 2015 11:43:40 -0400 Received: by wgbgq6 with SMTP id gq6so13287673wgb.3 for ; Wed, 27 May 2015 08:43:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=QkJ0v0MorHYZpP9Tnz+sOna5DHB+hvkVGPSzL4x67+s=; b=YpD6dRhju7J3a3GKuruDaAMYbrNDtPfrvWkUF8j8LwRH37DHd8OxoIl+9/TxuxzsoD OfhUH6NkWwJWc33l7+Xuob+I552v3kE6vlMiMt+doqj/8bfurZMEJeyzhjTln6ciXSkG rp2xR5FhzxUkRRURGDr/0D9TyIAIHIAa7h0TU= 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:date :message-id:subject:from:to:cc:content-type; bh=QkJ0v0MorHYZpP9Tnz+sOna5DHB+hvkVGPSzL4x67+s=; b=Lv6Arr94RvUVY88qdpszpPJj/ZrvojKBYxfBdsDna2FFb1BPcljNoWKgfmXHhma0nQ dBG2NapcEKTbVXuwsS+uZEjE8pQTMrPpgMA/97v397KLPS7soDDJPtrAo0NAsXusScj5 ZKCKg4Kamh3Eib5Ey2kHjOTsf4S4rf/NlYehDer9ITvmPN9OFeaiLoT/Cm24kJo5tNvp IOquqDue3JwhFSpoaSRrmWP18JsMLWV4ZjnyylcH9kOsQPJuwid9LSx+0zTe8WwmxNw9 zsFTj9qoOdi9MHSSuvWshzRWMqNh1/c73+Dg9Kr1MD6cSaNQBxUpsD7CJAYvSXvAZ06X JDhw== X-Gm-Message-State: ALoCoQnaGnOMA8bs6DX3Cg44nFImnK4HMfZpYE1cWTO84D5napw4j0wxrFLq23xASj2spbEw7gHvgwiRpO5wkuASMTzqMRLSHF6PD7VoGeQ0mD2lUQtwTaHcQybEuD72TVuO/+ZePcpA X-Received: by 10.194.59.46 with SMTP id w14mr44960477wjq.106.1432741419171; Wed, 27 May 2015 08:43:39 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.194.59.46 with SMTP id w14mr44960458wjq.106.1432741419060; Wed, 27 May 2015 08:43:39 -0700 (PDT) Received: by 10.27.184.196 with HTTP; Wed, 27 May 2015 08:43:38 -0700 (PDT) In-Reply-To: References: <5565DD11.6080608@giovannangeli.fr> Date: Wed, 27 May 2015 16:43:38 +0100 Message-ID: From:Arseniy Alekseyev To:Ben Millwood Cc:Joris Giovannangeli , caml users Content-Type: multipart/alternative; boundary=047d7ba976c856a9d30517121b50 X-JS-Processed-by: mailcore Subject: Re: [Caml-list] Matching exhausitvity with GADT and modules --047d7ba976c856a9d30517121b50 Content-Type: text/plain; charset=UTF-8 Interestingly, giving names to constructors is not sufficient. You must give *distinct* names. In particular, the following produces a warning for [g], but not for [f]: module A= struct type foo = T type bar = T type 'a gadt = Foo : int -> foo gadt | Bar : int -> bar gadt let f : foo gadt -> int = function | Foo i -> i end module B = struct open A let g : foo gadt -> int = function | Foo i -> i end Joris, I think you can still kind-of use this idea for abstract data types, at the cost of adding a wrapper type. In particular, this works: module A= struct type foo type bar type foo_marker = Foo of foo type bar_marker = Bar of bar type 'a gadt = Foo : int -> foo_marker gadt | Bar : int -> bar_marker gadt let f : foo_marker gadt -> int = function | Foo i -> i end module B = struct open A let g : foo_marker gadt -> int = function | Foo i -> i end On Wed, May 27, 2015 at 4:14 PM, Ben Millwood wrote: > This is a common problem that has annoyed me as well. The issue is that B > sees foo and bar as abstract types, so cannot be sure they are different, > so cannot be sure that a value of type foo gadt can't be constructed with > Bar. If you add explicit constructors for both currently-empty types, then > their inequality will be exposed and your pattern match should work. > > On 27 May 2015 at 16:04, Joris Giovannangeli > wrote: > >> Hi, >> >> The following snippet is compiling without warning : >> >> module A = struct >> >> type foo >> type bar >> >> type 'a gadt = >> Foo : int -> foo gadt >> | Bar : int -> bar gadt >> >> let f = function >> | Foo i -> i >> end >> >> But if I split the code into two modules : >> >> module A = struct >> >> type foo >> type bar >> >> type 'a gadt = >> Foo : int -> foo gadt >> | Bar : int -> bar gadt >> >> end >> >> module B = struct >> include A >> >> let f : foo gadt -> int = function >> | Foo i -> i >> end >> >> I get the following warning : >> >> Warning 8: this pattern-matching is not exhaustive. >> Here is an example of a value that is not matched: >> Bar _ >> >> How can i work around this issue ? As far as i can tell, it is not >> possible for Bar to be matched by the function f. >> >> Best regards, >> joris >> >> >> -- >> Caml-list mailing list. Subscription management and archives: >> https://sympa.inria.fr/sympa/arc/caml-list >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs > > > --047d7ba976c856a9d30517121b50 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Interestingly, giving names to constructors is not su= fficient. You must give *distinct* names. In particular, the following prod= uces a warning for [g], but not for [f]:

module A= =3D struct

=C2=A0 type foo =3D T
=C2=A0 = type bar =3D T

=C2=A0 type 'a gadt =3D
=C2=A0 =C2=A0 =C2=A0 Foo : int -> foo gadt
=C2=A0 =C2=A0 | = Bar : int -> bar gadt

=C2=A0 let f : foo gadt -= > int =3D function
=C2=A0 =C2=A0 =C2=A0| Foo i -> i

end

module B =3D struct
=C2=A0 open A

=C2=A0 let g : foo gadt -> int = =3D function
=C2=A0 =C2=A0 =C2=A0| Foo i -> i
end

Joris, I think you can still kind-of use= this idea for abstract data types, at the cost of adding a wrapper type. I= n particular, this works:

module A=3D st= ruct

=C2=A0 type foo
=C2=A0 type bar
=C2=A0 type foo_marker =3D Foo of foo
=C2=A0 type bar_mark= er =3D Bar of bar

=C2=A0 type 'a gadt =3D
=C2=A0 =C2=A0 =C2=A0 Foo : int -> foo_marker gadt
=C2=A0= =C2=A0 | Bar : int -> bar_marker gadt

=C2=A0 l= et f : foo_marker gadt -> int =3D function
=C2=A0 =C2=A0 =C2= =A0| Foo i -> i

end

mo= dule B =3D struct
=C2=A0 open A

=C2=A0 l= et g : foo_marker gadt -> int =3D function
=C2=A0 =C2=A0 =C2= =A0| Foo i -> i
end


<= /div>

On Wed= , May 27, 2015 at 4:14 PM, Ben Millwood <bmillwood@janestreet.com> wrote:
Thi= s is a common problem that has annoyed me as well. The issue is that B sees= foo and bar as abstract types, so cannot be sure they are different, so ca= nnot be sure that a value of type foo gadt can't be constructed with Ba= r. If you add explicit constructors for both currently-empty types, then th= eir inequality will be exposed and your pattern match should work.

<= br>

--047d7ba976c856a9d30517121b50--