feat: lint on open statements within namespace which do not open all candidate namespaces (#14325)

This PR adds a linter which warns on `open` statements which do not in
fact open all namespaces which end in the given name.

Example:
```lean
def A.B.a1 : Nat := 0
def B.a2 : Nat := 0

namespace A
open B

#check a2
```

Here, we lint on `open B` since `_root_.B` is not actually opened.

This will help with fixing downstream fallout from adding new
namespaces. Suppose we have just
```lean
def B.a2 : Nat := 0

namespace A
open B

#check a2
```

This compiles. Now suppose upstream adds `def A.B.a1 : Nat := 0`. Then
the above snippet no longer compiles, with only an `unknown identifier`
error on `a2`. With the new linter, we now also get a warning on the
`open B` which warns us that `_root_.B` is no longer imported, which
should help with understanding the `unknown identifier` error (because
usually from the context of the file it is quite clear that we want
`_root_.B`, not `_root_.A.B`!).

Author: TwoFX

src/Init/Data/Fin/Lemmas.lean

@@ -152,7 +152,7 @@ attribute [scoped instance] instIntCast
 
 end IntCast
 
-open IntCast in
+open Fin.IntCast in
 theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
     (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := rfl
 

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -78,7 +78,7 @@ where
 
 end ToExpr
 
-open ToExpr
+open Lean.Compiler.LCNF.ToExpr
 
 private def Arg.toExprM (arg : Arg pu) : ToExprM Expr :=
   return arg.toExpr.abstract' (← read) (← get)

src/Lean/Elab/Open.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Util
 public import Lean.Parser.Command
 meta import Lean.Parser.Command
+public import Lean.Linter.AmbiguousOpen
 import Init.Omega
 
 public section
@@ -75,31 +76,38 @@ def elabOpenDecl [MonadOptions m] [MonadResolveName m] [MonadInfoTree m] (stx :
     match stx with
     | `(Parser.Command.openDecl| $nss*) =>
       for ns in nss do
-        for ns in (← resolveNamespace ns) do
+        let resolved ← resolveNamespace ns
+        Linter.checkAmbiguousOpen ns resolved
+        for ns in resolved do
           addOpenDecl (OpenDecl.simple ns [])
           activateScoped ns
     | `(Parser.Command.openDecl| scoped $nss*) =>
       for ns in nss do
-        for ns in (← resolveNamespace ns) do
+        let resolved ← resolveNamespace ns
+        Linter.checkAmbiguousOpen ns resolved
+        for ns in resolved do
           activateScoped ns
     | `(Parser.Command.openDecl| $ns ($ids*)) =>
       let nss ← resolveNamespace ns
+      Linter.checkAmbiguousOpen ns nss
       for idStx in ids do
         let declName ← resolveNameUsingNamespacesCore nss idStx
         if (← getInfoState).enabled then
           addConstInfo idStx declName
         addOpenDecl (OpenDecl.explicit idStx.getId declName)
-    | `(Parser.Command.openDecl| $ns hiding $ids*) =>
-      let ns ← resolveUniqueNamespace ns
+    | `(Parser.Command.openDecl| $nsStx hiding $ids*) =>
+      let ns ← resolveUniqueNamespace nsStx
+      Linter.checkAmbiguousOpen nsStx [ns]
       activateScoped ns
       for id in ids do
         let declName ← resolveId ns id
         if (← getInfoState).enabled then
           addConstInfo id declName
       let ids := ids.map (·.getId) |>.toList
       addOpenDecl (OpenDecl.simple ns ids)
-    | `(Parser.Command.openDecl| $ns renaming $[$froms -> $tos],*) =>
-      let ns ← resolveUniqueNamespace ns
+    | `(Parser.Command.openDecl| $nsStx renaming $[$froms -> $tos],*) =>
+      let ns ← resolveUniqueNamespace nsStx
+      Linter.checkAmbiguousOpen nsStx [ns]
       for («from», to) in froms.zip tos do
         let declName ← resolveId ns «from»
         if (← getInfoState).enabled then

src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean

@@ -24,7 +24,7 @@ side of `@[spec]` into the same database, and looking up the specs matching a pr
 
 namespace Lean.Elab.Tactic.Do.Internal
 
-open SpecAttr
+open Lean.Elab.Tactic.Do.Internal.SpecAttr
 
 /-- Returns `true` if `e` is already internalized into the current `SymM` share table, in which case
 `shareCommon e` returns `e` unchanged. -/

src/Lean/Elab/Tactic/Grind/Anchor.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 namespace Lean.Elab.Tactic.Grind
-open Meta Grind
+open Meta Lean.Meta.Grind
 
 public def elabAnchorRef (anchor : TSyntax `hexnum) : CoreM AnchorRef := do
   let numDigits := anchor.getHexNumSize

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -324,7 +324,7 @@ def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
   catch _ =>
     pure false
 
-open Grind
+open Lean.Meta.Grind
 
 /-
 **Note**: Recall that `grind` uses the reducibility specified at `Config.reducible`

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -83,7 +83,7 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 
-open Meta Grind
+open Meta Lean.Meta.Grind
 
 @[builtin_grind_tactic finish] def evalFinish : GrindTactic := fun stx => withMainContext do
   let `(grind| finish $[$configItems]* $[only%$only]? $[[$params?,*]]?) := stx | throwUnsupportedSyntax

src/Lean/Elab/Tactic/Grind/Cbv.lean

@@ -8,7 +8,7 @@ prelude
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Meta.Tactic.Cbv.Main
 namespace Lean.Elab.Tactic.Grind
-open Meta Grind
+open Meta
 
 @[builtin_grind_tactic Parser.Tactic.Grind.symCbv] def evalSymCbv : GrindTactic := fun _ => withMainContext do
   ensureSym

src/Lean/Elab/Tactic/Grind/DSimp.lean

@@ -11,7 +11,7 @@ import Lean.Meta.Sym.DSimp.Variant
 import Lean.Meta.Sym.DSimp.Reduce
 import Lean.Meta.Sym.DSimp.DSimproc
 namespace Lean.Elab.Tactic.Grind
-open Meta Grind
+open Meta
 open Sym.DSimp
 
 def elabDSimpArgs (args? : Option (Array (TSyntax [`token.«*», `ident]))) : GrindTacticM DSimpArgs := do

src/Lean/Elab/Tactic/Grind/Filter.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Meta.Tactic.Grind.Filter
 namespace Lean.Elab.Tactic.Grind
-open Meta Grind
+open Meta Lean.Meta.Grind
 
 public partial def elabFilter (filter? : Option (TSyntax `grind_filter)) : GrindTacticM Filter := do
   let some filter := filter? | return .true