feat: warn on transitive deprecations

src/Lean/Attributes.lean

@@ -260,22 +260,29 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   filterExport : Environment → Name → α → Bool := fun env n _ =>
     env.contains (skipRealize := false) n
 
-def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
-  let ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α) ← registerPersistentEnvExtension {
-    name            := impl.ref
+def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false)
+    (filterExport : Environment → Name → α → Bool := fun env n _ =>
+      env.contains (skipRealize := false) n) :
+    IO (PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) :=
+  registerPersistentEnvExtension {
+    name            := ref
     mkInitial       := pure ([], {})
     addImportedFn   := fun _ => pure ([], {})
     addEntryFn      := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2)
     exportEntriesFnEx := fun env (decls, m) => Id.run do
-      let all := if impl.preserveOrder then
+      let all := if preserveOrder then
         decls.toArray.reverse.filterMap (fun n => return (n, ← m.find? n))
       else
         let r := m.foldl (fun a n p => a.push (n, p)) #[]
         r.qsort (fun a b => Name.quickLt a.1 b.1)
-      let exported := all.filter (fun ⟨n, a⟩ => impl.filterExport env n a)
+      let exported := all.filter (fun ⟨n, a⟩ => filterExport env n a)
       { exported, server := exported, «private» := all }
     statsFn         := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size
   }
+
+def registerParametricAttributeForExt (impl : ParametricAttributeImpl α)
+    (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) :
+    IO (ParametricAttribute α) := do
   let attrImpl : AttributeImpl := {
     impl.toAttributeImplCore with
     add   := fun decl stx kind => do
@@ -290,27 +297,40 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl, ext, preserveOrder := impl.preserveOrder }
 
+def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
+  let ext ← registerParametricAttributeExt (α := α) impl.ref impl.preserveOrder impl.filterExport
+  registerParametricAttributeForExt impl ext
+
 namespace ParametricAttribute
 
-def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
+def getParamFromExt? [Inhabited α]
+    (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α))
+    (preserveOrder : Bool) (env : Environment) (decl : Name) : Option α :=
   match env.getModuleIdxFor? decl with
   | some modIdx =>
-    let entry? := if attr.preserveOrder then
-      (attr.ext.getModuleEntries env modIdx).find? (·.1 == decl)
+    let entry? := if preserveOrder then
+      (ext.getModuleEntries env modIdx).find? (·.1 == decl)
     else
-      (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1)
+      (ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1)
     match entry? with
     | some (_, val) => some val
     | none          => none
-  | none        => (attr.ext.getState env).2.find? decl
+  | none        => (ext.getState env).2.find? decl
 
-def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
+def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
+  getParamFromExt? attr.ext attr.preserveOrder env decl
+
+def setParamFromExt
+  (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) (attr : AttributeImpl) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
-    Except.error (s!"Failed to add parametric attribute `[{attr.attr.name}]` to `{decl}`: Declaration is in an imported module")
-  else if ((attr.ext.getState env).2.find? decl).isSome then
-    Except.error (s!"Failed to add parametric attribute `[{attr.attr.name}]` to `{decl}`: Attribute has already been set")
+    Except.error (s!"Failed to add parametric attribute `[{attr.name}]` to `{decl}`: Declaration is in an imported module")
+  else if ((ext.getState env).2.find? decl).isSome then
+    Except.error (s!"Failed to add parametric attribute `[{attr.name}]` to `{decl}`: Attribute has already been set")
   else
-    Except.ok (attr.ext.addEntry env (decl, param))
+    Except.ok (ext.addEntry env (decl, param))
+
+def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
+  setParamFromExt attr.ext attr.attr env decl param
 
 end ParametricAttribute
 

src/Lean/Linter/Deprecated.lean

@@ -21,22 +21,60 @@ register_builtin_option linter.deprecated : Bool := {
   descr := "if true, generate deprecation warnings"
 }
 
+register_builtin_option linter.deprecated.deprecatedTarget : Bool := {
+  defValue := true
+  descr := "if true, warn when a `@[deprecated]` attribute points at a declaration that is \
+    itself deprecated"
+}
+
 structure DeprecationEntry where
   newName? : Option Name := none
   text? : Option String := none
   since? : Option String := none
   deriving Inhabited
 
-builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
-  registerParametricAttribute {
+open Meta in
+def deprecationTypeMismatchNote? (oldName newName : Name) : CoreM (Option MessageData) := do
+  let env ← getEnv
+  let some old := env.find? oldName | return none
+  let some new := env.find? newName | return none
+  if ← MetaM.run' <| withReducible <| isDefEqGuarded old.type new.type then
+    return none
+  return some <| .note m!"The suggested replacement has a different type:{indentExpr new.type}\
+    \ninstead of{indentExpr old.type}"
+
+builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do
+  let ext ← registerParametricAttributeExt (α := DeprecationEntry) `Lean.Linter.deprecatedAttr
+  registerParametricAttributeForExt (ext := ext) {
     name := `deprecated
     descr := "mark declaration as deprecated",
-    getParam := fun _ stx => do
+    getParam := fun declName stx => do
       let `(attr| deprecated $[$id?]? $[$text?]? $[(since := $since?)]?) := stx
         | throwError "Invalid `[deprecated]` attribute syntax"
       let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo
       if let some newName := newName? then
         recordExtraModUseFromDecl (isMeta := false) newName
+        if getLinterValue linter.deprecated (← getLinterOptions)
+            && linter.deprecated.deprecatedTarget.get (← getOptions) then
+          let env ← getEnv
+          match ParametricAttribute.getParamFromExt? ext (preserveOrder := false) env newName with
+          | none => pure ()
+          | some entry =>
+            let disableNote : MessageData := .note m!"This warning can be disabled with \
+              `set_option {linter.deprecated.deprecatedTarget.name} false`"
+            match entry.newName? with
+            | some next =>
+              if next != newName && next != declName then
+                let mut msg := m!"`{.ofConstName newName true}` is itself deprecated in favor of \
+                  `{.ofConstName next true}`; consider deprecating `{.ofConstName declName true}` \
+                  in favor of `{.ofConstName next true}` instead"
+                if let some note ← deprecationTypeMismatchNote? declName next then
+                  msg := msg ++ note
+                logWarning <| msg ++ disableNote
+            | none =>
+              logWarning <| m!"`{.ofConstName newName true}` is itself deprecated, but without an \
+                explicit replacement; `{.ofConstName declName true}` is being deprecated in favor \
+                of a deprecated declaration" ++ disableNote
       let text? := text?.map TSyntax.getString
       let since? := since?.map TSyntax.getString
       if id?.isNone && text?.isNone then

tests/elab/7993.lean

@@ -35,6 +35,13 @@ example := foo
 
 abbrev Bar := Nat
 
+-- `Foo.foo` is itself deprecated in favor of `Foo.bar`, so deprecating `Bar.bar` towards it warns.
+/--
+warning: `Foo.foo` is itself deprecated in favor of `Foo.bar`; consider deprecating `Bar.bar` in favor of `Foo.bar` instead
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
 @[deprecated Foo.foo (since := "2025-01-01")]
 def Bar.bar : Bar → Bar := id
 

tests/elab/deprecatedTransitive.lean

@@ -0,0 +1,125 @@
+/-!
+# Warn when a `@[deprecated]` attribute points at an already-deprecated declaration
+
+When `A` is deprecated in favor of `B`, and `B` is itself deprecated in favor of `C`, deprecating
+`A` towards `B` is discouraged: `B`'s deprecation record points at `C`, so `A` should point at `C`
+instead. The `@[deprecated]` attribute inspects `B`'s deprecation record (only one step) and warns
+accordingly. The check can be turned off with `linter.deprecated.deprecatedTarget`.
+-/
+
+set_option linter.deprecated true
+
+def c1 : Nat := 0
+
+@[deprecated c1 (since := "2020-01-01")]
+def b1 : Nat := 0
+
+/--
+warning: `b1` is itself deprecated in favor of `c1`; consider deprecating `a1` in favor of `c1` instead
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
+@[deprecated b1 (since := "2020-01-01")]
+def a1 : Nat := 0
+
+/-! Longer chain `a2 → b2 → c2 → d2`: only one step is followed, so `a2` is pointed at `c2`. -/
+
+def d2 : Nat := 0
+
+set_option linter.deprecated false in
+@[deprecated d2 (since := "2020-01-01")]
+def c2 : Nat := 0
+
+set_option linter.deprecated false in
+@[deprecated c2 (since := "2020-01-01")]
+def b2 : Nat := 0
+
+/--
+warning: `b2` is itself deprecated in favor of `c2`; consider deprecating `a2` in favor of `c2` instead
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
+@[deprecated b2 (since := "2020-01-01")]
+def a2 : Nat := 0
+
+/-! Text-only terminal: `b3` is deprecated without an explicit replacement. -/
+
+@[deprecated "no replacement" (since := "2020-01-01")]
+def b3 : Nat := 0
+
+/--
+warning: `b3` is itself deprecated, but without an explicit replacement; `a3` is being deprecated in favor of a deprecated declaration
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
+@[deprecated b3 (since := "2020-01-01")]
+def a3 : Nat := 0
+
+/-! One step at a target that is itself text-only deprecated: `a4` is pointed at `c4`. -/
+
+@[deprecated "no replacement" (since := "2020-01-01")]
+def c4 : Nat := 0
+
+set_option linter.deprecated false in
+@[deprecated c4 (since := "2020-01-01")]
+def b4 : Nat := 0
+
+/--
+warning: `b4` is itself deprecated in favor of `c4`; consider deprecating `a4` in favor of `c4` instead
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
+@[deprecated b4 (since := "2020-01-01")]
+def a4 : Nat := 0
+
+/-! Type disagreement between the initial declaration and the suggested replacement. -/
+
+def c5 : Bool := true
+
+@[deprecated c5 (since := "2020-01-01")]
+def b5 : Bool := true
+
+/--
+warning: `b5` is itself deprecated in favor of `c5`; consider deprecating `a5` in favor of `c5` instead
+
+Note: The suggested replacement has a different type:
+  Bool
+instead of
+  Nat
+
+Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false`
+-/
+#guard_msgs in
+@[deprecated b5 (since := "2020-01-01")]
+def a5 : Nat := 0
+
+/-! No warning when the target is not itself deprecated. -/
+
+def c6 : Nat := 0
+
+#guard_msgs in
+@[deprecated c6 (since := "2020-01-01")]
+def a6 : Nat := 0
+
+/-! Disabling via `linter.deprecated.deprecatedTarget` suppresses the check. -/
+
+def c8 : Nat := 0
+
+@[deprecated c8 (since := "2020-01-01")]
+def b8 : Nat := 0
+
+set_option linter.deprecated.deprecatedTarget false in
+#guard_msgs in
+@[deprecated b8 (since := "2020-01-01")]
+def a8 : Nat := 0
+
+/-! Turning off `linter.deprecated` entirely also suppresses the check. -/
+
+set_option linter.deprecated false in
+#guard_msgs in
+@[deprecated b8 (since := "2020-01-01")]
+def a9 : Nat := 0