io - In Idris, can IO happen in any universe?

Question

That's my question. Idris has a cumulative universe hierarchy where the universe is inferred by the compiler. Does the use of dosomethingreal : IO imply the lowest universe in the hierarchy? Is IO : Type and never IO : Type 1? Or can I have IO actions in any universe?

Answer 1

You can. For example, the type Type -> Type is in a higher universe than the argument type. So Type -> Type is definitely not in the lowest universe and neither is IO (Type -> Type), but

test : IO (Type -> Type)
test = return List

runs fine.