rewrite does not find seeming exact match with primitive projections

[andres-erbsen]

Description of the problem

I got curious what the situation with primitive projections is like these days, so I tried out what it would be like to use this feature for pairs. In Ascii.v I hit what looks like a real footgun. A match-goal-with calling rewrite with the matched term then has the rewrite fail to find that term in the goal, and manually performing the same invocation of rewrite fails similarly. Almost 2/3 of stdlib (by cloc) still builds, though.

Small Coq file to illustrate the bug

match goal with
| [ |- context[(fst ?x, snd ?x)] ] =>
   rewrite <-(surjective_pairing x)
end. (* fails *)

Cherry-pick the linked commit for actual repro.

Version of Coq where this bug occurs

632031c

Last version of Coq where the bug did not occur

No response

[SkySkimmer]

Classic unfolded vs folded primitive projection issue

Set Primitive Projections.

Record prod A B := pair { fst  :A ; snd : B }.
Arguments pair {_ _}.
Arguments fst {_ _}.
Arguments snd {_ _}.

Lemma surjective_pairing {A B} (p:prod A B) : p = pair (fst p) (snd p).
Proof. reflexivity. Qed.

Lemma surjective_pairing' {A B} (p:prod A B) : p = pair (fst p) (snd p).
Proof.
  cbv.
  Set Printing Unfolded Projection As Match.
  (* |- p = {| fst := let '{| fst := fst |} := p in fst; snd := let '{| snd := snd |} := p in snd |} *)
  match goal with
    |- context[pair (fst ?x) (snd ?x)] =>
      rewrite <-(surjective_pairing x)
  end.
  (* Found no subterm matching "{| fst := fst p; snd := snd p |}" in the current goal. *)

[SkySkimmer]

cc @rlepigre @Janno

[andres-erbsen]

Thank you for the triage. Let's create a well-known tag for it, maybe wellknown: unfolded primitive projections break tactics?

Also might be worth documenting Set Printing Unfolded Projection As Match, I had missed it so far and it seems like exactly the right tool to troubleshoot this kind of issues. Do you know what PR added it?

[SkySkimmer]

It was added in #16994

[andres-erbsen]

And I even commented, and there is documentation -- just without "Set" in front of the option name, evading my misguided search. 👍