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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id D6CCE7ED11 for ; Wed, 21 Sep 2016 12:14:54 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lukstafi@gmail.com; spf=Pass smtp.mailfrom=lukstafi@gmail.com; spf=None smtp.helo=postmaster@mail-yw0-f178.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.161.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 209.85.161.178 as permitted sender) identity=mailfrom; client-ip=209.85.161.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-yw0-f178.google.com) identity=helo; client-ip=209.85.161.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-yw0-f178.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AYO31fhNMpgY3ya++cH4l6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0KPv/rarrMEGX3/hxlliBBdydsKMezbKM+PmxEUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkIt?= =?us-ascii?q?f6KuS9SU1578jrH60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdr?= =?us-ascii?q?ce72ppIVWOg0S0vZ/or9ZLuh5dsPM59sNGTb6yP+FhFeQZX3waNDUQ7dfoqAKL?= =?us-ascii?q?aAyT+n9UBmAfiBlVGE7A6w3mWr/+tyL7sqx23yzMbuPsSrVhfSmh5rx5ACT0gS?= =?us-ascii?q?kGMT8w8ymDjtFzl75SrhOJqBl2woqSa4aQYqktNpjBdM8XEDISFv1aUDZMV8bl?= =?us-ascii?q?N9MC?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CJAAD4XOJXhrKhVdFeGwEBAQMBAQEJA?= =?us-ascii?q?QEBFwEBBAEBCgEBgxABAQEBAYFiDweNLKtEggSGHgKBXQc4FAEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBAQgLCwkZL4IyBAEVAQSCEAEBAQMBEhEdARsdAQMBCwYFCw0CAiYCAiEBA?= =?us-ascii?q?REBBQEcBhMIEweIDgEDDwigcIEyPjKLPYFrgl8FhAEKGScNVIJeAQEBAQEFAQE?= =?us-ascii?q?BARsCBhB2hTGEVIJHhQGCWgEEmT81jG2CdI9siFeED4I6Ex6BER6DQR6BXDw0h?= =?us-ascii?q?S2BQAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CJAAD4XOJXhrKhVdFeGwEBAQMBAQEJAQEBFwEBBAEBCgE?= =?us-ascii?q?BgxABAQEBAYFiDweNLKtEggSGHgKBXQc4FAEBAQEBAQEBAQEBEgEBAQgLCwkZL?= =?us-ascii?q?4IyBAEVAQSCEAEBAQMBEhEdARsdAQMBCwYFCw0CAiYCAiEBAREBBQEcBhMIEwe?= =?us-ascii?q?IDgEDDwigcIEyPjKLPYFrgl8FhAEKGScNVIJeAQEBAQEFAQEBARsCBhB2hTGEV?= =?us-ascii?q?IJHhQGCWgEEmT81jG2CdI9siFeED4I6Ex6BER6DQR6BXDw0hS2BQAEBAQ?= X-IronPort-AV: E=Sophos;i="5.30,373,1470693600"; d="scan'208";a="194157088" Received: from mail-yw0-f178.google.com ([209.85.161.178]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Sep 2016 12:14:53 +0200 Received: by mail-yw0-f178.google.com with SMTP id g192so44547874ywh.1 for ; Wed, 21 Sep 2016 03:14:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=CRPcZW0a1qrgmv1gQMT1i08uSZ6LfHrEUsqnkuQhEvs=; b=QDt11a2pZw+iOZR4kaANpYlfWldnOAZYlIdxJTsIgSmFFct1DjuN0xM490k/cUjLU9 WsOlFUh2wJq7SdtXRoeWXHume/ePy6IYNcCdqJdq5HSbXB0U35faCgU4uBwp6TIUc5hn 4CZIqk5gkTIpzFNzPeh5vJelY82bIk2aZd1aidhSRXLKlPOQbE11itnmixw5ha3iyJKn GL2MTpCyNDNTJW+80Yk++ADD/le5NYyIxvv8Thp4ELSU/6OORCzQs0t/Ey/Tq6WoKoFN JZA8O1U+WrQ7NvgyjwBU4Ft1pbX+w8Ff0+Jn8u/pmS7r2EfWYH9oQkWcjx7jF7VFOvbz vhTg== 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:from:date :message-id:subject:to:cc; bh=CRPcZW0a1qrgmv1gQMT1i08uSZ6LfHrEUsqnkuQhEvs=; b=IRYLR7ja65gNMc5TrwaVEYmuaCwj9h2BYlZyYnn1N0WCeRwxqXcypFQPZxz4lWkvrO dzUbFXB4VML56soFjWenfIzpEZtC1DIbb+kOjuLUAPRyasMjXWlAN/HsU5rWUnm4x0BP e3WxOzpsh7SHSCprreRBjwkDnsKXb5ALmYeBoFKfYRdYsYYklQbjAo4O2l8VLu+SIPrP pGmFm0KZfYVISe2nNkgDsJllHmljS380z4GT75NLadXwXlDK1UFXtBDpeANsP6xHZuTB AG4nJ60yloZo/HeY6xh1LINyWWdw/RyG5RMsOrAoeM3k07iqWzlYpOh9Xt7BKUgBYzpK i4FQ== X-Gm-Message-State: AE9vXwNDlm6zkTbdj2pkCmVFoMrPhSbMVQJeFxMJE0RBLJOJ2VlsEDX61B4VOaFYPG25doOO4WPhJMgpE9r/2w== X-Received: by 10.13.223.22 with SMTP id i22mr27413183ywe.32.1474452892164; Wed, 21 Sep 2016 03:14:52 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.136.195 with HTTP; Wed, 21 Sep 2016 03:14:31 -0700 (PDT) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Lukasz Stafiniak Date: Wed, 21 Sep 2016 12:14:31 +0200 Message-ID: To: Markus Mottl Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Covariant GADTs On Wed, Sep 21, 2016 at 12:11 PM, Lukasz Stafiniak wrote: > > A simple solution would be to "A-transform" (IIRC the term) accesses Sorry, I forgot to define this. I mean rewrite rules like: [f r.x] ==> [let x = r.x in f x] where subsequently the existential variable is introduced (unpacked) at the let-binding level. This corresponds to a single-variant GADT pattern match. > to fields with existential type variables. This would give a more > narrow scope on the expression level than you suggest, but a > well-defined one prior to type inference. To broaden the scope you > would need to let-bind the field access yourself at the appropriate > level.