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 5F6195D5 for ; Thu, 17 Jan 2019 10:01:56 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208,217";a="364477559" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jan 2019 11:01:54 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 7B4167FEFC; Thu, 17 Jan 2019 11:01:54 +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 D01EC7FEFC for ; Thu, 17 Jan 2019 11:01:42 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f169.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A+jMlnRadq6QXwi87+qwH+an/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZr8i+bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhz?= =?us-ascii?q?sGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJWCNBDIGz?= =?us-ascii?q?YYsBAeQCIOhWsZXyqkAUoheiHwShHv/jxiNKi3LwwKY00/4hEQbD3AE4HtwBqm?= =?us-ascii?q?/brM/0NKgMVeC+0bTGwinDb/xIwzfy9pLIeQ0mrPGDR71/atDRyUgxGAPBlFmQ?= =?us-ascii?q?spDqPzOL2eQXrWeb9fFtVe2qi2E9qgFxpiKjydsrionMn48YzE3P+yt+wIYwP9?= =?us-ascii?q?K4SUh7bMarEJtVqS6aLY92QsIkQ21ypSk11LsLsoO4cigS0Jkr2QLTZvidf4WL?= =?us-ascii?q?4h/vTvidLSlmiH5/Zb6yhhK//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CCSv?= =?us-ascii?q?Rn/0eh3S+D1xnQ6u1ZOEw0m7fXJp8lz7IqmZoTtkPDHiDymErolqOZakIk+u2w?= =?us-ascii?q?5+TmZLXpuIOcOpdqhg3iNqkigM+yDOQiPgQQQWSX5/6w2KDi8ED9WLlKi+c5kq?= =?us-ascii?q?jdsJDUP8Qboau5Dhda0ok58Bm/FTam38ocnXUdN1JKZBKHgJbzO17QOvD1Fvi/?= =?us-ascii?q?g1G2nzdqw/DKJKHuApLILnTbirfuYa5961JAyAo01d1Q+4hbCrQFIP7qXk/xtc?= =?us-ascii?q?fYDgMiPgyvw+fnDc192ZkEVWKOBK+ZKqLSvkWS6uIhOenfLLMS7R39Mfk++/n2?= =?us-ascii?q?jXIj0W0ceKykx54ebnbwSv9mOUSCfX30gtobOWgPsxA6TeqshFDUAhBJYHPncK?= =?us-ascii?q?s2/DA2DMqdBofOXI23yOiO1S2hH5BSIHtNCl2WHG3AeICNWvNKYyWXdJwy2gcY?= =?us-ascii?q?XKSsHtdynSqlsxX3nv8+drKNq38o8Kn73d0w3NX90BQ79Dh6FcOYijjfQGR9n2?= =?us-ascii?q?dOTDgzjvkm/R5Nj2yb2K09uMR2UMRJ7qoQAAg/PJ/Yied9DoKqA1+TTpKyUF+j?= =?us-ascii?q?B+6eL3QxQ9Y2mYFcZk98H5C7jUmG0XP0UvkakLuEAJFy+aXZjSD8?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DdAQACUkBchqneVdFjHgEGBwaBVAYLA?= =?us-ascii?q?YIoQU8zJ4QBgR2CXpABgg2KIo9XDR+ETQKCVBoHAQQzBg0BAwEBAgEBAQEBEwE?= =?us-ascii?q?BAQgLCwgpIwyCOikBgmcBAgIBIwQZARsdAQMBCwYDAgQHNwICIgERAQUBHAYTg?= =?us-ascii?q?yIBgWgBAw0ID48KkAo8ixt8FgUBF4J4BYRCChknDV6BNwIGEowtgVc/gRGDEog?= =?us-ascii?q?KglcCiTxKh1KQOAcCgiwEhHKKcRiCMo9ZjxiLZw8hgTtKgS4zGiNQMYI7CYISD?= =?us-ascii?q?A4Jg0sziiFBMIszAQE?= X-IPAS-Result: =?us-ascii?q?A0DdAQACUkBchqneVdFjHgEGBwaBVAYLAYIoQU8zJ4QBgR2?= =?us-ascii?q?CXpABgg2KIo9XDR+ETQKCVBoHAQQzBg0BAwEBAgEBAQEBEwEBAQgLCwgpIwyCO?= =?us-ascii?q?ikBgmcBAgIBIwQZARsdAQMBCwYDAgQHNwICIgERAQUBHAYTgyIBgWgBAw0ID48?= =?us-ascii?q?KkAo8ixt8FgUBF4J4BYRCChknDV6BNwIGEowtgVc/gRGDEogKglcCiTxKh1KQO?= =?us-ascii?q?AcCgiwEhHKKcRiCMo9ZjxiLZw8hgTtKgS4zGiNQMYI7CYISDA4Jg0sziiFBMIs?= =?us-ascii?q?zAQE?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208,217";a="292237565" Received: from mail-qk1-f169.google.com ([209.85.222.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Jan 2019 11:01:41 +0100 Received: by mail-qk1-f169.google.com with SMTP id g125so5651704qke.4 for ; Thu, 17 Jan 2019 02:01:41 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=mIJ7frN9Bz+oVZL0+8fWKPP8Hwec1uZO5aO+fC2+a+s=; b=uUwdZuqiQV5vQSjyqnzyT/EMo9NvzEzYdw6mXqWOgLQBzc4fSbCCPxKN8MW+VBEMsV MxoVJWI2rjE2SNxggGBZ8Wt7OWJksjL2EXmIu+yqYX4oUvat83gpxgKbQnEh6+lOiNC8 xQXFwhn0ib5tDncNVyAgmBfIOJOipbVe3cU3+4KT0NX5YLamWz4UGrjd2v7V5ybIIk/c Lr9p1qhQYNFFtpDohuH5im0fqhh2cSfqla8LvKeqWJ55SOoIxof71wSsC57AfQOOPnS7 DMXGstBEdh2NiBbspRtt7BSwqLcOYZYsbcE8JyyT1D60bdJs+Bz/lT2//SoVln/j5AxR /7QQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=mIJ7frN9Bz+oVZL0+8fWKPP8Hwec1uZO5aO+fC2+a+s=; b=iPC9bPQTcFXGdewyQ0Zb6WgcOIhkiH4r536ahWkQ+Iqm0QcF/exw8kDGKBRz1cZTO6 EAreK2szgOOnZIAxU+xioa+WVIiYoEdv2JH3dGBvsy6QS+YmJKzSzpWhhMK54oMA6esr /oY3DITWiMYZr/Zx7VoQRKZLgsJLWSHRrRS71G3fwstV2qJwGz2xjkQ5RqjzLe8e4kzn ZQmijPRvENKW3hxXiAnF1i413RUHvdigKIOT0shGpBmNj6eU2HXOYwO75qORbRSnso2c bczYYF+lV8CKUFX6pFXu+nJvKvUHBDJJCVqWqQrNGM1wlGmc3V61iAC/vFHzGZVf1yNb 7xRA== X-Gm-Message-State: AJcUukfnazwz0o7x06WpWrky8Drt2H0eHgv/EakrN127aG08Mj0YnHdk vJ7x8BQqj1pmy0QZm2Q3wDXTTsnG+y/YbKil4Oe3ONbQ X-Google-Smtp-Source: ALg8bN6x3tmZbBQF3Opco0oYQqrwU1Dpj5Z6n5EGt7gWnHyWppaz+b8j083GEdlNs8xyITmy+eNOCnDfBBz2bzX7uaE= X-Received: by 2002:ae9:ed89:: with SMTP id c131mr10169613qkg.222.1547719300014; Thu, 17 Jan 2019 02:01:40 -0800 (PST) MIME-Version: 1.0 References: <20190117104611.3288dd5a@mortimer.gmerlin.de> In-Reply-To: <20190117104611.3288dd5a@mortimer.gmerlin.de> From: Gabriel Scherer Date: Thu, 17 Jan 2019 11:12:02 +0100 Message-ID: To: Christopher Zimmermann Cc: caml users Content-Type: multipart/alternative; boundary="00000000000016f551057fa47b67" Subject: Re: [Caml-list] matching GADT option types Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17308 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: --00000000000016f551057fa47b67 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. 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. 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. On Thu, Jan 17, 2019 at 10:46 AM Christopher Zimmermann < christopher@gmerlin.de> 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 > > > -- > http://gmerlin.de > OpenPGP: http://gmerlin.de/christopher.pub > CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 > --=20 Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list Forum: https://discuss.ocaml.org/ Bug reports: http://caml.inria.fr/bin/caml-bugs= --00000000000016f551057fa47b67 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Matching on a constructor of a GADT may introduce a t= yping 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 dec= ide which equations from both sides are preserved in the result, computing = a sort of intersection.

Released versions of OCaml= avoid this difficulty by not supporting GADTs in or-patterns at all; you h= ave to expand the pattern into two branches, as you did in your function `f= ` above.

In the current trunk, a change from Thoma= s 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 n= ow accepted, and will be typeable in 4.08. Other examples, where you need t= o use an equation (provided by both sides of the or-patterns) in the body o= f the clause, will still be rejected.


On Thu, Jan 1= 7, 2019 at 10:46 AM Christopher Zimmermann <christopher@gmerlin.de> wrote:
Hi,

why does the f type correctly while g fails to type?

Christopher

type 'a t =3D
=C2=A0 | A : unit t

let f =3D
=C2=A0 fun (type a) ~(p :a t option) () -> match p with
=C2=A0 =C2=A0 | Some A -> ()
=C2=A0 =C2=A0 | None -> ()

let g =3D
=C2=A0 fun (type a) ~(p :a t option) () -> match p with
=C2=A0 =C2=A0 | Some A (* TYPING ERROR HERE *)
=C2=A0 =C2=A0 | None -> ()

Error: This pattern matches values of type unit t
=C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was expected which matches values = of type a t
=C2=A0 =C2=A0 =C2=A0 =C2=A0Type unit is not compatible with type a


--
http://g= merlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2=C2=A0 0DEF 87E2 92A7 13E5 DEE1
--00000000000016f551057fa47b67--