Bad state after C-c C-s (solve)

[andreasabel]

Using latest version (0.5.1) of the agda-mode, Agda 2.7.0.1, vscode 1.96.0, and this file:

data Nat : Set where
  zero : Nat
  suc : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}

data Fin : Nat → Set where
  zero : {n : Nat} → Fin (suc n)
  suc  : {n : Nat} (i : Fin n) → Fin (suc n)

three : Fin 5
three = suc {n = {!   !} } (suc (suc zero))

Now press C-c C-s which will put 4 in the hole, but interaction into a bad state.
It does not seem to respond to any command any more.

• Locating the hole, pressing C-c C-. there does not update the goal buffer.
• C-c C-l updates the goal buffer with "Loading..." which never disappears.

Only closing the goal buffer gets me out of the bad state: I can then load again with C-c C-l.