I have some trouble understanding how the type inference engine manages polymorphic functions and their type annotation, and, more specifically, why its behaviour regarding them changes depending in which scope the function is declared.
Let me give you an example (I use OCaml 4.07) :
let f : 'a -> 'a = fun x -> x let () = let g : 'a -> 'a = fun x -> x in ignore (f 1); ignore (f "a"); ignore (g 1); ignore (g "a")
This example would fail to compile, because of a typing error occuring on the last line :
`This expression has type string but an expression was expected of type int
Basically, it seems that the existence of the term
g 1 somehow “specializes” the type of
g, making it an
int -> int function in the type inference engine’s point of view rather than a polymorphic
'a -> 'a function, thus making the term
g "a" unsound.
What I don’t understand is :
1/ Why does this occur for
g and not for
f ? They have the exact same definition but are declared in different scopes. What is it supposed to demonstrate regarding the way the type inference engine manages them ?
2/ I have explicitely annotated
g as a
'a -> 'a function when declaring it. If I hadn’t, and had let the compiler infer its type, it would have worked ! i.e. the following code :
let () = let g = fun x -> x in ignore (g 1); ignore (g "a")
would compile neatly. So would the following :
let () = let g : type a. a -> a = fun x -> x in ignore (g 1); ignore (g "a")
where I explicitely state that I expect the type term
a -> a to be universally quantificated over type
Does it mean that typing
let g : 'a -> 'a = ... implies an existential quantification over type
At this point, all I know is that I’m no longer sure how the type inference works, so any explanation would be very welcome
Thanks in advance !