Re: [Haskell-cafe] Is "let" special?

2010/11/3 Petr Pudlak :

...

f = (\x -> x x) (\y -> y) g = let x = \y -> y in x x

The function "f" is not typable in the Hindley-Milner type system, while "g" is is (and its type is "a -> a"). The reason is that in the first case (f), the typing system tries to assign a single type to "x", which is impossible

And just to be clear, this is specific to the H-M system. The function "f" is typeable--but not inferable--in GHC-Haskell-with-extensions, i.e. the definition:

{-# LANGUAGE Rank2Types #-}

f = ((\x -> x x) :: forall a. (forall b. b -> b) -> a -> a) (\y -> y)

...is valid and will have the correct type for "f". The more restricted system provided by H-M is interesting largely because everything typeable in it is also inferable. - C.