diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+# 0.3.0.0
+
+* Add `Bluefin.Internal.OneWayCoercible` module and related instances
+
+* Add `Bluefin.Internal.OneWayCoercibleHandle` and related functions
+
 ## 0.2.1.0
 
 * Add `handleImpl`, `HandleD` and `handleMapHandle`
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.1.0
+version:            0.3.0.0
 license:            MIT
 license-file:       LICENSE
 author:             Tom Ellis
@@ -86,6 +86,7 @@
       Bluefin.Internal.Examples,
       Bluefin.Internal.Exception.Scoped,
       Bluefin.Internal.Key,
+      Bluefin.Internal.OneWayCoercible,
       Bluefin.Internal.Pipes,
       Bluefin.Internal.System.IO
 
diff --git a/src/Bluefin/Internal.hs b/src/Bluefin/Internal.hs
--- a/src/Bluefin/Internal.hs
+++ b/src/Bluefin/Internal.hs
@@ -2,15 +2,26 @@
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UnliftedNewtypes #-}
 {-# OPTIONS_HADDOCK not-home #-}
 
 module Bluefin.Internal where
 
 import qualified Bluefin.Internal.Exception.Scoped as ScopedException
+import Bluefin.Internal.OneWayCoercible
+  ( OneWayCoercible (oneWayCoercibleImpl),
+    OneWayCoercion,
+    gOneWayCoercible,
+    oneWayCoerce,
+    oneWayCoerceWith,
+    oneWayCoercible,
+    unsafeOneWayCoercible,
+  )
 import qualified Control.Concurrent.Async as Async
 import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)
 import qualified Control.Exception
@@ -27,6 +38,7 @@
 import Data.Proxy (Proxy (Proxy))
 import Data.Type.Coercion (Coercion (Coercion))
 import GHC.Exts (Proxy#, proxy#)
+import GHC.Generics (Generic)
 import System.IO.Unsafe (unsafePerformIO)
 import Unsafe.Coerce (unsafeCoerce)
 import Prelude hiding (drop, head, read, return)
@@ -40,12 +52,18 @@
 
 type (:&) = Union
 
-type role Eff nominal representational
-
 newtype Eff (es :: Effects) a = UnsafeMkEff {unsafeUnEff :: IO a}
   deriving stock (Functor)
   deriving newtype (Applicative, Monad)
 
+type role Eff nominal representational
+
+instance (e :> es) => OneWayCoercible (Eff e) (Eff es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
+instance (e :> es) => OneWayCoercible (Eff e r) (Eff es r) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 -- | Because doing 'IO' operations inside 'Eff' requires a value-level
 -- argument we can't give @IO@-related instances to @Eff@ directly.
 -- Instead we wrap it in @EffReader@.
@@ -327,18 +345,30 @@
 -- | Handle to an exception of type @exn@
 newtype Exception exn (e :: Effects)
   = MkException (forall a. exn -> Eff e a)
+  deriving (Handle) via OneWayCoercibleHandle (Exception exn)
 
 type role Exception representational nominal
 
+instance (e :> es) => OneWayCoercible (Exception ex e) (Exception ex es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 -- | A handle to a strict mutable state of type @s@
 newtype State s (e :: Effects) = UnsafeMkState (IORef s)
+  deriving (Handle) via OneWayCoercibleHandle (State s)
 
 type role State representational nominal
 
+instance (e :> es) => OneWayCoercible (State s e) (State s es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 -- | A handle to a coroutine that yields values of type @a@ and then
 -- expects values of type @b@.
 newtype Coroutine a b (e :: Effects) = MkCoroutine (a -> Eff e b)
+  deriving (Handle) via OneWayCoercibleHandle (Coroutine a b)
 
+instance (e :> es) => OneWayCoercible (Coroutine a b e) (Coroutine a b es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 -- | A handle to a stream that yields values of type @a@.  It is
 -- implemented as a handle to a coroutine that yields values of type
 -- @a@ and then expects values of type @()@.
@@ -358,30 +388,15 @@
 --
 -- @
 -- data Application e = MkApplication
---   { queryDatabase :: forall e'. String -> Int -> Eff (e' :& e) [String],
+--   { queryDatabase :: String -> Int -> Eff e [String],
 --     applicationState :: State (Int, Bool) e,
 --     logger :: Stream String e
 --   }
--- @
---
--- To define @mapHandle@ for @Application@ you should apply
--- @mapHandle@ to all the fields that are themeselves handles and
--- apply 'useImplUnder' to all the fields that are dynamic effects:
+--   deriving (Generic)
+--   deriving (Handle) via 'OneWayCoercibleHandle' Application
 --
--- @
--- instance Handle Application where
---   'handleImpl' =
---     'handleMapHandle' $
---       \\MkApplication
---          { queryDatabase = q,
---            applicationState = a,
---            logger = l
---          } ->
---           MkApplication
---             { queryDatabase = \\s i -> 'useImplUnder' (q s i),
---               applicationState = 'mapHandle' a,
---               logger = mapHandle l
---             }
+-- instance (e :> es) => 'OneWayCoercible' (Application e) (Application es) where
+--   oneWayCoercibleImpl = 'gOneWayCoercible'
 -- @
 class Handle (h :: Effects -> Type) where
   {-# MINIMAL handleImpl | mapHandle #-}
@@ -405,6 +420,22 @@
   -- you should change it to
   --
   -- @
+  -- data MyHandle e = ...
+  --   deriving (Generic)
+  --   deriving (Handle) via OneWayCoercibleHandle MyHandle
+  --
+  -- instance (e :> es) => OneWayCoercible (MyHandle e) (MyHandle es) where
+  --   oneWayCoercibleImpl = gOneWayCoercible
+  -- @
+  --
+  -- If that doesn't work for any reason you can always reuse your old
+  -- definition of @mapHandle@ as follows.  However,
+  -- 'handleMapHandle' will be removed at some point in the future, so
+  -- you can [open a new issue on
+  -- Bluefin](https://github.com/tomjaguarpaw/bluefin/issues/new) to
+  -- ask for advice.
+  --
+  -- @
   -- instance Handle MyHandle where
   --   handleImpl = handleMapHandle $ \\h -> \<definition\>
   -- @
@@ -422,23 +453,40 @@
   HandleD h
 handleMapHandle = MkHandleD
 
-instance Handle (State s) where
-  handleImpl = handleMapHandle $ \(UnsafeMkState s) -> UnsafeMkState s
+handleOneWayCoercible ::
+  (forall e es. (e :> es) => OneWayCoercible (h e) (h es)) =>
+  -- | ͘
+  HandleD h
+handleOneWayCoercible = MkHandleD oneWayCoerce
 
-instance Handle (Exception s) where
-  handleImpl = handleMapHandle $ \(MkException s) ->
-    MkException (weakenEff has . s)
+handleOneWayCoercion ::
+  (forall e es. (e :> es) => OneWayCoercion (h e) (h es)) ->
+  -- | ͘
+  HandleD h
+handleOneWayCoercion owc = MkHandleD (oneWayCoerceWith owc)
 
-instance Handle (Coroutine a b) where
-  handleImpl = handleMapHandle $ \(MkCoroutine f) ->
-    MkCoroutine (fmap useImpl f)
+-- { OneWayCoercibleHandle
 
-instance Handle (Writer w) where
-  handleImpl = handleMapHandle $ \(Writer wr) -> Writer (mapHandle wr)
+-- | 'OneWayCoercibleHandle' is used to derive 'Handle' instances
+-- using @DerivingVia@
+newtype OneWayCoercibleHandle a es = MkOneWayCoercibleHandle (a es)
+  deriving stock (Generic)
 
-instance Handle IOE where
-  handleImpl = handleMapHandle $ \MkIOE -> MkIOE
+instance
+  forall h.
+  (forall e' es'. (e' :> es') => OneWayCoercible (OneWayCoercibleHandle h e') (OneWayCoercibleHandle h es')) =>
+  Handle (OneWayCoercibleHandle h)
+  where
+  handleImpl = handleOneWayCoercible
 
+instance
+  (OneWayCoercible (h e) (h es)) =>
+  OneWayCoercible (OneWayCoercibleHandle h e) (OneWayCoercibleHandle h es)
+  where
+  oneWayCoercibleImpl = gOneWayCoercible
+
+-- }
+
 -- | 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.
@@ -1286,9 +1334,13 @@
 
 -- | Handle that allows you to run 'IO' operations
 data IOE (e :: Effects) = MkIOE
+  deriving (Handle) via OneWayCoercibleHandle IOE
 
 type role IOE nominal
 
+instance (e :> es) => OneWayCoercible (IOE e) (IOE es) where
+  oneWayCoercibleImpl = unsafeOneWayCoercible
+
 -- | Run an 'IO' operation in 'Eff'
 --
 -- @
@@ -1373,7 +1425,11 @@
     Left (l, _) -> Left l
 
 newtype Writer w e = Writer (Stream w e)
+  deriving (Handle) via OneWayCoercibleHandle (Writer w)
 
+instance (e :> es) => OneWayCoercible (Writer w e) (Writer w es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 -- |
 -- @
 -- >>> 'Data.Monoid.getAny' $ snd $ runPureEff $ runWriter $ \\w -> do
@@ -1429,6 +1485,9 @@
 newtype Reader r e = MkReader (State r e)
   deriving newtype (Handle)
 
+instance (e :> es) => OneWayCoercible (Reader r e) (Reader r es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 runReader ::
   -- | Initial value for @Reader@.
   r ->
@@ -1548,16 +1607,20 @@
     useImplIn k h'
 
 instance (Handle h) => Handle (HandleReader h) where
+  -- This handleImpl is now a special case that doesn't use
+  -- OneWayCoercion. We can only fix that when we store a
+  -- OneWayCoercion inside `Handle`.
   handleImpl = handleMapHandle mapHandleReader
 
 newtype ConstEffect r (e :: Effects) = MkConstEffect r
+  deriving (Handle) via OneWayCoercibleHandle (ConstEffect r)
 
+instance (e :> es) => OneWayCoercible (ConstEffect r e) (ConstEffect r es) where
+  oneWayCoercibleImpl = oneWayCoercible
+
 runConstEffect ::
   r ->
   (forall e. ConstEffect r e -> Eff (e :& es) a) ->
   -- | ͘
   Eff es a
 runConstEffect r k = useImplIn k (MkConstEffect r)
-
-instance Handle (ConstEffect r) where
-  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
@@ -1,9 +1,14 @@
+{-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE NoMonoLocalBinds #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 
 module Bluefin.Internal.Examples where
 
 import Bluefin.Internal hiding (b, w)
+import Bluefin.Internal.OneWayCoercible
+  ( OneWayCoercible (oneWayCoercibleImpl),
+    gOneWayCoercible,
+  )
 import Bluefin.Internal.Pipes
   ( Producer,
     runEffect,
@@ -20,6 +25,7 @@
 import Data.Foldable (for_)
 import Data.Monoid (Any (Any, getAny))
 import Data.Proxy (Proxy (Proxy))
+import GHC.Generics (Generic)
 import Text.Read (readMaybe)
 import Prelude hiding
   ( break,
@@ -663,22 +669,20 @@
 -- Counter 5
 
 data Counter5 e = MkCounter5
-  { incCounter5Impl :: forall e'. Eff (e' :& e) (),
-    getCounter5Impl :: forall e'. String -> Eff (e' :& e) Int
+  { incCounter5Impl :: Eff e (),
+    getCounter5Impl :: String -> Eff e Int
   }
+  deriving (Generic)
+  deriving (Handle) via OneWayCoercibleHandle Counter5
 
-instance Handle Counter5 where
-  handleImpl = handleMapHandle $ \c ->
-    MkCounter5
-      { incCounter5Impl = useImplUnder (incCounter5Impl c),
-        getCounter5Impl = \msg -> useImplUnder (getCounter5Impl c msg)
-      }
+instance (e :> es) => OneWayCoercible (Counter5 e) (Counter5 es) where
+  oneWayCoercibleImpl = gOneWayCoercible
 
 incCounter5 :: (e :> es) => Counter5 e -> Eff es ()
-incCounter5 e = makeOp (incCounter5Impl (mapHandle e))
+incCounter5 e = incCounter5Impl (mapHandle e)
 
 getCounter5 :: (e :> es) => Counter5 e -> String -> Eff es Int
-getCounter5 e msg = makeOp (getCounter5Impl (mapHandle e) msg)
+getCounter5 e msg = getCounter5Impl (mapHandle e) msg
 
 runCounter5 ::
   (e1 :> es) =>
@@ -723,21 +727,18 @@
 -- Counter 6
 
 data Counter6 e = MkCounter6
-  { incCounter6Impl :: forall e'. Eff (e' :& e) (),
+  { incCounter6Impl :: Eff e (),
     counter6State :: State Int e,
     counter6Stream :: Stream String e
   }
+  deriving (Generic)
+  deriving (Handle) via OneWayCoercibleHandle Counter6
 
-instance Handle Counter6 where
-  handleImpl = handleMapHandle $ \c ->
-    MkCounter6
-      { incCounter6Impl = useImplUnder (incCounter6Impl c),
-        counter6State = mapHandle (counter6State c),
-        counter6Stream = mapHandle (counter6Stream c)
-      }
+instance (e :> es) => OneWayCoercible (Counter6 e) (Counter6 es) where
+  oneWayCoercibleImpl = gOneWayCoercible
 
 incCounter6 :: (e :> es) => Counter6 e -> Eff es ()
-incCounter6 e = makeOp (incCounter6Impl (mapHandle e))
+incCounter6 e = incCounter6Impl (mapHandle e)
 
 getCounter6 :: (e :> es) => Counter6 e -> String -> Eff es Int
 getCounter6 (MkCounter6 _ st y) msg = do
@@ -860,23 +861,21 @@
 -- FileSystem
 
 data FileSystem es = MkFileSystem
-  { readFileImpl :: forall e. FilePath -> Eff (e :& es) String,
-    writeFileImpl :: forall e. FilePath -> String -> Eff (e :& es) ()
+  { readFileImpl :: FilePath -> Eff es String,
+    writeFileImpl :: FilePath -> String -> Eff es ()
   }
+  deriving (Generic)
+  deriving (Handle) via OneWayCoercibleHandle FileSystem
 
-instance Handle FileSystem where
-  handleImpl = handleMapHandle $ \fs ->
-    MkFileSystem
-      { readFileImpl = \fp -> useImplUnder (readFileImpl fs fp),
-        writeFileImpl = \fp s -> useImplUnder (writeFileImpl fs fp s)
-      }
+instance (e :> es) => OneWayCoercible (FileSystem e) (FileSystem es) where
+  oneWayCoercibleImpl = gOneWayCoercible
 
 readFile :: (e :> es) => FileSystem e -> FilePath -> Eff es String
-readFile fs filepath = makeOp (readFileImpl (mapHandle fs) filepath)
+readFile fs filepath = readFileImpl (mapHandle fs) filepath
 
 writeFile :: (e :> es) => FileSystem e -> FilePath -> String -> Eff es ()
 writeFile fs filepath contents =
-  makeOp (writeFileImpl (mapHandle fs) filepath contents)
+  writeFileImpl (mapHandle fs) filepath contents
 
 runFileSystemPure ::
   (e1 :> es) =>
@@ -948,24 +947,15 @@
 -- instance Handle example
 
 data Application e = MkApplication
-  { queryDatabase :: forall e'. String -> Int -> Eff (e' :& e) [String],
+  { queryDatabase :: String -> Int -> Eff e [String],
     applicationState :: State (Int, Bool) e,
     logger :: Stream String e
   }
+  deriving (Generic)
+  deriving (Handle) via OneWayCoercibleHandle Application
 
-instance Handle Application where
-  handleImpl =
-    handleMapHandle $
-      \MkApplication
-         { queryDatabase = q,
-           applicationState = a,
-           logger = l
-         } ->
-          MkApplication
-            { queryDatabase = \s i -> useImplUnder (q s i),
-              applicationState = mapHandle a,
-              logger = mapHandle l
-            }
+instance (e :> es) => OneWayCoercible (Application e) (Application es) where
+  oneWayCoercibleImpl = gOneWayCoercible
 
 -- This example shows a case where we can use @bracket@ polymorphically
 -- in order to perform correct cleanup if @es@ is instantiated to a
@@ -1047,14 +1037,14 @@
     Right contents -> contents
 
 data DynamicReader r e = DynamicReader
-  { askLRImpl :: forall e'. Eff (e' :& e) r,
+  { askLRImpl :: Eff e r,
     localLRImpl :: forall e' a. (r -> r) -> Eff e' a -> Eff (e' :& e) a
   }
 
 instance Handle (DynamicReader r) where
   handleImpl = handleMapHandle $ \h ->
     DynamicReader
-      { askLRImpl = useImplUnder (askLRImpl h),
+      { askLRImpl = useImpl (askLRImpl h),
         localLRImpl = \f k -> useImplUnder (localLRImpl h f k)
       }
 
@@ -1062,7 +1052,7 @@
   (e :> es) =>
   DynamicReader r e ->
   Eff es r
-askLR c = makeOp (askLRImpl (mapHandle c))
+askLR c = askLRImpl (mapHandle c)
 
 localLR ::
   (e :> es) =>
@@ -1082,7 +1072,7 @@
       k
       DynamicReader
         { askLRImpl = ask h,
-          localLRImpl = \f k' -> makeOp (local h f (useImpl k'))
+          localLRImpl = \f k' -> local h f (useImpl k')
         }
 
 -- Fails to compile unless '(e :> es) => e :> (x :& es)' is incoherent
diff --git a/src/Bluefin/Internal/OneWayCoercible.hs b/src/Bluefin/Internal/OneWayCoercible.hs
new file mode 100644
--- /dev/null
+++ b/src/Bluefin/Internal/OneWayCoercible.hs
@@ -0,0 +1,122 @@
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Bluefin.Internal.OneWayCoercible
+  ( module Bluefin.Internal.OneWayCoercible,
+    Generic,
+  )
+where
+
+import Data.Coerce (Coercible, coerce)
+import Data.Type.Coercion (Coercion (Coercion))
+import GHC.Generics
+import Unsafe.Coerce (unsafeCoerce)
+
+gOneWayCoercion ::
+  forall a b. (GOneWayCoercible (Rep a) (Rep b)) => OneWayCoercion a b
+gOneWayCoercion = unsafeOneWayCoercion
+
+gOneWayCoercible ::
+  (GOneWayCoercible (Rep (h e)) (Rep (h es))) =>
+  -- | ͘
+  OneWayCoercibleD (h e) (h es)
+gOneWayCoercible = MkOneWayCoercibleD gOneWayCoercion
+
+gOneWayCoercible2 ::
+  (GOneWayCoercible (Rep (h e e')) (Rep (h es es'))) =>
+  OneWayCoercibleD (h e e') (h es es')
+gOneWayCoercible2 = MkOneWayCoercibleD gOneWayCoercion
+
+oneWayCoercible :: (Coercible a b) => OneWayCoercibleD a b
+oneWayCoercible = MkOneWayCoercibleD (MkOneWayCoercion Coercion)
+
+unsafeOneWayCoercion :: forall a b. OneWayCoercion a b
+unsafeOneWayCoercion = MkOneWayCoercion (unsafeCoerce (Coercion @a @a))
+
+unsafeOneWayCoercible :: forall a b. OneWayCoercibleD a b
+unsafeOneWayCoercible = MkOneWayCoercibleD unsafeOneWayCoercion
+
+newtype OneWayCoercion a b = MkOneWayCoercion (Coercion a b)
+
+newtype OneWayCoercibleD a b = MkOneWayCoercibleD (OneWayCoercion a b)
+
+oneWayCoercion :: (OneWayCoercible a b) => OneWayCoercion a b
+oneWayCoercion = case oneWayCoercibleImpl of
+  MkOneWayCoercibleD oneWay -> oneWay
+
+oneWayCoerce :: forall a b. (OneWayCoercible a b) => a -> b
+oneWayCoerce = oneWayCoerceWith (oneWayCoercion @a @b)
+
+oneWayCoerceWith :: OneWayCoercion a b -> a -> b
+oneWayCoerceWith (MkOneWayCoercion Coercion) = coerce
+
+unsafeCoercionOfOneWayCoercion :: OneWayCoercion a b -> Coercion a b
+unsafeCoercionOfOneWayCoercion (MkOneWayCoercion c) = c
+
+unsafeCoercionOfOneWayCoercible ::
+  forall a b. (OneWayCoercible a b) => Coercion a b
+unsafeCoercionOfOneWayCoercible = case oneWayCoercion @a @b of
+  MkOneWayCoercion c -> c
+
+class OneWayCoercible a b where
+  oneWayCoercibleImpl :: OneWayCoercibleD a b
+
+instance {-# INCOHERENT #-} OneWayCoercible s s where
+  oneWayCoercibleImpl = oneWayCoercible
+
+instance OneWayCoercible () () where
+  oneWayCoercibleImpl = oneWayCoercible
+
+instance
+  (OneWayCoercible a1 a2) =>
+  OneWayCoercible (Maybe a1) (Maybe a2)
+  where
+  oneWayCoercibleImpl = case unsafeCoercionOfOneWayCoercible @a1 @a2 of
+    Coercion -> oneWayCoercible
+
+instance
+  (OneWayCoercible a1 a2, OneWayCoercible b1 b2) =>
+  OneWayCoercible (Either a1 b1) (Either a2 b2)
+  where
+  oneWayCoercibleImpl = case unsafeCoercionOfOneWayCoercible @a1 @a2 of
+    Coercion -> case unsafeCoercionOfOneWayCoercible @b1 @b2 of
+      Coercion -> oneWayCoercible
+
+-- | Other sizes of tuples follow this pattern. We will add them when
+-- someone needs them.
+instance
+  (OneWayCoercible a1 a2, OneWayCoercible b1 b2) =>
+  OneWayCoercible (a1, b1) (a2, b2)
+  where
+  oneWayCoercibleImpl = case unsafeCoercionOfOneWayCoercible @a1 @a2 of
+    Coercion -> case unsafeCoercionOfOneWayCoercible @b1 @b2 of
+      Coercion -> oneWayCoercible
+
+trans :: OneWayCoercion a b -> OneWayCoercion b c -> OneWayCoercion a c
+trans c1 c2 = case unsafeCoercionOfOneWayCoercion c1 of
+  Coercion -> case unsafeCoercionOfOneWayCoercion c2 of
+    Coercion -> MkOneWayCoercion Coercion
+
+class GOneWayCoercible a b
+
+instance GOneWayCoercible U1 U1
+
+instance
+  (OneWayCoercible c c') =>
+  GOneWayCoercible (K1 i c) (K1 i' c')
+
+instance
+  (GOneWayCoercible f f') =>
+  GOneWayCoercible (M1 i t f) (M1 i' t' f')
+
+instance
+  (GOneWayCoercible f f', GOneWayCoercible g g') =>
+  GOneWayCoercible (f :*: g) (f' :*: g')
+
+instance
+  (OneWayCoercible a a', OneWayCoercible b b') =>
+  OneWayCoercible (a' -> b) (a -> b')
+  where
+  oneWayCoercibleImpl = case oneWayCoercion @a @a' of
+    MkOneWayCoercion Coercion -> case oneWayCoercion @b @b' of
+      MkOneWayCoercion Coercion ->
+        MkOneWayCoercibleD (MkOneWayCoercion Coercion)