Converting a list to a type-safe vector
haskell
Solution
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
Problem
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?