From cf12c6bfb40d3cfebb33ae54cb9ce4249e7bf4d0 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/3] 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 9817d0f612db30a0bb45439202fab2be3fb1aa4a 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/3] 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 e565a0367b9d99d15a0cacd8bc03e8b4faf74644 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/3] 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