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: https://github.com/coq/coq/blob/7f2e4bfc0ec0e2e6ff24a91e9060933e06c31d46/pretyping/patternops.ml#L193. 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.
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.
make a PR to change it and we will see if it has any impact
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: https://github.com/coq/coq/issues/3661. 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..
The relevant commit is https://github.com/coq/coq/commit/0f17c70288662bf8abd1bae59d32a94054481f26
Last updated: Dec 07 2023 at 09:01 UTC