Catching mvars in `MVarId.apply`

Stream: lean4 dev

[Leni Aniva]

I think the MVarId catching logic in MVarId.apply should get mvars from the actual expression assignment to the current goal:

    let otherMVarIds ← getMVarsNoDelayed (mkAppN e newMVars)

as opposed to

    let otherMVarIds ← getMVarsNoDelayed e

This is because the isDefEqApply in the go loop could potentially delay assign some mvars in newMVars, in which case the value of the delayed assignment would be lost since otherMVarIds only contain mvars from e.

I found a corner case in my project that suffers from this issue, but I don't know how to reliably reproduce this case.

[Leni Aniva]

Specifically when ctxApprox is true, isExprDefEq can cause mvars in newMVars to be assigned to another (unassigned) mvar with a smaller context, so there should be a way to catch them.

e.g.

    let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned

Instead of this, we could have

  let newMVars ← newMVars.filterMapM fun mvar => do
    match ← getExprMVarAssignment? mvar with
    | .none => pure $ .some mvar
    | .some (.mvar inner) => pure $ .some inner
    | .some _ => pure .none

which will ensure ctxApprox'd mvars are accounted for.

[Leni Aniva]

I don't know how to reliably trigger ctxApprox. Otherwise I can write a MWE that showcases when .apply loses track of a mvar.