diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for checked-exceptions
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2020 Zachary Churchill
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,42 @@
+# checked-exceptins
+
+A monad transformer that allows you to throw and catch a restricted set of exceptions, tracked at the type level
+
+Consider the following example:
+
+```haskell
+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
+    -- or
+    withOneOf @() e $ \() -> putStrLn "()"
+    withOneOf @Int e $ \n -> print $ n + 1
+    withOneOf @Bool e $ \_ -> pure ()
+    -- or
+    caseException e
+      (  (\() -> putStrLn "()")
+      <: (\n -> print $ n + 1)
+      <: CaseAny (\x -> putStrLn $ encodeException x)
+      -- <: (\b -> putStrLn "bool")
+      -- <: (\s -> putStrLn "string")
+      -- <: CaseEnd
+      )
+  Right () -> putStrLn "Right"
+```
+
+The facilities this library provides will alert you when you have, intentionally or unintentionally, introduced a new possible exception in your code that is presently unaccounted for.
+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 documenation 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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/checked-exceptions.cabal b/checked-exceptions.cabal
new file mode 100644
--- /dev/null
+++ b/checked-exceptions.cabal
@@ -0,0 +1,71 @@
+cabal-version: 2.0
+-- Initial package description 'checked-exceptions.cabal' generated by
+-- 'cabal init'. For further documentation, see
+-- http://haskell.org/cabal/users-guide/
+
+name: checked-exceptions
+version: 0.1.0.0
+synopsis: mtl-style checked exceptions
+description: A monad transformer that allows you to throw and catch a restricted set of exceptions, tracked at the type level.
+-- bug-reports:
+license: MIT
+license-file: LICENSE
+author: Zachary Churchill
+maintainer: zacharyachurchill@gmail.com
+homepage: http://github.com/haskell/checked-exceptions
+bug-reports: http://github.com/haskell/checked-exceptions/issues
+-- copyright:
+category: Control
+build-type: Simple
+tested-with: GHC == 9.10.1
+extra-source-files: CHANGELOG.md, README.md
+
+source-repository head
+  type: git
+  location: https://github.com/goolord/checked-exceptions.git
+
+library
+  exposed-modules:
+      Control.Monad.CheckedExcept
+    , Control.Monad.CheckedExcept.Plugin
+    , Control.Monad.CheckedExcept.QualifiedDo
+  other-modules:
+      Control.Monad.CheckedExcept.Plugin.Bind
+  ghc-options: -Wall
+  -- other-modules:
+  -- other-extensions:
+  build-depends:
+      base >=4.12.0.0 && < 5
+    , mtl >= 2.0.0.0 && < 3.0.0.0
+    , transformers >= 0.6.0.0 && < 0.7.0.0
+    , constraints >= 0.14 && < 0.15
+    --
+    , ghc >=8.6.5 && <10
+    , ghc-tcplugins-extra >= 0.4 && < 0.6
+  hs-source-dirs: lib
+  default-language: Haskell2010
+
+test-suite test
+  type:
+    exitcode-stdio-1.0
+  hs-source-dirs:
+    test
+  main-is:
+    Main.hs
+  other-modules:
+    CompTest
+  build-depends:
+      HUnit
+    , tasty
+    , base
+    , tasty-hunit
+    , tasty-quickcheck
+    , QuickCheck
+    , checked-exceptions
+    , text
+    , mtl
+    , transformers
+  ghc-options:
+    -Wall
+  default-language:
+    Haskell2010
diff --git a/lib/Control/Monad/CheckedExcept.hs b/lib/Control/Monad/CheckedExcept.hs
new file mode 100644
--- /dev/null
+++ b/lib/Control/Monad/CheckedExcept.hs
@@ -0,0 +1,265 @@
+{-# LANGUAGE
+    KindSignatures
+  , TypeFamilies
+  , DataKinds
+  , TypeOperators
+  , UndecidableInstances
+  , GADTs
+  , TypeApplications
+  , ScopedTypeVariables
+  , RankNTypes
+  , StandaloneDeriving
+  , DefaultSignatures
+  , DerivingVia
+  , PolyKinds
+  , LambdaCase
+  , MultiParamTypeClasses
+  , AllowAmbiguousTypes
+  , ConstraintKinds
+#-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Control.Monad.CheckedExcept
+  ( -- * types
+    CheckedExceptT(..)
+  , CheckedExcept
+  , OneOf(..)
+  , CaseException(..)
+  , pattern CaseEnd
+  , ShowException(..)
+  , ExceptionException(..)
+  -- * type families / constraints
+  , Contains
+  , Elem
+  , NotElemTypeError
+  , Nub
+  , Remove
+  , type (++)
+  -- * typeclass
+  , CheckedException(..)
+  -- * utility functions
+  , runCheckedExcept
+  , throwCheckedException
+  , applyAll
+  , weakenExceptions
+  , weakenOneOf
+  , withOneOf
+  , withOneOf'
+  , caseException
+  , (<:)
+  , catchSomeException
+  ) where
+
+import Data.Functor ((<&>))
+import Control.Exception (Exception(..), catch, SomeException)
+import Control.Monad.Except
+import Data.Functor.Identity
+import Data.Kind
+import Data.Type.Bool
+import GHC.TypeLits
+import Data.Constraint
+import Data.Typeable (Typeable, cast, eqT)
+import Data.Type.Equality
+import Control.Monad.IO.Class (MonadIO (liftIO))
+import Control.Monad.Trans (MonadTrans (..))
+import Data.Constraint.Unsafe (unsafeCoerceConstraint)
+
+-- | isomorphic to 'ExceptT' over our open-union exceptions type
+-- 'OneOf es'. because many effects systems have an 'ExceptT' analogue,
+-- this would be pretty simple to port to any effects system.
+-- see "Control.Monad.CheckedExcept.QualifiedDo" for example usages
+newtype CheckedExceptT (exceptions :: [Type]) m a
+  = CheckedExceptT { runCheckedExceptT :: m (Either (OneOf exceptions) a) }
+  deriving (Monad, Applicative, Functor, MonadFail, MonadIO, MonadError (OneOf exceptions)) via (ExceptT (OneOf exceptions) m)
+  deriving (MonadTrans) via (ExceptT (OneOf exceptions))
+
+-- | pure checked exceptions
+type CheckedExcept es a = CheckedExceptT es Identity a
+
+-- | see 'weakenOneOf'
+weakenExceptions :: forall exceptions1 exceptions2 m a.
+     Functor m
+  => Contains exceptions1 exceptions2
+  => CheckedExceptT exceptions1 m a
+  -> CheckedExceptT exceptions2 m a
+weakenExceptions (CheckedExceptT ma) = CheckedExceptT $ do
+  ma <&> \case
+    Left e -> Left $ weakenOneOf @exceptions1 @exceptions2 e
+    Right a -> Right a
+
+-- | Given a proof that 'exceptions1' is a subset of 'exceptions2',
+-- reconstruct the value of the 'OneOf exceptions1' open union to be part of the larger
+-- 'OneOf exceptions2' open union. this allows us to compose 'CheckedExceptT' stacks
+-- with differing exception sets
+weakenOneOf :: forall exceptions1 exceptions2.
+     Contains exceptions1 exceptions2
+  => OneOf exceptions1
+  -> OneOf exceptions2
+weakenOneOf (OneOf e') = weakenE e'
+  where
+  weakenE :: forall e.
+      ( Elem e exceptions1
+      , CheckedException e
+      , Typeable e
+      )
+    => e
+    -> OneOf exceptions2
+  weakenE e = do
+    -- idk how to safely prove this, but the `Contains` constraint guarentees this is true/safe
+    let dict1 :: Dict (Elem e exceptions2)
+        dict1 = proveElem @exceptions1 @exceptions2 @e
+    OneOf e \\ dict1
+
+-- | Prove that if 'e' is an element of 'exceptions1' and 'exceptions1' is a subset of 'exceptions2',
+-- then 'e' is an element of 'exceptions2'.
+proveElem :: forall exceptions1 exceptions2 e.
+  ( Contains exceptions1 exceptions2
+  , Elem e exceptions1
+  ) => Dict (Elem e exceptions2)
+proveElem = withDict (unsafeCoerceConstraint :: (Elem e exceptions1, Contains exceptions1 exceptions2) :- (Elem e exceptions2)) Dict
+
+-- get the error from 'CheckedExcept'
+runCheckedExcept :: CheckedExcept es a -> Either (OneOf es) a
+runCheckedExcept ce = runIdentity (runCheckedExceptT ce)
+
+-- | the class for checked exceptions
+class Typeable e => CheckedException e where
+  -- | encode an exception to 'String'. defaults to 'displayException' when available.
+  encodeException :: e -> String
+  -- | reify the exception. defaults to 'withOneOf\' e cast'
+  fromOneOf :: forall es. OneOf es -> Maybe e
+
+  default encodeException :: Exception e => e -> String
+  encodeException = displayException
+
+  default fromOneOf :: Typeable e => OneOf es -> Maybe e
+  fromOneOf e = withOneOf' e cast
+
+-- | DerivingVia newtype wrapper to derive 'CheckedException' from a 'Show' instance declaration.
+-- Useful for prototyping, but I wouldn't recommend this for serious work.
+newtype ShowException a = ShowException a
+
+instance (Show a, Typeable a) => CheckedException (ShowException a) where
+  encodeException (ShowException x) = show x
+
+-- | DerivingVia newtype wrapper to derive 'CheckedException' from 'Exception'
+newtype ExceptionException a = ExceptionException a
+
+instance (Show a, Typeable a, Exception a) => CheckedException (ExceptionException a) where
+  encodeException (ExceptionException e) = displayException e
+
+deriving via (ExceptionException SomeException) instance CheckedException SomeException
+
+-- | A sort of pseudo-open union that is easy to construct but difficult to
+-- deconstruct. in lieu of singletons we opt for 'Typeable' to prove the type
+-- of the existentially quantified exception 'e' in the set 'es'
+data OneOf (es :: [Type]) where
+  OneOf :: forall e es. (Elem e es, CheckedException e, Typeable e) => !e -> OneOf es
+
+-- | data type used for constructing a coverage checked case-like `catch`
+data CaseException x es where
+  CaseEndWith :: x -> CaseException x '[]
+  CaseCons :: Typeable e => (e -> x) -> CaseException x es -> CaseException x (e ': es)
+  CaseAny :: (forall e. CheckedException e => (e -> x)) -> CaseException x es
+
+-- | pattern synonym for `CaseEndWith (error "impossible")` since 'caseException' does not
+-- accept empty lists
+pattern CaseEnd :: forall x. CaseException x '[]
+pattern CaseEnd <- _ where
+  CaseEnd = CaseEndWith (error "impossible")
+
+-- | infix CaseCons with proper fixity
+infixr 7 <:
+(<:) :: Typeable e => (e -> x) -> CaseException x es -> CaseException x (e : es)
+(<:) = CaseCons
+
+-- | throw a checked exception 'e' that is a member of the exception set 'es'
+throwCheckedException :: forall e es m a. (Elem e es, CheckedException e, Applicative m) => e -> CheckedExceptT es m a
+throwCheckedException e = do
+  let oneOf :: OneOf es
+      oneOf = OneOf e
+  CheckedExceptT $ pure $ Left oneOf
+
+-- | apply a function 'f' over a checked exception, using methods from the 'CheckedException' typeclass
+applyAll :: (forall e. CheckedException e => e -> b) -> OneOf es -> b
+applyAll f (OneOf e) = f e
+
+-- | catch an exception or 'mempty' (think 'pure ()' or 'Nothing')
+withOneOf :: (Elem e es, Monoid a, CheckedException e) => OneOf es -> (e -> a) -> a
+withOneOf e f = case fromOneOf e of
+  Just x -> f x
+  Nothing -> mempty
+
+-- | catch an exception, totally
+withOneOf' :: OneOf es -> (forall e. (Elem e es, CheckedException e, Typeable e) => e -> a) -> a
+withOneOf' (OneOf e) f = f e
+
+-- | Remove duplicates from a type-level list.
+type family Nub xs where
+  Nub '[] = '[]
+  Nub (x ': xs) = x ': Nub (Remove x xs)
+
+-- | type-level list concatenation
+infixr 5 ++
+type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
+    '[]       ++ ys = ys
+    (x ': xs) ++ ys = x ': xs ++ ys
+
+-- | Remove element from a type-level list.
+type family Remove x xs where
+  Remove x '[]       = '[]
+  Remove x (x ': ys) =      Remove x ys
+  Remove x (y ': ys) = y ': Remove x ys
+
+-- | is `x` present in the list `xs`?
+type family Elem' x xs where
+  Elem' x '[] = 'False
+  Elem' x (x ': xs) = 'True
+  Elem' x (y ': xs) = Elem' x xs
+
+-- | type Elem x xs = Elem' x xs ~ 'True
+-- sometimes causes weird type errors when it doesn't propagate correctly ??
+type family Elem x xs :: Constraint where
+  Elem x xs =
+    If (Elem' x xs)
+      (() :: Constraint)
+      (NotElemTypeError x xs)
+
+-- | type error for when 'Elem e es' fails to hold
+type NotElemTypeError x xs = TypeError ('ShowType x ':<>: 'Text " is not a member of " ':<>: 'ShowType xs)
+
+-- | constraint that the list 'as' is a subset of list 'bs'
+type family Contains (as :: [k]) (bs :: [k]) :: Constraint where
+  Contains '[] _ = ()
+  Contains as as = ()
+  Contains (a ': as) bs = (Elem' a bs ~ 'True, Contains as bs)
+
+-- | type-level proof that a list is non-empty, used for constraining 'caseException' so that you don't
+-- pointlessly throw error
+type family NonEmpty xs :: Constraint where
+  NonEmpty '[] = TypeError ('Text "type level list must be non-empty")
+  NonEmpty _ = () :: Constraint
+
+-- TODO: exceptions can show up more than once in the list, which we handle with
+-- 'Nub', but the error message we give to the use for trying to catch an exception
+-- twice is really bad
+caseException :: NonEmpty es => OneOf es -> CaseException x (Nub es) -> x
+caseException (OneOf e') = go e'
+  where
+  test :: (Typeable e1, Typeable e2) => e2 -> (e1 -> x) -> Maybe (e1 :~: e2)
+  test _ _ = eqT
+  go :: (CheckedException e, Typeable e) => e -> CaseException x es -> x
+  go e (CaseCons f rec) = case test e f of
+    Just Refl -> f e
+    Nothing -> go e rec
+  go e (CaseAny f) = f e
+  go _ (CaseEndWith x) = x
+
+-- | add 'SomeException' to the exceptions set. preferably, call this before catching the checked
+-- exceptions so there are no surprising exceptions.
+catchSomeException :: (Monad m, MonadIO m) => Elem SomeException es => CheckedExceptT es m ()
+catchSomeException = do
+  me <- lift $ liftIO $ catch (pure Nothing) (pure . Just)
+  case me of
+    Nothing -> pure ()
+    Just e -> throwCheckedException (e :: SomeException)
diff --git a/lib/Control/Monad/CheckedExcept/Plugin.hs b/lib/Control/Monad/CheckedExcept/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/lib/Control/Monad/CheckedExcept/Plugin.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE CPP #-}
+
+module Control.Monad.CheckedExcept.Plugin (plugin) where
+
+import GHC.Plugins
+import Control.Monad.CheckedExcept.Plugin.Bind
+
+-- | help resolve ambiguous type variables resulting from the
+-- very general type of Control.Monad.CheckedExcept.QualifiedDo.(>>=)
+plugin :: Plugin
+plugin = defaultPlugin
+    { tcPlugin = bindPlugin
+#if __GLASGOW_HASKELL__ >= 806
+    , pluginRecompile  = purePlugin
+#endif
+    }
+
diff --git a/lib/Control/Monad/CheckedExcept/Plugin/Bind.hs b/lib/Control/Monad/CheckedExcept/Plugin/Bind.hs
new file mode 100644
--- /dev/null
+++ b/lib/Control/Monad/CheckedExcept/Plugin/Bind.hs
@@ -0,0 +1,426 @@
+{-# LANGUAGE
+    ViewPatterns
+  , OverloadedStrings
+  , NamedFieldPuns
+  , LambdaCase
+  , TupleSections
+  , RecordWildCards
+  , MultiWayIf
+  , TypeApplications
+  , OverloadedRecordDot
+  , ScopedTypeVariables
+#-}
+
+{-# OPTIONS_GHC -Wno-unused-local-binds #-}
+
+module Control.Monad.CheckedExcept.Plugin.Bind
+  ( bindPlugin
+  -- disable unused warnings
+  , tcPrintLn
+  , tcPrint
+  , tcPrintOutputable
+  , tcTraceLabel
+  , evByFiat
+  )
+where
+
+import GHC.Plugins hiding ((<>))
+import GHC.Tc.Types.Constraint
+import qualified GHC.Tc.Plugin as TC
+import qualified GHC.Tc.Types as TC
+import GHC.Tc.Types.Evidence (EvTerm (..), evCast)
+import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
+import GHC.Tc.Plugin (tcPluginTrace)
+import Data.List (nubBy)
+import GHC.Types.Unique (hasKey)
+import GHC.Builtin.Names (consDataConKey)
+import Data.Maybe (mapMaybe, listToMaybe)
+import Data.Bifunctor (second)
+import GHC.Core.Reduction (Reduction(..))
+import GHC.Tc.Utils.TcType (eqType)
+import Control.Monad (join)
+
+{-
+    ************************************************************
+    *                                                          *
+    *                  Plugin initialization                   *
+    *                                                          *
+    ************************************************************
+-}
+
+data Environment = Environment
+  { containsTyCon :: TyCon
+  , elem'TyCon :: TyCon
+  , elemTyCon :: TyCon
+  , checkedExceptTTyCon :: TyCon
+  , notElemTypeErrorTyCon :: TyCon
+  }
+
+bindPlugin :: TcPlugin
+bindPlugin _ = Just $ TC.TcPlugin
+  { TC.tcPluginInit = do
+      checkedExceptMod <- lookupCheckedExceptMod
+      containsTyCon <- lookupContains checkedExceptMod
+      elem'TyCon <- lookupElem' checkedExceptMod
+      elemTyCon <- lookupElem checkedExceptMod
+      checkedExceptTTyCon <- lookupCheckedExceptT checkedExceptMod
+      notElemTypeErrorTyCon <- lookupNotElemTypeError checkedExceptMod
+      pure Environment {..}
+  , TC.tcPluginSolve = solveBind
+  , TC.tcPluginStop = const $ pure ()
+  , TC.tcPluginRewrite = mkRewriter
+  }
+
+lookupTyConWithMod :: String -> Module -> TC.TcPluginM TyCon
+lookupTyConWithMod name modCE = do
+  let tyCo_OccName = mkTcOcc name
+  tyCo <- TC.lookupOrig modCE tyCo_OccName
+  TC.tcLookupTyCon tyCo
+
+lookupCheckedExceptMod :: TC.TcPluginM Module
+lookupCheckedExceptMod = do
+   findResult <- TC.findImportedModule ( mkModuleName "Control.Monad.CheckedExcept" ) NoPkgQual -- ( Just "checked-exceptions" )
+   case findResult of
+     TC.Found _ modCE -> pure modCE
+     _ -> error "Couldn't find Control.Monad.CheckedExcept"
+
+lookupContains :: Module -> TC.TcPluginM TyCon
+lookupContains = lookupTyConWithMod "Contains"
+
+lookupElem' :: Module -> TC.TcPluginM TyCon
+lookupElem' = lookupTyConWithMod "Elem'"
+
+lookupElem :: Module -> TC.TcPluginM TyCon
+lookupElem = lookupTyConWithMod "Elem"
+
+lookupCheckedExceptT :: Module -> TC.TcPluginM TyCon
+lookupCheckedExceptT modCE = do
+  let
+    myTyFam_OccName :: OccName
+    myTyFam_OccName = mkTcOcc "CheckedExceptT"
+  myTyFam_Name <- TC.lookupOrig modCE myTyFam_OccName
+  TC.tcLookupTyCon myTyFam_Name
+
+lookupNotElemTypeError :: Module -> TC.TcPluginM TyCon
+lookupNotElemTypeError = lookupTyConWithMod "NotElemTypeError"
+
+{-
+    ************************************************************
+    *                                                          *
+    *     Control.Monad.CheckedExcept constraint solver        *
+    *                                                          *
+    ************************************************************
+-}
+
+solveBind :: Environment -> TC.TcPluginSolver
+solveBind _ _ _ [] = pure $ TC.TcPluginOk [] []
+solveBind env@Environment{..} _evBinds _givens wanteds = do
+  (solved, insoluable, newCt) <- concatUnzip3 <$> traverse solve1Wanted wanteds
+  pure TC.TcPluginSolveResult
+    { tcPluginInsolubleCts = insoluable
+    , tcPluginSolvedCts = solved
+    , tcPluginNewCts = newCt
+    }
+  where
+  solve1Wanted ::
+       Ct
+    -> TC.TcPluginM
+          ( [(EvTerm, Ct)] -- solved
+          , [Ct] -- unsolved
+          , [Ct] -- new work
+          )
+  solve1Wanted unzonkedWanted =
+    TC.zonkCt unzonkedWanted >>= \wanted ->
+      let noNewWork _ _ = False
+          yesNewWork _ _ = True
+
+          -- not quite right, since we do substitutions...
+          newWorkIfVar ty1 ty2 = not (isUnified ty1 && isUnified ty2)
+
+          defWork = yesNewWork
+
+          transformConstraint label ir_ev ir_reason ty1Unzonked ty2Unzonked hasNewWork mkNewPred = do
+            tcTraceLabel (label <> "_ir_ev") ir_ev
+            tcTraceLabel (label <> "_ir_reason") ir_reason
+            mtys <- disambiguateTypeVarsUsingReturnType env wanted ty1Unzonked ty2Unzonked
+            let mkNewWanted ty1 ty2 newPred = do
+                  if hasNewWork ty1 ty2
+                  then mkNonCanonical <$> TC.newWanted (ctLoc wanted) newPred
+                  else pure $ mkNonCanonical (setCtEvPredType ir_ev $ newPred)
+            case mtys of
+              Nothing -> do
+                pure mempty -- catch this in the rewriter
+              Just (ty1, ty2) -> do
+                let newPred = substituteTypeVars [(ty1Unzonked, ty1), (ty2Unzonked, ty2)] $ mkNewPred ty1 ty2
+                newWanted <- mkNewWanted ty1 ty2 newPred
+                pure
+                  ( [ ( trustMeBro ("checked-exceptions:" <> label <> ":ambiguous") (ctEvExpr $ ctEvidence newWanted) (ctPred newWanted) (ctPred wanted)
+                       , wanted
+                       )
+                    ]
+                  , []
+                  , if hasNewWork ty1 ty2 then [newWanted] else []
+                  )
+      in
+      case wanted of
+        CIrredCan (IrredCt {ir_ev = ir_ev@CtWanted{..}, ir_reason}) -> do
+          if
+            -- Check if it's `Contains`
+            | Just (tc, [tk], [ty1Unzonked, ty2Unzonked]) <- splitTyConAppIgnoringKind ctev_pred
+            , tc == containsTyCon
+            -> transformConstraint "contains" ir_ev ir_reason ty1Unzonked ty2Unzonked defWork (\ty1 ty2 -> substContains env tk ty1 ty2 ctev_pred)
+
+            -- Check if it's `If (Elem'`
+            | Just (tcIf, _, [elemTf, _, _]) <- splitTyConAppIgnoringKind ctev_pred
+            , getOccName tcIf == mkTcOcc "If"
+            , Just (tcElem', _, [ty1Unzonked, ty2Unzonked]) <- splitTyConAppIgnoringKind elemTf
+            , tcElem' == elem'TyCon
+            -> do transformConstraint "if_1" ir_ev ir_reason ty1Unzonked ty2Unzonked defWork (\ty1 ty2 -> substElem' env ty1 ty2 ctev_pred)
+
+            -- Check if it's `Elem`
+            | Just (tcElem, _, [ty1Unzonked, ty2Unzonked]) <- splitTyConAppIgnoringKind ctev_pred
+            , tcElem == elemTyCon
+            -> do transformConstraint "elem_2" ir_ev ir_reason ty1Unzonked ty2Unzonked defWork (\ty1 ty2 -> substElem env ty1 ty2 ctev_pred)
+
+            | otherwise -> do
+                tcTraceLabel "unwanted2" (ctKind wanted, wanted)
+                pure ([], [wanted], [])
+
+        _ -> do
+          tcTraceLabel "unwanted" (ctKind wanted, wanted)
+          pure ([], [wanted], [])
+
+substContains :: Environment -> Type -> Type -> Type -> PredType -> PredType
+substContains _env _tk ty1 _ty2 predTy =
+  case getTyVar_maybe ty1 of
+    Nothing -> predTy
+    Just ty1Var -> substTyWith [ty1Var] [emptyListKindTy] predTy
+
+substElem' :: Environment -> Type -> Type -> PredType -> PredType
+substElem' _env _ty1 ty2 predTy =
+  case getTyVar_maybe ty2 of
+    Nothing -> predTy
+    Just ty2Var -> substTyWith [ty2Var] [emptyListKindTy] predTy
+
+substElem :: Environment -> Type -> Type -> PredType -> PredType
+substElem _env _ty1 ty2 predTy =
+  case getTyVar_maybe ty2 of
+    Nothing -> predTy
+    Just ty2Var -> substTyWith [ty2Var] [emptyListKindTy] predTy
+
+-- Function to disambiguate type variables using the return type of the function from which the wanted constraint arises
+disambiguateTypeVarsUsingReturnType :: Environment -> Ct -> Type -> Type -> TC.TcPluginM (Maybe (Type, Type))
+disambiguateTypeVarsUsingReturnType Environment {..} wanted ty1 ty2 = do
+  fnType <- lookupReturnType (ctLocEnv (ctLoc wanted))
+  tcTraceLabel "fnType" fnType
+  esType <- do
+      let fnTyArgs = getRuntimeArgTysOrTy fnType
+          mts = case lastMaybe fnTyArgs of
+                Just (st,_) -> do
+                  ts1 <- findTyArgs checkedExceptTTyCon (irrelevantMult st)
+                  esType <- case ts1 of
+                    [esType, _, _] -> Just esType
+                    _ -> Nothing
+                  extractMPromotedList esType
+                Nothing -> Nothing
+      case mts of
+        Just ts ->  uniquePromotedList <$> traverse TC.zonkTcType ts
+        Nothing -> do
+
+          let ts1 = case lastMaybe fnTyArgs of
+                Just (st,_) -> do
+                  findTyArgs checkedExceptTTyCon (irrelevantMult st)
+                Nothing -> Nothing
+          tcTraceLabel "fnTyArgs" fnTyArgs
+          tcTraceLabel "ts1" ts1
+          failWithTrace "impossibru"
+  tcTraceLabel "esType" esType
+  if isUnified ty1 && isUnified ty2
+  then pure Nothing
+  else do
+    zonkedTy1 <- TC.zonkTcType ty1
+    zonkedTy2 <- TC.zonkTcType ty2
+    let disambiguatedTy1 = if isUnified zonkedTy1 then zonkedTy1 else esType
+        disambiguatedTy2 = if isUnified zonkedTy2 then zonkedTy2 else esType
+    tcTraceLabel "ambiguous    " (ty1, ty2)
+    tcTraceLabel "disambiguated" (disambiguatedTy1, disambiguatedTy2)
+    pure $ Just (disambiguatedTy1, disambiguatedTy2)
+
+-- Function to lookup the return type from the environment
+lookupReturnType :: CtLocEnv -> TC.TcPluginM (Type, Arity)
+lookupReturnType env = case ctl_bndrs env of
+  ts@(TC.TcIdBndr tcid _:_) -> do
+      tcTraceLabel "lookupReturnType" ts
+      pure $ (idType tcid, idArity tcid)
+  [] -> failWithTrace "No return type found in environment"
+  _ -> failWithTrace "Unresolved return type"
+
+{-
+    ************************************************************
+    *                                                          *
+    *     Control.Monad.CheckedExcept type family rewriter     *
+    *                                                          *
+    ************************************************************
+-}
+
+mkRewriter :: Environment -> UniqFM TyCon TC.TcPluginRewriter
+mkRewriter env@Environment{..} = listToUFM 
+  [ (elem'TyCon, rewriteElem' env)
+  , (elemTyCon, rewriteElem env)
+  , (containsTyCon, rewriteContains env)
+  ]
+
+rewriteElem' :: Environment -> TC.TcPluginRewriter
+rewriteElem' env@Environment{..} = rewriteBothElem trueCase falseCase env
+  where
+  trueCase = mkTyConApp promotedTrueDataCon []
+  falseCase _ ty1 ty2 = mkTyConApp notElemTypeErrorTyCon [ty1, ty2]
+
+rewriteElem :: Environment -> TC.TcPluginRewriter
+rewriteElem env@Environment{..} = rewriteBothElem trueCase falseCase env
+  where
+  trueCase = mkConstraintTupleTy []
+  falseCase _tk ty1 ty2 = mkTyConApp notElemTypeErrorTyCon [ty1, ty2]
+
+rewriteBothElem :: Applicative f => Type -> (Type -> Type -> Type -> Type) -> Environment -> p1 -> p2 -> [Type] -> f TC.TcPluginRewriteResult
+rewriteBothElem trueCase falseCase Environment{..} _rewriteEnv _givens [tk, ty, tys] =
+  case extractMPromotedList tys of
+    Nothing -> pure TC.TcPluginNoRewrite
+    Just tyList -> do
+      let result = if any (eqType ty) tyList
+                   then trueCase
+                   else falseCase tk ty tys
+      let coercion = mkUnivCo (PluginProv "checked-exceptions") Nominal (mkTyConApp elem'TyCon [ty, tys]) result
+      pure $ TC.TcPluginRewriteTo (Reduction coercion result) []
+rewriteBothElem _ _ _ _ _ _ = pure TC.TcPluginNoRewrite
+
+rewriteContains :: Environment -> TC.TcPluginRewriter
+rewriteContains Environment{..} _rewriteEnv _givens [tk, tys1, tys2] = do
+  case extractMPromotedList tys1 of
+    Just tyList1 -> do
+      let mkElemConstraint x = mkTyConApp elemTyCon [tk, x, tys2]
+          result = mkConstraintTupleTy $ fmap mkElemConstraint tyList1
+      let coercion = mkUnivCo (PluginProv "checked-exceptions") Nominal (mkTyConApp elem'TyCon [tys1, tys2]) result
+      pure $ TC.TcPluginRewriteTo (Reduction coercion result) []
+    _ -> pure TC.TcPluginNoRewrite
+rewriteContains _ _ _ _ = do
+  pure TC.TcPluginNoRewrite
+
+{-
+    ************************************************************
+    *                                                          *
+    *                    Utility functions                     *
+    *                                                          *
+    ************************************************************
+-}
+
+concatUnzip3 :: [([a],[b],[c])] -> ([a],[b],[c])
+concatUnzip3 xs = (concat a, concat b, concat c)
+    where (a,b,c) = unzip3 xs
+
+failWithTrace :: forall x. String -> TC.TcPluginM x
+failWithTrace s = do
+  tcTraceLabel "fail" (mkFastString s)
+  fail s
+
+tcPrintLn :: String -> TC.TcPluginM ()
+tcPrintLn = TC.tcPluginIO . putStrLn
+
+tcPrint :: String -> TC.TcPluginM ()
+tcPrint = TC.tcPluginIO . putStr
+
+tcPrintOutputable :: Outputable a => a -> TC.TcPluginM ()
+tcPrintOutputable = tcPrintLn . showSDocUnsafe . ppr
+
+tcTraceLabel :: Outputable a => String -> a -> TC.TcPluginM ()
+tcTraceLabel label x = tcPluginTrace ("[checked-exceptions] " <> label) (ppr x)
+
+isUnified :: Type -> Bool
+isUnified ty =
+     isTauTy ty
+  && isConcreteType ty
+  && (not $ isTyVarTy ty)
+
+emptyListKindTy :: Type
+emptyListKindTy = mkPromotedListTy tYPEKind []
+
+uniquePromotedList :: [Type] -> Type
+uniquePromotedList tys = mkPromotedListTy tYPEKind $ nubBy eqType tys
+
+-- | Extract the elements of a promoted list, returns Nothing if not a promoted list
+extractMPromotedList :: Type -> Maybe [Type]
+extractMPromotedList tys = go tys
+  where
+    go list_ty
+      | Just (tc, _, [t, ts]) <- splitTyConAppIgnoringKind list_ty
+      = assert (tc `hasKey` consDataConKey) $
+        case go ts of
+          Nothing -> Nothing
+          Just ts' -> Just $ t : ts'
+
+      | Just (tc, _, []) <- splitTyConAppIgnoringKind list_ty
+      = assert (tc `hasKey` nilDataConKey)
+        Just []
+
+      | otherwise
+      = Nothing
+
+ctKind :: Ct -> FastString
+ctKind = \case
+  CDictCan     {} -> "CDictCan     "
+  CIrredCan    {} -> "CIrredCan    "
+  CEqCan       {} -> "CEqCan       "
+  CQuantCan    {} -> "CQuantCan    "
+  CNonCanonical{} -> "CNonCanonical"
+
+-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce'
+evByFiat :: String -- ^ Name the coercion should have
+         -> Type   -- ^ The LHS of the equivalence relation (~)
+         -> Type   -- ^ The RHS of the equivalence relation (~)
+         -> EvTerm
+evByFiat name t1 t2 = EvExpr $ Coercion $ mkUnivCo (PluginProv name) Nominal t1 t2
+
+-- a *slightly* more safe version of evByFiat that will succeed even when
+-- the new wanted's core expr is not emitted
+trustMeBro :: String -- ^ Name the coercion should have
+         -> Expr CoreBndr
+         -> Type   -- ^ The LHS of the equivalence relation (~)
+         -> Type   -- ^ The RHS of the equivalence relation (~)
+         -> EvTerm
+trustMeBro name expr t1 t2 = evCast expr $ mkUnivCo (PluginProv name) Nominal t1 t2
+
+-- accepts a map of types to substitute if they are type variables
+-- and performs those substitutions on the tyUnsubbed argument
+substituteTypeVars :: [(Type,Type)] -> Type -> Type
+substituteTypeVars tyMap tyUnsubbed =
+  let (tyVars,concTys) =
+        unzip $ mapMaybe
+          (\(tyVarTy,tyRepl) -> do
+              tyVar <- getTyVar_maybe tyVarTy
+              pure (tyVar, tyRepl)
+          )
+          tyMap
+  in substTyWith tyVars concTys tyUnsubbed
+
+splitTyConAppIgnoringKind :: Type -> Maybe (TyCon, [Type], [Type])
+splitTyConAppIgnoringKind ty = do
+  (tyCon, tys) <- splitTyConApp_maybe ty
+  let (invisTys, visTys) = partitionInvisibleTypes tyCon tys
+  pure (tyCon, invisTys, visTys)
+
+-- getRunTimeArgTys can decompose certain types of arity 0 (like newtypes)
+-- so we have to check the arity ourselves
+getRuntimeArgTysOrTy :: (Type, Arity) -> [(Scaled Type, Maybe FunTyFlag)]
+getRuntimeArgTysOrTy (ty, arity) = case arity of
+  0 -> [(unrestricted ty, Nothing)]
+  _ -> fmap (second Just) (getRuntimeArgTys ty)
+
+findTyArgs :: TyCon -> Type -> Maybe [Type]
+findTyArgs findTyCon ty = do
+  (tyCon, _, tys) <- splitTyConAppIgnoringKind ty
+  if tyCon == findTyCon
+  then Just tys
+  else
+    case instNewTyCon_maybe tyCon tys of
+      Nothing -> join $ listToMaybe $ fmap (findTyArgs findTyCon) tys
+      Just (ty', _) -> findTyArgs findTyCon ty'
diff --git a/lib/Control/Monad/CheckedExcept/QualifiedDo.hs b/lib/Control/Monad/CheckedExcept/QualifiedDo.hs
new file mode 100644
--- /dev/null
+++ b/lib/Control/Monad/CheckedExcept/QualifiedDo.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE
+    TypeApplications
+  , ScopedTypeVariables
+  , LambdaCase
+#-}
+
+module Control.Monad.CheckedExcept.QualifiedDo
+  ( (>>=)
+  , (>>)
+  , pure
+  , return
+  , fail
+  ) where
+
+import Control.Monad.CheckedExcept
+import Prelude hiding (Monad(..), Applicative(..), MonadFail(..))
+import qualified Prelude
+
+-- | Bind operator for 'CheckedExceptT' that allows chaining computations
+-- that may expand the exception set.
+(>>=) :: forall exceptions1 exceptions2 exceptions3 m a.
+  ( Contains exceptions1 exceptions3
+  , Contains exceptions2 exceptions3
+  , Prelude.Monad m
+  )
+  => CheckedExceptT exceptions1 m a
+  -> (a -> CheckedExceptT exceptions2 m a)
+  -> CheckedExceptT exceptions3 m a
+m >>= f = do
+  CheckedExceptT $ do
+    runCheckedExceptT m Prelude.>>= \case
+      Left e -> Prelude.pure $ Left (weakenOneOf @exceptions1 @exceptions3 e)
+      Right a -> runCheckedExceptT (weakenExceptions (f a))
+
+-- | 'pure' function for 'CheckedExceptT'.
+pure :: Prelude.Monad m => a -> CheckedExceptT es m a
+pure = Prelude.pure
+
+-- | 'return' function for 'CheckedExceptT'.
+return :: Prelude.Monad m => a -> CheckedExceptT es m a
+return = Prelude.return
+
+-- | Sequentially compose two actions, discarding any value produced by the first.
+(>>) :: forall exceptions1 exceptions2 exceptions3 m a x.
+  ( Contains exceptions1 exceptions3
+  , Contains exceptions2 exceptions3
+  , Prelude.Monad m
+  )
+  => CheckedExceptT exceptions1 m x
+  -> CheckedExceptT exceptions2 m a
+  -> CheckedExceptT exceptions3 m a
+a >> b = weakenExceptions a Prelude.>> weakenExceptions b
+
+-- | 'fail' function for 'CheckedExceptT'.
+fail :: Prelude.MonadFail m => String -> CheckedExceptT es m a
+fail = Prelude.fail
+
+{-
+Example usage:
+
+module CompTest where
+
+import Control.Monad.CheckedExcept
+import Control.Monad.Trans.Class (lift)
+import qualified Control.Monad.CheckedExcept.QualifiedDo as CheckedExcept
+
+testCE1 :: CheckedExceptT '[()] IO ()
+testCE1 = CheckedExcept.do
+  lift $ putStrLn "1"
+  lift $ pure ()
+  pure ()
+
+testCE2 :: CheckedExceptT '[Int] IO ()
+testCE2 = CheckedExcept.do
+  lift $ putStrLn "2"
+  throwCheckedException (1 :: Int)
+  pure ()
+
+testCE3 :: CheckedExceptT '[Bool] IO ()
+testCE3 = CheckedExcept.do
+  lift $ putStrLn "3"
+  throwCheckedException False
+  pure ()
+
+testCE4 :: CheckedExceptT '[String] IO ()
+testCE4 = CheckedExcept.do
+  lift $ putStrLn "4"
+  throwCheckedException "err"
+  pure ()
+
+testCE5 :: CheckedExceptT '[Char] IO ()
+testCE5 = CheckedExcept.do
+  lift $ putStrLn "5"
+  throwCheckedException 'c'
+  pure ()
+
+testCE :: CheckedExceptT '[(), Int, Bool, String] IO ()
+testCE = CheckedExcept.do
+  () <- testCE1
+  () <- testCE2
+  () <- testCE3
+  () <- testCE4
+  -- () <- testCE5 -- doesn't compile
+  pure ()
+
+test :: CheckedExcept TestExceptions () -> IO ()
+test ce = case runCheckedExcept ce of
+  Left e -> do
+    applyAll (putStrLn . encodeException) e
+    -- or
+    withOneOf @() e $ \() -> putStrLn "()"
+    withOneOf @Int e $ \n -> print $ n + 1
+    withOneOf @Bool e $ \_ -> pure ()
+    -- or
+    caseException e
+      (  (\() -> putStrLn "()")
+      <: (\n -> print $ n + 1)
+      <: CaseAny (\x -> putStrLn $ encodeException x)
+      -- <: (\b -> putStrLn "bool")
+      -- <: (\s -> putStrLn "string")
+      -- <: CaseEnd
+      )
+  Right () -> putStrLn "Right"
+
+type TestExceptions = '[(), Int, Bool, String]
+
+deriving via (ShowException ()) instance CheckedException ()
+deriving via (ShowException Int) instance CheckedException Int
+deriving via (ShowException Bool) instance CheckedException Bool
+deriving via (ShowException String) instance CheckedException [Char]
+deriving via (ShowException Char) instance CheckedException Char
+-}
diff --git a/test/CompTest.hs b/test/CompTest.hs
new file mode 100644
--- /dev/null
+++ b/test/CompTest.hs
@@ -0,0 +1,111 @@
+{-# OPTIONS_GHC
+    -fno-warn-orphans
+#-}
+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file
+#-}
+{-# OPTIONS_GHC -fplugin Control.Monad.CheckedExcept.Plugin -fplugin-opt Control.Monad.CheckedExcept.Plugin:verbose  #-}
+
+{-# LANGUAGE
+    MagicHash
+  , TemplateHaskell
+  , TypeApplications
+  , DataKinds
+  , StandaloneDeriving
+  , DerivingVia
+  , QualifiedDo
+  , FlexibleInstances
+  , TypeFamilies
+#-}
+
+module CompTest where
+
+-- import Test.Tasty.HUnit
+import Control.Monad.CheckedExcept
+import Control.Monad.Trans.Class (lift)
+import qualified Control.Monad.CheckedExcept.QualifiedDo as CheckedExcept
+
+-- badTestCE1 :: CheckedExceptT '[Int] IO ()
+-- badTestCE1 = CheckedExcept.do
+--   lift $ putStrLn "bad 1"
+--   throwCheckedException 'c' -- this shouldn't work
+
+testCE1 :: CheckedExceptT '[()] IO ()
+testCE1 = CheckedExcept.do
+  lift $ putStrLn "1"
+  lift $ pure ()
+  pure ()
+
+testCE2 :: CheckedExceptT '[Int] IO ()
+testCE2 = CheckedExcept.do
+  lift $ putStrLn "2"
+  throwCheckedException (1 :: Int)
+  pure ()
+
+testCE3 :: CheckedExceptT '[Bool] IO ()
+testCE3 = CheckedExcept.do
+  lift $ putStrLn "3"
+  throwCheckedException False
+  pure ()
+
+testCE4 :: CheckedExceptT '[String] IO ()
+testCE4 = CheckedExcept.do
+  lift $ putStrLn "4"
+  throwCheckedException "err"
+  pure ()
+
+testCE5 :: CheckedExceptT '[Char] IO ()
+testCE5 = CheckedExcept.do
+  lift $ putStrLn "5"
+  throwCheckedException 'c'
+  pure ()
+
+testCE :: CheckedExceptStack ()
+testCE = CheckedExceptStack $ CheckedExcept.do
+  () <- testCE1
+  () <- testCE2
+  () <- testCE3
+  () <- testCE4
+  -- () <- testCE5 -- doesn't compile
+  pure ()
+
+test :: CheckedExcept TestExceptions () -> IO ()
+test ce = case runCheckedExcept ce of
+  Left e -> do
+    applyAll (putStrLn . encodeException) e
+    -- or
+    withOneOf @() e $ \() -> putStrLn "()"
+    withOneOf @Int e $ \n -> print $ n + 1
+    withOneOf @Bool e $ \_ -> pure ()
+    -- or
+    caseException e
+      (  (\() -> putStrLn "()")
+      <: (\n -> print $ n + 1)
+      <: (\_b -> putStrLn "bool")
+      <: (\_s -> putStrLn "string")
+      <: CaseEnd
+      )
+    caseException e
+      (  (\() -> putStrLn "()")
+      <: CaseAny (\x -> putStrLn $ encodeException x)
+      )
+  Right () -> putStrLn "Right"
+
+{-
+-- doens't compile
+test2 :: CheckedExcept '[] () -> IO ()
+test2 ce =
+  case runCheckedExcept ce of
+    Left (OneOf e) -> do
+      caseException (Proxy @'[]) e Nil
+    Right () -> putStrLn "Right"
+-}
+
+type TestExceptions = '[(), Int, Bool, String]
+
+deriving via (ShowException ()) instance CheckedException ()
+deriving via (ShowException Int) instance CheckedException Int
+deriving via (ShowException Bool) instance CheckedException Bool
+deriving via (ShowException String) instance CheckedException [Char]
+deriving via (ShowException Char) instance CheckedException Char
+
+newtype CheckedExceptStack a = CheckedExceptStack { runCheckedExceptStack :: CheckedExceptT TestExceptions IO a }
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,33 @@
+{-# OPTIONS_GHC
+    -fno-warn-orphans
+#-}
+
+{-# LANGUAGE
+    MagicHash
+  , TemplateHaskell
+  , TypeApplications
+  , DataKinds
+  , StandaloneDeriving
+  , DerivingVia
+  , QualifiedDo
+#-}
+
+module Main where
+
+import Test.Tasty
+-- import Test.Tasty.HUnit
+-- import Control.Monad.CheckedExcept
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests" [unitTests]
+
+unitTests :: TestTree
+unitTests = testGroup "Unit tests"
+  [
+  ]
+
+unwrap :: Either a b -> b
+unwrap = either (error "unwrap") id