From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 118007ED11 for ; Wed, 21 Sep 2016 12:11:30 +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-f180.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.180; 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.180 as permitted sender) identity=mailfrom; client-ip=209.85.161.180; 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-f180.google.com) identity=helo; client-ip=209.85.161.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-yw0-f180.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ApsCn4BaNIbJnSx8dEO+CENj/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZpcu+bnLW6fgltlLVR4KTs6sC0LuM9fi6EjVRqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZv?= =?us-ascii?q?IaytQ8iJ3p7xj7r5osybSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYe?= =?us-ascii?q?VcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jOvAPA?= =?us-ascii?q?UBDHw3wATmFexh9BGQvY91f/WYvttgP1s+N83G+ROsigHp4uXjH3y7poQQT6wB?= =?us-ascii?q?wbPjA49mDeiYQkiL9Yuw6oqR1XzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmx?= =?us-ascii?q?Os5WV7IM?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CUAQCYW+JXhrShVdFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxABAQEBAYFiDwe6dIYeAoFdBzwQAQEBAQEBAQEBAQESAQEBCAs?= =?us-ascii?q?LCRkvgjIEARUBBIIRAQEEEhEdARsdAQMMBgULDQICJgICIQEBEQEFARwGExsHi?= =?us-ascii?q?A4BAxegboEyPjKLPYFrgl8FhAEKGScNVIJeAQEBAQEFAQEBARsCBhB2hTGEVIJ?= =?us-ascii?q?HgUWDPIJaBZk/NYxtgnSPbIhXhA+COhMegRE1gyoegVw8NIROX4FAAQEB?= X-IPAS-Result: =?us-ascii?q?A0CUAQCYW+JXhrShVdFeHAEBBAEBCgEBFwEBBAEBCgEBgxA?= =?us-ascii?q?BAQEBAYFiDwe6dIYeAoFdBzwQAQEBAQEBAQEBAQESAQEBCAsLCRkvgjIEARUBB?= =?us-ascii?q?IIRAQEEEhEdARsdAQMMBgULDQICJgICIQEBEQEFARwGExsHiA4BAxegboEyPjK?= =?us-ascii?q?LPYFrgl8FhAEKGScNVIJeAQEBAQEFAQEBARsCBhB2hTGEVIJHgUWDPIJaBZk/N?= =?us-ascii?q?YxtgnSPbIhXhA+COhMegRE1gyoegVw8NIROX4FAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,373,1470693600"; d="scan'208";a="194156625" Received: from mail-yw0-f180.google.com ([209.85.161.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Sep 2016 12:11:29 +0200 Received: by mail-yw0-f180.google.com with SMTP id u82so44142603ywc.2 for ; Wed, 21 Sep 2016 03:11:29 -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=YvpWSsuHGI+nRMCPUyn51utweL5QPpLpWMAJNDpCw0I=; b=ToHBm8vut6RuEdK+t18ZCsnLkvmq3OWlqi2dEwpaBVQWhaP6InzLnLFewusWi+P6wp B+gU3kYJ3ZS/EgcFfGomr6Nd0sC/JQ2G2S42mFBirmadbVXkJCdgAgMld+Mw99KYA0CH 3SpF1tktz2vUFvIPTwsVN1NXaY54releWlk/P1Jab9c0o9aCDHTUwmB6kDkXtqmYEgTt 5L8GEked9+AwJbmOkurLIFlybFKX+wEgOMUwnye5maozMsSuE963mFoqIqwyb5p2CeRu ewleyTQN8Ycao5eARnqwVvEEmBdk0Q0pexHuWKPoPA8IFB8clCxT41Xws3yPSrk6SEf4 bpVg== 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=YvpWSsuHGI+nRMCPUyn51utweL5QPpLpWMAJNDpCw0I=; b=hsclzMzklCC5jiNzlP5YYNybJ8WdiIImqZth/7IgVBrABpoSTKyZMZ9fY3WFRSI3qW ryYMjabtt3Yex09IWtuCIaYD7rzNSGZCmMFVIM6ph3t2js1o5JO0x+43ZtYS0Q5o7XdA tChnSaXDJK2528mp57oYHJ9F2FXcP8fJnipQh5Sy0pzBsQkw388KJSLg/LFzONfl+BMg zOnrPCwM9iUJ1APCYL0n6mw1AoTaV7D522K+ix7uvSCYH6twVYa4SbOg5NyttzowNSDh OGGubAbNgnq+vzZtDiBFAlWOMx3MZ/TiRxWkhgWjAwkx5SkDYjrSa8FAKIi9vRHDKQSh E6zg== X-Gm-Message-State: AE9vXwNqsyY+Jfuq+ZqVVXu+WSI5IVWHq7ZzKCkopy7gQeOhT6pA0WYFcO/TTLhJ527fsgiiWuHY7vOhzUgkLA== X-Received: by 10.129.86.131 with SMTP id k125mr33761104ywb.21.1474452687953; Wed, 21 Sep 2016 03:11:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.136.195 with HTTP; Wed, 21 Sep 2016 03:11:07 -0700 (PDT) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Lukasz Stafiniak Date: Wed, 21 Sep 2016 12:11:07 +0200 Message-ID: To: Markus Mottl Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Covariant GADTs On Tue, Sep 20, 2016 at 11:07 PM, Markus Mottl wrote: > > Existentially quantified type variables need a well-defined scope. > It's easy to define this scope with GADTs and first class modules: it > starts with a pattern match or when unpacking the module. But > accessing a record field as such doesn't create a binding. This would > require some care when establishing the scope. Maybe one could define > the start as the topmost binding whose type depends on a given > existential type as obtained through field accesses. > > Another issue: when accessing an immutable field twice, one could > assign the same existential type to bindings of their values. But > accessing a mutable field twice would require two distinct existential > types, because intermittent changes to the field could substitute > values of incompatible types. Maybe there are even more awkward > things that I haven't thought about. > > Any thoughts? A simple solution would be to "A-transform" (IIRC the term) accesses 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.