Force links when input of a subsequent premise

[FissoreD]

TC.Pending_mode "+".
Class A (i: nat -> nat -> nat).

Global Hint Mode A + : typeclass_instances.

Axiom (f : nat -> nat -> nat).
Instance instA: A f := {}.

Class B (i: nat).
Instance instB : forall R, A R -> forall x y, B (R x y) := {}.

Goal B (f 2 3).
  apply _.
Qed.

The problem:

1. R x y is a potential beta producing the link $X =_\beta R\ x\ y$
2. This link is not triggered, when $X$ is assigned to f 2 3 since we still hope someone "correctily" instantiate $R$
3. $R$ is still flexible and the recursive call $A\ R` is made
4. The first arg of $A$ should be not flexible
5. Here the failure...

[FissoreD]

here the test