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 BE01C7EF10 for ; Tue, 24 Feb 2015 19:26:48 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of dra-news@metastack.com) identity=pra; client-ip=62.13.149.81; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of dra-news@metastack.com designates 62.13.149.81 as permitted sender) identity=mailfrom; client-ip=62.13.149.81; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.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@outmail149081.authsmtp.net) identity=helo; client-ip=62.13.149.81; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="postmaster@outmail149081.authsmtp.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BdAQDYwexUnFGVDT5bDoJWdFoEsEIGkkyFeAKBLEMBAQEBAQEQAQEBAQEIFAlChA8BAQEDAQMkEz8FCwIBCA4KChQQMiUBAQQODYgfCQPUegEBAQEGAQEBAQEBARuGB4UMhD0xB4MXgRQFjWSFUoVlAYEagxWLSYM+g1M9b4FEfwEBAQ X-IPAS-Result: A0BdAQDYwexUnFGVDT5bDoJWdFoEsEIGkkyFeAKBLEMBAQEBAQEQAQEBAQEIFAlChA8BAQEDAQMkEz8FCwIBCA4KChQQMiUBAQQODYgfCQPUegEBAQEGAQEBAQEBARuGB4UMhD0xB4MXgRQFjWSFUoVlAYEagxWLSYM+g1M9b4FEfwEBAQ X-IronPort-AV: E=Sophos;i="5.09,640,1418079600"; d="scan'208";a="123225627" Received: from outmail149081.authsmtp.net ([62.13.149.81]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Feb 2015 19:26:48 +0100 Received: from mail-c235.authsmtp.com (mail-c235.authsmtp.com [62.13.128.235]) by punt18.authsmtp.com (8.14.2/8.14.2/) with ESMTP id t1OIQjkL069464; Tue, 24 Feb 2015 18:26:45 GMT Received: from romulus.metastack.com (cpc1-cmbg5-0-0-cust241.5-4.cable.virginm.net [81.98.252.242]) (authenticated bits=0) by mail.authsmtp.com (8.14.2/8.14.2/) with ESMTP id t1OIQhnM076107; Tue, 24 Feb 2015 18:26:43 GMT Received: from remus.metastack.local (remus.metastack.com [172.16.0.1]) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id t1OIQhdl013949 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=FAIL); Tue, 24 Feb 2015 18:26:43 GMT Received: from Remus.metastack.local ([fe80::547c:3c42:e1da:eda2]) by Remus.metastack.local ([fe80::547c:3c42:e1da:eda2%10]) with mapi id 14.03.0224.002; Tue, 24 Feb 2015 18:26:43 +0000 From: David Allsopp To: Leo White CC: OCaml List Thread-Topic: [Caml-list] Match error with abstract types in modules Thread-Index: AdBQVu0mHoJ7Sr46RUmuhYPLJuzpGwABRyFWAABNT5A= Date: Tue, 24 Feb 2015 18:26:41 +0000 Message-ID: References: <000401d05056$ed605f70$c8211e50$@metastack.com> <87wq372noc.fsf@study.localdomain> In-Reply-To: <87wq372noc.fsf@study.localdomain> Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [172.16.0.18] Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Organization: MetaStack Solutions Ltd. X-Scanned-By: MIMEDefang 2.65 on 172.16.0.20 X-Server-Quench: af44f72d-bc52-11e4-b396-002590a15da7 X-AuthReport-Spam: If SPAM / abuse - report it at: http://www.authsmtp.com/abuse X-AuthRoute: OCd1ZAARAlZZVg1f DC4bFwdFRBksPQFF ChxFJgxfNl8UURhQ KkJXbgASJgdAAn9U UXkJW1VRQFx5U2Fz YQ5VIw1cfENGQQdv UlZLRlBNFgB3AVJF B2FnM0EsCgVBfn9w YghlX3hZEhUscUIr RUwACD9VYGV9aWFK VF0KdApSbQNKfBpM agF+USdcZitlE3Bw LCQ6OjR0OTRENBEd ZwgRJlJaTFwRGSR0 WBEeHX0mF1YZXSw4 M1Q6O0YRBw4QNA03 Nlc8XV8DWwA8 X-Authentic-SMTP: 61633634383431.1023:706 X-AuthFastPath: 0 (Was 255) X-AuthSMTP-Origin: 81.98.252.242/25 X-AuthVirus-Status: No virus detected - but ensure you scan with your own anti-virus system. Subject: RE: [Caml-list] Match error with abstract types in modules Leo White wrote: > > Please could someone remind me what it is about types in modules which > > means that > > > > module Foo =3D struct > > type 'a foo > > end > > > > type _ t =3D A : int Foo.foo t > > | B : float Foo.foo t > > > > let foo A =3D () > > > > is non-exhaustive pattern matching, but: > > > > type 'a bar > > > > type _ u =3D C : int bar u > > | D : float bar u > > > > let bar C =3D () > > > > is exhaustive? Or is it actually a bug (given that foo B is a type > error)? > > >=20 > If Foo is replaced with: >=20 > module Foo : sig > type 'a foo > end =3D struct > type 'a foo =3D unit > end >=20 > so that `int foo` is equal to `float foo`, then your match isn't really > exhaustive. How so? What's (very) confusing to me is that it seems to permit nonsensica= l matches without warning. In both the unconstrained and constrained versio= ns of Foo, the resulting type of the function [foo] is [int Foo.foo t -> un= it] so [foo B] is always rejected. But you get no warning about an unusable= match case with: let foo =3D function A -> () | B -> () although=20 let foo =3D function A | B -> () unsurprisingly does not type. > In the second version, the compiler cheats. Since `bar` is definied in the > same module, it knows that the abstract `bar` type it can see is actually > the definition, not just an abstraction of a type defined elsewhere, so it > knows that `int bar` cannot equal `float bar`. >=20 > Personally, I dislike this behaviour and would prefer both cases to give > an error. What's to dislike? It's rather useful - the constructors of a GADT are part= ionable by type. What caught me out was that two constructors with distinct= types (in my actual use with different instantiations of 'a BatSet.t) were= being regarded as equal in terms of pattern matching. I'd be quite happy i= f a type annotation were necessary to make it explicit that I meant to do i= t: let foo (key : int Foo.foo t) =3D match key with A -> () Especially with that explicit type, I find it very odd to get a warning abo= ut a constructor whose type is not permitted in this context and so cannot = be matched. Ta for the explanation behind the difference in behaviour, regardless! David