Write length function for list with statically typed length

Given a list with a statically typed length (taking this as an example): ``` data Zero data Succ nat data List el len where Nil :: List el Zero Cons :: el -> List el len -> List el (Succ len) ``` is it possible to write a length function that calculates the length using the static typing rather than the usual recursion? 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: ``` class HasLength a where length :: a -> 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* ``` 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. update Since length returns Natural, I incorrectly wrote `length _ = 1 + ...`. The correct instance (using the answer given below) is ``` instance HasLength (List el len) => HasLength (List el (Succ len)) where length _ = succ $ length (undefined :: List el len) ```