io - Agda：如何在没有（不推荐使用的？）∞风格的共归纳的情况下进行非终止 IO（getLine）？

Question

在这个关于如何getLine在 Agda 中做的问题中，主要答案建议使用偏性 monad 来处理可能不终止使用生成的 Costring 的情况。

另一方面，在 2.5.3 版本中，Coinduction的手册页建议不要使用 ∞，称它可以用来证明荒谬。但是 ∞ 用于IO.IO 和 IO.run的定义以及偏性monad。

问题：

1. 是否可以使用没有 ∞ 的标准库来进行偏心和非终止 IO？如果没有，有什么替代方案？
2. 标准库/文档是否过时？
3. ∞ 的问题是由于与大小类型的交互吗？

谢谢！