congruence fails to specialize

[mrhaandi]

Description of the problem

As per documentation of congruence the following goal is solved using hypothesis specialization.

Axiom p : (nat -> nat) -> nat.
Definition ap {X Y : Type} (f : X -> Y) (x : X) := f x.

Goal (forall f, p f = ap f 0) -> forall f, p f = ap f 0.
Proof. congruence. Qed.

However, unfolding ap results in a very similar goal which fails:

Goal (forall f, p f = f 0) -> forall f, p f = f 0.
Proof. Fail congruence. Admitted.

This is because the former pattern p ?f = ap ?f 0 can be used by congruence whereas the p ?f = ?f 0 cannot.
Specifically, the variable ?f cannot appear as the head of an application in ?f 0.
See zulip discussion.

Coq Version

8.13.2