typechecking too eager?

[Andres Loeh]

> So, does that mean that ideally we would like it to type
> check, but for implementation reasons it cannot easily
> be done without a type signature?

Not purely for implementation reasons, but also because 
of theoretical limitations. Depending on what fragment of
System F you want to allow, you lose either decidability
of type inference or the principal types property if you
do not choose to require explicit type signatures.

There are certainly design choices here, and one can certainly
implement a system that would infer a type for your example
without an explicit signature. However, the current implementation
has the advantage of (a) being not difficult to implement, and
(b) having clear rules for when explicit type signatures are
required (the exact rules are given in the "Practical type
inference ..." paper by Peyton Jones and Shields). 

A more powerful alternative is described in the "MLF"
paper by Le Botlan and Remy.

The use of type signatures when things get difficult isn't
uncommon in Haskell: type signatures are required for
functions involving polymorphic recursion, and for functions
involving ambiguous overloading, and nowadays for some 
functions that make use of GADTs.

Cheers,
  Andres