Invalid LCNF application

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Does this look like a compiler bug worth reporting?

/-
Lean 4.23.0-nightly-2025-08-04
Target: x86_64-unknown-linux-gnu
-/
#version

/-
invalid LCNF application
  ⟨Type 1, Type⟩
argument
  Type
has type
  (fun A => A) lcAny
must be a free variable
-/
def pair : (A : Type 2) × A :=
  ⟨Type 1, Type 0⟩

set_option compiler.checkTypes true in
/-
type mismatch at LCNF application
  ⟨Type 1, Type⟩
argument Type has type
  Type 1
but is expected to have type
  (fun A => A) lcAny
-/
def pair' : (A : Type 2) × A :=
  ⟨Type 1, Type 0⟩

[Cameron Zwarich]

Yes. I have seen this before during development (of a patch I never landed) on a much more complicated example and couldn't quite decide the right course of action. This is almost as simple as it gets, so it will probably be illuminating. My guess is that there are slightly different assumptions in different parts of the frontend of the compiler about what exactly should be erased.

Note that compiler.checkTypes isn't particularly helpful in general, since there are lots of little things that can legitimately destroy typeability during compilation.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Reported under lean4#9692.