I’m specifically talking about the “Produces a non-empty, finite, prefix of a possibly infinite result” part on that page. As long as your server generates finite responses in finite times, Idris recognizes your code as total.

When dealing with corecursion (infinite streams) you don't care about whether you terminate, but rather, whether the infinite stream is _productive_ meaning it doesn't stop producing values. The prime example of a function that's impossible(?) to prove productive (for all cases) is filter – since it takes a predicate function that decides whether values are returned or not. If you give filter a predicate that always returns false you will never produce any values, hence that wouldn't be productive.

If you have codata you can have infinite loops in total functional programming.

https://en.wikipedia.org/wiki/Corecursion