bug: using `private import` can lead to panic in downstream file

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In at least one situation, adding a private import to a file in the lean4 repository leads to panic in a dependent file. The panic disappears if the import is made private.

Context

This occurred while working on #8841, which left a TODO above the problematic import in Init.Data.Vector.Basic.

Steps to Reproduce

I was not able to disentangle the problem from the lean4 repository so far. This PR, however, contains a minimal set of changes to the lean4 repository that reproduce it.

1. Check out the branch of the PR.
2. Try to build using make. (Just looking at the CI build logs does not suffice because the build was aborted after finding sorrys that were introduced as part of the minimization.)

Expected behavior: [Clear and concise description of what you expect to happen]

Build goes through. Because the build goes through without the import and with a public import, I would expect it to succeed also with a private import and definitely not panic.

Actual behavior: [Clear and concise description of what actually happens]

The build panics in Init.Data.Grind.Poly with:

PANIC at Lean.MapDeclarationExtension.insert Lean.EnvExtension:151:2: assertion violation: env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension

The whole back trace is attached below.

Versions

I can confirm that this behavior persists on the 2nd of July nightly.

#version output for a recent reproduction:

Lean 4.23.0, commit ff5becc41a3c62b541c6800b3fed7bdff2a0f7e4
Target: arm64-apple-darwin24.5.0 macOS

Additional Information

Error message:

PANIC at Lean.MapDeclarationExtension.insert Lean.EnvExtension:151:2: assertion violation: env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
  
backtrace:
0   libleanshared.dylib                 0x000000010cd8aeb4 lean_panic + 272
1   libleanshared.dylib                 0x000000010cd8b0b8 lean_panic_fn + 32
2   libleanshared.dylib                 0x000000010c34cee0 l_Lean_addDecl___lam__2 + 668
3   libleanshared.dylib                 0x000000010afa9ac8 l_Lean_Elab_Eqns_mkEqns_doRealize + 3792
4   libleanshared.dylib                 0x000000010cd9d740 lean_apply_5 + 1188
5   libleanshared.dylib                 0x00000001099b45b4 l_Lean_Meta_realizeConst_realizeAndReport___lam__0 + 168
6   libleanshared.dylib                 0x000000010cd9d344 lean_apply_5 + 168
7   libleanshared.dylib                 0x00000001099a9608 l_IO_withStderr___at___IO_FS_withIsolatedStreams___at___Lean_Meta_realizeConst_realizeAndReport_spec__1_spec__3___redArg + 156
8   libleanshared.dylib                 0x000000010cd9dc40 lean_apply_5 + 2468
9   libleanshared.dylib                 0x00000001099a8ba8 l_IO_withStdout___at___IO_FS_withIsolatedStreams___at___Lean_Meta_realizeConst_realizeAndReport_spec__1_spec__1___redArg + 156
10  libleanshared.dylib                 0x000000010cd9dc40 lean_apply_5 + 2468
11  libleanshared.dylib                 0x00000001099a90d8 l_IO_withStdin___at___IO_FS_withIsolatedStreams___at___Lean_Meta_realizeConst_realizeAndReport_spec__1_spec__2___redArg + 156
12  libleanshared.dylib                 0x00000001099a9b88 l_IO_FS_withIsolatedStreams___at___Lean_Meta_realizeConst_realizeAndReport_spec__1___redArg + 480
13  libleanshared.dylib                 0x00000001099b61e4 l_Lean_Meta_realizeConst_realizeAndReport + 4268
14  libleanshared.dylib                 0x000000010cd9a9d8 lean_apply_3 + 2332
15  libleanshared.dylib                 0x000000010c5cf93c l_Lean_Environment_realizeConst + 5900
16  libleanshared.dylib                 0x00000001099b9784 l_Lean_Meta_realizeConst___lam__3 + 444
17  libleanshared.dylib                 0x00000001099bbce4 l_Lean_Meta_realizeConst___lam__3___boxed + 92
18  libleanshared.dylib                 0x000000010cd9e100 lean_apply_5 + 3684
19  libleanshared.dylib                 0x00000001099bb88c l_Lean_Meta_realizeConst + 1532
20  libleanshared.dylib                 0x000000010afaaaf0 l_Std_Range_forIn_x27_loop___at___Lean_Elab_Eqns_mkEqns_spec__0___redArg + 1940
21  libleanshared.dylib                 0x000000010afadbd8 l_Lean_Elab_Eqns_mkEqns + 7380
22  libleanshared.dylib                 0x000000010b0524fc l_Lean_Elab_Nonrec_getEqnsFor_x3f + 1352
23  libleanshared.dylib                 0x000000010cd9f1d0 lean_apply_6 + 2112
24  libleanshared.dylib                 0x0000000109aad370 l_List_forIn_x27_loop___at_____private_Lean_Meta_Eqns_0__Lean_Meta_getEqnsFor_x3fCore_spec__0___redArg + 516
25  libleanshared.dylib                 0x0000000109aae604 l___private_Lean_Meta_Eqns_0__Lean_Meta_getEqnsFor_x3fCore___lam__0 + 1204
26  libleanshared.dylib                 0x000000010cd9de60 lean_apply_5 + 3012
27  libleanshared.dylib                 0x0000000109989b8c l_Lean_Meta_withLCtx___at_____private_Lean_Meta_Basic_0__Lean_Meta_mkLevelErrorMessageCore_spec__2___redArg + 16
28  libleanshared.dylib                 0x0000000109aaf920 l_Lean_Meta_getEqnsFor_x3f___lam__0___boxed + 24
29  libleanshared.dylib                 0x000000010cd9d344 lean_apply_5 + 168
30  libleanshared.dylib                 0x0000000109989b8c l_Lean_Meta_withLCtx___at_____private_Lean_Meta_Basic_0__Lean_Meta_mkLevelErrorMessageCore_spec__2___redArg + 16
31  libleanshared.dylib                 0x0000000108681d64 l_Lean_Meta_mkSimpEntryOfDeclToUnfold + 2464
32  libleanshared.dylib                 0x000000010a9d10a8 l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabDeclToUnfoldOrTheorem + 2924
33  libleanshared.dylib                 0x000000010a9d9458 l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArg + 6420
34  libleanshared.dylib                 0x000000010a9deca0 l_Array_forIn_x27Unsafe_loop___at___Lean_Elab_Tactic_elabSimpArgs_spec__3 + 752
35  libleanshared.dylib                 0x000000010a9eab88 l_Lean_Elab_Tactic_elabSimpArgs___lam__0 + 280
36  libleanshared.dylib                 0x000000010a9ecf2c l_Lean_Elab_Tactic_elabSimpArgs___lam__0___boxed + 352
37  libleanshared.dylib                 0x000000010cda2c4c lean_apply_9 + 1868
38  libleanshared.dylib                 0x000000010a9e7320 l_Lean_Meta_withTrackingZetaDeltaSet___at___Lean_Elab_Tactic_elabSimpArgs_spec__6___redArg + 1276
39  libleanshared.dylib                 0x000000010a9ed69c l_Lean_Elab_Tactic_elabSimpArgs___lam__1___boxed + 256
40  libleanshared.dylib                 0x000000010cda2c4c lean_apply_9 + 1868
41  libleanshared.dylib                 0x000000010cd9d740 lean_apply_5 + 1188
42  libleanshared.dylib                 0x000000010a3b97f8 l_Lean_MVarId_withContext___at___Lean_Elab_Tactic_withMainContext_spec__0___redArg + 148
43  libleanshared.dylib                 0x000000010a3b9b5c l_Lean_Elab_Tactic_withMainContext___redArg + 576
44  libleanshared.dylib                 0x000000010cd9ff84 lean_apply_7 + 204
45  libleanshared.dylib                 0x000000010a9efe8c l_Lean_Elab_Tactic_mkSimpContext___lam__0 + 2212
46  libleanshared.dylib                 0x000000010a9f07d4 l_Lean_Elab_Tactic_mkSimpContext + 180
47  libleanshared.dylib                 0x000000010aa0ac98 l_Lean_Elab_Tactic_evalSimp___lam__0 + 316
48  libleanshared.dylib                 0x000000010cda2878 lean_apply_9 + 888
49  libleanshared.dylib                 0x000000010aa08824 l_Lean_Elab_Tactic_withSimpDiagnostics + 152
50  libleanshared.dylib                 0x000000010cda2584 lean_apply_9 + 132
51  libleanshared.dylib                 0x000000010cd9d740 lean_apply_5 + 1188
52  libleanshared.dylib                 0x000000010a3b97f8 l_Lean_MVarId_withContext___at___Lean_Elab_Tactic_withMainContext_spec__0___redArg + 148
53  libleanshared.dylib                 0x000000010a3b9b5c l_Lean_Elab_Tactic_withMainContext___redArg + 576
54  libleanshared.dylib                 0x000000010cda2584 lean_apply_9 + 132
55  libleanshared.dylib                 0x000000010a38b8d0 l_Lean_Elab_withInfoTreeContext___at___Lean_Elab_Tactic_evalTactic_eval_spec__5___redArg + 572
56  libleanshared.dylib                 0x000000010cda2990 lean_apply_9 + 1168
57  libleanshared.dylib                 0x000000010a38d3ec l_Lean_Elab_Tactic_evalTactic_eval + 996
58  libleanshared.dylib                 0x000000010a39cbc8 l_Lean_Elab_Tactic_evalTactic___lam__1 + 1104
59  libleanshared.dylib                 0x000000010cda2584 lean_apply_9 + 132
60  libleanshared.dylib                 0x000000010a39d938 l_Lean_Elab_Tactic_evalTactic___lam__4 + 1280
61  libleanshared.dylib                 0x000000010cd9afe4 lean_apply_3 + 3880
62  libleanshared.dylib                 0x000000010cd975bc lean_apply_1 + 4380
63  libleanshared.dylib                 0x0000000107fe3f5c l_Lean_profileitIOUnsafe___redArg___lam__0 + 20
64  libleanshared.dylib                 0x000000010cd971b0 lean_apply_1 + 3344
65  libleanshared.dylib                 0x00000001075692f0 l_unsafeBaseIO___redArg + 20
66  libleanshared.dylib                 0x0000000107fe4374 l_Lean_profileitIOUnsafe___redArg___lam__1___boxed + 24
67  libleanshared.dylib                 0x000000010cd971b0 lean_apply_1 + 3344
68  libleanshared.dylib                 0x000000010ccf06ac lean_profileit + 128
69  libleanshared.dylib                 0x0000000107fe4248 l_Lean_profileitIOUnsafe___redArg + 168
70  libleanshared.dylib                 0x000000010a39536c l_Lean_Elab_Tactic_evalTactic + 776
71  libleanshared.dylib                 0x000000010a396d78 l_Lean_Elab_Tactic_evalTactic_expandEval___lam__3___boxed + 52
72  libleanshared.dylib                 0x000000010cda2ea8 lean_apply_9 + 2472
73  libleanshared.dylib                 0x000000010a38b8d0 l_Lean_Elab_withInfoTreeContext___at___Lean_Elab_Tactic_evalTactic_eval_spec__5___redArg + 572
74  libleanshared.dylib                 0x000000010a395994 l_Lean_Elab_Tactic_evalTactic_expandEval + 1180
75  libleanshared.dylib                 0x000000010a39cbc8 l_Lean_Elab_Tactic_evalTactic___lam__1 + 1104
76  libleanshared.dylib                 0x000000010cda2584 lean_apply_9 + 132
77  libleanshared.dylib                 0x000000010a39d938 l_Lean_Elab_Tactic_evalTactic___lam__4 + 1280
78  libleanshared.dylib                 0x000000010cd9afe4 lean_apply_3 + 3880
79  libleanshared.dylib                 0x000000010cd975bc lean_apply_1 + 4380
80  libleanshared.dylib                 0x0000000107fe3f5c l_Lean_profileitIOUnsafe___redArg___lam__0 + 20
81  libleanshared.dylib                 0x000000010cd971b0 lean_apply_1 + 3344
82  libleanshared.dylib                 0x00000001075692f0 l_unsafeBaseIO___redArg + 20
83  libleanshared.dylib                 0x0000000107fe4374 l_Lean_profileitIOUnsafe___redArg___lam__1___boxed + 24
84  libleanshared.dylib                 0x000000010cd971b0 lean_apply_1 + 3344
85  libleanshared.dylib                 0x000000010ccf06ac lean_profileit + 128
86  libleanshared.dylib                 0x0000000107fe4248 l_Lean_profileitIOUnsafe___redArg + 168
87  libleanshared.dylib                 0x000000010a39536c l_Lean_Elab_Tactic_evalTactic + 776
88  libleanshared.dylib                 0x000000010a2ac8b4 l_Lean_Elab_Tactic_evalSepTactics_goEven___lam__5 + 628
89  libleanshared.dylib                 0x000000010a2b0af0 l_Lean_Elab_Tactic_evalSepTactics_goEven___lam__5___boxed + 128
90  libleanshared.dylib                 0x000000010cda2c4c lean_apply_9 + 1868
91  libleanshared.dylib                 0x000000010bcead84 l_Lean_Elab_Term_withNarrowedTacticReuse___at___Lean_Elab_Term_withNarrowedArgTacticReuse___at___Lean_Elab_Term_runTactic_spec__2_spec__2___redArg___lam__0___boxed + 144
92  libleanshared.dylib                 0x000000010cda3958 lean_apply_10 + 1040
93  libleanshared.dylib                 0x000000010cda2e00 lean_apply_9 + 2304
94  libleanshared.dylib                 0x000000010a2b039c l_Lean_Elab_Tactic_evalSepTactics_goEven + 1160
95  libleanshared.dylib                 0x000000010cda2584 lean_apply_9 + 132
96  libleanshared.dylib                 0x000000010bcead84 l_Lean_Elab_Term_withNarrowedTacticReuse___at___Lean_Elab_Term_withNarrowedArgTacticReuse___at___Lean_Elab_Term_runTactic_spec__2_spec__2___redArg___lam__0___boxed + 144
97  libleanshared.dylib                 0x000000010cda3958 lean_apply_10 + 1040
98  libleanshared.dylib                 0x000000010cda2e00 lean_apply_9 + 2304
99  libleanshared.dylib                 0x000000010a2b1168 l_Lean_Elab_Tactic_evalTacticSeq1Indented + 156
bash: line 1: 94560 Abort trap: 6           /Users/paul/code/lean4/build/release/stage0/bin/lean $LEAN_OPTS -o "../build/release/stage1/lib/lean/Init/Grind/Ring/Poly.olean" -i "../build/release/stage1/lib/lean/Init/Grind/Ring/Poly.ilean" --c="../build/release/stage1/lib/temp/Init/Grind/Ring/Poly.c.tmp" "Init/Grind/Ring/Poly.lean"
make[7]: *** [../build/release/stage1/lib/lean/Init/Grind/Ring/Poly.olean] Error 134

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Check out the branch from PR #9126 and run make to reproduce the panic in Init.Data.Grind.Poly. Read the TODO and import context in Init.Data.Vector.Basic, then trace the failure around the reported Lean.MapDeclarationExtension.insert assertion. Done means the build succeeds with the private import and no panic.