diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index f508f9785b..358b5aa740 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1531,7 +1531,7 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
           | ex => match isAutoBoundImplicitLocalException? ex with
             | some n =>
               -- Restore state, declare `n`, and try again
-              s.restore
+              s.restore (restoreInfo := true)
               withLocalDecl n .implicit (← mkFreshTypeMVar) fun x =>
                 withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
                   loop (← saveState)
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 679735d30a..3fe4323d45 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -9,10 +9,6 @@ x : Fam2 α✝ β
 a : α
 ⊢ α
 [Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
-      • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-        • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-        • α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-      • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
       • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
         • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
         • α : Type @ ⟨7, 13⟩-⟨7, 14⟩
diff --git a/tests/lean/interactive/4078.lean b/tests/lean/interactive/4078.lean
new file mode 100644
index 0000000000..771b72ac57
--- /dev/null
+++ b/tests/lean/interactive/4078.lean
@@ -0,0 +1,17 @@
+def foo1 {β} (i : ∀ α, List α) : List β := i β
+                  --^ textDocument/hover
+
+def foo2 (i : ∀ α, List α) : List β := i β
+              --^ textDocument/hover
+
+def foo3 (i : (α : _) → List α) : List β := i β
+              --^ textDocument/hover
+
+def foo4 (i : (α : id _) → List α) : List β := i β
+              --^ textDocument/hover
+
+def foo5 (i : (α : Type _) → List α) : List β := i β
+              --^ textDocument/hover
+
+def foo6 (i : (α : Type 0) → List α) : List β := i β
+              --^ textDocument/hover
diff --git a/tests/lean/interactive/4078.lean.expected.out b/tests/lean/interactive/4078.lean.expected.out
new file mode 100644
index 0000000000..e810dad41d
--- /dev/null
+++ b/tests/lean/interactive/4078.lean.expected.out
@@ -0,0 +1,42 @@
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 0, "character": 20}}
+{"range":
+ {"start": {"line": 0, "character": 20}, "end": {"line": 0, "character": 21}},
+ "contents": {"value": "```lean\nα : Type u_1\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 3, "character": 16}}
+{"range":
+ {"start": {"line": 3, "character": 16}, "end": {"line": 3, "character": 17}},
+ "contents": {"value": "```lean\nα : Type u_1\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 6, "character": 16}}
+{"range":
+ {"start": {"line": 6, "character": 14}, "end": {"line": 6, "character": 30}},
+ "contents":
+ {"value":
+  "```lean\nType (u_1 + 1)\n```\n***\nThe dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually\nreserve the latter for propositions. Also written as `Π x : α, β` (the \"Pi-type\")\nin the literature. ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 9, "character": 16}}
+{"range":
+ {"start": {"line": 9, "character": 14}, "end": {"line": 9, "character": 33}},
+ "contents":
+ {"value":
+  "```lean\nType (u_1 + 1)\n```\n***\nThe dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually\nreserve the latter for propositions. Also written as `Π x : α, β` (the \"Pi-type\")\nin the literature. ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 12, "character": 16}}
+{"range":
+ {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 35}},
+ "contents":
+ {"value":
+  "```lean\nType (u_1 + 1)\n```\n***\nThe dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually\nreserve the latter for propositions. Also written as `Π x : α, β` (the \"Pi-type\")\nin the literature. ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///4078.lean"},
+ "position": {"line": 15, "character": 16}}
+{"range":
+ {"start": {"line": 15, "character": 14}, "end": {"line": 15, "character": 35}},
+ "contents":
+ {"value":
+  "```lean\nType 1\n```\n***\nThe dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually\nreserve the latter for propositions. Also written as `Π x : α, β` (the \"Pi-type\")\nin the literature. ",
+  "kind": "markdown"}}