diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,19 @@
 # Changelog for polysemy
 
+## 0.2.2.0 (2019-05-30)
+
+- Added `getInspectorT` to the `Tactical` functions, which allows polysemy code
+    to be run in external callbacks
+- A complete rewrite of `Polysemy.Internal.TH.Effect` (thanks to @TheMatten)
+- Fixed a bug in the TH generation of effects where the splices could contain
+    usages of effects that were ambiguous
+
+## 0.2.1.0 (2019-05-27)
+
+- Fixed a bug in the `Alternative` instance for `Sem`, where it would choose the
+    *last* success instead of the first
+- Added `MonadPlus` and `MonadFail` instances for `Sem`
+
 ## 0.2.0.0 (2019-05-23)
 
 - Fixed a serious bug in `interpretH` and friends, where higher-order effects
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,3 +1,9 @@
+<p align="center">
+<img src="https://raw.githubusercontent.com/isovector/polysemy/master/polysemy.png" alt="Polysemy" title="Polysemy">
+</p>
+
+<p>&nbsp;</p>
+
 # polysemy
 
 [![Build Status](https://api.travis-ci.org/isovector/polysemy.svg?branch=master)](https://travis-ci.org/isovector/polysemy)
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: d24941def9c13073c8c65e68d2cb76cddd1df3fad645148e5dfffa914a749250
+-- hash: c0c48158ef37719851ad6b2bef99ba3236628e92c385792bac924109605febe9
 
 name:           polysemy
-version:        0.2.1.0
+version:        0.2.2.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
@@ -71,10 +71,12 @@
   ghc-options: -Wall
   build-depends:
       base >=4.7 && <5
+    , containers >=0.6 && <=0.7
     , mtl >=2.2.2 && <3
     , random >=1.1 && <1.2
-    , syb >=0.7 && <0.8
+    , 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
   if flag(dump-core)
     ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
@@ -91,6 +93,7 @@
       AlternativeSpec
       FusionSpec
       HigherOrderSpec
+      InspectorSpec
       OutputSpec
       Paths_polysemy
   hs-source-dirs:
@@ -99,13 +102,15 @@
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
+    , containers >=0.6 && <=0.7
     , hspec >=2.6.0 && <3
     , inspection-testing >=0.4.1.1 && <0.5
     , mtl >=2.2.2 && <3
     , polysemy
     , random >=1.1 && <1.2
-    , syb >=0.7 && <0.8
+    , 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
   default-language: Haskell2010
 
@@ -120,13 +125,15 @@
   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
     , criterion
     , free
     , freer-simple
     , mtl
     , polysemy
     , random >=1.1 && <1.2
-    , syb >=0.7 && <0.8
+    , 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
   default-language: Haskell2010
diff --git a/src/Polysemy.hs b/src/Polysemy.hs
--- a/src/Polysemy.hs
+++ b/src/Polysemy.hs
@@ -107,6 +107,8 @@
   , pureT
   , runT
   , bindT
+  , getInspectorT
+  , Inspector (..)
 
   -- * Deprecated Names
   -- | The following exports are deprecated, and are exposed only for
diff --git a/src/Polysemy/Error.hs b/src/Polysemy/Error.hs
--- a/src/Polysemy/Error.hs
+++ b/src/Polysemy/Error.hs
@@ -10,6 +10,7 @@
 
     -- * Interpretations
   , runError
+  , runErrorAsAnother
   , runErrorInIO
   ) where
 
@@ -30,6 +31,11 @@
 makeSem ''Error
 
 
+hush :: Either e a -> Maybe a
+hush (Right a) = Just a
+hush (Left _) = Nothing
+
+
 ------------------------------------------------------------------------------
 -- | Run an 'Error' effect in the style of
 -- 'Control.Monad.Trans.Except.ExceptT'.
@@ -39,9 +45,12 @@
 runError (Sem m) = Sem $ \k -> E.runExceptT $ m $ \u ->
   case decomp u of
     Left x -> E.ExceptT $ k $
-      weave (Right ()) (either (pure . Left) runError_b) x
-    Right (Yo (Throw e) _ _ _) -> E.throwE e
-    Right (Yo (Catch try handle) s d y) ->
+      weave (Right ())
+            (either (pure . Left) runError_b)
+            hush
+            x
+    Right (Yo (Throw e) _ _ _ _) -> E.throwE e
+    Right (Yo (Catch try handle) s d y _) ->
       E.ExceptT $ usingSem k $ do
         ma <- runError_b $ d $ try <$ s
         case ma of
@@ -58,6 +67,34 @@
     -> Sem r (Either e a)
 runError_b = runError
 {-# NOINLINE runError_b #-}
+
+
+------------------------------------------------------------------------------
+-- | Transform one 'Error' into another. This function can be used to aggregate
+-- multiple errors into a single type.
+--
+-- @since 0.2.2.0
+runErrorAsAnother
+  :: Member (Error e2) r
+  => (e1 -> e2)
+  -> Sem (Error e1 ': r) a
+  -> Sem r a
+runErrorAsAnother f = interpretH $ \case
+  Throw e -> throw $ f e
+  Catch action handler -> do
+    a  <- runT action
+    h  <- bindT handler
+
+    mx <- raise $ runError a
+    case mx of
+      Right x -> pure x
+      Left e -> do
+        istate <- getInitialStateT
+        mx' <- raise $ runError $ h $ e <$ istate
+        case mx' of
+          Right x -> pure x
+          Left e' -> throw $ f e'
+{-# INLINE runErrorAsAnother #-}
 
 
 newtype WrappedExc e = WrappedExc { unwrapExc :: e }
diff --git a/src/Polysemy/Internal.hs b/src/Polysemy/Internal.hs
--- a/src/Polysemy/Internal.hs
+++ b/src/Polysemy/Internal.hs
@@ -218,10 +218,12 @@
       True  -> b
   {-# INLINE (<|>) #-}
 
+-- | @since 0.2.1.0
 instance (Member NonDet r) => MonadPlus (Sem r) where
   mzero = empty
   mplus = (<|>)
 
+-- | @since 0.2.1.0
 instance (Member NonDet r) => MonadFail (Sem r) where
   fail = const empty
 
@@ -332,7 +334,7 @@
 runM :: Monad m => Sem '[Lift m] a -> m a
 runM (Sem m) = m $ \z ->
   case extract z of
-    Yo e s _ f -> do
+    Yo e s _ f _ -> do
       a <- unLift e
       pure $ f $ a <$ s
 {-# INLINE runM #-}
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
@@ -64,8 +64,8 @@
 interpretH f (Sem m) = m $ \u ->
   case decomp u of
     Left  x -> liftSem $ hoist (interpretH_b f) x
-    Right (Yo e s d y) -> do
-      a <- runTactics s d (f e)
+    Right (Yo e s d y v) -> do
+      a <- runTactics s d v $ f e
       pure $ y a
 {-# INLINE interpretH #-}
 
@@ -82,9 +82,11 @@
     case decomp u of
         Left x -> S.StateT $ \s' ->
           k . fmap swap
-            . weave (s', ()) (uncurry $ interpretInStateT_b f)
+            . weave (s', ())
+                    (uncurry $ interpretInStateT_b f)
+                    (Just . snd)
             $ x
-        Right (Yo e z _ y) ->
+        Right (Yo e z _ y _) ->
           fmap (y . (<$ z)) $ S.mapStateT (usingSem k) $ f e
 {-# INLINE interpretInStateT #-}
 
@@ -101,9 +103,11 @@
     case decomp u of
         Left x -> LS.StateT $ \s' ->
           k . fmap swap
-            . weave (s', ()) (uncurry $ interpretInLazyStateT_b f)
+            . weave (s', ())
+                    (uncurry $ interpretInLazyStateT_b f)
+                    (Just . snd)
             $ x
-        Right (Yo e z _ y) ->
+        Right (Yo e z _ y _) ->
           fmap (y . (<$ z)) $ LS.mapStateT (usingSem k) $ f e
 {-# INLINE interpretInLazyStateT #-}
 
@@ -141,8 +145,8 @@
 reinterpretH f (Sem m) = Sem $ \k -> m $ \u ->
   case decompCoerce u of
     Left x  -> k $ hoist (reinterpretH_b f) $ x
-    Right (Yo e s d y) -> do
-      a <- usingSem k $ runTactics s (raiseUnder . d) $ f e
+    Right (Yo e s d y v) -> do
+      a <- usingSem k $ runTactics s (raiseUnder . d) v $ f e
       pure $ y a
 {-# INLINE[3] reinterpretH #-}
 -- TODO(sandy): Make this fuse in with 'stateful' directly.
@@ -176,8 +180,8 @@
 reinterpret2H f (Sem m) = Sem $ \k -> m $ \u ->
   case decompCoerce u of
     Left x  -> k $ weaken $ hoist (reinterpret2H_b f) $ x
-    Right (Yo e s d y) -> do
-      a <- usingSem k $ runTactics s (raiseUnder2 . d) $ f e
+    Right (Yo e s d y v) -> do
+      a <- usingSem k $ runTactics s (raiseUnder2 . d) v $ f e
       pure $ y a
 {-# INLINE[3] reinterpret2H #-}
 
@@ -206,8 +210,8 @@
 reinterpret3H f (Sem m) = Sem $ \k -> m $ \u ->
   case decompCoerce u of
     Left x  -> k . weaken . weaken . hoist (reinterpret3H_b f) $ x
-    Right (Yo e s d y) -> do
-      a <- usingSem k $ runTactics s (raiseUnder3 . d) $ f e
+    Right (Yo e s d y v) -> do
+      a <- usingSem k $ runTactics s (raiseUnder3 . d) v $ f e
       pure $ y a
 {-# INLINE[3] reinterpret3H #-}
 
@@ -256,8 +260,8 @@
     -> Sem r a
 interceptH f (Sem m) = Sem $ \k -> m $ \u ->
   case prj u of
-    Just (Yo e s d y) ->
-      usingSem k $ fmap y $ runTactics s (raise . d) $ f e
+    Just (Yo e s d y v) ->
+      usingSem k $ fmap y $ runTactics s (raise . d) v $ f e
     Nothing -> k u
 {-# INLINE interceptH #-}
 
diff --git a/src/Polysemy/Internal/Effect.hs b/src/Polysemy/Internal/Effect.hs
--- a/src/Polysemy/Internal/Effect.hs
+++ b/src/Polysemy/Internal/Effect.hs
@@ -63,6 +63,7 @@
       :: (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)
 
@@ -75,9 +76,10 @@
          )
       => 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)
+  weave s _ _ = coerce . fmap' (<$ s)
   {-# INLINE weave #-}
 
   -- | Lift a natural transformation from @m@ to @n@ over the effect. 'hoist'
@@ -118,5 +120,6 @@
   = fmap' runIdentity
   . weave (Identity ())
           (fmap Identity . f . runIdentity)
+          (Just . runIdentity)
 {-# INLINE defaultHoist #-}
 
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
@@ -1,53 +1,61 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TemplateHaskell   #-}
-{-# LANGUAGE TupleSections     #-}
-
 {-# OPTIONS_HADDOCK not-home #-}
 
--- Originally ported from code written by Sandy Maguire (@isovector), available
--- at https://github.com/IxpertaSolutions/freer-effects/pull/28.
-
-{-|
-This module provides Template Haskell functions for automatically generating
-effect operation functions (that is, functions that use 'send') from a given
-effect algebra. For example, using the @FileSystem@ effect from the example in
-the module documentation for "Polysemy", we can write the following:
-
-@
-data FileSystem m a where
-  ReadFile :: 'FilePath' -> FileSystem 'String'
-  WriteFile :: 'FilePath' -> 'String' -> FileSystem ()
-'makeSem' ''FileSystem
-@
-
-This will automatically generate the following functions:
-
-@
-readFile :: 'Member' FileSystem r => 'FilePath' -> 'Sem' r 'String'
-readFile a = 'send' (ReadFile a)
+{-# LANGUAGE NamedFieldPuns  #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections   #-}
 
-writeFile :: 'Member' FileSystem r => 'FilePath' -> 'String' -> 'Sem' r ()
-writeFile a b = 'send' (WriteFile a b)
-@
--}
+-- | This module provides Template Haskell functions for automatically generating
+-- effect operation functions (that is, functions that use 'send') from a given
+-- effect algebra. For example, using the @FileSystem@ effect from the example in
+-- the module documentation for "Polysemy", we can write the following:
+--
+-- @
+-- data FileSystem m a where
+--   ReadFile  :: 'FilePath' -> FileSystem 'String'
+--   WriteFile :: 'FilePath' -> 'String' -> FileSystem ()
+--
+-- 'makeSem' ''FileSystem
+-- @
+--
+-- This will automatically generate (approximately) the following functions:
+--
+-- @
+-- readFile :: 'Member' FileSystem r => 'FilePath' -> 'Sem' r 'String'
+-- readFile a = 'send' (ReadFile a)
+--
+-- writeFile :: 'Member' FileSystem r => 'FilePath' -> 'String' -> 'Sem' r ()
+-- writeFile a b = 'send' (WriteFile a b)
+-- @
 module Polysemy.Internal.TH.Effect
   ( makeSem
   , makeSem_
-  )
-where
+  ) where
 
-import Control.Monad (join, forM, unless)
-import Data.Char (toLower)
+import Prelude hiding ((<>))
+
+import Control.Monad
+import Data.Bifunctor
+import Data.Char                      (toLower)
+import Data.Either
+import Data.Generics
 import Data.List
-import Generics.SYB
+import Data.Tuple
 import Language.Haskell.TH
-import Polysemy.Internal (send, Member, Sem)
+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
 
--- | If @T@ is a GADT representing an effect algebra, as described in the module
--- documentation for "Polysemy", @$('makeSem' ''T)@ automatically
--- generates a smart constructor for every data constructor of @T@.
+-- TODO: write tests for what should (not) compile
+
+------------------------------------------------------------------------------
+-- | If @T@ is a GADT representing an effect algebra, as described in the
+-- module documentation for "Polysemy", @$('makeSem' ''T)@ automatically
+-- generates a smart constructor for every data constructor of @T@. This also
+-- works for data family instances.
 --
 -- @since 0.1.2.0
 makeSem :: Name -> Q [Dec]
@@ -58,152 +66,276 @@
 -- function.
 --
 -- @
--- data Lang m a where
---   Output :: String -> Lang ()
+-- data Output o m a where
+--   Output :: o -> Output o m ()
 --
--- makeSem_ ''Lang
+-- makeSem_ ''Output
 --
--- -- | Output a string.
--- output :: Member Lang r
---        => String         -- ^ String to output.
+-- -- | Output the value \@o\@.
+-- output :: forall o r
+--        .  Member (Output o) r
+--        => o         -- ^ Value to output.
 --        -> Sem r ()  -- ^ No result.
 -- @
 --
--- Note that 'makeSem_' must be used /before/ the explicit type signatures.
+-- Because of limitations in Template Haskell, signatures have to follow some
+-- rules to work properly:
 --
+-- * 'makeSem_' must be used /before/ the explicit type signatures
+-- * signatures have to specify argument of 'Sem' representing union of
+-- effects as @r@ (e.g. @'Sem' r ()@)
+-- * all arguments in effect's type constructor have to follow naming scheme
+-- from effect's declaration:
+--
+-- @
+-- data Foo e m a where
+--   FooC1 :: Foo x m ()
+--   FooC2 :: Foo (Maybe x) m ()
+-- @
+--
+-- should have @e@ in type signature of @fooC1@:
+--
+-- @fooC1 :: forall e r. Member (Foo e) r => Sem r ()@
+--
+-- but @x@ in signature of @fooC2@:
+--
+-- @fooC2 :: forall x r. Member (Foo (Maybe x)) r => Sem r ()@
+--
+-- * all effect's type variables and @r@ have to be explicitly quantified
+-- using @forall@ (order is not important)
+--
+-- These restrictions may be removed in the future, depending on changes to
+-- the compiler.
+--
 -- @since 0.1.2.0
 makeSem_ :: Name -> Q [Dec]
 makeSem_ = genFreer False
+-- NOTE(makeSem_):
+-- This function uses an ugly hack to work --- it enables change of names in
+-- annotation of applied data constructor to capturable ones, based of names
+-- in effect's definition. This allows user to provide them to us from their
+-- signature through 'forall' with 'ScopedTypeVariables' enabled, so that we
+-- can compile liftings of constructors with ambiguous type arguments (see
+-- issue #48).
+--
+-- 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 makeSigs tcName = do
-  -- The signatures for the generated definitions require FlexibleContexts.
-  isExtEnabled FlexibleContexts
-    >>= flip unless (fail "makeSem requires FlexibleContexts to be enabled")
-  hasTyFams <- isExtEnabled TypeFamilies
+genFreer should_mk_sigs type_name = do
+  checkExtensions [ScopedTypeVariables, FlexibleContexts]
+  dt_info    <- reifyDatatype type_name
+  cl_infos   <- traverse (mkCLInfo dt_info) $ datatypeCons dt_info
+  tyfams_on  <- isExtEnabled TypeFamilies
+  def_mod_fi <- sequence [ TySynInstD ''DefiningModule
+                             . TySynEqn [ConT $ datatypeName dt_info]
+                             . LitT
+                             . StrTyLit
+                             . loc_module
+                           <$> location
+                         | tyfams_on
+                         ]
+  decs       <- traverse (genDec should_mk_sigs) cl_infos
 
-  reify tcName >>= \case
-    TyConI (DataD _ _ _ _ cons _) -> do
-      sigs <- filter (const makeSigs) <$> mapM genSig cons
-      decs <- join <$> mapM genDecl cons
-      loc <- location
+  let sigs = [ genSig <$> cl_infos | should_mk_sigs ]
 
-      return $
-        [ TySynInstD ''DefiningModule
-            . TySynEqn [ConT tcName]
-            . LitT
-            . StrTyLit
-            $ loc_module loc
-        | hasTyFams
-        ] ++ sigs ++ decs
+  return $ join $ def_mod_fi : sigs ++ decs
 
-    _ -> fail "makeSem expects a type constructor"
+------------------------------------------------------------------------------
+-- | Generates signature for lifting function and type arguments to apply in
+-- its body on effect's data constructor.
+genSig :: ConLiftInfo -> Dec
+genSig cli
+  = SigD (cliFunName cli) $ quantifyType
+  $ ForallT [] (member_cxt : cliFunCxt cli)
+  $ foldArrows $ cliFunArgs cli ++ [sem `AppT` cliResType 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)
 
--- | Given the name of a GADT constructor, return the name of the corresponding
--- lifted function.
-getDeclName :: Name -> Name
-getDeclName = mkName . overFirst toLower . nameBase
- where
-  overFirst f (a : as) = f a : as
-  overFirst _ as       = as
+------------------------------------------------------------------------------
+-- | 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"
 
--- | Builds a function definition of the form @x a b c = send $ X a b c@.
-genDecl :: Con -> Q [Dec]
-genDecl (ForallC _       _     con) = genDecl con
-genDecl (GadtC   [cName] tArgs _  ) = do
-  let fnName = getDeclName cName
-  let arity  = length tArgs - 1
-  dTypeVars <- forM [0 .. arity] $ const $ newName "a"
-  pure $
-    [PragmaD (InlineP fnName Inlinable ConLike AllPhases)
-    , FunD fnName . pure $ Clause
-        (VarP <$> dTypeVars)
-        (NormalB . AppE (VarE 'send) $ foldl
-          (\b -> AppE b . VarE)
-          (ConE cName)
-          dTypeVars
-        )
-        []
+  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)
+
+  return
+    [ PragmaD $ InlineP (cliFunName cli) Inlinable ConLike AllPhases
+    , FunD (cliFunName cli)
+        [ Clause (VarP <$> fun_args_names)
+                 (NormalB $ AppE (VarE 'send) $ SigE action eff)
+                 []
+        ]
     ]
-genDecl _ = fail "genDecl expects a GADT constructor"
 
-tyVarBndrName :: TyVarBndr -> Name
-tyVarBndrName (PlainTV n) = n
-tyVarBndrName (KindedTV n _) = n
+-------------------------------------------------------------------------------
+-- | Info about constructor being lifted; use 'mkCLInfo' to create one.
+data ConLiftInfo = CLInfo
+  { cliEffName   :: Name    -- ^ name of effect's type constructor
+  , cliEffArgs   :: [Type]  -- ^ effect specific type arguments
+  , cliResType   :: Type    -- ^ result type specific to action
+  , cliConName   :: Name    -- ^ name of action constructor
+  , cliFunName   :: Name    -- ^ name of final function
+  , cliFunArgs   :: [Type]  -- ^ final function arguments
+  , cliFunCxt    :: Cxt     -- ^ constraints of final function
+  , cliUnionName :: Name    -- ^ name of type variable parameterizing 'Sem'
+  } deriving Show
 
-tyVarBndrKind :: TyVarBndr -> Maybe Type
-tyVarBndrKind (PlainTV _) = Nothing
-tyVarBndrKind (KindedTV _ k) = Just k
+------------------------------------------------------------------------------
+-- | 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
 
--- | Generates a function type from the corresponding GADT type constructor
--- @x :: Member (Effect e) r => a -> b -> c -> Sem r r@.
-genType :: Con -> Q (Type, Maybe Name, Maybe Type)
-genType (ForallC tyVarBindings conCtx con) = do
-  (t, mn, _) <- genType con
-  let k = do n <- mn
-             z <- find ((== n) . tyVarBndrName) tyVarBindings
-             tyVarBndrKind z
-      free = everything mappend freeVars t
-  pure ( ForallT (filter (flip elem free . tyVarBndrName) tyVarBindings) conCtx t
-       , mn
-       , k
-       )
-genType (GadtC   _ tArgs' (eff `AppT` m `AppT` tRet)) = do
-  r <- newName "r"
-  let
-    tArgs            = fmap snd tArgs'
-    memberConstraint = ConT ''Member `AppT` eff `AppT` VarT r
-    resultType       = ConT ''Sem `AppT` VarT r `AppT` tRet
+  (raw_cli_eff_args, [m_arg, raw_cli_res_arg]) <-
+    case splitAtEnd 2 $ datatypeInstTypes dti of
+      r@(_, [_, _]) -> return r
+      _             -> missingEffTArgs cliEffName
 
-    replaceMType t | t == m = ConT ''Sem `AppT` VarT r
-                   | otherwise = t
-    ts = everywhere (mkT replaceMType) tArgs
-    tn = case tRet of
-           VarT n -> Just n
-           _ -> Nothing
+  m_name <-
+    case tVarName m_arg of
+      Just r        -> return r
+      Nothing       -> mArgNotVar cliEffName m_arg
 
-  pure
-    . (, tn, Nothing)
-    .  ForallT [PlainTV r] [memberConstraint]
-    .  foldArrows
-    $  ts
-    ++ [resultType]
--- TODO: Although this should never happen, we obviously need a better error message below.
-genType _       = fail "genSig expects a GADT constructor"
+  cliUnionName <- newName "r"
 
--- | Turn all (KindedTV tv StarT) into (PlainTV tv) in the given type
--- This can prevent the need for KindSignatures
-simplifyBndrs :: Maybe Type -> Type -> Type
-simplifyBndrs star = everywhere (mkT $ simplifyBndr star)
+  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
 
--- | Turn TvVarBndrs of the form (KindedTV tv StarT) into (PlainTV tv)
--- This can prevent the need for KindSignatures
-simplifyBndr :: Maybe Type -> TyVarBndr -> TyVarBndr
-simplifyBndr (Just star) (KindedTV tv k) | star == k = PlainTV tv
-simplifyBndr _ (KindedTV tv StarT) = PlainTV tv
-simplifyBndr _ bndr = bndr
+      cliEffArgs            = normalizeType <$> raw_cli_eff_args
+      cliResType            = normalizeType     raw_cli_res_arg
+      cliConName            = constructorName ci
+      cliFunName            = mkName $ mapHead toLower $ nameBase
+                            $ constructorName ci
+      cliFunArgs            = normalizeType <$> constructorFields ci
 
--- | Generates a type signature of the form
--- @x :: Member (Effect e) r => a -> b -> c -> Sem r r@.
-genSig :: Con -> Q Dec
-genSig con = do
-  let
-    getConName (ForallC _ _ c) = getConName c
-    getConName (GadtC [n] _ _) = pure n
-    getConName c = fail $ "failed to get GADT name from " ++ show c
-  conName <- getConName con
-  (t, _, k) <- genType con
-  pure $ SigD (getDeclName conName) $ simplifyBndrs k t
+  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"
+
+missingEffTArgs :: Name -> Q a
+missingEffTArgs 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 = mkName $ nameBase $ 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
+
+------------------------------------------------------------------------------
+-- | 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
+
+------------------------------------------------------------------------------
 -- | Folds a list of 'Type's into a right-associative arrow 'Type'.
 foldArrows :: [Type] -> Type
-foldArrows = foldr1 (AppT . AppT ArrowT)
+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
 
-freeVars :: Data a => a -> [Name]
-freeVars = mkQ [] $ \case
-  VarT n -> [n]
-  _ -> []
+------------------------------------------------------------------------------
+-- | Constructs capturable name from base of input name.
+capturableBase :: Name -> Name
+capturableBase = mkName . nameBase
 
+------------------------------------------------------------------------------
+-- | 'splitAt' counting from the end.
+splitAtEnd :: Int -> [a] -> ([a], [a])
+splitAtEnd n = swap . join bimap reverse . splitAt n . reverse
+
+------------------------------------------------------------------------------
+-- | Applies function to head of list, if there is one.
+mapHead :: (a -> a) -> [a] -> [a]
+mapHead _ []     = []
+mapHead f (x:xs) = f x : xs
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
@@ -1,10 +1,12 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 {-# OPTIONS_HADDOCK not-home #-}
 
 module Polysemy.Internal.Tactics
   ( Tactics (..)
   , getInitialStateT
+  , getInspectorT
+  , Inspector (..)
   , runT
   , bindT
   , pureT
@@ -78,6 +80,7 @@
 data Tactics f n r m a where
   GetInitialState     :: Tactics f n r m (f ())
   HoistInterpretation :: (a -> n b) -> Tactics f n r m (f a -> Sem r (f b))
+  GetInspector        :: Tactics f n r m (Inspector f)
 
 
 ------------------------------------------------------------------------------
@@ -89,6 +92,40 @@
 
 
 ------------------------------------------------------------------------------
+-- | Get a natural transformation capable of potentially inspecting values
+-- inside of @f@. Binding the result of 'getInspectorT' produces a function that
+-- can sometimes peek inside values returned by 'bindT'.
+--
+-- This is often useful for running callback functions that are not managed by
+-- polysemy code.
+--
+-- ==== Example
+--
+-- We can use the result of 'getInspectT' to "undo" 'pureT' (or any of the other
+-- 'Tactical' functions):
+--
+-- @
+-- ins <- 'getInspectorT'
+-- fa <- 'pureT' "hello"
+-- fb <- 'pureT' True
+-- let a = 'inspect' ins fa   -- Just "hello"
+--     b = 'inspect' ins fb   -- Just True
+-- @
+--
+-- We
+getInspectorT :: forall e f m r. Sem (WithTactics e f m r) (Inspector f)
+getInspectorT = send @(Tactics _ m (e ': r)) GetInspector
+
+
+------------------------------------------------------------------------------
+-- | A container for 'inspect'. See the documentation for 'getInspectorT'.
+newtype Inspector f = Inspector
+  { inspect :: forall x. f x -> Maybe x
+    -- ^ See the documnetation for 'getInspectorT'.
+  }
+
+
+------------------------------------------------------------------------------
 -- | Lift a value into 'Tactical'.
 pureT :: a -> Tactical e m r a
 pureT a = do
@@ -150,15 +187,18 @@
    :: Functor f
    => f ()
    -> (∀ x. f (m x) -> Sem r2 (f x))
+   -> (∀ x. f x -> Maybe x)
    -> Sem (Tactics f m r2 ': r) a
    -> Sem r a
-runTactics s d (Sem m) = m $ \u ->
+runTactics s d v (Sem m) = m $ \u ->
   case decomp u of
-    Left x -> liftSem $ hoist (runTactics_b s d) x
-    Right (Yo GetInitialState s' _ y) ->
+    Left x -> liftSem $ hoist (runTactics_b s d v) x
+    Right (Yo GetInitialState s' _ y _) ->
       pure $ y $ s <$ s'
-    Right (Yo (HoistInterpretation na) s' _ y) -> do
+    Right (Yo (HoistInterpretation na) s' _ y _) -> do
       pure $ y $ (d . fmap na) <$ s'
+    Right (Yo GetInspector s' _ y _) -> do
+      pure $ y $ Inspector v <$ s'
 {-# INLINE runTactics #-}
 
 
@@ -166,6 +206,7 @@
    :: Functor f
    => f ()
    -> (∀ x. f (m x) -> Sem r2 (f x))
+   -> (∀ x. f x -> Maybe x)
    -> Sem (Tactics f m r2 ': r) a
    -> Sem r a
 runTactics_b = runTactics
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
@@ -31,6 +31,7 @@
   , Nat (..)
   ) where
 
+import Control.Monad
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Type.Equality
@@ -61,24 +62,26 @@
      -> f ()
      -> (forall x. f (m x) -> n (f x))
      -> (f a -> b)
+     -> (forall x. f x -> Maybe x)
      -> Yo e n b
 
 instance Functor (Yo e m) where
-  fmap f (Yo e s d f') = Yo e s d (f . f')
+  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 (Yo e s nt f) =
+  weave s' d v' (Yo e s nt f v) =
     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
+liftYo e = Yo e (Identity ()) (fmap Identity . runIdentity) runIdentity (Just . runIdentity)
 {-# INLINE liftYo #-}
 
 
@@ -88,7 +91,7 @@
 
 
 instance Effect (Union r) where
-  weave s f (Union w e) = Union w $ weave s f e
+  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
diff --git a/src/Polysemy/NonDet.hs b/src/Polysemy/NonDet.hs
--- a/src/Polysemy/NonDet.hs
+++ b/src/Polysemy/NonDet.hs
@@ -10,6 +10,7 @@
   ) where
 
 import Control.Applicative
+import Data.Maybe
 import Polysemy.Internal
 import Polysemy.Internal.NonDet
 import Polysemy.Internal.Union
@@ -58,10 +59,14 @@
 runNonDet (Sem m) = Sem $ \k -> runNonDetC $ m $ \u ->
   case decomp u of
     Left x  -> NonDetC $ \cons nil -> do
-      z <- k $ weave [()] (fmap concat . traverse runNonDet) x
+      z <- k $ weave [()]
+                     (fmap concat . traverse runNonDet)
+                     -- TODO(sandy): Is this the right semantics?
+                     listToMaybe
+                     x
       foldr cons nil z
-    Right (Yo Empty _ _ _) -> empty
-    Right (Yo (Choose ek) s _ y) -> do
+    Right (Yo Empty _ _ _ _) -> empty
+    Right (Yo (Choose ek) s _ y _) -> do
       z <- pure (ek False) <|> pure (ek True)
       pure $ y $ z <$ s
 
diff --git a/src/Polysemy/State.hs b/src/Polysemy/State.hs
--- a/src/Polysemy/State.hs
+++ b/src/Polysemy/State.hs
@@ -105,9 +105,10 @@
               . weave (s, ())
                       (\(s', m') -> fmap swap
                                   $ S.runStateT m' s')
+                      (Just . snd)
               $ hoist hoistStateIntoStateT_b x
-    Right (Yo Get z _ y)     -> fmap (y . (<$ z)) $ S.get
-    Right (Yo (Put s) z _ y) -> fmap (y . (<$ z)) $ S.put s
+    Right (Yo Get z _ y _)     -> fmap (y . (<$ z)) $ S.get
+    Right (Yo (Put s) z _ y _) -> fmap (y . (<$ z)) $ S.put s
 {-# INLINE hoistStateIntoStateT #-}
 
 
diff --git a/test/InspectorSpec.hs b/test/InspectorSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/InspectorSpec.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module InspectorSpec where
+
+import Control.Monad
+import Data.IORef
+import Polysemy
+import Polysemy.Error
+import Polysemy.State
+import Test.Hspec
+
+
+
+data Callback m a where
+  Callback :: m String -> Callback m ()
+
+makeSem ''Callback
+
+
+
+spec :: Spec
+spec = describe "Inspector" $ do
+  it "should inspect State effects" $ do
+    withNewTTY $ \ref -> do
+      void . (runM .@ runCallback ref)
+           . runState False
+           $ do
+        sendM $ pretendPrint ref "hello world"
+        callback $ show <$> get @Bool
+        modify not
+        callback $ show <$> get @Bool
+
+      result <- readIORef ref
+      result `shouldContain` ["hello world"]
+      result `shouldContain` ["False", "True"]
+
+  it "should not inspect thrown Error effects" $ do
+    withNewTTY $ \ref -> do
+      void . (runM .@ runCallback ref)
+           . runError @()
+           $ do
+        callback $ throw ()
+        callback $ pure "nice"
+
+      result <- readIORef ref
+      result `shouldContain` [":(", "nice"]
+
+
+runCallback
+    :: Member (Lift IO) r
+    => IORef [String]
+    -> (forall x. Sem r x -> IO x)
+    -> Sem (Callback ': r) a
+    -> Sem r a
+runCallback ref lower = interpretH $ \case
+  Callback cb -> do
+    cb' <- runT cb
+    ins <- getInspectorT
+    sendM $ doCB ref $ do
+      v <- lower .@ runCallback ref $ cb'
+      pure $ maybe ":(" id $ inspect ins v
+    getInitialStateT
+
+
+doCB :: IORef [String] -> IO String -> IO ()
+doCB ref m = m >>= pretendPrint ref
+
+
+pretendPrint :: IORef [String] -> String -> IO ()
+pretendPrint ref msg = modifyIORef ref (++ [msg])
+
+
+withNewTTY :: (IORef [String] -> IO a) -> IO a
+withNewTTY f = do
+  ref <- newIORef []
+  f ref
+