5938dbbd14
The `elab_as_elim` elaborator eagerly elaborates arguments that can help
with elaborating the motive, however it does not include the transitive
closure of parameters appearing in types of parameters appearing in ...
types of targets.
This leads to counter-intuitive behavior where arguments supplied to the
eliminator may unexpectedly have postponed elaboration, causing motives
to be type incorrect for under-applied eliminators such as the
following:
```lean
class IsEmpty (α : Sort u) : Prop where
protected false : α → False
@[elab_as_elim]
def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
(IsEmpty.false a).elim
example {α : Type _} [IsEmpty α] :
id (α → False) := isEmptyElim (α := α)
```
The issue is that when `isEmptyElim (α := α)` is computing its motive,
the value of the postponed argument `α` is still an unassignable
metavariable. With this PR, this argument is now among those that are
eagerly elaborated since it appears as the type of the target `a`.
This PR also contains some other fixes:
* When underapplied, does unification when instantiating foralls in the
expected type.
* When overapplied, type checks the generalized-and-reverted expected
type.
* When collecting targets, collects them in the correct order.
Adds trace class `trace.Elab.app.elab_as_elim`.
This is a followup to #4722, which added motive type checking but
exposed the eagerness issue.
|
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||