Understanding Haskell RankNTypes Error message

I'm trying to understand RankNTypes.

Why does the compiler complain in this case can a NOT be [a]?

> :{
> | tupleF2 :: (forall a . a -> b) -> (a1, a2) -> (b, b)
> | tupleF2 elemF2 (x, y) = (elemF2 x, elemF2 y)
> | :}

> :t tupleF2  tupleF2 :: (forall a. a -> b) -> (a1, a2) -> (b, b)

> :t tupleF2 length

<interactive>:1:9: error:
    • Couldn't match type ‘a’ with ‘[a0]’
      ‘a’ is a rigid type variable bound by
        a type expected by the context:
          forall a. a -> Int
        at <interactive>:1:1-14
      Expected type: a -> Int
        Actual type: [a0] -> Int
    • In the first argument of ‘tupleF2’, namely ‘length’
      In the expression: tupleF2 length

While the following typechecks fine? and t is OK with t a.

> :t tupleF length
tupleF length :: Foldable t => (t a, t a) -> (Int, Int)
:t tupleF
tupleF :: (t -> b) -> (t, t) -> (b, b)

Is the above failure to compile only happens with enabling RankNTypes. Any pointers in understanding what is happening would be great.

Thanks.

Solution

forall a . a -> b is the type of a function f that can convert a value of any type a to some value of type b. Note that f must be ready to accept absolutely anything as input, i.e. all of these must type check

f ()
f 32
f True
f 'a'
f "hello"
f (True, [2], False)

length does not satisfy the requirement since e.g. length () is ill typed -- length wants a foldable (like a list) as input, and () is not OK.

Hence, tupleF2 length is ill typed.

Pragmatically, note that f can only be a constant function, like

f x = True  -- assuming b = Bool

Indeed, parametricity guarantees that only a constant function can have type forall a . a -> b. You can try tupleF2 (const True) ((),"hello") and obtain (True, True).