Stream: Coq users

Topic: Debugging Canonical Structures

view this post on Zulip Patrick Nicodemus (Apr 05 2023 at 16:00):

I do not understand how to debug canonical structures when it doesn't work as I expect.
Others have mentioned similar difficulties.
Is there any systematic method or effective heuristic I can use to identify precisely what is going wrong when my unification fails?

view this post on Zulip Patrick Nicodemus (Apr 05 2023 at 16:02):

For example, the interaction of canonical structures with typeclasses can be error-prone. How can I detect what has gone wrong when I am trying to use both of them together?

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 20:15):

oh, the CS + typeclasses combination is black magic. Iris sometimes replaces instances by Hint Externs that use apply:, since that uses a unification algorithm that deals with TCs better.

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 20:16):

But Iris's CS setup isn't standard, so I'm not sure that's enough.

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 20:17):

The more robust solution, AFAIK, is to avoid the combination.

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 20:18):

There are plans to fix typeclass search to use evarconv (the better unification algorithm), but this plan appears to have struggled for years

view this post on Zulip Patrick Nicodemus (Apr 05 2023 at 20:39):

Do you think it's realistic to write custom resolution/unification tactics for this kind of thing in Elpi?

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 23:48):

IIUC Enrico plans to rewrite TC search in coq-elpi with a PhD student?

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 23:49):

but the hint I mentioned aren't terrible to write for specific cases (and this should be easy to automate with elpi)

Global Hint Extern 0 (FromAssumption _ _ _) =>
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 23:50):

That's an example from Iris — that uses notypeclasses refine not apply:, but comments confirm this is to use the better unification (evarconv)

view this post on Zulip Enrico Tassi (Apr 07 2023 at 12:50):

Patrick Nicodemus said:

Do you think it's realistic to write custom resolution/unification tactics for this kind of thing in Elpi?

I believe so. What I'm working on is replacing TC search, which is related but not the same thing. In some sense it is complementary or a maybe a prerequisite of what you want.

Last updated: Apr 16 2024 at 20:02 UTC