'eauto using' fails on (some) primitive projections

[RalfJung]

Description of the problem

I tried the following code:

From Coq.ssr Require Export ssreflect.
From Coq Require Export Utf8 Lia.

Declare Scope stdpp_scope.
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.

Global Hint Extern 1000 => lia : lia.

Class ValidN (A : Type) := validN : nat → A → Prop.
Global Hint Mode ValidN ! : typeclass_instances.
Notation "✓{ n } x" := (validN n x)
  (at level 20, n at next level, format "✓{ n }  x").

Class Valid (A : Type) := valid : A → Prop.
Global Hint Mode Valid ! : typeclass_instances.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.

(** Bundled version *)
Structure cmra := Cmra' {
  cmra_car :> Type;
  cmra_valid : Valid cmra_car;
  cmra_validN : ValidN cmra_car;
}.

Add Printing Constructor cmra.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.

(** * Discrete CMRAs *)
#[projections(primitive=yes)]
Class CmraDiscrete (A : cmra) := {
  cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
}.
Global Hint Mode CmraDiscrete ! : typeclass_instances.

Section cmra.
Context {A : cmra}.
Implicit Types x y z : A.
Implicit Types xs ys zs : list A.

Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
Proof. Admitted.
Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
Proof. Admitted.

Lemma cmra_discrete_valid_iff `{!CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.

Note that CmraDiscrete is a record with primitive projections. This proof script fails in the last eauto saying

Error: Not clever enough to deal with evars dependent in other evars.

If I make CmraDiscrete a regular record, the proof script works. Alternatively, eauto using @cmra_discrete_valid, cmra_validN_le with lia also works. But using the primitive projection without @ seems to confuse eauto. Doing eapply cmra_discrete_valid works just fine.

Coq Version

8.17.0