Projecting out from `Exists`

Stream: lean4

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

The following term is not well-typed and will generate a kernel error, but the term elaborator produces no error on it. Should there be an error?

#check fun (x : ∃ (x : Nat), x = x) => x.2

If we use it in an example, the kernel complains:

/- (kernel) invalid projection
  x.1 -/
example : True := by
  let a := fun (x : ∃ (x : Nat), x = x) => x.2
  exact True.intro

[Notification Bot]

This topic was moved here from #lean4 dev > Projecting out from `Exists` by Mario Carneiro.