Without these annotations, Lean will timeout when trying to synthesize
the type class instance `decidable_eq uint32`. The type class resolution
problem will produce the unification problem:
```
decidable (@eq uint32 a b) =?= decidable (@eq usize ?x ?y)
```
which Lean tries to solve by assigning `?x := a`.
During the assignment, the types of `?x` and `a` are unified with "full
force". Thus, we get the constraint
```
usize_sz =?= uint32_sz
```
which will take forever to be solved when peforming the computation in
unary arithmetic.
Remark: this commit also makes sure that `type_context` will not unfold
irreducible definitions when trying to unify/match the types.
The new test `type_class_performance1.lean` exposes the problem fixed
by this commit.
The array dimension is now stored inside the array.
The main motivation is that it reflects the actual runtime implementation.
We need to store the array size to be able to GC it.
So, it feels silly to have the array size stored in each array object,
but we cannot use this information.
For example, in the `hashmap` we implemented the bucket array using
`array`, and we store the `size` of the array.
Same for the Lean3 `buffer` object.
The `buffer` object doesn't even need to exist.
The actual `array` implementation is the `buffer`
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.
Before this commit, the unifier would try to solve the unification consraint
?m =?= fun x_1 ... x_n, ?m x_1 ... x_n
by assigning
?m := fun x_1 ... x_n, ?m x_1 ... x_n
which fails the occurs check.
This commit skips the assignment by using eta-reduction.
