[Agda] implicit arguments weirdness

[Florent Balestrieri]

Hi Christoph,

Sorry, in the previous message, I mistyped `k = k' instead of
`n = k' so you should read:

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

where the signature of `cons' is:

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

@Christoph {
You said : `Agda probably does not know at the point. Just
say {k : \bn}'

But I believe it is unnecessary, because agda can infere
the type from the fact that `k' given as an argument to
`cons' would be constrained to be `Nat' since `Vec _ k'
appears in the signature of `cons'.

Anyway, even if I write instead:

> \ (k : Nat) -> cons {k} x

the same problem arise; the error is now:

> Nat !=< Set
> when checking that the expression k has type Set

And similarly if I give the argument name, agda accepts the
program:

> \ (k : Nat) -> cons {n = k} x

Also, in your answer, when you say `n = k is a Set', I'm
confused: it is the equal symbol here, not the \== of
propositional equality. I'm talking about the implicit
variable syntax when you give a name to the argument (which
should match the name given in the definition).
}

Cheers
-- Florent