feat: all direct parents of classes create projections

Before, all class ancestors that were representable as subobject fields had their projections be instances. This (1) didn't include all direct parents and (2) might include indirect parents. Now, all direct parent classes are instances.

Features:
- Only parents that are not ancestors of other parents get instances. This allows "discretionary" indirect parents to be inserted without having an impact on typeclass synthesis for the purpose of computing strict resolution orders when `structure.strictResolutionOrder` is enabled.
- Non-subobject projections are now theorems if the parent is a proposition.
- Parent projections are no longer added as instances for the `structure` command. Only the `class` command`.

Closes #2905

src/Lean/Elab/Structure.lean

@@ -854,6 +854,7 @@ private def setSourceInstImplicit (type : Expr) : Expr :=
 Creates a projection function to a non-subobject parent.
 -/
 private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do
+  let isProp ← Meta.isProp parentType
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
@@ -883,17 +884,23 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       return result
     let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType)))
     let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n)
-    addAndCompile <| Declaration.defnDecl {
-      name        := declName
-      levelParams := levelParams
-      type        := declType
-      value       := declVal
-      hints       := ReducibilityHints.abbrev
-      safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
-    }
-    if binfo.isInstImplicit then
-      addInstance declName AttributeKind.global (eval_prio default)
+    -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque)
+    let cval : ConstantVal := { name := declName, levelParams, type := declType }
+    if isProp then
+      addDecl <|
+        if view.modifiers.isUnsafe then
+          -- Theorems cannot be unsafe.
+          Declaration.opaqueDecl { cval with value := declVal, isUnsafe := true }
+        else
+          Declaration.thmDecl { cval with value := declVal }
     else
+      addAndCompile <| Declaration.defnDecl { cval with
+        value       := declVal
+        hints       := ReducibilityHints.abbrev
+        safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+      }
+    -- Logic from `mk_projections`: non-instance-implicits that aren't props become reducible.
+    if !binfo.isInstImplicit && !(← Meta.isProp parentType) then
       setReducibleAttribute declName
     return { structName := parentStructName, subobject := false, projFn := declName }
 
@@ -965,6 +972,21 @@ private def checkResolutionOrder (structName : Name) : TermElabM Unit := do
         must come after {MessageData.andList conflicts.toList}" :: defects
     logWarning m!"failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}"
 
+/--
+Adds each direct parent projection to a class as an instance, so long as the parent isn't an ancestor of the others.
+-/
+private def addParentInstances (_structName : Name) (parents : Array StructureParentInfo) : MetaM Unit := do
+  let env ← getEnv
+  let instParents := parents.filter fun parent => isClass env parent.structName
+  -- We only want to add instances that aren't implied by the other parents.
+  let resOrders : Array (Array Name) ← instParents.mapM fun parent => getStructureResolutionOrder parent.structName
+  let isImplied : Array Bool := resOrders.mapIdx fun i resOrder =>
+    let parentName := instParents[i]!.structName
+    resOrder[0]! != parentName && resOrders.any (·.contains parentName)
+  for instParent in instParents, implied in isImplied do
+    unless implied do
+      addInstance instParent.projFn AttributeKind.global (eval_prio default)
+
 def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
   let scopeLevelNames ← Term.getLevelNames
   let isUnsafe := view.modifiers.isUnsafe
@@ -1008,9 +1030,6 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
           addProjections r fieldInfos
           registerStructure view.declName fieldInfos
           mkAuxConstructions view.declName
-          let instParents ← fieldInfos.filterM fun info => do
-            let decl ← Term.getFVarLocalDecl! info.fvar
-            pure (info.isSubobject && decl.binderInfo.isInstImplicit)
           withSaveInfoContext do  -- save new env
             Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
             if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then
@@ -1021,8 +1040,6 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
                 Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
           withRef view.declId do
             Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
-          let projInstances := instParents.toList.map fun info => info.declName
-          projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
           let parentInfos ← r.parents.mapM fun parent => do
             if parent.subobject then
               let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
@@ -1031,6 +1048,8 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
               mkCoercionToCopiedParent levelParams params view parent.structName parent.type
           setStructureParents view.declName parentInfos
           checkResolutionOrder view.declName
+          if view.isClass then
+            addParentInstances view.declName parentInfos
 
           let lctx ← getLCtx
           /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations

tests/lean/run/mathlibetaissue.lean

@@ -161,6 +161,6 @@ instance Field.isDomain [Field K] : IsDomain K :=
 end Mathlib.Algebra.Field.Basic
 
 set_option synthInstance.maxHeartbeats 200 in
-/-- info: MonoidWithZero.toZero -/
+/-- info: MulZeroClass.toZero -/
 #guard_msgs in
 #synth Zero Int