Using new local declarations in the elaborator

Stream: lean4

[Simon Hudon]

I have the following code snippet:

def test : TermElabM Unit :=
let nat := mkConst ``Nat []
withLocalDeclD `x nat λ x => do
  let e ← Term.elabTerm (← `(x + x)) nat
  println!"{← instantiateMVars e}"

#eval test

and I get this print out:

HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (sorryAx.{1} Nat Bool.true) (sorryAx.{1} Nat Bool.true)
<CoreM>:0:0: error: unknown identifier 'x'

<CoreM>:0:0: error: unknown identifier 'x'

I was hoping that withLocalDeclD would make the new variable x available in the elaborator but it only elaborates it into sorryAx and then printing the resulting term gives two error messages (they disappear if I remove the println). How can I make x visible during elaboration?

[Kyle Miller]

@Simon Hudon Here's one way to make it be "visible", though it's by making sure to insert x as an expression:

open Lean Elab Tactic Meta in
def test : TermElabM Unit :=
  let nat := mkConst ``Nat []
  withLocalDeclD `x nat λ x => do
    let x' ← Term.exprToSyntax x
    let e ← Term.elabTerm (← `($x' + $x')) nat
    --Term.synthesizeSyntheticMVars -- < optional here
    dbg_trace "{← instantiateMVars e}"

[Kyle Miller]

If you're really going for name capture, then you can adjust the hygiene settings for the quasiquotation:

open Lean Elab Tactic Meta in
def test : TermElabM Unit :=
  let nat := mkConst ``Nat []
  withLocalDeclD `x nat λ _ => do
    let e ← Term.elabTerm (← set_option hygiene false in `(x + x)) nat
    dbg_trace "{← instantiateMVars e}"

[Gabriel Ebner]

IMHO the preferred option is to just use the right x as the free variable name:

import Lean
open Lean Meta Elab

def test : TermElabM Unit := do
  let nat := .const ``Nat []
  withLocalDeclD (← `(x)).1.getId nat fun x => do
    let e ← Term.elabTerm (← `(x + x)) nat
    logInfo (← instantiateMVars e)

#eval test

[Gabriel Ebner]

--Term.synthesizeSyntheticMVars -- < optional here

BTW, I've recently learned of withSynthesize which only synthesizes the mvars created in the block. (As opposed to synthesizeSyntheticMVars, which also tries to synthesize all synthetic mvars from other, previous elaborators.)

[Simon Hudon]

Thank you both! If I understand correctly, my problem came from the fact that I used `x as the name of my variable but when the elaborator encounters x in the syntax tree, it doesn't look up x but `x._@.Module._hyg.1 (for the given hygienic scope). Is this right?

[Simon Hudon]

BTW, I've recently learned of withSynthesize which only synthesizes the mvars created in the block. (As opposed to synthesizeSyntheticMVars, which also tries to synthesize all synthetic mvars from other, previous elaborators.)

Cool so it's like you separate two elaborators with a withNewMCtxDepth call, is that right?

[Gabriel Ebner]

A bit, yeah. The withSynthesize combinator resets the list of synthetic mvars at the beginning of the block and then appends them again when it's finished.

[Simon Hudon]

I think I still have a whole lot to learn about meta variable kinds and I wasn't aware that there was a list of synthetic variables. I assume meta variables get added to it when you call mkFreshExprMVar and otherwise, there's probably no reasons to add anything to it.

[Gabriel Ebner]

Oh, then you're completely confused. :smile: Synthetic metavariables and metavariables are completely different things. Synthetic metavariables are 1) type class constraints + 2) tactic blocks + 3) postponed term elaborators. Synthesizing the synthetic metavariables means running TC synthesis, running the tactic blocks, and trying the term elaborators again.

[Kyle Miller]

It gets added if you do docs#Lean.Elab.Term.registerSyntheticMVar

[Simon Hudon]

Aaah! Thanks!

Synthetic metavariables and metavariables are completely different things.

But they still use Expr.mvar nodes, I assume, don't they? How different is completely different?

[Kyle Miller]

My understanding is that a synthetic metavariable is three things together: the Expr.mvar node (and an entry in the metavariable table), an entry in the synthetic metavariables table, and its presence in the pending metavariables list.

[Simon Hudon]

That clears it up, thank you. I should bookmark this answer