perf: whnf projections during defeq

[gebner]

Fixes #1986. Kevin's example now takes 24ms instead of 1770ms to elaborate.

What this PR changes is that we now eagerly reduce projections during unification. When solving foo.1 =?= bar, we now try to reduce foo first. And if it reduces to a constructor ⟨a, b⟩, then we continue unifying a =?= bar. This actually makes the code simpler, since we went out of our way to avoid reducing projections before.

I am convinced that this is the right choice for type class instances. When unifying @Group.toMul G inst1 =?= @Group.toMul G inst2 we should never try to unify the Group G instances (which usually involves unifying all fields) when we only need the multiplication to be equal. And we have various other mechanisms to assign type class instance metavariables besides unification (which is super brittle): nested type class resolution, as well as type class resolution in the elaborator.

I can see some potential regressions with structures, for example when unifying (a, b).1 =?= (?m).1. But all tests still pass and mathlib4 builds with very minor changes:

• When elaborating foo (↑f) h then the coercion is not elaborated before elaborating h.
• rw [@foo] works while rw [foo] doesn't (only an issue with the notoriously flaky CovariantClass type class)
• Two sources in structure instances require a type annotation because they don't get an expected type.

[leodemoura]

I can see some potential regressions with structures, for example when unifying (a, b).1 =?= (?m).1.

Yes, and supporting this use case was pointed out as important in the past.

[leodemoura]

Let's discuss this issue in the next dev meeting. The file src/Lean/Meta/ExprDefEq.lean is very delicate.

[gebner]

!bench

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit bf45a27.
There were no significant changes against commit 5424386.

[leanprover-bot]

Here are the benchmark results for commit 9cc819b.
There were no significant changes against commit 6281217.

[gebner]

Add a test with heartbeat limit.

[bollu]

I can see some potential regressions with structures, for example when unifying (a, b).1 =?= (?m).1. But all tests still pass and mathlib4 builds with very minor changes...

I wanted to note that I suspect I will witness these regressions in opencompl/lean-mlir --- Zulip thread: performance of equality with projections/mutual,

AFAIU, our bug reports were why this commit was landed, which says:

feat: improve isDefEq for projections
When solving a.i =?= b.i, we first reduce a and b without using
delta reduction. If at least one become a structure, we reduce the
projection. Otherwise, we try to solve a =?= b, only reduce a.i
and b.i if it fails.

There are some more commits in the same vein:

• 14260f4
• 2196a35

All of which have to do with similar regressions.

[gebner]

I wanted to note that I suspect I will witness these regressions in opencompl/lean-mlir --- Zulip thread: performance of equality with projections/mutual,

Thanks for the pointer! It would be awesome if we could get an actual regression from lean-mlir.

Do you have any plans to update the Lean version in the repo though? There's been a lot of changes in the last three months, and it no longer builds.

[gebner]

FWIW, all the tests in the commits you've linked to (which are the examples from the Zulip thread) still work without any noticeable slowdown.

[gebner]

This PR has major performance improvements for mathlib: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20benchmark/near/320915653

[Kha]

I wanted to profile the total impact of this PR on mathlib4, but I'm seeing a TC inference failure in mathlib4 HEAD after merging this PR with master, but not before

$ nix build nale+github:leanprover-community/mathlib4#Mathlib --override-input lean github:leanprover/lean4/pull/2003/merge
warning: not writing modified lock file of flake 'nale+github:leanprover-community/mathlib4':
• Updated input 'lean':
    'github:leanprover/lean4-nightly/8cd9ce06843c9d42d6d6dc43d3e81e3b49dfc20f' (2023-01-11)
  → 'github:leanprover/lean4/a5a64f334ea37c52bb8adb1059c0cf9846ee06a9' (2023-01-12)
error: builder for '/nix/store/bl50jfdaa7apamij18dhlncyyywyl8qn-Mathlib.Algebra.GroupWithZero.Defs.drv' failed with exit code 1;
       last 2 log lines:
       > Mathlib/Algebra/GroupWithZero/Defs.lean:152:2: error: failed to synthesize instance
       >   IsLeftCancelMulZero ?m.6093
       For full logs, run 'nix log /nix/store/bl50jfdaa7apamij18dhlncyyywyl8qn-Mathlib.Algebra.GroupWithZero.Defs.drv'.
error: 1 dependencies of derivation '/nix/store/9c3xq2jifq29sfx2l26ygyh58g81wvm3-Mathlib-depRoot.drv' failed to build
$ nix build nale+github:leanprover-community/mathlib4#Mathlib --override-input lean github:leanprover/lean4
warning: not writing modified lock file of flake 'nale+github:leanprover-community/mathlib4':
• Updated input 'lean':
    'github:leanprover/lean4-nightly/8cd9ce06843c9d42d6d6dc43d3e81e3b49dfc20f' (2023-01-11)
  → 'github:leanprover/lean4/9b1f5c4df4d07c83bd7b692ed725dacaf829a763' (2023-01-12)

[gebner]

@Kha Some small changes to mathlib are required. https://github.com/leanprover-community/mathlib4/compare/bump2003?expand=1

[gebner]

rw [@foo] works while rw [foo] doesn't (only an issue with the notoriously flaky CovariantClass type class)

Shorter repro:

#check (add_tsub_cancel_left)

What's happening here is that nested TC synthesis behaves differently than non-nested TC synthesis. Usually TC synthesis aborts when it would need to assign a metavariable but can't (e.g. we're synthesizing an instance Group ?m_1 by applying an instance Group Rat). But if we encounter such a situation inside nested TC synthesis inside unification inside TC synthesis, then we don't abort and instead pretend that the instance doesn't exist.

[Vierkantor]

I'm happy to let you know that these changes fix a pair of timeouts in code ported from Lean 3: leanprover-community/mathlib4#1587. It's great service to have the fixing PR out before I run into the issue :D

[gebner]

There is an issue where this PR doesn't help, namely if one of the sides is a projection of a metavariable, because then the projections don't reduce:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20goes.20haywire/near/322785742

This is now #2055