[Agda] implicit parameters and 'with'

[Ulf Norell]

On Thu, Apr 15, 2010 at 6:38 PM, Florent Balestrieri <fbalestrieri at orange.fr
> wrote:

> Hello,
>
> I noticed a weird behaviour of the typechecker. If you
> confirm that it is not right then I will take the time to
> fill a bug report.
>
> Here is the problem: when an expression is on the right hand
> side of a function declaration, Agda doesn't have any trouble
> filling the implicit variables ; but if I move that
> expression on the left hand side, using the 'with' construct,
> then Agda fails. The example is quite complex so I didn't
> want to spend ages simplifying it in case the behaviour
> turned out to be known.
>

The difference might be that when you put an expression in a with the
type checker has no idea what the type of the expression should be,
whereas when it appears in a right hand side the expected type is known.

In some cases you'd expected it to work though. For instance,

nil : {A : Set} -> List A

foo : List Nat
foo with nil
... | xs = xs

In this case the type checker ought to be able to figure out that the
implicit argument to nil must be Nat.

I've opened a new issue for this (
http://code.google.com/p/agda/issues/detail?id=261).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100415/2fa59ed4/attachment.html