Stream: Coq devs & plugin devs

Topic: pattern_of_constr on primitive projections

view this post on Zulip Janno (Aug 26 2022 at 09:29):

I've been naughty and used pattern_of_constr on terms with unbound Rels. This worked fine until my code came across terms containing primitive projections. As usual, the code of pattern_of_constr has been made to support primitive projections by falling back to compatibility constants via retyping: In this scenario this strikes me as odd because there is little to no guarantee that the parameters inferred by retyping are of reasonable syntactic shape. Would it not make more sense to simply fill the parameters of the compatibility constant with anonymous PMetas? I wonder if I am missing an advantage to the retyping approach in this particular context.

view this post on Zulip Janno (Aug 26 2022 at 09:46):

To spell it out a bit more explicitly: it seems odd that terms not contained in original term fed to pattern_of_constr will have an impact on the result of pattern matching.

view this post on Zulip Gaëtan Gilbert (Aug 26 2022 at 16:57):

make a PR to change it and we will see if it has any impact

view this post on Zulip Janno (Sep 07 2022 at 14:55):

I was about to start working on the change but I decided to check the git logs since it seemed to be done the way it is right now on purpose. Turns out this was done to fix a bug: I don't yet understand what exactly is going on there but I'll probably play around with that some more before I make the change. My gut says retyping can't be right solution but maybe it was actually necessary. Another interesting fact is that pattern_of_constr currently cannot produce Proj nodes. Fixing this might help with the general chaos of matching the various kinds of projection representations. Or maybe it will introduce even more chaos..

view this post on Zulip Janno (Sep 07 2022 at 15:10):

The relevant commit is

Last updated: Jun 09 2023 at 07:01 UTC