[Agda] when with-abstraction fails?

[Andreas Abel]

Agda cannot a priori know whether to expect to abstract the 
with-expression in the goal or not, so it considers both as fine. 
Wherever it finds it, it will abstract it, but if it does not find it, 
maybe the user wanted just a non-dependent case.

If we separated these use cases (non-dependent case vs. dependent with) 
into two separate keywords, we could give an error if `with` found 
nothing to abstract.

If this is wanted, welcome to submit a proposal to the Agda issue 
tracker for discussion.

On 2022-04-05 05:42, Jason Hu wrote:
> 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.
>