From 6b7a803bf44ba24cb4feee7d13a580790a4238bd Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 16 May 2025 16:46:23 +0200 Subject: [PATCH] fix: mapError to store message data context (#8375) This PR ensures that using `mapError` to expand an error message uses `addMessageContext` to include the current context, so that expressions are rendered correctly. Also adds a `preprendError` variant with a more convenient argument order for the common cases of prepending-and-indenting. --- .../Elab/PreDefinition/PartialFixpoint/Induction.lean | 4 ++-- src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean | 2 +- .../Elab/PreDefinition/Structural/FindRecArg.lean | 2 +- src/Lean/Elab/PreDefinition/Structural/Main.lean | 3 +-- src/Lean/Elab/PreDefinition/WF/Unfold.lean | 4 ++-- src/Lean/Elab/Tactic/Monotonicity.lean | 4 ++-- src/Lean/Meta/Basic.lean | 11 +++++++++-- src/Lean/Meta/Match/MatcherApp/Transform.lean | 4 ++-- src/Lean/Meta/Tactic/FunInd.lean | 6 +++--- tests/lean/run/issue8213.lean | 5 ++--- 10 files changed, 25 insertions(+), 20 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean index 893e71c8fb..77c2969c99 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean @@ -97,7 +97,7 @@ def deriveInduction (name : Name) : MetaM Unit := let inductName := name ++ `fixpoint_induct realizeConst name inductName do trace[Elab.definition.partialFixpoint] "Called deriveInduction for {inductName}" - mapError (f := (m!"Cannot derive fixpoint induction principle (please report this issue)\n{indentD ·}")) do + prependError m!"Cannot derive fixpoint induction principle (please report this issue)" do let some eqnInfo := eqnInfoExt.find? (← getEnv) name | throwError "{name} is not defined by partial_fixpoint" let infos ← eqnInfo.declNames.mapM getConstInfoDefn @@ -314,7 +314,7 @@ def derivePartialCorrectness (name : Name) : MetaM Unit := do unless (← getEnv).contains fixpointInductThm do deriveInduction name - mapError (f := (m!"Cannot derive partial correctness theorem (please report this issue)\n{indentD ·}")) do + prependError m!"Cannot derive partial correctness theorem (please report this issue)" do let some eqnInfo := eqnInfoExt.find? (← getEnv) name | throwError "{name} is not defined by partial_fixpoint" diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean index 07dff52338..4b60b6321b 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean @@ -174,7 +174,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do mkSorry goal (synthetic := true) else let hmono ← mkFreshExprSyntheticOpaqueMVar goal - mapError (f := (m!"Could not prove '{preDef.declName}' to be monotone in its recursive calls:{indentD ·}")) do + prependError m!"Could not prove '{preDef.declName}' to be monotone in its recursive calls:" do solveMono failK hmono.mvarId! trace[Elab.definition.partialFixpoint] "monotonicity proof for {preDef.declName}: {hmono}" instantiateMVars hmono diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 754016a5d6..aa3af8fbcf 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -121,7 +121,7 @@ def getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array if let .some termMeasure := termMeasure? then -- User explicitly asked to use a certain measure, so throw errors eagerly let recArgInfo ← withRef termMeasure.ref do - mapError (f := (m!"cannot use specified measure for structural recursion:{indentD ·}")) do + prependError m!"cannot use specified measure for structural recursion:" do let args := fixedParamPerm.buildArgs xs ys getRecArgInfo fnName fixedParamPerm args (← termMeasure.structuralArg) return (#[recArgInfo], m!"") diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean index 733864d2d2..ef2eb58933 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Main.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean @@ -175,8 +175,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array ( state.addMatchers.forM liftM preDefsNonRec.forM fun preDefNonRec => do let preDefNonRec ← eraseRecAppSyntax preDefNonRec - -- state.addMatchers.forM liftM - mapError (f := (m!"structural recursion failed, produced type incorrect term{indentD ·}")) do + prependError m!"structural recursion failed, produced type incorrect term" do -- We create the `_unsafe_rec` before we abstract nested proofs. -- Reason: the nested proofs may be referring to the _unsafe_rec. addNonRec preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList) diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean index 5e09ca718d..94471f47e5 100644 --- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean +++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean @@ -75,7 +75,7 @@ private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Un def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do let baseName := preDef.declName let name := Name.str baseName unfoldThmSuffix - mapError (f := (m!"Cannot derive {name}{indentD ·}")) do + prependError m!"Cannot derive {name}" do withOptions (tactic.hygienic.set · false) do lambdaTelescope preDef.value fun xs body => do let us := preDef.levelParams.map mkLevelParam @@ -109,7 +109,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U let baseName := preDef.declName let name := Name.str baseName unfoldThmSuffix let unaryEqName := Name.str unaryPreDefName unfoldThmSuffix - mapError (f := (m!"Cannot derive {name} from {unaryEqName}{indentD ·}")) do + prependError m!"Cannot derive {name} from {unaryEqName}" do withOptions (tactic.hygienic.set · false) do lambdaTelescope preDef.value fun xs body => do let us := preDef.levelParams.map mkLevelParam diff --git a/src/Lean/Elab/Tactic/Monotonicity.lean b/src/Lean/Elab/Tactic/Monotonicity.lean index 6ccc0911e4..d074e1bf68 100644 --- a/src/Lean/Elab/Tactic/Monotonicity.lean +++ b/src/Lean/Elab/Tactic/Monotonicity.lean @@ -57,7 +57,7 @@ private def defaultFailK (f : Expr) (monoThms : Array Name) : MetaM α := throwError "Failed to prove monotonicity of:{indentExpr f}\n{extraMsg}" private def applyConst (goal : MVarId) (name : Name) : MetaM (List MVarId) := do - mapError (f := (m!"Could not apply {.ofConstName name}:{indentD ·}")) do + prependError m!"Could not apply {.ofConstName name}:" do goal.applyConst name (cfg := { synthAssignedInstances := false}) /-- @@ -150,7 +150,7 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul failK f #[] let b' := f.updateLambdaE! f.bindingDomain! b let p ← mkAppOptM ``monotone_letFun #[α, β, γ, inst_α, inst_β, v, b'] - let new_goals ← mapError (f := (m!"Could not apply {p}:{indentD ·}")) do + let new_goals ← prependError m!"Could not apply {p}:" do goal.apply p let [new_goal] := new_goals | throwError "Unexpected number of goals after {.ofConstName ``monotone_letFun}." diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 5a0fd3485e..58a81a814b 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -2048,17 +2048,24 @@ instance : Alternative MetaM where (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ Format.line ++ m₂) : m α := do controlAt MetaM fun runInBase => orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg -/-- Execute `x`, and apply `f` to the produced error message -/ def mapErrorImp (x : MetaM α) (f : MessageData → MessageData) : MetaM α := do try x catch - | Exception.error ref msg => throw <| Exception.error ref <| f msg + | Exception.error ref msg => + let msg' := f msg + let msg' ← addMessageContext msg' + throw <| Exception.error ref msg' | ex => throw ex +/-- Execute `x`, and apply `f` to the produced error message -/ @[inline] def mapError [MonadControlT MetaM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α := controlAt MetaM fun runInBase => mapErrorImp (runInBase x) f +/-- Execute `x`. If it throws an error, indent and prepend `msg` to it. -/ +@[inline] def prependError [MonadControlT MetaM m] [Monad m] (msg : MessageData) (x : m α) : m α := do + mapError x fun e => m!"{msg}{indentD e}" + /-- Sort free variables using an order `x < y` iff `x` was defined before `y`. If a free variable is not in the local context, we use their id. -/ diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 3c0995b5fe..7e7e8d9a07 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -282,7 +282,7 @@ def transform let aux1 := mkApp aux1 motive' let aux1 := mkAppN aux1 discrs' unless (← isTypeCorrect aux1) do - mapError (f := (m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\n{indentD ·}")) do + prependError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\nfailed with" do check aux1 let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1 @@ -294,7 +294,7 @@ def transform let aux2 := mkApp aux2 motive' let aux2 := mkAppN aux2 discrs' unless (← isTypeCorrect aux2) do - mapError (f := (m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\n{indentD ·}")) do + prependError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\nfailed with" do check aux2 let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2 diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index 9de97b7001..286136218d 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -1212,7 +1212,7 @@ def unpackMutualInduction (unfolding : Bool) (eqnInfo : WF.EqnInfo) : MetaM Name return inductName where doRealize inductName := do let unaryInductName ← deriveUnaryInduction (unfolding := unfolding) eqnInfo.declNameNonRec - mapError (f := (m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)\n{indentD ·}")) do + prependError m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)" do let ci ← getConstInfo unaryInductName let us := ci.levelParams let value := .const ci.name (us.map mkLevelParam) @@ -1568,7 +1568,7 @@ are not variables, to avoid having to generalize them. def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do let casesName := getFunCasesName (unfolding := unfolding) name realizeConst name casesName do - mapError (f := (m!"Cannot derive functional cases principle (please report this issue)\n{indentD ·}")) do + prependError m!"Cannot derive functional cases principle (please report this issue)" do let info ← getConstInfo name let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) name | throwError "'{name}' does not have an unfold theorem nor a value" @@ -1655,7 +1655,7 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details. -/ def deriveInduction (unfolding : Bool) (name : Name) : MetaM Unit := do - mapError (f := (m!"Cannot derive functional induction principle (please report this issue)\n{indentD ·}")) do + prependError m!"Cannot derive functional induction principle (please report this issue)" do if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then let unaryInductName ← deriveUnaryInduction unfolding eqnInfo.declNameNonRec if eqnInfo.declNames.size > 1 then diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean index 325509928b..9cd63f764e 100644 --- a/tests/lean/run/issue8213.lean +++ b/tests/lean/run/issue8213.lean @@ -13,10 +13,9 @@ def myTest {α} /-- error: Failed to realize constant myTest.fun_cases: Cannot derive functional cases principle (please report this issue) - ⏎ failed to transform matcher, type error when constructing new pre-splitter motive: - @myTest.match_1 _fvar.27 (fun x => @_fvar.32 x _fvar.34 _fvar.35) _fvar.33 - ⏎ + myTest.match_1 (fun x => motive x h_1 h_2) x + failed with Application type mismatch: In the application motive x✝ h_1 the argument