diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,19 @@
 # Changelog for polysemy
 
+## Unreleased
+
+## 1.6.0.0 (2021-07-12)
+
+### Breaking Changes
+
+* Deprecate `traceToIO` and replace it with `traceToStdout` and `traceToStderr`
+* Support GHC 9.0.1
+
+### Other Changes
+
+* Added the combinator `insertAt`, which allows adding effects at a specified index into the effect stack
+* Added `Semigroup` and `Monoid` for `Sem`
+
 ## 1.5.0.0 (2021-03-30)
 
 ### Breaking Changes
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -300,15 +300,15 @@
 [solution](https://github.com/lexi-lambda/ghc-proposals/blob/delimited-continuation-primops/proposals/0000-delimited-continuation-primops.md) -
 set of primops that will allow interpretation of effects at runtime, with
 minimal overhead. It's not *zero-cost* as we hoped for with `polysemy` at
-first, but it should have negligible effect on performance in real life  and
+first, but it should have negligible effect on performance in real life and
 compared to current solutions, it should be much more predictable and even
 resolve some problems with behaviour of
 [specific effects](https://github.com/polysemy-research/polysemy/issues/246).
 You can try out experimental library that uses proposed features
 [here](https://github.com/hasura/eff).
 
-When it comes to `polysemy`, once GHC proposal lands, we consider option of
-switching to implementation based on it. This will probably require some
+When it comes to `polysemy`, once GHC proposal lands, we will consider the option of
+switching to an implementation based on it. This will probably require some
 breaking changes, but should resolve performance issues and maybe even make
 implementation of higher-order effects easier.
 
diff --git a/polysemy.cabal b/polysemy.cabal
--- a/polysemy.cabal
+++ b/polysemy.cabal
@@ -5,9 +5,9 @@
 -- see: https://github.com/sol/hpack
 
 name:           polysemy
-version:        1.5.0.0
+version:        1.6.0.0
 synopsis:       Higher-order, low-boilerplate free monads.
-description:    Please see the README on GitHub at <https://github.com/isovector/polysemy#readme>
+description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy#readme>
 category:       Language
 homepage:       https://github.com/polysemy-research/polysemy#readme
 bug-reports:    https://github.com/polysemy-research/polysemy/issues
@@ -62,8 +62,10 @@
       Polysemy.Internal.CustomErrors.Redefined
       Polysemy.Internal.Fixpoint
       Polysemy.Internal.Forklift
+      Polysemy.Internal.Index
       Polysemy.Internal.Kind
       Polysemy.Internal.NonDet
+      Polysemy.Internal.Sing
       Polysemy.Internal.Strategy
       Polysemy.Internal.Tactics
       Polysemy.Internal.TH.Common
@@ -118,7 +120,6 @@
     , th-abstraction >=0.3.1.0 && <0.5
     , transformers >=0.5.2.0 && <0.6
     , type-errors >=0.2.0.0
-    , type-errors-pretty >=0.0.0.0 && <0.1
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions:
@@ -189,7 +190,7 @@
     , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
-    , doctest >=0.16.0.1 && <0.17
+    , doctest >=0.16.0.1 && <0.19
     , first-class-families >=0.5.0.0 && <0.9
     , hspec >=2.6.0 && <3
     , inspection-testing >=0.4.2 && <0.5
@@ -201,7 +202,6 @@
     , th-abstraction >=0.3.1.0 && <0.5
     , transformers >=0.5.2.0 && <0.6
     , type-errors >=0.2.0.0
-    , type-errors-pretty >=0.0.0.0 && <0.1
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions:
@@ -248,7 +248,6 @@
     , th-abstraction >=0.3.1.0 && <0.5
     , transformers >=0.5.2.0 && <0.6
     , type-errors >=0.2.0.0
-    , type-errors-pretty >=0.0.0.0 && <0.1
     , unagi-chan >=0.4.0.0 && <0.5
   if impl(ghc < 8.6)
     default-extensions:
diff --git a/src/Polysemy.hs b/src/Polysemy.hs
--- a/src/Polysemy.hs
+++ b/src/Polysemy.hs
@@ -35,6 +35,7 @@
   , raise3Under
   , raise_
   , subsume_
+  , insertAt
 
     -- * Trivial Interpretation
   , subsume
diff --git a/src/Polysemy/Bundle.hs b/src/Polysemy/Bundle.hs
--- a/src/Polysemy/Bundle.hs
+++ b/src/Polysemy/Bundle.hs
@@ -9,13 +9,13 @@
   , runBundle
   , subsumeBundle
     -- * Miscellaneous
-  , KnownList
   ) where
 
 import Polysemy
 import Polysemy.Internal
-import Polysemy.Internal.Bundle
 import Polysemy.Internal.Union
+import Polysemy.Internal.Bundle (subsumeMembership)
+import Polysemy.Internal.Sing (KnownList (singList))
 
 ------------------------------------------------------------------------------
 -- | An effect for collecting multiple effects into one effect.
@@ -58,8 +58,8 @@
   -> Sem (Append r' r) a
 runBundle = hoistSem $ \u -> hoist runBundle $ case decomp u of
   Right (Weaving (Bundle pr e) s wv ex ins) ->
-    Union (extendMembership @_ @r pr) $ Weaving e s wv ex ins
-  Left g -> weakenList @r' @r g
+    Union (extendMembershipRight @r' @r pr) $ Weaving e s wv ex ins
+  Left g -> weakenList @r' @r (singList @r') g
 {-# INLINE runBundle #-}
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Internal.hs b/src/Polysemy/Internal.hs
--- a/src/Polysemy/Internal.hs
+++ b/src/Polysemy/Internal.hs
@@ -30,6 +30,7 @@
   , Subsume (..)
   , subsume
   , subsumeUsing
+  , insertAt
   , Embed (..)
   , usingSem
   , liftSem
@@ -44,6 +45,8 @@
 import Control.Applicative
 import Control.Monad
 #if __GLASGOW_HASKELL__ < 808
+
+
 import Control.Monad.Fail
 #endif
 import Control.Monad.Fix
@@ -53,10 +56,13 @@
 import Polysemy.Embed.Type
 import Polysemy.Fail.Type
 import Polysemy.Internal.Fixpoint
+import Polysemy.Internal.Index (InsertAtUnprovidedIndex, InsertAtIndex(insertAtIndex))
 import Polysemy.Internal.Kind
 import Polysemy.Internal.NonDet
 import Polysemy.Internal.PluginLookup
 import Polysemy.Internal.Union
+import Type.Errors (WhenStuck)
+import Polysemy.Internal.Sing (ListOfLength (listOfLength))
 
 
 -- $setup
@@ -267,7 +273,7 @@
 
 
 instance Applicative (Sem f) where
-  pure a = Sem $ const $ pure a
+  pure a = Sem $ \_ -> pure a
   {-# INLINE pure #-}
 
   Sem f <*> Sem a = Sem $ \k -> f k <*> a k
@@ -307,7 +313,14 @@
   fail = send . Fail
   {-# INLINE fail #-}
 
+-- | @since 1.6.0.0
+instance Semigroup a => Semigroup (Sem f a) where
+  (<>) = liftA2 (<>)
 
+-- | @since 1.6.0.0
+instance Monoid a => Monoid (Sem f a) where
+  mempty = pure mempty
+
 ------------------------------------------------------------------------------
 -- | This instance will only lift 'IO' actions. If you want to lift into some
 -- other 'MonadIO' type, use this instance, and handle it via the
@@ -533,7 +546,33 @@
     go
 {-# INLINE subsumeUsing #-}
 
+------------------------------------------------------------------------------
+-- | Introduce a set of effects into 'Sem' at the index @i@, before the effect
+-- that previously occupied that position. This is intended to be used with a
+-- type application:
+--
+-- @
+-- let
+--   sem1 :: Sem [e1, e2, e3, e4, e5] a
+--   sem1 = insertAt @2 (sem0 :: Sem [e1, e2, e5] a)
+-- @
+--
+-- @since 1.6.0.0
+insertAt
+  :: forall index inserted head oldTail tail old full a
+   . ( ListOfLength index head
+     , WhenStuck index InsertAtUnprovidedIndex
+     , old ~ Append head oldTail
+     , tail ~ Append inserted oldTail
+     , full ~ Append head tail
+     , InsertAtIndex index head tail oldTail full inserted)
+  => Sem old a
+  -> Sem full a
+insertAt = hoistSem $ \u -> hoist (insertAt @index @inserted @head @oldTail) $
+  weakenMid @oldTail (listOfLength @index @head) (insertAtIndex @Effect @index @head @tail @oldTail @full @inserted) u
+{-# INLINE insertAt #-}
 
+
 ------------------------------------------------------------------------------
 -- | Embed an effect into a 'Sem'. This is used primarily via
 -- 'Polysemy.makeSem' to implement smart constructors.
@@ -579,11 +618,6 @@
       a <- unEmbed e
       pure $ f $ a <$ s
 {-# INLINE runM #-}
-
-
-type family Append l r where
-  Append (a ': l) r = a ': (Append l r)
-  Append '[] r = r
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Internal/Bundle.hs b/src/Polysemy/Internal/Bundle.hs
--- a/src/Polysemy/Internal/Bundle.hs
+++ b/src/Polysemy/Internal/Bundle.hs
@@ -2,15 +2,11 @@
 
 {-# OPTIONS_HADDOCK not-home #-}
 
-module Polysemy.Internal.Bundle (
-  module Polysemy.Internal.Bundle,
-  Append,
-) where
+module Polysemy.Internal.Bundle where
 
-import Data.Proxy
-import Polysemy
-import Polysemy.Internal (Append)
-import Polysemy.Internal.Union
+import Polysemy (Members)
+import Polysemy.Internal.Union (ElemOf(..), membership)
+import Polysemy.Internal.Kind (Append)
 
 extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
 extendMembership Here = Here
@@ -21,35 +17,3 @@
 subsumeMembership Here = membership @e @r'
 subsumeMembership (There (pr :: ElemOf e r'')) = subsumeMembership @r'' @r' pr
 {-# INLINE subsumeMembership #-}
-
-weakenList :: forall r' r m a
-            . KnownList r'
-           => Union r m a
-           -> Union (Append r' r) m a
-weakenList u = unconsKnownList @_ @r' u (\_ (_ :: Proxy r'') -> weaken (weakenList @r'' u))
-{-# INLINE weakenList #-}
-
-
-------------------------------------------------------------------------------
--- | A class for type-level lists with a known spine.
---
--- This constraint is eventually satisfied as @r@ is instantied to a
--- concrete list.
-class KnownList (l :: [k]) where
-  unconsKnownList :: (l ~ '[] => a)
-                  -> (  forall x r
-                      . (l ~ (x ': r), KnownList r)
-                     => Proxy x
-                     -> Proxy r
-                     -> a
-                     )
-                  -> a
-
-instance KnownList '[] where
-  unconsKnownList b _ = b
-  {-# INLINE unconsKnownList #-}
-
-instance KnownList r => KnownList (x ': r) where
-  unconsKnownList _ b = b Proxy Proxy
-  {-# INLINE unconsKnownList #-}
-
diff --git a/src/Polysemy/Internal/Combinators.hs b/src/Polysemy/Internal/Combinators.hs
--- a/src/Polysemy/Internal/Combinators.hs
+++ b/src/Polysemy/Internal/Combinators.hs
@@ -59,7 +59,7 @@
 -- transforming it into other effects inside of @r@.
 interpret
     :: FirstOrder e "interpret"
-    => (∀ x rInitial. e (Sem rInitial) x -> Sem r x)
+    => (∀ rInitial x. e (Sem rInitial) x -> Sem r x)
        -- ^ A natural transformation from the handled effect to other effects
        -- already in 'Sem'.
     -> Sem (e ': r) a
@@ -75,7 +75,7 @@
 --
 -- See the notes on 'Tactical' for how to use this function.
 interpretH
-    :: (∀ x rInitial . e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
+    :: (∀ rInitial x . e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
        -- ^ A natural transformation from the handled effect to other effects
        -- already in 'Sem'.
     -> Sem (e ': 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
@@ -13,6 +13,8 @@
   , UnhandledEffect
   , DefiningModule
   , DefiningModuleForEffect
+  , type (<>)
+  , type (%)
   ) where
 
 import Data.Kind
@@ -21,7 +23,6 @@
 import Polysemy.Internal.Kind
 import Polysemy.Internal.CustomErrors.Redefined
 import Type.Errors hiding (IfStuck, WhenStuck, UnlessStuck)
-import Type.Errors.Pretty (type (<>), type (%))
 
 
 ------------------------------------------------------------------------------
@@ -36,6 +37,20 @@
   DefiningModuleForEffect (e a) = DefiningModuleForEffect e
   DefiningModuleForEffect e     = DefiningModule e
 
+-- These are taken from type-errors-pretty because it's not in stackage for 9.0.1
+-- See https://github.com/polysemy-research/polysemy/issues/401
+type family ToErrorMessage (t :: k) :: ErrorMessage where
+    ToErrorMessage (t :: Symbol) = 'Text t
+    ToErrorMessage (t :: ErrorMessage) = t
+    ToErrorMessage t = 'ShowType t
+
+infixl 5 <>
+type family (<>) (l :: k1) (r :: k2) :: ErrorMessage where
+    l <> r = ToErrorMessage l ':<>: ToErrorMessage r
+
+infixr 4 %
+type family (%) (t :: k1) (b :: k2) :: ErrorMessage where
+    t % b = ToErrorMessage t ':$$: ToErrorMessage b
 
 -- TODO(sandy): Put in type-errors
 type ShowTypeBracketed t = "(" <> t <> ")"
diff --git a/src/Polysemy/Internal/Index.hs b/src/Polysemy/Internal/Index.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/Index.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Index where
+
+import GHC.TypeLits (Nat)
+import Type.Errors (TypeError, ErrorMessage(ShowType))
+
+import Polysemy.Internal.CustomErrors (type (<>), type (%))
+import Polysemy.Internal.Sing (SList (SEnd, SCons))
+
+------------------------------------------------------------------------------
+-- | Infer a partition of the result type @full@ so that for the fixed segments
+-- @head@ and @tail@, the new segment @inserted@ contains the missing effects
+-- between them.
+class InsertAtIndex (index :: Nat) (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k]) where
+  insertAtIndex :: SList inserted
+
+instance inserted ~ '[] => InsertAtIndex index head oldTail oldTail full inserted where
+  insertAtIndex = SEnd
+  {-# INLINE insertAtIndex #-}
+
+instance {-# INCOHERENT #-} (
+    InsertAtIndex index head tail oldTail full insertedTail,
+    inserted ~ (e ': insertedTail)
+  ) => InsertAtIndex index head (e ': tail) oldTail full inserted where
+    insertAtIndex = SCons (insertAtIndex @_ @index @head @tail @oldTail @full)
+    {-# INLINE insertAtIndex #-}
+
+instance {-# INCOHERENT #-} TypeError (InsertAtFailure index oldTail head full)
+       => InsertAtIndex index head tail oldTail full inserted where
+  insertAtIndex = error "unreachable"
+
+type family InsertAtUnprovidedIndex where
+  InsertAtUnprovidedIndex = TypeError (
+    "insertAt: You must provide the index at which the effects should be inserted as a type application."
+    % "Example: insertAt @5"
+    )
+
+type InsertAtFailure index soughtTail head full =
+  "insertAt: Failed to insert effects at index " <> 'ShowType index
+  % "There is a mismatch between what's been determined as the head and tail between the newly inserted effects,"
+  <> " and the actual desired return type."
+  % "Determined head before inserted effects:"
+  % "\t" <> 'ShowType head
+  % "Determined tail after the inserted effects:"
+  % "\t" <> 'ShowType soughtTail
+  % "Actual desired return type:"
+  % "\t" <> 'ShowType full
+  % "Make sure that the index provided to insertAt is correct, and that the desired return type simply requires"
+  <> " inserting effects."
diff --git a/src/Polysemy/Internal/Kind.hs b/src/Polysemy/Internal/Kind.hs
--- a/src/Polysemy/Internal/Kind.hs
+++ b/src/Polysemy/Internal/Kind.hs
@@ -1,6 +1,8 @@
+{-# OPTIONS_HADDOCK not-home #-}
+
 module Polysemy.Internal.Kind where
 
-import Data.Kind
+import Data.Kind (Type)
 
 ------------------------------------------------------------------------------
 -- | The kind of effects.
@@ -14,3 +16,7 @@
 -- @since 0.5.0.0
 type EffectRow = [Effect]
 
+
+type family Append l r where
+  Append (a ': l) r = a ': (Append l r)
+  Append '[] r = r
diff --git a/src/Polysemy/Internal/Sing.hs b/src/Polysemy/Internal/Sing.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/Sing.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Sing where
+
+import GHC.TypeLits (type (-), Nat)
+import Polysemy.Internal.Kind (Effect)
+
+data SList l where
+  SEnd  :: SList '[]
+  SCons :: SList xs -> SList (x ': xs)
+
+class KnownList l where
+  singList :: SList l
+
+instance KnownList '[] where
+  singList = SEnd
+  {-# INLINE singList #-}
+
+instance KnownList xs => KnownList (x ': xs) where
+  singList = SCons singList
+  {-# INLINE singList #-}
+
+class ListOfLength (n :: Nat) (l :: [Effect]) where
+  listOfLength :: SList l
+
+instance {-# OVERLAPPING #-} (l ~ '[]) => ListOfLength 0 l where
+  listOfLength = SEnd
+  {-# INLINE listOfLength #-}
+
+instance (ListOfLength (n - 1) xs, l ~ (x ': xs)) => ListOfLength n l where
+  listOfLength = SCons (listOfLength @(n - 1))
+  {-# INLINE listOfLength #-}
diff --git a/src/Polysemy/Internal/TH/Common.hs b/src/Polysemy/Internal/TH/Common.hs
--- a/src/Polysemy/Internal/TH/Common.hs
+++ b/src/Polysemy/Internal/TH/Common.hs
@@ -215,7 +215,11 @@
       )
   where
     base = capturableBase name
+#if MIN_VERSION_template_haskell(2,17,0)
+    args = flip PlainTV () . mkName <$> ["m", "a"]
+#else
     args = PlainTV . mkName <$> ["m", "a"]
+#endif
 
 notDataCon :: Name -> Q a
 notDataCon name = fail $ show
@@ -226,12 +230,20 @@
 -- TH utilities --------------------------------------------------------------
 ------------------------------------------------------------------------------
 
+arrows :: Type -> Bool
+arrows = \case
+  ArrowT -> True
+#if MIN_VERSION_template_haskell(2,17,0)
+  AppT MulArrowT _ -> True
+#endif
+  _ -> False
+
 ------------------------------------------------------------------------------
 -- | Pattern constructing function type and matching on one that may contain
 -- type annotations on arrow itself.
 infixr 1 :->
 pattern (:->) :: Type -> Type -> Type
-pattern a :-> b <- (removeTyAnns -> ArrowT) `AppT` a `AppT` b where
+pattern a :-> b <- (arrows . removeTyAnns -> True) `AppT` a `AppT` b where
   a :-> b = ArrowT `AppT` a `AppT` b
 
 
@@ -249,8 +261,13 @@
   VarT n          -> VarT $ capturableBase n
   ForallT bs cs t -> ForallT (goBndr <$> bs) (capturableTVars <$> cs) t
     where
+#if MIN_VERSION_template_haskell(2,17,0)
+      goBndr (PlainTV n flag) = PlainTV (capturableBase n) flag
+      goBndr (KindedTV n flag k) = KindedTV (capturableBase n) flag $ capturableTVars k
+#else
       goBndr (PlainTV n   ) = PlainTV $ capturableBase n
       goBndr (KindedTV n k) = KindedTV (capturableBase n) $ capturableTVars k
+#endif
   t -> t
 
 
@@ -274,8 +291,13 @@
   SigT t VarT{}   -> t
   ForallT bs cs t -> ForallT (goBndr <$> bs) (simplifyKinds <$> cs) t
     where
-      goBndr (KindedTV n StarT ) = PlainTV n
+#if MIN_VERSION_template_haskell(2,17,0)
+      goBndr (KindedTV n flag StarT) = PlainTV n flag
+      goBndr (KindedTV n flag VarT{}) = PlainTV n flag
+#else
+      goBndr (KindedTV n StarT) = PlainTV n
       goBndr (KindedTV n VarT{}) = PlainTV n
+#endif
       goBndr b = b
   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
@@ -108,7 +108,7 @@
 makeSem_ = genFreer False
 -- NOTE(makeSem_):
 -- This function uses an ugly hack to work --- it changes names in data
--- constructor's type to capturable ones. This allows user to provide them to
+-- constructor's type to capturable ones. This allows users 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).
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
@@ -127,7 +127,7 @@
 
 ------------------------------------------------------------------------------
 -- | Lift a value into 'Tactical'.
-pureT :: a -> Tactical e m r a
+pureT :: Functor f => a -> Sem (WithTactics e f m r) (f a)
 pureT a = do
   istate <- getInitialStateT
   pure $ a <$ istate
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
@@ -39,7 +39,11 @@
   -- * Checking membership
   , KnownRow
   , tryMembership
-  ) where
+  , extendMembershipLeft
+  , extendMembershipRight
+  , injectMembership
+  , weakenList
+  , weakenMid) where
 
 import Control.Monad
 import Data.Functor.Compose
@@ -48,6 +52,7 @@
 import Data.Typeable
 import Polysemy.Internal.Kind
 import {-# SOURCE #-} Polysemy.Internal
+import Polysemy.Internal.Sing (SList (SEnd, SCons))
 
 #ifndef NO_ERROR_MESSAGES
 import Polysemy.Internal.CustomErrors
@@ -251,7 +256,42 @@
 tryMembership = tryMembership' @r @e
 {-# INLINE tryMembership #-}
 
+
 ------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @r@ to a proof that @e@ is an
+-- element of the concatenation of the lists @l@ and @r@.
+-- @l@ must be specified as a singleton list proof.
+extendMembershipLeft :: forall l r e. SList l -> ElemOf e r -> ElemOf e (Append l r)
+extendMembershipLeft SEnd pr = pr
+extendMembershipLeft (SCons l) pr = There (extendMembershipLeft l pr)
+{-# INLINE extendMembershipLeft #-}
+
+
+------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @l@ to a proof that @e@ is an
+-- element of the concatenation of the lists @l@ and @r@.
+extendMembershipRight :: forall l r e. ElemOf e l -> ElemOf e (Append l r)
+extendMembershipRight Here = Here
+extendMembershipRight (There e) = There (extendMembershipRight @_ @r e)
+{-# INLINE extendMembershipRight #-}
+
+
+------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @left <> right@ to a proof that
+-- @e@ is an element of @left <> mid <> right@.
+-- Both @left@ and @right@ must be specified as singleton list proofs.
+injectMembership :: forall right e left mid
+                  . SList left
+                 -> SList mid
+                 -> ElemOf e (Append left right)
+                 -> ElemOf e (Append left (Append mid right))
+injectMembership SEnd sm pr = extendMembershipLeft sm pr
+injectMembership (SCons _) _ Here = Here
+injectMembership (SCons sl) sm (There pr) = There (injectMembership @right sl sm pr)
+{-# INLINE injectMembership #-}
+
+
+------------------------------------------------------------------------------
 -- | Decompose a 'Union'. Either this union contains an effect @e@---the head
 -- of the @r@ list---or it doesn't.
 decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)
@@ -282,11 +322,31 @@
 
 
 ------------------------------------------------------------------------------
--- | Weaken a 'Union' so it is capable of storing a new sort of effect.
+-- | Weaken a 'Union' so it is capable of storing a new sort of effect at the
+-- head.
 weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
 weaken (Union pr a) = Union (There pr) a
 {-# INLINE weaken #-}
 
+
+------------------------------------------------------------------------------
+-- | Weaken a 'Union' so it is capable of storing a number of new effects at
+-- the head, specified as a singleton list proof.
+weakenList :: SList l -> Union r m a -> Union (Append l r) m a
+weakenList sl (Union pr e) = Union (extendMembershipLeft sl pr) e
+{-# INLINE weakenList #-}
+
+
+------------------------------------------------------------------------------
+-- | Weaken a 'Union' so it is capable of storing a number of new effects
+-- somewhere within the previous effect list.
+-- Both the prefix and the new effects are specified as singleton list proofs.
+weakenMid :: forall right m a left mid
+           . SList left -> SList mid
+          -> Union (Append left right) m a
+          -> Union (Append left (Append mid right)) m a
+weakenMid sl sm (Union pr e) = Union (injectMembership @right sl sm pr) e
+{-# INLINE weakenMid #-}
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Trace.hs b/src/Polysemy/Trace.hs
--- a/src/Polysemy/Trace.hs
+++ b/src/Polysemy/Trace.hs
@@ -8,6 +8,9 @@
   , trace
 
     -- * Interpretations
+  , traceToHandle
+  , traceToStdout
+  , traceToStderr
   , traceToIO
   , runTraceList
   , ignoreTrace
@@ -19,6 +22,7 @@
 
 import Polysemy
 import Polysemy.Output
+import System.IO (stdout, stderr, hPutStrLn, Handle)
 
 
 ------------------------------------------------------------------------------
@@ -30,13 +34,41 @@
 
 
 ------------------------------------------------------------------------------
+-- | Run a 'Trace' effect by printing the messages to the provided 'Handle'.
+--
+-- @since 1.6.0.0
+traceToHandle :: Member (Embed IO) r => Handle -> Sem (Trace ': r) a -> Sem r a
+traceToHandle handle = interpret $ \case
+  Trace m -> embed $ hPutStrLn handle m
+{-# INLINE traceToHandle #-}
+
+
+------------------------------------------------------------------------------
 -- | Run a 'Trace' effect by printing the messages to stdout.
 --
+-- @since 1.6.0.0
+traceToStdout :: Member (Embed IO) r => Sem (Trace ': r) a -> Sem r a
+traceToStdout = traceToHandle stdout
+{-# INLINE traceToStdout #-}
+
+
+------------------------------------------------------------------------------
+-- | Run a 'Trace' effect by printing the messages to stderr.
+--
+-- @since 1.6.0.0
+traceToStderr :: Member (Embed IO) r => Sem (Trace ': r) a -> Sem r a
+traceToStderr = traceToHandle stderr
+{-# INLINE traceToStderr #-}
+
+
+------------------------------------------------------------------------------
+-- | Run a 'Trace' effect by printing the messages to stdout.
+--
 -- @since 1.0.0.0
 traceToIO :: Member (Embed IO) r => Sem (Trace ': r) a -> Sem r a
-traceToIO = interpret $ \case
-  Trace m -> embed $ putStrLn m
+traceToIO = traceToStdout
 {-# INLINE traceToIO #-}
+{-# deprecated traceToIO "Use traceToStdout" #-}
 
 
 ------------------------------------------------------------------------------
diff --git a/test/FusionSpec.hs b/test/FusionSpec.hs
--- a/test/FusionSpec.hs
+++ b/test/FusionSpec.hs
@@ -36,7 +36,6 @@
 spec = parallel $ do
   describe "fusion" $ do
 -- #if __GLASGOW_HASKELL__ >= 807
---     -- TODO: Investigate why this test fails mysteriously on GHC < 8.6
 --     it "Union proofs should simplify" $ do
 --       shouldSucceed $(inspectTest $ 'countDown `hasNoType` ''SNat)
 -- #endif
diff --git a/test/TypeErrors.hs b/test/TypeErrors.hs
--- a/test/TypeErrors.hs
+++ b/test/TypeErrors.hs
@@ -91,8 +91,8 @@
 -- ...
 -- ... Unhandled effect 'Embed IO'
 -- ...
--- ... Expected type: Sem '[Embed m] (Bool, ())
--- ... Actual type: Sem '[] (Bool, ())
+-- ... Expected... Sem '[Embed m] (Bool, ())
+-- ... Actual... Sem '[] (Bool, ())
 -- ...
 runningTooManyEffects = ()
 
@@ -119,8 +119,8 @@
 --  in runM $ lowerResource foo
 -- :}
 -- ...
--- ... Couldn't match expected type ...
--- ... with actual type ...
+-- ... Couldn't match expected type...
+-- ... with actual type...
 -- ... Probable cause: ... is applied to too few arguments
 -- ...
 missingArgumentToRunResourceInIO = ()