title: Datatype promotion for dependently challenged
body: <p>After reading through the ghc 7.4. pre-release notes and the <a href="http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf">Giving Haskell a Promotion</a> paper, I'm still confused on what you actually do with promoted types. For example, the GHC manual gives the following examples on promoted datatypes:</p>
  
  <pre><code>data Nat = Ze | Su Nat
  
  data List a = Nil | Cons a (List a)
  
  data Pair a b = Pair a b
  
  data Sum a b = L a | R b
  </code></pre>
  
  <p>What kind of uses do these have as kinds? Can you give (code) examples?</p>