universe level が問題になる例: Stream の doc comment

universe level が問題になることはめったにないが、たまに問題になることがある。
どういうときに問題になるのか、典型的な例を調べてまとめておきたい。

Stream の module doc に次のように書かれている。

Remark: we considered using the following alternative design

structure Stream (α : Type u) where
  stream : Type u
  next? : stream → Option (α × stream)

class ToStream (collection : Type u) (value : outParam (Type v)) where
  toStream : collection → Stream value

where Stream is not a class, and its state is encapsulated.
The key problem is that the type Stream α "lives" in a universe higher than α.
This is a problem because we want to use Streams in monadic code.

Start from the Stream module doc and read the quoted alternative Stream and ToStream definitions, then investigate the universe-level issue described there. Document typical situations where the higher universe causes problems in monadic code, using clear examples. Done means the Stream documentation explains when and why this design becomes problematic.