"Eta reduce" is not always held in Haskell?

Question

I found that I can say

{-# LANGUAGE RankNTypes #-}
f1 :: (forall b.b -> b) -> (forall c.c -> c)
f1 f = id f

(and HLint tell me I can do "Eta reduce" here), but

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id

fail to compile:

Couldn't match expected type `c -> c'
            with actual type `forall b. b -> b'
Expected type: (forall b. b -> b) -> c -> c
  Actual type: (forall b. b -> b) -> forall b. b -> b
In the expression: id
In an equation for `f2': f2 = id

Actually I have a similar problem in a more complicated situation but this is the simplest example I can think of. So either HLint is fail to provide proper advise here, or the compiler shall detect this situation, is it?

UPDATE

Another revelent question looks similar. However although both answers are quite useful, neither satisfy me, since they seems not touching the heart of the question.

For example, I am not even allowed to assign id with the proposed rank 2 type:

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id :: (forall b.b -> b) -> (forall c.c -> c)

If the problem is just about type inference, an explicit type notation shall solve it (id have type a -> a, and it has been constrained to (forall b.b -> b) -> (forall c.c -> c). Therefore to justify this use, (forall b.b -> b) must match (forall c.c -> c) and that is true). But the above example shows this is not the case. Thus, this IS a true exception of "eta reduce": you have to explicitly add parameters to both sides to convert a rank 1 typed value in to rank 2 typed value.

But why there is such a limitation? Why the computer cannot unify rank 1 type and rank 2 type automatically (forget about type inference, all types can be given by notations)?

Answer 1

I'm not sure HLint is aware of RankNTypes at all, perhaps not.

Indeed eta reduction is often impossible with that extension on. GHC can't just unify a->a and (forall b.b -> b) -> (forall c.c -> c), otherwise it would completely mess up its type inference capability for Rank1-code¹. OTOH, it's not a problem to unify (forall b.b -> b) with the a argument; the result is confimed to be (forall b.b -> b) which matches with (forall c.c -> c).

---

¹Consider map id [(+1), (*2)]. If id were allowed to have the type you're dealing with, the compiler could end up producing different instance choice for the polymorphic Num functions, which certainly shouldn't be possible. Or should it? I'm not sure, thinking about it...

At any rate, I'm pretty sure its proven that with RankNTypes, full type inference is not possible, so to get it at least in the Rank1 subset GHC must usually default to this as a less-than-possible polymorphic choice.