diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,30 +1,30 @@
-Copyright (c) 2014, Anthony Vandikas
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-    * Redistributions of source code must retain the above copyright
-      notice, this list of conditions and the following disclaimer.
-
-    * Redistributions in binary form must reproduce the above
-      copyright notice, this list of conditions and the following
-      disclaimer in the documentation and/or other materials provided
-      with the distribution.
-
-    * Neither the name of Anthony Vandikas nor the names of other
-      contributors may be used to endorse or promote products derived
-      from this software without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+Copyright (c) 2014, Anthony Vandikas
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Anthony Vandikas nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,2 @@
-import Distribution.Simple
-main = defaultMain
+import Distribution.Simple
+main = defaultMain
diff --git a/effin.cabal b/effin.cabal
--- a/effin.cabal
+++ b/effin.cabal
@@ -1,5 +1,5 @@
 name:                effin
-version:             0.2.1.3
+version:             0.3.0.3
 synopsis:            A Typeable-free implementation of extensible effects
 homepage:            https://github.com/YellPika/effin
 license:             BSD3
@@ -11,7 +11,7 @@
 build-type:          Simple
 cabal-version:       >=1.10
 description:
-  This package implements extensible effects, and alternative to monad
+  This package implements extensible effects, an alternative to monad
   transformers. The original paper can be found at
   <http://okmij.org/ftp/Haskell/extensible/exteff.pdf>. The main differences
   between this library and the one described in the paper are that this library
@@ -66,7 +66,7 @@
     Data.Type.Nat
     Data.Union
 
-  build-depends: base >= 4.7 && < 4.8
+  build-depends: base >= 4.7 && < 4.11
   if flag(mtl)
     build-depends: mtl >= 2.1 && < 3
 
diff --git a/src/Control/Effect/Bracket.hs b/src/Control/Effect/Bracket.hs
--- a/src/Control/Effect/Bracket.hs
+++ b/src/Control/Effect/Bracket.hs
@@ -14,7 +14,6 @@
     Handler, exceptAny, bracket, finally
 ) where
 
-import Control.Applicative ((<$>))
 import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
 import Data.Type.Equality ((:~:) (..), TestEquality (..))
 import Control.Effect.Witness
@@ -35,8 +34,8 @@
 type instance Is Bracket f = IsBracket f
 
 type family IsBracket f where
-    IsBracket (Bracket s) = True
-    IsBracket f = False
+    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
@@ -44,7 +43,7 @@
 -- | 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 = conceal $ Tag toString <$> rename BWitness newToken
+newTag toString = conceal $ fmap (Tag toString) (rename BWitness newToken)
 
 -- | Raises an exception of the specified class and value.
 raiseWith :: EffectBracket s l => Tag s b -> b -> Effect l a
@@ -66,7 +65,7 @@
 -- 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
+    let try (Handler j f) = fmap (\Refl -> f x) (testEquality i j)
         results = mapMaybe try handlers
     in fromMaybe (raiseWith i x) (listToMaybe results)
 
@@ -108,10 +107,10 @@
 
 -- | 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 :: (forall s. Effect (Bracket s ':+ l) a) -> Effect l a
 runBracket effect = runWitness (convert effect)
 
-convert :: Effect (Bracket s :+ l) a -> Effect (Witness s :+ l) a
+convert :: Effect (Bracket s ':+ l) a -> Effect (Witness s ':+ l) a
 convert =
     eliminate
         return
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
@@ -19,8 +19,8 @@
 type instance Is Coroutine f = IsCoroutine f
 
 type family IsCoroutine f where
-    IsCoroutine (Coroutine i o) = True
-    IsCoroutine f = False
+    IsCoroutine (Coroutine i o) = 'True
+    IsCoroutine f = 'False
 
 class MemberEffect Coroutine (Coroutine i o) l => EffectCoroutine i o l
 instance MemberEffect Coroutine (Coroutine i o) l => EffectCoroutine i o l
@@ -31,7 +31,7 @@
 suspend = send . Coroutine id
 
 -- | Converts a `Coroutine` effect into an `Iterator`.
-runCoroutine :: Effect (Coroutine i o :+ l) a -> Effect l (Iterator i o l a)
+runCoroutine :: Effect (Coroutine i o ':+ l) a -> Effect l (Iterator i o l a)
 runCoroutine = eliminate (return . Done) (\(Coroutine f x) k -> return (Next (k . f) x))
 
 -- | A suspended computation.
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
@@ -23,40 +23,37 @@
 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
+instance (EffectBracket s l, Member (Exception s e) l, Exception s 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)
+newtype Exception s e a = Exception (Tag s e -> a)
 
 type instance Is Exception f = IsException f
 
 type family IsException f where
-    IsException (Exception e) = True
-    IsException f = False
+    IsException (Exception s e) = 'True
+    IsException f = 'False
 
-class MemberEffect Exception (Exception e) l => EffectException e l
-instance MemberEffect Exception (Exception e) l => EffectException e l
+class (EffectBracket s l, MemberEffect Exception (Exception s e) l) => EffectException s e l
+instance (EffectBracket s l, MemberEffect Exception (Exception s e) l) => EffectException s e l
 
 -- | Raises an exception.
-raise :: EffectException e l => e -> Effect l a
-raise = send . Raise
+raise :: EffectException s e l => e -> Effect l a
+raise e = sendEffect (Exception (\tag -> raiseWith tag e))
 
 -- | 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)
+except :: EffectException s e l => Effect l a -> (e -> Effect l a) -> Effect l a
+except x f = sendEffect (Exception (\tag -> exceptWith tag x f))
 
 -- | Completely handles an exception effect.
-runException :: (EffectBracket s l, Show e) => Effect (Exception e :+ l) a -> Effect l (Either e a)
+runException :: (EffectBracket s l, Show e) => Effect (Exception s e ':+ l) a -> Effect l (Either e a)
 runException effect = do
     tag <- newTag show
     exceptWith tag
-        (eliminate (return . Right) (bind tag) effect)
+        (eliminate (return . Right) (\(Exception f) k -> k (f tag)) effect)
         (return . Left)
-  where
-    bind tag (Raise e) _ = raiseWith tag e
-    bind tag (Catch x f) k = exceptWith tag (k x) (k . 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
@@ -30,8 +30,8 @@
 type instance Is Lift f = IsLift f
 
 type family IsLift f where
-    IsLift (Lift m) = True
-    IsLift f = False
+    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
@@ -46,7 +46,7 @@
 
 -- | Converts a computation containing only monadic
 -- effects into a monadic computation.
-runLift :: Monad m => Effect (Lift m :+ Nil) a -> m a
+runLift :: Monad m => Effect (Lift m ':+ 'Nil) a -> m a
 runLift = runEffect . eliminate
     (return . return)
     (\(Lift m) k -> return $ m >>= runEffect . k)
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
@@ -16,7 +16,7 @@
 
 import Control.Monad.Effect
 import Control.Arrow (second)
-import Control.Applicative (Alternative (..), (<$>))
+import Control.Applicative (Alternative (..))
 import Control.Monad (MonadPlus (..), (<=<), join)
 
 -- | A nondeterminism (backtracking) effect.
@@ -25,8 +25,8 @@
 type instance Is List f = IsList f
 
 type family IsList f where
-    IsList List = True
-    IsList f = False
+    IsList List = 'True
+    IsList f = 'False
 
 class Member List l => EffectList l
 instance Member List l => EffectList l
@@ -45,8 +45,8 @@
 
 -- | Obtains all possible values from a computation
 -- parameterized by a nondeterminism effect.
-runList :: Effect (List :+ l) a -> Effect l [a]
-runList = eliminate (return . return) (\(List xs) k -> concat <$> mapM k xs)
+runList :: Effect (List ':+ l) a -> Effect l [a]
+runList = eliminate (return . return) (\(List xs) k -> fmap concat (mapM k xs))
 
 instance EffectList l => Alternative (Effect l) where
     empty = never
@@ -76,7 +76,7 @@
 
 -- | 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 :: 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
@@ -86,7 +86,7 @@
     -- 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 :: EffectList l => Effect (Cut ':+ l) a -> Effect l (Bool, [a])
     reifyCut =
         intercept return (\(List xs) k -> runAll (map k xs)) .
         eliminate
@@ -98,4 +98,4 @@
         (cutRequested, x') <- x
         if cutRequested
         then return (True, x')
-        else second (x' ++) <$> runAll xs
+        else fmap (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
@@ -20,7 +20,6 @@
 
 import Control.Effect.State
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 
 #ifdef MTL
 import Data.Type.Row
@@ -39,8 +38,8 @@
 type instance Is Reader f = IsReader f
 
 type family IsReader f where
-    IsReader (Reader r) = True
-    IsReader f = False
+    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
@@ -51,7 +50,7 @@
 
 -- | Retrieves a value that is a function of the current environment.
 asks :: EffectReader r l => (r -> a) -> Effect l a
-asks f = f <$> ask
+asks f = fmap f ask
 
 -- | Runs a computation with a modified environment.
 local :: EffectReader r l => (r -> r) -> Effect l a -> Effect l a
@@ -61,12 +60,12 @@
 
 -- | 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 :: EffectState s l => Effect (Reader s ':+ l) a -> Effect l a
 stateReader = eliminate return (\Ask k -> get >>= k)
 
 -- | 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 :: r -> Effect (Reader r ':+ l) a -> Effect l a
 runReader env = eliminate return (bind env)
 
 bind :: r -> Reader r a -> (a -> s) -> s
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
@@ -19,7 +19,6 @@
     state, withState
 ) where
 
-import Control.Applicative ((<$>))
 import Control.Monad.Effect
 
 #ifdef MTL
@@ -38,8 +37,8 @@
 type instance Is State f = IsState f
 
 type family IsState f where
-    IsState (State s) = True
-    IsState f = False
+    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
@@ -50,7 +49,7 @@
 
 -- | Gets a value that is a function of the current state.
 gets :: EffectState s l => (s -> a) -> Effect l a
-gets f = f <$> get
+gets f = fmap f get
 
 -- | Replaces the current state.
 put :: EffectState s l => s -> Effect l ()
@@ -79,15 +78,15 @@
 
 -- | 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 :: s -> Effect (State s ':+ l) a -> Effect l (a, s)
 runState = flip $ eliminate
     (\x s -> return (x, s))
     (\(State f) k s -> let (x, s') = f s in k x s')
 
 -- | Completely handles a `State` effect, and discards the final state.
-evalState :: s -> Effect (State s :+ l) a -> Effect l a
+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 -> 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
--- a/src/Control/Effect/Thread.hs
+++ b/src/Control/Effect/Thread.hs
@@ -12,7 +12,6 @@
 
 import Control.Effect.Lift
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 import Control.Monad (void)
 import qualified Control.Concurrent as IO
 
@@ -36,7 +35,7 @@
 
 -- | Executes a threaded computation synchronously.
 -- Completes when the main thread exits.
-runMain :: Effect (Thread :+ l) () -> Effect l ()
+runMain :: Effect (Thread ':+ l) () -> Effect l ()
 runMain = run [] . toAST
   where
     run auxThreads thread = do
@@ -55,12 +54,12 @@
         result <- thread
         case result of
             AbortAST -> runAll xs
-            YieldAST k -> (k:) <$> runAll xs
-            ForkAST child parent -> (parent:) <$> runAll (child:xs)
+            YieldAST k -> fmap (k:) (runAll xs)
+            ForkAST child parent -> fmap (parent:) (runAll (child:xs))
 
 -- | Executes a threaded computation synchronously.
 -- Does not complete until all threads have exited.
-runSync :: Effect (Thread :+ l) () -> Effect l ()
+runSync :: Effect (Thread ':+ l) () -> Effect l ()
 runSync = run . (:[]) . toAST
   where
     run [] = return ()
@@ -72,7 +71,7 @@
             ForkAST child parent -> run (child:xs ++ [parent])
 
 -- | Executes a threaded computation asynchronously.
-runAsync :: Effect (Thread :+ Lift IO :+ Nil) () -> IO ()
+runAsync :: Effect (Thread ':+ Lift IO ':+ 'Nil) () -> IO ()
 runAsync = run . toAST
   where
     run thread = do
@@ -94,7 +93,7 @@
 -- 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 :+ l) () -> Effect l (ThreadAST l)
+toAST :: Effect (Thread ':+ l) () -> Effect l (ThreadAST l)
 toAST = eliminate (\_ -> return AbortAST) bind
   where
     bind Abort _ = return AbortAST
diff --git a/src/Control/Effect/Witness.hs b/src/Control/Effect/Witness.hs
--- a/src/Control/Effect/Witness.hs
+++ b/src/Control/Effect/Witness.hs
@@ -40,8 +40,8 @@
 type instance Is Witness f = IsWitness f
 
 type family IsWitness f where
-    IsWitness (Witness s) = True
-    IsWitness f = False
+    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
@@ -56,7 +56,7 @@
 
 -- | 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 :: (forall s. Effect (Witness s ':+ l) a) -> Effect l a
 runWitness effect = run effect
   where
     run = eliminate return $ \NewToken k ->
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
@@ -19,9 +19,10 @@
 ) where
 
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 import Control.Arrow (second)
+#if !MIN_VERSION_base(4, 8, 0)
 import Data.Monoid (Monoid (..))
+#endif
 import Control.Effect.State
 
 #ifdef MTL
@@ -41,8 +42,8 @@
 type instance Is Writer f = IsWriter f
 
 type family IsWriter f where
-    IsWriter (Writer w) = True
-    IsWriter f = False
+    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
@@ -79,17 +80,17 @@
     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 :: (Monoid s, EffectState s l) => Effect (Writer s ':+ l) a -> Effect l a
 stateWriter = eliminate return (\(Tell l) k -> modify (mappend l) >> k ())
 
 -- | 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 :: 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 a -> (a -> Effect l (b, w)) -> Effect l (b, w)
-bind (Tell l) k = second (mappend l) <$> k ()
+bind (Tell l) k = second (mappend l) `fmap` 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,203 +1,206 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Monad.Effect (
-    -- * The Effect Monad
-    Effect, runEffect,
-    send, sendEffect,
-
-    -- * Effect Handlers
-    Effectful (EffectsOf),
-
-    eliminate, intercept,
-    extend, enable,
-    conceal, reveal, rename,
-    swap, rotate,
-    mask, unmask,
-
-    -- * Unions
-    Union, flatten, unflatten,
-
-    -- * Membership
-    Member, MemberEffect, Is,
-
-    -- * Effect Rows
-    Row (..), type (:++),
-    KnownLength, Inclusive
-) where
-
-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 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 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) -> (forall b. Union l b -> (b -> r) -> r) -> r)
-
-unEffect :: (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> Effect l a -> r
-unEffect point bind (Effect f) = f point bind
-
-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 f >>= g = Effect $ \point bind ->
-        f (unEffect point bind . g) bind
-
--- | Converts an computation that produces no effects into a regular value.
-runEffect :: Effect Nil a -> a
-runEffect (Effect f) = f id Union.absurd
-
--- | Executes an effect of type @f@ that produces a return value of type @a@.
-send :: Member f l => f a -> Effect l a
-send x = Effect $ \point bind -> bind (Union.inject x) point
-
--- | 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
--- @Member f l => f (Effect l a) -> Effect l a@, which allows users
--- to send effects parameterized by effects.
-sendEffect :: (Member f l, Effectful l r) => f r -> r
-sendEffect x = relay (Union.inject x) id
-
--- | 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 (* -> *)
-
-    relay :: Union l a -> (a -> 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 f = join $ Effect $ \point bind -> bind u (point . f)
-
-instance Effectful l r => Effectful l (a -> r) where
-    type EffectsOf (a -> r) = EffectsOf r
-    relay u f y = relay u (\x -> f x y)
-
--- | Handles an effect without eliminating it. The second function parameter is
--- passed an effect value and a continuation function.
---
--- The most common instantiation of this function is:
---
--- > (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) -> (forall b. f b -> (b -> r) -> r) -> Effect l a -> r
-intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)
-
--- | Completely handles an effect. The second function parameter is passed an
--- effect value and a continuation function.
---
--- 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) -> (forall b. f b -> (b -> r) -> r) -> Effect (f :+ l) a -> r
-eliminate point bind = unEffect point (either bind relay . Union.pop)
-
--- | Adds an arbitrary effect to the head of the effect list.
-extend :: Effect l a -> Effect (f :+ l) a
-extend = translate Union.push
-
--- | Enables an effect that was previously disabled.
-enable :: Effect (f :- l) a -> Effect l a
-enable = translate Union.enable
-
--- | Hides an effect @f@ by translating each instance of the effect into an
--- equivalent effect further into the effect list.
---
--- prop> conceal = eliminate return (\x k -> send x >>= k)
-conceal :: Member f l => Effect (f :+ l) a -> Effect l a
-conceal = translate Union.conceal
-
--- | Hides an effect @f@ by translating each instance of the effect into an
--- equivalent effect at the head of the effect list.
-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.
---
--- prop> rename f = eliminate return (\x k -> send (f x) >>= k) . swap . extend
-rename :: (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@.
---
--- @ mask f = `conceal` . `rename` f . `unflatten` @
-mask :: (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
-
--- | Converts an effect @f@ into a set of effects @l@.
---
--- @ unmask f = `flatten` . `rename` f . `reveal` @
-unmask :: (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
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Monad.Effect (
+    -- * The Effect Monad
+    Effect, runEffect,
+    send, sendEffect,
+
+    -- * Effect Handlers
+    Effectful (EffectsOf),
+
+    eliminate, intercept,
+    extend, enable,
+    conceal, reveal, rename,
+    swap, rotate,
+    mask, unmask,
+
+    -- * Unions
+    Union, flatten, unflatten,
+
+    -- * Membership
+    Member, MemberEffect, Is,
+
+    -- * Effect Rows
+    Row (..), type (:++),
+    KnownLength, Inclusive
+) where
+
+import Data.Union (Union)
+import qualified Data.Union as Union
+
+import Data.Type.Row
+
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative (Applicative (..))
+#endif
+import Control.Monad (join)
+
+-- | 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 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) -> (forall b. Union l b -> (b -> r) -> r) -> r)
+
+unEffect :: (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> Effect l a -> r
+unEffect point bind (Effect f) = f point bind
+
+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 f >>= g = Effect $ \point bind ->
+        f (unEffect point bind . g) bind
+
+-- | Converts an computation that produces no effects into a regular value.
+runEffect :: Effect 'Nil a -> a
+runEffect (Effect f) = f id Union.absurd
+
+-- | Executes an effect of type @f@ that produces a return value of type @a@.
+send :: Member f l => f a -> Effect l a
+send x = Effect $ \point bind -> bind (Union.inject x) point
+
+-- | 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
+-- @Member f l => f (Effect l a) -> Effect l a@, which allows users
+-- to send effects parameterized by effects.
+sendEffect :: (Member f l, Effectful l r) => f r -> r
+sendEffect x = relay (Union.inject x) id
+
+-- | 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 (* -> *)
+
+    relay :: Union l a -> (a -> 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 f = join $ Effect $ \point bind -> bind u (point . f)
+
+instance Effectful l r => Effectful l (a -> r) where
+    type EffectsOf (a -> r) = EffectsOf r
+    relay u f y = relay u (\x -> f x y)
+
+-- | Handles an effect without eliminating it. The second function parameter is
+-- passed an effect value and a continuation function.
+--
+-- The most common instantiation of this function is:
+--
+-- > (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) -> (forall b. f b -> (b -> r) -> r) -> Effect l a -> r
+intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)
+
+-- | Completely handles an effect. The second function parameter is passed an
+-- effect value and a continuation function.
+--
+-- 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) -> (forall b. f b -> (b -> r) -> r) -> Effect (f ':+ l) a -> r
+eliminate point bind = unEffect point (either bind relay . Union.pop)
+
+-- | Adds an arbitrary effect to the head of the effect list.
+extend :: Effect l a -> Effect (f ':+ l) a
+extend = translate Union.push
+
+-- | Enables an effect that was previously disabled.
+enable :: Effect (f ':- l) a -> Effect l a
+enable = translate Union.enable
+
+-- | Hides an effect @f@ by translating each instance of the effect into an
+-- equivalent effect further into the effect list.
+--
+-- prop> conceal = eliminate return (\x k -> send x >>= k)
+conceal :: Member f l => Effect (f ':+ l) a -> Effect l a
+conceal = translate Union.conceal
+
+-- | Hides an effect @f@ by translating each instance of the effect into an
+-- equivalent effect at the head of the effect list.
+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.
+--
+-- prop> rename f = eliminate return (\x k -> send (f x) >>= k) . swap . extend
+rename :: (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@.
+--
+-- @ mask f = `conceal` . `rename` f . `unflatten` @
+mask :: (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
+
+-- | Converts an effect @f@ into a set of effects @l@.
+--
+-- @ unmask f = `flatten` . `rename` f . `reveal` @
+unmask :: (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
--- a/src/Data/Index.hs
+++ b/src/Data/Index.hs
@@ -29,16 +29,16 @@
         | i == j = Just (unsafeCoerce Refl)
         | otherwise = Nothing
 
-zero :: Index (e :+ l) e
+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 'Nil e -> a
 absurd (Index i) = i `seq` error "absurd Index"
 
-trivial :: Index (e :+ Nil) f -> f :~: e
+trivial :: Index (e ':+ 'Nil) f -> f :~: e
 trivial (Index i)
     | i == 0 = unsafeCoerce Refl
     | otherwise = error "non-trivial Index"
@@ -46,39 +46,39 @@
 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 l e -> Index (f ':+ l) e
 push (Index i) = Index (i + 1)
 
-pop :: Index (f :+ l) e -> Index l e
+pop :: Index (f ':+ l) e -> Index l e
 pop (Index i) = Index (i - 1)
 
-disable :: Index l e -> Index (f :- l) e
+disable :: Index l e -> Index (f ':- l) e
 disable (Index i) = Index (i + 1)
 
-enable :: Index (f :- l) e -> Index l e
+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 :: 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 :: 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 (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 (e ':+ f ':+ g ':+ l) h -> Index (f ':+ g ':+ e ':+ l) h
 rotate (Index i)
     | i == 0 = Index 2
     | i == 1 = Index 0
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -13,8 +13,8 @@
 class KnownNat (n :: Nat) where
     natVal :: proxy n -> Integer
 
-instance KnownNat Zero where
+instance KnownNat 'Zero where
     natVal _ = 0
 
-instance KnownNat n => KnownNat (Succ n) where
+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
--- a/src/Data/Type/Row.hs
+++ b/src/Data/Type/Row.hs
@@ -1,86 +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
+{-# 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,89 +1,89 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Data.Union (
-    Union, absurd,
-    wrap, unwrap,
-    inject, project,
-    swap, rotate,
-    push, pop,
-    enable, disable,
-    conceal, reveal,
-    flatten, unflatten
-) where
-
-import Data.Index (Index)
-import qualified Data.Index as Index
-
-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 @l@ parameterized
--- by @a@. As an effect, it represents the union of each type constructor's
--- corresponding effect. From the user's perspective, it provides a way to
--- encapsulate multiple effects.
-data Union l a where
-    Union :: Index l f -> f a -> Union l a
-
-absurd :: Union Nil a -> b
-absurd (Union i _) = Index.absurd i
-
-wrap :: f a -> Union (f :+ l) a
-wrap = inject
-
-unwrap :: Union (f :+ Nil) a -> f a
-unwrap (Union i x) = gcastWith (Index.trivial i) x
-
-inject :: Member f l => f a -> Union l a
-inject = Union Index.index
-
-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
-
-swap :: Union (f :+ g :+ l) a -> Union (g :+ f :+ l) a
-swap (Union i x) = Union (Index.swap i) x
-
-rotate :: Union (f :+ g :+ h :+ l) a -> Union (g :+ h :+ f :+ l) a
-rotate (Union i x) = Union (Index.rotate i) x
-
-push :: Union l a -> Union (f :+ l) a
-push (Union i x) = Union (Index.push i) x
-
-pop :: Union (f :+ l) a -> Either (f a) (Union l a)
-pop (Union i x) =
-    case testEquality i Index.zero of
-        Just Refl -> Left x
-        Nothing -> Right (Union (Index.pop i) x)
-
-enable :: Union (f :- l) a -> Union l a
-enable (Union i x) = Union (Index.enable i) x
-
-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)
-
-conceal :: Member f l => Union (f :+ l) a -> Union l a
-conceal (Union i x) = Union (Index.conceal i) x
-
-reveal :: Member f l => Union l a -> Union (f :+ l) a
-reveal (Union i x) = Union (Index.reveal i) x
-
-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
-
-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
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Union (
+    Union, absurd,
+    wrap, unwrap,
+    inject, project,
+    swap, rotate,
+    push, pop,
+    enable, disable,
+    conceal, reveal,
+    flatten, unflatten
+) where
+
+import Data.Index (Index)
+import qualified Data.Index as Index
+
+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 @l@ parameterized
+-- by @a@. As an effect, it represents the union of each type constructor's
+-- corresponding effect. From the user's perspective, it provides a way to
+-- encapsulate multiple effects.
+data Union l a where
+    Union :: Index l f -> f a -> Union l a
+
+absurd :: Union 'Nil a -> b
+absurd (Union i _) = Index.absurd i
+
+wrap :: f a -> Union (f ':+ l) a
+wrap = inject
+
+unwrap :: Union (f ':+ 'Nil) a -> f a
+unwrap (Union i x) = gcastWith (Index.trivial i) x
+
+inject :: Member f l => f a -> Union l a
+inject = Union Index.index
+
+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
+
+swap :: Union (f ':+ g ':+ l) a -> Union (g ':+ f ':+ l) a
+swap (Union i x) = Union (Index.swap i) x
+
+rotate :: Union (f ':+ g ':+ h ':+ l) a -> Union (g ':+ h ':+ f ':+ l) a
+rotate (Union i x) = Union (Index.rotate i) x
+
+push :: Union l a -> Union (f ':+ l) a
+push (Union i x) = Union (Index.push i) x
+
+pop :: Union (f ':+ l) a -> Either (f a) (Union l a)
+pop (Union i x) =
+    case testEquality i Index.zero of
+        Just Refl -> Left x
+        Nothing -> Right (Union (Index.pop i) x)
+
+enable :: Union (f ':- l) a -> Union l a
+enable (Union i x) = Union (Index.enable i) x
+
+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)
+
+conceal :: Member f l => Union (f ':+ l) a -> Union l a
+conceal (Union i x) = Union (Index.conceal i) x
+
+reveal :: Member f l => Union l a -> Union (f ':+ l) a
+reveal (Union i x) = Union (Index.reveal i) x
+
+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
+
+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