diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,12 @@
 # Changelog for free-algebras
 
+## Version 0.0.5.0
+- `FreeAlgebra` renamed `proof` to `codom`, added `Proof` smart constructor `proof`.
+- `FreeAlgebra` instance for `Identity` functor
+- generic `Free` type
+- `DList` and `FreeGroup` based on `DList`, `FreeGroupL`
+- documentation on strictness / laziness improved
+
 ## Version 0.0.4.0
 
 - `S` new type wrapper in `SSet`, and overlappable instance for
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
 # Free Algebras
+[![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)
+[![Travis Build Status](https://travis-ci.org/coot/free-algebras.svg?branch=master)](https://travis-ci.org/coot/free-algebras)
 
 Universal algebra 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).
 
-For an example check out [this](https://github.com/coot/free-algebras/blob/master/example/src/Network/TCP.hs).
+For an example check out [this](https://github.com/coot/free-algebras/blob/master/examples/src/Network/TCP.hs).
diff --git a/free-algebras.cabal b/free-algebras.cabal
--- a/free-algebras.cabal
+++ b/free-algebras.cabal
@@ -1,11 +1,5 @@
--- This file has been generated from package.yaml by hpack version 0.28.2.
---
--- see: https://github.com/sol/hpack
---
--- hash: d8b73793975417d05559e647f1e6239464f6261be7191fbb8ec438df38ca6548
-
 name:           free-algebras
-version:        0.0.4.0
+version:        0.0.5.0
 synopsis:       Free algebras in Haskell.
 description:    Universal algebra approach to free algebras including higher kinded algebraic structures like functors, applicative functors or monads.
 category:       Algebra, Control, Monads
@@ -21,6 +15,7 @@
 extra-source-files:
     ChangeLog.md
     README.md
+tested-with:    GHC==8.0.2, GHC==8.2.2, GHC==8.4.3
 
 source-repository head
   type: git
@@ -31,11 +26,6 @@
   manual: True
   default: False
 
-flag documentation
-  description: Add dependecies to link documentation
-  manual: True
-  default: False
-
 library
   exposed-modules:
       Control.Algebra.Free
@@ -54,45 +44,21 @@
       src
   default-extensions: ConstraintKinds DataKinds DeriveFunctor EmptyDataDecls FlexibleInstances FlexibleContexts KindSignatures InstanceSigs MultiParamTypeClasses OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TupleSections TypeApplications TypeFamilies
   build-depends:
-      base >=4.11 && <5
-    , constraints
-    , containers
-    , data-fix
-    , free
-    , groups
-    , kan-extensions
-    , mtl
-    , natural-numbers
-    , transformers
+      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
+    , free            >= 4.0 && <6.0
+    , 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
   if flag(develop)
     ghc-options: -Werror -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wno-deprecations
   else
     ghc-options: -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wno-deprecations
-  if flag(documentation)
-    build-depends:
-        base >=4.11 && <5
-      , constraints
-      , containers
-      , data-fix
-      , free
-      , groups
-      , kan-extensions
-      , mmorph
-      , mtl
-      , natural-numbers
-      , transformers
-  else
-    build-depends:
-        base >=4.11 && <5
-      , constraints
-      , containers
-      , data-fix
-      , free
-      , groups
-      , kan-extensions
-      , mtl
-      , natural-numbers
-      , transformers
   default-language: Haskell2010
 
 test-suite free-algebras-test
@@ -101,16 +67,18 @@
   other-modules:
       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
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      base >=4.11 && <5
+      base            >= 4.9 && <5
     , constraints
     , containers
     , data-fix
+    , dlist
     , free
     , free-algebras
     , groups
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
@@ -6,6 +6,7 @@
       AlgebraType0
     , AlgebraType
     , Proof (..)
+    , proof
     , FreeAlgebra1 (..)
     -- * Combinators
     , wrapFree
@@ -60,7 +61,7 @@
 import qualified Data.Functor.Day as Day
 import           Data.Functor.Identity (Identity (..))
 
-import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))
+import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..), proof)
 
 -- |
 -- Higher kinded version of @'FreeAlgebra'@.  Instances includes free functors,
@@ -107,7 +108,7 @@
     -- a functor from the full subcategory of types of kind @Type -> Type@
     -- which satisfy @'AlgebraType0' m f@ to ones that satisfy @'AlgebraType'
     -- m f@.
-    proof1  :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
+    codom1  :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
 
     -- |
     -- A proof that the forgetful functor from the full subcategory of types of
@@ -194,7 +195,7 @@
            => (forall x. f x -> g x) -- ^ a natural transformation @f ~> g@
            -> m f a
            -> m g a
-hoistFree1 nat = case proof1 @m @g of
+hoistFree1 nat = case codom1 @m @g of
     Proof Dict -> foldNatFree (liftFree . nat)
 
 -- |
@@ -228,7 +229,7 @@
              )
           => m (m f) a
           -> m f a
-joinFree1 = case proof1 @m @f of
+joinFree1 = case codom1 @m @f of
     Proof Dict -> case forget1 @m @(m f) of
         Proof Dict -> foldFree1
 
@@ -249,7 +250,7 @@
           => m f a
           -> (forall x . f x -> m g x) -- ^ natural transformation @f ~> m g@
           -> m g a
-bindFree1 mfa nat = case proof1 @m @g of
+bindFree1 mfa nat = case codom1 @m @g of
     Proof Dict -> foldNatFree nat mfa
 
 assocFree1 :: forall m f a .
@@ -260,9 +261,9 @@
            => m f (m f a)
            -> m (m f) (f a)
 assocFree1 = case forget1 @m @f of
-    Proof Dict -> case proof1 @m @f of
+    Proof Dict -> case codom1 @m @f of
         Proof Dict -> case forget1 @m @(m f) of
-            Proof Dict -> case proof1 @m @(m f) of
+            Proof Dict -> case codom1 @m @(m f) of
                 Proof Dict -> case forget1 @m @(m (m f)) of
                     Proof Dict -> fmap g <$> foldNatFree f
     where
@@ -316,8 +317,8 @@
     liftFree = liftCoyoneda
     foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'Ap'@ are the applicative functors.
@@ -330,8 +331,8 @@
     liftFree  = Ap.liftAp
     foldNatFree = Ap.runAp
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 type instance AlgebraType0 Fast.Ap g = Functor g
 type instance AlgebraType  Fast.Ap g = Applicative g
@@ -339,8 +340,8 @@
     liftFree  = Fast.liftAp
     foldNatFree = Fast.runAp
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 type instance AlgebraType0 Final.Ap g = Functor g
 type instance AlgebraType  Final.Ap g = Applicative g
@@ -348,8 +349,8 @@
     liftFree  = Final.liftAp
     foldNatFree = Final.runAp
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- @'Day' f f@ newtype wrapper.  It is isomorphic with @'Ap' f@ for applicative
@@ -375,8 +376,8 @@
     foldNatFree nat (DayF day)
         = Day.dap . Day.trans2 nat . Day.trans1 nat $ day
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'Free'@ monad is the class of all monads.
@@ -388,8 +389,8 @@
     liftFree    = Free.liftF
     foldNatFree = Free.foldFree
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 type instance AlgebraType0 Church.F f = Functor f
 type instance AlgebraType  Church.F m = Monad m
@@ -397,8 +398,8 @@
     liftFree    = Church.liftF
     foldNatFree = Church.foldF
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 type instance AlgebraType0 Alt f = Functor f
 type instance AlgebraType  Alt m = Alternative m
@@ -406,8 +407,8 @@
     liftFree    = Alt.liftAlt
     foldNatFree = Alt.runAlt
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'L.StateT'@ monad is the class of all state
@@ -431,8 +432,8 @@
         put s
         return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'S.StateT'@ monad is the class of all state
@@ -450,8 +451,8 @@
         put s
         return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer
@@ -464,8 +465,8 @@
     liftFree = lift
     foldNatFree nat (L.WriterT m) = fst <$> nat m
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer
@@ -479,8 +480,8 @@
     liftFree = lift
     foldNatFree nat (S.WriterT m) = fst <$> nat m
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader
@@ -494,8 +495,8 @@
     foldNatFree nat (ReaderT g) =
         ask >>= nat . g
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader
@@ -512,8 +513,8 @@
             Left e  -> throwError e
             Right a -> return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    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
@@ -527,8 +528,8 @@
         tell w
         return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    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
@@ -542,8 +543,8 @@
         tell w
         return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- |
 -- Algebra type for @'ListT'@ monad transformer.
@@ -568,8 +569,8 @@
         a <- foldM (\x y -> x `mappend1_` y) empty as
         return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
 
 -- $monadContT
 --
@@ -595,5 +596,5 @@
             Nothing -> point
             Just a  -> return a
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
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
@@ -3,14 +3,13 @@
 module Control.Monad.Action where
 
 import           Control.Monad (join)
-import           Data.Constraint (Dict (..))
 import           Data.Functor.Const (Const (..))
 
 import           Control.Algebra.Free
     ( AlgebraType0
     , AlgebraType
     , FreeAlgebra1 (..)
-    , Proof (..)
+    , proof
     )
 import           Data.Algebra.Pointed (Pointed (point))
 import           Data.Algebra.Free (FreeAlgebra, foldFree)
@@ -63,5 +62,5 @@
     liftFree = FreeMAction . return
     foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa
 
-    proof1  = Proof Dict
-    forget1 = Proof Dict
+    codom1  = proof
+    forget1 = proof
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,3 +1,4 @@
+{-# LANGUAGE CPP   #-}
 {-# LANGUAGE GADTs #-}
 module Data.Algebra.Free
     ( -- * Algebra type
@@ -6,6 +7,7 @@
       -- * FreeAlgebra class
     , FreeAlgebra (..)
     , Proof (..)
+    , proof
       -- * Combinators
     , unFoldMapFree
     , foldFree
@@ -18,13 +20,18 @@
     , foldrFree'
     , foldlFree
     , foldlFree'
+    , Free (..)
     )
     where
 
 import           Prelude
 
 import           Data.Constraint (Dict (..))
+import           Data.DList (DList)
+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 (..))
@@ -35,7 +42,7 @@
 -- |
 -- Type family which for each free algebra @m@ returns a type level lambda from
 -- types to constraints.  It is describe the class of algebras for which this
--- free algebra is free. 
+-- free algebra is free.
 --
 -- A lawful instance for this type family must guarantee
 -- that the constraint @'AlgebraType0' m f@ is implied by the @'AlgebraType'
@@ -56,13 +63,19 @@
 newtype Proof (c :: Constraint) (a :: l) = Proof (Dict c)
 
 -- |
+-- @'Proof'@ smart constructor.
+proof :: c => Proof (c :: Constraint) (a :: l)
+proof = Proof Dict
+
+-- |
 -- A lawful instance has to guarantee that @'unFoldFree'@ is an inverse of
--- @'foldMapFree'@.
--- 
--- This in turn guaranties that @m@ is a left adjoint functor from Hask to
--- algebras of type @'AlgebraType m'@.  The right adjoint is the forgetful
--- functor.  The 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@.
+-- @'foldMapFree'@ (in the category of algebras of type @'AlgebraType' m@).
+--
+-- This in turn guaranties that @m@ is a left adjoint functor from full
+-- subcategory of Hask (of types constrained by @'AlgebraType0' m) to algebras
+-- of type @'AlgebraType' m@.  The right adjoint is the forgetful functor.  The
+-- 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
     -- | Injective map that embeds generators @a@ into @m@.
     returnFree :: a -> m a
@@ -79,8 +92,9 @@
     -- Proof that @AlgebraType0 m a => m a@ is an algebra of type @AlgebraType m@.
     -- This proves that @m@ is a mapping from the full subcategory of @Hask@ of
     -- types satisfying @AlgebraType0 m a@ constraint to the full subcategory
-    -- satisfying @AlgebraType m a@, @fmapFree@ below proves that it's a functor.
-    proof  :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
+    -- 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)
     -- |
     -- Proof that the forgetful functor from types @a@ satisfying @AgelbraType
     -- m a@ to @AlgebraType0 m a@ is well defined.
@@ -154,7 +168,7 @@
          => (a -> b)
          -> m a
          -> m b
-fmapFree f ma = case proof @m @b of
+fmapFree f ma = case codom @m @b of
     Proof Dict -> foldMapFree (returnFree . f) ma
 
 -- |
@@ -165,7 +179,7 @@
           )
          => m (m a)
          -> m a
-joinFree mma = case proof @m @a of
+joinFree mma = case codom @m @a of
     Proof Dict -> foldFree mma
 
 -- |
@@ -179,7 +193,7 @@
          => m a
          -> (a -> m b)
          -> m b
-bindFree ma f = case proof @m @b of
+bindFree ma f = case codom @m @b of
     Proof Dict -> foldMapFree f ma
 
 -- |
@@ -268,8 +282,20 @@
     where
     f' x k z = k $! f z x
 
+type instance AlgebraType0 Identity a = ()
+type instance AlgebraType  Identity a = ()
+instance FreeAlgebra Identity where
+    returnFree = Identity
+    foldMapFree f = f . runIdentity
+
+    codom  = proof
+    forget = proof
+
 type instance AlgebraType0 NonEmpty a = ()
 type instance AlgebraType  NonEmpty m = Semigroup m
+-- |
+-- @'NonEmpty'@ is the free semigroup in the class of semigroup which are
+-- strict in the left argument.
 instance FreeAlgebra NonEmpty where
     returnFree a = a :| []
     -- @'foldMap'@ requires @'Monoid' d@ constraint which we don't need to
@@ -277,15 +303,30 @@
     foldMapFree f (a :| []) = f a
     foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs)
 
-    proof  = Proof Dict
+    codom  = Proof Dict
     forget = Proof Dict
 
 type instance AlgebraType0 [] a = ()
 type instance AlgebraType  [] m = Monoid m
+-- | 
+-- Note that @'[]'@ is a free monoid only for monoids which multiplication is
+-- strict in the left argument
+-- [ref](http://comonad.com/reader/2015/free-monoids-in-haskell/). Note that
+-- being strict adds additional equation to the monoid laws:
+--
+-- prop> undefined <> a = undefined
+--
+-- Thus, expectedly we get an equational theory for left / right / two-sided
+-- strict monoids.
+--
+-- Snoc lists are free monoids in the class of monoids which are strict in the
+-- right argument, @'Free' Monoid@ and @'DList' are free in the class of all
+-- Haskell monoids.
 instance FreeAlgebra [] where
     returnFree a = [a]
     foldMapFree = foldMap
-    proof  = Proof Dict
+
+    codom  = Proof Dict
     forget = Proof Dict
 
 type instance AlgebraType0 Maybe a = ()
@@ -295,5 +336,74 @@
     foldMapFree _ Nothing  = point
     foldMapFree f (Just a) = f a
 
-    proof  = Proof Dict
+    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 }
+
+instance Semigroup (Free Semigroup a) where
+    Free f <> Free g = Free $ \k -> f k <> g k
+
+type instance AlgebraType0 (Free Semigroup) a = ()
+type instance AlgebraType  (Free Semigroup) a = Semigroup a
+instance FreeAlgebra (Free Semigroup) where
+    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
+    mappend = (<>)
+#endif
+
+
+type instance AlgebraType0 (Free Monoid) a = ()
+type instance AlgebraType  (Free Monoid) a = Monoid a
+instance FreeAlgebra (Free Monoid) where
+    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
+-- |
+-- @'DList'@ is isomorphic to @'Free' Monoid@; it is free in the class of all
+-- monoids.
+instance FreeAlgebra DList where
+    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
+    mappend = (<>)
+#endif
+
+instance Group (Free Group a) where
+    invert (Free k) = Free (k . invert)
+
+type instance AlgebraType0 (Free Group) a = ()
+type instance AlgebraType  (Free Group) a = Group a
+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
@@ -1,9 +1,13 @@
+{-# LANGUAGE CPP                  #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Data.Algebra.Pointed
     ( Pointed (..)
     , PointedMonoid (..)
     ) where
 
+#if __GLASGOW_HASKELL__ <= 822
+import Data.Semigroup (Semigroup (..))
+#endif
 
 -- |
 -- Class of pointed sets
@@ -23,6 +27,9 @@
 
 instance Monoid m => Monoid (PointedMonoid m) where
     mempty = PointedMonoid mempty
+#if __GLASGOW_HASKELL__ <= 822
+    mappend (PointedMonoid m) (PointedMonoid n) = PointedMonoid $ mappend m n
+#endif
 
 instance Monoid m => Pointed (PointedMonoid m) where
     point = mempty
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
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {- |
    Free groups
 
@@ -7,13 +8,19 @@
  -}
 module Data.Group.Free
     ( FreeGroup
+    , fromDList
+    , toDList
+    , normalize
+
+    , FreeGroupL
     , fromList
     , toList
-    , normalize
+    , normalizeL
     ) where
 
 import           Control.Monad (ap)
-import           Data.Constraint (Dict (..))
+import           Data.DList (DList)
+import qualified Data.DList as DList
 import           Data.Group (Group (..))
 import           Data.Semigroup (Semigroup (..))
 
@@ -21,7 +28,7 @@
     ( AlgebraType
     , AlgebraType0
     , FreeAlgebra (..)
-    , Proof (..)
+    , proof
     )
 
 -- |
@@ -34,19 +41,22 @@
 --
 -- It is a monad on a full subcategory of @Hask@ which constists of types which
 -- satisfy the @'Eq'@ constraint.
-newtype FreeGroup a = FreeGroup { runFreeGroup :: [Either a a] }
-    deriving (Show, Eq, Ord)
+--
+-- @'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) }
+    deriving (Eq, Ord, Show)
 
 instance Functor FreeGroup where
-    fmap f (FreeGroup as) = FreeGroup $ map (either (Left . f) (Right . f)) as
+    fmap f (FreeGroup as) = FreeGroup $ fmap (either (Left . f) (Right . f)) as
 
 instance Applicative FreeGroup where
     pure  = returnFree
     (<*>) = ap
 
 instance Monad FreeGroup where
-    return a = FreeGroup [Right a]
-    FreeGroup as >>= f = FreeGroup $ concatMap (runFreeGroup . either f f) as
+    return a = FreeGroup $ DList.singleton (Right a)
+    FreeGroup as >>= f = FreeGroup $ as >>= runFreeGroup . either f f
 
 -- |
 -- Normalize a list, i.e. remove adjusten inverses from a word, i.e.
@@ -55,60 +65,93 @@
 -- Complexity: @O(n)@
 normalize
     :: Eq a
-    => [Either a a]
-    -> [Either a a]
-
-normalize (Left a : Right b : bs)
-    | a == b    = normalize bs
-    | otherwise = case normalize (Right b : bs) of
-        Right b' : bs' | a == b'
-                       -> bs'
-                       | otherwise
-                       -> Left a : Right b' : bs'
-        bs'            -> Left a : bs'
-
-normalize (Right a : Left b : bs)
-    | a == b    = normalize bs
-    | otherwise = case normalize (Left b : bs) of
-        Left b' : bs' | a == b'
-                      -> bs'
-                      | otherwise
-                      -> Right a : Left b' : bs'
-        bs'           -> Right a : bs'
-
-normalize (a : as) = case normalize as of
-    a' : as' | either Right Left a == a'
-             -> as'
-             | otherwise
-             -> a : a' : as'
-    []       -> [a]
-
-normalize [] = []
+    => DList (Either a a)
+    -> DList (Either a a)
+normalize = DList.foldr fn DList.empty
+    where
+    fn a as = case as of
+        DList.Nil -> DList.singleton a
+        _         ->
+            let b  = DList.head as
+                bs = DList.tail as
+            in case (a, b) of
+                (Left x,  Right y) | x == y -> bs
+                (Right x, Left y)  | x == y -> bs
+                _                           -> DList.cons a as
 
 -- |
 -- Smart constructor which normalizes a list.
-fromList :: Eq a => [Either a a] -> FreeGroup a
-fromList = FreeGroup . normalize
-
-toList :: FreeGroup a -> [Either a a]
-toList = runFreeGroup
+fromDList :: Eq a => DList (Either a a) -> FreeGroup a
+fromDList = FreeGroup . normalize
 
+toDList :: FreeGroup a -> DList (Either a a)
+toDList = runFreeGroup
 
 instance Eq a => Semigroup (FreeGroup a) where
-    FreeGroup as <> FreeGroup bs = FreeGroup $ normalize (as ++ bs)
+    FreeGroup as <> FreeGroup bs = FreeGroup $ normalize (as `DList.append` bs)
 
 instance Eq a => Monoid (FreeGroup a) where
-    mempty = FreeGroup []
+    mempty = FreeGroup DList.empty
+#if __GLASGOW_HASKELL__ <= 822
+    mappend = (<>)
+#endif
 
 instance Eq a => Group (FreeGroup a) where
-    invert (FreeGroup as) = FreeGroup $ foldl (\acu a -> either Right Left a : acu) [] as
+    invert (FreeGroup as) = FreeGroup $ foldl (\acu a -> either Right Left a `DList.cons` acu) DList.empty as
 
 type instance AlgebraType0 FreeGroup a = Eq a
 type instance AlgebraType  FreeGroup g = (Eq g, Group g)
 instance FreeAlgebra FreeGroup where
-    returnFree a = FreeGroup [Right a]
-    foldMapFree _ (FreeGroup [])       = mempty
-    foldMapFree f (FreeGroup (a : as)) = either (invert . f) f a <> foldMapFree f (FreeGroup as)
+    returnFree a = FreeGroup (DList.singleton (Right a))
+    foldMapFree _ (FreeGroup DList.Nil) = mempty
+    foldMapFree f (FreeGroup as)        =
+        let a'  = DList.head as
+            as' = DList.tail as
+        in either (invert . f) f a' `mappend` foldMapFree f (FreeGroup as')
 
-    proof  = Proof Dict
-    forget = Proof Dict
+    codom  = proof
+    forget = proof
+
+-- |
+-- Free group in the class of groups which multiplication is strict on the left, i.e.
+--
+-- prop> undefined <> a = undefined
+newtype FreeGroupL a = FreeGroupL { runFreeGroupL :: [Either a a] }
+    deriving (Show, Eq, Ord)
+
+normalizeL
+    :: Eq a
+    => [Either a a]
+    -> [Either a a]
+normalizeL = DList.toList . normalize . DList.fromList
+
+-- |
+-- Smart constructors
+fromList :: Eq a => [Either a a] -> FreeGroupL a
+fromList = FreeGroupL . normalizeL
+
+toList :: FreeGroupL a -> [Either a a]
+toList = runFreeGroupL
+
+instance Eq a => Semigroup (FreeGroupL a) where
+    FreeGroupL as <> FreeGroupL bs = FreeGroupL $ normalizeL (as ++ bs)
+
+instance Eq a => Monoid (FreeGroupL a) where
+    mempty = FreeGroupL []
+#if __GLASGOW_HASKELL__ <= 822
+    mappend = (<>)
+#endif
+
+instance Eq a => Group (FreeGroupL a) where
+    invert (FreeGroupL as) = FreeGroupL $ foldl (\acu a -> either Right Left a : acu) [] as
+
+type instance AlgebraType0 FreeGroupL a = Eq a
+type instance AlgebraType  FreeGroupL g = (Eq g, Group g)
+instance FreeAlgebra FreeGroupL where
+    returnFree a = FreeGroupL [Right a]
+    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
@@ -1,14 +1,14 @@
+{-# LANGUAGE CPP #-}
 module Data.Monoid.Abelian
     ( FreeAbelianMonoid (..)
     ) where
 
-import           Data.Constraint (Dict (..))
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import           Data.Semigroup (stimes)
+import           Data.Semigroup (Semigroup (..), stimes)
 import           Data.Natural (Natural)
 
-import           Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..), Proof (..))
+import           Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..), proof)
 import           Data.Semigroup.Abelian (AbelianSemigroup)
 
 -- |
@@ -23,12 +23,15 @@
 instance Ord a => AbelianSemigroup (FreeAbelianMonoid a)
 
 instance Ord a => Monoid (FreeAbelianMonoid a) where
-    mempty = FreeAbelianMonoid (Map.empty)
+    mempty = FreeAbelianMonoid Map.empty
+#if __GLASGOW_HASKELL__ <= 822
+    mappend = (<>)
+#endif
 
 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 
-    proof  = Proof Dict
-    forget = Proof Dict
+    codom  = proof
+    forget = proof
diff --git a/src/Data/Monoid/MSet.hs b/src/Data/Monoid/MSet.hs
--- a/src/Data/Monoid/MSet.hs
+++ b/src/Data/Monoid/MSet.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP           #-}
 {-# LANGUAGE DeriveFunctor #-}
 {- |
     Monoid and [group actions](https://en.wikipedia.org/wiki/Group_action) (M-Sets and G-Sets).
@@ -16,23 +17,25 @@
     ) where
 
 import           Control.Monad (ap)
-import           Data.Constraint (Dict (..))
 import           Data.Functor.Const (Const (..))
 import           Data.Functor.Identity (Identity (..))
 import qualified Data.Functor.Product as Functor (Product)
 import qualified Data.Functor.Sum as Functor (Sum)
 import           Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as NE
 import           Data.Monoid (Monoid, Endo (..), Sum (..))
 import           Data.Natural (Natural)
-import           Data.Ord (Down)
+import           Data.Ord (Down (..))
+import           Data.Semigroup (Semigroup (..))
 import           Data.Set (Set)
+import qualified Data.Set as Set
 
 import           Data.Semigroup.SSet (SSet (..), S (..), fact, rep)
 import           Data.Algebra.Free
     ( AlgebraType
     , AlgebraType0
     , FreeAlgebra (..)
-    , Proof (..)
+    , proof
     , bindFree
     , foldrFree
     )
@@ -49,63 +52,153 @@
 -- Note that if @g@ is a @'Group'@ then an @MSet@ is simply a @GSet@, this
 -- is because monoids and groups share the same morphisms (a monoid homomorphis
 -- between groups necessarily preserves inverses).
-class (Monoid m, SSet m a) => MSet m a
+#if __GLASGOW_HASKELL__ > 822
+class (Monoid m , SSet m a) => MSet m a
+  mact :: m -> a -> a
+  mact = act
+#else
+class Monoid m => MSet m a where
+  mact :: m -> a -> a
+#endif
 
-instance Monoid m => MSet m m
+instance Monoid m => MSet m m where
+#if __GLASGOW_HASKELL__ <= 822
+  mact = mappend
+#endif
 
-instance (MSet m a, MSet m b) => MSet m (a, b)
+instance (MSet m a, MSet m b) => MSet m (a, b) where
+#if __GLASGOW_HASKELL__ <= 822
+  mact m (a, b) = (mact m a, mact m b)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c) => MSet m (a, b, c)
+instance (MSet m a, MSet m b, MSet m c) => MSet m (a, b, c) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c) = (mact m a, mact m b, mact m c)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c, MSet m d) => MSet m (a, b, c, d)
+instance (MSet m a, MSet m b, MSet m c, MSet m d) => MSet m (a, b, c, d) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c, d) = (mact m a, mact m b, mact m c, mact m d)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e) => MSet m (a, b, c, d, e)
+instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e) => MSet m (a, b, c, d, e) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c, d, e) = (mact m a, mact m b, mact m c, mact m d, mact m e)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f) => MSet m (a, b, c, d, e, f)
+instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f) => MSet m (a, b, c, d, e, f) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c, d, e, f) = (mact m a, mact m b, mact m c, mact m d, mact m e, mact m f)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h) => MSet m (a, b, c, d, e, f, h)
+instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h) => MSet m (a, b, c, d, e, f, h) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c, d, e, f, h) = (mact m a, mact m b, mact m c, mact m d, mact m e, mact m f, mact m h)
+#endif
 
-instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h, MSet m i) => MSet m (a, b, c, d, e, f, h, i)
+instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h, MSet m i) => MSet m (a, b, c, d, e, f, h, i) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (a, b, c, d, e, f, h, i) = (mact m a, mact m b, mact m c, mact m d, mact m e, mact m f, mact m h, mact m i)
+#endif
 
-instance MSet m a => MSet m [a]
+instance MSet m a => MSet m [a] where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m = map (mact m)
+#endif
 
-instance MSet m a => MSet m (NonEmpty a)
+instance MSet m a => MSet m (NonEmpty a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m = NE.map (mact m)
+#endif
 
-instance (MSet m a, Ord a) => MSet m (Set a)
+instance (MSet m a, Ord a) => MSet m (Set a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m as = Set.map (mact m) as
+#endif
 
 {--
   - instance {-# OVERLAPPABLE #-} (Functor f, MSet m a) => MSet m (f a) where
   -     act m fa = fmap (act m) fa
   --}
 
-instance MSet m a => MSet m (Identity a)
 
-instance MSet m a => MSet (Identity m) a
+#if __GLASGOW_HASKELL__ <= 822
+fmact :: (Functor f, MSet s a) => s -> f a -> f a
+fmact s = fmap (mact s)
+#endif
 
-instance MSet m a => MSet m (Maybe a)
 
-instance MSet m b => MSet m (Either a b)
+instance MSet m a => MSet m (Identity a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = fmact
+#endif
 
-instance MSet m a => MSet m (Down a)
+instance MSet m a => MSet (Identity m) a where
+#if __GLASGOW_HASKELL__ <= 822
+    mact (Identity f) a = f `mact` a
+#endif
 
-instance MSet m a => MSet m (IO a)
+instance MSet m a => MSet m (Maybe a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = fmact
+#endif
 
-instance MSet m b => MSet m (a -> b)
+instance MSet m b => MSet m (Either a b) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = fmact
+#endif
 
-instance MSet (Endo a) a
+instance MSet m a => MSet m (Down a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact m (Down a) =  Down (mact m a)
+#endif
 
-instance {-# OVERLAPPABLE #-} MSet m a => MSet (S m) a
+instance MSet m a => MSet m (IO a) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = fmact
+#endif
 
-instance {-# OVERLAPPING #-} MSet m b => MSet (S m) (Endo b)
+instance MSet m b => MSet m (a -> b) where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = fmact
+#endif
 
-instance Monoid m => MSet (Sum Natural) m
+instance MSet (Endo a) a where
+#if __GLASGOW_HASKELL__ <= 822
+    mact = appEndo
+#endif
 
-instance MSet m a => MSet m (Const a b)
+instance {-# OVERLAPPABLE #-} MSet m a => MSet (S m) a where
+#if __GLASGOW_HASKELL__ <= 822
+    S m `mact` a = m `mact` a
+#endif
 
-instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Product f h a)
+instance {-# OVERLAPPING #-} MSet m b => MSet (S m) (Endo b) where
+#if __GLASOW_HASKELL__ <= 822
+    mact m (Endo f) = Endo $ mact m . f
+#endif
 
-instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Sum f h a)
+instance Monoid m => MSet (Sum Natural) m where
+#if __GLASOW_HASKELL__ <= 822
+    mact (Sum 0) _ = mempty
+    mact (Sum n) s = s `mappend` mact (Sum (n - 1)) s
+#endif
 
+instance MSet m a => MSet m (Const a b) where
+#if __GLASOW_HASKELL__ <= 822
+    mact s (Const a) = Const $ s `mact` a
+#endif
+
+instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Product f h a) where
+#if __GLASOW_HASKELL__ <= 822
+    mact = fmact 
+#endif
+
+instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Sum f h a) where
+#if __GLASOW_HASKELL__ <= 822
+    mact = fmact 
+#endif
+
 newtype FreeMSet m a = FreeMSet { runFreeMSet :: (m, a) }
     deriving (Show, Ord, Eq, Functor)
 
@@ -119,14 +212,18 @@
     pure  = returnFree
     (<*>) = ap
 
-instance Monoid m => Monad (FreeMSet m) where
+instance ( Monoid m
+         ) => Monad (FreeMSet m) where
     return = returnFree
     (>>=)  = bindFree
 
 instance Semigroup m => SSet m (FreeMSet m a) where
-    act m (FreeMSet (h, a)) = FreeMSet $ (m <> h, a)
+    act m (FreeMSet (h, a)) = FreeMSet (m <> h, a)
 
-instance Monoid m => MSet m (FreeMSet m a)
+instance Monoid m => MSet m (FreeMSet m a) where
+#if __GLASOW_HASKELL__ <= 822
+    mact m (FreeMSet (h, a)) = FreeMSet (m `mappend` h, a)
+#endif
 
 -- |
 -- @'foldrFree'@ for @'FreeMSet'@
@@ -135,8 +232,9 @@
 
 type instance AlgebraType0 (FreeMSet m) a = ()
 type instance AlgebraType  (FreeMSet m) a = MSet m a
-instance Monoid m => FreeAlgebra (FreeMSet m) where
+instance ( Monoid m
+         ) => FreeAlgebra (FreeMSet m) where
     returnFree a = FreeMSet (mempty, a)
-    foldMapFree f (FreeMSet (m, a)) = act m (f a)
-    proof  = Proof Dict
-    forget = Proof Dict
+    foldMapFree f (FreeMSet (m, a)) = mact m (f a)
+    codom  = proof
+    forget = proof
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
@@ -5,7 +5,6 @@
     , fromNonEmpty
     ) where
 
-import           Data.Constraint (Dict (..))
 import           Data.IntSet (IntSet)
 import           Data.List.NonEmpty (NonEmpty)
 import qualified Data.List.NonEmpty as NE
@@ -13,7 +12,7 @@
 import qualified Data.Map as Map
 import           Data.Set (Set)
 import           Data.Semigroup
-    ( Semigroup
+    ( Semigroup (..)
     , All
     , Any
     , Dual
@@ -29,7 +28,7 @@
     ( AlgebraType
     , AlgebraType0
     , FreeAlgebra (..)
-    , Proof (..)
+    , proof
     )
 
 -- |
@@ -66,7 +65,7 @@
 -- |
 -- Free abelian semigroup is isomorphic to a non empty map with keys @a@ and
 -- values positive natural numbers.
-newtype FreeAbelianSemigroup a = FreeAbelianSemigroup { runFreeAbelianSemigroup :: Map a Integer }
+newtype FreeAbelianSemigroup a = FreeAbelianSemigroup (Map a Integer)
     deriving (Ord, Eq, Show)
 
 toNonEmpty :: FreeAbelianSemigroup a -> NonEmpty (a, Integer)
@@ -99,7 +98,7 @@
         replicate_ a n = a : replicate_ a (n - 1)                             
 
         toNonEmpty_ :: Map a Integer -> NonEmpty a
-        toNonEmpty_ = NE.fromList . concat . map (uncurry replicate_) . Map.toList
+        toNonEmpty_ = NE.fromList . concatMap (uncurry replicate_) . Map.toList
 
-    proof  = Proof Dict
-    forget = Proof Dict
+    codom  = proof
+    forget = proof
diff --git a/src/Data/Semigroup/SSet.hs b/src/Data/Semigroup/SSet.hs
--- a/src/Data/Semigroup/SSet.hs
+++ b/src/Data/Semigroup/SSet.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {- |
     Actions of [semigroup](https://en.wikipedia.org/wiki/Semigroup_action) (SSet).
  -}
@@ -8,7 +9,7 @@
     , S (..)
     ) where
 
-import           Data.Semigroup (Endo (..), Sum (..))
+import           Data.Semigroup (Semigroup (..), Endo (..), Sum (..))
 import           Data.Functor.Const (Const (..))
 import           Data.Functor.Identity (Identity (..))
 import qualified Data.Functor.Product as Functor (Product)
@@ -17,7 +18,7 @@
 import           Data.List.NonEmpty (NonEmpty)
 import qualified Data.List.NonEmpty as NE
 import           Data.Natural (Natural)
-import           Data.Ord (Down)
+import           Data.Ord (Down (..))
 import           Data.Set (Set)
 import qualified Data.Set as Set
 
@@ -38,7 +39,7 @@
 rep :: SSet s a => s -> Endo a
 rep s = Endo (act s)
 
-instance Semigroup s => SSet s s where
+instance {-# OVERLAPPING #-} Semigroup s => SSet s s where
     act = (<>)
 
 instance (SSet s a, SSet s b) => SSet s (a, b) where
@@ -89,7 +90,8 @@
     act = fact
 
 instance SSet s a => SSet s (Down a) where
-    act = fact 
+    act s (Down a) =  Down (act s a)
+
 instance SSet s a => SSet s (IO a) where
     act = fact
 
@@ -97,7 +99,7 @@
     act = fact
 
 instance SSet (Endo a) a where
-    act (Endo f) a = f a
+    act = appEndo
 
 -- |
 -- A newtype wrapper to avoid overlapping instances.
@@ -108,20 +110,26 @@
 
 instance Monoid m => Monoid (S m) where
     mempty = S mempty
+#if __GLASGOW_HASKELL__ <= 822
+    S s `mappend` S s' = S $ s `mappend` s'
+#endif
 
-instance {-# OVERLAPPABLE #-} SSet m a => SSet (S m) a where
-    act (S m) a = act m a
+-- instance {-# OVERLAPPABLE #-} SSet m a => SSet (S m) a where
+    -- act (S m) a = act m a
 
-instance {-# OVERLAPPABLE #-} SSet s a => SSet (S s) (Endo a) where
+-- instance {-# OVERLAPPABLE #-} SSet s a => SSet (S s) (Endo a) where
+    -- act s (Endo f) = Endo $ act s . f
+
+instance {-# OVERLAPPABLE #-} SSet s a => SSet s (Endo a) where
     act s (Endo f) = Endo $ act s . f
 
 instance Monoid s => SSet (Sum Natural) s where
     act (Sum 0) _ = mempty
-    act (Sum n) s = s <> act (Sum (n - 1)) s
+    act (Sum n) s = s `mappend` act (Sum (n - 1)) s
 
 instance Group g => SSet (Sum Integer) g where
-    act (Sum n) g | n < 0      = invert g <> act (Sum (n + 1)) g
-                  | n > 0      = g <> act (Sum (n - 1)) g
+    act (Sum n) g | n < 0      = invert g `mappend` act (Sum (n + 1)) g
+                  | n > 0      = g `mappend` act (Sum (n - 1)) g
                   | otherwise  = mempty
 
 instance SSet s a => SSet s (Const a b) where
diff --git a/src/Data/Semigroup/SemiLattice.hs b/src/Data/Semigroup/SemiLattice.hs
--- a/src/Data/Semigroup/SemiLattice.hs
+++ b/src/Data/Semigroup/SemiLattice.hs
@@ -5,11 +5,10 @@
     , toNonEmpty
     ) where
 
-import           Data.Constraint (Dict (..))
 import           Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import           Data.IntSet (IntSet)
-import           Data.Semigroup (All, Any, sconcat)
+import           Data.Semigroup (All, Any, Semigroup, sconcat)
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Void (Void)
@@ -18,7 +17,7 @@
     ( AlgebraType
     , AlgebraType0
     , FreeAlgebra (..)
-    , Proof (..)
+    , proof
     )
 import           Data.Semigroup.Abelian (AbelianSemigroup)
 
@@ -36,7 +35,7 @@
 
 -- |
 -- @'FreeSemiLattice'@ is a non empty set.
-newtype FreeSemiLattice a = FreeSemiLattice { runFreeSemiLattice :: Set a }
+newtype FreeSemiLattice a = FreeSemiLattice (Set a)
     deriving (Ord, Eq, Show, Semigroup)
 
 instance Ord a => AbelianSemigroup (FreeSemiLattice a)
@@ -55,5 +54,5 @@
     returnFree a = FreeSemiLattice $ Set.singleton a
     foldMapFree f (FreeSemiLattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as
 
-    proof  = Proof Dict
-    forget = Proof Dict
+    codom  = proof
+    forget = proof
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -5,6 +5,7 @@
 import           Control.Monad (unless)
 import           System.Exit (exitFailure)
 
+import qualified Test.Data.Group.Free (tests)
 import qualified Test.Data.Algebra.Free (tests)
 import qualified Test.Control.Algebra.Free (tests)
 
@@ -19,4 +20,5 @@
     runTests
         [ Test.Data.Algebra.Free.tests
         , Test.Control.Algebra.Free.tests
+        , Test.Data.Group.Free.tests
         ]
diff --git a/test/Test/Data/Group/Free.hs b/test/Test/Data/Group/Free.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/Group/Free.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Test.Data.Group.Free
+    ( tests
+    ) where
+
+import           Control.Monad (mapM)
+import           Data.Semigroup (Semigroup (..))
+import           Data.Group (invert)
+import           Data.DList (DList)
+import qualified Data.DList as DList
+import           Hedgehog (Property, PropertyT, Gen, property, (===))
+import qualified Hedgehog as H
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+import           Data.Group.Free (FreeGroup, fromDList, normalize)
+
+genDList :: Gen a -> Gen (DList (Either a a))
+genDList gen = do
+    as <- Gen.list (Range.linear 0 100) gen
+    DList.fromList <$> mapM
+        (\a -> do
+            b <- Gen.bool
+            if b
+            then return $ Right a
+            else return $ Left a
+        )
+        as
+
+prop_normalize :: Property
+prop_normalize = property $ do
+    as <- H.forAll (genDList Gen.bool)
+
+    normalize (normalize as) === normalize as
+    normalize (as `DList.append` rev as) === DList.empty
+    where
+    rev :: DList (Either a a) -> DList (Either a a)
+    rev = DList.foldr (\a as -> DList.snoc as (either Right Left a)) DList.empty
+
+prop_invert :: Property
+prop_invert = property $ do
+    fg <- fromDList <$> H.forAll (genDList Gen.bool)
+
+    invert (invert fg) === fg
+    invert fg <> fg    === mempty
+    fg <> invert fg    === mempty
+
+prop_unit :: Property
+prop_unit = property $ do
+    fg <- fromDList <$> H.forAll (genDList Gen.bool)
+
+    fg <> mempty       === fg
+    mempty <> fg       === fg
+
+prop_associativity :: Property
+prop_associativity = property $ do
+    fg   <- fromDList <$> H.forAll (genDList Gen.bool)
+    fg'  <- fromDList <$> H.forAll (genDList Gen.bool)
+    fg'' <- fromDList <$> H.forAll (genDList Gen.bool)
+
+    (fg <> fg') <> fg'' === fg <> (fg' <> fg'')
+
+tests :: IO Bool
+tests = H.checkParallel $$(H.discover)