<br><div class="gmail_quote">On Thu, Apr 15, 2010 at 6:38 PM, Florent Balestrieri <span dir="ltr"><<a href="mailto:fbalestrieri@orange.fr">fbalestrieri@orange.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
Hello,<br>
<br>
I noticed a weird behaviour of the typechecker. If you<br>
confirm that it is not right then I will take the time to<br>
fill a bug report.<br>
<br>
Here is the problem: when an expression is on the right hand<br>
side of a function declaration, Agda doesn't have any trouble<br>
filling the implicit variables ; but if I move that<br>
expression on the left hand side, using the 'with' construct,<br>
then Agda fails. The example is quite complex so I didn't<br>
want to spend ages simplifying it in case the behaviour<br>
turned out to be known.<br></blockquote><div><br>The difference might be that when you put an expression in a with the<br>type checker has no idea what the type of the expression should be,<br>whereas when it appears in a right hand side the expected type is known.<br>
<br>In some cases you'd expected it to work though. For instance,<br><br>nil : {A : Set} -> List A<br><br>foo : List Nat<br>foo with nil<br>... | xs = xs<br><br>In this case the type checker ought to be able to figure out that the<br>
implicit argument to nil must be Nat.<br><br>I've opened a new issue for this (<a href="http://code.google.com/p/agda/issues/detail?id=261">http://code.google.com/p/agda/issues/detail?id=261</a>).<br><br>/ Ulf<br></div>
</div>