[Agda] implicit arguments weirdness

[Florent Balestrieri]

Hello,

I am puzzled by the behaviour of agda (2.2.4). Given the
following function:

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

If I write (for some `x' with a given type `A')

 > \ k -> cons {k} x

then agda complains:

 > _97 n x v !=< Set
 > when checking that the expression k has type Set

Which is crazy since `k' is supposed to have type `Nat', not
`Set'.  Now if I write:

 > \ k -> cons {k = k} x

then it's fine.

My conclusions are:

  1) There is only one implicit argument, so why can't agda
     figure it out in the first case?
 
  2) The error message is misleading because it says `Set'
   instead of `Nat'

Cheers
-- Florent