@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
Now, the elaborator only uses the quasi-pattern unifier approximation
for inferring the implicit motive in recursor-like applications.
This change was motivated by counterintuitive behavior associated with
this approximation. For example, before this commit
```
variables {δ σ : Type}
def ex1 : state_t δ (state_t σ id) σ :=
monad_lift (get : state_t σ id σ) -- doesn't work
def ex2 : state_t δ (state_t σ id) σ :=
do s ← monad_lift (get : state_t σ id σ), -- works
return s
```
The first one doesn't work because when we elaborate
`@monad_lift ?m ?n ?c ?α (get : state_t σ id σ) : ?n ?α`
with expected type `state_t δ (state_t σ id) σ`
It first produces the following unification problem by processing
matching the inferred type with the expected one.
```
?n ?α =?= state_t δ (state_t σ id) σ
==> (approximate using first-order unification)
?n := state_t δ (state_t σ id)
?α := σ
```
Then we try to solve
```
?m ?α =?= state_t σ id σ
==> instantiate metavars
?m σ =?= state_t σ id σ
==> (approximate since it is a quasi-pattern unification constraint)
?m := λ σ, state_t σ id σ
```
Remark: the constraint is not a Milner pattern because `σ` is in
the local context of `?m`. By assuming it is a Milner pattern,
we are ignoring the other possible solutions:
```
?m := λ σ', state_t σ id σ
?m := λ σ', state_t σ' id σ
?m := λ σ', state_t σ id σ'
```
We need the quasi-pattern approximation for elaborating recursors.
So, this commit enable this kind of approximation only when
elaborating recursors and executing induction-like tactics.
If we had used first-order unification, then we would have produced
the right answer: `?m := state_t σ id`
Haskell would solve this example since it always uses
first-order unification during elaboration.
The second one works because when we elaborate
`monad_lift (get : state_t σ id σ)`, the expected type is `state_t δ (state_t σ id) ?α`.
So, `?m ?α =?= state_t σ id σ` will not considered to be a quasi-pattern
since `?α` is not yet assigned to a local constant.
We are not fully confident this commit produces a better user
experience. We know that
- Full higher-order unification (used in Lean2) produces a combinatoric
explosion, and generates a lot of non-termination in complex type class
hierarchies (monad library, has_coe, etc). The problem is that
higher-order unification manages to create new solutions that we
cannot find using first-order unification.
- Lean3 is more reliable than Lean2 for elaborating monadic code because
it does not use higher-order unification.
- For elaborating recursor-like applications, we need at least the
quasi-patterns. We need it when trying to infer the implicit
motive. First-order unification works poorly in this case. Note that
the lack of higher-order unification in Lean3 forces us to provide the
motive explicitly for terms that Lean2 can elaborate.
- We need quasi-patterns for solving unification constraints in the
induction-like tactics. Similar to the previous item. We use it to infer
the motive. (edited) I will try to disable the quasi-pattern
approximation when elaborating regular applications. At least, we will
behave like Haskell for this kind of application.
It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.
Remark: so far, caching, in the tactic framework, only makes a difference for the `simp` tactic.
This is not surprising since the simplifier tries to apply rewriting
lemmas over and over again.
@kha the following idiom is not safe
```
while (is_pi(t)) {
t = whnf(binding_body(t));
}
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
while (is_pi(t)) {
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
@kha: I decided to implement this change before I start the
type_context modifications. The change did not affect the corelib and
test suite much. The only annoying problem is that `out` cannot be
used to name locals anymore.
`{s with ...}` is now `{..., ..s}`, which more clearly expresses that the
result type is not necessarily equal to the type of `s` (in absence of an
expected type and a structure name, we still default to the type of `s`).
Multiple fallback sources can be given: `{..., ..s, ..t}` will fall back to
searching a field in `s`, then in `t`. The last component can also be `..`,
which will replace any missing fields with a placeholder.
The old notation will be removed in the future.
Function applications `(f ...)` were not being elaborated correctly when
`f` has implicit parameters occurring after auto_params.
The new test exposes the problem.
This bug was found when developing the red black tree module.
This commit also fixes the following bugs:
- Invoke type class resolution again after tactic execution at
synthesize method. Reason: metavariables occurring in type
class instances may have been synthesized by tactics.
- mctx.assign optimization at invoke_tactic was incorrect
when the metavariable was assigned by typing rules.
