[Agda] implicit arguments weirdness

[Andreas Abel]

Florent Balestrieri a écrit :
> where the signature of `cons' is:
> 
>> cons : {n} (x : a) (xs : Vec a n) -> Vec a (suc n)

The complete type signature for cons is

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

This explains why Agda complains about k not being a Set.

The parameters of an inductive data type (here: Vec) become 
automatically hidden arguments of their constructors (here: cons).

If you do not address implicit arguments by name, then it is first come, 
first serve.

> 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

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/