Why does the compiler stop complaining about `type unit` in this case?

Question

If I do let f1 x = x; x+1, compiler will complain: Warning 10: this expression should have type unit.

If I do let f2 f = f(); 5, compiler will give val f2 : (unit -> 'a) -> int = <fun>.

Questions

1. The type system infers that f is a function which take unit as parameter and returns 'a. But if it returns 'a, why the compiler does not give Warning 10?
2. If compiler does not give Warning 10, it means it thinks f() returns unit, doesn't it? Then why it give 'a as the return type?

Answer 1

If compiler does not give Warning 10, it means it thinks f() returns unit, doesn't it?

Obviously, if the compiler gives f2 the type (unit -> 'a) -> int, that means it thinks f returns 'a.

What would you do in the compiler's place?

• Would you warn that f2 may be applied to some functions that return non-unit results, although it may never actually be applied thus?

• Would you give f2 the type (unit -> unit) -> int and make it less useful, forcing it to be used only with functions that return ()?

• Would you invent a complicated system of postponed warnings where f2 has type (unit -> 'a) -> int but produces an additional warning at compile-time if it is applied to a function that does not return ()? Would you make this system work across modules (the postponed warnings of a function would have to be part of the module signatures)?

Warnings are only helpful hints, not guarantees. When in doubt, not emitting the warning is the usual solution (and nearly all compilers adopt this solution, not just the OCaml compilers).

Answer 2

I think this is legacy behaviour from the compiler. Use -strict-sequence to fix it:

$ ocaml
# let f2 f = f(); 5;;
val f2 : (unit -> 'a) -> int = <fun>

But:

$ ocaml -strict-sequence
# let f2 f = f(); 5;;
val f2 : (unit -> unit) -> int = <fun>

If you use ocamlbuild, you should put this in your _tags file:

true: strict_sequence

Answer 3

Let me add a bit to Pascal's answer.

Try

let f1'  (y : 'a)      x = y; x+1
let f1'' (y : 'a list) x = y; x+1

let f2'  (f : unit -> 'a)      = f(); 5
let f2'' (f : unit -> 'a list) = f(); 5

f1' and f2' give you no warning but f1'' and f2'' do.

Why only for f1'' and f2''? Since OCaml type checker surely knows that the types of e1 in e1 ; e2 are not unit (they are 'a list).

For f1' and f2', the type of e1 is a type variable 'a. They may be instantiated to unit depending on how f1' and f2' are used, so there is a chance that they can be used "properly". Thinking of this possibility, the compiler does not warn them.

I personally prefer to simply force the type of e1's type in e1 ; e2 be unit. But OCaml is more relaxed here.