OCaml typesystem unintended nesting

Question

In an OCaml toplevel, I have the following type definition:

type 'a lazy_list =
| Nil
| Cons of 'a * 'a lazy_list
| LazyCons of 'a * 'a lazy_list

(Simplified for this example)

And this function definition:

let head = function
| Nil -> Nil
| Cons(x,_) | LazyCons(x,_) -> x

The ocaml toplevel tells me the type of head is 'a lazy_list lazy_list -> 'a lazylist Why is the type not 'a lazy_list -> 'a, which is what I would expect?

Answer 1

One possible result of your function is Nil. Nil is a lazy_list. Therefore the result type of head must be a t lazy_list for some (or possibly all) types t.

The other possible result of head is x where x is an element of the given list. Therefore the result type of head must be the element type of the given list.

By combining these two pieces of information we can conclude that the element type of the given list must itself be a list. Therefore your function can only operate on lists of lists.

If the type of head were merely 'a laty_list -> 'a, Nil would not be valid result for it.