Rank-1 Type requires Rank2Types extension

Question

Haskell wiki page on Rank-N-Types tells that this type

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

has Rank 1. I believe in this fact and it seems quite understandable for me (keeping in mind what I already know about how to determine rank of function). However, when I'm trying to write next code:

{-# LANGUAGE ExplicitForAll #-}

foo :: forall a . a -> (forall b . b -> a)
foo = undefined

it doesn't compile (ghc 8.0.1) resulting in next error:

• Illegal polymorphic type: forall b. b -> a
  Perhaps you intended to use RankNTypes or Rank2Types
• In the type signature:
    foo :: forall a. a -> (forall b. b -> a)

So I wonder: does foo type really have Rank-2? Or GHC just doesn't have some smart mechanism to detect true rank of function? Sometimes in educational purposes I want to have some ghci command like rank to inspect true ranks of function types...

ghci> :rank foo
foo :: forall a . a -> (forall b . b -> a)  -- Rank 1

Answer 1

The reason for this behavior is documented in the typechecker's TcValidity module.

Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Technically
            Int -> forall a. a->a
is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
validity checker allow a forall after an arrow only if we allow it
before — that is, with Rank2Types or RankNTypes

I'm not a good language lawyer but it seems the Haskell 98 specification seems to prevent quantifiers after any arrows, despite that that is a more stringent requirement than rank-1'd-ness. As Haskell 2010 only lightly updated the specification I believe this is applicable to 2010 as well.

I believe (but am not certain) the way GHC encodes this is with a let r1 = LimitedRank True r0 in the checkValidType function, which specifies that foralls can appear at the beginning of a type declaration but subsequent function arguments must be rank zero, which precludes the forall b. b -> a in your type.

standard disclaimer: i'm no expert, all i had was github search