IR eta-expansion through trivial structure

Prerequisites

• 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

Eta-expansion doesn't appear to work through Subtype, even though it's a trivial structure.

Steps to Reproduce

Run the following program:

abbrev StackedM := ReaderT String (StateM Nat)

variable {α : Type} {m : Type → Type} [Monad m]

instance [Nonempty (m β)] : Nonempty {_v : m β // True} :=
  ⟨⟨Classical.choice inferInstance, trivial⟩⟩

@[specialize] partial def whileSub [Nonempty (m β)]
    (f : α → m (α ⊕ β)) (a : α) : {_v : m β // True} :=
  ⟨do match ← f a with
      | .inl a' => (whileSub f a').val
      | .inr b  => pure b,
   trivial⟩

@[inline] def whileViaSub [Nonempty (m β)] (f : α → m (α ⊕ β)) (a : α) : m β :=
  (whileSub f a).val

@[specialize] partial def whileDirect [Nonempty (m β)]
    (f : α → m (α ⊕ β)) (a : α) : m β := do
  match ← f a with
  | .inl a' => whileDirect f a'
  | .inr b  => pure b

set_option trace.Compiler.result true

def testSub (n : Nat) : StackedM Nat :=
  whileViaSub (fun i => pure (if i < n then .inl (i + 1) else .inr i)) 0

def testDirect (n : Nat) : StackedM Nat :=
  whileDirect (fun i => pure (if i < n then .inl (i + 1) else .inr i)) 0

Expected behavior: testSub and testDirect optimize to the same code

Actual behavior: testSub allocates a PAP in the recursive case

Versions

Lean 4.30.0-rc2
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Run the self-contained program with trace.Compiler.result enabled and compare the generated code for testSub and testDirect. Investigate the compiler IR handling of Subtype and eta-expansion, using the whileSub recursive case as the failing example. Done means both definitions optimize to the same code without a recursive-case PAP.