feat: only direct parents of classes create projections

src/Lean/Elab/Structure.lean

@@ -548,8 +548,9 @@ where
       let parentType ← whnf type
       let parentStructName ← getStructureName parentType
       if parents.any (fun info => info.structName == parentStructName) then
-        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}'"
-      if let some existingFieldName ← findExistingField? infos parentStructName then
+        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}', skipping"
+        go (i + 1) infos parents
+      else if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
           logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
         let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType }
@@ -854,6 +855,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 +885,24 @@ 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.
+    -- (Instances will get instance reducibility in `Lean.Elab.Command.addParentInstances`.)
+    if !binfo.isInstImplicit && !(← Meta.isProp parentType) then
       setReducibleAttribute declName
     return { structName := parentStructName, subobject := false, projFn := declName }
 
@@ -965,6 +974,19 @@ 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 (parents : Array StructureParentInfo) : MetaM Unit := do
+  let env ← getEnv
+  let instParents := parents.filter fun parent => isClass env parent.structName
+  -- A parent is an ancestor of the others if it appears with index ≥ 1 in one of the resolution orders.
+  let resOrders : Array (Array Name) ← instParents.mapM fun parent => getStructureResolutionOrder parent.structName
+  let instParents := instParents.filter fun parent =>
+    !resOrders.any (fun resOrder => resOrder[1:].any (· == parent.structName))
+  for instParent in instParents 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 parentInfos
 
           let lctx ← getLCtx
           /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations

tests/lean/run/2905.lean

@@ -0,0 +1,45 @@
+import Lean
+/-!
+# Only direct parents of classes are instances
+
+https://github.com/leanprover/lean4/issues/2905
+-/
+
+set_option structure.strictResolutionOrder true
+
+class A
+class B
+class C extends A
+class D extends A, B
+class E extends C, D
+
+/-!
+These were or were not instances before #5902 and still are or are not.
+-/
+/-- info: some 1000 -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E.toC)
+/-- info: some 1000 -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E.toD)
+/-- info: none -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E.toA)
+
+/-!
+This was an instance before #5902 and no longer is.
+-/
+/-- info: none -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E.toB)
+
+
+/-!
+Check that `A` is not an instance, since it is implied by the others.
+-/
+class E' extends C, D, A
+
+/-- info: none -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E'.toA_1)
+/-- info: none -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E'.toB)
+/-- info: some 1000 -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E'.toC)
+/-- info: some 1000 -/
+#guard_msgs in #eval return (←Lean.Meta.getInstancePriority? `E'.toD)

tests/lean/run/3313.lean

@@ -32,18 +32,9 @@ set_option maxSynthPendingDepth 2 in
 #guard_msgs in
 #synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works
 
-/--
-info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `set_option maxSynthPendingDepth <limit>`
-  [type_class] AddCommGroup Ruse `set_option diagnostics.threshold <num>` to control threshold for reporting counters
----
-error: failed to synthesize
-  HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))
+/-!
+After https://github.com/leanprover/lean4/pull/5920 works without changing maxSynthPendingDepth.
 -/
-#guard_msgs in
-set_option diagnostics true in
-#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails
-
-set_option maxSynthPendingDepth 2 in
 /-- info: Submodule.hasQuotient -/
 #guard_msgs in
-#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- still works
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))

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

tests/lean/struct1.lean

@@ -1,55 +1,56 @@
 --
 
-structure A (α : Type) :=
+structure A (α : Type) where
 (x : α)
 
-structure B (α : Type) :=
+structure B (α : Type) where
 (x : α)
 
-structure S : Nat := -- error expected Type
+structure S : Nat where -- error expected Type
 (x : Nat)
 
-structure S extends Nat → Nat := -- error expected structure
+structure S extends Nat → Nat where -- error expected structure
 (x : Nat)
 set_option structureDiamondWarning true in
-structure S' extends A Nat, A Bool := -- error field `x` already declared
+structure S' extends A Nat, B Nat where -- error field `x` already declared
 (x : Nat)
+structure SDup extends A Nat, A Nat where -- duplicate parent structure 'A'
 
-structure S extends A Nat, B Bool := -- error field `x` from `B` has already been declared
+structure S extends A Nat, B Bool where -- error field `x` from `B` has already been declared
 (x : Nat)
 
-structure S1 :=
+structure S1 where
 (_x : Nat)
 
-structure S2 :=
+structure S2 where
 (x _y : Nat)
 
-structure S :=
+structure S where
 (x : Nat)
 (x : Nat) -- error
 
-structure S extends A Nat :=
+structure S extends A Nat where
 (x : Nat) -- error
 
-structure S' extends A Nat :=
+structure S' extends A Nat where
 (x := true) -- error type mismatch
 
-structure S extends A Nat :=
+structure S extends A Nat where
 (x : Bool := true) -- error omit type
 
-structure S'' :=
+structure S'' where
 (x : Nat := true) -- error type mismatch
 
-private structure S :=
+private structure S where
 private mk :: (x : Nat)
 
-private structure S :=
+private structure S where
 protected mk :: (x : Nat)
 
-private structure S :=
+private structure S where
 protected (x : Nat)
 
-private structure S :=
+private structure S where
 mk2 :: (x : Nat)
 
 #check S

tests/lean/struct1.lean.expected.out

@@ -1,32 +1,29 @@
 struct1.lean:9:14-9:17: error: invalid structure type, expecting 'Type _' or 'Prop'
 struct1.lean:12:20-12:29: error: expected structure
-struct1.lean:15:28-15:34: warning: duplicate parent structure 'A'
-struct1.lean:15:28-15:34: warning: field 'x' from 'A' has already been declared
-struct1.lean:15:28-15:34: error: parent field type mismatch, field 'x' from parent 'A' has type
+struct1.lean:15:28-15:33: warning: field 'x' from 'B' has already been declared
+struct1.lean:16:1-16:2: error: field 'x' has been declared in parent structure
+struct1.lean:17:30-17:35: warning: duplicate parent structure 'A', skipping
+struct1.lean:19:27-19:33: error: parent field type mismatch, field 'x' from parent 'B' has type
   Bool : Type
 but is expected to have type
   Nat : Type
-struct1.lean:18:27-18:33: error: parent field type mismatch, field 'x' from parent 'B' has type
-  Bool : Type
-but is expected to have type
-  Nat : Type
-struct1.lean:29:1-29:2: error: field 'x' has already been declared
-struct1.lean:32:1-32:2: error: field 'x' has been declared in parent structure
-struct1.lean:35:6-35:10: error: type mismatch
+struct1.lean:30:1-30:2: error: field 'x' has already been declared
+struct1.lean:33:1-33:2: error: field 'x' has been declared in parent structure
+struct1.lean:36:6-36:10: error: type mismatch
   true
 has type
   Bool : Type
 but is expected to have type
   Nat : Type
-struct1.lean:38:5-38:9: error: omit field 'x' type to set default value
-struct1.lean:41:12-41:16: error: type mismatch
+struct1.lean:39:5-39:9: error: omit field 'x' type to set default value
+struct1.lean:42:12-42:16: error: type mismatch
   true
 has type
   Bool : Type
 but is expected to have type
   Nat : Type
-struct1.lean:44:0-44:13: error: invalid 'private' constructor in a 'private' structure
-struct1.lean:47:0-47:15: error: invalid 'protected' constructor in a 'private' structure
-struct1.lean:50:0-50:19: error: invalid 'protected' field in a 'private' structure
+struct1.lean:45:0-45:13: error: invalid 'private' constructor in a 'private' structure
+struct1.lean:48:0-48:15: error: invalid 'protected' constructor in a 'private' structure
+struct1.lean:51:0-51:19: error: invalid 'protected' field in a 'private' structure
 S : Type
 S.mk2 (x : Nat) : S