Breaking Hindley-Milner Typing

Which is the shortest λ-term which cannot be assigned a type in the Hindley-Milner typing discipline but in System F?

Probably self-application, λx. x x.

In Haskell 

    bar :: (forall x. x) -> c
    bar = \ x -> x x
If we leave out the type signature, type inference fails, e.g. 
    $ ghc -fglasgow-exts ...
    Occurs check: cannot construct the infinite type: t = t -> t1
        Expected type: t
        Inferred type: t -> t1
    In the first argument of `x', namely `x'
    In a lambda abstraction: x x
We can also type self-application with the recursive type T = T → T.

Valid HTML 4.01! Andreas Abel, http://www.tcs.informatik.uni-muenchen.de/~abel/fomega/
Last modified: Fri Feb 6 15:21:07 CET 2004 		Valid CSS!