[Agda] implicit arguments weirdness

[Christoph HERRMANN]

Hi Florent,

On 16 Dec 2009, at 17:01, Florent Balestrieri wrote:

> 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'.  

Agda probably does not know at the point. Just say  "{k : \bn}"

> Now if I write:
> 
>> \ k -> cons {k = k} x
> 
> then it's fine.

Because k=k is a set.

I'm surprised that it works with k=k though without
specifying k.

> 
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532