From 82401938cfe99f4a12195aa18a076b27399e20ae Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 21 May 2024 12:34:58 +0200 Subject: [PATCH] fix: hovers on binders with metavariables (#4192) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit this fixes #4078. It is an alternative fix to the one in #4137, suggested by @kmill. Incidentially, it makes the unused variable linter better. My theory is that if we don’t reset the info when backtracking, the binder shows up more than once in the info tree, and then it is considered “used”, although there are just multiple binders. --- src/Lean/Elab/Term.lean | 2 +- .../1018unknowMVarIssue.lean.expected.out | 4 -- tests/lean/interactive/4078.lean | 17 ++++++++ tests/lean/interactive/4078.lean.expected.out | 42 +++++++++++++++++++ 4 files changed, 60 insertions(+), 5 deletions(-) create mode 100644 tests/lean/interactive/4078.lean create mode 100644 tests/lean/interactive/4078.lean.expected.out 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"}}