title: Write length function for list with statically typed length
body: <p>Given a list with a statically typed length (taking <a href="http://jeltsch.wordpress.com/2012/04/30/dependently-typed-programming-and-theorem-proving-in-haskell/" rel="nofollow">this</a> as an example):</p>
  
  <pre><code>data Zero
  
  data Succ nat
  
  data List el len where
      Nil  ::                      List el Zero
      Cons :: el -&gt; List el len -&gt; List el (Succ len)
  </code></pre>
  
  <p>is it possible to write a length function that calculates the length using the static typing rather than the usual recursion?</p>
  
  <p>My efforts thus far have led me to the conclusion that it is not possible, as it would require "unlifting" the type information in order to recur on it:</p>
  
  <pre><code>class HasLength a where
      length :: a -&gt; Natural
  
  instance HasLength (List el Zero) where
      length _ = 0
  
  instance HasLength (List el (Succ len)) where
      length _ = 1 + *how to recur on type of len*
  </code></pre>
  
  <p>However, I am only just beginning to learn about all the magic possible with types, so I know that my not being able to conceive of a solution does not imply the absence of one.</p>
  
  <p><strong>update</strong></p>
  
  <p>Since length returns Natural, I incorrectly wrote <code>length _ = 1 + ...</code>. The correct instance (using the answer given below) is</p>
  
  <pre><code>instance HasLength (List el len) =&gt; HasLength (List el (Succ len)) where
      length _ = succ $ length (undefined :: List el len)
  </code></pre>