Haskell beginner here. I've defined the following types:

```
data Nat = Z | S Nat
data Vector a n where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixl 5 :-
```

I'm trying to write the function, takeWhileVector which behaves the same as takeWhile does on lists, but on Vectors.

My implementation is as follows:

```
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
takeWhileVector f Nil = Nil
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil
```

This doesn't compile and produces the following error:

```
Could not deduce (m ~ 'S n0)
from the context (n ~ 'S n1)
bound by a pattern with constructor
:- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n),
in an equation for ‘takeWhileVector’
at takeWhileVector.hs:69:20-26
‘m’ is a rigid type variable bound by
the type signature for
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
at takeWhileVector.hs:67:20
Expected type: Vector a m
Actual type: Vector a ('S n0)
Relevant bindings include
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
(bound at takeWhileVector.hs:69:1)
In the expression: (x :- takeWhileVector f xs)
In an equation for ‘takeWhileVector’:
takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)
```

I would have thought that my type definition for takeWhileVector says the following:

For all types 'a' and 'n's of kind Nat, this function returns a 'Vector a m', where 'm' is kind Nat.

Do I need to change the type signature of takeWhileVector to be more specific so that it shows that the result is Vector a (m :: Nat)? Otherwise, how can I change this to have it compile?