[ fix #1368 ] ⊤-returning IO functions made level polymorphic (#1369)

Author: gallais

CHANGELOG.md

@@ -27,6 +27,9 @@ Bug-fixes
 
 * Added version to library name
 
+* In `IO`, `⊤`-returning functions (such as `putStrLn`) have been made level polymorphic.
+  This may force you to add more type or level annotations to your programs.
+
 Non-backwards compatible changes
 --------------------------------
 

README/Debug/Trace.agda

@@ -56,12 +56,13 @@ div m n    = just (go m m) where
 -- We add two calls to trace to see when div is evaluated and when the returned
 -- number is forced (by a call to show).
 
+open import Level using (0ℓ)
 open import IO
 
 main =
   let r = trace "Call to div" (div 4 2)
       j = λ n → trace "Forcing the result wrapped in just." (putStrLn (show n)) in
-  run (maybe′ j (return _) r)
+  run {a = 0ℓ} (maybe′ j (return _) r)
 
 -- We get the following trace where we can see that checking that the
 -- maybe-solution is just-headed does not force the natural number. Once forced,

src/IO.agda

@@ -12,6 +12,7 @@ open import Codata.Musical.Notation
 open import Codata.Musical.Costring
 open import Data.Unit.Polymorphic
 open import Data.String
+import Data.Unit as Unit0
 open import Function
 import IO.Primitive as Prim
 open import Level
@@ -145,28 +146,32 @@ readFile f = lift (Prim.readFile f)
 readFiniteFile : String → IO String
 readFiniteFile f = lift (Prim.readFiniteFile f)
 
-writeFile∞ : String → Costring → IO ⊤
-writeFile∞ f s = ignore (lift (Prim.writeFile f s))
+private
+  lift′ : Prim.IO Unit0.⊤ → IO {a} ⊤
+  lift′ io = lift (io Prim.>>= λ _ → Prim.return _)
+
+writeFile∞ : String → Costring → IO {a} ⊤
+writeFile∞ f s = lift′ (Prim.writeFile f s)
 
-writeFile : String → String → IO ⊤
+writeFile : String → String → IO {a} ⊤
 writeFile f s = writeFile∞ f (toCostring s)
 
-appendFile∞ : String → Costring → IO ⊤
-appendFile∞ f s = ignore (lift (Prim.appendFile f s))
+appendFile∞ : String → Costring → IO {a} ⊤
+appendFile∞ f s = lift′ (Prim.appendFile f s)
 
-appendFile : String → String → IO ⊤
+appendFile : String → String → IO {a} ⊤
 appendFile f s = appendFile∞ f (toCostring s)
 
-putStr∞ : Costring → IO ⊤
-putStr∞ s = ignore (lift (Prim.putStr s))
+putStr∞ : Costring → IO {a} ⊤
+putStr∞ s = lift′ (Prim.putStr s)
 
-putStr : String → IO ⊤
+putStr : String → IO {a} ⊤
 putStr s = putStr∞ (toCostring s)
 
-putStrLn∞ : Costring → IO ⊤
-putStrLn∞ s = ignore (lift (Prim.putStrLn s))
+putStrLn∞ : Costring → IO {a} ⊤
+putStrLn∞ s = lift′ (Prim.putStrLn s)
 
-putStrLn : String → IO ⊤
+putStrLn : String → IO {a} ⊤
 putStrLn s = putStrLn∞ (toCostring s)
 
 -- Note that the commands writeFile, appendFile, putStr and putStrLn