Surprising Failure in Type Class Inference

[JoJoDeveloping]

Description of the problem

In the following example, I expected the definition to work, instead of failing with a type class error.

The type classes can be properly inferred "on their own," as can be seen in this example:

Class SomeClass (T : Type) := {}.
Instance : forall T, SomeClass T := {}.
(* Axiom gmap : forall (K V : Type), Type. *) (* Works *)
Axiom gmap : forall K {C : SomeClass K} (V : Type), Type. (* Fails *)
Class MBind (M : Type -> Type) := mbind : forall {A B}, (A -> M B) -> M A -> M B.
Hint Mode MBind ! : typeclass_instances.
Instance option_bind : MBind option. Admitted.
Goal True.
unshelve epose (test := fix go (n : nat) : option (gmap unit unit) :=
          match n return option (gmap unit unit) with
          | 0 => None
          | S n => mbind (A:=_) (B:=_) (fun t => @Some _ t) (go n)
          end).
1: apply _.
easy.
Qed.

Extra context: https://coq.zulipchat.com/#narrow/channel/237977-Coq-users/topic/Surprising.20failure.20to.20infer.20typeclasses

Small Rocq / Coq file to reproduce the bug

Class SomeClass (T : Type) := {}.
Instance : forall T, SomeClass T := {}.
(* Axiom gmap : forall (K V : Type), Type. *) (* Works *)
Axiom gmap : forall K {C : SomeClass K} (V : Type), Type. (* Fails *)
Class MBind (M : Type -> Type) := mbind : forall {A B}, (A -> M B) -> M A -> M B.
Hint Mode MBind ! : typeclass_instances.
Instance option_bind : MBind option. Admitted.
Definition test := fix go (n : nat) : option (gmap unit unit) :=
          match n return option (gmap unit unit) with
          | 0 => None
          | S n => mbind (A:=_) (B:=_) (fun t => @Some _ t) (go n)
          end.

Version of Rocq / Coq where this bug occurs

8.20.0

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

No response