Delayed-assigned mvars footgun

Stream: lean4

[Jannis Limperg]

At some point in Aesop I need to determine whether a partially completed proof e : Expr is sorry-free:

e.hasSorry

Of course I recognise Lean's biggest footgun, so I write instead:

(<- instantiateMVars e).hasSorry

But in fact this is incorrect as well: if e contains a delayed-assigned mvar ?m, then ?m is not instantiated by instantiateMVars but its assignment may still contain sorry. So the (probably) correct version is something like this:

partial def hasSorry (e : Expr) : MetaM Bool :=
  (·.isSome) <$> e.findM? λ
    | .mvar mvarId => do
      if let some ass ← getDelayedMVarAssignment? mvarId then
        hasSorry $ .mvar ass.mvarIdPending
      else if let some ass ← getExprMVarAssignment? mvarId then
        hasSorry ass
      else
        return false
    | .const ``sorryAx _ => return true
    | _ => return false

I figured this out when debugging an issue, so this is a real scenario (albeit a rare one because delayed-assigned mvars are rare). I suspect that a lot of core and Mathlib code contains this bug since (<- instantiateMVars e).foldM or (<- instantiateMVars e).findM is a common pattern.

[David Renshaw]

why does instantiateMVars not take into account delayed mvar assignments?

[Kyle Miller]

@David Renshaw It does, but it only substitutes them in once the mvar it's been delayed assigned to itself instantiates to something without any mvars.