Why does Idris give me Type mismatch error for the following code?

Question

I am a newbie trying to learn Idris and wanted to create a function test that returns a Vector whose type is parameterized by the function argument.

vecreplicate : (len : Nat) -> (x : elem) -> Vect len elem
vecreplicate Z     x = []
vecreplicate (S k) x = x :: vecreplicate k x

test : (k:Nat) -> Nat -> Vect k Int
test Z = vecreplicate Z (toIntegerNat Z)
test k = vecreplicate k (toIntegerNat k)

When I try to compile the code with Idris I get the following type error

Type mismatch between
    Vect len elem (Type of vecreplicate len x)
and
    Nat -> Vect 0 Int (Expected type)

Specifically:
    Type mismatch between
            Vect len
    and
            \uv => Nat -> uv

Why am I getting this error?

Answer 1

test : (k:Nat) -> Nat -> Vect k Int takes two arguments, but you only match on k. That's why the expected type is a lambda (Nat -> Vect 0 Int). Just drop one Nat: test : (k : Nat) -> Vect k Int.

Also, toIntegerNat returns Integer not Int. :search Nat -> Int returns toIntNat, so that's what you want to use there.