Type class inference failure in pi type

[hrmacbeth]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This is a failure of type class inference (possibly relevant: in a pi-type), which did not occur in Lean 3.

Steps to Reproduce

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 _ }

end pi

Expected behavior: [What you expect to happen]

No errors. (Note that this works in Lean 3.)

Actual behavior: [What actually happens]

"failed to synthesize instance SMulZeroClass R (f x✝)" on the SMulZeroClass.smul_zero _

Reproduces how often: [What percentage of the time does it reproduce?]

Always

Versions

Nightly 2023-01-04

Additional Information

Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20failure.20in.20pi.20type
Mathlib PR where this arose: leanprover-community/mathlib4#1283