diff --git a/CHANGELOG.md b/CHANGELOG.md
index 24fb3493a4..dc3c702779 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,7 @@ Non-backwards compatible changes
   parametrized by _raw_ bundles, and as such take a proof of transitivity.
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
   parametrized by _raw_ bundles, and as such take a proof of reflexivity.
+* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Other major improvements
 ------------------------
@@ -66,6 +67,11 @@ Deprecated names
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
   ```
 
+* In `IO.Base`:
+  ```agda
+  untilRight  ↦  untilInj₂
+  ```
+
 New modules
 -----------
 
@@ -137,6 +143,12 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* New IO primitives to handle buffering
+  ```agda
+  IO.Primitive.Handle
+  IO.Handle
+  ```
+
 * `System.Random` bindings:
   ```agda
   System.Random.Primitive
@@ -418,13 +430,34 @@ Additions to existing modules
   between : String → String → String → String
   ```
 
+* Re-exported new types and functions in `IO`:
+  ```agda
+  BufferMode : Set
+  noBuffering : BufferMode
+  lineBuffering : BufferMode
+  blockBuffering : Maybe ℕ → BufferMode
+  Handle : Set
+  stdin : Handle
+  stdout : Handle
+  stderr : Handle
+  hSetBuffering : Handle → BufferMode → IO ⊤
+  hGetBuffering : Handle → IO BufferMode
+  hFlush : Handle → IO ⊤
+  ```
+
+* Added new functions in `IO.Base`:
+  ```agda
+  whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤
+  forever : IO ⊤ → IO ⊤
+  ```
+
 * In `Data.Word.Base`:
   ```agda
   _≤_ : Rel Word64 zero
   ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
-  ```
+  ```agda
   transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
   ```
 
diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index c3aa8ed710..d7895f96db 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -56,11 +56,14 @@ unsafeModules = map modToFile
   , "IO"
   , "IO.Base"
   , "IO.Categorical"
+  , "IO.Handle"
   , "IO.Infinite"
   , "IO.Instances"
   , "IO.Effectful"
   , "IO.Finite"
   , "IO.Primitive"
+  , "IO.Primitive.Core"
+  , "IO.Primitive.Handle"
   , "IO.Primitive.Infinite"
   , "IO.Primitive.Finite"
   , "Relation.Binary.PropositionalEquality.TrustMe"
diff --git a/doc/README/IO.agda b/doc/README/IO.agda
index 37553edd1d..bf913bbfdd 100644
--- a/doc/README/IO.agda
+++ b/doc/README/IO.agda
@@ -13,6 +13,7 @@ open import Data.Nat.Base
 open import Data.Nat.Show using (show)
 open import Data.String.Base using (String; _++_; lines)
 open import Data.Unit.Polymorphic
+open import Function.Base using (_$_)
 open import IO
 
 ------------------------------------------------------------------------
@@ -86,10 +87,21 @@ cat fp = do
   let ls = lines content
   List.mapM′ putStrLn ls
 
-open import Codata.Musical.Notation
-open import Codata.Musical.Colist
-open import Data.Bool
-open import Data.Unit.Polymorphic.Base
+------------------------------------------------------------------------
+-- TOP-LEVEL LOOP
+
+-- If you simply want to repeat the same action over and over again, you
+-- can use `forever` e.g. the following defines a REPL that echos whatever
+-- the user types
+
+echo : IO ⊤
+echo = do
+  hSetBuffering stdout noBuffering
+  forever $ do
+    putStr "echo< "
+    str ← getLine
+    putStrLn ("echo> " ++ str)
+
 
 ------------------------------------------------------------------------
 -- GUARDEDNESS
@@ -101,6 +113,10 @@ open import Data.Unit.Polymorphic.Base
 -- In this case you cannot use the convenient combinators that make `do`-notations
 -- and have to revert back to the underlying coinductive constructors.
 
+open import Codata.Musical.Notation
+open import Codata.Musical.Colist using (Colist; []; _∷_)
+open import Data.Bool
+open import Data.Unit.Polymorphic.Base
 
 -- Whether a colist is finite is semi decidable: just let the user wait until
 -- you reach the end!
diff --git a/src/Foreign/Haskell/Coerce.agda b/src/Foreign/Haskell/Coerce.agda
index 3eb411c325..4383a1ac86 100644
--- a/src/Foreign/Haskell/Coerce.agda
+++ b/src/Foreign/Haskell/Coerce.agda
@@ -35,7 +35,7 @@ open import Level using (Level; _⊔_)
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Int
 
-import IO.Primitive            as STD
+import IO.Primitive.Core       as STD
 import Data.List.Base          as STD
 import Data.List.NonEmpty.Base as STD
 import Data.Maybe.Base         as STD
diff --git a/src/IO.agda b/src/IO.agda
index 96f7db2760..0462d9b8b9 100644
--- a/src/IO.agda
+++ b/src/IO.agda
@@ -14,7 +14,7 @@ open import Data.Unit.Polymorphic.Base
 open import Data.String.Base using (String)
 import Data.Unit.Base as Unit0
 open import Function.Base using (_∘_; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 open import Level
 
 private
@@ -27,6 +27,7 @@ private
 -- Re-exporting the basic type and functions
 
 open import IO.Base public
+open import IO.Handle public
 
 ------------------------------------------------------------------------
 -- Utilities
diff --git a/src/IO/Base.agda b/src/IO/Base.agda
index 8c44474935..54aff90dfc 100644
--- a/src/IO/Base.agda
+++ b/src/IO/Base.agda
@@ -16,13 +16,14 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 import Agda.Builtin.Unit as Unit0
 open import Data.Unit.Polymorphic.Base
 open import Function.Base using (_∘′_; const; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 
 private
   variable
-    a b : Level
+    a b e : Level
     A : Set a
     B : Set b
+    E : Set e
 
 ------------------------------------------------------------------------
 -- The IO monad
@@ -106,18 +107,37 @@ lift′ io = lift (io Prim.>>= λ _ → Prim.pure _)
 ignore : IO A → IO ⊤
 ignore io = io >> pure _
 
+
+------------------------------------------------------------------------
 -- Conditional executions
+
+-- Only run the action if the boolean is true
 when : Bool → IO {a} ⊤ → IO ⊤
 when true m = m
 when false _ = pure _
 
+-- Only run the action if the boolean is false
 unless : Bool → IO {a} ⊤ → IO ⊤
 unless = when ∘′ not
 
+-- Run the action if the `Maybe` computation was successful
 whenJust : Maybe A → (A → IO {a} ⊤) → IO ⊤
 whenJust (just a) k = k a
 whenJust nothing  _ = pure _
 
+-- Run the action if the `E ⊎_` computation was successful
+whenInj₂ : E ⊎ A → (A → IO {a} ⊤) → IO ⊤
+whenInj₂ (inj₂ a) k = k a
+whenInj₂ (inj₁ _) _ = pure _
+
+
+------------------------------------------------------------------------
+-- Loops
+
+-- Keep running the action forever
+forever : IO {a} ⊤ → IO {a} ⊤
+forever act = seq (♯ act) (♯ forever act)
+
 -- Keep running an IO action until we get a value. Convenient when user
 -- input is involved and it may be malformed.
 untilJust : IO (Maybe A) → IO A
@@ -127,7 +147,22 @@ untilJust m = bind (♯ m) λ where
   nothing  → ♯ untilJust m
   (just a) → ♯ pure a
 
-untilRight : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
-untilRight f x = bind (♯ f x) λ where
-  (inj₁ x′) → ♯ untilRight f x′
+untilInj₂ : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
+untilInj₂ f x = bind (♯ f x) λ where
+  (inj₁ x′) → ♯ untilInj₂ f x′
   (inj₂ y) → ♯ pure y
+
+
+
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATIONS
+
+untilRight = untilInj₂
+{-# WARNING_ON_USAGE untilRight
+"Warning: untilRight was deprecated in v2.1.
+Please use untilInj₂ instead."
+#-}
diff --git a/src/IO/Finite.agda b/src/IO/Finite.agda
index 44b5edc050..1827d471b9 100644
--- a/src/IO/Finite.agda
+++ b/src/IO/Finite.agda
@@ -12,7 +12,7 @@ open import Data.Unit.Polymorphic.Base
 open import Agda.Builtin.String
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Finite as Prim
 open import Level
 
diff --git a/src/IO/Handle.agda b/src/IO/Handle.agda
new file mode 100644
index 0000000000..0c15906201
--- /dev/null
+++ b/src/IO/Handle.agda
@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --guardedness #-}
+
+module IO.Handle where
+
+open import Level using (Level)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import IO.Base using (IO; lift; lift′)
+
+private variable a : Level
+
+------------------------------------------------------------------------
+-- Re-exporting types and constructors
+
+open import IO.Primitive.Handle as Prim public
+  using ( BufferMode
+        ; noBuffering
+        ; lineBuffering
+        ; blockBuffering
+        ; Handle
+        ; stdin
+        ; stdout
+        ; stderr
+        )
+
+------------------------------------------------------------------------
+-- Wrapping functions
+
+hSetBuffering : Handle → BufferMode → IO {a} ⊤
+hSetBuffering hdl bm = lift′ (Prim.hSetBuffering hdl bm)
+
+hGetBuffering : Handle → IO BufferMode
+hGetBuffering hdl = lift (Prim.hGetBuffering hdl)
+
+hFlush : Handle → IO {a} ⊤
+hFlush hdl = lift′ (Prim.hFlush hdl)
diff --git a/src/IO/Infinite.agda b/src/IO/Infinite.agda
index f2137cc4c6..90afd8989d 100644
--- a/src/IO/Infinite.agda
+++ b/src/IO/Infinite.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.String
 open import Data.Unit.Polymorphic.Base
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Infinite as Prim
 open import Level
 
diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda
index 8014a2bd7c..324a32b643 100644
--- a/src/IO/Primitive.agda
+++ b/src/IO/Primitive.agda
@@ -1,38 +1,15 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Primitive IO: simple bindings to Haskell types and functions
+-- This module is DEPRECATED. Please use IO.Primitive.Core instead
 ------------------------------------------------------------------------
 
--- NOTE: the contents of this module should be accessed via `IO`.
-
 {-# OPTIONS --cubical-compatible #-}
 
 module IO.Primitive where
 
-open import Level using (Level)
-private
-  variable
-    a : Level
-    A B : Set a
-
-------------------------------------------------------------------------
--- The IO monad
-
-open import Agda.Builtin.IO public
-  using (IO)
-
-infixl 1 _>>=_
-
-postulate
-  pure : A → IO A
-  _>>=_  : IO A → (A → IO B) → IO B
-
-{-# COMPILE GHC pure = \_ _ -> return    #-}
-{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
-{-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
-{-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+open import IO.Primitive.Core public
 
--- Haskell-style alternative syntax
-return : A → IO A
-return = pure
+{-# WARNING_ON_IMPORT
+"IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."
+#-}
diff --git a/src/IO/Primitive/Core.agda b/src/IO/Primitive/Core.agda
new file mode 100644
index 0000000000..6fd22a03fb
--- /dev/null
+++ b/src/IO/Primitive/Core.agda
@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive IO: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+-- NOTE: the contents of this module should be accessed via `IO`.
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive.Core where
+
+open import Level using (Level)
+private
+  variable
+    a : Level
+    A B : Set a
+
+------------------------------------------------------------------------
+-- The IO monad
+
+open import Agda.Builtin.IO public
+  using (IO)
+
+infixl 1 _>>=_
+
+postulate
+  pure : A → IO A
+  _>>=_  : IO A → (A → IO B) → IO B
+
+{-# COMPILE GHC pure = \_ _ -> return    #-}
+{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
+{-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
+{-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+
+-- Haskell-style alternative syntax
+return : A → IO A
+return = pure
diff --git a/src/IO/Primitive/Handle.agda b/src/IO/Primitive/Handle.agda
new file mode 100644
index 0000000000..f6b01a70be
--- /dev/null
+++ b/src/IO/Primitive/Handle.agda
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+-- NOTE: the contents of this module should be accessed via `IO`.
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive.Handle where
+
+open import Data.Maybe.Base using (Maybe)
+open import Data.Nat.Base using (ℕ)
+
+data BufferMode : Set where
+  noBuffering lineBuffering : BufferMode
+  blockBuffering : Maybe ℕ → BufferMode
+{-# FOREIGN GHC import System.IO #-}
+{-# FOREIGN GHC
+    data AgdaBufferMode
+      = AgdaNoBuffering
+      | AgdaLineBuffering
+      | AgdaBlockBuffering (Maybe Integer)
+    toBufferMode :: AgdaBufferMode -> BufferMode
+    toBufferMode x = case x of
+      AgdaNoBuffering       -> NoBuffering
+      AgdaLineBuffering     -> LineBuffering
+      AgdaBlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
+    fromBufferMode :: BufferMode -> AgdaBufferMode
+    fromBufferMode x = case x of
+      NoBuffering       -> AgdaNoBuffering
+      LineBuffering     -> AgdaLineBuffering
+      BlockBuffering mi -> AgdaBlockBuffering (fromIntegral <$> mi)
+#-}
+
+{-# COMPILE GHC BufferMode = data AgdaBufferMode
+                           ( AgdaNoBuffering
+                           | AgdaLineBuffering
+                           | AgdaBlockBuffering
+                           )
+#-}
+
+open import Data.Unit.Base using (⊤)
+open import IO.Primitive.Core using (IO)
+
+postulate
+  Handle : Set
+  stdin stdout stderr : Handle
+  hSetBuffering : Handle → BufferMode → IO ⊤
+  hGetBuffering : Handle → IO BufferMode
+  hFlush : Handle → IO ⊤
+
+{-# FOREIGN GHC import System.IO #-}
+{-# COMPILE GHC Handle = type Handle #-}
+{-# COMPILE GHC stdin = stdin #-}
+{-# COMPILE GHC stdout = stdout #-}
+{-# COMPILE GHC stderr = stderr #-}
+{-# COMPILE GHC hSetBuffering = \ h -> hSetBuffering h . toBufferMode #-}
+{-# COMPILE GHC hGetBuffering = fmap fromBufferMode . hGetBuffering #-}
+{-# COMPILE GHC hFlush = hFlush #-}
diff --git a/src/System/Clock/Primitive.agda b/src/System/Clock/Primitive.agda
index 330b9e36c4..9e394af190 100644
--- a/src/System/Clock/Primitive.agda
+++ b/src/System/Clock/Primitive.agda
@@ -9,7 +9,7 @@
 module System.Clock.Primitive where
 
 open import Agda.Builtin.Nat using (Nat)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Foreign.Haskell using (Pair)
 
 data Clock : Set where
diff --git a/src/System/Environment/Primitive.agda b/src/System/Environment/Primitive.agda
index c1f8533e03..9408613641 100644
--- a/src/System/Environment/Primitive.agda
+++ b/src/System/Environment/Primitive.agda
@@ -14,7 +14,7 @@
 
 module System.Environment.Primitive where
 
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
 open import Data.String.Base using (String)
diff --git a/src/System/FilePath/Posix/Primitive.agda b/src/System/FilePath/Posix/Primitive.agda
index ed4cd56792..8226666ba6 100644
--- a/src/System/FilePath/Posix/Primitive.agda
+++ b/src/System/FilePath/Posix/Primitive.agda
@@ -14,7 +14,7 @@ open import Agda.Builtin.List using (List)
 open import Agda.Builtin.Maybe using (Maybe)
 open import Agda.Builtin.String using (String)
 open import Foreign.Haskell as FFI using (Pair; Either)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 
 -- A filepath has a nature: it can be either relative or absolute.
 -- We postulate this nature rather than defining it as an inductive
diff --git a/src/System/Process/Primitive.agda b/src/System/Process/Primitive.agda
index aa2bdfcbf2..828a275433 100644
--- a/src/System/Process/Primitive.agda
+++ b/src/System/Process/Primitive.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.List
 open import Agda.Builtin.String
 open import Agda.Builtin.Unit
 open import Foreign.Haskell using (Pair)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import System.Exit.Primitive using (ExitCode)
 
 postulate
diff --git a/tests/runtests.agda b/tests/runtests.agda
index a7840838b5..c6ad22e0ce 100644
--- a/tests/runtests.agda
+++ b/tests/runtests.agda
@@ -23,6 +23,7 @@ systemTests = mkTestPool "System modules"
   $ "ansi"
   ∷ "directory"
   ∷ "environment"
+  ∷ "io"
   ∷ "random"
   ∷ []
 
diff --git a/tests/system/io/Main.agda b/tests/system/io/Main.agda
new file mode 100644
index 0000000000..4d2697ea27
--- /dev/null
+++ b/tests/system/io/Main.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --guardedness #-}
+
+module Main where
+
+open import Data.String.Base
+open import Function.Base using (_$_; case_of_)
+open import IO
+open import System.Exit using (exitSuccess)
+
+main : Main
+main = run $ do
+  -- Ensure no buffering so that the prompt "echo< "
+  -- gets outputed immediately
+  hSetBuffering stdout noBuffering
+  forever $ do
+    putStr "echo< "
+    -- Get a line from the user and immediately inspect it
+    -- If it's a magic "exit" keyword then we exit, otherwise
+    -- we print the echo'd message and let the `forever` action
+    -- continue
+    str ← getLine
+    case str of λ where
+      "exit" → exitSuccess
+      _ → putStrLn ("echo> " ++ str)
diff --git a/tests/system/io/expected b/tests/system/io/expected
new file mode 100644
index 0000000000..361d15957e
--- /dev/null
+++ b/tests/system/io/expected
@@ -0,0 +1,6 @@
+echo< echo> hello
+echo< echo> my
+echo< echo> name
+echo< echo> is
+echo< echo> Agda
+echo< 
\ No newline at end of file
diff --git a/tests/system/io/input b/tests/system/io/input
new file mode 100644
index 0000000000..bba046a9d5
--- /dev/null
+++ b/tests/system/io/input
@@ -0,0 +1,6 @@
+hello
+my
+name
+is
+Agda
+exit
\ No newline at end of file
diff --git a/tests/system/io/io.agda-lib b/tests/system/io/io.agda-lib
new file mode 100644
index 0000000000..74c23d5ccc
--- /dev/null
+++ b/tests/system/io/io.agda-lib
@@ -0,0 +1,2 @@
+name: io
+include: ../../../src/ .
diff --git a/tests/system/io/run b/tests/system/io/run
new file mode 100644
index 0000000000..ad42dc90b2
--- /dev/null
+++ b/tests/system/io/run
@@ -0,0 +1,5 @@
+$1 --compile-dir=../../_build -c Main.agda > log
+./../../_build/Main hello world < input > output
+
+rm ../../_build/Main
+rm ../../_build/MAlonzo/Code/Main*
\ No newline at end of file