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 C62A87FC86 for ; Thu, 19 Mar 2015 12:05:14 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jdimino@janestreet.com) identity=pra; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jdimino@janestreet.com"; x-sender="jdimino@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jdimino@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="jdimino@janestreet.com"; x-sender="jdimino@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="jdimino@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A/AAD0rApVnHDIaSZchDIEgwnIfAKBQgdMAQEBAQEBEQEBAQEBBhYJQoQPAQEBAwESEQQZAQE3AQQLCwsNAgImAgIiEgEFARwGEwgaiAUIA6U+PjGKQXCEYgEFlxYBAQEBAQEEAQEBAQEBARUGCoEXiXaEPjMHgmiBRZo7kl4SI4EVhBBvgkMBAQE X-IPAS-Result: A0A/AAD0rApVnHDIaSZchDIEgwnIfAKBQgdMAQEBAQEBEQEBAQEBBhYJQoQPAQEBAwESEQQZAQE3AQQLCwsNAgImAgIiEgEFARwGEwgaiAUIA6U+PjGKQXCEYgEFlxYBAQEBAQEEAQEBAQEBARUGCoEXiXaEPjMHgmiBRZo7kl4SI4EVhBBvgkMBAQE X-IronPort-AV: E=Sophos;i="5.11,429,1422918000"; d="scan'208";a="126728648" Received: from mxout1.mail.janestreet.com ([38.105.200.112]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 19 Mar 2015 12:05:14 +0100 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 1YYYGG-0008KD-VB for caml-list@inria.fr; Thu, 19 Mar 2015 07:05:12 -0400 X-JS-Flow: external Received: by tot-qpr-mailcore2 with JS-mailcore (0.1) (envelope-from ) id BVCq1o-AAACe9-dw; 2015-03-19 07:05:12.953192-04:00 Received: from mail-ie0-f174.google.com ([209.85.223.174]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1YYYGG-0000DP-P0 for caml-list@inria.fr; Thu, 19 Mar 2015 07:05:12 -0400 Received: by ieclw3 with SMTP id lw3so62360121iec.2 for ; Thu, 19 Mar 2015 04:05:12 -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:content-transfer-encoding; bh=6lTr5kejBDh4HIsVgU1gCb70XqCzjuwLZPGFt8OaoNY=; b=QDMaZbgTFTesw9n1kiuCsuSRYXupYwxVEZJvj3ozrFdFmaNCc3KrSqRcvUX1LpCcn9 s+nSRBjVajyaEJsT5vXlPUapuihuS5FPYEEhlh/ySYts2SYWSIT/LyF0DJ3ZA04c7WET nCYi8Gx4p4CcWSp83RMoeHmAvaV1eTC3oXdyA= 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 :content-transfer-encoding; bh=6lTr5kejBDh4HIsVgU1gCb70XqCzjuwLZPGFt8OaoNY=; b=MkB3fjB2dyEAQEFLFzgivVjnkqdFcoQLe+6p6a1WyRiAiKOJTtYiAJQV9S9fhN0eVr hNwBsF4bcYlGJDfZIm50xuGUVWLT8c8dEXv6OB9gHavhcQAxWtuIyetHjZc00EqAHHLF 4f2yX0uocbsGsjk0ryTG5S54xH6N/Oy0nlDiQnsfcGTtiBo9hiWV0e1sA3FVXvDCh9sv i4+j29IFTWYKHfHzdlhaU0HGdRXXuHYNq/UEM2p9MGdhXQf9TcC9vNJbzvTAyQ0P8WUo 6IfU+892rZUmlYaqlY/QX9ObMhA9oSyue2LcveOuWPvrvfuAp1vI7B1waZh15JmL37oZ Px/w== X-Gm-Message-State: ALoCoQnv63vSqVLiWnJ5F+vgrsuD28bLDnTrsmDRNt/1vjOQy5pfohlAfzOGY9eSItLZLiUP8OfVA/3Gj8qWQaVCdkhopyaifgWEin3zFstTQWFY7kG/AmXcC24juisnwiOAuXzQunot X-Received: by 10.43.64.203 with SMTP id xj11mr10148922icb.54.1426763112391; Thu, 19 Mar 2015 04:05:12 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.43.64.203 with SMTP id xj11mr10148905icb.54.1426763112257; Thu, 19 Mar 2015 04:05:12 -0700 (PDT) Received: by 10.50.252.20 with HTTP; Thu, 19 Mar 2015 04:05:12 -0700 (PDT) In-Reply-To: References: <2AB388B4D07D4DDABA30298A7C890319@erratique.ch> <596DAEC11B474882835CEA10AAACE35E@erratique.ch> Date: Thu, 19 Mar 2015 11:05:12 +0000 Message-ID: From:Jeremie Dimino To:=?UTF-8?Q?Daniel_B=C3=BCnzli?= Cc:=?UTF-8?Q?Milan_Stanojevi=C4=87?= , Caml-list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-JS-Processed-by: mailcore Subject: Re: [Caml-list] GADT existential escape On Thu, Mar 19, 2015 at 10:44 AM, Daniel B=C3=BCnzli wrote: > tried to check, but Core fails on me in the toplevel Core should work in the toplevel, why is it failing? > Trying the following [1] self-contained implementation of the idea [1] th= e compiler still complains about escaping types. You need to help the typer a bit: let lookup : type a. 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 :> a) in find d --=20 Jeremie