I've been naughty and used pattern_of_constr
on terms with unbound Rel
s. 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 PMeta
s? 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: Oct 13 2024 at 01:02 UTC