autoParam in structure fields lost in inheritance

[raghuram-13]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

autoParams defined for fields of a structure A are sometimes lost in structures B extending them (as far as I can tell, when A is not the first structure B inherits from).

Steps to Reproduce

class magma (α) where op : α → α → α

infix:70 " ⋆ " => magma.op (self := inferInstance)

class leftIdMagma (α) extends magma α where
  identity : α
  id_op (a : α) : identity ⋆ a = a := by intro; rfl

class rightIdMagma (α) extends magma α where
  identity : α
  op_id (a : α) : a ⋆ identity = a := by intro; rfl

class semigroup (α) extends magma α where
  assoc (a b c : α) : (a ⋆ b) ⋆ c = a ⋆ (b ⋆ c) := by intro _ _ _; rfl

class idMagma (α) extends leftIdMagma α, rightIdMagma α

class monoid (α) extends idMagma α, semigroup α

def fnCompMonoid {base : Sort _} : monoid (base → base) :=
{ op := Function.comp, identity := id
-- , op_id := by intro; rfl
-- , assoc := by intros; rfl
}

Expected behavior: fnCompMonoid is successfully defined with the op_id and assoc fields produced using the tactics specified for those fields.

Actual behavior: The op_id and assoc fields need to be specified as in the commented-out lines.

Reproduces how often: Only for fields inherited from a parent structure other than the first parent of a structure (as far as I can tell).

Versions

• 4th milestone release
• d13fac6

Additional Information

The above example worked in a nightly version from October 2021.

[raghuram-13]

Based on this example, it seems that autoParams for fields of B fail to transfer to structures E extending it if one of the fields of B has a type dependent on another field which is common to the first structure E extends. If this happens, then it fails to transfer for all fields of B, even those whose type is not dependent like this.

structure A (α) where
  subsingleton : ∀ a b : α, a = b := by assumption

structure B (α) where
  op : α → α → α
  idempotent : ∀ a : α, op a a = a := by assumption
  fav : α := by assumption

structure C (α) where
  op : α → α → α
  comm : ∀ a b : α, op a b = op b a := by assumption

structure D (α) extends A α, B α
structure E (α) extends C α, B α

-- Let's reuse these
theorem s (a b : Unit) : a = b := rfl
def op (_ _ : Unit) : Unit := ()
def i (a : Unit) : op a a = a := s _ a
def c (a b : Unit) : op a b = op b a := s _ _

-- Successfully defined
def d : D Unit := have := s; have := i; have := ()
                  { op }

-- fields `idempotent` and `fav` are missing
def e : E Unit := have := c; have := i; have := ()
                  { op --, idempotent := i, fav := ()
                    }

structure F (α) extends D α, E α
structure G (α) extends E α, D α

-- `comm` alone missing
def f : F Unit := have := s; have := i; have := c; have := ()
                  { op --, comm := c
                    }
-- `idempotent`, `fav` missing
def g : G Unit := have := s; have := i; have := c; have := ()
                  { op --, idempotent := i, fav := ()
                    }