The root issue is that your annotation is less explicit. A small example of the problem is

```
let sum: 'a -> 'b -> 'c = fun x y -> x + y
```

Notice that the typechecker is happy with `sum`

even if its type is in fact `int -> int -> int`

and not a polymorphic type , something like `for all 'a, 'b and 'c, 'a -> 'b -> 'c`

. The reason is that `'a`

, `'b`

and `'c`

are unification type variables that can be freely unified with any concrete type. So going from `'a -> 'b -> 'c`

to `int -> int -> int`

is perfectly valid.

Thus in your case, the the type of `aux : 'a -> int`

is unified to `aux: int -> int`

at the first call of `aux 1`

. Consequently `aux true`

fails with

Error: This expression has type bool but an expression was expected of type int

This is why it is necessary to use an explicit polymorphic annotation (or universal quantification). Going back to my toy example, this means writing

```
let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y
```

with this explicit annotation, the typechecker fails with an error

Error: This definition has type int -> int -> int which is less general than

'a 'b 'c. 'a -> 'b -> 'c

Here, `'a 'b 'c. 'a -> 'b -> 'c`

is the OCaml syntax for `for all types 'a, 'b, 'c. sum: 'a -> 'b -> 'c`

. Thus the typechecker knows that you intended the function to be polymorphic and can fail here.

Similarly with the explicit polymorphic annotation

```
let rec aux: 'a. 'a -> int = 42
and main () = aux 1 + aux true
```

the typechecker knows from the definition that aux is polymorphic in its first argument and that it should not deduce that `aux:int -> _`

from the call `aux 1`

.

See also the manual .