chore: make IO.RealWorld opaque

[kim-em]

[leanprover-community-mathlib4-bot]

• ❌ Mathlib branch lean-pr-testing-2656 built against this PR, but testing failed. (2023-10-11 05:27:13) View Log
• 💥 Mathlib branch lean-pr-testing-2656 build failed against this PR. (2023-10-11 09:00:31) View Log
• ✅ Mathlib branch lean-pr-testing-2656 has successfully built against this PR. (2023-10-12 05:52:51) View Log

[Kha]

Do the test diffs imply we're doing more refcounting? !bench (edit: ugh, I can never remember which commands work as part of a larger comment)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit fafd028e5c3d7fe1ad0128688a355af312487fbc. There were no significant changes against commit 0700925bbeb86c7b883719a82241595f5f905e5c.

[kim-em]

@Kha, do you think this is okay to merge, given that benchmarking was okay?

[Kha]

@Kha, do you think this is okay to merge, given that benchmarking was okay?

Yes! Sorry for the 13-month delay :)

[zwarich]

I don't think this is really blocked by the new code generator.

[zwarich]

Closing this in favor of #9631.