title: Add Type Level Natural Numbers
body: <p>I assume, that it is not possible to just add two type level natural numbers in haskell. Is this true? </p>
  
  <p>Suppose the natural numbers are defined like so:</p>
  
  <pre><code>class HNat a
  
  data HZero
  instance HNat HZero
  
  data HSucc n
  instance (HNat n) =&gt; HNat (HSucc n)
  </code></pre>
  
  <p>Is it pssible to define HAdd in a way similar to:</p>
  
  <pre><code>class (HNat n1, HNat n2, HNat ne) =&gt; HAdd n1 n2 ne | n1 n2 -&gt; ne
  instance             HAdd HZero HZero HZero
  instance (HNat x) =&gt; HAdd HZero x     x
  instance (HNat n1 
           ,HNat x) =&gt; HAdd (HSucc n1)  x (HAdd n1 (HSucc x) (???))
  </code></pre>