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.7
+version:             0.7.1
 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
diff --git a/src/Data/Constraint/Class1.hs b/src/Data/Constraint/Class1.hs
--- a/src/Data/Constraint/Class1.hs
+++ b/src/Data/Constraint/Class1.hs
@@ -1,62 +1,160 @@
 {-# LANGUAGE
     PolyKinds
+  , DataKinds
   , RankNTypes
+  , TypeFamilies
   , TypeOperators
+  , ConstraintKinds
+  , FlexibleContexts
+  , DefaultSignatures
   , FlexibleInstances
   , ScopedTypeVariables
   , UndecidableInstances
   , MultiParamTypeClasses
-  , FunctionalDependencies
   #-}
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Constraint.Class1
+-- Module      :  Data.Constraint.HasSuperClasses
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
 -- Stability   :  experimental
 -- Portability :  non-portable
 -----------------------------------------------------------------------------
-module Data.Constraint.Class1 (Class1(..), SuperClass1(..)) where
+module Data.Constraint.Class1 where
 
 import Data.Constraint
+import Data.Proxy
+import Prelude hiding (id, (.))
 
 import Control.Applicative
-import Control.Arrow
+import Control.Arrow (Arrow, ArrowZero, ArrowPlus, ArrowLoop, ArrowApply, ArrowChoice)
 import Control.Category
 import Control.Comonad
 import Data.Biapplicative
 import Data.Functor.Contravariant
 import Data.Functor.Contravariant.Divisible
+import Data.Profunctor
 
-class Class1 b h | h -> b where
-  cls1 :: h x :- b x
+-- | Proof that @b@ is a superclass of @h@, i.e. @h x@ entails @b x@.
+scls1 :: forall b h x. SuperClass1 b h => h x :- b x
+scls1 = containsSelf . isSubset (Proxy :: Proxy x) (Proxy :: Proxy (SuperClasses b)) (Proxy :: Proxy (SuperClasses h)) . superClasses
 
-instance Class1 Functor Applicative where cls1 = Sub Dict
-instance Class1 Applicative Alternative where cls1 = Sub Dict
-instance Class1 Applicative Monad where cls1 = Sub Dict
-instance Class1 Functor Traversable where cls1 = Sub Dict
-instance Class1 Functor Comonad where cls1 = Sub Dict
-instance Class1 Contravariant Divisible where cls1 = Sub Dict
-instance Class1 Divisible Decidable where cls1 = Sub Dict
+type SuperClass1 b h = (HasSuperClasses h, HasSuperClasses b, SuperClasses b `Subset` SuperClasses h, IsSubset (SuperClasses b) (SuperClasses h))
 
-instance Class1 Category Arrow where cls1 = Sub Dict
-instance Class1 Arrow ArrowZero where cls1 = Sub Dict
-instance Class1 ArrowZero ArrowPlus where cls1 = Sub Dict
-instance Class1 Arrow ArrowChoice where cls1 = Sub Dict
-instance Class1 Arrow ArrowApply where cls1 = Sub Dict
-instance Class1 Arrow ArrowLoop where cls1 = Sub Dict
+class HasSuperClasses (c :: k -> Constraint) where
+  type SuperClasses c :: [k -> Constraint]
+  type SuperClasses c = '[c]
+  superClasses :: c x :- FoldConstraints (SuperClasses c) x
+  default superClasses :: c x :- FoldConstraints '[c] x
+  superClasses = Sub Dict
+  containsSelf :: FoldConstraints (SuperClasses c) x :- c x
+  default containsSelf :: FoldConstraints '[c] x :- c x
+  containsSelf = Sub Dict
 
-instance Class1 Bifunctor Biapplicative where cls1 = Sub Dict
+instance HasSuperClasses Functor
+instance HasSuperClasses Applicative where
+  type SuperClasses Applicative = Applicative ': SuperClasses Functor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Alternative where
+  type SuperClasses Alternative = Alternative ': SuperClasses Applicative
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Monad where
+  type SuperClasses Monad = Monad ': SuperClasses Applicative
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Foldable
+instance HasSuperClasses Traversable where
+  type SuperClasses Traversable = Traversable ': SuperClasses Functor ++ SuperClasses Foldable
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Comonad where
+  type SuperClasses Comonad = Comonad ': SuperClasses Functor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
 
--- | Automatically find superclasses by searching the `Class1` instances
-class SuperClass1 b h where
-  scls1 :: h x :- b x
+instance HasSuperClasses Contravariant
+instance HasSuperClasses Divisible where
+  type SuperClasses Divisible = Divisible ': SuperClasses Contravariant
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Decidable where
+  type SuperClasses Decidable = Decidable ': SuperClasses Divisible
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
 
-instance {-# OVERLAPPING #-} SuperClass1 b b where
-  scls1 = refl
+instance HasSuperClasses Category
+instance HasSuperClasses Arrow where
+  type SuperClasses Arrow = Arrow ': SuperClasses Category
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses ArrowZero where
+  type SuperClasses ArrowZero = ArrowZero ': SuperClasses Arrow
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses ArrowPlus where
+  type SuperClasses ArrowPlus = ArrowPlus ': SuperClasses ArrowZero
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses ArrowChoice where
+  type SuperClasses ArrowChoice = ArrowChoice ': SuperClasses Arrow
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses ArrowApply where
+  type SuperClasses ArrowApply = ArrowApply ': SuperClasses Arrow
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses ArrowLoop where
+  type SuperClasses ArrowLoop = ArrowLoop ': SuperClasses Arrow
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
 
-instance {-# OVERLAPPABLE #-} (SuperClass1 b c, Class1 c h) => SuperClass1 b h where
-  scls1 = h where
-    h :: forall x. h x :- b x
-    h = trans (scls1 :: c x :- b x) (cls1 :: h x :- c x)
+instance HasSuperClasses Bifunctor
+instance HasSuperClasses Biapplicative where
+  type SuperClasses Biapplicative = Biapplicative ': SuperClasses Bifunctor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+
+instance HasSuperClasses Profunctor
+instance HasSuperClasses Strong where
+  type SuperClasses Strong = Strong ': SuperClasses Profunctor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Choice where
+  type SuperClasses Choice = Choice ': SuperClasses Profunctor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+instance HasSuperClasses Closed where
+  type SuperClasses Closed = Closed ': SuperClasses Profunctor
+  superClasses = Sub Dict
+  containsSelf = Sub Dict
+
+
+type family (++) (as :: [k]) (bs :: [k]) :: [k] where
+  (++) a '[] = a
+  (++) '[] b = b
+  (++) (a ': as) bs = a ': (as ++ bs)
+
+type family FoldConstraints (cs :: [k -> Constraint]) (x :: k) :: Constraint
+type instance FoldConstraints '[] x = ()
+type instance FoldConstraints (c ': cs) x = (c x, FoldConstraints cs x)
+
+class Elem (c :: k -> Constraint) (cs :: [k -> Constraint]) where
+  isElem :: Proxy cs -> FoldConstraints cs x :- c x
+instance {-# OVERLAPPING #-} Elem c (c ': cs) where
+  isElem _ = weaken1
+instance {-# OVERLAPPABLE #-} Elem b cs => Elem b (c ': cs) where
+  isElem _ = isElem (Proxy :: Proxy cs) . weaken2
+
+class IsSubset as bs where
+  isSubset :: as `Subset` bs => Proxy x -> Proxy as -> Proxy bs -> FoldConstraints bs x :- FoldConstraints as x
+instance IsSubset '[] bs where
+  isSubset _ _ _ = top
+instance IsSubset as bs => IsSubset (a ': as) bs where
+  isSubset px _ pbs = isElem pbs &&& isSubset px (Proxy :: Proxy as) pbs
+
+type family Subset (xs :: [k]) (ys :: [k]) :: Constraint
+type instance Subset '[] bs = ()
+type instance Subset (a ': as) bs = (Elem a bs, Subset as bs)
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
@@ -6,6 +6,7 @@
   , FlexibleContexts
   , FlexibleInstances
   , ScopedTypeVariables
+  , UndecidableInstances
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -89,14 +90,14 @@
       h :: (c f, Monoid m) => (c f :- Foldable f) -> (a -> m) -> f a -> m
       h (Sub Dict) = foldMap
 
-instance (SuperClass1 Functor c, SuperClass1 Foldable c, SuperClass1 Traversable c) => Traversable (HCofree c g) where
+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
 
 -- | The cofree comonad of a functor.
-instance (SuperClass1 Functor c, SuperClass1 Comonad c) => Comonad (HCofree c g) where
+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
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
@@ -4,6 +4,7 @@
   , ConstraintKinds
   , FlexibleContexts
   , ScopedTypeVariables
+  , UndecidableInstances
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -85,7 +86,7 @@
       h :: c g => (c g :- Functor g) -> (a -> b) -> g a -> g b
       h (Sub Dict) = fmap
 
-instance (SuperClass1 Functor c, SuperClass1 Applicative c) => Applicative (HFree c f) where
+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
@@ -95,7 +96,7 @@
       h :: c g => (c g :- Applicative g) -> g (a -> b) -> g a -> g b
       h (Sub Dict) = (<*>)
 
-instance (SuperClass1 Functor c, SuperClass1 Applicative c, SuperClass1 Alternative c) => Alternative (HFree c f) where
+instance SuperClass1 Alternative c => Alternative (HFree c f) where
   empty = HFree $ const (h scls1)
     where
       h :: c g => (c g :- Alternative g) -> g a
@@ -106,7 +107,7 @@
       h (Sub Dict) = (<|>)
 
 -- | The free monad of a functor.
-instance (SuperClass1 Functor c, SuperClass1 Applicative c, SuperClass1 Monad c) => Monad (HFree c f) where
+instance SuperClass1 Monad c => Monad (HFree c f) where
   return = pure
   HFree f >>= g = HFree $ \k -> h scls1 (f k) (rightAdjunct k . g)
     where
@@ -122,7 +123,7 @@
       h :: c g => (c g :- Contravariant g) -> (b -> a) -> g a -> g b
       h (Sub Dict) = contramap
 
-instance (SuperClass1 Contravariant c, SuperClass1 Divisible c) => Divisible (HFree c f) where
+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
@@ -132,7 +133,7 @@
       h :: c g => (c g :- Divisible g) -> g a
       h (Sub Dict) = conquer
 
-instance (SuperClass1 Contravariant c, SuperClass1 Divisible c, SuperClass1 Decidable c) => Decidable (HFree c f) where
+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
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
@@ -90,7 +90,7 @@
       h :: c g => (c g :- Category g) -> g b d -> g a b -> g a d
       h (Sub Dict) = (.)
 
-instance (SuperClass1 Category c, SuperClass1 Arrow c) => Arrow (HHFree c f) where
+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
@@ -100,31 +100,31 @@
       h :: c g => (c g :- Arrow g) -> g a b -> g d e -> g (a, d) (b, e)
       h (Sub Dict) = (***)
 
-instance (SuperClass1 Category c, SuperClass1 Arrow c, SuperClass1 ArrowZero c) => ArrowZero (HHFree c f) where
+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 (SuperClass1 Category c, SuperClass1 Arrow c, SuperClass1 ArrowZero c, SuperClass1 ArrowPlus c) => ArrowPlus (HHFree c f) where
+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 (SuperClass1 Category c, SuperClass1 Arrow c, SuperClass1 ArrowChoice c) => ArrowChoice (HHFree c f) where
+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 (SuperClass1 Category c, SuperClass1 Arrow c, SuperClass1 ArrowApply c) => ArrowApply (HHFree c f) where
+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 (SuperClass1 Category c, SuperClass1 Arrow c, SuperClass1 ArrowLoop c) => ArrowLoop (HHFree c f) where
+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
@@ -136,7 +136,7 @@
       h :: c g => (c g :- Bifunctor g) -> (a -> b) -> (e -> d) -> g a e -> g b d
       h (Sub Dict) = bimap
 
-instance (SuperClass1 Bifunctor c, SuperClass1 Biapplicative c) => Biapplicative (HHFree c f) where
+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
@@ -152,19 +152,19 @@
       h :: c g => (c g :- Profunctor g) -> (b -> a) -> (e -> d) -> g a e -> g b d
       h (Sub Dict) = dimap
 
-instance (SuperClass1 Profunctor c, SuperClass1 Strong c) => Strong (HHFree c f) where
+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 (SuperClass1 Profunctor c, SuperClass1 Choice c) => Choice (HHFree c f) where
+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 (SuperClass1 Profunctor c, SuperClass1 Closed c) => Closed (HHFree c f) where
+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)