title: What is the DataKinds extension of Haskell?
body: <p>I am trying to find an explanation of the DataKinds extension that will make sense to me having come from only having read <a href="http://learnyouahaskell.com/">Learn You a Haskell</a>. Is there a standard source that will make sense to me with what little I've learned?</p>
  
  <p>Edit: For example the <a href="http://www.haskell.org/ghc/docs/7.6.2/html/users_guide/promotion.html">documentation</a> says</p>
  
  <blockquote>
    <p>With -XDataKinds, GHC automatically promotes every suitable datatype
    to be a kind, and its (value) constructors to be type constructors.
    The following types</p>
  </blockquote>
  
  <p>and  gives the example</p>
  
  <pre><code>data Nat = Ze | Su Nat
  </code></pre>
  
  <p>give rise to the following kinds and type constructors:</p>
  
  <pre><code>Nat :: BOX
  Ze :: Nat
  Su :: Nat -&gt; Nat
  </code></pre>
  
  <p>I am not getting the point. Although I don't understand what <code>BOX</code> means, the statements <code>Ze :: Nat</code> and <code>Su :: Nat -&gt; Nat</code> seem to state what is already normally the case that Ze and Su are normal data constructors exactly as you would expect to see with ghci</p>
  
  <pre><code>Prelude&gt; :t Su
  Su :: Nat -&gt; Nat
  </code></pre>