title: Lists of fixed length and type literals
body: <p>I'm trying to define a type for lists of fixed length in Haskell. When I use the standard way to encode natural numbers as types in unary, everything works fine. However, when I try to build everything on GHC's type literals, I run into tons of problems.</p>
  
  <p>My first shot at the desired list type was</p>
  
  <pre><code>data List (n :: Nat) a where
    Nil :: List 0 a
    (:&gt;) :: a -&gt; List n a -&gt; List (n+1) a
  </code></pre>
  
  <p>which unfortunately didn't allow for writing a zip function with type</p>
  
  <pre><code>zip :: List n a -&gt; List n b -&gt; List n (a,b)
  </code></pre>
  
  <p>I could solve this problem by subtracting 1 from the type variable <code>n</code> in the type of <code>(:&gt;)</code>:</p>
  
  <pre><code>data List (n :: Nat) a where
    Nil :: List 0 a
    (:&gt;) :: a -&gt; List (n-1) a -&gt; List n a -- subtracted 1 from both n's
  </code></pre>
  
  <p>Next, I tried to define an append function:</p>
  
  <pre><code>append :: List n1 a -&gt; List n2 a -&gt; List (n1 + n2) a
  append Nil       ys = ys
  append (x :&gt; xs) ys = x :&gt; (append xs ys)
  </code></pre>
  
  <p>Unfortunately, GHC tells me</p>
  
  <pre><code>Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’
  </code></pre>
  
  <p>Adding the constraint <code>((n1 + n2) - 1) ~ ((n1 - 1) + n2)</code> to the signature doesn't solve the problems since GHC complains</p>
  
  <pre><code>Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1))
  from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2))
  </code></pre>
  
  <p>Now, I'm obviously caught in some kind of infinite loop.</p>
  
  <p>So, I'd like to know if it is possible to define a type for lists of fixed length using type literals at all. Did I perhaps even oversee a library for precisely this purpose? Basically, the only requirement is that I want to write something like <code>List 3 a</code> instead of <code>List (S (S (S Z))) a</code>.</p>