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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 3B32D7ED1D for ; Mon, 12 Oct 2015 16:20:49 +0200 (CEST) IronPort-PHdr: 9a23:hEvdWBFhIJHu1vif6k5TwJ1GYnF86YWxBRYc798ds5kLTJ75rsiwAkXT6L1XgUPTWs2DsrQf27aQ4/qrBjZIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6biodaMOU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCmG7WIBX35evRNSGQnK8RyyCpj4qDH7ufdw8CyTIc2wS7k7XiWrqrotQRSuij9RZBAj92SCo8p8gbhA6CqsuxFli6DJb4ScMvw2Kqrbcd4AXkJPQ8lUXipHRIWxc91cXKI6Ie9Eotyl9BM1phykCFzpXbu3xw== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=anders@fugmann.net; spf=Pass smtp.mailfrom=anders@fugmann.net; spf=None smtp.helo=postmaster@gw.fugmann.net Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of anders@fugmann.net) identity=pra; client-ip=90.184.182.235; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anders@fugmann.net"; x-sender="anders@fugmann.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of anders@fugmann.net designates 90.184.182.235 as permitted sender) identity=mailfrom; client-ip=90.184.182.235; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anders@fugmann.net"; x-sender="anders@fugmann.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@gw.fugmann.net) identity=helo; client-ip=90.184.182.235; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anders@fugmann.net"; x-sender="postmaster@gw.fugmann.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CFBgC6wBtW/+u2uFpdDgiDEFRugmWzRolAHYJ2ggp/AoExPBABAQEBAQEBAYEJgh+CCAEBBAwXBAsBBQgBATYBAQ8JAhgCAgUWCwICCQMCAQIBRQYNCAKILgmNG5xFcYRlAQWOQQEBCBwGgSKKT4RaMweCaYFFlhiFGYJwhmlIhnOPAYNvOCuCBA0dgRZAb4dqAQEB X-IPAS-Result: A0CFBgC6wBtW/+u2uFpdDgiDEFRugmWzRolAHYJ2ggp/AoExPBABAQEBAQEBAYEJgh+CCAEBBAwXBAsBBQgBATYBAQ8JAhgCAgUWCwICCQMCAQIBRQYNCAKILgmNG5xFcYRlAQWOQQEBCBwGgSKKT4RaMweCaYFFlhiFGYJwhmlIhnOPAYNvOCuCBA0dgRZAb4dqAQEB X-IronPort-AV: E=Sophos;i="5.17,673,1437429600"; d="scan'208";a="182358343" Received: from gw.fugmann.net ([90.184.182.235]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 12 Oct 2015 16:20:48 +0200 Received: from [10.0.0.8] (0137900668.0.fullrate.dk [2.110.173.152]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by gw.fugmann.net (Postfix) with ESMTPSA id 059822BF9BB3; Mon, 12 Oct 2015 16:20:45 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=fugmann.net; s=mail; t=1444659646; bh=/SCWYNodiMiwo+j8l9nwwK7ip4IqW7IEye9C0r4odXs=; h=Subject:To:References:Cc:From:Date:In-Reply-To:From; b=alwoalT30bBA9SQVDofDzP4aMEMYGS5Wb4RSbS2L19p+TFtlSQ4vSFeXpcjQRMcoe xThPhtxHNhwi0inK4UoutA6Gi/GMkbsIUrE9fegrBhM2XFp5py5kr+amFj/lJa3+Wc MAZ6TXye54XPQ2EnWzV/en0FxoV4PH9UWstQpgXc= To: Jacques Garrigue References: <5616BA18.8000808@fugmann.net> <8ABD4D90-3BC1-4EDF-90DA-21DD056527D5@math.nagoya-u.ac.jp> Cc: OCaML List Mailing From: Anders Peter Fugmann Message-ID: <561BC1BC.8070602@fugmann.net> Date: Mon, 12 Oct 2015 16:20:44 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Icedove/38.2.0 MIME-Version: 1.0 In-Reply-To: <8ABD4D90-3BC1-4EDF-90DA-21DD056527D5@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Strange Gadt error Hi Jacques, Thanks for detailed explanation. I think I understand now why the error occurs and more specifically how to fix it in a consistent way. (However, changing 'add' to be 'add': int -> int -> int = fun n m-> n + m does not seem to help in my case) Thanks /Anders On 09/10/15 01:17, Jacques Garrigue wrote: > On 2015/10/09 03:46, Anders Peter Fugmann wrote: >> >> Hi, >> >> I the following example (boiled down from a real use case): >> >> type _ elem = >> | Int: int elem >> >> let rec incr: type a. a elem -> a -> int = function >> | Int -> fun i -> add i 1 >> and add n m = n + m >> >> 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 ‘i’. > > It is not completely wrong as you can indeed fix it by adding a local type > annotation changing the type of ‘i’ from ‘a’ to ‘int’. > >> I can get rid of the error by annotating the type of i in line 5 like this: >> >> | Int -> fun (i : int) -> add i 1 >> ^^^ > > However, the real cause is not so much ‘i', whose type is indeed known (but as `a’, not `int’), > but rather the absence of type annotation on ‘add'. > Changing add in the following way fixes the problem: > > and add : int -> int -> int = fun n m -> n + m > >> Or move add above incr like this: >> >> let rec add n m = n + m >> and incr: type a. a elem -> a -> int = 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 ‘i’ has type ‘a’, not ‘int’. > In the local scope, those two types are equivalent, but once you leave if they are different. > Since we do not know yet the type of add, making a choice between the two seems arbitrary, > hence the error message. > > The only conclusive source on how this works is my paper with Didier Rémy: > 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 equivalent > (but different) types is leaked out of their equivalence scope. What happens here is > a bit complicated. First the typer tries to give the type [a -> int -> int] to `add', avoiding > ambivalence. However, `a’ is not allowed to leak out of the definition of `incr’, so it > gets expanded into `int’. 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’ and the pattern-matching on `Int’ where such ambiguity might exists.) > By adding a local annotation on `i’, the problem is avoided, because then we are assuming > that `add’ has type [int -> int -> int] from the beginning (the ambivalence on `i’ does not leak). > Same thing with adding an annotation on `add’. > > As specific remark on what happens when you change the order (without -principal): > 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 for > 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 >