Re: [Agda] Weird behaviour inside of ‘let’

[Ulf Norell]

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.

/ Ulf


On Sun, Jan 19, 2014 at 11:27 AM, Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk
> wrote:

> On 19/01/14 09:58, Ulf Norell wrote:
> > Actually, looking at the code we never supported the let f x = ... form
> > without a type signature for f (which can be f : _). The things you can
> say
> > in a let without giving a type signature are
> >   - simple aliases: let x = e in ...
> >   - record unpacking: let x , y = p in ...
> > I'm changing the ticket to a feature request. It should be possible to
> also
> > support let f x y = e in ...
> >
> > / Ulf
> >
> >
> > On Sun, Jan 19, 2014 at 10:46 AM, Ulf Norell <ulf.norell at gmail.com>
> wrote:
> >
> >> That's a straight up bug. I made a ticket:
> >> https://code.google.com/p/agda/issues/detail?id=1028
> >>
> >> Thanks for spotting it.
> >>
> >> / Ulf
> >>
> >>
> >> On Sun, Jan 19, 2014 at 9:46 AM, Mateusz Kowalczyk <
> >> fuuzetsu at fuuzetsu.co.uk> wrote:
> >>
> >>> Hi,
> >>>
> >>> I was turning some expressions of the form ‘foo = λ a b c → f c b a’
> >>> that I had inside a let into the ‘foo a b c = …’ form but I
> >>> encountered a rather weird behaviour, ranging from things being
> >>> claimed not in scope to parse errors. See [1] for some snippets. Can
> >>> someone explain these?
> >>>
> >>> [1]: http://lpaste.net/98754
> >>>
> >>> --
> >>> Mateusz K.
> >>> _______________________________________________
> >>> Agda mailing list
> >>> Agda at lists.chalmers.se
> >>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>
> >>
> >>
> >
>
> 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.
>
> --
> Mateusz K.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140119/1007e831/attachment.html