<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">&lt;<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>&gt;</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>
&gt; Actually, looking at the code we never supported the let f x = ... form<br>
&gt; without a type signature for f (which can be f : _). The things you can say<br>
&gt; in a let without giving a type signature are<br>
&gt;   - simple aliases: let x = e in ...<br>
&gt;   - record unpacking: let x , y = p in ...<br>
&gt; I&#39;m changing the ticket to a feature request. It should be possible to also<br>
&gt; support let f x y = e in ...<br>
&gt;<br>
&gt; / Ulf<br>
&gt;<br>
&gt;<br>
&gt; On Sun, Jan 19, 2014 at 10:46 AM, Ulf Norell &lt;<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt;&gt; That&#39;s a straight up bug. I made a ticket:<br>
&gt;&gt; <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>
&gt;&gt;<br>
&gt;&gt; Thanks for spotting it.<br>
&gt;&gt;<br>
&gt;&gt; / Ulf<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On Sun, Jan 19, 2014 at 9:46 AM, Mateusz Kowalczyk &lt;<br>
&gt;&gt; <a href="mailto:fuuzetsu@fuuzetsu.co.uk">fuuzetsu@fuuzetsu.co.uk</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt;&gt; Hi,<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; I was turning some expressions of the form ‘foo = λ a b c → f c b a’<br>
&gt;&gt;&gt; that I had inside a let into the ‘foo a b c = …’ form but I<br>
&gt;&gt;&gt; encountered a rather weird behaviour, ranging from things being<br>
&gt;&gt;&gt; claimed not in scope to parse errors. See [1] for some snippets. Can<br>
&gt;&gt;&gt; someone explain these?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; [1]: <a href="http://lpaste.net/98754" target="_blank">http://lpaste.net/98754</a><br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; --<br>
&gt;&gt;&gt; Mateusz K.<br>
&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
<br>
</div></div>Ah great, it&#39;ll be a welcome enhancement. Can you explain what&#39;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&#39;m rather interested<br>
what it&#39;s trying to do. Perhaps it&#39;s trying to unpack on some (possible)<br>
mixfix, but that&#39;s just a guess.<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Mateusz K.<br>
</font></span></blockquote></div><br></div>