[Agda] implicit arguments weirdness

[Florent Balestrieri]

I that I think I can answer my own question: in the
constructor

 > _::_ : {n} (x : a) (xs : Vec a n) -> Vec a (suc n)

there is a first implicit argument which is {a : Set} the
parameter from the data specification and that we don't
repeat for the constructor signatures.

so when I write \ k -> _::_ {k} x

agda tries use `k' for the variable `a' of the set instead of
the variable `n' as I thought before.

Sorry for polluting the mailing list with such triviality.

Cheers -- Florent