How to prove inhabited and nonempty for partial function def

Stream: lean4

[Sterea Stefan Octavian]

I'm trying to write the Haskell forever function in Lean, defined in Haskell as:

forever :: (Applicative f) => f a -> f b
forever a = let a' = a *> a' in a'

this function doesn't generally terminate and so can only be a partial function in Lean. However, the docs are not very explicit about how to prove the type implemented by such a function is inhabited and nonempty. I tried

partial def forever {α β} [Applicative f] [Inhabited β] (a : f α) : f β :=
  let rec a' : f β := a *> a'; a'

thinking that, since the function is meant to not terminate but take whatever applicative type, that type should be inhabited, right? How to make this work?

[Eric Wieser]

This seems like a bad error message:

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

It would be good if it actually showed the type in question in the message.

[Eric Wieser]

This works:

/-- Not safe as a global instance, conflicts with `(default : List Nat) = []` elsewhere -/
def Pure.toInhabited [Pure f] [Inhabited α] : Inhabited (f α) where
  default := pure default

attribute [instance] Pure.toInhabited in
partial def forever {α β} [Applicative f] [Inhabited β] (a : f α) : f β :=
  a *> forever a

[Gabriel Ebner]

-- Safe-ish as a global instance because it is in Prop, but the `f α` might match more than it should
instance Pure.toNonempty [Pure f] : [Nonempty α] → Nonempty (f α)
  | ⟨a⟩ => ⟨pure a⟩

partial def forever {α β} [Applicative f] [Inhabited β] (a : f α) : f β :=
  a *> forever a

[James Gallicchio]

it's still a bit odd to me that the nonempty can only be supplied by typeclass, instead of typeclass being a fallback for some optional syntax on defs...