Now, if we switch to an analogous, though slightly more complicated type, GHC's type checker accepts the following code:

    bar :: (forall b. b -> String, Int)
    bar = (const "hi", 0)
    foo :: forall b.(b -> String, Int)
    foo = (const "hi", 0)

however GHC's type checker rejects the following code (I now think this is correct):

    bar :: (forall b. b -> String, Int)
    bar = (const "hi", 0)
    foo :: forall b.(b -> String, Int)
    foo = bar

with the error :

    Couldn't match expected type `b -> String'
           against inferred type `forall b1. b1 -> String'

and yet GHC accepts the following code:

    bar :: (forall b. b -> String, Int)
    bar = (const "hi", 0)
    foo :: forall b.(b -> String, Int)
    foo = (fst bar, snd bar)

which is just the eta-expansion of the previous code.

This behavior seems inconsistent to me. I don't see any reason why the (f = b) should be different than (foo = bar). In fact, thinking more carefully about the types, I think that (f = b) should not type and the eta expansion (f = \x -> b x) should be required.