(kernel) invalid projection when extracting the proposition from an `Exists` statement.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following code explains the issue:

set_option pp.rawOnError true
/- Error:
(kernel) invalid projection
  h.2
-/
example (h : ∃ _ : Nat, P) : P := h.2

/- Works -/
example (h : ∃ _ : Nat, P) : P := by
  let ⟨_, P⟩ := h
  exact P

Context

The issue is discussed here. It seems that the error makes sense, but Alex suggested me to open an issue since it's a kernel error.

Versions

The error appears since Lean (version 4.0.0, commit ec941735c80d, Release) up til v4.2.0-rc1, on a Mac Intel.

Others

As mentioned above, the error makes sense from a human perspective, so if this kernel error is intended, feel free to close this issue :)

Start by running the minimal reproducer in the issue and comparing the failing h.2 projection with the working pattern-matching example. Investigate the kernel's handling of projections from Exists; done means the behavior is clarified and either corrected or documented as intended.