Issue finding `Inhabited` instances in partial definition

[fgdorais]

Prerequisites

• [X] 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)

[fgdorais]

After a discussion on Zulip I think that the first let instance is not that problematic. I also understand that the second let instance is because the let rec doesn't automatically capture all local instances by design. That, I think, is problematic in this context. Adding the first let instance does not change the error message, which suggests that a different inhabited instance is necessary. When I first encountered this issue, I spent a long time checking that I got the right types and adding different instances to no avail. It's only by accident that I came across the solution.

Perhaps this can be remedied with a better error message: can the partial definition checker point out where the inhabited instance is missing? Or perhaps there is a way to force Lean to consider all local instances for the purpose of checking partial definitions?

[david-christiansen]

I think we should perhaps consider special-casing Inhabited and Nonempty instances when compiling partial functions, propagating them to lets.

Here's another program with this issue:

partial def outer' [Nonempty α] (i : Unit) : α := inner' i
where
  inner' : Unit → α
    | () => inner' ()

failed to compile partial definition 'outer'.inner'', failed to show that type is inhabited and non empty

It can be fixed by causing a spurious use of the instance:

partial def outer'' [Nonempty α] (i : Unit) : α := inner'' i
where
  inner'' : Unit → α
    | () => have : Nonempty α := inferInstance; inner'' ()

but this is a quite obscure transformation.

[david-christiansen]

And this is still an issue in Lean 4.11 as well as the nightly from 2024-09-17.