Re: [Caml-list] Strange Gadt error

[Anders Peter Fugmann <anders@fugmann.net>]

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
>