Re: [Caml-list] Strange Gadt error

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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