7.8. Kind polymorphism

This section describes kind polymorphism, and extension enabled by -XPolyKinds. It is described in more detail in the paper Giving Haskell a Promotion, which appeared at TLDI 2012.

7.8.1. Overview of kind polymorphism

Currently there is a lot of code duplication in the way Typeable is implemented (Section 7.5.3, “Deriving clause for extra classes (Typeable, Data, etc)”):

class Typeable (t :: *) where
  typeOf :: t -> TypeRep

class Typeable1 (t :: * -> *) where
  typeOf1 :: t a -> TypeRep

class Typeable2 (t :: * -> * -> *) where
  typeOf2 :: t a b -> TypeRep

Kind polymorphism (with -XPolyKinds) allows us to merge all these classes into one:

data Proxy t = Proxy

class Typeable t where
  typeOf :: Proxy t -> TypeRep

instance Typeable Int  where typeOf _ = TypeRep
instance Typeable []   where typeOf _ = TypeRep

Note that the datatype Proxy has kind forall k. k -> * (inferred by GHC), and the new Typeable class has kind forall k. k -> Constraint.

7.8.2. Overview

Generally speaking, with -XPolyKinds, GHC will infer a polymorphic kind for un-decorated whenever possible. For example:

data T m a = MkT (m a)
-- GHC infers kind   T :: forall k. (k -> *) -> k -> *

Just as in the world of terms, you can restrict polymorphism using a signature (-XPolyKinds implies -XKindSignatures):

data T m (a :: *) = MkT (m a)
-- GHC now infers kind   T :: (* -> *) -> * -> *

There is no "forall" for kind variables. Instead, you can simply mention a kind variable in a kind signature, thus:

data T (m :: k -> *) a = MkT (m a)
-- GHC now infers kind   T :: forall k. (k -> *) -> k -> *

7.8.3. Polymorphic kind recursion and complete kind signatures

Just as in type inference, kind inference for recursive types can only use monomorphic recursion. Consider this (contrived) example:

data T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind  T :: (* -> *) -> * -> *

The recursive use of T forced the second argument to have kind *. However, just as in type inference, you can achieve polymorphic recursion by giving a complete kind signature for T. The way to give a complete kind signature for a data type is to use a GADT-style declaration with an explicit kind signature thus:

data T :: (k -> *) -> k -> * where
  MkT :: m a -> T Maybe (m a) -> T m a

The complete user-supplied kind signature specifies the polymorphic kind for T, and this signature is used for all the calls to T including the recursive ones. In particular, the recursive use of T is at kind *.

What exactly is considered to be a "complete user-supplied kind signature" for a type constructor? These are the forms:

  • A GADT-style data type declaration, with an explicit "::" in the header. For example:

    data T1 :: (k -> *) -> k -> *       where ...   -- Yes  T1 :: forall k. (k->*) -> k -> *
    data T2 (a :: k -> *) :: k -> *     where ...   -- Yes  T2 :: forall k. (k->*) -> k -> *
    data T3 (a :: k -> *) (b :: k) :: * where ...   -- Yes  T3 :: forall k. (k->*) -> k -> *
    data T4 a (b :: k)             :: * where ...   -- YES  T4 :: forall k. * -> k -> *
    
    data T5 a b                         where ...   -- NO  kind is inferred
    data T4 (a :: k -> *) (b :: k)      where ...   -- NO  kind is inferred
    

    It makes no difference where you put the "::" but it must be there. You cannot give a complete kind signature using a Haskell-98-style data type declaration; you must use GADT syntax.

  • A type or data family declaration always have a complete user-specified kind signature; no "::" is required:

    data family D1 a           	-- D1 :: * -> *
    data family D2 (a :: k)    	-- D2 :: forall k. k -> *
    data family D3 (a :: k) :: *    -- D3 :: forall k. k -> *
    type family S1 a :: k -> *      -- S1 :: forall k. * -> k -> *
    

In a complete user-specified kind signature, any un-decorated type variable to the left of the "::" is considered to have kind "*". If you want kind polymorphism, specify a kind variable.