feat: breadcrumb path for assert_not_exists (#10940)

As [requested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/assert_not_exists/near/423181469).



Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>

Mathlib/Util/AssertExists.lean

@@ -28,7 +28,8 @@ in the current import scope.
 Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).
 -/
 elab "assert_exists " n:ident : command => do
-  -- this throw an error if the user types something ambiguous or doesn't exist, otherwise succeed
+  -- this throws an error if the user types something ambiguous or
+  -- something that doesn't exist, otherwise succeeds
   let _ ← resolveGlobalConstNoOverloadWithInfo n
 
 /--
@@ -47,9 +48,21 @@ In this case, you should refactor your work
 (for example by creating new files rather than adding imports to existing files).
 You should *not* delete the `assert_not_exists` statement without careful discussion ahead of time.
 -/
-elab "assert_not_exists " n:ident : command =>
-  do let [] ← try resolveGlobalConstWithInfos n catch _ => return
-      | throw <| .error n m!"Declaration {n} is not allowed to be imported by this file.\n\n\
-          These invariants are maintained by `assert_not_exists` statements, \
-          and exist in order to ensure that \"complicated\" parts of the library \
-          are not accidentally introduced as dependencies of \"simple\" parts of the library."
+elab "assert_not_exists " n:ident : command => do
+  let decl ← try resolveGlobalConstNoOverloadWithInfo n catch _ => return
+  let env ← getEnv
+  let c ← mkConstWithLevelParams decl
+  let msg ← (do
+    let mut some idx := env.getModuleIdxFor? decl
+      | pure m!"Declaration {c} is defined in this file."
+    let mut msg := m!"Declaration {c} is not allowed to be imported by this file.\n\
+      It is defined in {env.header.moduleNames[idx.toNat]!},"
+    for i in [idx.toNat+1:env.header.moduleData.size] do
+      if env.header.moduleData[i]!.imports.any (·.module == env.header.moduleNames[idx.toNat]!) then
+        idx := i
+        msg := msg ++ m!"\n  which is imported by {env.header.moduleNames[i]!},"
+    pure <| msg ++ m!"\n  which is imported by this file.")
+  throw <| .error n m!"{msg}\n\n\
+    These invariants are maintained by `assert_not_exists` statements, \
+    and exist in order to ensure that \"complicated\" parts of the library \
+    are not accidentally introduced as dependencies of \"simple\" parts of the library."