[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?

[Jesper Cockx]

Hi Manny,

"Solve constraints" (C-c C-s) only works when Agda can see that there is a
*unique* solution for a given hole. But the meaning of 'unique' here is a
bit subtle: it considers `<>` to be different from, say, `if b then <> else
<>`, even though the latter will evaluate to `<>` for any value of b.
Technically speaking, Agda requires the solution to be unique up to
definitional equality.

If you define One as a record type instead of as a datatype, then Agda will
replace any value of type One (such as `if b then <> else <>`) by `<>`.
This is called the eta rule for One. Agda has eta-rules built-in for record
types but not for datatypes. So the following should work:

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

record One : Set where
constructor <>

idOne : One -> One
idOne <> = ?

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

I assume the tutorials you read used the definition of One as a record type
instead of as a datatype, which is why C-c C-s works in their case. I hope
this helps!

cheers,
Jesper

Post by 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.
---------------
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?
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda