diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,31 @@
 # Changelog for polysemy
 
+
+## 1.3.0.0 (2020-02-14)
+
+### Breaking Changes
+- The semantics for `runNonDet` when `<|>` is used inside a higher-order action
+    of another effect has been reverted to that of 1.1.0.0 and earlier.
+    (See [issue #246](https://github.com/polysemy-research/polysemy/issues/246))
+- Type parameters for `outputToTrace` have been rearranged (thanks to
+    @juanpaucar)
+
+### Other Changes
+- Added `Bundle` effect, for bundling multiple effects into a single one.
+- Added `Tagged` effect, for annotating and disambiguating identical effects.
+- Added `View` effect, an `Input`-like effect for caching an expensive
+    computation.
+- Added `fromException`/`Via` and `fromExceptionSem`/`Via`
+- Added `note`
+- Added `catchJust`, `try` and `tryJust` (thanks to @bolt12)
+- Using `listen` with `runWriterTVar` or `writerToIO` will no longer delay writing
+    until the `listen` completes.
+- Added `runStateSTRef` and `stateToST` (thanks to @incertia)
+- Added `execState` and `execLazyState` (thanks to @tjweir)
+- Added `Polysemy.Law`, which offers machinery for creating laws for effects.
+- Added `Polysemy.Membership` for retrieving and making use of effect membership
+    proofs.
+
 ## 1.2.3.0 (2019-10-29)
 
 - Polysemy now works on GHC 8.8.1 (thanks to @googleson78 and @sevanspowell)
@@ -32,7 +58,7 @@
 - Type variables for certain internal functions, `failToEmbed`, and
     `atomicState'` have been rearranged.
 
-## Other changes
+### Other changes
 
 - Added `Final` effect, an effect for embedding higher-order actions in the
     final monad of the effect stack. Any interpreter should use this instead of
@@ -260,4 +286,3 @@
 
 - Changed the tyvars of `fromEitherM`, `runErrorAsAnother`, `runEmbedded`,
   `asks` and `gets`
-
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -9,6 +9,7 @@
 [![Build Status](https://api.travis-ci.org/polysemy-research/polysemy.svg?branch=master)](https://travis-ci.org/polysemy-research/polysemy)
 [![Hackage](https://img.shields.io/hackage/v/polysemy.svg?logo=haskell&label=polysemy)](https://hackage.haskell.org/package/polysemy)
 [![Hackage](https://img.shields.io/hackage/v/polysemy-plugin.svg?logo=haskell&label=polysemy-plugin)](https://hackage.haskell.org/package/polysemy-plugin)
+[![Zulip chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://funprog.zulipchat.com/#narrow/stream/216942-Polysemy)
 
 ## Dedication
 
@@ -67,10 +68,15 @@
 <sup><a name="fn1">1</a></sup>: Unfortunately this is not true in GHC 8.6.3, but
 will be true in GHC 8.10.1.
 
-## Tutorial
 
-Raghu Kaippully wrote a beginner friendly [tutorial](https://haskell-explained.gitlab.io/blog/posts/2019/07/28/polysemy-is-cool-part-1/index.html).
+## Tutorials and Resources
 
+- Raghu Kaippully wrote a beginner friendly [tutorial](https://haskell-explained.gitlab.io/blog/posts/2019/07/28/polysemy-is-cool-part-1/index.html).
+- Paweł Szulc gave a [great talk](https://youtu.be/idU7GdlfP9Q?t=1394) on how to start thinking about polysemy.
+- I've given a talk on some of the [performance implementation](https://www.youtube.com/watch?v=-dHFOjcK6pA)
+- I've also written [some](http://reasonablypolymorphic.com/blog/freer-higher-order-effects/) [blog posts](http://reasonablypolymorphic.com/blog/tactics/) on other implementation details.
+
+
 ## Examples
 
 Make sure you read the [Necessary Language
@@ -226,7 +232,7 @@
 
 ## Stellar Engineering - Aligning the stars to optimize `polysemy` away
 
-Several things need to be in place to fully realize our performance goals: 
+Several things need to be in place to fully realize our performance goals:
 
 - GHC Version
   - GHC 8.9+
@@ -239,4 +245,28 @@
   - `-fplugin=Polysemy.Plugin`
 - Additional concerns:
   - additional core passes (turned on by the plugin)
+
+
+## Acknowledgements, citations, and related work
+
+The following is a non-exhaustive list of people and works that have had a
+significant impact, directly or indirectly, on `polysemy`’s design and
+implementation:
+
+  - Oleg Kiselyov, Amr Sabry, and Cameron Swords — [Extensible Effects: An alternative to monad transfomers][oleg:exteff]
+  - Oleg Kiselyov and Hiromi Ishii — [Freer Monads, More Extensible Effects][oleg:more]
+  - Nicolas Wu, Tom Schrijvers, and Ralf Hinze — [Effect Handlers in Scope][wu:scope]
+  - Nicolas Wu and Tom Schrijvers — [Fusion for Free: Efficient Algebraic Effect Handlers][schrijvers:fusion]
+  - Andy Gill and other contributors — [`mtl`][hackage:mtl]
+  - Rob Rix, Patrick Thomson, and other contributors — [`fused-effects`][gh:fused-effects]
+  - Alexis King and other contributors — [`freer-simple`][gh:freer-simple]
+
+[docs]: https://hasura.github.io/eff/Control-Effect.html
+[gh:fused-effects]: https://github.com/fused-effects/fused-effects
+[gh:freer-simple]: https://github.com/lexi-lambda/freer-simple
+[hackage:mtl]: https://hackage.haskell.org/package/mtl
+[oleg:exteff]: http://okmij.org/ftp/Haskell/extensible/exteff.pdf
+[oleg:more]: http://okmij.org/ftp/Haskell/extensible/more.pdf
+[schrijvers:fusion]: https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/mpc2015.pdf
+[wu:scope]: https://www.cs.ox.ac.uk/people/nicolas.wu/papers/Scope.pdf
 
diff --git a/polysemy.cabal b/polysemy.cabal
--- a/polysemy.cabal
+++ b/polysemy.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5fb909edb732407e798db0fa3e2e0a62dbeb807e960b77564b99b34a3235fdb3
+-- hash: 0f1599ec8e1caf24489536a197f2eb261ecdfb3613fdc2f2221186cdb0f31a5e
 
 name:           polysemy
-version:        1.2.3.0
+version:        1.3.0.0
 synopsis:       Higher-order, low-boilerplate, zero-cost free monads.
 description:    Please see the README on GitHub at <https://github.com/isovector/polysemy#readme>
 category:       Language
@@ -48,6 +48,7 @@
       Polysemy
       Polysemy.Async
       Polysemy.AtomicState
+      Polysemy.Bundle
       Polysemy.Embed
       Polysemy.Embed.Type
       Polysemy.Error
@@ -57,6 +58,7 @@
       Polysemy.Fixpoint
       Polysemy.Input
       Polysemy.Internal
+      Polysemy.Internal.Bundle
       Polysemy.Internal.Combinators
       Polysemy.Internal.CustomErrors
       Polysemy.Internal.CustomErrors.Redefined
@@ -71,12 +73,17 @@
       Polysemy.Internal.Union
       Polysemy.Internal.Writer
       Polysemy.IO
+      Polysemy.Law
+      Polysemy.Membership
       Polysemy.NonDet
       Polysemy.Output
       Polysemy.Reader
       Polysemy.Resource
       Polysemy.State
+      Polysemy.State.Law
+      Polysemy.Tagged
       Polysemy.Trace
+      Polysemy.View
       Polysemy.Writer
   other-modules:
       Polysemy.Internal.PluginLookup
@@ -85,10 +92,11 @@
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   ghc-options: -Wall
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
-    , first-class-families >=0.5.0.0 && <0.7
+    , first-class-families >=0.5.0.0 && <0.8
     , mtl >=2.2.2 && <3
     , stm >=2 && <3
     , syb >=0.7 && <0.8
@@ -100,9 +108,6 @@
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions: MonadFailDesugaring TypeInType
-  if impl(ghc >= 8.7)
-    build-depends:
-        loopbreaker >=0.1 && <0.2
   if flag(dump-core)
     ghc-options: -fplugin=DumpCore -fplugin-opt=DumpCore:core-html
     build-depends:
@@ -110,8 +115,6 @@
   if impl(ghc < 8.2.2)
     build-depends:
         unsupported-ghc-version >1 && <1
-  if impl(ghc >= 8.7)
-    ghc-options: -fplugin=Loopbreaker
   if flag(error-messages)
     cpp-options: -DCABAL_SERIOUSLY_CMON_MATE
   else
@@ -126,6 +129,7 @@
       AsyncSpec
       BracketSpec
       DoctestSpec
+      ErrorSpec
       FailSpec
       FinalSpec
       FixpointSpec
@@ -133,9 +137,12 @@
       HigherOrderSpec
       InspectorSpec
       InterceptSpec
+      KnownRowSpec
+      LawsSpec
       OutputSpec
       ThEffectSpec
       TypeErrors
+      ViewSpec
       WriterSpec
       Paths_polysemy
   hs-source-dirs:
@@ -145,11 +152,12 @@
   build-tool-depends:
       hspec-discover:hspec-discover >=2.0
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
     , doctest >=0.16.0.1 && <0.17
-    , first-class-families >=0.5.0.0 && <0.7
+    , first-class-families >=0.5.0.0 && <0.8
     , hspec >=2.6.0 && <3
     , inspection-testing >=0.4.2 && <0.5
     , mtl >=2.2.2 && <3
@@ -164,9 +172,6 @@
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions: MonadFailDesugaring TypeInType
-  if impl(ghc >= 8.7)
-    build-depends:
-        loopbreaker >=0.1 && <0.2
   default-language: Haskell2010
 
 benchmark polysemy-bench
@@ -179,11 +184,12 @@
       bench
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
     , criterion
-    , first-class-families >=0.5.0.0 && <0.7
+    , first-class-families >=0.5.0.0 && <0.8
     , free
     , freer-simple
     , mtl
@@ -198,7 +204,4 @@
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions: MonadFailDesugaring TypeInType
-  if impl(ghc >= 8.7)
-    build-depends:
-        loopbreaker >=0.1 && <0.2
   default-language: Haskell2010
diff --git a/src/Polysemy/Bundle.hs b/src/Polysemy/Bundle.hs
new file mode 100644
--- /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/Error.hs b/src/Polysemy/Error.hs
--- a/src/Polysemy/Error.hs
+++ b/src/Polysemy/Error.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell     #-}
 
 module Polysemy.Error
   ( -- * Effect
@@ -9,6 +10,14 @@
   , catch
   , fromEither
   , fromEitherM
+  , fromException
+  , fromExceptionVia
+  , fromExceptionSem
+  , fromExceptionSemVia
+  , note
+  , try
+  , tryJust
+  , catchJust
 
     -- * Interpretations
   , runError
@@ -50,7 +59,7 @@
     -> Sem r a
 fromEither (Left e) = throw e
 fromEither (Right a) = pure a
-
+{-# INLINABLE fromEither #-}
 
 ------------------------------------------------------------------------------
 -- | A combinator doing 'embed' and 'fromEither' at the same time. Useful for
@@ -65,9 +74,122 @@
     => m (Either e a)
     -> Sem r a
 fromEitherM = fromEither <=< embed
+{-# INLINABLE fromEitherM #-}
 
 
 ------------------------------------------------------------------------------
+-- | Lift an exception generated from an 'IO' action into an 'Error'.
+fromException
+    :: forall e r a
+     . ( X.Exception e
+       , Member (Error e) r
+       , Member (Embed IO) r
+       )
+    => IO a
+    -> Sem r a
+fromException = fromExceptionVia @e id
+{-# INLINABLE fromException #-}
+
+
+------------------------------------------------------------------------------
+-- | Like 'fromException', but with the ability to transform the exception
+-- before turning it into an 'Error'.
+fromExceptionVia
+    :: ( X.Exception exc
+       , Member (Error err) r
+       , Member (Embed IO) r
+       )
+    => (exc -> err)
+    -> IO a
+    -> Sem r a
+fromExceptionVia f m = do
+  r <- embed $ X.try m
+  case r of
+    Left e -> throw $ f e
+    Right a -> pure a
+{-# INLINABLE fromExceptionVia #-}
+
+------------------------------------------------------------------------------
+-- | Run a @Sem r@ action, converting any 'IO' exception generated by it into an 'Error'.
+fromExceptionSem
+    :: forall e r a
+     . ( X.Exception e
+       , Member (Error e) r
+       , Member (Final IO) r
+       )
+    => Sem r a
+    -> Sem r a
+fromExceptionSem = fromExceptionSemVia @e id
+{-# INLINABLE fromExceptionSem #-}
+
+------------------------------------------------------------------------------
+-- | Like 'fromExceptionSem', but with the ability to transform the exception
+-- before turning it into an 'Error'.
+fromExceptionSemVia
+    :: ( X.Exception exc
+       , Member (Error err) r
+       , Member (Final IO) r
+       )
+    => (exc -> err)
+    -> Sem r a
+    -> Sem r a
+fromExceptionSemVia f m = do
+  r <- withStrategicToFinal $ do
+    m' <- runS m
+    s  <- getInitialStateS
+    pure $ (fmap . fmap) Right m' `X.catch` \e -> (pure (Left e <$ s))
+  case r of
+    Left e -> throw $ f e
+    Right a -> pure a
+{-# INLINABLE fromExceptionSemVia #-}
+
+------------------------------------------------------------------------------
+-- | Attempt to extract a @'Just' a@ from a @'Maybe' a@, throwing the
+-- provided exception upon 'Nothing'.
+note :: Member (Error e) r => e -> Maybe a -> Sem r a
+note e Nothing  = throw e
+note _ (Just a) = pure a
+{-# INLINABLE note #-}
+
+------------------------------------------------------------------------------
+-- | Similar to @'catch'@, but returns an @'Either'@ result which is (@'Right' a@) 
+-- if no exception of type @e@ was @'throw'@n, or (@'Left' ex@) if an exception of type 
+-- @e@ was @'throw'@n and its value is @ex@. 
+try :: Member (Error e) r => Sem r a -> Sem r (Either e a)
+try m = catch (Right <$> m) (return . Left)
+{-# INLINABLE try #-}
+
+------------------------------------------------------------------------------
+-- | A variant of @'try'@ that takes an exception predicate to select which exceptions
+-- are caught (c.f. @'catchJust'@). If the exception does not match the predicate, 
+-- it is re-@'throw'@n.
+tryJust :: Member (Error e) r => (e -> Maybe b) -> Sem r a -> Sem r (Either b a)
+tryJust f m = do
+    r <- try m
+    case r of
+      Right v -> return (Right v)
+      Left e -> case f e of
+                  Nothing -> throw e
+                  Just b -> return $ Left b
+{-# INLINABLE tryJust #-}
+
+------------------------------------------------------------------------------
+-- | The function @'catchJust'@ is like @'catch'@, but it takes an extra argument 
+-- which is an exception predicate, a function which selects which type of exceptions 
+-- we're interested in.
+catchJust :: Member (Error e) r 
+          => (e -> Maybe b) -- ^ Predicate to select exceptions
+          -> Sem r a  -- ^ Computation to run
+          -> (b -> Sem r a) -- ^ Handler
+          -> Sem r a
+catchJust ef m bf = catch m handler
+  where
+      handler e = case ef e of
+                    Nothing -> throw e
+                    Just b -> bf b
+{-# INLINABLE catchJust #-}
+
+------------------------------------------------------------------------------
 -- | Run an 'Error' effect in the style of
 -- 'Control.Monad.Trans.Except.ExceptT'.
 runError
@@ -81,9 +203,9 @@
             hush
             x
     Right (Weaving (Throw e) _ _ _ _) -> E.throwE e
-    Right (Weaving (Catch try handle) s d y _) ->
+    Right (Weaving (Catch main handle) s d y _) ->
       E.ExceptT $ usingSem k $ do
-        ma <- runError $ d $ try <$ s
+        ma <- runError $ d $ main <$ s
         case ma of
           Right a -> pure . Right $ y a
           Left e -> do
@@ -93,7 +215,6 @@
               Right a -> pure . Right $ y a
 {-# INLINE runError #-}
 
-
 ------------------------------------------------------------------------------
 -- | Transform one 'Error' into another. This function can be used to aggregate
 -- multiple errors into a single type.
@@ -208,11 +329,11 @@
     -> Sem r a
 runErrorAsExc lower = interpretH $ \case
   Throw e -> embed $ X.throwIO $ WrappedExc e
-  Catch try handle -> do
+  Catch main handle -> do
     is <- getInitialStateT
-    t  <- runT try
+    m  <- runT main
     h  <- bindT handle
     let runIt = lower . runErrorAsExc lower
-    embed $ X.catch (runIt t) $ \(se :: WrappedExc e) ->
+    embed $ X.catch (runIt m) $ \(se :: WrappedExc e) ->
       runIt $ h $ unwrapExc se <$ is
 {-# INLINE runErrorAsExc #-}
diff --git a/src/Polysemy/Internal.hs b/src/Polysemy/Internal.hs
--- a/src/Polysemy/Internal.hs
+++ b/src/Polysemy/Internal.hs
@@ -12,6 +12,7 @@
   , MemberWithError
   , Members
   , send
+  , sendUsing
   , embed
   , run
   , runM
@@ -20,6 +21,7 @@
   , raiseUnder2
   , raiseUnder3
   , subsume
+  , subsumeUsing
   , Embed (..)
   , usingSem
   , liftSem
@@ -351,8 +353,8 @@
 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 = 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 = 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,17 +398,53 @@
 --
 -- @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 1.3.0.0
+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.
 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 #-}
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Internal/Bundle.hs b/src/Polysemy/Internal/Bundle.hs
new file mode 100644
--- /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
--- a/src/Polysemy/Internal/Combinators.hs
+++ b/src/Polysemy/Internal/Combinators.hs
@@ -19,6 +19,10 @@
   , reinterpret2H
   , reinterpret3H
 
+  -- * Conditional
+  , interceptUsing
+  , interceptUsingH
+
     -- * Statefulness
   , stateful
   , lazilyStateful
@@ -281,15 +285,61 @@
     -> 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'.
+--
+-- @since 1.3.0.0
+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.
+--
+-- @since 1.3.0.0
+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
 -- effect stack.
 --
@@ -302,7 +352,7 @@
 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
--- a/src/Polysemy/Internal/CustomErrors.hs
+++ b/src/Polysemy/Internal/CustomErrors.hs
@@ -76,7 +76,7 @@
   % "    " <> 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
--- a/src/Polysemy/Internal/Tactics.hs
+++ b/src/Polysemy/Internal/Tactics.hs
@@ -100,7 +100,7 @@
 --
 -- ==== 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
--- 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 @@
   , 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 @@
 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,120 @@
 
 ------------------------------------------------------------------------------
 -- | 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'.
+--
+-- @since 1.3.0.0
+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 #-}
 
+------------------------------------------------------------------------------
+-- | 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
+  LocateEffect t '[] = UnhandledEffect t
+#endif
+  LocateEffect t (t ': ts) = '()
+  LocateEffect t (u ': ts) = LocateEffect t ts
 
-type family IndexOf (ts :: [k]) (n :: Nat) :: k where
-  IndexOf (k ': ks) 'Z = k
-  IndexOf (k ': ks) ('S n) = IndexOf ks n
+class Find (t :: k) (r :: [k]) where
+  membership' :: ElemOf t r
 
+instance {-# OVERLAPPING #-} Find t (t ': z) where
+  membership' = Here
+  {-# INLINE membership' #-}
 
-type family Found (ts :: [k]) (t :: k) :: Nat where
-#ifndef NO_ERROR_MESSAGES
-  Found '[]       t = UnhandledEffect t
-#endif
-  Found (t ': ts) t = 'Z
-  Found (u ': ts) t = 'S (Found ts t)
+instance Find t z => Find t (_1 ': z) where
+  membership' = There $ membership' @_ @t @z
+  {-# INLINE membership' #-}
 
+------------------------------------------------------------------------------
+-- | 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)
 
-class Find (r :: [k]) (t :: k) where
-  finder :: SNat (Found r t)
+instance KnownRow '[] where
+  tryMembership' = Nothing
+  {-# INLINE tryMembership' #-}
 
-instance {-# OVERLAPPING #-} Find (t ': z) t where
-  finder = SZ
-  {-# INLINE finder #-}
+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 +258,28 @@
 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 +294,22 @@
             (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 +319,19 @@
        )
     => 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 +341,6 @@
     -> 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/Internal/Writer.hs b/src/Polysemy/Internal/Writer.hs
--- a/src/Polysemy/Internal/Writer.hs
+++ b/src/Polysemy/Internal/Writer.hs
@@ -5,13 +5,18 @@
 import Control.Concurrent.STM
 import Control.Exception
 import Control.Monad
+import qualified Control.Monad.Trans.Writer.Lazy as Lazy
 
+import Data.Bifunctor (first)
 import Data.Semigroup
 
 import Polysemy
 import Polysemy.Final
 
+import Polysemy.Internal
+import Polysemy.Internal.Union
 
+
 ------------------------------------------------------------------------------
 -- | An effect capable of emitting and intercepting messages.
 data Writer o m a where
@@ -85,68 +90,97 @@
       tvar   <- newTVarIO mempty
       switch <- newTVarIO False
       fa     <-
-        restore (wv (runWriterSTMAction (write' tvar switch) m' <$ s))
-          `onException` commit tvar switch id
-      o      <- commit tvar switch id
+        restore (wv (runWriterSTMAction (writeListen tvar switch) m' <$ s))
+          `onException` commitListen tvar switch
+      o      <- commitListen tvar switch
       return $ (fmap . fmap) (o, ) fa
   Pass m -> do
     m'  <- runT m
     ins <- getInspectorT
     raise $ withWeavingToFinal $ \s wv ins' -> mask $ \restore -> do
+      -- See below to understand how this works
       tvar   <- newTVarIO mempty
       switch <- newTVarIO False
       t      <-
-        restore (wv (runWriterSTMAction (write' tvar switch) m' <$ s))
-          `onException` commit tvar switch id
-      _      <- commit tvar switch
+        restore (wv (runWriterSTMAction (writePass tvar switch) m' <$ s))
+          `onException` commitPass tvar switch id
+      commitPass tvar switch
         (maybe id fst $ ins' t >>= inspect ins)
       return $ (fmap . fmap) snd t
 
   where
     {- KingoftheHomeless:
-      'write'' is used by the argument computation to a 'listen' or 'pass'
-      in order to 'tell', rather than directly using the 'write'.
+      'writeListen'/'writePass' is used by the argument computation to a
+      'listen' or 'pass' in order to 'tell', rather than directly using
+      the provided 'write'.
       This is because we need to temporarily store its
-      'tell's seperately in order for the 'listen'/'pass' to work
-      properly. Once the 'listen'/'pass' completes, we 'commit' the
-      changes done to the local tvar globally through 'write'.
+      'tell's locally in order for the 'listen'/'pass' to work
+      properly. In the case of 'listen', this is done in parallel with
+      the global 'write's. In the case of 'pass', the argument computation
+      doesn't use 'write' at all, and instead, when the computation completes,
+      commit the changes it made to the local tvar by 'commitPass',
+      globally 'write'ing it all at once.
+      ('commitListen' serves only as a (likely unneeded)
+      safety measure.)
 
-      'commit' is protected by 'mask'+'onException'. Combine this
-      with the fact that the 'withWeavingToFinal' can't be interrupted
-      by pure errors emitted by effects (since these will be
+      'commitListen'/'commitPass' is protected by 'mask'+'onException'.
+      Combine this with the fact that the 'withWeavingToFinal' can't be
+      interrupted by pure errors emitted by effects (since these will be
       represented as part of the functorial state), and we
       guarantee that no writes will be lost if the argument computation
       fails for whatever reason.
 
-      The argument computation to a 'listen'/'pass' may also spawn
+      The argument computation to a 'pass' may also spawn
       asynchronous computations which do 'tell's of their own.
       In order to make sure these 'tell's won't be lost once a
-      'listen'/'pass' completes, a switch is used to
-      control which tvar 'write'' writes to. The switch is flipped
+      'pass' completes, a switch is used to
+      control which tvar 'writePass' writes to. The switch is flipped
       atomically together with commiting the writes of the local tvar
       as part of 'commit'. Once the switch is flipped,
-      any asynchrounous computations spawned by the argument
+      any asynchronous computations spawned by the argument
       computation will write to the global tvar instead of the local
       tvar (which is no longer relevant), and thus no writes will be
       lost.
     -}
-    write' :: TVar o
-           -> TVar Bool
-           -> o
-           -> STM ()
-    write' tvar switch = \o -> do
+
+    writeListen :: TVar o
+                -> TVar Bool
+                -> o
+                -> STM ()
+    writeListen tvar switch = \o -> do
+      alreadyCommited <- readTVar switch
+      unless alreadyCommited $ do
+        s <- readTVar tvar
+        writeTVar tvar $! s <> o
+      write o
+    {-# INLINE writeListen #-}
+
+    writePass :: TVar o
+              -> TVar Bool
+              -> o
+              -> STM ()
+    writePass tvar switch = \o -> do
       useGlobal <- readTVar switch
       if useGlobal then
         write o
       else do
         s <- readTVar tvar
         writeTVar tvar $! s <> o
+    {-# INLINE writePass #-}
 
-    commit :: TVar o
-           -> TVar Bool
-           -> (o -> o)
-           -> IO o
-    commit tvar switch f = atomically $ do
+    commitListen :: TVar o
+                 -> TVar Bool
+                 -> IO o
+    commitListen tvar switch = atomically $ do
+      writeTVar switch True
+      readTVar tvar
+    {-# INLINE commitListen #-}
+
+    commitPass :: TVar o
+               -> TVar Bool
+               -> (o -> o)
+               -> IO ()
+    commitPass tvar switch f = atomically $ do
       o <- readTVar tvar
       let !o' = f o
       -- Likely redundant, but doesn't hurt.
@@ -154,5 +188,34 @@
       unless alreadyCommited $
         write o'
       writeTVar switch True
-      return o'
+    {-# INLINE commitPass #-}
 {-# INLINE runWriterSTMAction #-}
+
+
+-- TODO (KingoftheHomeless):
+-- Benchmark to see if switching to a more flexible variant
+-- would incur a performance loss
+interpretViaLazyWriter
+  :: forall o e r a
+   . Monoid o
+  => (forall m x. Monad m => Weaving e (Lazy.WriterT o m) x -> Lazy.WriterT o m x)
+  -> Sem (e ': r) a
+  -> Sem r (o, a)
+interpretViaLazyWriter f sem = Sem $ \(k :: forall x. Union r (Sem r) x -> m x) ->
+  let
+    go :: forall x. Sem (e ': r) x -> Lazy.WriterT o m x
+    go = usingSem $ \u -> case decomp u of
+      Right (Weaving e s wv ex ins) -> f $ Weaving e s (go . wv) ex ins
+      Left g -> Lazy.WriterT $ do
+        ~(o, a) <- k $
+          weave
+            (mempty, ())
+            (\ ~(o, m) -> (fmap . first) (o <>) (interpretViaLazyWriter f m))
+            (Just . snd)
+            g
+        return (a, o)
+    {-# INLINE go #-}
+  in do
+    ~(a,s) <- Lazy.runWriterT (go sem)
+    return (s, a)
+{-# INLINE interpretViaLazyWriter #-}
diff --git a/src/Polysemy/Law.hs b/src/Polysemy/Law.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Law.hs
@@ -0,0 +1,197 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+#if __GLASGOW_HASKELL__ < 806
+-- There is a bug in older versions of Haddock that don't allow documentation
+-- on GADT arguments.
+#define HADDOCK --
+#else
+#define HADDOCK -- ^
+#endif
+
+module Polysemy.Law
+  ( Law (..)
+  , runLaw
+  , MakeLaw (..)
+  , Citizen (..)
+  , printf
+  , module Test.QuickCheck
+  ) where
+
+import Control.Arrow (first)
+import Data.Char
+import Polysemy
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | Associates the name @r@ with the eventual type @a@. For example,
+-- @'Citizen' (String -> Bool) Bool@ can produce arbitrary @Bool@s by calling
+-- the given function with arbitrary @String@s.
+class Citizen r a | r -> a where
+  -- | Generate two @a@s via two @r@s. Additionally, produce a list of strings
+  -- corresponding to any arbitrary arguments we needed to build.
+  getCitizen :: r -> r -> Gen ([String], (a, a))
+
+instance {-# OVERLAPPING #-} Citizen (Sem r a -> b) (Sem r a -> b) where
+  getCitizen r1 r2 = pure ([], (r1, r2))
+
+instance Citizen (Sem r a) (Sem r a) where
+  getCitizen r1 r2 = pure ([], (r1, r2))
+
+instance (Arbitrary a, Show a, Citizen b r) => Citizen (a -> b) r where
+  getCitizen f1 f2 = do
+    a <- arbitrary
+    first (show a :) <$> getCitizen (f1 a) (f2 a)
+
+
+------------------------------------------------------------------------------
+-- | A law that effect @e@ must satisfy whenever it is in environment @r@. You
+-- can use 'runLaw' to transform these 'Law's into QuickCheck-able 'Property's.
+data Law e r where
+  -- | A pure 'Law', that doesn't require any access to 'IO'.
+  Law
+      :: ( Eq a
+         , Show a
+         , Citizen i12n (Sem r x -> a)
+         , Citizen res (Sem (e ': r) x)
+         )
+      => i12n
+         HADDOCK An interpretation from @'Sem' r x@ down to a pure value. This is
+         -- likely 'run'.
+      -> String
+         HADDOCK A string representation of the left-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the right-handed side was called with.
+      -> String
+         HADDOCK A string representation of the right-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the left-handed side was called with.
+      -> Law e r
+  -- | Like 'Law', but for 'IO'-accessing effects.
+  LawIO
+      :: ( Eq a
+         , Show a
+         , Citizen i12n (Sem r x -> IO a)
+         , Citizen res (Sem (e ': r) x)
+         )
+      => i12n
+         HADDOCK An interpretation from @'Sem' r x@ down to an 'IO' value. This is
+         -- likely 'runM'.
+      -> String
+         HADDOCK A string representation of the left-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the right-handed side was called with.
+      -> String
+         HADDOCK A string representation of the right-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the left-handed side was called with.
+      -> Law e r
+
+
+------------------------------------------------------------------------------
+-- | A typeclass that provides the smart constructor 'mkLaw'.
+class MakeLaw e r where
+  -- | A smart constructor for building 'Law's.
+  mkLaw
+      :: (Eq a, Show a, Citizen res (Sem (e ': r) a))
+      => String
+      -> res
+      -> String
+      -> res
+      -> Law e r
+
+instance MakeLaw e '[] where
+  mkLaw = Law run
+
+instance MakeLaw e '[Embed IO] where
+  mkLaw = LawIO runM
+
+
+------------------------------------------------------------------------------
+-- | Produces a QuickCheck-able 'Property' corresponding to whether the given
+-- interpreter satisfies the 'Law'.
+runLaw :: InterpreterFor e r -> Law e r -> Property
+runLaw i12n (Law finish str1 a str2 b) = property $ do
+  (_, (lower, _)) <- getCitizen finish finish
+  (args, (ma, mb)) <- getCitizen a b
+  let run_it = lower . i12n
+      a' = run_it ma
+      b' = run_it mb
+  pure $
+    counterexample
+      (mkCounterexampleString str1 a' str2 b' args)
+      (a' == b')
+runLaw i12n (LawIO finish str1 a str2 b) = property $ do
+  (_, (lower, _)) <- getCitizen finish finish
+  (args, (ma, mb)) <- getCitizen a b
+  let run_it = lower . i12n
+  pure $ ioProperty $ do
+    a' <- run_it ma
+    b' <- run_it mb
+    pure $
+      counterexample
+        (mkCounterexampleString str1 a' str2 b' args)
+        (a' == b')
+
+
+------------------------------------------------------------------------------
+-- | Make a string representation for a failing 'runLaw' property.
+mkCounterexampleString
+    :: Show a
+    => String
+    -> a
+    -> String
+    -> a
+    -> [String]
+    -> String
+mkCounterexampleString str1 a str2 b args =
+  mconcat
+    [ printf str1 args , " (result: " , show a , ")\n /= \n"
+    , printf str2 args , " (result: " , show b , ")"
+    ]
+
+
+------------------------------------------------------------------------------
+-- | A bare-boned implementation of printf. This function will replace tokens
+-- of the form @"%n"@ in the first string with @args !! n@.
+--
+-- This will only work for indexes up to 9.
+--
+-- For example:
+--
+-- >>> printf "hello %1 %2% %3 %1" ["world", "50"]
+-- "hello world 50% %3 world"
+printf :: String -> [String] -> String
+printf str args = splitArgs str
+  where
+    splitArgs :: String -> String
+    splitArgs s =
+      case break (== '%') s of
+        (as, "") -> as
+        (as, _ : b : bs)
+          | isDigit b
+          , let d = read [b] - 1
+          , d < length args
+            -> as ++ (args !! d) ++ splitArgs bs
+        (as, _ : bs) ->  as ++ "%" ++ splitArgs bs
+
diff --git a/src/Polysemy/Membership.hs b/src/Polysemy/Membership.hs
new file mode 100644
--- /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/NonDet.hs b/src/Polysemy/NonDet.hs
--- a/src/Polysemy/NonDet.hs
+++ b/src/Polysemy/NonDet.hs
@@ -13,6 +13,7 @@
 
 import Control.Applicative
 import Control.Monad.Trans.Maybe
+import Data.Maybe
 
 import Polysemy
 import Polysemy.Error
@@ -108,46 +109,15 @@
 runNonDetInC :: Sem (NonDet ': r) a -> NonDetC (Sem r) a
 runNonDetInC = usingSem $ \u ->
   case decomp u of
-    Left x  -> consC $ fmap getNonDetState $
-      liftSem $ weave (NonDetState (Just ((), empty)))
-                  distribNonDetC
-                  -- TODO(KingoftheHomeless): Is THIS the right semantics?
-                  (fmap fst . getNonDetState)
+    Left x  -> NonDetC $ \c b -> do
+      l <- liftSem $ weave [()]
+                  -- KingoftheHomeless: This is NOT the right semantics, but
+                  -- the known alternatives are worse. See Issue #246.
+                  (fmap concat . traverse runNonDet)
+                  listToMaybe
                   x
+      foldr c b l
     Right (Weaving Empty _ _ _ _) -> empty
     Right (Weaving (Choose left right) s wv ex _) -> fmap ex $
       runNonDetInC (wv (left <$ s)) <|> runNonDetInC (wv (right <$ s))
 {-# INLINE runNonDetInC #-}
-
--- This choice of functorial state is inspired from the
--- MonadBaseControl instance for 'ListT' from 'list-t'.
---
--- TODO(KingoftheHomeless):
--- Is there a different representation of this which doesn't require
--- 'unconsC' in 'distribNonDetC'?
-newtype NonDetState r a = NonDetState {
-  getNonDetState :: Maybe (a, NonDetC (Sem r) a)
-  } deriving (Functor)
-
--- KingoftheHomeless: The performance of this could be improved
--- if we weren't forced to use unconsC, which causes this to have
--- potentially O(n^2) behaviour.
-distribNonDetC :: NonDetState r (Sem (NonDet ': r) a) -> Sem r (NonDetState r a)
-distribNonDetC = \case
-  NonDetState (Just (a, r)) ->
-    fmap NonDetState $ unconsC $ runNonDetInC a <|> (r >>= runNonDetInC)
-  _ ->
-    pure (NonDetState Nothing)
-{-# INLINE distribNonDetC #-}
-
--- O(n)
-unconsC :: NonDetC (Sem r) a -> Sem r (Maybe (a, NonDetC (Sem r) a))
-unconsC (NonDetC n) = n (\a r -> pure (Just (a, consC r))) (pure Nothing)
-{-# INLINE unconsC #-}
-
-consC :: Sem r (Maybe (a, NonDetC (Sem r) a)) -> NonDetC (Sem r) a
-consC m = NonDetC $ \cons nil -> m >>= \case
-  Just (a, r) -> cons a (unNonDetC r cons nil)
-  _           -> nil
-{-# INLINE consC #-}
-
diff --git a/src/Polysemy/Output.hs b/src/Polysemy/Output.hs
--- a/src/Polysemy/Output.hs
+++ b/src/Polysemy/Output.hs
@@ -9,8 +9,11 @@
 
     -- * Interpretations
   , runOutputList
+  , runLazyOutputList
   , runOutputMonoid
+  , runLazyOutputMonoid
   , runOutputMonoidAssocR
+  , runLazyOutputMonoidAssocR
   , runOutputMonoidIORef
   , runOutputMonoidTVar
   , outputToIOMonoid
@@ -22,6 +25,7 @@
 
 import Data.IORef
 import Control.Concurrent.STM
+import qualified Control.Monad.Trans.Writer.Lazy as Lazy
 
 import Data.Semigroup (Endo(..))
 import Data.Bifunctor (first)
@@ -29,7 +33,10 @@
 import Polysemy.State
 import Control.Monad (when)
 
+import Polysemy.Internal.Union
+import Polysemy.Internal.Writer
 
+
 ------------------------------------------------------------------------------
 -- | An effect capable of sending messages. Useful for streaming output and for
 -- logging.
@@ -53,7 +60,23 @@
   )
 {-# INLINE runOutputList #-}
 
+
 ------------------------------------------------------------------------------
+-- | Run an 'Output' effect by transforming it into a list of its values,
+-- lazily.
+--
+-- __Warning: This inherits the nasty space leak issue of__
+-- __'Lazy.WriterT'! Don't use this if you don't have to.__
+--
+-- @since 1.3.0.0
+runLazyOutputList
+    :: forall o r a
+     . Sem (Output o ': r) a
+    -> Sem r ([o], a)
+runLazyOutputList = runLazyOutputMonoidAssocR pure
+{-# INLINE runLazyOutputList #-}
+
+------------------------------------------------------------------------------
 -- | Run an 'Output' effect by transforming it into a monoid.
 --
 -- @since 1.0.0.0
@@ -69,7 +92,26 @@
   )
 {-# INLINE runOutputMonoid #-}
 
+
 ------------------------------------------------------------------------------
+-- | Run an 'Output' effect by transforming it into a monoid, and accumulate
+-- it lazily.
+--
+-- __Warning: This inherits the nasty space leak issue of__
+-- __'Lazy.WriterT'! Don't use this if you don't have to.__
+--
+-- @since 1.3.0.0
+runLazyOutputMonoid
+    :: forall o m r a
+     . Monoid m
+    => (o -> m)
+    -> Sem (Output o ': r) a
+    -> Sem r (m, a)
+runLazyOutputMonoid f = interpretViaLazyWriter $ \(Weaving e s _ ex _) ->
+  case e of
+    Output o -> ex s <$ Lazy.tell (f o)
+
+------------------------------------------------------------------------------
 -- | Like 'runOutputMonoid', but right-associates uses of '<>'.
 --
 -- This asymptotically improves performance if the time complexity of '<>' for
@@ -89,6 +131,31 @@
     fmap (first (`appEndo` mempty))
   . runOutputMonoid (\o -> let !o' = f o in Endo (o' <>))
 {-# INLINE runOutputMonoidAssocR #-}
+
+------------------------------------------------------------------------------
+-- | Like 'runLazyOutputMonoid', but right-associates uses of '<>'.
+--
+-- This asymptotically improves performance if the time complexity of '<>' for
+-- the 'Monoid' depends only on the size of the first argument.
+--
+-- You should always use this instead of 'runLazyOutputMonoid' if the monoid
+-- is a list, such as 'String'.
+--
+-- __Warning: This inherits the nasty space leak issue of__
+-- __'Lazy.WriterT'! Don't use this if you don't have to.__
+--
+-- @since 1.3.0.0
+runLazyOutputMonoidAssocR
+    :: forall o m r a
+     . Monoid m
+    => (o -> m)
+    -> Sem (Output o ': r) a
+    -> Sem r (m, a)
+runLazyOutputMonoidAssocR f =
+    fmap (first (`appEndo` mempty))
+  . runLazyOutputMonoid (\o -> let o' = f o in Endo (o' <>))
+                              --   ^ N.B. No bang pattern
+{-# INLINE runLazyOutputMonoidAssocR #-}
 
 ------------------------------------------------------------------------------
 -- | Run an 'Output' effect by transforming it into atomic operations
diff --git a/src/Polysemy/State.hs b/src/Polysemy/State.hs
--- a/src/Polysemy/State.hs
+++ b/src/Polysemy/State.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Polysemy.State
@@ -14,17 +15,23 @@
     -- * Interpretations
   , runState
   , evalState
+  , execState
   , runLazyState
   , evalLazyState
+  , execLazyState
   , runStateIORef
   , stateToIO
+  , runStateSTRef
+  , stateToST
 
     -- * Interoperation with MTL
   , hoistStateIntoStateT
   ) where
 
+import           Control.Monad.ST
 import qualified Control.Monad.Trans.State as S
 import           Data.IORef
+import           Data.STRef
 import           Data.Tuple (swap)
 import           Polysemy
 import           Polysemy.Internal
@@ -85,7 +92,16 @@
 evalState s = fmap snd . runState s
 {-# INLINE evalState #-}
 
+------------------------------------------------------------------------------
+-- | Run a 'State' effect with local state.
+--
+-- @since 1.2.3.1
+execState :: s -> Sem (State s ': r) a -> Sem r s
+execState s = fmap fst . runState s
+{-# INLINE execState #-}
 
+
+
 ------------------------------------------------------------------------------
 -- | Run a 'State' effect with local state, lazily.
 runLazyState :: s -> Sem (State s ': r) a -> Sem r (s, a)
@@ -104,6 +120,16 @@
 
 
 ------------------------------------------------------------------------------
+-- | Run a 'State' effect with local state, lazily.
+--
+-- @since 1.2.3.1
+execLazyState :: s -> Sem (State s ': r) a -> Sem r s
+execLazyState s = fmap fst . runLazyState s
+{-# INLINE execLazyState #-}
+
+
+
+------------------------------------------------------------------------------
 -- | Run a 'State' effect by transforming it into operations over an 'IORef'.
 --
 -- /Note/: This is not safe in a concurrent setting, as 'modify' isn't atomic.
@@ -156,6 +182,61 @@
   end <- embed $ readIORef ref
   return (end, res)
 {-# INLINE stateToIO #-}
+
+------------------------------------------------------------------------------
+-- | Run a 'State' effect by transforming it into operations over an 'STRef'.
+--
+-- @since 1.3.0.0
+runStateSTRef
+    :: forall s st r a
+     . Member (Embed (ST st)) r
+    => STRef st s
+    -> Sem (State s ': r) a
+    -> Sem r a
+runStateSTRef ref = interpret $ \case
+  Get   -> embed $ readSTRef ref
+  Put s -> embed $ writeSTRef ref s
+{-# INLINE runStateSTRef #-}
+
+--------------------------------------------------------------------
+-- | Run an 'State' effect in terms of operations
+-- in 'ST'.
+--
+-- Internally, this simply creates a new 'STRef', passes it to
+-- 'runStateSTRef', and then returns the result and the final value
+-- of the 'STRef'.
+--
+-- /Beware/: As this uses an 'STRef' internally,
+-- all other effects will have local
+-- state semantics in regards to 'State' effects
+-- interpreted this way.
+-- For example, 'Polysemy.Error.throw' and 'Polysemy.Error.catch' will
+-- never revert 'put's, even if 'Polysemy.Error.runError' is used
+-- after 'stateToST'.
+--
+-- When not using the plugin, one must introduce the existential @st@ type to
+-- 'stateToST', so that the resulting type after 'runM' can be resolved into
+-- @forall st. ST st (s, a)@ for use with 'runST'. Doing so requires
+-- @-XScopedTypeVariables@.
+--
+-- @
+-- stResult :: forall s a. (s, a)
+-- stResult = runST ( (runM $ stateToST \@_ \@st undefined $ pure undefined) :: forall st. ST st (s, a) )
+-- @
+--
+-- @since 1.3.0.0
+stateToST
+    :: forall s st r a
+     . Member (Embed (ST st)) r
+    => s
+    -> Sem (State s ': r) a
+    -> Sem r (s, a)
+stateToST s sem = do
+  ref <- embed @(ST st) $ newSTRef s
+  res <- runStateSTRef ref sem
+  end <- embed $ readSTRef ref
+  return (end, res)
+{-# INLINE stateToST #-}
 
 ------------------------------------------------------------------------------
 -- | Hoist a 'State' effect into a 'S.StateT' monad transformer. This can be
diff --git a/src/Polysemy/State/Law.hs b/src/Polysemy/State/Law.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/State/Law.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Polysemy.State.Law where
+
+import Polysemy
+import Polysemy.Law
+import Polysemy.State
+import Control.Applicative
+import Control.Arrow
+
+
+------------------------------------------------------------------------------
+-- | A collection of laws that show a `State` interpreter is correct.
+prop_lawfulState
+    :: forall r s
+     . (Eq s, Show s, Arbitrary s, MakeLaw (State s) r)
+    => InterpreterFor (State s) r
+    -> Property
+prop_lawfulState i12n = conjoin
+  [ runLaw i12n law_putTwice
+  , runLaw i12n law_getTwice
+  , runLaw i12n law_getPutGet
+  ]
+
+
+law_putTwice
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_putTwice =
+  mkLaw
+    "put %1 >> put %2 >> get"
+    (\s s' -> put @s s >> put @s s' >> get @s)
+    "put %2 >> get"
+    (\_ s' ->             put @s s' >> get @s)
+
+law_getTwice
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_getTwice =
+  mkLaw
+    "liftA2 (,) get get"
+    (liftA2 (,) (get @s) (get @s))
+    "(id &&& id) <$> get"
+    ((id &&& id) <$> get @s)
+
+law_getPutGet
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_getPutGet =
+  mkLaw
+    "get >>= put >> get"
+    (get @s >>= put @s >> get @s)
+    "get"
+    (get @s)
+
diff --git a/src/Polysemy/Tagged.hs b/src/Polysemy/Tagged.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Tagged.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Polysemy.Tagged
+  (
+    -- * Effect
+    Tagged (..)
+
+    -- * Actions
+  , tag
+  , tagged
+
+    -- * Interpretations
+  , untag
+  , retag
+  ) where
+
+import Polysemy
+import Polysemy.Internal
+import Polysemy.Internal.Union
+
+
+------------------------------------------------------------------------------
+-- | An effect for annotating effects and disambiguating identical effects.
+newtype Tagged k e m a where
+  Tagged :: forall k e m a. e m a -> Tagged k e m a
+
+
+------------------------------------------------------------------------------
+-- | Tag uses of an effect, effectively gaining access to the
+-- tagged effect locally.
+--
+-- This may be used to create @tagged-@ variants of regular actions.
+--
+-- For example:
+--
+-- @
+-- taggedLocal :: forall k i r a
+--              . 'Member' ('Tagged' k ('Polysemy.Reader.Reader' i)) r
+--             => (i -> i)
+--             -> 'Sem' r a
+--             -> 'Sem' r a
+-- taggedLocal f m =
+--   'tag' @k @('Polysemy.Reader.Reader' i) $ 'Polysemy.Reader.local' @i f ('raise' m)
+-- @
+--
+tag
+    :: forall k e r a
+     . Member (Tagged k e) r
+    => Sem (e ': r) a
+    -> Sem r a
+tag = hoistSem $ \u -> case decomp u of
+  Right (Weaving e s wv ex ins) ->
+    injWeaving $ Weaving (Tagged @k e) s (tag @k . wv) ex ins
+  Left g -> hoist (tag @k) g
+{-# INLINE tag #-}
+
+
+------------------------------------------------------------------------------
+-- | A reinterpreting version of 'tag'.
+tagged
+    :: forall k e r a
+     . Sem (e ': r) a
+    -> Sem (Tagged k e ': r) a
+tagged = hoistSem $ \u ->
+  case decompCoerce u of
+    Right (Weaving e s wv ex ins) ->
+      injWeaving $ Weaving (Tagged @k e) s (tagged @k . wv) ex ins
+    Left g -> hoist (tagged @k) g
+{-# INLINE tagged #-}
+
+
+
+------------------------------------------------------------------------------
+-- | Run a @'Tagged' k e@ effect through reinterpreting it to @e@
+untag
+    :: forall k e r a
+     . Sem (Tagged k e ': r) a
+    -> Sem (e ': r) a
+-- TODO(KingoftheHomeless): I think this is safe to replace with 'unsafeCoerce',
+-- but doing so probably worsens performance, as it hampers optimizations.
+-- 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 Here (Weaving e s (untag . wv) ex ins)
+  Left g -> hoist untag g
+{-# INLINE untag #-}
+
+
+------------------------------------------------------------------------------
+-- | Transform a @'Tagged' k1 e@ effect into a @'Tagged' k2 e@ effect
+retag
+    :: forall k1 k2 e r a
+     . Member (Tagged k2 e) r
+    => Sem (Tagged k1 e ': r) a
+    -> Sem r a
+retag = hoistSem $ \u -> case decomp u of
+  Right (Weaving (Tagged e) s wv ex ins) ->
+    injWeaving $ Weaving (Tagged @k2 e) s (retag @_ @k2 . wv) ex ins
+  Left g -> hoist (retag @_ @k2) g
+{-# INLINE retag #-}
+
diff --git a/src/Polysemy/Trace.hs b/src/Polysemy/Trace.hs
--- a/src/Polysemy/Trace.hs
+++ b/src/Polysemy/Trace.hs
@@ -77,16 +77,17 @@
 
 
 ------------------------------------------------------------------------------
--- | Transform an 'Output' 'String' effect into a 'Trace' effect.
+-- | Transform an @'Output' w@ effect into a 'Trace' effect given a function
+-- to transform each @w@ to a 'String'.
 --
 -- @since 1.0.0.0
 outputToTrace
-    :: ( Show w
-       , Member Trace r
-       )
-    => Sem (Output w ': r) a
-    -> Sem r a
-outputToTrace = interpret $ \case
-  Output m -> trace $ show m
+  :: forall w r a
+   . Member Trace r
+  => (w -> String)
+  -> Sem (Output w ': r) a
+  -> Sem r a
+outputToTrace show' = interpret $ \case
+  Output m -> trace $ show' m
 {-# INLINE outputToTrace #-}
 
diff --git a/src/Polysemy/View.hs b/src/Polysemy/View.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/View.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Polysemy.View
+  ( -- * Effect
+    View (..)
+
+    -- * Actions
+  , see
+
+    -- * Interpretations
+  , viewToState
+  , viewToInput
+  ) where
+
+import Polysemy
+import Polysemy.Input
+import Polysemy.State
+import Polysemy.Tagged
+
+
+------------------------------------------------------------------------------
+-- | A 'View' is an expensive computation that should be cached.
+data View v m a where
+  See :: View v m v
+
+makeSem ''View
+
+
+------------------------------------------------------------------------------
+-- | Transform a 'View' into an 'Input'.
+viewToInput
+    :: forall v i r a
+     . Member (Input i) r
+    => (i -> v)
+    -> Sem (View v ': r) a
+    -> Sem r a
+viewToInput f = interpret $ \case
+  See -> f <$> input
+
+
+------------------------------------------------------------------------------
+-- | Get a 'View' as an exensive computation over an underlying 'State' effect.
+-- This 'View' is only invalidated when the underlying 'State' changes.
+viewToState
+    :: forall v s r a
+     . Member (State s) r
+    => (s -> Sem r v)
+    -> Sem (View v ': r) a
+    -> Sem r a
+viewToState f = do
+  evalState Dirty
+    . untag @"view" @(State (Cached v))
+    . intercept @(State s)
+      ( \case
+        Get -> get
+        Put s -> do
+          put s
+          tag @"view" @(State (Cached v)) $ put $ Dirty @v
+      )
+    . reinterpret @(View v)
+      ( \case
+          See -> do
+            dirty <- tagged @"view" $ get @(Cached v)
+            case dirty of
+              Dirty -> do
+                s <- get
+                v' <- raise $ f s
+                tagged @"view" $ put $ Cached v'
+                pure v'
+              Cached v -> pure v
+      )
+
+
+data Cached a = Cached a | Dirty
+  deriving (Eq, Ord, Show, Functor)
+
diff --git a/src/Polysemy/Writer.hs b/src/Polysemy/Writer.hs
--- a/src/Polysemy/Writer.hs
+++ b/src/Polysemy/Writer.hs
@@ -12,7 +12,9 @@
 
     -- * Interpretations
   , runWriter
+  , runLazyWriter
   , runWriterAssocR
+  , runLazyWriterAssocR
   , runWriterTVar
   , writerToIOFinal
   , writerToIOAssocRFinal
@@ -23,6 +25,7 @@
   ) where
 
 import Control.Concurrent.STM
+import qualified Control.Monad.Trans.Writer.Lazy as Lazy
 
 import Data.Bifunctor (first)
 import Data.Semigroup
@@ -31,6 +34,7 @@
 import Polysemy.Output
 import Polysemy.State
 
+import Polysemy.Internal.Union
 import Polysemy.Internal.Writer
 
 
@@ -55,7 +59,8 @@
 
 
 ------------------------------------------------------------------------------
--- | Run a 'Writer' effect in the style of 'Control.Monad.Trans.Writer.WriterT'
+-- | Run a 'Writer' effect in the style of
+-- 'Control.Monad.Trans.Writer.Strict.WriterT'
 -- (but without the nasty space leak!)
 runWriter
     :: Monoid o
@@ -81,6 +86,35 @@
   )
 {-# INLINE runWriter #-}
 
+
+------------------------------------------------------------------------------
+-- | Run a 'Writer' effect in the style of 'Control.Monad.Trans.Writer.WriterT'
+-- lazily.
+--
+-- __Warning: This inherits the nasty space leak issue of__
+-- __'Lazy.WriterT'! Don't use this if you don't have to.__
+--
+-- @since 1.3.0.0
+runLazyWriter
+    :: forall o r a
+     . Monoid o
+    => Sem (Writer o ': r) a
+    -> Sem r (o, a)
+runLazyWriter = interpretViaLazyWriter $ \(Weaving e s wv ex ins) ->
+  case e of
+    Tell o   -> ex s <$ Lazy.tell o
+    Listen m -> do
+      let m' = wv (m <$ s)
+      ~(fa, o) <- Lazy.listen m'
+      return $ ex $ (,) o <$> fa
+    Pass m -> do
+      let m' = wv (m <$ s)
+      Lazy.pass $ do
+        ft <- m'
+        let f = maybe id fst (ins ft)
+        return (ex (fmap snd ft), f)
+{-# INLINE runLazyWriter #-}
+
 -----------------------------------------------------------------------------
 -- | Like 'runWriter', but right-associates uses of '<>'.
 --
@@ -101,6 +135,31 @@
   . writerToEndoWriter
   . raiseUnder
 {-# INLINE runWriterAssocR #-}
+
+
+-----------------------------------------------------------------------------
+-- | Like 'runLazyWriter', but right-associates uses of '<>'.
+--
+-- This asymptotically improves performance if the time complexity of '<>'
+-- for the 'Monoid' depends only on the size of the first argument.
+--
+-- You should always use this instead of 'runLazyWriter' if the monoid
+-- is a list, such as 'String'.
+--
+-- __Warning: This inherits the nasty space leak issue of__
+-- __'Lazy.WriterT'! Don't use this if you don't have to.__
+--
+-- @since 1.3.0.0
+runLazyWriterAssocR
+    :: Monoid o
+    => Sem (Writer o ': r) a
+    -> Sem r (o, a)
+runLazyWriterAssocR =
+    (fmap . first) (`appEndo` mempty)
+  . runLazyWriter
+  . writerToEndoWriter
+  . raiseUnder
+{-# INLINE runLazyWriterAssocR #-}
 
 --------------------------------------------------------------------
 -- | Transform a 'Writer' effect into atomic operations
diff --git a/test/AlternativeSpec.hs b/test/AlternativeSpec.hs
--- a/test/AlternativeSpec.hs
+++ b/test/AlternativeSpec.hs
@@ -5,6 +5,7 @@
 import Test.Hspec
 import Control.Applicative
 import Polysemy.Trace
+import Polysemy.Reader
 
 runAlt :: Alternative f => Sem '[NonDet] a -> f a
 runAlt = run . runNonDet
@@ -17,6 +18,12 @@
            => Sem r ()
 failtrace' = trace "sim" *> empty <|> trace "salabim"
 
+inHigherOrder :: Members '[NonDet, Trace, Reader ()] r
+              => Sem r ()
+inHigherOrder = do
+  local (\_ -> ()) $ trace "1" <|> trace "2"
+  trace "3"
+
 spec :: Spec
 spec = parallel $ do
   describe "Alternative instance" $ do
@@ -38,3 +45,13 @@
         `shouldBe` Just (["salabim"], ())
       (run . runTraceList . runNonDetMaybe) failtrace'
         `shouldBe` (["sim", "salabim"], Just ())
+
+  describe "runNonDet" $ do
+    it "should have terrible semantics when <|> is used within\
+       \ a higher-order action of a later effect (See Issue #246.)" $ do
+      (fst . run . runTraceList . runReader () . runNonDet @[]) inHigherOrder
+        `shouldBe` ["1","2","3","3"]
+      (fst . run . runTraceList . runReader () . runNonDet @[]) inHigherOrder
+        `shouldNotBe` ["1","3","2","3"] -- This is what we actually WANT it to be.
+      (fst . run . runTraceList . runNonDet @[] . runReader ()) inHigherOrder
+        `shouldBe` ["1","3","2","3"]
diff --git a/test/ErrorSpec.hs b/test/ErrorSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/ErrorSpec.hs
@@ -0,0 +1,38 @@
+module ErrorSpec where
+
+import qualified Control.Exception as X
+import           Polysemy
+import           Polysemy.Error
+import           Polysemy.Resource
+import           Test.Hspec
+
+newtype MyExc = MyExc String
+  deriving (Show, Eq)
+
+instance X.Exception MyExc
+
+spec :: Spec
+spec = parallel $ do
+  describe "fromException" $ do
+    it "should catch exceptions" $ do
+      a <-
+        runM $ runError $ fromException @MyExc $ do
+          _ <- X.throwIO $ MyExc "hello"
+          pure ()
+      a `shouldBe` (Left $ MyExc "hello")
+
+    it "should not catch non-exceptions" $ do
+      a <-
+        runM $ runError @MyExc $ fromException @MyExc $ pure ()
+      a `shouldBe` Right ()
+
+    it "should happen before Resource" $ do
+      a <-
+        runM $ resourceToIO $ runError @MyExc $ do
+          onException
+            (fromException @MyExc $ do
+              _ <- X.throwIO $ MyExc "hello"
+              pure ()
+            ) $ pure $ error "this exception shouldn't happen"
+      a `shouldBe` (Left $ MyExc "hello")
+
diff --git a/test/FusionSpec.hs b/test/FusionSpec.hs
--- a/test/FusionSpec.hs
+++ b/test/FusionSpec.hs
@@ -35,11 +35,11 @@
 spec :: Spec
 spec = parallel $ do
   describe "fusion" $ do
-#if __GLASGOW_HASKELL__ >= 807
-    -- TODO: Investigate why this test fails mysteriously on GHC < 8.6
-    it "Union proofs should simplify" $ do
-      shouldSucceed $(inspectTest $ 'countDown `hasNoType` ''SNat)
-#endif
+-- #if __GLASGOW_HASKELL__ >= 807
+--     -- TODO: Investigate why this test fails mysteriously on GHC < 8.6
+--     it "Union proofs should simplify" $ do
+--       shouldSucceed $(inspectTest $ 'countDown `hasNoType` ''SNat)
+-- #endif
 
     it "internal uses of StateT should simplify" $ do
       shouldSucceed $(inspectTest $ 'countDown `doesNotUse` ''S.StateT)
@@ -57,14 +57,14 @@
       shouldSucceed $(inspectTest $ 'jank `doesNotUse` 'Sem)
       shouldSucceed $(inspectTest $ 'tryIt `doesNotUse` 'Sem)
 
-#if __GLASGOW_HASKELL__ >= 807
-    it "who needs Weaving even?" $ do
-      shouldSucceed $(inspectTest $ 'jank `doesNotUse` 'Weaving)
-      shouldSucceed $(inspectTest $ 'countDown `doesNotUse` 'Weaving)
-#if __GLASGOW_HASKELL__ >= 810
-      shouldSucceed $(inspectTest $ 'tryIt `doesNotUse` 'Weaving)
-#endif
-#endif
+-- #if __GLASGOW_HASKELL__ >= 807
+--     it "who needs Weaving even?" $ do
+--       shouldSucceed $(inspectTest $ 'jank `doesNotUse` 'Weaving)
+--       shouldSucceed $(inspectTest $ 'countDown `doesNotUse` 'Weaving)
+-- #if __GLASGOW_HASKELL__ >= 810
+--       shouldSucceed $(inspectTest $ 'tryIt `doesNotUse` 'Weaving)
+-- #endif
+-- #endif
 
 
 go :: Sem '[State Int] Int
diff --git a/test/KnownRowSpec.hs b/test/KnownRowSpec.hs
new file mode 100644
--- /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"
diff --git a/test/LawsSpec.hs b/test/LawsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/LawsSpec.hs
@@ -0,0 +1,20 @@
+module LawsSpec where
+
+import Polysemy
+import Polysemy.Law
+import Polysemy.State
+import Polysemy.State.Law
+import Test.Hspec
+
+spec :: Spec
+spec = parallel $ do
+  describe "State effects" $ do
+    it "runState should pass the laws" $
+      property $ prop_lawfulState @'[] $ fmap snd . runState @Int 0
+
+    it "runLazyState should pass the laws" $
+      property $ prop_lawfulState @'[] $ fmap snd . runLazyState @Int 0
+
+    it "stateToIO should pass the laws" $
+      property $ prop_lawfulState @'[Embed IO] $ fmap snd . stateToIO @Int 0
+
diff --git a/test/ViewSpec.hs b/test/ViewSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/ViewSpec.hs
@@ -0,0 +1,40 @@
+module ViewSpec where
+
+import Polysemy
+import Polysemy.State
+import Polysemy.Trace
+import Polysemy.View
+import Test.Hspec
+
+
+check_see :: Members '[View String, Trace] r => Sem r ()
+check_see = trace . ("saw " ++) =<< see
+
+spec :: Spec
+spec = parallel $ do
+  describe "View effect" $ do
+    it "should cache views" $ do
+      let a = run
+            . runTraceList
+            . runState @Int 0
+            . viewToState @String @Int (\i -> do
+                  trace $ "caching "  ++ show i
+                  pure $ show i  ) $ do
+              check_see
+              check_see
+              put @Int 3
+              trace "it's lazy"
+              put @Int 5
+              check_see
+              check_see
+              get @Int
+
+      a `shouldBe` ([ "caching 0"
+                    , "saw 0"
+                    , "saw 0"
+                    , "it's lazy"
+                    , "caching 5"
+                    , "saw 5"
+                    , "saw 5"
+                    ], (5, 5))
+
diff --git a/test/WriterSpec.hs b/test/WriterSpec.hs
--- a/test/WriterSpec.hs
+++ b/test/WriterSpec.hs
@@ -11,6 +11,7 @@
 import Polysemy
 import Polysemy.Async
 import Polysemy.Error
+import Polysemy.Input
 import Polysemy.Writer
 
 censor' :: forall e s a r
@@ -156,3 +157,44 @@
       Right end2 <- runFinal . runError $ test6
       end1 `shouldBe` "message has been received"
       end2 `shouldBe` "message has been received"
+
+  describe "runLazyWriter" $ do
+    let
+      runLazily     = run . runInputConst () . runLazyWriter @[Int]
+      runSemiLazily = runLazily . runError @()
+      runStrictly   = run . runError @() . runLazyWriter @[Int]
+      runStrictlyM  = runM . runLazyWriter @[Int]
+
+      act :: Member (Writer [Int]) r => Sem r ()
+      act = do
+        tell @[Int] [1]
+        tell @[Int] [2]
+        error "strict"
+
+    it "should build the final output lazily, if the interpreters after \
+       \runLazyWriter and the final monad are lazy" $ do
+      (take 2 . fst . runLazily) act `shouldBe` [1,2]
+      (take 2 . fst . runSemiLazily) act `shouldBe` [1,2]
+      evaluate (runStrictly act) `shouldThrow` errorCall "strict"
+      runStrictlyM act `shouldThrow` errorCall "strict"
+
+    it "should listen lazily if all interpreters and final monad are lazy" $ do
+      let
+        listenAct :: Member (Writer [Int]) r => Sem r [Int]
+        listenAct = do
+          (end,_) <- listen @[Int] act
+          return (take 2 end)
+      (snd . runLazily) listenAct `shouldBe` [1,2]
+
+      evaluate ((snd . runSemiLazily) listenAct) `shouldThrow` errorCall "strict"
+      evaluate (runStrictly listenAct) `shouldThrow` errorCall "strict"
+      runStrictlyM listenAct `shouldThrow` errorCall "strict"
+
+    it "should censor lazily if all interpreters and final monad are lazy" $ do
+      let
+        censorAct :: Member (Writer [Int]) r => Sem r ()
+        censorAct = censor @[Int] (\(_:y:_) -> [0,y]) act
+      (fst . runLazily) censorAct `shouldBe` [0,2]
+      evaluate ((fst . runSemiLazily) censorAct) `shouldThrow` errorCall "strict"
+      evaluate (runStrictly censorAct) `shouldThrow` errorCall "strict"
+      runStrictlyM censorAct `shouldThrow` errorCall "strict"
