Re: [Caml-list] annotations and type-checking

[Johannes Kanig <johannes.kanig@gmail.com>]

Philippe wrote:
> Le 29 juil. 09 à 01:28, Jon Harrop <jon@ffconsultancy.com> a écrit :
>> I'm guessing the scope of the 'a is not what you'd expect but I have 
>> no idea
>> why. I'd have thought the latter would be a harmless type annotation...
> 
> My guess is that the problem here is not about scope but about 
> quantifiers : the type of f is quantified universally by default but the 
> annotation constrains the type of f to a fixed (yet unknown) type in the 
> subsequent expression (in that sense, yes, the scope of f plays a 
> crucial role).

I think John Harrop is right and the scope of 'a is really the issue 
here. First of all, transforming "let ... in" into a top-level let makes 
the code work again:

# let f (x : 'a) : 'a = x;;
val f : 'a -> 'a = <fun>
# f true;;
- : bool = true
# f 3;;
- : int = 3

which suggests that the scope of type variables in annotations is a 
top-level let-binding. I think I have read about this somewhere, but I 
can't find the right page of the manual ...

Also, the following code fails:

# let f (x : 'a) : 'a = x in (f true, (3 : 'a));;
Error: This expression has type int but an expression was expected of 
type bool


Here it is clear that all annotations are talking about the same 
variable 'a. If 'a was existentially bound twice (once for the function 
definition, once for the constant 3), a type error would not occur.

Johannes