diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,16 @@
 # Revision history for capability
 
+## 0.4.0.0 -- 2021-03-15
+
+* Fix infinite loop in `writer`.
+  See [#85](https://github.com/tweag/capability/pull/85)
+
+* Introduce `Capability.Reflection` to define ad-hoc interpreters.
+  See [#86](https://github.com/tweag/capability/pull/86)
+
+* Fix compatibility with GHC 8.10.
+  See [#87](https://github.com/tweag/capability/pull/87)
+
 ## 0.3.0.0 -- 2020-03-19
 
 * Rename HasStream to HasSink, for symmetry.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -132,10 +132,7 @@
 
 ### Nix Shell
 
-Some of this package's dependencies require patches to build with GHC 8.6.
-These patches are defined in
-[`nix/haskell/default.nix`](nix/haskell/default.nix).
-A development environment with all patched dependencies in scope is defined in
+A development environment with all dependencies in scope is defined in
 [`shell.nix`](shell.nix).
 
 ### Build
diff --git a/capability.cabal b/capability.cabal
--- a/capability.cabal
+++ b/capability.cabal
@@ -1,5 +1,5 @@
 name: capability
-version: 0.3.0.0
+version: 0.4.0.0
 homepage: https://github.com/tweag/capability
 license: BSD3
 license-file: LICENSE.md
@@ -12,7 +12,7 @@
   CONTRIBUTING.md
   README.md
 cabal-version: 1.18
-tested-with: GHC==8.6.1
+tested-with: GHC==8.10.4
 synopsis: Extensional capabilities and deriving combinators
 description:
   Standard capability type classes for extensional effects and combinators
@@ -44,6 +44,7 @@
     Capability.Reader
     Capability.Reader.Internal.Class
     Capability.Reader.Internal.Strategies
+    Capability.Reflection
     Capability.Sink
     Capability.Sink.Internal.Class
     Capability.Sink.Internal.Strategies
@@ -59,22 +60,23 @@
     Capability.Writer
     Capability.Writer.Discouraged
   build-depends:
-      base >= 4.12 && < 5.0
-    , constraints >= 0.1 && < 0.12
+      base >= 4.14 && < 5.0
+    , constraints >= 0.1 && < 0.13
     , dlist >= 0.8 && < 0.9
     , exceptions >= 0.6 && < 0.11
-    , generic-lens >= 1.0 && < 1.3
+    , generic-lens >= 2.0 && < 2.1
     , lens >= 4.16 && < 5.0
     , monad-control >= 1.0 && < 1.1
     , monad-unlift >= 0.2 && < 0.3
     , mtl >= 2.0 && < 3.0
     , mutable-containers >= 0.3 && < 0.4
     , primitive >= 0.6 && < 0.8
+    , reflection >= 2.1 && < 2.2
     , safe-exceptions >= 0.1 && < 0.2
     , streaming >= 0.2 && < 0.3
     , transformers >= 0.5.5 && < 0.6
     , unliftio >= 0.2 && < 0.3
-    , unliftio-core >= 0.1 && < 0.2
+    , unliftio-core >= 0.1 && < 0.3
   if flag(dev)
     ghc-options: -Wall -Werror -Wcompat
                  -Wincomplete-record-updates
@@ -88,6 +90,7 @@
 test-suite examples
   type: exitcode-stdio-1.0
   other-modules:
+    Reflection
     WordCount
     CountLog
     Error
@@ -98,17 +101,18 @@
     Writer
   main-is: Test.hs
   build-depends:
-      base >= 4.12 && < 5.0
+      base >= 4.14 && < 5.0
     , capability
-    , containers >= 0.6 && < 0.7
-    , hspec >= 2.0 && < 3.0
-    , lens >= 4.16 && < 5.0
-    , mtl >= 2.0 && < 3.0
-    , silently >= 1.2 && < 1.3
-    , streaming >= 0.2 && < 0.3
-    , temporary >= 1.0 && < 1.4
-    , text >= 0.2 && < 1.3
-    , unliftio >= 0.2 && < 0.3
+    , containers
+    , dlist
+    , hspec
+    , lens
+    , mtl
+    , silently
+    , streaming
+    , temporary
+    , text
+    , unliftio
   if flag(hspec-jenkins)
     build-depends: hspec-jenkins
   if flag(dev)
diff --git a/examples/CountLog.hs b/examples/CountLog.hs
--- a/examples/CountLog.hs
+++ b/examples/CountLog.hs
@@ -22,6 +22,7 @@
 import qualified Data.Char
 import Data.Coerce (coerce)
 import Data.IORef
+import Data.Kind (Type)
 import GHC.Generics (Generic)
 import Test.Common
 import Test.Hspec
@@ -63,7 +64,7 @@
 
 
 -- | Deriving @HasReader@ from @MonadReader@.
-newtype LogM m (a :: *) = LogM (ReaderT LogCtx m a)
+newtype LogM m (a :: Type) = LogM (ReaderT LogCtx m a)
   deriving (Functor, Applicative, Monad)
   deriving Logger via
     (TheLoggerReader (Field "logger" ()
@@ -110,7 +111,7 @@
 -- ReaderT IORef instance --------------------------------------------
 
 -- | Deriving @HasState@ from @HasReader@ of an @IORef@.
-newtype Counter'M m (a :: *) = Counter'M (ReaderT (IORef Int) m a)
+newtype Counter'M m (a :: Type) = Counter'M (ReaderT (IORef Int) m a)
   deriving (Functor, Applicative, Monad)
   deriving Counter via
     TheCounterState (ReaderIORef (MonadReader (ReaderT (IORef Int) m)))
@@ -139,7 +140,7 @@
 
 
 -- | Deriving two capabilities from the record fields of @MonadReader@.
-newtype CountLogM m (a :: *) = CountLogM (ReaderT CountLogCtx m a)
+newtype CountLogM m (a :: Type) = CountLogM (ReaderT CountLogCtx m a)
   deriving (Functor, Applicative, Monad)
   deriving Counter via
     TheCounterState (ReaderIORef (Rename "countCtx" (Field "countCtx" ()
diff --git a/examples/Error.hs b/examples/Error.hs
--- a/examples/Error.hs
+++ b/examples/Error.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
diff --git a/examples/Reader.hs b/examples/Reader.hs
--- a/examples/Reader.hs
+++ b/examples/Reader.hs
@@ -14,6 +14,7 @@
 import Capability.Source
 import Control.Monad.IO.Class (MonadIO, liftIO)
 import Control.Monad.Reader (ReaderT (..))
+import Data.Kind (Type)
 import GHC.Generics (Generic)
 import Test.Common
 import Test.Hspec
@@ -21,8 +22,8 @@
 data Foo
 data Bar
 
-type instance TypeOf * Foo = Int
-type instance TypeOf * Bar = Int
+type instance TypeOf Type Foo = Int
+type instance TypeOf Type Bar = Int
 
 ----------------------------------------------------------------------
 -- Example Programs
@@ -65,7 +66,7 @@
 -- Instances
 
 -- | @HasReader@ instance derived via @MonadReader@.
-newtype FooReaderT m (a :: *) = FooReaderT (ReaderT Int m a)
+newtype FooReaderT m (a :: Type) = FooReaderT (ReaderT Int m a)
   deriving (Functor, Applicative, Monad, MonadIO)
   deriving (HasSource Foo Int) via MonadReader (ReaderT Int m)
   deriving (HasReader Foo Int) via MonadReader (ReaderT Int m)
diff --git a/examples/Reflection.hs b/examples/Reflection.hs
new file mode 100644
--- /dev/null
+++ b/examples/Reflection.hs
@@ -0,0 +1,255 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Reflection where
+
+import Capability.Error
+import Capability.Reader
+import Capability.Reflection
+import Capability.Sink
+import Capability.Source
+import Capability.State
+import Capability.Writer
+import Control.Monad (forM_, replicateM)
+import qualified Control.Monad.Except as MTL
+import qualified Control.Monad.State as MTL
+import Data.DList (DList)
+import qualified Data.DList as DList
+import Data.Monoid (Product (..))
+import Test.Hspec
+
+----------------------------------------------------------------------
+-- Instances
+
+newtype Logger s a = Logger (MTL.State (DList String, s) a)
+  deriving (Functor, Applicative, Monad)
+  deriving
+    (HasSink "log" String)
+    via SinkDList (SinkLog (Rename 1 (Pos 1 () (MonadState (MTL.State (DList String, s))))))
+  deriving
+    (HasState "test" s, HasSource "test" s, HasSink "test" s)
+    via Rename 2 (Pos 2 () (MonadState (MTL.State (DList String, s))))
+
+runLogger :: s -> Logger s a -> (a, s, [String])
+runLogger s0 (Logger m) =
+  case MTL.runState m (mempty, s0) of
+    (a, (log', s)) -> (a, s, DList.toList log')
+
+----------------------------------------------------------------------
+-- Test Cases
+
+spec :: Spec
+spec = do
+  describe "interpret_" $ do
+    it "evaluates HasSource" $ do
+      runLogger
+        [1, 2, 3 :: Int]
+        ( interpret_ @"source"
+            ReifiedSource
+              { _await = do
+                  yield @"log" "await"
+                  state @"test" $ \case
+                    (x : xs) -> (x, xs)
+                    [] -> error "empty stream"
+              }
+            (replicateM 3 $ await @"source")
+        )
+        `shouldBe` ([1, 2, 3], [], ["await", "await", "await"])
+    it "evaluates HasSink" $ do
+      runLogger
+        []
+        ( interpret_ @"sink"
+            ReifiedSink
+              { _yield = \x -> do
+                  yield @"log" "yield"
+                  modify @"test" (x :)
+              }
+            (forM_ [1, 2, 3 :: Int] $ yield @"sink")
+        )
+        `shouldBe` ((), [3, 2, 1], ["yield", "yield", "yield"])
+    it "evaluates HasReader" $ do
+      runLogger
+        (42 :: Int)
+        ( interpret_ @"reader"
+            ReifiedReader
+              { _readerSource =
+                  ReifiedSource
+                    { _await = do
+                        yield @"log" "ask"
+                        get @"test"
+                    },
+                _local = \f m -> do
+                  yield @"log" "local"
+                  r <- state @"test" $ \r -> (r, f r)
+                  a <- m
+                  put @"test" r
+                  pure a,
+                _reader = \f -> do
+                  yield @"log" "reader"
+                  f <$> get @"test"
+              }
+            ( sequence
+                [ ask @"reader",
+                  local @"reader" succ $ do
+                    asks @"reader" succ,
+                  reader @"reader" pred
+                ]
+            )
+        )
+        `shouldBe` ([42, 44, 41], 42, ["ask", "local", "ask", "reader"])
+    it "evaluates HasState" $ do
+      runLogger
+        (42 :: Int)
+        ( interpret_ @"state"
+            ReifiedState
+              { _stateSource =
+                  ReifiedSource
+                    { _await = do
+                        yield @"log" "get"
+                        get @"test"
+                    },
+                _stateSink =
+                  ReifiedSink
+                    { _yield = \x -> do
+                        yield @"log" "put"
+                        put @"test" x
+                    },
+                _state = \f -> do
+                  yield @"log" "state"
+                  state @"test" f
+              }
+            ( do
+                old <- get @"state"
+                put @"state" 0
+                state @"state" (\new -> (old, succ new))
+            )
+        )
+        `shouldBe` (42, 1, ["get", "put", "state"])
+    it "evaluates HasWriter" $ do
+      runLogger
+        (mempty :: Product Int)
+        ( interpret_ @"writer"
+            ReifiedWriter
+              { _writerSink =
+                  ReifiedSink
+                    { _yield = \w -> do
+                        yield @"log" "tell"
+                        modify @"test" (<> w)
+                    },
+                _writer = \(a, w) -> do
+                  yield @"log" "writer"
+                  modify @"test" (<> w)
+                  pure a,
+                _listen = \m -> do
+                  yield @"log" "listen"
+                  w0 <- state @"test" $ \s -> (s, mempty)
+                  a <- m
+                  w <- state @"test" $ \s -> (s, w0 <> s)
+                  pure (a, w),
+                _pass = \m -> do
+                  yield @"log" "pass"
+                  w0 <- state @"test" $ \s -> (s, mempty)
+                  (a, f) <- m
+                  modify' @"test" $ \s -> w0 <> f s
+                  pure a
+              }
+            ( do
+                tell @"writer" 2
+                writer @"writer" ((), 3)
+                ((), w) <- listen @"writer" $ do
+                  tell @"writer" 5
+                pass @"writer" $ do
+                  tell @"writer" 6
+                  pure ((), (+ 1))
+                pure w
+            )
+        )
+        `shouldBe` (5, 2 * 3 * 5 * 7, ["tell", "writer", "listen", "tell", "pass", "tell"])
+    it "evaluates HasThrow" $ do
+      runLogger
+        ()
+        ( MTL.runExceptT $
+            interpret_ @"throw"
+              ReifiedThrow
+                { _throw = \e -> do
+                    MTL.lift $ yield @"log" "throw"
+                    MTL.throwError e
+                }
+              ( do
+                  _ <- throw @"throw" "some error"
+                  pure $! tail ""
+              )
+        )
+        `shouldBe` (Left "some error", (), ["throw"])
+    it "evaluates HasCatch" $ do
+      runLogger
+        ()
+        ( MTL.runExceptT $
+            interpret_ @"catch"
+              ReifiedCatch
+                { _catchThrow =
+                    ReifiedThrow
+                      { _throw = \e -> do
+                          MTL.lift $ yield @"log" "throw"
+                          MTL.throwError e
+                      },
+                  _catch = \m h -> do
+                    MTL.lift $ yield @"log" "catch"
+                    MTL.catchError m h,
+                  _catchJust = \f m h -> do
+                    MTL.lift $ yield @"log" "catchJust"
+                    MTL.catchError m $ \e ->
+                      case f e of
+                        Just b -> h b
+                        Nothing -> MTL.throwError e
+                }
+              ( do
+                  e1 <-
+                    catch @"catch"
+                      ( do
+                          _ <- throw @"catch" "some error"
+                          pure $! tail ""
+                      )
+                      pure
+                  catchJust @"catch"
+                    (const Nothing)
+                    ( do
+                        _ <- throw @"catch" ("again " ++ e1)
+                        pure $! tail ""
+                    )
+                    pure
+              )
+        )
+        `shouldBe` (Left "again some error", (), ["catch", "throw", "catchJust", "throw"])
+  describe "interpret" $ do
+    it "can be nested" $ do
+      runLogger
+        ()
+        ( interpret @"source" @'[HasSink "log" String]
+            ReifiedSource
+              { _await = do
+                  yield @"log" "await"
+                  pure ()
+              }
+            ( interpret @"sink" @'[HasSink "log" String, HasSource "source" ()]
+                ReifiedSink
+                  { _yield = \() -> do
+                      yield @"log" "yield"
+                      pure ()
+                  }
+                ( do
+                    yield @"log" "begin"
+                    await @"source"
+                    yield @"sink" ()
+                    yield @"log" "end"
+                )
+            )
+        )
+        `shouldBe` ((), (), ["begin", "await", "yield", "end"])
diff --git a/examples/Test.hs b/examples/Test.hs
--- a/examples/Test.hs
+++ b/examples/Test.hs
@@ -14,6 +14,7 @@
 import qualified CountLog
 import qualified Error
 import qualified Reader
+import qualified Reflection
 import qualified State
 import qualified Sink
 import qualified Writer
@@ -25,6 +26,7 @@
   describe "CountLog" CountLog.spec
   describe "Error" Error.spec
   describe "Reader" Reader.spec
+  describe "Reflection" Reflection.spec
   describe "State" State.spec
   describe "Sink" Sink.spec
   describe "Writer" Writer.spec
diff --git a/src/Capability.hs b/src/Capability.hs
--- a/src/Capability.hs
+++ b/src/Capability.hs
@@ -108,14 +108,18 @@
 -- combinators which you can use if you absolutely must: they are correct, but
 -- inefficient, so we recommend that you do not.
 --
--- Finally there is
+-- Finally there are
 --
 -- * "Capability.Derive"
---
 -- Which exports a (still experimental) 'Capability.Derive.derive' function,
 -- which lets you run a computation which requires capabilities which are not
 -- directly provided by the ambient monad, but can be derived from the
 -- capabilities provided by the ambient monad.
+-- * "Capability.Reflection"
+-- Which exports 'Capability.Reflection.interpret_' and
+-- 'Capability.Reflection.interpret', which let you define an ad-hoc
+-- interpretation of a capability based on the capabilities provided by the
+-- ambient monad.
 --
 -- == Further considerations
 --
diff --git a/src/Capability/Accessors.hs b/src/Capability/Accessors.hs
--- a/src/Capability/Accessors.hs
+++ b/src/Capability/Accessors.hs
@@ -20,6 +20,7 @@
 
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Primitive (PrimMonad)
+import Data.Kind (Type)
 import GHC.TypeLits (Nat, Symbol)
 
 -- | Coerce the type in the context @m@ to @to@.
@@ -37,7 +38,7 @@
 -- @'Capability.Reader.MonadReader' (Reader Int)@ to a
 -- @'Capability.Reader.HasReader' \"a\" MyInt@
 -- instance using @Coercible Int MyInt@.
-newtype Coerce (to :: *) m (a :: *) = Coerce (m a)
+newtype Coerce (to :: Type) m (a :: Type) = Coerce (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Rename the tag.
@@ -58,7 +59,7 @@
 -- and @Rename@ is redundant in this example.
 --
 -- See 'Pos' below for a common use-case.
-newtype Rename (oldtag :: k) m (a :: *) = Rename (m a)
+newtype Rename (oldtag :: k) m (a :: Type) = Rename (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Access the record field @field@ in the context @m@.
@@ -78,7 +79,7 @@
 -- instance by focusing on the field @foo@ in the @Foo@ record.
 --
 -- See 'Rename' for a way to change the tag.
-newtype Field (field :: Symbol) (oldtag :: k) m (a :: *) = Field (m a)
+newtype Field (field :: Symbol) (oldtag :: k) m (a :: Type) = Field (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Access the value at position @pos@ in the context @m@.
@@ -104,7 +105,7 @@
 --   deriving (HasReader "foo" Int) via
 --     Rename 1 (Pos 1 () (MonadReader (Reader (Int, Bool))))
 -- @
-newtype Pos (pos :: Nat) (oldtag :: k) m (a :: *) = Pos (m a)
+newtype Pos (pos :: Nat) (oldtag :: k) m (a :: Type) = Pos (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Choose the given constructor in the sum-type in context @m@.
@@ -122,7 +123,7 @@
 -- @'Capability.Error.MonadError' (ExceptT MyError Identity)@ to a
 -- @'Capability.Error.HasThrow' \"ErrB\" String@
 -- instance by wrapping thrown @String@s in the @ErrB@ constructor.
-newtype Ctor (ctor :: Symbol) (oldtag :: k) m (a :: *) = Ctor (m a)
+newtype Ctor (ctor :: Symbol) (oldtag :: k) m (a :: Type) = Ctor (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Skip one level in a monad transformer stack.
@@ -143,7 +144,7 @@
 -- the @'Capability.State.HasState' "\foo\" Bool@ instance of the underlying
 -- @'Capability.State.MonadState' (State Bool)@ over the
 -- @StateT Int@ monad transformer.
-newtype Lift m (a :: *) = Lift (m a)
+newtype Lift m (a :: Type) = Lift (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 
@@ -152,10 +153,10 @@
 -- This is not necessary in deriving via clauses, but in places where a
 -- transformer is expected as a type argument. E.g. 'HasError.wrapError'.
 newtype (:.:)
-  (t2 :: (* -> *) -> * -> *)
-  (t1 :: (* -> *) -> * -> *)
-  (m :: * -> *)
-  (a :: *)
+  (t2 :: (Type -> Type) -> Type -> Type)
+  (t1 :: (Type -> Type) -> Type -> Type)
+  (m :: Type -> Type)
+  (a :: Type)
   = (:.:) (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 infixr 9 :.:
diff --git a/src/Capability/Constraints.hs b/src/Capability/Constraints.hs
--- a/src/Capability/Constraints.hs
+++ b/src/Capability/Constraints.hs
@@ -16,12 +16,12 @@
   ) where
 
 import Data.Constraint (Dict(..))
-import Data.Kind (Constraint)
+import Data.Kind (Constraint, Type)
 
--- | A 'Capability' takes a type constructor @* -> *@ (e.g., a monad) and
+-- | A 'Capability' takes a type constructor @Type -> Type@ (e.g., a monad) and
 -- returns a 'Constraint'. Examples of capabilities includ: @HasReader "foo"
 -- Int@, @MonadIO@, …
-type Capability = (* -> *) -> Constraint
+type Capability = (Type -> Type) -> Constraint
 
 -- | Type family used used to express a conjunction of constraints over a single
 -- type.
diff --git a/src/Capability/Error.hs b/src/Capability/Error.hs
--- a/src/Capability/Error.hs
+++ b/src/Capability/Error.hs
@@ -39,6 +39,7 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -65,6 +66,8 @@
   , MonadUnliftIO(..)
     -- ** Modifiers
   , module Capability.Accessors
+    -- * Reflection
+  , Reified(..)
     -- * Re-exported
   , Exception(..)
   , Typeable
@@ -73,6 +76,7 @@
 import Capability.Accessors
 import Capability.Constraints
 import Capability.Derive (derive)
+import Capability.Reflection
 import Capability.TypeOf
 import Control.Exception (Exception(..))
 import qualified Control.Exception.Safe as Safe
@@ -87,6 +91,7 @@
 import Control.Monad.Trans.Control (MonadTransControl(..))
 import Data.Coerce (Coercible, coerce)
 import qualified Data.Generics.Sum.Constructors as Generic
+import Data.Kind (Type)
 import Data.Typeable (Typeable)
 import GHC.Exts (Proxy#, proxy#)
 import qualified UnliftIO.Exception as UnliftIO
@@ -96,7 +101,7 @@
 -- @HasThrow@/@HasCatch@ capabilities at different tags should be independent.
 -- See 'HasCatch'.
 class Monad m
-  => HasThrow (tag :: k) (e :: *) (m :: * -> *) | tag m -> e
+  => HasThrow (tag :: k) (e :: Type) (m :: Type -> Type) | tag m -> e
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasReader'.
@@ -106,7 +111,7 @@
 
 -- | Throw an exception in the specified exception capability.
 throw :: forall tag e m a. HasThrow tag e m => e -> m a
-throw = throw_ (proxy# @_ @tag)
+throw = throw_ (proxy# @tag)
 {-# INLINE throw #-}
 
 -- | Capability to catch exceptions of type @e@ under @tag@.
@@ -124,7 +129,7 @@
 --
 -- See 'wrapError' for a way to combine multiple exception types into one.
 class HasThrow tag e m
-  => HasCatch (tag :: k) (e :: *) (m :: * -> *) | tag m -> e
+  => HasCatch (tag :: k) (e :: Type) (m :: Type -> Type) | tag m -> e
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasReader'.
@@ -140,14 +145,14 @@
 -- | Provide a handler for exceptions thrown in the given action
 -- in the given exception capability.
 catch :: forall tag e m a. HasCatch tag e m => m a -> (e -> m a) -> m a
-catch = catch_ (proxy# @_ @tag)
+catch = catch_ (proxy# @tag)
 {-# INLINE catch #-}
 
 -- | Like 'catch', but only handle the exception if the provided function
 -- returns 'Just'.
 catchJust :: forall tag e m a b. HasCatch tag e m
   => (e -> Maybe b) -> m a -> (b -> m a) -> m a
-catchJust = catchJust_ (proxy# @_ @tag)
+catchJust = catchJust_ (proxy# @tag)
 {-# INLINE catchJust #-}
 
 -- | Wrap exceptions @inner@ originating from the given action according to
@@ -177,7 +182,7 @@
 --   What would the meaning of the tag be?
 
 -- | Derive 'HasError from @m@'s 'Control.Monad.Except.MonadError' instance.
-newtype MonadError m (a :: *) = MonadError (m a)
+newtype MonadError m (a :: Type) = MonadError (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance Except.MonadError e m => HasThrow tag e (MonadError m) where
@@ -200,7 +205,7 @@
   {-# INLINE catchJust_ #-}
 
 -- | Derive 'HasThrow' from @m@'s 'Control.Monad.Catch.MonadThrow' instance.
-newtype MonadThrow (e :: *) m (a :: *) = MonadThrow (m a)
+newtype MonadThrow (e :: Type) m (a :: Type) = MonadThrow (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance (Catch.Exception e, Catch.MonadThrow m)
@@ -211,7 +216,7 @@
     {-# INLINE throw_ #-}
 
 -- | Derive 'HasCatch from @m@'s 'Control.Monad.Catch.MonadCatch instance.
-newtype MonadCatch (e :: *) m (a :: *) = MonadCatch (m a)
+newtype MonadCatch (e :: Type) m (a :: Type) = MonadCatch (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
   deriving (HasThrow tag e) via MonadThrow e m
 
@@ -238,7 +243,7 @@
 
 -- | Derive 'HasError' using the functionality from the @safe-exceptions@
 -- package.
-newtype SafeExceptions (e :: *) m (a :: *) = SafeExceptions (m a)
+newtype SafeExceptions (e :: Type) m (a :: Type) = SafeExceptions (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance (Safe.Exception e, Safe.MonadThrow m)
@@ -269,7 +274,7 @@
     {-# INLINE catchJust_ #-}
 
 -- | Derive 'HasError' using the functionality from the @unliftio@ package.
-newtype MonadUnliftIO (e :: *) m (a :: *) = MonadUnliftIO (m a)
+newtype MonadUnliftIO (e :: Type) m (a :: Type) = MonadUnliftIO (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance (UnliftIO.Exception e, MonadIO m)
@@ -416,7 +421,7 @@
 
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasThrow tag e (t2 (t1 m)) )
@@ -424,7 +429,7 @@
 
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasCatch tag e (t2 (t1 m)) )
@@ -437,3 +442,46 @@
 -- | Type synonym using the 'TypeOf' type family to specify 'HasCatch'
 -- constraints without having to specify the type associated to a tag.
 type HasCatch' (tag :: k) = HasCatch tag (TypeOf k tag)
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasThrow tag e) m = ReifiedThrow {_throw :: forall a. e -> m a}
+
+data instance Reified tag (HasCatch tag e) m = ReifiedCatch
+  { _catchThrow :: Reified tag (HasThrow tag e) m,
+    _catch :: forall a. m a -> (e -> m a) -> m a,
+    _catchJust :: forall a b. (e -> Maybe b) -> m a -> (b -> m a) -> m a
+  }
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasThrow tag e) m)
+  ) =>
+  HasThrow tag e (Reflected s (HasThrow tag e) m)
+  where
+  throw_ :: forall a. Proxy# tag -> e -> Reflected s (HasThrow tag e) m a
+  throw_ _ = coerce @(e -> m a) $ _throw $ reified @s
+  {-# INLINE throw_ #-}
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasCatch tag e) m)
+  ) =>
+  HasThrow tag e (Reflected s (HasCatch tag e) m)
+  where
+  throw_ :: forall a. Proxy# tag -> e -> Reflected s (HasCatch tag e) m a
+  throw_ _ = coerce @(e -> m a) $ _throw $ _catchThrow $ reified @s
+  {-# INLINE throw_ #-}
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasCatch tag e) m)
+  ) =>
+  HasCatch tag e (Reflected s (HasCatch tag e) m)
+  where
+  catch_ :: forall a. Proxy# tag -> Reflected s (HasCatch tag e) m a -> (e -> Reflected s (HasCatch tag e) m a) -> Reflected s (HasCatch tag e) m a
+  catch_ _ = coerce @(m a -> (e -> m a) -> m a) $ _catch $ reified @s
+  {-# INLINE catch_ #-}
+  catchJust_ :: forall a b. Proxy# tag -> (e -> Maybe b) -> Reflected s (HasCatch tag e) m a -> (b -> Reflected s (HasCatch tag e) m a) -> Reflected s (HasCatch tag e) m a
+  catchJust_ _ = coerce @((e -> Maybe b) -> m a -> (b -> m a) -> m a) $ _catchJust $ reified @s
+  {-# INLINE catchJust_ #-}
diff --git a/src/Capability/Reader/Internal/Class.hs b/src/Capability/Reader/Internal/Class.hs
--- a/src/Capability/Reader/Internal/Class.hs
+++ b/src/Capability/Reader/Internal/Class.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -7,6 +10,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeInType #-}
 
@@ -19,12 +23,15 @@
   , local
   , reader
   , magnify
+  , Reified(..)
   ) where
 
 import Capability.Constraints
-import Capability.Source.Internal.Class
 import Capability.Derive (derive)
-import Data.Coerce (Coercible)
+import Capability.Reflection
+import Capability.Source.Internal.Class
+import Data.Coerce (Coercible, coerce)
+import Data.Kind (Type)
 import GHC.Exts (Proxy#, proxy#)
 
 -- | Reader capability
@@ -41,7 +48,7 @@
 -- prop> local @t f (m >>= \x -> k x) = local @t f m >>= \x -> local @t f (k x)
 -- prop> reader @t f = f <$> ask @t
 class (Monad m, HasSource tag r m)
-  => HasReader (tag :: k) (r :: *) (m :: * -> *) | tag m -> r
+  => HasReader (tag :: k) (r :: Type) (m :: Type -> Type) | tag m -> r
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasReader'.
@@ -74,7 +81,7 @@
 -- where @e@ is the environment of the reader capability @tag@.
 -- Symbolically: @return e = ask \@tag@.
 local :: forall tag r m a. HasReader tag r m => (r -> r) -> m a -> m a
-local = local_ (proxy# @_ @tag)
+local = local_ (proxy# @tag)
 {-# INLINE local #-}
 
 -- | @reader \@tag act@
@@ -83,7 +90,7 @@
 --
 -- It happens to coincide with @asks@: @reader = asks@.
 reader :: forall tag r m a. HasReader tag r m => (r -> a) -> m a
-reader = reader_ (proxy# @_ @tag)
+reader = reader_ (proxy# @tag)
 {-# INLINE reader #-}
 
 -- | Execute the given reader action on a sub-component of the current context
@@ -103,3 +110,33 @@
 magnify =
   derive @t @'[HasReader innertag inner] @cs
 {-# INLINE magnify #-}
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasReader tag r) m = ReifiedReader
+  { _readerSource :: Reified tag (HasSource tag r) m,
+    _local :: forall a. (r -> r) -> m a -> m a,
+    _reader :: forall a. (r -> a) -> m a
+  }
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasReader tag r) m)
+  ) =>
+  HasSource tag r (Reflected s (HasReader tag r) m)
+  where
+  await_ _ = coerce $ _await $ _readerSource $ reified @s
+  {-# INLINE await_ #-}
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasReader tag r) m)
+  ) =>
+  HasReader tag r (Reflected s (HasReader tag r) m)
+  where
+  local_ :: forall a. Proxy# tag -> (r -> r) -> Reflected s (HasReader tag r) m a -> Reflected s (HasReader tag r) m a
+  local_ _ = coerce @((r -> r) -> m a -> m a) $ _local (reified @s)
+  {-# INLINE local_ #-}
+  reader_ :: forall a. Proxy# tag -> (r -> a) -> Reflected s (HasReader tag r) m a
+  reader_ _ = coerce @((r -> a) -> m a) $ _reader (reified @s)
+  {-# INLINE reader_ #-}
diff --git a/src/Capability/Reader/Internal/Strategies.hs b/src/Capability/Reader/Internal/Strategies.hs
--- a/src/Capability/Reader/Internal/Strategies.hs
+++ b/src/Capability/Reader/Internal/Strategies.hs
@@ -40,6 +40,7 @@
 import Data.Coerce (Coercible, coerce)
 import qualified Data.Generics.Product.Fields as Generic
 import qualified Data.Generics.Product.Positions as Generic
+import Data.Kind (Type)
 import GHC.Exts (Proxy#)
 
 instance Reader.MonadReader r m => HasReader tag r (MonadReader m) where
@@ -167,7 +168,7 @@
     {-# INLINE reader_ #-}
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasReader tag r (t2 (t1 m)) )
diff --git a/src/Capability/Reflection.hs b/src/Capability/Reflection.hs
new file mode 100644
--- /dev/null
+++ b/src/Capability/Reflection.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Use this module to provide an ad-hoc interpreter for a capability using
+-- type class reflection.
+--
+-- Use the functions 'interpret_' or 'interpret' for ad-hoc interpretation of
+-- capabilities.
+--
+-- Refer to 'Reflected' if you would like to enable reflection for a new
+-- capability.
+--
+-- More complex examples using this module can be found in the
+-- [Reflection example
+-- module](https://github.com/tweag/capability/blob/master/examples/Reflection.hs).
+--
+-- For details on reflection refer to the tutorial at
+-- <https://www.tweag.io/posts/2017-12-21-reflection-tutorial.html> and the
+-- @reflection@ library at <https://hackage.haskell.org/package/reflection>.
+
+module Capability.Reflection
+  ( -- * Reflection
+    interpret_
+  , interpret
+  , Reified
+  , Reflected (..)
+  , reified
+    -- * Re-exported
+  , Reifies
+  , reify
+  , reflect
+  , Proxy (..)
+  ) where
+
+import Capability.Constraints
+import Capability.Derive
+import Data.Kind (Type)
+import Data.Proxy
+import Data.Reflection
+
+-- | @interpret_ \@tag dict action@
+--
+-- Execute @action@ using the ad-hoc interpretation of a capability @c@ under
+-- @tag@ defined by @dict@, where @dict@ is a value of type @'Reified' tag c@,
+-- i.e. a record providing the implementation of the methods of capability @c@.
+--
+-- For example, the following provides an ad-hoc interpretation for the
+-- 'Capability.Source.HasSource' capability.
+--
+-- >>> :{
+--   interpret_ @"my-source"
+--     ReifiedSource { _await = pure "capabilities" }
+--     (replicateM 3 (await @"my-source"))
+--   :}
+-- ["capabilities", "capabilities", "capabilities"]
+interpret_ ::
+  forall tag c m a.
+  ( Monad m,
+    forall s. Reifies s (Reified tag c m) => c (Reflected s c m)
+  ) =>
+  Reified tag c m ->
+  (forall m'. c m' => m' a) ->
+  m a
+interpret_ = interpret @tag @'[] @c
+{-# INLINE interpret_ #-}
+
+-- | @interpret \@tag \@ambient dict action@
+--
+-- Like 'interpret_' but forwards the ambient capabilities @ambient@ into the
+-- context of @action@ as well.
+--
+-- For example, the following provides an ad-hoc interpretation for the
+-- 'Capability.Source.HasSource' capability, while using an ambient
+-- 'Capability.Sink.HasSink' capability.
+--
+-- >>> :{
+--   interpret @"my-source" @'[HasSink "my-sink" String]
+--     ReifiedSource { _await = pure "capabilities" }
+--     (replicateM_ 3 (await @"my-source" >>= yield @"my-sink"))
+--   :}
+interpret ::
+  forall tag (cs :: [Capability]) c m a.
+  ( Monad m,
+    All cs m,
+    forall s. Reifies s (Reified tag c m) => c (Reflected s c m)
+  ) =>
+  Reified tag c m ->
+  (forall m'. All (c ': cs) m' => m' a) ->
+  m a
+interpret dict action =
+  reify dict $ \(_ :: Proxy s) ->
+    derive @(Reflected s c) @'[c] @cs action
+{-# INLINE interpret #-}
+
+-- | @Reified tag capability m@
+--
+-- Defines the dictionary type for the methods of @capability@ under @tag@ in
+-- the monad @m@. Refer to 'interpret_' for an example use-case.
+--
+-- For example, the 'Capability.Sink.HasSink' capability has the method
+-- @'Capability.Sink.yield' :: a -> m ()@. The corresponding dictionary type is
+-- defined as follows.
+--
+-- >>> :{
+--   data instance Reified tag (HasSink tag a) m =
+--     ReifiedSink { _yield :: forall a. a -> m () }
+--   :}
+--
+-- Superclass dictionaries are represented as nested records. For example, the
+-- 'Capability.State.HasState' capability has the superclasses
+-- 'Capability.Source.HasSource' and 'Capability.Sink.HasSink' and the method
+-- @'Capability.State.state' :: (s -> (a, s)) -> m a@. The corresponding
+-- dictionary type is defined as follows.
+--
+-- >>> :{
+--   data instance Reified tag (HasState tag s) m =
+--     ReifiedState
+--       { _stateSource :: Reified tag (HasSource tag s) m,
+--         _stateSink :: Reified tag (HasSink tag s) m,
+--         _state :: forall a. (s -> (a, s)) -> m a
+--       }
+--   :}
+data family Reified (tag :: k) (c :: Capability) (m :: Type -> Type)
+
+-- | @Reflected s capability m@
+--
+-- Carries the type class instance for @capability@ in the monad @m@ defined by
+-- the dictionary reflected in @s@ in the type system.
+--
+-- For most use-cases it is not necessary to use this type directly. Use
+-- 'interpret_' or 'interpret' instead.
+--
+-- If you wish to enable reflection for a new capability, then you will need to
+-- define a type class instance for @Reflected@ for the new capability. Note,
+-- you will also need to define an instance of 'Reified' which defines the
+-- dictionary type of the new capability. Hint, you can use @'reified' \@s@ to
+-- obtain the dictionary from the context in the instance implementation.
+--
+-- For example, the @Reflected@ instance for the 'Capability.Sink.HasSink'
+-- capability can be defined as follows. Assuming the dictionary described in
+-- 'Reified'.
+--
+-- >>> :{
+--   instance
+--     (Monad m, Reifies s (Reified tag (HasSink tag a) m)) =>
+--     HasSink tag a (Reflected s (HasSink tag a) m)
+--     where
+--     yield a = Reflect $ _yield (reified @s) a
+--   :}
+newtype Reflected (s :: Type) (c :: Capability) (m :: Type -> Type) (a :: Type) = Reflect (m a)
+  deriving (Functor, Applicative, Monad)
+
+-- | @reified \@s@
+--
+-- Obtain the dictionary that is reflected in the type system under @s@.
+--
+-- This is a convenience wrapper around 'Data.Reflection.reflect'.
+reified :: forall s tag c m. Reifies s (Reified tag c m) => Reified tag c m
+reified = reflect (Proxy @s)
+{-# INLINE reified #-}
diff --git a/src/Capability/Sink/Internal/Class.hs b/src/Capability/Sink/Internal/Class.hs
--- a/src/Capability/Sink/Internal/Class.hs
+++ b/src/Capability/Sink/Internal/Class.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnboxedTuples #-}
@@ -21,6 +22,9 @@
 
 module Capability.Sink.Internal.Class where
 
+import Capability.Reflection
+import Data.Coerce (coerce)
+import Data.Kind (Type)
 import GHC.Exts (Proxy#, proxy#)
 
 -- | Sinking capability.
@@ -28,7 +32,7 @@
 -- An instance does not need to fulfill any additional laws
 -- besides the monad laws.
 class Monad m
-  => HasSink (tag :: k) (a :: *) (m :: * -> *) | tag m -> a
+  => HasSink (tag :: k) (a :: Type) (m :: Type -> Type) | tag m -> a
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasSink'.
@@ -39,5 +43,18 @@
 -- | @yield \@tag a@
 -- emits @a@ in the sink capability @tag@.
 yield :: forall tag a m. HasSink tag a m => a -> m ()
-yield = yield_ (proxy# @_ @tag)
+yield = yield_ (proxy# @tag)
 {-# INLINE yield #-}
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasSink tag a) m = ReifiedSink {_yield :: a -> m ()}
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasSink tag a) m)
+  ) =>
+  HasSink tag a (Reflected s (HasSink tag a) m)
+  where
+  yield_ _ = coerce $ _yield (reified @s)
+  {-# INLINE yield_ #-}
diff --git a/src/Capability/Sink/Internal/Strategies.hs b/src/Capability/Sink/Internal/Strategies.hs
--- a/src/Capability/Sink/Internal/Strategies.hs
+++ b/src/Capability/Sink/Internal/Strategies.hs
@@ -34,29 +34,27 @@
 import Capability.State.Internal.Class
 import Capability.State.Internal.Strategies.Common
 import Control.Lens (set)
-import Control.Monad.IO.Class (MonadIO)
-import Control.Monad.Primitive (PrimMonad)
 import qualified Control.Monad.State.Class as State
-import Control.Monad.Trans.Class (MonadTrans, lift)
 import Data.Coerce (Coercible, coerce)
 import Data.DList (DList)
 import qualified Data.DList as DList
 import qualified Data.Generics.Product.Fields as Generic
 import qualified Data.Generics.Product.Positions as Generic
 import Data.IORef
+import Data.Kind (Type)
 import Data.Mutable
 import Streaming
 import qualified Streaming.Prelude as S
 
 -- | Accumulate sunk values in a reverse order list.
-newtype SinkStack m (a :: *) = SinkStack (m a)
+newtype SinkStack m (a :: Type) = SinkStack (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 instance HasState tag [a] m => HasSink tag a (SinkStack m) where
   yield_ _ a = coerce @(m ()) $ modify' @tag (a:)
   {-# INLINE yield_ #-}
 
 -- | Accumulate sunk values in forward order in a difference list.
-newtype SinkDList m (a :: *) = SinkDList (m a)
+newtype SinkDList m (a :: Type) = SinkDList (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 -- | This instance may seem a bit odd at first. All it does is wrap each
 -- 'yield'ed value in a single element difference list. How does re-yielding
@@ -75,7 +73,7 @@
   {-# INLINE yield_ #-}
 
 -- | Accumulate sunk values with their own monoid.
-newtype SinkLog m (a :: *) = SinkLog (m a)
+newtype SinkLog m (a :: Type) = SinkLog (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 instance (Monoid w, HasState tag w m) => HasSink tag w (SinkLog m) where
     yield_ _ w = coerce @(m ()) $ modify' @tag (<> w)
@@ -105,7 +103,7 @@
     {-# INLINE yield_ #-}
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasSink tag a (t2 (t1 m)) )
diff --git a/src/Capability/Source/Internal/Class.hs b/src/Capability/Source/Internal/Class.hs
--- a/src/Capability/Source/Internal/Class.hs
+++ b/src/Capability/Source/Internal/Class.hs
@@ -27,6 +27,7 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -35,6 +36,9 @@
 
 module Capability.Source.Internal.Class where
 
+import Capability.Reflection
+import Data.Coerce (coerce)
+import Data.Kind (Type)
 import GHC.Exts (Proxy#, proxy#)
 
 -- | Sourcing capability.
@@ -42,7 +46,7 @@
 -- An instance does not need to fulfill any additional laws
 -- besides the monad laws.
 class Monad m
-  => HasSource (tag :: k) (a :: *) (m :: * -> *) | tag m -> a
+  => HasSource (tag :: k) (a :: Type) (m :: Type -> Type) | tag m -> a
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasSource'.
@@ -53,7 +57,7 @@
 -- | @await \@tag a@
 -- takes @a@ from the source capability @tag@.
 await :: forall tag a m. HasSource tag a m => m a
-await = await_ (proxy# @_ @tag)
+await = await_ (proxy# @tag)
 {-# INLINE await #-}
 
 -- | @awaits \@tag@
@@ -64,3 +68,16 @@
 awaits :: forall tag r m a. HasSource tag r m => (r -> a) -> m a
 awaits f = f <$> await @tag
 {-# INLINE awaits #-}
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasSource tag a) m = ReifiedSource {_await :: m a}
+
+instance
+  ( Monad m,
+    Reifies s (Reified tag (HasSource tag a) m)
+  ) =>
+  HasSource tag a (Reflected s (HasSource tag a) m)
+  where
+  await_ _ = coerce $ _await (reified @s)
+  {-# INLINE await_ #-}
diff --git a/src/Capability/Source/Internal/Strategies.hs b/src/Capability/Source/Internal/Strategies.hs
--- a/src/Capability/Source/Internal/Strategies.hs
+++ b/src/Capability/Source/Internal/Strategies.hs
@@ -38,12 +38,12 @@
 import Control.Lens (view)
 import Control.Monad.Catch (MonadMask)
 import Control.Monad.IO.Class (MonadIO, liftIO)
-import Control.Monad.Primitive (PrimMonad)
 import qualified Control.Monad.Reader.Class as Reader
 import qualified Control.Monad.State.Class as State
 import Control.Monad.Trans.Class (MonadTrans, lift)
 import Data.Coerce (Coercible, coerce)
 import Data.IORef
+import Data.Kind (Type)
 import Data.Mutable
 import qualified Data.Generics.Product.Fields as Generic
 import qualified Data.Generics.Product.Positions as Generic
@@ -52,7 +52,7 @@
 
 -- | Derive 'HasSource' from @m@'s 'Control.Monad.Reader.Class.MonadReader'
 -- instance.
-newtype MonadReader (m :: * -> *) (a :: *) = MonadReader (m a)
+newtype MonadReader (m :: Type -> Type) (a :: Type) = MonadReader (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance Reader.MonadReader r m => HasSource tag r (MonadReader m) where
@@ -74,7 +74,7 @@
 -- exceptions.
 --
 -- See 'ReadState'.
-newtype ReadStatePure (m :: * -> *) (a :: *) = ReadStatePure (m a)
+newtype ReadStatePure (m :: Type -> Type) (a :: Type) = ReadStatePure (m a)
   deriving (Functor, Applicative, Monad)
 
 instance HasState tag r m => HasSource tag r (ReadStatePure m) where
@@ -86,7 +86,7 @@
 -- Use this if the monad stack allows catching exceptions.
 --
 -- See 'ReadStatePure'.
-newtype ReadState (m :: * -> *) (a :: *) = ReadState (m a)
+newtype ReadState (m :: Type -> Type) (a :: Type) = ReadState (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 instance
@@ -104,7 +104,7 @@
       awaits @oldtag $ view (Generic.position' @pos)
     {-# INLINE await_ #-}
 
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasSource tag r (t2 (t1 m)) )
diff --git a/src/Capability/State/Internal/Class.hs b/src/Capability/State/Internal/Class.hs
--- a/src/Capability/State/Internal/Class.hs
+++ b/src/Capability/State/Internal/Class.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -22,13 +25,16 @@
   , modify'
   , gets
   , zoom
+  , Reified (..)
   ) where
 
 import Capability.Constraints
 import Capability.Derive (derive)
+import Capability.Reflection
 import Capability.Source.Internal.Class
 import Capability.Sink.Internal.Class
-import Data.Coerce (Coercible)
+import Data.Coerce (Coercible, coerce)
+import Data.Kind (Type)
 import GHC.Exts (Proxy#, proxy#)
 
 -- | State capability
@@ -43,7 +49,7 @@
 -- prop> put @t s >> get @t = put @t s >> pure s
 -- prop> state @t f = get @t >>= \s -> let (a, s') = f s in put @t s' >> pure a
 class (Monad m, HasSource tag s m, HasSink tag s m)
-  => HasState (tag :: k) (s :: *) (m :: * -> *) | tag m -> s
+  => HasState (tag :: k) (s :: Type) (m :: Type -> Type) | tag m -> s
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasState.
@@ -70,7 +76,7 @@
 -- Given the current state @s@ of the state capability @tag@
 -- and @(a, s') = f s@, update the state to @s'@ and return @a@.
 state :: forall tag s m a. HasState tag s m => (s -> (a, s)) -> m a
-state = state_ (proxy# @_ @tag)
+state = state_ (proxy# @tag)
 {-# INLINE state #-}
 
 -- | @modify \@tag f@
@@ -129,3 +135,39 @@
 zoom =
   derive @t @'[HasState innertag inner] @cs
 {-# INLINE zoom #-}
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasState tag s) m = ReifiedState
+  { _stateSource :: Reified tag (HasSource tag s) m,
+    _stateSink :: Reified tag (HasSink tag s) m,
+    _state :: forall a. (s -> (a, s)) -> m a
+  }
+
+instance
+  ( Monad m,
+    Reifies s' (Reified tag (HasState tag s) m)
+  ) =>
+  HasSource tag s (Reflected s' (HasState tag s) m)
+  where
+  await_ _ = coerce $ _await $ _stateSource $ reified @s'
+  {-# INLINE await_ #-}
+
+instance
+  ( Monad m,
+    Reifies s' (Reified tag (HasState tag s) m)
+  ) =>
+  HasSink tag s (Reflected s' (HasState tag s) m)
+  where
+  yield_ _ = coerce $ _yield $ _stateSink $ reified @s'
+  {-# INLINE yield_ #-}
+
+instance
+  ( Monad m,
+    Reifies s' (Reified tag (HasState tag s) m)
+  ) =>
+  HasState tag s (Reflected s' (HasState tag s) m)
+  where
+  state_ :: forall a. Proxy# tag -> (s -> (a, s)) -> Reflected s' (HasState tag s) m a
+  state_ _ = coerce @((s -> (a, s)) -> m a) $ _state (reified @s')
+  {-# INLINE state_ #-}
diff --git a/src/Capability/State/Internal/Strategies.hs b/src/Capability/State/Internal/Strategies.hs
--- a/src/Capability/State/Internal/Strategies.hs
+++ b/src/Capability/State/Internal/Strategies.hs
@@ -34,13 +34,13 @@
 import Capability.Source.Internal.Strategies ()
 import Capability.Sink.Internal.Strategies ()
 import Control.Monad.IO.Class (MonadIO, liftIO)
-import Control.Monad.Primitive (PrimMonad)
 import qualified Control.Monad.State.Class as State
 import Control.Monad.Trans.Class (MonadTrans, lift)
 import Data.Coerce (Coercible, coerce)
 import qualified Data.Generics.Product.Fields as Generic
 import qualified Data.Generics.Product.Positions as Generic
 import Data.IORef
+import Data.Kind (Type)
 import Data.Mutable
 import GHC.Exts (Proxy#)
 
@@ -106,7 +106,7 @@
     {-# INLINE state_ #-}
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasState tag s (t2 (t1 m)) )
diff --git a/src/Capability/State/Internal/Strategies/Common.hs b/src/Capability/State/Internal/Strategies/Common.hs
--- a/src/Capability/State/Internal/Strategies/Common.hs
+++ b/src/Capability/State/Internal/Strategies/Common.hs
@@ -31,10 +31,11 @@
 
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Primitive (PrimMonad)
+import Data.Kind (Type)
 
 -- | Derive 'HasState' from @m@'s
 -- 'Control.Monad.State.Class.MonadState' instance.
-newtype MonadState (m :: * -> *) (a :: *) = MonadState (m a)
+newtype MonadState (m :: Type -> Type) (a :: Type) = MonadState (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
 
 -- | Derive a state monad from a reader over an 'Data.IORef.IORef'.
@@ -66,5 +67,5 @@
 -- >   => HasState "foo" Int (MyState m)
 --
 -- See 'ReaderIORef' for a specialized version over 'Data.IORef.IORef'.
-newtype ReaderRef m (a :: *) = ReaderRef (m a)
+newtype ReaderRef m (a :: Type) = ReaderRef (m a)
   deriving (Functor, Applicative, Monad, MonadIO, PrimMonad)
diff --git a/src/Capability/TypeOf.hs b/src/Capability/TypeOf.hs
--- a/src/Capability/TypeOf.hs
+++ b/src/Capability/TypeOf.hs
@@ -4,12 +4,14 @@
 
 module Capability.TypeOf where
 
+import Data.Kind (Type)
+
 -- | Type family associating a tag to the corresponding type. It is intended to
 -- simplify constraint declarations, by removing the need to redundantly specify
 -- the type associated to a tag.
 --
 -- It is poly-kinded, which allows users to define their own kind of tags.
--- Standard haskell types can also be used as tags by specifying the '*' kind
+-- Standard haskell types can also be used as tags by specifying the 'Type' kind
 -- when defining the type family instance.
 --
 -- Defining 'TypeOf' instances for 'GHC.TypeLits.Symbol's (typelevel string
@@ -26,11 +28,11 @@
 --
 --     data Foo
 --     data Bar
---     type instance TypeOf * Foo = Int
---     type instance TypeOf * Bar = String
+--     type instance TypeOf Type Foo = Int
+--     type instance TypeOf Type Bar = String
 --
 --     -- Same as: foo :: HasReader Foo Int M => …
 --     foo :: HasReader' Foo m => …
 --     foo = …
 -- @
-type family TypeOf k (s :: k) :: *
+type family TypeOf k (s :: k) :: Type
diff --git a/src/Capability/Writer.hs b/src/Capability/Writer.hs
--- a/src/Capability/Writer.hs
+++ b/src/Capability/Writer.hs
@@ -33,6 +33,7 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -55,14 +56,18 @@
   , SinkLog (..)
     -- ** Modifiers
   , module Capability.Accessors
+    -- * Reflection
+  , Reified (..)
   ) where
 
 import Capability.Accessors
+import Capability.Reflection
 import Capability.Sink
 import Capability.State
 -- import deprecated module to reexport deprecated item for back-compat.
 import Capability.Stream
 import Data.Coerce (Coercible, coerce)
+import Data.Kind (Type)
 import GHC.Exts (Proxy#, proxy#)
 
 -- | Writer capability
@@ -92,7 +97,7 @@
 -- regardless of whatever additional methods it provides and laws by which it
 -- abides.
 class (Monoid w, Monad m, HasSink tag w m)
-  => HasWriter (tag :: k) (w :: *) (m :: * -> *) | tag m -> w
+  => HasWriter (tag :: k) (w :: Type) (m :: Type -> Type) | tag m -> w
   where
     -- | For technical reasons, this method needs an extra proxy argument.
     -- You only need it if you are defining new instances of 'HasReader'.
@@ -117,13 +122,13 @@
 -- Appends @w@ to the output of the writer capability @tag@
 -- and returns the value @a@.
 writer :: forall tag w m a. HasWriter tag w m => (a, w) -> m a
-writer = writer @tag
+writer = writer_ (proxy# @tag)
 {-# INLINE writer #-}
 
 -- | @tell \@tag w@
 -- appends @w@ to the output of the writer capability @tag@.
 tell :: forall tag w m. HasWriter tag w m => w -> m ()
-tell = yield_ (proxy# @_ @tag)
+tell = yield_ (proxy# @tag)
 {-# INLINE tell #-}
 
 -- | @listen \@tag m@
@@ -131,7 +136,7 @@
 -- in the writer capability @tag@ along with result of @m@.
 -- Appends the output of @m@ to the output of the writer capability @tag@.
 listen :: forall tag w m a. HasWriter tag w m => m a -> m (a, w)
-listen = listen_ (proxy# @_ @tag)
+listen = listen_ (proxy# @tag)
 {-# INLINE listen #-}
 
 -- | @pass \@tag m@
@@ -139,11 +144,11 @@
 -- @w@ to the output of the writer capability @tag@.
 -- @pass \@tag m@ instead appends @w' = f w@ to the output and returns @a@.
 pass :: forall tag w m a. HasWriter tag w m => m (a, w -> w) -> m a
-pass = pass_ (proxy# @_ @tag)
+pass = pass_ (proxy# @tag)
 {-# INLINE pass #-}
 
 -- | Compose two accessors.
-deriving via ((t2 :: (* -> *) -> * -> *) ((t1 :: (* -> *) -> * -> *) m))
+deriving via ((t2 :: (Type -> Type) -> Type -> Type) ((t1 :: (Type -> Type) -> Type -> Type) m))
   instance
   ( forall x. Coercible (m x) (t2 (t1 m) x)
   , Monad m, HasWriter tag w (t2 (t1 m)) )
@@ -178,3 +183,39 @@
 -- | Type synonym using the 'TypeOf' type family to specify 'HasWriter'
 -- constraints without having to specify the type associated to a tag.
 type HasWriter' (tag :: k) = HasWriter tag (TypeOf k tag)
+
+--------------------------------------------------------------------------------
+
+data instance Reified tag (HasWriter tag w) m = ReifiedWriter
+  { _writerSink :: Reified tag (HasSink tag w) m,
+    _writer :: forall a. (a, w) -> m a,
+    _listen :: forall a. m a -> m (a, w),
+    _pass :: forall a. m (a, w -> w) -> m a
+  }
+
+instance
+  ( Monoid w,
+    Monad m,
+    Reifies s (Reified tag (HasWriter tag w) m)
+  ) =>
+  HasSink tag w (Reflected s (HasWriter tag w) m)
+  where
+  yield_ _ = coerce $ _yield $ _writerSink $ reified @s
+  {-# INLINE yield_ #-}
+
+instance
+  ( Monad m,
+    Monoid w,
+    Reifies s (Reified tag (HasWriter tag w) m)
+  ) =>
+  HasWriter tag w (Reflected s (HasWriter tag w) m)
+  where
+  writer_ :: forall a. Proxy# tag -> (a, w) -> Reflected s (HasWriter tag w) m a
+  writer_ _ = coerce @((a, w) -> m a) $ _writer (reified @s)
+  {-# INLINE writer_ #-}
+  listen_ :: forall a. Proxy# tag -> Reflected s (HasWriter tag w) m a -> Reflected s (HasWriter tag w) m (a, w)
+  listen_ _ = coerce @(m a -> m (a, w)) $ _listen (reified @s)
+  {-# INLINE listen_ #-}
+  pass_ :: forall a. Proxy# tag -> Reflected s (HasWriter tag w) m (a, w -> w) -> Reflected s (HasWriter tag w) m a
+  pass_ _ = coerce @(m (a, w -> w) -> m a) $ _pass (reified @s)
+  {-# INLINE pass_ #-}