[Agda] implicit arguments weirdness

[Christoph HERRMANN]

On 16 Dec 2009, at 17:06, Christoph HERRMANN wrote:

> 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}"

Sorry, I meant say "{n : Nat}" in the type signature for cons.
> 
>> 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
> 
> 
> 
> 
> _______________________________________________
> 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