λ with ⟨⟩ consumes following implicit arguments

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.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

If the ⟨⟩ brackets are used in a lambda binder, and the result type is a function with implicit arguments, those arguments are "implicitly introd", as though there were the same number of _ binders after the binder using ⟨⟩.

Steps to Reproduce

Consider the program

structure foo :=
(val : ℕ)

def bar : Π (x : foo) {k₁ k₂ : ℕ} (l : ℕ), ℕ := λ ⟨n⟩ m, m

#reduce bar ⟨1⟩ 2

Expected behavior: bar should be an error, since the right-hand side should be a function of only two arguments.
This is the behavior if k₁ and k₂ are explicit arguments, or if λ ⟨n⟩ is replaced by λ y.
(It makes no difference whether x is explicit or not.)

Actual behavior: bar compiles successfully and the #reduce line prints 2.

Reproduces how often: Always

Versions

Lean (version 3.26.0, commit 5a5c139af3e9, Release)
Ubuntu 20.04 LTS

Start by running the self-contained Lean reproducer and compare the behavior of the lambda using ⟨n⟩ with the versions using explicit arguments or λ y. Trace the compiler entry point that elaborates lambda binders and implicit function arguments. Done means the shown definition is rejected while the intended valid comparisons retain their existing behavior.