From 97a460f92bd97c301a653194f2d37a68f3588b76 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 18 Jun 2026 08:25:52 +0000 Subject: [PATCH 1/8] decl check --- src/Lean/AddDecl.lean | 81 +++++++++++++++++++++++++++++++ tests/elab/declCheckImplicit.lean | 51 +++++++++++++++++++ 2 files changed, 132 insertions(+) create mode 100644 tests/elab/declCheckImplicit.lean diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 7e42c1e684bd..f6d47d9b784f 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -12,6 +12,9 @@ public import Lean.OriginalConstKind public import Lean.AutoDecl import Lean.Linter.Init import Lean.Compiler.MetaAttr +import Lean.Meta.Check -- for the `linter.declCheckImplicit` linter +import Lean.Meta.Instances -- for the `linter.declCheckImplicit` linter +import Lean.ReducibilityAttrs -- for the `linter.declCheckImplicit` linter import all Lean.OriginalConstKind -- for accessing `privateConstKindsExt` public section @@ -93,6 +96,83 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do -- This case should not happen, but it ensures a warning will get logged no matter what. logWarning <| .tagged `hasSorry m!"declaration uses `sorry`" +/-- If `linter.declCheckImplicit` is set to true, declarations whose type is type-correct at +`.default` transparency but not at `.implicit` transparency generate a warning suggesting the +definitions that should be marked `@[implicit_reducible]`. -/ +register_builtin_option linter.declCheckImplicit : Bool := { + defValue := false + descr := "warn when a declaration's type is not type-correct at `.implicit` transparency" +} + +/-- The top-level `(name, type)` pairs whose types `warnIfDeclIllTypedAtImplicit` checks: +definitions, theorems, opaque constants, and axioms. Inductives and `Quot` are skipped. -/ +private def declTypesToCheck : Declaration → Array (Name × Expr) + | .axiomDecl v => #[(v.name, v.type)] + | .defnDecl v => #[(v.name, v.type)] + | .thmDecl v => #[(v.name, v.type)] + | .opaqueDecl v => #[(v.name, v.type)] + | .mutualDefnDecl vs => (vs.map fun v => (v.name, v.type)).toArray + | .inductDecl .. => #[] + | .quotDecl => #[] + +/-- Returns the semireducible non-instance definitions that `Meta.check declType .default` +unfolds but the `.implicit` check would not, or `none` if `declType` is already type-correct at +`.implicit` transparency (or is not even type-correct at `.default`). Mirrors the inner loop of +`Lean.Linter.tacticCheckInstances`. -/ +private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array Name)) := do + let origDiag := (← get).diag + let result : Option (Array Name) ← withOptions (diagnostics.set · true) do + -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. + try Meta.check declType .default catch _ => return none + let counterDefault := (← get).diag.unfoldCounter + -- Reset the unfold counter and re-check at `.implicit`. + modify ({ · with diag := origDiag }) + try + Meta.check declType .implicit + return none + catch _ => + let counterImplicit := (← get).diag.unfoldCounter + let env ← getEnv + -- Definitions unfolded by the `.default` check but not the `.implicit` one are the + -- candidates for `@[implicit_reducible]`; keep only semireducible non-instances. + let mut candidates : Array Name := #[] + for (n, countDefault) in counterDefault do + let countImplicit := counterImplicit.find? n |>.getD 0 + if countDefault > countImplicit + && getReducibilityStatusCore env n matches .semireducible + && !Meta.isInstanceCore env n then + candidates := candidates.push n + return some candidates + -- Always restore the original diagnostics snapshot, mirroring `tacticCheckInstances`. + modify ({ · with diag := origDiag }) + return result + +/-- +If `linter.declCheckImplicit` is enabled, warns when a declaration's type is type-correct at +`.default` transparency but not at `.implicit` transparency, listing the semireducible definitions +that would need to be marked `@[implicit_reducible]` to fix the mismatch. + +Unlike `linter.tacticCheckInstances`, which checks tactic goals, this runs on every declaration +added to the environment, so the warning also fires for declarations synthesized by attributes +such as `@[simps]` and `@[reassoc]`. Following the convention of the core tactic linter, it does +*not* participate in `linter.all`. +-/ +def warnIfDeclIllTypedAtImplicit (decl : Declaration) : CoreM Unit := do + unless linter.declCheckImplicit.get (← getOptions) do return + -- Stay quiet on declarations that already produced errors, as `warnIfUsesSorry` does. + if ← MonadLog.hasErrors then return + for (declName, declType) in declTypesToCheck decl do + -- Compiler-internal auto-declarations (equation lemmas, etc.) would be noisy; skip them. + if ← isAutoDeclOrPrivate_Internal declName then continue + let some candidates ← (checkImplicitTransparency declType).run' | continue + if candidates.isEmpty then continue + let bullets := MessageData.joinSep + (candidates.toList.map (m!"{MessageData.ofConstName ·}")) Format.line + Linter.logLint linter.declCheckImplicit (← getRef) + m!"declaration {MessageData.ofConstName declName} is not type-correct at \ + `.implicit` transparency; consider marking some of the following as \ + `@[implicit_reducible]`:{indentD bullets}" + builtin_initialize registerTraceClass `addDecl @@ -182,6 +262,7 @@ where profileitM Exception "type checking" (← getOptions) do withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do warnIfUsesSorry decl + warnIfDeclIllTypedAtImplicit decl try let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException diff --git a/tests/elab/declCheckImplicit.lean b/tests/elab/declCheckImplicit.lean new file mode 100644 index 000000000000..8cd7ca72f130 --- /dev/null +++ b/tests/elab/declCheckImplicit.lean @@ -0,0 +1,51 @@ +import Lean + +/-! +# The `linter.declCheckImplicit` linter + +`linter.declCheckImplicit` warns when a declaration's type is type-correct at `.default` +transparency but not at `.implicit` transparency, suggesting the semireducible definitions that +should be marked `@[implicit_reducible]`. + +Because the check runs in `addDecl`, the warning fires for *every* declaration, including ones +synthesized by attributes such as `@[simps]` and `@[reassoc]` (here modeled with a hand-written +lemma whose type mentions a semireducible definition). +-/ + +structure Fn where + toFun : Nat → Nat + +/-- `MyFn` is semireducible, so it does not unfold at `.implicit` transparency. -/ +def MyFn : Type := Fn + +def idFn : MyFn := (⟨id⟩ : Fn) + +/-! ## Off by default: no warning even though the type is not correct at `.implicit`. -/ + +#guard_msgs in +theorem idFn_toFun_off : (idFn : Fn).toFun = id := rfl + +set_option linter.declCheckImplicit true + +/-! ## Enabled: the ill-typed-at-`.implicit` type is reported, blaming `MyFn`. -/ + +/-- +warning: declaration idFn_toFun is not type-correct at `.implicit` transparency; consider marking some of the following as `@[implicit_reducible]`: + MyFn + +Note: This linter can be disabled with `set_option linter.declCheckImplicit false` +-/ +#guard_msgs in +theorem idFn_toFun : (idFn : Fn).toFun = id := rfl + +/-! ## A type that is fine at `.implicit` is not reported. -/ + +#guard_msgs in +theorem reflexive_eq : (1 : Nat) = 1 := rfl + +/-! ## Marking `MyFn` `@[implicit_reducible]` fixes the mismatch: no more warning. -/ + +attribute [implicit_reducible] MyFn + +#guard_msgs in +theorem idFn_toFun_fixed : (idFn : Fn).toFun = id := rfl From db7abd7920de2de3475fd9344e0a735085f693ac Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 18 Jun 2026 09:14:16 +0000 Subject: [PATCH 2/8] enable by default --- src/Lean/AddDecl.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index f6d47d9b784f..da2340faafc1 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -100,7 +100,7 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do `.default` transparency but not at `.implicit` transparency generate a warning suggesting the definitions that should be marked `@[implicit_reducible]`. -/ register_builtin_option linter.declCheckImplicit : Bool := { - defValue := false + defValue := true descr := "warn when a declaration's type is not type-correct at `.implicit` transparency" } From bdc7d3709a4e3f35588a723942c0a2245503210f Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 19 Jun 2026 08:07:42 +0000 Subject: [PATCH 3/8] implicit check first --- src/Lean/AddDecl.lean | 57 ++++++++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 20 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index da2340faafc1..42ac6b791f4e 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -118,31 +118,48 @@ private def declTypesToCheck : Declaration → Array (Name × Expr) /-- Returns the semireducible non-instance definitions that `Meta.check declType .default` unfolds but the `.implicit` check would not, or `none` if `declType` is already type-correct at `.implicit` transparency (or is not even type-correct at `.default`). Mirrors the inner loop of -`Lean.Linter.tacticCheckInstances`. -/ -private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array Name)) := do +`Lean.Linter.tacticCheckInstances`. + +Runs under `Core.withCurrHeartbeats` and treats heartbeat exhaustion as `none` (skip): this +diagnostic must never abort the surrounding elaboration, nor draw on a tactic's already-spent +heartbeat budget. Interrupt exceptions are re-raised, never swallowed. -/ +private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array Name)) := + Core.withCurrHeartbeats do + -- Fast path: a type that is already type-correct at `.implicit` needs no report. Checking at + -- `.implicit` does not unfold semireducible definitions, so this is cheap even when the + -- `.default` check below would unfold large terms (e.g. a `bv_decide` goal mentioning + -- semireducible definitions). Only when this fails do we run the expensive `.default` check. + let implicitFailed : Bool ← + try + Meta.check declType .implicit + pure false + catch e => + if e.isInterrupt then throw e + else if e.isMaxHeartbeat then return none + else pure true + unless implicitFailed do return none let origDiag := (← get).diag let result : Option (Array Name) ← withOptions (diagnostics.set · true) do -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. - try Meta.check declType .default catch _ => return none + try Meta.check declType .default + catch e => if e.isInterrupt then throw e else return none let counterDefault := (← get).diag.unfoldCounter - -- Reset the unfold counter and re-check at `.implicit`. + -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. modify ({ · with diag := origDiag }) - try - Meta.check declType .implicit - return none - catch _ => - let counterImplicit := (← get).diag.unfoldCounter - let env ← getEnv - -- Definitions unfolded by the `.default` check but not the `.implicit` one are the - -- candidates for `@[implicit_reducible]`; keep only semireducible non-instances. - let mut candidates : Array Name := #[] - for (n, countDefault) in counterDefault do - let countImplicit := counterImplicit.find? n |>.getD 0 - if countDefault > countImplicit - && getReducibilityStatusCore env n matches .semireducible - && !Meta.isInstanceCore env n then - candidates := candidates.push n - return some candidates + try Meta.check declType .implicit + catch e => if e.isInterrupt then throw e + let counterImplicit := (← get).diag.unfoldCounter + let env ← getEnv + -- Definitions unfolded by the `.default` check but not the `.implicit` one are the + -- candidates for `@[implicit_reducible]`; keep only semireducible non-instances. + let mut candidates : Array Name := #[] + for (n, countDefault) in counterDefault do + let countImplicit := counterImplicit.find? n |>.getD 0 + if countDefault > countImplicit + && getReducibilityStatusCore env n matches .semireducible + && !Meta.isInstanceCore env n then + candidates := candidates.push n + return some candidates -- Always restore the original diagnostics snapshot, mirroring `tacticCheckInstances`. modify ({ · with diag := origDiag }) return result From 84635d8b54ff3fbdca16471d4357acb2d032bcd3 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 22 Jun 2026 10:08:30 +0000 Subject: [PATCH 4/8] fix test --- tests/elab/declCheckImplicit.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/elab/declCheckImplicit.lean b/tests/elab/declCheckImplicit.lean index 8cd7ca72f130..168f2d640dae 100644 --- a/tests/elab/declCheckImplicit.lean +++ b/tests/elab/declCheckImplicit.lean @@ -20,14 +20,13 @@ def MyFn : Type := Fn def idFn : MyFn := (⟨id⟩ : Fn) -/-! ## Off by default: no warning even though the type is not correct at `.implicit`. -/ +/-! ## Disabled explicitly: no warning even though the type is not correct at `.implicit`. -/ #guard_msgs in +set_option linter.declCheckImplicit false in theorem idFn_toFun_off : (idFn : Fn).toFun = id := rfl -set_option linter.declCheckImplicit true - -/-! ## Enabled: the ill-typed-at-`.implicit` type is reported, blaming `MyFn`. -/ +/-! ## On by default: the ill-typed-at-`.implicit` type is reported, blaming `MyFn`. -/ /-- warning: declaration idFn_toFun is not type-correct at `.implicit` transparency; consider marking some of the following as `@[implicit_reducible]`: From a659f8b3e6af42ef6c25701f2d578e22434cf25b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 22 Jun 2026 12:28:29 +0000 Subject: [PATCH 5/8] cleanup --- src/Lean/AddDecl.lean | 71 ++++++++++++++++++++++++++++--------------- 1 file changed, 46 insertions(+), 25 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 42ac6b791f4e..76dedd261865 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -96,16 +96,20 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do -- This case should not happen, but it ensures a warning will get logged no matter what. logWarning <| .tagged `hasSorry m!"declaration uses `sorry`" -/-- If `linter.declCheckImplicit` is set to true, declarations whose type is type-correct at -`.default` transparency but not at `.implicit` transparency generate a warning suggesting the -definitions that should be marked `@[implicit_reducible]`. -/ +/-- +If `linter.declCheckImplicit` is set to true, declarations whose type is type-correct at +`.default` transparency but not at `.implicit` transparency generate a warning suggesting +definitions that could be marked `@[implicit_reducible]`. +-/ register_builtin_option linter.declCheckImplicit : Bool := { defValue := true descr := "warn when a declaration's type is not type-correct at `.implicit` transparency" } -/-- The top-level `(name, type)` pairs whose types `warnIfDeclIllTypedAtImplicit` checks: -definitions, theorems, opaque constants, and axioms. Inductives and `Quot` are skipped. -/ +/-- +The top-level `(name, type)` pairs whose types `warnIfDeclIllTypedAtImplicit` checks: +definitions, theorems, opaque constants, and axioms. Inductives are skipped for now. +-/ private def declTypesToCheck : Declaration → Array (Name × Expr) | .axiomDecl v => #[(v.name, v.type)] | .defnDecl v => #[(v.name, v.type)] @@ -115,43 +119,63 @@ private def declTypesToCheck : Declaration → Array (Name × Expr) | .inductDecl .. => #[] | .quotDecl => #[] -/-- Returns the semireducible non-instance definitions that `Meta.check declType .default` -unfolds but the `.implicit` check would not, or `none` if `declType` is already type-correct at +/-- +Returns the semireducible non-instance definitions that `Meta.check declType .default` +unfolds but the `.implicit` check does not, or `none` if `declType` is already type-correct at `.implicit` transparency (or is not even type-correct at `.default`). Mirrors the inner loop of `Lean.Linter.tacticCheckInstances`. -Runs under `Core.withCurrHeartbeats` and treats heartbeat exhaustion as `none` (skip): this +Runs under `Core.withCurrHeartbeats` and returns `none` in case of heartbeat exhaustion.: this diagnostic must never abort the surrounding elaboration, nor draw on a tactic's already-spent -heartbeat budget. Interrupt exceptions are re-raised, never swallowed. -/ +heartbeat budget. Interrupt exceptions are re-raised, never swallowed. +-/ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array Name)) := Core.withCurrHeartbeats do - -- Fast path: a type that is already type-correct at `.implicit` needs no report. Checking at - -- `.implicit` does not unfold semireducible definitions, so this is cheap even when the - -- `.default` check below would unfold large terms (e.g. a `bv_decide` goal mentioning - -- semireducible definitions). Only when this fails do we run the expensive `.default` check. + -- Fast path: Check the type at `.implicit`, without `diagnostics true`. Failure should be the + -- absolute exception, so we optimize for the frequent case. let implicitFailed : Bool ← try Meta.check declType .implicit pure false catch e => if e.isInterrupt then throw e - else if e.isMaxHeartbeat then return none + else if e.isRuntime then + logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" + return none else pure true unless implicitFailed do return none let origDiag := (← get).diag let result : Option (Array Name) ← withOptions (diagnostics.set · true) do -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. try Meta.check declType .default - catch e => if e.isInterrupt then throw e else return none + catch e => + if e.isInterrupt then + modify ({ · with diag := origDiag }) + throw e + else + -- Any error while checking the type at default transparency is an unexpected error. + logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at default transparency.\n{e.toMessageData}" + return none let counterDefault := (← get).diag.unfoldCounter -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. modify ({ · with diag := origDiag }) try Meta.check declType .implicit - catch e => if e.isInterrupt then throw e + catch e => + if e.isInterrupt then + modify ({ · with diag := origDiag }) + throw e + else if e.isRuntime then + -- Warn if a resource limit has been reached. + logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" + return none + else + -- This check is expected to fail, so nothing to do in this case. + -- The `else` branch only exists for clarity. + pure () let counterImplicit := (← get).diag.unfoldCounter let env ← getEnv -- Definitions unfolded by the `.default` check but not the `.implicit` one are the - -- candidates for `@[implicit_reducible]`; keep only semireducible non-instances. + -- candidates for `@[implicit_reducible]`. Only consider semireducible non-instances. let mut candidates : Array Name := #[] for (n, countDefault) in counterDefault do let countImplicit := counterImplicit.find? n |>.getD 0 @@ -160,23 +184,20 @@ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array N && !Meta.isInstanceCore env n then candidates := candidates.push n return some candidates - -- Always restore the original diagnostics snapshot, mirroring `tacticCheckInstances`. + -- Always restore the original diagnostics snapshot. modify ({ · with diag := origDiag }) return result /-- If `linter.declCheckImplicit` is enabled, warns when a declaration's type is type-correct at -`.default` transparency but not at `.implicit` transparency, listing the semireducible definitions -that would need to be marked `@[implicit_reducible]` to fix the mismatch. +`.default` transparency but not at `.implicit` transparency, listing the suggesting semireducible +constants that could be be marked `@[implicit_reducible]` to fix the mismatch. -Unlike `linter.tacticCheckInstances`, which checks tactic goals, this runs on every declaration -added to the environment, so the warning also fires for declarations synthesized by attributes -such as `@[simps]` and `@[reassoc]`. Following the convention of the core tactic linter, it does -*not* participate in `linter.all`. +TODO: participate in linter.all? -/ def warnIfDeclIllTypedAtImplicit (decl : Declaration) : CoreM Unit := do unless linter.declCheckImplicit.get (← getOptions) do return - -- Stay quiet on declarations that already produced errors, as `warnIfUsesSorry` does. + -- Stay quiet on declarations that already produced errors. if ← MonadLog.hasErrors then return for (declName, declType) in declTypesToCheck decl do -- Compiler-internal auto-declarations (equation lemmas, etc.) would be noisy; skip them. From 24db27d0d9dc70c99bff785b58260ea807851fc1 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 22 Jun 2026 13:16:08 +0000 Subject: [PATCH 6/8] test: happy-path performance measurement --- src/Lean/AddDecl.lean | 103 +++++++++++++++++++++--------------------- 1 file changed, 52 insertions(+), 51 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 76dedd261865..d4cda69d88ad 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -133,7 +133,7 @@ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array N Core.withCurrHeartbeats do -- Fast path: Check the type at `.implicit`, without `diagnostics true`. Failure should be the -- absolute exception, so we optimize for the frequent case. - let implicitFailed : Bool ← + let _ : Bool ← try Meta.check declType .implicit pure false @@ -143,50 +143,51 @@ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array N logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" return none else pure true - unless implicitFailed do return none - let origDiag := (← get).diag - let result : Option (Array Name) ← withOptions (diagnostics.set · true) do - -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. - try Meta.check declType .default - catch e => - if e.isInterrupt then - modify ({ · with diag := origDiag }) - throw e - else - -- Any error while checking the type at default transparency is an unexpected error. - logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at default transparency.\n{e.toMessageData}" - return none - let counterDefault := (← get).diag.unfoldCounter - -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. - modify ({ · with diag := origDiag }) - try Meta.check declType .implicit - catch e => - if e.isInterrupt then - modify ({ · with diag := origDiag }) - throw e - else if e.isRuntime then - -- Warn if a resource limit has been reached. - logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" - return none - else - -- This check is expected to fail, so nothing to do in this case. - -- The `else` branch only exists for clarity. - pure () - let counterImplicit := (← get).diag.unfoldCounter - let env ← getEnv - -- Definitions unfolded by the `.default` check but not the `.implicit` one are the - -- candidates for `@[implicit_reducible]`. Only consider semireducible non-instances. - let mut candidates : Array Name := #[] - for (n, countDefault) in counterDefault do - let countImplicit := counterImplicit.find? n |>.getD 0 - if countDefault > countImplicit - && getReducibilityStatusCore env n matches .semireducible - && !Meta.isInstanceCore env n then - candidates := candidates.push n - return some candidates - -- Always restore the original diagnostics snapshot. - modify ({ · with diag := origDiag }) - return result + return none -- TODO + -- unless implicitFailed do return none + -- let origDiag := (← get).diag + -- let result : Option (Array Name) ← withOptions (diagnostics.set · true) do + -- -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. + -- try Meta.check declType .default + -- catch e => + -- if e.isInterrupt then + -- modify ({ · with diag := origDiag }) + -- throw e + -- else + -- -- Any error while checking the type at default transparency is an unexpected error. + -- logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at default transparency.\n{e.toMessageData}" + -- return none + -- let counterDefault := (← get).diag.unfoldCounter + -- -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. + -- modify ({ · with diag := origDiag }) + -- try Meta.check declType .implicit + -- catch e => + -- if e.isInterrupt then + -- modify ({ · with diag := origDiag }) + -- throw e + -- else if e.isRuntime then + -- -- Warn if a resource limit has been reached. + -- logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" + -- return none + -- else + -- -- This check is expected to fail, so nothing to do in this case. + -- -- The `else` branch only exists for clarity. + -- pure () + -- let counterImplicit := (← get).diag.unfoldCounter + -- let env ← getEnv + -- -- Definitions unfolded by the `.default` check but not the `.implicit` one are the + -- -- candidates for `@[implicit_reducible]`. Only consider semireducible non-instances. + -- let mut candidates : Array Name := #[] + -- for (n, countDefault) in counterDefault do + -- let countImplicit := counterImplicit.find? n |>.getD 0 + -- if countDefault > countImplicit + -- && getReducibilityStatusCore env n matches .semireducible + -- && !Meta.isInstanceCore env n then + -- candidates := candidates.push n + -- return some candidates + -- -- Always restore the original diagnostics snapshot. + -- modify ({ · with diag := origDiag }) + -- return result /-- If `linter.declCheckImplicit` is enabled, warns when a declaration's type is type-correct at @@ -204,12 +205,12 @@ def warnIfDeclIllTypedAtImplicit (decl : Declaration) : CoreM Unit := do if ← isAutoDeclOrPrivate_Internal declName then continue let some candidates ← (checkImplicitTransparency declType).run' | continue if candidates.isEmpty then continue - let bullets := MessageData.joinSep - (candidates.toList.map (m!"{MessageData.ofConstName ·}")) Format.line - Linter.logLint linter.declCheckImplicit (← getRef) - m!"declaration {MessageData.ofConstName declName} is not type-correct at \ - `.implicit` transparency; consider marking some of the following as \ - `@[implicit_reducible]`:{indentD bullets}" + -- let bullets := MessageData.joinSep + -- (candidates.toList.map (m!"{MessageData.ofConstName ·}")) Format.line + -- Linter.logLint linter.declCheckImplicit (← getRef) + -- m!"declaration {MessageData.ofConstName declName} is not type-correct at \ + -- `.implicit` transparency; consider marking some of the following as \ + -- `@[implicit_reducible]`:{indentD bullets}" builtin_initialize registerTraceClass `addDecl From babe9c6eedcc9e2711598bfe537adcf610858961 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 24 Jun 2026 12:15:59 +0200 Subject: [PATCH 7/8] Revert "test: happy-path performance measurement" This reverts commit 24db27d0d9dc70c99bff785b58260ea807851fc1. --- src/Lean/AddDecl.lean | 103 +++++++++++++++++++++--------------------- 1 file changed, 51 insertions(+), 52 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index d4cda69d88ad..76dedd261865 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -133,7 +133,7 @@ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array N Core.withCurrHeartbeats do -- Fast path: Check the type at `.implicit`, without `diagnostics true`. Failure should be the -- absolute exception, so we optimize for the frequent case. - let _ : Bool ← + let implicitFailed : Bool ← try Meta.check declType .implicit pure false @@ -143,51 +143,50 @@ private def checkImplicitTransparency (declType : Expr) : MetaM (Option (Array N logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" return none else pure true - return none -- TODO - -- unless implicitFailed do return none - -- let origDiag := (← get).diag - -- let result : Option (Array Name) ← withOptions (diagnostics.set · true) do - -- -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. - -- try Meta.check declType .default - -- catch e => - -- if e.isInterrupt then - -- modify ({ · with diag := origDiag }) - -- throw e - -- else - -- -- Any error while checking the type at default transparency is an unexpected error. - -- logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at default transparency.\n{e.toMessageData}" - -- return none - -- let counterDefault := (← get).diag.unfoldCounter - -- -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. - -- modify ({ · with diag := origDiag }) - -- try Meta.check declType .implicit - -- catch e => - -- if e.isInterrupt then - -- modify ({ · with diag := origDiag }) - -- throw e - -- else if e.isRuntime then - -- -- Warn if a resource limit has been reached. - -- logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" - -- return none - -- else - -- -- This check is expected to fail, so nothing to do in this case. - -- -- The `else` branch only exists for clarity. - -- pure () - -- let counterImplicit := (← get).diag.unfoldCounter - -- let env ← getEnv - -- -- Definitions unfolded by the `.default` check but not the `.implicit` one are the - -- -- candidates for `@[implicit_reducible]`. Only consider semireducible non-instances. - -- let mut candidates : Array Name := #[] - -- for (n, countDefault) in counterDefault do - -- let countImplicit := counterImplicit.find? n |>.getD 0 - -- if countDefault > countImplicit - -- && getReducibilityStatusCore env n matches .semireducible - -- && !Meta.isInstanceCore env n then - -- candidates := candidates.push n - -- return some candidates - -- -- Always restore the original diagnostics snapshot. - -- modify ({ · with diag := origDiag }) - -- return result + unless implicitFailed do return none + let origDiag := (← get).diag + let result : Option (Array Name) ← withOptions (diagnostics.set · true) do + -- A type that is not even correct at `.default` is a more fundamental problem; ignore it here. + try Meta.check declType .default + catch e => + if e.isInterrupt then + modify ({ · with diag := origDiag }) + throw e + else + -- Any error while checking the type at default transparency is an unexpected error. + logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at default transparency.\n{e.toMessageData}" + return none + let counterDefault := (← get).diag.unfoldCounter + -- Reset the unfold counter and re-check at `.implicit` to record what it unfolds. + modify ({ · with diag := origDiag }) + try Meta.check declType .implicit + catch e => + if e.isInterrupt then + modify ({ · with diag := origDiag }) + throw e + else if e.isRuntime then + -- Warn if a resource limit has been reached. + logWarning m!"The `declCheckImplicit` linter failed with an unexpected error while checking the type of `{declType}` at implicit transparency.\n{e.toMessageData}" + return none + else + -- This check is expected to fail, so nothing to do in this case. + -- The `else` branch only exists for clarity. + pure () + let counterImplicit := (← get).diag.unfoldCounter + let env ← getEnv + -- Definitions unfolded by the `.default` check but not the `.implicit` one are the + -- candidates for `@[implicit_reducible]`. Only consider semireducible non-instances. + let mut candidates : Array Name := #[] + for (n, countDefault) in counterDefault do + let countImplicit := counterImplicit.find? n |>.getD 0 + if countDefault > countImplicit + && getReducibilityStatusCore env n matches .semireducible + && !Meta.isInstanceCore env n then + candidates := candidates.push n + return some candidates + -- Always restore the original diagnostics snapshot. + modify ({ · with diag := origDiag }) + return result /-- If `linter.declCheckImplicit` is enabled, warns when a declaration's type is type-correct at @@ -205,12 +204,12 @@ def warnIfDeclIllTypedAtImplicit (decl : Declaration) : CoreM Unit := do if ← isAutoDeclOrPrivate_Internal declName then continue let some candidates ← (checkImplicitTransparency declType).run' | continue if candidates.isEmpty then continue - -- let bullets := MessageData.joinSep - -- (candidates.toList.map (m!"{MessageData.ofConstName ·}")) Format.line - -- Linter.logLint linter.declCheckImplicit (← getRef) - -- m!"declaration {MessageData.ofConstName declName} is not type-correct at \ - -- `.implicit` transparency; consider marking some of the following as \ - -- `@[implicit_reducible]`:{indentD bullets}" + let bullets := MessageData.joinSep + (candidates.toList.map (m!"{MessageData.ofConstName ·}")) Format.line + Linter.logLint linter.declCheckImplicit (← getRef) + m!"declaration {MessageData.ofConstName declName} is not type-correct at \ + `.implicit` transparency; consider marking some of the following as \ + `@[implicit_reducible]`:{indentD bullets}" builtin_initialize registerTraceClass `addDecl From d5ea8df7e919b83ac3bf721636994d9faaaaffaf Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 24 Jun 2026 12:18:03 +0200 Subject: [PATCH 8/8] cleanup --- src/Lean/AddDecl.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 76dedd261865..8a3f80e40c6b 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -12,10 +12,10 @@ public import Lean.OriginalConstKind public import Lean.AutoDecl import Lean.Linter.Init import Lean.Compiler.MetaAttr -import Lean.Meta.Check -- for the `linter.declCheckImplicit` linter -import Lean.Meta.Instances -- for the `linter.declCheckImplicit` linter -import Lean.ReducibilityAttrs -- for the `linter.declCheckImplicit` linter -import all Lean.OriginalConstKind -- for accessing `privateConstKindsExt` +import Lean.Meta.Check +import Lean.Meta.Instances +import Lean.ReducibilityAttrs +import all Lean.OriginalConstKind public section