diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,19 @@
 # Changelog for free-algebras
 
+## Version 0.0.8.0
+- Added two properties for each: `foldMapFree`, `foldNatFree` and
+  `foldNatFree2`.
+- Added default implementations of `codom` / `forget`, `codom1` / `forget` and
+  `codom2` / `forget2`, what simplifies writting instances.
+- Changed internal representation of FreeAbelianSemigroup: use Natural
+- removed `natural-number` dependency and use `Numeric.Natural.Natural` instead.
+- Applicative instance for `FreeMAction`.
+- Added `Free1` type.
+- Removed `constraints` dependency.
+- Renamed `Data.Semigroup.SemiLattice` to `Data.Semigroup.Semilattice`, also
+  `FreeSemiLattice` renamed to `FreeSemilattice`.
+- various optimisation (rewrite rules & inline pragmas)
+
 ## Version 0.0.7.2
 - Enhanced documentation, and properly attributed fix in ChangeLog.
 
@@ -46,5 +60,3 @@
 
 ## Version 0.0.2.0
 - Simplified `Proof` type.
-
-## Unreleased changes
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,8 +4,14 @@
 
 Universal algebra approach (which is compatible with categorical approach) to
 free algebras (including higher order structures like functors, applicative
-functors or monads).  Mathematical introduction alongside with some Haskell
-ideas can be found
-[here](https://marcinszamotulski.me/posts/free-monads.html).
+functors or monads).  Mathematical introduction alongside with some of the
+Haskell ideas is exposed in this [blog](https://coot.me/posts/free-monads.html)
+post.
 
-For an example check out [this](https://github.com/coot/free-algebras/blob/master/examples/src/Network/TCP.hs).
+Examples:
+---------
+
+* [TCP as a free monad](https://github.com/coot/free-algebras/blob/master/examples/src/Network/TCP.hs)
+* [free categories](https://coot.me/posts/kleisli-categories-and-free-monads.html)
+* [free categories with monadic effects](https://coot.me/posts/categories-with-monadic-effects.html)
+* [free category package](https://hackage.haskell.org/package/free-category)
diff --git a/free-algebras.cabal b/free-algebras.cabal
--- a/free-algebras.cabal
+++ b/free-algebras.cabal
@@ -1,7 +1,9 @@
 name:           free-algebras
-version:        0.0.7.2
+version:        0.0.8.0
 synopsis:       Free algebras in Haskell.
-description:    Universal algebra approach to free algebras including higher kinded algebraic structures like functors, applicative functors or monads.
+description:    Universal algebra approach to free algebras including higher
+                kinded algebraic structures like functors, applicative
+                functors, monads or categories .
 category:       Algebra, Control, Monads
 homepage:       https://github.com/coot/free-algebras#readme
 bug-reports:    https://github.com/coot/free-algebras/issues
@@ -15,7 +17,7 @@
 extra-source-files:
     ChangeLog.md
     README.md
-tested-with:    GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.3
+tested-with:    GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.3, GHC==8.8.1
 
 source-repository head
   type: git
@@ -31,14 +33,11 @@
       Data.Group.Free
       Data.Monoid.Abelian
       Data.Semigroup.Abelian
-      Data.Semigroup.SemiLattice
-  other-modules:
-      Paths_free_algebras
+      Data.Semigroup.Semilattice
   hs-source-dirs:
       src
   build-depends:
       base            >= 4.9 && <5
-    , constraints     >= 0.8 && <0.11.0 
     , containers      >= 0.4.2 && <0.7
     , data-fix                  <0.3
     , dlist           >= 0.8 && <0.9
@@ -46,7 +45,6 @@
     , groups          >= 0.3 && <0.5
     , kan-extensions  >= 4.1 && <6.0
     , mtl             >= 2.2 && <2.3
-    , natural-numbers >= 0.1 && <0.2
     , transformers    >= 0.5 && <0.6
   ghc-options:
     -Wall
@@ -56,50 +54,39 @@
     -Wno-deprecations
   default-language: Haskell2010
 
-test-suite free-algebras-test
+test-suite test-free-algebras
   type: exitcode-stdio-1.0
   main-is: Main.hs
   other-modules:
+      Control.Algebra.Free
+      Control.Algebra.Free2
+      Control.Monad.Action
+      Data.Algebra.Free
+      Data.Algebra.Pointed
+      Data.Group.Free
+      Data.Monoid.Abelian
+      Data.Semigroup.Abelian
+      Data.Semigroup.Semilattice
       Test.Control.Algebra.Free
       Test.Data.Algebra.Free
       Test.Data.Group.Free
-      Paths_free_algebras
   hs-source-dirs:
       test
-  default-extensions:
-      ConstraintKinds
-      DataKinds
-      DeriveFunctor
-      EmptyDataDecls
-      FlexibleInstances
-      FlexibleContexts
-      KindSignatures
-      InstanceSigs
-      MultiParamTypeClasses
-      OverloadedStrings
-      PolyKinds
-      RankNTypes
-      ScopedTypeVariables
-      TupleSections
-      TypeApplications
-      TypeFamilies
+      src
   ghc-options:
       -threaded
       -rtsopts
       -with-rtsopts=-N
       -Wall
   build-depends:
-      base            >= 4.9 && < 5
-    , constraints
+      base           >= 4.9 && < 5
     , containers
     , data-fix
     , dlist
     , free
-    , free-algebras
     , groups
-    , hedgehog
+    , hedgehog       >= 0.6 && < 1.1
     , kan-extensions
     , mtl
-    , natural-numbers
     , transformers
   default-language: Haskell2010
diff --git a/src/Control/Algebra/Free.hs b/src/Control/Algebra/Free.hs
--- a/src/Control/Algebra/Free.hs
+++ b/src/Control/Algebra/Free.hs
@@ -1,10 +1,22 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE ConstraintKinds            #-}
+{-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs               #-}
 {-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints      #-}
+{-# LANGUAGE UndecidableInstances       #-}
+#endif
 
 -- 'ListT' transformer is depreciated
 {-# OPTIONS_GHC -Wno-deprecations       #-}
@@ -14,7 +26,6 @@
       FreeAlgebra1 (..)
       -- ** Type level witnesses
     , Proof (..)
-    , proof
       -- ** Higher algebra type \/ constraints
     , AlgebraType0
     , AlgebraType
@@ -33,19 +44,31 @@
     , DayF (..)
     , dayToAp
     , apToDay
+
+      -- * Free construction in continuation passing style
+    , Free1 (..)
       -- * Various classes (higher algebra types)
     , MonadList (..)
     , MonadMaybe (..)
+
     ) where
 
-import           Control.Applicative (Alternative)
+import           Control.Applicative ( Alternative (..)
+#if __GLASGOW_HASKELL__ >= 806
+                                     , liftA2
+#endif
+                                     )
 import           Control.Applicative.Free (Ap)
 import qualified Control.Applicative.Free as Ap
 import qualified Control.Applicative.Free.Fast as Fast
 import qualified Control.Applicative.Free.Final as Final
 import           Control.Alternative.Free (Alt (..))
 import qualified Control.Alternative.Free as Alt
-import           Control.Monad (foldM, join)
+#if __GLASGOW_HASKELL__ >= 806
+import           Control.Monad ( MonadPlus (..), foldM, join)
+#else
+import           Control.Monad (                 foldM, join)
+#endif
 import           Control.Monad.Except (ExceptT (..), MonadError (..))
 import           Control.Monad.Free (Free)
 import qualified Control.Monad.Free as Free
@@ -63,15 +86,17 @@
 import           Control.Monad.Writer.Class (MonadWriter (..))
 import qualified Control.Monad.Writer.Lazy as L (WriterT (..))
 import qualified Control.Monad.Writer.Strict as S (WriterT (..))
-import           Data.Constraint (Dict (..))
-import           Data.Kind (Type)
+#if __GLASGOW_HASKELL__ >= 806
+import           Control.Monad.Zip (MonadZip (..))
+#endif
+import           Data.Kind (Constraint, Type)
 import           Data.Fix (Fix, cataM)
 import           Data.Functor.Coyoneda (Coyoneda (..), liftCoyoneda)
 import           Data.Functor.Day (Day (..))
 import qualified Data.Functor.Day as Day
 import           Data.Functor.Identity (Identity (..))
 
-import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..), proof)
+import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))
 
 -- |
 -- Higher kinded version of @'FreeAlgebra'@.  Instances includes free functors,
@@ -98,10 +123,17 @@
 -- * @MMonad@ via @embed = flip bindFree1@
 -- * @MonadTrans@ via @lift = liftFree@
 class FreeAlgebra1 (m :: (k -> Type) -> k -> Type) where
+
+    {-# MINIMAL liftFree, foldNatFree #-}
+
     -- | Natural transformation that embeds generators into @m@.
     liftFree :: AlgebraType0 m f => f a -> m f a
 
     -- | The freeness property.
+    --
+    -- prop> foldNatFree nat (liftFree m) = nat m
+    -- prop> foldNatFree nat . foldNatFree nat' = foldNatFree (foldNatFree nat . nat')
+    --
     foldNatFree
         :: forall d f a .
            ( AlgebraType  m d
@@ -120,12 +152,20 @@
     -- m f@.
     codom1  :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
 
+    default codom1 :: forall a. AlgebraType m (m a)
+                   => Proof (AlgebraType m (m a)) (m a)
+    codom1 = Proof
+
     -- |
     -- A proof that the forgetful functor from the full subcategory of types of
     -- kind @Type -> Type@ satisfying @'AlgebraType' m f@ constraint to types
     -- satisfying @'AlgebraType0' m f@ is well defined.
     forget1 :: forall f. AlgebraType  m f => Proof (AlgebraType0 m f) (m f)
 
+    default forget1 :: forall a. AlgebraType0 m a
+                    => Proof (AlgebraType0 m a) (m a)
+    forget1 = Proof
+
 -- |
 -- Anything that carries @'FreeAlgebra1'@ constraint is also an instance of
 -- @'Control.Monad.Free.Class.MonadFree'@, but not vice versa. You can use
@@ -146,7 +186,7 @@
     => f (m f a)
     -> m f a
 wrapFree = join . liftFree
-{-# INLINE wrapFree #-}
+{-# INLINABLE wrapFree #-}
 
 -- |
 -- @'FreeAlgebra1' m@ implies that @m f@ is a foldable.
@@ -171,8 +211,8 @@
           => m f a
           -> f a
 foldFree1 = case forget1 :: Proof (AlgebraType0 m f) (m f) of
-    Proof Dict -> foldNatFree id
-{-# INLINE foldFree1 #-}
+    Proof -> foldNatFree id
+{-# INLINABLE foldFree1 #-}
 
 -- |
 -- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@
@@ -217,9 +257,19 @@
            -> m f a
            -> m g a
 hoistFree1 nat = case codom1 :: Proof (AlgebraType m (m g)) (m g) of
-    Proof Dict -> foldNatFree (liftFree . nat)
-{-# INLINE hoistFree1 #-}
+    Proof -> foldNatFree (liftFree . nat)
+{-# INLINABLE [1] hoistFree1 #-}
 
+{-# RULES
+
+"hositFree1/foldNatFree"
+    forall (nat  :: forall (x :: k).  g x -> c x)
+           (nat0 :: forall (x :: k). f x -> g x)
+           (f :: m f a).
+    foldNatFree nat (hoistFree1 nat0 f) = foldNatFree (nat . nat0) f
+
+#-}
+
 -- |
 -- @
 --  'hoistFreeH' . 'hoistFreeH' = 'hoistFreeH'
@@ -240,8 +290,15 @@
         => m f a
         -> n f a
 hoistFreeH = foldNatFree liftFree
-{-# INLINE hoistFreeH #-}
+{-# INLINABLE [1] hoistFreeH #-}
 
+{-# RULES
+
+"hoistFreeH/foldNatFree" forall (nat :: forall (x :: k). f x -> c x)
+                                (f :: AlgebraType m c => m f a).
+                         foldNatFree nat (hoistFreeH f) = foldNatFree nat f
+#-}
+
 -- |
 -- @'joinFree1'@ makes @m@ a monad in some subcatgory of types of kind @Type -> Type@
 -- (usually the endo-functor category of @Hask@).  It is just a specialization
@@ -253,9 +310,9 @@
           => m (m f) a
           -> m f a
 joinFree1 = case codom1 :: Proof (AlgebraType m (m f)) (m f) of
-    Proof Dict -> case forget1 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
-        Proof Dict -> foldFree1
-{-# INLINE joinFree1 #-}
+    Proof -> case forget1 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
+        Proof -> foldFree1
+{-# INLINABLE joinFree1 #-}
 
 -- |
 -- Bind operator for the @'joinFree1'@ monad, this is just @'foldNatFree'@ in
@@ -275,8 +332,8 @@
           -> (forall x . f x -> m g x) -- ^ natural transformation @f ~> m g@
           -> m g a
 bindFree1 mfa nat = case codom1 :: Proof (AlgebraType m (m g)) (m g) of
-    Proof Dict -> foldNatFree nat mfa
-{-# INLINE bindFree1 #-}
+    Proof -> foldNatFree nat mfa
+{-# INLINABLE bindFree1 #-}
 
 assocFree1 :: forall m f a .
               ( FreeAlgebra1 m
@@ -286,11 +343,11 @@
            => m f (m f a)
            -> m (m f) (f a)
 assocFree1 = case forget1 :: Proof (AlgebraType0 m f) (m f) of
-    Proof Dict -> case codom1 :: Proof (AlgebraType m (m f)) (m f) of
-        Proof Dict -> case forget1 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
-            Proof Dict -> case codom1 :: Proof (AlgebraType m (m (m f))) (m (m f)) of
-                Proof Dict -> fmap foldFree1 <$> foldNatFree (hoistFree1 liftFree . liftFree)
-{-# INLINE assocFree1 #-}
+    Proof -> case codom1 :: Proof (AlgebraType m (m f)) (m f) of
+        Proof -> case forget1 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
+            Proof -> case codom1 :: Proof (AlgebraType m (m (m f))) (m (m f)) of
+                Proof -> fmap foldFree1 . foldNatFree (hoistFree1 liftFree . liftFree)
+{-# INLINABLE assocFree1 #-}
 
 -- |
 -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and
@@ -321,7 +378,7 @@
           -> m f a
           -> a
 iterFree1 f = runIdentity . foldNatFree (Identity . f)
-{-# INLINE iterFree1 #-}
+{-# INLINABLE iterFree1 #-}
 
 -- Instances
 
@@ -333,9 +390,6 @@
     liftFree = liftCoyoneda
     foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'Ap'@ are the applicative functors.
 type instance AlgebraType0 Ap g = Functor g
@@ -347,27 +401,18 @@
     liftFree  = Ap.liftAp
     foldNatFree = Ap.runAp
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 Fast.Ap g = Functor g
 type instance AlgebraType  Fast.Ap g = Applicative g
 instance FreeAlgebra1 Fast.Ap where
     liftFree  = Fast.liftAp
     foldNatFree = Fast.runAp
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 Final.Ap g = Functor g
 type instance AlgebraType  Final.Ap g = Applicative g
 instance FreeAlgebra1 Final.Ap where
     liftFree  = Final.liftAp
     foldNatFree = Final.runAp
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- @'Day' f f@ newtype wrapper.  It is isomorphic with @'Ap' f@ for applicative
 -- functors @f@ via @'dayToAp'@ (and @'apToDay'@).
@@ -392,9 +437,6 @@
     foldNatFree nat (DayF day)
         = Day.dap . Day.trans2 nat . Day.trans1 nat $ day
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'Free'@ monad is the class of all monads.
 type instance AlgebraType0 Free f = Functor f
@@ -405,27 +447,18 @@
     liftFree    = Free.liftF
     foldNatFree = Free.foldFree
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 Church.F f = Functor f
 type instance AlgebraType  Church.F m = Monad m
 instance FreeAlgebra1 Church.F where
     liftFree    = Church.liftF
     foldNatFree = Church.foldF
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 Alt f = Functor f
 type instance AlgebraType  Alt m = Alternative m
 instance FreeAlgebra1 Alt where
     liftFree    = Alt.liftAlt
     foldNatFree = Alt.runAlt
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'L.StateT'@ monad is the class of all state
 -- monads.
@@ -448,9 +481,6 @@
         put s
         return a
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'S.StateT'@ monad is the class of all state
 -- monads.
@@ -467,9 +497,6 @@
         put s
         return a
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer
 -- monads.
@@ -481,9 +508,6 @@
     liftFree = lift
     foldNatFree nat (L.WriterT m) = fst <$> nat m
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer
 -- monads.
@@ -496,9 +520,6 @@
     liftFree = lift
     foldNatFree nat (S.WriterT m) = fst <$> nat m
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader
 -- monads.
@@ -513,9 +534,6 @@
     foldNatFree nat (ReaderT g) =
         ask >>= nat . g
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader
 -- monads.
@@ -531,9 +549,6 @@
             Left e  -> throwError e
             Right a -> return a
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 (L.RWST r w s) m = ( Monad m, Monoid w )
 type instance AlgebraType  (L.RWST r w s) m = MonadRWS r w s m
 instance FreeAlgebra1 (L.RWST r w s) where
@@ -546,9 +561,6 @@
         tell w
         return a
 
-    codom1  = proof
-    forget1 = proof
-
 type instance AlgebraType0 (S.RWST r w s) m = ( Monad m, Monoid w )
 type instance AlgebraType  (S.RWST r w s) m = MonadRWS r w s m
 instance FreeAlgebra1 (S.RWST r w s) where
@@ -561,9 +573,6 @@
         tell w
         return a
 
-    codom1  = proof
-    forget1 = proof
-
 -- |
 -- Algebra type for @'ListT'@ monad transformer.
 class Monad m => MonadList m where
@@ -572,7 +581,7 @@
 
 mappend1_ :: MonadList m => a -> a -> m a
 mappend1_ a b = return a `mappend1` return b
-{-# INLINE mappend1_ #-}
+{-# INLINABLE mappend1_ #-}
 
 instance Monad m => MonadList (ListT m) where
     mempty1 = ListT (return [])
@@ -584,13 +593,114 @@
     liftFree = lift
     foldNatFree nat (ListT mas) = do
         as <- nat mas
-        empty <- mempty1
-        a <- foldM (\x y -> x `mappend1_` y) empty as
-        return a
+        empty1 <- mempty1
+        foldM (\x y -> x `mappend1_` y) empty1 as
 
-    codom1  = proof
-    forget1 = proof
+-- |
+-- Free construction for kinds @'Type' -> 'Type'@.  @'Free1' 'Functor'@ is
+-- isomorhpic to @'Coyoneda'@ via @'hoistFreeH'@, and @'Free1' 'Applicative'@
+-- is isomorphic to @'Ap'@ (also via @'hoistFreeH'@).
+--
+-- Note: useful instance are only provided for ghc-8.6 using quantified
+-- constraints.
+newtype Free1 (c :: (Type -> Type) -> Constraint)
+              (f ::  Type -> Type)
+              a
+      = Free1 {
+          runFree1 :: forall g. c g => (forall x. f x -> g x) -> g a
+        }
 
+#if __GLASGOW_HASKELL__ >= 806
+--
+-- instances for @'Free1'@ using quantified constraints
+--
+
+-- |
+-- @'Free1'@ is a functor whenever @c f@ implies @'Functor' f@ .
+--
+instance (forall h. c h => Functor h)
+         => Functor (Free1 c f) where
+
+    fmap :: forall a b. (a -> b) -> Free1 c f a -> Free1 c f b
+    fmap f (Free1 g) = Free1 $ \h -> fmap f (g h)
+
+    a <$ Free1 g = Free1 $ \h -> a <$ g h
+
+-- |
+-- @'Free1'@ is an applicative functor whenever @c f@ implies 
+-- @'Applicative' f@.
+--
+instance (forall h. c h => Applicative h)
+         => Applicative (Free1 c f) where
+
+    pure a = Free1 $ \_ -> pure a
+
+    Free1 f <*> Free1 g = Free1 $ \h -> f h <*> g h
+
+    liftA2 f (Free1 x) (Free1 y) = Free1 $ \h -> liftA2 f (x h) (y h)
+
+    Free1 f *> Free1 g = Free1 $ \h -> f h *> g h
+
+    Free1 f <* Free1 g = Free1 $ \h -> f h <* g h
+
+
+-- |
+-- @'Free1'@ is a monad whenever @c f@ implies 
+-- @'Monad' f@.
+instance (forall h. c h => Monad h)
+         => Monad (Free1 c f) where
+
+    return = pure
+
+    Free1 f >>= k = Free1 $ \h ->
+        f h >>= (\a -> case k a of Free1 l -> l h)
+
+    Free1 f >> Free1 g = Free1 $ \h -> f h >> g h
+
+#if __GLASGOW_HASKELL__ < 808
+    fail s = Free1 $ \_ -> fail s
+#endif
+
+
+instance (forall h. c h => Alternative h)
+         => Alternative (Free1 c f) where
+    empty = Free1 $ \_ -> empty
+
+    Free1 f <|> Free1 g = Free1 $ \h -> f h <|> g h
+
+    some (Free1 f) = Free1 $ \h -> some (f h)
+
+    many (Free1 f) = Free1 $ \h -> many (f h)
+
+
+instance (forall h. c h => MonadPlus h)
+         => MonadPlus (Free1 c f) where
+
+    mzero = Free1 $ \_ -> mzero
+
+    Free1 f `mplus` Free1 g = Free1 $ \h -> f h `mplus` g h 
+
+
+instance (forall h. c h => MonadZip h)
+         => MonadZip (Free1 c f) where
+
+    Free1 f `mzip` Free1 g = Free1 $ \h -> f h `mzip` g h
+
+    mzipWith k (Free1 f) (Free1 g) = Free1 $ \h -> mzipWith k (f h) (g h)
+
+    munzip (Free1 f) = (Free1 $ \h -> fst (munzip (f h)), Free1 $ \h -> snd (munzip (f h)))
+
+
+type instance AlgebraType0 (Free1 c) f = ()
+type instance AlgebraType  (Free1 c) f = (c f)
+instance (forall f. c (Free1 c f)) => FreeAlgebra1 (Free1 c) where
+
+    liftFree = \fa -> Free1 $ \g -> g fa
+
+    foldNatFree nat (Free1 f) = f nat
+
+#endif
+
 -- $monadContT
 --
 -- @'ContT' r m@ is not functorial in @m@, so there is no chance it can admit
@@ -614,6 +724,3 @@
         nat mma >>= \ma -> case ma of
             Nothing -> point
             Just a  -> return a
-
-    codom1  = proof
-    forget1 = proof
diff --git a/src/Control/Algebra/Free2.hs b/src/Control/Algebra/Free2.hs
--- a/src/Control/Algebra/Free2.hs
+++ b/src/Control/Algebra/Free2.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DefaultSignatures   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PolyKinds           #-}
 {-# LANGUAGE RankNTypes          #-}
@@ -15,7 +16,6 @@
       FreeAlgebra2 (..)
       -- ** Type level witnesses
     , Proof (..)
-    , proof
       -- ** Algebra types \/ constraints
     , AlgebraType0
     , AlgebraType
@@ -31,10 +31,9 @@
     ) where
 
 import           Control.Monad (join)
-import           Data.Constraint (Dict (..))
 import           Data.Kind (Type)
 
-import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..), proof)
+import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))
 
 -- |
 -- Free algebra class similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but for
@@ -42,6 +41,8 @@
 --
 class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where
 
+    {-# MINIMAL liftFree2, foldNatFree2 #-}
+
     -- |
     -- Lift a graph @f@ satsifying the constraint @'AlgebraType0'@ to
     -- a free its object @m f@.
@@ -59,6 +60,9 @@
     -- satisfies the constraint @AlgebraType m d@ then we can construct
     -- a morphism from @m f@ to @d@.
     --
+    -- prop> foldNatFree2 nat (liftFree2 tr) = nat tr
+    -- prop> foldNatFree2 nat . foldNatFree2 nat' = foldNatFree2 (foldNatFree2 nat . nat')
+    --
     foldNatFree2 :: forall (d :: k -> k -> Type)
                            (f :: k -> k -> Type) a b .
                     ( AlgebraType  m d
@@ -79,6 +83,10 @@
                AlgebraType0 m f
             => Proof (AlgebraType m (m f)) (m f)
 
+    default codom2 :: forall a. AlgebraType m (m a)
+                   => Proof (AlgebraType m (m a)) (m a)
+    codom2 = Proof
+
     -- | 
     -- A proof that each type @f :: k -> k -> Type@ satisfying the
     -- @Algebra m f@ constraint also satisfies @AlgebraType0 m f@.  This
@@ -88,14 +96,17 @@
     -- satisfy the @AlgebraType0 m@ constraint.
     --
     forget2 :: forall (f :: k -> k -> Type).
-               AlgebraType  m f
+               AlgebraType m f
             => Proof (AlgebraType0 m f) (m f)
 
---
--- Combinaators
+    default forget2 :: forall a. AlgebraType0 m a
+                    => Proof (AlgebraType0 m a) (m a)
+    forget2 = Proof
+
+-- Combinators
 --
 
--- | A version of @wrap@ from __free__ package but for graphs.
+-- | Version of @wrap@ from @free@ package but for graphs.
 --
 wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)
                     (f :: Type -> Type -> Type)
@@ -107,7 +118,7 @@
           => f a (m f a b)
           -> m f a b
 wrapFree2 = join . liftFree2
-{-# INLINE wrapFree2 #-}
+{-# INLINABLE wrapFree2 #-}
 
 -- | Like @'foldFree'@ or @'foldFree1'@ but for graphs.
 -- 
@@ -129,8 +140,8 @@
           => m f a b
           -> f a b
 foldFree2 = case forget2 :: Proof (AlgebraType0 m f) (m f) of
-    Proof Dict -> foldNatFree2 id
-{-# INLINE foldFree2 #-}
+    Proof -> foldNatFree2 id
+{-# INLINABLE foldFree2 #-}
 
 -- | 
 -- Inverse of @'foldNatFree2'@.
@@ -149,7 +160,7 @@
     => (forall x y. m f x y -> d x y)
     -> f a b -> d a b
 unFoldNatFree2 nat = nat . liftFree2
-{-# INLINE unFoldNatFree2 #-}
+{-# INLINABLE unFoldNatFree2 #-}
 
 -- |
 -- Hoist the underlying graph in the free structure.
@@ -171,9 +182,19 @@
            -> m f a b
            -> m g a b
 hoistFree2 nat = case codom2 :: Proof (AlgebraType m (m g)) (m g) of
-    Proof Dict -> foldNatFree2 (liftFree2 . nat)
-{-# INLINE hoistFree2 #-}
+    Proof -> foldNatFree2 (liftFree2 . nat)
+{-# INLINABLE [1] hoistFree2 #-}
 
+{-# RULES
+
+"hositFree2/foldNatFree2"
+    forall (nat  :: forall (x :: k) (y :: k). g x y -> c x y)
+           (nat0 :: forall (x :: k) (y :: k). f x y -> g x y)
+           (f :: m f a b).
+    foldNatFree2 nat (hoistFree2 nat0 f) = foldNatFree2 (nat . nat0) f
+
+#-}
+
 -- |
 -- Hoist the top level free structure.
 --
@@ -187,12 +208,22 @@
         => m f a b
         -> n f a b
 hoistFreeH2 = foldNatFree2 liftFree2
-{-# INLINE hoistFreeH2 #-}
+{-# INLINABLE [1] hoistFreeH2 #-}
 
--- |
--- @'FreeAlgebra2' m@ is a monad on some subcategory of graphs (types of kind
--- @k -> k -> Type@), @'joinFree'@ it is the @join@ of this monad.
+{-# RULES
+
+"hoistFreeH2/foldNatFree2" forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
+                                  (f :: AlgebraType m c => m f a b).
+                           foldNatFree2 nat (hoistFreeH2 f) = foldNatFree2 nat f
+#-}
+
+-- | 'FreeAlgebra2' m@ is a monad on some subcategory of graphs (types of kind
+-- @k -> k -> 'Type'@), 'joinFree' it is the 'join' of this monad.
 --
+-- prop> foldNatFree2 nat . joinFree2 = foldNatFree2 (foldNatFree2 nat)
+--
+-- This property is analogous to @foldMap f . concat = foldMap (foldMap f)@,
+--
 joinFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)
                     (f :: k -> k -> Type)
                     a b .
@@ -202,14 +233,16 @@
           => m (m f) a b
           -> m f a b
 joinFree2 = case codom2 :: Proof (AlgebraType m (m f)) (m f) of
-    Proof Dict -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
-        Proof Dict -> foldFree2
-{-# INLINE joinFree2 #-}
+    Proof -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
+        Proof -> foldFree2
+{-# INLINABLE joinFree2 #-}
 
 -- |
--- @bind@ of the monad defined by @m@ on the subcategory of graphs (typed of
+-- @bind@ of the monad defined by @m@ on the subcategory of graphs (types of
 -- kind @k -> k -> Type@).
 --
+-- prop> foldNatFree2 nat (bindFree mf nat') = foldNatFree2 (foldNatFree2 nat . nat') mf
+--
 bindFree2 :: forall m f g a b .
              ( FreeAlgebra2 m
              , AlgebraType0 m g
@@ -219,8 +252,8 @@
           -> (forall x y . f x y -> m g x y)
           -> m g a b
 bindFree2 mfa nat = case codom2 :: Proof (AlgebraType m (m g)) (m g) of
-    Proof Dict -> foldNatFree2 nat mfa
-{-# INLINE bindFree2 #-}
+    Proof -> foldNatFree2 nat mfa
+{-# INLINABLE bindFree2 #-}
 
 assocFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)
                      (f :: Type -> Type -> Type)
@@ -232,8 +265,8 @@
            => m f a (m f a b)
            -> m (m f) a (f a b)
 assocFree2 = case forget2 :: Proof (AlgebraType0 m f) (m f) of
-    Proof Dict -> case codom2 :: Proof (AlgebraType m (m f)) (m f) of
-        Proof Dict -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
-            Proof Dict -> case codom2 :: Proof (AlgebraType m (m (m f))) (m (m f)) of
-                Proof Dict -> fmap foldFree2 <$> foldNatFree2 (hoistFree2 liftFree2 . liftFree2)
-{-# INLINE assocFree2 #-}
+    Proof -> case codom2 :: Proof (AlgebraType m (m f)) (m f) of
+        Proof -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
+            Proof -> case codom2 :: Proof (AlgebraType m (m (m f))) (m (m f)) of
+                Proof -> fmap foldFree2 . foldNatFree2 (hoistFree2 liftFree2 . liftFree2)
+{-# INLINABLE assocFree2 #-}
diff --git a/src/Control/Monad/Action.hs b/src/Control/Monad/Action.hs
--- a/src/Control/Monad/Action.hs
+++ b/src/Control/Monad/Action.hs
@@ -9,14 +9,14 @@
 
 import           Control.Monad (join)
 import           Data.Functor.Const (Const (..))
+import           Data.Functor.Compose (Compose (..))
 import           Data.Kind (Type)
 
 import           Control.Algebra.Free
-    ( AlgebraType0
-    , AlgebraType
-    , FreeAlgebra1 (..)
-    , proof
-    )
+                    ( AlgebraType0
+                    , AlgebraType
+                    , FreeAlgebra1 (..)
+                    )
 import           Data.Algebra.Pointed (Pointed (point))
 import           Data.Algebra.Free (FreeAlgebra, foldFree)
 
@@ -57,17 +57,27 @@
 -- |
 -- Free algebra associated with the @'MAction' constraint.
 newtype FreeMAction (m :: Type -> Type) (f :: Type -> Type) a =
-    FreeMAction { runFreeMAction :: m (f a) }
+    FreeMAction {
+        runFreeMAction :: m (f a)
+    }
     deriving (Show, Eq, Ord, Functor)
 
+instance (Applicative m, Applicative f) => Applicative (FreeMAction m f) where
+
+    pure = FreeMAction . getCompose . pure
+
+    FreeMAction mfa <*> FreeMAction mfb =
+        FreeMAction $ getCompose $ Compose mfa <*> Compose mfb
+
+
 instance (Monad m, Functor f) => MAction m (FreeMAction m f) where
-    mact mfa = FreeMAction $ join $ runFreeMAction <$> mfa
 
+    mact mfa = FreeMAction $ mfa >>= runFreeMAction
+
+
 type instance AlgebraType  (FreeMAction m) f = MAction m f
 type instance AlgebraType0 (FreeMAction m) f = Functor f
 instance Monad m => FreeAlgebra1 (FreeMAction m) where
     liftFree = FreeMAction . return
-    foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa
-
-    codom1  = proof
-    forget1 = proof
+    foldNatFree nat (FreeMAction mfa)
+             = mact $ nat <$> mfa
diff --git a/src/Data/Algebra/Free.hs b/src/Data/Algebra/Free.hs
--- a/src/Data/Algebra/Free.hs
+++ b/src/Data/Algebra/Free.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP                 #-}
 {-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE DefaultSignatures   #-}
 {-# LANGUAGE FlexibleInstances   #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE InstanceSigs        #-}
@@ -14,7 +15,6 @@
       FreeAlgebra (..)
       -- ** Type level witnesses
     , Proof (..)
-    , proof
     , -- ** Algebra types \/ constraints
       AlgebraType
     , AlgebraType0
@@ -37,17 +37,25 @@
 
 import           Prelude
 
-import           Data.Constraint (Dict (..))
+#if __GLASGOW_HASKELL__ < 808
 import           Data.DList (DList)
+#endif
 import           Data.DList as DList
 import           Data.Functor.Identity (Identity (..))
 import           Data.Fix (Fix, cata)
 import           Data.Group (Group (..))
 import           Data.Kind (Constraint, Type)
 import           Data.List.NonEmpty (NonEmpty (..))
-import           Data.Monoid (Endo (..), Monoid (..), Dual (..))
-import           Data.Semigroup (Semigroup, (<>))
-
+import           Data.Monoid ( Endo (..)
+#if __GLASGOW_HASKELL__ < 808
+                             , Monoid (..)
+#endif
+                             , Dual (..))
+#if __GLASGOW_HASKELL__ < 808
+import           Data.Semigroup ( Semigroup
+                                , (<>)
+                                )
+#endif
 import           Data.Algebra.Pointed (Pointed (..))
 
 --
@@ -75,13 +83,8 @@
 
 -- |
 -- A proof that constraint @c@ holds for type @a@.
-newtype Proof (c :: Constraint) (a :: l) = Proof (Dict c)
-
--- |
--- @'Proof'@ smart constructor.
-proof :: c => Proof (c :: Constraint) (a :: l)
-proof = Proof Dict
-{-# INLINE proof #-}
+data Proof (c :: Constraint) (a :: l) where
+    Proof :: c => Proof c a
 
 -- |
 -- A lawful instance has to guarantee that @'unFoldFree'@ is an inverse of
@@ -93,8 +96,12 @@
 -- composition of left adjoin and the right one is always a monad, this is why
 -- we will be able to build monad instance for @m@.
 class FreeAlgebra (m :: Type -> Type)  where
+
+    {-# MINIMAL returnFree, foldMapFree #-}
+
     -- | Injective map that embeds generators @a@ into @m@.
     returnFree :: a -> m a
+
     -- | The freeness property.
     foldMapFree
         :: forall d a
@@ -111,11 +118,19 @@
     -- satisfying @AlgebraType m a@, @'fmapFree'@ below proves that it's a functor.
     -- (@'codom'@ from codomain)
     codom  :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
+
+    default codom :: forall a. AlgebraType m (m a)
+                  => Proof (AlgebraType m (m a)) (m a)
+    codom = Proof
+
     -- |
     -- Proof that the forgetful functor from types @a@ satisfying @AgelbraType
     -- m a@ to @AlgebraType0 m a@ is well defined.
     forget :: forall a. AlgebraType  m a => Proof (AlgebraType0 m a) (m a)
 
+    default forget :: forall a. AlgebraType0 m a
+                   => Proof (AlgebraType0 m a) (m a)
+    forget = Proof
 
 --
 -- Free combinators
@@ -124,6 +139,8 @@
 -- |
 -- Inverse of @'foldMapFree'@
 --
+-- It is uniquelly determined by its universal property (by Yonneda lemma):
+--
 -- prop> unFoldMapFree id = returnFree
 --
 -- Note that @'unFoldMapFree' id@ is the unit of the
@@ -134,13 +151,11 @@
     => (m a -> d)
     -> (a -> d)
 unFoldMapFree f = f . returnFree
-{-# INLINE unFoldMapFree #-}
+{-# INLINABLE unFoldMapFree #-}
 
 -- |
 -- All types which satisfy @'FreeAlgebra'@ constraint are foldable.
 --
--- It is uniquelly determined by its universal property (by Yonneda lemma):
---
 -- prop> foldFree . returnFree == id
 --
 -- @foldFree@ is the
@@ -164,8 +179,8 @@
     => m a
     -> a
 foldFree ma = case forget @m @a of
-    Proof Dict -> foldMapFree id ma
-{-# INLINE foldFree #-}
+    Proof -> foldMapFree id ma
+{-# INLINABLE foldFree #-}
 
 -- |
 -- The canonical quotient map from a free algebra of a wider class to a free
@@ -190,7 +205,7 @@
         => m a
         -> n a
 natFree = foldMapFree returnFree
-{-# INLINE natFree #-}
+{-# INLINABLE natFree #-}
 
 -- |
 -- All types which satisfy @'FreeAlgebra'@ constraint are functors.
@@ -204,8 +219,8 @@
          -> m a
          -> m b
 fmapFree f ma = case codom @m @b of
-    Proof Dict -> foldMapFree (returnFree . f) ma
-{-# INLINE fmapFree #-}
+    Proof -> foldMapFree (returnFree . f) ma
+{-# INLINABLE fmapFree #-}
 
 -- |
 -- @'FreeAlgebra'@ constraint implies @Monad@ constrain.
@@ -216,8 +231,8 @@
          => m (m a)
          -> m a
 joinFree mma = case codom @m @a of
-    Proof Dict -> foldFree mma
-{-# INLINE joinFree #-}
+    Proof -> foldFree mma
+{-# INLINABLE joinFree #-}
 
 -- |
 -- The monadic @'bind'@ operator.  @'returnFree'@ is the corresponding
@@ -231,8 +246,8 @@
          -> (a -> m b)
          -> m b
 bindFree ma f = case codom @m @b of
-    Proof Dict -> foldMapFree f ma
-{-# INLINE bindFree #-}
+    Proof -> foldMapFree f ma
+{-# INLINABLE bindFree #-}
 
 -- |
 -- @'Fix' m@ is the initial algebra in the category of algebras of type
@@ -332,9 +347,6 @@
     returnFree = Identity
     foldMapFree f = f . runIdentity
 
-    codom  = proof
-    forget = proof
-
 type instance AlgebraType0 NonEmpty a = ()
 type instance AlgebraType  NonEmpty m = Semigroup m
 -- |
@@ -347,9 +359,6 @@
     foldMapFree f (a :| []) = f a
     foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs)
 
-    codom  = Proof Dict
-    forget = Proof Dict
-
 type instance AlgebraType0 [] a = ()
 type instance AlgebraType  [] m = Monoid m
 -- | 
@@ -370,9 +379,6 @@
     returnFree a = [a]
     foldMapFree = foldMap
 
-    codom  = Proof Dict
-    forget = Proof Dict
-
 type instance AlgebraType0 Maybe a = ()
 type instance AlgebraType  Maybe m = Pointed m
 instance FreeAlgebra Maybe where
@@ -380,13 +386,12 @@
     foldMapFree _ Nothing  = point
     foldMapFree f (Just a) = f a
 
-    codom  = Proof Dict
-    forget = Proof Dict
-
 -- |
 -- @'Free' c a@ represents free algebra for a constraint @c@ generated by
 -- type @a@.
-newtype Free c a = Free { runFree :: forall r. c r => (a -> r) -> r }
+newtype Free (c :: Type -> Constraint) a = Free {
+          runFree :: forall r. c r => (a -> r) -> r
+        }
 
 instance Semigroup (Free Semigroup a) where
     Free f <> Free g = Free $ \k -> f k <> g k
@@ -397,15 +402,12 @@
     returnFree a = Free $ \k -> k a
     foldMapFree f (Free k) = k f
 
-    codom  = Proof Dict
-    forget = Proof Dict
-
 instance Semigroup (Free Monoid a) where
     Free f <> Free g = Free $ \k -> f k `mappend` g k
 
 instance Monoid (Free Monoid a) where
     mempty = Free (const mempty)
-#if __GLASGOW_HASKELL__ <= 822
+#if __GLASGOW_HASKELL__ <= 802
     mappend = (<>)
 #endif
 
@@ -416,9 +418,6 @@
     returnFree a = Free $ \k -> k a
     foldMapFree f (Free k) = k f
 
-    codom  = proof
-    forget = proof
-
 type instance AlgebraType0 DList a = ()
 type instance AlgebraType  DList a = Monoid a
 -- |
@@ -428,15 +427,12 @@
     returnFree = DList.singleton
     foldMapFree = foldMap
 
-    codom  = proof
-    forget = proof
-
 instance Semigroup (Free Group a) where
     Free f <> Free g = Free $ \k -> f k `mappend` g k
 
 instance Monoid (Free Group a) where
     mempty = Free (const mempty)
-#if __GLASGOW_HASKELL__ <= 822
+#if __GLASGOW_HASKELL__ <= 802
     mappend = (<>)
 #endif
 
@@ -448,6 +444,3 @@
 instance FreeAlgebra (Free Group) where
     returnFree a = Free $ \k -> k a
     foldMapFree f (Free k) = k f
-
-    codom  = proof
-    forget = proof
diff --git a/src/Data/Algebra/Pointed.hs b/src/Data/Algebra/Pointed.hs
--- a/src/Data/Algebra/Pointed.hs
+++ b/src/Data/Algebra/Pointed.hs
@@ -7,7 +7,7 @@
     , PointedMonoid (..)
     ) where
 
-#if __GLASGOW_HASKELL__ <= 822
+#if __GLASGOW_HASKELL__ <= 802
 import Data.Semigroup (Semigroup (..))
 #endif
 
@@ -29,7 +29,7 @@
 
 instance Monoid m => Monoid (PointedMonoid m) where
     mempty = PointedMonoid mempty
-#if __GLASGOW_HASKELL__ <= 822
+#if __GLASGOW_HASKELL__ <= 802
     mappend (PointedMonoid m) (PointedMonoid n) = PointedMonoid $ mappend m n
 #endif
 
diff --git a/src/Data/Group/Free.hs b/src/Data/Group/Free.hs
--- a/src/Data/Group/Free.hs
+++ b/src/Data/Group/Free.hs
@@ -24,15 +24,17 @@
 import           Control.Monad (ap)
 import           Data.DList (DList)
 import qualified Data.DList as DList
+import           Data.Bifunctor (bimap)
 import           Data.Group (Group (..))
+#if __GLASGOW_HASKELL__ < 808
 import           Data.Semigroup (Semigroup (..))
+#endif
 
 import           Data.Algebra.Free
-    ( AlgebraType
-    , AlgebraType0
-    , FreeAlgebra (..)
-    , proof
-    )
+                    ( AlgebraType
+                    , AlgebraType0
+                    , FreeAlgebra (..)
+                    )
 
 -- |
 -- Free group generated by a type @a@.  Internally it's represented by a list
@@ -47,22 +49,24 @@
 --
 -- @'FreeGroup' a@ is isomorphic with @'Free' Group a@ (but the latter does not
 -- require @Eq@ constraint, hence is more general).
-newtype FreeGroup a = FreeGroup { runFreeGroup :: DList (Either a a) }
+newtype FreeGroup a = FreeGroup {
+        runFreeGroup :: DList (Either a a)
+    }
     deriving (Eq, Ord, Show)
 
 instance Functor FreeGroup where
-    fmap f (FreeGroup as) = FreeGroup $ fmap (either (Left . f) (Right . f)) as
+    fmap f (FreeGroup as) = FreeGroup $ bimap f f <$> as
 
 instance Applicative FreeGroup where
-    pure  = returnFree
+    pure  = return
     (<*>) = ap
 
 instance Monad FreeGroup where
-    return a = FreeGroup $ DList.singleton (Right a)
+    return a           = FreeGroup $ DList.singleton (Right a)
     FreeGroup as >>= f = FreeGroup $ as >>= runFreeGroup . either f f
 
 -- |
--- Normalize a @Dlist@, i.e. remove adjusten inverses from a word, i.e.
+-- Normalize a @Dlist@, i.e. remove adjacent inverses from a word, i.e.
 -- @ab⁻¹ba⁻¹c = c@.  Note that this function is implemented using
 -- @'normalizeL'@, implemnting it directly on @DList@s would be @O(n^2)@
 -- instead of @O(n)@.
@@ -113,9 +117,6 @@
             as' = DList.tail as
         in either (invert . f) f a' `mappend` foldMapFree f (FreeGroup as')
 
-    codom  = proof
-    forget = proof
-
 -- |
 -- Free group in the class of groups which multiplication is strict on the
 -- left, i.e.
@@ -176,6 +177,3 @@
     foldMapFree _ (FreeGroupL []) = mempty
     foldMapFree f (FreeGroupL (a : as)) =
         either (invert . f) f a `mappend` foldMapFree f (FreeGroupL as)
-
-    codom  = proof
-    forget = proof
diff --git a/src/Data/Monoid/Abelian.hs b/src/Data/Monoid/Abelian.hs
--- a/src/Data/Monoid/Abelian.hs
+++ b/src/Data/Monoid/Abelian.hs
@@ -8,19 +8,27 @@
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Semigroup (Semigroup (..), stimes)
-import           Data.Natural (Natural)
+import           Numeric.Natural (Natural)
 
-import           Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..), proof)
+import           Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..))
 import           Data.Semigroup.Abelian (AbelianSemigroup)
 
 -- |
 -- Free abelian monoid.  Note that `FreeAbelianMonoid () ≅ Natural` as
 -- expected.
-newtype FreeAbelianMonoid a = FreeAbelianMonoid (Map a Natural)
+--
+-- It is a monad on the full subcategory which satisfies the `Ord` constraint,
+-- but base does not allow to define a functor \/ applicative \/ monad
+-- instances which are constraint by a class.
+--
+newtype FreeAbelianMonoid a = FreeAbelianMonoid {
+        runFreeAbelianMonoid :: Map a Natural
+    }
     deriving (Eq, Ord, Show)
 
 instance Ord a => Semigroup (FreeAbelianMonoid a) where
-    (FreeAbelianMonoid a) <> (FreeAbelianMonoid b) = FreeAbelianMonoid $ Map.unionWith (+) a b
+    FreeAbelianMonoid a <> FreeAbelianMonoid b =
+        FreeAbelianMonoid $ Map.unionWith (+) a b
 
 instance Ord a => AbelianSemigroup (FreeAbelianMonoid a)
 
@@ -32,8 +40,9 @@
 
 type instance AlgebraType0 FreeAbelianMonoid a = Ord a
 type instance AlgebraType  FreeAbelianMonoid m = (Ord m, Monoid m, AbelianSemigroup m)
+
 instance FreeAlgebra FreeAbelianMonoid where
     returnFree a = FreeAbelianMonoid (Map.singleton a 1)
-    foldMapFree g (FreeAbelianMonoid as) = Map.foldMapWithKey (\a n -> stimes n $ g a) as 
-    codom  = proof
-    forget = proof
+
+    foldMapFree g (FreeAbelianMonoid as)
+                 = Map.foldMapWithKey (\a n -> stimes n $ g a) as
diff --git a/src/Data/Semigroup/Abelian.hs b/src/Data/Semigroup/Abelian.hs
--- a/src/Data/Semigroup/Abelian.hs
+++ b/src/Data/Semigroup/Abelian.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP          #-}
 {-# LANGUAGE TypeFamilies #-}
 
 module Data.Semigroup.Abelian
@@ -13,25 +14,30 @@
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Set (Set)
+#if __GLASGOW_HASKELL__ < 808
 import           Data.Semigroup
-    ( Semigroup (..)
-    , All
-    , Any
-    , Dual
-    , Max
-    , Min
-    , Option
-    , Product
-    , Sum
-    )
+                    ( Semigroup (..),
+#else
+import           Data.Semigroup
+                    (
+#endif
+                      All
+                    , Any
+                    , Dual
+                    , Max
+                    , Min
+                    , Option
+                    , Product
+                    , Sum
+                    )
 import           Data.Void (Void)
+import           Numeric.Natural (Natural)
 
 import           Data.Algebra.Free
-    ( AlgebraType
-    , AlgebraType0
-    , FreeAlgebra (..)
-    , proof
-    )
+                    ( AlgebraType
+                    , AlgebraType0
+                    , FreeAlgebra (..)
+                    )
 
 -- |
 -- Class of commutative monoids, e.g. with additional law:
@@ -67,20 +73,25 @@
 -- |
 -- Free abelian semigroup is isomorphic to a non empty map with keys @a@ and
 -- values positive natural numbers.
-newtype FreeAbelianSemigroup a = FreeAbelianSemigroup (Map a Integer)
+--
+-- It is a monad on the full subcategory which satisfies the `Ord` constraint,
+-- but base does not allow to define a functor \/ applicative \/ monad
+-- instances which are constraint by a class.
+--
+newtype FreeAbelianSemigroup a = FreeAbelianSemigroup (Map a Natural)
     deriving (Ord, Eq, Show)
 
-toNonEmpty :: FreeAbelianSemigroup a -> NonEmpty (a, Integer)
+toNonEmpty :: FreeAbelianSemigroup a -> NonEmpty (a, Natural)
 toNonEmpty (FreeAbelianSemigroup as) = NE.fromList . Map.toList $ as
 
 -- |
 -- Smart constructor which creates `FreeAbelianSemigroup` from a non empty list
--- of pairs @(a, n) :: (a, Integer)@ where @n > 0@.
-fromNonEmpty :: Ord a => NonEmpty (a, Integer) -> Maybe (FreeAbelianSemigroup a)
+-- of pairs @(a, n) :: (a, Natural)@ where @n > 0@.
+fromNonEmpty :: Ord a => NonEmpty (a, Natural) -> Maybe (FreeAbelianSemigroup a)
 fromNonEmpty = fmap (FreeAbelianSemigroup . Map.fromList) . go . NE.toList
     where
-    go [] = Just []
-    go ((a, n) : as) | n < 0     = Nothing
+    go []            = Just []
+    go ((a, n) : as) | n == 0    = Nothing
                      | otherwise = ((a, n) :) <$> go as
 
 instance Ord a => Semigroup (FreeAbelianSemigroup a) where
@@ -90,17 +101,17 @@
 
 type instance AlgebraType0 FreeAbelianSemigroup a = Ord a
 type instance AlgebraType  FreeAbelianSemigroup a = (Ord a, AbelianSemigroup a)
+
 instance FreeAlgebra FreeAbelianSemigroup where
     returnFree a = FreeAbelianSemigroup $ Map.singleton a 1
-    foldMapFree f (FreeAbelianSemigroup as) = foldMapFree f (toNonEmpty_ as)
-        where
-        replicate_ :: a -> Integer -> [a]                                     
+
+    foldMapFree f (FreeAbelianSemigroup as)
+                 = foldMapFree f (toNonEmpty_ as)
+      where
+        replicate_ :: a -> Natural -> [a]                                     
         replicate_ _ n | n <= 0 = error "foldMapFree @FreeAbelianSemigroup: impossible"
         replicate_ a 1 = [a]                                                   
         replicate_ a n = a : replicate_ a (n - 1)                             
 
-        toNonEmpty_ :: Map a Integer -> NonEmpty a
+        toNonEmpty_ :: Map a Natural -> NonEmpty a
         toNonEmpty_ = NE.fromList . concatMap (uncurry replicate_) . Map.toList
-
-    codom  = proof
-    forget = proof
diff --git a/src/Data/Semigroup/SemiLattice.hs b/src/Data/Semigroup/SemiLattice.hs
deleted file mode 100644
--- a/src/Data/Semigroup/SemiLattice.hs
+++ /dev/null
@@ -1,60 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TypeFamilies               #-}
-
-module Data.Semigroup.SemiLattice
-    ( FreeSemiLattice
-    , fromNonEmpty
-    , toNonEmpty
-    ) where
-
-import           Data.List.NonEmpty (NonEmpty (..))
-import qualified Data.List.NonEmpty as NE
-import           Data.IntSet (IntSet)
-import           Data.Semigroup (All, Any, Semigroup, sconcat)
-import           Data.Set (Set)
-import qualified Data.Set as Set
-import           Data.Void (Void)
-
-import           Data.Algebra.Free
-    ( AlgebraType
-    , AlgebraType0
-    , FreeAlgebra (..)
-    , proof
-    )
-import           Data.Semigroup.Abelian (AbelianSemigroup)
-
--- |
--- Class of abelian semigroups in which every element is idempontent, i.e.
--- @a <> a = a@.
-class AbelianSemigroup m => SemiLattice m
-
-instance SemiLattice Void
-instance SemiLattice ()
-instance SemiLattice All
-instance SemiLattice Any
-instance Ord a => SemiLattice (Set a)
-instance SemiLattice IntSet
-
--- |
--- @'FreeSemiLattice'@ is a non empty set.
-newtype FreeSemiLattice a = FreeSemiLattice (Set a)
-    deriving (Ord, Eq, Show, Semigroup)
-
-instance Ord a => AbelianSemigroup (FreeSemiLattice a)
-
-instance Ord a => SemiLattice (FreeSemiLattice a)
-
-fromNonEmpty :: Ord a => NonEmpty a -> FreeSemiLattice a
-fromNonEmpty = FreeSemiLattice . Set.fromList . NE.toList
-
-toNonEmpty :: FreeSemiLattice a -> NonEmpty a
-toNonEmpty (FreeSemiLattice as) = NE.fromList $ Set.toList as
-
-type instance AlgebraType0 FreeSemiLattice a = Ord a
-type instance AlgebraType  FreeSemiLattice a = (Ord a, SemiLattice a)
-instance FreeAlgebra FreeSemiLattice where
-    returnFree a = FreeSemiLattice $ Set.singleton a
-    foldMapFree f (FreeSemiLattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as
-
-    codom  = proof
-    forget = proof
diff --git a/src/Data/Semigroup/Semilattice.hs b/src/Data/Semigroup/Semilattice.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Semigroup/Semilattice.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies               #-}
+
+module Data.Semigroup.Semilattice
+    ( FreeSemilattice
+    , fromNonEmpty
+    , toNonEmpty
+    ) where
+
+import           Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NE
+import           Data.IntSet (IntSet)
+import           Data.Semigroup ( All
+                                , Any
+#if __GLASGOW_HASKELL__ < 808
+                                , Semigroup
+#endif
+                                , sconcat)
+import           Data.Set (Set)
+import qualified Data.Set as Set
+import           Data.Void (Void)
+
+import           Data.Algebra.Free ( AlgebraType
+                                   , AlgebraType0
+                                   , FreeAlgebra (..)
+                                   )
+import           Data.Semigroup.Abelian (AbelianSemigroup)
+
+-- |
+-- Class of abelian semigroups in which every element is idempontent, i.e.
+-- @a <> a = a@.
+class AbelianSemigroup m => Semilattice m
+
+instance Semilattice Void
+instance Semilattice ()
+instance Semilattice All
+instance Semilattice Any
+instance Ord a => Semilattice (Set a)
+instance Semilattice IntSet
+
+-- |
+-- @'FreeSemilattice'@ is a non empty set.
+newtype FreeSemilattice a = FreeSemilattice (Set a)
+    deriving (Ord, Eq, Show, Semigroup)
+
+instance Ord a => AbelianSemigroup (FreeSemilattice a)
+
+instance Ord a => Semilattice (FreeSemilattice a)
+
+fromNonEmpty :: Ord a => NonEmpty a -> FreeSemilattice a
+fromNonEmpty = FreeSemilattice . Set.fromList . NE.toList
+
+toNonEmpty :: FreeSemilattice a -> NonEmpty a
+toNonEmpty (FreeSemilattice as) = NE.fromList $ Set.toList as
+
+type instance AlgebraType0 FreeSemilattice a = Ord a
+type instance AlgebraType  FreeSemilattice a = (Ord a, Semilattice a)
+instance FreeAlgebra FreeSemilattice where
+    returnFree a = FreeSemilattice $ Set.singleton a
+    foldMapFree f (FreeSemilattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -3,6 +3,7 @@
    ) where
 
 import           Control.Monad (unless)
+import           System.IO (hSetEncoding, stdout, utf8)
 import           System.Exit (exitFailure)
 
 import qualified Test.Control.Algebra.Free (tests)
@@ -17,6 +18,7 @@
 
 main :: IO ()
 main = do
+    hSetEncoding stdout utf8
     runTests
         [ Test.Control.Algebra.Free.tests
         , Test.Data.Algebra.Free.tests
diff --git a/test/Test/Control/Algebra/Free.hs b/test/Test/Control/Algebra/Free.hs
--- a/test/Test/Control/Algebra/Free.hs
+++ b/test/Test/Control/Algebra/Free.hs
@@ -1,5 +1,10 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+
 module Test.Control.Algebra.Free
     ( tests
     ) where
@@ -8,23 +13,27 @@
 import qualified Control.Applicative.Free as Ap
 import           Control.Monad.Free (Free)
 import qualified Control.Monad.Free as Free
+import qualified Control.Monad.State.Strict as S
+import           Data.Functor (($>))
 import           Data.Functor.Identity (Identity (..))
 import           Data.Functor.Coyoneda (Coyoneda (..), lowerCoyoneda)
-import           Data.Proxy (Proxy (..))
 import           Hedgehog (Property, PropertyT, Gen, property, (===))
 import qualified Hedgehog as H
 import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
+import           Text.Show.Functions ()
 
 import           Data.Algebra.Free ( AlgebraType )
+import           Data.Proxy (Proxy (..))
 import           Control.Algebra.Free
-    ( AlgebraType0
-    , FreeAlgebra1 (..)
-    , unFoldNatFree
-    , foldFree1
-    , hoistFree1
-    , iterFree1
-    )
+                    ( AlgebraType0
+                    , FreeAlgebra1 (..)
+                    , Proof (..)
+                    , unFoldNatFree
+                    , foldFree1
+                    , hoistFree1
+                    , iterFree1
+                    )
 
 genIntToInt :: Integral n => Gen (n -> n)
 genIntToInt = do
@@ -103,12 +112,13 @@
 foldMapFree1_property
     :: forall m f d a
     .  ( FreeAlgebra1 m
-       , AlgebraType m d
-       , AlgebraType m f
+       , AlgebraType  m d
+       , AlgebraType  m f
        , AlgebraType0 m f
-       , Show a
+       , Show    a
        , Show (f a)
-       , Eq (d a)
+       , Eq   (f a)
+       , Eq   (d a)
        , Show (d a)
        )
     => Gen (m f a)
@@ -120,23 +130,20 @@
     = property $ do
         mfa <- H.forAllWith (show . foldFree1) gen_mfa
         fa  <- H.forAll gen_fa
-        H.assert $ fd_id (Proxy :: Proxy m) fd fa == fd fa
-        H.assert $ mfd_id mfd mfa == mfd mfa
-    where
-    fd_id :: Proxy m
-          -> (forall x. f x -> d x)
-          -> (forall x. f x -> d x)
-    fd_id _ nat =
-        let nat' :: forall y . m f y -> d y
-            nat' = foldNatFree nat
-        in unFoldNatFree nat'
-
-    mfd_id :: (forall x. m f x -> d x)
-           -> (forall x. m f x -> d x)
-    mfd_id nat =
-        let nat' :: forall y . f y -> d y
-            nat' = unFoldNatFree nat
-        in foldNatFree nat'
+        H.assert $
+            unFoldNatFree (foldNatFree fd :: forall x. m f x -> d x) fa
+          ==
+            fd fa
+        H.assert $
+            foldNatFree (unFoldNatFree mfd :: forall y. f y -> d y) mfa
+          ==
+            mfd mfa
+        -- this is a consequence of the first property since
+        -- `foldFree1 = foldNatFree id`
+        H.assert $
+            unFoldNatFree (foldFree1 @m) fa
+          ==
+            fa
 
 prop_foldMapFree1_coyoneda :: Property
 prop_foldMapFree1_coyoneda
@@ -195,17 +202,17 @@
 hoistFree1_property
     :: forall m f g a
     .  ( FreeAlgebra1 m
-       , AlgebraType m f
-       , AlgebraType m (m g)
+       , AlgebraType  m f
+       , AlgebraType  m (m g)
        , AlgebraType0 m f
-       , AlgebraType m g
+       , AlgebraType  m g
        , AlgebraType0 m g
        )
     => Gen (m f a)
     -> (m f a -> String)
     -> (m g a -> m g a -> Bool)
-    -> (forall x. f x -> g x)
-    -> ((forall x . f x -> g x) -> m f a -> m g a)
+    -> (forall  x. f x -> g x)
+    -> ((forall x. f x -> g x) -> m f a -> m g a)
     -- ^ reference hoist impelentation
     -> Property
 hoistFree1_property gen show_mfa eq_mga nat refImpl = property $ do
@@ -239,17 +246,17 @@
 iterFree1_property
     :: forall m f a
     .  ( FreeAlgebra1 m
-       , AlgebraType m f
+       , AlgebraType  m f
        , AlgebraType0 m f
-       , AlgebraType m Identity
+       , AlgebraType  m Identity
        , AlgebraType0 m Identity
        , Eq a
        , Show a
        )
     => Gen (m f a)
     -> (m f a -> String)
-    -> (forall x. f x -> x)
-    -> ((forall x . f x -> x) -> m f a -> a)
+    -> (forall x.  f x -> x)
+    -> ((forall x. f x -> x) -> m f a -> a)
     -- ^ reference implementation
     -> Property
 iterFree1_property gen show_mfa nat refImpl = property $ do
@@ -276,7 +283,143 @@
     (show . Ap.retractAp)
     runIdentity
     Ap.iterAp
-    where
+
+foldNatFree_liftFree_property
+    :: forall m g f a proxy n.
+       ( FreeAlgebra1 m
+       , AlgebraType0 m f
+       , AlgebraType  m g
+       , AlgebraType0 m g
+       , Eq (g a)
+       , Monad n
+       )
+    => proxy m
+    -> Gen (f a)
+    -> (f a -> String)
+    -> (forall x. f x -> g x)
+    -> PropertyT n ()
+foldNatFree_liftFree_property _ gen show_fa nat = do
+    (fa :: f a) <- H.forAllWith show_fa gen
+    H.assert $ (foldNatFree nat :: m f a -> g a) (liftFree fa :: m f a) == nat fa
+
+prop_foldNatFree_liftFree_coyoneda :: Property
+prop_foldNatFree_liftFree_coyoneda
+    = property $ foldNatFree_liftFree_property
+        (Proxy :: Proxy Coyoneda)
+        (Gen.maybe $ Gen.word8 (Range.linear 0 255))
+        show
+        (maybe (Left ()) Right)
+
+prop_foldNatFree_liftFree_ap :: Property
+prop_foldNatFree_liftFree_ap
+    = property $ foldNatFree_liftFree_property
+        (Proxy :: Proxy Ap)
+        (Gen.maybe $ Gen.word8 (Range.linear 0 255))
+        show
+        (maybe (Left ()) Right)
+
+prop_foldNatFree_liftFree_free :: Property
+prop_foldNatFree_liftFree_free
+    = property $ foldNatFree_liftFree_property
+        (Proxy :: Proxy Free)
+        (Gen.maybe $ Gen.word8 (Range.linear 0 255))
+        show
+        (maybe (Left ()) Right)
+
+foldNatFree_foldNatFree_property
+    :: forall m f g h a proxy n.
+       ( FreeAlgebra1 m
+       , AlgebraType0 m f
+       , AlgebraType0 m g
+       , AlgebraType  m g
+       , AlgebraType  m h
+       , Monad n
+       )
+    => proxy m
+    -> Gen (m f a)
+    -> (m f a -> String)
+    -> (h a -> h a -> Bool)
+    -> (forall x. g x -> h x)
+    -> (forall x. f x -> m g x)
+    -> PropertyT n ()
+foldNatFree_foldNatFree_property _ gen show_mfa eq_ha nat nat' =
+    case codom1 :: Proof (AlgebraType m (m g)) (m g) of
+      Proof -> do
+          (mfa :: m f a) <- H.forAllWith show_mfa gen
+          H.assert $ (foldNatFree nat :: m g a -> h a) (foldNatFree nat' mfa)
+                  `eq_ha` foldNatFree (foldNatFree nat . nat') mfa
+
+prop_foldNatFree_foldNatFree_coyoneda :: Property
+prop_foldNatFree_foldNatFree_coyoneda = property $ do
+    n <- H.forAll $ Gen.integral (Range.linear 0 255)
+    foldNatFree_foldNatFree_property
+      (Proxy :: Proxy Coyoneda)
+      (genCoyoneda toOdd :: Gen (Coyoneda Maybe Int))
+      show
+      (==)
+      (maybe (Left ()) Right)
+      (liftFreeCoyonedaN n)
+  where
+    liftFreeCoyonedaN :: Int -> Maybe x -> Coyoneda Maybe x
+    liftFreeCoyonedaN 0 fx = liftFree fx
+    liftFreeCoyonedaN n fx = id <$> liftFreeCoyonedaN (pred n) fx
+
+prop_foldNatFree_foldNatFree_ap :: Property
+prop_foldNatFree_foldNatFree_ap
+    = property $ do
+        n  <- H.forAll $ Gen.integral (Range.linear 0 255)
+        foldNatFree_foldNatFree_property
+          (Proxy :: Proxy Ap)
+          (genAp (Gen.integral (Range.linear 0 255)) genIntToInt :: Gen (Ap Maybe Int))
+          (const "blind")
+          (==)
+          (maybe (Left ()) Right)
+          (liftApN n id)
+  where
+    liftApN :: Int -> (x -> x) -> Maybe x -> Ap Maybe x
+    liftApN 0 _ ma = Ap.liftAp ma
+    liftApN n f ma = pure f <*> liftApN (pred n) f ma
+
+prop_foldNatFree_foldNatFree_free :: Property
+prop_foldNatFree_foldNatFree_free = property $ do
+    n <- H.forAll $ Gen.integral (Range.linear 0 255)
+    foldNatFree_foldNatFree_property
+      (Proxy :: Proxy Free)
+      (genFree (Gen.integral (Range.linear 0 255)) :: Gen (Free Maybe Int))
+      show
+      (==)
+      (maybe (Left ()) Right)
+      (liftFreeN n)
+  where
+    liftFreeN :: Int -> Maybe a -> Free Maybe a
+    liftFreeN 0 ma = liftFree ma
+    -- each bind wraps the lhs in a 'Free' constructor
+    liftFreeN n ma = liftFreeN (pred n) ma >>= liftFree . Just
+
+prop_foldNatFree_foldNatFree_StateT :: Property
+prop_foldNatFree_foldNatFree_StateT = property $ do
+    f1 <- H.forAll genIntToInt
+    f2 <- H.forAll genIntToInt
+    f3 <- H.forAll genIntToInt
+    foldNatFree_foldNatFree_property
+      (Proxy :: Proxy (S.StateT Int))
+      gen
+      (const "blind")
+      (\s s' -> S.runStateT s 0 == S.runStateT s' 0)
+      ((\s -> s >>= \x -> S.modify f1 >> pure x)
+        :: forall x. S.StateT Int Identity x -> S.StateT Int Identity x)
+      ((\(Identity x) -> S.lift (S.modify f2) >> S.modify f3 $> x)
+        :: forall x. Identity x -> S.StateT Int (S.StateT Int Identity) x)
+  where
+    gen :: Gen (S.StateT Int Identity Int)
+    gen = do
+      a <- Gen.int $ Range.linear 0 9
+      if a >= 3
+        then do
+          s <- Gen.int $ Range.linear 0 100
+          x <- Gen.int $ Range.linear 0 100
+          pure (S.put s $> x)
+        else pure S.get
 
 tests :: IO Bool
 tests = H.checkParallel $$(H.discover)
diff --git a/test/Test/Data/Algebra/Free.hs b/test/Test/Data/Algebra/Free.hs
--- a/test/Test/Data/Algebra/Free.hs
+++ b/test/Test/Data/Algebra/Free.hs
@@ -1,4 +1,7 @@
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+
 module Test.Data.Algebra.Free
     ( tests
     ) where
@@ -13,16 +16,16 @@
 import qualified Hedgehog.Range as Range
 
 import           Data.Algebra.Free
-    ( AlgebraType
-    , AlgebraType0
-    , FreeAlgebra (..)
-    , foldFree
-    , unFoldMapFree
-    , natFree
-    , fmapFree
-    , joinFree
-    , bindFree
-    )
+                    ( AlgebraType
+                    , AlgebraType0
+                    , FreeAlgebra (..)
+                    , foldFree
+                    , unFoldMapFree
+                    , natFree
+                    , fmapFree
+                    , joinFree
+                    , bindFree
+                    )
 
 natFree_property
     :: ( FreeAlgebra  f
diff --git a/test/Test/Data/Group/Free.hs b/test/Test/Data/Group/Free.hs
--- a/test/Test/Data/Group/Free.hs
+++ b/test/Test/Data/Group/Free.hs
@@ -1,9 +1,12 @@
+{-# LANGUAGE CPP             #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Test.Data.Group.Free
     ( tests
     ) where
 
+#if __GLASGOW_HASKELL__ < 808
 import           Data.Semigroup (Semigroup (..))
+#endif
 import           Data.Bool (bool)
 import           Data.Group (invert)
 import           Data.DList (DList)