type class inference failure in pi type

Stream: lean4

[Heather Macbeth]

In the thread a few days ago about typeclass inference looping, @Kevin Buzzard mentioned another example which had been causing problems in the same mathlib4 PR. This one is a failure of typeclass inference.

[Heather Macbeth]

I have now made that example import-free and checked that it works in Lean 3.

class Zero (α : Type) where
  zero : α

notation " ◯ " => Zero.zero

class SMul (R α : Type) where
  smul : R → α → α

infixr:73 " • " => SMul.smul

class SMulZeroClass (R α : Type) [Zero α] extends SMul R α where
  smul_zero : ∀ r : R, r • (◯ : α) = ◯

namespace pi
variable {I : Type}
variable {f : I → Type}

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

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

instance (R) [∀ i, Zero (f i)] [∀ i, SMulZeroClass R (f i)] :
    SMulZeroClass R (∀ i, f i) :=
  { pi.instSMul with
    smul_zero := fun _ => funext fun _ => SMulZeroClass.smul_zero _ }
    -- failed to synthesize instance SMulZeroClass R (f x✝)

end pi

[Heather Macbeth]

I opened https://github.com/leanprover/lean4/issues/2011 for this.

[Gabriel Ebner]

As a workaround you can remove pi.instSMul with.