RFC: Make IO universe polymorphic

[eric-wieser]

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.

[kim-em]

I don't understand the motivation here. slim_check should not be sampling from higher universes in the first place.

[kim-em]

e.g.

import Std

example : ∃ (α : Type _) (l : List α), l ≠ l ++ l := by
  refine ⟨Int, ?_⟩
  refine ⟨[37], ?_⟩
  simp

[eric-wieser]

That example is a bit misleading, because Lean unifies the _ to 0. It fails if you use Type u.

[eric-wieser]

leanprover-community/mathlib4#9135 makes slim_check work on that statement, but it can't easily be generalized to do work in the IO monad unless we make the change suggested in this RFC.

[Kha]

How would you ever make use of a higher-universe IO if main etc. remain in IO.{0}?

[eric-wieser]

Making EStateM.bind universe-polymorphic, as I do in #3010, is sufficient I think. You wouldn't be able to use do notation to jump between universes, but you could call EStateM.bind directly, or an IO.bind wrapper for it.