Performance issue with `CompleteBooleanAlgebra`

Stream: mathlib4

[Anatole Dedecker]

There seems to be a performance issue with CompleteDistribLattice(ported in mathlib4#1107) that I don't understand: all three instances of it declared in this file take a lot of time (I'd say more than everything else in the file) to compile. If that matters, note that all of them are declared as { someFrameInstance, someCoframeInstance with }. I tried changing the definition of CompleteDistribLattice to just extend both Frame and Coframe, but it didn't make things any better.
Is this related to the fact that there are a lot of common fields to Frame and Coframe?

[Kevin Buzzard]

That's interesting! It's precisely the instances of CompleteDistribLattice which are orders of magnitude slower than anything else in the file.

[Kevin Buzzard]

I'll try to minimise one of them, I have some Lean time right now

[Kevin Buzzard]

I think the hold-up in the last example might be this:

@[reducible]
protected def Function.Injective.completeDistribLattice [HasSup α] [HasInf α] [SupSet α] [InfSet α]
    [Top α] [Bot α] [CompleteDistribLattice β] (f : α → β) (hf : Function.Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_supₛ : ∀ s, f (supₛ s) = ⨆ a ∈ s, f a) (map_infₛ : ∀ s, f (infₛ s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteDistribLattice α :=
  let foo : Frame α := hf.frame f map_sup map_inf map_supₛ map_infₛ map_top map_bot
  let bar : Coframe α := hf.coframe f map_sup map_inf map_supₛ map_infₛ map_top map_bot
  have moo : ∀ (a : α) (s : Set.{u} α),
    @LE.le.{u} α
      (@Preorder.toLE.{u} α
        (@PartialOrder.toPreorder.{u} α
          (@SemilatticeSup.toPartialOrder.{u} α
            (@Lattice.toSemilatticeSup.{u} α
              (@CompleteLattice.toLattice.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar))))))
      (@infᵢ.{u, u + 1} α (@CompleteLattice.toInfSet.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar)) α
        fun (b : α) ↦
          @infᵢ.{u, 0} α (@CompleteLattice.toInfSet.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar))
            (@Membership.mem.{u, u} α (Set.{u} α) (@Set.instMembershipSet.{u} α) b s)
            fun (h : @Membership.mem.{u, u} α (Set.{u} α) (@Set.instMembershipSet.{u} α) b s) ↦
              @HasSup.sup.{u} α
                (@SemilatticeSup.toHasSup.{u} α
                  (@Lattice.toSemilatticeSup.{u} α
                    (@CompleteLattice.toLattice.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar))))
                a b)
      (@HasSup.sup.{u} α
        (@SemilatticeSup.toHasSup.{u} α
          (@Lattice.toSemilatticeSup.{u} α
            (@CompleteLattice.toLattice.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar))))
        a (@InfSet.infₛ.{u} α (@CompleteLattice.toInfSet.{u} α (@Order.Coframe.toCompleteLattice.{u} α bar)) s)) =
    @LE.le.{u} α
      (@Preorder.toLE.{u} α
        (@PartialOrder.toPreorder.{u} α
          (@SemilatticeSup.toPartialOrder.{u} α
            (@Lattice.toSemilatticeSup.{u} α
              (@CompleteLattice.toLattice.{u} α
                (@Order.Frame.toCompleteLattice.{u} α
                  (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
                    (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))))))
      (@infᵢ.{u, u + 1} α
        (@CompleteLattice.toInfSet.{u} α
          (@Order.Frame.toCompleteLattice.{u} α
            (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
              (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))
        α
        fun (b : α) ↦
          @infᵢ.{u, 0} α
            (@CompleteLattice.toInfSet.{u} α
              (@Order.Frame.toCompleteLattice.{u} α
                (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
                  (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))
            (@Membership.mem.{u, u} α (Set.{u} α) (@Set.instMembershipSet.{u} α) b s)
            fun (h : @Membership.mem.{u, u} α (Set.{u} α) (@Set.instMembershipSet.{u} α) b s) ↦
              @HasSup.sup.{u} α
                (@SemilatticeSup.toHasSup.{u} α
                  (@Lattice.toSemilatticeSup.{u} α
                    (@CompleteLattice.toLattice.{u} α
                      (@Order.Frame.toCompleteLattice.{u} α
                        (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
                          (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))))
                a b)
      (@HasSup.sup.{u} α
        (@SemilatticeSup.toHasSup.{u} α
          (@Lattice.toSemilatticeSup.{u} α
            (@CompleteLattice.toLattice.{u} α
              (@Order.Frame.toCompleteLattice.{u} α
                (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
                  (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))))
        a
        (@InfSet.infₛ.{u} α
          (@CompleteLattice.toInfSet.{u} α
            (@Order.Frame.toCompleteLattice.{u} α
              (@Order.Frame.mk.{u} α (@Order.Frame.toCompleteLattice.{u} α foo)
                (@Order.Frame.inf_supₛ_le_supᵢ_inf.{u} α foo))))
          s)) := by intros a s; rfl
  sorry #exit

The rfl near the end is taking a while. It displays as

((⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s) = ((⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

[Anatole Dedecker]

So indeed it looks like the problem has to do with the common fields of Frame and Coframe...

[Kevin Buzzard]

Yes the left hand side is full of hf.coframe and the right hand side is full of hf.frame, so maybe it finds a proof of what you are claiming to be the infᵢ_sup_le_sup_infₛ field and then takes a while checking that this proof is actually a proof of the statement it wants.

[Kevin Buzzard]

instance : CompleteDistribLattice αᵒᵈ :=
CompleteDistribLattice.mk (OrderDual.coframe.infᵢ_sup_le_sup_infₛ) -- super-quick
--{ @OrderDual.frame α _, @OrderDual.coframe α _ with } -- super-slow
--{ OrderDual.frame, OrderDual.coframe with } -- super-slow

[Kevin Buzzard]

instance Pi.completeDistribLattice {ι : Type} {π : ι → Type _}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ) -- super-quick

[Kevin Buzzard]

/-- Pullback a `complete_distrib_lattice` along an injection. -/
@[reducible]
protected def Function.Injective.completeDistribLattice [HasSup α] [HasInf α] [SupSet α] [InfSet α]
    [Top α] [Bot α] [CompleteDistribLattice β] (f : α → β) (hf : Function.Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_supₛ : ∀ s, f (supₛ s) = ⨆ a ∈ s, f a) (map_infₛ : ∀ s, f (infₛ s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteDistribLattice α :=
@CompleteDistribLattice.mk _ (hf.frame f map_sup map_inf map_supₛ map_infₛ map_top map_bot)
  (hf.coframe f map_sup map_inf map_supₛ map_infₛ map_top map_bot).infᵢ_sup_le_sup_infₛ

With those proofs, the entire file compiles in the time it was taking to compile one of those declarations with the version currently on GH. So I don't know what's going on. I'll try to minimise again but at least this is a workaround.

[Kevin Buzzard]

I've essentially minimised the problem, modulo the fact that I don't understand enough about Lean 4 notation. It's the two bottom declarations. It's too long for Zulip but it can probably be shortened. It's here. The mk constructor is quick, the { } constructor is slow.

[Scott Morrison]

I wonder if the slow-down that @Frédéric Dupuis reports in #1099: https://github.com/leanprover-community/mathlib4/pull/1099#discussion_r1051747996 is related.

[Eric Wieser]

Does using old-style structures (by manually copying all the fields rather than using extends) help at all here?

[Kevin Buzzard]

https://github.com/leanprover/lean4/issues/1986

[Kevin Buzzard]

Eric Wieser said:

Does using old-style structures (by manually copying all the fields rather than using extends) help at all here?

Don't know -- didn't try yet.

[Kevin Buzzard]

Wait a minute -- I thought the whole problem with old-style structures was that they caused super-huge terms and we necessarily have to move away from them?

[Eric Wieser]

Sounds like this would be a good place to test that in practice

[Kevin Buzzard]

class Preorder (α : Type u) where
  le : α → α → α
  lt : α → α → α
  le_refl : ∀ a : α, a ≤ a -- failed to synthesize instance LE α

@Eric Wieser you want me to literally define CompleteDistribLattice by writing down all the 37 fields and then manually constructing all the projections to the other structures it used to extend?

[Kevin Buzzard]

OK I will allow myself to extend notation typeclasses

[Kevin Buzzard]

If what you're suggesting is that I write definitions like this

class Coframe (α : Type _) extends LE α, LT α, HasInf α, HasSup α, SupSet α,
  InfSet α, Top α, Bot α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := λ a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
  protected inf_le_left : ∀ a b : α, a ⊓ b ≤ a
  protected inf_le_right : ∀ a b : α, a ⊓ b ≤ b
  protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c
  protected le_sup_left : ∀ a b : α, a ≤ a ⊔ b
  protected le_sup_right : ∀ a b : α, b ≤ a ⊔ b
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
  le_supₛ : ∀ s, ∀ a, a ∈ s → a ≤ supₛ s
  supₛ_le : ∀ s a, (∀ b, b ∈ s → b ≤ a) → supₛ s ≤ a
  infₛ_le : ∀ s, ∀ a, a ∈ s → infₛ s ≤ a
  le_infₛ : ∀ s a, (∀ b, b ∈ s → a ≤ b) → a ≤ infₛ s
  protected le_top : ∀ x : α, x ≤ ⊤
  protected bot_le : ∀ x : α, ⊥ ≤ x
  infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ s

instance Coframe.toCompleteLattice [Coframe α] : CompleteLattice α :=
{ ‹Coframe α› with }

instead of

class Coframe (α : Type _) extends CompleteLattice α where
  infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ s
  -- should be ⨅ b ∈ s but I had problems with notation

then yes it fixes the timeout.

[Gabriel Ebner]

I think this should be pretty much equivalent to the 37 fields version:

class Coframe (α : Type _) extends LE α, CompleteLattice α where
  infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ s

[Kevin Buzzard]

Changing Coframe to that definition makes

instance Pi.completeDistribLattice' {ι : Type _} {π : ι → Type _}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ)

(the formerly quick instance) now time out.

[Kevin Buzzard]

Aah! But also changing the definition of Frame to

class Frame (α : Type _) extends LE α, CompleteLattice α where

makes both instances quick! Whatever is going on?

[Kevin Buzzard]

Should these definitions be changed in mathlib master for some reason?

[Kevin Buzzard]

Indeed, making the following changes in Mathlib.Order.CompleteBooleanAlgebra:

/-- A frame, aka complete Heyting algebra, is a complete lattice whose `⊓` distributes over `⨆`. -/
class Order.Frame (α : Type _) extends LE α, CompleteLattice α where
  inf_supₛ_le_supᵢ_inf (a : α) (s : Set α) : a ⊓ supₛ s ≤ ⨆ b ∈ s, a ⊓ b
#align order.frame Order.Frame

...

/-- A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose `⊔` distributes over `⨅`. -/
class Order.Coframe (α : Type _) extends LE α, CompleteLattice α where
  infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (⨅ b ∈ s, a ⊔ b) ≤ a ⊔ infₛ s
#align order.coframe Order.Coframe

(both classes now extend LE) makes the file compile very quickly. Prior to this change, the three instances of CompleteDistribLattice defined on lines 264, 267 and 360 each took around 5 seconds of wall clock time to compile (if someone could tell me how to profile a declaration I'd be very interested BTW). With the change they're not obviously any slower than any of the other declarations. What is going on?

[Kevin Buzzard]

Is there a similar simple change which makes this instance in mathlib not need max heartbeats raised to over 300000?

set_option maxHeartbeats 304000
instance : LinearOrderedCommGroup { x : K // 0 < x } :=
  { Positive.Subtype.inv, Positive.linearOrderedCancelCommMonoid with
    mul_left_inv := fun a => Subtype.ext <| inv_mul_cancel a.2.ne' }

[Eric Wieser]

So it sounds like the optimization is to directly extend the notation classes (making them new-style extensions), but then extend all the algebraic structures last (resulting in the fields being manually copied)

[Eric Wieser]

Kevin Buzzard said:

Should these definitions be changed in mathlib master for some reason?

This change is effectively already there in mathlib3 master (in a slightly stronger form than needed in lean 4) due to old_structure_cmd

[Kevin Buzzard]

I minimised the LinearOrderedCommGroup slow instance (the one where we have to increase the heartbeats to over 300000) because it's Christmas. The mathlib-free minimisation is here. The actual issue in mathlib where we increase the heartbeats is here. The minimisation is too long to post on Zulip. It took me ages to construct. It would be really nice to have a machine which helped to minimise these things. I don't yet know a workaround.

[Heather Macbeth]

@Kevin Buzzard mathlib4#1283 also has weird performance issues, would you be interested in looking at it? This is something that fails slowly rather than succeeding slowly so it is not necessarily the same problem.

[Kevin Buzzard]

~/lean-projects/mathlib4$ lake build +Mathlib.Algebra.Module.Pi
error: no such file or directory (error code: 2)
  file: ./././Mathlib/Algebra/Regular/Smul.lean

[Heather Macbeth]

Oh, someone renamed recently, Smul to SMul, and I didn't update after merging master. Sorry!

[Kevin Buzzard]

Now the file is full of errors for me :-(

[Heather Macbeth]

Indeed, I only barely started porting the file. But it was the (erroring) instance mulActionWithZero that I wanted to ask about.

[Kevin Buzzard]

I sorried out some proofs which were causing trouble. On my file (which might not be the same as yours) this

instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
MulActionWithZero.mk (Pi.smulWithZero _).smul_zero (Pi.smulWithZero _).zero_smul

is quick if you just want a cheap workaround

[Heather Macbeth]

Do you know why it takes so long to fail?

[Kevin Buzzard]

The issue feels to me to be similar to https://github.com/leanprover/lean4/issues/1986 : for example (from that issue)

instance Pi.completeDistribLattice'' {ι : Type _} {π : ι → Type _}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
  { Pi.frame, Pi.coframe with }

takes a long time and looks kind of the same. I had expected it to succeed though if given long enough so maybe it's not the same (I let it run for ages and it didn't succeed)

[Heather Macbeth]

Actually,

instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
  { Pi.mulAction α, Pi.smulWithZero α with }

makes it succeed and succeed fast. Weird!

[Kevin Buzzard]

I just came back to tell you this and you'd got there first!

[Kevin Buzzard]

instances.png
It seems to me that typeclass inference does actually get into a loop

[Heather Macbeth]

Ugh. We should make a mwe, I can't do it today (but if you can, feel free!)

[Kevin Buzzard]

I'll do it because the thing I'm supposed to be doing is even more boring!

[Heather Macbeth]

By the way,

  { Pi.mulAction _, Pi.smulWithZero α with }

also succeeds fast, so it's just the Pi.smulWithZero that has issues.

[Kevin Buzzard]

What am I doing wrong here?

import Mathlib.Algebra.SMulWithZero

universe u v

variable {I : Type u}

variable {f : I → Type v}

variable (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] (i : I) in
#synth SMulZeroClass α (f i) -- works fine

instance Pi.smulWithZero (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    smul_zero := fun a => funext fun i => SMulZeroClass.smul_zero a -- fails with error
    /-
    failed to synthesize instance
    SMulZeroClass α (f i)
    -/
    zero_smul := sorry }

[Kevin Buzzard]

    smul_zero := fun a => funext fun i => @SMulZeroClass.smul_zero α (f i) _ _ a -- works :-/

I don't have a good mental model for why this is failing. Help!

[Kevin Buzzard]

Regardless of that issue, I've minimised:

universe u v w

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

class Nontrivial (α : Type _) : Prop where
  exists_pair_ne : ∃ x y : α, x ≠ y

class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0

class AddSemigroup (G : Type u) extends Add G where
  /-- Addition is associative -/
  add_assoc : ∀ a b c : G, a + b + c = a + (b + c)

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class AddCommSemigroup (G : Type u) extends AddSemigroup G where
  add_comm : ∀ a b : G, a + b = b + a

class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class AddZeroClass (M : Type u) extends Zero M, Add M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀

class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀

class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ

instance instHSMul (M : Type _) (α : Type _) [SMul M α] : HSMul M α α where
  hSMul := SMul.smul

infixr:73 " • " => HSMul.hSMul

class MulAction (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
  protected one_smul : ∀ b : β, (1 : α) • b = b
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b


variable (R M)

class MulActionWithZero [MonoidWithZero R] [Zero M] extends MulAction R M where
  -- these fields are copied from `SMulWithZero`, as `extends` behaves poorly
  /-- Scalar multiplication by any element send `0` to `0`. -/
  smul_zero : ∀ r : R, r • (0 : M) = 0
  /-- Scalar multiplication by the scalar `0` is `0`. -/
  zero_smul : ∀ m : M, (0 : R) • m = 0

/-- Typeclass for scalar multiplication that preserves `0` on the right. -/
class SMulZeroClass (M A : Type _) [Zero A] extends SMul M A where
  /-- Multiplying `0` by a scalar gives `0` -/
  smul_zero : ∀ a : M, a • (0 : A) = 0

class SMulWithZero [Zero R] [Zero M] extends SMulZeroClass R M where
  /-- Scalar multiplication by the scalar `0` is `0`. -/
  zero_smul : ∀ m : M, (0 : R) • m = 0

instance (priority := 100) MulActionWithZero.toSMulWithZero [MonoidWithZero R] [Zero M] [m : MulActionWithZero R M] :
    SMulWithZero R M :=
  { m with }

variable {I : Type u}

variable {f : I → Type v}

namespace Pi

instance instZero [∀ i, Zero <| f i] : Zero (∀ i : I, f i) :=
  ⟨fun _ => 0⟩

variable {M}

instance instSMul [∀ i, SMul M <| f i] : SMul M (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

instance smulWithZero (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    -- Next line fails without @ -- "faied to synthesize instance `SMulZeroClass α (f i)`"
    smul_zero := fun a => funext fun i => @SMulZeroClass.smul_zero α (f i) _ _ a
    zero_smul := fun _ => funext fun _ => SMulWithZero.zero_smul _ }

instance mulAction (α) {m : Monoid α} [∀ i, MulAction α <| f i] :
    @MulAction α (∀ i : I, f i) m where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ => MulAction.mul_smul _ _ _
  one_smul _ := funext fun _ => MulAction.one_smul _

set_option trace.Meta.synthInstance true

set_option maxHeartbeats 10000 -- consider turning trace off if you make this much bigger

-- seems to be looping
instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
 { Pi.mulAction _, Pi.smulWithZero _ with }

/-
...
[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] ✅ (i : I) → MulAction α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] ✅ (i : I) → MulAction α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] ✅ (i : I) → MulAction α (f i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α ((fun i => f i) i) ▶

...

-/

I think it's not the same as lean4#1986 because it seems to me to be actually looping.

[Kevin Buzzard]

I wonder whether the failure to synthesize SMulZeroClass α (f i) above is relevant.

[Kevin Buzzard]

Screenshot-from-2023-01-02-19-54-16.png

I don't understand that screenshot from the instance trace. Lean is continually failing to find an instance of SMulWithZero α (f i) and I'm not really used to these new instance logs but does the attached screenshot say that type class inference is failing to solve Zero α because it complains "no instances for MonoidWithZero α" despite it being visible in the local context??

[Kevin Buzzard]

What's the difference between an explosion and an X emoji?

[Yaël Dillies]

The dramatic effect. :upside_down:

[Kevin Buzzard]

Basically what does this red X mean here:

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▼
  [] new goal (i : I) → SMulWithZero α (f i) ▶
  [] 💥 apply MulActionWithZero.toSMulWithZero to (i : I) → SMulWithZero α (f i) ▼
    [tryResolve] 💥 SMulWithZero α (f i) ≟ SMulWithZero (?m.13709 i) (?m.13710 i) ▼
      [] ❌ Zero α ▶
      [] ✅ I → MonoidWithZero α ▶

It unfolds to

      [] ❌ Zero α ▼
        [] new goal Zero α ▶
        [] ✅ apply @MonoidWithZero.toZero to Zero α ▶
        [] ✅ apply @AddMonoid.toZero to Zero α ▶
        [] ✅ apply @MulZeroOneClass.toZero to Zero α ▶
        [] ✅ apply @MonoidWithZero.toMulZeroOneClass to MulZeroOneClass α ▶
        [] ✅ apply @AddZeroClass.toZero to Zero α ▶
        [] ✅ apply @AddMonoid.toAddZeroClass to AddZeroClass α ▶
        [] ✅ apply @SemigroupWithZero.toZero to Zero α ▶
        [] ✅ apply @MonoidWithZero.toSemigroupWithZero to SemigroupWithZero α ▶
        [] ✅ apply @MulZeroClass.toZero to Zero α ▶
        [] ✅ apply @MulZeroOneClass.toMulZeroClass to MulZeroClass α ▶
        [] ✅ apply @SemigroupWithZero.toMulZeroClass to MulZeroClass α ▶
        [] ✅ apply @Zero.ofOfNat0 to Zero α ▶
        [] ✅ apply @Zero.toOfNat0 to OfNat α 0 ▶

Why does a fistful of ticks lead to a cross?

[Reid Barton]

Are those ▶s things you can unfold further? maybe there are subsequent failures on those branches?

[Reid Barton]

though I don't understand that because it looks like e.g. apply @MonoidWithZero.toMulZeroOneClass to MulZeroOneClass α arose from the previous line

[Kevin Buzzard]

Yes you can unfold them all; in my screenshot I unfold one of the ticks and it looks like it's failing with "no instances for MonoidWithZero alpha" despite there being one in the local context.

[Kevin Buzzard]

I posted the mathlib-free MWE above if you want to experiment.

[Reid Barton]

Well that's odd

[Kevin Buzzard]

Screenshot-from-2023-01-02-20-21-51.png
It's right there on your left Lean!

[Heather Macbeth]

Wow, this is crazy. Thanks for minimizing Kevin.