Application type mismatch with _nested argument

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following code

namespace List
  def keys (pairs : List (α × β)) : List α
    := match pairs with
      | [] => []
      | ⟨a, _⟩ :: rest => a :: keys rest

  def values (pairs : List (α × β)) : List β
    := match pairs with
      | [] => []
      | ⟨_, b⟩ :: rest => b :: values rest
end List

inductive Term : Type where
  | var : String → Term
  | app : Term → Term → Term
  | lam : String → Term → Term
  | record : (entries : List (String × Term)) → (unique : entries.keys.Nodup) → Term

results in an error:

application type mismatch
  List.keys entries
argument has type
  _nested.List_1
but function has type
  List (String × Term) → List String

Context

People on Lean Zulip suggested to file a bug report.

Steps to Reproduce

Put the code above into VSCode editor, wait for lean infoview to execute.

Expected behavior: The code should type check

Actual behavior: Error thrown

Versions

Lean version: 4.11.0-rc1

Start with the minimal reproducer in the issue in the VSCode editor or on the Lean nightly release, focusing on the application type mismatch involving the _nested argument and List.keys. Confirm the behavior against the stated Lean 4.11.0-rc1 version and latest nightly; done when the example type checks without the reported error.