:ac causes infinite loop

[michaelmesser]

Credit to Jean-Esther van Gobseck for discovering this issue
This causes the LSP to go into an infinite loop when producing code actions.

Steps to Reproduce

After loading this file:

extNat : {0 f, g : Nat -> b} -> ((x : Nat) -> f x = g x) -> f = g

in the REPL run:

Main> :ac 1 extNat

Expected Behavior

Return result or fail in less than 5 seconds

Observed Behavior

Never returns result

[gallais]

This is my understanding: the first explicit argument is a function so idris2 picks f
as a name and then chaos ensues because it's getting confused over the implicit vs.
explicit f. Strangely enough you don't even need f to show up in the return type for
idris to go into an infinite loop:

extNat : {0 f, g : Nat} -> Not (f = g) -> ()

If you use :ac on extNat : {0 f, g : Nat} -> Not (f = g) instead, idris picks prf
as the name for the argument of type f = g and everything is fine. If you go for
extNat : {0 prf, g : Nat} -> Not (prf = g) instead then you also get an infinite loop
presumably because of a similar prf/prf clash.