`Agda: Auto` sometimes removes the next hole

[fredrik-bakke]

Sometimes the hole after the current one will be removed when Agda: Auto is used, leading to syntax errors or ill-typed expressions. I'm not presently sure what the precise conditions are for when this happens.

As always, I'm experiencing this error in literate Agda Markdown files.

[fredrik-bakke]

Sorry, this is an incomplete example, but in the following picture when I ask Agda to autofill hole 4 it also removes hole 5.

[fredrik-bakke]

This is the after-state:

[banacorn]

Sorry, I'm having some trouble reproducing this bug. I searched for "strong preunivalence" and found some related commits and files like this one: https://github.com/fredrik-bakke/agda-unimath/blob/2217476d308c235c379db94559b2e781547225cc/src/foundation/strong-preunivalence.lagda.md. I've also found some code snippets from this Mathstodon post: https://mathstodon.xyz/@FredrikBakke/113980401059186473. But none of them matched the image you have provided exactly.

However, I think maybe this bug will be fixed by the coming v0.6.0 release, which revamped the whole hole management thing!