error

unzip_hvect.idr:7:1-6:When checking left hand side of unzip_hvect.unzip:
When checking an application of unzip_hvect.unzip:
        Type mismatch between
                HVect [] (Type of [])
        and
                HVect (zipWith (\t1 => \t2 => (t1, t2)) ts1 ts2) (Expected type)

        Specifically:
                Type mismatch between
                        []
                and
                        zipWith (\t1 => \t2 => (t1, t2)) ts1 ts2
Holes: unzip_hvect.unzip

unzip_hvect.idr

module zip_hvect

import Data.Vect
import Data.HVect

unzip : {ts1, ts2 : Vect n Type} -> HVect (zipWith (\t1,t2 => the Type (t1, t2)) ts1 ts2) -> (HVect ts1, HVect ts2)
unzip []           = ([], [])
unzip ((l, r)::xs) with (unzip xs)
  | (lefts, rights) = (l::lefts, r::rights)

This works:

unzip : {ts1, ts2 : Vect n Type} -> HVect (zipWith (\t1,t2 => the Type (t1, t2)) ts1 ts2) -> (HVect ts1, HVect ts2)
unzip {ts1 = []} {ts2 = []} [] = ([], [])
unzip {ts1 = t1 :: ts1} {ts2 = (t2 :: ts2)} ((x, y) :: zs) with (unzip zs)
  unzip {ts1 = t1 :: ts1} {ts2 = (t2 :: ts2)} ((x, y) :: zs) | (xs, ys) = (x :: xs, y :: ys)

So it might be a bug in dependent pattern matching here - I'd have to look closer.

It passes the type check and compiles, but

zip_hvect.unzip [(1, 2)]

results in an error

(input):1:17:When checking an application of function zip_hvect.unzip:
        Type mismatch between
                HVect [(Integer, Integer)] (Type of [(1, 2)])
        and
                HVect (zipWith (\t1 => \t2 => (t1, t2)) ts1 ts2) (Expected type)

        Specifically:
                Type mismatch between
                        [(Integer, Integer)]
                and
                        zipWith (\t1 => \t2 => (t1, t2)) ts1 ts2

I would expect

([1], [2]) : (HVect [Integer], HVect [Integer])

The type checker won't run the computation backwards for you here. But you can provide it with the necessary info:

λΠ> zip_hvect.unzip (the (HVect (zipWith (\x,y=>(x,y)) [Int] [Nat])) [(1,2)])
([1], [2]) : (HVect [Int], HVect [Nat])

What causes this issue?