RankNTypes and PolyKinds
haskell, higher-rank-types, polykinds, polymorphism
Solution
`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
Problem
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.