Lean.MetavarContext

The metavariable context stores metavariable declarations and their assignments. It is used in the elaborator, tactic framework, unifier (aka isDefEq), and type class resolution (TC). First, we list all the requirements imposed by these modules.

We may invoke TC while executing isDefEq. We need this feature to WellFoundedRelationbe able to solve unification problems such as:
```
f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
```
where (?a : Type) (?s : Ring ?a) (?x ?y : ?a).

During isDefEq (i.e., unification), it will need to solve the constrain
```
ringAdd ?s =?= intAdd
```
We say ringAdd ?s is stuck because it cannot be reduced until we synthesize the term ?s : Ring ?a using TC. This can be done since we have assigned ?a := Int when solving ?a =?= Int.
TC uses isDefEq, and isDefEq may create TC problems as shown above. Thus, we may have nested TC problems.
isDefEq extends the local context when going inside binders. Thus, the local context for nested TC may be an extension of the local context for outer TC.
TC should not assign metavariables created by the elaborator, simp, tactic framework, and outer TC problems. Reason: TC commits to the first solution it finds. Consider the TC problem Coe Nat ?x, where ?x is a metavariable created by the caller. There are many solutions to this problem (e.g., ?x := Int, ?x := Real, ...), and it doesn’t make sense to commit to the first one since TC does not know the constraints the caller may impose on ?x after the TC problem is solved.

Remark: we claim it is not feasible to make the whole system backtrackable, and allow the caller to backtrack back to TC and ask it for another solution if the first one found did not work. We claim it would be too inefficient.
TC metavariables should not leak outside of TC. Reason: we want to get rid of them after we synthesize the instance.
simp invokes isDefEq for matching the left-hand-side of equations to terms in our goal. Thus, it may invoke TC indirectly.
In Lean3, we didn’t have to create a fresh pattern for trying to match the left-hand-side of equations when executing simp. We had a mechanism called "tmp" metavariables. It avoided this overhead, but it created many problems since simp may indirectly call TC which may recursively call TC. Moreover, we may want to allow TC to invoke tactics in the future. Thus, when simp invokes isDefEq, it may indirectly invoke a tactic and simp itself. The Lean3 approach assumed that metavariables were short-lived, this is not true in Lean4, and to some extent was also not true in Lean3 since simp, in principle, could trigger an arbitrary number of nested TC problems.

Here are some possible call stack traces we could have in Lean3 (and Lean4).

Elaborator (-> TC -> isDefEq)+
Elaborator -> isDefEq (-> TC -> isDefEq)*
Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*

In Lean4, TC may also invoke tactics in the future.

In Lean3 and Lean4, TC metavariables are not really short-lived. We solve an arbitrary number of unification problems, and we may have nested TC invocations.
TC metavariables do not share the same local context even in the same invocation. In the C++ and Lean implementations we use a trick to ensure they do:
Metavariables may be natural, synthetic or syntheticOpaque.
1. Natural metavariables may be assigned by unification (i.e., isDefEq).
2. Synthetic metavariables may still be assigned by unification, but whenever possible isDefEq will avoid the assignment. For example, if we have the unification constraint ?m =?= ?n, where ?m is synthetic, but ?n is not, isDefEq solves it by using the assignment ?n := ?m. We use synthetic metavariables for type class resolution. Any module that creates synthetic metavariables, must also check whether they have been assigned by isDefEq, and then still synthesize them, and check whether the synthesized result is compatible with the one assigned by isDefEq.
3. SyntheticOpaque metavariables are never assigned by isDefEq. That is, the constraint ?n =?= Nat.succ Nat.zero always fail if ?n is a syntheticOpaque metavariable. This kind of metavariable is created by tactics such as intro. Reason: in the tactic framework, subgoals as represented as metavariables, and a subgoal ?n is considered as solved whenever the metavariable is assigned.
This distinction was not precise in Lean3 and produced counterintuitive behavior. For example, the following hack was added in Lean3 to work around one of these issues:
When creating lambda/forall expressions, we need to convert/abstract free variables and convert them to bound variables. Now, suppose we are trying to create a lambda/forall expression by abstracting free variable xs and a term t[?m] which contains a metavariable ?m, and the local context of ?m contains xs. The term
```
fun xs => t[?m]
```
will be ill-formed if we later assign a term s to ?m, and s contains free variables in xs. We address this issue by changing the free variable abstraction procedure. We consider two cases: ?m is natural or synthetic, or ?m is syntheticOpaque. Assume the type of ?m is A[xs]. Then, in both cases we create an auxiliary metavariable ?n with type forall xs => A[xs], and local context := local context of ?m - xs. In both cases, we produce the term fun xs => t[?n xs]
1. If ?m is natural or synthetic, then we assign ?m := ?n xs, and we produce the term fun xs => t[?n xs]
2. If ?m is syntheticOpaque, then we mark ?n as a syntheticOpaque variable. However, ?n is managed by the metavariable context itself. We say we have a "delayed assignment" ?n xs := ?m. That is, after a term s is assigned to ?m, and s does not contain metavariables, we replace any occurrence ?n ts with s[xs := ts].
Gruesome details:
- When we create the type forall xs => A for ?n, we may encounter the same issue if A contains metavariables. So, the process above is recursive. We claim it terminates because we keep creating new metavariables with smaller local contexts.
- Suppose, we have t[?m] and we want to create a let-expression by abstracting a let-decl free variable x, and the local context of ?m contains x. Similarly to the previous case
```
let x : T := v; t[?m]
```
  will be ill-formed if we later assign a term s to ?m, and s contains free variable x. Again, assume the type of ?m is A[x].
  1. If ?m is natural or synthetic, then we create ?n : (let x : T := v; A[x]) with and local context := local context of ?m - x, we assign ?m := ?n, and produce the term let x : T := v; t[?n]. That is, we are just making sure ?n must never be assigned to a term containing x.
  2. If ?m is syntheticOpaque, we create a fresh syntheticOpaque ?n with type ?n : T -> (let x : T := v; A[x]) and local context := local context of ?m - x, create the delayed assignment ?n #[x] := ?m, and produce the term let x : T := v; t[?n x].
    
    Now suppose we assign s to ?m. We do not assign the term fun (x : T) => s to ?n, since fun (x : T) => s may not even be type correct. Instead, we just replace applications ?n r with s[x/r]. The term r may not necessarily be a bound variable. For example, a tactic may have reduced let x : T := v; t[?n x] into t[?n v].
    
    We are essentially using the pair "delayed assignment + application" to implement a delayed substitution.
We use TC for implementing coercions. Both Joe Hendrix and Reid Barton reported a nasty limitation. In Lean3, TC will not be used if there are metavariables in the TC problem. For example, the elaborator will not try to synthesize Coe Nat ?x. This is good, but this constraint is too strict for problems such as Coe (Vector Bool ?n) (BV ?n). The coercion exists independently of ?n. Thus, during TC, we want isDefEq to throw an exception instead of return false whenever it tries to assign a metavariable owned by its caller. The idea is to sign to the caller that it cannot solve the TC problem at this point, and more information is needed. That is, the caller must make progress an assign its metavariables before trying to invoke TC again.

In Lean4, we are using a simpler design for the MetavarContext.
No distinction between temporary and regular metavariables.
Metavariables have a depth Nat field.
MetavarContext also has a depth field.
We bump the MetavarContext depth when we create a nested problem.

Example: Elaborator (depth = 0) -> Simplifier matcher (depth = 1) -> TC (level = 2) -> TC (level = 3) -> ...
When MetavarContext is at depth N, isDefEq does not assign variables from depth < N.
Metavariables from depth N+1 must be fully assigned before we return to level N.
New design even allows us to invoke tactics from TC.
Main concern

We don't have tmp metavariables anymore in Lean4. Thus, before trying to match the left-hand-side of an equation in simp. We first must bump the level of the MetavarContext, create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with these metavariables. We are hoping to minimize this overhead by
- Using better indexing data structures in simp. They should reduce the number of time simp must invoke isDefEq.
- Implementing isDefEqApprox which ignores metavariables and returns only false or undef. It is a quick filter that allows us to fail quickly and avoid the creation of new fresh metavariables, and a new pattern.
- Adding built-in support for arithmetic, Logical connectives, etc. Thus, we avoid a bunch of lemmas in the simp set.
- Adding support for AC-rewriting. In Lean3, users use AC lemmas as rewriting rules for "sorting" terms. This is inefficient, requires a quadratic number of rewrite steps, and does not preserve the structure of the goal.

The temporary metavariables were also used in the "app builder" module used in Lean3. The app builder uses isDefEq. So, it could, in principle, invoke an arbitrary number of nested TC problems. However, in Lean3, all app builder uses are controlled. That is, it is mainly used to synthesize implicit arguments using very simple unification and/or non-nested TC. So, if the "app builder" becomes a bottleneck without tmp metavars, we may solve the issue by implementing isDefEqCheap that never invokes TC and uses tmp metavars.

Notes on artificial eta-expanded terms due to metavariables. #