[Agda] when with-abstraction fails?

[Georgi Lyubenov]

Hi!

I can't give you a concrete reason or way to fix it, but when this 
happens for me, usually the "inspect idiom" fixes it. This is in the 
standard library, but as of recent, it's also been built into the 
language in some shape or form.

See the section on the changelog on "inspect idiom" - 
https://github.com/agda/agda/blob/master/doc/release-notes/2.6.2.md
and the documentation here - 
https://agda.readthedocs.io/en/v2.6.2.1/language/with-abstraction.html#with-abstraction-equality

Cheers,
Georgi

On 4/5/22 06:42, Jason Hu wrote:
>
> Hi all,
>
> I realize that in some situations, with-abstraction does nothing. E.g.
>
> a-function x y z
>
>   with a-term-that-is-in-the-goal
>
> ...  | x = ?
>
> The with-abstraction does not report any error, but rather it does 
> nothing. I know that in some situation with-abstraction is impossible 
> but in those cases, Agda would throw an error. However, in other 
> cases, a tiny bit of change in the code would just turn 
> with-abstraction into a noop and I don’t know why.
>
> I do encounter situations like this in my real project but I do not 
> know how to concentrate a minimal reproducible example. However, I do 
> realize the following methods might or might not solve this problem:
>
>  1. Add more arguments to the function to a point where everything
>     involved in a-term-that-is-in-the-goal  appears in the argument list.
>  2. If the previous method still doesn’t work (as it happens at this
>     moment), then it seems to have something to do with deeply nested
>     where clauses, e.g. if the example function above is in a where
>     clause, then moving it outside of the where clause will almost
>     certainly make the with-abstraction work again.
>
> As a consequence of this problem, rewrite will also cease to work. 
> Should I consider this a bug (which I really intend to) or is there 
> some behavior that I don’t understand in Agda?
>
> Thanks,
>
> Jason Hu
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220405/9c60689d/attachment.html>