Am I correct in my understanding of these types?

  Vect a n = vector of a with known length n
  (n ** Vect a n) = vector of a with unknown length n

When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.