Agda: how to do non-terminating IO (getLine) without (the deprecated?) ∞-style coinduction?

Question

In this question about how to do getLine in Agda the main answer suggests using the partiality monad to deal with the possible non-termination of working with the resulting Costring.

On the other hand, in version 2.5.3 the manual page on Coinduction advises against ∞, saying it can be used to prove absurdity. However ∞ is used in the definition of both IO.IO and IO.run and the partiality monad.

Questions:

1. Is it possible to do partiality and non-terminating IO using the standard library without ∞? If not, what are the alternatives?
2. Is the standard library/documentation outdated?
3. Is the problem with ∞ due to the interaction with sized types?

Thanks!