diff --git a/package.yaml b/package.yaml
index 8c73ad9..3543e12 100644
--- a/package.yaml
+++ b/package.yaml
@@ -80,6 +80,7 @@ library:
   - text
   - hashable
   - deepseq
+  - bytestring
 
 tests:
   pantomime-test:
@@ -92,6 +93,7 @@ tests:
     dependencies:
     - pantomime
     - hspec
+    - hspec-expectations
     - HUnit
     - ghc-paths
     - directory
diff --git a/pantomime.cabal b/pantomime.cabal
index 24b26b9..912a8c2 100644
--- a/pantomime.cabal
+++ b/pantomime.cabal
@@ -49,6 +49,7 @@ library
       Pantomime.Grisette.Mergeable
       Pantomime.Grisette.UnionT
       Pantomime.Literal
+      Pantomime.Marker
       Pantomime.Orphan.GHC
       Pantomime.Orphan.Grisette
       Pantomime.Passes
@@ -56,6 +57,7 @@ library
       Pantomime.Solve
       Pantomime.Subst
       Pantomime.Symbolise
+      Pantomime.TH
       Pantomime.Unification
       Pantomime.Util
   other-modules:
@@ -92,6 +94,7 @@ library
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module
   build-depends:
       base >=4.7 && <5
+    , bytestring
     , composition
     , constraints >=0.14.2
     , containers
@@ -153,6 +156,7 @@ test-suite pantomime-test
     , ghc-paths
     , grisette >=0.13.0.0
     , hspec
+    , hspec-expectations
     , mtl
     , pantomime
     , silently
diff --git a/src/Pantomime.hs b/src/Pantomime.hs
index b8374a6..e2f1172 100644
--- a/src/Pantomime.hs
+++ b/src/Pantomime.hs
@@ -5,6 +5,10 @@ module Pantomime
 
   , Theory (..)
   , PluginAxioms (..)
+  , pantomime
+  , pantomimeMarker
+  , pantomimeNothing
+  , pantomimeJust
   ) where
 
 import GHC.Plugins hiding (empty, (<>))
@@ -12,6 +16,9 @@ import GHC.Plugins hiding (empty, (<>))
 import Pantomime.Annotation
 import Pantomime.Axiom
 import Pantomime.Passes
+import Pantomime.TH (pantomime)
+import Pantomime.Marker
+
 
 plugin :: Plugin
 plugin = defaultPlugin
diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index f6ad2a1..79c04e5 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -236,7 +236,7 @@ instance Monoid PluginAxiomsR where
 resolvePluginAxioms
   :: HasCallStack
   -- TODO: Adjust these errors!
-  => Error () :> es
+  => Error String :> es
   => Error (LookupError TH.Name) :> es
   => Error (LookupError Name) :> es
   => THNameToGHCName :> es
@@ -350,7 +350,7 @@ resolvePluginAxioms PluginAxioms { .. } = do
 
     -- Throw an error if we could not create any.
     when (null dictsNew) do
-      throwError ()
+      throwError @String "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms"
 
     -- Insert all dictionaries.
     pure $ foldlBy dicts dictsNew \acc dict -> do
diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs
index ccd3427..cb2e43d 100644
--- a/src/Pantomime/BuiltIn.hs
+++ b/src/Pantomime/BuiltIn.hs
@@ -626,6 +626,7 @@ pattern False <- (convert -> Prelude.False)
 {-# COMPLETE True, False #-}
 
 -- | Convert the standard Haskell Boolean to a symbolic Boolean.
+{-# INLINE boolean #-}
 boolean :: Prelude.Bool -> Bool
 boolean = \case
   Prelude.True -> True
diff --git a/src/Pantomime/Embed.hs b/src/Pantomime/Embed.hs
index 99ff8f0..93a8970 100644
--- a/src/Pantomime/Embed.hs
+++ b/src/Pantomime/Embed.hs
@@ -274,7 +274,7 @@ embed
   :: forall a es
    . HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Reflect a
@@ -287,7 +287,7 @@ project
   :: forall a es
    . HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Reflect a
@@ -301,7 +301,7 @@ project subst = project' subst $ reflect @a
 embed'
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Subst
@@ -323,7 +323,7 @@ embed' subst sty repr = case sty of
     Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty
     let co' = mkSymCo $ mkSubCo co
     mkCast lit co'
-  SPrimitiveTy _ -> throwE ()
+  SPrimitiveTy _ -> throwE @String "embed': cannot directly embed a PrimitiveTy — use project' first"
   SLambda aty rty -> do
     -- Gather the type for the lambda.
     ty <- liftEff $ embedSTy subst sty
@@ -353,8 +353,8 @@ embed' subst sty repr = case sty of
   SNaturalTy -> hoistEff repr >>= absurd
   SNatural -> hoistEff repr >>= absurd
   SAddTy _ _ -> hoistEff repr >>= absurd
-  SLEqTy _ _ -> throwE ()
-  SKnownNatTy _n -> throwE ()
+  SLEqTy _ _ -> throwE @String "embed': SLEqTy cannot be embedded directly"
+  SKnownNatTy _n -> throwE @String "embed': SKnownNatTy cannot be embedded directly"
   STYPE _ -> absurd <$> hoistEff repr
   SRuntimeRepTy -> absurd <$> hoistEff repr
   SBoxedRep _ -> absurd <$> hoistEff repr
@@ -363,12 +363,12 @@ embed' subst sty repr = case sty of
   SUnsafeEqualityTy {} -> do
     -- Get the type of the expression.
     ty <- liftEff $ embedSTy subst sty
-    (tc, args) <- failWithE () $ splitTyConApp_maybe ty
+    (tc, args) <- failWithE @String "embed': expected TyCon application for UnsafeEqualityTy" $ splitTyConApp_maybe ty
 
     -- Fetch the 'UnsafeRefl' DataCon.
     dc <- case tyConDataCons_maybe tc of
       Just [dc] -> pure dc
-      _ -> throwE ()
+      _ -> throwE @String "embed': expected a single data constructor for UnsafeEqualityTy"
 
     -- Construct the spine.
     let spine = mkCon $ mkDataCon @64 dc
@@ -376,7 +376,7 @@ embed' subst sty repr = case sty of
     -- Fetch the type arguments directly.
     (kind, tyL, tyR) <- case args of
       [kind, tyL, tyR] -> pure (kind, tyL, tyR)
-      _ -> throwE ()
+      _ -> throwE @String "embed': expected exactly three type arguments for UnsafeEqualityTy"
 
     -- Force the coercion.
     co <- hoistEff repr
@@ -387,7 +387,7 @@ embed' subst sty repr = case sty of
 project'
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Subst
@@ -397,24 +397,24 @@ project'
 project' subst sty expr = case sty of
   SBoolTy -> hoistEff expr >>= \case
     Lit (Bool b) -> pure b
-    _ -> throwE ()
+    _ -> throwE @String "project': expected a Bool literal"
   SIntegerTy -> hoistEff expr >>= \case
     Lit (Integer i) -> pure i
-    _ -> throwE ()
+    _ -> throwE @String "project': expected an Integer literal"
   SBitVecTy _n -> do
     Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty
     inner <- hoistEff expr
     expr' <- mkCast inner $ mkSubCo co
     case expr' of
       Lit (BitVec bv) -> pure $ SomeBitVec bv
-      _ -> throwE ()
+      _ -> throwE @String "project': expected a BitVec literal"
   SArrayTy _ _ -> do
     Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty
     inner <- hoistEff expr
     expr' <- mkCast inner $ mkSubCo co
     case expr' of
       Lit (Array bv) -> pure $ SomeArray bv
-      _ -> throwE ()
+      _ -> throwE @String "project': expected an Array literal"
   SPrimitiveTy pty -> do
     _ <- hoistEff expr
     pty' <- liftEff $ embedSTy subst pty
@@ -440,9 +440,9 @@ project' subst sty expr = case sty of
     Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty
     repr <- hoistEff expr
     mkCast repr $ mkSubCo co
-  SNaturalTy -> throwE ()
-  SNatural -> throwE ()
-  SAddTy _ _ -> throwE ()
+  SNaturalTy -> throwE @String "project': SNaturalTy cannot be projected directly"
+  SNatural -> throwE @String "project': SNatural cannot be projected directly"
+  SAddTy _ _ -> throwE @String "project': SAddTy cannot be projected directly"
   SLEqTy _ _ -> do
     -- TODO: I guess we should actually ensure that this is well formed? It's
     -- a type family though, so I'm not sure how much actually remains of this
@@ -455,7 +455,7 @@ project' subst sty expr = case sty of
     -- Construct a coercion from the Pantomime 'KnownNat' to 'Integer'. Note
     -- that we do not want to fully instantiate newtypes as this would lead us
     -- to the Haskell 'Integer'.
-    co <- failWithE () do
+    co <- failWithE @String "project': could not construct KnownNat to Integer coercion" do
       (tc, args) <- splitTyConApp_maybe ty
       (ty', co) <- instNewTyCon_maybe tc args
       (tc', args') <- splitTyConApp_maybe ty'
@@ -471,18 +471,18 @@ project' subst sty expr = case sty of
       -- value, the error should be something closed to an 'unknown' SMT solver
       -- result. Nothing in fact is invalid, it is just not solvable.
       Lit (Integer i) | Just n <- toCon i >>= someNatVal -> pure n
-      _ -> throwE ()
-  STYPE _ -> throwE ()
-  SRuntimeRepTy -> throwE ()
-  SBoxedRep _ -> throwE ()
-  SLevityTy -> throwE ()
-  SLifted -> throwE ()
+      _ -> throwE @String "project': expected a concrete Integer for KnownNat projection"
+  STYPE _ -> throwE @String "project': STYPE cannot be projected directly"
+  SRuntimeRepTy -> throwE @String "project': SRuntimeRepTy cannot be projected directly"
+  SBoxedRep _ -> throwE @String "project': SBoxedRep cannot be projected directly"
+  SLevityTy -> throwE @String "project': SLevityTy cannot be projected directly"
+  SLifted -> throwE @String "project': SLifted cannot be projected directly"
   SUnsafeEqualityTy {} -> do
     expr' <- hoistEff expr
     let (_spine, args) = collectArgs expr'
     case args of
       [_kind, _ty, co] -> liftEff $ forceCo co
-      _ -> throwE ()
+      _ -> throwE @String "project': expected exactly three arguments for UnsafeEqualityTy"
 
 embedSTy
   :: HasCallStack
diff --git a/src/Pantomime/Expr.hs b/src/Pantomime/Expr.hs
index cf46045..9e7ffb5 100644
--- a/src/Pantomime/Expr.hs
+++ b/src/Pantomime/Expr.hs
@@ -76,7 +76,9 @@ import GHC.Utils.Outputable
   ( Outputable (..)
   , IsLine (..)
   , SDoc
+  , text
   , ($+$)
+  , (<+>)
   , parens
   , hang
   , nest
@@ -437,16 +439,16 @@ mkEnumCon
   :: forall n es
    . KnownPos n
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => SymBitVec n
   -> Type
   -> Eval es Expr
 mkEnumCon tag ty = do
   -- Ensure we have an enumeration type.
-  (tc, targs) <- failWithE () $ splitTyConApp_maybe ty
+  (tc, targs) <- failWithE @String "Expected a TyCon application for enumeration type" $ splitTyConApp_maybe ty
   unless (isEnumerationTyCon tc) do
-    throwE ()
+    throwE @String "Expected an enumeration TyCon for mkEnumCon"
 
   -- Construct the data constructor and its type arguments.
   let dc = mkCon $ EnumCon tag tc
@@ -461,7 +463,7 @@ constructorTyCon = \case
 
 -- | Get the 'Type' of a constructor.
 constructorType
-  :: Error () :> es
+  :: Error String :> es
   => Constructor
   -> Eff es Type
 constructorType con = do
@@ -469,7 +471,7 @@ constructorType con = do
     DataCon dc -> pure dc
     EnumCon _tag tc
       | dc : _ <- tyConDataCons tc -> pure dc
-      | otherwise -> throwError ()
+      | otherwise -> throwError @String "Cannot get constructor type: enumeration TyCon has no data constructors"
   pure $ varType (dataConWorkId dc)
 
 pprExpr
@@ -607,7 +609,7 @@ mkLam ty closure = Lam ty <$> deferE closure
 mkApp
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> Arg
@@ -626,12 +628,12 @@ mkApp fun arg = case fun of
       | isForAllTy ty -> do
         forced <- forceTyCo arg
         pure $ App fun (Forced forced)
-      | otherwise -> throwError ()
+      | otherwise -> throwError @String "Cannot apply argument: expression type is neither a function nor a forall"
 
 pushCoArg
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => CoercionR
   -> Arg
@@ -643,14 +645,14 @@ pushCoArg co arg = if
     ty <- forceTy arg
 
     -- Attempt to push the coercion into the type argument.
-    (ty', rco) <- failWith () $ pushCoTyArg co ty
+    (ty', rco) <- failWith @String "pushCoArg: could not push coercion into type argument" $ pushCoTyArg co ty
 
     -- Return the type argument and result coercion.
     pure (pure $ mkType ty', rco)
 
   | otherwise -> do
     -- Attempt to split the coercion into an argument and result coercion.
-    (aco, rco) <- failWith () $ pushCoValArg co
+    (aco, rco) <- failWith @String "pushCoArg: could not push coercion into value argument" $ pushCoValArg co
 
     -- Cast the argument and return the result coercion.
     arg' <- defer do
@@ -662,7 +664,7 @@ pushCoArg co arg = if
 mkApps
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> [Arg]
@@ -671,7 +673,7 @@ mkApps = foldM mkApp
 
 mkCastMCo
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> MCoercionR
@@ -682,7 +684,7 @@ mkCastMCo expr = \case
 
 mkCast
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> CoercionR
@@ -690,14 +692,12 @@ mkCast
 mkCast expr co = do
   -- Ensure the coercion has role representational.
   unless (coercionRole co == Representational) do
-    -- FIXME: Make this a proper error.
-    throwE ()
+    throwE @String "mkCast: coercion role must be Representational"
 
   -- Ensure the cast can be applied to the expression.
   ty <- liftEff $ exprType expr
   unless (eqType ty $ coercionLKind co) do
-    -- FIXME: Make this a proper error.
-    throwE ()
+    throwE @String "mkCast: expression type does not match coercion source type"
 
   case expr of
     Cast body co' -> do
@@ -746,7 +746,7 @@ mkRaise = mkVariant . Raise
 forceTyCo
   :: forall es
    . HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Arg
   -> Eff es (Either Type Coercion)
 forceTyCo = runRuntime >>> \case
@@ -756,30 +756,30 @@ forceTyCo = runRuntime >>> \case
     | Coercion co <- value -> pure $ Right co
 
   -- The expression was not in the expected shape.
-  _ -> throwError ()
+  _ -> throwError @String "forceTyCo: expected a single Type or Coercion expression"
 
 -- | Force an expression into a type using 'forceTyCo'.
 forceTy
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Arg
   -> Eff es Type
-forceTy = forceTyCo >=> either pure (const $ throwError ())
+forceTy = forceTyCo >=> either pure (const $ throwError @String "forceTy: expected a Type, got a Coercion")
 
 -- | Force an expression into a coercion using 'forceTyCo'.
 forceCo
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Arg
   -> Eff es Coercion
-forceCo = forceTyCo >=> either (const $ throwError ()) pure
+forceCo = forceTyCo >=> either (const $ throwError @String "forceCo: expected a Coercion, got a Type") pure
 
 -- | Equivalence between constructors.
 --
 -- Will throw an error if the types do not match.
 eqCon
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Constructor
   -> Constructor
   -> Eff es SymBool
@@ -789,20 +789,20 @@ eqCon = \cases
   (EnumCon @l ltag ltc) (EnumCon @r rtag rtc)
     | ltc == rtc
     , Just Refl <- eqT @l @r -> pure $ ltag .== rtag
-  _ _ -> throwError ()
+  _ _ -> throwError @String "eqCon: mismatched constructor types"
 
 -- TODO: This function deserves some clean-up! My syntax highlighter is even
 -- breaking on it...
 exprType
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> Eff es Type
 exprType = \case
   Lit lit -> embedLitTyOf lit
   Con con -> constructorType con
-  Type _ -> throwError ()
+  Type _ -> throwError @String "exprType: cannot get the type of a Type expression"
   Coercion co -> pure $ coercionType co
   Lam ty _ -> pure ty
   App fun arg -> do
@@ -813,14 +813,14 @@ exprType = \case
         aty <- case arg of
           Forced (Right co) -> pure $ mkCoercionTy co
           Forced (Left ty) -> pure ty
-          _ -> throwError ()
+          _ -> throwError @String "exprType: expected a forced Type or Coercion argument"
         let scope = mkInScopeSet $ tyCoVarsOfTypes [aty, rty]
         let subst = GHC.extendTCvSubst (GHC.mkEmptySubst scope) var aty
         pure $ GHC.substTy subst rty
 
       | Just (_, _, _, rty) <- splitFunTy_maybe fty -> pure rty
 
-      | otherwise -> throwError ()
+      | otherwise -> throwError @String "exprType: expected a function or forall type in application"
   Cast _ co -> pure $ coercionRKind co
 
 -- | Collect the arguments of an application.
@@ -868,7 +868,7 @@ unthunk = \case
 collectScrut
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Expr
   -> Eval es (Either Expr Constructor, [Arg])
@@ -883,7 +883,7 @@ collectScrut = \case
     let (spine, args) = collectThunks body'
     spine' <- case spine of
       Con lit -> pure lit
-      _ -> throwE ()
+      _ -> throwE @String "collectScrut: expected a constructor at the spine of a cast expression"
 
     -- Only a DataCon spine may have its arguments pushed.
     dc <- case spine' of
@@ -891,7 +891,7 @@ collectScrut = \case
       -- Any Enum DataCon suffices, as we only use its type (and all enum con
       -- have the same type).
       EnumCon _ tc | dc : _ <- tyConDataCons tc -> pure dc
-      _ -> throwE ()
+      _ -> throwE @String "collectScrut: expected a DataCon or EnumCon with data constructors"
 
     -- Push the coercion into the arguments.
     (_univ, args') <- liftEff $ pushCoDataCon dc args co
@@ -917,7 +917,7 @@ collectScrut = \case
 pushCoDataCon
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => DataCon
   -> [Thunk]
@@ -926,9 +926,9 @@ pushCoDataCon
 pushCoDataCon dc args co = do
   -- Check whether the outer type is a TyConAppCo.
   let tyR = coercionRKind co
-  (tcR, univArgsR) <- failWith () $ splitTyConApp_maybe tyR
+  (tcR, univArgsR) <- failWith @String "pushCoDataCon: expected a TyConApp coercion" $ splitTyConApp_maybe tyR
   unless (tcR == dataConTyCon dc) do
-    throwError ()
+    throwError @String "pushCoDataCon: TyCon mismatch in coercion"
 
   -- Gather information on type variables of the DataCon.
   let dcUnivVars = dataConUnivTyVars dc
@@ -940,10 +940,10 @@ pushCoDataCon dc args co = do
     exTys <- for exArgs \case
       -- TODO: Do we need to wrap Coercions with mkCoercionTy?
       Forced (Left ty) -> pure ty
-      _ -> throwError ()
+      _ -> throwError @String "pushCoDataCon: expected forced type arguments for existential type variables"
     valArgs' <- for valArgs \case
       Thunked value -> pure value
-      Forced _ -> throwError ()
+      Forced _ -> throwError @String "pushCoDataCon: expected thunked value arguments"
     pure (exTys, valArgs')
 
   -- Get coercions for the universal type variables.
diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs
index 0643b9d..e5c5054 100644
--- a/src/Pantomime/Fresh.hs
+++ b/src/Pantomime/Fresh.hs
@@ -12,7 +12,7 @@ import GHC.Core.TyCo.Rep (scaledThing, UnivCoProvenance (..))
 import GHC.Core.TyCon.Env (TyConEnv, lookupTyConEnv)
 import GHC.Core.Unify (tcUnifyTysFG, alwaysBindFun, UnifyResultM (..))
 import GHC.Types.Unique (Uniquable (..), getKey)
-import GHC.Utils.Outputable (Outputable (..))
+import GHC.Utils.Outputable (Outputable (..), text, (<+>), showSDocUnsafe)
 import GHC.Plugins qualified as GHC
 import GHC.Plugins
   ( Var
@@ -159,7 +159,7 @@ symbolicVar var dst = case varArgs var of
 freshExpr
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader FamInstEnvs :> es
   => Context Reader BuiltInTyCon :> es
   => TyConEnv TyCon
@@ -193,7 +193,7 @@ freshExpr axioms root = do
         -- some sort of 'asum' like operation? Actually, NonDet from 'effectful'
         -- would be perfect! We should move the code that deals with
         -- reifyLitType adjecent to its call once we do this!
-        result <- liftEff . runErrorNoCallStack @() $ projectLitTy ty
+        result <- liftEff . runErrorNoCallStack @String $ projectLitTy ty
 
         let isEqPred' ty' = do
               (tc, args) <- splitTyConApp_maybe ty'
@@ -383,10 +383,9 @@ freshExpr axioms root = do
             -- For enum TyCon, we of course do plan to use it, so there we do need
             -- the Unreachable statement.
 
-          -- TODO: Throw proper error!
           | otherwise -> do
             dbgE ["could not create fresh value for", ppr ty]
-            throwE ()
+            throwE $ showSDocUnsafe $ text "Could not create a fresh symbolic value for type:" <+> ppr ty
 
   go Variable
     { varName = GHC.varName root
@@ -398,25 +397,24 @@ freshExpr axioms root = do
 freshArgs
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => TypeAxiomsR
+  -> [String]
   -> Type
   -> InScopeSet
   -> Eff es ([(Var, Arg)], InScopeSet)
-freshArgs axioms ty scope0 = do
+freshArgs axioms valNames ty scope0 = do
   -- Gather the argument types.
   let (tyVars, funTy) = splitForAllTyVars ty
   let (argTys, _resTy) = splitFunTys funTy
 
-  -- TODO: Isn't there some infinite sequence of names that could be used
-  -- instead of this?
-  -- Names for the arguments.
-  let names = repeat "arg"
+  -- Names for the arguments as FastStrings.
+  let names = map GHC.fsLit $ valNames ++ repeat "arg"
 
   -- Create fresh type arguments.
-  let kinds = zip names $ fmap tyVarKind tyVars
+  let kinds = zip (repeat (GHC.fsLit "arg")) $ fmap tyVarKind tyVars
   let (tyArgs, scope1) = freshTyVars kinds scope0
 
   -- Create fresh value arguments.
diff --git a/src/Pantomime/Literal.hs b/src/Pantomime/Literal.hs
index 2b8a3d1..d5d2f16 100644
--- a/src/Pantomime/Literal.hs
+++ b/src/Pantomime/Literal.hs
@@ -47,6 +47,7 @@ import GHC.Plugins
   , Outputable (..)
   , SDoc
   , IsLine (..)
+  , text
   , mkTyConTy
   , mkNumLitTy
   , mkTyConApp
@@ -347,7 +348,7 @@ embedLitTyOf (Literal ty _) = embedLitTy ty
 -- reduced.
 projectLitTy
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Type
@@ -367,13 +368,13 @@ projectLitTy ty = do
 -- any type families or aliases.
 projectLitTy'
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Type
   -> Eff es SomeLiteralType
 projectLitTy' ty = do
   -- TODO: We should fix the recursive callstack grow!
-  (tc, targs) <- failWith () $ splitTyConApp_maybe ty
+  (tc, targs) <- failWith @String "projectLitTy': expected a TyCon application" $ splitTyConApp_maybe ty
   BuiltInTyCon { .. } <- get
   if
     | tc == tcBool
@@ -385,8 +386,8 @@ projectLitTy' ty = do
     | tc == tcBitVec
     , [narg] <- targs -> do
       let knownNatTy = isNumLitTy >=> someNatVal
-      SomeNat @n _ <- failWith () $ knownNatTy narg
-      Dict <- failWith () $ posNat @n
+      SomeNat @n _ <- failWith @String "projectLitTy': expected a KnownNat literal" $ knownNatTy narg
+      Dict <- failWith @String "projectLitTy': expected a positive Nat for BitVec size" $ posNat @n
       pure $ SomeLiteralType (BitVecType @n)
 
     | tc == tcArray
@@ -395,4 +396,4 @@ projectLitTy' ty = do
       SomeLiteralType valTy' <- projectLitTy' valTy
       pure $ SomeLiteralType (ArrayType keyTy' valTy')
 
-    | otherwise -> throwError ()
+    | otherwise -> throwError @String "projectLitTy': unsupported literal type"
diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs
new file mode 100644
index 0000000..4bc8486
--- /dev/null
+++ b/src/Pantomime/Marker.hs
@@ -0,0 +1,18 @@
+module Pantomime.Marker
+  ( pantomimeMarker
+  , pantomimeNothing
+  , pantomimeJust
+  ) where
+
+pantomimeMarker :: String -> Maybe String
+pantomimeMarker name = error $
+  "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass."
+{-# NOINLINE pantomimeMarker #-}
+
+pantomimeNothing :: Maybe String
+pantomimeNothing = Nothing
+{-# NOINLINE pantomimeNothing #-}
+
+pantomimeJust :: String -> Maybe String
+pantomimeJust x = Just x
+{-# NOINLINE pantomimeJust #-}
diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs
index a43469a..58d47b7 100644
--- a/src/Pantomime/Passes.hs
+++ b/src/Pantomime/Passes.hs
@@ -7,6 +7,8 @@ import GHC.Plugins hiding (empty, (<>), thNameToGhcName, getFirstAnnotations)
 import GHC.Core.Lint
 import GHC.Driver.Config.Core.Lint (initLintConfig)
 
+import GHC.Core.Make (mkStringExpr)
+
 import Grisette
   ( GrisetteSMTConfig (..)
   , SMTConfig (..)
@@ -16,13 +18,16 @@ import Grisette
 
 import Data.Data (Data)
 import Data.Traversable (for)
+import Data.Maybe (catMaybes)
+import Data.ByteString.Char8 qualified as BS8
+import Pantomime.Marker
 
 import Control.Error
 
 import Language.Haskell.TH qualified as TH
 
-import Pantomime.Unification
 import Pantomime.Solve
+import Pantomime.Unification
 import Pantomime.Axiom (resolvePluginAxioms)
 import Pantomime.Annotation
 
@@ -100,7 +105,7 @@ runSymbolic
     , Error OversaturatedError
     , Error UnificationError
     , Error SolverError
-    , Error ()
+    , Error String
     , Provider_ Solver ()
     , HasAnnotations
     , THNameToGHCName
@@ -131,7 +136,7 @@ runSymbolic guts
   . runThNameToGhcName
   . runHasAnnotations
   . runProvider_ (const $ runSolver solver)
-  . runErrorWith @() propagateErrorShow
+  . runErrorWith @String propagateErrorShow
   . runErrorWith @SolverError propagateErrorShow
   . runErrorWith @UnificationError propagateError
   . runErrorWith @OversaturatedError propagateError
@@ -174,7 +179,7 @@ runSymbolic guts
 checkValidityPass :: CoreToDo
 checkValidityPass = do
   let name = TH.nameBase 'checkValidityPass
-  let pass guts = runSymbolic guts $ annBindsPass checkValidity guts
+  let pass guts = runSymbolic guts $ checkValidityAndEmbed guts
   CoreDoPluginPass name pass
 
 printAndLint
@@ -193,24 +198,158 @@ printAndLint bind = do
   debug res
   pure bind
 
-checkValidity
-  :: HasCallStack
-  => Error () :> es
-  => Error (LookupError Name) :> es
-  => Error (LookupError TH.Name) :> es
-  => Error SolverError :> es
-  => Context Reader CoreProgram :> es
-  => Context Reader [TyCon] :> es
-  => Provider_ Solver () :> es
-  => HasFamInstEnvs :> es
-  => HasThings :> es
-  => THNameToGHCName :> es
-  => Theory
-  -> CoreBind'
-  -> Eff es CoreBind'
--- TODO: The check itself permits recursive binders, so we should not restrict
--- the input here really!
-checkValidity (Theory axioms) (Bind' var expr) = do
-  axioms' <- resolvePluginAxioms axioms
-  checkValid axioms' expr
-  pure $ Bind' var expr
+checkValidityAndEmbed
+  :: ( HasCallStack
+     , Error String :> es
+     , Error (LookupError Name) :> es
+     , Error (LookupError TH.Name) :> es
+     , Error SolverError :> es
+     , Context Reader CoreProgram :> es
+     , Context Reader [TyCon] :> es
+     , Provider_ Solver () :> es
+     , HasFamInstEnvs :> es
+     , HasThings :> es
+     , THNameToGHCName :> es
+     , HasAnnotations :> es
+     , CoreE :> es
+     , IOE :> es
+     , HasDynFlagsE :> es
+     )
+  => ModGuts
+  -> Eff es ModGuts
+checkValidityAndEmbed guts = do
+  (_, anns) <- getFirstAnnotations @Theory deserializeWithData guts
+
+  markerPrimeId <- thNameToGhcName 'pantomimeMarker >>= lookupIdAll
+  nothingId <- thNameToGhcName 'pantomimeNothing >>= lookupIdAll
+  justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll
+
+  (binds, results) <- fmap unzip $ for (mg_binds guts) \case
+    NonRec x e | Just (Theory axioms) <- lookupUFM anns $ varName x -> do
+      axioms' <- resolvePluginAxioms axioms
+      mCounterexample <- checkValid axioms' e
+      let varNameStr = getOccString x
+      case mCounterexample of
+        Nothing -> do
+          pure (NonRec x e, Just (varNameStr, Var nothingId))
+        Just counterexample -> do
+          let ceStr = showSDocUnsafe (ppr counterexample)
+          ceExpr <- liftCore $ mkStringExpr ceStr
+          pure (NonRec x e, Just (varNameStr, App (Var justId) ceExpr))
+    b -> pure (b, Nothing)
+
+  let results' = catMaybes results
+
+  let resultNames = map fst results'
+  case findMissingAnnotations markerPrimeId resultNames binds of
+    [] -> pure ()
+    (missing : _) ->
+      throwIO $ PprProgramError "checkValidityPass" $
+        text ("Symbolic check result not found for '" ++ missing ++ "'. Did you forget to add the {-# ANN " ++ missing ++ " (Theory ...) #-} annotation?")
+
+  let binds' = replaceMarkerInBinds markerPrimeId results' binds
+  pure guts { mg_binds = binds' }
+
+-- | Recursively traverses all bindings in the module and replaces occurrences of
+-- the 'pantomimeMarker' call with the pre-generated proof result expressions.
+replaceMarkerInBinds
+  :: Id
+  -> [(String, CoreExpr)]
+  -> [CoreBind]
+  -> [CoreBind]
+replaceMarkerInBinds markerPrimeId results = map goBind
+  where
+    goBind (NonRec b e) = NonRec b (replaceMarker markerPrimeId results e)
+    goBind (Rec bs) = Rec (map (\(b, e) -> (b, replaceMarker markerPrimeId results e)) bs)
+
+-- | Replaces any application of the 'pantomimeMarker' with its corresponding
+-- compile-time Z3 proof result expression.
+replaceMarker
+  :: Id
+  -> [(String, CoreExpr)]
+  -> CoreExpr
+  -> CoreExpr
+replaceMarker markerPrimeId results expr = go expr
+  where
+    go :: CoreExpr -> CoreExpr
+    go (App f a)
+      | Just () <- isMarkerPrimeCall f =
+          case exprToString a of
+            Just assertionName ->
+              case lookup assertionName results of
+                Just replacementExpr -> replacementExpr
+                Nothing -> App (go f) (go a)
+            Nothing -> App (go f) (go a)
+      | otherwise = App (go f) (go a)
+            
+    go (Var v) = Var v
+    go (Lit l) = Lit l
+    go (Lam b e) = Lam b (go e)
+    go (Let (NonRec b r) e) = Let (NonRec b (go r)) (go e)
+    go (Let (Rec bs) e) = Let (Rec (map (\(b, r) -> (b, go r)) bs)) (go e)
+    go (Case e b t alts) = Case (go e) b t (map goAlt alts)
+    go (Cast e c) = Cast (go e) c
+    go (Tick t e) = Tick t (go e)
+    go (Type t) = Type t
+    go (Coercion c) = Coercion c
+
+    goAlt (Alt con binders e) = Alt con binders (go e)
+
+    isMarkerPrimeCall :: CoreExpr -> Maybe ()
+    isMarkerPrimeCall (Var v) | v == markerPrimeId = Just ()
+    isMarkerPrimeCall (App f' _) = isMarkerPrimeCall f'
+    isMarkerPrimeCall (Cast e' _) = isMarkerPrimeCall e'
+    isMarkerPrimeCall (Tick _ e') = isMarkerPrimeCall e'
+    isMarkerPrimeCall _ = Nothing
+
+-- | Rxtract a Haskell 'String' value from a GHC 'CoreExpr'
+-- representing a string literal. Return Nothing if the expression is not
+-- a string literal.
+exprToString :: CoreExpr -> Maybe String
+exprToString (Tick _ e) = exprToString e
+exprToString (Cast e _) = exprToString e
+exprToString (App (Var f) (Lit (LitString bs)))
+  | getOccString f == "unpackCString#" || getOccString f == "unpackCStringUtf8#" =
+      Just (BS8.unpack bs)
+exprToString (Lit (LitString bs)) = Just (BS8.unpack bs)
+exprToString _ = Nothing
+
+-- | Scans the Core bindings for any call to 'pantomimeMarker' and returns the
+-- names of all assertions that are referenced by a splice but lack the corresponding
+-- 'Theory' annotation.
+findMissingAnnotations
+  :: Id
+  -> [String]
+  -> [CoreBind]
+  -> [String]
+findMissingAnnotations markerPrimeId resultNames binds = concatMap (goExpr . getExpr) binds
+  where
+    getExpr (NonRec _ e) = e
+    getExpr (Rec bs) = Let (Rec bs) (Var markerPrimeId)
+
+    goExpr :: CoreExpr -> [String]
+    goExpr (App f a) =
+      case isMarkerPrimeCall f of
+        Just () ->
+          case exprToString a of
+            Just assertionName
+              | assertionName `notElem` resultNames -> [assertionName]
+            _ -> goExpr f ++ goExpr a
+        Nothing -> goExpr f ++ goExpr a
+    goExpr (Var _) = []
+    goExpr (Lit _) = []
+    goExpr (Lam _ e) = goExpr e
+    goExpr (Let (NonRec _ r) e) = goExpr r ++ goExpr e
+    goExpr (Let (Rec bs) e) = concatMap (goExpr . snd) bs ++ goExpr e
+    goExpr (Case e _ _ alts) = goExpr e ++ concatMap (\(Alt _ _ body) -> goExpr body) alts
+    goExpr (Cast e _) = goExpr e
+    goExpr (Tick _ e) = goExpr e
+    goExpr (Type _) = []
+    goExpr (Coercion _) = []
+
+    isMarkerPrimeCall :: CoreExpr -> Maybe ()
+    isMarkerPrimeCall (Var v) | v == markerPrimeId = Just ()
+    isMarkerPrimeCall (App f' _) = isMarkerPrimeCall f'
+    isMarkerPrimeCall (Cast e' _) = isMarkerPrimeCall e'
+    isMarkerPrimeCall (Tick _ e') = isMarkerPrimeCall e'
+    isMarkerPrimeCall _ = Nothing
diff --git a/src/Pantomime/PrimOps.hs b/src/Pantomime/PrimOps.hs
index c489f71..8426167 100644
--- a/src/Pantomime/PrimOps.hs
+++ b/src/Pantomime/PrimOps.hs
@@ -138,6 +138,7 @@ import Prelude
   , Num (..)
   , Integral (..)
   , Maybe (..)
+  , String
   , type (~)
   , ($)
   , (<$>)
@@ -159,7 +160,7 @@ import Prelude
 type PrimOp es
   =  HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => Eval es Expr
@@ -190,7 +191,7 @@ type TagToEnumOp
 tagToEnum :: PrimOp es
 tagToEnum = embed2 @TagToEnumOp \ty bvE -> do
   SomeBitVec @n bv <- hoistEff bvE
-  Refl <- failWithE () $ eqT @n @64
+  Refl <- failWithE @String "tagToEnum: expected 64-bit bitvector" $ eqT @n @64
   -- TODO: I'm not sure how this interacts with the whole type normalisation.
   -- I don't think this is correct. Maybe we should reduce the type first? I
   -- guess we could also opt to do this within the embedding. This one is likely
@@ -221,7 +222,7 @@ embed2
   => Wrapped (Deferred a) ~ Runtime (Repr ty)
   => Defer es a
   => Wrap (Deferred a)
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => a
@@ -245,7 +246,7 @@ dataToTag = embed2 @DataToTagOp \_ _ valueE -> do
   case fst $ collectArgs value of
     Con (DataCon dc) -> pure $ SomeBitVec @64 (fromIntegral $ dataConTagZ dc)
     Con (EnumCon @n tag _) | Just Refl <- eqT @n @64 -> pure $ SomeBitVec tag
-    _ -> throwE ()
+    _ -> throwE @String "dataToTag: expected a DataCon or EnumCon constructor"
 
 type RaiseOp
   =   Forall 0 LevityTy
@@ -285,7 +286,7 @@ not = embed2 @(BoolTy :-> BoolTy) \value -> do
 boolbinary
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (SymBool -> SymBool -> SymBool)
@@ -320,7 +321,7 @@ type IntegerBitVecOp
 i2bv :: PrimOp es
 i2bv = embed2 @IntegerBitVecOp \_ n _ i -> do
   SomeNat @n _ <- hoistEff n
-  Dict <- failWithE () $ posNat @n
+  Dict <- failWithE @String "i2bv: expected a positive Nat" $ posNat @n
   i' <- hoistEff i
   pure $ SomeBitVec @n (symFromIntegral i')
 
@@ -335,7 +336,7 @@ iabs = embed2 @(IntegerTy :-> IntegerTy) \value -> do
 ibinary
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (SymInteger -> SymInteger -> SymInteger)
@@ -360,7 +361,7 @@ imod = ibinary mod
 icompare
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (SymInteger -> SymInteger -> SymBool)
@@ -410,7 +411,7 @@ type UnBitVecOp
 bvunary
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (forall n. KnownPos n => SymBitVec n -> SymBitVec n)
@@ -436,7 +437,7 @@ type BinBitVecOp
 bvbinary
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (forall n. KnownPos n => SymBitVec n -> SymBitVec n -> SymBitVec n)
@@ -444,7 +445,7 @@ bvbinary
 bvbinary f = embed2 @BinBitVecOp \_n lhs rhs -> do
   SomeBitVec @nl lhs' <- hoistEff lhs
   SomeBitVec @nr rhs' <- hoistEff rhs
-  Refl <- failWithE () $ eqT @nl @nr
+  Refl <- failWithE @String "Bitvector binary operation: width mismatch" $ eqT @nl @nr
   pure $ SomeBitVec (f lhs' rhs')
 
 asSignedBin
@@ -522,7 +523,7 @@ type CompareBitVecOp
 bvcompare
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
   => (forall n. KnownPos n => SymBitVec n -> SymBitVec n -> SymBool)
@@ -530,7 +531,7 @@ bvcompare
 bvcompare f = embed2 @CompareBitVecOp \_ lhs rhs -> do
   SomeBitVec @nl lhs' <- hoistEff lhs
   SomeBitVec @nr rhs' <- hoistEff rhs
-  Refl <- failWithE () $ eqT @nl @nr
+  Refl <- failWithE @String "Bitvector comparison: width mismatch" $ eqT @nl @nr
   pure $ f lhs' rhs'
 
 asSignedCmp
@@ -598,8 +599,8 @@ bvextend
 bvextend f = embed2 @ExtendBitVecOp \_ _ r _ bv -> do
   SomeBitVec @l bv' <- hoistEff bv
   SomeNat @r _ <- hoistEff r
-  Dict <- failWithE () $ leqNat @l @r
-  Dict <- failWithE () $ posNat @r
+  Dict <- failWithE @String "Bitvector extend: size constraint violation (l <= r)" $ leqNat @l @r
+  Dict <- failWithE @String "Bitvector extend: expected positive result size" $ posNat @r
   pure $ SomeBitVec (f (Proxy @r) bv')
 
 bvzext :: PrimOp es
@@ -631,9 +632,9 @@ bvselect = embed2 @SelectBitVecOp \_ _ _ idx width _ _  bv -> do
   SomeNat @idx _ <- hoistEff idx
   SomeNat @width _ <- hoistEff width
   SomeBitVec @n bv' <- hoistEff bv
-  Dict <- failWithE () $ posNat @width
+  Dict <- failWithE @String "Bitvector select: expected positive width" $ posNat @width
   SNat @sum <- pure $ SNat @idx %+ SNat @width
-  Dict <- failWithE () $ leqNat @sum @n
+  Dict <- failWithE @String "Bitvector select: index+width exceeds bitvector size" $ leqNat @sum @n
   pure $ SomeBitVec (sizedBVSelect (Proxy @idx) (Proxy @width) bv')
 
 -- :: forall k v. Primitive k => Primitive v => v -> Array k v
@@ -653,7 +654,7 @@ aconst = embed2 @ArrayConstOp \_ _ pk _ valE -> do
   -- Gather the literal, knowing it is one due to the constraint.
   Literal @v vty val <- hoistEff valE >>= \case
     Lit lit -> pure lit
-    _ -> throwE ()
+    _ -> throwE @String "aconst: expected a literal value"
 
   -- Gather evidence required to perform the array operation.
   Dict <- pure $ evidence kty
@@ -679,10 +680,10 @@ aselect = embed2 @ArraySelectOp \_ _ arrE keyE -> do
   -- Gather the literal, knowing it is one due to the constraint.
   Literal kty key <- hoistEff keyE >>= \case
     Lit lit -> pure lit
-    _ -> throwE ()
+    _ -> throwE @String "aselect: expected a literal key"
 
   -- Gather evidence required to perform the array operation.
-  Refl <- failWithE () $ eqLiteralType (literalType @k) kty
+  Refl <- failWithE @String "aselect: key type mismatch" $ eqLiteralType (literalType @k) kty
 
   -- Select the value out of the array and wrap it back into an expression.
   let val = Literal (literalType @v) $ Array.select arr key
@@ -705,16 +706,16 @@ astore = embed2 @ArrayStoreOp \_ _ arrE keyE valE -> do
   -- Gather the literal, knowing it is one due to the constraint.
   Literal kty key <- hoistEff keyE >>= \case
     Lit lit -> pure lit
-    _ -> throwE ()
+    _ -> throwE @String "astore: expected a literal key"
 
   -- Gather the literal, knowing it is one due to the constraint.
   Literal vty val <- hoistEff valE >>= \case
     Lit lit -> pure lit
-    _ -> throwE ()
+    _ -> throwE @String "astore: expected a literal value"
 
   -- Gather evidence required to perform the array operation.
-  Refl <- failWithE () $ eqLiteralType (literalType @k) kty
-  Refl <- failWithE () $ eqLiteralType (literalType @v) vty
+  Refl <- failWithE @String "astore: key type mismatch" $ eqLiteralType (literalType @k) kty
+  Refl <- failWithE @String "astore: value type mismatch" $ eqLiteralType (literalType @v) vty
 
   -- Create the modified array.
   let array = Array.store arr key val
@@ -732,6 +733,6 @@ aeq = embed2 @ArrayEqOp \_ _ arrL arrR -> do
   SomeArray @kL @vL arrL' <- hoistEff arrL
   SomeArray @kR @vR arrR' <- hoistEff arrR
 
-  Refl <- failWithE () $ eqLiteralType (literalType @kL) (literalType @kR)
-  Refl <- failWithE () $ eqLiteralType (literalType @vL) (literalType @vR)
+  Refl <- failWithE @String "Array equality: key type mismatch" $ eqLiteralType (literalType @kL) (literalType @kR)
+  Refl <- failWithE @String "Array equality: value type mismatch" $ eqLiteralType (literalType @vL) (literalType @vR)
   pure $ arrL' .== arrR'
diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs
index 74c61f5..a6c79f9 100644
--- a/src/Pantomime/Solve.hs
+++ b/src/Pantomime/Solve.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeApplications #-}
 -- TODO: I want to remove many of these pragmas, also for the other files. Most
 -- of them should just be included in the top-level flags. There also seems to
 -- be a lot of obsolete stuff. Perhaps its good to first find out which flags
@@ -15,10 +17,13 @@
 
 module Pantomime.Solve
   ( checkValid
+  , Counterexample (..)
+  , counterexampleToPairs
   ) where
 
 import GHC.Core qualified as GHC
 import GHC.Core.FamInstEnv (FamInstEnvs)
+import GHC.Types.Id.Make (nospecId)
 import GHC.Generics (Generic)
 import GHC.Plugins
   ( CoreProgram
@@ -30,20 +35,23 @@ import GHC.Plugins
   , varType
   , vcat
   , emptyInScopeSet
+  , getOccString
+  , showSDocUnsafe
+  , isId
   )
-import GHC.Types.Id.Make (nospecId)
 import GHC.Utils.Outputable
   ( Outputable (..)
   , IsLine (..)
   , SDoc
+  , text
   , (<+>)
+  , empty
   )
 
 import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion)
 
 import Control.DeepSeq (NFData (..))
 
-import Data.Foldable (for_)
 import Data.Traversable (for)
 
 import Language.Haskell.TH qualified as TH
@@ -103,7 +111,7 @@ type SymboliseEff =
   [ Context Reader BuiltInTyCon
   , Context Reader InterfaceThings
   , Context Reader FamInstEnvs
-  , Error ()
+  , Error String
   ]
 
 newtype Lie a where
@@ -118,7 +126,7 @@ construct
   => Context Reader BuiltInTyCon :> es
   => Context Reader InterfaceThings :> es
   => Context Reader FamInstEnvs :> es
-  => Error () :> es
+  => Error String :> es
   => [(Var, forall fs. PrimOp fs)]
   -> PluginAxiomsR
   -> CoreProgram
@@ -151,14 +159,14 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe
 
   -- Create fresh arguments.
   let ty = exprType expr
-  (args, _scope) <- freshArgs typeAxiomsR ty emptyInScopeSet
+  (args, _scope) <- freshArgs typeAxiomsR (collectValBinders expr) ty emptyInScopeSet
 
   result <- defer do
     fun <- symbolise subst expr
     res <- mkApps fun $ fmap snd args
     case res of
       Lit (Bool value) -> pure value
-      _ -> throwE ()
+      _ -> throwE @String "Result of symbolic evaluation is not a Boolean literal"
 
   -- TODO: What to do about raise? Do we really just want to return false? I
   -- guess for now it is fine.
@@ -169,10 +177,28 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe
         Right value -> value
   pure (eq, Lie $ pure args)
 
+data Counterexample = Counterexample
+  { counterexampleBindings :: [(String, String)]
+  }
+
+-- | Formats a counterexample into a list of name-value string pairs.
+counterexampleToPairs :: Counterexample -> [(String, String)]
+counterexampleToPairs = counterexampleBindings
+
+instance Outputable Counterexample where
+  ppr (Counterexample bindings) = pprBindings bindings
+    where
+      pprBindings [] = empty
+      pprBindings ((name, val) : rest) = vcat
+        [ "==================="
+        , text name <+> "=" <+> text val
+        , pprBindings rest
+        ]
+
 checkValid
   :: forall es
    . HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Error (LookupError TH.Name) :> es
   => Error (LookupError Name) :> es
   => Error SolverError :> es
@@ -183,7 +209,7 @@ checkValid
   => Provider_ Solver () :> es
   => PluginAxiomsR
   -> CoreExpr
-  -> Eff es ()
+  -> Eff es (Maybe Counterexample)
 checkValid axioms expr = runBuiltInTypes do
   -- TODO: Somehow this code doesn't read very nice. I think I should review it.
   program <- get @CoreProgram
@@ -223,18 +249,26 @@ checkValid axioms expr = runBuiltInTypes do
       -- TODO: I should probably check whether the arguments are recursive
       -- before printing? Alternatively, I could just have a maximum depth.
       args' <- inject args
-      for_ args' \(bndr, arg) -> do
-        let arg' = evalSym True model arg
-        let argdoc = pprArg id arg'
-        dbg $ vcat
-          [ "==================="
-          , ppr bndr <+> "::" <+> ppr (varType bndr)
-          , argdoc
-          ]
-      error "Expression was **not** valid!"
+      let bindings = flip map args' \(bndr, arg) ->
+            let arg' = evalSym True model arg
+                name = getOccString bndr
+                value = showSDocUnsafe (pprArg id arg')
+            in (name, value)
+      pure $ Just (Counterexample bindings)
     Unsatisfiable -> do
       dbg @SDoc "Expression was valid!"
-      pure ()
+      pure Nothing
     -- FIXME: I don't think this is always true. e.g. not sure about some of the
     -- floating point stuff for example.
     Unknown -> throwIO $ ErrorCall "checks are in decidable fragment"
+
+collectValBinders :: CoreExpr -> [String]
+collectValBinders expr = go expr
+  where
+    go (GHC.Lam b e)
+      | isId b    = getOccString b : go e
+      | otherwise = go e
+    go (GHC.Tick _ e) = go e
+    go (GHC.Cast e _) = go e
+    go (GHC.Let _ e)  = go e
+    go _ = []
diff --git a/src/Pantomime/Subst.hs b/src/Pantomime/Subst.hs
index 813a1e6..1458812 100644
--- a/src/Pantomime/Subst.hs
+++ b/src/Pantomime/Subst.hs
@@ -60,7 +60,7 @@ mkEmptySubst = Subst
 -- | Extend the substitution with the given mapping.
 extendSubst
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Subst
   -> Var
   -> Arg
@@ -92,7 +92,7 @@ extendSubst subst var arg = if
 -- | Extend the substitution with the given mappings.
 extendSubstMany
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Foldable f
   => Subst
   -> f (Var, Arg)
@@ -102,7 +102,7 @@ extendSubstMany = foldM $ uncurry . extendSubst
 -- | Extend the identifier substitution with the given mapping.
 extendIdSubst
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Subst
   -> Id
   -> Spine
@@ -112,12 +112,12 @@ extendIdSubst subst var arg = if
     -- Extend the identifier substitution.
     let idSubst' = extendVarEnv (idSubst subst) var arg
     pure subst { idSubst = idSubst' }
-  | otherwise -> throwError ()
+  | otherwise -> throwError "extendIdSubst: expected an Id variable"
 
 -- | Extend the identifier substitution with the given mappings.
 extendIdSubstMany
   :: HasCallStack
-  => Error () :> es
+  => Error String :> es
   => Foldable f
   => Subst
   -> f (Id, Spine)
diff --git a/src/Pantomime/Symbolise.hs b/src/Pantomime/Symbolise.hs
index d80c3fc..de0b4d7 100644
--- a/src/Pantomime/Symbolise.hs
+++ b/src/Pantomime/Symbolise.hs
@@ -7,6 +7,7 @@ module Pantomime.Symbolise
   ) where
 
 import GHC.Plugins qualified as GHC
+import GHC.Utils.Outputable (text, ($+$), (<+>), showSDocUnsafe)
 import GHC.Builtin.Types.Prim
   ( intPrimTyCon
   , int8PrimTyCon
@@ -41,7 +42,7 @@ import Effectful.Context
 symbolise
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader InterfaceThings :> es
   => Subst
@@ -90,7 +91,12 @@ symbolise = go
             , GHC.ppr var
             , GHC.ppr $ GHC.idDetails var
             ]
-          throwE ()
+          throwE $ showSDocUnsafe $
+            text "Unbound variable in symbolise:" <+> GHC.ppr var
+            <+> text "of type:" <+> GHC.ppr (GHC.varType var)
+            $+$ text "The variable is not in the substitution, has no unfolding,"
+            <+> text "is not a data constructor, and is not erased evidence."
+            $+$ text "Consider providing a term axiom mapping for this variable."
 
       GHC.Lit lit -> symboliseLit subst lit
 
@@ -120,7 +126,8 @@ symbolise = go
         let expectedTy = substTy subst $ GHC.varType bndr
         scrutTy <- liftEff $ exprType scrut'
         unless (eqType scrutTy expectedTy) do
-          throwE ()
+          throwE $ showSDocUnsafe $ text "Case scrutinee type mismatch: expected"
+            <+> GHC.ppr expectedTy <+> text "but got" <+> GHC.ppr scrutTy
 
         -- TODO: This is a bit ugly now. I guess it handles all the cases, but
         -- it could deserve some cleanup. It somehow feels weird to gather the
@@ -158,7 +165,7 @@ symbolise = go
             GHC.LitAlt lit | Left spine' <- spine -> do
               symboliseEqLit subst spine' lit
             GHC.DEFAULT -> pure true
-            _ -> throwE ()
+            _ -> throwE "Unsupported case alternative: expected DataAlt, LitAlt, or DEFAULT"
 
           -- TODO: Perhaps it's a good idea to check that the number of
           -- arguments match the binders (unless it is a DEFAULT, in which case
@@ -195,7 +202,7 @@ symboliseBind
   :: forall es
    . HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader InterfaceThings :> es
   => Subst
@@ -219,7 +226,7 @@ symboliseBindMany
    . HasCallStack
   => Deferrable es
   => Foldable f
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader InterfaceThings :> es
   => Subst
@@ -251,7 +258,7 @@ isPrimType ty = case GHC.splitTyConApp_maybe ty of
 symboliseLit
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader InterfaceThings :> es
   => Subst
@@ -278,11 +285,11 @@ symboliseLit subst lit = do
         GHC.LitNumWord16 -> pure (toWord16Id, BitVec @16 num')
         GHC.LitNumWord32 -> pure (toWord32Id, BitVec @32 num')
         GHC.LitNumWord64 -> pure (toWord64Id, BitVec @64 num')
-        GHC.LitNumBigNat -> throwE ()
-    _ -> throwE ()
+        GHC.LitNumBigNat -> throwE "BigNat literals are not supported"
+    _ -> throwE "Unsupported literal type"
 
   -- Lookup the equality function.
-  convert <- failWithE () $ lookupIdSubst subst convertId
+  convert <- failWithE "Conversion function for literal type not found in substitution" $ lookupIdSubst subst convertId
   convert' <- hoistEff convert
 
   mkApps convert' [pure $ mkLit lit']
@@ -294,7 +301,7 @@ symboliseLit subst lit = do
 symboliseEqLit
   :: HasCallStack
   => Deferrable es
-  => Error () :> es
+  => Error String :> es
   => Context Reader InterfaceThings :> es
   => Context Reader BuiltInTyCon :> es
   => Subst
@@ -316,11 +323,11 @@ symboliseEqLit subst lhs rhs = do
       GHC.LitNumWord16 -> pure eqWord16Id
       GHC.LitNumWord32 -> pure eqWord32Id
       GHC.LitNumWord64 -> pure eqWord64Id
-      GHC.LitNumBigNat -> throwE ()
-    _ -> throwE ()
+      GHC.LitNumBigNat -> throwE "BigNat literals are not supported in equality check"
+    _ -> throwE "Unsupported literal type in equality check"
 
   -- Lookup the equality function.
-  eq <- failWithE () $ GHC.maybeUnfoldingTemplate (GHC.realIdUnfolding eqId)
+  eq <- failWithE "Equality function for literal type not found" $ GHC.maybeUnfoldingTemplate (GHC.realIdUnfolding eqId)
   eq' <- symbolise subst eq
 
   lit <- deferE $ symboliseLit subst rhs
@@ -329,4 +336,4 @@ symboliseEqLit subst lhs rhs = do
   result <- mkApps eq' [pure lhs, lit]
   case result of
     Lit (Bool result') -> pure result'
-    _ -> throwE ()
+    _ -> throwE "Literal equality check did not produce a Boolean result"
diff --git a/src/Pantomime/TH.hs b/src/Pantomime/TH.hs
new file mode 100644
index 0000000..b50cb71
--- /dev/null
+++ b/src/Pantomime/TH.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TemplateHaskellQuotes #-}
+
+module Pantomime.TH
+  ( pantomime
+  ) where
+
+import Language.Haskell.TH qualified as TH
+import Pantomime.Marker
+
+pantomime :: TH.Name -> TH.Q TH.Exp
+pantomime name = do
+  let nameStr = TH.nameBase name
+  pure $ TH.AppE (TH.VarE 'pantomimeMarker) (TH.LitE (TH.StringL nameStr))
diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs
index 59243d8..1462c3b 100644
--- a/src/Pantomime/Unification.hs
+++ b/src/Pantomime/Unification.hs
@@ -1,48 +1,44 @@
 {-# LANGUAGE OverloadedStrings #-}
+
 -- TODO: Rename to Pantomime.Unify, I think it's cleaner and it also mirrors the
 -- naming from GHC.
 -- TODO: Add module docs.
 module Pantomime.Unification
-  ( UnificationError (..)
-  , OversaturatedError (..)
-  , unifyApp
-  , unifyApps
-  , unifyExprs
-  , resolveInstances
-  , resolveInstancesWith
-  , subsumeExpr
-  ) where
-
-import Prelude hiding (break)
+  ( UnificationError (..),
+    OversaturatedError (..),
+    unifyApp,
+    unifyApps,
+    unifyExprs,
+    resolveInstances,
+    resolveInstancesWith,
+    subsumeExpr,
+  )
+where
 
-import GHC.Plugins hiding ((<>))
+import Control.Applicative (Alternative ((<|>)))
+import Control.Error (LookupError (..))
+import Control.Monad (when)
+import Data.List (intersperse)
+import Data.Traversable (for)
+import Effectful
+import Effectful.Break
+import Effectful.Context
+import Effectful.Error.Static
+import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst)
 import GHC.Core.Class (Class)
-import GHC.Core.Unify (tcUnifyTys, alwaysBindFun, tcMatchTy)
+import GHC.Core.InstEnv (instanceDFunId)
 import GHC.Core.Map.Type (TypeMap)
 import GHC.Core.Predicate (isEvVar)
-import GHC.Core.InstEnv (instanceDFunId)
-import GHC.Core.TyCo.Rep (Type (..), Scaled (..), scaledThing)
-import GHC.Data.TrieMap (TrieMap (..), insertTM)
+import GHC.Core.TyCo.Rep (Scaled (..), Type (..), scaledThing)
+import GHC.Core.Unify (alwaysBindFun, tcMatchTy, tcUnifyTys)
 import GHC.Data.Maybe (rightToMaybe, whenIsJust)
-import GHC.Tc.Utils.TcType (tcSplitSigmaTy, substTy)
-
-import Data.List (intersperse)
-import Data.Traversable (for)
-
-import Control.Applicative (Alternative ((<|>)))
-import Control.Monad (when)
-import Control.Error (LookupError (..))
-
+import GHC.Data.TrieMap (TrieMap (..), insertTM)
+import GHC.Plugins hiding ((<>))
+import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy)
 import Lens.Micro
 import Lens.Micro.Extras (view)
-
 import Pantomime.Util
-
-import Effectful
-import Effectful.Error.Static
-import Effectful.Break
-import Effectful.Context
-import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst)
+import Prelude hiding (break)
 
 -- | Error to indicate unification failure.
 --
@@ -67,65 +63,70 @@ instance Outputable OversaturatedError where
     let vsep' = vcat' . intersperse ""
 
     -- Pretty print an expression with its type.
-    let pprExpr expr = vcat'
-          [ "::" <+> ppr (exprType expr)
-          , ppr expr
-          ]
+    let pprExpr expr =
+          vcat'
+            [ "::" <+> ppr (exprType expr),
+              ppr expr
+            ]
 
     -- The actual pretty print.
     vsep'
       [ hang "Function is oversaturated" 2 do
-        pprExpr fun
-      , hang "Given arguments" 2 do
-        vsep' $ fmap pprExpr args
+          pprExpr fun,
+        hang "Given arguments" 2 do
+          vsep' $ fmap pprExpr args
       ]
 
 -- | Mapping used to track information for unification.
 data Unification = Unification
-  { _substitution :: Subst
-  -- ^ The substitution as dictated by a GHC unification.
-  , _dictionaries :: TypeMap CoreExpr
-  -- ^ The dictionary expressions/variables currently in-scope.
-  , _quantifiers :: DTyCoVarSet
-  -- ^ The quantifiers currently in use.
+  { -- | The substitution as dictated by a GHC unification.
+    _substitution :: Subst,
+    -- | The dictionary expressions/variables currently in-scope.
+    _dictionaries :: TypeMap CoreExpr,
+    -- | The quantifiers currently in use.
+    _quantifiers :: DTyCoVarSet
   }
 
 -- | An empty unification mapping.
 emptyUnif :: Unification
-emptyUnif = Unification
-  { _substitution = emptySubst
-  , _dictionaries = emptyTM
-  , _quantifiers = emptyDVarSet
-  }
+emptyUnif =
+  Unification
+    { _substitution = emptySubst,
+      _dictionaries = emptyTM,
+      _quantifiers = emptyDVarSet
+    }
 
 -- | Lens into substitution of the 'Unification'.
 substitution :: Lens' Unification Subst
 substitution f unif = do
-  let rebuild subst = Unification
-        { _substitution = subst
-        , _dictionaries = _dictionaries unif
-        , _quantifiers = _quantifiers unif
-        }
+  let rebuild subst =
+        Unification
+          { _substitution = subst,
+            _dictionaries = _dictionaries unif,
+            _quantifiers = _quantifiers unif
+          }
   rebuild <$> f (_substitution unif)
 
 -- | Lens into dictionaries of the 'Unification'.
 dictionaries :: Lens' Unification (TypeMap CoreExpr)
 dictionaries f unif = do
-  let rebuild dict = Unification
-        { _substitution = _substitution unif
-        , _dictionaries = dict
-        , _quantifiers = _quantifiers unif
-        }
+  let rebuild dict =
+        Unification
+          { _substitution = _substitution unif,
+            _dictionaries = dict,
+            _quantifiers = _quantifiers unif
+          }
   rebuild <$> f (_dictionaries unif)
 
 -- | Lens into quantifiers of the 'Unification'.
 quantifiers :: Lens' Unification DVarSet
 quantifiers f unif = do
-  let rebuild quants = Unification
-        { _substitution = _substitution unif
-        , _dictionaries = _dictionaries unif
-        , _quantifiers = quants
-        }
+  let rebuild quants =
+        Unification
+          { _substitution = _substitution unif,
+            _dictionaries = _dictionaries unif,
+            _quantifiers = quants
+          }
   rebuild <$> f (_quantifiers unif)
 
 -- | A lens into the 'InScopeSet' of a 'Subst'.
@@ -138,11 +139,11 @@ scopeSubst f (Subst scope' ids tvs cvs) = do
 --
 -- This will not resolve instances. The purpose of this lookup is to not have
 -- duplicate dictionary constraints in a unified expression.
-lookupDict
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => Type
-  -> Eff es CoreExpr
+lookupDict ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  Type ->
+  Eff es CoreExpr
 lookupDict ty = runBreak do
   -- We need to use the new type for lookup in order to properly deduplicate
   -- constraints.
@@ -165,23 +166,23 @@ lookupDict ty = runBreak do
   pure fresh'
 
 -- | Multiple lookups using 'lookupDict'.
-lookupDicts
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => Traversable f
-  => f Type
-  -> Eff es (f CoreExpr)
+lookupDicts ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  (Traversable f) =>
+  f Type ->
+  Eff es (f CoreExpr)
 lookupDicts = traverse lookupDict
 
 -- | Lookup the unifying type of a type variable.
 --
 -- This will additionally track the type variables that are used by the new,
 -- unified type in the unification map.
-lookupTy
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => TyVar
-  -> Eff es Type
+lookupTy ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  TyVar ->
+  Eff es Type
 lookupTy var = do
   -- Lookup the unifying type.
   unif <- get @Unification
@@ -201,21 +202,21 @@ lookupTy var = do
   pure ty
 
 -- | Multiple lookups using 'lookupTy'.
-lookupTys
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => Traversable f
-  => f TyVar
-  -> Eff es (f Type)
+lookupTys ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  (Traversable f) =>
+  f TyVar ->
+  Eff es (f Type)
 lookupTys = traverse lookupTy
 
 -- | Fetches all free type variables.
 --
 -- The intent for this is to close expressions which we unified using
 -- 'applyUnification'.
-freeTyVars
-  :: Context Reader Unification :> es
-  => Eff es [TyVar]
+freeTyVars ::
+  (Context Reader Unification :> es) =>
+  Eff es [TyVar]
 freeTyVars = do
   unif <- get @Unification
   pure $ unif ^. quantifiers . to dVarSetElems
@@ -224,9 +225,9 @@ freeTyVars = do
 --
 -- The intent for this is to close expressions which we unified using
 -- 'applyUnification'.
-freeDictIds
-  :: Context Reader Unification :> es
-  => Eff es [DictId]
+freeDictIds ::
+  (Context Reader Unification :> es) =>
+  Eff es [DictId]
 freeDictIds = do
   unif <- get @Unification
   let select = \case
@@ -238,10 +239,10 @@ freeDictIds = do
 --
 -- It is assumed that this expression has been first unified using the
 -- 'applyUnification'.
-closeExpr
-  :: Context Reader Unification :> es
-  => CoreExpr
-  -> Eff es CoreExpr
+closeExpr ::
+  (Context Reader Unification :> es) =>
+  CoreExpr ->
+  Eff es CoreExpr
 closeExpr expr = do
   tyVars <- freeTyVars
   dictIds <- freeDictIds
@@ -252,21 +253,21 @@ splitExprTy :: CoreExpr -> ([TyVar], ThetaType, Type)
 splitExprTy = tcSplitSigmaTy . exprType
 
 -- | Unify two types using 'unifyTypes'.
-unifyType
-  :: Error UnificationError :> es
-  => Type
-  -> Type
-  -> Eff es Unification
+unifyType ::
+  (Error UnificationError :> es) =>
+  Type ->
+  Type ->
+  Eff es Unification
 unifyType lhs rhs = unifyTypes [(lhs, rhs)]
 
 -- | Unify the given types.
 --
 -- Creates a unification map for use in 'applyUnification'.
-unifyTypes
-  :: HasCallStack
-  => Error UnificationError :> es
-  => [(Type, Type)]
-  -> Eff es Unification
+unifyTypes ::
+  (HasCallStack) =>
+  (Error UnificationError :> es) =>
+  [(Type, Type)] ->
+  Eff es Unification
 unifyTypes tys = do
   let err = UnificationError tys
   let (lhs, rhs) = unzip tys
@@ -282,11 +283,11 @@ unifyTypes tys = do
 -- The returned expression will have free variables as dictated by the
 -- unification mapping. However way the expression is used, make sure to
 -- eventually close the expression using 'closeExpr'.
-applyUnification
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => CoreExpr
-  -> Eff es CoreExpr
+applyUnification ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  CoreExpr ->
+  Eff es CoreExpr
 applyUnification expr = do
   -- Split the type variables and theta type.
   let (tyVars, thetaTy, _) = splitExprTy expr
@@ -300,22 +301,22 @@ applyUnification expr = do
   pure $ mkApps expr args
 
 -- | Multiple applications of the unification via 'applyUnification'.
-applyUnifications
-  :: Context Reader Unification :> es
-  => Context Writer Unification :> es
-  => Traversable f
-  => f CoreExpr
-  -> Eff es (f CoreExpr)
+applyUnifications ::
+  (Context Reader Unification :> es) =>
+  (Context Writer Unification :> es) =>
+  (Traversable f) =>
+  f CoreExpr ->
+  Eff es (f CoreExpr)
 applyUnifications = traverse applyUnification
 
 -- | A single unifying application using 'unifyApps'.
-unifyApp
-  :: HasCallStack
-  => Error UnificationError :> es
-  => Error OversaturatedError :> es
-  => CoreExpr
-  -> CoreArg
-  -> Eff es CoreExpr
+unifyApp ::
+  (HasCallStack) =>
+  (Error UnificationError :> es) =>
+  (Error OversaturatedError :> es) =>
+  CoreExpr ->
+  CoreArg ->
+  Eff es CoreExpr
 unifyApp fun arg = unifyApps fun [arg]
 
 -- | Application that unifies polymorphic types.
@@ -323,13 +324,13 @@ unifyApp fun arg = unifyApps fun [arg]
 -- This will apply the given arguments to the spine. Any type or dictionary
 -- variables that occur prior any of the body type are unified and placed as
 -- outer type and dictionary variables.
-unifyApps
-  :: HasCallStack
-  => Error UnificationError :> es
-  => Error OversaturatedError :> es
-  => CoreExpr
-  -> [CoreArg]
-  -> Eff es CoreExpr
+unifyApps ::
+  (HasCallStack) =>
+  (Error UnificationError :> es) =>
+  (Error OversaturatedError :> es) =>
+  CoreExpr ->
+  [CoreArg] ->
+  Eff es CoreExpr
 unifyApps fun args = do
   -- Get the base types without type variables or theta type of all expressions.
   let bodyTy = view _3 . splitExprTy
@@ -356,11 +357,11 @@ unifyApps fun args = do
 --
 -- This can be used to compare two expressions that are quantified different,
 -- but are otherwise comparable.
-unifyExprs
-  :: Error UnificationError :> es
-  => CoreExpr
-  -> CoreExpr
-  -> Eff es (CoreExpr, CoreExpr)
+unifyExprs ::
+  (Error UnificationError :> es) =>
+  CoreExpr ->
+  CoreExpr ->
+  Eff es (CoreExpr, CoreExpr)
 unifyExprs lhs rhs = do
   -- Get the unifiable part of the type.
   let bodyTy = view _3 . splitExprTy
@@ -386,24 +387,29 @@ unifyExprs lhs rhs = do
 -- TODO: Using 'TypeMap CoreExpr' for instances is extremely fragile. It would
 -- be a lot better to use InstEnv to resolve typeclasses. This goes for other
 -- functions in this module as well!
-subsumeExpr
-  :: HasCallStack
-  => Error () :> es
-  => TypeMap CoreExpr
-  -> CoreExpr
-  -> Type
-  -> Eff es CoreExpr
+subsumeExpr ::
+  (HasCallStack) =>
+  (Error String :> es) =>
+  TypeMap CoreExpr ->
+  CoreExpr ->
+  Type ->
+  Eff es CoreExpr
 subsumeExpr dicts expr ty = do
   -- Get the unifiable part of the type.
   let (curTv, curEv, curTy) = splitExprTy expr
   let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty
 
   -- Match the types and add all dictionaries we care about.
-  let err = () -- TODO: This should be a better error.
+  let err =
+        "subsumeExpr: type matching failed"
+          <> "\n  current type:  "
+          <> showSDocUnsafe (ppr curTy)
+          <> "\n  required type: "
+          <> showSDocUnsafe (ppr reqTy)
   subst <- failWith err $ tcMatchTy curTy reqTy
 
   -- Make evidence variables.
-  let names = ("dict", ) . unrestricted <$> reqEv
+  let names = ("dict",) . unrestricted <$> reqEv
   let (lamEv, _) = freshIds names $ mkInScopeSetList reqTv
 
   -- Construct the arguments to supply to the expression to unify.
@@ -412,7 +418,11 @@ subsumeExpr dicts expr ty = do
         insertTM (varType ev) (Var ev) acc
   let curEv' = substTy subst <$> curEv
   argsEv <- for curEv' \ev -> do
-    failWith () $ lookupTM ev dicts'
+    let err' =
+          "subsumeExpr: type variable instance not found in dictionary"
+            <> "\n  type: "
+            <> showSDocUnsafe (ppr ev)
+    failWith @String err' $ lookupTM ev dicts'
 
   -- Construct the new expression.
   let open = mkApps expr $ fmap Type argsTv <> argsEv
@@ -421,13 +431,13 @@ subsumeExpr dicts expr ty = do
 -- | Lookup a class instance in the instantiation environment.
 --
 -- This will return a dictionary instance as core expression.
-lookupClassInst
-  :: forall es
-   . HasCallStack
-  => Error (LookupError Type) :> es
-  => HasInstEnvs :> es
-  => Type
-  -> Eff es CoreExpr
+lookupClassInst ::
+  forall es.
+  (HasCallStack) =>
+  (Error (LookupError Type) :> es) =>
+  (HasInstEnvs :> es) =>
+  Type ->
+  Eff es CoreExpr
 lookupClassInst ty = do
   let failWith' :: Maybe a -> Eff es a
       failWith' = failWith $ LookupError ty
@@ -452,10 +462,10 @@ lookupClassInst ty = do
 -- typeclass. Instead, this function is intended to be used together with other
 -- unification-like functions in this module, as these unifications can create
 -- resolvable typeclass constraints.
-resolveInstances
-  :: HasInstEnvs :> es
-  => CoreExpr
-  -> Eff es CoreExpr
+resolveInstances ::
+  (HasInstEnvs :> es) =>
+  CoreExpr ->
+  Eff es CoreExpr
 resolveInstances expr = do
   -- Get a mapping from constraints to instances.
   let theta = splitExprTy expr ^. _2
@@ -465,17 +475,17 @@ resolveInstances expr = do
 
   -- Convert this mapping into a trie map.
   let dicts = foldlBy emptyTM instances \acc (ty, inst) -> do
-          -- Alter the dictionary map if we found an instance.
-          alterTM ty (inst <|>) acc
+        -- Alter the dictionary map if we found an instance.
+        alterTM ty (inst <|>) acc
 
   -- Resolve the instances with this mapping.
   pure $ resolveInstancesWith dicts expr
 
-resolveInstancesWith
-  :: TypeMap CoreExpr
-  -- ^ Mapping from dictionary types to their instance.
-  -> CoreExpr
-  -> CoreExpr
+resolveInstancesWith ::
+  -- | Mapping from dictionary types to their instance.
+  TypeMap CoreExpr ->
+  CoreExpr ->
+  CoreExpr
 resolveInstancesWith dicts expr = do
   -- Set this dictionary for a unification.
   let unif = emptyUnif & dictionaries .~ dicts
diff --git a/test/Spec.hs b/test/Spec.hs
index d0b61ae..fca6e6a 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,108 +1,58 @@
+{-# OPTIONS_GHC -fplugin=Pantomime #-}
+{-# LANGUAGE BlockArguments #-}
+
 module Main
   ( main
   ) where
 
 import Test.Hspec
-import Test.HUnit
-
-import System.Directory (listDirectory)
-
-import GHC
-import GHC.Paths (libdir)
-import GHC.Plugins (HasDynFlags (..), showGhcExceptionUnsafe)
--- import GHC.Utils.Panic (handleGhcException)
-import GHC.Driver.Session (updOptLevel)
-import GHC.Data.EnumSet qualified as EnumSet
-
-import Language.Haskell.TH.LanguageExtensions
-
-import Control.Monad (forM_)
-
-import Data.Function ((&))
-import Data.List (isSuffixOf)
-
--- | Plugin setup.
---
--- This ensure the flags and session are set up to test out plugin.
-setupPlugin :: Ghc ()
-setupPlugin = do
-  dflags <- getDynFlags
-  setSessionDynFlags $ updOptLevel 1 dflags
-    { pluginModNames = mkModuleName "Pantomime" : pluginModNames dflags
-    , extensionFlags = extensionFlags dflags 
-      & EnumSet.insert TemplateHaskellQuotes
-    , generalFlags = generalFlags dflags
-      & EnumSet.insert Opt_ExposeAllUnfoldings
-      -- & EnumSet.delete Opt_KeepHiFiles
-      -- & EnumSet.delete Opt_KeepOFiles
-    }
-
--- | Run the ghc monad.
-runGhc' :: Ghc a -> IO a
-runGhc' = runGhc $ Just libdir
-
--- | Compile the given file.
---
--- This will additionally return an error if it occurred during the compilation.
--- FIXME: It seems GHC already catches all thrown errors from the plugin. Can
-compile :: FilePath -> Ghc (Either GhcException ())
-compile path = do
-  -- Compile the given module.
-  _ <- compileToCoreModule path
-
-  -- Remove the target after compiling to ensure we don't run it twice.
-  target <- guessTarget path Nothing Nothing
-  removeTarget $ targetId target
+import Test.Hspec.Expectations (expectationFailure)
+
+import Pantomime
+import Pantomime.BuiltIn qualified as Pantomime
+
+-- =============================================================================
+-- Test Case Definitions
+-- =============================================================================
+
+-- | Peirce's Law: ((p -> q) -> p) -> p.
+-- This is a classical logic tautology that is non-trivial to prove/recognize.
+{-# ANN validAssertion (Theory mempty) #-}
+validAssertion :: Bool -> Bool -> Pantomime.Bool
+validAssertion p q =
+  let p' = Pantomime.boolean p
+      q' = Pantomime.boolean q
+  in ((p' `Pantomime.implies` q') `Pantomime.implies` p') `Pantomime.implies` p'
+
+-- | Fallacy of Affirming the Consequent: ((p -> q) ∧ q) -> p.
+-- This is invalid: if p is False and q is True, the premise holds but the conclusion is False.
+{-# ANN invalidAssertion (Theory mempty) #-}
+invalidAssertion :: Bool -> Bool -> Pantomime.Bool
+invalidAssertion p q =
+  let p' = Pantomime.boolean p
+      q' = Pantomime.boolean q
+      (&&.) = (Pantomime.&&)
+  in ((p' `Pantomime.implies` q') &&. q') `Pantomime.implies` p'
+
+-- =============================================================================
+-- Test Suite
+-- =============================================================================
 
-  pure $ Right ()
-
-  -- let handler = pure . Left
-  -- operation
-  -- handleGhcException handler operation
-
--- | Fetches the files we consider for tests.
-progPaths :: IO [FilePath]
-progPaths = do
-  let listDirectory' dir = do
-        files <- listDirectory dir
-        pure $ fmap (dir <>) files
-  paths <- listDirectory' "tests/"
-  let isSrc path = isSuffixOf ".hs" path && not ("ForceEmbedding.hs" `isSuffixOf` path)
-  pure $ filter isSrc paths
-
--- -- | Compiles the given files, running them through the plugin.
--- runFiles :: [FilePath] -> IO [Either GhcException ()]
--- runFiles paths = runGhc' $ do
---   setupPlugin
---   forM paths compile
-
--- -- | Check the result of the compilation.
--- check :: FilePath -> Either GhcException () -> SpecWith ()
--- check path result = do
---   it ("checks " <> "\"" <> path <> "\"") $ do
---     let pprFail = assertFailure . flip showGhcExceptionUnsafe ""
---     either pprFail pure result
-
-check' :: FilePath -> SpecWith ()
-check' path = do
-  it ("checks " <> "\"" <> path <> "\"") $ do
-    -- result <- hSilence [stdout, stderr] . runGhc' $ do
-    result <- runGhc' $ do
-      setupPlugin
-      compile path
-
-    let pprFail = assertFailure . flip showGhcExceptionUnsafe ""
-    either pprFail pure result
-
-    -- let pprFail = assertFailure . flip showGhcExceptionUnsafe ""
-    -- either pprFail pure result
-
--- | Performs the plugin in a number of files.
 main :: IO ()
 main = hspec $ do
-  paths <- runIO progPaths
-  forM_ paths check'
-  -- results <- runIO $ runFiles paths
-
-  -- let results' = zip paths results
-  -- forM_ results' $ uncurry check
+  describe "Pantomime Symbolic Checker Unit Tests" $ do
+    it "verifies validAssertion (should succeed with Nothing)" $ do
+      $(pantomime 'validAssertion) `shouldBe` Nothing
+
+    it "detects invalidAssertion (should fail with Just counterexample)" $ do
+      checkInvalid $(pantomime 'invalidAssertion)
+
+-- | Assert that a counterexample was found and print it.
+checkInvalid :: Maybe String -> Expectation
+checkInvalid = \case
+  Just ce -> do
+    putStrLn ""
+    putStrLn "Counterexample found:"
+    putStrLn ce
+    putStrLn ""
+  Nothing -> expectationFailure "Expected a counterexample but assertion was valid"
diff --git a/tests/ForceEmbedding.hs b/tests/ForceEmbedding.hs
deleted file mode 100644
index d8884d6..0000000
--- a/tests/ForceEmbedding.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-module ForceEmbeddings
-  ( theory
-  ) where
-
--- FIXME: Right now, 'collectScrut' will throw an error if we force a
--- literal. I'm not 100% sure what the behaviour should be, but it
--- definitely shouldn't throw. The only thing I'm not sure about, is
--- what to do with constraints: should they now be part of the outer
--- expression?
---
--- Example faulting expression. I was not able to reproduce it for a
--- different type than an embedded Array type... I think it's due to
--- the way it is embedded (that is, it is a 'Cast' at the outer layer).
-{-# NOINLINE test #-}
-test :: Memory -> Pantomime.Bool
-test !_ = Pantomime.True
-
-{-# ANN theory (Theory $ Base.axioms <> Clash.axioms <> RISCV.axioms) #-}
-theory :: Pantomime.Bool
-theory = test $ constM 0
diff --git a/tests/Prune.hs b/tests/Prune.hs
deleted file mode 100644
index d53a46a..0000000
--- a/tests/Prune.hs
+++ /dev/null
@@ -1,45 +0,0 @@
-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE ImportQualifiedPost #-}
-
-module Prune
-  ( loopy
-  , doubleCase
-  , share
-  ) where
-
-import GHC.Base (noinline)
-import Pantomime
-import Pantomime.BuiltIn qualified as Pantomime
-
-{-# ANN loopy (Theory mempty) #-}
-loopy :: Bool -> Pantomime.Bool
-loopy value = Pantomime.boolean do
-  let go x = case x of
-        True -> True
-        False -> go $ not x
-  go value
-
-infinite :: a
-infinite = noinline infinite
-
-{-# ANN doubleCase (Theory mempty) #-}
-doubleCase :: Bool -> Pantomime.Bool
-doubleCase value = Pantomime.boolean do
-  case value of
-    True -> True
-    False -> case value of
-      True -> infinite
-      False -> True
-
-{-# ANN share (Theory mempty) #-}
-share :: Bool -> Bool -> Pantomime.Bool
-share lhs rhs = Pantomime.boolean do
-  let x = case lhs || rhs of
-        True -> True
-        False -> infinite
-  case lhs of
-    True -> x
-    False -> case rhs of
-      True -> x
-      False -> True
-