Inhabited and Nonempty for Applicative

Stream: lean4

[François G. Dorais]

These are in Init.Prelude:

instance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) where
  default := pure

instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where
  default := pure default

instance [Monad m] : [Nonempty α] → Nonempty (m α)
  | ⟨x⟩ => ⟨pure x⟩

These all work for Applicative instead of Monad (actually Pure is enough but that's sketchy and presumably not that useful).

Is there a reason these aren't declared a few lines above after the definition of Applicative?

[François G. Dorais]

RFC lean4#12042 / PR lean4#12041

[Eric Wieser]

I think for some monads we want default to be failure instead; certainly that's the case for IO

[Eric Wieser]

Or at least, the choice that panic! uses Inhabited rather than some PanicValue makes that desirable for now

[François G. Dorais]

This is so early in the instance chain, I'm not worried it will be overridden by a smarter choice. Lowering the priority does make sense though.

[Eric Wieser]

Overriding instances isn't really a safe pattern, because if you go via a generic function you end up with a non-overriden instance