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