diff --git a/examples/NonEmptyList.hs b/examples/NonEmptyList.hs
--- a/examples/NonEmptyList.hs
+++ b/examples/NonEmptyList.hs
@@ -5,8 +5,6 @@
 
 import Control.Comonad
 
-import Data.Semigroup
-
 -- A free semigroup allows you to create singletons and append them.
 -- So it is a non-empty list.
 type NonEmptyList = Free Semigroup
diff --git a/free-functors.cabal b/free-functors.cabal
--- a/free-functors.cabal
+++ b/free-functors.cabal
@@ -1,5 +1,5 @@
 name:                free-functors
-version:             0.8.4
+version:             0.9
 synopsis:            Free functors, adjoint to functors that forget class constraints.
 description:         A free functor is a left adjoint to a forgetful functor. It used to be the case
                      that the only category that was easy to work with in Haskell was Hask itself, so
@@ -47,13 +47,13 @@
     Haskell2010
 
   build-depends:
-    base == 4.11.*,
-    template-haskell == 2.13.*,
+    base == 4.12.*,
+    template-haskell == 2.14.*,
     constraints == 0.10.*,
     transformers == 0.5.*,
     comonad == 5.*,
     algebraic-classes == 0.9.*,
-    contravariant == 1.4.*,
+    contravariant == 1.5.*,
     bifunctors == 5.*,
     profunctors == 5.*
 
diff --git a/src/Data/Functor/Cofree.hs b/src/Data/Functor/Cofree.hs
--- a/src/Data/Functor/Cofree.hs
+++ b/src/Data/Functor/Cofree.hs
@@ -1,12 +1,8 @@
 {-# LANGUAGE
     ConstraintKinds
-  , RankNTypes
-  , TypeOperators
-  , FlexibleInstances
   , GADTs
-  , MultiParamTypeClasses
   , UndecidableInstances
-  , ScopedTypeVariables
+  , QuantifiedConstraints
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -25,9 +21,6 @@
 import Control.Monad
 import Control.Comonad
 
-import Data.Constraint
-import Data.Constraint.Forall
-
 import Data.Functor.Identity
 import Data.Functor.Compose
 
@@ -43,15 +36,6 @@
 leftAdjunct :: c a => (a -> b) -> a -> Cofree c b
 leftAdjunct f a = Cofree f a
 
-leftAdjunctF :: ForallF c f => (f a -> b) -> f a -> Cofree c b
-leftAdjunctF = h instF leftAdjunct
-  where
-    h :: ForallF c f
-      => (ForallF c f :- c (f a))
-      -> (c (f a) => (f a -> b) -> f a -> Cofree c b)
-      -> (f a -> b) -> f a -> Cofree c b
-    h (Sub Dict) f = f
-
 -- | @unit = leftAdjunct id@
 unit :: c b => b -> Cofree c b
 unit = leftAdjunct id
@@ -67,15 +51,15 @@
   extract = counit
   duplicate (Cofree k a) = Cofree (leftAdjunct k) a
 
-instance (ForallF c Identity, ForallF c (Compose (Cofree c) (Cofree c)))
+instance (forall x. c (Identity x), forall x. c (Compose (Cofree c) (Cofree c) x))
   => Applicative (Cofree c) where
-  pure = leftAdjunctF runIdentity . Identity
+  pure = leftAdjunct runIdentity . Identity
   (<*>) = ap
 
-instance (ForallF c Identity, ForallF c (Compose (Cofree c) (Cofree c)))
+instance (forall x. c (Identity x), forall x. c (Compose (Cofree c) (Cofree c) x))
   => Monad (Cofree c) where
   return = pure
-  m >>= g = leftAdjunctF (extract . extract . getCompose) (Compose $ fmap g m)
+  m >>= g = leftAdjunct (extract . extract . getCompose) (Compose $ fmap g m)
 
 convert :: (c (w a), Comonad w) => w a -> Cofree c a
 convert = leftAdjunct extract
diff --git a/src/Data/Functor/Free.hs b/src/Data/Functor/Free.hs
--- a/src/Data/Functor/Free.hs
+++ b/src/Data/Functor/Free.hs
@@ -34,7 +34,6 @@
   , deriveInstances
   , unit
   , rightAdjunct
-  , rightAdjunctF
   , counit
   , leftAdjunct
   , transform
diff --git a/src/Data/Functor/Free/TH.hs b/src/Data/Functor/Free/TH.hs
--- a/src/Data/Functor/Free/TH.hs
+++ b/src/Data/Functor/Free/TH.hs
@@ -13,12 +13,12 @@
   , TemplateHaskell
   , PolyKinds
   , DataKinds
+  , QuantifiedConstraints
   #-}
 module Data.Functor.Free.TH where
 
 import Data.Constraint hiding (Class)
 import Data.Constraint.Class1
-import Data.Constraint.Forall
 
 import Control.Comonad
 import Data.Algebra
@@ -41,15 +41,6 @@
 rightAdjunct :: c b => (a -> b) -> Free c a -> b
 rightAdjunct f g = runFree g f
 
-rightAdjunctF :: ForallF c f => (a -> f b) -> Free c a -> f b
-rightAdjunctF = h instF rightAdjunct
-  where
-    h :: ForallF c f
-      => (ForallF c f :- c (f b))
-      -> (c (f b) => (a -> f b) -> Free c a -> f b)
-      -> (a -> f b) -> Free c a -> f b
-    h (Sub Dict) f = f
-
 -- | @counit = rightAdjunct id@
 counit :: c a => Free c a -> a
 counit = rightAdjunct id
@@ -78,10 +69,10 @@
 
 newtype Extract a = Extract { getExtract :: a }
 newtype Duplicate f a = Duplicate { getDuplicate :: f (f a) }
-instance (ForallF c Extract, ForallF c (Duplicate (Free c)))
+instance (forall x. c (Extract x), forall x. c (Duplicate (Free c) x))
   => Comonad (Free c) where
-  extract = getExtract . rightAdjunctF Extract
-  duplicate = getDuplicate . rightAdjunctF (Duplicate . unit . unit)
+  extract = getExtract . rightAdjunct Extract
+  duplicate = getDuplicate . rightAdjunct (Duplicate . unit . unit)
       
 
 class ForallLifted c where
diff --git a/src/Data/Functor/HCofree.hs b/src/Data/Functor/HCofree.hs
--- a/src/Data/Functor/HCofree.hs
+++ b/src/Data/Functor/HCofree.hs
@@ -3,10 +3,8 @@
   , RankNTypes
   , TypeOperators
   , ConstraintKinds
-  , FlexibleContexts
-  , FlexibleInstances
-  , ScopedTypeVariables
   , UndecidableInstances
+  , QuantifiedConstraints
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -28,9 +26,8 @@
 
 import Control.Comonad
 import Control.Comonad.Trans.Class
+import Data.Foldable
 import Data.Functor.Identity
-import Data.Constraint
-import Data.Constraint.Class1
 
 -- | Natural transformations.
 type f :~> g = forall b. f b -> g b
@@ -78,31 +75,36 @@
 unwrap :: HCofree Comonad g a -> g (HCofree Comonad g a)
 unwrap = counit . duplicate
 
-instance SuperClass1 Functor c => Functor (HCofree c g) where
-  fmap f (HCofree k a) = HCofree k (h scls1 f a)
-    where
-      h :: c f => (c f :- Functor f) -> (a -> b) -> f a -> f b
-      h (Sub Dict) = fmap
+instance (forall x. c x => Functor x) => Functor (HCofree c g) where
+  fmap f (HCofree k a) = HCofree k (fmap f a)
+  a <$ HCofree k b = HCofree k (a <$ b)
 
-instance SuperClass1 Foldable c => Foldable (HCofree c g) where
-  foldMap f (HCofree _ a) = h scls1 f a
-    where
-      h :: (c f, Monoid m) => (c f :- Foldable f) -> (a -> m) -> f a -> m
-      h (Sub Dict) = foldMap
+instance (forall x. c x => Foldable x) => Foldable (HCofree c g) where
+  foldMap f (HCofree _ a) = foldMap f a
+  fold (HCofree _ a) = fold a
+  foldr f z (HCofree _ a) = foldr f z a
+  foldl f z (HCofree _ a) = foldl f z a
+  foldl' f z (HCofree _ a) = foldl' f z a
+  foldr1 f (HCofree _ a) = foldr1 f a
+  foldr' f z (HCofree _ a) = foldr' f z a
+  foldl1 f (HCofree _ a) = foldl1 f a
+  toList (HCofree _ a) = toList a
+  null (HCofree _ a) = null a
+  length (HCofree _ a) = length a
+  elem e (HCofree _ a) = elem e a
+  maximum (HCofree _ a) = maximum a
+  minimum (HCofree _ a) = minimum a
+  sum (HCofree _ a) = sum a
+  product (HCofree _ a) = product a
 
-instance SuperClass1 Traversable c => Traversable (HCofree c g) where
-  traverse f (HCofree k a) = HCofree k <$> h scls1 f a
-    where
-      h :: (c t, Applicative f) => (c t :- Traversable t) -> (a -> f b) -> t a -> f (t b)
-      h (Sub Dict) = traverse
+instance (forall x. c x => Traversable x) => Traversable (HCofree c g) where
+  traverse f (HCofree k a) = HCofree k <$> traverse f a
+  sequenceA (HCofree k a) = HCofree k <$> sequenceA a
+  mapM f (HCofree k a) = HCofree k <$> mapM f a
+  sequence (HCofree k a) = HCofree k <$> sequence a
 
 -- | The cofree comonad of a functor.
-instance SuperClass1 Comonad c => Comonad (HCofree c g) where
-  extract (HCofree _ a) = h scls1 a
-    where
-      h :: c f => (c f :- Comonad f) -> f a -> a
-      h (Sub Dict) = extract
-  extend f (HCofree k a) = HCofree k $ h scls1 (f . HCofree k) a
-    where
-      h :: c f => (c f :- Comonad f) -> (f a -> b) -> (f a -> f b)
-      h (Sub Dict) = extend
+instance (forall x. c x => Comonad x) => Comonad (HCofree c g) where
+  extract (HCofree _ a) = extract a
+  extend f (HCofree k a) = HCofree k $ extend (f . HCofree k) a
+  duplicate (HCofree k a) = HCofree k $ extend (HCofree k) a
diff --git a/src/Data/Functor/HFree.hs b/src/Data/Functor/HFree.hs
--- a/src/Data/Functor/HFree.hs
+++ b/src/Data/Functor/HFree.hs
@@ -2,9 +2,8 @@
     RankNTypes
   , TypeOperators
   , ConstraintKinds
-  , FlexibleContexts
-  , ScopedTypeVariables
   , UndecidableInstances
+  , QuantifiedConstraints
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -29,11 +28,7 @@
 import Data.Functor.Identity
 import Data.Functor.Contravariant
 import Data.Functor.Contravariant.Divisible
-import Data.Constraint
-import Data.Constraint.Class1
-import Data.Void
 
-
 -- | Natural transformations.
 type f :~> g = forall b. f b -> g b
 
@@ -80,65 +75,41 @@
 wrap as = unit as >>= id
 
 
-instance SuperClass1 Functor c => Functor (HFree c f) where
-  fmap f (HFree g) = HFree $ \k -> h scls1 f (g k)
-    where
-      h :: c g => (c g :- Functor g) -> (a -> b) -> g a -> g b
-      h (Sub Dict) = fmap
+instance (forall x. c x => Functor x) => Functor (HFree c f) where
+  fmap f (HFree g) = HFree $ \k -> fmap f (g k)
+  a <$ HFree g = HFree $ \k -> a <$ g k
 
-instance SuperClass1 Applicative c => Applicative (HFree c f) where
-  pure a = HFree $ const (h scls1 a)
-    where
-      h :: c g => (c g :- Applicative g) -> a -> g a
-      h (Sub Dict) = pure
-  HFree f <*> HFree g = HFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- Applicative g) -> g (a -> b) -> g a -> g b
-      h (Sub Dict) = (<*>)
+instance (forall x. c x => Applicative x) => Applicative (HFree c f) where
+  pure a = HFree $ const (pure a)
+  HFree f <*> HFree g = HFree $ \k -> f k <*> g k
+  HFree f <* HFree g = HFree $ \k -> f k <* g k
+  HFree f *> HFree g = HFree $ \k -> f k *> g k
+  liftA2 f (HFree g) (HFree h) = HFree $ \k -> liftA2 f (g k) (h k)
 
-instance SuperClass1 Alternative c => Alternative (HFree c f) where
-  empty = HFree $ const (h scls1)
-    where
-      h :: c g => (c g :- Alternative g) -> g a
-      h (Sub Dict) = empty
-  HFree f <|> HFree g = HFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- Alternative g) -> g a -> g a -> g a
-      h (Sub Dict) = (<|>)
+instance (forall x. c x => Alternative x) => Alternative (HFree c f) where
+  empty = HFree $ const empty
+  HFree f <|> HFree g = HFree $ \k -> f k <|> g k
+  many (HFree f) = HFree $ \k -> many (f k)
+  some (HFree f) = HFree $ \k -> some (f k)
 
 -- | The free monad of a functor.
-instance SuperClass1 Monad c => Monad (HFree c f) where
+instance (forall x. c x => Monad x) => Monad (HFree c f) where
   return = pure
-  HFree f >>= g = HFree $ \k -> h scls1 (f k) (rightAdjunct k . g)
-    where
-      h :: c g => (c g :- Monad g) -> g a -> (a -> g b) -> g b
-      h (Sub Dict) = (>>=)
+  HFree f >>= g = HFree $ \k -> f k >>= rightAdjunct k . g
+  HFree f >> HFree g = HFree $ \k -> f k >> g k
+  fail s = HFree $ const (fail s)
 
 -- HFree Monad is only a monad transformer if rightAdjunct is called with monad morphisms.
 -- F.e. lift . return == return fails if the results are inspected with rightAdjunct (const Nothing).
 
-instance SuperClass1 Contravariant c => Contravariant (HFree c f) where
-  contramap f (HFree g) = HFree $ \k -> h scls1 f (g k)
-    where
-      h :: c g => (c g :- Contravariant g) -> (b -> a) -> g a -> g b
-      h (Sub Dict) = contramap
+instance (forall x. c x => Contravariant x) => Contravariant (HFree c f) where
+  contramap f (HFree g) = HFree $ \k -> contramap f (g k)
+  a >$ HFree g = HFree $ \k -> a >$ g k
 
-instance SuperClass1 Divisible c => Divisible (HFree c f) where
-  divide f (HFree a) (HFree b) = HFree $ \k -> h scls1 f (a k) (b k)
-    where
-      h :: c g => (c g :- Divisible g) -> (a -> (b, d)) -> g b -> g d -> g a
-      h (Sub Dict) = divide
-  conquer = HFree $ const (h scls1)
-    where
-      h :: c g => (c g :- Divisible g) -> g a
-      h (Sub Dict) = conquer
+instance (forall x. c x => Divisible x) => Divisible (HFree c f) where
+  divide f (HFree a) (HFree b) = HFree $ \k -> divide f (a k) (b k)
+  conquer = HFree $ const conquer
 
-instance SuperClass1 Decidable c => Decidable (HFree c f) where
-  choose f (HFree a) (HFree b) = HFree $ \k -> h scls1 f (a k) (b k)
-    where
-      h :: c g => (c g :- Decidable g) -> (a -> Either b d) -> g b -> g d -> g a
-      h (Sub Dict) = choose
-  lose f = HFree $ const (h scls1 f)
-    where
-      h :: c g => (c g :- Decidable g) -> (a -> Void) -> g a
-      h (Sub Dict) = lose
+instance (forall x. c x => Decidable x) => Decidable (HFree c f) where
+  choose f (HFree a) (HFree b) = HFree $ \k -> choose f (a k) (b k)
+  lose f = HFree $ const (lose f)
diff --git a/src/Data/Functor/HHCofree.hs b/src/Data/Functor/HHCofree.hs
--- a/src/Data/Functor/HHCofree.hs
+++ b/src/Data/Functor/HHCofree.hs
@@ -8,6 +8,7 @@
   , ScopedTypeVariables
   , UndecidableInstances
   , MultiParamTypeClasses
+  , QuantifiedConstraints
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -26,15 +27,12 @@
 module Data.Functor.HHCofree where
 
 import Prelude hiding ((.), id)
-import Data.Constraint (Dict(..), (:-)(..))
-import Data.Constraint.Class1
-import Data.Functor.HHFree (HHFree(..))
-import qualified Data.Functor.HHFree as F
 
 import Control.Category
-import Data.Bifunctor (Bifunctor(bimap))
+import Data.Bifunctor
 import Data.Bifunctor.Functor
 import Data.Profunctor
+import Data.Profunctor.Unsafe
 import Data.Profunctor.Monad
 
 
@@ -85,32 +83,25 @@
   produplicate = hextend id
 
 
-instance SuperClass1 Bifunctor c => Bifunctor (HHCofree c g) where
-  bimap f g (HHCofree k a) = HHCofree k (h scls1 f g a)
-    where
-      h :: c f => (c f :- Bifunctor f) -> (a -> a') -> (b -> b') -> f a b -> f a' b'
-      h (Sub Dict) = bimap
+instance (forall x. c x => Bifunctor x) => Bifunctor (HHCofree c g) where
+  bimap f g (HHCofree k a) = HHCofree k (bimap f g a)
+  first f (HHCofree k a) = HHCofree k (first f a)
+  second f (HHCofree k a) = HHCofree k (second f a)
       
-instance SuperClass1 Profunctor c => Profunctor (HHCofree c g) where
-  dimap f g (HHCofree k a) = HHCofree k (h scls1 f g a)
-    where
-      h :: c f => (c f :- Profunctor f) -> (a' -> a) -> (b -> b') -> f a b -> f a' b'
-      h (Sub Dict) = dimap
+instance (forall x. c x => Profunctor x) => Profunctor (HHCofree c g) where
+  dimap f g (HHCofree k a) = HHCofree k (dimap f g a)
+  lmap f (HHCofree k a) = HHCofree k (lmap f a)
+  rmap f (HHCofree k a) = HHCofree k (rmap f a)
+  f #. HHCofree k g = HHCofree k (f #. g)
+  HHCofree k g .# f = HHCofree k (g .# f)
       
-instance SuperClass1 Strong c => Strong (HHCofree c f) where
-  first' (HHCofree k a) = HHCofree k (h scls1 a)
-    where
-      h :: c g => (c g :- Strong g) -> g a b -> g (a, d) (b, d)
-      h (Sub Dict) = first'
+instance (forall x. c x => Strong x) => Strong (HHCofree c f) where
+  first' (HHCofree k a) = HHCofree k (first' a)
+  second' (HHCofree k a) = HHCofree k (second' a)
       
-instance SuperClass1 Choice c => Choice (HHCofree c f) where
-  left' (HHCofree k a) = HHCofree k (h scls1 a)
-    where
-      h :: c g => (c g :- Choice g) -> g a b -> g (Either a d) (Either b d)
-      h (Sub Dict) = left'
+instance (forall x. c x => Choice x) => Choice (HHCofree c f) where
+  left' (HHCofree k a) = HHCofree k (left' a)
+  right' (HHCofree k a) = HHCofree k (right' a)
       
-instance SuperClass1 Closed c => Closed (HHCofree c f) where
-  closed (HHCofree k a) = HHCofree k (h scls1 a)
-    where
-      h :: c g => (c g :- Closed g) -> g a b -> g (d -> a) (d -> b)
-      h (Sub Dict) = closed
+instance (forall x. c x => Closed x) => Closed (HHCofree c f) where
+  closed (HHCofree k a) = HHCofree k (closed a)
diff --git a/src/Data/Functor/HHFree.hs b/src/Data/Functor/HHFree.hs
--- a/src/Data/Functor/HHFree.hs
+++ b/src/Data/Functor/HHFree.hs
@@ -1,11 +1,9 @@
 {-# LANGUAGE
     RankNTypes
   , TypeOperators
-  , MonoLocalBinds
   , ConstraintKinds
-  , FlexibleContexts
-  , ScopedTypeVariables
   , UndecidableInstances
+  , QuantifiedConstraints
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -24,15 +22,15 @@
 module Data.Functor.HHFree where
 
 import Prelude hiding ((.), id)
-import Data.Constraint (Dict(..), (:-)(..))
-import Data.Constraint.Class1
 
 import Control.Arrow
 import Control.Category
-import Data.Bifunctor (Bifunctor(bimap))
+import Data.Bifunctor (Bifunctor)
+import qualified Data.Bifunctor as B (Bifunctor(..))
 import Data.Bifunctor.Functor
-import Data.Biapplicative (Biapplicative(bipure, (<<*>>)))
+import Data.Biapplicative (Biapplicative(..))
 import Data.Profunctor
+import Data.Profunctor.Unsafe
 import Data.Profunctor.Monad
 
 
@@ -81,92 +79,61 @@
   projoin = bind id
 
 
-instance SuperClass1 Category c => Category (HHFree c f) where
-  id = HHFree $ const (h scls1)
-    where
-      h :: c g => (c g :- Category g) -> g a a
-      h (Sub Dict) = id
-  HHFree f . HHFree g = HHFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- Category g) -> g b d -> g a b -> g a d
-      h (Sub Dict) = (.)
+instance (forall x. c x => Category x) => Category (HHFree c f) where
+  id = HHFree $ const id
+  HHFree f . HHFree g = HHFree $ \k -> f k . g k
 
-instance SuperClass1 Arrow c => Arrow (HHFree c f) where
-  arr f = HHFree $ const (h scls1 f)
-    where
-      h :: c g => (c g :- Arrow g) -> (a -> b) -> g a b
-      h (Sub Dict) = arr
-  HHFree f *** HHFree g = HHFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- Arrow g) -> g a b -> g d e -> g (a, d) (b, e)
-      h (Sub Dict) = (***)
+instance (forall x. c x => Arrow x) => Arrow (HHFree c f) where
+  arr f = HHFree $ const (arr f)
+  first (HHFree f) = HHFree $ \k -> first (f k)
+  second (HHFree f) = HHFree $ \k -> second (f k)
+  HHFree f *** HHFree g = HHFree $ \k -> f k *** g k
+  HHFree f &&& HHFree g = HHFree $ \k -> f k &&& g k
 
-instance SuperClass1 ArrowZero c => ArrowZero (HHFree c f) where
-  zeroArrow = HHFree $ const (h scls1)
-    where
-      h :: c g => (c g :- ArrowZero g) -> g a b
-      h (Sub Dict) = zeroArrow
+instance (forall x. c x => ArrowZero x) => ArrowZero (HHFree c f) where
+  zeroArrow = HHFree $ const zeroArrow
 
-instance SuperClass1 ArrowPlus c => ArrowPlus (HHFree c f) where
-  HHFree f <+> HHFree g = HHFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- ArrowPlus g) -> g a b -> g a b -> g a b
-      h (Sub Dict) = (<+>)
+instance (forall x. c x => ArrowPlus x) => ArrowPlus (HHFree c f) where
+  HHFree f <+> HHFree g = HHFree $ \k -> f k <+> g k
 
-instance SuperClass1 ArrowChoice c => ArrowChoice (HHFree c f) where
-  HHFree f +++ HHFree g = HHFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- ArrowChoice g) -> g a b -> g d e -> g (Either a d) (Either b e)
-      h (Sub Dict) = (+++)
+instance (forall x. c x => ArrowChoice x) => ArrowChoice (HHFree c f) where
+  left (HHFree f) = HHFree $ \k -> left (f k)
+  right (HHFree f) = HHFree $ \k -> right (f k)
+  HHFree f +++ HHFree g = HHFree $ \k -> f k +++ g k
+  HHFree f ||| HHFree g = HHFree $ \k -> f k ||| g k
 
-instance SuperClass1 ArrowApply c => ArrowApply (HHFree c f) where
-  app = HHFree $ h scls1
-    where
-      h :: c g => (c g :- ArrowApply g) -> (f :~~> g) -> g (HHFree c f a b, a) b
-      h (Sub Dict) k = app . arr (first (rightAdjunct k))
+instance (forall x. c x => ArrowApply x) => ArrowApply (HHFree c f) where
+  app = HHFree $ \k -> app . arr (first (rightAdjunct k))
 
-instance SuperClass1 ArrowLoop c => ArrowLoop (HHFree c f) where
-  loop (HHFree f) = HHFree $ \k -> h scls1 (f k)
-    where
-      h :: c g => (c g :- ArrowLoop g) -> g (b, d) (a, d) -> g b a
-      h (Sub Dict) = loop
+instance (forall x. c x => ArrowLoop x) => ArrowLoop (HHFree c f) where
+  loop (HHFree f) = HHFree $ \k -> loop (f k)
 
-instance SuperClass1 Bifunctor c => Bifunctor (HHFree c f) where
-  bimap p q (HHFree g) = HHFree $ \k -> h scls1 p q (g k)
-    where
-      h :: c g => (c g :- Bifunctor g) -> (a -> b) -> (e -> d) -> g a e -> g b d
-      h (Sub Dict) = bimap
+instance (forall x. c x => Bifunctor x) => Bifunctor (HHFree c f) where
+  first f (HHFree g) = HHFree $ \k -> B.first f (g k)
+  second f (HHFree g) = HHFree $ \k -> B.second f (g k)
+  bimap p q (HHFree g) = HHFree $ \k -> B.bimap p q (g k)
 
-instance SuperClass1 Biapplicative c => Biapplicative (HHFree c f) where
-  bipure a b = HHFree $ const (h scls1 a b)
-    where
-      h :: c g => (c g :- Biapplicative g) -> a -> b -> g a b
-      h (Sub Dict) = bipure
-  HHFree f <<*>> HHFree g = HHFree $ \k -> h scls1 (f k) (g k)
-    where
-      h :: c g => (c g :- Biapplicative g) -> g (a -> d) (b -> e) -> g a b -> g d e
-      h (Sub Dict) = (<<*>>)
+instance (forall x. c x => Biapplicative x) => Biapplicative (HHFree c f) where
+  bipure a b = HHFree $ const (bipure a b)
+  HHFree f <<*>> HHFree g = HHFree $ \k -> f k <<*>> g k
+  HHFree f *>> HHFree g = HHFree $ \k -> f k *>> g k
+  HHFree f <<* HHFree g = HHFree $ \k -> f k <<* g k
+  biliftA2 p q (HHFree g) (HHFree h) = HHFree $ \k -> biliftA2 p q (g k) (h k)
 
-instance SuperClass1 Profunctor c => Profunctor (HHFree c f) where
-  dimap p q (HHFree g) = HHFree $ \k -> h scls1 p q (g k)
-    where
-      h :: c g => (c g :- Profunctor g) -> (b -> a) -> (e -> d) -> g a e -> g b d
-      h (Sub Dict) = dimap
+instance (forall x. c x => Profunctor x) => Profunctor (HHFree c f) where
+  lmap f (HHFree g) = HHFree $ \k -> lmap f (g k)
+  rmap f (HHFree g) = HHFree $ \k -> rmap f (g k)
+  f #. HHFree g = HHFree $ \k -> f #. g k
+  HHFree g .# f = HHFree $ \k -> g k .# f
+  dimap p q (HHFree g) = HHFree $ \k -> dimap p q (g k)
 
-instance SuperClass1 Strong c => Strong (HHFree c f) where
-  first' (HHFree f) = HHFree $ \k -> h scls1 (f k)
-    where
-      h :: c g => (c g :- Strong g) -> g a b -> g (a, d) (b, d)
-      h (Sub Dict) = first'
+instance (forall x. c x => Strong x) => Strong (HHFree c f) where
+  first' (HHFree f) = HHFree $ \k -> first' (f k)
+  second' (HHFree f) = HHFree $ \k -> second' (f k)
 
-instance SuperClass1 Choice c => Choice (HHFree c f) where
-  left' (HHFree f) = HHFree $ \k -> h scls1 (f k)
-    where
-      h :: c g => (c g :- Choice g) -> g a b -> g (Either a d) (Either b d)
-      h (Sub Dict) = left'
+instance (forall x. c x => Choice x) => Choice (HHFree c f) where
+  left' (HHFree f) = HHFree $ \k -> left' (f k)
+  right' (HHFree f) = HHFree $ \k -> right' (f k)
 
-instance SuperClass1 Closed c => Closed (HHFree c f) where
-  closed (HHFree f) = HHFree $ \k -> h scls1 (f k)
-    where
-      h :: c g => (c g :- Closed g) -> g a b -> g (d -> a) (d -> b)
-      h (Sub Dict) = closed
+instance (forall x. c x => Closed x) => Closed (HHFree c f) where
+  closed (HHFree f) = HHFree $ \k -> closed (f k)