diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index fdc4a57f45..23ece3a5b0 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -183,7 +183,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
         -- for binders, hide the last hypothesis (the binder itself)
         let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
         let goal ← ci.runMetaM lctx' do
-          Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
+          Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
         let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
         return some { goal with range }
       else
diff --git a/tests/lean/interactive/expectedTypeAsGoal.lean b/tests/lean/interactive/expectedTypeAsGoal.lean
new file mode 100644
index 0000000000..78f2237537
--- /dev/null
+++ b/tests/lean/interactive/expectedTypeAsGoal.lean
@@ -0,0 +1,9 @@
+def big : IO Unit := do
+  let x := 10
+  if true then
+    IO.println s!"a{x}"
+   --^ $/lean/plainTermGoal
+  if false then
+    IO.println "b"
+  if 1 < 3 then
+    IO.println "c"
diff --git a/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out
new file mode 100644
index 0000000000..1c6ad9bbf7
--- /dev/null
+++ b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out
@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file://expectedTypeAsGoal.lean"},
+ "position": {"line": 3, "character": 5}}
+{"range":
+ {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 23}},
+ "goal": "x : Nat := 10\n⊢ IO Unit"}