title: How exactly do kind lists work?
body: <p>I've been reading on <code>vinyl</code> recently, which uses weird "list of kinds" kinda types. After reading a bit on kinds and vinyl, I've gotten somewhat of an intuitive understanding of them, and I've been able to hack this together</p>
  
  <pre><code>{-# LANGUAGE DataKinds,
               TypeOperators,
               FlexibleInstances,
               FlexibleContexts,
               KindSignatures,
               GADTs #-}
  module Main where
  
  -- from the data kinds page, with HCons replaced with :+:
  data HList :: [*] -&gt; * where
    HNil :: HList '[]
    (:+:) :: a -&gt; HList t -&gt; HList (a ': t)
  
  infixr 8 :+:
  
  
  instance Show (HList '[]) where
    show _ = "[]"
  instance (Show a, Show (HList t)) =&gt; Show (HList (a ': t)) where
    show (x :+: xs) = show x ++ " : " ++  show xs
  
  class ISum a where
    isum :: Integral t =&gt; a -&gt; t
  
  instance ISum (HList '[]) where
    isum _ = 0
  
  
  instance (Integral a, ISum (HList t)) =&gt; ISum (HList (a ': t)) where
    isum (x :+: xs) = fromIntegral x + isum xs
  
  -- explicit type signatures just to check if I got them right
  alist :: HList '[Integer]
  alist = (3::Integer) :+: HNil
  
  blist :: HList '[Integer,Int]
  blist =  (3::Integer) :+: (3::Int) :+: HNil
  
  main :: IO ()
  main = do
    print alist
    print (isum alist :: Int)
    print blist
    print (isum blist :: Integer)
  </code></pre>
  
  <p><code>:i HList</code> yields</p>
  
  <pre><code>data HList $a where
    HNil :: HList ('[] *)
    (:+:) :: a -&gt; (HList t) -&gt; HList ((':) * a t)
      -- Defined at /tmp/test.hs:10:6
  instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10
  instance (Show a, Show (HList t)) =&gt; Show (HList ((':) * a t))
    -- Defined at /tmp/test.hs:19:10
  instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10
  instance (Integral a, ISum (HList t)) =&gt; ISum (HList ((':) * a t))
    -- Defined at /tmp/test.hs:29:10
  *Main&gt; :i HList
  data HList $a where
    HNil :: HList ('[] *)
    (:+:) :: a -&gt; (HList t) -&gt; HList ((':) * a t)
      -- Defined at /tmp/test.hs:10:6
  instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10
  instance (Show a, Show (HList t)) =&gt; Show (HList ((':) * a t))
    -- Defined at /tmp/test.hs:19:10
  instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10
  instance (Integral a, ISum (HList t)) =&gt; ISum (HList ((':) * a t))
    -- Defined at /tmp/test.hs:29:10
  </code></pre>
  
  <p>From which I gather that <code>'[]</code> is sugar for <code>'[] *</code> and <code>x ': y</code> for <code>(':) * x y</code>. What is that * doing there? Is it the kind of the list elements? Also, what exactly is such a list anyway? Is it something built into the language?</p>