partial def resolveExprMVars {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (e : TypedTLAPlus.Expr) : m TypedTLAPlus.Expr

Eliminates every mvar node inside e, walking bottom-up so a nested mvar resolves before an outer one that might wrap it. Each metavariable defaults to its recorded upper bound, if there's exactly one; no recorded bound is an unconstrained-metavariable error, and more than one is unsupported (would need per-site tracking to substitute soundly).

Only eliminates Expression.mvar wrapper nodes, not Typ.mvar occurrences embedded in a node's stored type field — those are resolved by resolveMVars below, as a second pass.

def instantiateMVars {m : Type → Type} [Monad m] [MonadElaborator m] : TypedTLAPlus.Typ → m TypedTLAPlus.Typ

Best-effort metavariable substitution for a Typ, named after Lean.Meta.instantiateMVars since it does the same job for the same reason: an already-resolved metavariable (e.g. pinned by an earlier operand in the same call) is substituted with its solution; one that's never been constrained is left as Typ.mvar n (rendered ?n) rather than erroring. Originally written for a Typ about to be embedded in a thrown TCError (so the message shows a concrete type instead of a raw ?n), but the same gap shows up whenever a Typ obtained from inferExpr is about to be pattern-matched against a specific shape (.record/.set/.function/…): a scheme operator's result can carry a metavariable its own argument-checking already solved (subtype's _, .mvar b case, in Elaborator/Subtyping.lean), but nothing rewrites the Typ tree in place, so a bare structural match sees .mvar n and not the solution — e.g. \E m \in DOMAIN someBag : m.field fails to elaborate m.field even though m's type is fully known by then. Calling this before such a match (as Elaborator/Expressions.lean's domain-binder/record-access/index/EXCEPT-step rules do) fixes that: read-only over the metavariable context, so calling it anywhere never affects checking's soundness, only whether an already-decided type is visible yet.

Equations

• instantiateMVars = resolveTypeMVarsWith✝ (pure ∘ SurfaceTLAPlus.Typ.mvar)

def resolveMVars {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (e : TypedTLAPlus.Expr) : m TypedTLAPlus.Expr

Closes out an elaborated expression: resolveExprMVars above eliminates every Expression.mvar wrapper node (assigning whatever metavariables it names along the way), then this second pass walks the result once more resolving any Typ.mvar left behind in a stored type field.

Equations

• resolveMVars e = do let e' ← resolveExprMVars e TypedTLAPlus.Expression.traverse (resolveTypeMVars✝ (posOf e')) e'