where to put `instantiateMVars`?

Stream: lean4

[Jireh Loreaux]

I don't understand why the metavariable here isn't instantiated with p when I apply the test tactic. I guess I need instantiateMVars, but I don't know where. Or am I missing something bigger?

import Lean

open Lean Expr Meta

def test (goal : MVarId) (e : Expr) : MetaM (List MVarId) := do
  goal.withContext do
    let ty ← whnfR (← inferType e)
    dbg_trace s!"`ty` is {ty}"
    return [goal]

elab "test" e:term : tactic => do
  let e ← Elab.Term.elabTerm e none
  Elab.Tactic.liftMetaTactic (test · e)

example (p : Nat → Prop) (h : ∀ x, p x) : True := by
  -- why is `p` a metavariable? presumably I need to insert `instantiateMVars` somewhere, but where?
  test h -- `ty` is forall (x : Nat), _uniq.14039 x
  exact True.intro

[Jireh Loreaux]

oh, if I change the dbg_trace line to:

dbg_trace s!"`ty` is {← ppExpr ty}" -- then I get: `ty` is ∀ (x : ℕ), p x

[Jireh Loreaux]

I'm still confused though.

[Thomas Murrills]

Note that _uniq.14039 is not a metavariable but a free variable, and is the FVarId of p in the local context! (Metavariables are always prefixed by ? when printed.)

I think this is more an issue with dbg_trace than anything else. I'd recommend e.g. trace[debug] "`ty` is {ty}" with set_option trace.debug true, because then you get nice string interpolation and pretty-printing (though you sacrifice inline code lens traces).

[Patrick Massot]

You can't really call that a bug. Jireh is getting what he is asking for. He could also ask what he actually wants, which is a pretty-printed expression, using dbg_trace s!"`ty` is {← Meta.ppExpr ty}"

[Patrick Massot]

Oh crap, I just saw Jireh's second message. :face_palm:

[Thomas Murrills]

Oh, indeed, I didn't mean to suggest this was a bug with dbg_trace! I simply meant to say that the issue can be thought of as arising from choosing to use dbg_trace instead of e.g. trace[debug]; I should have said that it's an issue with using dbg_trace instead.

[Patrick Massot]

Let me try again to actually bring new information to this discussion. What Thomas suggest will do more than pretty-printing is actually uses a docs#Lean.MessageData which is also interactive (you can Ctrl-click stuff etc.)

[Patrick Massot]

Thomas, you need to use more backquotes around around your things containings backquotes.

[Thomas Murrills]

You're right, that was copypasta; edited. :)

[Patrick Massot]

I know, I do it all the time.

[Jireh Loreaux]

Thanks both! This all makes sense now, and I learned some new tricks!