Inconsistently occurring `kernel: invalid projection`

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

I was testing out passing around a proof that a type X is a product, and using this to compute x.fst/x.snd in context. I've encountered a bunch of inconsistency in which what appears a valid proof gets kernel: invalid projection x.1.

I assume has to do with code generation because it goes away if the definitions are marked noncomputable? And the proofs are accepted as valid in that case.

Here is an example with three different approaches:

def P1 (X : Type) := exists A B, X = Prod A B

def pelim1 {R : X -> Type} (f : {A B : Type} -> (p : Prod A B = X) -> (a : A) -> (b : B) -> R (cast p (a, b))) : P1 X -> (x : X) -> R x
  := fun p x =>
    let q := p.choose_spec.choose_spec
    let y := cast q x
    let r := f q.symm y.fst y.snd
    let h : cast q.symm y = x := by simp [y]
    h ▸ r

inductive P2 (X : Type) : Type 1 where
  | p : (A B : Type) -> X = Prod A B -> P2 X

def pelim2 {R : X -> Type} (f : {A B : Type} -> (p : Prod A B = X) -> (a : A) -> (b : B) -> R (cast p (a, b))) : P2 X -> (x : X) -> R x
  := fun (.p A B q) x =>
    let y := cast q x
    let r := f q.symm y.fst y.snd
    let h : cast q.symm y = x := by simp [y]
    h ▸ r

def pfst (p : P1 X) : X -> p.choose
  := fun x => Prod.fst $ cast p.choose_spec.choose_spec x

def psnd (p : P1 X) : X -> p.choose_spec.choose
  := fun x => Prod.snd $ cast p.choose_spec.choose_spec x

def pelim3 {R : X -> Type} (f : {A B : Type} -> (p : Prod A B = X) -> (a : A) -> (b : B) -> R (cast p (a, b))) : P1 X -> (x : X) -> R x
  := fun p x =>
    let q := p.choose_spec.choose_spec
    let a := pfst p x
    let b := psnd p x
    let r := f q.symm a b
    let h : cast q.symm (a, b) = x := by simp [a, b, pfst, psnd]; apply cast_cast
    h ▸ r

When I test on the stable release, pelim1 and pelim2 both error with:

(kernel) invalid projection
  x.1

...and when I move to the nightly release, pelim1 and pelim2 both work, but pfst/psnd/pelim3 do not.

I submit this as pointing at some issue in the compiler, and I personally would be interested to better understand what's going on. (I'm new enough that I don't know where to proceed to investigate the different treatment.)

Start by running the supplied minimal reproducer against the stable and nightly releases, comparing the behavior of pelim1, pelim2, pfst, psnd, and pelim3. Investigate the compiler or kernel handling of the projection expressions; done means the valid examples are treated consistently without invalid-projection errors.