fix: process delayed assignment metavariables correctly in Lean.Meta.Closure
#6414
Conversation
…Closure This PR fixes a bug in `Lean.Meta.Closure` that would introduce under-applied delayed assignment metavariables, which would keep them from ever getting instantiated. This bug affected `match` elaboration when the expected type contains postponed elaboration problems, for example tactic blocks. Closes leanprover#6354
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
builds-mathlib
| if let some { fvars, .. } ← getDelayedMVarAssignment? mvarId then | ||
| -- Eta expand `e` for the requisite number of arguments. | ||
| forallBoundedTelescope mvarDecl.type fvars.size fun args _ => do | ||
| mkLambdaFVars args <| mkAppN e args |
There was a problem hiding this comment.
Have you considered other solutions that do not require eta-expansion for this issue, even if they apply only to special cases? If they are not worth pursuing, we should document that here.
There was a problem hiding this comment.
I couldn't think of any other solution @leodemoura, other than to relax the assumption on delayed assignment metavariables and have instantiateMVars itself do the eta expansion. This results in the same expression in the end, and it seems better to me to keep instantiateMVars simple.
It did cross my mind that I could try matching on the case where the delayed assignment metavariable is applied to fvars, but it wasn't clear to me that the added code complexity would be worth it. We would still need the eta expansion code path for correctness.
In another PR, I'm going to try to fix one of the main triggers of this bug, which comes from structure instance notation when there are autoParams and a structure that extends another structure. This won't eradicate the bug however.
There was a problem hiding this comment.
It did cross my mind that I could try matching on the case where the delayed assignment metavariable is applied to fvars, but it wasn't clear to me that the added code complexity would be worth it. We would still need the eta expansion code path for correctness.
Let's add an extra comment documenting this decision.
This PR fixes a bug in
Lean.Meta.Closurethat would introduce under-applied delayed assignment metavariables, which would keep them from ever getting instantiated. This bug affectedmatchelaboration when the expected type contained postponed elaboration problems, for example tactic blocks.Closes #5925, closes #6354