Unifying MVars with newly created FVars

Stream: metaprogramming / tactics

[Tate Rowney]

Good evening! I'm trying to unify some metavariables with expressions containing fvars that were created after the metavariables were (for the purpose of making a lambda expression). Specifically, I'm running into the error created by the second example below:

def ok : MetaM Expr := do
  withLocalDecl `x default q(Nat) fun binderExpr => do
    let m ← mkFreshExprMVar none

    unless ← isDefEq m binderExpr do throwError m!"Couldn't unify :("
    mkLambdaFVars #[binderExpr] m
#eval ok -- works fine

def bad : MetaM Expr := do
  let m ← mkFreshExprMVar none
  withLocalDecl `x default q(Nat) fun binderExpr => do

    unless ← isDefEq m binderExpr do throwError m!"Couldn't unify :("
    mkLambdaFVars #[binderExpr] m
#eval bad -- throws an error (want this to work)

isDefEq appears to dislike this, apparently because the MVarDecl associated with m carries a LocalContext that doesn't have the FVar binderExpr in it. I did notice one could get around this by simply modifying the MVar directly (like let updatedLCtx ← getLCtx; setMCtx <| (← getMCtx).modifyExprMVarLCtx m.mvarId! (fun _ => updatedLCtx)), which seemed to work well empirically; however, I couldn't help but notice the ominous warning on modifyExprMVarLCtx about requiring any modification to be "legal".

My question: is such a modification to existing MVars a safe thing to do? (even considering that everything is turned into bvars right afterwards by mkLambdaFVars?) And is there a more intelligent way to go about this?

I greatly appreciate y'all's help!

[Leni Aniva]

It doesn't make sense for this to succeed. Otherwise you can prove anything

?m1
|- False

Suppose we have (this is very easy to produce)

?m2
x : False
|- False

and if the unification succeeded it could assign ?m1 to x and prove False.

However, if you have a way to produce something that has the same type as x in ?m1's context, you can assign (mkLambdaFVars #[binderExpr] m2).beta #[arg] to m.

[Tate Rowney]

This is very helpful, thank you! I see now how my strategy could be problematic absent other invariants.

I unfortunately don't have many guarentees on information about the types, etc. of ?m1. However, perhaps some other reduction wizardry could help, I will keep searching...

[Sebastian Graf]

I don't think you can generate any unsoundness by extending the local context of an MVar after it has been created. After all, meta variables are an elaboration time concept and the kernel does reject any program with a meta variable.

However, extending the context of the meta variable can potentially lead to dangling free vars if the metavariable has been used in expressions where the added fvar is not in scope. This is no different to forgetting to do an, e.g. mkLambdaFVars. If you have control of all the use sites of the metavariable, I don't think it's problematic to extend its local context. It's just questionable why you haven't created the metavariable in the extended context in the first place. Also be sure that the new local context is actually strictly an extension of the old context. (No clear has happened.)

[Tate Rowney]

Thanks! It seems that both the issues above might be remediated if the mvar in question can only have its local context extended if it appears solely within the body of the function, so that the fvar will never be dangling. Is this sufficient to ensure that this modification won't cause problems?

(The reason I am in this situation is because I am taking Exprs elaborated in many different contexts, abstracting their metavariables, and putting them all in a single context using abstractMVars, which creates all the new mvars at once. Another workaround could involve modifying that API to wait to declare some mvars, but this seems like it would introduce its own set of headaches).

[Sebastian Graf]

I'm not sure I'm following. If you already have Exprs es that contain metavariables, then the metavariables live in the same local context as es. abstractMVars shouldn't change that. So I'm not sure which free variables you are referring to; perhaps you are referring to bound variables in the specific es?

On the other hand, you are saying

I am taking Exprs elaborated in many different contexts, [...] and putting them all in a single context

and that doesn't sound well-defined to me. What if one Expr refers to an FVar that is not defined in another context? Are you by chance doing mkForallFVars? Either way, doing isDefEq ?m e in the original context of the expression from whence the metavariable came should assign the metavariable.

[Tate Rowney]

As with the example above, I'm taking let/forall/lambda expressions and creating a withLocalDecl at each one after mvars are created, changing the localContext (so that expressions from other contexts with the same fvar names will be changed to bvars as appropriate). I don't doubt there are situations in which this is undefined; in fact I make a point of type-checking everything afterwards to provide a message to the user if the expressions they input act in this way. I'm unsure that using the original mvar context would work, as I hope that e will eventually consist of a more complex expression, potentially including mvars of its own from a different context.

Applications aside, I'm still curious if a modification to the MCtx as described above is legal if the mvar in question isn't used outside the withLocalDecl? Thanks!

[Aaron Liu]

Can you maybe abstract the mvars and make new ones in the new local context?

[Tate Rowney]

Wait this is a really interesting idea. I’d assume that if the mvar is used elsewhere in a bad place it’ll just become decoupled/not the same mvar anymore, which I think I’d be fine with… I’ll experiment with this when I get a chance, thanks Aaron!

[Sebastian Graf]

If you create ?m : Nat and want it to scope over a local x : Nat introduced later on, you could do a "reverse mkForallFVars #[x]" (intro?) and create ?m instead as ?m : Nat -> Nat, then use ?m x as "the MVar".

import Lean
import Qq

open Lean Meta Qq

def ok : MetaM Expr := do
  withLocalDecl `x default q(Nat) fun binderExpr => do
    let m ← mkFreshExprMVar none

    unless ← isDefEq m binderExpr do throwError m!"Couldn't unify :("
    mkLambdaFVars #[binderExpr] m
#eval ok -- works fine

def bad : MetaM Expr := do
  let m ← mkFreshExprMVar none
  withLocalDecl `x default q(Nat) fun binderExpr => do

    unless ← isDefEq m binderExpr do throwError m!"Couldn't unify :("
    mkLambdaFVars #[binderExpr] m
#eval bad -- throws an error (want this to work)

def better : MetaM Expr := do
  let m ← mkFreshExprMVar q(Nat → Nat)
  withLocalDecl `x default q(Nat) fun binderExpr => do
    let m := mkApp m binderExpr -- "intro x"
    unless ← isDefEq m binderExpr do throwError m!"Couldn't unify :("
    mkLambdaFVars #[binderExpr] m
#eval better -- throws an error (want this to work)