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 11F697ED1D for ; Tue, 13 Oct 2015 03:42:33 +0200 (CEST) IronPort-PHdr: 9a23:Vfg3aBPYyH0LUvs0Lj4l6mtUPXoX/o7sNwtQ0KIMzox0KPX9rarrMEGX3/hxlliBBdydsKIYzbqM+Pq5AyQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbDosMeKOU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCKJ6nYGSS0unwZFGUDr8R7/V5H3+n/zsOZwwjKyM9D5SLkyX3Kk4rs9GzHyjyJSFTcy6XzakYRfhbhBoR28qlQrzIfOeoCaKfdWe6rBfZUcTGVGT88USmpICcW+d91cXKI6Ie9Eotyl9BM1phykCFzpXbu3xw== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DbAQA3YRxWnAWCBoVdFoNkboJlvRAXBoJ2ggp/AoFyEAEBAQEBAQEBEAEBAQEBCBQJT4IfggcBAQEDAQwXBBkDATUBAQ4JAhgCAhgOAgJXBog5Bw6PHJxFcYRrAooZhFIBAQEBAQUBAQEBAQEBFAEGgSKHYYJuhFozB4IuOxQdgRSOCIgRhRmCcIURgVhIlXSDbziCPBYHgWNihnEBAQE X-IPAS-Result: A0DbAQA3YRxWnAWCBoVdFoNkboJlvRAXBoJ2ggp/AoFyEAEBAQEBAQEBEAEBAQEBCBQJT4IfggcBAQEDAQwXBBkDATUBAQ4JAhgCAhgOAgJXBog5Bw6PHJxFcYRrAooZhFIBAQEBAQUBAQEBAQEBFAEGgSKHYYJuhFozB4IuOxQdgRSOCIgRhRmCcIURgVhIlXSDbziCPBYHgWNihnEBAQE X-IronPort-AV: E=Sophos;i="5.17,676,1437429600"; d="scan'208";a="150338030" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Oct 2015 03:42:03 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B61406533; Tue, 13 Oct 2015 10:42:00 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172 [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 39ACB4148; Tue, 13 Oct 2015 10:42:00 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=pRUZ8G6OZHxo5NVfr0F3VN3lHKo=; b=pZWSYDnak5E/+6EzZGO59CryUJ+C WQ6coiCerKeusdIpoXU03hPGooaa3Tsyd7Nh9Ajrr1l+I9MZL4oM1snNYQiKpmxb a1p68k2QyNonTQ564gYFc0QuP9kQOujMbTKqlxmJlg9Ewkf3h+XH1omMEdTEeOy1 6PpFrqi6PUKYVDA= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=l0+K1OzRDhNCBJ8uKmtlA+LOpdGNM0qfwV4Ihy19Yul+grhmS7m4CxSFbxTqZPsLY0CbKKxh56c0Dkk5i8ZTZ86HUgBHg/J+k3dd9sYYw8ap0qsCjCsQmGaXp2ICjLjm6sxD2vq+Sg2Ix8PO5y5HUXNED71JA3M/FDy1T3ngtZ8=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 2ADC86B7D; Tue, 13 Oct 2015 10:40:56 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) From: Jacques Garrigue In-Reply-To: <561BC1BC.8070602@fugmann.net> Date: Tue, 13 Oct 2015 10:41:59 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <6E45A23F-36D5-48C9-88FD-858AFEDA48D6@math.nagoya-u.ac.jp> References: <5616BA18.8000808@fugmann.net> <8ABD4D90-3BC1-4EDF-90DA-21DD056527D5@math.nagoya-u.ac.jp> <561BC1BC.8070602@fugmann.net> To: Anders Peter Fugmann X-Mailer: Apple Mail (2.2104) Subject: Re: [Caml-list] Strange Gadt error On 2015/10/12 23:20, Anders Peter Fugmann wrote: >=20 > Hi Jacques, >=20 > Thanks for detailed explanation. I think I understand now why the error o= ccurs and more specifically how to fix it in a consistent way. >=20 > (However, changing 'add' to be > 'add': int -> int -> int =3D fun n m-> n + m > does not seem to help in my case) Interesting. This appears to be a rare case where it types with -principal, but not with= out it. This is bug. I shall investigate it. Jacques Garrigue >=20 > Thanks > /Anders >=20 > On 09/10/15 01:17, Jacques Garrigue wrote: >> On 2015/10/09 03:46, Anders Peter Fugmann wrote: >>>=20 >>> Hi, >>>=20 >>> I the following example (boiled down from a real use case): >>>=20 >>> type _ elem =3D >>> | Int: int elem >>>=20 >>> let rec incr: type a. a elem -> a -> int =3D function >>> | Int -> fun i -> add i 1 >>> and add n m =3D n + m >>>=20 >>> I get the error (Ocaml 4.02.3): >>> File "example.ml", line 5, characters 24-25: >>> Error: This expression has type int but an expression was expected of t= ype >>> int >>> This instance of int is ambiguous: >>> it would escape the scope of its equation >>=20 >> Interesting error. >> I see your confusion in seeing an error on =E2=80=98i=E2=80=99. >>=20 >> It is not completely wrong as you can indeed fix it by adding a local ty= pe >> annotation changing the type of =E2=80=98i=E2=80=99 from =E2=80=98a=E2= =80=99 to =E2=80=98int=E2=80=99. >>=20 >>> I can get rid of the error by annotating the type of i in line 5 like t= his: >>>=20 >>> | Int -> fun (i : int) -> add i 1 >>> ^^^ >>=20 >> However, the real cause is not so much =E2=80=98i', whose type is indeed= known (but as `a=E2=80=99, not `int=E2=80=99), >> but rather the absence of type annotation on =E2=80=98add'. >> Changing add in the following way fixes the problem: >>=20 >> and add : int -> int -> int =3D fun n m -> n + m >>=20 >>> Or move add above incr like this: >>>=20 >>> let rec add n m =3D n + m >>> and incr: type a. a elem -> a -> int =3D function >>> | Int -> fun i -> add i 1 >>=20 >> This change of order only works by chance. If you use ocaml -principal, = you still get >> a type error here with this code. >>=20 >>> Is there an explanation to why I need to give the type of i in this cas= e? As 'i' _must_ be an int (from the type annotation of incr), annotating t= he function seems ambiguous. >>=20 >>=20 >> If you look carefully, you will see that the annotation says that =E2=80= =98i=E2=80=99 has type =E2=80=98a=E2=80=99, not =E2=80=98int=E2=80=99. >> In the local scope, those two types are equivalent, but once you leave i= f they are different. >> Since we do not know yet the type of add, making a choice between the tw= o seems arbitrary, >> hence the error message. >>=20 >> The only conclusive source on how this works is my paper with Didier R= =C3=A9my: >> Ambivalent types for principal type inference with GADTs >> http://pauillac.inria.fr/~remy/gadts/ >>=20 >> In a nutshell, ambiguity occurs when a type obtained by unifying two equ= ivalent >> (but different) types is leaked out of their equivalence scope. What hap= pens here is >> a bit complicated. First the typer tries to give the type [a -> int -> i= nt] to `add', avoiding >> ambivalence. However, `a=E2=80=99 is not allowed to leak out of the defi= nition of `incr=E2=80=99, so it >> gets expanded into `int=E2=80=99. And this is that expansion which trigg= ers the ambiguity >> error. (An interesting remark is that, since add cannot have type [a -> = int -> int] anyway, >> there seems to be no ambiguity here. However, there is a scope between t= he >> definition of `incr=E2=80=99 and the pattern-matching on `Int=E2=80=99 w= here such ambiguity might exists.) >> By adding a local annotation on `i=E2=80=99, the problem is avoided, bec= ause then we are assuming >> that `add=E2=80=99 has type [int -> int -> int] from the beginning (the = ambivalence on `i=E2=80=99 does not leak). >> Same thing with adding an annotation on `add=E2=80=99. >>=20 >> As specific remark on what happens when you change the order (without -p= rincipal): >> Since add is typed first, and receives type [int -> int -> int], this ty= pe is handled as >> though it was explicitly known when entering the gadt scope. This is don= e for >> the type of all external identifiers, except for their non-generalized t= ype variables. >> As a result, you get the same behavior as adding a type annotation on ad= d. >>=20 >> Thank you for this very demonstrative example. >>=20 >> Jacques Garrigue >>=20 >=20