Instantiating MVars in decls

Stream: lean4

[Jannis Limperg]

I just wrote this function:

def instantiateMVarsInMVarType (mvarId : MVarId) : MetaM Expr := do
  let type ← instantiateMVars (← getMVarDecl mvarId).type
  setMVarType mvarId type
  return type

I was wondering why this isn't defined in the stdlib (or maybe I just didn't find it). Isn't it a good idea to replace an expression with its mvar-instantiated counterpart whenever possible?

[Leonardo de Moura]

We have

def instantiateMVarDeclMVars (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=

which instantiates all assigned metavariables in the MetavarDecl for mvarId.
It is not just the type, but the local context too.
We used this function in the by tac implementation. It is executed at the beginning. I can see it may be useful for tactics like the one you are building.

[Jannis Limperg]

Ah nice, thanks! I'll continue to do this sort of caching then.