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?
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?
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.
But Iris's CS setup isn't standard, so I'm not sure that's enough.
The more robust solution, AFAIK, is to avoid the combination.
There are plans to fix typeclass search to use evarconv (the better unification algorithm), but this plan appears to have struggled for years
Do you think it's realistic to write custom resolution/unification tactics for this kind of thing in Elpi?
IIUC Enrico plans to rewrite TC search in coq-elpi with a PhD student?
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.
That's an example from Iris — that uses notypeclasses refine
not apply:
, but comments confirm this is to use the better unification (evarconv)
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: Oct 13 2024 at 01:02 UTC