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