fix: autoParam is structure fields lost in multiple inheritance

closes #1158

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* [Fix `autoParam` in structure fields lost in multiple inheritance.](https://github.com/leanprover/lean4/issues/1158).
+
 * Add `[eliminator]` attribute. It allows users to specify default recursor/eliminators for the `induction` and `cases` tactics.
   It is an alternative for the `using` notation. Example:
   ```lean

src/Lean/Elab/Structure.lean

@@ -305,6 +305,9 @@ private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fi
     let projType ← Meta.transform projType (post := visit)
     if projType.containsFVar parent.fvarId! then
       throwError "unsupported dependent field in {fieldName} : {projType}"
+    if let some info := getFieldInfo? (← getEnv) (← getStructureName parentType) fieldName then
+      if let some autoParamExpr := info.autoParam? then
+        return (← mkAppM ``autoParam #[projType, autoParamExpr])
     return projType
 
 private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do
@@ -704,6 +707,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           fieldName  := info.name
           projFn     := info.declName
           binderInfo := (← getFVarLocalDecl info.fvar).binderInfo
+          autoParam? := (← inferType info.fvar).getAutoParamTactic?
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match (← getEnv).find? info.declName with

tests/lean/run/1158.lean

@@ -0,0 +1,68 @@
+class magma (α) where op : α → α → α
+
+infix:70 " ⋆ " => magma.op (self := inferInstance)
+
+class leftIdMagma (α) extends magma α where
+  identity : α
+  id_op (a : α) : identity ⋆ a = a := by intros; rfl
+
+class rightIdMagma (α) extends magma α where
+  identity : α
+  op_id (a : α) : a ⋆ identity = a := by intros; rfl
+
+class semigroup (α) extends magma α where
+  assoc (a b c : α) : (a ⋆ b) ⋆ c = a ⋆ (b ⋆ c) := by intros; rfl
+
+class idMagma (α) extends leftIdMagma α, rightIdMagma α
+
+class monoid (α) extends idMagma α, semigroup α
+
+def magmaMonoid : leftIdMagma (base → base) := {
+  op := Function.comp
+  identity := id
+}
+
+def fnCompMonoid : monoid (base → base) := {
+  op := Function.comp, identity := id
+}
+
+namespace Ex2
+
+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 }
+
+def e : E Unit := have := c; have := i; have := ()
+                  { op }
+
+structure F (α) extends D α, E α
+structure G (α) extends E α, D α
+
+def f : F Unit := have := s; have := i; have := c; have := ()
+                  { op }
+-- `idempotent`, `fav` missing
+def g : G Unit := have := s; have := i; have := c; have := ()
+                  { op }
+
+end Ex2