Why two different error messages in OCaml type checking?

Question

Starting from a full expression, everything works as expected in the ocaml evaluator.

# fst (fst ((1, 2), 3)) ;;
- : int = 1

Imagine the result of passing functions around but failing to put them in proper context. I'll exemplify in these examples:

# fst fst ;;  # expect error
Error: This expression has type 'a * 'b -> 'a
       but an expression was expected of type 'c * 'd
# (fst fst) whatever ;;
Error: This expression has type 'a * 'b -> 'a
       but an expression was expected of type 'c * 'd
# fst fst whatever ;;
Error: This expression has type 'a * 'b -> 'a
       but an expression was expected of type ('c -> 'd) * 'e

The last Error message has what I don't understand. What is it that makes ocaml substitute type ('c -> 'd) * 'e for 'c * 'd when analyzing the last expression which has three tokens but no brackets?

Looking at Function application I can only guess (but can't say) that this might have to do with associations and how ocaml looks at a function and arguments juxtaposed. Any hints as to where to look?

ivg ivg · Accepted Answer · 2015-01-28T12:57:36

In short, you just hit a different path of the unification algorithm, that lies in the heart of OCaml type inference.

Both cases, parenthesized and the last one are semantically equivalent, but due to some subtleness in a grammar a represented slightly different. (This is because there're and rules in the grammar, and parenthesis, creates a , but actually this doesn't matter).

Since we have slightly different syntax tree, the unification chose two different paths here. In a first case, it tried to typecheck parenthesized simple expression first. On the second case, it tried to infer the overall function type, and afterwards moved to the unification of the arguments (roughly). In any case the typechecker will stop as soon as possible. Thats why on a first case, typechecker even didn't try to look after the parenthesis, because he already knew, that the expression is not valid.

The reasoning on the second case, can be expressed something like this: in order for this expression x y z to typecheck, x y should evaluate to function expression that can accept z expression, i.e., (x y) : 'c -> 'd, where 'c and 'd are just type variables. Since x has type 'a * 'b -> 'a, that means that 'a must have type 'c -> 'd, substituting 'a we get the type of y to be inferred as ('c -> 'd) * 'e. Now, we look at the actual type of y and see that it has completely different type, that cannot be unified with the inferred one. We raise the error.

Why two different error messages in OCaml type checking?

1 Answers