diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,5 +1,18 @@
 CHANGELOG
 
+0.6.5 -> 0.7
+  - Allow contravariant uses of HFree
+  - Added HHFree for free profunctors/categories/arrows
+  - Updated to base-4.9
+  - Updated to template-haskell-2.11
+  - Updated to comonad-5
+  - Updated to constraints-0.9
+  - Updated to algebraic-classes-0.7
+
+0.6.4.1 -> 0.6.5
+  - Updated to transformers-0.5.0.0
+  - Updated to constraints-0.6
+
 0.6.4 -> 0.6.4.1
   - Raise lower bounds of template-haskell
 
diff --git a/examples/Automaton.hs b/examples/Automaton.hs
--- a/examples/Automaton.hs
+++ b/examples/Automaton.hs
@@ -46,5 +46,8 @@
 tailS :: Stream a -> Stream a
 tailS = act ()
 
+zipWithS :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
+zipWithS f as bs = f <$> as <*> bs
+
 fromStream :: Stream a -> [a]
 fromStream = map headS . iterate tailS
diff --git a/examples/NonEmptyList.hs b/examples/NonEmptyList.hs
--- a/examples/NonEmptyList.hs
+++ b/examples/NonEmptyList.hs
@@ -1,15 +1,12 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, UndecidableInstances #-}
 module NonEmptyList where
 
 import Data.Functor.Free
 
-import Control.Applicative
 import Control.Comonad
-import Data.Functor.Identity
-import Data.Functor.Compose
 
 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
@@ -18,21 +15,15 @@
 deriveInstances ''Semigroup
 
 -- The next two instances make NonEmptyList a Comonad.
-instance Semigroup (Identity a) where
+instance Semigroup (Extract a) where
   a <> _ = a
 
-instance Semigroup (Compose NonEmptyList NonEmptyList a) where
-  Compose l <> Compose r = Compose $ ((<> extract r) <$> l) <> r
-
+instance Semigroup (Duplicate NonEmptyList a) where
+  Duplicate l <> Duplicate r = Duplicate $ ((<> extract r) <$> l) <> r
 
-  
 fromList :: [a] -> NonEmptyList a
-fromList = foldr1 (<>) . map return
-
-toList :: NonEmptyList a -> [a]
-toList = convert
-
+fromList = foldr1 (<>) . map pure
 
--- Test the comonad instance, returns [10,9,7,4].
+-- Test the comonad and foldable instances, returns [10,9,7,4].
 test :: NonEmptyList Int
-test = extend (sum . toList) $ (pure 1 <> pure 2) <> (pure 3 <> pure 4)
+test = extend sum $ (pure 1 <> pure 2) <> (pure 3 <> (pure 4 <> pure 5))
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.6.5
+version:             0.7
 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
@@ -32,22 +32,26 @@
     src
 
   exposed-modules:
+    Data.Constraint.Class1,
     Data.Functor.Cofree,
     Data.Functor.Free,
     Data.Functor.HCofree,
-    Data.Functor.HFree
+    Data.Functor.HFree,
+    Data.Functor.HHFree
 
   default-language:
     Haskell2010
 
   build-depends:
-    base == 4.8.*,
-    template-haskell == 2.10.0.*,
-    constraints >= 0.6 && < 0.7,
-    transformers >= 0.2.0.0 && < 0.6,
-    comonad >= 4.0 && < 4.3,
-    void >= 0.4 && < 0.8,
-    algebraic-classes == 0.6.*
+    base == 4.9.*,
+    template-haskell == 2.11.*,
+    constraints == 0.9.*,
+    transformers == 0.5.*,
+    comonad == 5.*,
+    algebraic-classes == 0.7.*,
+    contravariant == 1.4.*,
+    bifunctors == 5.*,
+    profunctors == 5.*
 
 
 source-repository head
diff --git a/src/Data/Constraint/Class1.hs b/src/Data/Constraint/Class1.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Class1.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE
+    PolyKinds
+  , RankNTypes
+  , TypeOperators
+  , FlexibleInstances
+  , ScopedTypeVariables
+  , UndecidableInstances
+  , MultiParamTypeClasses
+  , FunctionalDependencies
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Constraint.Class1
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Constraint.Class1 (Class1(..), SuperClass1(..)) where
+
+import Data.Constraint
+
+import Control.Applicative
+import Control.Arrow
+import Control.Category
+import Control.Comonad
+import Data.Biapplicative
+import Data.Functor.Contravariant
+import Data.Functor.Contravariant.Divisible
+
+class Class1 b h | h -> b where
+  cls1 :: h x :- b x
+
+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
+
+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
+
+instance Class1 Bifunctor Biapplicative where cls1 = Sub Dict
+
+-- | Automatically find superclasses by searching the `Class1` instances
+class SuperClass1 b h where
+  scls1 :: h x :- b x
+
+instance {-# OVERLAPPING #-} SuperClass1 b b where
+  scls1 = refl
+
+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)
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,7 +1,7 @@
 {-# LANGUAGE
     ConstraintKinds
   , RankNTypes
-  , TypeOperators  
+  , TypeOperators
   , FlexibleInstances
   , GADTs
   , MultiParamTypeClasses
@@ -21,10 +21,9 @@
 -- In this package the forgetful functor forgets class constraints.
 -----------------------------------------------------------------------------
 module Data.Functor.Cofree where
-  
+
 import Control.Monad
 import Control.Comonad
-import Control.Applicative
 
 import Data.Constraint
 import Data.Constraint.Forall
@@ -37,6 +36,7 @@
 data Cofree c b where
   Cofree :: c a => (a -> b) -> a -> Cofree c b
 
+
 counit :: Cofree c b -> b
 counit (Cofree k a) = k a
 
@@ -63,16 +63,16 @@
 instance Functor (Cofree c) where
   fmap f (Cofree k a) = Cofree (f . k) a
 
-instance ForallF c (Cofree c) => Comonad (Cofree c) where
+instance Comonad (Cofree c) where
   extract = counit
-  extend = leftAdjunctF
+  duplicate (Cofree k a) = Cofree (leftAdjunct k) a
 
-instance (ForallF c Identity, ForallF c (Cofree c), ForallF c (Compose (Cofree c) (Cofree c)))
+instance (ForallF c Identity, ForallF c (Compose (Cofree c) (Cofree c)))
   => Applicative (Cofree c) where
   pure = leftAdjunctF runIdentity . Identity
   (<*>) = ap
 
-instance (ForallF c Identity, ForallF c (Cofree c), ForallF c (Compose (Cofree c) (Cofree c)))
+instance (ForallF c Identity, ForallF c (Compose (Cofree c) (Cofree c)))
   => Monad (Cofree c) where
   return = pure
   m >>= g = leftAdjunctF (extract . extract . getCompose) (Compose $ fmap g m)
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
@@ -39,6 +39,8 @@
   , unfold
   , convert
   , convertClosed
+  , Extract(..)
+  , Duplicate(..)
 
   -- * Coproducts
   , Coproduct
@@ -50,15 +52,12 @@
 
   ) where
 
-import Control.Applicative
 import Control.Comonad
 import Data.Function
 
 import Data.Constraint hiding (Class)
 import Data.Constraint.Forall
 
-import Data.Functor.Identity
-import Data.Functor.Compose
 import Data.Foldable (Foldable(..))
 import Data.Traversable
 import Data.Void
@@ -141,10 +140,12 @@
   return = unit
   as >>= f = transform (\k -> rightAdjunct k . f) as
 
-instance (ForallF c Identity, ForallF c (Compose (Free c) (Free c)))
+newtype Extract a = Extract { getExtract :: a }
+newtype Duplicate f a = Duplicate { getDuplicate :: f (f a) }
+instance (ForallF c Extract, ForallF c (Duplicate (Free c)))
   => Comonad (Free c) where
-  extract = runIdentity . rightAdjunctF Identity
-  duplicate = getCompose . rightAdjunctF (Compose . unit . unit)
+  extract = getExtract . rightAdjunctF Extract
+  duplicate = getDuplicate . rightAdjunctF (Duplicate . unit . unit)
 
 instance c ~ Class f => Algebra f (Free c a) where
   algebra fa = Free $ \k -> evaluate (fmap (rightAdjunct k) fa)
@@ -221,4 +222,4 @@
   showsPrec p (ShowRec f) = showsPrec p f
 
 instance (Show a, Show (Signature c (ShowHelper (Signature c) a)), c (ShowHelper (Signature c) a)) => Show (Free c a) where
-  show = show . rightAdjunct (ShowUnit :: a -> ShowHelper (Signature c) a)
+  showsPrec p = showsPrec p . rightAdjunct (ShowUnit :: a -> ShowHelper (Signature c) a)
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
@@ -1,9 +1,11 @@
 {-# LANGUAGE
-    ConstraintKinds
+    GADTs
   , RankNTypes
-  , TypeOperators  
+  , TypeOperators
+  , ConstraintKinds
+  , FlexibleContexts
   , FlexibleInstances
-  , GADTs
+  , ScopedTypeVariables
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -25,61 +27,81 @@
 
 import Control.Comonad
 import Control.Comonad.Trans.Class
-import Data.Foldable
-import Data.Traversable
 import Data.Functor.Identity
+import Data.Constraint
+import Data.Constraint.Class1
 
 -- | Natural transformations.
 type f :~> g = forall b. f b -> g b
 
 -- | The higher order cofree functor for constraint @c@.
 data HCofree c g a where
-  HCofree :: (c f, Functor f) => (f :~> g) -> f a -> HCofree c g a
+  HCofree :: c f => (f :~> g) -> f a -> HCofree c g a
 
-instance Functor (HCofree c g) where
-  fmap f (HCofree k a) = HCofree k (fmap f a)
 
 counit :: HCofree c g :~> g
 counit (HCofree k fa) = k fa
 
-leftAdjunct :: (c f, Functor f) => (f :~> g) -> f :~> HCofree c g
+leftAdjunct :: c f => (f :~> g) -> f :~> HCofree c g
 leftAdjunct k fa = HCofree k fa
 
 -- | @unit = leftAdjunct id@
-unit :: (c g, Functor g) => g :~> HCofree c g
+unit :: c g => g :~> HCofree c g
 unit = leftAdjunct id
 
 -- | @rightAdjunct f = counit . f@
 rightAdjunct :: (f :~> HCofree c g) -> f :~> g
 rightAdjunct f = counit . f
 
+transform :: (forall r. c r => (r :~> f) -> r :~> g) -> HCofree c f :~> HCofree c g
+transform t (HCofree k a) = HCofree (t k) a
+
 hfmap :: (f :~> g) -> HCofree c f :~> HCofree c g
-hfmap f (HCofree k a) = HCofree (f . k) a
+hfmap f = transform (\k -> f . k)
 
-liftCofree :: (c f, Functor f) => f a -> HCofree c f a
+hextend :: (HCofree c f :~> g) -> HCofree c f :~> HCofree c g
+hextend f = transform (\k -> f . leftAdjunct k)
+
+liftCofree :: c f => f a -> HCofree c f a
 liftCofree = leftAdjunct id
 
 lowerCofree :: HCofree c f a -> f a
 lowerCofree = counit
 
-convert :: (c (t f), Functor (t f), Comonad f, ComonadTrans t) => t f a -> HCofree c f a
+convert :: (c (t f), Comonad f, ComonadTrans t) => t f a -> HCofree c f a
 convert = leftAdjunct lower
 
 coiter :: c Identity => (forall b. b -> f b) -> a -> HCofree c f a
 coiter f = leftAdjunct (f . runIdentity) . Identity
 
-instance Foldable (HCofree Foldable g) where
-  foldMap f (HCofree _ a) = foldMap f a
-instance Foldable (HCofree Traversable g) where
-  foldMap f (HCofree _ a) = foldMap f a
-instance Traversable (HCofree Traversable g) where
-  traverse f (HCofree k a) = HCofree k <$> traverse f a
-
--- | The cofree comonad of a functor.
-instance Comonad (HCofree Comonad 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
-
 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 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 (SuperClass1 Functor c, SuperClass1 Foldable c, 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
+  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
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
@@ -1,8 +1,9 @@
 {-# LANGUAGE
-    ConstraintKinds
-  , RankNTypes
+    RankNTypes
   , TypeOperators
-  , FlexibleInstances
+  , ConstraintKinds
+  , FlexibleContexts
+  , ScopedTypeVariables
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -21,74 +22,122 @@
 -- transformations between them.
 -----------------------------------------------------------------------------
 module Data.Functor.HFree where
-  
+
 import Control.Applicative
-import Control.Monad
 import Control.Monad.Trans.Class
 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
 
 -- | The higher order free functor for constraint @c@.
-newtype HFree c f a = HFree { runHFree :: forall g. (c g, Functor g) => (f :~> g) -> g a }
+newtype HFree c f a = HFree { runHFree :: forall g. c g => (f :~> g) -> g a }
 
 unit :: f :~> HFree c f
 unit fa = HFree $ \k -> k fa
 
-rightAdjunct :: (c g, Functor g) => (f :~> g) -> HFree c f :~> g
+rightAdjunct :: c g => (f :~> g) -> HFree c f :~> g
 rightAdjunct f h = runHFree h f
 
 -- | @counit = rightAdjunct id@
-counit :: (c f, Functor f) => HFree c f :~> f
+counit :: c f => HFree c f :~> f
 counit = rightAdjunct id
 
 -- | @leftAdjunct f = f . unit@
 leftAdjunct :: (HFree c f :~> g) -> f :~> g
 leftAdjunct f = f . unit
 
-instance Functor (HFree c f) where
-  fmap f (HFree g) = HFree (fmap f . g)
+transform :: (forall r. c r => (g :~> r) -> f :~> r) -> HFree c f :~> HFree c g
+transform t h = HFree $ \k -> rightAdjunct (t k) h
+-- transform t = HFree . (. t) . runHFree
 
 hfmap :: (f :~> g) -> HFree c f :~> HFree c g
-hfmap f (HFree g) = HFree $ \k -> g (k . f)
+hfmap f = transform (\k -> k . f)
 
+bind :: (f :~> HFree c g) -> HFree c f :~> HFree c g
+bind f = transform (\k -> rightAdjunct k . f)
+
 liftFree :: f a -> HFree c f a
 liftFree = unit
 
-lowerFree :: (c f, Functor f) => HFree c f a -> f a
+lowerFree :: c f => HFree c f a -> f a
 lowerFree = counit
 
-convert :: (c (t f), Functor (t f), Monad f, MonadTrans t) => HFree c f a -> t f a
+convert :: (c (t f), Monad f, MonadTrans t) => HFree c f a -> t f a
 convert = rightAdjunct lift
 
 iter :: c Identity => (forall b. f b -> b) -> HFree c f a -> a
 iter f = runIdentity . rightAdjunct (Identity . f)
 
-instance Applicative (HFree Monad f) where
-  pure = return
-  (<*>) = ap
-  
+wrap :: f (HFree Monad f a) -> HFree Monad f a
+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 (SuperClass1 Functor c, 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 (SuperClass1 Functor c, SuperClass1 Applicative c, 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) = (<|>)
+
 -- | The free monad of a functor.
-instance Monad (HFree Monad f) where
-  return a = HFree $ const (return a)
-  HFree f >>= g = HFree $ \k -> f k >>= (rightAdjunct k . g)
+instance (SuperClass1 Functor c, SuperClass1 Applicative c, SuperClass1 Monad c) => 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 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 MonadTrans (HFree Monad) where
---   lift = liftFree
-  
-instance Applicative (HFree Applicative f) where
-  pure a = HFree $ const (pure a)
-  HFree f <*> HFree g = HFree $ \k -> f k <*> g k
 
-instance Applicative (HFree Alternative f) where
-  pure a = HFree $ const (pure a)
-  HFree f <*> HFree g = HFree $ \k -> f k <*> g k
-instance Alternative (HFree Alternative f) where
-  empty = HFree $ const empty
-  HFree f <|> HFree g = HFree $ \k -> f k <|> g k
-  
-wrap :: f (HFree Monad f a) -> HFree Monad f a
-wrap = join . unit
+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 (SuperClass1 Contravariant c, 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 (SuperClass1 Contravariant c, SuperClass1 Divisible c, 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
diff --git a/src/Data/Functor/HHFree.hs b/src/Data/Functor/HHFree.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/HHFree.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE
+    RankNTypes
+  , TypeOperators
+  , ConstraintKinds
+  , FlexibleContexts
+  , ScopedTypeVariables
+  , UndecidableInstances
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Functor.HHFree
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- A free functor is left adjoint to a forgetful functor.
+-- In this package the forgetful functor forgets class constraints.
+--
+-- Compared to @Data.Functor.HHFree@ we have 2 two parameters.
+-----------------------------------------------------------------------------
+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.Functor
+import Data.Biapplicative (Biapplicative(bipure, (<<*>>)))
+import Data.Profunctor
+import Data.Profunctor.Monad
+
+
+-- | Natural transformations.
+type f :~~> g = forall a b. f a b -> g a b
+
+-- | The higher order free functor over two type parameters for constraint @c@.
+newtype HHFree c f a b = HHFree { runHHFree :: forall g. c g => (f :~~> g) -> g a b }
+
+unit :: f :~~> HHFree c f
+unit fa = HHFree $ \k -> k fa
+
+rightAdjunct :: c g => (f :~~> g) -> HHFree c f :~~> g
+rightAdjunct f h = runHHFree h f
+
+-- | @counit = rightAdjunct id@
+counit :: c f => HHFree c f :~~> f
+counit = rightAdjunct id
+
+-- | @leftAdjunct f = f . unit@
+leftAdjunct :: (HHFree c f :~~> g) -> f :~~> g
+leftAdjunct f = f . unit
+
+transform :: (forall r. c r => (g :~~> r) -> f :~~> r) -> HHFree c f :~~> HHFree c g
+transform t h = HHFree $ \k -> rightAdjunct (t k) h
+-- transform t = HHFree . (. t) . runHHFree
+
+hfmap :: (f :~~> g) -> HHFree c f :~~> HHFree c g
+hfmap f = transform (\k -> k . f)
+
+bind :: (f :~~> HHFree c g) -> HHFree c f :~~> HHFree c g
+bind f = transform (\k -> rightAdjunct k . f)
+
+instance BifunctorFunctor (HHFree c) where
+  bifmap = hfmap
+
+instance BifunctorMonad (HHFree c) where
+  bireturn = unit
+  bibind = bind
+
+instance ProfunctorFunctor (HHFree c) where
+  promap = hfmap
+
+instance ProfunctorMonad (HHFree c) where
+  proreturn = unit
+  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 (SuperClass1 Category c, 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 (SuperClass1 Category c, SuperClass1 Arrow c, 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
+  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
+  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
+  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
+  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 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 (SuperClass1 Bifunctor c, 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 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 (SuperClass1 Profunctor c, 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
+  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
+  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