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

[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

On Fri, Jan 5, 2018 at 7:44 PM, Manny Romero <mannyromero at mail.com> wrote:

> 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?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180105/0bf92296/attachment.html>