9.2 regresssion with higher-order unification

[silene]

Description of the problem

In the minimized example below, there are several ways of instantiating f in Q. Among them, there are f (i.e., fun x' => f x') and fun _ => f x. Up to 9.1, Rocq was choosing the non-degenerate instance f. (This behavior dates back from 8.4 at least, and presumably since the beginning.) But starting with 9.2, it chooses the degenerate instance fun _ => f x.

Obviously, both ways of instantiating f are legit, so this does not qualify as a bug. (Though one may argue that choosing the degenerate instance is more often than not the useless choice.) But this breaks a bunch of proofs. Moreover, it is quite difficult to debug in a real proof, since you might not be able to see that Rocq chose the degenerate instance.

Note that replacing refine by eapply makes Rocq revert to the old behavior. Doing revert fx before refine also makes Rocq revert to the old behavior.

Small Rocq / Coq file to reproduce the bug

Axiom P : option nat -> Prop.
Definition b (f : nat -> option nat) x := match x with Some x => f x | None => None end.
Axiom R : (nat -> option nat) -> Prop.
Axiom Q : forall f x, R f -> P (b f x).

Goal forall f x, R f -> P (f x).
intros f x Rf.
set (fx := f x).
refine (Q _ (Some x) _).
exact Rf.
(* The term "Rf" has type "R f" while it is expected to have type "R (fun _ : nat => fx)". *)

Version of Rocq / Coq where this bug occurs

9.2

Last version of Rocq / Coq where the bug did not occur

every version up to 9.1

[SkySkimmer]

Caused by 77f55d5 (#19987)