Alternative to forgetful inheritance

Stream: mathlib4

[Raghuram]

I'm trying to understand the design choices in the typeclass hierarchy in Mathlib and their rationale better.
Has the following alternative pattern to forgetful inheritance been considered before? What are its pros and cons compared to forgetful inheritance?

/-! # SMul -/
class SMul (A B : Type*) where
  smul :  A -> B -> B

/-! # AddMonoid -/
class AddMonoid X where
  -- Usual definition, without nsmul, nsmul_zero, nsmul_succ

/-! # Compatibility -/
-- The specification of compatibility conditions moves here.
class Compatible.AddMonoid_SMulNat (X) (_ : SMul Nat X) (_ : AddMonoid X) where
  nsmul_zero x : 0 \bu x = 0
  nsmul_succ n x : (n + 1) \bu x = n \bu x + x

-- The default implementation moves here
def AddMonoid.toSMulNat {X} [AddMonoid X] : SMul Nat X where
  smul n x := -- default implementation of nsmul

instance {X} [inst : AddMonoid X] : Compatible inst.AddMonoid_SMulNat inst where
  -- default proof of compatibility

/-! # Users -/

section Default -- an AddMonoid using the default nsmul

variable {X : Type*}

instance : AddMonoid X where
  -- just the monoid structure

instance : SMul Nat X := AddMonoid.toSMulNat

-- An instance of Compatible is inferred automatically

end Default

section NonDefault -- an AddMonoid not using the default nsmul

variable {Y : Type*} [SMul Nat Y]

instance : AddMonoid Y where
  -- just the monoid structure

-- SMul Nat Y already exists

instance : Compatible inferInstance inferInstance where
  -- prove compatibility

end NonDefault

[Raghuram]

What I can think of: this seems like it shifts the burden of compatibility conditions between different structures from many fields of the same classes to a few fields each of many classes. I'm not sure which is better, but this version does look like it makes it easier to achieve modularity / separation of concerns (e.g., in theory one might not need to import UniformSpace to define MetricSpace, although in that particular case probably even the most basic results about metric spaces use uniform space theory so it wouldn't be useful).