From 70aa6bc81d0ca07f009b7af850b119f19e30a4eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Feb 2026 19:46:06 -0800 Subject: [PATCH] fix: detect stuck mvars through auxiliary parent projections (#12564) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Kim Morrison --- src/Lean/Elab/Structure.lean | 1 + src/Lean/Meta/WHNF.lean | 49 ++++++++++++++++++------------- src/Lean/ProjFns.lean | 28 ++++++++++++++++++ stage0/src/stdlib_flags.h | 1 + tests/lean/run/3807.lean | 1 + tests/lean/run/auxParentProj.lean | 21 +++++++++++++ 6 files changed, 81 insertions(+), 20 deletions(-) create mode 100644 tests/lean/run/auxParentProj.lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 175b7edd26..f5bd25a1f4 100644 --- a/src/Lean/Elab/Structure.lean +++ b/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 } /-- diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 76b8c8c0cf..d05e0e694a 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/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 diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index 4e5b0ca647..99e7106e95 100644 --- a/src/Lean/ProjFns.lean +++ b/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 diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ad491b0de1 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean { diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index 3670e4cfac..7d02202058 100644 --- a/tests/lean/run/3807.lean +++ b/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 diff --git a/tests/lean/run/auxParentProj.lean b/tests/lean/run/auxParentProj.lean new file mode 100644 index 0000000000..a7a78a23d0 --- /dev/null +++ b/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']