Issue finding `Inhabited` instances in partial definition

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following definition fails to compile because Lean can't infer that m (Unit × β) is inhabited.

variable {α β ε : Type _} (m : Type _ → Type _) [Monad m] [MonadExcept ε m]

partial def test (q : m β) : m (Unit × β) :=
  let rec loop (p : Unit) : m (Unit × β) :=
    try
      return (p, ← q)
    catch _ => do
      loop p
  loop ()

The following workaround does compile.

variable {α β ε : Type _} (m : Type _ → Type _) [Monad m] [MonadExcept ε m]

partial def test' (q : m β) : m (Unit × β) :=
  let inst := Inhabited.mk do return ((), (← q))
  let rec loop (p : Unit) : m (Unit × β) :=
    try
      return (p, ← q)
    catch _ => do
      let _ := inst
      loop p
  loop ()

Both lets are necessary to compile. The second let is especially confusing, I think just fixing that would already be a significant improvement.

Versions

On MacOs with Lean (version 4.0.0-nightly-2023-04-20, commit f9da1d8b55ca, Release)

Start with the self-contained partial def test reproducer and compare it with the compiling test' workaround. Investigate how partial definitions infer Inhabited for m (Unit × β), especially why the inner let _ := inst changes compilation. Done means the original definition, or an equivalent minimal case, compiles without the confusing second let.