RankNTypes and PolyKinds

Question

What is the difference between f1 and f2?

$ ghci -XRankNTypes -XPolyKinds
Prelude> let f1 = undefined :: (forall a        m. m a -> Int) -> Int
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int
Prelude> :t f1
f1 :: (forall            (a :: k) (m :: k -> *). m a -> Int) -> Int
Prelude> :t f2
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) -> Int

Related to this question on RankNTypes and scope of forall. Example taken from the GHC user's guide on kind polymorphism.

Answer 1

f2 requires its argument to be polymorphic in the kind k, while f1 is just polymorphic in the kind itself. So if you define

{-# LANGUAGE RankNTypes, PolyKinds #-}
f1 = undefined :: (forall a m. m a -> Int) -> Int
f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int
x = undefined :: forall (a :: *) m. m a -> Int

then :t f1 x types fine, while :t f2 x complains:

*Main> :t f2 x

<interactive>:1:4:
    Kind incompatibility when matching types:
      m0 :: * -> *
      m :: k -> *
    Expected type: m a -> Int
      Actual type: m0 a0 -> Int
    In the first argument of ‘f2’, namely ‘x’
    In the expression: f2 x