refactor: Add motive to Expr.proj

[digama0]

This is an experiment to add a motive to Expr.proj. It is the same as the motive passed to the underlying casesOn application, and the kernel checks that it is type correct. This gives the elaborator more flexibility to type projections (see magical.lean, also fixes #2697 and supersedes #2700 ), and also (possibly) improves the performance of type inference. But it does add handling of projection motives everywhere, and we need to find out if it is a perf win (or at least neutral).

The plan for this PR was shared ahead of time to @leodemoura . It rewrites .proj handling essentially everywhere it is done: in the kernel, in projections.cpp, in the app elaborator, in WHNF, and in Meta.Check.

[digama0]

!bench please?

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 07fcda5.
There were significant changes against commit fb0d024:

  Benchmark     Metric         Change
  ==============================================
- reduceMatch   instructions     1.7% (1466.5 σ)
- stdlib        maxrss           2.6%   (52.5 σ)

[leodemoura]

@digama0 Did it fix the cubic performance issue you mentioned last week?

[eric-wieser]

This docstring is outdated

[digama0]

@digama0 Did it fix the cubic performance issue you mentioned last week?

It's unclear. It eliminates this issue for inferType, but when checking the type you still have to do basically the same work and I'm not sure what the distribution is between inferring and checking in the kernel in practice. (The same thing happens in the elaborator.) It does fix a bug where the elaborator was not catching an issue that the kernel discovered but there are less invasive ways to fix that and I'm not sure it is enough motivation on its own. Unfortunately there are a lot of things to do just to get this to compile, you can't really test it without doing the full migration anyway.

Do we have any kernel stress tests? I'm not really sure the existing test suite is sufficient to evaluate kernel performance. I'll see if I can fix the remaining bugs and get a mathlib run (although that will almost certainly require more patching since every expr match is affected).

[leodemoura]

@digama0 Thanks for the additional information.

It's unclear. It eliminates this issue for inferType, but when checking the type you still have to do basically the same work and I'm not sure what the distribution is between inferring and checking in the kernel in practice.

The kernel performs a lot of checking. Inferring may happen too (e.g., while we are reducing Eq.rec), but I would be surprised if it is used more often than checking in the kernel.

It does fix a bug where the elaborator was not catching an issue that the kernel discovered but there are less invasive ways to fix that and I'm not sure it is enough motivation on its own.

A less invasive solution would be perfect for the bug fix.

Do we have any kernel stress tests?

Unfortunately, we don't have. We must need to increase the number of performance tests in core. I have been pushing for more benchmarks and tests in the core repo. It will help us to streamline PRs.

For this PR, an excellent first step is to construct an example that exhibits the cubic behavior you are concerned about.

[Vtec234]

Very minor Lean.Widget change LGTM!