Confused by Metavariable occurance

Stream: metaprogramming / tactics

[William Sørensen]

I was trying to see what certain expressions elab to so i wrote this little piece of code

open Parser.Term
elab "#test" t:term : command =>
  runTermElabM fun _ => do
    let x ← Elab.Term.elabTerm t none
    let xType ← inferType x
    let xChecked ← Elab.Term.ensureHasType xType x
    let xFinal ← instantiateMVars xChecked
    dbg_trace (← ppExpr xFinal)
    dbg_trace (repr xFinal)

#test (match Nat.zero with | _ => Nat.zero)
#test let rec x := 0; x

but it yielded some very suprising results:

?m.17667
Lean.Expr.mvar (Lean.Name.mkNum `_uniq 17667)

On the line with the match.

(fun x => x) ?m.17669
Lean.Expr.app
  (Lean.Expr.lam
    `x
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 17673))
    (Lean.Expr.mdata
      { entries := [(`_recApp,
                     Lean.DataValue.ofSyntax
                       (Lean.Syntax.ident
                         (Lean.SourceInfo.original
                           "".toSubstring
                           { byteIdx := 6701 }
                           "\n".toSubstring
                           { byteIdx := 6702 })
                         "x".toSubstring
                         `x
                         []))] }
      (Lean.Expr.bvar 0))
    (Lean.BinderInfo.default))
  (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 17669))

On the line with the let rec

So now my question is as follows, why are these mvars appearing here? I would expect these to elab into complete exprs, why do they not?

[William Sørensen]

Fixed a small error, was using the wrong elab, but results are still confusing

[Jannis Limperg]

It seems like the elaborator decided to postpone some tasks; the metavariables stand in for the postponed parts of the term. If you disable postponing, you at least get an informative error for the match. (Same behaviour as before for the let rec, but that one also confuses me in general.)

import Lean

open Lean Lean.Meta Lean.Elab.Command Lean.Elab.Term

elab "#test" t:term : command =>
  liftTermElabM do
    withoutPostponing do
    withSynthesize do
    withoutErrToSorry do
    let x ← Elab.Term.elabTerm t none
    let xType ← inferType x
    let xChecked ← Elab.Term.ensureHasType xType x
    let xFinal ← instantiateMVars xChecked
    dbg_trace (← ppExpr xFinal)
    dbg_trace (repr xFinal)

#test (match Nat.zero with | _ => Nat.zero)
#test let rec x := 0; x

The withSynthesize and withoutErrToSorry don't affect this example, but are needed in general if you want to elaborate something without allowing any funny business.

(Btw #mwe in future please, you were missing an import and some opens.)

[William Sørensen]

Ok nice thanks for the help, maybe Ill find some hack to avoid the let rec then...

[William Sørensen]

For closure on this, it looks like let recs are lifted up out of the expression and elab'd kinda like a def so i think this explains why the let rec did not elab, it needed a place to be lifted. idk this is kinda off vibes but noteworthy anyway