Typeclass inference failure with lambda

[kbuzzard]

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

Typeclass inference fails to discover an instance which I can create manually using instances known to Lean, and there does not seem to be a type class diamond or loop involved.

class has_note (M : Type) where
  note : M

notation "♩" => has_note.note

class has_note2 (M : Type) extends has_note M

variable {ι : Type} (β : ι → Type)

structure foo [∀ i, has_note (β i)] : Type where
  to_fun : ∀ i, β i

instance foo.has_note [∀ i, has_note (β i)] : has_note (foo (λ i => β i)) where
  note := { to_fun := λ _ => ♩ }

instance foo.has_note2 [∀ i, has_note2 (β i)] : has_note2 (foo (λ i => β i)) where
  note := ♩

variable (α : Type) (M : Type)

structure bar [has_note M] where
  to_fun : α → M

instance bar.has_note [has_note M] : has_note (bar α M) where
  note := { to_fun := λ _ => ♩ }

instance bar.has_note2 [has_note2 M] : has_note2 (bar α M) where
  note := ♩

example [has_note2 M] : has_note2 (foo (λ (i : ι) => bar (β i) M)) :=
inferInstance -- fails

example [has_note2 M] : has_note2 (foo (λ (i : ι) => bar (β i) M)) :=
foo.has_note2 _ -- works

The trace for the failing inferInstance is

  [Meta.synthInstance.generate] instance foo.has_note2
  [Meta.synthInstance.tryResolve] 
    [Meta.synthInstance.tryResolve] has_note2
      (foo fun (i : ι) => bar (β i) M) =?= has_note2 (foo fun (i : ?m.1321) => ?m.1322 i)
    [Meta.synthInstance.tryResolve] failure
  [Meta.synthInstance] failed

This also fails in Lean 3. [This shows up when building algebraic instances for finsupp and dfinsupp (finitely supported functions, i.e. functions which take the note value (0 or 1) for all but finitely many inputs)].

Expected behavior: [What you expect to happen]

I am expecting type class inference to succeed but my understanding of Lean 4's type class system is poor.

Versions

Lean (version 4.0.0-nightly-2021-06-03, commit c47fff1, Release)
Linux bob 5.4.0-74-generic #83-Ubuntu SMP Sat May 8 02:35:39 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux
DISTRIB_DESCRIPTION="Ubuntu 20.04.2 LTS"