(Properly) inferring types in meta code

Stream: lean4

[Alex Keizer]

I'm trying to infer the type of an ambiguous let binding, whose type should be able to be inferred by it's usage in a later function.

import Lean
open Lean Meta Elab Term

elab "dbg_type" fv:ident tail:term : term => do
  let name := fv.getId
  let some fv ← resolveId? fv
    | panic! ""

  synthesizeSyntheticMVarsNoPostponing
  let ty ← inferType fv

  dbg_trace "trace: '{name}' has type '{ty}'"
  if ty.isMVar then
    dbg_trace "{ty} is an MVar"
  else
    dbg_trace "{ty} is not an MVar"
  Elab.Term.elabTerm tail none




def force_nat : Nat → Nat := id

example : True :=
  let n := 2
  let _ := force_nat n
  let _ := dbg_type n 1
  .intro

The infoview shows n : Nat as expected, but the trace just says

trace: 'n' has type '?_uniq.3943'
?_uniq.3943 is an MVar

I get the feeling I need to so more synthesizing of MVars somehow, is there some method stronger than synthesizeSyntheticMVars?

[Jannis Limperg]

Looks to me like the mvar is getting assigned just fine, you just need to instantiateMVars ty.

[Jannis Limperg]

Yep, that fixes it. It's maybe mildly surprising that inferType doesn't already do this.

[Alex Keizer]

Aha, so to make sure I understand correctly: the environment already has a mapping that the mvar ?_uniq.3943 should stand for Nat, and instantiateMVars just goes to check this mapping and replaces any (pre-assigned) mvars with their assigned value, right?

[Jannis Limperg]

Yes. Lean does not remember which expressions a metavariable ?m may appear in. So when a metavariable is assigned, these expressions remain unchanged and still contain ?m. You must then manually synchronise the expressions with the assignment by calling instantiateMVars. Forgetting to do this is one of the most common mistakes in tactic code. Many builtin functions (e.g. whnf) also do instantiateMVars for you, but when in doubt it's better to instantiate too much than too little since instantiateMVars is quite well-optimised. In particular, it's an immediate no-op for (sub)expressions which don't contain any metavariables.