inferType and expressions introduced by have

Stream: lean4

[Tomaz Gomes Mascarenhas]

Hello! I would like to understand why inferType gives me this output when used in an expression introduced by a have without specifying it's type. I am writting a tactic that produces several intermediate terms using have and I would like to not have to specify their type, but this behavior of inferType is causing some trouble. Is there a way around it?

import Lean
open Lean Lean.Elab.Tactic

syntax (name := tac) "tac" term : tactic

@[tactic tac] def evalTac : Tactic := fun stx => withMainContext do
  let e ← elabTerm stx[1] none
  let t ← Meta.inferType e
  logInfo t

example : A ∨ B → True := by
  intro h
  tac h -- A ∨ B
  have h2 := h
  tac h2 -- ?m655
  exact True.intro

[Adam Topaz]

I'm not an expert, but docs4#Lean.instantiateMVars might be required.

[Adam Topaz]

At least the following seems to work for me:

@[tactic tac] def evalTac : Tactic := fun stx => withMainContext do
  let e ← elabTerm stx[1] none
  let t ← instantiateMVars (← Meta.inferType e)
  logInfo t

[Tomaz Gomes Mascarenhas]

that works, thanks!