diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,29 @@
 # Changelog for polysemy
 
+## 0.5.0.0 (2019-06-26)
+
+### Breaking Changes
+
+- Removed the internal `Effect` machinery
+
+### New Effects and Interpretations
+
+- New effect; `Async`, for describing asynchronous computations
+- New interpretation for `Resource`: `runResourceBase`, which can lower
+    `Resource` effects without giving a lowering natural transformation
+- New interpretation for `Trace`: `runTraceAsList`
+- New combinator: `withLowerToIO`, which is capable of transforming
+    `IO`-invariant functions as effects.
+
+### Other Changes
+
+- Lots of hard work on the package and CI infrastructure to make it green on
+    GHC 8.4.4 (thanks to @jkachmar)
+- Changed the order of the types for `runMonadicInput` to be more helpful
+    (thanks to @tempname11)
+- Improved the error machinery to be more selective about when it runs
+- Factored out the TH into a common library for third-party consumers
+
 ## 0.4.0.0 (2019-06-12)
 
 ### Breaking Changes
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@
 
 # polysemy
 
-[![Build Status](https://api.travis-ci.org/isovector/polysemy.svg?branch=master)](https://travis-ci.org/isovector/polysemy)
+[![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)
 
@@ -35,7 +35,7 @@
 
 Additionally, unlike `mtl`, `polysemy` has no functional dependencies, so you
 can use multiple copies of the same effect. This alleviates the need for ~~ugly
-hacks~~band-aids like [classy
+hacks~~ band-aids like [classy
 lenses](http://hackage.haskell.org/package/lens-4.17.1/docs/Control-Lens-TH.html#v:makeClassy),
 the [`ReaderT`
 pattern](https://www.fpcomplete.com/blog/2017/06/readert-design-pattern) and
diff --git a/bench/Poly.hs b/bench/Poly.hs
--- a/bench/Poly.hs
+++ b/bench/Poly.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BlockArguments   #-}
 {-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs            #-}
@@ -57,7 +56,9 @@
 runConsoleBoring inputs
   = runFoldMapOutput (:[])
   . runListInput inputs
-  . reinterpret2 \case
+  . reinterpret2
+  (\case
       ReadLine -> maybe "" id <$> input
       WriteLine msg -> output msg
+  )
 
diff --git a/polysemy.cabal b/polysemy.cabal
--- a/polysemy.cabal
+++ b/polysemy.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.1.
+-- This file has been generated from package.yaml by hpack version 0.31.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 4be5160aee3aafedfc1de37204f6dbea8e61f8aceaee0deaa59520e662451bd3
+-- hash: 5871506acb960e1595dcd500e8680727e555c25cfbd825e98b767b01c91cffc9
 
 name:           polysemy
-version:        0.4.0.0
+version:        0.5.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
@@ -40,17 +40,20 @@
 library
   exposed-modules:
       Polysemy
+      Polysemy.Async
       Polysemy.Error
       Polysemy.Fixpoint
       Polysemy.Input
       Polysemy.Internal
       Polysemy.Internal.Combinators
       Polysemy.Internal.CustomErrors
-      Polysemy.Internal.Effect
       Polysemy.Internal.Fixpoint
+      Polysemy.Internal.Forklift
+      Polysemy.Internal.Kind
       Polysemy.Internal.Lift
       Polysemy.Internal.NonDet
       Polysemy.Internal.Tactics
+      Polysemy.Internal.TH.Common
       Polysemy.Internal.TH.Effect
       Polysemy.Internal.Union
       Polysemy.IO
@@ -68,19 +71,29 @@
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   ghc-options: -Wall
   build-depends:
-      base >=4.7 && <5
-    , containers >=0.6 && <=0.7
+      async >=2.2 && <3
+    , base >=4.9 && <5
+    , containers >=0.5 && <0.7
+    , first-class-families >=0.5.0.0 && <0.6
     , mtl >=2.2.2 && <3
-    , syb >=0.7 && <=0.8
-    , template-haskell >=2.14.0.0 && <2.15
-    , th-abstraction >=0.3 && <=0.4
-    , transformers >=0.5.5.0 && <0.6
+    , syb >=0.7 && <0.8
+    , template-haskell >=2.12.0.0 && <3
+    , th-abstraction >=0.3.1.0 && <0.4
+    , transformers >=0.5.2.0 && <0.6
+    , unagi-chan >=0.4.0.0 && <0.5
+  if impl(ghc < 8.6)
+    default-extensions: MonadFailDesugaring TypeInType
   if flag(dump-core)
     ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
     build-depends:
         dump-core
+  if impl(ghc < 8.2.2)
+    build-depends:
+        unsupported-ghc-version >1 && <1
   if flag(error-messages)
-    cpp-options: -DERROR_MESSAGES
+    cpp-options: -DCABAL_SERIOUSLY_CMON_MATE
+  else
+    cpp-options: -DNO_ERROR_MESSAGES
   default-language: Haskell2010
 
 test-suite polysemy-test
@@ -88,28 +101,39 @@
   main-is: Main.hs
   other-modules:
       AlternativeSpec
+      AsyncSpec
       BracketSpec
+      DoctestSpec
       FusionSpec
       HigherOrderSpec
       InspectorSpec
       OutputSpec
       ThEffectSpec
+      TypeErrors
       Paths_polysemy
   hs-source-dirs:
       test
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-tool-depends:
+      hspec-discover:hspec-discover >=2.0
   build-depends:
-      base >=4.7 && <5
-    , containers >=0.6 && <=0.7
+      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.6
     , hspec >=2.6.0 && <3
-    , inspection-testing >=0.4.1.1 && <0.5
+    , inspection-testing >=0.4.2 && <0.5
     , mtl >=2.2.2 && <3
     , polysemy
-    , syb >=0.7 && <=0.8
-    , template-haskell >=2.14.0.0 && <2.15
-    , th-abstraction >=0.3 && <=0.4
-    , transformers >=0.5.5.0 && <0.6
+    , syb >=0.7 && <0.8
+    , template-haskell >=2.12.0.0 && <3
+    , th-abstraction >=0.3.1.0 && <0.4
+    , transformers >=0.5.2.0 && <0.6
+    , unagi-chan >=0.4.0.0 && <0.5
+  if impl(ghc < 8.6)
+    default-extensions: MonadFailDesugaring TypeInType
   default-language: Haskell2010
 
 benchmark polysemy-bench
@@ -122,15 +146,20 @@
       bench
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   build-depends:
-      base >=4.7 && <5
-    , containers >=0.6 && <=0.7
+      async >=2.2 && <3
+    , base >=4.9 && <5
+    , containers >=0.5 && <0.7
     , criterion
+    , first-class-families >=0.5.0.0 && <0.6
     , free
     , freer-simple
     , mtl
     , polysemy
-    , syb >=0.7 && <=0.8
-    , template-haskell >=2.14.0.0 && <2.15
-    , th-abstraction >=0.3 && <=0.4
-    , transformers >=0.5.5.0 && <0.6
+    , syb >=0.7 && <0.8
+    , template-haskell >=2.12.0.0 && <3
+    , th-abstraction >=0.3.1.0 && <0.4
+    , transformers >=0.5.2.0 && <0.6
+    , unagi-chan >=0.4.0.0 && <0.5
+  if impl(ghc < 8.6)
+    default-extensions: MonadFailDesugaring TypeInType
   default-language: Haskell2010
diff --git a/src/Polysemy.hs b/src/Polysemy.hs
--- a/src/Polysemy.hs
+++ b/src/Polysemy.hs
@@ -3,6 +3,7 @@
     Sem ()
   , Member
   , Members
+  , LastMember
 
   -- * Running Sem
   , run
@@ -35,7 +36,7 @@
     -- to generate smart constructors for the actions. These smart constructors
     -- can be invoked directly inside of the 'Sem' monad.
     --
-    -- >>> makeSem ''Console
+    -- > makeSem ''Console
     --
     -- results in the following definitions:
     --
@@ -63,7 +64,7 @@
     -- where 'Polysemy.Error.Catch' is an action that can run an exception
     -- handler if its first argument calls 'Polysemy.Error.throw'.
     --
-    -- >>> makeSem ''Error
+    -- > makeSem ''Error
     --
     -- @
     -- 'Polysemy.Error.throw' :: 'Member' ('Polysemy.Error.Error' e) r => e -> 'Sem' r a
@@ -88,6 +89,13 @@
   , reinterpret2H
   , reinterpret3H
 
+    -- * Combinators for Interpreting Directly to IO
+  , withLowerToIO
+
+    -- * Kind Synonyms
+  , Effect
+  , EffectRow
+
     -- * Composing IO-based Interpreters
   , (.@)
   , (.@@)
@@ -113,6 +121,9 @@
 
 import Polysemy.Internal
 import Polysemy.Internal.Combinators
+import Polysemy.Internal.Forklift
+import Polysemy.Internal.Kind
 import Polysemy.Internal.TH.Effect
 import Polysemy.Internal.Tactics
+import Polysemy.Internal.Union
 
diff --git a/src/Polysemy/Async.hs b/src/Polysemy/Async.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Async.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Polysemy.Async
+  ( -- * Effect
+    Async (..)
+
+    -- * Actions
+  , async
+  , await
+
+    -- * Interpretations
+  , runAsync
+  , runAsyncInIO
+  ) where
+
+import qualified Control.Concurrent.Async as A
+import           Polysemy
+
+
+
+------------------------------------------------------------------------------
+-- | An effect for spawning asynchronous computations.
+--
+-- The 'Maybe' returned by 'async' is due to the fact that we can't be sure an
+-- 'Polysemy.Error.Error' effect didn't fail locally.
+--
+-- @since 0.5.0.0
+data Async m a where
+  Async :: m a -> Async m (A.Async (Maybe a))
+  Await :: A.Async a -> Async m a
+
+makeSem ''Async
+
+------------------------------------------------------------------------------
+-- | A more flexible --- though less performant ---  version of 'runAsyncInIO'.
+--
+-- This function is capable of running 'Async' effects anywhere within an
+-- effect stack, without relying on an explicit function to lower it into 'IO'.
+-- Notably, this means that 'Polysemy.State.State' effects will be consistent
+-- in the presence of 'Async'.
+--
+-- @since 0.5.0.0
+runAsync
+    :: LastMember (Lift IO) r
+    => Sem (Async ': r) a
+    -> Sem r a
+runAsync m = withLowerToIO $ \lower _ -> lower $
+  interpretH
+    ( \case
+        Async a -> do
+          ma  <- runT a
+          ins <- getInspectorT
+          fa  <- sendM $ A.async $ lower $ runAsync_b ma
+          pureT $ fmap (inspect ins) fa
+
+        Await a -> pureT =<< sendM (A.wait a)
+    )  m
+{-# INLINE runAsync #-}
+
+
+runAsync_b
+    :: LastMember (Lift IO) r
+    => Sem (Async ': r) a
+    -> Sem r a
+runAsync_b = runAsync
+{-# NOINLINE runAsync_b #-}
+
+
+------------------------------------------------------------------------------
+-- | Run an 'Async' effect via in terms of 'A.async'.
+--
+--
+-- @since 0.5.0.0
+runAsyncInIO
+    :: Member (Lift IO) r
+    => (forall x. Sem r x -> IO x)
+       -- ^ Strategy for lowering a 'Sem' action down to 'IO'. This is likely
+       -- some combination of 'runM' and other interpreters composed via '.@'.
+    -> Sem (Async ': r) a
+    -> Sem r a
+runAsyncInIO lower m = interpretH
+    ( \case
+        Async a -> do
+          ma  <- runT a
+          ins <- getInspectorT
+          fa  <- sendM $ A.async $ lower $ runAsyncInIO_b lower ma
+          pureT $ fmap (inspect ins) fa
+
+        Await a -> pureT =<< sendM (A.wait a)
+    )  m
+{-# INLINE runAsyncInIO #-}
+
+runAsyncInIO_b
+    :: Member (Lift IO) r
+    => (forall x. Sem r x -> IO x)
+    -> Sem (Async ': r) a
+    -> Sem r a
+runAsyncInIO_b = runAsyncInIO
+{-# NOINLINE runAsyncInIO_b #-}
+
diff --git a/src/Polysemy/Error.hs b/src/Polysemy/Error.hs
--- a/src/Polysemy/Error.hs
+++ b/src/Polysemy/Error.hs
@@ -20,7 +20,6 @@
 import           Data.Typeable
 import           Polysemy
 import           Polysemy.Internal
-import           Polysemy.Internal.Effect
 import           Polysemy.Internal.Union
 
 
diff --git a/src/Polysemy/Input.hs b/src/Polysemy/Input.hs
--- a/src/Polysemy/Input.hs
+++ b/src/Polysemy/Input.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BlockArguments  #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Polysemy.Input
@@ -31,7 +30,7 @@
 ------------------------------------------------------------------------------
 -- | Run an 'Input' effect by always giving back the same value.
 runConstInput :: i -> Sem (Input i ': r) a -> Sem r a
-runConstInput c = interpret \case
+runConstInput c = interpret $ \case
   Input -> pure c
 {-# INLINE runConstInput #-}
 
@@ -43,18 +42,20 @@
     :: [i]
     -> Sem (Input (Maybe i) ': r) a
     -> Sem r a
-runListInput is = fmap snd . runState is . reinterpret \case
-  Input -> do
-    s <- gets uncons
-    for_ s $ put . snd
-    pure $ fmap fst s
+runListInput is = fmap snd . runState is . reinterpret
+  (\case
+      Input -> do
+        s <- gets uncons
+        for_ s $ put . snd
+        pure $ fmap fst s
+  )
 {-# INLINE runListInput #-}
 
 
 ------------------------------------------------------------------------------
 -- | Runs an 'Input' effect by evaluating a monadic action for each request.
-runMonadicInput :: Sem r i -> Sem (Input i ': r) a -> Sem r a
-runMonadicInput m = interpret \case
+runMonadicInput :: forall i r a. Sem r i -> Sem (Input i ': r) a -> Sem r a
+runMonadicInput m = interpret $ \case
   Input -> m
 {-# INLINE runMonadicInput #-}
 
diff --git a/src/Polysemy/Internal.hs b/src/Polysemy/Internal.hs
--- a/src/Polysemy/Internal.hs
+++ b/src/Polysemy/Internal.hs
@@ -33,7 +33,6 @@
 import Control.Monad.IO.Class
 import Data.Functor.Identity
 import Data.Kind
-import Polysemy.Internal.Effect
 import Polysemy.Internal.Fixpoint
 import Polysemy.Internal.Lift
 import Polysemy.Internal.NonDet
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
@@ -26,7 +26,6 @@
 import qualified Control.Monad.Trans.State.Strict as S
 import           Polysemy.Internal
 import           Polysemy.Internal.CustomErrors
-import           Polysemy.Internal.Effect
 import           Polysemy.Internal.Tactics
 import           Polysemy.Internal.Union
 
@@ -148,7 +147,8 @@
 --
 -- See the notes on 'Tactical' for how to use this function.
 reinterpretH
-    :: (∀ m x. e1 m x -> Tactical e1 m (e2 ': r) x)
+    :: forall e1 e2 r a
+     . (∀ m x. e1 m x -> Tactical e1 m (e2 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effect.
     -> Sem (e1 ': r) a
     -> Sem (e2 ': r) a
@@ -168,7 +168,8 @@
 -- 'Polysemy.State.runState', meaning it's free to 'reinterpret' in terms of
 -- the 'Polysemy.State.State' effect and immediately run it.
 reinterpret
-    :: FirstOrder m0 e1 "reinterpret"
+    :: forall e1 e2 m0 r a
+     . FirstOrder m0 e1 "reinterpret"
     => (∀ m x. e1 m x -> Sem (e2 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effect.
     -> Sem (e1 ': r) a
@@ -183,7 +184,8 @@
 --
 -- See the notes on 'Tactical' for how to use this function.
 reinterpret2H
-    :: (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': r) x)
+    :: forall e1 e2 e3 r a
+     . (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effects.
     -> Sem (e1 ': r) a
     -> Sem (e2 ': e3 ': r) a
@@ -199,7 +201,8 @@
 ------------------------------------------------------------------------------
 -- | Like 'reinterpret', but introduces /two/ intermediary effects.
 reinterpret2
-    :: FirstOrder m0 e1 "reinterpret2"
+    :: forall e1 e2 e3 m0 r a
+     . FirstOrder m0 e1 "reinterpret2"
     => (∀ m x. e1 m x -> Sem (e2 ': e3 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effects.
     -> Sem (e1 ': r) a
@@ -213,7 +216,8 @@
 --
 -- See the notes on 'Tactical' for how to use this function.
 reinterpret3H
-    :: (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': e4 ': r) x)
+    :: forall e1 e2 e3 e4 r a
+     . (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': e4 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effects.
     -> Sem (e1 ': r) a
     -> Sem (e2 ': e3 ': e4 ': r) a
@@ -229,7 +233,8 @@
 ------------------------------------------------------------------------------
 -- | Like 'reinterpret', but introduces /three/ intermediary effects.
 reinterpret3
-    :: FirstOrder m0 e1 "reinterpret3"
+    :: forall e1 e2 e3 e4 m0 r a
+     . FirstOrder m0 e1 "reinterpret3"
     => (∀ m x. e1 m x -> Sem (e2 ': e3 ': e4 ': r) x)
        -- ^ A natural transformation from the handled effect to the new effects.
     -> Sem (e1 ': r) a
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
@@ -1,7 +1,7 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {-# OPTIONS_HADDOCK not-home #-}
 
@@ -16,7 +16,9 @@
 
 import Data.Coerce
 import Data.Kind
+import Fcf
 import GHC.TypeLits
+import Polysemy.Internal.Kind
 
 
 type family DefiningModule (t :: k) :: Symbol
@@ -26,16 +28,19 @@
   DefiningModuleForEffect e     = DefiningModule e
 
 
-
 data T1 m a
 
 type family Break (c :: Constraint)
-                  (rep :: (* -> *) -> * -> *) :: Constraint where
+                  (rep :: Effect) :: Constraint where
   Break _ T1 = ((), ())
   Break _ c  = ()
 
 
+type family IfStuck (tyvar :: k) (b :: k1) (c :: Exp k1) :: k1 where
+  IfStuck T1 b c = b
+  IfStuck a  b c = Eval c
 
+
 type AmbigousEffectMessage r e t vs =
         ( 'Text "Ambiguous use of effect '"
     ':<>: 'ShowType e
@@ -123,7 +128,14 @@
 --
 -- Note that the parameter 'm' is only required to work around supporting
 -- versions of GHC without QuantifiedConstraints
-type FirstOrder m e fn = Coercible (e m) (e (FirstOrderError e fn))
+type FirstOrder m e fn = IfStuck e (() :: Constraint) (FirstOrderFcf m e fn)
+
+data FirstOrderFcf
+    :: (Type -> Type)
+    -> Effect
+    -> Symbol
+    -> Exp Constraint
+type instance Eval (FirstOrderFcf m e fn) = Coercible (e m) (e (FirstOrderError e fn))
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Internal/Effect.hs b/src/Polysemy/Internal/Effect.hs
deleted file mode 100644
--- a/src/Polysemy/Internal/Effect.hs
+++ /dev/null
@@ -1,125 +0,0 @@
-{-# LANGUAGE DefaultSignatures     #-}
-
-{-# OPTIONS_HADDOCK not-home #-}
-
-module Polysemy.Internal.Effect where
-
-import Data.Coerce
-import Data.Functor.Identity
-
-
-------------------------------------------------------------------------------
--- | The class for semantic effects.
---
--- An effect @e@ is a type @e m a@, where the other types are given by:
---
--- * The @m@ type variable corresponds to a monad, which will eventually be
--- instantiated at 'Polysemy.Sem'---meaning it is capable of encoding
--- arbitrary other effects.
---
--- * The @a@ type is handled automatically and uninteresting.
---
--- The type @e m@ must be a 'Functor', but this instance can always be given
--- for free via the @-XDeriveFunctor@ language extension. Often this instance
--- must be derived as a standalone (@-XStandaloneDeriving@):
---
--- @
--- deriving instance Functor (MyEffect m)
--- @
---
--- If the effect doesn't use @m@ whatsoever it is said to be /first-order/.
--- First-order effects can be given an instance of 'Effect' for free with
--- @-XDeriveAnyClass@.
---
--- @
--- deriving instance Effect MyEffect
--- @
-class Effect e where
-  -- | Provide a specialised version of 'fmap' to work around versions of GHC
-  -- that cannot express the quantified constraint '(∀ m. Functor m => Functor (e m))'
-  --
-  -- This must always be equal to 'fmap', and can be removed once GHC 8.6 is the
-  -- minimum version supported by this library
-  fmap' :: (a -> b) -> (e m a -> e m b)
-
-  default fmap' :: Functor (e m) => (a -> b) -> (e m a -> e m b)
-  fmap' = fmap
-  {-# INLINE fmap' #-}
-
-  -- | Higher-order effects require the ability to distribute state from other
-  -- effects throughout themselves. This state is given by an initial piece of
-  -- state @s ()@, and a distributive law that describes how to move the state
-  -- through an effect.
-  --
-  -- When the effect @e@ has multiple computations in the @m@ monad, 'weave'
-  -- defines the semantics for how these computations will view with the state:
-  --
-  -- * If the resulting state from one computation is fed to another, the second
-  -- computation will see the state that results from the first computation.
-  --
-  -- * If instead it is given the intial state, both computations will see the
-  -- same state, but the result of (at least) one will necessarily be ignored.
-  weave
-      :: (Functor s, Functor m, Functor n)
-      => s ()
-      -> (∀ x. s (m x) -> n (s x))
-      -> (∀ x. s x -> Maybe x)
-      -> e m a
-      -> e n (s a)
-
-  -- | When @e@ is first order, 'weave' can be given for free.
-  default weave
-      :: ( Coercible (e m (s a)) (e n (s a))
-         , Functor s
-         , Functor m
-         , Functor n
-         )
-      => s ()
-      -> (∀ x. s (m x) -> n (s x))
-      -> (∀ x. s x -> Maybe x)
-      -> e m a
-      -> e n (s a)
-  weave s _ _ = coerce . fmap' (<$ s)
-  {-# INLINE weave #-}
-
-  -- | Lift a natural transformation from @m@ to @n@ over the effect. 'hoist'
-  -- should be defined as 'defaultHoist', but can be hand-written if the
-  -- default performance isn't sufficient.
-  hoist
-        :: ( Functor m
-           , Functor n
-           )
-        => (∀ x. m x -> n x)
-        -> e m a
-        -> e n a
-
-  -- | When @e@ is first order, 'hoist' be given for free.
-  default hoist
-      :: ( Coercible (e m a) (e n a)
-         , Functor m
-         )
-      => (∀ x. m x -> n x)
-      -> e m a
-      -> e n a
-  hoist _ = coerce
-  {-# INLINE hoist #-}
-
-
-------------------------------------------------------------------------------
--- | A default implementation of 'hoist'. Particularly performance-sensitive
--- effects should give a hand-written their own implementation of 'hoist'.
-defaultHoist
-      :: ( Functor m
-         , Functor n
-         , Effect e
-         )
-      => (∀ x. m x -> n x)
-      -> e m a
-      -> e n a
-defaultHoist f
-  = fmap' runIdentity
-  . weave (Identity ())
-          (fmap Identity . f . runIdentity)
-          (Just . runIdentity)
-{-# INLINE defaultHoist #-}
-
diff --git a/src/Polysemy/Internal/Forklift.hs b/src/Polysemy/Internal/Forklift.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/Forklift.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE NumDecimals     #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies    #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Forklift where
+
+import qualified Control.Concurrent.Async as A
+import           Control.Concurrent.Chan.Unagi
+import           Control.Concurrent.MVar
+import           Control.Monad
+import           Polysemy.Internal
+import           Polysemy.Internal.Union
+
+
+------------------------------------------------------------------------------
+-- | A promise for interpreting an effect of the union @r@ in another thread.
+--
+-- @since 0.5.0.0
+data Forklift r = forall a. Forklift
+  { responseMVar :: MVar (Sem '[Lift IO] a)
+  , request      :: Union r (Sem r) a
+  }
+
+
+------------------------------------------------------------------------------
+-- | A strategy for automatically interpreting an entire stack of effects by
+-- just shipping them off to some other interpretation context.
+--
+-- @since 0.5.0.0
+runViaForklift
+    :: LastMember (Lift IO) r
+    => InChan (Forklift r)
+    -> Sem r a
+    -> Sem '[Lift IO] a
+runViaForklift chan (Sem m) = Sem $ \k -> m $ \u -> do
+  case decompLast u of
+    Left x -> usingSem k $ join $ sendM $ do
+      mvar <- newEmptyMVar
+      writeChan chan $ Forklift mvar x
+      takeMVar mvar
+    Right y -> k $ hoist (runViaForklift_b chan) y
+{-# INLINE runViaForklift #-}
+
+
+runViaForklift_b
+    :: LastMember (Lift IO) r
+    => InChan (Forklift r)
+    -> Sem r a
+    -> Sem '[Lift IO] a
+runViaForklift_b = runViaForklift
+{-# NOINLINE runViaForklift_b #-}
+
+
+------------------------------------------------------------------------------
+-- | Run an effect stack all the way down to 'IO' by running it in a new
+-- thread, and temporarily turning the current thread into an event poll.
+--
+-- This function creates a thread, and so should be compiled with @-threaded@.
+--
+-- @since 0.5.0.0
+withLowerToIO
+    :: LastMember (Lift IO) r
+    => ((forall x. Sem r x -> IO x) -> IO () -> IO a)
+       -- ^ A lambda that takes the lowering function, and a finalizing 'IO'
+       -- action to mark a the forked thread as being complete. The finalizing
+       -- action need not be called.
+    -> Sem r a
+withLowerToIO action = do
+  (inchan, outchan) <- sendM newChan
+  signal <- sendM newEmptyMVar
+
+  res <- sendM $ A.async $ do
+    a <- action (runM . runViaForklift inchan)
+                (putMVar signal ())
+    putMVar signal ()
+    pure a
+
+  let me = do
+        raced <- sendM $ A.race (takeMVar signal) $ readChan outchan
+        case raced of
+          Left () -> sendM $ A.wait res
+          Right (Forklift mvar req) -> do
+            resp <- liftSem req
+            sendM $ putMVar mvar $ pure resp
+            me_b
+      {-# INLINE me #-}
+
+      me_b = me
+      {-# NOINLINE me_b #-}
+
+  me
+
diff --git a/src/Polysemy/Internal/Kind.hs b/src/Polysemy/Internal/Kind.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/Kind.hs
@@ -0,0 +1,16 @@
+module Polysemy.Internal.Kind where
+
+import Data.Kind
+
+------------------------------------------------------------------------------
+-- | The kind of effects.
+--
+-- @since 0.5.0.0
+type Effect    = (Type -> Type) -> Type -> Type
+
+------------------------------------------------------------------------------
+-- | The kind of effect rows.
+--
+-- @since 0.5.0.0
+type EffectRow = [Effect]
+
diff --git a/src/Polysemy/Internal/Lift.hs b/src/Polysemy/Internal/Lift.hs
--- a/src/Polysemy/Internal/Lift.hs
+++ b/src/Polysemy/Internal/Lift.hs
@@ -4,7 +4,9 @@
 
 module Polysemy.Internal.Lift where
 
+import Data.Kind
 
+
 ------------------------------------------------------------------------------
 -- | An effect which allows a regular 'Monad' @m@ into the 'Polysemy.Sem'
 -- ecosystem. Monadic actions in @m@ can be lifted into 'Polysemy.Sem' via
@@ -25,6 +27,6 @@
 --
 -- Consider using 'Polysemy.Trace.trace' and 'Polysemy.Trace.runTraceIO' as
 -- a substitute for using 'putStrLn' directly.
-newtype Lift m (z :: * -> *) a where
+newtype Lift m (z :: Type -> Type) a where
   Lift :: { unLift :: m a } -> Lift m z a
 
diff --git a/src/Polysemy/Internal/NonDet.hs b/src/Polysemy/Internal/NonDet.hs
--- a/src/Polysemy/Internal/NonDet.hs
+++ b/src/Polysemy/Internal/NonDet.hs
@@ -6,9 +6,12 @@
 
 module Polysemy.Internal.NonDet where
 
+import Data.Kind
+
+
 ------------------------------------------------------------------------------
 -- | An effect corresponding to the 'Control.Applicative.Alternative' typeclass.
-data NonDet (m :: * -> *) a
+data NonDet (m :: Type -> Type) a
   = Empty
   | Choose (Bool -> a)
 
diff --git a/src/Polysemy/Internal/TH/Common.hs b/src/Polysemy/Internal/TH/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/TH/Common.hs
@@ -0,0 +1,287 @@
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE NamedFieldPuns  #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections   #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+
+module Polysemy.Internal.TH.Common
+  ( ConLiftInfo (..)
+  , getEffectMetadata
+  , makeMemberConstraint
+  , makeMemberConstraint'
+  , makeSemType
+  , makeInterpreterType
+  , makeEffectType
+  , makeUnambiguousSend
+  , checkExtensions
+  , foldArrows
+  ) where
+
+import           Control.Monad
+import           Data.Bifunctor
+import           Data.Char (toLower)
+import           Data.Either
+import           Data.Generics hiding (Fixity)
+import           Data.List
+import qualified Data.Map.Strict as M
+import           Data.Tuple
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Datatype
+import           Language.Haskell.TH.PprLib
+import           Polysemy.Internal (Sem, Member, send)
+
+#if __GLASGOW_HASKELL__ >= 804
+import           Prelude hiding ((<>))
+#endif
+
+
+------------------------------------------------------------------------------
+-- | Given an effect name, eg @''State@, get information about the type
+-- constructor, and about each of its data constructors.
+getEffectMetadata :: Name -> Q (DatatypeInfo, [ConLiftInfo])
+getEffectMetadata type_name = do
+  dt_info  <- reifyDatatype type_name
+  cl_infos <- traverse (mkCLInfo dt_info) $ datatypeCons dt_info
+  pure (dt_info, cl_infos)
+
+
+------------------------------------------------------------------------------
+-- | Turn a 'ConLiftInfo' for @Foo@ into a @Member Foo r@ constraint.
+makeMemberConstraint :: Name -> ConLiftInfo -> Pred
+makeMemberConstraint r cli = makeMemberConstraint' r $ makeEffectType cli
+
+
+------------------------------------------------------------------------------
+-- | Given a 'ConLiftInfo', get the corresponding effect type.
+makeEffectType :: ConLiftInfo -> Type
+makeEffectType cli
+  = foldl' AppT (ConT $ cliEffName cli)
+  $ cliEffArgs cli
+
+
+------------------------------------------------------------------------------
+-- | @'makeMemberConstraint'' r type@ will produce a @Member type r@
+-- constraint.
+makeMemberConstraint' :: Name -> Type -> Pred
+makeMemberConstraint' r eff = classPred ''Member [eff, VarT r]
+
+
+------------------------------------------------------------------------------
+-- | @'makeSemType' r a@ will produce a @'Polysemy.Sem' r a@ type.
+makeSemType :: Name -> Type -> Type
+makeSemType r result = ConT ''Sem `AppT` VarT r `AppT` result
+
+
+------------------------------------------------------------------------------
+-- | @'makeInterpreterType' con r a@ will produce a @'Polysemy.Sem' (Effect ':
+-- r) a -> 'Polysemy.Sem' r a@ type, where @Effect@ is the effect corresponding
+-- to the 'ConLiftInfo' for @con@.
+makeInterpreterType :: ConLiftInfo -> Name -> Type -> Type
+makeInterpreterType cli r result =
+  foldArrows (makeSemType r result)
+    $ pure
+    $ ConT ''Sem
+        `AppT` (PromotedConsT `AppT` makeEffectType cli `AppT` VarT r)
+        `AppT` result
+
+
+------------------------------------------------------------------------------
+-- | Given a 'ConLiftInfo', this will produce an action for it. It's arguments
+-- will come from any variables in scope that correspond to the 'cliArgs' of
+-- the 'ConLiftInfo'.
+makeUnambiguousSend :: Bool -> ConLiftInfo -> Exp
+makeUnambiguousSend should_mk_sigs cli =
+  let fun_args_names = fmap fst $ cliArgs cli
+      action = foldl1' AppE
+             $ ConE (cliConName cli) : (VarE <$> fun_args_names)
+      eff    = foldl' AppT (ConT $ cliEffName cli) $ args
+               -- see NOTE(makeSem_)
+      args   = (if should_mk_sigs then id else map capturableTVars)
+             $ cliEffArgs cli ++ [sem, cliResType cli]
+      sem    = ConT ''Sem `AppT` VarT (cliUnionName cli)
+   in AppE (VarE 'send) $ SigE action eff
+
+
+------------------------------------------------------------------------------
+-- | Info about constructor being lifted; use 'mkCLInfo' to create one.
+data ConLiftInfo = CLInfo
+  { -- | Name of effect's type constructor
+    cliEffName   :: Name
+    -- | Effect-specific type arguments
+  , cliEffArgs   :: [Type]
+    -- | Result type specific to action
+  , cliResType   :: Type
+    -- | Name of action constructor
+  , cliConName   :: Name
+    -- | Name of final function
+  , cliFunName   :: Name
+    -- | Fixity of function used as an operator
+  , cliFunFixity :: Maybe Fixity
+    -- | Final function arguments
+  , cliArgs   :: [(Name, Type)]
+    -- | Constraints of final function
+  , cliFunCxt    :: Cxt
+    -- | Name of type variable parameterizing 'Sem'
+  , cliUnionName :: Name
+  } deriving Show
+
+
+------------------------------------------------------------------------------
+-- | Creates info about smart constructor being created from info about action
+-- and it's parent type.
+mkCLInfo :: DatatypeInfo -> ConstructorInfo -> Q ConLiftInfo
+mkCLInfo dti ci = do
+  let cliEffName            = datatypeName dti
+
+  (raw_cli_eff_args, [m_arg, raw_cli_res_arg]) <-
+    case splitAtEnd 2 $ datatypeInstTypes dti of
+      r@(_, [_, _]) -> pure r
+      _             -> missingEffArgs cliEffName
+
+  m_name <-
+    case tVarName m_arg of
+      Just r        -> pure r
+      Nothing       -> mArgNotVar cliEffName m_arg
+
+  cliUnionName <- newName "r"
+  cliFunFixity <- reifyFixity $ constructorName ci
+
+  let normalizeType         = replaceMArg m_name cliUnionName
+                            . simplifyKinds
+                            . applySubstitution eq_pairs
+      -- We extract equality constraints with variables to unify them
+      -- manually - this makes type errors more readable. Plus we replace
+      -- kind of result with 'Type' if it is a type variable.
+      (eq_pairs, cliFunCxt) = first (M.fromList . maybeResKindToType)
+                            $ partitionEithers
+                            $ eqPairOrCxt <$> constructorContext ci
+      maybeResKindToType    = maybe id (\k ps -> (k, StarT) : ps)
+                            $ tVarName $ tvKind $ last
+                            $ datatypeVars dti
+
+      cliEffArgs            = normalizeType <$> raw_cli_eff_args
+      cliResType            = normalizeType     raw_cli_res_arg
+      cliConName            = constructorName ci
+      cliFunName            = liftFunNameFromCon cliConName
+      arg_types             = normalizeType <$> constructorFields ci
+
+  arg_names <- replicateM (length arg_types) $ newName "x"
+
+  pure CLInfo{cliArgs = zip arg_names arg_types, ..}
+
+
+------------------------------------------------------------------------------
+-- Error messages and checks
+
+mArgNotVar :: Name -> Type -> Q a
+mArgNotVar name mArg = fail $ show
+  $  text "Monad argument ‘" <> ppr mArg <> text "’ in effect ‘"
+  <> ppr name <> text "’ is not a type variable"
+
+
+missingEffArgs :: Name -> Q a
+missingEffArgs name = fail $ show
+  $   text "Effect ‘" <> ppr name
+      <> text "’ has not enough type arguments"
+  $+$ nest 4
+      (   text "At least monad and result argument are required, e.g.:"
+      $+$ nest 4
+          (   text ""
+          $+$ ppr (DataD [] base args Nothing [] []) <+> text "..."
+          $+$ text ""
+          )
+      )
+  where
+    base = capturableBase name
+    args = PlainTV . mkName <$> ["m", "a"]
+
+
+------------------------------------------------------------------------------
+-- | Fail the 'Q' monad whenever the given 'Extension's aren't enabled in the
+-- current module.
+checkExtensions :: [Extension] -> Q ()
+checkExtensions exts = do
+  states <- zip exts <$> traverse isExtEnabled exts
+  maybe (pure ())
+        (\(ext, _) -> fail $ show
+          $ char '‘' <> text (show ext) <> char '’'
+            <+> text "extension needs to be enabled for Polysemy's Template Haskell to work")
+        (find (not . snd) states)
+
+------------------------------------------------------------------------------
+-- | Constructs capturable name from base of input name.
+capturableBase :: Name -> Name
+capturableBase = mkName . nameBase
+
+------------------------------------------------------------------------------
+-- | Replaces use of @m@ in type with @Sem r@.
+replaceMArg :: TypeSubstitution t => Name -> Name -> t -> t
+replaceMArg m r = applySubstitution $ M.singleton m $ ConT ''Sem `AppT` VarT r
+
+------------------------------------------------------------------------------
+-- Removes 'Type' and variable kind signatures from type.
+simplifyKinds :: Type -> Type
+simplifyKinds = everywhere $ mkT $ \case
+  SigT t StarT    -> t
+  SigT t VarT{}   -> t
+  ForallT bs cs t -> ForallT (goBndr <$> bs) (simplifyKinds <$> cs) t
+    where
+      goBndr (KindedTV n StarT ) = PlainTV n
+      goBndr (KindedTV n VarT{}) = PlainTV n
+      goBndr b = b
+  t -> t
+
+------------------------------------------------------------------------------
+-- | Converts equality constraint with type variable to name and type pair if
+-- possible or leaves constraint as is.
+eqPairOrCxt :: Pred -> Either (Name, Type) Pred
+eqPairOrCxt p = case asEqualPred p of
+  Just (VarT n, b) -> Left (n, b)
+  Just (a, VarT n) -> Left (n, a)
+  _                -> Right p
+
+------------------------------------------------------------------------------
+-- | Creates name of lifting function from action name.
+liftFunNameFromCon :: Name -> Name
+liftFunNameFromCon n = mkName $
+  case nameBase n of
+    ':' : cs -> cs
+    c   : cs -> toLower c : cs
+    ""       -> error "liftFunNameFromCon: empty constructor name"
+
+------------------------------------------------------------------------------
+-- | Folds a list of 'Type's into a right-associative arrow 'Type'.
+foldArrows :: Type -> [Type] -> Type
+foldArrows = foldr (AppT . AppT ArrowT)
+
+------------------------------------------------------------------------------
+-- | Extracts name from type variable (possibly nested in signature and/or
+-- some context), returns 'Nothing' otherwise.
+tVarName :: Type -> Maybe Name
+tVarName = \case
+  ForallT _ _ t -> tVarName t
+  SigT t _      -> tVarName t
+  VarT n        -> Just n
+  ParensT t     -> tVarName t
+  _             -> Nothing
+
+------------------------------------------------------------------------------
+-- | 'splitAt' counting from the end.
+splitAtEnd :: Int -> [a] -> ([a], [a])
+splitAtEnd n = swap . join bimap reverse . splitAt n . reverse
+
+------------------------------------------------------------------------------
+-- | Converts names of all type variables in type to capturable ones based on
+-- original name base. Use with caution, may create name conflicts!
+capturableTVars :: Type -> Type
+capturableTVars = everywhere $ mkT $ \case
+  VarT n          -> VarT $ capturableBase n
+  ForallT bs cs t -> ForallT (goBndr <$> bs) (capturableTVars <$> cs) t
+    where
+      goBndr (PlainTV n   ) = PlainTV $ capturableBase n
+      goBndr (KindedTV n k) = KindedTV (capturableBase n) $ capturableTVars k
+  t -> t
+
diff --git a/src/Polysemy/Internal/TH/Effect.hs b/src/Polysemy/Internal/TH/Effect.hs
--- a/src/Polysemy/Internal/TH/Effect.hs
+++ b/src/Polysemy/Internal/TH/Effect.hs
@@ -32,22 +32,11 @@
   , makeSem_
   ) where
 
-import Prelude hiding ((<>))
-
 import Control.Monad
-import Data.Bifunctor
-import Data.Char (toLower)
-import Data.Either
-import Data.Generics hiding (Fixity)
-import Data.List
-import Data.Tuple
 import Language.Haskell.TH
-import Language.Haskell.TH.PprLib
 import Language.Haskell.TH.Datatype
-import Polysemy.Internal (send, Member, Sem)
 import Polysemy.Internal.CustomErrors (DefiningModule)
-
-import qualified Data.Map.Strict as M
+import Polysemy.Internal.TH.Common
 
 -- TODO: write tests for what should (not) compile
 
@@ -64,6 +53,8 @@
 makeSem :: Name -> Q [Dec]
 makeSem = genFreer True
 
+
+------------------------------------------------------------------------------
 -- | Like 'makeSem', but does not provide type signatures and fixities. This
 -- can be used to attach Haddock comments to individual arguments for each
 -- generated function.
@@ -124,29 +115,29 @@
 -- Please, change this as soon as GHC provides some way of inspecting
 -- signatures, replacing code or generating haddock documentation in TH.
 
+
 ------------------------------------------------------------------------------
 -- | Generates declarations and possibly signatures for functions to lift GADT
 -- constructors into 'Sem' actions.
 genFreer :: Bool -> Name -> Q [Dec]
 genFreer should_mk_sigs type_name = do
   checkExtensions [ScopedTypeVariables, FlexibleContexts]
-  dt_info    <- reifyDatatype type_name
-  cl_infos   <- traverse (mkCLInfo dt_info) $ datatypeCons dt_info
+  (dt_info, cl_infos) <- getEffectMetadata type_name
   tyfams_on  <- isExtEnabled TypeFamilies
-  def_mod_fi <- sequence [ TySynInstD ''DefiningModule
-                             . TySynEqn [ConT $ datatypeName dt_info]
-                             . LitT
-                             . StrTyLit
-                             . loc_module
-                           <$> location
+  def_mod_fi <- sequence [ tySynInstDCompat
+                             ''DefiningModule
+                             Nothing
+                             [pure . ConT $ datatypeName dt_info]
+                             (LitT . StrTyLit . loc_module <$> location)
                          | tyfams_on
                          ]
-  decs       <- traverse (genDec should_mk_sigs) cl_infos
+  decs <- traverse (genDec should_mk_sigs) cl_infos
 
   let sigs = if should_mk_sigs then genSig <$> cl_infos else []
 
-  return $ join $ def_mod_fi : sigs ++ decs
+  pure $ join $ def_mod_fi : sigs ++ decs
 
+
 ------------------------------------------------------------------------------
 -- | Generates signature for lifting function and type arguments to apply in
 -- its body on effect's data constructor.
@@ -155,205 +146,28 @@
   =  maybe [] (pure . flip InfixD (cliFunName cli)) (cliFunFixity cli)
   ++ [ SigD (cliFunName cli) $ quantifyType
        $ ForallT [] (member_cxt : cliFunCxt cli)
-       $ foldArrows $ cliFunArgs cli ++ [sem `AppT` cliResType cli]
+       $ foldArrows sem
+       $ fmap snd
+       $ cliArgs cli
      ]
   where
-    member_cxt = classPred ''Member [eff, VarT $ cliUnionName cli]
-    eff        = foldl' AppT (ConT $ cliEffName cli) $ cliEffArgs cli
-    sem        = ConT ''Sem `AppT` VarT (cliUnionName cli)
+    member_cxt = makeMemberConstraint (cliUnionName cli) cli
+    sem        = makeSemType (cliUnionName cli) (cliResType cli)
 
+
 ------------------------------------------------------------------------------
 -- | Builds a function definition of the form
 -- @x a b c = send (X a b c :: E m a)@.
 genDec :: Bool -> ConLiftInfo -> Q [Dec]
 genDec should_mk_sigs cli = do
-  fun_args_names <- replicateM (length $ cliFunArgs cli) $ newName "x"
-
-  let action = foldl1' AppE
-             $ ConE (cliConName cli) : (VarE <$> fun_args_names)
-      eff    = foldl' AppT (ConT $ cliEffName cli) $ args
-               -- see NOTE(makeSem_)
-      args   = (if should_mk_sigs then id else map capturableTVars)
-             $ cliEffArgs cli ++ [sem, cliResType cli]
-      sem    = ConT ''Sem `AppT` VarT (cliUnionName cli)
+  let fun_args_names = fmap fst $ cliArgs cli
 
-  return
+  pure
     [ PragmaD $ InlineP (cliFunName cli) Inlinable ConLike AllPhases
     , FunD (cliFunName cli)
         [ Clause (VarP <$> fun_args_names)
-                 (NormalB $ AppE (VarE 'send) $ SigE action eff)
+                 (NormalB $ makeUnambiguousSend should_mk_sigs cli)
                  []
         ]
     ]
 
-------------------------------------------------------------------------------
--- | Info about constructor being lifted; use 'mkCLInfo' to create one.
-data ConLiftInfo = CLInfo
-  { -- | Name of effect's type constructor
-    cliEffName   :: Name
-    -- | Effect-specific type arguments
-  , cliEffArgs   :: [Type]
-    -- | Result type specific to action
-  , cliResType   :: Type
-    -- | Name of action constructor
-  , cliConName   :: Name
-    -- | Name of final function
-  , cliFunName   :: Name
-    -- | Fixity of function used as an operator
-  , cliFunFixity :: Maybe Fixity
-    -- | Final function arguments
-  , cliFunArgs   :: [Type]
-    -- | Constraints of final function
-  , cliFunCxt    :: Cxt
-    -- | Name of type variable parameterizing 'Sem'
-  , cliUnionName :: Name
-  } deriving Show
-
-------------------------------------------------------------------------------
--- | Creates info about smart constructor being created from info about action
--- and it's parent type.
-mkCLInfo :: DatatypeInfo -> ConstructorInfo -> Q ConLiftInfo
-mkCLInfo dti ci = do
-  let cliEffName            = datatypeName dti
-
-  (raw_cli_eff_args, [m_arg, raw_cli_res_arg]) <-
-    case splitAtEnd 2 $ datatypeInstTypes dti of
-      r@(_, [_, _]) -> return r
-      _             -> missingEffArgs cliEffName
-
-  m_name <-
-    case tVarName m_arg of
-      Just r        -> return r
-      Nothing       -> mArgNotVar cliEffName m_arg
-
-  cliUnionName <- newName "r"
-  cliFunFixity <- reifyFixity $ constructorName ci
-
-  let normalizeType         = replaceMArg m_name cliUnionName
-                            . simplifyKinds
-                            . applySubstitution eq_pairs
-      -- We extract equality constraints with variables to unify them
-      -- manually - this makes type errors more readable. Plus we replace
-      -- kind of result with 'Type' if it is a type variable.
-      (eq_pairs, cliFunCxt) = first (M.fromList . maybeResKindToType)
-                            $ partitionEithers
-                            $ eqPairOrCxt <$> constructorContext ci
-      maybeResKindToType    = maybe id (\k ps -> (k, StarT) : ps)
-                            $ tVarName $ tvKind $ last
-                            $ datatypeVars dti
-
-      cliEffArgs            = normalizeType <$> raw_cli_eff_args
-      cliResType            = normalizeType     raw_cli_res_arg
-      cliConName            = constructorName ci
-      cliFunName            = liftFunNameFromCon cliConName
-      cliFunArgs            = normalizeType <$> constructorFields ci
-
-  return CLInfo{..}
-
-------------------------------------------------------------------------------
--- Error messages and checks
-
-mArgNotVar :: Name -> Type -> Q a
-mArgNotVar name mArg = fail $ show
-  $  text "Monad argument ‘" <> ppr mArg <> text "’ in effect ‘"
-  <> ppr name <> text "’ is not a type variable"
-
-missingEffArgs :: Name -> Q a
-missingEffArgs name = fail $ show
-  $   text "Effect ‘" <> ppr name
-      <> text "’ has not enough type arguments"
-  $+$ nest 4
-      (   text "At least monad and result argument are required, e.g.:"
-      $+$ nest 4
-          (   text ""
-          $+$ ppr (DataD [] base args Nothing [] []) <+> text "..."
-          $+$ text ""
-          )
-      )
-  where
-    base = capturableBase name
-    args = PlainTV . mkName <$> ["m", "a"]
-
-checkExtensions :: [Extension] -> Q ()
-checkExtensions exts = do
-  states <- zip exts <$> traverse isExtEnabled exts
-  maybe (return ())
-        (\(ext, _) -> fail $ show
-          $ char '‘' <> text (show ext) <> char '’'
-            <+> text "extension needs to be enabled\
-                     \ for smart constructors to work")
-        (find (not . snd) states)
-
-------------------------------------------------------------------------------
--- | Converts names of all type variables in type to capturable ones based on
--- original name base. Use with caution, may create name conflicts!
-capturableTVars :: Type -> Type
-capturableTVars = everywhere $ mkT $ \case
-  VarT n          -> VarT $ capturableBase n
-  ForallT bs cs t -> ForallT (goBndr <$> bs) (capturableTVars <$> cs) t
-    where
-      goBndr (PlainTV n   ) = PlainTV $ capturableBase n
-      goBndr (KindedTV n k) = KindedTV (capturableBase n) $ capturableTVars k
-  t -> t
-
-------------------------------------------------------------------------------
--- | Constructs capturable name from base of input name.
-capturableBase :: Name -> Name
-capturableBase = mkName . nameBase
-
-------------------------------------------------------------------------------
--- | Replaces use of @m@ in type with @Sem r@.
-replaceMArg :: TypeSubstitution t => Name -> Name -> t -> t
-replaceMArg m r = applySubstitution $ M.singleton m $ ConT ''Sem `AppT` VarT r
-
-------------------------------------------------------------------------------
--- Removes 'Type' and variable kind signatures from type.
-simplifyKinds :: Type -> Type
-simplifyKinds = everywhere $ mkT $ \case
-  SigT t StarT    -> t
-  SigT t VarT{}   -> t
-  ForallT bs cs t -> ForallT (goBndr <$> bs) (simplifyKinds <$> cs) t
-    where
-      goBndr (KindedTV n StarT ) = PlainTV n
-      goBndr (KindedTV n VarT{}) = PlainTV n
-      goBndr b = b
-  t -> t
-
-------------------------------------------------------------------------------
--- | Converts equality constraint with type variable to name and type pair if
--- possible or leaves constraint as is.
-eqPairOrCxt :: Pred -> Either (Name, Type) Pred
-eqPairOrCxt p = case asEqualPred p of
-  Just (VarT n, b) -> Left (n, b)
-  Just (a, VarT n) -> Left (n, a)
-  _                -> Right p
-
-------------------------------------------------------------------------------
--- | Creates name of lifting function from action name.
-liftFunNameFromCon :: Name -> Name
-liftFunNameFromCon n = mkName $ case nameBase n of
-                         ':':cs -> cs
-                         c  :cs -> toLower c : cs
-                         ""     -> error
-                           "liftFunNameFromCon: empty constructor name"
-
-------------------------------------------------------------------------------
--- | Folds a list of 'Type's into a right-associative arrow 'Type'.
-foldArrows :: [Type] -> Type
-foldArrows = foldr1 $ AppT . AppT ArrowT
-
-------------------------------------------------------------------------------
--- | Extracts name from type variable (possibly nested in signature and/or
--- some context), returns 'Nothing' otherwise.
-tVarName :: Type -> Maybe Name
-tVarName = \case
-  ForallT _ _ t -> tVarName t
-  SigT t _      -> tVarName t
-  VarT n        -> Just n
-  ParensT t     -> tVarName t
-  _             -> Nothing
-
-------------------------------------------------------------------------------
--- | 'splitAt' counting from the end.
-splitAtEnd :: Int -> [a] -> ([a], [a])
-splitAtEnd n = swap . join bimap reverse . splitAt n . reverse
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
@@ -17,7 +17,6 @@
   ) where
 
 import Polysemy.Internal
-import Polysemy.Internal.Effect
 import Polysemy.Internal.Union
 
 
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,19 +1,22 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE CPP                   #-}
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StrictData            #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE CPP                     #-}
+{-# LANGUAGE ConstraintKinds         #-}
+{-# LANGUAGE FlexibleInstances       #-}
+{-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE MultiParamTypeClasses   #-}
+{-# LANGUAGE StrictData              #-}
+{-# LANGUAGE TypeFamilies            #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 {-# OPTIONS_HADDOCK not-home #-}
 
 module Polysemy.Internal.Union
   ( Union (..)
   , Yo (..)
-  , liftYo
   , Member
+  , weave
+  , hoist
   -- * Building Unions
   , inj
   , weaken
@@ -26,15 +29,18 @@
   -- * Witnesses
   , SNat (..)
   , Nat (..)
+  , LastMember (..)
   ) where
 
+import Data.Bifunctor
 import Control.Monad
 import Data.Functor.Compose
 import Data.Functor.Identity
+import Data.Kind
 import Data.Type.Equality
-import Polysemy.Internal.Effect
+import Polysemy.Internal.Kind
 
-#ifdef ERROR_MESSAGES
+#ifndef NO_ERROR_MESSAGES
 import Polysemy.Internal.CustomErrors
 #endif
 
@@ -42,15 +48,18 @@
 ------------------------------------------------------------------------------
 -- | An extensible, type-safe union. The @r@ type parameter is a type-level
 -- list of effects, any one of which may be held within the 'Union'.
-data Union (r :: [(* -> *) -> * -> *]) (m :: * -> *) a where
+data Union (r :: EffectRow) (m :: Type -> Type) a where
   Union
-      :: SNat n
-         -- ^ A proof that the effect is actually in @r@.
-      -> Yo (IndexOf r n) m a
-         -- ^ The effect to wrap. The functions 'prj' and 'decomp' can help
+      :: -- A proof that the effect is actually in @r@.
+         SNat n
+         -- The effect to wrap. The functions 'prj' and 'decomp' can help
          -- retrieve this value later.
+      -> Yo (IndexOf r n) m a
       -> Union r m a
 
+instance Functor (Union r m) where
+  fmap f (Union w t) = Union w $ fmap f t
+  {-# INLINE fmap #-}
 
 
 data Yo e m a where
@@ -66,33 +75,32 @@
   fmap f (Yo e s d f' v) = Yo e s d (f . f') v
   {-# INLINE fmap #-}
 
-instance Effect (Yo e) where
-  weave s' d v' (Yo e s nt f v) =
+
+
+weave
+    :: (Functor s, Functor m, Functor n)
+    => s ()
+    -> (∀ x. s (m x) -> n (s x))
+    -> (∀ x. s x -> Maybe x)
+    -> Union r m a
+    -> Union r n (s a)
+weave s' d v' (Union w (Yo e s nt f v)) = Union w $
     Yo e (Compose $ s <$ s')
          (fmap Compose . d . fmap nt . getCompose)
          (fmap f . getCompose)
          (v <=< v' . getCompose)
-  {-# INLINE weave #-}
-
-  hoist = defaultHoist
-  {-# INLINE hoist #-}
-
-liftYo :: Functor m => e m a -> Yo e m a
-liftYo e = Yo e (Identity ()) (fmap Identity . runIdentity) runIdentity (Just . runIdentity)
-{-# INLINE liftYo #-}
-
-
-instance Functor (Union r m) where
-  fmap f (Union w t) = Union w $ fmap' f t
-  {-# INLINE fmap #-}
+{-# INLINE weave #-}
 
 
-instance Effect (Union r) where
-  weave s f v (Union w e) = Union w $ weave s f v e
-  {-# INLINE weave #-}
-
-  hoist f (Union w e) = Union w $ hoist f e
-  {-# INLINE hoist #-}
+hoist
+    :: ( Functor m
+       , Functor n
+       )
+    => (∀ x. m x -> n x)
+    -> Union r m a
+    -> Union r n a
+hoist f' (Union w (Yo e s nt f v)) = Union w $ Yo e s (f' . nt) f v
+{-# INLINE hoist #-}
 
 
 ------------------------------------------------------------------------------
@@ -101,14 +109,18 @@
 type Member e r = Member' e r
 
 type Member' e r =
-  ( Find r e
-  , e ~ IndexOf r (Found r e)
-#ifdef ERROR_MESSAGES
+  ( MemberNoError e r
+#ifndef NO_ERROR_MESSAGES
   , Break (AmbiguousSend r e) (IndexOf r (Found r e))
 #endif
   )
 
+type MemberNoError e r =
+  ( Find r e
+  , e ~ IndexOf r (Found r e)
+  )
 
+
 ------------------------------------------------------------------------------
 -- | The kind of type-level natural numbers.
 data Nat = Z | S Nat
@@ -116,7 +128,7 @@
 
 ------------------------------------------------------------------------------
 -- | A singleton for 'Nat'.
-data SNat :: Nat -> * where
+data SNat :: Nat -> Type where
   SZ :: SNat 'Z
   SS :: SNat n -> SNat ('S n)
 
@@ -137,7 +149,7 @@
 
 
 type family Found (ts :: [k]) (t :: k) :: Nat where
-#ifdef ERROR_MESSAGES
+#ifndef NO_ERROR_MESSAGES
   Found '[]       t = UnhandledEffect 'S t
 #endif
   Found (t ': ts) t = 'Z
@@ -185,15 +197,20 @@
 
 ------------------------------------------------------------------------------
 -- | Weaken a 'Union' so it is capable of storing a new sort of effect.
-weaken :: Union r m a -> Union (e ': r) m a
+weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
 weaken (Union n a) = Union (SS n) a
 {-# INLINE weaken #-}
 
 
+
 ------------------------------------------------------------------------------
 -- | Lift an effect @e@ into a 'Union' capable of holding it.
 inj :: forall r e a m. (Functor m , Member e r) => e m a -> Union r m a
-inj e = Union (finder @_ @r @e) $ liftYo e
+inj e = Union (finder @_ @r @e) $
+  Yo e (Identity ())
+       (fmap Identity . runIdentity)
+       runIdentity
+       (Just . runIdentity)
 {-# INLINE inj #-}
 
 
@@ -224,4 +241,21 @@
     SS n -> Left (Union (SS n) a)
 {-# INLINE decompCoerce #-}
 
+
+------------------------------------------------------------------------------
+-- | A proof that @end@ is the last effect in the row.
+--
+-- @since 0.5.0.0
+class MemberNoError end r => LastMember end r | r -> end where
+  decompLast
+      :: Union r m a
+      -> Either (Union r m a) (Union '[end] m a)
+
+instance {-# OVERLAPPABLE #-} (LastMember end r, MemberNoError end (eff ': r))
+      => LastMember end (eff ': r) where
+  decompLast (Union SZ u)     = Left $ Union SZ u
+  decompLast (Union (SS n) u) = first weaken $ decompLast $ Union n u
+
+instance LastMember end '[end] where
+  decompLast = Right
 
diff --git a/src/Polysemy/NonDet.hs b/src/Polysemy/NonDet.hs
--- a/src/Polysemy/NonDet.hs
+++ b/src/Polysemy/NonDet.hs
@@ -14,7 +14,6 @@
 import Polysemy.Internal
 import Polysemy.Internal.NonDet
 import Polysemy.Internal.Union
-import Polysemy.Internal.Effect
 
 
 --------------------------------------------------------------------------------
diff --git a/src/Polysemy/Output.hs b/src/Polysemy/Output.hs
--- a/src/Polysemy/Output.hs
+++ b/src/Polysemy/Output.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BlockArguments  #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Polysemy.Output
@@ -35,15 +34,17 @@
     => (o -> m)
     -> Sem (Output o ': r) a
     -> Sem r (m, a)
-runFoldMapOutput f = runState mempty . reinterpret \case
-  Output o -> modify (<> f o)
+runFoldMapOutput f = runState mempty . reinterpret
+  (\case
+      Output o -> modify (`mappend` f o)
+  )
 {-# INLINE runFoldMapOutput #-}
 
 
 ------------------------------------------------------------------------------
 -- | Run an 'Output' effect by ignoring it.
 runIgnoringOutput :: Sem (Output o ': r) a -> Sem r a
-runIgnoringOutput = interpret \case
+runIgnoringOutput = interpret $ \case
   Output _ -> pure ()
 {-# INLINE runIgnoringOutput #-}
 
@@ -68,7 +69,7 @@
       Output o -> do
         (nacc, acc) <- get
         let no     = length o
-            total  = acc <> o
+            total  = mappend acc o
             ntotal = nacc + no
 
             emitting n ls
diff --git a/src/Polysemy/Resource.hs b/src/Polysemy/Resource.hs
--- a/src/Polysemy/Resource.hs
+++ b/src/Polysemy/Resource.hs
@@ -13,6 +13,7 @@
     -- * Interpretations
   , runResource
   , runResourceInIO
+  , runResourceBase
   ) where
 
 import qualified Control.Exception as X
@@ -26,21 +27,21 @@
 data Resource m a where
   Bracket
     :: m a
-       -- ^ Action to allocate a resource.
+       -- Action to allocate a resource.
     -> (a -> m c)
-       -- ^ Action to cleanup the resource. This is guaranteed to be
+       -- Action to cleanup the resource. This is guaranteed to be
        -- called.
     -> (a -> m b)
-       -- ^ Action which uses the resource.
+       -- Action which uses the resource.
     -> Resource m b
   BracketOnError
     :: m a
-       -- ^ Action to allocate a resource.
+       -- Action to allocate a resource.
     -> (a -> m c)
-       -- ^ Action to cleanup the resource. This will only be called if the
+       -- Action to cleanup the resource. This will only be called if the
        -- "use" block fails.
     -> (a -> m b)
-       -- ^ Action which uses the resource.
+       -- Action which uses the resource.
     -> Resource m b
 
 makeSem ''Resource
@@ -147,6 +148,57 @@
 {-# INLINE runResource #-}
 
 
+------------------------------------------------------------------------------
+-- | A more flexible --- though less safe ---  version of 'runResourceInIO'.
+--
+-- This function is capable of running 'Resource' effects anywhere within an
+-- effect stack, without relying on an explicit function to lower it into 'IO'.
+-- Notably, this means that 'Polysemy.State.State' effects will be consistent
+-- in the presence of 'Resource'.
+--
+-- 'runResourceBase' is safe whenever you're concerned about exceptions thrown
+-- by effects _already handled_ in your effect stack, or in 'IO' code run
+-- directly inside of 'bracket'. It is not safe against exceptions thrown
+-- explicitly at the main thread. If this is not safe enough for your use-case,
+-- use 'runResourceInIO' instead.
+--
+-- This function creates a thread, and so should be compiled with @-threaded@.
+--
+-- @since 0.5.0.0
+runResourceBase
+    :: forall r a
+     . LastMember (Lift IO) r
+    => Sem (Resource ': r) a
+    -> Sem r a
+runResourceBase = interpretH $ \case
+  Bracket a b c -> do
+    ma <- runT a
+    mb <- bindT b
+    mc <- bindT c
+
+    withLowerToIO $ \lower finish -> do
+      let done :: Sem (Resource ': r) x -> IO x
+          done = lower . raise . runResourceBase_b
+      X.bracket
+          (done ma)
+          (\x -> done (mb x) >> finish)
+          (done . mc)
+
+  BracketOnError a b c -> do
+    ma <- runT a
+    mb <- bindT b
+    mc <- bindT c
+
+    withLowerToIO $ \lower finish -> do
+      let done :: Sem (Resource ': r) x -> IO x
+          done = lower . raise . runResourceBase_b
+      X.bracketOnError
+          (done ma)
+          (\x -> done (mb x) >> finish)
+          (done . mc)
+{-# INLINE runResourceBase #-}
+
+
 runResource_b
     :: ∀ r a
      . Sem (Resource ': r) a
@@ -162,4 +214,12 @@
     -> Sem r a
 runResourceInIO_b = runResourceInIO
 {-# NOINLINE runResourceInIO_b #-}
+
+runResourceBase_b
+    :: forall r a
+     . LastMember (Lift IO) r
+    => Sem (Resource ': r) a
+    -> Sem r a
+runResourceBase_b = runResourceBase
+{-# NOINLINE runResourceBase_b #-}
 
diff --git a/src/Polysemy/State.hs b/src/Polysemy/State.hs
--- a/src/Polysemy/State.hs
+++ b/src/Polysemy/State.hs
@@ -25,7 +25,6 @@
 import           Polysemy
 import           Polysemy.Internal
 import           Polysemy.Internal.Combinators
-import           Polysemy.Internal.Effect
 import           Polysemy.Internal.Union
 
 
diff --git a/src/Polysemy/Trace.hs b/src/Polysemy/Trace.hs
--- a/src/Polysemy/Trace.hs
+++ b/src/Polysemy/Trace.hs
@@ -9,6 +9,7 @@
 
     -- * Interpretations
   , runTraceIO
+  , runTraceAsList
   , runIgnoringTrace
   , runTraceAsOutput
 
@@ -53,6 +54,21 @@
 runTraceAsOutput = interpret $ \case
   Trace m -> output m
 {-# INLINE runTraceAsOutput #-}
+
+
+------------------------------------------------------------------------------
+-- | Get the result of a 'Trace' effect as a list of 'String's.
+--
+-- @since 0.5.0.0
+runTraceAsList
+    :: Sem (Trace ': r) a
+    -> Sem r ([String], a)
+runTraceAsList = runFoldMapOutput @String (: []) . reinterpret (
+  \case
+    Trace m -> output m
+  )
+{-# INLINE runTraceAsList #-}
+
 
 ------------------------------------------------------------------------------
 -- | Transform a 'Trace' effect into a 'Output' 'String' effect.
diff --git a/src/Polysemy/Writer.hs b/src/Polysemy/Writer.hs
--- a/src/Polysemy/Writer.hs
+++ b/src/Polysemy/Writer.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BlockArguments  #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TupleSections   #-}
 
@@ -22,6 +21,7 @@
 import Polysemy.Output
 import Polysemy.State
 
+
 ------------------------------------------------------------------------------
 -- | An effect capable of emitting and intercepting messages.
 data Writer o m a where
@@ -35,7 +35,7 @@
 ------------------------------------------------------------------------------
 -- | Transform an 'Output' effect into a 'Writer' effect.
 runOutputAsWriter :: Member (Writer o) r => Sem (Output o ': r) a -> Sem r a
-runOutputAsWriter = interpret \case
+runOutputAsWriter = interpret $ \case
   Output o -> tell o
 {-# INLINE runOutputAsWriter #-}
 
@@ -47,17 +47,19 @@
     :: Monoid o
     => Sem (Writer o ': r) a
     -> Sem r (o, a)
-runWriter = runState mempty . reinterpretH \case
-  Tell o -> do
-    modify (<> o) >>= pureT
-  Listen m -> do
-    mm <- runT m
-    -- TODO(sandy): this is fucking stupid
-    (o, fa) <- raise $ runWriter mm
-    pure $ fmap (o, ) fa
-  Censor f m -> do
-    mm <- runT m
-    ~(o, a) <- raise $ runWriter mm
-    modify (<> f o)
-    pure a
+runWriter = runState mempty . reinterpretH
+  (\case
+      Tell o -> do
+        modify (`mappend` o) >>= pureT
+      Listen m -> do
+        mm <- runT m
+        -- TODO(sandy): this is fucking stupid
+        (o, fa) <- raise $ runWriter mm
+        pure $ fmap (o, ) fa
+      Censor f m -> do
+        mm <- runT m
+        ~(o, a) <- raise $ runWriter mm
+        modify (`mappend` f o)
+        pure a
+  )
 
diff --git a/test/AlternativeSpec.hs b/test/AlternativeSpec.hs
--- a/test/AlternativeSpec.hs
+++ b/test/AlternativeSpec.hs
@@ -16,7 +16,7 @@
 
 
 spec :: Spec
-spec = do
+spec = parallel $ do
   describe "Alternative instance" $ do
     it "should choose the first branch" $ do
       runAlt (pure '1' <|> pure '2') `shouldBe` (Just '1')
diff --git a/test/AsyncSpec.hs b/test/AsyncSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/AsyncSpec.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE NumDecimals #-}
+
+module AsyncSpec where
+
+import Control.Concurrent
+import Control.Monad
+import Polysemy
+import Polysemy.Async
+import Polysemy.State
+import Polysemy.Trace
+import Test.Hspec
+
+
+spec :: Spec
+spec = describe "async" $ do
+  it "should thread state and not lock" $ do
+    (ts, (s, r)) <- runM
+                  . runTraceAsList
+                  . runState "hello"
+                  . runAsync $ do
+      let message :: Member Trace r => Int -> String -> Sem r ()
+          message n msg = trace $ mconcat
+            [ show n, "> ", msg ]
+
+      a1 <- async $ do
+          v <- get @String
+          message 1 v
+          put $ reverse v
+
+          sendM $ threadDelay 1e5
+          get >>= message 1
+
+          sendM $ threadDelay 1e5
+          get @String
+
+      void $ async $ do
+          sendM $ threadDelay 5e4
+          get >>= message 2
+          put "pong"
+
+      await a1 <* put "final"
+
+    ts `shouldContain` ["1> hello", "2> olleh", "1> pong"]
+    s `shouldBe` "final"
+    r `shouldBe` Just "pong"
diff --git a/test/BracketSpec.hs b/test/BracketSpec.hs
--- a/test/BracketSpec.hs
+++ b/test/BracketSpec.hs
@@ -10,18 +10,26 @@
 
 
 runTest
-  :: Sem '[Error (), Resource, State [Char], Trace, Output String] a
+  :: Sem '[Error (), Resource, State [Char], Trace] a
   -> ([String], ([Char], Either () a))
 runTest = run
-        . runFoldMapOutput @String (:[])
-        . runTraceAsOutput
+        . runTraceAsList
         . runState ""
         . runResource
         . runError @()
 
+runTest2
+  :: Sem '[Error (), Resource, State [Char], Trace, Lift IO] a
+  -> IO ([String], ([Char], Either () a))
+runTest2 = runM
+         . runTraceAsList
+         . runState ""
+         . runResourceBase
+         . runError @()
 
+
 spec :: Spec
-spec = do
+spec = parallel $ do
   describe "pure bracket" $ do
     it "persist state and call the finalizer" $ do
       let (ts, (s, e)) = runTest $ do
@@ -79,4 +87,57 @@
       ts `shouldNotContain` ["starting block"]
       s `shouldBe` "don't get here"
       e `shouldBe` Right ()
+
+
+  describe "io dispatched bracket" $ do
+    it "persist state and call the finalizer" $ do
+      (ts, (s, e)) <- runTest2 $ do
+            bracket
+              (put "allocated" >> pure ())
+              (\() -> do
+                get >>= trace
+                put "finalized"
+              )
+              (\() -> do
+                get >>= trace
+                put "starting block"
+                _ <- throw ()
+                put "don't get here"
+              )
+      ts `shouldContain` ["allocated"]
+      ts `shouldContain` ["starting block"]
+      s `shouldBe` "finalized"
+      e `shouldBe` Left ()
+
+    it "should not lock when done recursively" $ do
+      (ts, (s, e)) <- runTest2 $ do
+            bracket
+              (put "hello 1")
+              (\() -> do
+                get >>= trace
+                put "finished"
+              )
+              (\() -> do
+                get >>= trace
+                bracket (put "hello 2")
+                        (const $ do
+                          get >>= trace
+                          put "goodbye 2"
+                        )
+                        (const $ do
+                          get >>= trace
+                          put "RUNNING"
+                          throw ()
+                        )
+                -- This doesn't run due to the thrown error above
+                get >>= trace
+                put "goodbye 1"
+              )
+      ts `shouldContain` [ "hello 1"
+                         , "hello 2"
+                         , "RUNNING"
+                         , "goodbye 2"
+                         ]
+      s `shouldBe` "finished"
+      e `shouldBe` Left ()
 
diff --git a/test/DoctestSpec.hs b/test/DoctestSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/DoctestSpec.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE CPP #-}
+
+module DoctestSpec where
+
+import Test.Hspec
+import Test.DocTest
+
+spec :: Spec
+spec = parallel $ describe "Error messages" $ it "should pass the doctest" $ doctest
+  [ "-isrc/"
+  , "--fast"
+  , "-XDataKinds"
+  , "-XDeriveFunctor"
+  , "-XFlexibleContexts"
+  , "-XGADTs"
+  , "-XLambdaCase"
+  , "-XPolyKinds"
+  , "-XRankNTypes"
+  , "-XScopedTypeVariables"
+  , "-XStandaloneDeriving"
+  , "-XTypeApplications"
+  , "-XTypeFamilies"
+  , "-XTypeOperators"
+  , "-XUnicodeSyntax"
+
+#if __GLASGOW_HASKELL__ < 806
+  , "-XMonadFailDesugaring"
+  , "-XTypeInType"
+#endif
+
+  , "test/TypeErrors.hs"
+
+  -- Modules that are explicitly imported for this test must be listed here
+  , "src/Polysemy.hs"
+  , "src/Polysemy/Output.hs"
+  , "src/Polysemy/Reader.hs"
+  , "src/Polysemy/Resource.hs"
+  , "src/Polysemy/State.hs"
+  , "src/Polysemy/Trace.hs"
+  ]
diff --git a/test/FusionSpec.hs b/test/FusionSpec.hs
--- a/test/FusionSpec.hs
+++ b/test/FusionSpec.hs
@@ -1,9 +1,14 @@
-{-# LANGUAGE BlockArguments   #-}
+{-# LANGUAGE CPP              #-}
 {-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE TemplateHaskell  #-}
 {-# LANGUAGE TypeApplications #-}
 {-# OPTIONS_GHC -O2           #-}
 
+
+#if __GLASGOW_HASKELL__ < 804
+{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
+#endif
+
 module FusionSpec where
 
 import qualified Control.Monad.Trans.Except as E
@@ -11,7 +16,6 @@
 import           Polysemy.Error
 import           Polysemy.Internal
 import           Polysemy.Internal.Combinators
-import           Polysemy.Internal.Effect
 import           Polysemy.Internal.Union
 import           Polysemy.State
 import           Test.Hspec
@@ -27,10 +31,13 @@
 
 
 spec :: Spec
-spec = do
+spec = parallel $ do
   describe "fusion" $ do
+#if __GLASGOW_HASKELL__ >= 806
+    -- 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)
@@ -60,11 +67,10 @@
 
 
 tryIt :: Either Bool String
-tryIt = run . runError @Bool $ do
+tryIt = run . runError @Bool $
   catch @Bool
-    do
-      throw False
-    \_ -> pure "hello"
+    (throw False)
+    (\_ -> pure "hello")
 
 
 countDown :: Int -> Int
diff --git a/test/HigherOrderSpec.hs b/test/HigherOrderSpec.hs
--- a/test/HigherOrderSpec.hs
+++ b/test/HigherOrderSpec.hs
@@ -6,7 +6,7 @@
 
 
 spec :: Spec
-spec = describe "Reader local" $ do
+spec = parallel $ describe "Reader local" $ do
   it "should nest with itself" $ do
     let foo = run . runReader "hello" $ do
                 local (++ " world") $ do
diff --git a/test/InspectorSpec.hs b/test/InspectorSpec.hs
--- a/test/InspectorSpec.hs
+++ b/test/InspectorSpec.hs
@@ -19,7 +19,7 @@
 
 
 spec :: Spec
-spec = describe "Inspector" $ do
+spec = parallel $ describe "Inspector" $ do
   it "should inspect State effects" $ do
     withNewTTY $ \ref -> do
       void . (runM .@ runCallback ref)
diff --git a/test/OutputSpec.hs b/test/OutputSpec.hs
--- a/test/OutputSpec.hs
+++ b/test/OutputSpec.hs
@@ -7,7 +7,7 @@
 
 
 spec :: Spec
-spec = do
+spec = parallel $ do
   describe "runBatchOutput" $ do
     it "should return nothing at batch size 0" $ do
       let (ms, ()) = runOutput 0 $ output @[Int] [0..100]
diff --git a/test/ThEffectSpec.hs b/test/ThEffectSpec.hs
--- a/test/ThEffectSpec.hs
+++ b/test/ThEffectSpec.hs
@@ -9,7 +9,7 @@
 import Language.Haskell.TH hiding (Type)
 
 spec :: Spec
-spec = it "should compile" True
+spec = parallel $ it "should compile" True
 
 -- Infix effects and actions -------------------------------------------------
 
diff --git a/test/TypeErrors.hs b/test/TypeErrors.hs
new file mode 100644
--- /dev/null
+++ b/test/TypeErrors.hs
@@ -0,0 +1,167 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
+module TypeErrors where
+
+-- $setup
+-- >>> default ()
+-- >>> :m +Polysemy
+-- >>> :m +Polysemy.Output
+-- >>> :m +Polysemy.Reader
+-- >>> :m +Polysemy.Resource
+-- >>> :m +Polysemy.State
+-- >>> :m +Polysemy.Trace
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- foo :: Sem r ()
+-- foo = put ()
+-- :}
+-- ...
+-- ... Ambiguous use of effect 'State'
+-- ...
+-- ... (Member (State ()) r) ...
+-- ...
+ambiguousMonoState = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- foo :: Sem r ()
+-- foo = put 5
+-- :}
+-- ...
+-- ... Ambiguous use of effect 'State'
+-- ...
+-- ... (Member (State s0) r) ...
+-- ...
+-- ... 's0' directly...
+-- ...
+ambiguousPolyState = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- TODO(sandy): should this mention 'Reader i' or just 'Reader'?
+--
+-- >>> :{
+-- interpret @Reader $ \case
+--   Ask -> undefined
+-- :}
+-- ...
+-- ... 'Reader i' is higher-order, but 'interpret' can help only
+-- ... with first-order effects.
+-- ...
+-- ... 'interpretH' instead.
+-- ...
+interpretBadFirstOrder = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- runFoldMapOutput
+--     :: forall o m r a
+--      . Monoid m
+--     => (o -> m)
+--     -> Sem (Output o ': r) a
+--     -> Sem r (m, a)
+-- runFoldMapOutput f = runState mempty . reinterpret $ \case
+--   Output o -> modify (`mappend` f o)
+-- :}
+-- ...
+-- ... Probable cause: ...reinterpret... is applied to too few arguments
+-- ...
+tooFewArgumentsReinterpret = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- let reinterpretScrub :: Sem (Output Int ': m) a -> Sem (State Bool ': Trace ': m) a
+--     reinterpretScrub = undefined
+--     foo :: Sem '[Output Int] ()
+--     foo = pure ()
+--     foo' = reinterpretScrub foo
+--     foo'' = runState True foo'
+--     foo''' = runTraceIO foo''
+--  in runM foo'''
+-- :}
+-- ...
+-- ... Ambiguous use of effect 'Lift'
+-- ...
+-- ... add (Member (Lift IO) '[]) ...
+-- ...
+--
+-- PROBLEM: We're trying to run more effects than exist in the eff row. This is
+-- indeed a problem, but the error message isn't helpful.
+--
+-- SOLUTION: Add a special case to `AmbiguousSend` when `r ~ '[]`.
+runningTooManyEffects'WRONG = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- foo :: Sem (State Int ': r) ()
+-- foo = put ()
+-- :}
+-- ...
+-- ... Ambiguous use of effect 'State'
+-- ...
+-- ... (Member (State ()) State Int : r) ...
+-- ...
+--
+-- PROBLEM: There should be parentheses around `State Int : r`
+--
+-- SOLUTION: Emit parens only when the effect row is of the form `e1 ': ...`
+missingParens'WRONG = ()
+
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- let foo :: Member Resource r => Sem r ()
+--     foo = undefined
+--  in runM $ runResourceInIO foo
+-- :}
+-- ...
+-- ... Ambiguous use of effect 'Lift'
+-- ...
+-- ... (Member (Lift IO) r0) ...
+-- ...
+-- ... Could not deduce: (Member Resource r1)
+-- ...
+--
+-- PROBLEM: This error is totally bogus. We forgot to give an argument to
+-- 'runResourceInIO'. For comparison, the standard error GHC gives in this case
+-- is significantly more helpful:
+--
+--    <interactive>:192:13: error:
+--        • Couldn't match expected type ‘Sem '[Lift m] a’
+--                      with actual type ‘Sem (Resource : r0) a0 -> Sem r0 a0’
+--        • Probable cause: ‘runResourceInIO’ is applied to too few arguments
+--          In the second argument of ‘($)’, namely ‘runResourceInIO foo’
+--          In the expression: runM $ runResourceInIO foo
+--          In the expression:
+--            let
+--              foo :: Member Resource r => Sem r ()
+--              foo = undefined
+--            in runM $ runResourceInIO foo
+--        • Relevant bindings include
+--            it :: m a (bound at <interactive>:190:2)
+--    <interactive>:192:29: error:
+--        • Couldn't match expected type ‘Sem r0 x -> IO x’
+--                      with actual type ‘Sem r1 ()’
+--        • In the first argument of ‘runResourceInIO’, namely ‘foo’
+--          In the second argument of ‘($)’, namely ‘runResourceInIO foo’
+--          In the expression: runM $ runResourceInIO foo
+--
+--
+-- SOLUTION: Honestly I'm not sure!
+missingArgumentToRunResourceInIO'WRONG = ()
+
+
+