checked-exceptions

A monad transformer that allows you to throw and catch a restricted set of exceptions, tracked at the type level.

Requires GHC 9.8+ for the core library. The type-checker plugin (checked-exceptions:plugin) requires GHC 9.10+ with a matching ghc package.

Example

build-depends:
    checked-exceptions
  , checked-exceptions:plugin

ghc-options: -fplugin Control.Monad.CheckedExcept.Plugin

{-# OPTIONS_GHC -fplugin Control.Monad.CheckedExcept.Plugin #-}
{-# LANGUAGE
    TypeApplications
  , DataKinds
  , StandaloneDeriving
  , DerivingVia
  , QualifiedDo
  , FlexibleInstances
#-}

type TestExceptions = '[(), Int, Bool, String]

testCE :: CheckedExceptT TestExceptions IO ()
testCE = CheckedExcept.do
  () <- testCE1 :: CheckedExceptT '[()] IO ()
  () <- testCE2 :: CheckedExceptT '[Int] IO ()
  () <- testCE3 :: CheckedExceptT '[Bool] IO ()
  () <- testCE4 :: CheckedExceptT '[String] IO ()
  -- () <- testCE5 :: CheckedExceptT '[Char] IO () -- doesn't compile
  pure ()

test :: CheckedExcept TestExceptions () -> IO ()
test ce = case runCheckedExcept ce of
  Left e -> do
    applyAll (putStrLn . encodeException) e
    withOneOf @() e $ \() -> putStrLn "()"
    withOneOf @Int e $ \n -> print $ n + 1
    withOneOf @Bool e $ \_ -> pure ()
    caseException e
      (  (\() -> putStrLn "()")
      <: (\n -> print $ n + 1)
      <: CaseAny (\x -> putStrLn $ encodeException x)
      -- <: (\b -> putStrLn "bool")
      -- <: (\s -> putStrLn "string")
      -- <: CaseEnd
      )
  Right () -> putStrLn "Right"

Intentionally or unintentionally, introducing a new possible exception in your code that is presently unaccounted for throws a typ eerror. Since we enforce at the type level what kinds of exceptions are permissible, you can safely trust the exceptions set in the type signature to do something like generate OpenAPI documentation for an HTTP handler's error responses.

When catching an exception, we provide the CaseException type to allow coverage checking with a case-like API (caseException), or you can use methods provided by the CheckedException typeclass to perform common operations on exceptions without inspecting the type of the exception.

Membership witnesses

Elem and Contains are type classes backed by value-level witnesses:

• ElemIx e es: index of e inside es (Here / There)
• Subset es1 es2: every element of es1 appears in es2 (SubRefl, SubNil, SubCons)
• lookupSubset: translate an ElemIx along a Subset witness
• containsRefl: reflexive Subset es es for abstract exception lists

OneOf is constructed with oneOf, not a data constructor pattern. The internal constructor carries an ElemIx witness so subset widening (weakenOneOf, weakenExceptions) is structurally total.

Plugin

Required for QualifiedDo blocks. See the Example for Cabal setup (checked-exceptions:plugin in build-depends plus -fplugin).

The plugin lives in a separate public sublibrary so the core library does not depend on ghc.

The plugin proposes default values for ambiguous exception-list metavariables created by >>= in QualifiedDo blocks (and similar).

GHC verifies each proposal; only a solving assignment is committed. No fiat coercions are emitted

Optional tracing: -fplugin-opt Control.Monad.CheckedExcept.Plugin:verbose

QualifiedDo >>= unions exception sets with Nub (es1 ++ es2) in the result type so binds accumulate exceptions without ambiguous metavariables when possible.

Deriving CheckedException

DerivingVia with ShowException or ExceptionException is supported. fromOneOf unwraps the newtype correctly when reading bare values from OneOf.

Custom CheckedException instances should only return Just from fromOneOf when the payload type matches e (same contract as the default eqT witness path). withOneOf uses that witness path directly and does not depend on a custom fromOneOf.