Partial function crashes when hidden behind a type class

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

Sorry for the cryptic title, I'm not 100% sure how to explain this. I've been playing around with a DSL embedded using a tagless-final style with typeclasses, and I managed to crash Lean with what seems like it should be a pretty innocuous piece of code. Here's the MWE (or at least as minimal as I could come up with):

class RandomChoice (m : Type → Type) where
  choose : (lo hi : Nat) → (h : lo ≤ hi) → m Nat

def RandomChoice.pick [Monad m] [RandomChoice m] (x y : m α) := do
  if (← choose 0 1 (by simp)) == 0 then x else y

open RandomChoice

def Gen (α : Type) := ∀ {m : Type → Type} [Monad m] [RandomChoice m], m α

instance : RandomChoice IO where
  choose lo hi _ := IO.rand lo hi

partial def Nat.arbitrary : Gen Nat := do
  pick
    (pure 0)
    (do
      let n ← Nat.arbitrary
      pure (n + 1))

def Gen.runIO (g : Gen α) : IO α := g

-- Works fine.
#eval (Nat.arbitrary : IO Nat)

-- This breaks!
#eval Gen.runIO Nat.arbitrary

Context

I encountered this when working with @nomeata on some partial_fixpoint stuff. Originally I thought this must be related to that, but it turns out it works with partial too. The type-class embedding I'm doing is pretty central to the approach, so unfortunately I don't have a good way to work around this problem.

Steps to Reproduce

See the example above. (Tested on nightly.)

Expected behavior: The second #eval behaves the same as the first.

Actual behavior: The second #eval crashes Lean.

Versions

Tested on the Lean online editor on nightly.

Start by running the minimal Lean example and compare the two #eval expressions, especially the Gen.runIO Nat.arbitrary path. Trace where the type-class-hidden partial function is handled and identify the crash entry point. Done means the second evaluation behaves like the first without crashing Lean.