semiOutParam synth error

Stream: lean4

[Mac Malone]

If a semiOutParam class feeds into an outParam class, synthesis will fail if a single instance (e.g., the first tested) of the semiOutParam class is not def-eq to the target type. I encountered this while adding a new feature to Lake. I am not sure if this is a bug or a feature of type class synthesis. So, I am posting the issue here first to verify. Here is a #mwe:

def R (α : Type u) := α
def R.mk (a : α) : R α := a

instance : MonadReaderOf Nat R := ⟨R.mk default⟩
instance : MonadReaderOf Int R := ⟨R.mk default⟩

def test : R Int :=
  MonadReaderOf.read -- works

set_option trace.Meta.synthInstance true in
def test' : R Int :=
  read -- errors
/-
result type
  MonadReader Int R
is not definitionally equal to
  MonadReader Nat R
-/

One can workaround the error with priorities (to get it to try the instance you want it to first), but I am not sure if that is appropriate or if there is a proper, more principled solution.