diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 08a470ce2b..de3aa18522 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -48,7 +48,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let parentName? ← getDeclName?
-      let declName := parentName?.getD Name.anonymous ++ shortDeclName
+      let mut declName := parentName?.getD Name.anonymous ++ shortDeclName
+      let env ← getEnv
+      if env.header.isModule && !env.isExporting then
+        declName := mkPrivateName env declName
       if decls.any fun decl => decl.declName == declName then
         withRef declId do
           throwError "`{.ofConstName declName}` has already been declared"
@@ -116,15 +119,12 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
   let toLift ← views.mapIdxM fun i view => do
     let value := values[i]!
     let termination := view.termination.rememberExtraParams view.binderIds.size value
-    let env ← getEnv
     pure {
       ref            := view.ref
       fvarId         := fvars[i]!.fvarId!
       attrs          := view.attrs
       shortDeclName  := view.shortDeclName
-      declName       :=
-        if env.isExporting || !env.header.isModule then view.declName
-        else mkPrivateName env view.declName
+      declName       := view.declName
       parentName?    := view.parentName?
       lctx
       localInstances
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..810cb1ac9e 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,6 @@
 #include "util/options.h"
 
+// Please update
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/interactive/incomingCallHierarchyWhere.lean b/tests/lean/interactive/incomingCallHierarchyWhere.lean
new file mode 100644
index 0000000000..0d16412a3e
--- /dev/null
+++ b/tests/lean/interactive/incomingCallHierarchyWhere.lean
@@ -0,0 +1,17 @@
+--^ waitForILeans
+module
+
+-- Regression test for a bug where the module system broke the call hierarchy when tracking it
+-- through a `where` in a `public def` of a `module`.
+
+public section
+
+def f := 0
+   --^ incomingCallHierarchy
+
+def foo : Nat :=
+  bar
+where
+  bar : Nat := f
+
+def foobar := foo
diff --git a/tests/lean/interactive/incomingCallHierarchyWhere.lean.expected.out b/tests/lean/interactive/incomingCallHierarchyWhere.lean.expected.out
new file mode 100644
index 0000000000..358b6a185a
--- /dev/null
+++ b/tests/lean/interactive/incomingCallHierarchyWhere.lean.expected.out
@@ -0,0 +1,65 @@
+[{"item":
+  {"uri": "file:///incomingCallHierarchyWhere.lean",
+   "selectionRange":
+   {"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
+   "range":
+   {"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
+   "name": "f",
+   "kind": 14,
+   "data":
+   {"name": "f",
+    "module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
+  "fromRanges": [],
+  "children":
+  [{"item":
+    {"uri": "file:///incomingCallHierarchyWhere.lean",
+     "selectionRange":
+     {"start": {"line": 14, "character": 2},
+      "end": {"line": 14, "character": 5}},
+     "range":
+     {"start": {"line": 14, "character": 2},
+      "end": {"line": 14, "character": 16}},
+     "name": "foo.bar",
+     "kind": 14,
+     "data":
+     {"name":
+      "_private.«external:file:///incomingCallHierarchyWhere.lean».0.foo.bar",
+      "module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
+    "fromRanges":
+    [{"start": {"line": 14, "character": 15},
+      "end": {"line": 14, "character": 16}}],
+    "children":
+    [{"item":
+      {"uri": "file:///incomingCallHierarchyWhere.lean",
+       "selectionRange":
+       {"start": {"line": 11, "character": 4},
+        "end": {"line": 11, "character": 7}},
+       "range":
+       {"start": {"line": 11, "character": 0},
+        "end": {"line": 14, "character": 16}},
+       "name": "foo",
+       "kind": 14,
+       "data":
+       {"name": "foo",
+        "module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
+      "fromRanges":
+      [{"start": {"line": 12, "character": 2},
+        "end": {"line": 12, "character": 5}}],
+      "children":
+      [{"item":
+        {"uri": "file:///incomingCallHierarchyWhere.lean",
+         "selectionRange":
+         {"start": {"line": 16, "character": 4},
+          "end": {"line": 16, "character": 10}},
+         "range":
+         {"start": {"line": 16, "character": 0},
+          "end": {"line": 16, "character": 17}},
+         "name": "foobar",
+         "kind": 14,
+         "data":
+         {"name": "foobar",
+          "module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
+        "fromRanges":
+        [{"start": {"line": 16, "character": 14},
+          "end": {"line": 16, "character": 17}}],
+        "children": []}]}]}]}]
diff --git a/tests/lean/snapshotTree.lean.expected.out b/tests/lean/snapshotTree.lean.expected.out
index ae3e9c54bd..6da83e28ea 100644
--- a/tests/lean/snapshotTree.lean.expected.out
+++ b/tests/lean/snapshotTree.lean.expected.out
@@ -1,78 +1,78 @@
-[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range> 
   [Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
   [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited> 
-[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range> 
   [Elab.snapshotTree] Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩ 
     [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩ 
       [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩ 
         [Elab.snapshotTree] ⟨15, 2⟩-⟨15, 9⟩ 
           [Elab.snapshotTree] <range inherited> 
-        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+        [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
         [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩ 
           [Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩ 
             [Elab.snapshotTree] <range inherited> 
-          [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+          [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
           [Elab.snapshotTree] Lean.cdot⟨17, 2⟩-⟨24, 13⟩ 
             [Elab.snapshotTree] Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩ 
-              [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩ 
-                [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+              [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩ 
+                [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range> 
                 [Elab.snapshotTree] Lean.Parser.Tactic.induction<range inherited> 
                   [Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩ 
                     [Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range> 
                     [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩ 
                       [Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩ 
                         [Elab.snapshotTree] <range inherited> 
-                      [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                      [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
                       [Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩ 
-                        [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩ 
-                          [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+                        [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩ 
+                          [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range> 
                           [Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited> 
                             [Elab.snapshotTree] <range inherited> 
                               [Elab.snapshotTree] <range inherited> 
                             [Elab.snapshotTree] <no range> 
                             [Elab.snapshotTree] <range inherited> 
                               [Elab.snapshotTree] <range inherited> 
-                        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                        [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
                         [Elab.snapshotTree] <no range> 
                           [Elab.snapshotTree] <range inherited> 
                     [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩ 
                       [Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩ 
                         [Elab.snapshotTree] <range inherited> 
-                      [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                      [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
                       [Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩ 
-                        [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩ 
-                          [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+                        [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩ 
+                          [Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range> 
                           [Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited> 
                             [Elab.snapshotTree] <range inherited> 
                               [Elab.snapshotTree] <range inherited> 
                             [Elab.snapshotTree] <no range> 
                             [Elab.snapshotTree] <range inherited> 
                               [Elab.snapshotTree] <range inherited> 
-                        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                        [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
                         [Elab.snapshotTree] <no range> 
                           [Elab.snapshotTree] <range inherited> 
-                  [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                  [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
                   [Elab.snapshotTree] <no range> 
                     [Elab.snapshotTree] <range inherited> 
-              [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+              [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
               [Elab.snapshotTree] <no range> 
                 [Elab.snapshotTree] <range inherited> 
-            [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+            [Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
             [Elab.snapshotTree] <no range> 
               [Elab.snapshotTree] <range inherited> 
       [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
   [Elab.snapshotTree] <no range> 
   [Elab.snapshotTree] <no range> 
   [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range> 
       • Goals accomplished!
       
   [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited> 
-[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range> 
   [Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
-  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
+  [Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
   [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>