diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs
index a7403b76..4a909643 100644
--- a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs
+++ b/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs
@@ -76,7 +76,7 @@ data FindConstraint = FindConstraint
 -- | Given a list of constraints, filter out the 'FindConstraint's.
 getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
 getFindConstraints (findClass -> cls) cts = do
-  cd@CDictCan{cc_class = cls', cc_tyargs = [_, r, eff]} <- cts
+  cd@CDictCan{cc_class = cls', cc_tyargs = [_, eff, r]} <- cts
   guard $ cls == cls'
   pure $ FindConstraint
     { fcLoc = ctLoc cd
@@ -163,7 +163,7 @@ extractRowFromSem (semTyCon -> sem) ty = do
 
 ------------------------------------------------------------------------------
 -- | Given a list of bogus @r@s, and the wanted constraints, produce bogus
--- evidence terms that will prevent @IfStuck (IndexOf r _) _ _@ error messsages.
+-- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.
 solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
 solveBogusError stuff wanteds = do
   let splitTyConApp_list = maybeToList  . splitTyConApp_maybe
@@ -172,8 +172,8 @@ solveBogusError stuff wanteds = do
   ct@(CIrredCan ce _) <- wanteds
   (stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce
   guard $ stuck == ifStuckTyCon stuff
-  (idx, [_, r, _]) <- splitTyConApp_list expr
-  guard $ idx == indexOfTyCon stuff
+  (idx, [_, _, r]) <- splitTyConApp_list expr
+  guard $ idx == locateEffectTyCon stuff
   guard $ elem @[] (OrdType r) $ coerce bogus
   pure (error "bogus proof for stuck type family", ct)
 
diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs
index df97ce1d..f24d3ed6 100644
--- a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs
+++ b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs
@@ -23,10 +23,10 @@ import Outputable (pprPanic, empty, text, (<+>), ($$))
 -- When @l ~ 'Locations@, each of these is just a pair of strings. When @l
 -- ~ 'Things@, it's actually references to the stuff.
 data PolysemyStuff (l :: LookupState) = PolysemyStuff
-  { findClass    :: ThingOf l Class
-  , semTyCon     :: ThingOf l TyCon
-  , ifStuckTyCon :: ThingOf l TyCon
-  , indexOfTyCon :: ThingOf l TyCon
+  { findClass         :: ThingOf l Class
+  , semTyCon          :: ThingOf l TyCon
+  , ifStuckTyCon      :: ThingOf l TyCon
+  , locateEffectTyCon :: ThingOf l TyCon
   }
 
 
@@ -34,10 +34,10 @@ data PolysemyStuff (l :: LookupState) = PolysemyStuff
 -- | All of the things we need to lookup.
 polysemyStuffLocations :: PolysemyStuff 'Locations
 polysemyStuffLocations = PolysemyStuff
-  { findClass    = ("Polysemy.Internal.Union",                  "Find")
-  , semTyCon     = ("Polysemy.Internal",                        "Sem")
-  , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
-  , indexOfTyCon = ("Polysemy.Internal.Union",                  "IndexOf")
+  { findClass         = ("Polysemy.Internal.Union",                  "Find")
+  , semTyCon          = ("Polysemy.Internal",                        "Sem")
+  , ifStuckTyCon      = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
+  , locateEffectTyCon = ("Polysemy.Internal.Union",                  "LocateEffect")
   }
 
 
diff --git a/polysemy.cabal b/polysemy.cabal
index e89b9ae6..9614e4f6 100644
--- a/polysemy.cabal
+++ b/polysemy.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.24
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: aac2227e71e3a98458fa5746be7fcbb87da0dc342cdd53913041c95c128871fe
+-- hash: 582807c5d69a34a9e991a77c6111532c05dbb54a5d7aa6662267b7af2d3047ee
 
 name:           polysemy
 version:        1.2.3.0
@@ -48,6 +48,7 @@ library
       Polysemy
       Polysemy.Async
       Polysemy.AtomicState
+      Polysemy.Bundle
       Polysemy.Embed
       Polysemy.Embed.Type
       Polysemy.Error
@@ -57,6 +58,7 @@ library
       Polysemy.Fixpoint
       Polysemy.Input
       Polysemy.Internal
+      Polysemy.Internal.Bundle
       Polysemy.Internal.Combinators
       Polysemy.Internal.CustomErrors
       Polysemy.Internal.CustomErrors.Redefined
@@ -72,6 +74,7 @@ library
       Polysemy.Internal.Writer
       Polysemy.IO
       Polysemy.Law
+      Polysemy.Membership
       Polysemy.NonDet
       Polysemy.Output
       Polysemy.Reader
@@ -134,6 +137,7 @@ test-suite polysemy-test
       HigherOrderSpec
       InspectorSpec
       InterceptSpec
+      KnownRowSpec
       LawsSpec
       OutputSpec
       ThEffectSpec
diff --git a/src/Polysemy/Bundle.hs b/src/Polysemy/Bundle.hs
new file mode 100644
index 00000000..7b00bb86
--- /dev/null
+++ b/src/Polysemy/Bundle.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Polysemy.Bundle
+  ( -- * Effect
+    Bundle (..)
+    -- * Actions
+  , sendBundle
+  , injBundle
+    -- * Interpretations
+  , runBundle
+  , subsumeBundle
+    -- * Miscellaneous
+  , KnownList
+  ) where
+
+import Polysemy
+import Polysemy.Internal
+import Polysemy.Internal.Bundle
+import Polysemy.Internal.Union
+
+------------------------------------------------------------------------------
+-- | An effect for collecting multiple effects into one effect.
+--
+-- Useful for effect newtypes -- effects defined through creating a newtype
+-- over an existing effect, and then defining actions and interpretations on
+-- the newtype by using 'rewrite' and 'transform'.
+--
+-- By making a newtype of 'Bundle', it's possible to wrap multiple effects in
+-- one newtype.
+data Bundle r m a where
+  Bundle :: ElemOf e r -> e m a -> Bundle r m a
+
+------------------------------------------------------------------------------
+-- | Injects an effect into a 'Bundle'. Useful together with 'transform'.
+injBundle :: forall e r m a. Member e r => e m a -> Bundle r m a
+injBundle = Bundle membership
+{-# INLINE injBundle #-}
+
+------------------------------------------------------------------------------
+-- | Send uses of an effect to a 'Bundle' containing that effect.
+sendBundle
+  :: forall e r' r a
+   . (Member e r', Member (Bundle r') r)
+  => Sem (e ': r) a
+  -> Sem r a
+sendBundle = hoistSem $ \u -> case decomp u of
+  Right (Weaving e s wv ex ins) ->
+    injWeaving $
+      Weaving (Bundle (membership @e @r') e) s (sendBundle @e @r' . wv) ex ins
+  Left g -> hoist (sendBundle @e @r') g
+{-# INLINE sendBundle #-}
+
+------------------------------------------------------------------------------
+-- | Run a @'Bundle' r@ by prepending @r@ to the effect stack.
+runBundle
+  :: forall r' r a
+   . KnownList r'
+  => Sem (Bundle r' ': r) a
+  -> Sem (Append r' r) a
+runBundle = hoistSem $ \u -> hoist runBundle $ case decomp u of
+  Right (Weaving (Bundle pr e) s wv ex ins) ->
+    Union (extendMembership @_ @r pr) $ Weaving e s wv ex ins
+  Left g -> weakenList @r' @r g
+{-# INLINE runBundle #-}
+
+------------------------------------------------------------------------------
+-- | Run a @'Bundle' r@ if the effect stack contains all effects of @r@.
+subsumeBundle
+  :: forall r' r a
+   . Members r' r
+  => Sem (Bundle r' ': r) a
+  -> Sem r a
+subsumeBundle = hoistSem $ \u -> hoist subsumeBundle $ case decomp u of
+  Right (Weaving (Bundle pr e) s wv ex ins) ->
+    Union (subsumeMembership pr) (Weaving e s wv ex ins)
+  Left g -> g
+{-# INLINE subsumeBundle #-}
diff --git a/src/Polysemy/Internal.hs b/src/Polysemy/Internal.hs
index 1606dcbc..e215b727 100644
--- a/src/Polysemy/Internal.hs
+++ b/src/Polysemy/Internal.hs
@@ -12,6 +12,7 @@ module Polysemy.Internal
   , MemberWithError
   , Members
   , send
+  , sendUsing
   , embed
   , run
   , runM
@@ -20,6 +21,7 @@ module Polysemy.Internal
   , raiseUnder2
   , raiseUnder3
   , subsume
+  , subsumeUsing
   , Embed (..)
   , usingSem
   , liftSem
@@ -351,8 +353,8 @@ raiseUnder :: ∀ e2 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': r) a
 raiseUnder = hoistSem $ hoist raiseUnder . weakenUnder
   where
     weakenUnder :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': r) m x
-    weakenUnder (Union SZ a) = Union SZ a
-    weakenUnder (Union (SS n) a) = Union (SS (SS n)) a
+    weakenUnder (Union Here a) = Union Here a
+    weakenUnder (Union (There n) a) = Union (There (There n)) a
     {-# INLINE weakenUnder #-}
 {-# INLINE raiseUnder #-}
 
@@ -366,14 +368,14 @@ raiseUnder2 :: ∀ e2 e3 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': r) a
 raiseUnder2 = hoistSem $ hoist raiseUnder2 . weakenUnder2
   where
     weakenUnder2 ::  ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': r) m x
-    weakenUnder2 (Union SZ a) = Union SZ a
-    weakenUnder2 (Union (SS n) a) = Union (SS (SS (SS n))) a
+    weakenUnder2 (Union Here a) = Union Here a
+    weakenUnder2 (Union (There n) a) = Union (There (There (There n))) a
     {-# INLINE weakenUnder2 #-}
 {-# INLINE raiseUnder2 #-}
 
 
 ------------------------------------------------------------------------------
--- | Like 'raise', but introduces two new effects underneath the head of the
+-- | Like 'raise', but introduces three new effects underneath the head of the
 -- list.
 --
 -- @since 1.2.0.0
@@ -381,8 +383,8 @@ raiseUnder3 :: ∀ e2 e3 e4 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': e4
 raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
   where
     weakenUnder3 ::  ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': e4 ': r) m x
-    weakenUnder3 (Union SZ a) = Union SZ a
-    weakenUnder3 (Union (SS n) a) = Union (SS (SS (SS (SS n)))) a
+    weakenUnder3 (Union Here a) = Union Here a
+    weakenUnder3 (Union (There n) a) = Union (There (There (There (There n)))) a
     {-# INLINE weakenUnder3 #-}
 {-# INLINE raiseUnder3 #-}
 
@@ -396,11 +398,37 @@ raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
 --
 -- @since 1.2.0.0
 subsume :: Member e r => Sem (e ': r) a -> Sem r a
-subsume = hoistSem $ \u -> hoist subsume $ case decomp u of
-  Right w -> injWeaving w
-  Left  g -> g
+subsume = subsumeUsing membership
 {-# INLINE subsume #-}
 
+------------------------------------------------------------------------------
+-- | Interprets an effect in terms of another identical effect, given an
+-- explicit proof that the effect exists in @r@.
+--
+-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
+-- in order to conditionally make use of effects. For example:
+--
+-- @
+-- tryListen :: 'Polysemy.Membership.KnownRow' r => 'Sem' r a -> Maybe ('Sem' r ([Int], a))
+-- tryListen m = case 'Polysemy.Membership.tryMembership' @('Polysemy.Writer.Writer' [Int]) of
+--   Just pr -> Just $ 'subsumeUsing' pr ('Polysemy.Writer.listen' ('raise' m))
+--   _       -> Nothing
+-- @
+--
+-- @since TODO
+subsumeUsing :: forall e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a
+subsumeUsing pr =
+  let
+    go :: forall x. Sem (e ': r) x -> Sem r x
+    go = hoistSem $ \u -> hoist go $ case decomp u of
+      Right w -> Union pr w
+      Left  g -> g
+    {-# INLINE go #-}
+  in
+    go
+{-# INLINE subsumeUsing #-}
+
+
 ------------------------------------------------------------------------------
 -- | Embed an effect into a 'Sem'. This is used primarily via
 -- 'Polysemy.makeSem' to implement smart constructors.
@@ -408,6 +436,16 @@ send :: Member e r => e (Sem r) a -> Sem r a
 send = liftSem . inj
 {-# INLINE[3] send #-}
 
+------------------------------------------------------------------------------
+-- | Embed an effect into a 'Sem', given an explicit proof
+-- that the effect exists in @r@.
+--
+-- This is useful in conjunction with 'Polysemy.Membership.tryMembership',
+-- in order to conditionally make use of effects.
+sendUsing :: ElemOf e r -> e (Sem r) a -> Sem r a
+sendUsing pr = liftSem . injUsing pr
+{-# INLINE[3] sendUsing #-}
+
 
 ------------------------------------------------------------------------------
 -- | Embed a monadic action @m@ in 'Sem'.
diff --git a/src/Polysemy/Internal/Bundle.hs b/src/Polysemy/Internal/Bundle.hs
new file mode 100644
index 00000000..7394818a
--- /dev/null
+++ b/src/Polysemy/Internal/Bundle.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Bundle where
+
+import Data.Proxy
+import Polysemy
+import Polysemy.Internal.Union
+
+type family Append l r where
+  Append (a ': l) r = a ': (Append l r)
+  Append '[] r = r
+
+extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
+extendMembership Here = Here
+extendMembership (There e) = There (extendMembership @_ @r' e)
+{-# INLINE extendMembership #-}
+
+subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'
+subsumeMembership Here = membership @e @r'
+subsumeMembership (There (pr :: ElemOf e r'')) = subsumeMembership @r'' @r' pr
+{-# INLINE subsumeMembership #-}
+
+weakenList :: forall r' r m a
+            . KnownList r'
+           => Union r m a
+           -> Union (Append r' r) m a
+weakenList u = unconsKnownList @_ @r' u (\_ (_ :: Proxy r'') -> weaken (weakenList @r'' u))
+{-# INLINE weakenList #-}
+
+
+------------------------------------------------------------------------------
+-- | A class for type-level lists with a known spine.
+--
+-- This constraint is eventually satisfied as @r@ is instantied to a
+-- concrete list.
+class KnownList (l :: [k]) where
+  unconsKnownList :: (l ~ '[] => a)
+                  -> (  forall x r
+                      . (l ~ (x ': r), KnownList r)
+                     => Proxy x
+                     -> Proxy r
+                     -> a
+                     )
+                  -> a
+
+instance KnownList '[] where
+  unconsKnownList b _ = b
+  {-# INLINE unconsKnownList #-}
+
+instance KnownList r => KnownList (x ': r) where
+  unconsKnownList _ b = b Proxy Proxy
+  {-# INLINE unconsKnownList #-}
+
diff --git a/src/Polysemy/Internal/Combinators.hs b/src/Polysemy/Internal/Combinators.hs
index 858df1bb..27d75789 100644
--- a/src/Polysemy/Internal/Combinators.hs
+++ b/src/Polysemy/Internal/Combinators.hs
@@ -19,6 +19,10 @@ module Polysemy.Internal.Combinators
   , reinterpret2H
   , reinterpret3H
 
+  -- * Conditional
+  , interceptUsing
+  , interceptUsingH
+
     -- * Statefulness
   , stateful
   , lazilyStateful
@@ -281,13 +285,55 @@ interceptH
     -> Sem r a
        -- ^ Unlike 'interpretH', 'interceptH' does not consume any effects.
     -> Sem r a
-interceptH f (Sem m) = Sem $ \k -> m $ \u ->
-  case prj u of
-    Just (Weaving e s d y v) ->
-      usingSem k $ fmap y $ runTactics s (raise . d) v $ f e
-    Nothing -> k $ hoist (interceptH f) u
+interceptH = interceptUsingH membership
 {-# INLINE interceptH #-}
 
+------------------------------------------------------------------------------
+-- | A variant of 'intercept' that accepts an explicit proof that the effect
+-- is in the effect stack rather then requiring a 'Member' constraint.
+--
+-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
+-- in order to conditionally perform 'intercept'.
+interceptUsing
+    :: FirstOrder e "interceptUsing"
+    => ElemOf e r
+       -- ^ A proof that the handled effect exists in @r@.
+       -- This can be retrieved through 'Polysemy.Membership.membership' or
+       -- 'Polysemy.Membership.tryMembership'.
+    -> (∀ x m. e m x -> Sem r x)
+       -- ^ A natural transformation from the handled effect to other effects
+       -- already in 'Sem'.
+    -> Sem r a
+       -- ^ Unlike 'interpret', 'intercept' does not consume any effects.
+    -> Sem r a
+interceptUsing pr f = interceptUsingH pr $ \(e :: e m x) -> liftT @m $ f e
+{-# INLINE interceptUsing #-}
+
+------------------------------------------------------------------------------
+-- | A variant of 'interceptH' that accepts an explicit proof that the effect
+-- is in the effect stack rather then requiring a 'Member' constraint.
+--
+-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
+-- in order to conditionally perform 'interceptH'.
+--
+-- See the notes on 'Tactical' for how to use this function.
+interceptUsingH
+    :: ElemOf e r
+       -- ^ A proof that the handled effect exists in @r@.
+       -- This can be retrieved through 'Polysemy.Membership.membership' or
+       -- 'Polysemy.Membership.tryMembership'.
+    -> (∀ x m. e m x -> Tactical e m r x)
+       -- ^ A natural transformation from the handled effect to other effects
+       -- already in 'Sem'.
+    -> Sem r a
+       -- ^ Unlike 'interpretH', 'interceptUsingH' does not consume any effects.
+    -> Sem r a
+interceptUsingH pr f (Sem m) = Sem $ \k -> m $ \u ->
+  case prjUsing pr u of
+    Just (Weaving e s d y v) ->
+      usingSem k $ fmap y $ runTactics s (raise . d) v $ f e
+    Nothing -> k $ hoist (interceptUsingH pr f) u
+{-# INLINE interceptUsingH #-}
 
 ------------------------------------------------------------------------------
 -- | Rewrite an effect @e1@ directly into @e2@, and put it on the top of the
@@ -302,7 +348,7 @@ rewrite
 rewrite f (Sem m) = Sem $ \k -> m $ \u ->
   k $ hoist (rewrite f) $ case decompCoerce u of
     Left x -> x
-    Right (Weaving e s d n y) -> injWeaving $ Weaving (f e) s d n y
+    Right (Weaving e s d n y) -> Union Here $ Weaving (f e) s d n y
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Internal/CustomErrors.hs b/src/Polysemy/Internal/CustomErrors.hs
index facda16c..6117fe5d 100644
--- a/src/Polysemy/Internal/CustomErrors.hs
+++ b/src/Polysemy/Internal/CustomErrors.hs
@@ -76,7 +76,7 @@ type AmbigousEffectMessage (rstate :: EffectRowCtor)
   % "    " <> PrettyPrintList vs <> " directly, or activate polysemy-plugin which"
   % "      can usually infer the type correctly."
 
-type AmbiguousSend r e =
+type AmbiguousSend e r =
       (IfStuck r
         (AmbiguousSendError 'TyVarR r e)
         (Pure (AmbiguousSendError (UnstuckRState r) r e)))
diff --git a/src/Polysemy/Internal/Tactics.hs b/src/Polysemy/Internal/Tactics.hs
index 1db92911..ad0b92c7 100644
--- a/src/Polysemy/Internal/Tactics.hs
+++ b/src/Polysemy/Internal/Tactics.hs
@@ -100,7 +100,7 @@ getInitialStateT = send @(Tactics _ m (e ': r)) GetInitialState
 --
 -- ==== Example
 --
--- We can use the result of 'getInspectT' to "undo" 'pureT' (or any of the other
+-- We can use the result of 'getInspectorT' to "undo" 'pureT' (or any of the other
 -- 'Tactical' functions):
 --
 -- @
diff --git a/src/Polysemy/Internal/Union.hs b/src/Polysemy/Internal/Union.hs
index 4beae597..dd6623e3 100644
--- a/src/Polysemy/Internal/Union.hs
+++ b/src/Polysemy/Internal/Union.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE AllowAmbiguousTypes     #-}
 {-# LANGUAGE CPP                     #-}
 {-# LANGUAGE ConstraintKinds         #-}
+{-# LANGUAGE EmptyCase               #-}
 {-# LANGUAGE FlexibleInstances       #-}
 {-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE InstanceSigs            #-}
 {-# LANGUAGE MultiParamTypeClasses   #-}
 {-# LANGUAGE StrictData              #-}
 {-# LANGUAGE TypeFamilies            #-}
@@ -20,24 +22,30 @@ module Polysemy.Internal.Union
   , hoist
   -- * Building Unions
   , inj
+  , injUsing
   , injWeaving
   , weaken
   -- * Using Unions
   , decomp
   , prj
+  , prjUsing
   , extract
   , absurdU
   , decompCoerce
   -- * Witnesses
-  , SNat (..)
-  , Nat (..)
+  , ElemOf (..)
+  , membership
+  , sameMember
+  -- * Checking membership
+  , KnownRow
+  , tryMembership
   ) where
 
 import Control.Monad
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Kind
-import Data.Type.Equality
+import Data.Typeable
 import Polysemy.Internal.Kind
 
 #ifndef NO_ERROR_MESSAGES
@@ -51,10 +59,10 @@ import Polysemy.Internal.CustomErrors
 data Union (r :: EffectRow) (m :: Type -> Type) a where
   Union
       :: -- A proof that the effect is actually in @r@.
-         SNat n
+         ElemOf e r
          -- The effect to wrap. The functions 'prj' and 'decomp' can help
          -- retrieve this value later.
-      -> Weaving (IndexOf r n) m a
+      -> Weaving e m a
       -> Union r m a
 
 instance Functor (Union r m) where
@@ -129,74 +137,118 @@ type Member e r = MemberNoError e r
 
 ------------------------------------------------------------------------------
 -- | Like 'Member', but will produce an error message if the types are
--- ambiguous.
+-- ambiguous. This is the constraint used for actions generated by
+-- 'Polysemy.makeSem'.
 --
--- @since TODO
+-- /Be careful with this./ Due to quirks of 'GHC.TypeLits.TypeError',
+-- the custom error messages emitted by this can potentially override other,
+-- more helpful error messages.
+-- See the discussion in
+-- <https://github.com/polysemy-research/polysemy/issues/227 Issue #227>.
+--
+-- @since 1.2.3.0
 type MemberWithError e r =
   ( MemberNoError e r
 #ifndef NO_ERROR_MESSAGES
     -- NOTE: The plugin explicitly pattern matches on
-    -- `WhenStuck (IndexOf r _) _`, so if you change this, make sure to change
+    -- `WhenStuck (LocateEffect _ r) _`, so if you change this, make sure to change
     -- the corresponding implementation in
     -- Polysemy.Plugin.Fundep.solveBogusError
-  , WhenStuck (IndexOf r (Found r e)) (AmbiguousSend r e)
+  , WhenStuck (LocateEffect e r) (AmbiguousSend e r)
 #endif
   )
 
 type MemberNoError e r =
-  ( Find r e
-  , e ~ IndexOf r (Found r e)
+  ( Find e r
+#ifndef NO_ERROR_MESSAGES
+  , LocateEffect e r ~ '()
+#endif
   )
 
-
 ------------------------------------------------------------------------------
--- | The kind of type-level natural numbers.
-data Nat = Z | S Nat
-
+-- | A proof that @e@ is an element of @r@.
+--
+-- Due to technical reasons, @'ElemOf' e r@ is not powerful enough to
+-- prove @'Member' e r@; however, it can still be used send actions of @e@
+-- into @r@ by using 'Polysemy.Internal.subsumeUsing'.
+data ElemOf e r where
+  -- | @e@ is located at the head of the list.
+  Here  :: ElemOf e (e ': r)
+  -- | @e@ is located somewhere in the tail of the list.
+  There :: ElemOf e r -> ElemOf e (e' ': r)
 
 ------------------------------------------------------------------------------
--- | A singleton for 'Nat'.
-data SNat :: Nat -> Type where
-  SZ :: SNat 'Z
-  SS :: SNat n -> SNat ('S n)
+-- | Checks if two membership proofs are equal. If they are, then that means
+-- that the effects for which membership is proven must also be equal.
+sameMember :: forall e e' r
+            . ElemOf e r
+           -> ElemOf e' r
+           -> Maybe (e :~: e')
+sameMember Here       Here =
+  Just Refl
+sameMember (There pr) (There pr') =
+  sameMember @e @e' pr pr'
+sameMember (There _)  _ =
+  Nothing
+sameMember _          _ =
+  Nothing
 
-instance TestEquality SNat where
-  testEquality SZ     SZ     = Just Refl
-  testEquality (SS _) SZ     = Nothing
-  testEquality SZ     (SS _) = Nothing
-  testEquality (SS n) (SS m) =
-    case testEquality n m of
-      Nothing -> Nothing
-      Just Refl -> Just Refl
-  {-# INLINE testEquality #-}
 
-
-type family IndexOf (ts :: [k]) (n :: Nat) :: k where
-  IndexOf (k ': ks) 'Z = k
-  IndexOf (k ': ks) ('S n) = IndexOf ks n
-
-
-type family Found (ts :: [k]) (t :: k) :: Nat where
+------------------------------------------------------------------------------
+-- | Used to detect ambiguous uses of effects. If @r@ isn't concrete,
+-- and we haven't been given @'LocateEffect' e r ~ '()@ from a
+-- @'Member' e r@ constraint, then @'LocateEffect' e r@ will get stuck.
+type family LocateEffect (t :: k) (ts :: [k]) :: () where
 #ifndef NO_ERROR_MESSAGES
-  Found '[]       t = UnhandledEffect t
+  LocateEffect t '[] = UnhandledEffect t
 #endif
-  Found (t ': ts) t = 'Z
-  Found (u ': ts) t = 'S (Found ts t)
+  LocateEffect t (t ': ts) = '()
+  LocateEffect t (u ': ts) = LocateEffect t ts
+
+class Find (t :: k) (r :: [k]) where
+  membership' :: ElemOf t r
 
+instance {-# OVERLAPPING #-} Find t (t ': z) where
+  membership' = Here
+  {-# INLINE membership' #-}
 
-class Find (r :: [k]) (t :: k) where
-  finder :: SNat (Found r t)
+instance Find t z => Find t (_1 ': z) where
+  membership' = There $ membership' @_ @t @z
+  {-# INLINE membership' #-}
 
-instance {-# OVERLAPPING #-} Find (t ': z) t where
-  finder = SZ
-  {-# INLINE finder #-}
+------------------------------------------------------------------------------
+-- | A class for effect rows whose elements are inspectable.
+--
+-- This constraint is eventually satisfied as @r@ is instantied to a
+-- monomorphic list.
+-- (E.g when @r@ becomes something like
+-- @'['Polysemy.State.State' Int, 'Polysemy.Output.Output' String, 'Polysemy.Embed' IO]@)
+class KnownRow r where
+  tryMembership' :: forall e. Typeable e => Maybe (ElemOf e r)
+
+instance KnownRow '[] where
+  tryMembership' = Nothing
+  {-# INLINE tryMembership' #-}
+
+instance (Typeable e, KnownRow r) => KnownRow (e ': r) where
+  tryMembership' :: forall e'. Typeable e' => Maybe (ElemOf e' (e ': r))
+  tryMembership' = case eqT @e @e' of
+    Just Refl -> Just Here
+    _         -> There <$> tryMembership' @r @e'
+  {-# INLINE tryMembership' #-}
 
-instance ( Find z t
-         , Found (_1 ': z) t ~ 'S (Found z t)
-         ) => Find (_1 ': z) t where
-  finder = SS $ finder @_ @z @t
-  {-# INLINE finder #-}
+------------------------------------------------------------------------------
+-- | Given @'Member' e r@, extract a proof that @e@ is an element of @r@.
+membership :: Member e r => ElemOf e r
+membership = membership'
+{-# INLINE membership #-}
 
+------------------------------------------------------------------------------
+-- | Extracts a proof that @e@ is an element of @r@ if that
+-- is indeed the case; otherwise returns @Nothing@.
+tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
+tryMembership = tryMembership' @r @e
+{-# INLINE tryMembership #-}
 
 ------------------------------------------------------------------------------
 -- | Decompose a 'Union'. Either this union contains an effect @e@---the head
@@ -204,29 +256,28 @@ instance ( Find z t
 decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)
 decomp (Union p a) =
   case p of
-    SZ   -> Right a
-    SS n -> Left $ Union n a
+    Here  -> Right a
+    There pr -> Left $ Union pr a
 {-# INLINE decomp #-}
 
-
 ------------------------------------------------------------------------------
 -- | Retrieve the last effect in a 'Union'.
 extract :: Union '[e] m a -> Weaving e m a
-extract (Union SZ a) = a
-extract _ = error "impossible"
+extract (Union Here a)   = a
+extract (Union (There g) _) = case g of {}
 {-# INLINE extract #-}
 
 
 ------------------------------------------------------------------------------
 -- | An empty union contains nothing, so this function is uncallable.
 absurdU :: Union '[] m a -> b
-absurdU = absurdU
+absurdU (Union pr _) = case pr of {}
 
 
 ------------------------------------------------------------------------------
 -- | Weaken a 'Union' so it is capable of storing a new sort of effect.
 weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
-weaken (Union n a) = Union (SS n) a
+weaken (Union pr a) = Union (There pr) a
 {-# INLINE weaken #-}
 
 
@@ -241,10 +292,22 @@ inj e = injWeaving $
             (Just . runIdentity)
 {-# INLINE inj #-}
 
+
+------------------------------------------------------------------------------
+-- | Lift an effect @e@ into a 'Union' capable of holding it,
+-- given an explicit proof that the effect exists in @r@
+injUsing :: forall e r m a. Functor m => ElemOf e r -> e m a -> Union r m a
+injUsing pr e = Union pr $
+  Weaving e (Identity ())
+            (fmap Identity . runIdentity)
+            runIdentity
+            (Just . runIdentity)
+{-# INLINE injUsing #-}
+
 ------------------------------------------------------------------------------
 -- | Lift a @'Weaving' e@ into a 'Union' capable of holding it.
 injWeaving :: forall e r m a. Member e r => Weaving e m a -> Union r m a
-injWeaving = Union (finder @_ @r @e)
+injWeaving = Union membership
 {-# INLINE injWeaving #-}
 
 ------------------------------------------------------------------------------
@@ -254,12 +317,19 @@ prj :: forall e r m a
        )
     => Union r m a
     -> Maybe (Weaving e m a)
-prj (Union sn a) =
-  case testEquality sn (finder @_ @r @e) of
-    Nothing -> Nothing
-    Just Refl -> Just a
+prj = prjUsing membership
 {-# INLINE prj #-}
 
+------------------------------------------------------------------------------
+-- | Attempt to take an @e@ effect out of a 'Union', given an explicit
+-- proof that the effect exists in @r@.
+prjUsing
+  :: forall e r m a
+   . ElemOf e r
+  -> Union r m a
+  -> Maybe (Weaving e m a)
+prjUsing pr (Union sn a) = (\Refl -> a) <$> sameMember pr sn
+{-# INLINE prjUsing #-}
 
 ------------------------------------------------------------------------------
 -- | Like 'decomp', but allows for a more efficient
@@ -269,6 +339,6 @@ decompCoerce
     -> Either (Union (f ': r) m a) (Weaving e m a)
 decompCoerce (Union p a) =
   case p of
-    SZ -> Right a
-    SS n -> Left (Union (SS n) a)
+    Here  -> Right a
+    There pr -> Left (Union (There pr) a)
 {-# INLINE decompCoerce #-}
diff --git a/src/Polysemy/Membership.hs b/src/Polysemy/Membership.hs
new file mode 100644
index 00000000..0b45c3b1
--- /dev/null
+++ b/src/Polysemy/Membership.hs
@@ -0,0 +1,17 @@
+module Polysemy.Membership
+  ( -- * Witnesses
+    ElemOf (..)
+  , membership
+  , sameMember
+  -- * Checking membership
+  , KnownRow
+  , tryMembership
+  -- * Using membership
+  , subsumeUsing
+  , interceptUsing
+  , interceptUsingH
+  ) where
+
+import Polysemy.Internal
+import Polysemy.Internal.Combinators
+import Polysemy.Internal.Union
diff --git a/src/Polysemy/Tagged.hs b/src/Polysemy/Tagged.hs
index bb64c5a7..4273197f 100644
--- a/src/Polysemy/Tagged.hs
+++ b/src/Polysemy/Tagged.hs
@@ -80,7 +80,7 @@ untag
 -- Once GHC 8.10 rolls out, I will benchmark and compare.
 untag = hoistSem $ \u -> case decompCoerce u of
   Right (Weaving (Tagged e) s wv ex ins) ->
-    Union SZ (Weaving e s (untag . wv) ex ins)
+    Union Here (Weaving e s (untag . wv) ex ins)
   Left g -> hoist untag g
 {-# INLINE untag #-}
 
diff --git a/test/KnownRowSpec.hs b/test/KnownRowSpec.hs
new file mode 100644
index 00000000..60ea62e4
--- /dev/null
+++ b/test/KnownRowSpec.hs
@@ -0,0 +1,35 @@
+module KnownRowSpec where
+
+import Polysemy
+import Polysemy.Error
+import Polysemy.State
+import Polysemy.Internal
+import Polysemy.Internal.Union
+
+import Test.Hspec
+
+-- | A variant of 'runState' that uses 'stateToIO' if @r@ contains @Embed IO@.
+-- (Can also be extended to check for @Final IO@)
+runState' :: forall s r a. KnownRow r => s -> Sem (State s ': r) a -> Sem r (s, a)
+runState' s sem = case tryMembership @(Embed IO) of
+  Just proof -> subsumeUsing proof (stateToIO s (raiseUnder sem))
+  _          -> runState s sem
+
+
+test :: (Member (Error ()) r, KnownRow r)
+     => Sem r String
+test = fmap fst $ runState' "" $ do
+  put "local state"
+  _ <- (put "global state" >> throw ()) `catch` \() -> return ()
+  return ()
+
+spec :: Spec
+spec = parallel $ describe "tryMembership" $ do
+  it "should return a valid proof when the targeted \
+     \ effect is part of the row" $ do
+    res <- runM . runError @() $ test
+    res `shouldBe` Right "global state"
+  it "should not return a valid proof when the targeted \
+     \ effect is not part of the row" $ do
+    let res = run . runError @() $ test
+    res `shouldBe` Right "local state"