[Agda] What does does it mean if "-invert730" shows up in a goal?

[Joey Eremondi]

Basically what the title says. I've got a goal I'm trying to fill, but the
type of the goal is "ModuleName.-invert730 arg1 arg2 ... | someExpr arg1 |
someEqProof arg2 ".

If I try to pattern match on "someExpr arg1" I get the dreaded "someExpr
arg1 != w" error.
And if I try to do a rewrite on "someEqProof arg2" I get "lhs != someExpr
arg1".

I'm wondering:
* Does the -invert autogenerated variable give any hints as to why this is
happening? Or is this just normal problems with "with" and "rewrite", and
the "-invert" is just an intermediate name that's exposed because
evaluation got stuck?
* Is there any general way to debug/understand what causes the "w !=" or
"lhs !=" errors? I'm getting them repeatedly when I work with Agda, and I'd
love to actually know what's going on.

I realize it's hard to know what's going on without a minimal example, but
the code I've got right now is too big to ask anyone to look at.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200604/c21a4be5/attachment.html>