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

[Nils Anders Danielsson]

On 2020-06-04 20:35, Joey Eremondi wrote:
> * 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?

This name suffix seems to be related to the work of Guillame Allais on
irrefutable matching for with.

> * 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.

The manual contains a section called "Ill-typed with-abstractions":

   https://agda.readthedocs.io/en/latest/language/with-abstraction.html#ill-typed-with-abstractions

-- 
/NAD