Brandon Moore (Dec 01 2020 at 04:58): 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?
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.
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.
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.
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.
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.
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).
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: Oct 13 2024 at 01:02 UTC