[Agda] implicit arguments weirdness

[Nils Anders Danielsson]

On 2009-12-16 17:01, Florent Balestrieri wrote:
> 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)

I assume that cons is a constructor. The parameters of a data type are
implicit arguments to its constructors (but only in expressions, not in
patterns).

> 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

It seems as if Agda knows that the type of k (meta-variable 97) is
distinct from Set, whereas Vec's first parameter has to be a Set.

--
/NAD