fix: hovers on binders with metavariables #4137
Conversation
|
Mostly as a learning experience, I wanted to be see if I can fix a bug this part of the code based. I wonder if this is really the right fix, because I don’t see much |
github-actions
bot
added
the
toolchain-available
| @@ -211,8 +211,9 @@ private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Ar | |||
| let id := binderView.id.getId | |||
| let kind := kindOfBinderName id | |||
| withLocalDecl id binderView.bi type (kind := kind) fun fvar => do | |||
| addLocalVarInfo binderView.ref fvar | |||
| loop (i+1) (fvars.push (binderView.id, fvar)) | |||
| withSaveInfoContext do | |||
There was a problem hiding this comment.
I don't know this part of the code base very well (in particular, when withSaveInfoContext is needed), but it seems to me that the error actually has something to do with autoimplicits. Over in Lean.Elab.Term.withAutoBoundImplicit when the new autoimplicit is declared, the state is restored, but there's nothing recording the new state in the info trees. Maybe withSaveInfoContext should go there instead?
One piece of evidence for this is that there's no error when hovering over α when autoImplicits isn't activated:
def oops {β} (i : ∀ α, List α) : List β := i βThere was a problem hiding this comment.
Good catch, let’s try.
(Unrelatedly, but given that backtracking implementation of auto bound implicit, I wonder how easily that can increase elaboration time significantly.)
There was a problem hiding this comment.
Nope,
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index ee1014f944..476d807dda 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1533,7 +1533,8 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
s.restore
withLocalDecl n .implicit (← mkFreshTypeMVar) fun x =>
withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
- loop (← saveState)
+ withSaveInfoContext do
+ loop (← saveState)
| none => throw ex
loop (← saveState)
elsedoes not help.
There was a problem hiding this comment.
It seems to be that there's stale info because s.restore doesn't restore infotrees. Assuming we want full backtracking, then maybe this is the solution?
partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
let flag := autoImplicit.get (← getOptions)
if flag then
withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) do
let rec loop (s : SavedState) : TermElabM α := withIncRecDepth do
checkSystem "auto-implicit"
try
withSaveInfoContext k
catch
| ex => match isAutoBoundImplicitLocalException? ex with
| some n =>
-- Restore state, declare `n`, and try again
s.restore (restoreInfo := true)
withLocalDecl n .implicit (← mkFreshTypeMVar) fun x =>
withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
loop (← saveState)
| none => throw ex
loop (← saveState)
else
k
There was a problem hiding this comment.
In further testing, doing s.restore (restoreInfo := true) is enough and withSaveInfoContext isn't necessary.
There was a problem hiding this comment.
Feel free to push here and take over, or open a new PR
There was a problem hiding this comment.
Trying that in #4192
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
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.
this fixes #4078