[Caml-list] Strange Gadt error

[Caml-list] Strange Gadt error

[Anders Peter Fugmann]

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

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
                    ^^^

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

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.

/Anders

Re: [Caml-list] Strange Gadt error

[Jacques Garrigue]

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

Re: [Caml-list] Strange Gadt error

[Anders Peter Fugmann]

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
>

Re: [Caml-list] Strange Gadt error

[Jacques Garrigue]

On 2015/10/12 23:20, Anders Peter Fugmann wrote:
> 
> 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)

Interesting.
This appears to be a rare case where it types with -principal, but not without it.
This is bug. I shall investigate it.

Jacques Garrigue

> 
> 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
>> 
>