Question about `elabTermEnsuringType`

Stream: lean4

[Arthur Paulino]

I found this by accident, but I don't understand what it means:

import Lean

open Lean.Elab.Command Lean.Elab.Term in
elab "#foo" : command =>
  liftTermElabM `bar do
    let termNat5 ← elabTerm (← `(5)) none
    let hmm? ← elabTermEnsuringType (← `(Nat)) termNat5
    dbg_trace termNat5
    dbg_trace hmm?

#foo
-- OfNat.ofNat.{?_uniq.1288} ?_uniq.1287 5 ?_uniq.1289
-- Nat

How come Lean was able to elaborate (← `(Nat)) as a term using termNat5 as the expected type?

[Arthur Paulino]

Ah, I guess it's because of metavariables whose elaboration was postponed. It stopped working as soon as I added synthesizeSyntheticMVarsNoPostponing