Convert list to safe for vector

Question

I am trying to write a function

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

using this vector definition

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 gives an 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 due to the type signature (:|).

Is there any way around this error?

Answer 1

The mistake is that your type signature is universally quantified in n, that is, it says "for anyone n, we can build a length vector nfrom a list." It is easy, the definition of the function states that the vector always has the length of the given list.

, ( " n, n - " ). , - . , , - GADT,

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

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