diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,19 @@
+## 0.2.1.0
+
+* Add `handleImpl`, `HandleD` and `handleMapHandle`
+
+* Add type role for `Exception`. This is technically a breaking change
+  but it seems extremely unlikely to break working code, so we are not
+  imposing a major version bump.
+
+* Internal details of proof terms
+
+  * Add proof terms for `:>~ instances.
+
+  * Use `ZW` as the argument instead of `(# #)`.
+
+  * Add `unsafeAxiom`
+
 ## 0.2.0.0
 
 * Choose different incoherent instance for `:>` for better type
diff --git a/bluefin-internal.cabal b/bluefin-internal.cabal
--- a/bluefin-internal.cabal
+++ b/bluefin-internal.cabal
@@ -1,6 +1,6 @@
 cabal-version:      3.0
 name:               bluefin-internal
-version:            0.2.0.0
+version:            0.2.1.0
 license:            MIT
 license-file:       LICENSE
 author:             Tom Ellis
diff --git a/src/Bluefin/Internal.hs b/src/Bluefin/Internal.hs
--- a/src/Bluefin/Internal.hs
+++ b/src/Bluefin/Internal.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UnboxedTuples #-}
@@ -264,7 +265,7 @@
 weakenEff _ = unsafeCoerceEff
 
 insertFirst :: Eff b r -> Eff (c1 :& b) r
-insertFirst = weakenEff (drop (eq (# #)))
+insertFirst = weakenEff (drop (eq ZW))
 
 insertSecond :: Eff (c1 :& b) r -> Eff (c1 :& (c2 :& b)) r
 insertSecond = insertManySecond
@@ -273,13 +274,13 @@
 insertManySecond = weakenEff (bimap has has)
 
 assoc1Eff :: Eff ((a :& b) :& c) r -> Eff (a :& (b :& c)) r
-assoc1Eff = weakenEff (assoc1 (# #))
+assoc1Eff = weakenEff (assoc1 ZW)
 
 pushFirst :: Eff a r -> Eff (a :& b) r
-pushFirst = weakenEff (fstI (# #))
+pushFirst = weakenEff (fstI ZW)
 
 mergeEff :: Eff (a :& a) r -> Eff a r
-mergeEff = weakenEff (merge (# #))
+mergeEff = weakenEff (merge ZW)
 
 inContext :: (e2 :> e1) => Eff (e1 :& e2) r -> Eff e1 r
 inContext = weakenEff (subsume1 has)
@@ -327,6 +328,8 @@
 newtype Exception exn (e :: Effects)
   = MkException (forall a. exn -> Eff e a)
 
+type role Exception representational nominal
+
 -- | A handle to a strict mutable state of type @s@
 newtype State s (e :: Effects) = UnsafeMkState (IORef s)
 
@@ -367,60 +370,112 @@
 --
 -- @
 -- instance Handle Application where
---   mapHandle
---     MkApplication
---       { queryDatabase = q,
---         applicationState = a,
---         logger = l
---       } =
---       MkApplication
---         { queryDatabase = \\s i -> useImplUnder (q s i),
---           applicationState = mapHandle a,
---           logger = mapHandle l
---         }
+--   'handleImpl' =
+--     'handleMapHandle' $
+--       \\MkApplication
+--          { queryDatabase = q,
+--            applicationState = a,
+--            logger = l
+--          } ->
+--           MkApplication
+--             { queryDatabase = \\s i -> 'useImplUnder' (q s i),
+--               applicationState = 'mapHandle' a,
+--               logger = mapHandle l
+--             }
 -- @
 class Handle (h :: Effects -> Type) where
+  {-# MINIMAL handleImpl | mapHandle #-}
+  -- | Define @handleImpl@ using 'handleMapHandle'.
+  handleImpl :: HandleD h
+  handleImpl = MkHandleD mapHandle
+
   -- | Used to create compound effects, i.e. handles that contain
   -- other handles.
+  --
+  -- You should not define this method in your type classes. Instead
+  -- define @handleImpl@.  In a future version of Bluefin, @mapHandle@
+  -- will no longer be a method.  If you previously had a definition
+  -- of @mapHandle@, for example like this:
+  --
+  -- @
+  -- instance Handle MyHandle where
+  --   mapHandle h = \<definition\>
+  -- @
+  --
+  -- you should change it to
+  --
+  -- @
+  -- instance Handle MyHandle where
+  --   handleImpl = handleMapHandle $ \\h -> \<definition\>
+  -- @
   mapHandle :: (e :> es) => h e -> h es
+  mapHandle = case handleImpl of MkHandleD f -> f
 
+-- | The type of the 'handleImpl' method of the 'Handle' class.
+-- Create a @HandleD@ using 'handleMapHandle'.
+newtype HandleD h = MkHandleD (forall e es. (e :> es) => h e -> h es)
+
+-- | For defining the 'handleImpl' method of the 'Handle' class.
+handleMapHandle ::
+  (forall e es. (e :> es) => h e -> h es) ->
+  -- | ͘
+  HandleD h
+handleMapHandle = MkHandleD
+
 instance Handle (State s) where
-  mapHandle (UnsafeMkState s) = UnsafeMkState s
+  handleImpl = handleMapHandle $ \(UnsafeMkState s) -> UnsafeMkState s
 
 instance Handle (Exception s) where
-  mapHandle (MkException s) = MkException (weakenEff has . s)
+  handleImpl = handleMapHandle $ \(MkException s) ->
+    MkException (weakenEff has . s)
 
 instance Handle (Coroutine a b) where
-  mapHandle (MkCoroutine f) = MkCoroutine (fmap useImpl f)
+  handleImpl = handleMapHandle $ \(MkCoroutine f) ->
+    MkCoroutine (fmap useImpl f)
 
 instance Handle (Writer w) where
-  mapHandle (Writer wr) = Writer (mapHandle wr)
+  handleImpl = handleMapHandle $ \(Writer wr) -> Writer (mapHandle wr)
 
 instance Handle IOE where
-  mapHandle MkIOE = MkIOE
+  handleImpl = handleMapHandle $ \MkIOE -> MkIOE
 
+-- | A convenience type whose only purpose is to avoid writing @(# #)@
+-- as an argument to functions which are only function because
+-- top-level definitions of unlifted kind are forbidden.
+newtype ZW = MkZW (# #)
+
+pattern ZW :: ZW
+pattern ZW <- MkZW (# #)
+  where
+    ZW = MkZW (# #)
+
+{-# COMPLETE ZW #-}
+
 newtype In (a :: Effects) (b :: Effects) = In# (# #)
 
-merge :: (# #) -> (a :& a) `In` a
-merge (# #) = In# (# #)
+unsafeInAxiom :: ZW -> e1 `In` e2
+unsafeInAxiom ZW = In# (# #)
 
-eq :: (# #) -> a `In` a
-eq (# #) = In# (# #)
+merge :: ZW -> (a :& a) `In` a
+merge ZW = In# (# #)
 
-fstI :: (# #) -> a `In` (a :& b)
-fstI (# #) = In# (# #)
+eq :: ZW -> a `In` a
+eq ZW = unsafeInAxiom ZW
 
-sndI :: (# #) -> a `In` (b :& a)
-sndI (# #) = In# (# #)
+fstI :: ZW -> a `In` (a :& b)
+fstI ZW = unsafeInAxiom ZW
 
+sndI :: ZW -> a `In` (b :& a)
+sndI ZW = unsafeInAxiom ZW
+
 cmp :: a `In` b -> b `In` c -> a `In` c
-cmp (In# (# #)) (In# (# #)) = In# (# #)
+cmp (In# (# #)) (In# (# #)) = unsafeInAxiom ZW
 
 bimap :: a `In` b -> c `In` d -> (a :& c) `In` (b :& d)
-bimap (In# (# #)) (In# (# #)) = In# (# #)
+bimap (In# (# #)) (In# (# #)) = unsafeInAxiom ZW
 
-assoc1 :: (# #) -> ((a :& b) :& c) `In` (a :& (b :& c))
-assoc1 (# #) = In# (# #)
+assoc1 :: ZW -> ((a :& b) :& c) `In` (a :& (b :& c))
+assoc1 ZW = unsafeInAxiom ZW
 
 drop :: a `In` b -> a `In` (c :& b)
 drop h = w2 (b h)
@@ -429,22 +484,22 @@
 here h = w (b2 h)
 
 w :: (a :& b) `In` c -> (a `In` c)
-w = cmp (fstI (# #))
+w = cmp (fstI ZW)
 
 w2 :: (b :& a) `In` c -> (a `In` c)
-w2 = cmp (sndI (# #))
+w2 = cmp (sndI ZW)
 
 b2 :: (a `In` b) -> ((a :& c) `In` (b :& c))
-b2 h = bimap h (eq (# #))
+b2 h = bimap h (eq ZW)
 
 b :: (a `In` b) -> (c :& a) `In` (c :& b)
-b = bimap (eq (# #))
+b = bimap (eq ZW)
 
 subsume1 :: (e2 `In` e1) -> (e1 :& e2) `In` e1
-subsume1 i = cmp (bimap (eq (# #)) i) (merge (# #))
+subsume1 i = cmp (bimap (eq ZW) i) (merge ZW)
 
 subsume2 :: (e1 `In` e2) -> (e1 :& e2) `In` e2
-subsume2 i = cmp (bimap i (eq (# #))) (merge (# #))
+subsume2 i = cmp (bimap i (eq ZW)) (merge ZW)
 
 -- | Effect subset constraint
 class (es1 :: Effects) :> (es2 :: Effects)
@@ -452,10 +507,16 @@
 -- | A set of effects @e@ is a subset of itself
 instance e :> e
 
+instanceProof1 :: ZW -> e `In` e
+instanceProof1 ZW = eq ZW
+
 -- | If @e@ is subset of @es@ then @e@ is a subset of a larger set, @x
 -- :& es@
 instance {-# INCOHERENT #-} (e :> es) => e :> (x :& es)
 
+instanceProof2 :: e `In` es -> e `In` (x :& es)
+instanceProof2 = drop
+
 -- Do we want this?
 -- instance {-# incoherent #-} (e :> es) => (e' :& e) :> (e' :> es)
 
@@ -464,13 +525,19 @@
 -- | @e@ is a subset of a larger set @e :& es@
 instance e :> (e :& es)
 
+instanceProof3 :: ZW -> e `In` (e :& es)
+instanceProof3 ZW = fstI ZW
+
 subset ::
   forall e1 es m.
   (Monad m) =>
   (e1 :> es) =>
   m ()
-subset = pure ()
+subset = satisfied @(e1 :> es)
 
+satisfied :: forall c m. (Monad m, c) => m ()
+satisfied = pure ()
+
 effTag :: Eff es (Proxy es)
 effTag = pure Proxy
 
@@ -499,7 +566,9 @@
 throw h = case mapHandle h of MkException throw_ -> throw_
 
 has :: forall a b. (a :> b) => a `In` b
-has = In# (# #)
+-- This is safe because, as shown by instanceProof1/2/3, the only way
+-- to construct `a :> b` is if `a `In` b`.
+has = unsafeInAxiom ZW
 
 data Dict c where
   Dict :: forall c. (c) => Dict c
@@ -1398,6 +1467,8 @@
   Eff es a
 asks (MkReader st) f = fmap f (get st)
 
+-- | Locally override the value in the @Reader@. It will be restored
+-- when the @local@ block ends.
 local ::
   (e1 :> es) =>
   Reader r e1 ->
@@ -1476,7 +1547,8 @@
 
     useImplIn k h'
 
-instance (Handle h) => Handle (HandleReader h) where mapHandle = mapHandleReader
+instance (Handle h) => Handle (HandleReader h) where
+  handleImpl = handleMapHandle mapHandleReader
 
 newtype ConstEffect r (e :: Effects) = MkConstEffect r
 
@@ -1488,4 +1560,4 @@
 runConstEffect r k = useImplIn k (MkConstEffect r)
 
 instance Handle (ConstEffect r) where
-  mapHandle = coerce
+  handleImpl = handleMapHandle coerce
diff --git a/src/Bluefin/Internal/Examples.hs b/src/Bluefin/Internal/Examples.hs
--- a/src/Bluefin/Internal/Examples.hs
+++ b/src/Bluefin/Internal/Examples.hs
@@ -668,7 +668,7 @@
   }
 
 instance Handle Counter5 where
-  mapHandle c =
+  handleImpl = handleMapHandle $ \c ->
     MkCounter5
       { incCounter5Impl = useImplUnder (incCounter5Impl c),
         getCounter5Impl = \msg -> useImplUnder (getCounter5Impl c msg)
@@ -729,7 +729,7 @@
   }
 
 instance Handle Counter6 where
-  mapHandle c =
+  handleImpl = handleMapHandle $ \c ->
     MkCounter6
       { incCounter6Impl = useImplUnder (incCounter6Impl c),
         counter6State = mapHandle (counter6State c),
@@ -792,7 +792,7 @@
   }
 
 instance Handle Counter7 where
-  mapHandle c =
+  handleImpl = handleMapHandle $ \c ->
     MkCounter7
       { incCounter7Impl = \ex -> useImplUnder (incCounter7Impl c ex),
         counter7State = mapHandle (counter7State c),
@@ -865,7 +865,7 @@
   }
 
 instance Handle FileSystem where
-  mapHandle fs =
+  handleImpl = handleMapHandle $ \fs ->
     MkFileSystem
       { readFileImpl = \fp -> useImplUnder (readFileImpl fs fp),
         writeFileImpl = \fp s -> useImplUnder (writeFileImpl fs fp s)
@@ -954,17 +954,18 @@
   }
 
 instance Handle Application where
-  mapHandle
-    MkApplication
-      { queryDatabase = q,
-        applicationState = a,
-        logger = l
-      } =
-      MkApplication
-        { queryDatabase = \s i -> useImplUnder (q s i),
-          applicationState = mapHandle a,
-          logger = mapHandle l
-        }
+  handleImpl =
+    handleMapHandle $
+      \MkApplication
+         { queryDatabase = q,
+           applicationState = a,
+           logger = l
+         } ->
+          MkApplication
+            { queryDatabase = \s i -> useImplUnder (q s i),
+              applicationState = mapHandle a,
+              logger = mapHandle l
+            }
 
 -- This example shows a case where we can use @bracket@ polymorphically
 -- in order to perform correct cleanup if @es@ is instantiated to a
@@ -1051,7 +1052,7 @@
   }
 
 instance Handle (DynamicReader r) where
-  mapHandle h =
+  handleImpl = handleMapHandle $ \h ->
     DynamicReader
       { askLRImpl = useImplUnder (askLRImpl h),
         localLRImpl = \f k -> useImplUnder (localLRImpl h f k)
@@ -1091,14 +1092,14 @@
   evalState () $ \st1 ->
     evalState () $ \st2 -> do
       Proxy :: Proxy es <- effTag
-      subset @es @es
+      satisfied @(es :> es)
 
       Proxy :: Proxy e1 <- handleTag st1
       Proxy :: Proxy e2 <- handleTag st2
 
-      subset @e1 @e1
-      subset @e2 @e2
-      subset @e1 @(e1 :& e2)
-      subset @e2 @(e1 :& e2)
+      satisfied @(e1 :> e1)
+      satisfied @(e2 :> e2)
+      satisfied @(e1 :> (e1 :& e2))
+      satisfied @(e2 :> (e1 :& e2))
 
-      subset @(e1 :& e2) @(e1 :& e2)
+      satisfied @((e1 :& e2) :> (e1 :& e2))