Left hand side of a generalized zip function never typechecks

I am trying to write a zip function in Idris that combines arbitrarily many vectors of the same length (len) into a single vector of HLists.

That is, I am trying to generalize the following function:

module Zip

import Data.Vect

%default total

zip2 : (Vect len a, Vect len b) -> Vect len (a, b)
zip2 ([], []) = []
zip2 ((x :: xs), (y :: ys)) = (x, y) :: zip2 (xs, ys)

I define my own HList ("heterogenous list") using vectors:

data HList : Vect n Type -> Type  where
  Nil : HList []
  (::) : (x : a) -> (xs : HList as) -> HList (a :: as)

Here is a variant of the zip2 function using this HList:

zip2H : HList [Vect len a, Vect len b] -> Vect len (HList [a, b])
zip2H [[], []] = []
zip2H [(x :: xs), (y :: ys)] = [x, y] :: zip2H [xs, ys]

So far, so good.

Now the general case.

The type signature for arbitrarily many vectors to zip gets a fair bit more complicated, but I am confident that I got it right.

n is the number of vectors to zip. len is the length of each of these vectors:

vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as
-- Example:
-- `vects len [a, b] = [Vect len a, Vect len b]`
-- You cannot pattern-match on types in Idris, so you cannot get an `a` from an `Vect len a`. Instead, I go the other way around in `zip` and pass my `a`s implicitly.

zip : {types : Vect (S n) Type} -> {len : Nat} -> HList (vects len types) -> Vect len (HList types)

Now my problem is: I cannot write even the left hand side of the definition of zip. The type checker keeps complaining.

An example:

zip {n = Z} [xs] = ?zip_rhs1
zip xs = ?zip_rhs2

When checking left hand side of Zip.zip:
When checking an application of Zip.zip:
        Type mismatch between
                HList [a] (Type of [xs])
        and
                HList (Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                 Vect len
                                                                                                      type)
                                                                                              types) (Expected type)

        Specifically:
                Type mismatch between
                        [a]
                and
                        Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                  Vect len
                                                                                                       type)
                                                                                               types

What am I missing? Am I using the implicit parameters in a wrong manner? Do I need to write some proofs? Is there a better way to structure the function type signature?

(My Idris version is 1.3.1-git:a93d8c9.)

EDIT: Using HTNW's code I still get basically the same error:

module Zip

import Data.Vect

%default total

data HList : Vect n Type -> Type  where
  Nil : HList []
  (::) : (x : a) -> (xs : HList as) -> HList (a :: as)

vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as

multiUnCons : {len : Nat} -> {types : Vect n Type} ->
              HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
  | (ys, yss) = (x :: ys, xs :: yss)

zip : {types : Vect n Type} -> {len : Nat} ->
      HList (vects len types) -> Vect len (HList types)
zip {len = Z} _ = []
zip {len = S n} xss with (multiUnCons xss)
  | (ys, yss) = ys :: zip yss

testVectors : HList [Vect 3 Nat, Vect 3 Char]
testVectors = [[1, 2, 3], ['a', 'b', 'c']]

*zip> :t Zip.zip testVectors
(input):1:4-23:When checking an application of function Zip.zip:
        Type mismatch between
                HList [Vect 3 Nat, Vect 3 Char] (Type of testVectors)
        and
                HList (vects len types) (Expected type)

        Specifically:
                Type mismatch between
                        [Vect 3 Nat, Vect 3 Char]
                and
                        Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                  Vect len
                                                                                                       type)
                                                                                               types

RESOLUTION: zip needs more information:

*zip> the (Vect 3 (HList [Nat, Char])) (zip testVectors)
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])

*zip> zip {types=[Nat, Char]} testVectors
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])

Solution

You have to match on types, too. By matching on types, you also reveal something about vects len types, and this is what allows you to further match on the HList (vects len types) argument. Also, the S n length requirement on types is unnecessary and broken. Finally, I think you actually need to recurse on len first, then on types. The recursion on types is best written as a different function:

multiUnCons : {len : Nat} -> {types : Vect n Type} ->
              HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
  | (ys, yss) = (x :: ys, xs :: yss)

And zip itself is pretty simple:

zip : {types : Vect n Type} -> {len : Nat} ->
      HList (vects len types) -> Vect len (HList types)
zip {len = Z} _ = []
zip {len = S n} xss with (multiUnCons xss)
  | (ys, yss) = ys :: zip yss