-
Notifications
You must be signed in to change notification settings - Fork 353
Metaprogramming gotchas
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.
Lean expressions can contain mvars ("metavariables"), which contain an id that points to a table containing what the mvar 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. This is because the match expression just sees an mvar -- it won't instantiate them automatically.
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.
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
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.
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).
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'.
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.
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?.
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.
The fundamental pattern for handling the locally nameless lambda calculus is that, given .forallE n t b i, you do withLocalDecl n t b fun v => ... b.instantiate1 v ... to turn the bvar into an fvar in the body. However, if t is a class, this does not add an instance to the local instance cache. If you are relying on instances, then you should do forallBoundedTelescope e (some 1) fun vs b => let v := vs[0]!; ... since this function (like all telescope functions) is responsible for maintaining the local instance cache.