Why is this eta expansion necessary?

Question

Can someone help me understand this/point me to some reading materials? The following works fine:

type F a b = Functor f => f a -> f b
fComp :: F b c -> F a b -> F a c
fComp f f' = f . f'

But if I write fComp = (.) instead, the type checker complains:

Couldn't match type ‘b0 -> f c’
              with ‘forall (f1 :: * -> *). Functor f1 => f1 b -> f1 c’

(This specific example isn't particularly useful; I'm just trying to shrink an example that came up while studying lenses.)

Answer 1

fComp has a higher-rank type and type inference for higher-rank types is very limited. It might be a little easier to understand (but much longer!) if we expand the type synonym:

fComp :: forall f a b c. Functor f => 
                (forall f1. Functor f1 => f1 b -> f1 c) ->
                (forall f2. Functor f2 => f2 a -> f2 b) ->
                (f a -> f c)

The higher-rank types of f and f' are specified explicitly in this type signature. This lets the type inference start already knowing the types of f and f' and so being able to unify them with the type of ..

However, if you get rid of f and f', the type that . has to take is not known. Unfortunately, the system can't infer higher-rank types like this, so you get a type error.

In essence, the compiler can't create higher-rank types to fill unknowns during type inference and has to rely on programmer annotations and we need both the name (f and f') and the type signature to get those annotations.

An easier example to understand would be a higher-rank id function:

myId :: (forall a. a) -> (forall b. b)

The definition myId x = id x compiles, but myId = id gives the following error:

/home/tikhon/Documents/so/eta-expansion-needed.hs:11:8:
    Couldn't match type ‘b’ with ‘forall a. a’
      ‘b’ is a rigid type variable bound by
          the type signature for myId :: (forall a. a) -> b
          at /home/tikhon/Documents/so/eta-expansion-needed.hs:11:1
    Expected type: (forall a. a) -> b
      Actual type: b -> b
    In the expression: id
    In an equation for ‘myId’: myId = id
Failed, modules loaded: none.

(Keep in mind that forall b. (forall a. a) -> b is the same as (forall a. a) -> (forall b. b).)