Implementing a type class using a GADT

Question

I have written the following linear algebra vector in Haskell

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

data Vector n e where
    Nil :: Vector Zero e
    (:|) :: (Show e, Num e) => e -> Vector n e -> Vector (Succ n) e
infixr :|

instance Foldable -- ... Vector ..., but how do I implement this?

When I try to implement Foldable, I run into the problem that Zero and Succ have different definitions (ie. * and * -> *).

Is there an obvious solution to this problem?

Answer 1

It's just

instance Foldable (Vector n) where
  fold Nil       = mempty
  fold (a :| as) = a <> fold as

I would not recommend adding constraints to the e type, though.