From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <yallop@gmail.com>
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 70E747FC86
	for <caml-list@sympa.inria.fr>; Thu, 19 Mar 2015 12:02:32 +0100 (CET)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  yallop@gmail.com) identity=pra; client-ip=209.85.216.179;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="yallop@gmail.com";
  x-sender="yallop@gmail.com"; x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  yallop@gmail.com designates 209.85.216.179 as permitted
  sender) identity=mailfrom; client-ip=209.85.216.179;
  receiver=mail2-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 (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-qc0-f179.google.com) identity=helo;
  client-ip=209.85.216.179;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="yallop@gmail.com";
  x-sender="postmaster@mail-qc0-f179.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0A/AADOqwpVm7PYVdFchDIEgwnIfAKBQgdMAQEBAQEBEQEBAQEBBgsLCRQuhBABAQQSEQQZARsdAQMMBgULDQICJgICIgERAQUBHAYTIod4AQMRpUE+MYsxgWuCd5ETChknDVSEXAEBAQEGAQEBARgBBQ6BE4l2hD4zB4JogUUFmjaBG49GgX0SI4EMCYQQPjGCQwEBAQ
X-IPAS-Result: A0A/AADOqwpVm7PYVdFchDIEgwnIfAKBQgdMAQEBAQEBEQEBAQEBBgsLCRQuhBABAQQSEQQZARsdAQMMBgULDQICJgICIgERAQUBHAYTIod4AQMRpUE+MYsxgWuCd5ETChknDVSEXAEBAQEGAQEBARgBBQ6BE4l2hD4zB4JogUUFmjaBG49GgX0SI4EMCYQQPjGCQwEBAQ
X-IronPort-AV: E=Sophos;i="5.11,429,1422918000"; 
   d="scan'208";a="126727976"
Received: from mail-qc0-f179.google.com ([209.85.216.179])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Mar 2015 12:02:31 +0100
Received: by qcbjx9 with SMTP id jx9so23531488qcb.0
        for <caml-list@inria.fr>; Thu, 19 Mar 2015 04:02:31 -0700 (PDT)
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=wWZrXge3dpJdSLFJKAr5dprO5az8Sgj/egKz+eeotcI=;
        b=PO31HG2H7Um7bauLk5dN/IWOLfH2Z9qn+tAaA1PnhgdguFODuqeU9NNBQ84sNuy91b
         jNnDvFf6b8qBSIhzi3ZIZCKRTA18ha9tCIrAsiJvCEX0t1KZmXmNE2TBpn60gAtGBsl6
         /GF/+T26+hjUFiyRlLNG37OlTHASdGTJYikDbmtg/PYB4+0r/6siOFsqre2XDV+Fc67v
         jofWFG13cX44kTytVx/yu1p1cVOX7+Nwak6Dn147Ftb5TUOfoJ21tYD3ySRWdapIY6la
         AJo07YNWV5nf2TbjM12k5pUh/zkUphYWyPm8w6xnxQ6UTQErr58ttohm9lUOkQ2VP4Ki
         3K6w==
MIME-Version: 1.0
X-Received: by 10.140.91.71 with SMTP id y65mr91694630qgd.90.1426762951161;
 Thu, 19 Mar 2015 04:02:31 -0700 (PDT)
Received: by 10.229.160.11 with HTTP; Thu, 19 Mar 2015 04:02:31 -0700 (PDT)
In-Reply-To: <A9833AA6DB2C40058D2E66B6A381E599@erratique.ch>
References: <2AB388B4D07D4DDABA30298A7C890319@erratique.ch>
	<CAKR7PS_K5A5XR0nDnMv4z23LjxGBoi299vKY3+fccd1HuSEM-A@mail.gmail.com>
	<596DAEC11B474882835CEA10AAACE35E@erratique.ch>
	<CAKR7PS_fFML9gvqF1Zr0qa+2uEMUg4FQfp2f9gXuhN1Ee7_n=A@mail.gmail.com>
	<A9833AA6DB2C40058D2E66B6A381E599@erratique.ch>
Date: Thu, 19 Mar 2015 11:02:31 +0000
Message-ID: <CAAxsn=FDU-24dbK2xHm0n8BOSPJgZ+xzZF=kOytoM8ed9ak7Vw@mail.gmail.com>
From: Jeremy Yallop <yallop@gmail.com>
To: =?UTF-8?Q?Daniel_B=C3=BCnzli?= <daniel.buenzli@erratique.ch>
Cc: =?UTF-8?Q?Milan_Stanojevi=C4=87?= <milanst@gmail.com>, 
	Caml-list <caml-list@inria.fr>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [Caml-list] GADT existential escape

On 19 March 2015 at 10:44, Daniel B=C3=BCnzli <daniel.buenzli@erratique.ch>=
 wrote:
> Le jeudi, 19 mars 2015 =C3=A0 02:27, Milan Stanojevi=C4=87 a =C3=A9crit :
>> This is doable in OCaml.
[...]
> However are you sure your example compiles (tried to check, but Core fail=
s on me in the toplevel) ? Trying the following [1] self-contained implemen=
tation of the idea [1] the compiler still complains about escaping types.
[...]
> let lookup : dict -> 'a key -> 'a option =3D fun d k ->
>   let rec find =3D function
>   | [] -> None
>   | B (k', v) :: bs ->
>       match eq k k' with
>       | None -> find bs
>       | Some Eq -> Some v
>   in
>   find d

This needs a locally-abstract type ("type a. ") to allow type
refinement when you match against the GADT

   let lookup : type a. dict -> a key -> a option =3D fun d k ->

and an additional annotation for the inner function:

  let rec find : dict -> a option =3D function

Jeremy.