chore: warn on [expose] on private definition (#9917)

src/Init/NotationExtra.lean

@@ -77,7 +77,11 @@ macro_rules
     for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
       body ← `($c₁ = $c₂ → $body)
     let hint : Ident ← `(hint)
-    `($[$doc?:docComment]? @[$kind unification_hint, expose] def $(n.getD hint) $bs* : Sort _ := $body)
+    match kind with
+    | `(attrKind| local) =>
+      `($[$doc?:docComment]? @[$kind unification_hint] private def $(n.getD hint) $bs* : Sort _ := $body)
+    | _ =>
+      `($[$doc?:docComment]? @[$kind unification_hint, expose] public def $(n.getD hint) $bs* : Sort _ := $body)
 end Lean
 
 open Lean

src/Lean/Elab/Deriving/Basic.lean

@@ -227,6 +227,8 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandE
   -- When any of the types are private, the deriving handler will need access to the private scope
   -- (and should also make sure to put its outputs in the private scope).
   withoutExporting (when := typeNames.any isPrivateName) do
+  -- Deactivate some linting options that only make writing deriving handlers more painful.
+  withScope (fun sc => { sc with opts := sc.opts.setBool `warn.exposeOnPrivate false }) do
   withTraceNode `Elab.Deriving (fun _ => return m!"running deriving handlers for `{.ofConstName className}`") do
     match (← derivingHandlersRef.get).find? className with
     | some handlers =>

src/Lean/Elab/MutualDef.lean

@@ -1140,6 +1140,11 @@ private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElab
 structure AsyncBodyInfo where
 deriving TypeName
 
+register_builtin_option warn.exposeOnPrivate : Bool := {
+  defValue := true
+  descr    := "warn about uses of `@[expose]` on private declarations"
+}
+
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1248,6 +1253,14 @@ where
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
   finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => do
     let env ← getEnv
+    if warn.exposeOnPrivate.get (← getOptions) then
+      if env.header.isModule && !env.isExporting then
+        for header in headers do
+          for attr in header.modifiers.attrs do
+            if attr.name == `expose then
+              logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \
+                definitions only"
+
     withExporting (isExporting :=
       headers.any (fun header =>
         header.modifiers.isInferredPublic env &&