Bug with partial def?

Stream: lean4

[François G. Dorais]

I can't figure out what's going on with test below. Adding a bunch of Inhabited instances doesn't seem to help (even though test0 and test1 work fine).

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

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

-- fine
partial def test0 (q : m β) : m β :=
  let rec loop : m β :=
    try
      q
    catch _ =>
      loop
  loop

-- fine
partial def test1 (q : m (Option β)) : m (Unit × Option β) :=
  let rec loop (p : Unit) : m (Unit × Option β) :=
    try
      return (p, ← q)
    catch _ =>
      loop p
  loop ()

[François G. Dorais]

Aha! This one works:

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

I don't see why the let is necessary. (But ultimately, there is no reason to need β to be inhabited at all.)

[François G. Dorais]

Finally! Here is a complete workaround:

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

[François G. Dorais]

I just filed a bug report about this: <https://github.com/leanprover/lean4/issues/2204>

[Mac Malone]

@François G. Dorais The Inhabited instance is definitely necessary. There is no way for Lean to infer that m (Unit x B) is inhabited by itself (as the evidence of its inhabitant comes from evaluating a function argument). I think the second let is necessary because outer local instances are not automatically captured by let rec (which I think is a deliberate design decision).

[François G. Dorais]

@Mac That makes sense. The second one is the one that nags me. When I got the error message, the first thing I tried was adding the first let. Since that didn't work, I scratched my head for hours wondering what other instance was needed. It's only by accident that I stumbled upon adding the same instance twice.