feat: add linter.redundantExpose for redundant @[expose]/@[no_expose] attributes

src/Lean/Elab/MutualDef.lean

@@ -1184,6 +1184,11 @@ register_builtin_option warn.exposeOnPrivate : Bool := {
   descr    := "warn about uses of `@[expose]` on private declarations"
 }
 
+register_builtin_option linter.redundantExpose : Bool := {
+  defValue := true
+  descr    := "warn on redundant `@[expose]`/`@[no_expose]` attributes"
+}
+
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1336,6 +1341,49 @@ where
               logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \
                 definitions only"
 
+    if Linter.getLinterValue linter.redundantExpose (← Linter.getLinterOptions) then
+      let inExposeSection := sc.attrs.any (· matches `(attrInstance| expose))
+      for header in headers do
+        for attr in header.modifiers.attrs do
+          unless attr.stx.getHeadInfo matches .original .. do continue
+          if attr.name == `expose then do
+            if !env.header.isModule then
+              logWarningAt attr.stx m!"`@[expose]` has no effect outside a `module` file{
+                .note m!"This linter can be disabled with \
+                  `set_option {linter.redundantExpose.name} false`"}"
+            else if env.isExporting then
+              if header.kind == .abbrev then
+                logWarningAt attr.stx m!"`@[expose]` has no effect on `abbrev` declarations; \
+                  they are always exposed{
+                  .note m!"This linter can be disabled with \
+                    `set_option {linter.redundantExpose.name} false`"}"
+              else if header.kind == .instance && !(← isProp header.type) then
+                logWarningAt attr.stx m!"`@[expose]` has no effect on data `instance` declarations; \
+                  they are always exposed{
+                  .note m!"This linter can be disabled with \
+                    `set_option {linter.redundantExpose.name} false`"}"
+              else if header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && inExposeSection then
+                logWarningAt attr.stx m!"`@[expose]` has no effect inside an `@[expose] section`{
+                  .note m!"This linter can be disabled with \
+                    `set_option {linter.redundantExpose.name} false`"}"
+          else if attr.name == `no_expose then
+            if !env.header.isModule then
+              logWarningAt attr.stx m!"`@[no_expose]` has no effect outside a `module` file{
+                .note m!"This linter can be disabled with \
+                  `set_option {linter.redundantExpose.name} false`"}"
+            else if env.isExporting then
+              -- Would the declaration be exposed without `@[no_expose]`?
+              let wouldBeExposed :=
+                (header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && inExposeSection) ||
+                header.modifiers.attrs.any (·.name == `expose) ||
+                header.kind == .abbrev ||
+                (header.kind == .instance && !(← isProp header.type))
+              if !wouldBeExposed then
+                logWarningAt attr.stx m!"`@[no_expose]` has no effect; this declaration would not \
+                  be exposed by default{
+                  .note m!"This linter can be disabled with \
+                    `set_option {linter.redundantExpose.name} false`"}"
+
     -- Switch to private scope if...
     withoutExporting (when :=
       (← headers.allM (fun header => do

tests/elab/linterRedundantExpose.lean

@@ -0,0 +1,56 @@
+module
+
+set_option linter.all true
+set_option linter.missingDocs false
+
+public section
+
+-- `@[expose]` on abbrev should warn
+/--
+warning: `@[expose]` has no effect on `abbrev` declarations; they are always exposed
+
+Note: This linter can be disabled with `set_option linter.redundantExpose false`
+-/
+#guard_msgs in
+@[expose] abbrev myAbbrev := 1
+
+-- `@[expose]` on a regular public def should not warn
+#guard_msgs in
+@[expose] def myDef := 1
+
+-- `@[no_expose]` on a regular def outside expose section should warn
+/--
+warning: `@[no_expose]` has no effect; this declaration would not be exposed by default
+
+Note: This linter can be disabled with `set_option linter.redundantExpose false`
+-/
+#guard_msgs in
+@[no_expose] def myDef3 := 3
+
+-- `@[no_expose]` on abbrev should not warn (it overrides auto-expose)
+#guard_msgs in
+@[no_expose] abbrev myAbbrev2 := 5
+
+end
+
+-- `@[expose]` inside `@[expose] section` on a def should warn
+@[expose] public section
+/--
+warning: `@[expose]` has no effect inside an `@[expose] section`
+
+Note: This linter can be disabled with `set_option linter.redundantExpose false`
+-/
+#guard_msgs in
+@[expose] def myDef2 := 2
+
+-- `@[no_expose]` inside `@[expose] section` should not warn (it's meaningful)
+#guard_msgs in
+@[no_expose] def myDef4 := 4
+end
+
+-- disabling the linter should suppress warnings
+public section
+#guard_msgs in
+set_option linter.redundantExpose false in
+@[expose] abbrev myAbbrev3 := 6
+end