Irene Yoon (Sep 19 2022 at 20:08): Irene Yoon (Sep 19 2022 at 20:08):Just out of curiosity, I was wondering where in the source code I could find the implementation of typeclass resolution. I was reading through "First-class Typeclasses" https://sozeau.gitlabpages.inria.fr/www/research/publications/First-Class_Type_Classes.pdf and couldn't really get a full picture of how the unification algorithm works. Does anyone know where in the source I can crawl through to take a look? (If there are other sources of documentation that I could try reading, I would also appreciate that a lot. Thanks)
Matthieu Sozeau (Sep 19 2022 at 20:10):Hi Irene, I'm afraid the source is the only reliable source if you're looking at the details of the unification. But the reference manual chapter should also give you some information.
Irene Yoon (Sep 19 2022 at 20:14):Hi Matthieu, I see, where in the source can I find it, if you don't mind? I'm having a hard time paging through all the various directories in the repo
Paolo Giarrusso (Sep 19 2022 at 20:21):If you're looking for unification as used in TC search, a reasonable entry point is class_apply... with the caveat that TC search doesn't loop over hints using class_apply, but first filters hints using dnets accounting for hint opacity
Irene Yoon (Sep 19 2022 at 20:23):I see, as found here? https://github.com/coq/coq/blob/611468b3bb25e8c2ee18bc7e03e3a5b1726df9c0/theories/Classes/Init.v#L26 Thanks as always Paulo, I'll take a look and see what I can make out of it.
Matthieu Sozeau (Sep 20 2022 at 06:25):The search algorithm proper is in class_tactics.ml
Irene Yoon (Sep 20 2022 at 16:47):Thanks Matthieu!
Irene Yoon (Sep 20 2022 at 17:51):Ah, more curious poking here, is the UniCoq project (https://people.mpi-sws.org/~beta/papers/unicoq.pdf) upstreamed to the main dev branch for coq? Or is it only be available as a plugin for now? (Is there a good reason that it's not upstreamed if it's more powerful?)
I'm trying to clean up some resolution issues for higher-order objects so I'm trying to see what the best solution is
Gaëtan Gilbert (Sep 20 2022 at 17:53):I believe it is differently powerful, not more
Paolo Giarrusso (Sep 20 2022 at 20:28):The usual summary is that UniCoq is the third unification algorithm for Coq after tactic unification (used by tactics) and evarconv (used by ssreflect tactics), and the first with a documented semantics. The "unifall" branch planned to replace tactic unification by evarconv, at least in typeclass search, but it breaks too much...
Paolo Giarrusso (Sep 20 2022 at 20:29):When an instance/hint resolve doesn't apply because of tactic unification (say because of canonical structures like in Iris), the usual workaround is to write Hint Externs that use ssreflect's apply:.
Paolo Giarrusso (Sep 20 2022 at 20:30):And I'm remembering that you do use Iris, @Irene Yoon , so maybe this is the problem you run into? My summary is biased to Iris users anyway...
Enrico Tassi (Sep 20 2022 at 20:59):FTR evarconv is also used by the pretyper, which means it is used when typing Definition ... and Lemma ....
Enrico Tassi (Sep 20 2022 at 21:00):"tactic unification" is used only by a few tactics, like apply. As you mention, changing the behavior of a very common tactic like apply is not easy
Paolo Giarrusso (Sep 20 2022 at 21:14):Among other reasons, ltac practice ensures that even "make tactics strictly more powerful" is a breaking change, and in combination with backtracking it becomes a fun one. And I guess evarconv might be slower sometimes?
Irene Yoon (Sep 20 2022 at 21:19):OK. I've been running into issues for a project that does not use Iris, canonical structures, or ssreflect.
I must say I do not understand the expected behavior of tactic unification, but indeed the main issue was apply or rewrite failing, where I had to write some custom tactics for inferring the evars in the context instead of directly using apply or rewrite.
I was wondering if there was an easy way to extend the evar resolution/unification, maybe I should instead look into extending the unification using canonical structures? Does extending unification using canonical structures work nicely with setoid_rewrite?
Enrico Tassi (Sep 21 2022 at 05:14):evarconv is slower, yes. Although it is typical of software which aims at being sound and complete to be slower than software which shortcuts in random ways :-)
Janno (Sep 21 2022 at 07:38):refine can serve as a (non-ssreflect) alternative to apply if you know the number of arguments to your lemma in advance. It uses evarconv and might help with the problem of inferring evars.
Janno (Sep 21 2022 at 07:40):Does extending unification using canonical structures work nicely with setoid_rewrite?
don't have a lot of first-hand experience with the interaction of TC search and CS resolution but I hear it doesn't work all that well. That might be outdated, though. Still, this could mean that setoid_rewrite with CS won't solve your problem.
Paolo Giarrusso (Sep 21 2022 at 08:00):Isn't the problem precisely that TC search uses tactic unification which does not handle CSes well?
Janno (Sep 21 2022 at 09:01):Yes but I never really understood what that means exactly
Janno (Sep 21 2022 at 09:02):Clearly tactic unification does CS resolution otherwise a lot of things would just not work at all. I remember a few MRs in the past few years that were related to this problem but I don't know if any of them went in. Maybe they were all part of unifall?
Gaëtan Gilbert (Sep 21 2022 at 09:11):Paolo Giarrusso said:
Isn't the problem precisely that TC search uses tactic unification which does not handle CSes well?
what problem?
Paolo Giarrusso (Sep 21 2022 at 09:38):Since we're discussing using CS to tweak tactic unification, this seems potentially relevant, as long as both unification strategies are treated as almost-black-boxes:
https://gitlab.mpi-sws.org/iris/iris/-/wikis/coq-bugs
[HIGH] #6294: apply (including TC search) and canonical structures don't mix very well, so we randomly use apply: and cannot grow our algebraic hierarchy any further.
Paolo Giarrusso (Sep 21 2022 at 09:41):And to be sure, I'd prefer discussing the unification algorithms by their specifications, rather than "by superstition" as I'm doing, but I understand their behaviors are unspecified for good reason since they're too complex and quirky, which unicoq fixes...
Paolo Giarrusso (Sep 21 2022 at 09:41):(and I'm sad I've never read the unicoq paper)
Irene Yoon (Sep 21 2022 at 14:33):Oh, thanks for the pointer on the Iris side.
[HIGH] #7916: Cannot set mode for Reflexive because setoid_rewrite makes some strange queries, so we suffer from backtracking and slow rewriting whenever Reflexive ? comes up.
This (now closed) issue also sounds close to the problem I'm coming across. I should also try out my development against 8.16 and see if that helps as well
Irene Yoon (Sep 21 2022 at 14:42):It's especially good to know that there are potential issues with apply+CS as Robbert pointed out in issue #6294. Well, I guess I will go carve out some smaller examples where resolution goes awry in my development, and experiment to see what 8.16 fixes / unicoq can do in my situation. I might come back for more questions, but I think I have enough pointers for now. Thanks for the help everyone!
Janno (Sep 21 2022 at 14:57):A small thing to be aware of regarding unicoq and CS: unicoq has not been patched to implement the recent improvements to CS (see https://coq.inria.fr/refman/changes.html#id383). I don't think many people use these new features yet but I thought I'd mention it just in case you do.
Kazuhiko Sakaguchi (Sep 21 2022 at 17:20):The UniCoq paper says that it purposely lacks a technique known as constraint postponement. At some point, I observed some cases that evarconv works but UniCoq fails, in MathComp.
Paolo Giarrusso (Sep 21 2022 at 17:21):@Irene Yoon if you have Reflexive trouble, remember that 8.16 does not set the mode, it just has code that doesn't break if you do...
Notification Bot (Nov 05 2022 at 16:10):A message was moved from this topic to #Coq devs & plugin devs > Typeclass resolution algorithm? by Karl Palmskog.
Last updated: Oct 01 2023 at 17:01 UTC