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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id C72597EE20 for ; Sat, 17 Nov 2012 19:20:49 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=74.125.82.180; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 74.125.82.180 as permitted sender) identity=mailfrom; client-ip=74.125.82.180; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f180.google.com) identity=helo; client-ip=74.125.82.180; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-we0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AooCAEXUp1BKfVK0k2dsb2JhbABFhiC9BggjAQEBAQkJCwkUBCOCHgEBBSMEGQEbHQEDDAYFCw0CAiYCAiEBAREBBQEcBhMIh3IBAw+hAItkT4J4hCoKGScNWYh1AQUMgRaKKWmDeoETA5JKgV2BVYsygzAWKYQR X-IronPort-AV: E=Sophos;i="4.83,270,1352070000"; d="scan'208";a="181973853" Received: from mail-we0-f180.google.com ([74.125.82.180]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Nov 2012 19:20:49 +0100 Received: by mail-we0-f180.google.com with SMTP id t57so1807485wey.39 for ; Sat, 17 Nov 2012 10:20:49 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=Ck6sCQ99MhsDVb5VdKnsgdbiNOmo3vIwmCs4+hFNO8Q=; b=hELTxaD0Qz7/fqfnwJV2wZlzx3Xca+uHkgkYZc92E2I+9XZVpqIlZMX8boJWfj+Bps 5b0Bvgbvw/wfQ/8JGfEXGOUK33yyxYBGTZDp/9A7TJzWht5KPnMk1QUadNMmbnF/PL3H q5JYi/2qUQN0Gqst+Xx0aJwpJluGRMH9R6KjdDVQDbRJ38gCjL/Giz3B94wGwR0BzdLf Jg1tnqiqzkR1P3bumyqrWH8JSKkV4fl4Qpvx6ytpsobFquLP38g6FePCVTu2aHPI2cQ7 IshcW6lXh2JqL/soXR/LQpml500g24llMZnl45x1qIlVnI++6dqCn1lHkJEq/VrXjHLl +wbA== MIME-Version: 1.0 Received: by 10.180.92.132 with SMTP id cm4mr2879046wib.12.1353176448870; Sat, 17 Nov 2012 10:20:48 -0800 (PST) Received: by 10.194.58.101 with HTTP; Sat, 17 Nov 2012 10:20:48 -0800 (PST) In-Reply-To: <6E1FE11E-72C5-4AA7-B24A-7E83E139F30C@gmail.com> References: <6E1FE11E-72C5-4AA7-B24A-7E83E139F30C@gmail.com> Date: Sat, 17 Nov 2012 18:20:48 +0000 Message-ID: From: Jeremy Yallop To: Kaspar Rohrer Cc: caml-list@yquem.inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] GADT exhaustiveness check Dear Kaspar, On 17 November 2012 12:44, Kaspar Rohrer wrote: > I'm messing around with the new GADT feature in OCaml 4.0, trying to writ= e a (more or less) strongly typed EDSL. And I've run into non-exhaustive pa= ttern-matching warnings (see below for an example). I'm pretty sure that it= is just an inherent shortcoming of GADTs, not a bug. The workaround is eas= y as well, simply add a catch all clause with a runtime error to silence th= e warning, and prove manually that the offending patterns can not occur. [...] > module T : > sig > type 'a t > val int : int t > end > =3D > struct > type 'a t =3D () > let int =3D () > end > > type ('r,_) args =3D > | ANil : ('r,'r) args > | ACons : 'a * ('r,'b) args -> ('r,'a -> 'b) args > > let a =3D ANil > let b =3D ACons (3, ANil) > > type ('r,'a) fun' =3D > | FVoid : 'r T.t -> ('r,'r) fun' > | FLambda : 'a T.t * ('r,'b) fun' -> ('r,'a -> 'b) fun' > > let f =3D FVoid T.int > let g =3D FLambda (T.int, f) > > let rec apply : type r a . (r,a) fun' * (r,a) args -> unit =3D function > | FVoid t, ANil -> () > | FLambda (t,f), ACons (_,a) -> apply (f,a) > (* > Warning 8: this pattern-matching is not exhaustive. > Here is an example of a value that is not matched: > (FLambda (_, _), ANil) > *) Here's how you know that the offending pattern can never match a value: the ANil constructor would constrain "r" and "a" to denote the same type, and t= he arguments of the FLambda constructor would have types "'a T.t" and "('a -> = 'b, 'b) fun'" (for suitable 'a and 'b). It's then sufficient to show that at least one of these types is not inhabited. However, in order to show this = you need to use information about the possible ways of building values of those types: for example, you need to know that there's no polymorphic value of t= ype "'a t". If you add such a value to the T module: module T : sig type 'a t val int : int t val poly : 'a t end =3D struct type 'a t =3D () let int =3D () let poly =3D () end then you *can* build values that match the missing patterns: # apply (FLambda (T.int, FVoid T.poly), ANil) Exception: Match_failure ("//toplevel//", 113, 9). I don't think that the exhaustiveness checker has any information available regarding the possible ways of constructing values of an abstract type. Here's an example without GADTs illustrating the same issue. Suppose we ha= ve your original definition of the T module: module T : sig type 'a t val int : int t end =3D struct type 'a t =3D () let int =3D () end We can define a datatype with two constructors using T.t: type s =3D Int of int T.t | Float of float T.t Since there is no value of type "float T.t", patterns involving the Float constructor are redundant. However, the exhaustiveness checker doesn't know that, so you'll still get a warning for omitting the Float case: Characters 8-28: let f =3D function Int _ -> ();; ^^^^^^^^^^^^^^^^^^^^ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Float _ Hope that helps a bit, Jeremy.