Nested Delayed Assigned Metavariable

Stream: metaprogramming / tactics

[Leni Aniva]

Is it possible for the mvarIdPending of a delayed assigned mvar be itself delayed assigned? I looked through the code of instantiateMVars and there does not seem to be any handling of this.

[Leni Aniva]

I ran some fuzzing tests and it seems like this is possible

[Leni Aniva]

Also, it seems like a mvar can be simultaneously assigned and delayed assigned, or delayed assignments could create a cycle, or mvar's eAssignment or dAssignment can change over time.

This happens when there are lots of revert and intro calls

[Leni Aniva]

Is there any guarantee that once a mvar is assigned it would not change? Or maybe this can be enforced at runtime?

[Sebastian Graf]

Is it possible for the mvarIdPending of a delayed assigned mvar be itself delayed assigned?

I think yes; otherwise I don't see the point in functions like getDelayedMVarRoot.

I looked through the code of instantiateMVars and there does not seem to be any handling of this.

Indeed puzzling. Maybe open an issue with a clear reproduction instruction? That is, give meta code that does something like

1. Create a synth opaque MVar ?m in a context where x is in scope
2. Create a synth opaque MVar ?n in a context where x and y are in scope
3. Abstract ?n over y (do mkForallFVars or something linke that); store as e1 (e1 will be of the form ?n' y, where ?n' is delayed assigned to fun y => ?n.)
4. Abstract ?m over x. Store abstraction of ?m as e2 (e2 will be of the form ?m' x, where ?m' is delayed assigned to fun x => ?m.)
5. assign ?m to e1
6. assign some inhabitant to ?n, for example () : Unit or y.
7. instantiate MVars at e2

Then if you don't see a fully ground expression, instantiate MVars did the wrong thing.

Also, it seems like a mvar can be simultaneously assigned and delayed assigned, or delayed assignments could create a cycle, or mvar's eAssignment or dAssignment can change over time.

Regular assignments take precedence over delayed assignments. Also of course there can be cycles when using MVarId.assign directly; it's an unchecked API. Maybe use checkAssign or withAssignableSyntheticOpaque <| isDefEq . ..

Is there any guarantee that once a mvar is assigned it would not change? Or maybe this can be enforced at runtime?

Not if you use assign directly. At least intro checks whether the MVar in question has already been assigned.

[Leni Aniva]

I don't know how I can construct a case where there's m1 delayed assigned to m2 delayed assigned to m3. Maybe something via revert would work? I'll try your test sequence.

In instantiate_mvars.cpp, there is this condition gating the pending of a delayed assigned mvar:

            optional<expr> val = get_assignment(mid_pending);
            if (!val)
                // mid_pending has not been assigned yet.
                return visit_mvar_app_args(e);

so what would happen to nested mvars here? One hypothesis is that a delayed assigned mvar can later get e-assigned.

[Sebastian Graf]

I don't know how I can construct a case where there's m1 delayed assigned to m2 delayed assigned to m3.

I edited my idea above with a few more details. Does that help?

[Leni Aniva]

e1 is not a mvar, so what do you mean by assign ?m to e1?

#eval do
  let sentence ← Elab.Term.elabTerm (← `(term|∀ (x y : Nat), True)) .none
  Meta.forallBoundedTelescope sentence (maxFVars? := .some 1) λ fvars target => do
    let #[x] := fvars | unreachable!
    let mTarget ← Elab.Term.elabTerm (← `(term|Unit)) .none
    let m ← Meta.mkFreshExprSyntheticOpaqueMVar mTarget
    let e2 ← Meta.mkForallFVars #[x] m
    Meta.forallBoundedTelescope target (maxFVars? := .some 1) λ fvars _target' => do
      let #[y] := fvars | unreachable!
      let nTarget ← Elab.Term.elabTerm (← `(term|Unit)) .none
      let n ← Meta.mkFreshExprSyntheticOpaqueMVar nTarget
      let e1 ← Meta.mkForallFVars #[y] n

[Sebastian Graf]

Here's what I had in mind:

import Lean

open Lean Meta

set_option pp.mvars.delayed true
#eval do
  let Nat := Nat.mkType
  let dm ← withLocalDeclD `x Nat fun x => do
    let m ← mkFreshExprSyntheticOpaqueMVar Nat `m
    withLocalDeclD `y Nat fun y => do
      let n ← mkFreshExprSyntheticOpaqueMVar Nat `n
      let dn ← mkLambdaFVars #[y] n
      let dm ← mkLambdaFVars #[x] m
      -- Note that `m!""` does `instantiateMVars` internally and instantiate `n`
      logInfo m!"m: {m}, n: {n}, dm: {dm}, dn: {dn}"
      m.mvarId!.withContext (m.mvarId!.assign (dn.beta #[mkNatLit 0]))
      logInfo m!"m: {m}, n: {n}, dm: {dm}, dn: {dn}"
      n.mvarId!.withContext (n.mvarId!.assign (mkNatLit 42))
      logInfo m!"m: {m}, n: {n}, dm: {dm}, dn: {dn}"
      return dm
  instantiateMVars dm

Note that after the second assignment, we have

?m.3 |-dAss [x]-> ?m |-eAss-> ?m.4 |-dAss [y]-> n |-eAss-> 42

And this would be a chain of delayed assignments if ?m was instantiated to its assignment ?m.4 0. But it isn't, so this is not really a reproducer.

I suppose you could reproduce by using delayedAssign, but that's playing fast and loose with the invariants about delayed assignment. Note that MkBinding.elimMVar (called by abstractM, mkLambdaFVars, etc.) is careful not to introduce a chain of delayed assignments:

        /- If `mvarId` is the lhs of a delayed assignment `?m #[x_1, ... x_n] := ?mvarPending`,
           then `nestedFVars` is `#[x_1, ..., x_n]`.
           In this case, `newMVarId` is also `syntheticOpaque` and we add the delayed assignment delayed assignment
           ```
           ?newMVar #[y_1, ..., y_m, x_1, ... x_n] := ?m
           ```
           where `#[y_1, ..., y_m]` is `toRevert` after `collectForwardDeps`.
        -/
        let (mvarIdPending, nestedFVars) ← match (← getDelayedMVarAssignment? mvarId) with
          | none => pure (mvarId, #[])
          | some { fvars, mvarIdPending } => pure (mvarIdPending, fvars)
        assignDelayedMVar newMVarId (toRevert ++ nestedFVars) mvarIdPending
      return (mkAppN result args, toRevert)

So maybe the correct answer to

Leni Aniva said:

Is it possible for the mvarIdPending of a delayed assigned mvar be itself delayed assigned?

is: existing APIs should not create delayed assignment chains.

[Leni Aniva]

I see, so chains of delayed assigned mvars should be treated as bugs.

[Sebastian Graf]

I cannot answer this, as I haven't written the code. At least it seems that chains of delayed assigned mvars are not completely instantiated by instantiateMVars, but it also has some gotchas wrt. delayed assignments in general.