inferType returns a meta-variable

Stream: lean4

[Son Ho]

I'm trying to write an equivalent of the lettactic as an exercise (custom_let in the code snippet below). However, I have the issue that the type infered for the expression is sometimes a meta-variable. For instance, if in a proof I do custom_let x := 4, in my context I see x : ?m.31609 := 4. Would it be possible to force the inference to "choose" a type which works (Nat or Int)?

def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
  -- I don't think we need that
  Lean.Elab.Tactic.withMainContext do
  --
  let val ← elabTerm val .none
  let type ← inferType val -- TODO: not enough
  --synthesizeAppInstMVars
  withLetDecl name type val fun nval => do
    dbg_trace f!" type: {type}"
    -- For debugging
    let lctx ← Lean.MonadLCtx.getLCtx
    let fid := nval.fvarId!
    let decl := lctx.get! fid
    dbg_trace f!"  nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
    --
    -- Tranform the main goal `?m0` to `let x = nval in ?m1`
    let mvarId ← Tactic.getMainGoal
    let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
    let newVal ← mkLetFVars #[nval] newMVar
    -- Focus on the current goal
    Tactic.focus do
    -- Assign the main goal.
    -- We must do this *after* we focused on the current goal, because
    -- after we assigned the meta variable the goal is considered as solved
    mvarId.assign newVal
    -- Replace the list of goals with the new goal - we can do this because
    -- we focused on the current goal
    Lean.Elab.Tactic.setGoals [newMVar.mvarId!]

elab "custom_let " n:ident " := " v:term : tactic =>
  evalCustomLet n.getId v

[Kyle Miller]

Lean.Elab.Tactic.elabTerm should already do that. I expect that what you're missing is just let type ← instantiateMVars (← inferType val).

[Kyle Miller]

Lots of things work with assigned metavariables inside them, but if you want the metavariables to be replaced with their values in a particular expression, that's what instantiateMVars is for

[Kyle Miller]

Note that if you did logInfo m!" type: {type}" rather than use dbg_trace, you'd get a pretty printed expression with the metavariables all substituted away. That's both helpful (since you don't need to instantiate them in the expression), and a potential debugging danger since some calculations are sensitive to metavariables.

[Son Ho]

Thanks for the information! But I actually still see the meta variables after usinginstantiateMVars (note that I also tried variations, for instance : let val ← instantiateMVars (← elabTerm val .none)). Is there something else that I could try?

[Scott Morrison]

You need the instantiateMVars on the inferType line. (not tested)

[Scott Morrison]

Just instantiating the mvars in val doesn't guarantee you won't have uninstantiated mvars after you inferType val!

[Son Ho]

Sorry for my confusing message : I did test let type ← instantiateMVars (← inferType val), but as it didn't work I also tried by additionally inserting instantiateMVars in other places (and also let lctx ← instantiateLCtxMVars (<- Lean.MonadLCtx.getLCtx), etc.). None of those made a difference.

[Son Ho]

After further investigation (and exploring some of the tactics provided by Lean): adding synthesizeSyntheticMVarsUsingDefault after inferType solves the problem