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 10D3D5D5 for ; Thu, 17 Jan 2019 10:08:27 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208,217";a="364479414" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jan 2019 11:08:26 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 383168256D; Thu, 17 Jan 2019 11:08:26 +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 ESMTPS id E8F3F7FEFC for ; Thu, 17 Jan 2019 11:08:18 +0100 (CET) Authentication-Results: mail2-smtp-roc.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-qt1-f171.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AA9z5xh/gi2s2af9uRHKM819IXTAuvvDOBiVQ1KB3?= =?us-ascii?q?1+4cTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsVSmpPXMlfVyJPDICh?= =?us-ascii?q?YYURE+UMJvxXo5XnqlYUsReyGQuhCeXywTFInH/22qg63vwgHw7cxwMgBdMOv2?= =?us-ascii?q?rQrN7oKakdTeC1w7fSzTrddfNdxDDw6IfSfR86u/GMXKx/cc7LxUk0CwzFjkuf?= =?us-ascii?q?qZb7MDOPzekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LHiIUVylXe+iV4xoY4Pd?= =?us-ascii?q?K4SEtlbt6+FJtQtieaO5FrTcw8RWxjpSU0yqUetJKlYCQHzI4ryh3fZvCdboSF?= =?us-ascii?q?4w7vWPyMLTp6mX5ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrnUN2AbS6siDU/?= =?us-ascii?q?d951uh1SuW2wDd9+1JI104mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue2?= =?us-ascii?q?9+TqeqvqqoOYOoNuiQzzMr4iltG+DOgkKAQCQmqW9fmk2L3m50L5QbFKjvMskq?= =?us-ascii?q?netZDXPcsbqbSiDA9P04Ys9RK/Ay290NsEnXkIMkhFdwydj4XyNFHOJer3Dfa7?= =?us-ascii?q?g1i2jDhrwPXGMqX7AprRNnjDjKvhfbFl5kFA0gUzyNRf64tQCrEAO/LzRlT8tM?= =?us-ascii?q?fYDx88Kwy72fzrCNR71oMEWGKAGLWVMK3IsQzA2uV6COmWZZQJvy79JuJt1f/r?= =?us-ascii?q?iHIjnFYbe+H91psNaWukGexmLl+xbn/hmNMAFyEGs1xtYvbtjQitWDRJZnu2F5?= =?us-ascii?q?k35jwhBZjuWYjKTJqsjbjHxyy7E4dbfEhJD1mNFTHjcIDSCKREUz6bPsI0ym9M?= =?us-ascii?q?brOmUYJ0kEj27FarmYoiFfLd/2gjjbym0dF04+PJkhRrrG57Cs2c1yeGSGQmxz?= =?us-ascii?q?pUFQ9z57h2pAlG8nnGybJx2qUKGtla5vcPWQA/Z8aFkr5KTuvqUweERe+nDVar?= =?us-ascii?q?RtL8X2M0R9M1hsYSOgNzQor7yB/E2CWuDvkekLnZXJE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A4AAC3UkBch6ugVdFjHAEBAQQBAQcEA?= =?us-ascii?q?QGBUQcBAQsBgmlPMyeEAYEdgl6EH4tigg2KIo1cgXsNH4RNAoJUGgcBBDAJDQE?= =?us-ascii?q?DAQECAQEBAQETAQEBCA0JCCkjDII6KQGCZgEBAQECASMEGQEbHQEDAQsGAwIEB?= =?us-ascii?q?w0qAgIiAREBBQEcBhODIgGBaAEDDQgPjw2QCjyLG3wWBQEXgngFhEIKGScNXoE?= =?us-ascii?q?3AgYSjC2BVz+BEYMSiAqCVwKiEAcCgiwEhHKKcRiCMo9ZjxiLZw8hgSVggS4zG?= =?us-ascii?q?iNQMYI7CYISGoNUM4ohQTCLMwEB?= X-IPAS-Result: =?us-ascii?q?A0A4AAC3UkBch6ugVdFjHAEBAQQBAQcEAQGBUQcBAQsBgml?= =?us-ascii?q?PMyeEAYEdgl6EH4tigg2KIo1cgXsNH4RNAoJUGgcBBDAJDQEDAQECAQEBAQETA?= =?us-ascii?q?QEBCA0JCCkjDII6KQGCZgEBAQECASMEGQEbHQEDAQsGAwIEBw0qAgIiAREBBQE?= =?us-ascii?q?cBhODIgGBaAEDDQgPjw2QCjyLG3wWBQEXgngFhEIKGScNXoE3AgYSjC2BVz+BE?= =?us-ascii?q?YMSiAqCVwKiEAcCgiwEhHKKcRiCMo9ZjxiLZw8hgSVggS4zGiNQMYI7CYISGoN?= =?us-ascii?q?UM4ohQTCLMwEB?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208,217";a="364479356" Received: from mail-qt1-f171.google.com ([209.85.160.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Jan 2019 11:08:13 +0100 Received: by mail-qt1-f171.google.com with SMTP id l11so10741792qtp.0 for ; Thu, 17 Jan 2019 02:08:13 -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=PuB476jeMs2a3naFlAsILUeY8SyaLgqkjnyhCgwRNgU=; b=NjRS/PQbK1OfCQND4NSRdwZKA1idpa2VYEsNc/Vpt1isryuF3sPv3qWxahFsjxrfQo wiQnMjqp0ex+r+3ufNsx/2bm5HnK7CMa/g1aLZ8X3menoi6qq/dglff+1vgRUPOA3zOG Zgf4BkA7v2lm00qF3FM7uzMMLbptXzq+LS6J0EKe9FAF788K5fBqwGQcw6nPdI9cJ8hg tx8uX76ghBp17KmNF4JyhoyEYGT5ON+jzM2lBGFKGK++sW2E3oXWVB/EIB0yDG4zmOZu MBTYq51z1hSSTbUskWDn1ZpXqKQmI+wbSCjlIJQYDcP2VrsjwlPO/z6DVGbziuWagKPY vEoQ== 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=PuB476jeMs2a3naFlAsILUeY8SyaLgqkjnyhCgwRNgU=; b=WJ5whVMYGB2dLJZpjWXfASqxURGZS3nyeNm0CPlmO9h4FwfEnMb9qDJdz60/uc8GAv x0bh2W7E7DKaSu4WrnVzQKyUjwApjCUZ+DMY+3blNdKO1WOI2pL8m9wMM5QLvrvCcU44 rhAASaiBM0CKvAOoG9gE83NLmu7MsJ+HvHzrt81FUFw0H8J+V12NsLGrfr9efapxOfHI km5lJPzr6f+NVD3Wrpui2wGQWYosWUUbAtCmEtcP5bGM4wCYkczLmLsk2OEvn40l2uyY eogy3RzqEcbGbKfFisVuqEo5XfsvWz76BMzIa3FL4QrNDXbPLG5pX7jssyfRiBvXSuxd cJDg== X-Gm-Message-State: AJcUukfQB93hNh79qb51xQECvEAVPHjl0Ca1aKPCVB5c3Bjt42nQXhBE ARUEK5m8OviIW0Oalq614Zh18uRxgXXAUPY9gshLwa8D X-Google-Smtp-Source: ALg8bN7qRZI0VQXkMgCL7nNLo++XXbYbwEe9+sW/AWSBC7YIQrkCX+7MnbLhY9NYaMk+GgkPu6jzrBI8cVKaJQ5o1Wg= X-Received: by 2002:a0c:8a29:: with SMTP id 38mr10416674qvt.222.1547719692377; Thu, 17 Jan 2019 02:08:12 -0800 (PST) MIME-Version: 1.0 References: <20190117104611.3288dd5a@mortimer.gmerlin.de> <20190117110227.3368e34b@mortimer.gmerlin.de> In-Reply-To: <20190117110227.3368e34b@mortimer.gmerlin.de> From: Gabriel Scherer Date: Thu, 17 Jan 2019 11:18:34 +0100 Message-ID: To: Christopher Zimmermann Cc: caml users Content-Type: multipart/alternative; boundary="00000000000079e427057fa492b2" Subject: Re: [Caml-list] matching GADT option types Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17310 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: --00000000000079e427057fa492b2 Content-Type: text/plain; charset="UTF-8" Your function g is incorrect; in the None case, it claims that the constructor A has the type (a t) for an unknown (arbitrary) type parameter (a). A only has the type (a t) for a specific type (a = [`A]), not for all types. If you want g to be able to return a value of type (a t) for *some* type (a) that g chooses, instead of for *any* type (a) chosen by the context/caller, then you should use an existential type wrapping: type any_t = Any : a t -> any_t. [...] | Some A -> Any A | Some B -> Any B | None -> Any A On Thu, Jan 17, 2019 at 11:02 AM Christopher Zimmermann < christopher@gmerlin.de> wrote: > 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 = > | A : unit t > > let f = > fun (type a) ~(p :a t option) () -> match p with > | Some A -> () > | None -> () > > let g = > 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 = > | A : [`A] t > | B : [`A|`B] t > > let f = > fun (type a) ~(p :a t) () -> match p with > | A -> (A: a t) > | B -> (B: a t) > > let g = > 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 > > -- > http://gmerlin.de > OpenPGP: http://gmerlin.de/christopher.pub > CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 > -- 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 --00000000000079e427057fa492b2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Your function g is incorrect; in the None case, it cl= aims that the constructor A has the type (a t) for an unknown (arbitrary) t= ype parameter (a). A only has the type (a t) for a specific type (a =3D [`A= ]), not for all types.
If you want g to be able to return a value= of type (a t) for *some* type (a) that g chooses, instead of for *any* typ= e (a) chosen by the context/caller, then you should use an existential type= wrapping:

=C2=A0 type any_t =3D Any : a t -> a= ny_t.

=C2=A0 [...]
=C2=A0 | Some A -= > Any A
=C2=A0 | Some B -> Any B
=C2=A0 | Non= e -> Any A

On Thu, Jan 17, 2019 at 11:02 AM Christopher Zimmerm= ann <christopher@gmerlin.de> wrote:
On = Thu, 17 Jan 2019 10:46:11 +0100
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



to add to the confusion, why does f type while g fails to type ?

type 'a t =3D
=C2=A0 | A : [`A] t
=C2=A0 | B : [`A|`B] t

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

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

Error: This expression has type [ `A ] t
=C2=A0 =C2=A0 =C2=A0 =C2=A0but an expression was expected of type a t
=C2=A0 =C2=A0 =C2=A0 =C2=A0Type [ `A ] 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
--00000000000079e427057fa492b2--