Ignoring default value for field warning

[gebner]

class Zero (α : Type u) where
  zero : α
class AddZeroClass (M : Type u) extends Zero M, Add M
class AddMonoid (M : Type u) extends AddZeroClass M where
  nsmul : Nat → M → M := fun _ _ => Zero.zero
class AddCommMonoid (M : Type u) extends Zero M, AddMonoid M
class AddMonoidWithOne (R : Type u) extends AddMonoid R
class AddCommMonoidWithOne (R : Type u) extends AddMonoidWithOne R, AddCommMonoid R
class NonAssocSemiring (α : Type u) extends Zero α, AddCommMonoidWithOne α
class Semiring (α : Type u) extends Zero α, NonAssocSemiring α
  -- ignoring default value for field 'nsmul'

The last class declaration unexpectedly produces the above warning, with no apparent way to fix it. Declaring the default value again in Semiring does not help either.

[gebner]

I think I know where it's going wrong:

#print NonAssocSemiring.nsmul._default
/-
@[reducible] def NonAssocSemiring.nsmul._default.{u_1} : {α : Type u_1} →
  Zero α → Add α → (Nat → α → α) → Nat → α → α :=
fun {α} toZero toAdd nsmul => id fun x x => Zero.zero
-/