[Agda] Show/Solve constraints (C-c C-= and C-c C-s) stopped working

[Manny Romero]

I'm very new on Emacs. (And everything else, for that matter!) While doing various Agda tutorials (not messing about with Emacs or anything) I'd noticed lately that sometimes the "solve constraints" command (C-c C-s in a hole) wouldn't work when the tutorial said it should. Sometimes I'd find the problem would go away in a future Emacs session, but it has returned and doesn't seem to be going away.

To be sure about it, I started a new Emacs session and opened a new file where I wrote:

---------------

data One : Set where
  <> : One

idOne : One -> One
idOne <> = ?

----------------

and loaded to create the hole at "?". Then I go in the hole, and C-c C-s doesn't work! Neither does C-c C-=. All other commands seem to work. I can use C-c C-f and C-c C-b to navigate into the hole; I can use C-c C-, and C-c C-. to give me information. I used C-c C-c in the first place on "idOne x = {!!}" to case split on x and get the present program. I can even, indeed, use C-c C-r on the present program to fill the hole automatically (as well as C-c C-SPC to fill it manually). And so forth. But I just can't get C-c C-s or C-c C-= to work (or the corresponding dropdown menu options), under this or any circumstance!

What might be going on? How might I troubleshoot?