• Forgetting instantiateMVars
• Forgetting to clean up metadata or annotations
• Forgetting Expr.consumeMData
• Forgetting Expr.cleanupAnnotations
• Forgetting whnfR
• Forgetting to wrap the tactic in withMainContext
• Forgetting to complete elaboration by synthesizing pending synthetic metavariables
• Forgetting to revert the mvar state on error when recovering
• assigning a metavariable without doing isDefEq with the metavariable's type
• Using withLocalDecl instead of forallBoundedTelescope e (some 1) for instances