From 3c30dbd1ded4012ad6856ad58641e644e005e072 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Mon, 17 Nov 2025 17:32:44 +0100
Subject: [PATCH 01/11] [ #432 ] Initial jab at implementing exceptions

---
 lib/base/Haskell/Control/Exception.agda | 51 +++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 3 deletions(-)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index 5b9ed8ca..a80ca1d0 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -1,11 +1,56 @@
 module Haskell.Control.Exception where
 
 open import Haskell.Prim
+open import Haskell.Prim.Either
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Monad
+open import Haskell.Prim.Show
+open import Haskell.Prim.String
 
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 
-assert : (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
+record Exception (e : Set) : Set where
+  no-eta-equality
+  field
+    overlap {{iShow}} : Show e
+    displayException : e → String
+
+postulate
+  IOException : Set
+  instance
+    iEqIOException : Eq IOException
+    iExceptionIOException : Exception IOException
+
+  AssertionFailed : Set
+  instance
+    iExceptionAssertionFailed : Exception AssertionFailed
+
+postulate
+  @0 MayThrow : Set → Set
+
+  throw : {{Exception e}} → @0 {{MayThrow e}} → e → a
+  throwIO : {{Exception e}} → e → IO a
+
+  catch : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → (e → IO a) → IO a
+  catchJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → (b → IO a) → IO a
+
+handle : {{Exception e}} → (e → IO a) → (@0 {{MayThrow e}} → IO a) → IO a
+handle = flip catch
+
+handleJust : {{Exception e}} → (e → Maybe b) → (b → IO a) → (@0 {{MayThrow e}} → IO a) → IO a
+handleJust f = flip (catchJust f)
+
+try : {{Exception e}} → IO a → IO (Either e a)
+try a = catch (fmap Right a) (return ∘ Left)
+
+tryJust : {{Exception e}} → (e → Maybe b) → IO a → IO (Either b a)
+tryJust p a = catchJust p (fmap Right a) (return ∘ Left)
+
+assert : @0{{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
-assert _ {{False ⟨ _ ⟩}} x = oops
-  where postulate oops : _
+assert _ {{False ⟨ _ ⟩}} x = throw oops
+  where postulate oops : AssertionFailed

From f2af165c5a7493fd7366751a29e216c599af5e56 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 18 Nov 2025 15:19:06 +0100
Subject: [PATCH 02/11] [ #432 ] Update test cases using assert

---
 lib/base/Haskell/Control/Exception.agda | 2 +-
 test/Assert.agda                        | 2 +-
 test/RuntimeCast.agda                   | 8 +++++---
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index a80ca1d0..79748632 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -50,7 +50,7 @@ try a = catch (fmap Right a) (return ∘ Left)
 tryJust : {{Exception e}} → (e → Maybe b) → IO a → IO (Either b a)
 tryJust p a = catchJust p (fmap Right a) (return ∘ Left)
 
-assert : @0{{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
+assert : @0 {{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
 assert _ {{False ⟨ _ ⟩}} x = throw oops
   where postulate oops : AssertionFailed
diff --git a/test/Assert.agda b/test/Assert.agda
index e3145162..279e20c2 100644
--- a/test/Assert.agda
+++ b/test/Assert.agda
@@ -4,7 +4,7 @@ open import Haskell.Control.Exception
 open import Haskell.Law.Ord
 open import Haskell.Extra.Dec
 
-subtractChecked : Nat → Nat → Nat
+subtractChecked : @0 {{MayThrow AssertionFailed}} → Nat → Nat → Nat
 subtractChecked x y = assert (IsFalse (x < y)) (x - y)
 
 {-# COMPILE AGDA2HS subtractChecked #-}
diff --git a/test/RuntimeCast.agda b/test/RuntimeCast.agda
index 2cac8300..c9e0a9ed 100644
--- a/test/RuntimeCast.agda
+++ b/test/RuntimeCast.agda
@@ -14,8 +14,8 @@ it : {{A}} → A
 it {{x}} = x
 
 data _~_ : (A : Set) (B : Set) → Set₁
-cast  : A ~ B → A → B
-cast' : A ~ B → B → A
+cast  : @0 {{MayThrow AssertionFailed}} → A ~ B → A → B
+cast' : @0 {{MayThrow AssertionFailed}} → A ~ B → B → A
 
 data _~_ where
   refl : A ~ A
@@ -78,7 +78,9 @@ module Sqrt where
 
   {-# COMPILE AGDA2HS eqr inline #-}
 
-  checkedSqrt : (x : Double) → ∃ Double (λ y → IsTrue (y >= 0) × IsTrue (abs (x - y * y) <= 0.01))
+  checkedSqrt : @0 {{MayThrow AssertionFailed}}
+              → (x : Double)
+              → ∃ Double (λ y → IsTrue (y >= 0) × IsTrue (abs (x - y * y) <= 0.01))
   checkedSqrt = cast eqr mySqrt
 
   {-# COMPILE AGDA2HS checkedSqrt #-}

From 2d94386a8278201cf5127974fdc30f91444366ec Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 18 Nov 2025 15:23:28 +0100
Subject: [PATCH 03/11] [ #432 ] Also add MayThrow constraint to throwIO, try,
 and tryJust

---
 lib/base/Haskell/Control/Exception.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index 79748632..5c89dd60 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -33,7 +33,7 @@ postulate
   @0 MayThrow : Set → Set
 
   throw : {{Exception e}} → @0 {{MayThrow e}} → e → a
-  throwIO : {{Exception e}} → e → IO a
+  throwIO : {{Exception e}} → @0 {{MayThrow e}} → e → IO a
 
   catch : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → (e → IO a) → IO a
   catchJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → (b → IO a) → IO a
@@ -44,10 +44,10 @@ handle = flip catch
 handleJust : {{Exception e}} → (e → Maybe b) → (b → IO a) → (@0 {{MayThrow e}} → IO a) → IO a
 handleJust f = flip (catchJust f)
 
-try : {{Exception e}} → IO a → IO (Either e a)
+try : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → IO (Either e a)
 try a = catch (fmap Right a) (return ∘ Left)
 
-tryJust : {{Exception e}} → (e → Maybe b) → IO a → IO (Either b a)
+tryJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → IO (Either b a)
 tryJust p a = catchJust p (fmap Right a) (return ∘ Left)
 
 assert : @0 {{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a

From ff3a7822f601adf753b78022360c8d66853738bc Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 18 Nov 2025 15:25:11 +0100
Subject: [PATCH 04/11] [ #432 ] Make Exception into an actual class

---
 lib/base/Haskell/Control/Exception.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index 5c89dd60..4a888d0f 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -18,6 +18,9 @@ record Exception (e : Set) : Set where
   field
     overlap {{iShow}} : Show e
     displayException : e → String
+open Exception {{...}} public
+
+{-# COMPILE AGDA2HS Exception existing-class #-}
 
 postulate
   IOException : Set

From 027fce07bef6fb1b71e133400378b4ac136a26f7 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 18 Nov 2025 16:58:04 +0100
Subject: [PATCH 05/11] [ #432 ] Add IOError, userError, ioException, and
 ioError

---
 lib/base/Haskell/Control/Exception.agda | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index 4a888d0f..7871d2a0 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -28,6 +28,12 @@ postulate
     iEqIOException : Eq IOException
     iExceptionIOException : Exception IOException
 
+IOError = IOException
+
+postulate
+  userError : String → IOError
+
+postulate
   AssertionFailed : Set
   instance
     iExceptionAssertionFailed : Exception AssertionFailed
@@ -57,3 +63,9 @@ assert : @0 {{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} →
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
 assert _ {{False ⟨ _ ⟩}} x = throw oops
   where postulate oops : AssertionFailed
+
+ioException : @0 {{MayThrow IOException}} → IOException → IO a
+ioException = throwIO
+
+ioError : @0 {{MayThrow IOError}} → IOError → IO a
+ioError = ioException

From 57c6cc6f859465f08c733226c59ad961aaf5f65c Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 18 Nov 2025 17:09:12 +0100
Subject: [PATCH 06/11] [ #433 ] Add Haskell.System.Environment

---
 lib/base/Haskell/System/Environment.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 lib/base/Haskell/System/Environment.agda

diff --git a/lib/base/Haskell/System/Environment.agda b/lib/base/Haskell/System/Environment.agda
new file mode 100644
index 00000000..9134270f
--- /dev/null
+++ b/lib/base/Haskell/System/Environment.agda
@@ -0,0 +1,18 @@
+
+open import Haskell.Prelude
+open import Haskell.Control.Exception
+
+module Haskell.System.Environment where
+
+postulate
+  getArgs : IO (List String)
+  getProgName : IO String
+  executablePath : Maybe (IO (Maybe FilePath))
+  getExecutablePath : IO FilePath
+  getEnv : @0 {{MayThrow IOException}} → String → IO String
+  lookupEnv : String → IO (Maybe String)
+  setEnv : @0 {{MayThrow IOException}} → String → String → IO ⊤
+  unsetEnv : @0 {{MayThrow IOException}} → String → IO ⊤
+  withArgs : List String → IO a → IO a
+  withProgName : String → IO a → IO a
+  getEnvironment : IO (List (String × String))

From d567a63094ad7272b9c33cb8ecb784a6285a0a91 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 20 Nov 2025 16:55:35 +0100
Subject: [PATCH 07/11] Rename TypeError ->  UnsatisfiedConstraint

---
 lib/base/Haskell/Prelude.agda      | 2 +-
 lib/base/Haskell/Prim.agda         | 2 +-
 lib/base/Haskell/Prim/Int.agda     | 2 +-
 lib/base/Haskell/Prim/Integer.agda | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda
index dbe4b34e..8f3e4d25 100644
--- a/lib/base/Haskell/Prelude.agda
+++ b/lib/base/Haskell/Prelude.agda
@@ -6,7 +6,7 @@ open Haskell.Prim public using
   ( Type;
     Bool; True; False; Char; Integer;
     List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
+    UnsatisfiedConstraint; ⊥; iNumberNat; lengthNat;
     IsTrue; IsFalse; NonEmpty;
     All; allNil; allCons;
     Any; anyHere; anyThere;
diff --git a/lib/base/Haskell/Prim.agda b/lib/base/Haskell/Prim.agda
index 43b52006..62a7fc94 100644
--- a/lib/base/Haskell/Prim.agda
+++ b/lib/base/Haskell/Prim.agda
@@ -124,7 +124,7 @@ data IsFalse : Bool → Type where
 data NonEmpty {a : Type} : List a → Type where
   instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
 
-data TypeError (err : AgdaString) : Type where
+data UnsatisfiedConstraint (err : AgdaString) : Type where
 
 it : ∀ {@0 ℓ} {@0 a : Type ℓ} → ⦃ a ⦄ → a
 it ⦃ x ⦄ = x
diff --git a/lib/base/Haskell/Prim/Int.agda b/lib/base/Haskell/Prim/Int.agda
index 095940f5..c7f4a946 100644
--- a/lib/base/Haskell/Prim/Int.agda
+++ b/lib/base/Haskell/Prim/Int.agda
@@ -103,7 +103,7 @@ showInt a = showInteger (intToInteger a)
 
 @0 IsNonNegativeInt : Int → Type
 IsNonNegativeInt a@(int64 _) =
-  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
+  if isNegativeInt a then UnsatisfiedConstraint (primStringAppend (primStringFromList (showInt a)) " is negative")
                      else ⊤
 
 intToNat : (a : Int) → @0 ⦃ IsNonNegativeInt a ⦄ → Nat
diff --git a/lib/base/Haskell/Prim/Integer.agda b/lib/base/Haskell/Prim/Integer.agda
index 3496b9c9..3d0fc4a9 100644
--- a/lib/base/Haskell/Prim/Integer.agda
+++ b/lib/base/Haskell/Prim/Integer.agda
@@ -103,4 +103,4 @@ isNegativeInteger (negsuc _) = True
 @0 IsNonNegativeInteger : Integer → Type
 IsNonNegativeInteger (pos _)      = ⊤
 IsNonNegativeInteger n@(negsuc _) =
-  TypeError (primStringAppend (primShowInteger n) (" is negative"))
+  UnsatisfiedConstraint (primStringAppend (primShowInteger n) (" is negative"))

From 6771965c80eba985b05b629dfbad770ea85d14d8 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 20 Nov 2025 16:56:32 +0100
Subject: [PATCH 08/11] [ refactor ] Avoid importing Prelude in Extra.Dec and
 Extra.Refinement

---
 lib/base/Haskell/Extra/Dec.agda        | 7 +++++--
 lib/base/Haskell/Extra/Refinement.agda | 7 ++-----
 lib/base/Haskell/Prim.agda             | 2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/lib/base/Haskell/Extra/Dec.agda b/lib/base/Haskell/Extra/Dec.agda
index 4bbdffc6..e1915b4c 100644
--- a/lib/base/Haskell/Extra/Dec.agda
+++ b/lib/base/Haskell/Extra/Dec.agda
@@ -1,11 +1,14 @@
 module Haskell.Extra.Dec where
 
-open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
 open import Haskell.Extra.Refinement
+
 open import Agda.Primitive
 
 private variable
-  ℓ : Level
   P : Type
 
 @0 Reflects : Type ℓ → Bool → Type ℓ
diff --git a/lib/base/Haskell/Extra/Refinement.agda b/lib/base/Haskell/Extra/Refinement.agda
index d8621f6a..85428087 100644
--- a/lib/base/Haskell/Extra/Refinement.agda
+++ b/lib/base/Haskell/Extra/Refinement.agda
@@ -1,10 +1,7 @@
 module Haskell.Extra.Refinement where
 
-open import Haskell.Prelude
-open import Agda.Primitive
-
-private variable
-  ℓ ℓ′ : Level
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
 
 record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
   constructor _⟨⟩
diff --git a/lib/base/Haskell/Prim.agda b/lib/base/Haskell/Prim.agda
index 62a7fc94..bcca37c9 100644
--- a/lib/base/Haskell/Prim.agda
+++ b/lib/base/Haskell/Prim.agda
@@ -23,7 +23,7 @@ open import Agda.Builtin.Strict     public
 open import Agda.Builtin.List       public
 
 variable
-  @0 ℓ : Level
+  @0 ℓ ℓ′ : Level
   a b c d e : Type
   f m s t : Type → Type
 

From bb7cd81d98a602b522003aa01c824c8c55c39d29 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 20 Nov 2025 17:00:42 +0100
Subject: [PATCH 09/11] Move IOError, ioError, and userError to Haskell.Prelude

---
 lib/base/Haskell/Control/Exception.agda |  8 --------
 lib/base/Haskell/Prelude.agda           | 12 ++++++++++++
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index 7871d2a0..ea3a1589 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -28,11 +28,6 @@ postulate
     iEqIOException : Eq IOException
     iExceptionIOException : Exception IOException
 
-IOError = IOException
-
-postulate
-  userError : String → IOError
-
 postulate
   AssertionFailed : Set
   instance
@@ -66,6 +61,3 @@ assert _ {{False ⟨ _ ⟩}} x = throw oops
 
 ioException : @0 {{MayThrow IOException}} → IOException → IO a
 ioException = throwIO
-
-ioError : @0 {{MayThrow IOError}} → IOError → IO a
-ioError = ioException
diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda
index 8f3e4d25..5b529bf5 100644
--- a/lib/base/Haskell/Prelude.agda
+++ b/lib/base/Haskell/Prelude.agda
@@ -43,6 +43,8 @@ open import Haskell.Prim.Traversable public
 open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
 open import Haskell.Prim.Word        public
 
+open import Haskell.Control.Exception
+
 -- Problematic features
 --  - [Partial]:  Could pass implicit/instance arguments to prove totality.
 --  - [Float]:    Or Float (Agda floats are Doubles)
@@ -127,6 +129,16 @@ lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
 lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
+-------------------------------------------------
+-- Exception handling in the I/O monad
+
+IOError = IOException
+
+ioError : @0 {{MayThrow IOError}} → IOError → IO a
+ioError = throwIO
+
+postulate
+  userError : String → IOError
 
 -------------------------------------------------
 -- Unsafe functions

From 06ce5f24645cfaa7934a3f4c63d6bfde5330ccbb Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 20 Nov 2025 17:01:20 +0100
Subject: [PATCH 10/11] Add a bunch of additional functionality to
 Control.Exception

---
 lib/base/Haskell/Control/Exception.agda | 91 +++++++++++++++++++++++--
 1 file changed, 87 insertions(+), 4 deletions(-)

diff --git a/lib/base/Haskell/Control/Exception.agda b/lib/base/Haskell/Control/Exception.agda
index ea3a1589..6ed8fe3d 100644
--- a/lib/base/Haskell/Control/Exception.agda
+++ b/lib/base/Haskell/Control/Exception.agda
@@ -7,12 +7,16 @@ open import Haskell.Prim.Functor
 open import Haskell.Prim.IO
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Monad
+open import Haskell.Prim.Ord
 open import Haskell.Prim.Show
 open import Haskell.Prim.String
 
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 
+private variable
+  e1 e2 : Set
+
 record Exception (e : Set) : Set where
   no-eta-equality
   field
@@ -28,10 +32,77 @@ postulate
     iEqIOException : Eq IOException
     iExceptionIOException : Exception IOException
 
-postulate
-  AssertionFailed : Set
-  instance
-    iExceptionAssertionFailed : Exception AssertionFailed
+data ArithException : Set where
+  Overflow UnderFlow LossOfPrecision DivideByZero Denormal : ArithException
+  RatioZeroDenominator : ArithException
+
+postulate instance
+  iOrdArithException : Ord ArithException
+  iExceptionArithException : Exception ArithException
+
+data ArrayException : Set where
+  IndexOutOfBounds UndefinedElement : String → ArrayException
+
+postulate instance
+  iOrdArrayException : Ord ArrayException
+  iExceptionArrayException : Exception ArrayException
+
+record AssertionFailed : Set where
+  no-eta-equality; pattern
+  field theFailedAssertion : String
+
+postulate instance
+  iExceptionAssertionFailed : Exception AssertionFailed
+
+record NoMethodError : Set where
+  no-eta-equality; pattern
+  field theNoMethodError : String
+
+postulate instance
+  iExceptionNoMethodError : Exception NoMethodError
+
+record PatternMatchFail : Set where
+  no-eta-equality; pattern
+  field thePatternMatchFail : String
+
+postulate instance
+  iExceptionPatternMatchFail : Exception PatternMatchFail
+
+record RecConError : Set where
+  no-eta-equality; pattern
+  field theRecConError : String
+
+postulate instance
+  iExceptionRecConError : Exception RecConError
+
+record RecSelError : Set where
+  no-eta-equality; pattern
+  field theRecSelError : String
+
+postulate instance
+  iExceptionRecSelError : Exception RecSelError
+
+record RecUpdError : Set where
+  no-eta-equality; pattern
+  field theRecUpdError : String
+
+postulate instance
+  iExceptionRecUpdError : Exception RecUpdError
+
+record ErrorCall : Set where
+  no-eta-equality; pattern
+  field theErrorCall : String
+
+postulate instance
+  iOrdErrorCall : Ord ErrorCall
+  iExceptionErrorCall : Exception ErrorCall
+
+record TypeError : Set where
+  no-eta-equality; pattern
+  field theTypeError : String
+
+postulate instance
+  iExceptionTypeError : Exception TypeError
 
 postulate
   @0 MayThrow : Set → Set
@@ -39,6 +110,7 @@ postulate
   throw : {{Exception e}} → @0 {{MayThrow e}} → e → a
   throwIO : {{Exception e}} → @0 {{MayThrow e}} → e → IO a
 
+postulate
   catch : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → (e → IO a) → IO a
   catchJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → (b → IO a) → IO a
 
@@ -54,10 +126,21 @@ try a = catch (fmap Right a) (return ∘ Left)
 tryJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → IO (Either b a)
 tryJust p a = catchJust p (fmap Right a) (return ∘ Left)
 
+postulate
+  evaluate : a → IO a
+  mapException : {{Exception e1}} → {{Exception e2}} → (e1 → e2) → a → a
+
 assert : @0 {{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
 assert _ {{False ⟨ _ ⟩}} x = throw oops
   where postulate oops : AssertionFailed
 
+postulate
+  bracket : IO a → (a → IO b) → (a → IO c) → IO c
+  bracket_ : IO a → IO b → IO c → IO c
+  bracketOnError : IO a → (a → IO b) → (a → IO c) → IO c
+  finally : IO a → IO b → IO a
+  onException : IO a → IO b → IO a
+
 ioException : @0 {{MayThrow IOException}} → IOException → IO a
 ioException = throwIO

From 5206c0567568d2060e30325100cd3c46cb2420dd Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 20 Nov 2025 15:02:53 +0100
Subject: [PATCH 11/11] Add test case using exceptions and System.Environment
 functions

---
 test/AllTests.agda             |  2 ++
 test/ParseOrValidate.agda      | 57 ++++++++++++++++++++++++++++++++++
 test/golden/AllTests.hs        |  1 +
 test/golden/ParseOrValidate.hs | 36 +++++++++++++++++++++
 4 files changed, 96 insertions(+)
 create mode 100644 test/ParseOrValidate.agda
 create mode 100644 test/golden/ParseOrValidate.hs

diff --git a/test/AllTests.agda b/test/AllTests.agda
index bc786d2b..bc6399e1 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -106,6 +106,7 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -209,4 +210,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate
 #-}
diff --git a/test/ParseOrValidate.agda b/test/ParseOrValidate.agda
new file mode 100644
index 00000000..53f96adc
--- /dev/null
+++ b/test/ParseOrValidate.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --erasure #-}
+
+open import Haskell.Prelude
+open import Haskell.Control.Exception
+open import Haskell.Control.Monad
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Erase
+open import Haskell.Extra.Refinement
+open import Haskell.System.Environment
+
+it : {{a}} → a
+it {{x}} = x
+
+{-# COMPILE AGDA2HS it inline #-}
+
+{-# TERMINATING #-}
+split : Char → String → List String
+split c s = case rest of λ where
+                []     → chunk ∷ []
+                (_ ∷ rest) → chunk ∷ split c rest
+  where
+    broken = break (_== c) s
+    chunk = fst broken
+    rest = snd broken
+
+{-# COMPILE AGDA2HS split #-}
+
+-- The below example is taken from the classic blog post by Alexis King
+-- "Parse, don't validate". Here I ignore her advice but instead implement
+-- a validation function that returns evidence of the property it checked.
+
+validateNonEmpty : @0 {{MayThrow IOException}} → (xs : List a) → IO (Erase (NonEmpty xs))
+validateNonEmpty [] = throwIO (userError "list cannot be empty")
+validateNonEmpty (x ∷ xs) = return it
+
+{-# COMPILE AGDA2HS validateNonEmpty #-}
+
+getConfigurationDirectories : @0 {{MayThrow IOException}} → IO (∃ (List FilePath) NonEmpty)
+getConfigurationDirectories = do
+  configDirsString <- getEnv "CONFIG_DIRS"
+  let configDirsList = split ',' configDirsString
+  validateNonEmpty configDirsList
+  pure (configDirsList ⟨⟩)
+
+{-# COMPILE AGDA2HS getConfigurationDirectories #-}
+
+-- TODO: implement this function?
+postulate
+  initializeCache : String → IO ⊤
+{-# COMPILE AGDA2HS initializeCache #-}
+
+main : @0 {{MayThrow IOException}} → IO ⊤
+main = do
+  configDirs ⟨ i ⟩ <- getConfigurationDirectories
+  initializeCache (head configDirs {{i}})
+
+{-# COMPILE AGDA2HS main #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 8c90d4aa..0fb3df2b 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -101,4 +101,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate
 
diff --git a/test/golden/ParseOrValidate.hs b/test/golden/ParseOrValidate.hs
new file mode 100644
index 00000000..597df7b7
--- /dev/null
+++ b/test/golden/ParseOrValidate.hs
@@ -0,0 +1,36 @@
+module ParseOrValidate where
+
+import Control.Exception (throwIO)
+import System.Environment (getEnv)
+
+split :: Char -> String -> [String]
+split c s
+  = case rest of
+        [] -> [chunk]
+        _ : rest -> chunk : split c rest
+  where
+    broken :: ([Char], [Char])
+    broken = break (== c) s
+    chunk :: [Char]
+    chunk = fst broken
+    rest :: [Char]
+    rest = snd broken
+
+validateNonEmpty :: [a] -> IO ()
+validateNonEmpty [] = throwIO (userError "list cannot be empty")
+validateNonEmpty (x : xs) = return ()
+
+getConfigurationDirectories :: IO [FilePath]
+getConfigurationDirectories
+  = do configDirsString <- getEnv "CONFIG_DIRS"
+       validateNonEmpty (split ',' configDirsString)
+       pure (split ',' configDirsString)
+
+initializeCache :: String -> IO ()
+initializeCache = error "postulate: String -> IO ()"
+
+main :: IO ()
+main
+  = do configDirs <- getConfigurationDirectories
+       initializeCache (head configDirs)
+