Hi everyone,

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

.

Does it mean that typing `let g : 'a -> 'a = ...`

implies an existential quantification over type `'a`

?

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 !