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 748F25D5 for ; Thu, 17 Jan 2019 10:02:49 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="364477852" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jan 2019 11:02:47 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 6CD5E8256D; Thu, 17 Jan 2019 11:02:47 +0100 (CET) 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 26FA07FFA1 for ; Thu, 17 Jan 2019 11:02:38 +0100 (CET) Authentication-Results: mail3-smtp-sop.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=3AQXzFsxBQfFkjQcVS6VJQUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT7r8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykC?= =?us-ascii?q?oJOT43/n/KhMJzjq1brhWvqBNjzIPPb4GZKOBzc7nHcN8GW2ZMWNtaWSxbAoO7?= =?us-ascii?q?aosCF/QMPeZCr4n8vFsOsRy+BRGsBOzx0D9Dm3z53aw/0+QkDw7GxgkgEMgIsH?= =?us-ascii?q?TSsd74M7sdUeCvzKnJ1jXDc/RW2S/96IfWaBAsuv6MXbdufsrLzUkvFgXFgk+N?= =?us-ascii?q?poP7Jj6Y0PkGvWac7+plT+2vimgnphl+ojiq2MgskI3JhoMTylze6Cp23oA4Ls?= =?us-ascii?q?C7Rk5jedOoDoZcuz+AO4doXM8vQXtktDskxrAHo5K3YSsHxZY/yxPca/GLaZaE?= =?us-ascii?q?7g/9WOqLPDt1i3BodKiiixuz/0WtzPD3WNOu31ZQtCVFl8HBtnAT2BzX7ciKUv?= =?us-ascii?q?59/kC82TaTzQzT6fxEIUYpmqXFLZ4h2aA/loANsUvdBC/6glj5g7GOekUl/Oin?= =?us-ascii?q?9fjnb634qpOBKYN4kB/yProsl8ClHOg0LAkDU3KG9em/1rDv5Uj5T69Ljv0ynK?= =?us-ascii?q?nZqpfaJcEDq6GlAw9VyIcj6w2jDzehyNQYnWcILEhedRKIiojmJUvOIPT5Dfe5?= =?us-ascii?q?mVijjSlky+jcPrL9GpXNMmTDkLD5cLlh8UFczQ4zwclb55JVEbEBPOn+WlTxtd?= =?us-ascii?q?zdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjd7esqJ6yIZZQJkDf7MfksofD0?= =?us-ascii?q?3lEjnlpIVqmz3IALb2i4E+4uEUScZHf2h94HFy9etQokTff2j0WCXCR7aHO/Ra?= =?us-ascii?q?Y94Hc3BdT1Xs/4WomxjenZj2+AFZpMazUeUwHeITLTb4yBHsw0RmeXK85lnCYD?= =?us-ascii?q?UOH7GYAk2AuqtQm8x7c1drOIqB1djorq0Z1O38OWjQs7rGYmAMGQyWWMSSd4kz?= =?us-ascii?q?FQHmJk7OVEuUV4j2y7/+14jvhfT4YB4vRUTkE5KJjQwuphBsrsVxiHctrbEFs?= =?us-ascii?q?=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BrAQACUkBcgLt+49RjH4F4gmqBAieXf?= =?us-ascii?q?YIND5dvgXsIBR8MAYRAAoJUGgYGMAkNAQMBAQIBAQEBARMBAQkNCQgnJQyCOiK?= =?us-ascii?q?CbwMDJ2ILIRMSD0gZgyOCBQEKq2czijOCbYlSF4F/gRGDEoM1ghmFEwKiEAmBF?= =?us-ascii?q?4EZhHKKZSRlgU2HaYdwjxiLdoFGYIEucU+CbAmGM4ohPjOBBQEBiiwBAQ?= X-IPAS-Result: =?us-ascii?q?A0BrAQACUkBcgLt+49RjH4F4gmqBAieXfYIND5dvgXsIBR8?= =?us-ascii?q?MAYRAAoJUGgYGMAkNAQMBAQIBAQEBARMBAQkNCQgnJQyCOiKCbwMDJ2ILIRMSD?= =?us-ascii?q?0gZgyOCBQEKq2czijOCbYlSF4F/gRGDEoM1ghmFEwKiEAmBF4EZhHKKZSRlgU2?= =?us-ascii?q?HaYdwjxiLdoFGYIEucU+CbAmGM4ohPjOBBQEBiiwBAQ?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="292237746" Received: from mout.kundenserver.de ([212.227.126.187]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-GCM-SHA256; 17 Jan 2019 11:02:37 +0100 Received: from mortimer.gmerlin.de ([85.212.147.163]) by mrelayeu.kundenserver.de (mreue011 [212.227.15.167]) with ESMTPSA (Nemesis) id 1MPowd-1gXbvL2rEh-00MqAA for ; Thu, 17 Jan 2019 11:02:36 +0100 Date: Thu, 17 Jan 2019 11:02:27 +0100 From: Christopher Zimmermann To: caml-list@inria.fr Message-ID: <20190117110227.3368e34b@mortimer.gmerlin.de> In-Reply-To: <20190117104611.3288dd5a@mortimer.gmerlin.de> 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_/KezQOl.3ysBa4/qjjMAKwTq"; protocol="application/pgp-signature" X-Provags-ID: V03:K1:ZqPKu3YM7uQkBNcTe7dLDodkI+87y6ROk+hcBrf0tRPHUhLuZ/A LnBenYdBQbsmZ+Gf7/w1l0tFoh7pyFuTpX+EVlYTgmVZ0JwS13S4cuKx1sBiNdKmLyURYYH 9IMgaCi0OTsjUm5MDUBJyuv3NK9X8vxAUgunIYuFGM9fE1YiDgvUU6Mkvxz2K9PBYjDBf9c TFxs6bxpQreNKeYkWF0dw== X-Spam-Flag: NO X-UI-Out-Filterresults: notjunk:1;V03:K0:175gwqWC6fA=:q/dNN3wRzwejjfTNIX1+ck 30azUB/MRK7PqrkT/X+FkilpaLF2SfK6mzlhoaN+pfMkAB5z0U3bpsEA4RlaQqtxJqqja8w7j djICfYmETpflMpy3k2i+i7VRttijKKERFELJ4Ns5HMAQjlUKmW8idxP9YGqUnmRqi9jxomacj Bj1tE6rdxm5MF3p8tHgNpuIM4CQPMXMmQ3s5+6R20AnQLJsPbvuOmhoVWI8ZiyfQJgwZVYYam tVQDrTJyEnyjzQf5KIrXDBfA5LTuchuij8cQ9XxZf4jekN5gg8sMTzF/FWLfY5DM5Bm/c6TZS GYwrrM1zhay/ftYDxOhyw3Q6EdR7jJVWDgMR8ghmlzFNLqOIkGROi4Xa6hDk4ya0EY+9ZIgg8 cP3xq9OY7rKrhtGm6p7tayO738tfyAA4T3HkbSGcDJCBmm9qst6LGNpmSV+i0LzalJAOsO6fT 6d8G1Vhoo5baTzR/t+RyN0oyBgy8itFytTy/vKmDh3q8I2pApCYwgdW1nsHQEHxrlqlBIZ6vZ PILRqzubRVIpXANBqImFngXB5iRYtN9B5SmlcfFHrM+CvEg57iltGox6SsSCOuzVDNDz7jFhE CTR3A2tHQpjas+LPZwstMANQ9vS3e9C9EaiO+ddHSpsauTSoqA2m0B/shkId1XNAsifPjiv56 r/mgghC2Cbu+q/9mkwkhfHZZ3JVSNY75jDHLd3QeOrt3+01VCNmcB2OZ/GMqoXvDMpZkCCVdb WzJjY4zxrlJLRoSK229Dd42StktbHa38nSkU81//gxINo9bC1CE3HcmurYI= Subject: Re: [Caml-list] matching GADT option types Reply-To: Christopher Zimmermann X-Loop: caml-list@inria.fr X-Sequence: 17309 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_/KezQOl.3ysBa4/qjjMAKwTq Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: quoted-printable On Thu, 17 Jan 2019 10:46:11 +0100 Christopher Zimmermann wrote: 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 to add to the confusion, why does f type while g fails to type ? 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 --=20 http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 --Sig_/KezQOl.3ysBa4/qjjMAKwTq Content-Type: application/pgp-signature Content-Description: OpenPGP digital signature -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE+CT73l6XX3KFKq8nJS8PWAcyqzQFAlxAUrMACgkQJS8PWAcy qzRvzBAAoR1aLMOHVUcPUOFVzeq2ZPzcQ8lrIdzmuTKRRFZFMRo05eWCDT3Dstmm gJS5/yTWC8j2k1KV7PnRDVX9wMyfQ/3FMWZ4sltlSKJ1QqJDdP6oqZ1o9/8wS+G/ rbyHsaGztf08eZZ/ijsZMhmBtSe+hwbreNOgBaEfVnqvPlZdd9wsirZ1pvg71TGb oRSISVsSC7VL31CAzvVBe2pE//AjUrz+1Rf+atwjKW+KoGzBdUAhhT6QxxwvYAiA oHEMtDK7P+/8WyXR23JlRhNrGCKYxmAqvfZz572BMF5Mth7yvfHnZUYXCkfW9Km9 FIazvD6a6iCReYeAa6v8/pavg5IDGe+/mqOIcmtV+ThzrCw1ZcxEc5ZEFVeroWcu XedoyRArOE9D5+mnEstC4OMjBZUobNXp2+KeBoFfYJk5Hwh0xmGZMbULtXHb/nLB Bug5xD0pvjs0+g1lVtdwEjCx9fKWw5ijgtOX0O91zOAkCIuoyR9oL7DXnR28jfuN RV0kJPuAs98MzjV5eDtQEuK05gz05X328oEWEIq9FfAiQmRIJyAQjKdKUKmXu3ug ZZIm4IpPBSaodh2S+v4+bCfBajmLmGzRdheVyTnl3jHqAFhuLasCReyGIT8th7w3 ft6E3PR32pxWYhlbjeFR0JMlmYHwn3GAe9EhwtxpG3P+l1ZDTm0= =KOAr -----END PGP SIGNATURE----- --Sig_/KezQOl.3ysBa4/qjjMAKwTq--