Calling unification from meta to remove metavariables

Stream: lean4

[Andrés Goens]

I'm trying to build an expr in meta code and I know it's type, but the type has some metavariables at elaboration time that could be figured out through unification (and in fact def has no trouble with that unification). How do I call unification explicitly to get rid of those metavariables? Here's an MWE, maybe that makes more sense:

import Lean
open Lean Elab Command

inductive Foo : Nat → Type
  | mk0 : Foo 0
  | mkn n : Foo n
deriving Repr

def Foo0 := Foo 0
def foo0 := Foo.mk0
#check foo0 -- foo0 : Foo 0
def foo0' := Foo.mkn 0
#check foo0' -- foo0' : Foo 0

syntax (name := ppExprCmd) "#ppExpr" term : command
syntax (name := evalFoo0Cmd) "#evalFoo0" term : command

@[command_elab ppExprCmd]
def ppExprCmdImpl : CommandElab := fun stx => do
  let expr ← liftTermElabM <| Term.elabTerm stx[1] none
  liftTermElabM Elab.Term.synthesizeSyntheticMVarsNoPostponing
  logInfo s!"{repr expr}"
  return ()

@[command_elab evalFoo0Cmd]
unsafe def evalExprCmdImpl : CommandElab := fun stx => do
  let expr ← liftTermElabM <| Term.elabTerm stx[1] none
  liftTermElabM Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let foo0 ← liftTermElabM <| Lean.Meta.evalExpr' (α := Foo 0) `Foo0 expr
  logInfo s!"{repr foo0}"
  return ()

#ppExpr Foo.mkn 0
/-
Lean.Expr.app
  (Lean.Expr.const `Foo.mkn [])
  (Lean.Expr.app
    (Lean.Expr.app
      (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 1999)))
      (Lean.Expr.lit (Lean.Literal.natVal 0)))
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 2000)))
-/
#evalFoo0 Foo.mkn 0
/-
 failed to evaluate expression, it contains metavariables
  Foo.mkn 0
-/

#ppExpr Foo.mk0
/-
Lean.Expr.const `Foo.mk0 []
-/
#evalFoo0 Foo.mk0
/-
unexpected type at evalExpr
  Foo 0
-/

[Andrés Goens]

(I realize I'm probably using evalExpr' wrong here but that's orthogonal to this, I guess)

[Henrik Böving]

I'm definitely not an expert on meta programming but aren't you forgetting to instantiateMVars in your expr to actually make use of the fact that they might have been resolved by synthesizeSyntheticMVarsNoPostponing?

[Henrik Böving]

That said in general the "entrypoint" for unification is isDefEq which can end up assigning meta variables under the hood and then you can make use of that gained knowledge using instantiateMVars

[Andrés Goens]

Henrik Böving said:

I'm definitely not an expert on meta programming but aren't you forgetting to instantiateMVars in your expr to actually make use of the fact that they might have been resolved by synthesizeSyntheticMVarsNoPostponing?

oh, I thought synthesizeSyntheticMVarsNoPostponing would instantiate them. In any case, calling instantiateMVars in that MWE doesn't seem to fix it either

[Henrik Böving]

oh but we are a pure programming language, no function is going to touch your expr unless you pass it as arguments^^

[Andrés Goens]

Henrik Böving said:

oh but we are a pure programming language, no function is going to touch your expr unless you pass it as arguments^^

Huh, I'm confused, I thought in a monad it would (why does synthesizeSyntheticMVarsNoPostponing return Unit otherwise)?

[Henrik Böving]

well functions like that or isDefEq will register the mvar to be resolved in the context yes. But Expr is still just a piece of data that's flowing around somewhere and it has an .mvar constructor that points to some mvar. When you then call instantiateMVars it will traverse your term, looking for such constructors and if it finds them + a resolved entry in the context it will replace them with whatever the mvar was resolved to

[Kyle Miller]

The "metavariable" concept consists of a couple things:

1. the Expr.mvar node in an expression that contains a metavariable ID
2. the table of metavariable declarations in the monad, mapping IDs to Option Expr (the assignments)

"Assignment" is the process of adding entries to the table, and "instantiation" is the process of replacing Expr.mvars with their assigned values in a given expression.

[Andrés Goens]

Hm, isDefEq also doesn't seem to work:

import Lean
open Lean Elab Command

inductive Foo : Nat → Type
  | mk0 : Foo 0
  | mkn n : Foo n
deriving Repr

def Foo0 := Foo 0
def foo0 := Foo.mk0
#check foo0 -- foo0 : Foo 0
def foo0' := Foo.mkn 0
#check foo0' -- foo0 : Foo 0

syntax (name := ppExprCmd) "#ppExpr" term : command
syntax (name := evalFoo0Cmd) "#evalFoo0" term : command

@[command_elab ppExprCmd]
def ppExprCmdImpl : CommandElab := fun stx => do
  let expr ← liftTermElabM <| Term.elabTerm stx[1] none
  liftTermElabM Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← liftTermElabM <| instantiateMVars expr
  liftTermElabM Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let tyExpr ← liftTermElabM <| Meta.inferType expr
  logInfo s!"{repr expr}"
  let _ ← liftTermElabM <| Meta.isDefEq tyExpr (Expr.const `Foo0 [])
  logInfo s!"{repr expr}"
  return ()

#ppExpr Foo.mkn 0
/-
Lean.Expr.app
  (Lean.Expr.const `Foo.mkn [])
  (Lean.Expr.app
    (Lean.Expr.app
      (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 1781)))
      (Lean.Expr.lit (Lean.Literal.natVal 0)))
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 1782)))
MWE.lean:30:0
unknown metavariable '?_uniq.1781'
-/

[Kyle Miller]

Furthermore, a synthetic metavariable also has

3. an entry in the synthetic metavariable table, explaining what the elaborator needs to do to synthesize an assignment.

Elab.Term.synthesizeSyntheticMVarsNoPostponing is a checkpoint for evaluating everything in this table, guaranteeing all the synthetic metavariables have assignments (if there is no overt failure), guaranteeing instantiation will eliminate metavariables

[Andrés Goens]

Kyle Miller said:

The "metavariable" concept consists of a couple things:

1. the Expr.mvar node in an expression that contains a metavariable ID
2. the table of metavariable declarations in the monad, mapping IDs to Option Expr (the assignments)

"Assignment" is the process of adding entries to the table, and "instantiation" is the process of replacing Expr.mvars with their assigned values in a given expression.

I guess then the right order would be

1. unification
2. assigning metavar
3. instantiating metavar?

[Kyle Miller]

For CommandElabM, you have to be careful with your transitions to TermElabM. The liftTermElabM creates a fresh elaborator state. Make sure to stay within it during all of your elaboration activities.

@[command_elab ppExprCmd]
def ppExprCmdImpl : CommandElab := fun stx => liftTermElabM <| do
  let expr ←  Term.elabTerm stx[1] none
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let tyExpr ← Meta.inferType expr
  logInfo s!"{repr expr}"
  let _ ← Meta.isDefEq tyExpr (Expr.const `Foo0 [])
  logInfo s!"{repr expr}"
  return ()

[Andrés Goens]

ahhh, that makes sense! thanks a lot! (that works!)

[Kyle Miller]

Here's how the order probably should go:

@[command_elab ppExprCmd]
def ppExprCmdImpl : CommandElab := fun stx => liftTermElabM <| do
  let expr ← Term.elabTerm stx[1] none
  let _ ← Meta.isDefEq (← Meta.inferType expr) (Expr.const `Foo0 [])
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  let tyExpr ← instantiateMVars (← Meta.inferType expr)
  logInfo s!"{repr expr}"
  logInfo s!"{repr tyExpr}"
  return ()

[Kyle Miller]

This doesn't guarantee there are no metavariables by the way. It just guarantees there are no synthetic metavariables (like instances or coercions)

[Kyle Miller]

You can use expr.hasMVar to check. There are also things you can do like abstract out all the remaining metavariables to make a function, depending on what your goal is.

[Andrés Goens]

Kyle Miller said:

You can use expr.hasMVar to check. There are also things you can do like abstract out all the remaining metavariables to make a function, depending on what your goal is.

Right, but those are in a sense "semantic" metavariables, so I need to deal with them differently I guess. I imagine def does something like that to make a function?

[Kyle Miller]

def just complains, though for universe level metavariables it can turn those into universe level variables.

By the way, here's a nicer way to write the command, using elab_rules:

syntax (name := ppExprCmd) "#ppExpr" term : command

elab_rules : command
  | `(command| #ppExpr $stx) => liftTermElabM <| do
    let expr ← Term.elabTerm stx none
    let _ ← Meta.isDefEq (← Meta.inferType expr) (Expr.const `Foo0 [])
    Elab.Term.synthesizeSyntheticMVarsNoPostponing
    let expr ← instantiateMVars expr
    let tyExpr ← instantiateMVars (← Meta.inferType expr)
    if expr.hasMVar then
      throwErrorAt stx "still has metavariables"
    logInfo s!"{repr expr}"
    logInfo s!"{repr tyExpr}"
    return ()

#ppExpr 1 + (_ : Nat)
-- still has metavariables

[Kyle Miller]

Is there a reason you're using repr? You can write logInfo m!"{expr}" to get a pretty printed output

[Kyle Miller]

Example of abstraction:

syntax (name := ppExprCmd) "#ppExpr" term : command

elab_rules : command
  | `(command| #ppExpr $stx) => liftTermElabM <| do
    let expr ← Term.elabTerm stx none
    let _ ← Meta.isDefEq (← Meta.inferType expr) (Expr.const `Foo0 [])
    Elab.Term.synthesizeSyntheticMVarsNoPostponing
    let expr ← instantiateMVars expr
    let res ← Meta.abstractMVars expr
    logInfo m!"{res.expr} : {← Meta.inferType res.expr}"
    return ()

#ppExpr 1 + (_ : Nat)
-- fun x_0 => 1 + x_0 : Nat → Nat

[Andrés Goens]

Kyle Miller said:

Is there a reason you're using repr? You can write logInfo m!"{expr}" to get a pretty printed output

oh, because the pretty printed output doesn't show that synthetic metavariable!

[Andrés Goens]

so I couldn't see the error without repr

[Andrés Goens]

I guess that makes the name for the command in the MWE a not so ideal choice though :sweat_smile:

[Marcus Rossel]

Andrés Goens said:

Kyle Miller said:
oh, because the pretty printed output doesn't show that synthetic metavariable!

When using the "proper" pretty printing, you can set options like pp.raw to see more details. Not sure if you can bake that into your command as a default though.

[Kyle Miller]

logInfo responds to set_option if you use m! strings

set_option pp.all true

#ppExpr 1 + (_ : Nat)
/-
fun (x_0 : Nat) =>
  @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
    x_0 : Nat → Nat
-/

[Marcus Rossel]

But could you, e.g., have it use pp.raw true by default?

[Kyle Miller]

    withOptions (fun opt => opt.set pp.raw.name true) do
      logInfo m!"{res.expr} : {← Meta.inferType res.expr}"

[Andrés Goens]

I guess that's cleaner for a proper command, I just jotted that down when writing an MWE (my actual code is quite different anyway, I don't want to print it, was just trying to figure out what went wrong)

[Eric Wieser]

Should the s! elaborator reject an expected type of MessageData?