Missing metavariable in infotree

Stream: lean4

[Eric Wieser]

When I run inferType on termInfos in the InfoTree, it seems that sometimes they fail.

My testcase is the following

import Lean

-- template thanks to Kyle
open Lean Elab Command in
elab "#info " c:command : command => do
  let initInfoTrees ← getResetInfoTrees
  try
    elabCommand c
    let #[t] := (← getInfoTrees).toArray | throwError "Expected one tree"
    t.visitM'
      (preNode := fun ctx info _ => do
        if let .ofTermInfo ti := info then
          discard <| ctx.runMetaM ti.lctx do
            let t ← Meta.inferType ti.expr
            PrettyPrinter.ppExpr t
            )
  finally
    modify fun st =>
      { st with infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } }

theorem add_comm {α} [Add α] (a b : α) : a + b = b + a := sorry

#info
theorem test (x : ℕ) : 1 + 2 = 3 := by
  rewrite [add_comm] at *
  sorry

I get

unknown metavariable '?_uniq.1860'

[Eric Wieser]

The problem is specifically the at *; presumably the infotree is being populated with garbage by rw [add_comm] at x

[Eric Wieser]

Generally speaking, is it safe to inferType on terms within infotrees? Will they contain unresolved metavariables? Or are the trees populated only once everything is resolved?

[Kyle Miller]

There seems to be something wrong with whatever ctx.runMetaM does. At the least, since it adapts the MetaM monad to IO, it drops all log info.

You can set the mctx and lctx manually if you switch to TermElabM:

open Lean Elab Command in
elab "#info " c:command : command => do
  let initInfoTrees ← getResetInfoTrees
  try
    elabCommand c
    let #[t] := (← getInfoTrees).toArray | throwError "Expected one tree"
    liftTermElabM do
      t.visitM'
        (preNode := fun ctx info _ => do
          if let .ofTermInfo ti := info then
            Meta.withMCtx ctx.mctx <| Meta.withLCtx ti.lctx {} do
              let t ← Meta.inferType ti.expr
              logInfo m!"{t}"
              )
  finally
    modify fun st =>
      { st with infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } }

[Kyle Miller]

(I used TermElabM just because it's convenient to enter it from CommandM. If there's a function to go straight to MetaM, you could use that too.)

[Eric Wieser]

Does that fix my example above?

[Kyle Miller]

I thought it did, but I didn't investigate the errors in the log messages. Using set_option pp.rawOnError true suggests that the problem is that something is forgetting to save the context for some of the terms, and that's why you get the unknown metavariable error.

[Kyle Miller]

Generally speaking, is it safe to inferType on terms within infotrees? Will they contain unresolved metavariables? Or are the trees populated only once everything is resolved?

It should be safe, and they can contain unresolved metavariables. The unknown metavariable error isn't about whether it's resolved -- any record of it is completely missing from the metavariable context, which is an error.

[Eric Wieser]

What I'm confused about is how the context gets updated if the metavariables are resolved after the info tree is created

[Kyle Miller]

The infotree has special context nodes that generally contain context after its subtrees are created.

[Eric Wieser]

Ah, so an inner term node can reference a metavariable, while the actual assignment is stored in an ancestor context node somewhere?

[Eric Wieser]

Kyle Miller said:

There seems to be something wrong with whatever ctx.runMetaM does. At the least, since it adapts the MetaM monad to IO, it drops all log info.

Yes, I had a fix to this locally and figured it was a distraction here. Thanks for your spelling, I'll compare it to mine to see if you or I missed anything (yours is cleaner!)

[Eric Wieser]

Ah, src#Lean.Elab.ContextInfo.runMetaM also restores a bunch of other data from info

[Eric Wieser]

In particular

  /-
    We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
    have been used in `lctx` and `info.mctx`.
  -/