Why is this OCaml definition accepted with a wrong type?

Question

I have defined a buggy function:

let first : 'a -> 'b -> 'a = fun x y -> y ;;
(* Result: val first : 'a -> 'a -> 'a = <fun> *)

The compiler accepts it and changes the type from 'a->'b->'a to 'a->'a->'a. It should not work because the return type should be 'a, not 'b. Correct implementation:

let first : 'a -> 'b -> 'a = fun x y -> x ;;
(* Result: val first : 'a -> 'b -> 'a = <fun> *)

Why does it work and how to prevent the compiler from changing the type like so? It becomes a problem with more complex expressions.

Answer 1

By default, types variables in explicit annotations in OCaml are unification variables. In particular, they can be useful to add some equality constraints. For instance, the 'a annotation shared by x and y allows the compiler to detect that in

let rec eq (x:'a) (y:'a) = match x, y with
| `Leaf _, `Node _ -> false 
| `Node n1,`Node n2 ->
  eq n1#left n2#left && eq n1#right n2#right 

the case

| _, `Leaf -> ...

is missing but that would not work without refining the type variable 'a to the quite complicated type of x.

The issue is thus that annotation is not the one that you wanted. If you want to enforce that a function has the polymorphic type 'a -> 'b -> 'a, you can use an explicit universal quantification:

let wrong: type a b. a -> b -> a = fun x y -> y

With this annotation, the typechecking fails with an error:

Error: This expression has type b but an expression was expected of type a

as expected. Whereas the correct function

let ok: type a b. a -> b -> a = fun x y -> x

compiles without troubles.

Here, the prefix type a b. reads "for all possible types a and b" and this annotation enforces that the type of f will be equal to 'a -> 'b -> 'a without any refinement (aka unification) of the type variables 'a and 'b.