Application type mismatch with _nested argument

Anatolay commented 2 months ago

Prerequisites

[X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[X] 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

kmill commented 2 months ago

A somewhat related issue is #4824, where values in optParams aren't being updated when processing nesting. There's another solution in that case, but this issue is fixed first it's worth seeing if it closes that one as well.

nomeata commented 2 months ago

I doubt that this issue will be fixed soon (besides, maybe, with a better error message), unless I am mistaken. This kind of nesting is hard™ to do.

leanprover / lean4