λ with ⟨⟩ consumes following implicit arguments

[rwbarton]

Prerequisites

• [X] 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