test: avoid testing colliding private inductives (#11041)

`prelude-injectivity.lean` was testing inj thm generation for all
inductives in core, including private ones, which could lead to name
clashes that should not be able to occur in actual files. Put it under
the module system to not load private decls in the first place.

Author: Kha

src/Lean/AddDecl.lean

@@ -137,6 +137,11 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
       trace[addDecl] "no matching async adding rules, adding synchronously"
       return (← doAdd)
 
+  -- Check early so we can avoid related env ext panics that would happen before the check in the
+  -- kernel.
+  if (← getEnv).containsOnBranch name then
+    throwKernelException <| .alreadyDeclared (← getEnv).toKernelEnv name
+
   if decl.getTopLevelNames.all isPrivateName then
     if (← ResolveName.backward.privateInPublic.getM) then
       trace[addDecl] "private decl under `privateInPublic`, exporting as is"
@@ -152,9 +157,9 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
       trace[addDecl] "no matching exporting rules, exporting as is"
       exportedInfo? := some info
 
+  let env ← getEnv
   -- no environment extension changes to report after kernel checking; ensures we do not
   -- accidentally wait for this snapshot when querying extension states
-  let env ← getEnv
   let async ← env.addConstAsync (reportExts := false) name kind
     (exportedKind? := exportedInfo?.map (.ofConstantInfo))
   -- report preliminary constant info immediately

tests/lean/run/bvarcrash.lean

@@ -629,17 +629,16 @@ def decl_9 : Lean.Declaration :=
     type := expr_443
     value := expr_0
   }
-run_meta Lean.addDecl decl_0
-run_meta Lean.addDecl decl_1
-run_meta Lean.addDecl decl_2
-run_meta Lean.addDecl decl_3
-run_meta Lean.addDecl decl_4
-run_meta Lean.addDecl decl_5
-run_meta Lean.addDecl decl_6
-run_meta Lean.addDecl decl_7
-run_meta Lean.addDecl decl_8
+
+open Lean
+
+-- We avoid `Lean.addDecl` as it may be doing additional checks that hide the expected error.
+run_meta do
+  for decl in [decl_0, decl_1, decl_2, decl_3, decl_4, decl_5, decl_6, decl_7, decl_8] do
+    setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl none)
 /--
 error: (kernel) type checker does not support loose bound variables, replace them with free variables before invoking it
 -/
 #guard_msgs in
-run_meta Lean.addDecl decl_9
+run_meta
+    setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_9 none)

tests/lean/run/prelude-injectivity.lean

@@ -1,12 +1,12 @@
+module
+
 import Lean
 
 open Lean Meta
 
 -- without this, the catch below does not catch kernel errors
 set_option Elab.async false
 
-#exit -- **TODO**: remove after fixing async panic
-
 /--
 info: Possible candidates for Init/Core.lean (these do not need to be added if they are irrelevant for verification):
 gen_injective_theorems% MacroScopesView
@@ -16,7 +16,6 @@ gen_injective_theorems% TSyntax
 gen_injective_theorems% Macro.Context
 gen_injective_theorems% Macro.Exception
 gen_injective_theorems% Macro.Methods
-gen_injective_theorems% Macro.State
 gen_injective_theorems% Syntax.Preresolved
 gen_injective_theorems% Syntax.SepArray
 gen_injective_theorems% Syntax.TSepArray