bump to 2023-02-06

Stream: mathlib4

[Johan Commelin]

This bump will bring https://github.com/leanprover/lean4/pull/2093 to mathlib.

First error is in Data.Rat.Defs:

instance isDomain : IsDomain ℚ :=
  NoZeroDivisors.to_isDomain _
-- failed to synthesize
--   NoZeroDivisors ℚ
-- (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option
-- synthInstance.maxHeartbeats <num>' to set the limit)

[Eric Wieser]

Do you have a branch/PR for this already?

[Johan Commelin]

!4#2105 -- bump-2023-02-06

[Eric Wieser]

I'll have a look once the cache is ready

[Johan Commelin]

Failing trace:

[Meta.synthInstance] ✅ Ring ℚ ▶

[Meta.isDefEq] ✅ ?m.28264 =?= CommRing.toRing ▶

[Meta.synthInstance] ✅ Nontrivial ℚ ▶

[Meta.isDefEq] ✅ ?m.28265 =?= CommGroupWithZero.toNontrivial ▶

[Meta.synthInstance] 💥 NoZeroDivisors ℚ ▼
  [] new goal NoZeroDivisors ℚ ▶
  [] ❌ apply @CanonicallyOrderedCommSemiring.toNoZeroDivisors to NoZeroDivisors ℚ ▶
  [] ❌ apply @LinearOrderedRing.noZeroDivisors to NoZeroDivisors ℚ ▶

[Meta.isDefEq] ✅ IsDomain ℚ =?= IsDomain ℚ ▶

[Meta.synthInstance] 💥 NoZeroDivisors ℚ ▼
  [] new goal NoZeroDivisors ℚ ▶
  [] ❌ apply @CanonicallyOrderedCommSemiring.toNoZeroDivisors to NoZeroDivisors ℚ ▶
  [] ❌ apply @LinearOrderedRing.noZeroDivisors to NoZeroDivisors ℚ ▶

[Meta.isDefEq] ✅ IsDomain ℚ =?= IsDomain ℚ

Start of succesful trace (with maxHeartbeats):

[Meta.synthInstance] ✅ Ring ℚ ▶

[Meta.isDefEq] ✅ ?m.28264 =?= CommRing.toRing ▶

[Meta.synthInstance] ✅ Nontrivial ℚ ▶

[Meta.isDefEq] ✅ ?m.28265 =?= CommGroupWithZero.toNontrivial ▶

[Meta.synthInstance] ✅ NoZeroDivisors ℚ ▼
  [] new goal NoZeroDivisors ℚ ▶
  [] ❌ apply @CanonicallyOrderedCommSemiring.toNoZeroDivisors to NoZeroDivisors ℚ ▼
    [tryResolve] ❌ NoZeroDivisors ℚ ≟ NoZeroDivisors ?m.29337 ▼
      [isDefEq] ❌ NoZeroDivisors ℚ =?= NoZeroDivisors ?m.29337 ▼
        [] ✅ ℚ =?= ?m.29337 ▶
        [synthInstance] ❌ CanonicallyOrderedCommSemiring ℚ ▼
          [] no instances for CanonicallyOrderedCommSemiring ℚ ▼
            [instances] #[]
        [] ❌ NonUnitalNonAssocRing.toMul =?= CanonicallyOrderedCommSemiring.toMul ▼
          [] ❌ NonAssocRing.toNonUnitalNonAssocRing.2 =?= ?m.29338.2 ▼
            [] ❌ NonAssocRing.toNonUnitalNonAssocRing =?= ?m.29338 ▼
              [] NonAssocRing.toNonUnitalNonAssocRing [nonassignable] =?= ?m.29338 [assignable]
              [] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocRing ℚ ▼
                [] ❌ CanonicallyOrderedCommSemiring =?= NonUnitalNonAssocRing
                [onFailure] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocRing ℚ
                [onFailure] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocRing ℚ
              [] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocRing ℚ
            [] ❌ NonUnitalNonAssocSemiring.toMul =?= ?m.29338.2 ▼
              [] ❌ NonUnitalSemiring.toNonUnitalNonAssocSemiring.2 =?= ?m.29338.2 ▼
                [] ❌ NonUnitalSemiring.toNonUnitalNonAssocSemiring =?= ?m.29338 ▼
                  [] NonUnitalSemiring.toNonUnitalNonAssocSemiring [nonassignable] =?= ?m.29338 [assignable]
                  [] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocSemiring ℚ ▼
                    [] ❌ CanonicallyOrderedCommSemiring =?= NonUnitalNonAssocSemiring
                    [onFailure] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocSemiring ℚ
                    [onFailure] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocSemiring ℚ
                  [] ❌ CanonicallyOrderedCommSemiring ℚ =?= NonUnitalNonAssocSemiring ℚ
                [] ❌ { mul := fun x x_1 => x * x_1 } =?= ?m.29338.2 ▼
                  [] ✅ Mul ℚ =?= Mul ℚ ▼
                    [] ✅ ℚ =?= ℚ
                  [] ❌ Mul.mul =?= fun x x_1 => x * x_1 ▼
                    [] ❌ fun x x_1 => x * x_1 =?= fun a => Mul.mul a ▼
                      [] ✅ ℚ =?= ℚ
                      [] ❌ fun x => x✝ * x =?= Mul.mul x✝ ▼
                        [] ❌ fun x => x✝ * x =?= fun a => Mul.mul x✝ a ▼
                          [] ✅ ℚ =?= ℚ
                          [] ❌ x✝¹ * x✝ =?= Mul.mul x✝¹ x✝ ▼
                            [] ❌ Mul.mul x✝¹ x✝ =?= Mul.mul x✝¹ x✝ ▼
                              [] ✅ x✝¹ =?= x✝¹
                              [] ✅ x✝ =?= x✝
                              [] ✅ ℚ =?= ℚ
                              [] ❌ Rat.instMulRat =?= ?m.29338.2 ▼
                                [] ❌ { mul := Rat.mul } =?= ?m.29338.2 ▼
                                  [] ✅ Mul ℚ =?= Mul ℚ ▶
                                  [] ❌ Mul.mul =?= Rat.mul ▼
                                    [] ❌ ?m.29338.2.1 =?= Rat.mul ▼
                                      [onFailure] ❌ ?m.29338.2.1 =?= Rat.mul
                                  [onFailure] ❌ { mul := Rat.mul } =?= ?m.29338.2
                              [] ❌ Rat.instMulRat.1 x✝¹ x✝ =?= ?m.29338.2.1 x✝¹ x✝ ▼
                                [] ❌ Rat.mul x✝¹ x✝ =?= ?m.29338.2.1 x✝¹ x✝ ▼
                                  [] ❌ Rat.mul =?= ?m.29338.2.1 ▼
                                    [onFailure] ❌ Rat.mul =?= ?m.29338.2.1
                                  [onFailure] ❌ Rat.mul x✝¹ x✝ =?= ?m.29338.2.1 x✝¹ x✝
                                  [onFailure] ❌ Rat.mul x✝¹ x✝ =?= ?m.29338.2.1 x✝¹ x✝
                  [onFailure] ❌ { mul := fun x x_1 => x * x_1 } =?= ?m.29338.2
        [onFailure] ❌ NoZeroDivisors ℚ =?= NoZeroDivisors ?m.29337
        [onFailure] ❌ NoZeroDivisors ℚ =?= NoZeroDivisors ?m.29337
  [] ❌ apply @LinearOrderedRing.noZeroDivisors to NoZeroDivisors ℚ ▼
    [tryResolve] ❌ NoZeroDivisors ℚ ≟ NoZeroDivisors ?m.29351 ▼
      [isDefEq] ❌ NoZeroDivisors ℚ =?= NoZeroDivisors ?m.29351 ▼
        [] ✅ ℚ =?= ?m.29351 ▼
          [] ℚ [nonassignable] =?= ?m.29351 [assignable]
          [] ✅ Type ?u.29335 =?= Type
        [] ❌ NonUnitalNonAssocRing.toMul =?= NonUnitalNonAssocRing.toMul ▼
          [] ✅ ℚ =?= ℚ
          [] ❌ NonAssocRing.toNonUnitalNonAssocRing =?= NonAssocRing.toNonUnitalNonAssocRing ▼
            [] ✅ ℚ =?= ℚ
            [] ❌ Ring.toNonAssocRing =?= Ring.toNonAssocRing ▼
              [] ✅ ℚ =?= ℚ
              [] ❌ CommRing.toRing =?= StrictOrderedRing.toRing ▼
                [] ❌ Rat.commRing.1 =?= LinearOrderedRing.toStrictOrderedRing.1 ▼
                  [] ❌ Rat.commRing =?= LinearOrderedRing.toStrictOrderedRing ▼
                    [] ❌ CommRing.mk Rat.mul_comm =?= LinearOrderedRing.toStrictOrderedRing ▼
                      [] ❌ StrictOrderedRing ℚ =?= CommRing ℚ ▼
                        [] ❌ StrictOrderedRing =?= CommRing
                        [onFailure] ❌ StrictOrderedRing ℚ =?= CommRing ℚ
                        [onFailure] ❌ StrictOrderedRing ℚ =?= CommRing ℚ
                      [] ❌ CommRing.mk Rat.mul_comm =?= ?m.29352.1 ▼
                        [] ❌ StrictOrderedRing ℚ =?= CommRing ℚ ▼
                          [] ❌ StrictOrderedRing =?= CommRing
                          [onFailure] ❌ StrictOrderedRing ℚ =?= CommRing ℚ
                          [onFailure] ❌ StrictOrderedRing ℚ =?= CommRing ℚ
                        [onFailure] ❌ CommRing.mk Rat.mul_comm =?= ?m.29352.1
                  [] ❌ Ring.mk zsmulRec Rat.add_left_neg =?= LinearOrderedRing.toStrictOrderedRing.1 ▼
                    [] ✅ Ring ℚ =?= Ring ℚ
                    [] ❌ Ring.toSemiring =?= Semiring.mk Rat.one_mul Rat.mul_one npowRec ▼
                      [] ✅ Semiring ℚ =?= Semiring ℚ
                      [] ❌ Semiring.toNonUnitalSemiring =?= NonUnitalSemiring.mk Rat.mul_assoc ▼
                        [] ✅ NonUnitalSemiring ℚ =?= NonUnitalSemiring ℚ
                        [] ❌ NonUnitalSemiring.toNonUnitalNonAssocSemiring =?= NonUnitalNonAssocSemiring.mk Rat.mul_add Rat.add_mul Rat.zero_mul
                              Rat.mul_zero ▼
                          [] ✅ NonUnitalNonAssocSemiring ℚ =?= NonUnitalNonAssocSemiring ℚ
                          [] ❌ NonUnitalNonAssocSemiring.toAddCommMonoid =?= AddCommMonoid.mk Rat.add_comm ▼
                            [] ✅ AddCommMonoid ℚ =?= AddCommMonoid ℚ
                            [] ❌ AddCommMonoid.toAddMonoid =?= AddMonoid.mk Rat.zero_add Rat.add_zero nsmulRec ▼
                              [] ✅ AddMonoid ℚ =?= AddMonoid ℚ
                              [] ❌ AddMonoid.toAddSemigroup =?= AddSemigroup.mk Rat.add_assoc ▼
                                [] ✅ AddSemigroup ℚ =?= AddSemigroup ℚ
                                [] ❌ AddSemigroup.toAdd =?= { add := fun x x_1 => x + x_1 } ▼
                                  [] ✅ Add ℚ =?= Add ℚ
                                  [] ❌ Add.add =?= fun x x_1 => x + x_1 ▶
                                  [] ❌ AddMonoid.toAddSemigroup.1 =?= { add := fun x x_1 => x + x_1 } ▼

[Johan Commelin]

I don't if this is now 2003 kicking in?

[Eric Wieser]

I was able to fix one of the 8 timeouts by locally bumping the set_option synthInstance.maxHeartbeat setting; maybe that's a reasonable thing to do while waiting for lean4#2003

[Johan Commelin]

I'm doing that in a score of files now

[Johan Commelin]

$ git diff --stat
 Mathlib/Algebra/Module/Basic.lean            | 1 +
 Mathlib/Algebra/Module/LinearMap.lean        | 3 +++
 Mathlib/Algebra/Order/Archimedean.lean       | 4 ++++
 Mathlib/Algebra/PUnitInstances.lean          | 1 +
 Mathlib/Algebra/Ring/Prod.lean               | 1 +
 Mathlib/Algebra/Star/SelfAdjoint.lean        | 2 ++
 Mathlib/Data/Fin/Basic.lean                  | 4 ++++
 Mathlib/Data/Int/AbsoluteValue.lean          | 1 +
 Mathlib/Data/Int/GCD.lean                    | 1 +
 Mathlib/Data/Int/Parity.lean                 | 4 ++++
 Mathlib/Data/Multiset/Basic.lean             | 1 +
 Mathlib/Data/Nat/Bitwise.lean                | 2 ++
 Mathlib/Data/Nat/ModEq.lean                  | 1 +
 Mathlib/Data/Rat/Defs.lean                   | 3 ++-
 Mathlib/Data/ZMod/Defs.lean                  | 1 +
 Mathlib/GroupTheory/GroupAction/ConjAct.lean | 1 +
 Mathlib/RingTheory/Congruence.lean           | 3 +++
 Mathlib/Tactic/Abel.lean                     | 1 +
 Mathlib/Tactic/Linarith/Parsing.lean         | 3 +++
 Mathlib/Tactic/Positivity/Basic.lean         | 1 +
 20 files changed, 38 insertions(+), 1 deletion(-)

[Johan Commelin]

But this is clearly not sustainable.

[Johan Commelin]

I don't think we should merge this PR with all those maxHeartbeats.

[Eric Wieser]

I'd argue that having slow typeclass resolution is better than having typeclass resolution that never works in some cases (as in mathlib4 master); so if it unblocks the port, I think adding these while waiting for 2003 is reasonable

[Johan Commelin]

theorem _root_.MulAut.conjNormal_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑(MulAut.conjNormal g h) = g * h * g⁻¹ :=
/-
function expected at
  ↑MulAut.conjNormal g
term has type
  (fun x => MulAut { x // x ∈ ?m.294870 }) g
-/

[Johan Commelin]

:up: is not solved by increasing heartbeats

[Eric Wieser]

docs4#MulAut.conjNormal

[Eric Wieser]

Does (MulAut.conjNormal g : MulAut H) h work in place of MulAut.conjNormal g h?

[Johan Commelin]

yes it does, and it's quite fast

[Johan Commelin]

do you understand why this change is needed by the bump?

[Eric Wieser]

I would guess that it found a different instance to the one it did before, and the new one is less helpful for unification

[Eric Wieser]

And that somehow, that unification failure is preventing the CoeFun instance from firing; maybe because the metavariable wasn't filled in

[Eric Wieser]

We have similar problems in mathlib3 where sometimes map_mul F x y fails but map_mul (F : some_annotation) x y works

[Eric Wieser]

It hasn't happened for has_coe_to_fun in Lean3, but Lean4 is sufficiently different that it wouldn't be too surprising for a similar thing to occur there

[Johan Commelin]

I pushed a commit that changes 24 files. It doesn't look like I'm almost done.

[Johan Commelin]

This looks like serious problems to me.

[Eric Wieser]

Can we change the default hearbeats globally?

[Johan Commelin]

I don't like that idea. mathlib 4 shouldn't be slower than mathlib 3.

[Johan Commelin]

I think we should fix these problems before pouring more person-weeks into the port.

[Eric Wieser]

The default hearbeat limit in lean4 is 5x smaller than the value in Lean3 I think

[Eric Wieser]

Johan Commelin said:

I think we should fix these problems before pouring more person-weeks into the port.

My worry is that if we don't make these workarounds, people will make worse workaround when porting that are harder to undo

[Johan Commelin]

Order.Partition.Finpartition is really bad, around L525. With

set_option maxHeartbeats 0 in -- Porting note: this is too slow
set_option synthInstance.maxHeartbeats 0 in -- Porting note: this is too slow

it just sits there and blankly stares you in the face.

[Eric Wieser]

Is there a wiki page on diagnosing these timeouts (what trace options to set, how to expand the tree view entirely, etc...)

[Johan Commelin]

Not that I know of

[Reid Barton]

I think what's happening is the version bump is allowing TC synthesis to explore some options that it previously couldn't, and then other TC issues is making these branches very expensive

[Johan Commelin]

Order.Partition.Finpartition has now been staring blankly in my face for > 20 minutes.

[Johan Commelin]

So this PR is very non-mergeable.

[Johan Commelin]

Yuchai!

set_option synthInstance.maxHeartbeats 0 in -- Porting note: this is too slow
open Classical in -- Porting note: haha

works!

[Johan Commelin]

$ git diff master... --stat
 Mathlib/Algebra/BigOperators/Finsupp.lean     |  2 +-
 Mathlib/Algebra/BigOperators/Intervals.lean   |  2 ++
 Mathlib/Algebra/DirectSum/Basic.lean          |  2 ++
 Mathlib/Algebra/GeomSum.lean                  |  2 ++
 Mathlib/Algebra/Module/Basic.lean             |  1 +
 Mathlib/Algebra/Module/LinearMap.lean         |  7 +++++++
 Mathlib/Algebra/Module/Submodule/Basic.lean   |  2 ++
 Mathlib/Algebra/Module/ULift.lean             |  4 ++++
 Mathlib/Algebra/Order/Archimedean.lean        |  4 ++++
 Mathlib/Algebra/PUnitInstances.lean           |  1 +
 Mathlib/Algebra/Periodic.lean                 |  4 ++++
 Mathlib/Algebra/Quandle.lean                  |  2 ++
 Mathlib/Algebra/Ring/Prod.lean                |  1 +
 Mathlib/Algebra/Star/SelfAdjoint.lean         |  2 ++
 Mathlib/Data/Fin/Basic.lean                   |  4 ++++
 Mathlib/Data/Finsupp/Order.lean               |  2 ++
 Mathlib/Data/Int/AbsoluteValue.lean           |  1 +
 Mathlib/Data/Int/GCD.lean                     |  1 +
 Mathlib/Data/Int/Parity.lean                  |  4 ++++
 Mathlib/Data/Multiset/Basic.lean              |  1 +
 Mathlib/Data/Nat/Bitwise.lean                 |  2 ++
 Mathlib/Data/Nat/ModEq.lean                   |  1 +
 Mathlib/Data/Rat/Defs.lean                    |  3 ++-
 Mathlib/Data/Real/Basic.lean                  |  1 +
 Mathlib/Data/Sign.lean                        |  6 ++++++
 Mathlib/Data/UInt.lean                        |  2 ++
 Mathlib/Data/ZMod/Defs.lean                   |  1 +
 Mathlib/GroupTheory/GroupAction/ConjAct.lean  | 10 +++++++---
 Mathlib/GroupTheory/Subgroup/Pointwise.lean   |  1 +
 Mathlib/GroupTheory/Submonoid/Pointwise.lean  |  2 ++
 Mathlib/Order/Partition/Finpartition.lean     | 16 ++++++++++------
 Mathlib/RingTheory/Congruence.lean            |  3 +++
 Mathlib/RingTheory/Subsemiring/Pointwise.lean |  3 ++-
 Mathlib/Tactic/Abel.lean                      |  1 +
 Mathlib/Tactic/Linarith/Parsing.lean          |  3 +++
 Mathlib/Tactic/Positivity/Basic.lean          |  1 +
 lean-toolchain                                |  2 +-
 37 files changed, 94 insertions(+), 13 deletions(-)

[Johan Commelin]

This branch now builds.... :turtle: :turtle: :turtle:

[Johan Commelin]

cc @Gabriel Ebner you might be interested in !4#2105 (aka bump-2023-02-06). It is the mathlib fallout of the eta for structures PR.

[Johan Commelin]

Ooh noes! CI is now complaining about a lot of linting failures because of timeouts.
https://github.com/leanprover-community/mathlib4/actions/runs/4104664586/jobs/7080448378

[Kevin Buzzard]

Do you dare try merging master into 2003 and seeing if it helps?

[Johan Commelin]

Do you mean merging 2003 into the bump branch?

[Johan Commelin]

I would have to figure out how to build my own Lean 4.

[Kevin Buzzard]

Yeah I mean maybe 2003 helps

[Kevin Buzzard]

I'm just an optimist

[Reid Barton]

I think there is a decent chance, because there were some failures from 2003 which might be fixed by the new patch.

[Johan Commelin]

I'll see if I can convince my computer to build 2003 (after merging master into it) and then convince elan to use that build

[Johan Commelin]

Merging master into leanprover/lean4#2003 should be done anyway, right?

[Kevin Buzzard]

Oh I guess

[Johan Commelin]

/me doesn't have a working cmake :sad:

[Reid Barton]

I can give it a shot.

[Johan Commelin]

nix-shell -A nix seems to work (-;

[Johan Commelin]

Ok, I have a local build of (2003 + lean4 master). How should I instruct elan to use that build to build mathlib 4?

[Jannis Limperg]

# set up the Lean 4 toolchain
elan toolchain link lean4-master build/release/stage1
# use the toolchain as an override in the mathlib4 directory
elan override set lean4-master

[Johan Commelin]

aha, thanks!

[Johan Commelin]

hmm, nix probably has different ideas about where stage1 ends up

[Jannis Limperg]

Ah yes, sorry, I was assuming the cmake build.

[Jannis Limperg]

I can't find instructions in the manual for using a Nix-based Lean 4 build to build a project. However, you might be able to get a working cmake via nix-shell.

[Johan Commelin]

anyway, 2003 seems to build fine after merging master. But the PR is from Gabriel's fork, so I can't update the PR anyways.

[Johan Commelin]

And it's about time I start catching a train, so I don't think I can do a mathlib build with that local toolchain today either.

[Reid Barton]

There are still the same errors.

[Reid Barton]

I think they are likely related to #2055

[Reid Barton]

hmm, actually probably not

[Johan Commelin]

ftr leanprover/lean4#2055

[Kevin Buzzard]

@Gabriel Ebner is there any way I can help making lean4#2055 easier to diagnose at the dev end?

[Reid Barton]

What's going on in Data.Rat.Defs:

1. We are trying to process instance isDomain : IsDomain ℚ := NoZeroDivisors.to_isDomain _
2. So we need lemma NoZeroDivisors.to_isDomain [Ring α] [h : Nontrivial α] [NoZeroDivisors α] : IsDomain α := [...]
3. So we need Nontrivial ℚ.
4. Now we try out instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α := [...]. Note: Of course ℚ actually does have characteristic zero, but we don't know that at this point of Data.Rat.Defs.
5. Next we try instance (priority := 100) StrictOrderedSemiring.to_charZero [StrictOrderedSemiring α] : CharZero α. Note however that CharZero has type class CharZero (R) [AddMonoidWithOne R] : Prop, so it has an implicit instance argument derived from the StrictOrderedSemiring one. At this point we also don't know anything about the compatibility of the ring structure and ordering of ℚ.
6. To apply this instance we unify @CharZero ℚ (AddMonoidWithOne instance for ℚ) =?= @CharZero ?t (... (?i : StrictOrderedSemiring ℚ)). We deduce ?t = ℚ and then try to make some more reductions but eventually realize we need to synthesize ?i.
7. This fails quickly because we don't have this instance yet. But, that doesn't cause the defeq problem we were working on to fail.
8. Now it spends a huge amount of time trying to solve a failing defeq problem for some reason.

[Reid Barton]

There is probably a lot of room for improvement here but I think the most unexpected thing here is in 7

[Kevin Buzzard]

Is it hard to minimise 7 and 8?

[Eric Wieser]

What instance are we expecting to find here?

[Reid Barton]

It never gets that far, so I don't know, but I trust that it follows from CommGroupWithZero somehow.

[Reid Barton]

Kevin Buzzard said:

Is it hard to minimise 7 and 8?

class A (α : Type) where
  a : α → α → α

class B (α : Type) extends A α where
  b : ∀ x y, a x y = a y x

class A' (α : Type) where
  a' : α → α → α

instance {α : Type} [A' α] : A α where
  a x y := id (A'.a' (id x) (id y))

class C (α : Type) [A α] where
  c : α → α → α

instance I {α : Type} [B α] : C α where
  c x _y := x

theorem T (α : Type) [A α] [C α] (x : α) : x = x := rfl

set_option pp.all true in
set_option trace.Meta.isDefEq true in
set_option trace.Meta.synthInstance true in
theorem U (α : Type) [i : A' α] (x : α) : x = x := T α x

Relevant section of trace output

[Meta.synthInstance] ❌ @C α (@instA α i)
  [Meta.synthInstance] new goal @C α (@instA α i)
    [Meta.synthInstance.instances] #[@I]
  [Meta.synthInstance] ❌ apply @I to @C α (@instA α i)
    [Meta.synthInstance.tryResolve] ❌ @C α (@instA α i) ≟ @C ?m.305 (@B.toA ?m.305 ?m.306)
      [Meta.isDefEq] ❌ @C α (@instA α i) =?= @C ?m.305 (@B.toA ?m.305 ?m.306)
        [Meta.isDefEq] ✅ α =?= ?m.305
          [Meta.isDefEq] α [nonassignable] =?= ?m.305 [assignable]
          [Meta.isDefEq] ✅ Type =?= Type
        [Meta.synthInstance] ❌ B α
          [Meta.synthInstance] no instances for B α
            [Meta.synthInstance.instances] #[]
        [Meta.isDefEq] ❌ @instA α i =?= @B.toA α ?m.306
          [Meta.isDefEq] ❌ @A.mk α fun (x y : α) =>
                @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= @B.toA α ?m.306
            [Meta.isDefEq] ✅ A α =?= A α
            [Meta.isDefEq] ❌ @A.a α
                  (@B.toA α ?m.306) =?= fun (x y : α) => @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y))
              [Meta.isDefEq] ❌ fun (x y : α) =>
                    @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= fun (a : α) => @A.a α (@B.toA α ?m.306) a
                [Meta.isDefEq] ✅ α =?= α
                [Meta.isDefEq] ❌ fun (y : α) =>
                      @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= @A.a α (@B.toA α ?m.306) x
                  [Meta.isDefEq] ❌ fun (y : α) =>
                        @id.{1} α
                          (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= fun (a : α) => @A.a α (@B.toA α ?m.306) x a
                    [Meta.isDefEq] ✅ α =?= α
                    [Meta.isDefEq] ❌ @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= @A.a α (@B.toA α ?m.306) x y
                      [Meta.isDefEq] ❌ @A'.a' α i (@id.{1} α x) (@id.{1} α y) =?= @A.a α (@B.toA α ?m.306) x y
                        [Meta.isDefEq] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= (@B.toA α ?m.306).1 x y
                          [Meta.isDefEq] ❌ i.1 =?= (@B.toA α ?m.306).1
                            [Meta.isDefEq.onFailure] ❌ i.1 =?= (@B.toA α ?m.306).1
                          [Meta.isDefEq.onFailure] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= (@B.toA α ?m.306).1 x y
                          [Meta.isDefEq.onFailure] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= (@B.toA α ?m.306).1 x y
            [Meta.isDefEq] ❌ @A.mk α fun (x y : α) => @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= ?m.306.1
              [Meta.isDefEq] ✅ A α =?= A α
                [Meta.isDefEq] ✅ α =?= α
              [Meta.isDefEq] ❌ @A.a α ?m.306.1 =?= fun (x y : α) => @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y))
                [Meta.isDefEq] ❌ fun (x y : α) =>
                      @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= fun (a : α) => @A.a α ?m.306.1 a
                  [Meta.isDefEq] ✅ α =?= α
                  [Meta.isDefEq] ❌ fun (y : α) =>
                        @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= @A.a α ?m.306.1 x
                    [Meta.isDefEq] ❌ fun (y : α) =>
                          @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= fun (a : α) => @A.a α ?m.306.1 x a
                      [Meta.isDefEq] ✅ α =?= α
                      [Meta.isDefEq] ❌ @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= @A.a α ?m.306.1 x y
                        [Meta.isDefEq] ❌ @A'.a' α i (@id.{1} α x) (@id.{1} α y) =?= @A.a α ?m.306.1 x y
                          [Meta.isDefEq] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= ?m.306.1.1 x y
                            [Meta.isDefEq] ❌ i.1 =?= ?m.306.1.1
                              [Meta.isDefEq.onFailure] ❌ i.1 =?= ?m.306.1.1
                            [Meta.isDefEq.onFailure] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= ?m.306.1.1 x y
                            [Meta.isDefEq.onFailure] ❌ i.1 (@id.{1} α x) (@id.{1} α y) =?= ?m.306.1.1 x y
              [Meta.isDefEq.onFailure] ❌ @A.mk α fun (x y : α) =>
                    @id.{1} α (@A'.a' α i (@id.{1} α x) (@id.{1} α y)) =?= ?m.306.1
        [Meta.isDefEq.onFailure] ❌ @C α (@instA α i) =?= @C ?m.305 (@B.toA ?m.305 ?m.306)
        [Meta.isDefEq.onFailure] ❌ @C α (@instA α i) =?= @C ?m.305 (@B.toA ?m.305 ?m.306)

[Johan Commelin]

So this is unrelated to lean4#2003, right?

[Johan Commelin]

Is it one of the other issues that Kevin has created over the past few weeks?

[Johan Commelin]

Or is it something new altogether?

[Reid Barton]

I don't recognize it as an existing issue

[Gabriel Ebner]

From what I can tell this is a somewhat unfortunate collaboration with the 2003 issue.

1. Due to 2003, we get lots of unification problems like (... : StrictOrderedRing ℚ).1 =?= Ring.mk ...
2. Structure eta then thinks "maybe we can solve it by adding another projection" and generates the new problem (... : StrictOrderedRing ℚ).1.toSemiring =?= ...
3. Note that .1 is a primitive projection and .toRing is a definition, so this cleverly disables caching.

[Reid Barton]

Well, it probably has something similarity to 2055 because that one also involves a failing defeq test doing a lot of work.

[Kevin Buzzard]

I was inspired by this conversation to try and minimise 2055 a bit more, and think I succeeded. I've also posted on github; hopefully this new version is much easier to grok. Reid can you minimise even further? I don't know how to remove simp but maybe you do.

class A1 (M : Type u) extends Mul M

class A2 (M : Type u) extends A1 M

class A3 (M : Type u) extends A2 M

class A4 (M : Type u) extends A3 M

class B1 (M : Type u) extends Mul M

class CommRing (M : Type u) extends B1 M, A4 M

-- given `CommRing R` there are two distinct routes to `Mul R`:
-- CommRing -> B1 -> Mul
-- CommRing -> A4 -> A3 -> A2 -> A1 -> Mul

-- random extra bad class plus simp lemma which causes all the trouble
class BadClass (M : Type u) extends A4 M
@[simp] theorem mul_right_eq_self {M : Type u} [inst : BadClass M] {a b c : M} :
    a * b = a ↔ b = c := sorry

set_option trace.Meta.synthInstance true

variable {R : Type _} [i : CommRing R] (a b c : R)
example :
  -- use the two multiplications to say a * b = c ↔ a * b = c
  (@HMul.hMul R R R
    (@instHMul R (@A1.toMul R (@A2.toA1 R (@A3.toA2 R (@A4.toA3 R (@CommRing.toA4 R i))))))
    a b) = c ↔
  (@HMul.hMul R R R
    (@instHMul R (@B1.toMul R (@CommRing.toB1 R i)))
    a b) = c := by
  -- ⊢ a * b = c ↔ a * b = c
  -- exact Iff.rfl -- works
  simp
/-
[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶
...
307 times
-/

[Reid Barton]

I still think it is surprising that we get to step 8 at all. It breaks the conception of the TC system as a little Prolog language. In addition to the facts that are added as instances, there's whatever facts Lean can "deduce" by unification.

[Johan Commelin]

@Gabriel Ebner Are you saying that adding 2003 to the current situation is only going to make things worse :fear: ?

[Kevin Buzzard]

I spent a lot of time trying to game the numbers. Increasing the B string does very little. Increasing the A string does lots. The optimal (in the sense that it makes the number of failures largest) place to put the bad class is coming off the last A class. No idea if this helps.

[Reid Barton]

@Kevin Buzzard Did you try using mul_right_eq_self as the whole proof?

[Gabriel Ebner]

Johan Commelin said:

Gabriel Ebner Are you saying that adding 2003 to the current situation is only going to make things worse :fear: ?

No completely the opposite.

[Reid Barton]

My messages this evening are with the patch for 2003 applied on top of current master.

[Johan Commelin]

Ah, then my interpretation of your use of the word "unfortunate" was somewhat unfortunate.

[Reid Barton]

If we don't have eta for classes then the failing TC problems will fail faster. Here, that's good.

[Reid Barton]

Or not even "the failing TC problems", but rather any sort of failing unification

[Johan Commelin]

Ooh, aha. So you're saying that yesterday's PR is making the 2003 situation worse?

[Johan Commelin]

Or not even that?

[Gabriel Ebner]

Yes, the two issues have great synergies.

[Gabriel Ebner]

Or at least, the issue which would be fixed by 2003 makes yesterday's PR much worse.

[Reid Barton]

I will test but I think the issue with Data.Rat.Defs discussed here is basically the same whether or not 2003 is included.

[Kevin Buzzard]

I feel like we're making progress in our understanding though, which is great.

[Reid Barton]

The tricky thing about these issues is that there are many opportunities to do better on each one, but also each change we could make to Lean affects many other things.

[Reid Barton]

Currently, in Lean 4, if you apply a lemma that has an [instance] argument, does Lean insist on TC synthesizing the argument, or can it solve for it by unification?

[Thomas Murrills]

I believe it insists on TC, at least based on the fact that changing [Foo] to {_ : Foo} changes whether some simp lemmas are able to be applied (TC fails but unification succeeds) (assuming no recent lean 4 PR’s have changed this, and assuming this is not actually a property of simp)

[Reid Barton]

In that case it really doesn't make sense to me that the TC synthesis failure in step 7 doesn't end the defeq test immediately.

[Reid Barton]

I looked at 2055 more closely and actually it is the same as what we are seeing here.

[Gabriel Ebner]

Thank you all and Johan in particular for all the effort in adapting mathlib to the change. It was very helpful to see where things break. I have reverted lean4#2093 for the moment so that we can continue to deploy other bugfixes.