Skip to content

Metaprogramming gotchas

Kyle Miller edited this page Aug 28, 2025 · 12 revisions

There is a lot going on in Lean's metaprogramming interface, and there are lots of things that can (and commonly do) go wrong. This page is a collection of metaprogramming gotchas.

There are many latent bugs in mathlib's tactic implementations. Tactics have been tested well enough to handle the "happy path", but sometimes when they are stressed the bugs are revealed. This page might help serve as a way to diagnose bugs.

Forgetting instantiateMVars

Lean expressions can contain mvars ("metavariables"), which are IDs that points into a table containing what the mvar has been assigned to and can be replaced with (if anything). The instantiateMVars function takes an expression and recursively replaces mvars with what they stand for.

Generally, you cannot assume an Expr handed to you has its mvars fully instantiated. Meta code that does pattern matching on mvars either needs to use Qq (which uses defeq checks during pattern matching) or otherwise instantiateMVars before matching. For example, when matching expressions for certain patterns, the pattern might not match becausee the match expression just sees an mvar -- it won't instantiate them automatically.

For tactics that want to instantiate all metavariables for a given goal, they can use instantiateMVarDeclMVars.

Forgetting to clean up metadata or annotations

There's a class of errors where tactics fail to clean up certain kinds of information that it considers to be irrelevant in a match. Depending on exactly what is considered to be irrelevant, the subsections here are giving different strengths if solution to the problem.

Forgetting Expr.consumeMData

Lean expressions can be wrapped in mdata ("metadata"), which is a special kind of expression that's meant to attach additional information to an expression. Metadata has no effect on the logical meaning of an expression -- it's purely for elaboration purposes. Many processes in Lean can attach metadata to a term.

Similarly to instantiateMVars, a common mistake is forgetting to consumeMData (i.e., erase any outermost mdata) before pattern matching.

Insert example of a test that exercises consumeMData

Forgetting Expr.cleanupAnnotations

Annotations are identity functions wrapped around local hypotheses that come from arguments with default values (for example, from a (x : Nat := 0) binder). Similarly to consumeMData, tactics can forget to do cleanupAnnotations. This function also does consumeMData, so you don't need to do both.

Forgetting whnfR

Often tactics actually want to do pattern matching up to reducible defeq. What whnfR does is put an expression into weak-head normal form while unfolding @[reducible] (and abbrev) definitions. This is a generalization of consumeMData and cleanupAnnotations, and it also is like a lazy version of instantiateMVars (it only instantiates mvars in the heads of applications, or if the entire expression is an mvar).

Forgetting to wrap the tactic in withMainContext

Part of the metaprogramming state is the current local context. This is used for anything that needs to evaluate an fvar, for example inferType, isDefEq, etc. Tactics that fail to set the local context (for example with withMainContext) will have errors such as unknown free variable '_fvar.1286'.

Forgetting to complete elaboration by synthesizing pending synthetic metavariables

It is a tactic's responsibility to make sure elaboration is fully completed. Part of the elaboration state are the pending synthetic metavariables, which are metavariables that come with a bit of code that tell Lean what needs to be done to synthesize them. For example, instance problems, tactic blocks, coercion problems, postponed elaborators, etc. This process only occurs at explicit checkpoints.

One way is to use Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing, which ensures that everything can be synthesized, or otherwise throws an error. Another is to wrap a tactic appropriately in Lean.Elab.Term.withSynthesize.

Tactics that fail to do this end up with crazy tactic states containing metavariables, where if you follow them up with a simple have := 1 the metavariables suddenly get solved for.

Forgetting to revert the mvar state on error when recovering

This is a more subtle error. Tactics generally have side effects, for example through isDefEq, which can set mvars, but if the tactic forgets to revert the mvar state on error, then it can't safely recover from that error itself. Use tools like observing?.

Note that try/catch for TacticM already reverts the state on error. This is a gotcha of its own, where in the catch the intermediate state is no longer available, which can affect error message generation. You need to switch into TermElabM or MetaM if you need such information.

assigning a metavariable without doing isDefEq with the metavariable's type

Let's say you have a metavariable m : MVarId and you know that x : Expr is an expression that would unify with m. Is it safe to just do m.assign x and skip the isDefEq check? No, it's not. You must be sure there has been code equivalent to isDefEq (← m.getType) (← inferType x) already. Metavariables have types that can themselves be metavariables (or otherwise contain metavariables), and this is an essential step to ensure that these metavariables are assigned. The Lean.MVarId.assign function is very low level: it merely assigns the metavariable. Using it on its own can lead to unassigned metavariables and inconsistent states.

The Lean.MVarId.assignIfDefeq function from std is a safer alternative to Lean.MVarId.assign, and it does this isDefEq check for you. It is also fine using Lean.MVarId.assign after functions such as elabTermEnsuringType, if the provided expected type is the metavariable, since such functions do the isDefEq check.

Forgetting withoutRecover when using evalTactic

Tactics might use the high-level evalTactic interface to evaluate tactic scripts, rather than use the lower-level tactic interface. Often, these tactic scripts do not include any user input. They are written in a way where the tactic expects the script to succeed. Or, at least, if there are errors, the entire tactic should fail rather than leave things in some intermediate state.

To this end, it's important to wrap these tactic scripts in withoutRecover. This disables error correction features that are useful to users who are writing tactic proofs (like for example inserting sorry when there is some elaboration error). Roughly speaking, it switches tactics from a mode where they log errors to a mode where they throw exceptions.

Forgetting to set a syntax ref

Another piece of metaprogramming state is the "ref", some Syntax that is used for its source position information. Exceptions (with throwError), the message log (with logInfo, logWarning, and logError), and the trace log (with trace[...]) all use the ref to localize the messages in the editor. Setting the ref is done using withRef/withRef?. It is OK if the provided ref has no source position information; these will not clear the ref. So for example using withRef generalStx <| withRef specificStx <| withRef? moreSpecificStx? <| ... is a way to preferentially use one of the later refs, depending on what actually has source position information available.

Usually the default ref is sensible — for elaborators, it is always set to the syntax being elaborated — but sometimes there are better refs to use. For example, the #check command uses the #check token itself as the ref for messages. In syntax quotations, the token can be extracted using #check%$stx syntax.

It's possible to set the ref using an array of syntaxes as well. For example, we may have a command foo that wants to report messages up to its => token. We can use the quotation `(foo%$fooTk $s1 =>%$arrow $s2) and then use withRef (mkNullNode #[fooTk, s1, arrow]) to use the given range. The syntaxes provided to mkNullNode ought to be in source-code order. It is ok if any of these syntaxes do not have any source position information.

Another main consumer of the syntax ref is syntax quotations, which use it to fill in the SourceInfo in the constructed syntaxes, via SourceInfo.fromRef. The resulting source position is "synthetic", which has some effect on how the LSP processes hover requests. When constructing some syntax in a macro, it can be very important to transfer source positions from the original syntax to the new syntax. Either this can be done with strategic withRefs, or for tokens using the same #check%$stx syntax. Identifiers need to be inserted with mkIdentFrom/mkIdentFromRef if they should have a specific ref.

Furthermore, when creating synthetic syntax inside of a larger elaborator, pay extra special attention that the ref is sensible. You likely do not want elaboration errors for some bit of syntax to highlight an entire command.

Lastly, MonadRef.withRef is the low-level function to unconditionally set the ref, for example MonadRef.withRef .missing ... effectively clears it. It shouldn't be used, except when implementing a MonadRef instance for a custom class, or if you are Sebastian Ullrich. I'm pointing it out just to point out that it is a different function from withRef.

Similar considerations for refs also apply to the InfoTree system. Their relevance to this section is limited, but there are two connections: (1) InfoTrees get source ranges from syntax, and if that syntax came from quotations then it's ultimately from the syntax ref, and (2) functions such as withTacticInfoContext, which create InfoTrees, take a Syntax argument, and this argument is used for its source position information.

Clone this wiki locally