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 EDFCC7ED99 for ; Wed, 27 May 2015 17:14:09 +0200 (CEST) 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.112; 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.112 as permitted sender) identity=mailfrom; client-ip=38.105.200.112; 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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CrAQBV3mVVnHDIaSZcg2ReBoMZr2GOOIICAQmFdwKBNgc8EAEBAQEBAQERAQEBAQEGFglPhCMBAQMBEhEEGQEBLAsBBAsLBAcaHQICIhIBBQEKEgYTEhCHdgMKCAMKoD8+MYpOcIRkAQWaNAOEewEBAQEBAQQBAQEBAQEBAQETBgqLMIUBBAeCLQwvEoEzhU8KkWmGWoEpPpFvgg8SI4EVgQSDGG6CRwEBAQ X-IPAS-Result: A0CrAQBV3mVVnHDIaSZcg2ReBoMZr2GOOIICAQmFdwKBNgc8EAEBAQEBAQERAQEBAQEGFglPhCMBAQMBEhEEGQEBLAsBBAsLBAcaHQICIhIBBQEKEgYTEhCHdgMKCAMKoD8+MYpOcIRkAQWaNAOEewEBAQEBAQQBAQEBAQEBAQETBgqLMIUBBAeCLQwvEoEzhU8KkWmGWoEpPpFvgg8SI4EVgQSDGG6CRwEBAQ X-IronPort-AV: E=Sophos;i="5.13,506,1427752800"; d="scan'208";a="155533899" 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:14:09 +0200 Received: from tot-qpr-mailcore2.delacy.com ([172.27.56.106] helo=tot-qpr-mailcore2) by mxout1.mail.janestreet.com with smtp (Exim 4.82) (envelope-from ) id 1Yxd1z-0008Gp-U7 for caml-list@inria.fr; Wed, 27 May 2015 11:14:07 -0400 X-JS-Flow: external Received: by tot-qpr-mailcore2 with JS-mailcore (0.1) (envelope-from ) id BVZd89-AAAGLh-Sm; 2015-05-27 11:14:05.596223-04:00 Received: from mail-qg0-f52.google.com ([209.85.192.52]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1Yxd1x-0006FR-HB for caml-list@inria.fr; Wed, 27 May 2015 11:14:05 -0400 Received: by qgf2 with SMTP id 2so4677264qgf.3 for ; Wed, 27 May 2015 08:14:05 -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=p9DTkJqKGrBVB6ogSHRM1f/VhX4DBL6HQLWCEXg+61s=; b=mJjENsi+UZzDm6cuJD7Jik3lA0JSgP4jcYup79Orwy3iadxmJF8Z0zvRHC20pDqu0X SIGo3aUYZUH4VyM1QsKRT5mRRJWe4jafGGL4vZmv4R6MijNiXQEor/P8/ez+Ku/9zlZh kzBRhkrTYcYHnbKjbVDd/xzc8CaaH6p4Sq+L4= 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=p9DTkJqKGrBVB6ogSHRM1f/VhX4DBL6HQLWCEXg+61s=; b=lhvJYqpwNMojxaNiFXhcunY3K5ZjorMA6N2BQv7w2ZGEV+zlyYL9J3CMmiG5OeZg5T 6WwJ/S+ZGIswyAW9jUgpbyk2kyI1kVrGsIOd8y/Wwx3FsnmuX8gqe4ye00cpbCFyyClM hi/HnJxeSfEzQks703gX+qsyGNsFwT5+clOsfTibz1spimH8YXWTayErFp9uwx/4BX7d fLDJx069bImcL5rhiaH784aQCdOxslJ2d7zxyrpyWMxBtM4HYl02Lc2aDUWcHzjGVjik Qir6OuCyydasWthfwFOH+cMLaQ0wcBPsxyo6TX13Q6HiT7/IZdhg/in+4tD0Szgbhtun kf8w== X-Gm-Message-State: ALoCoQlzEWNtUJLqt1Qfm84NhPvrMHXU2Khv92oWen1OjwpiWeuY+880yqrC6CTV+7H/OSDEydIfKX6wkGwPpfo7w4233hXWJwi8DBMRZ5KZ7/0FlvrUeSTvgnTps3ONgS65NIi3w/Ir X-Received: by 10.55.41.17 with SMTP id p17mr67175710qkh.86.1432739645238; Wed, 27 May 2015 08:14:05 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.55.41.17 with SMTP id p17mr67175682qkh.86.1432739645089; Wed, 27 May 2015 08:14:05 -0700 (PDT) Received: by 10.96.191.170 with HTTP; Wed, 27 May 2015 08:14:05 -0700 (PDT) In-Reply-To: <5565DD11.6080608@giovannangeli.fr> References: <5565DD11.6080608@giovannangeli.fr> Date: Wed, 27 May 2015 16:14:05 +0100 Message-ID: From:Ben Millwood To:Joris Giovannangeli Cc:caml users Content-Type: multipart/alternative; boundary=001a114068fc9a0c4a051711b1c0 X-JS-Processed-by: mailcore Subject: Re: [Caml-list] Matching exhausitvity with GADT and modules --001a114068fc9a0c4a051711b1c0 Content-Type: text/plain; charset=UTF-8 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 --001a114068fc9a0c4a051711b1c0 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
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 s= hould work.

= On 27 May 2015 at 16:04, Joris Giovannangeli <joris@giovannangeli.fr= > wrote:
Hi,

The following snippet is compiling without warning :

module A =3D struct

=C2=A0 type foo
=C2=A0 type bar

=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 =3D function
=C2=A0 =C2=A0 =C2=A0| Foo i -> i
end

But if I split the code into two modules :

module A =3D struct

=C2=A0 type foo
=C2=A0 type bar

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

end

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

=C2=A0 let f : foo gadt -> int =3D function
=C2=A0 =C2=A0 =C2=A0| 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.=C2=A0 Subscription management and archives:
ht= tps://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
<= br>
--001a114068fc9a0c4a051711b1c0--