Write length function for list with statically typed length

Question

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)

Answer 1

For example like this:

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = 1 + length (undefined :: List el len)

Note: this requires ScopedTypeVariables extension.