From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id 05F3A5D5 for ; Thu, 17 Jan 2019 10:08:47 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="364479575" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jan 2019 11:08:43 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id AAADC7FFA1; Thu, 17 Jan 2019 11:08:43 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTP id 4D0807FFA1 for ; Thu, 17 Jan 2019 11:08:37 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christopher@gmerlin.de; spf=None smtp.mailfrom=christopher@gmerlin.de; spf=None smtp.helo=postmaster@mout.kundenserver.de IronPort-PHdr: =?us-ascii?q?9a23=3Ax9nvIxQ7em8NHJkdTrMtBzuio9psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6yYxCN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0li?= =?us-ascii?q?gIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRPDI28?= =?us-ascii?q?cYUBEukPMuRWr4f6qFQBsQCzBQawCO710DJFnGP60K883u88EQ/GxgsgH9cWvX?= =?us-ascii?q?nKrNX1LqYSUfupzKnP1TXDb+1Z2S3g44fLcxAhpPSMUqxqccrU00YvEQXFhUiX?= =?us-ascii?q?pIP5PzOVzOUNs3OH7+pnTeKvi3Aoqxtqrzigw8cjlJPJhoYUylDC7yl23Zg6KM?= =?us-ascii?q?S+RUVmb9CkF55QuDubN4twWs4iTGRotzggyr0CuJ67ejIGx4k5yBPZdveJcJCI?= =?us-ascii?q?7wr9WOqMPzt0nmxpdKy9ihqo7ESs1OzxWtOp3FtEoSdJitrBu3AX2xDN98SLVO?= =?us-ascii?q?Fx8lqu1DuNzQzf9+BJLE4ymKHGMZAu2KQwmYAWsUnbHi/5hkH2jKiOe0Uh/eio?= =?us-ascii?q?9vjnbq/lpp+BMY97lx/xMqI1msOhG+Q4LBYBX3KB9euhyrLv5Uz5QLNUgf0qiq?= =?us-ascii?q?TVro3WKdoBqqKnHQNY0Jwv5wuhAzqnytgUgHcKIV1ddBKClYfpOlXOIP7iDfe4?= =?us-ascii?q?hlShiCtkx/DcPr3gGZXNMn/DkK/hfblj8U5R0wUzzdVB6JJODrEBIfTzVlXsu9?= =?us-ascii?q?PGFhM5KRC7w/77CNVh0YMTQX6ADbWcMKPWqFOI4uMvI/KQZIIOozb8K/0l5+b0?= =?us-ascii?q?gnMjmF8de7Op3ZoNZ3yiEPRmORbRXX25rd4LC2YHukIFR+znklCYGWpcbnyoXq?= =?us-ascii?q?84oCowCI+8AJ3rSYWkgbjH1yC+SM54fGdDX3uMC3bza4KcW/oWIBCTJ8psiDkN?= =?us-ascii?q?U77pH4QhzxC1qAjiy7d9BuXR9zcctJSl2NUjtL6brg076TEhV5fV6GqKVWwh2z?= =?us-ascii?q?pQH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQCFU1MJPGy+18Tdz/CFqYIoW5DW2+?= =?us-ascii?q?S9DjOgkfC8oryoZUMUl4Fs+mjxaF0yf4W+ZIxYzOP4Q99+fn51a0J8t5zCychq?= =?us-ascii?q?wmkkVgQdZJOWCgnaNl6QXJQYLEwR2U?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A8AAC3UkBcgIZ+49RjHAEBAQQBAQcEA?= =?us-ascii?q?QGBVAQBAQsBgmmBAieEAZN8gg0PiROQVwgFHwwBhEACglQaBgYzBg0BAwEBAgE?= =?us-ascii?q?BAQEBEwEBCQ0JCCclDII6KQGCZgEBAQECASMEUgULCxgJEw4CAg8SNgYTgyOBa?= =?us-ascii?q?QMNDAEKqm58M4gJDYIdgm2JUheBf4ERgxKCV4UzglcCiTxKh1KEfosHMwmBF4E?= =?us-ascii?q?ZhHKHOoMrJGWBTYdph3CPGIEVimGBXIF4cU+CbAmCHheDfoohPjOBBQEBiiwBA?= =?us-ascii?q?Q?= X-IPAS-Result: =?us-ascii?q?A0A8AAC3UkBcgIZ+49RjHAEBAQQBAQcEAQGBVAQBAQsBgmm?= =?us-ascii?q?BAieEAZN8gg0PiROQVwgFHwwBhEACglQaBgYzBg0BAwEBAgEBAQEBEwEBCQ0JC?= =?us-ascii?q?CclDII6KQGCZgEBAQECASMEUgULCxgJEw4CAg8SNgYTgyOBaQMNDAEKqm58M4g?= =?us-ascii?q?JDYIdgm2JUheBf4ERgxKCV4UzglcCiTxKh1KEfosHMwmBF4EZhHKHOoMrJGWBT?= =?us-ascii?q?Ydph3CPGIEVimGBXIF4cU+CbAmCHheDfoohPjOBBQEBiiwBAQ?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="364479518" Received: from mout.kundenserver.de ([212.227.126.134]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-GCM-SHA256; 17 Jan 2019 11:08:34 +0100 Received: from mortimer.gmerlin.de ([85.212.147.163]) by mrelayeu.kundenserver.de (mreue011 [212.227.15.167]) with ESMTPSA (Nemesis) id 1Mk0e8-1hUS1x1zqa-00kS2Y; Thu, 17 Jan 2019 11:08:33 +0100 Date: Thu, 17 Jan 2019 11:08:31 +0100 From: Christopher Zimmermann To: Gabriel Scherer Cc: caml users Message-ID: <20190117110831.7e23a284@mortimer.gmerlin.de> In-Reply-To: References: <20190117104611.3288dd5a@mortimer.gmerlin.de> X-Mailer: Claws Mail 3.17.1 (GTK+ 2.24.32; x86_64-unknown-openbsd6.4) MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/61ZcsrRRrgzijEew8HJKb0="; protocol="application/pgp-signature" X-Provags-ID: V03:K1:ShRgamewZbeWRFw2N1XF+yaAsNgjD68mdUrvFurolLbASVZfpZw Tszh6QKAjVm56MEAsP1Ttt7FcXhp3wsZ0/nrDCbkr5PRB7U+TXTN6ztL7K4w/tq7f8VjMRD q/wblxY7PmDMeqKNFwFbcyfe9F//6Up9+hOvZIwrDUyhv+uTt+ejI7Iw7s7CTwLKH9+Yqgo hUlNHYIS12OKE4nm9tzzA== X-Spam-Flag: NO X-UI-Out-Filterresults: notjunk:1;V03:K0:dK2m1E9vYjI=:HFJmXoVWxvuY1gY2LdyHxj vFnVDnDVMJ4Lgi/Q2jv0KvCPAU483xlrik6yrAVwm7uis93oo9DWjUVpBF/TIClUFrUgbJ2C8 Wrz39Fa2gPdY1OnOza+wdaCDL057do0DLuyMIJnz+msI5kHjE8v78F8IgZ0RmFdXmVLWudr2T 8HGCcMPMEIKppRm3Eok84bneFifVVE075zlZ8vuGbqSR54YAFHP4e44H/W9zJjJmSXB5RnNtF X9VfJqdWPGa+xUnC1hZbmzrpfkSVWmwaXNlLKQlVnarMdvpPLtu3bPmikhAjfplxyYXcy/QGN SAh3ht+gcfucXwKfxIx/k5Z2pHcJOw1JflCD2IA2EmWQGMqS5kzIvkRpRzmCZLelLHHX8Kk3b FhlBGmtdhAOpoG+1H6Q6E+T6gCxwn0aY3/TgqyIwcBxn/VoMEiAAQVPkVwWxu1PRPNJxDyipz rFILHQVNsOXwfuMO7MarfHM9hZIPBsw3jWvXslyVIWUsUzvxrLKrr2OA+rvDhybvVgR0A0sEn ZphXCjiczmlBmrEZBVjZdJvethOBOCpsxXF6RGF42X4UYaE6cb+0O4lYIt/rrmAI3VSIVBJ3q fnQNa2hTt239YjtuFLS/3ZWbv6hOyajWbwHEM3BHbtb3q412UPD1gUIdG6/ZplDAbzcZZMyrU fr9N9md3fQ9PhvJI2hn66k/UGusrwNsdE1pZqP+l2ehDvEZGhtkaoK3aJJ51JtYRQZ7iPLWsD 93syb8uw0eflQ9zNxi1YB/4Eze+UK+YHRJhy+6ohKHchKYeQlo86UO3w5pY= Subject: Re: [Caml-list] matching GADT option types Reply-To: Christopher Zimmermann X-Loop: caml-list@inria.fr X-Sequence: 17311 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --Sig_/61ZcsrRRrgzijEew8HJKb0= Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thank you for the fast answer! That means my second example will still be rejected in 4.08? type 'a t =3D | A : [`A] t | B : [`A|`B] t let f =3D fun (type a) ~(p :a t) () -> match p with | A -> (A: a t) | B -> (B: a t) let g =3D fun (type a) ~(p :a t option) () -> match p with | Some B -> (B: a t) | Some A -> (A: a t) | None -> (A (* TYPE ERROR HERE *) : a t) Error: This expression has type [ `A ] t but an expression was expected of type a t Type [ `A ] is not compatible with type a=20 On Thu, 17 Jan 2019 11:12:02 +0100 Gabriel Scherer wrote: > Matching on a constructor of a GADT may introduce a typing equation. > In your example, matching on `A` introduces the equation `a =3D unit`. > For this reason, the status of or-patterns (p1 | p2) containing GADT > constructors is delicate: to type-check them we have to decide which > equations from both sides are preserved in the result, computing a > sort of intersection. >=20 > Released versions of OCaml avoid this difficulty by not supporting > GADTs in or-patterns at all; you have to expand the pattern into two > branches, as you did in your function `f` above. >=20 > In the current trunk, a change from Thomas R=C3=A9fis and Leo White has > been merged that allows GADTs in or-patterns, but discards the > equations. Your specific example (the function `g`) is now accepted, > and will be typeable in 4.08. Other examples, where you need to use > an equation (provided by both sides of the or-patterns) in the body > of the clause, will still be rejected. >=20 >=20 > On Thu, Jan 17, 2019 at 10:46 AM Christopher Zimmermann < > christopher@gmerlin.de> wrote: =20 >=20 > > Hi, > > > > why does the f type correctly while g fails to type? > > > > Christopher > > > > type 'a t =3D > > | A : unit t > > > > let f =3D > > fun (type a) ~(p :a t option) () -> match p with > > | Some A -> () > > | None -> () > > > > let g =3D > > fun (type a) ~(p :a t option) () -> match p with > > | Some A (* TYPING ERROR HERE *) > > | None -> () > > > > Error: This pattern matches values of type unit t > > but a pattern was expected which matches values of type a t > > Type unit is not compatible with type a --=20 http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 --Sig_/61ZcsrRRrgzijEew8HJKb0= Content-Type: application/pgp-signature Content-Description: OpenPGP digital signature -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE+CT73l6XX3KFKq8nJS8PWAcyqzQFAlxAVB8ACgkQJS8PWAcy qzQgrw//XRKNsso23eHh8OnQW6IfJkiW/SVLzYbVi89k92FhHLTw1GPCfT4kC/Qv gjHh1jqJsXmqTJVXk9nYpOQQJkWnKTnIHbNAuNSPinYf2+42yhdpcMWdzuFeM50v USKdUhfzyQ5S7JtjVsAzkguAKxFzRwcsP7ZQs7f9WDK1eE8omrTRw1BSVsAq0F/r 1M6wWkp5WsuwLeOJs9M/DSIoGDTgLdxcWyDTFDSRO4gGbDMKf2EbCURCXOtM1Mvt oZ0LerSJhBGT8o3ULTZmuzmNJ8vcSSnggGP4nwjEd0BE26MyPDGO8b5vi+yjlQK6 JMqxoLB4Ap0UYcdgPBtQGmyW76qh0CArYjKh+dCirelBf12WS3okGUhv9i3DBi3G ENy/pGr4exzVxMBMpotJqWaQr65cGKppLWikBM6BSgcjpWzjPrfaduBG5NiV+q28 M4kkKMbR0uFVyshTAP/SQ7M8gn5kFsXqnAYZFyLk+ySgxG8Rod4OccDPmsvZpXQs QIbKsvfDNn6MDF/9uTFJnEQGEQ7BX1bgI1OHdFTGNuZvNTy7GWOGIee5L1SI9Vsz 65tdbtyzko1+NXCPBsh7RhsbnauS7L4/W2Yqmpd/7/T4kUF/IkEP5iiDjBPtAl7w SJDuVzMqGklZqUhaA7gm9LhFYMtln97CZi+Uyg9yPgMo9ApB094= =3W3v -----END PGP SIGNATURE----- --Sig_/61ZcsrRRrgzijEew8HJKb0=--