From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <kaspar.rohrer@gmail.com>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by sympa.inria.fr (Postfix) with ESMTPS id 7E6F37EE20
	for <caml-list@sympa.inria.fr>; Sat, 17 Nov 2012 13:44:28 +0100 (CET)
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  kaspar.rohrer@gmail.com) identity=pra;
  client-ip=209.85.215.180;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="kaspar.rohrer@gmail.com";
  x-sender="kaspar.rohrer@gmail.com";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of
  kaspar.rohrer@gmail.com designates 209.85.215.180 as
  permitted sender) identity=mailfrom;
  client-ip=209.85.215.180;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="kaspar.rohrer@gmail.com";
  x-sender="kaspar.rohrer@gmail.com";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-ea0-f180.google.com) identity=helo;
  client-ip=209.85.215.180;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="kaspar.rohrer@gmail.com";
  x-sender="postmaster@mail-ea0-f180.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgwCAHiGp1DRVde0k2dsb2JhbABFwyYIIwEBAQEJCQsJFAQjgkwTBgEbHgMSEF4RAQUBiC8BAw8EB51Ugm+MM4J4hFoKGScNWYh1AQUMjg6CRmEDlXyFa4h3P4QS
X-IronPort-AV: E=Sophos;i="4.83,270,1352070000"; 
   d="scan'208";a="162829915"
Received: from mail-ea0-f180.google.com ([209.85.215.180])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Nov 2012 13:44:21 +0100
Received: by mail-ea0-f180.google.com with SMTP id f13so1917370eai.39
        for <caml-list@yquem.inria.fr>; Sat, 17 Nov 2012 04:44:20 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=from:content-type:content-transfer-encoding:subject:date:message-id
         :to:mime-version:x-mailer;
        bh=uaQqMDcb5T5oJoZ+H42eMMV3REtDAoHOH4I10Ewxdng=;
        b=ZQbY8nBmhEQTZNb1RF4irtyBY53KW3B+r9+lIAO5DcuCioII7g0+dzYlA8+d9Efknf
         N2aaZs/v/bInPbBszOTeC/MRGvv6ZEzNzMU39A0wudd+3cKnwf1iy/BROjlIqt3d64xV
         Vm8iJ7pXoPva6TsALqQ5LSrEOaRhSGiSmyO0fCx3Xm+7DzZ6jR1ixGLwEW2ibCRnEYyO
         dyM4yiK50CQh4mtQCcdpwRQZGgpzJNbjkjdSgW4/TGmFlxWk/nW1ZUE1EFBSPuxXcnv5
         JApXVZcnzvSVwIq5TFG94LFbkPkuKkz6aJcprEr9sWSo96NR82r/bo6zbij7bvGTqP1j
         tDZg==
Received: by 10.14.205.3 with SMTP id i3mr6643549eeo.18.1353156260721;
        Sat, 17 Nov 2012 04:44:20 -0800 (PST)
Received: from [192.168.2.45] (80-219-162-235.dclient.hispeed.ch. [80.219.162.235])
        by mx.google.com with ESMTPS id f3sm10257117eeo.13.2012.11.17.04.44.19
        (version=TLSv1/SSLv3 cipher=OTHER);
        Sat, 17 Nov 2012 04:44:19 -0800 (PST)
From: Kaspar Rohrer <kaspar.rohrer@gmail.com>
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: quoted-printable
Date: Sat, 17 Nov 2012 13:44:17 +0100
Message-Id: <6E1FE11E-72C5-4AA7-B24A-7E83E139F30C@gmail.com>
To: caml-list@yquem.inria.fr
Mime-Version: 1.0 (Apple Message framework v1283)
X-Mailer: Apple Mail (2.1283)
Subject: [Caml-list] GADT exhaustiveness check

Hi List

I'm messing around with the new GADT feature in OCaml 4.0, trying to write =
a (more or less) strongly typed EDSL. And I've run into non-exhaustive patt=
ern-matching warnings (see below for an example). I'm pretty sure that it i=
s just an inherent shortcoming of GADTs, not a bug. The workaround is easy =
as well, simply add a catch all clause with a runtime error to silence the =
warning, and prove manually that the offending patterns can not occur.

I tried to find more information on this topic, but without getting all aca=
demic, documentation on GADT seems sparse at best. The description of the o=
riginal implementation at https://sites.google.com/site/ocamlgadt/ seems to=
 be the most comprehensive I've found so far. And I'm not sure the informat=
ion about exhaustiveness is still up to date.

It would be nice if somebody could maybe shed some more light on this.

Cheers
	Kaspar


Code that illustrates the problem:

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)
 *)=