I find this slightly more complicated case quite confusing with the current wording:
Prelude> :t (\x -> x) :: (a -> b) -> (a -> a) <interactive>:1:7: Couldn't match expected type `a' against inferred type `b' `a' is a rigid type variable bound by an expression type signature at <interactive>:1:14 `b' is a rigid type variable bound by an expression type signature at <interactive>:1:19 In the expression: x In the expression: (\ x -> x) :: (a -> b) -> (a -> a)
This message suggests that ghc has inferred type b for x.
Not really; but this looks like a nice simple example of what I was referring to: GHC is so careful not to bother the user with scary type stuff that it mentions types as little as possible. In particular, it never mentions the type of 'x'! It only mentions that it has run into 'a' and 'b' somewhere *while looking into 'x's type*, so those are conflicting types for some parts of 'x's type, not 'x's type itself. In more complex code, this peephole view can be really unhelpful, which is why I suggested [1] that type errors should give types for all expressions mentioned in the type error context (here 'x' and '(\x->x)', the latter's type is there only because it was part of the input). Claus [1] http://hackage.haskell.org/trac/ghc/ticket/1928#comment:2