RFC: Make `IO` universe polymorphic

Proposal

Right now, we have IO : Type → Type. This RFC suggests we change to IO : Type u → Type u.

This RFC does not suggest:

• Making all monads polymorphic within a chain of binds. This requires a massive redesign, and the tradeoffs are unclear.
• Changing any of the "real" IO api to operate in any universe other than 0.

• User Experience: How does this feature improve the user experience?

  • Users of IO.ofExcept will not get weird universe errors if they pass in an Except from a higher universe
  • Users of types in higher universes will not have to jump between the real IO monad and a hand-rolled IOButHigherUniverse

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

  • This would help with slim_check, which currently, in order to sample from types in higher universes, needs the monad itself to produce values in those universes
  • Mathlib's existing ULiftable infrastructure would be usable with IO; currently it cannot be because IO doesn't form a family of types over universes.
  • Users ask about this every few months

• Maintainability: Will this change streamline code maintenance or simplify its structure?

  • The change will replace a few (a b : Type u)s with (a : Type u) (b : Type v); the consequences are negligible.

Community Feedback

Some initial discussion, which suggests some benefit would arise even from just changing IO to allow higher universes: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO/near/282494539

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No files or tests are named in the issue; begin by locating the IO type declaration and reviewing the linked Zulip discussion. Done would mean implementing the proposed universe-polymorphic IO change without broadening the real IO API beyond universe 0, with the universe-related behavior verified.