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

Answer 2

The type of f1 places more restrictions on its definition, while the type of f2 places more restrictions on its argument.

That is: the type of f1 requires its definition to be polymorphic in the kind k, while the type of f2 requires its argument to be polymorphic in the kind k.

f1 :: forall (k::BOX). (forall          (a::k) (m::k->*). m a -> Int) -> Int
f2 ::                  (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int

-- Show restriction on *definition*
f1 g = g (Just True)  -- NOT OK. f1 must work for all k, but this assumes k is *
f2 g = g (Just True)  -- OK

-- Show restriction on *argument* (thanks to Ørjan)
x = undefined :: forall (a::*) (m::*->*). m a -> Int
f1 x  -- OK
f2 x  -- NOT OK. the argument for f2 must work for all k, but x only works for *

Answer 3

Let's be bloody. We must quantify everything and give the domain of quantification. Values have types; type-level things have kinds; kinds live in BOX.

f1 :: forall (k :: BOX).
      (forall (a :: k) (m :: k -> *). m a -> Int)
      -> Int

f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int)
      -> Int

Now, in neither example type is k quantified explicitly, so ghc is deciding where to put that forall (k :: BOX), based on whether and where k is mentioned. I am not totally sure I understand or am willing to defend the policy as stated.

Ørjan gives a good example of the difference in practice. Let's be bloody about that, too. I'll write /\ (a :: k). t to make explicit the abstraction that corresponds to forall, and f @ type for the corresponding application. The game is that we get to pick the @-ed arguments, but we have to be ready to put up with whatever /\-ed arguments the devil may choose.

We have

x :: forall (a :: *) (m :: * -> *). m a -> Int

and may accordingly discover that f1 x is really

f1 @ * (/\ (a :: *) (m :: * -> *). x @ a @ m)

However, if we try to give f2 x the same treatment, we see

f2 (/\ (k :: BOX) (a :: k) (m :: k -> *). x @ ?m0 @ ?a0)
?m0 :: *
?a0 :: * -> *
where  m a = m0 a0

The Haskell type system treats type application as purely syntactic, so the only way that equation can be solved is by identifying the functions and identifying the arguments

(?m0 :: * -> *) = (m :: k -> *)
(?a0 :: *)      = (a :: k)

but those equations are not even well kinded, because k is not free to be chosen: it's being /\-ed not @-ed.

Generally, to get to grips with these uber-polymorphic types, it's good to write out all the quantifiers and then figure out how that turns into your game against the devil. Who chooses what, and in what order. Moving a forall inside an argument type changes its chooser, and can often make the difference between victory and defeat.