title: Can I provide the type-checker with proofs about inductive naturals in GHC 7.6?
body: <p>GHC 7.6.1 comes with new features for programming at the type level, including <a href="http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/promotion.html">datatype promotion</a>. Taking the example about type-level naturals and vectors from there, I'd like to be able to write functions on vectors that rely on basic laws of arithmetic.</p>
  
  <p>Unfortunately, even though the laws I want are typically easy to prove on inductive naturals by case analysis and induction, I'm doubt I can convince the type-checker of this. As a simple example, type-checking the naive reverse function below requires a proof that <code>n + Su Ze ~ Su n</code>.</p>
  
  <p>Is there any way I can supply that proof, or am I really in the realm of full-blown dependent types now?</p>
  
  <pre><code>{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TypeOperators #-}
  
  data Nat = Ze | Su Nat
  
  data Vec :: * -&gt; Nat -&gt; * where
    Nil  :: Vec a Ze
    Cons :: a -&gt; Vec a n -&gt; Vec a (Su n)
  
  type family (m :: Nat) + (n :: Nat) :: Nat
  
  type instance Ze + n = n
  type instance (Su m + n) = Su (m + n)
  
  append :: Vec a m -&gt; Vec a n -&gt; Vec a (m + n)
  append Nil ys = ys
  append (Cons x xs) ys = Cons x (append xs ys)
  
  rev :: Vec a n -&gt; Vec a n
  rev Nil = Nil
  rev (Cons x xs) = rev xs `append` Cons x Nil
  </code></pre>