[Agda] Weird behaviour inside of ‘let’

[Andreas Abel]

On 19.01.2014 11:27, Mateusz Kowalczyk wrote:
> Ah great, it'll be a welcome enhancement. Can you explain what's
> happening when Agda sees
>
> f x y z = y
>
> Is it trying to do record unpacking or something along these lines? The
> ‘not in scope’ message is rather uninformative and I'm rather interested
> what it's trying to do. Perhaps it's trying to unpack on some (possible)
> mixfix, but that's just a guess.

Agda expects here

   p = rhs

where p is an irrefutable pattern whose parts are bound to the relevant 
projections of the rhs.

Checking the rhs first give the unlucky scope error for y.  I changed it 
such that it first tries to parse the lhs as pattern now.

   https://code.google.com/p/agda/issues/detail?id=1028

Cheers,
Andreas