Converting a list to a type-safe vector

Question

I am attempting to write the function

fromList :: [e] -> Vector n e
fromList [] = Nil
fromList (x:xs) = x :| fromList xs

using this definition of a vector

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

data Vector n e where
  Nil  :: Vector Zero e
  (:|) :: e -> Vector n e -> Vector (Succ n) e

infixr :|

However, Haskell is giving the error

    Couldn't match type 'Zero with 'Succ n0
    Expected type: Vector n e
      Actual type: Vector ('Succ n0) e
    In the expression: x :| fromList xs
    In an equation for `fromList': fromList (x : xs) = x :| fromList xs
Failed, modules loaded: none.

I believe the error is being thrown because of the type signature of (:|).

Is there a way to get around this error?

Answer 1

The error is that your type signature is universally quantified in n, i.e. it says "for any n, we can build a vector of length n from the list". Incompatibly, the function definition states that the vector has always the length of the given list.

Basically, you need existential quantification to define this function ("depending on the list length, there will be an n such that n is the length of the result vector"). Discussed only just yesterday, you can't have existentially-quantified type variables in a signature. What you can have though are existential types – preferrably again written as a GADT,

data DynVector e where
  DynVector :: Vector n e -> DynVector e

Then you can define

fromList' :: [e] -> DynVector e
fromList' [] = DynVector Nil
fromList' (x:xs) = case fromList xs of
   DynVector vs -> DynVector $ x :| vs