let rec in partial definition does not inherit Inhabitted α

Stream: general

[Ayhon]

When playing around with some definitions, I came accross the following surprising behavior (at least to me).

Consider the following code

partial
def foo {α}[Inhabited α] :=
  let rec go: α := go
  go

Lean fails to compile the previous definition with the following error message

failed to compile 'partial' definition `foo.go`, could not prove that the type
  {α : Sort u_1} → α
is nonempty.

If I add [Inhabitted α] to the definition of go Lean behaves as I would have first expected.

[Ayhon]

(deleted)