[refl] tag depends on order of instance arguments

The [refl] tag applies to refl theorems or definitions only if the instance arguments of the associated structure are ordered in a specific way, apparently, see also this Zulip thread. MWE testing some combinations:

import Mathlib.Algebra.Group.Opposite
import Mathlib.Algebra.Hom.Ring

structure RingEquiv0 (R S : Type _) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

structure RingEquiv1 (R S : Type _) [Mul S] [Mul R] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

structure RingEquiv2 (R S : Type _) [Mul R] [Mul S] [Add S] [Add R] extends R ≃ S, R ≃* S, R ≃+ S

structure RingEquiv3 (R S : Type _) [Mul R] [Add R] [Mul S] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

structure RingEquiv4 (R S : Type _) [Mul R] [Add S] [Mul S] [Add R] extends R ≃ S, R ≃* S, R ≃+ S

@[refl] -- works
def RingEquiv0.refl [Mul α] [Add α] : RingEquiv0 α α := sorry

@[refl] -- works
def RingEquiv1.refl [Mul α] [Add α] : RingEquiv1 α α := sorry

@[refl] -- works
def RingEquiv2.refl [Mul α] [Add α] : RingEquiv2 α α := sorry

@[refl] /- @[refl] attribute only applies to lemmas proving x ∼ x, got {α : Type u_1} →
  [inst : Mul α] → [inst_1 : Add α] → RingEquiv3 α α -/
def RingEquiv3.refl [Mul α] [Add α] : RingEquiv3 α α := sorry

@[refl] /- @[refl] attribute only applies to lemmas proving x ∼ x, got {α : Type u_1} →
  [inst : Mul α] → [inst_1 : Add α] → RingEquiv4 α α -/
def RingEquiv4.refl [Mul α] [Add α] : RingEquiv4 α α := sorry

Reproduce the supplied MWE using the imported Mathlib.Algebra.Group.Opposite and Mathlib.Algebra.Hom.Ring modules, comparing the five RingEquiv definitions and their [refl] declarations. Trace the [refl] attribute's validation entry point and determine why instance-argument order rejects RingEquiv3 and RingEquiv4. Done means the MWE's order variations are accepted consistently, with regression coverage for the failing cases.