fix: detect stuck mvars through auxiliary parent projections (#12564)

This PR fixes `getStuckMVar?` to detect stuck metavariables through
auxiliary parent projections created for diamond inheritance. These
coercions (e.g., `AddMonoid'.toAddZero'`) are not registered as regular
projections because they construct the parent value from individual
fields rather than extracting a single field. Previously,
`getStuckMVar?` would give up when encountering them, preventing TC
synthesis from being triggered.

- Add `AuxParentProjectionInfo` environment extension to `ProjFns.lean`
recording `numParams` and `fromClass` for these coercions
- Register the info during structure elaboration in
`mkCoercionToCopiedParent`
- Consult the new extension in `getStuckMVar?` as a fallback when
`getProjectionFnInfo?` returns `none`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

src/Lean/Elab/Structure.lean

@@ -1445,6 +1445,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
   if !binfo.isInstImplicit && !(← Meta.isProp parentType) then
     setReducibleAttribute declName
   addDeclarationRangesFromSyntax declName view.ref parent.ref
+  modifyEnv fun env => addAuxParentProjectionInfo env declName params.size (view.isClass && isClass env parent.structName)
   return { structName := parent.structName, subobject := false, projFn := declName }
 
 /--

src/Lean/Meta/WHNF.lean

@@ -341,27 +341,36 @@ mutual
         | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
         | _  =>
           unless e.hasExprMVar do return none
-          -- Projection function support
-          let some projInfo ← getProjectionFnInfo? fName | return none
-          -- This branch is relevant if `e` is a type class projection that is stuck because the instance has not been synthesized yet.
-          unless projInfo.fromClass do return none
           let args := e.getAppArgs
-          -- First check whether `e`s instance is stuck.
-          if let some major := args[projInfo.numParams]? then
-            if let some mvarId ← getStuckMVar? major then
-              return mvarId
-          /-
-          Then, recurse on the explicit arguments
-          We want to detect the stuck instance in terms such as
-          `HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) n (OfNat.ofNat Nat 2 ?m)`
-          See issue https://github.com/leanprover/lean4/issues/1408 for an example where this is needed.
-          -/
-          let info ← getFunInfo f
-          for pinfo in info.paramInfo, arg in args do
-            if pinfo.isExplicit then
-              if let some mvarId ← getStuckMVar? arg then
-                return some mvarId
-          return none
+          -- Projection function support
+          if let some projInfo ← getProjectionFnInfo? fName then
+            -- This branch is relevant if `e` is a type class projection that is stuck because the instance has not been synthesized yet.
+            unless projInfo.fromClass do return none
+            -- First check whether `e`s instance is stuck.
+            if let some major := args[projInfo.numParams]? then
+              if let some mvarId ← getStuckMVar? major then
+                return mvarId
+            /-
+            Then, recurse on the explicit arguments
+            We want to detect the stuck instance in terms such as
+            `HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) n (OfNat.ofNat Nat 2 ?m)`
+            See issue https://github.com/leanprover/lean4/issues/1408 for an example where this is needed.
+            -/
+            let info ← getFunInfo f
+            for pinfo in info.paramInfo, arg in args do
+              if pinfo.isExplicit then
+                if let some mvarId ← getStuckMVar? arg then
+                  return some mvarId
+            return none
+          -- Auxiliary parent projections created for diamond inheritance (not registered as projections).
+          else if let some auxInfo ← getAuxParentProjectionInfo? fName then
+            unless auxInfo.fromClass do return none
+            if let some major := args[auxInfo.numParams]? then
+              if let some mvarId ← getStuckMVar? major then
+                return mvarId
+            return none
+          else
+            return none
       | .proj _ _ e => getStuckMVar? (← whnf e)
       | _ => return none
     | _ => return none

src/Lean/ProjFns.lean

@@ -64,4 +64,32 @@ def isProjectionFn [MonadEnv m] [Monad m] (declName : Name) : m Bool :=
 def getProjectionFnInfo? [MonadEnv m] [Monad m] (declName : Name) : m (Option ProjectionFunctionInfo) :=
   return (← getEnv).getProjectionFnInfo? declName
 
+/--
+Auxiliary parent projection created when a parent structure cannot be represented as a subobject
+(e.g., due to diamond inheritance). Unlike regular projections, these construct the parent value
+from individual fields rather than extracting a single field.
+Example: `AddMonoid'.toAddZero'` when `AddZero'` cannot be a subobject of `AddMonoid'`.
+-/
+structure AuxParentProjectionInfo where
+  /-- Number of parameters in the child structure. -/
+  numParams : Nat
+  /-- `true` if the child structure is a class. -/
+  fromClass : Bool
+  deriving Inhabited, Repr
+
+builtin_initialize auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo ← mkMapDeclarationExtension
+
+def addAuxParentProjectionInfo (env : Environment) (projName : Name) (numParams : Nat) (fromClass : Bool) : Environment :=
+  auxParentProjInfoExt.insert env projName { numParams, fromClass }
+
+namespace Environment
+
+def getAuxParentProjectionInfo? (env : Environment) (projName : Name) : Option AuxParentProjectionInfo :=
+  auxParentProjInfoExt.find? env projName
+
+end Environment
+
+def getAuxParentProjectionInfo? [MonadEnv m] [Monad m] (declName : Name) : m (Option AuxParentProjectionInfo) :=
+  return (← getEnv).getAuxParentProjectionInfo? declName
+
 end Lean

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/3807.lean

@@ -2472,6 +2472,7 @@ instance (L : IntermediateField F E) : IsScalarTower F L E := sorry
 instance (L : IntermediateField F E) : Algebra F (adjoin L S) :=
   (IntermediateField.adjoin { x // x ∈ L } S).algebra'
 
+set_option synthInstance.maxHeartbeats 40000 in
 private theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E}
     (f : L →ₐ[F] K) :
     ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by

tests/lean/run/auxParentProj.lean

@@ -0,0 +1,21 @@
+/-!
+# Test for auxiliary parent projections (diamond inheritance)
+
+`getStuckMVar?` should detect stuck metavariables through auxiliary parent projections
+created for diamond inheritance. Previously, these coercions were not registered as projections,
+so `getStuckMVar?` would give up and TC synthesis was never triggered.
+-/
+
+class AddZero' (M : Type u_2) extends Zero M, Add M where
+
+class AddMonoid' (M : Type u) extends Add M, AddZero' M where
+
+instance : AddZero' Int where
+instance : AddMonoid' Int where
+
+theorem sub_nonneg' {α : Type u} [AddMonoid' α] [Sub α] [LE α] {a b : α} :
+  0 ≤ a - b ↔ b ≤ a := sorry
+
+-- This used to fail because `getStuckMVar?` could not find the stuck mvar
+-- through `AddMonoid'.toAddZero'` (an auxiliary parent projection from diamond inheritance).
+example (a b : Int) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg']