diff --git a/effin.cabal b/effin.cabal
--- a/effin.cabal
+++ b/effin.cabal
@@ -1,5 +1,5 @@
 name:                effin
-version:             0.1.1.0
+version:             0.2.0.0
 synopsis:            A Typeable-free implementation of extensible effects
 homepage:            https://github.com/YellPika/effin
 license:             BSD3
@@ -21,10 +21,9 @@
   For example, the following code implements a handler for exceptions:
   .
   > runException :: Effect (Exception e ': es) a -> Effect es (Either e a)
-  > runException =
-  >     handle (\x -> return (Right x))
-  >     $ eliminate (\(Exception e) -> return (Left e))
-  >     $ defaultRelay
+  > runException = eliminate
+  >     (\x -> return (Right x))
+  >     (\(Exception e) -> return (Left e))
   .
   Compare this to the corresponding code in extensible-effects
   (<http://hackage.haskell.org/package/extensible-effects>):
@@ -35,11 +34,8 @@
   >     loop (Val x) = return (Right x)
   >     loop (E u)   = handleRelay u loop (\(Exc e) -> return (Left e))
   .
-  In particular:
-  .
-  * Effect implementors are not required to do any recursion.
-  .
-  * The functions for writing effect handlers can be easily composed.
+  In particular, effect implementors are not required to do any recursion,
+  thereby making effect handlers more composeable.
 
 flag mtl
   description: Enable MTL support
@@ -49,18 +45,21 @@
 library
   exposed-modules:
     Control.Effect,
+    Control.Effect.Bracket,
     Control.Effect.Coroutine,
     Control.Effect.Exception,
+    Control.Effect.Reader,
     Control.Effect.Lift,
     Control.Effect.List,
-    Control.Effect.Reader,
     Control.Effect.State,
-    Control.Effect.Thread,
-    Control.Effect.Union,
+    Control.Effect.Witness,
     Control.Effect.Writer,
     Control.Monad.Effect
 
   other-modules:
+    Data.Index,
+    Data.Type.Row,
+    Data.Type.Nat
     Data.Union
 
   build-depends: base >= 4.7 && < 4.8
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
--- a/src/Control/Effect.hs
+++ b/src/Control/Effect.hs
@@ -1,23 +1,23 @@
 module Control.Effect (
+    module Control.Effect.Bracket,
     module Control.Effect.Coroutine,
     module Control.Effect.Exception,
     module Control.Effect.Lift,
     module Control.Effect.List,
     module Control.Effect.Reader,
     module Control.Effect.State,
-    module Control.Effect.Thread,
-    module Control.Effect.Union,
+    module Control.Effect.Witness,
     module Control.Effect.Writer,
     module Control.Monad.Effect
 ) where
 
+import Control.Effect.Bracket
 import Control.Effect.Coroutine
 import Control.Effect.Exception
 import Control.Effect.Lift
 import Control.Effect.List
 import Control.Effect.Reader
 import Control.Effect.State
-import Control.Effect.Thread
-import Control.Effect.Union
+import Control.Effect.Witness
 import Control.Effect.Writer
 import Control.Monad.Effect
diff --git a/src/Control/Effect/Bracket.hs b/src/Control/Effect/Bracket.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Bracket.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Bracket (
+    EffectBracket, Bracket, runBracket,
+    Tag, newTag, raiseWith, exceptWith,
+    Handler, exceptAny, bracket, finally
+) where
+
+import Control.Applicative ((<$>))
+import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Control.Effect.Witness
+import Control.Monad.Effect
+
+-- | Provides a base effect for exceptions. This effect allows the dynamic
+-- generation of exception classes at runtime.
+newtype Bracket s a = Bracket { unBracket :: Union (Raise s :+ Witness s :+ Nil) a }
+  deriving Functor
+
+-- | The type of placeholder values indicating an exception class.
+data Tag s a = Tag (a -> String) (Token s a)
+
+instance TestEquality (Tag s) where
+    testEquality (Tag _ i) (Tag _ j) = testEquality i j
+
+type instance Is Bracket f = IsBracket f
+
+type family IsBracket f where
+    IsBracket (Bracket s) = True
+    IsBracket f = False
+
+class MemberEffect Bracket (Bracket s) l => EffectBracket s l
+instance MemberEffect Bracket (Bracket s) l => EffectBracket s l
+
+-- | Creates a new tag. The function parameter describes the error message that
+-- is shown in the case of an uncaught exception.
+newTag :: EffectBracket s l => (a -> String) -> Effect l (Tag s a)
+newTag toString = mask' $ Tag toString <$> newToken
+
+-- | Raises an exception of the specified class and value.
+raiseWith :: EffectBracket s l => Tag s b -> b -> Effect l a
+raiseWith tag value = mask' $ send $ Raise tag value
+
+-- | Specifies a handler for exceptions of a given class.
+exceptWith :: EffectBracket s l => Tag s b -> Effect l a -> (b -> Effect l a) -> Effect l a
+exceptWith tag effect handler = exceptAny effect [Handler tag handler]
+
+-- | A handler for an exception. Use with `exceptAny`.
+data Handler s l a where
+    Handler :: Tag s b -> (b -> Effect l a) -> Handler s l a
+
+-- | Specifies a number of handlers for exceptions thrown by the given
+-- computation. This is prefered over chained calles to `exceptWith`, i.e.
+--
+-- > exceptWith t2 (exceptWith t1 m h1) h2
+--
+-- because @h2@ could catch exceptions thrown by @h1@.
+exceptAny :: EffectBracket s l => Effect l a -> [Handler s l a] -> Effect l a
+exceptAny effect handlers = effect `exceptAll` \i x ->
+    let try (Handler j f) = (\Refl -> f x) <$> testEquality i j
+        results = mapMaybe try handlers
+    in fromMaybe (raiseWith i x) (listToMaybe results)
+
+-- | Intercepts all exceptions. Used to implement `exceptWith` and `bracket`.
+-- Not exported. Is it really a good thing to allow catching all exceptions?
+-- The most common use case for catching all exceptions is to do cleanup, which
+-- is what bracket is for.
+exceptAll :: EffectBracket s l => Effect l a -> (forall b. Tag s b -> b -> Effect l a) -> Effect l a
+exceptAll effect handler = mask' $ run $ unmask' effect
+  where
+    run = intercept return $ \(Raise t x) -> unmask' (handler t x)
+
+-- | Executes a computation with a resource, and ensures that the resource is
+-- cleaned up afterwards.
+bracket :: EffectBracket s l
+        => Effect l a -- ^ The 'acquire' operation.
+        -> (a -> Effect l ()) -- ^ The 'release' operation.
+        -> (a -> Effect l b) -- ^ The computation to perform.
+        -> Effect l b
+bracket acquire destroy run = do
+    resource <- acquire
+    result <- run resource `exceptAll` \e x -> do
+        destroy resource
+        raiseWith e x
+    destroy resource
+    return result
+
+-- | A specialized version of `bracket` which
+-- does not require an 'acquire' operation.
+finally :: EffectBracket s l => Effect l a -> Effect l () -> Effect l a
+finally effect finalizer = bracket
+    (return ())
+    (const finalizer)
+    (const effect)
+
+-- | Executes a `Bracket` effect. The Rank-2 type ensures that `Tag`s do not
+-- escape their scope.
+runBracket :: (forall s. Effect (Bracket s :+ l) a) -> Effect l a
+runBracket effect =
+    runWitness
+    $ eliminate return (\(Raise (Tag f _) x) -> error (f x))
+    $ flatten
+    $ rename unBracket effect
+
+-- A couple helper functions for getting in and out of the base effects.
+mask' :: EffectBracket s l => Effect (Raise s :+ Witness s :+ l) a -> Effect l a
+mask' = mask Bracket
+
+unmask' :: EffectBracket s l => Effect l a -> Effect (Raise s :+ Witness s :+ l) a
+unmask' = unmask unBracket
+
+-- Quick and dirty exceptions (because Union works with existing functors).
+data Raise s a where
+    Raise :: Tag s b -> b -> Raise s a
+
+instance Functor (Raise s) where
+    fmap _ (Raise n x) = Raise n x
diff --git a/src/Control/Effect/Coroutine.hs b/src/Control/Effect/Coroutine.hs
--- a/src/Control/Effect/Coroutine.hs
+++ b/src/Control/Effect/Coroutine.hs
@@ -1,40 +1,52 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Effect.Coroutine (
-    EffectCoroutine, Coroutine, Iterator (..), runCoroutine, suspend
-) where
-
-import Control.Monad.Effect
-
--- | An effect describing a suspendable computation.
-data Coroutine i o a = Coroutine (o -> a) i
-  deriving Functor
-
--- | A suspended computation.
-data Iterator i o es a
-    = Done a -- ^ Describes a finished computation.
-    | Next (o -> Effect es (Iterator i o es a)) i
-    -- ^ Describes a computation that provided a value
-    -- of type `i` and awaits a value of type `o`.
-
-type EffectCoroutine i o es = (Member (Coroutine i o) es, '(i, o) ~ CoroutineType es)
-type family CoroutineType es where
-    CoroutineType (Coroutine i o ': es) = '(i, o)
-    CoroutineType (e ': es) = CoroutineType es
-
--- | Suspends the current computation by providing a value
--- of type `i` and then waiting for a value of type `o`.
-suspend :: EffectCoroutine i o es => i -> Effect es o
-suspend = send . Coroutine id
-
--- | Converts a `Coroutine` effect into an `Iterator`.
-runCoroutine :: Effect (Coroutine i o ': es) a -> Effect es (Iterator i o es a)
-runCoroutine =
-    handle (return . Done)
-    $ eliminate (\(Coroutine f k) -> return (Next f k))
-    $ defaultRelay
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Coroutine (
+    EffectCoroutine, Coroutine, runCoroutine, suspend,
+    Iterator (..), evalIterator
+) where
+
+import Control.Monad.Effect
+
+-- | An effect describing a suspendable computation.
+data Coroutine i o a = Coroutine (o -> a) i
+  deriving Functor
+
+type instance Is Coroutine f = IsCoroutine f
+
+type family IsCoroutine f where
+    IsCoroutine (Coroutine i o) = True
+    IsCoroutine f = False
+
+class MemberEffect Coroutine (Coroutine i o) es => EffectCoroutine i o es
+instance MemberEffect Coroutine (Coroutine i o) es => EffectCoroutine i o es
+
+-- | Suspends the current computation by providing a value
+-- of type `i` and then waiting for a value of type `o`.
+suspend :: EffectCoroutine i o es => i -> Effect es o
+suspend = send . Coroutine id
+
+-- | Converts a `Coroutine` effect into an `Iterator`.
+runCoroutine :: Effect (Coroutine i o :+ es) a -> Effect es (Iterator i o es a)
+runCoroutine = eliminate (return . Done) (\(Coroutine f k) -> return (Next f k))
+
+-- | A suspended computation.
+data Iterator i o es a
+    = Done a -- ^ Describes a finished computation.
+    | Next (o -> Effect es (Iterator i o es a)) i
+    -- ^ Describes a computation that provided a value
+    -- of type `i` and awaits a value of type `o`.
+
+-- | Evaluates an iterator by providing it with an input stream.
+evalIterator :: Iterator i o es a -> [o] -> Effect es (Iterator i o es a, [i])
+evalIterator (Next f v) (x:xs) = do
+    i <- f x
+    (r, vs) <- evalIterator i xs
+    return (r, v:vs)
+evalIterator i _ = return (i, [])
diff --git a/src/Control/Effect/Exception.hs b/src/Control/Effect/Exception.hs
--- a/src/Control/Effect/Exception.hs
+++ b/src/Control/Effect/Exception.hs
@@ -1,74 +1,64 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-#if MTL
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-#endif
-
-module Control.Effect.Exception (
-    EffectException, Exception, runException,
-    raise, except, finally
-) where
-
-import Control.Monad.Effect
-
-#ifdef MTL
-import qualified Control.Monad.Error.Class as E
-
-instance EffectException e es => E.MonadError e (Effect es) where
-    throwError = raise
-    catchError = except
-#endif
-
--- | An effect that describes the possibility of failure.
-newtype Exception e a = Exception { unException :: e }
-  deriving Functor
-
-type EffectException e es = (Member (Exception e) es, e ~ ExceptionType es)
-type family ExceptionType es where
-    ExceptionType (Exception e ': es) = e
-    ExceptionType (e ': es) = ExceptionType es
-
--- | Raises an exception.
-raise :: EffectException e es => e -> Effect es a
-raise = send . Exception
-
--- | Handles an exception. Intended to be used in infix form.
---
--- > myComputation `except` \ex -> doSomethingWith ex
-except :: EffectException e es => Effect es a -> (e -> Effect es a) -> Effect es a
-except = flip run
-  where
-    run handler =
-        handle return
-        $ intercept (handler . unException)
-        $ defaultRelay
-
--- | Ensures that a computation is run after another one completes,
--- regardless of whether an exception was raised. Intended to be
--- used in infix form.
---
--- > do x <- loadSomeResource
--- >    doSomethingWith x `finally` unload x
-finally :: EffectException e es => Effect es a -> Effect es () -> Effect es a
-finally effect finalizer = do
-    result <- effect `except` \e -> do
-        finalizer
-        raise e
-    finalizer
-    return result
-
--- | Completely handles an exception effect.
-runException :: Effect (Exception e ': es) a -> Effect es (Either e a)
-runException =
-    handle (return . Right)
-    $ eliminate (return . Left . unException)
-    $ defaultRelay
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Exception (
+    EffectException, Exception, runException,
+    raise, except
+) where
+
+import Control.Effect.Bracket
+import Control.Monad.Effect
+
+#ifdef MTL
+import Data.Type.Row
+import qualified Control.Monad.Error.Class as E
+
+instance (Member (Exception e) l, Exception e ~ InstanceOf Exception l) => E.MonadError e (Effect l) where
+    throwError = raise
+    catchError = except
+#endif
+
+-- | An effect that describes the possibility of failure.
+data Exception e a = Raise e | Catch a (e -> a)
+  deriving Functor
+
+type instance Is Exception f = IsException f
+
+type family IsException f where
+    IsException (Exception e) = True
+    IsException f = False
+
+class MemberEffect Exception (Exception e) l => EffectException e l
+instance MemberEffect Exception (Exception e) l => EffectException e l
+
+-- | Raises an exception.
+raise :: EffectException e l => e -> Effect l a
+raise = send . Raise
+
+-- | Handles an exception. Intended to be used in infix form.
+--
+-- > myComputation `except` \ex -> doSomethingWith ex
+except :: EffectException e l => Effect l a -> (e -> Effect l a) -> Effect l a
+except x f = sendEffect (Catch x f)
+
+-- | Completely handles an exception effect.
+runException :: (EffectBracket s l, Show e) => Effect (Exception e :+ l) a -> Effect l (Either e a)
+runException effect = do
+    tag <- newTag show
+    exceptWith tag
+        (eliminate (return . Right) (bind tag) effect)
+        (return . Left)
+  where
+    bind tag (Raise e) = raiseWith tag e
+    bind tag (Catch x f) = exceptWith tag x f
diff --git a/src/Control/Effect/Lift.hs b/src/Control/Effect/Lift.hs
--- a/src/Control/Effect/Lift.hs
+++ b/src/Control/Effect/Lift.hs
@@ -1,18 +1,20 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 #ifdef MTL
-{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 #endif
 
 module Control.Effect.Lift (
-    EffectLift, Lift, runLift, lift
+    EffectLift, Lift (..), runLift, lift, liftEffect
 ) where
 
 import Control.Monad.Effect
@@ -21,7 +23,7 @@
 #ifdef MTL
 import Control.Monad.Trans (MonadIO (..))
 
-instance EffectLift IO es => MonadIO (Effect es) where
+instance EffectLift IO l => MonadIO (Effect l) where
     liftIO = lift
 #endif
 
@@ -34,19 +36,26 @@
 instance Monad m => Functor (Lift m) where
     fmap f = Lift . liftM f . unLift
 
-type EffectLift m es = (Member (Lift m) es, m ~ LiftType es, Monad m)
-type family LiftType es where
-    LiftType (Lift m ': es) = m
-    LiftType (e ': es) = LiftType es
+type instance Is Lift f = IsLift f
 
+type family IsLift f where
+    IsLift (Lift m) = True
+    IsLift f = False
+
+class (Monad m, MemberEffect Lift (Lift m) l) => EffectLift m l
+instance (Monad m, MemberEffect Lift (Lift m) l) => EffectLift m l
+
 -- | Lifts a monadic value into an effect.
-lift :: EffectLift m es => m a -> Effect es a
+lift :: EffectLift m l => m a -> Effect l a
 lift = send . Lift
 
+-- | Lifts a monadic value into an effect.
+liftEffect :: EffectLift m l => m (Effect l a) -> Effect l a
+liftEffect = sendEffect . Lift
+
 -- | Converts a computation containing only monadic
 -- effects into a monadic computation.
-runLift :: Monad m => Effect '[Lift m] a -> m a
-runLift =
-    handle return
-    $ eliminate (join . unLift)
-    $ emptyRelay
+runLift :: Monad m => Effect (Lift m :+ Nil) a -> m a
+runLift = runEffect . eliminate
+    (return . return)
+    (return . join . liftM runEffect . unLift)
diff --git a/src/Control/Effect/List.hs b/src/Control/Effect/List.hs
--- a/src/Control/Effect/List.hs
+++ b/src/Control/Effect/List.hs
@@ -1,93 +1,104 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
-module Control.Effect.List (
-    EffectList, List, runList,
-    choose, never, select,
-
-    EffectCut, Cut,
-    cut, runCut
-) where
-
-import Control.Monad.Effect
-import Control.Arrow (second)
-import Control.Applicative (Alternative (..), (<$>))
-import Control.Monad (MonadPlus (..), (<=<), join)
-
--- | Describes a nondeterminism (backtracking) effect.
-newtype List a = List { unList :: [a] }
-  deriving Functor
-
-type EffectList = Member List
-
--- | Nondeterministically chooses a value from the input list.
-choose :: EffectList es => [a] -> Effect es a
-choose = send . List
-
--- | Describes a nondeterministic computation that never returns a value.
-never :: EffectList es => Effect es a
-never = choose []
-
--- | Nondeterministically chooses a value from a list of computations.
-select :: EffectList es => [Effect es a] -> Effect es a
-select = join . choose
-
--- | Obtains all possible values from a computation
--- parameterized by a nondeterminism effect.
-runList :: Effect (List ': es) a -> Effect es [a]
-runList =
-    handle (\x -> return [x])
-    $ eliminate (fmap concat . sequence . unList)
-    $ defaultRelay
-
-instance EffectList es => Alternative (Effect es) where
-    empty = never
-    x <|> y = select [x, y]
-
-instance EffectList es => MonadPlus (Effect es) where
-    mzero = empty
-    mplus = (<|>)
-
--- | Describes a Prolog-like cut effect.
--- This effect must be used with the `List` effect.
-data Cut a = Cut
-  deriving Functor
-
-type EffectCut = Member Cut
-
--- | Prevents backtracking past the point this value was invoked.
--- Unlike Prolog's '!' operator, `cut` will cause the current
--- computation to fail immediately, instead of when it backtracks.
-cut :: (EffectList es, EffectCut es) => Effect es a
-cut = send Cut
-
--- | Handles the `Cut` effect. `cut`s have no effect beyond
--- the scope of the computation passed to this function.
-runCut :: EffectList es => Effect (Cut ': es) a -> Effect es a
-runCut = choose . snd <=< reifyCut
-  where
-    -- Gather the results of a computation into a list (like in runList), but
-    -- also return a Bool indicating whether a cut was performed in the
-    -- computation. When we intercept the List effect, we get a continuation and
-    -- a list of values. If we map the continuation to the list of values, then
-    -- we get a list of computations. We can now execute each computation one by
-    -- one, and inspect the Bool after each computation to determine when we
-    -- should stop.
-    reifyCut :: EffectList es => Effect (Cut ': es) a -> Effect es (Bool, [a])
-    reifyCut =
-        handle (\x -> return (False, [x]))
-        $ eliminate (\Cut -> return (True, []))
-        $ intercept (\(List xs) -> runAll xs)
-        $ defaultRelay
-
-    runAll [] = return (False, [])
-    runAll (x:xs) = do
-        (cutRequested, x') <- x
-        if cutRequested
-        then return (True, x')
-        else second (x' ++) <$> runAll xs
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Control.Effect.List (
+    EffectList, List, runList,
+    choose, never, select,
+
+    CutEffect, Cut, runCut,
+    cut, cutFalse
+) where
+
+import Control.Monad.Effect
+import Control.Arrow (second)
+import Control.Applicative (Alternative (..), (<$>))
+import Control.Monad (MonadPlus (..), (<=<), join)
+
+-- | A nondeterminism (backtracking) effect.
+newtype List a = List { unList :: [a] }
+  deriving Functor
+
+type instance Is List f = IsList f
+
+type family IsList f where
+    IsList List = True
+    IsList f = False
+
+class Member List l => EffectList l
+instance Member List l => EffectList l
+
+-- | Nondeterministically chooses a value from the input list.
+choose :: EffectList l => [a] -> Effect l a
+choose = send . List
+
+-- | Describes a nondeterministic computation that never returns a value.
+never :: EffectList l => Effect l a
+never = choose []
+
+-- | Nondeterministically chooses a value from a list of computations.
+select :: EffectList l => [Effect l a] -> Effect l a
+select = join . choose
+
+-- | Obtains all possible values from a computation
+-- parameterized by a nondeterminism effect.
+runList :: Effect (List :+ l) a -> Effect l [a]
+runList = eliminate (return . return) (fmap concat . sequence . unList)
+
+instance EffectList l => Alternative (Effect l) where
+    empty = never
+    x <|> y = select [x, y]
+
+instance EffectList l => MonadPlus (Effect l) where
+    mzero = empty
+    mplus = (<|>)
+
+-- | Describes a Prolog-like cut effect.
+-- This effect must be used with the `List` effect.
+data Cut a = CutFalse
+  deriving Functor
+
+class (EffectList l, Member Cut l) => CutEffect l
+instance (EffectList l, Member Cut l) => CutEffect l
+
+-- | Prevents backtracking past the point this value was invoked,
+-- in the style of Prolog's "!" operator.
+cut :: CutEffect l => Effect l ()
+cut = return () <|> cutFalse
+
+-- | Prevents backtracking past the point this value was invoked.
+-- Unlike Prolog's "!" operator, `cutFalse` will cause the current
+-- computation to fail immediately, instead of when it backtracks.
+cutFalse :: CutEffect l => Effect l a
+cutFalse = send CutFalse
+
+-- | Handles the `Cut` effect. `cut`s have no effect beyond
+-- the scope of the computation passed to this function.
+runCut :: EffectList l => Effect (Cut :+ l) a -> Effect l a
+runCut = choose . snd <=< reifyCut
+  where
+    -- Gather the results of a computation into a list (like in runList), but
+    -- also return a Bool indicating whether a cut was performed in the
+    -- computation. When we intercept the List effect, we get a continuation and a
+    -- list of values. If we map the continuation to the list of values, then we
+    -- get a list of computations. We can now execute each computation one by
+    -- one, and inspect the Bool after each computation to determine when we
+    -- should stop.
+    reifyCut :: EffectList l => Effect (Cut :+ l) a -> Effect l (Bool, [a])
+    reifyCut =
+        intercept return (runAll . unList) .
+        eliminate
+            (\x -> return (False, [x]))
+            (\CutFalse -> return (True, []))
+
+    runAll [] = return (False, [])
+    runAll (x:xs) = do
+        (cutRequested, x') <- x
+        if cutRequested
+        then return (True, x')
+        else second (x' ++) <$> runAll xs
diff --git a/src/Control/Effect/Reader.hs b/src/Control/Effect/Reader.hs
--- a/src/Control/Effect/Reader.hs
+++ b/src/Control/Effect/Reader.hs
@@ -1,69 +1,72 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-#if MTL
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-#endif
-
-module Control.Effect.Reader (
-	EffectReader, Reader, runReader,
-    ask, asks, local
-) where
-
-import Control.Monad.Effect
-
-#ifdef MTL
-import qualified Control.Monad.Reader.Class as R
-
-instance EffectReader r es => R.MonadReader r (Effect es) where
-    ask = ask
-    local = local
-    reader = asks
-#endif
-
--- | An effect that describes an implicit environment.
-newtype Reader r a = Reader (r -> a)
-  deriving Functor
-
-type EffectReader r es = (Member (Reader r) es, r ~ ReaderType es)
-type family ReaderType es where
-    ReaderType (Reader r ': es) = r
-    ReaderType (e ': es) = ReaderType es
-
--- | Retrieves the current environment.
-ask :: EffectReader r es => Effect es r
-ask = asks id
-
--- | Retrieves a value that is a function of the current environment.
-asks :: EffectReader r es => (r -> a) -> Effect es a
-asks = send . Reader
-
--- | Runs a computation with a modified environment.
-local :: EffectReader r es => (r -> r) -> Effect es a -> Effect es a
-local f effect = do
-    env <- asks f
-    run env effect
-  where
-    run env =
-        handle return
-        $ intercept (bind env)
-        $ defaultRelay
-
--- | Completely handes a `Reader` effect by providing an
--- environment value to be used throughout the computation.
-runReader :: r -> Effect (Reader r ': es) a -> Effect es a
-runReader env =
-    handle return
-    $ eliminate (bind env)
-    $ defaultRelay
-
-bind :: r -> Reader r (Effect es b) -> Effect es b
-bind env (Reader k) = k env
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Reader (
+    EffectReader, Reader, runReader,
+    ask, asks, local,
+    stateReader
+) where
+
+import Control.Effect.State
+import Control.Monad.Effect
+
+#ifdef MTL
+import Data.Type.Row
+import qualified Control.Monad.Reader.Class as R
+
+instance (Member (Reader r) l, Reader r ~ InstanceOf Reader l) => R.MonadReader r (Effect l) where
+    ask = ask
+    local = local
+    reader = asks
+#endif
+
+-- | An effect that provides an implicit environment.
+newtype Reader r a = Reader (r -> a)
+  deriving Functor
+
+unReader :: r -> Reader r a -> a
+unReader x (Reader f) = f x
+
+type instance Is Reader f = IsReader f
+
+type family IsReader f where
+    IsReader (Reader r) = True
+    IsReader f = False
+
+class MemberEffect Reader (Reader r) l => EffectReader r l
+instance MemberEffect Reader (Reader r) l => EffectReader r l
+
+-- | Retrieves the current environment.
+ask :: EffectReader r l => Effect l r
+ask = asks id
+
+-- | Retrieves a value that is a function of the current environment.
+asks :: EffectReader r l => (r -> a) -> Effect l a
+asks = send . Reader
+
+-- | Runs a computation with a modified environment.
+local :: EffectReader r l => (r -> r) -> Effect l a -> Effect l a
+local f effect = do
+    env <- asks f
+    intercept return (unReader env) effect
+
+-- | Executes a reader computation which obtains
+-- its environment value from a state effect.
+stateReader :: EffectState s l => Effect (Reader s :+ l) a -> Effect l a
+stateReader = eliminate return (\(Reader f) -> get >>= f)
+
+-- | Completely handles a `Reader` effect by providing an
+-- environment value to be used throughout the computation.
+runReader :: r -> Effect (Reader r :+ l) a -> Effect l a
+runReader env = eliminate return (unReader env)
diff --git a/src/Control/Effect/State.hs b/src/Control/Effect/State.hs
--- a/src/Control/Effect/State.hs
+++ b/src/Control/Effect/State.hs
@@ -1,92 +1,95 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-#if MTL
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-#endif
-
-module Control.Effect.State (
-    EffectState, State, runState,
-    evalState, execState,
-    get, gets, put,
-    modify, modify',
-    state, withState
-) where
-
-import Control.Applicative ((<$>))
-import Control.Monad.Effect
-
-#ifdef MTL
-import qualified Control.Monad.State.Class as S
-
-instance EffectState s es => S.MonadState s (Effect es) where
-    get = get
-    put = put
-    state = state
-#endif
-
--- | An effect where a state value is threaded throughout the computation.
-newtype State s a = State (s -> (a, s))
-  deriving Functor
-
-type EffectState s es = (Member (State s) es, s ~ StateType es)
-type family StateType es where
-    StateType (State s ': es) = s
-    StateType (e ': es) = StateType es
-
--- | Gets the current state.
-get :: EffectState s es => Effect es s
-get = state $ \s -> (s, s)
-
--- | Gets a value that is a function of the current state.
-gets :: EffectState s es => (s -> a) -> Effect es a
-gets f = f <$> get
-
--- | Replaces the current state.
-put :: EffectState s es => s -> Effect es ()
-put x = state $ const ((), x)
-
--- | Applies a pure modifier to the state value.
-modify :: EffectState s es => (s -> s) -> Effect es ()
-modify f = get >>= put . f
-
--- | Applies a pure modifier to the state value.
--- The modified value is converted to weak head normal form.
-modify' :: EffectState s es => (s -> s) -> Effect es ()
-modify' f = do
-    x <- get
-    put $! f x
-
--- | Lifts a stateful computation to the `Effect` monad.
-state :: EffectState s es => (s -> (a, s)) -> Effect es a
-state = send . State
-
--- | Runs a computation with a modified state value.
---
--- prop> withState f x = modify f >> x
-withState :: EffectState s es => (s -> s) -> Effect es a -> Effect es a
-withState f x = modify f >> x
-
--- | Completely handles a `State` effect by providing an
--- initial state, and making the final state explicit.
-runState :: s -> Effect (State s ': es) a -> Effect es (a, s)
-runState = flip $
-    handle (\x s -> return (x, s))
-    $ eliminate (\(State k) s -> let (k', s') = k s in k' s')
-    $ relay (\x s -> sendEffect $ fmap ($ s) x)
-
--- | Completely handles a `State` effect, and discards the final state.
-evalState :: s -> Effect (State s ': es) a -> Effect es a
-evalState s = fmap fst . runState s
-
--- | Completely handles a `State` effect, and discards the final value.
-execState :: s -> Effect (State s ': es) a -> Effect es s
-execState s = fmap snd . runState s
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.State (
+    EffectState, State, runState,
+    evalState, execState,
+    get, gets, put,
+    modify, modify',
+    state, withState
+) where
+
+import Control.Applicative ((<$>))
+import Control.Monad.Effect
+
+#ifdef MTL
+import qualified Control.Monad.State.Class as S
+import Data.Type.Row
+
+instance (Member (State s) l, State s ~ InstanceOf State l) => S.MonadState s (Effect l) where
+    get = get
+    put = put
+    state = state
+#endif
+
+-- | An effect where a state value is threaded throughout the computation.
+newtype State s a = State (s -> (a, s))
+  deriving Functor
+
+type instance Is State f = IsState f
+
+type family IsState f where
+    IsState (State s) = True
+    IsState f = False
+
+class MemberEffect State (State s) l => EffectState s l
+instance MemberEffect State (State s) l => EffectState s l
+
+-- | Gets the current state.
+get :: EffectState s l => Effect l s
+get = state $ \s -> (s, s)
+
+-- | Gets a value that is a function of the current state.
+gets :: EffectState s l => (s -> a) -> Effect l a
+gets f = f <$> get
+
+-- | Replaces the current state.
+put :: EffectState s l => s -> Effect l ()
+put x = state $ const ((), x)
+
+-- | Applies a pure modifier to the state value.
+modify :: EffectState s l => (s -> s) -> Effect l ()
+modify f = get >>= put . f
+
+-- | Applies a pure modifier to the state value.
+-- The modified value is converted to weak head normal form.
+modify' :: EffectState s l => (s -> s) -> Effect l ()
+modify' f = do
+    x <- get
+    put $! f x
+
+-- | Lifts a stateful computation to the `Effect` monad.
+state :: EffectState s l => (s -> (a, s)) -> Effect l a
+state = send . State
+
+-- | Runs a computation with a modified state value.
+--
+-- prop> withState f x = modify f >> x
+withState :: EffectState s l => (s -> s) -> Effect l a -> Effect l a
+withState f x = modify f >> x
+
+-- | Completely handles a `State` effect by providing an
+-- initial state, and making the final state explicit.
+runState :: s -> Effect (State s :+ l) a -> Effect l (a, s)
+runState = flip $ eliminate
+    (\x s -> return (x, s))
+    (\(State k) s -> let (k', s') = k s in k' s')
+
+-- | Completely handles a `State` effect, and discards the final state.
+evalState :: s -> Effect (State s :+ l) a -> Effect l a
+evalState s = fmap fst . runState s
+
+-- | Completely handles a `State` effect, and discards the final value.
+execState :: s -> Effect (State s :+ l) a -> Effect l s
+execState s = fmap snd . runState s
diff --git a/src/Control/Effect/Thread.hs b/src/Control/Effect/Thread.hs
deleted file mode 100644
--- a/src/Control/Effect/Thread.hs
+++ /dev/null
@@ -1,105 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Effect.Thread (
-    EffectThread, Thread,
-    runMain, runSync, runAsync,
-    yield, fork, abort,
-) where
-
-import Control.Effect.Lift
-import Control.Monad.Effect
-import Control.Applicative ((<$>))
-import Control.Monad (void)
-import qualified Control.Concurrent as IO
-
--- | An effect that describes concurrent computation.
-data Thread a = Yield a | Fork a a | Abort
-  deriving Functor
-
-type EffectThread = Member Thread
-
--- | Yields to the next available thread.
-yield :: EffectThread es => Effect es ()
-yield = send (Yield ())
-
--- | Forks a child thread.
-fork :: EffectThread es => Effect es () -> Effect es ()
-fork child = sendEffect $ Fork child (return ())
-
--- | Immediately terminates the current thread.
-abort :: EffectThread es => Effect es ()
-abort = send Abort
-
--- | Executes a threaded computation synchronously.
--- Completes when the main thread exits.
-runMain :: Effect (Thread ': es) () -> Effect es ()
-runMain = run [] . toAST
-  where
-    run auxThreads thread = do
-        result <- thread
-        case result of
-            AbortAST -> return ()
-            YieldAST k -> do
-                auxThreads' <- runAll auxThreads
-                run auxThreads' k
-            ForkAST child parent -> do
-                auxThreads' <- runAll [child]
-                run (auxThreads ++ auxThreads') parent
-
-    runAll [] = return []
-    runAll (thread:xs) = do
-        result <- thread
-        case result of
-            AbortAST -> runAll xs
-            YieldAST k -> (k:) <$> runAll xs
-            ForkAST child parent -> (parent:) <$> runAll (child:xs)
-
--- | Executes a threaded computation synchronously.
--- Does not complete until all threads have exited.
-runSync :: Effect (Thread ': es) () -> Effect es ()
-runSync = run . (:[]) . toAST
-  where
-    run [] = return ()
-    run (thread:xs) = do
-        result <- thread
-        case result of
-            AbortAST -> run xs
-            YieldAST k -> run (xs ++ [k])
-            ForkAST child parent -> run (child:xs ++ [parent])
-
--- | Executes a threaded computation asynchronously.
-runAsync :: Effect '[Thread, Lift IO] () -> IO ()
-runAsync = run . toAST
-  where
-    run thread = do
-        result <- runLift thread
-        case result of
-            AbortAST -> return ()
-            YieldAST k -> do
-                IO.yield
-                run k
-            ForkAST child parent -> do
-                void $ IO.forkIO $ run child
-                run parent
-
-data ThreadAST es
-    = YieldAST (Effect es (ThreadAST es))
-    | ForkAST (Effect es (ThreadAST es)) (Effect es (ThreadAST es))
-    | AbortAST
-
--- Converts a threaded computation into its corresponding AST. This allows
--- different backends to interpret calls to fork/yield/abort as they please. See
--- the implementations of runAsync, runSync, and runMain.
-toAST :: Effect (Thread ': es) () -> Effect es (ThreadAST es)
-toAST =
-    handle (\() -> return AbortAST)
-    $ eliminate (\thread ->
-        case thread of
-            Abort -> return AbortAST
-            Yield k -> return (YieldAST k)
-            Fork child parent -> return (ForkAST child parent))
-    $ defaultRelay
diff --git a/src/Control/Effect/Union.hs b/src/Control/Effect/Union.hs
deleted file mode 100644
--- a/src/Control/Effect/Union.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Effect.Union (
-    EffectUnion, Union, runUnion, nest,
-    KnownList, type (++),
-) where
-
-import Control.Monad.Effect
-import Data.Union
-
-type EffectUnion es fs = (KnownList es, Member (Union es) fs, es ~ UnionType fs)
-type family UnionType fs where
-    UnionType (Union es ': fs) = es
-    UnionType (f ': fs) = UnionType fs
-
--- | Nests an effect with another.
-nest :: EffectUnion es fs => Effect es a -> Effect fs a
-nest =
-    handle return
-    $ relayUnion sendEffect
-
--- | Flattens a nested list of effects.
-runUnion :: KnownList es => Effect (Union es ': fs) a -> Effect (es ++ fs) a
-runUnion =
-    handle return
-    $ relayUnion (withUnion sendEffect . flatten)
-
-relayUnion :: (Union es b -> b) -> Handler es b
-relayUnion f = relay (f . inject)
diff --git a/src/Control/Effect/Witness.hs b/src/Control/Effect/Witness.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Witness.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Witness (
+    EffectWitness, Witness, runWitness,
+    Token, newToken
+) where
+
+import Control.Monad.Effect
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Data.Unique (Unique, newUnique)
+import System.IO.Unsafe (unsafePerformIO)
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | A unique identifier associated with a type @a@.
+-- If two tokens are equal, then so are their associated types.
+-- Use `testEquality` to safely cast between types.
+newtype Token s a = Token Unique
+  deriving Eq
+
+instance TestEquality (Token s) where
+    testEquality (Token i) (Token j)
+        | i == j = Just unsafeRefl
+        | otherwise = Nothing
+
+unsafeRefl :: a :~: b
+unsafeRefl = unsafeCoerce Refl
+
+-- | An effect describing the generation of unique identifiers.
+data Witness s a where
+    Witness :: (Token s b -> a) -> Witness s a
+
+instance Functor (Witness s) where
+    fmap f (Witness g) = Witness (f . g)
+
+type instance Is Witness f = IsWitness f
+
+type family IsWitness f where
+    IsWitness (Witness s) = True
+    IsWitness f = False
+
+class MemberEffect Witness (Witness s) l => EffectWitness s l
+instance MemberEffect Witness (Witness s) l => EffectWitness s l
+
+type family WitnessType l where
+    WitnessType (Witness s ': l) = s
+    WitnessType (e ': l) = WitnessType l
+
+-- | Generates a new, unique `Token`.
+newToken :: EffectWitness s l => Effect l (Token s a)
+newToken = send (Witness id)
+
+-- | Completely handles a `Witness` effect. The Rank-2 quantifier ensures that
+-- unique identifiers cannot escape the context in which they were created.
+runWitness :: (forall s. Effect (Witness s :+ l) a) -> Effect l a
+runWitness effect = run effect
+  where
+    run = eliminate return $ \(Witness k) ->
+        k $ Token $ unsafePerformIO newUnique
diff --git a/src/Control/Effect/Writer.hs b/src/Control/Effect/Writer.hs
--- a/src/Control/Effect/Writer.hs
+++ b/src/Control/Effect/Writer.hs
@@ -1,93 +1,95 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-#if MTL
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-#endif
-
-module Control.Effect.Writer (
-    EffectWriter, Writer, runWriter,
-    tell, listen, listens, pass, censor
-) where
-
-import Control.Monad.Effect
-import Control.Applicative ((<$>))
-import Control.Arrow (second)
-import Data.Monoid (Monoid (..))
-
-#ifdef MTL
-import qualified Control.Monad.Writer.Class as W
-
-instance EffectWriter e es => W.MonadWriter e (Effect es) where
-    tell = tell
-    listen = listen
-    pass = pass
-#endif
-
--- | An effect that allows accumulating output.
-data Writer w a = Writer w a
-  deriving Functor
-
-type EffectWriter w es = (Monoid w, Member (Writer w) es, w ~ WriterType es)
-type family WriterType es where
-    WriterType (Writer w ': es) = w
-    WriterType (t ': es) = WriterType es
-
--- | Writes a value to the output.
-tell :: EffectWriter w es => w -> Effect es ()
-tell x = send (Writer x ())
-
--- | Executes a computation, and obtains the writer output.
--- The writer output of the inner computation is still
--- written to the writer output of the outer computation.
-listen :: EffectWriter w es => Effect es a -> Effect es (a, w)
-listen effect = do
-    value@(_, output) <- run effect
-    tell output
-    return value
-  where
-    run =
-        handle point
-        $ intercept bind
-        $ defaultRelay
-
--- | Like `listen`, but the writer output is run through a function.
-listens :: EffectWriter w es => (w -> b) -> Effect es a -> Effect es (a, b)
-listens f = fmap (second f) . listen
-
--- | Runs a computation that returns a value and a function,
--- applies the function to the writer output, and then returns the value.
-pass :: EffectWriter w es => Effect es (a, w -> w) -> Effect es a
-pass effect = do
-    ((x, f), l) <- listen effect
-    tell (f l)
-    return x
-
--- | Applies a function to the writer output of a computation.
-censor :: EffectWriter w es => (w -> w) -> Effect es a -> Effect es a
-censor f effect = pass $ do
-    a <- effect
-    return (a, f)
-
--- | Completely handles a writer effect. The writer value must be a `Monoid`.
--- `mempty` is used as an initial value, and `mappend` is used to combine values.
--- Returns the result of the computation and the final output value.
-runWriter :: Monoid w => Effect (Writer w ': es) a -> Effect es (a, w)
-runWriter =
-    handle point
-    $ eliminate bind
-    $ defaultRelay
-
-point :: Monoid w => a -> Effect es (a, w)
-point x = return (x, mempty)
-
-bind :: Monoid w => Writer w (Effect es (b, w)) -> Effect es (b, w)
-bind (Writer l k) = second (mappend l) <$> k
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Writer (
+    EffectWriter, Writer, runWriter,
+    tell, listen, listens, pass, censor,
+    stateWriter
+) where
+
+import Control.Monad.Effect
+import Control.Applicative ((<$>))
+import Control.Arrow (second)
+import Data.Monoid (Monoid (..))
+import Control.Effect.State
+
+#ifdef MTL
+import Data.Type.Row
+import qualified Control.Monad.Writer.Class as W
+
+instance (Monoid w, Member (Writer w) l, Writer w ~ InstanceOf Writer l) => W.MonadWriter w (Effect l) where
+    tell = tell
+    listen = listen
+    pass = pass
+#endif
+
+-- | An effect that allows accumulating output.
+data Writer w a = Writer w a
+  deriving Functor
+
+type instance Is Writer f = IsWriter f
+
+type family IsWriter f where
+    IsWriter (Writer w) = True
+    IsWriter f = False
+
+class (Monoid w, MemberEffect Writer (Writer w) l) => EffectWriter w l
+instance (Monoid w, MemberEffect Writer (Writer w) l) => EffectWriter w l
+
+-- | Writes a value to the output.
+tell :: EffectWriter w l => w -> Effect l ()
+tell x = send (Writer x ())
+
+-- | Executes a computation, and obtains the writer output.
+-- The writer output of the inner computation is still
+-- written to the writer output of the outer computation.
+listen :: EffectWriter w l => Effect l a -> Effect l (a, w)
+listen effect = do
+    value@(_, output) <- intercept point bind effect
+    tell output
+    return value
+
+-- | Like `listen`, but the writer output is run through a function.
+listens :: EffectWriter w l => (w -> b) -> Effect l a -> Effect l (a, b)
+listens f = fmap (second f) . listen
+
+-- | Runs a computation that returns a value and a function,
+-- applies the function to the writer output, and then returns the value.
+pass :: EffectWriter w l => Effect l (a, w -> w) -> Effect l a
+pass effect = do
+    ((x, f), l) <- listen effect
+    tell (f l)
+    return x
+
+-- | Applies a function to the writer output of a computation.
+censor :: EffectWriter w l => (w -> w) -> Effect l a -> Effect l a
+censor f effect = pass $ do
+    a <- effect
+    return (a, f)
+
+-- | Executes a writer computation which sends its output to a state effect.
+stateWriter :: (Monoid s, EffectState s l) => Effect (Writer s :+ l) a -> Effect l a
+stateWriter = eliminate return (\(Writer l x) -> modify (mappend l) >> x)
+
+-- | Completely handles a writer effect. The writer value must be a `Monoid`.
+-- `mempty` is used as an initial value, and `mappend` is used to combine values.
+-- Returns the result of the computation and the final output value.
+runWriter :: Monoid w => Effect (Writer w :+ l) a -> Effect l (a, w)
+runWriter = eliminate point bind
+
+point :: Monoid w => a -> Effect l (a, w)
+point x = return (x, mempty)
+
+bind :: Monoid w => Writer w (Effect l (b, w)) -> Effect l (b, w)
+bind (Writer l k) = second (mappend l) <$> k
diff --git a/src/Control/Monad/Effect.hs b/src/Control/Monad/Effect.hs
--- a/src/Control/Monad/Effect.hs
+++ b/src/Control/Monad/Effect.hs
@@ -1,128 +1,200 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
--- | This module provides three things:
---
--- 1. An `Effect` monad for representing effectful computations,
--- 2. A DSL for effect handling that lets you cleanly handle an arbitrary number of effects, and
--- 3. A type-level list membership constraint.
 module Control.Monad.Effect (
     -- * The Effect Monad
-    Effect,
-    runEffect, send, sendEffect,
+    Effect, runEffect,
+    send, sendEffect,
 
     -- * Effect Handlers
-    -- | The following types and functions form a small DSL that allows users to
-    -- specify how to handle effects. A handler can be formed by a call to
-    -- `handle`, followed by a chain of calls to `eliminate`, `intercept`, and
-    -- ended by either a `defaultRelay`, `emptyRelay`, or a call to `relay`.
-    --
-    -- For example, a possible handler for the state effect would be:
-    --
-    -- > data State s a = State (s -> (s, a))
-    -- >
-    -- > runState :: Effect (State s ': es) a -> s -> Effect es (s, a)
-    -- > runState =
-    -- >     handle (\output state -> return (state, output))
-    -- >     $ eliminate (\(State transform) state ->
-    -- >         let (state', continue) = transform state
-    -- >         in continue state')
-    -- >     $ relay (\effect state -> do
-    -- >         continue <- sendEffect effect
-    -- >         return (continue state))
-    --
-    -- As an analogy to monads, `handle` lets you specify the return function,
-    -- while `eliminate`, `intercept`, and `relay`, let you specify the bind
-    -- function.
-    Handler, handle,
+    Effectful (EffectsOf),
+
     eliminate, intercept,
-    relay, defaultRelay, emptyRelay,
+    extend, enable,
+    conceal, reveal, rename,
+    swap, rotate,
+    mask, unmask,
 
+    -- * Unions
+    Union, flatten, unflatten,
+
     -- * Membership
-    Member
+    Member, MemberEffect, Is,
+
+    -- * Effect Rows
+    Row (..), type (:++),
+    KnownLength, Inclusive
 ) where
 
-import Data.Union
+import Data.Union (Union)
+import qualified Data.Union as Union
+
+import Data.Type.Row
+
 import Control.Applicative (Applicative (..), (<$>))
 import Control.Monad (join)
 
--- | An effectful computation. An @Effect es a@ may perform any of the effects
--- specified by the list of effects @es@ before returning a result of type @a@.
+-- | An effectful computation. An @Effect l a@ may perform any of the effects
+-- specified by the list of effects @l@ before returning a result of type @a@.
 -- The definition is isomorphic to the following GADT:
 --
--- > data Effect es a where
--- >     Done :: a -> Effect es a
--- >     Side :: `Union` es (Effect es a) -> Effect es a
-data Effect es a = Effect {
-    unEffect :: forall r. (a -> r) -> (Union es r -> r) -> r
-} deriving Functor
+-- @
+-- data Effect l a where
+--     Done :: a -> Effect l a
+--     Side :: `Union` l (Effect l a) -> Effect l a
+-- @
+newtype Effect l a = Effect (forall r. (a -> r) -> (Union l r -> r) -> r)
 
-instance Applicative (Effect es) where
-    pure x = Effect $ \p _ -> p x
-    Effect f <*> Effect x = Effect $ \p b ->
-        f (\f' -> x (p . f') b) b
+unEffect :: (a -> r) -> (Union l r -> r) -> Effect l a -> r
+unEffect point bind (Effect f) = f point bind
 
-instance Monad (Effect es) where
+instance Functor (Effect l) where
+    fmap f (Effect g) = Effect $ \point -> g (point . f)
+
+instance Applicative (Effect l) where
+    pure x = Effect $ \point _ -> point x
+    Effect f <*> Effect x = Effect $ \point bind ->
+        f (\f' -> x (point . f') bind) bind
+
+instance Monad (Effect l) where
     return = pure
-    Effect x >>= f = Effect $ \p b ->
-        x (\x' -> unEffect (f x') p b) b
+    Effect f >>= g = Effect $ \point bind ->
+        f (unEffect point bind . g) bind
 
 -- | Converts an computation that produces no effects into a regular value.
-runEffect :: Effect '[] a -> a
-runEffect (Effect f) = f id absurdUnion
+runEffect :: Effect Nil a -> a
+runEffect (Effect f) = f id Union.absurd
 
--- | Executes an effect of type @e@ that produces a return value of type @a@.
-send :: Member e es => e a -> Effect es a
-send x = Effect $ \point bind -> bind $ inject $ point <$> x
+-- | Executes an effect of type @f@ that produces a return value of type @a@.
+send :: (Functor f, Member f l) => f a -> Effect l a
+send x = Effect $ \point bind -> bind $ point <$> Union.inject x -- Inlined for efficiency (from relay).
 
--- | Executes an effect of type @e@ that produces a return value of type @a@.
-sendEffect :: Member e es => e (Effect es a) -> Effect es a
-sendEffect = join . send
+-- | Executes an effect of type @f@ that produces a return value of type @r@.
+-- Note that a specific instance of this function is of type
+-- @(Functor f, Member f l) => f (Effect l a) -> Effect l a@, which allows users
+-- to send effects parameterized by effects.
+sendEffect :: (Functor f, Member f l, Effectful l r) => f r -> r
+sendEffect = relay . Union.inject
 
--- | A handler for an effectful computation.
--- Combined with 'handle', allows one to convert a computation
--- parameterized by the effect list @es@ to a value of type @a@.
-data Handler es a = Handler (Union es a -> a)
+-- | The class of types which result in an effect. That is:
+--
+-- > Effect l r
+-- > a -> Effect l r
+-- > a -> b -> Effect l r
+-- > ...
+class l ~ EffectsOf r => Effectful l r where
+    -- | Determines the effects associated with the return type of a function.
+    type family EffectsOf r :: Row (* -> *)
 
--- | @handle p h@ transforms an effect into a value of type @b@.
+    relay :: Union l r -> r
+
+    -- Prevents the `Minimal Complete Definition` box from showing.
+    relay = undefined
+
+instance Effectful l (Effect l a) where
+    type EffectsOf (Effect l a) = l
+    relay u = join $ Effect $ \point bind -> bind $ point <$> u
+
+instance Effectful l r => Effectful l (a -> r) where
+    type EffectsOf (a -> r) = EffectsOf r
+    relay u x = relay (fmap ($ x) u)
+
+-- | Handles an effect without eliminating it. The given function is passed an
+-- effect value parameterized by the output type (i.e. the return type of
+-- `handle`).
 --
--- @p@ specifies how to convert pure values. That is,
+-- The most common instantiation of this function is:
 --
--- prop> handle p h (return x) = p x
+-- > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect l a -> Effect l b
+intercept :: (Effectful l r, Member f l) => (a -> r) -> (f r -> r) -> Effect l a -> r
+intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)
+
+-- | Completely handles an effect. The given function is passed an effect value
+-- parameterized by the output type (i.e. the return type of `handle`).
 --
--- @h@ specifies how to handle effects.
-handle :: (a -> b) -> Handler es b -> Effect es a -> b
-handle point (Handler bind) (Effect f) = f point bind
+-- The most common instantiation of this function is:
+--
+-- > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect (f ': l) a -> Effect l b
+eliminate :: Effectful l r => (a -> r) -> (f r -> r) -> Effect (f :+ l) a -> r
+eliminate point bind = unEffect point (either bind relay . Union.pop)
 
--- | Provides a way to completely handle an effect. The given function is passed
--- an effect value parameterized by the output type (i.e. the return type of
--- `handle`).
-eliminate :: (e b -> b) -> Handler es b -> Handler (e ': es) b
-eliminate bind (Handler pass) = Handler (either pass bind . reduce)
+-- | Adds an arbitrary effect to the head of the effect list.
+extend :: Effect l a -> Effect (f :+ l) a
+extend = translate Union.push
 
--- | Provides a way to handle an effect without eliminating it. The given
--- function is passed an effect value parameterized by the output type (i.e. the
--- return type of `handle`).
-intercept :: Member e es => (e b -> b) -> Handler es b -> Handler es b
-intercept bind (Handler pass) = Handler $ \u ->
-    maybe (pass u) bind (project u)
+-- | Enables an effect that was previously disabled.
+enable :: Effect (f :- l) a -> Effect l a
+enable = translate Union.enable
 
--- | Computes a basis handler. Provides a way to pass on effects of unknown
--- types. In most cases, `defaultRelay` is sufficient.
-relay :: (forall e. Member e es => e b -> b) -> Handler es b
-relay f = Handler (withUnion f)
+-- | Hides an effect @g@ by translating each instance of @g@ into an instance of
+-- another effect @f@.
+conceal :: Member f l => Effect (f :+ l) a -> Effect l a
+conceal = translate Union.conceal
 
--- | Relays all effects without examining them.
+-- | Hides an effect @g@ by translating each instance of another effect @f@ into
+-- an instance of @g@.
+reveal :: Member f l => Effect l a -> Effect (f :+ l) a
+reveal = translate Union.reveal
+
+-- | Translates the first effect in the effect list into another effect.
+rename :: Functor g => (forall r. f r -> g r) -> Effect (f :+ l) a -> Effect (g :+ l) a
+rename f = translate (either (Union.inject . f) Union.push . Union.pop)
+
+-- | Reorders the first two effects in a computation.
+swap :: Effect (f :+ g :+ l) a -> Effect (g :+ f :+ l) a
+swap = translate Union.swap
+
+-- | Rotates the first three effects in a computation.
+rotate :: Effect (f :+ g :+ h :+ l) a -> Effect (g :+ h :+ f :+ l) a
+rotate = translate Union.rotate
+
+-- | Distributes the sub-effects of a `Union` effect across a computation.
+flatten :: Inclusive l => Effect (Union l :+ m) a -> Effect (l :++ m) a
+flatten = translate Union.flatten
+
+-- | Collects some effects in a computation into a `Union` effect.
+unflatten :: KnownLength l => Effect (l :++ m) a -> Effect (Union l :+ m) a
+unflatten = translate Union.unflatten
+
+translate :: (forall r. Union l r -> Union m r) -> Effect l a -> Effect m a
+translate f = unEffect return (relay . f)
+
+-- | Converts a set of effects @l@ into a single effect @f@.
 --
--- prop> handle id defaultRelay x = x
-defaultRelay :: Handler es (Effect es a)
-defaultRelay = relay sendEffect
+-- @ mask f = `conceal` . `rename` f . `unflatten` @
+mask :: (Functor f, KnownLength l, Member f m) => (forall r. Union l r -> f r) -> Effect (l :++ m) a -> Effect m a
+mask f = conceal . rename f . unflatten
 
--- | A handler for when there are no effects. Since `Handler`s handle effects,
--- they cannot be run on a computation that never produces an effect. By the
--- principle of explosion, a handler that requires exactly zero effects can
--- produce any value.
-emptyRelay :: Handler '[] a
-emptyRelay = Handler absurdUnion
+-- | Converts an effect @f@ into a set of effects @l@.
+--
+-- @ unmask f = `flatten` . `rename` f . `reveal` @
+unmask :: (Functor f, Inclusive l, Member f m) => (forall r. f r -> Union l r) -> Effect m a -> Effect (l :++ m) a
+unmask f = flatten . rename f . reveal
+
+-- | A refined `Member`ship constraint that can infer @f@ from @l@, given
+-- @name@. In order for this to be used, @`Is` name f@ must be defined.
+-- For example:
+--
+-- > data Reader r a = ...
+-- >
+-- > type instance Is Reader f = IsReader f
+-- >
+-- > type IsReader f where
+-- >     IsReader (Reader r) = True
+-- >     IsReader f = False
+-- >
+-- > type ReaderEffect r l = MemberEffect Reader (Reader r) l
+-- >
+-- > ask :: ReaderEffect r l => Effect l r
+-- > ask = ...
+--
+-- Given the constraint @ReaderEffect r l@ in the above example, @r@ can be
+-- inferred from @l@.
+class (Member f l, f ~ InstanceOf name l) => MemberEffect name f l
+instance (Member f l, f ~ InstanceOf name l) => MemberEffect name f l
diff --git a/src/Data/Index.hs b/src/Data/Index.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Index.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Index (
+    Index,
+    zero, index,
+    absurd, trivial,
+    swap, rotate,
+    push, pop,
+    disable, enable,
+    conceal, reveal,
+    prepend, append, split
+) where
+
+import Data.Type.Row
+import Data.Type.Nat
+
+import Data.Proxy (Proxy (..))
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Unsafe.Coerce (unsafeCoerce)
+
+newtype Index (l :: Row k) (e :: k) = Index Integer
+  deriving Show
+
+instance TestEquality (Index l) where
+    testEquality (Index i) (Index j)
+        | i == j = Just (unsafeCoerce Refl)
+        | otherwise = Nothing
+
+zero :: Index (e :+ l) e
+zero = Index 0
+
+index :: forall e l. Member e l => Index l e
+index = Index $ natVal (Proxy :: Proxy (IndexOf e l))
+
+absurd :: Index Nil e -> a
+absurd (Index i) = i `seq` error "absurd Index"
+
+trivial :: Index (e :+ Nil) f -> f :~: e
+trivial (Index i)
+    | i == 0 = unsafeCoerce Refl
+    | otherwise = error "non-trivial Index"
+
+size :: forall l proxy. KnownLength l => proxy l -> Integer
+size _ = natVal (Proxy :: Proxy (Length l))
+
+push :: Index l e -> Index (f :+ l) e
+push (Index i) = Index (i + 1)
+
+pop :: Index (f :+ l) e -> Index l e
+pop (Index i) = Index (i - 1)
+
+disable :: Index l e -> Index (f :- l) e
+disable (Index i) = Index (i + 1)
+
+enable :: Index (f :- l) e -> Index l e
+enable (Index i) = Index (i - 1)
+
+conceal :: forall e f l. Member f l => Index (f :+ l) e -> Index l e
+conceal (Index i)
+    | i == 0 = Index j
+    | otherwise = Index (i - 1)
+  where
+    Index j = index :: Index l f
+
+reveal :: forall e f l. Member f l => Index l e -> Index (f :+ l) e
+reveal (Index i)
+    | i == j = Index 0
+    | otherwise = Index (i + 1)
+  where
+    Index j = index :: Index l f
+
+swap :: Index (e :+ f :+ l) g -> Index (f :+ e :+ l) g
+swap (Index i)
+    | i == 0 = Index 1
+    | i == 1 = Index 0
+    | otherwise = Index i
+
+rotate :: Index (e :+ f :+ g :+ l) h -> Index (f :+ g :+ e :+ l) h
+rotate (Index i)
+    | i == 0 = Index 2
+    | i == 1 = Index 1
+    | i == 2 = Index 0
+    | otherwise = Index i
+
+prepend :: KnownLength l => proxy l -> Index m e -> Index (l :++ m) e
+prepend p (Index i) = Index (i + size p)
+
+append :: Index l e -> proxy m -> Index (l :++ m) e
+append (Index i) _ = Index i
+
+split :: forall e l m. KnownLength l => Index (l :++ m) e -> Either (Index l e) (Index m e)
+split (Index i)
+    | i < n = Left (Index i)
+    | otherwise = Right (Index (i - 1))
+  where
+    n = size (Proxy :: Proxy l)
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.Type.Nat (
+    Nat (..), KnownNat (..)
+) where
+
+import Data.Proxy (Proxy (..))
+
+data Nat = Zero | Succ Nat
+
+class KnownNat (n :: Nat) where
+    natVal :: proxy n -> Integer
+
+instance KnownNat Zero where
+    natVal _ = 0
+
+instance KnownNat n => KnownNat (Succ n) where
+    natVal _ = 1 + natVal (Proxy :: Proxy n)
diff --git a/src/Data/Type/Row.hs b/src/Data/Type/Row.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Row.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Type.Row (
+    Row (..), (:++),
+    Length, KnownLength,
+    IndexOf, Member,
+    Inclusive,
+    Is, InstanceOf
+) where
+
+import Data.Type.Nat
+import Data.Type.Bool (If)
+
+infixr 5 :+, :-, :++
+
+-- | A type level list with explicit removals.
+data Row a
+    = Nil        -- ^ The empty list.
+    | a :+ Row a -- ^ Prepends an element (cons).
+    | a :- Row a -- ^ Deletes the first instance an element.
+
+-- | Appends two type level `Row`s.
+type family l :++ m where
+    Nil :++ l = l
+    (e :+ l) :++ m = e :+ l :++ m
+    (e :- l) :++ m = e :- l :++ m
+
+-- | Returns the length of the `Row` @l@.
+type family Length l where
+    Length Nil = Zero
+    Length (h :+ t) = Succ (Length t)
+    Length (h :- t) = Succ (Length t)
+
+-- | The class of `Row`s with statically known lengths.
+class KnownNat (Length l) => KnownLength l
+instance KnownNat (Length l) => KnownLength l
+
+-- | Returns the index of the first instance of @e@ in the `Row` @l@.
+type IndexOf e l = NthIndexOf Zero e l
+
+type family NthIndexOf n e l where
+    NthIndexOf Zero     e (e :+ l) = Zero
+    NthIndexOf (Succ n) e (e :+ l) = Succ (NthIndexOf n e l)
+    NthIndexOf n        e (f :+ l) = Succ (NthIndexOf n e l)
+    NthIndexOf n        e (e :- l) = Succ (NthIndexOf (Succ n) e l)
+    NthIndexOf n        e (f :- l) = Succ (NthIndexOf n e l)
+
+-- | A constraint specifying that @e@ is a member of the `Row` @l@.
+class KnownNat (IndexOf e l) => Member e l
+instance KnownNat (IndexOf e l) => Member e l
+
+-- | The class of `Row`s that do not contain deletions (`:-`).
+class KnownLength l => Inclusive l
+instance Inclusive Nil
+instance Inclusive l => Inclusive (e :+ l)
+
+-- | Returns a boolean value indicating whether @f@ belongs to the group of
+-- effects identified by @name@. This allows `MemberEffect` to infer the
+-- associated types for arbitrary effects.
+type family Is (name :: k) (f :: * -> *) :: Bool
+
+type InstanceOf name l = InstanceOfNone name '[] l
+
+-- Any instance of name in l but not in ex.
+type family InstanceOfNone name ex l where
+    InstanceOfNone name ex (f :- l) = InstanceOfNone name (f ': ex) l
+    InstanceOfNone name ex (f :+ l) =
+        If (Is name f)
+            (If (Elem f ex) (InstanceOfNone name (Remove f ex) l) f)
+            (InstanceOfNone name ex l)
+
+type family Elem e l where
+    Elem e '[] = False
+    Elem e (e ': l) = True
+    Elem e (f ': l) = Elem e l
+
+type family Remove e l where
+    Remove e (e ': l) = l
+    Remove e (f ': l) = f ': Remove e l
diff --git a/src/Data/Union.hs b/src/Data/Union.hs
--- a/src/Data/Union.hs
+++ b/src/Data/Union.hs
@@ -1,119 +1,92 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 module Data.Union (
-    Union, Member,
+    Union, absurd,
+    wrap, unwrap,
     inject, project,
-    reduce, flatten,
-    withUnion, absurdUnion,
-
-    KnownList, type (++)
+    swap, rotate,
+    push, pop,
+    enable, disable,
+    conceal, reveal,
+    flatten, unflatten
 ) where
 
-import Data.Proxy (Proxy (..))
-import Unsafe.Coerce (unsafeCoerce)
+import Data.Index (Index)
+import qualified Data.Index as Index
 
--- Union -----------------------------------------------------------------------
+import Data.Type.Row
+import Data.Proxy (Proxy (..))
+import Data.Type.Equality ((:~:) (..), apply, castWith, gcastWith, testEquality)
 
--- | Represents a union of the list of type constructors in @es@ parameterized
+-- | Represents a union of the list of type constructors in @l@ parameterized
 -- by @a@. As an effect, it represents the union of each type constructor's
--- corresponding effect.
-data Union es a where
-    Union :: Functor e => Index e es -> e a -> Union es a
+-- corresponding effect. From the user's perspective, it provides a way to
+-- encapsulate multiple effects.
+data Union l a where
+    Union :: Functor f => Index l f -> f a -> Union l a
 
-instance Functor (Union es) where
+instance Functor (Union l) where
     fmap f (Union i x) = Union i (fmap f x)
 
-inject :: Member e es => e a -> Union es a
-inject = Union index
-
-project :: forall a e es. Member e es => Union es a -> Maybe (e a)
-project (Union (Index i) x)
-    | i == j = Just (unsafeCoerce x)
-    | otherwise = Nothing
-  where
-    Index j = index :: Index e es
-
-reduce :: Union (e ': es) a -> Either (Union es a) (e a)
-reduce (Union (Index 0) x) = Right (unsafeCoerce x)
-reduce (Union (Index n) x) = Left (Union (Index (n - 1)) x)
-
-flatten :: KnownList es => Union (Union es ': fs) a -> Union (es ++ fs) a
-flatten = flatten' size . reduce
-  where
-    flatten' :: Size es -> Either (Union fs a) (Union es a) -> Union (es ++ fs) a
-    flatten' _ (Right (Union (Index i) x)) = Union (Index i) x
-    flatten' (Size n) (Left (Union (Index i) x)) = Union (Index (n + i)) x
-
-withUnion :: (forall e. Member e es => e a -> r) -> Union es a -> r
-withUnion f (Union i x) = withIndex (f x) (\Proxy -> i)
-
-absurdUnion :: Union '[] a -> b
-absurdUnion _ = error "absurdUnion"
-
--- Membership ------------------------------------------------------------------
-
--- | A constraint that requires that the type constructor @t :: * -> *@ is a
--- member of the list of types @ts :: [* -> *]@.
-class (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where
-    index :: Index t ts
+absurd :: Union Nil a -> b
+absurd (Union i _) = Index.absurd i
 
-instance (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where
-    index = index' (Proxy :: Proxy (IndexOf t ts))
+wrap :: Functor f => f a -> Union (f :+ l) a
+wrap = inject
 
-class Member' e es (n :: N) where
-    index' :: Proxy n -> Index e es
+unwrap :: Union (f :+ Nil) a -> f a
+unwrap (Union i x) = gcastWith (Index.trivial i) x
 
-instance Member' e (e ': es) Z where
-    index' _ = Index 0
+inject :: (Functor f, Member f l) => f a -> Union l a
+inject = Union Index.index
 
-instance (Member' e es n, IndexOf e (f ': es) ~ S n) => Member' e (f ': es) (S n) where
-    index' p = incr (index' (decr p))
-      where
-        incr :: Index e es -> Index e (f ': es)
-        incr (Index i) = Index (i + 1)
+project :: Member f l => Union l a -> Maybe (f a)
+project (Union i x) = fmap (\refl -> castWith (apply refl Refl) x) mRefl
+  where
+    mRefl = testEquality i Index.index
 
-        decr :: Proxy (S n) -> Proxy n
-        decr Proxy = Proxy
+swap :: Union (f :+ g :+ l) a -> Union (g :+ f :+ l) a
+swap (Union i x) = Union (Index.swap i) x
 
-newtype Index (e :: * -> *) (es :: [* -> *]) = Index Integer
+rotate :: Union (f :+ g :+ h :+ l) a -> Union (g :+ h :+ f :+ l) a
+rotate (Union i x) = Union (Index.rotate i) x
 
-withIndex :: (Member' e es (IndexOf e es) => r) -> (Proxy (IndexOf e es) -> Index e es) -> r
-withIndex = unsafeCoerce
+push :: Union l a -> Union (f :+ l) a
+push (Union i x) = Union (Index.push i) x
 
--- Type Level Indices ----------------------------------------------------------
-data N = Z | S N
+pop :: Union (f :+ l) a -> Either (f a) (Union l a)
+pop u@(Union i x) =
+    case project u of
+        Just r -> Left r
+        Nothing -> Right (Union (Index.pop i) x)
 
-type family IndexOf (t :: * -> *) ts where
-    IndexOf t (t ': ts) = Z
-    IndexOf t (u ': ts) = S (IndexOf t ts)
+enable :: Union (f :- l) a -> Union l a
+enable (Union i x) = Union (Index.enable i) x
 
--- Type Level Lists ------------------------------------------------------------
-newtype Size (es :: [* -> *]) = Size Integer
+disable :: Member f l => Union l a -> Either (f a) (Union (f :- l) a)
+disable u@(Union i x) =
+    case project u of
+        Just r -> Left r
+        Nothing -> Right (Union (Index.disable i) x)
 
--- | A 'known list' is a type level list who's size is known at compile time.
-class KnownList es where
-    size :: Size es
+conceal :: Member f l => Union (f :+ l) a -> Union l a
+conceal (Union i x) = Union (Index.conceal i) x
 
-instance KnownList '[] where
-    size = Size 0
+reveal :: Member f l => Union l a -> Union (f :+ l) a
+reveal (Union i x) = Union (Index.reveal i) x
 
-instance KnownList es => KnownList (e ': es) where
-    size = incr size
-      where
-        incr :: Size es -> Size (e ': es)
-        incr (Size n) = Size (n + 1)
+flatten :: Inclusive l => Union (Union l :+ m) a -> Union (l :++ m) a
+flatten = flatten' Proxy Proxy . pop
+  where
+    flatten' :: KnownLength l => proxy l -> proxy m -> Either (Union l a) (Union m a) -> Union (l :++ m) a
+    flatten' _ p (Left (Union i x)) = Union (Index.append i p) x
+    flatten' p _ (Right (Union i x)) = Union (Index.prepend p i) x
 
--- | Type level list append.
-type family es ++ fs :: [* -> *] where
-    '[] ++ fs = fs
-    (e ': es) ++ fs = e ': (es ++ fs)
+unflatten :: KnownLength l => Union (l :++ m) a -> Union (Union l :+ m) a
+unflatten (Union i x) =
+    case Index.split i of
+        Left j -> Union Index.zero (Union j x)
+        Right j -> Union (Index.push j) x