伊德里斯印章的类型

Question

我想在Idris写一个chop函数。 Haskell的等价物看起来像：

chop :: Int -> [t] -> [[t]]
chop n [] = []
chop n v = take n v : chop n (drop n v)

我在伊德里斯的初步尝试看起来像：

chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop n Nil = Nil
chop n v = (take n v) :: (chop n (drop n v))

类型检查错误：

Type mismatch between
               Vect 0 a (Type of [])
       and
               Vect (mult k n) a (Expected type)

       Specifically:
               Type mismatch between
                       0
               and
                       mult k n