Why is this eta expansion necessary?

haskell

Solution

`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)`.)

Problem

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.)

Original source