<div dir="ltr">The problem is that it first scope checks the right hand side and then tries to make sense of the pattern as a record pattern. This should really be done in the opposite order to get a nicer error message.<div>
<br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jan 19, 2014 at 11:27 AM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 19/01/14 09:58, Ulf Norell wrote:<br>
> Actually, looking at the code we never supported the let f x = ... form<br>
> without a type signature for f (which can be f : _). The things you can say<br>
> in a let without giving a type signature are<br>
> - simple aliases: let x = e in ...<br>
> - record unpacking: let x , y = p in ...<br>
> I'm changing the ticket to a feature request. It should be possible to also<br>
> support let f x y = e in ...<br>
><br>
> / Ulf<br>
><br>
><br>
> On Sun, Jan 19, 2014 at 10:46 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> wrote:<br>
><br>
>> That's a straight up bug. I made a ticket:<br>
>> <a href="https://code.google.com/p/agda/issues/detail?id=1028" target="_blank">https://code.google.com/p/agda/issues/detail?id=1028</a><br>
>><br>
>> Thanks for spotting it.<br>
>><br>
>> / Ulf<br>
>><br>
>><br>
>> On Sun, Jan 19, 2014 at 9:46 AM, Mateusz Kowalczyk <<br>
>> <a href="mailto:fuuzetsu@fuuzetsu.co.uk">fuuzetsu@fuuzetsu.co.uk</a>> wrote:<br>
>><br>
>>> Hi,<br>
>>><br>
>>> I was turning some expressions of the form ‘foo = λ a b c → f c b a’<br>
>>> that I had inside a let into the ‘foo a b c = …’ form but I<br>
>>> encountered a rather weird behaviour, ranging from things being<br>
>>> claimed not in scope to parse errors. See [1] for some snippets. Can<br>
>>> someone explain these?<br>
>>><br>
>>> [1]: <a href="http://lpaste.net/98754" target="_blank">http://lpaste.net/98754</a><br>
>>><br>
>>> --<br>
>>> Mateusz K.<br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>><br>
>><br>
>><br>
><br>
<br>
</div></div>Ah great, it'll be a welcome enhancement. Can you explain what's<br>
happening when Agda sees<br>
<br>
f x y z = y<br>
<br>
Is it trying to do record unpacking or something along these lines? The<br>
‘not in scope’ message is rather uninformative and I'm rather interested<br>
what it's trying to do. Perhaps it's trying to unpack on some (possible)<br>
mixfix, but that's just a guess.<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Mateusz K.<br>
</font></span></blockquote></div><br></div>