Typeclass resolution can lock coq-lsp responsiveness when looping

[Alizter]

It is a common occurrence to tweak a typeclass definition causing later lemmas to loop when searching. When this happens, it causes coq-lsp to become unresponsive.

[ejgallego]

Can you provide a test case?

[Alizter]

Here is a test case:

From Coq Require Import Prelude.

Axiom Loop : Type.
Existing Class Loop.

Axiom loop : Loop -> Loop.
#[export] Existing Instance loop.

Global Instance foo : Loop.
Proof. Admitted.

Goal Loop.
exact _.

Try commenting out foo and typeclass search will loop. When this happens, LSP becomes unresponsive.

[ejgallego]

Thanks a lot Ali, I have opened a file collecting uninterruptible cases, I hope to resolve them soon.

[ejgallego]

@Alizter note this example doesn't loop anymore, what'd be the suggested fix?

[ejgallego]

I did

Global Instance foo (a : Loop) : Loop.
Proof. Admitted.

for example, and that seems to work, but I don't know how TC work.

[Alizter]

If you give foo a lower priority with | 10 that should work.