title: Kind Signatures
body: <p>I am going through the Haskell wiki books GADTS</p>
  
  <p><a href="https://en.wikibooks.org/wiki/Haskell/GADT" rel="noreferrer">https://en.wikibooks.org/wiki/Haskell/GADT</a> guide.</p>
  
  <p>I was tracking pretty well until a Kind signature was added which generalizes the constrained type of the Cons constructor.</p>
  
  <pre><code>data Safe
  data NotSafe
  
  data MarkedList             ::  * -&gt; * -&gt; * where
    Nil                       ::  MarkedList t NotSafe
    Cons                      ::  a -&gt; MarkedList a b -&gt; MarkedList a c
  
  safeHead                    ::  MarkedList a Safe -&gt; a
  safeHead (Cons x _)          =  x
  
  
  silly 0                      =  Nil
  silly 1                      =  Cons () Nil
  silly n                      =  Cons () $ silly (n-1)
  </code></pre>
  
  <p>With the Kind Signature I can use the Cons constructor to construct and pattern match against both Safe and Unsafe MarkedLists. While I understand what going on I am unfortunately having trouble building any intuition as to how the Kind Signature is allowing this. Why do I need the Kind Signature? What is the Kind Signature doing? </p>