Implicit arguments in structure fields are not respected when using projection notation

For some reason structure fields are not elaborated the same as other definitions when using projection notation, even when all the binder types and attributes are the same:

class foo (α : Type) : Type := (f : α)
def foo.f' {α : Type} [c : foo α] : α := foo.f

#print foo.f  -- def foo.f : Π {α : Type} [c : foo α], α
#print foo.f' -- def foo.f' : Π {α : Type} [c : foo α], α

variables {α : Type} [c : foo α]
#check c.f  -- ok, should fail
#check c.f' -- fail

structure bar : Prop := (f : ∀ {m : ℕ}, m = 0)
def bar.f' : bar → ∀ {m : ℕ}, m = 0 := bar.f

#print bar.f -- def bar.f : bar → ∀ {m : ℕ}, m = 0
#print bar.f' -- def bar.f' : bar → ∀ {m : ℕ}, m = 0

variables (h : bar) (m : ℕ)

#check (h.f : ∀ {m : ℕ}, m = 0) -- ok
#check (h.f : m = 0) -- fail
#check (h.f m : m = 0) -- fail
#check (h.f' : m = 0) -- ok

Reproduce the Lean snippets in the issue and compare the elaboration of structure-field projection with the corresponding definitions. Trace the projection-notation behavior until the differing treatment of implicit arguments is identified; done when the shown checks and expected failures behave consistently.