Stream: Coq users

Topic: Can unification recognize typeclass implementations?


view this post on Zulip Brandon Moore (Dec 01 2020 at 04:58):

I have a goal mentioning some concrete definitions that were used to define an instance of a class, and would like to use lemmas referring to corresponding fields of the class. Is there any way to set things up so unification can succeed? The failed unification message looks something like my_foo_impl vs let (_, ... , foo , ...) := ?inst in foo), which reminds me of canonical projections. Can a typeclass field be declared a canonical projection?

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:38):

never seen that in the wild. If I saw that, I’d fix the goal, and possibly stop my_foo_impl from having a name.

view this post on Zulip Brandon Moore (Dec 01 2020 at 19:20):

I'm using the implementation function on purpose, because the class takes some extra parameters that are not used by that field, and not known or needed at the point where I'm using it.

view this post on Zulip Brandon Moore (Dec 01 2020 at 19:25):

Maybe our classes need to be split up, but it's not like an accident or some early reduction that's exposing the specific function used to implement that instance. It's the other way around - because the instance that includes the specific my_foo_impl that I mentioned takes extra parameters that are not mentioned in the field, those parameters have to be supplied to manually fold it to a use of the class method.

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 21:13):

fair enough! In that case, I suspect I’d pass enough type arguments that ?inst can be inferred.

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 21:16):

If you really want to try canonical structures ... I might be pessimistic but I’d expect an exciting amount of bugs due to untested feature interactions.
One way to even try it is probably to turn the class into a canonical structure and use Existing Class to make it a class as well.

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 21:17):

if canonical structures with parameters trigger problems, the params can be bound in the surrounding section (I think I’ve seen this part in Iris).

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 21:18):

for best unification results, probably you want to use ssreflect tactics, since their unification algorithm (evarconv, used e.g. by apply:) works better with canonical structures AFAICT than tactic unification (used e.g. by apply).


Last updated: Jan 27 2023 at 00:03 UTC