From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 A95FE7F7AF for ; Fri, 9 Oct 2015 01:17:52 +0200 (CEST) IronPort-PHdr: 9a23:KL0t5BD3tJ9NRvrnDaKVUyQJP3N1i/DPJgcQr6AfoPdwSP7yo8bcNUDSrc9gkEXOFd2CrakU16yJ7eu5CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkb/ssMSCKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZA2D62EHGl0bjhdSSybY4xTzWJG55iL8uudnwwGUIMLzRLYyHzKv8/E4ZgXvjXIlPjUg7WzMwuN5lrharw+s70hwypTOYY6IOdJ7d7/dO9UTSm1QV4NMESVKRIGkOdhcR9EdNPpV+tGu72AFqgGzUEz1XLvi 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: A0CZBAA6+RZWlwWCBoVeFoNkboJlvF0XBoJ2ggp/AoINEAEBAQEBAQEBEAEBAQEBCBYHT0EHgVeCBwEBAQMBDBcEGQMBNQEBAwsJAhgCAhgOAgJXBog5Bw6RZ5xFcYRrAopahF0BAQEBAQUBAQEBAQEBFAEGgSKHYYJuhFozB4IuOxQdgRSOA4gMhRiCb4URgVhIlWuDbziCPBYHgWNign6EbAEBAQ X-IPAS-Result: A0CZBAA6+RZWlwWCBoVeFoNkboJlvF0XBoJ2ggp/AoINEAEBAQEBAQEBEAEBAQEBCBYHT0EHgVeCBwEBAQMBDBcEGQMBNQEBAwsJAhgCAhgOAgJXBog5Bw6RZ5xFcYRrAopahF0BAQEBAQUBAQEBAQEBFAEGgSKHYYJuhFozB4IuOxQdgRSOA4gMhRiCb4URgVhIlWuDbziCPBYHgWNign6EbAEBAQ X-IronPort-AV: E=Sophos;i="5.17,656,1437429600"; d="scan'208";a="150030808" 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; 09 Oct 2015 01:17:50 +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 C45486559; Fri, 9 Oct 2015 08:17:46 +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 6564F24BA; Fri, 9 Oct 2015 08:17:46 +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=8m+dVVNfYp+bujbUadeQxhObzPE=; b=RTgMXLiRt9M/A9IcU12hYBLuBYmn brEVOc0TIqDJum+CiU6i45kTFNva8KLzr/A9nafVYCQtLK9o5vbFTHTHZV0NwcGM WeWl78/h7gzf+1SOxSNVgUITRmZXHqyLT6YghZPZdYLUN9u7UWE6z7+wCYBNPl2s dZ6/zoJ8k+tidOk= 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=xx1uZu5GhyzzvZJVgs+gtbNA2ymLH4uQdyp6fB2NPR+ZFh5ahlOEST0EhxZhJ0ZaQOfK+pxgTjgzyxHWsz0Gr8moNWpdqHdQTBR2aH2OMGIXsozJtZS5wy5vHVj6hmUtvEe60DL+8r9BJ9F3FiwZePR8yEUmjwbH2SToq5Cdetg=; 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 948CA6475; Fri, 9 Oct 2015 08:16:47 +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: <5616BA18.8000808@fugmann.net> Date: Fri, 9 Oct 2015 08:17:45 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <8ABD4D90-3BC1-4EDF-90DA-21DD056527D5@math.nagoya-u.ac.jp> References: <5616BA18.8000808@fugmann.net> To: Anders Peter Fugmann X-Mailer: Apple Mail (2.2104) Subject: Re: [Caml-list] Strange Gadt error 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 type > int > This instance of int is ambiguous: > it would escape the scope of its equation Interesting error. I see your confusion in seeing an error on =E2=80=98i=E2=80=99. It is not completely wrong as you can indeed fix it by adding a local type 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. > I can get rid of the error by annotating the type of i in line 5 like thi= s: >=20 > | Int -> fun (i : int) -> add i 1 > ^^^ However, the real cause is not so much =E2=80=98i', whose type is indeed kn= own (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: and add : int -> int -> int =3D fun n m -> n + m > 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 This change of order only works by chance. If you use ocaml -principal, you= still get a type error here with this code. > Is there an explanation to why I need to give the type of i in this case?= As 'i' _must_ be an int (from the type annotation of incr), annotating the= function seems ambiguous. If you look carefully, you will see that the annotation says that =E2=80=98= i=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 if t= hey are different. Since we do not know yet the type of add, making a choice between the two s= eems arbitrary, hence the error message. 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/ In a nutshell, ambiguity occurs when a type obtained by unifying two equiva= lent (but different) types is leaked out of their equivalence scope. What happen= s here is a bit complicated. First the typer tries to give the type [a -> int -> int]= to `add', avoiding ambivalence. However, `a=E2=80=99 is not allowed to leak out of the definit= ion of `incr=E2=80=99, so it gets expanded into `int=E2=80=99. And this is that expansion which triggers= 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 the definition of `incr=E2=80=99 and the pattern-matching on `Int=E2=80=99 wher= e such ambiguity might exists.) By adding a local annotation on `i=E2=80=99, the problem is avoided, becaus= e then we are assuming that `add=E2=80=99 has type [int -> int -> int] from the beginning (the amb= ivalence on `i=E2=80=99 does not leak). Same thing with adding an annotation on `add=E2=80=99. As specific remark on what happens when you change the order (without -prin= cipal): Since add is typed first, and receives type [int -> int -> int], this type = is handled as though it was explicitly known when entering the gadt scope. This is done f= or the type of all external identifiers, except for their non-generalized type= variables. As a result, you get the same behavior as adding a type annotation on add. Thank you for this very demonstrative example. Jacques Garrigue=