diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.8.1.2
+Version:		0.8.1.3
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -193,8 +193,8 @@
 Test-Suite test
   Type:                 exitcode-stdio-1.0
   Main-is:		Data_Test.hs
-  hs-source-dirs:	testsuite/tests examples
-  Build-Depends:        compdata, base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, 
+  hs-source-dirs:	testsuite/tests examples src
+  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, 
                         HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive,
                         th-expand-syns, deepseq, transformers
 
diff --git a/src/Data/Comp.hs b/src/Data/Comp.hs
--- a/src/Data/Comp.hs
+++ b/src/Data/Comp.hs
@@ -18,10 +18,10 @@
      module X
     ) where
 
-import Data.Comp.Term as X
 import Data.Comp.Algebra as X
-import Data.Comp.Sum as X
 import Data.Comp.Annotation as X
 import Data.Comp.Equality as X
-import Data.Comp.Ordering as X
 import Data.Comp.Generic as X
+import Data.Comp.Ordering as X
+import Data.Comp.Sum as X
+import Data.Comp.Term as X
diff --git a/src/Data/Comp/Algebra.hs b/src/Data/Comp/Algebra.hs
--- a/src/Data/Comp/Algebra.hs
+++ b/src/Data/Comp/Algebra.hs
@@ -1,5 +1,10 @@
-{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
-  FlexibleContexts, CPP #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Algebra
@@ -21,7 +26,7 @@
       cata,
       cata',
       appCxt,
-      
+
       -- * Monadic Algebras & Catamorphisms
       AlgM,
       algM,
@@ -104,12 +109,12 @@
       futuM
     ) where
 
-import Data.Comp.Term
+import Control.Monad hiding (mapM, sequence)
 import Data.Comp.Ops
+import Data.Comp.Term
 import Data.Traversable
-import Control.Monad hiding (sequence, mapM)
 
-import Prelude hiding (sequence, mapM)
+import Prelude hiding (mapM, sequence)
 
 
 
@@ -127,13 +132,13 @@
           run (Term t) = f (fmap run t)
 
 {-| Construct a catamorphism from the given algebra. -}
-cata :: forall f a . (Functor f) => Alg f a -> Term f -> a 
+cata :: forall f a . (Functor f) => Alg f a -> Term f -> a
 {-# NOINLINE [1] cata #-}
 -- cata f = free f undefined
 -- the above definition is safe since terms do not contain holes
 --
 -- a direct implementation:
-cata f = run 
+cata f = run
     where run :: Term f -> a
           run  = f . fmap run . unTerm
 
@@ -157,7 +162,7 @@
 {-| This type represents a monadic algebra. It is similar to 'Alg' but
 the return type is monadic.  -}
 
-type AlgM m f a = f a -> m a 
+type AlgM m f a = f a -> m a
 
 {-| Convert a monadic algebra into an ordinary algebra with a monadic
   carrier. -}
@@ -175,7 +180,7 @@
           run (Term t) = algm =<< mapM run t
 
 {-| Construct a monadic catamorphism from the given monadic algebra. -}
-cataM :: forall f m a. (Traversable f, Monad m) => AlgM m f a -> Term f -> m a 
+cataM :: forall f m a. (Traversable f, Monad m) => AlgM m f a -> Term f -> m a
 {-# NOINLINE [1] cataM #-}
 -- cataM = cata . algM
 cataM algm = run
@@ -351,7 +356,7 @@
 initial term algebra to the given term algebra. -}
 homMD :: forall f g m . (Traversable f, Functor g, Monad m)
           => HomMD m f g -> CxtFunM m f g
-homMD f = run 
+homMD f = run
     where run :: Cxt h f a -> m (Cxt h g a)
           run (Hole x) = return (Hole x)
           run (Term t) = liftM appCxt (f (fmap run t))
@@ -379,7 +384,7 @@
 {-| This function applies a signature function to the given context. -}
 appSigFunMD :: forall f g m . (Traversable f, Functor g, Monad m)
               => SigFunMD m f g -> CxtFunM m f g
-appSigFunMD f = run 
+appSigFunMD f = run
     where run :: Cxt h f a -> m (Cxt h g a)
           run (Hole x) = return (Hole x)
           run (Term t) = liftM Term (f (fmap run t))
@@ -466,7 +471,7 @@
 {-| Construct a monadic anamorphism from the given monadic coalgebra. -}
 anaM :: forall a m f. (Traversable f, Monad m)
           => CoalgM m f a -> a -> m (Term f)
-anaM f = run 
+anaM f = run
     where run :: a -> m (Term f)
           run t = liftM Term $ f t >>= mapM run
 
@@ -488,7 +493,7 @@
 type RAlgM m f a = f (Term f, a) -> m a
 
 {-| Construct a monadic paramorphism from the given monadic r-algebra. -}
-paraM :: (Traversable f, Monad m) => 
+paraM :: (Traversable f, Monad m) =>
          RAlgM m f a -> Term f -> m a
 paraM f = liftM snd . cataM run
     where run t = do
@@ -504,7 +509,7 @@
 
 {-| Construct an apomorphism from the given r-coalgebra. -}
 apo :: (Functor f) => RCoalg f a -> a -> Term f
-apo f = run 
+apo f = run
     where run = Term . fmap run' . f
           run' (Left t) = t
           run' (Right a) = run a
@@ -521,7 +526,7 @@
 {-| Construct a monadic apomorphism from the given monadic r-coalgebra. -}
 apoM :: (Traversable f, Monad m) =>
         RCoalgM m f a -> a -> m (Term f)
-apoM f = run 
+apoM f = run
     where run a = do
             t <- f a
             t' <- mapM run' t
@@ -714,7 +719,7 @@
 
   "appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.
     appHom a (appHom' h x) = appHom' (compHom a h) x;
-    
+
   "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
     appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;
 
@@ -738,7 +743,7 @@
 
   "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
     appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;
-    
+
   "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
     appSigFun f (appHom g x) = appSigFunHom f g x;
 
@@ -750,7 +755,7 @@
 
   "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
     appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;
-    
+
   "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
                                       (h :: SigFun f1 f2) x.
     appSigFunHom f g (appSigFun h x)
@@ -792,7 +797,7 @@
     appSigFunHom f1 f2 (appSigFunHom f3 f4 x)
       = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x; #-}
 
-{-# RULES 
+{-# RULES
   "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
      appHomM h x >>= cataM a =  appAlgHomM a h x;
 
diff --git a/src/Data/Comp/Annotation.hs b/src/Data/Comp/Annotation.hs
--- a/src/Data/Comp/Annotation.hs
+++ b/src/Data/Comp/Annotation.hs
@@ -1,6 +1,12 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables, FlexibleContexts,
-  ConstraintKinds #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Annotation
@@ -35,15 +41,13 @@
      project'
     ) where
 
-import Data.Comp.Term
-import Data.Comp.Sum
-import Data.Comp.Ops
+import Control.Monad
 import Data.Comp.Algebra
 import Data.Comp.Automata
 import Data.Comp.MacroAutomata
-import Control.Monad
-import Data.Traversable
 import Data.Comp.Number
+import Data.Comp.Ops
+import Data.Comp.Term
 
 
 {-| Transform a function with a domain constructed from a functor to a function
@@ -59,14 +63,14 @@
        => (s' a -> Cxt h s' a) -> s a -> Cxt h s a
 liftA' f v = let (v',p) = projectA v
              in ann p (f v')
-    
+
 {-| Strip the annotations from a term over a functor with annotations. -}
 stripA :: (RemA g f, Functor g) => CxtFun g f
 stripA = appSigFun remA
 
 {-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism
  over the same signatures, but extended with annotations. -}
-propAnn :: (DistAnn f p f', DistAnn g p g', Functor g) 
+propAnn :: (DistAnn f p f', DistAnn g p g', Functor g)
         => Hom f g -> Hom f' g'
 propAnn hom f' = ann p (hom f)
     where (f,p) = projectA f'
@@ -75,7 +79,7 @@
 -- | Lift a stateful term homomorphism over signatures @f@ and @g@ to
 -- a stateful term homomorphism over the same signatures, but extended with
 -- annotations.
-propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g) 
+propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g)
         => QHom f q g -> QHom f' q g'
 propAnnQ hom f' = ann p (hom f)
     where (f,p) = projectA f'
@@ -83,7 +87,7 @@
 -- | Lift a bottom-up tree transducer over signatures @f@ and @g@ to a
 -- bottom-up tree transducer over the same signatures, but extended
 -- with annotations.
-propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g) 
+propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g)
         => UpTrans f q g -> UpTrans f' q g'
 propAnnUp trans f' = (q, ann p t)
     where (f,p) = projectA f'
@@ -92,7 +96,7 @@
 -- | Lift a top-down tree transducer over signatures @f@ and @g@ to a
 -- top-down tree transducer over the same signatures, but extended
 -- with annotations.
-propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) 
+propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g)
         => DownTrans f q g -> DownTrans f' q g'
 propAnnDown trans q f' = ann p (trans q f)
     where (f,p) = projectA f'
@@ -100,7 +104,7 @@
 -- | Lift a macro tree transducer over signatures @f@ and @g@ to a
 -- macro tree transducer over the same signatures, but extended
 -- with annotations.
-propAnnMacro :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) 
+propAnnMacro :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g)
         => MacroTrans f q g -> MacroTrans f' q g'
 propAnnMacro trans q f' = ann p (trans q (fmap ann' f))
     where (f,p) = projectA f'
@@ -109,16 +113,16 @@
 -- | Lift a macro tree transducer with regular look-ahead over
 -- signatures @f@ and @g@ to a macro tree transducer with regular
 -- look-ahead over the same signatures, but extended with annotations.
-propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) 
+propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g)
                 => MacroTransLA f q p g -> MacroTransLA f' q p g'
 propAnnMacroLA trans q p f' = ann an (trans q p (fmap ann' f))
     where (f,an) = projectA f'
-          ann' (s,p) = (\q' -> s (fmap (ann an) q'), p)
+          ann' (s,p) = (s . fmap (ann an), p)
 
 
 {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic
   term homomorphism over the same signatures, but extended with annotations. -}
-propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m) 
+propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m)
          => HomM m f g -> HomM m f' g'
 propAnnM hom f' = liftM (ann p) (hom f)
     where (f,p) = projectA f'
diff --git a/src/Data/Comp/Arbitrary.hs b/src/Data/Comp/Arbitrary.hs
--- a/src/Data/Comp/Arbitrary.hs
+++ b/src/Data/Comp/Arbitrary.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE TypeOperators, TypeSynonymInstances, GADTs, TemplateHaskell, FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Arbitrary
@@ -17,13 +21,12 @@
     ( ArbitraryF(..)
     )where
 
-import Test.QuickCheck
-import Data.Comp.Term
-import Data.Comp.Sum
-import Data.Comp.Ops
-import Data.Comp.Derive.Utils
-import Data.Comp.Derive
 import Control.Applicative
+import Data.Comp.Derive
+import Data.Comp.Derive.Utils
+import Data.Comp.Ops
+import Data.Comp.Term
+import Test.QuickCheck
 
 {-| This lifts instances of 'ArbitraryF' to instances of 'Arbitrary'
 for the corresponding term type. -}
@@ -39,7 +42,7 @@
     shrinkF (v :&: p) = tail [v' :&: p'| v' <- v: shrinkF v, p' <- p : shrink p ]
 
 {-|
-  This lifts instances of 'ArbitraryF' to instances of 'ArbitraryF' for 
+  This lifts instances of 'ArbitraryF' to instances of 'ArbitraryF' for
   the corresponding context functor.
 -}
 instance (ArbitraryF f) => ArbitraryF (Context f) where
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE Rank2Types, FlexibleContexts, ImplicitParams, GADTs, TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs            #-}
+{-# LANGUAGE ImplicitParams   #-}
+{-# LANGUAGE Rank2Types       #-}
+{-# LANGUAGE TypeOperators    #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -14,7 +18,7 @@
 -- a state that is maintained separately by a bottom-up or top-down
 -- state transformation. Additionally, this module also provides
 -- combinators to run state transformations themselves.
--- 
+--
 -- Like regular term homomorphisms also stateful homomorphisms (as
 -- well as transducers) can be lifted to annotated signatures
 -- (cf. "Data.Comp.Annotation").
@@ -98,10 +102,10 @@
     , module Data.Comp.Automata.Product
     ) where
 
-import Data.Comp.Number
+import Data.Comp.Algebra
 import Data.Comp.Automata.Product
+import Data.Comp.Number
 import Data.Comp.Term
-import Data.Comp.Algebra
 import Data.Map (Map)
 import qualified Data.Map as Map
 
@@ -150,14 +154,14 @@
 -- | This type represents stateful term homomorphisms. Stateful term
 -- homomorphisms have access to a state that is provided (separately)
 -- by a bottom-up or top-down state transformation function (or both).
-                           
+
 type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
 
 
 -- | This function turns a stateful homomorphism with a fully
 -- polymorphic state type into a (stateless) homomorphism.
 pureHom :: (forall q . QHom f q g) -> Hom f g
-pureHom phom t = let ?above = undefined 
+pureHom phom t = let ?above = undefined
                      ?below = const undefined
                  in phom t
 
@@ -183,7 +187,7 @@
 -- algebra.
 
 upAlg :: (Functor g)  => UpTrans f q g -> Alg f (q, Term g)
-upAlg trans = fmap appCxt . trans 
+upAlg trans = fmap appCxt . trans
 
 -- | This function runs the given UTT on the given term.
 
@@ -205,7 +209,7 @@
     run (Term t) = fmap appCxt $ trans $ fmap run t
 
 -- | This function composes two UTTs. (see TATA, Theorem 6.4.5)
-    
+
 compUpTrans :: (Functor f, Functor g, Functor h)
                => UpTrans g p h -> UpTrans f q g -> UpTrans f (q,p) h
 compUpTrans t2 t1 x = ((q1,q2), c2) where
@@ -214,7 +218,7 @@
 
 
 -- | This function composes a UTT with an algebra.
-    
+
 compAlgUpTrans :: (Functor g)
                => Alg g a -> UpTrans f q g -> Alg f (q,a)
 compAlgUpTrans alg trans = fmap (cata' alg) . trans
@@ -227,7 +231,7 @@
     (q, x') = trans x
 
 -- | This combinator composes a signature function followed by a UTT.
-    
+
 compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h
 compUpTransSig trans sig = trans . sig
 
@@ -238,7 +242,7 @@
     (q, x') = trans x
 
 -- | This combinator composes a homomorphism followed by a UTT.
-    
+
 compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h
 compUpTransHom trans hom x  = runUpTrans' trans . hom $ x
 
@@ -268,7 +272,7 @@
 
 -- | This function constructs a UTT from a given stateful term
 -- homomorphism with the state propagated by the given UTA.
-    
+
 upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g
 upTrans st f t = (q, c)
     where q = st $ fmap fst t
@@ -276,7 +280,7 @@
 
 -- | This function applies a given stateful term homomorphism with
 -- a state space propagated by the given UTA to a term.
-          
+
 runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g
 runUpHom st hom = snd . runUpHomSt st hom
 
@@ -306,7 +310,7 @@
 upState f s = res where res = explicit f res id s
 
 -- | This combinator runs a GUTA on a term.
-                        
+
 runDUpState :: Functor f => DUpState f q q -> Term f -> q
 runDUpState = runUpState . upState
 
@@ -347,15 +351,15 @@
     run (Hole a) _ = Hole a
 
 -- | This function runs the given DTT on the given tree.
-    
+
 runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f (q -> a) -> Cxt h g a
 runDownTrans' tr q t = run t q where
-    run (Term t) q = appCxt $ tr q $ fmap run $ t
+    run (Term t) q = appCxt $ tr q $ fmap run t
     run (Hole a) q = Hole (a q)
 
 -- | This function composes two DTTs. (see W.C. Rounds /Mappings and
 -- grammars on trees/, Theorem 2.)
-    
+
 compDownTrans :: (Functor f, Functor g, Functor h)
               => DownTrans g p h -> DownTrans f q g -> DownTrans f (q,p) h
 compDownTrans t2 t1 (q,p) t = runDownTrans' t2  p $ t1 q (fmap curry t)
@@ -426,17 +430,17 @@
 -- | Apply the given state mapping to the given functorial value by
 -- adding the state to the corresponding index if it is in the map and
 -- otherwise adding the provided default state.
-          
+
 appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
                        -> q -> f (q -> b) -> f (q,b)
 appMap qmap q s = fmap qfun s'
     where s' = number s
           qfun k@(Numbered (_,a)) = let q' = Map.findWithDefault q k (qmap s')
-                                    in (q', a q') 
+                                    in (q', a q')
 
 -- | This function constructs a DTT from a given stateful term--
 -- homomorphism with the state propagated by the given DTA.
-          
+
 downTrans :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> DownTrans f q g
 downTrans st f q s = fmap snd $ explicit f q fst (appMap (curry st q) q s)
 
@@ -473,7 +477,7 @@
 
 -- | This combinator constructs the product of two dependant top-down
 -- state transformations.
-          
+
 prodDDownState :: (p :< c, q :< c)
                => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
 prodDDownState sp sq t = prodMap above above (sp t) (sq t)
@@ -492,7 +496,7 @@
 runDState :: Traversable f => DUpState' f (u,d) u -> DDownState' f (u,d) d -> d -> Term f -> u
 runDState up down d (Term t) = u where
         t' = fmap bel $ number t
-        bel (Numbered (i,s)) = 
+        bel (Numbered (i,s)) =
             let d' = Map.findWithDefault d (Numbered (i,undefined)) m
             in Numbered (i, (runDState up down d' s, d'))
         m = explicit down (u,d) unNumbered t'
@@ -501,14 +505,14 @@
 -- | This combinator runs a stateful term homomorphisms with a state
 -- space produced both on a bottom-up and a top-down state
 -- transformation.
-        
+
 runQHom :: (Traversable f, Functor g) =>
-           DUpState' f (u,d) u -> DDownState' f (u,d) d -> 
+           DUpState' f (u,d) u -> DDownState' f (u,d) d ->
            QHom f (u,d) g ->
            d -> Term f -> (u, Term g)
 runQHom up down trans d (Term t) = (u,t'') where
         t' = fmap bel $ number t
-        bel (Numbered (i,s)) = 
+        bel (Numbered (i,s)) =
             let d' = Map.findWithDefault d (Numbered (i,undefined)) m
                 (u', s') = runQHom up down trans d' s
             in Numbered (i, ((u', d'),s'))
diff --git a/src/Data/Comp/Automata/Product.hs b/src/Data/Comp/Automata/Product.hs
--- a/src/Data/Comp/Automata/Product.hs
+++ b/src/Data/Comp/Automata/Product.hs
@@ -1,6 +1,13 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-IncoherentInstances, TemplateHaskell, ScopedTypeVariables, DataKinds, TypeFamilies,
-UndecidableInstances, GADTs, ConstraintKinds, FlexibleContexts, PolyKinds #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Automata.Product
diff --git a/src/Data/Comp/Automata/Product/Derive.hs b/src/Data/Comp/Automata/Product/Derive.hs
--- a/src/Data/Comp/Automata/Product/Derive.hs
+++ b/src/Data/Comp/Automata/Product/Derive.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeOperators         #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Automata.Product.Derive
@@ -33,7 +35,7 @@
     where dirs = genDirs (n-1)
 
 genInst :: [Dir] -> Q Dec
-genInst dir = do 
+genInst dir = do
   n <- newName "a"
   ty <- genType n dir
   ex <- genEx dir
@@ -43,7 +45,7 @@
 genType n = gen
     where gen [] = varT n
           gen (L:dir) =  gen dir `pairT` (varT =<< newName "a")
-          gen (R:dir) =  (varT =<< newName "a") `pairT` gen dir 
+          gen (R:dir) =  (varT =<< newName "a") `pairT` gen dir
 
 genPat :: Name -> [Dir] -> PatQ
 genPat n = gen where
@@ -60,13 +62,13 @@
 genPatExp :: Name -> [Dir] -> Q (Pat, Exp)
 genPatExp n = gen where
     gen [] = return (WildP, VarE n)
-    gen (d:dir) = do 
-      (p,e) <- gen dir 
+    gen (d:dir) = do
+      (p,e) <- gen dir
       x <- newName "x"
       return $ case d of
         L -> (TupP [p,VarP x] , TupE [e,VarE x])
         R -> (TupP [VarP x,p] , TupE [VarE x,e])
-  
+
 
 
 pairT :: TypeQ -> TypeQ -> TypeQ
diff --git a/src/Data/Comp/Decompose.hs b/src/Data/Comp/Decompose.hs
--- a/src/Data/Comp/Decompose.hs
+++ b/src/Data/Comp/Decompose.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/DeepSeq.hs b/src/Data/Comp/DeepSeq.hs
--- a/src/Data/Comp/DeepSeq.hs
+++ b/src/Data/Comp/DeepSeq.hs
@@ -1,5 +1,8 @@
-{-# LANGUAGE GADTs, FlexibleContexts, FlexibleInstances, TypeOperators,
-  TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE TypeOperators     #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.DeepSeq
@@ -20,10 +23,10 @@
     )
     where
 
-import Data.Comp.Term
 import Control.DeepSeq
-import Data.Comp.Derive
 import Data.Comp.Annotation
+import Data.Comp.Derive
+import Data.Comp.Term
 
 
 instance (NFDataF f, NFData a) => NFData (Cxt h f a) where
diff --git a/src/Data/Comp/Derive.hs b/src/Data/Comp/Derive.hs
--- a/src/Data/Comp/Derive.hs
+++ b/src/Data/Comp/Derive.hs
@@ -48,24 +48,24 @@
      liftSum
     ) where
 
-import Control.DeepSeq (NFData(..))
-import Data.Comp.Derive.Utils (derive, liftSumGen)
-import Data.Comp.Derive.HaskellStrict
-import Data.Comp.Derive.Foldable
-import Data.Comp.Derive.Traversable
+import Control.DeepSeq (NFData (..))
+import Data.Comp.Derive.Arbitrary
 import Data.Comp.Derive.DeepSeq
-import Data.Comp.Derive.Show
-import Data.Comp.Derive.Ordering
 import Data.Comp.Derive.Equality
-import Data.Comp.Derive.Arbitrary
-import Data.Comp.Derive.SmartConstructors
+import Data.Comp.Derive.Foldable
+import Data.Comp.Derive.HaskellStrict
+import Data.Comp.Derive.Ordering
+import Data.Comp.Derive.Show
 import Data.Comp.Derive.SmartAConstructors
+import Data.Comp.Derive.SmartConstructors
+import Data.Comp.Derive.Traversable
+import Data.Comp.Derive.Utils (derive, liftSumGen)
 import Data.Comp.Ops ((:+:), caseF)
 
 import Language.Haskell.TH
 
-import qualified Data.DeriveTH as D
 import qualified Data.Derive.All as A
+import qualified Data.DeriveTH as D
 
 {-| Derive an instance of 'Functor' for a type constructor of any first-order
   kind taking at least one argument. -}
diff --git a/src/Data/Comp/Derive/Arbitrary.hs b/src/Data/Comp/Derive/Arbitrary.hs
--- a/src/Data/Comp/Derive/Arbitrary.hs
+++ b/src/Data/Comp/Derive/Arbitrary.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE GADTs, TemplateHaskell #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE TemplateHaskell #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Derive.Arbitrary
@@ -20,10 +21,10 @@
      makeArbitrary
     )where
 
-import Test.QuickCheck
 import Data.Comp.Derive.Utils hiding (derive)
-import Language.Haskell.TH
 import qualified Data.DeriveTH as D
+import Language.Haskell.TH
+import Test.QuickCheck
 
 {-| Derive an instance of 'Arbitrary' for a type constructor. -}
 makeArbitrary :: Name -> Q [Dec]
@@ -64,7 +65,7 @@
 {-|
   This function generates a declaration of a generator having the given name using
   the given constructors, i.e., something like this:
-  
+
   @
   \<name\> :: Gen \<type\>
   \<name\> = ...
@@ -96,10 +97,10 @@
                    let build = doE $
                                binds ++
                                [noBindS [|return $apps|]]
-                   if n == 0 
+                   if n == 0
                       then [|return $apps|]
                       else  [| sized $ \ size ->
-                                 $(letE [valD 
+                                 $(letE [valD
                                          newSizeP
                                          (normalB [|((size - 1) `div` $constrsE ) `max` 0|])
                                          [] ]
diff --git a/src/Data/Comp/Derive/DeepSeq.hs b/src/Data/Comp/Derive/DeepSeq.hs
--- a/src/Data/Comp/Derive/DeepSeq.hs
+++ b/src/Data/Comp/Derive/DeepSeq.hs
@@ -41,10 +41,10 @@
   rnfFDecl <- funD 'rnfF (rnfFClauses constrs')
   return [InstanceD preCond classType [rnfFDecl]]
       where rnfFClauses = map genRnfFClause
-            genRnfFClause (constr, args) = do 
+            genRnfFClause (constr, args) = do
               let n = length args
               varNs <- newNames n "x"
               let pat = ConP constr $ map VarP varNs
-                  allVars = map varE varNs 
+                  allVars = map varE varNs
               body <- foldr (\ x y -> [|rnf $x `seq` $y|]) [| () |] allVars
               return $ Clause [pat] (NormalB body) []
diff --git a/src/Data/Comp/Derive/Equality.hs b/src/Data/Comp/Derive/Equality.hs
--- a/src/Data/Comp/Derive/Equality.hs
+++ b/src/Data/Comp/Derive/Equality.hs
@@ -43,7 +43,7 @@
             defEqClause constrs
                 | length constrs  < 2 = []
                 | otherwise = [clause [wildP,wildP] (normalB [|False|]) []]
-            genEqClause (constr, n) = do 
+            genEqClause (constr, n) = do
               varNs <- newNames n "x"
               varNs' <- newNames n "y"
               let pat = ConP constr $ map VarP varNs
@@ -53,7 +53,7 @@
                   mkEq x y = let (x',y') = (return x,return y)
                              in [| $x' == $y'|]
                   eqs = listE $ zipWith mkEq vars vars'
-              body <- if n == 0 
+              body <- if n == 0
                       then [|True|]
                       else [|and $eqs|]
               return $ Clause [pat, pat'] (NormalB body) []
diff --git a/src/Data/Comp/Derive/Foldable.hs b/src/Data/Comp/Derive/Foldable.hs
--- a/src/Data/Comp/Derive/Foldable.hs
+++ b/src/Data/Comp/Derive/Foldable.hs
@@ -18,23 +18,22 @@
      makeFoldable
     ) where
 
+import Control.Monad
 import Data.Comp.Derive.Utils
-import Language.Haskell.TH
 import Data.Foldable
-import Control.Monad
-import Data.Monoid
 import Data.Maybe
-import qualified Prelude as P (foldl,foldr,foldl1,foldr1)
-import Prelude hiding  (foldl,foldr,foldl1,foldr1)
+import Data.Monoid
+import Language.Haskell.TH
+import Prelude hiding (foldl, foldl1, foldr, foldr1)
+import qualified Prelude as P (foldl, foldl1, foldr, foldr1)
 
 
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
 
-iter' n f e = run n f e
-    where run 0 _ e = e
-          run m f e = let f' = iter (m-1) [|fmap|] f
-                        in run (m-1) f (f' `appE` e)
+iter' 0 _ e = e
+iter' m f e = let f' = iter (m-1) [|fmap|] f
+              in iter' (m-1) f (f' `appE` e)
 
 {-| Derive an instance of 'Foldable' for a type constructor of any first-order
   kind taking at least one argument. -}
@@ -78,7 +77,7 @@
                        fp = if null vars then WildP else VarP fn
                    body <- case vars of
                              [] -> [|mempty|]
-                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $ 
+                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $
                                       map (\ (d,z) -> iter' (max (d-1) 0) [|fold|] (f' d `appE` z)) vars
                    return $ Clause [fp, pat] (NormalB body) []
             foldlClause (pat,vars) =
@@ -114,11 +113,11 @@
                    let f = varE fn
                        fp = case vars of
                               (d,_):r
-                                  | d > 0 || not (null r) -> VarP fn                              
-                              _ -> WildP 
+                                  | d > 0 || not (null r) -> VarP fn
+                              _ -> WildP
                        mkComp (d,x) = iter' d [|foldl1 $f|] x
-                   body <- case vars of 
-                             [] -> [|undefined|] 
+                   body <- case vars of
+                             [] -> [|undefined|]
                              _ -> P.foldl1 (\ x y -> [|$f $x $y|]) $ map mkComp vars
                    return $ Clause [fp, pat] (NormalB body) []
             foldr1Clause (pat,vars) =
@@ -126,10 +125,10 @@
                    let f = varE fn
                        fp = case vars of
                               (d,_):r
-                                  | d > 0 || not (null r) -> VarP fn                              
-                              _ -> WildP 
+                                  | d > 0 || not (null r) -> VarP fn
+                              _ -> WildP
                        mkComp (d,x) = iter' d [|foldr1 $f|] x
-                   body <- case vars of 
-                             [] -> [|undefined|] 
+                   body <- case vars of
+                             [] -> [|undefined|]
                              _ -> P.foldr1 (\ x y -> [|$f $x $y|]) $ map mkComp vars
                    return $ Clause [fp, pat] (NormalB body) []
diff --git a/src/Data/Comp/Derive/HaskellStrict.hs b/src/Data/Comp/Derive/HaskellStrict.hs
--- a/src/Data/Comp/Derive/HaskellStrict.hs
+++ b/src/Data/Comp/Derive/HaskellStrict.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE TemplateHaskell, TypeOperators, CPP, FlexibleContexts, ConstraintKinds #-}
+{-# LANGUAGE CPP              #-}
+{-# LANGUAGE ConstraintKinds  #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TemplateHaskell  #-}
+{-# LANGUAGE TypeOperators    #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Derive.HaskellStrict
@@ -19,16 +23,16 @@
      , haskellStrict'
     ) where
 
+import Control.Monad hiding (mapM, sequence)
 import Data.Comp.Derive.Utils
-import Language.Haskell.TH
-import Data.Maybe
-import Data.Comp.Thunk
 import Data.Comp.Sum
+import Data.Comp.Thunk
+import Data.Foldable hiding (any, or)
+import Data.Maybe
 import Data.Traversable
-import Data.Foldable hiding (any,or)
-import Control.Monad hiding (mapM, sequence)
-import qualified Prelude as P (foldl, foldr, mapM, all)
-import Prelude hiding  (foldl, foldr,mapM, sequence)
+import Language.Haskell.TH
+import Prelude hiding (foldl, foldr, mapM, sequence)
+import qualified Prelude as P (all, foldl, foldr, mapM)
 
 
 class HaskellStrict f where
@@ -70,7 +74,7 @@
      xn <- newName "x"
      doThunk <- [|thunk|]
      let sequenceDecl = FunD 'thunkSequence sc'
-         injectDecl = FunD 'thunkSequenceInject [Clause [VarP xn] (NormalB (doThunk `AppE` CaseE (VarE xn) matchPat)) []] 
+         injectDecl = FunD 'thunkSequenceInject [Clause [VarP xn] (NormalB (doThunk `AppE` CaseE (VarE xn) matchPat)) []]
          injectDecl' = FunD 'thunkSequenceInject' ic'
      return [InstanceD [] classType [sequenceDecl, injectDecl, injectDecl']]
       where isFarg fArg (constr, args) = (constr, map (containsStr fArg) args)
@@ -91,7 +95,7 @@
                        fvars = catMaybes $ filterVars args varNs (curry Just) (const Nothing)
                        allVars = map varE varNs
                        conAp = P.foldl appE (conE constr) allVars
-                       conBind (d, x) y = [| $(deepThunk d `appE` (varE x))  >>= $(lamE [varP x] y)|]
+                       conBind (d, x) y = [| $(deepThunk d `appE` varE x)  >>= $(lamE [varP x] y)|]
                    bodySC' <- P.foldr conBind [|return $conAp|] fvars
                    let sc' = Clause [pat] (NormalB bodySC') []
                    bodyMatch <- case fvars of
diff --git a/src/Data/Comp/Derive/Ordering.hs b/src/Data/Comp/Derive/Ordering.hs
--- a/src/Data/Comp/Derive/Ordering.hs
+++ b/src/Data/Comp/Derive/Ordering.hs
@@ -20,8 +20,8 @@
 import Data.Comp.Derive.Equality
 import Data.Comp.Derive.Utils
 
-import Data.Maybe
 import Data.List
+import Data.Maybe
 import Language.Haskell.TH hiding (Cxt)
 
 {-| Signature ordering. An instance @OrdF f@ gives rise to an instance
@@ -29,7 +29,7 @@
 class EqF f => OrdF f where
     compareF :: Ord a => f a -> f a -> Ordering
 
-    
+
 compList :: [Ordering] -> Ordering
 compList = fromMaybe EQ . find (/= EQ)
 
@@ -45,7 +45,7 @@
   eqAlgDecl <- funD 'compareF  (compareFClauses constrs)
   return [InstanceD preCond classType [eqAlgDecl]]
       where compareFClauses [] = []
-            compareFClauses constrs = 
+            compareFClauses constrs =
                 let constrs' = map abstractConType constrs `zip` [1..]
                     constPairs = [(x,y)| x<-constrs', y <- constrs']
                 in map genClause constPairs
@@ -53,7 +53,7 @@
                 | n == m = genEqClause c
                 | n < m = genLtClause c d
                 | otherwise = genGtClause c d
-            genEqClause (constr, n) = do 
+            genEqClause (constr, n) = do
               varNs <- newNames n "x"
               varNs' <- newNames n "y"
               let pat = ConP constr $ map VarP varNs
diff --git a/src/Data/Comp/Derive/SmartAConstructors.hs b/src/Data/Comp/Derive/SmartAConstructors.hs
--- a/src/Data/Comp/Derive/SmartAConstructors.hs
+++ b/src/Data/Comp/Derive/SmartAConstructors.hs
@@ -17,12 +17,12 @@
      smartAConstructors
     ) where
 
-import Language.Haskell.TH hiding (Cxt)
+import Control.Monad
+import Data.Comp.Annotation
 import Data.Comp.Derive.Utils
 import Data.Comp.Sum
 import Data.Comp.Term
-import Data.Comp.Annotation
-import Control.Monad
+import Language.Haskell.TH hiding (Cxt)
 
 {-| Derive smart constructors with products for a type constructor of any
   parametric kind taking at least one argument. The smart constructors are
diff --git a/src/Data/Comp/Derive/SmartConstructors.hs b/src/Data/Comp/Derive/SmartConstructors.hs
--- a/src/Data/Comp/Derive/SmartConstructors.hs
+++ b/src/Data/Comp/Derive/SmartConstructors.hs
@@ -12,16 +12,16 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Derive.SmartConstructors 
+module Data.Comp.Derive.SmartConstructors
     (
      smartConstructors
     ) where
 
-import Language.Haskell.TH hiding (Cxt)
+import Control.Monad
 import Data.Comp.Derive.Utils
 import Data.Comp.Sum
 import Data.Comp.Term
-import Control.Monad
+import Language.Haskell.TH hiding (Cxt)
 
 {-| Derive smart constructors for a type constructor of any first-order kind
  taking at least one argument. The smart constructors are similar to the
diff --git a/src/Data/Comp/Derive/Traversable.hs b/src/Data/Comp/Derive/Traversable.hs
--- a/src/Data/Comp/Derive/Traversable.hs
+++ b/src/Data/Comp/Derive/Traversable.hs
@@ -18,23 +18,22 @@
      makeTraversable
     ) where
 
+import Control.Applicative
+import Control.Monad hiding (mapM, sequence)
 import Data.Comp.Derive.Utils
-import Language.Haskell.TH
+import Data.Foldable hiding (any, or)
 import Data.Maybe
 import Data.Traversable
-import Data.Foldable hiding (any,or)
-import Control.Applicative
-import Control.Monad hiding (mapM, sequence)
+import Language.Haskell.TH
+import Prelude hiding (foldl, foldr, mapM, sequence)
 import qualified Prelude as P (foldl, foldr, mapM)
-import Prelude hiding  (foldl, foldr,mapM, sequence)
 
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
 
-iter' n f e = run n f e
-    where run 0 _ e = e
-          run m f e = let f' = iter (m-1) [|fmap|] f
-                        in run (m-1) f (f' `appE` e)
+iter' 0 _ e = e
+iter' m f e = let f' = iter (m-1) [|fmap|] f
+              in iter' (m-1) f (f' `appE` e)
 
 {-| Derive an instance of 'Traversable' for a type constructor of any
   first-order kind taking at least one argument. -}
diff --git a/src/Data/Comp/Derive/Utils.hs b/src/Data/Comp/Derive/Utils.hs
--- a/src/Data/Comp/Derive/Utils.hs
+++ b/src/Data/Comp/Derive/Utils.hs
@@ -15,10 +15,10 @@
 module Data.Comp.Derive.Utils where
 
 
-import Language.Haskell.TH
-import Language.Haskell.TH.Syntax
 import Control.Monad
+import Language.Haskell.TH
 import Language.Haskell.TH.ExpandSyns
+import Language.Haskell.TH.Syntax
 
 -- reportError is introduced only from version 7.6 of GHC
 #if __GLASGOW_HASKELL__ < 706
@@ -52,11 +52,11 @@
 
 
 normalCon' :: Con -> (Name,[Type])
-normalCon' = fmap (map snd) . normalCon 
+normalCon' = fmap (map snd) . normalCon
 
 -- | Same as normalCon' but expands type synonyms.
 normalConExp :: Con -> Q (Name,[Type])
-normalConExp c = do 
+normalConExp c = do
   let (n,ts) = normalCon' c
   ts' <- mapM expandSyns ts
   return (n, ts')
@@ -64,7 +64,7 @@
 
 -- | Same as normalConExp' but retains strictness annotations.
 normalConStrExp :: Con -> Q (Name,[StrictType])
-normalConStrExp c = do 
+normalConStrExp c = do
   let (n,ts) = normalCon c
   ts' <- mapM (\ (st,ty) -> do ty' <- expandSyns ty; return (st,ty')) ts
   return (n, ts')
@@ -146,7 +146,7 @@
   ClassI (ClassD _ name targs_ _ decs) _ <- reify fname
   let targs = map tyVarBndrName targs_
   splitM <- findSig targs decs
-  case splitM of 
+  case splitM of
     Nothing -> do reportError $ "Class " ++ show name ++ " cannot be lifted to sums!"
                   return []
     Just (ts1_, ts2_) -> do
@@ -167,8 +167,8 @@
               clause f = do x <- newName "x"
                             let b = NormalB (VarE caseName `AppE` VarE f `AppE` VarE f `AppE` VarE x)
                             return $ Clause [VarP x] b []
-                          
-                          
+
+
 findSig :: [Name] -> [Dec] -> Q (Maybe ([Name],[Name]))
 findSig targs decs = case map run decs of
                        []  -> return Nothing
@@ -177,7 +177,7 @@
                                     Nothing -> return Nothing
                                     Just n -> return $ splitNames n targs
   where run :: Dec -> Q (Maybe Name)
-        run (SigD _ ty) = do 
+        run (SigD _ ty) = do
           ty' <- expandSyns ty
           return $ getSig False ty'
         run _ = return Nothing
@@ -186,7 +186,7 @@
         getSig True (AppT ty _) = getSig True ty
         getSig True (VarT n) = Just n
         getSig _ _ = Nothing
-        splitNames y (x:xs) 
+        splitNames y (x:xs)
           | y == x = Just ([],xs)
           | otherwise = do (xs1,xs2) <- splitNames y xs
                            return (x:xs1,xs2)
diff --git a/src/Data/Comp/Desugar.hs b/src/Data/Comp/Desugar.hs
--- a/src/Data/Comp/Desugar.hs
+++ b/src/Data/Comp/Desugar.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, OverlappingInstances, TypeOperators, ConstraintKinds #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances  #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Desugar
diff --git a/src/Data/Comp/Equality.hs b/src/Data/Comp/Equality.hs
--- a/src/Data/Comp/Equality.hs
+++ b/src/Data/Comp/Equality.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeOperators, GADTs, TemplateHaskell #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators   #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Equality
@@ -18,14 +20,13 @@
      eqMod,
     ) where
 
-import Data.Comp.Term
-import Data.Comp.Sum
-import Data.Comp.Ops
+import Control.Monad hiding (mapM_)
 import Data.Comp.Derive.Equality
 import Data.Comp.Derive.Utils
+import Data.Comp.Ops
+import Data.Comp.Term
 import Data.Foldable
-import Control.Monad hiding (mapM_)
-import Prelude hiding (mapM_, all)
+import Prelude hiding (all, mapM_)
 
 -- instance (EqF f, Eq p) => EqF (f :*: p) where
 --    eqF (v1 :*: p1) (v2 :*: p2) = p1 == p2 && v1 `eqF` v2
diff --git a/src/Data/Comp/Generic.hs b/src/Data/Comp/Generic.hs
--- a/src/Data/Comp/Generic.hs
+++ b/src/Data/Comp/Generic.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE GADTs, ScopedTypeVariables, TypeOperators, ConstraintKinds, FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -16,16 +20,16 @@
 
 module Data.Comp.Generic where
 
-import Data.Comp.Term
-import Data.Comp.Sum
+import Control.Monad hiding (mapM)
 import Data.Comp.Algebra
 import Data.Comp.Automata
+import Data.Comp.Sum
+import Data.Comp.Term
 import Data.Foldable
 import Data.Maybe
 import Data.Traversable
 import GHC.Exts (build)
-import Control.Monad hiding (mapM)
-import Prelude hiding (foldl,mapM)
+import Prelude hiding (foldl, mapM)
 
 
 -- | This function returns the subterm of a given term at the position
@@ -87,11 +91,11 @@
 -- | Monadic version of 'transform'.
 transformM :: (Traversable f, Monad m) =>
              (Term f -> m (Term f)) -> Term f -> m (Term f)
-transformM  f = run 
+transformM  f = run
     where run t = f =<< liftM Term (mapM run $ unTerm t)
 
 query :: Foldable f => (Term f -> r) -> (r -> r -> r) -> Term f -> r
-query q c = run 
+query q c = run
     where run i@(Term t) = foldl (\s x -> s `c` run x) (q i) t
 -- query q c i@(Term t) = foldl (\s x -> s `c` query q c x) (q i) t
 
diff --git a/src/Data/Comp/MacroAutomata.hs b/src/Data/Comp/MacroAutomata.hs
--- a/src/Data/Comp/MacroAutomata.hs
+++ b/src/Data/Comp/MacroAutomata.hs
@@ -1,4 +1,7 @@
-{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.MacroAutomata
@@ -7,7 +10,7 @@
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
 -- Portability :  non-portable (GHC Extensions)
--- 
+--
 -- This module defines macro tree transducers (MTTs). It provides
 -- functions to run MTTs and to compose them with top down tree
 -- transducers. It also defines MTTs with regular look-ahead which
@@ -41,11 +44,11 @@
     )
     where
 
-import Data.Comp.Term
 import Data.Comp.Algebra
 import Data.Comp.Automata
-import Data.Comp.Ops
 import Data.Comp.Multi.HFunctor (I (..))
+import Data.Comp.Ops
+import Data.Comp.Term
 
 -- | This type represents total deterministic macro tree transducers
 -- (MTTs).
@@ -68,19 +71,19 @@
 -- | This function defines the semantics of MTTs. It applies a given
 -- MTT to an input with and an initial state.
 
-runMacroTrans :: (Functor g, Functor f, Functor q) => 
+runMacroTrans :: (Functor g, Functor f, Functor q) =>
                  MacroTrans f q g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a
 runMacroTrans tr q t = run t q where
     run (Term t) q = appCxt (tr q (fmap run' t))
     run (Hole a) _ = Hole a
     run' t q = run t (fmap appCxt q)
-    
 
+
 -- This function is a variant of 'runMacroTrans' that is used to
 -- define composition. Restricted to 'Term's, both functions coincide.
 
-runMacroTrans' :: forall g f q h a. 
-                  (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a) 
+runMacroTrans' :: forall g f q h a.
+                  (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a)
                -> Cxt h f (q (Cxt h g a) -> a) -> Cxt h g a
 runMacroTrans' tr q t = run t q where
     run :: Cxt h f (q (Cxt h g a) -> a) -> q (Cxt h g a) -> Cxt h g a
@@ -160,7 +163,7 @@
 -- | This type is a more convenient variant of 'MacroTransLA' with
 -- which one can avoid using 'Hole' explicitly when injecting
 -- placeholders in the result.
-type MacroTransLA' f q p g = forall a. q (Context g a) -> p -> 
+type MacroTransLA' f q p g = forall a. q (Context g a) -> p ->
                              f (q (Context g a) -> Context g a, p) -> Context g a
 
 
@@ -175,7 +178,7 @@
 -- look-ahead. It applies a given MTT with regular look-ahead
 -- (including an accompanying bottom-up state transition function) to
 -- an input with and an initial state.
-runMacroTransLA :: forall g f q p. (Functor g, Functor f, Functor q) => 
+runMacroTransLA :: forall g f q p. (Functor g, Functor f, Functor q) =>
                    UpState f p -> MacroTransLA f q p g -> q (Term g) -> Term f -> Term g
 runMacroTransLA st tr q t = fst (run t) q where
     run :: Term f -> (q (Term g) -> Term g, p)
diff --git a/src/Data/Comp/Matching.hs b/src/Data/Comp/Matching.hs
--- a/src/Data/Comp/Matching.hs
+++ b/src/Data/Comp/Matching.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE GADTs, FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Matching
@@ -19,15 +21,15 @@
      module Data.Comp.Variables
     ) where
 
-import Data.Comp.Term
 import Data.Comp.Equality
+import Data.Comp.Term
 import Data.Comp.Variables
-import qualified Data.Map as Map
+import Data.Foldable
 import Data.Map (Map)
+import qualified Data.Map as Map
 import Data.Traversable
-import Data.Foldable
 
-import Prelude hiding (mapM_, mapM, all)
+import Prelude hiding (all, mapM, mapM_)
 
 {-| This is an auxiliary function for implementing 'matchCxt'. It behaves
 similarly as 'match' but is oblivious to non-linearity. Therefore, the
@@ -58,7 +60,7 @@
 
 matchCxt :: (Ord v,EqF f, Eq (Cxt h f a), Functor f, Foldable f)
          => Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
-matchCxt c1 c2 = do 
+matchCxt c1 c2 = do
   res <- matchCxt' c1 c2
   let insts = Map.elems res
   mapM_ checkEq insts
diff --git a/src/Data/Comp/Multi.hs b/src/Data/Comp/Multi.hs
--- a/src/Data/Comp/Multi.hs
+++ b/src/Data/Comp/Multi.hs
@@ -8,7 +8,7 @@
 -- Portability :  non-portable (GHC Extensions)
 --
 -- This module defines the infrastructure necessary to use
--- /Generalised Compositional Data Types/. Generalised Compositional Data Types 
+-- /Generalised Compositional Data Types/. Generalised Compositional Data Types
 -- is an extension of Compositional Data Types with mutually recursive
 -- data types, and more generally GADTs. Examples of usage are bundled with the
 -- package in the library @examples\/Examples\/Multi@.
@@ -24,17 +24,17 @@
   , module Data.Comp.Multi.Generic
     ) where
 
-import Data.Comp.Multi.HFunctor
-import Data.Comp.Multi.Term
 import Data.Comp.Multi.Algebra
-import Data.Comp.Multi.Sum
 import Data.Comp.Multi.Annotation
 import Data.Comp.Multi.Equality
 import Data.Comp.Multi.Generic
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Sum
+import Data.Comp.Multi.Term
 
 {- $ex1
-The example illustrates how to use generalised compositional data types 
-to implement a small expression language, with a sub language of values, and 
+The example illustrates how to use generalised compositional data types
+to implement a small expression language, with a sub language of values, and
 an evaluation function mapping expressions to values.
 
 The following language extensions are needed in order to run the example:
@@ -45,7 +45,7 @@
 > import Data.Comp.Multi
 > import Data.Comp.Multi.Show ()
 > import Data.Comp.Multi.Derive
-> 
+>
 > -- Signature for values and operators
 > data Value e l where
 >   Const  ::        Int -> Value e Int
@@ -54,41 +54,41 @@
 >   Add, Mult  :: e Int -> e Int   -> Op e Int
 >   Fst        ::          e (s,t) -> Op e s
 >   Snd        ::          e (s,t) -> Op e t
-> 
+>
 > -- Signature for the simple expression language
 > type Sig = Op :+: Value
-> 
+>
 > -- Derive boilerplate code using Template Haskell (GHC 7 needed)
-> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors] 
+> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
 >          [''Value, ''Op])
-> 
+>
 > -- Term evaluation algebra
 > class Eval f v where
 >   evalAlg :: Alg f (Term v)
-> 
+>
 > instance (Eval f v, Eval g v) => Eval (f :+: g) v where
 >   evalAlg (Inl x) = evalAlg x
 >   evalAlg (Inr x) = evalAlg x
-> 
+>
 > -- Lift the evaluation algebra to a catamorphism
 > eval :: (HFunctor f, Eval f v) => Term f :-> Term v
 > eval = cata evalAlg
-> 
+>
 > instance (Value :<: v) => Eval Value v where
 >   evalAlg = inject
-> 
+>
 > instance (Value :<: v) => Eval Op v where
 >   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
 >   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
 >   evalAlg (Fst x)    = fst $ projP x
 >   evalAlg (Snd x)    = snd $ projP x
-> 
+>
 > projC :: (Value :<: v) => Term v Int -> Int
 > projC v = case project v of Just (Const n) -> n
-> 
+>
 > projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
 > projP v = case project v of Just (Pair x y) -> (x,y)
-> 
+>
 > -- Example: evalEx = iConst 2
 > evalEx :: Term Value Int
 > evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
@@ -96,7 +96,7 @@
 
 {- $ex2
 The example illustrates how to use generalised compositional data types to
-implement a small expression language, with a sub language of values, and a 
+implement a small expression language, with a sub language of values, and a
 monadic evaluation function mapping expressions to values.
 
 The following language extensions are needed in order to run the example:
@@ -108,7 +108,7 @@
 > import Data.Comp.Multi.Show ()
 > import Data.Comp.Multi.Derive
 > import Control.Monad (liftM)
-> 
+>
 > -- Signature for values and operators
 > data Value e l where
 >   Const  ::        Int -> Value e Int
@@ -117,29 +117,29 @@
 >   Add, Mult  :: e Int -> e Int   -> Op e Int
 >   Fst        ::          e (s,t) -> Op e s
 >   Snd        ::          e (s,t) -> Op e t
-> 
+>
 > -- Signature for the simple expression language
 > type Sig = Op :+: Value
-> 
+>
 > -- Derive boilerplate code using Template Haskell (GHC 7 needed)
 > $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
 >           makeHEqF, makeHShowF, smartConstructors]
 >          [''Value, ''Op])
-> 
+>
 > -- Monadic term evaluation algebra
 > class EvalM f v where
 >   evalAlgM :: AlgM Maybe f (Term v)
-> 
+>
 > instance (EvalM f v, EvalM g v) => EvalM (f :+: g) v where
 >   evalAlgM (Inl x) = evalAlgM x
 >   evalAlgM (Inr x) = evalAlgM x
-> 
+>
 > evalM :: (HTraversable f, EvalM f v) => Term f l -> Maybe (Term v l)
 > evalM = cataM evalAlgM
-> 
+>
 > instance (Value :<: v) => EvalM Value v where
 >   evalAlgM = return . inject
-> 
+>
 > instance (Value :<: v) => EvalM Op v where
 >   evalAlgM (Add x y)  = do n1 <- projC x
 >                            n2 <- projC y
@@ -149,15 +149,15 @@
 >                            return $ iConst $ n1 * n2
 >   evalAlgM (Fst v)    = liftM fst $ projP v
 >   evalAlgM (Snd v)    = liftM snd $ projP v
-> 
+>
 > projC :: (Value :<: v) => Term v Int -> Maybe Int
 > projC v = case project v of
 >             Just (Const n) -> return n; _ -> Nothing
-> 
+>
 > projP :: (Value :<: v) => Term v (a,b) -> Maybe (Term v a, Term v b)
 > projP v = case project v of
 >             Just (Pair x y) -> return (x,y); _ -> Nothing
-> 
+>
 > -- Example: evalMEx = Just (iConst 5)
 > evalMEx :: Maybe (Term Value Int)
 > evalMEx = evalM ((iConst 1) `iAdd`
@@ -165,7 +165,7 @@
 -}
 
 {- $ex3
-The example illustrates how to use generalised compositional data types 
+The example illustrates how to use generalised compositional data types
 to implement a small expression language, and  an evaluation function mapping
 intrinsically typed expressions to values.
 
@@ -177,7 +177,7 @@
 > import Data.Comp.Multi
 > import Data.Comp.Multi.Show ()
 > import Data.Comp.Multi.Derive
-> 
+>
 > -- Signature for values and operators
 > data Value e l where
 >   Const  ::        Int -> Value e Int
@@ -186,36 +186,36 @@
 >   Add, Mult  :: e Int -> e Int   -> Op e Int
 >   Fst        ::          e (s,t) -> Op e s
 >   Snd        ::          e (s,t) -> Op e t
-> 
+>
 > -- Signature for the simple expression language
 > type Sig = Op :+: Value
-> 
+>
 > -- Derive boilerplate code using Template Haskell (GHC 7 needed)
-> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors] 
+> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
 >          [''Value, ''Op])
-> 
+>
 > -- Term evaluation algebra
 > class EvalI f where
 >   evalAlgI :: Alg f I
-> 
+>
 > instance (EvalI f, EvalI g) => EvalI (f :+: g) where
 >   evalAlgI (Inl x) = evalAlgI x
 >   evalAlgI (Inr x) = evalAlgI x
-> 
+>
 > -- Lift the evaluation algebra to a catamorphism
 > evalI :: (HFunctor f, EvalI f) => Term f i -> i
 > evalI = unI . cata evalAlgI
-> 
+>
 > instance EvalI Value where
 >   evalAlgI (Const n) = I n
 >   evalAlgI (Pair (I x) (I y)) = I (x,y)
-> 
+>
 > instance EvalI Op where
 >   evalAlgI (Add (I x) (I y))  = I (x + y)
 >   evalAlgI (Mult (I x) (I y)) = I (x * y)
 >   evalAlgI (Fst (I (x,_)))    = I x
 >   evalAlgI (Snd (I (_,y)))    = I y
-> 
+>
 > -- Example: evalEx = 2
 > evalIEx :: Int
 > evalIEx = evalI (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
@@ -233,7 +233,7 @@
 > import Data.Comp.Multi
 > import Data.Comp.Multi.Show ()
 > import Data.Comp.Multi.Derive
-> 
+>
 > -- Signature for values, operators, and syntactic sugar
 > data Value e l where
 >   Const  ::        Int -> Value e Int
@@ -245,75 +245,75 @@
 > data Sugar e l where
 >   Neg   :: e Int   -> Sugar e Int
 >   Swap  :: e (s,t) -> Sugar e (t,s)
-> 
+>
 > -- Source position information (line number, column number)
 > data Pos = Pos Int Int
 >            deriving Show
-> 
+>
 > -- Signature for the simple expression language
 > type Sig = Op :+: Value
 > type SigP = Op :&: Pos :+: Value :&: Pos
-> 
+>
 > -- Signature for the simple expression language, extended with syntactic sugar
 > type Sig' = Sugar :+: Op :+: Value
 > type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
-> 
+>
 > -- Derive boilerplate code using Template Haskell (GHC 7 needed)
 > $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
 >           makeHEqF, makeHShowF, smartConstructors]
 >          [''Value, ''Op, ''Sugar])
-> 
+>
 > -- Term homomorphism for desugaring of terms
 > class (HFunctor f, HFunctor g) => Desugar f g where
 >   desugHom :: Hom f g
 >   desugHom = desugHom' . hfmap Hole
 >   desugHom' :: Alg f (Context g a)
 >   desugHom' x = appCxt (desugHom x)
-> 
+>
 > instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
 >   desugHom (Inl x) = desugHom x
 >   desugHom (Inr x) = desugHom x
 >   desugHom' (Inl x) = desugHom' x
 >   desugHom' (Inr x) = desugHom' x
-> 
+>
 > instance (Value :<: v, HFunctor v) => Desugar Value v where
 >   desugHom = simpCxt . inj
-> 
+>
 > instance (Op :<: v, HFunctor v) => Desugar Op v where
 >   desugHom = simpCxt . inj
-> 
+>
 > instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
 >   desugHom' (Neg x)  = iConst (-1) `iMult` x
 >   desugHom' (Swap x) = iSnd x `iPair` iFst x
-> 
+>
 > -- Term evaluation algebra
 > class Eval f v where
 >   evalAlg :: Alg f (Term v)
-> 
+>
 > instance (Eval f v, Eval g v) => Eval (f :+: g) v where
 >   evalAlg (Inl x) = evalAlg x
 >   evalAlg (Inr x) = evalAlg x
-> 
+>
 > instance (Value :<: v) => Eval Value v where
 >   evalAlg = inject
-> 
+>
 > instance (Value :<: v) => Eval Op v where
 >   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
 >   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
 >   evalAlg (Fst x)    = fst $ projP x
 >   evalAlg (Snd x)    = snd $ projP x
-> 
+>
 > projC :: (Value :<: v) => Term v Int -> Int
 > projC v = case project v of Just (Const n) -> n
-> 
+>
 > projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
 > projP v = case project v of Just (Pair x y) -> (x,y)
-> 
+>
 > -- Compose the evaluation algebra and the desugaring homomorphism to an
 > -- algebra
 > eval :: Term Sig' :-> Term Value
 > eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))
-> 
+>
 > -- Example: evalEx = iPair (iConst 2) (iConst 1)
 > evalEx :: Term Value (Int,Int)
 > evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2)
@@ -332,7 +332,7 @@
 > import Data.Comp.Multi
 > import Data.Comp.Multi.Show ()
 > import Data.Comp.Multi.Derive
-> 
+>
 > -- Signature for values, operators, and syntactic sugar
 > data Value e l where
 >   Const  ::        Int -> Value e Int
@@ -344,74 +344,74 @@
 > data Sugar e l where
 >   Neg   :: e Int   -> Sugar e Int
 >   Swap  :: e (s,t) -> Sugar e (t,s)
-> 
+>
 > -- Source position information (line number, column number)
 > data Pos = Pos Int Int
 >            deriving (Show, Eq)
-> 
+>
 > -- Signature for the simple expression language
 > type Sig = Op :+: Value
 > type SigP = Op :&: Pos :+: Value :&: Pos
-> 
+>
 > -- Signature for the simple expression language, extended with syntactic sugar
 > type Sig' = Sugar :+: Op :+: Value
 > type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
-> 
+>
 > -- Derive boilerplate code using Template Haskell (GHC 7 needed)
 > $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
 >           makeHEqF, makeHShowF, smartConstructors]
 >          [''Value, ''Op, ''Sugar])
-> 
+>
 > -- Term homomorphism for desugaring of terms
 > class (HFunctor f, HFunctor g) => Desugar f g where
 >   desugHom :: Hom f g
 >   desugHom = desugHom' . hfmap Hole
 >   desugHom' :: Alg f (Context g a)
 >   desugHom' x = appCxt (desugHom x)
-> 
+>
 > instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
 >   desugHom (Inl x) = desugHom x
 >   desugHom (Inr x) = desugHom x
 >   desugHom' (Inl x) = desugHom' x
 >   desugHom' (Inr x) = desugHom' x
-> 
+>
 > instance (Value :<: v, HFunctor v) => Desugar Value v where
 >   desugHom = simpCxt . inj
-> 
+>
 > instance (Op :<: v, HFunctor v) => Desugar Op v where
 >   desugHom = simpCxt . inj
-> 
+>
 > instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
 >   desugHom' (Neg x)  = iConst (-1) `iMult` x
 >   desugHom' (Swap x) = iSnd x `iPair` iFst x
-> 
+>
 > -- Lift the desugaring term homomorphism to a catamorphism
 > desug :: Term Sig' :-> Term Sig
 > desug = appHom desugHom
-> 
+>
 > -- Example: desugEx = iPair (iConst 2) (iConst 1)
 > desugEx :: Term Sig (Int,Int)
 > desugEx = desug $ iSwap $ iPair (iConst 1) (iConst 2)
-> 
+>
 > -- Lift desugaring to terms annotated with source positions
 > desugP :: Term SigP' :-> Term SigP
 > desugP = appHom (propAnn desugHom)
-> 
+>
 > iSwapP :: (DistAnn f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a)
 > iSwapP p x = Term (injectA p $ inj $ Swap x)
-> 
+>
 > iConstP :: (DistAnn f p f', Value :<: f) => p -> Int -> Term f' Int
 > iConstP p x = Term (injectA p $ inj $ Const x)
-> 
+>
 > iPairP :: (DistAnn f p f', Value :<: f) => p -> Term f' a -> Term f' b -> Term f' (a,b)
 > iPairP p x y = Term (injectA p $ inj $ Pair x y)
-> 
+>
 > iFstP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' a
 > iFstP p x = Term (injectA p $ inj $ Fst x)
-> 
+>
 > iSndP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' b
 > iSndP p x = Term (injectA p $ inj $ Snd x)
-> 
+>
 > -- Example: desugPEx = iPairP (Pos 1 0)
 > --                            (iSndP (Pos 1 0) (iPairP (Pos 1 1)
 > --                                                     (iConstP (Pos 1 2) 1)
diff --git a/src/Data/Comp/Multi/Algebra.hs b/src/Data/Comp/Multi/Algebra.hs
--- a/src/Data/Comp/Multi/Algebra.hs
+++ b/src/Data/Comp/Multi/Algebra.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE GADTs, Rank2Types, TypeOperators, ScopedTypeVariables, 
-  FlexibleContexts, KindSignatures #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Algebra
@@ -22,7 +26,7 @@
       cata,
       cata',
       appCxt,
-      
+
       -- * Monadic Algebras & Catamorphisms
       AlgM,
       freeM,
@@ -86,11 +90,11 @@
     ) where
 
 
-import Data.Comp.Multi.Term
+import Control.Monad
 import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HTraversable
+import Data.Comp.Multi.Term
 import Data.Comp.Ops
-import Control.Monad
 
 -- | This type represents multisorted @f@-algebras with a family @e@
 -- of carriers.
@@ -107,7 +111,7 @@
 
 -- | Construct a catamorphism from the given algebra.
 cata :: forall f a. HFunctor f => Alg f a -> Term f :-> a
-cata f = run 
+cata f = run
     where run :: Term f :-> a
           run (Term t) = f (hfmap run t)
 
@@ -342,7 +346,7 @@
 
 anaM :: forall a m f. (HTraversable f, Monad m)
           => CoalgM m f a -> NatM m a (Term f)
-anaM f = run 
+anaM f = run
     where run :: NatM m a (Term f)
           run t = liftM Term $ f t >>= hmapM run
 
@@ -367,7 +371,7 @@
 
 -- | This function constructs a monadic paramorphism from the given
 -- monadic r-algebra
-paraM :: forall f m a. (HTraversable f, Monad m) => 
+paraM :: forall f m a. (HTraversable f, Monad m) =>
          RAlgM m f a -> NatM m(Term f)  a
 paraM f = liftM fsnd . cataM run
     where run :: AlgM m f (Term f :*: a)
@@ -386,7 +390,7 @@
 -- | This function constructs an apomorphism from the given
 -- r-coalgebra.
 apo :: forall f a . (HFunctor f) => RCoalg f a -> a :-> Term f
-apo f = run 
+apo f = run
     where run :: a :-> Term f
           run = Term . hfmap run' . f
           run' :: Term f :+: a :-> Term f
@@ -402,7 +406,7 @@
 -- monadic r-coalgebra.
 apoM :: forall f m a . (HTraversable f, Monad m) =>
         RCoalgM m f a -> NatM m a (Term f)
-apoM f = run 
+apoM f = run
     where run :: NatM m a (Term f)
           run a = do
             t <- f a
diff --git a/src/Data/Comp/Multi/Annotation.hs b/src/Data/Comp/Multi/Annotation.hs
--- a/src/Data/Comp/Multi/Annotation.hs
+++ b/src/Data/Comp/Multi/Annotation.hs
@@ -1,5 +1,12 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, ConstraintKinds, FlexibleContexts,
-  FlexibleInstances, UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Annotation
@@ -27,12 +34,11 @@
      project'
     ) where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Sum
-import Data.Comp.Multi.Ops
-import qualified Data.Comp.Ops as O
 import Data.Comp.Multi.Algebra
 import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Ops
+import Data.Comp.Multi.Term
+import qualified Data.Comp.Ops as O
 
 -- | This function transforms a function with a domain constructed
 -- from a functor to a function with a domain constructed with the
@@ -54,7 +60,7 @@
        => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a
 liftA' f v = let (v' O.:&: p) = projectA v
              in ann p (f v')
-    
+
 {-| This function strips the annotations from a term over a
 functor with annotations. -}
 
@@ -62,7 +68,7 @@
 stripA = appSigFun remA
 
 
-propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g) 
+propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g)
                => Hom f g -> Hom f' g'
 propAnn alg f' = ann p (alg f)
     where (f O.:&: p) = projectA f'
diff --git a/src/Data/Comp/Multi/Derive.hs b/src/Data/Comp/Multi/Derive.hs
--- a/src/Data/Comp/Multi/Derive.hs
+++ b/src/Data/Comp/Multi/Derive.hs
@@ -42,13 +42,13 @@
 
 import Data.Comp.Derive.Utils (derive, liftSumGen)
 import Data.Comp.Multi.Derive.Equality
-import Data.Comp.Multi.Derive.Ordering
-import Data.Comp.Multi.Derive.Show
-import Data.Comp.Multi.Derive.HFunctor
 import Data.Comp.Multi.Derive.HFoldable
+import Data.Comp.Multi.Derive.HFunctor
 import Data.Comp.Multi.Derive.HTraversable
-import Data.Comp.Multi.Derive.SmartConstructors
+import Data.Comp.Multi.Derive.Ordering
+import Data.Comp.Multi.Derive.Show
 import Data.Comp.Multi.Derive.SmartAConstructors
+import Data.Comp.Multi.Derive.SmartConstructors
 import Data.Comp.Multi.Ops ((:+:), caseH)
 
 import Language.Haskell.TH
diff --git a/src/Data/Comp/Multi/Derive/Equality.hs b/src/Data/Comp/Multi/Derive/Equality.hs
--- a/src/Data/Comp/Multi/Derive/Equality.hs
+++ b/src/Data/Comp/Multi/Derive/Equality.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TemplateHaskell   #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Derive.Equality
@@ -41,7 +42,7 @@
             defEqClause constrs
                 | length constrs  < 2 = []
                 | otherwise = [clause [wildP,wildP] (normalB [|False|]) []]
-            genEqClause ftyp (constr, argts) = do 
+            genEqClause ftyp (constr, argts) = do
               let n = length argts
               varNs <- newNames n "x"
               varNs' <- newNames n "y"
@@ -54,7 +55,7 @@
                                    then [| $x' `keq` $y'|]
                                    else [| $x' == $y'|]
                   eqs = listE $ zipWith3 mkEq argts vars vars'
-              body <- if n == 0 
+              body <- if n == 0
                       then [|True|]
                       else [|and $eqs|]
               return $ Clause [pat, pat'] (NormalB body) []
diff --git a/src/Data/Comp/Multi/Derive/HFoldable.hs b/src/Data/Comp/Multi/Derive/HFoldable.hs
--- a/src/Data/Comp/Multi/Derive/HFoldable.hs
+++ b/src/Data/Comp/Multi/Derive/HFoldable.hs
@@ -18,25 +18,24 @@
      makeHFoldable
     )where
 
+import Control.Monad
 import Data.Comp.Derive.Utils
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
 import Data.Foldable
-import Language.Haskell.TH
-import Data.Monoid
 import Data.Maybe
-import qualified Prelude as P (foldl,foldr,foldl1)
-import Prelude hiding  (foldl,foldr,foldl1)
-import Control.Monad
+import Data.Monoid
+import Language.Haskell.TH
+import Prelude hiding (foldl, foldl1, foldr)
+import qualified Prelude as P (foldl, foldl1, foldr)
 
 
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
 
-iter' n f e = run n f e
-    where run 0 _ e = e
-          run m f e = let f' = iter (m-1) [|fmap|] f
-                      in run (m-1) f (f' `appE` e)
+iter' 0 _ e = e
+iter' m f e = let f' = iter (m-1) [|fmap|] f
+              in iter' (m-1) f (f' `appE` e)
 
 iterSp n f g e = run n e
     where run 0 e = e
@@ -86,7 +85,7 @@
                        fp = if null vars then WildP else VarP fn
                    body <- case vars of
                              [] -> [|mempty|]
-                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $ 
+                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $
                                       map (\ (d,z) -> iter' (max (d-1) 0) [|fold|] (f' d `appE` z)) vars
                    return $ Clause [fp, pat] (NormalB body) []
             foldlClause (pat,vars) =
diff --git a/src/Data/Comp/Multi/Derive/HFunctor.hs b/src/Data/Comp/Multi/Derive/HFunctor.hs
--- a/src/Data/Comp/Multi/Derive/HFunctor.hs
+++ b/src/Data/Comp/Multi/Derive/HFunctor.hs
@@ -18,13 +18,13 @@
      makeHFunctor
     ) where
 
+import Control.Monad
 import Data.Comp.Derive.Utils
 import Data.Comp.Multi.HFunctor
+import Data.Maybe
 import Language.Haskell.TH
-import qualified Prelude as P (mapM)
 import Prelude hiding (mapM)
-import Data.Maybe
-import Control.Monad
+import qualified Prelude as P (mapM)
 
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
diff --git a/src/Data/Comp/Multi/Derive/HTraversable.hs b/src/Data/Comp/Multi/Derive/HTraversable.hs
--- a/src/Data/Comp/Multi/Derive/HTraversable.hs
+++ b/src/Data/Comp/Multi/Derive/HTraversable.hs
@@ -18,16 +18,16 @@
      makeHTraversable
     ) where
 
+import Control.Applicative
+import Control.Monad hiding (mapM, sequence)
 import Data.Comp.Derive.Utils
 import Data.Comp.Multi.HTraversable
-import Language.Haskell.TH
+import Data.Foldable hiding (any, or)
 import Data.Maybe
 import Data.Traversable
-import Data.Foldable hiding (any,or)
-import Control.Applicative
-import Control.Monad hiding (mapM, sequence)
+import Language.Haskell.TH
+import Prelude hiding (foldl, foldr, mapM, sequence)
 import qualified Prelude as P (foldl, foldr, mapM)
-import Prelude hiding  (foldl, foldr,mapM, sequence)
 
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
diff --git a/src/Data/Comp/Multi/Derive/Ordering.hs b/src/Data/Comp/Multi/Derive/Ordering.hs
--- a/src/Data/Comp/Multi/Derive/Ordering.hs
+++ b/src/Data/Comp/Multi/Derive/Ordering.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
-  ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Derive.Ordering
@@ -18,10 +19,10 @@
      makeOrdHF
     ) where
 
-import Data.Comp.Multi.Ordering
 import Data.Comp.Derive.Utils
-import Data.Maybe
+import Data.Comp.Multi.Ordering
 import Data.List
+import Data.Maybe
 import Language.Haskell.TH hiding (Cxt)
 
 compList :: [Ordering] -> Ordering
@@ -43,7 +44,7 @@
   return [InstanceD [] classType [compareHFDecl]]
       where compareHFClauses :: Name -> [(Name,[Type])] -> [ClauseQ]
             compareHFClauses _ [] = []
-            compareHFClauses coArg constrs = 
+            compareHFClauses coArg constrs =
                 let constrs' = constrs `zip` [1..]
                     constPairs = [(x,y)| x<-constrs', y <- constrs']
                 in map (genClause coArg) constPairs
@@ -52,7 +53,7 @@
                 | n < m = genLtClause c d
                 | otherwise = genGtClause c d
             genEqClause :: Name -> (Name,[Type]) -> ClauseQ
-            genEqClause coArg (constr, args) = do 
+            genEqClause coArg (constr, args) = do
               varXs <- newNames (length args) "x"
               varYs <- newNames (length args) "y"
               let patX = ConP constr $ map VarP varXs
diff --git a/src/Data/Comp/Multi/Derive/Show.hs b/src/Data/Comp/Multi/Derive/Show.hs
--- a/src/Data/Comp/Multi/Derive/Show.hs
+++ b/src/Data/Comp/Multi/Derive/Show.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE TemplateHaskell, TypeOperators #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators   #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Derive.Show
@@ -20,8 +21,8 @@
     ) where
 
 import Data.Comp.Derive.Utils
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.Algebra
+import Data.Comp.Multi.HFunctor
 import Language.Haskell.TH
 
 {-| Signature printing. An instance @ShowHF f@ gives rise to an instance
@@ -58,7 +59,7 @@
             mkShow (isFArg, var)
                 | isFArg = [|unK $var|]
                 | otherwise = [| show $var |]
-            genShowFClause fArg (constr, args) = do 
+            genShowFClause fArg (constr, args) = do
               let n = length args
               varNs <- newNames n "x"
               let pat = ConP constr $ map VarP varNs
diff --git a/src/Data/Comp/Multi/Derive/SmartAConstructors.hs b/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
--- a/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
+++ b/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
@@ -12,17 +12,17 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Multi.Derive.SmartAConstructors 
+module Data.Comp.Multi.Derive.SmartAConstructors
     (
      smartAConstructors
     ) where
 
-import Language.Haskell.TH hiding (Cxt)
+import Control.Monad
 import Data.Comp.Derive.Utils
+import Data.Comp.Multi.Annotation
 import Data.Comp.Multi.Sum
 import Data.Comp.Multi.Term
-import Data.Comp.Multi.Annotation
-import Control.Monad
+import Language.Haskell.TH hiding (Cxt)
 
 {-| Derive smart constructors with products for a type constructor of any
   parametric kind taking at least two arguments. The smart constructors are
diff --git a/src/Data/Comp/Multi/Derive/SmartConstructors.hs b/src/Data/Comp/Multi/Derive/SmartConstructors.hs
--- a/src/Data/Comp/Multi/Derive/SmartConstructors.hs
+++ b/src/Data/Comp/Multi/Derive/SmartConstructors.hs
@@ -12,17 +12,17 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Multi.Derive.SmartConstructors 
+module Data.Comp.Multi.Derive.SmartConstructors
     (
      smartConstructors
     ) where
 
-import Language.Haskell.TH hiding (Cxt)
+import Control.Arrow ((&&&))
+import Control.Monad
 import Data.Comp.Derive.Utils
 import Data.Comp.Multi.Sum
 import Data.Comp.Multi.Term
-import Control.Arrow ((&&&))
-import Control.Monad
+import Language.Haskell.TH hiding (Cxt)
 
 {-| Derive smart constructors for a type constructor of any higher-order kind
  taking at least two arguments. The smart constructors are similar to the
diff --git a/src/Data/Comp/Multi/Desugar.hs b/src/Data/Comp/Multi/Desugar.hs
--- a/src/Data/Comp/Multi/Desugar.hs
+++ b/src/Data/Comp/Multi/Desugar.hs
@@ -1,5 +1,8 @@
-{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, TypeOperators, OverlappingInstances, ConstraintKinds #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances  #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Desugar
diff --git a/src/Data/Comp/Multi/Equality.hs b/src/Data/Comp/Multi/Equality.hs
--- a/src/Data/Comp/Multi/Equality.hs
+++ b/src/Data/Comp/Multi/Equality.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE TypeOperators     #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Equality
@@ -20,11 +22,10 @@
      heqMod
     ) where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Sum
-import Data.Comp.Multi.Ops
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Ops
+import Data.Comp.Multi.Term
 
 class KEq f where
     keq :: f i -> f j -> Bool
diff --git a/src/Data/Comp/Multi/Generic.hs b/src/Data/Comp/Multi/Generic.hs
--- a/src/Data/Comp/Multi/Generic.hs
+++ b/src/Data/Comp/Multi/Generic.hs
@@ -1,5 +1,10 @@
-{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, ScopedTypeVariables, 
-  Rank2Types, ConstraintKinds, FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds           #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE Rank2Types                #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE TypeOperators             #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -18,13 +23,13 @@
 
 module Data.Comp.Multi.Generic where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Sum
-import Data.Comp.Multi.HFunctor
+import Control.Monad
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HTraversable
+import Data.Comp.Multi.Sum
+import Data.Comp.Multi.Term
 import GHC.Exts
-import Control.Monad
 import Prelude
 
 import Data.Maybe
@@ -58,12 +63,12 @@
 -- | Monadic version of 'transform'.
 transformM :: forall f m . (HTraversable f, Monad m) =>
              NatM m (Term f) (Term f) -> NatM m (Term f) (Term f)
-transformM  f = run 
+transformM  f = run
     where run :: NatM m (Term f) (Term f)
           run t = f =<< liftM Term (hmapM run $ unTerm t)
 
 query :: HFoldable f => (Term f :=>  r) -> (r -> r -> r) -> Term f :=> r
--- query q c = run 
+-- query q c = run
 --     where run i@(Term t) = foldl (\s x -> s `c` run x) (q i) t
 query q c i@(Term t) = hfoldl (\s x -> s `c` query q c x) (q i) t
 
diff --git a/src/Data/Comp/Multi/HFoldable.hs b/src/Data/Comp/Multi/HFoldable.hs
--- a/src/Data/Comp/Multi/HFoldable.hs
+++ b/src/Data/Comp/Multi/HFoldable.hs
@@ -1,4 +1,10 @@
-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -21,9 +27,9 @@
      htoList
      ) where
 
-import Data.Monoid
-import Data.Maybe
 import Data.Comp.Multi.HFunctor
+import Data.Maybe
+import Data.Monoid
 
 -- | Higher-order functors that can be folded.
 --
@@ -58,7 +64,7 @@
 
 htoList :: (HFoldable f) => f a :=> [E a]
 htoList = hfoldr (\ n l ->  E n : l) []
-    
+
 kfoldr :: (HFoldable f) => (a -> b -> b) -> b -> f (K a) :=> b
 kfoldr f = hfoldr (\ (K x) y -> f x y)
 
diff --git a/src/Data/Comp/Multi/HFunctor.hs b/src/Data/Comp/Multi/HFunctor.hs
--- a/src/Data/Comp/Multi/HFunctor.hs
+++ b/src/Data/Comp/Multi/HFunctor.hs
@@ -1,4 +1,10 @@
-{-# LANGUAGE Rank2Types, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE Rank2Types                #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE UndecidableInstances      #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -81,7 +87,7 @@
     -- functor @f g@.
     --
     -- @ffmap :: (Functor g) => (a -> b) -> f g a -> f g b@
-    -- 
+    --
     -- We omit this, as it does not work for GADTs (see Johand and
     -- Ghani 2008).
 
@@ -92,4 +98,4 @@
 infixl 5 :.:
 
 -- | This data type denotes the composition of two functor families.
-data (f :.: g) e t = Comp f (g e) t
+data  (f :.: g) e t = Comp f (g e) t
diff --git a/src/Data/Comp/Multi/HTraversable.hs b/src/Data/Comp/Multi/HTraversable.hs
--- a/src/Data/Comp/Multi/HTraversable.hs
+++ b/src/Data/Comp/Multi/HTraversable.hs
@@ -1,4 +1,10 @@
-{-# LANGUAGE Rank2Types, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -18,9 +24,9 @@
      HTraversable (..)
     ) where
 
-import Data.Comp.Multi.HFunctor
-import Data.Comp.Multi.HFoldable
 import Control.Applicative
+import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
 
 class HFoldable t => HTraversable t where
 
diff --git a/src/Data/Comp/Multi/Number.hs b/src/Data/Comp/Multi/Number.hs
--- a/src/Data/Comp/Multi/Number.hs
+++ b/src/Data/Comp/Multi/Number.hs
@@ -8,22 +8,22 @@
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
 -- Portability :  non-portable (GHC Extensions)
--- 
+--
 -- This module provides functionality to number the components of a
 -- functorial value with consecutive integers.
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Multi.Number 
+module Data.Comp.Multi.Number
     ( Numbered (..)
     , unNumbered
     , number
     , HTraversable ()) where
 
-import Data.Comp.Multi.HTraversable
+import Data.Comp.Multi.Equality
 import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.HTraversable
 import Data.Comp.Multi.Ordering
-import Data.Comp.Multi.Equality
 
 
 import Control.Monad.State
@@ -44,7 +44,7 @@
 -- | This function numbers the components of the given functorial
 -- value with consecutive integers starting at 0.
 number :: HTraversable f => f a :-> f (Numbered a)
-number x = fst $ runState (hmapM run x) 0 where
+number x = evalState (hmapM run x) 0 where
   run b = do n <- get
              put (n+1)
              return $ Numbered (n,b)
diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs
--- a/src/Data/Comp/Multi/Ops.hs
+++ b/src/Data/Comp/Multi/Ops.hs
@@ -1,8 +1,18 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, OverlappingInstances,
-             FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
-             ScopedTypeVariables, FunctionalDependencies, UndecidableInstances, 
-             KindSignatures, RankNTypes, TypeFamilies, DataKinds, ConstraintKinds,
-             PolyKinds #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE TypeSynonymInstances   #-}
+{-# LANGUAGE UndecidableInstances   #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -20,12 +30,12 @@
 
 module Data.Comp.Multi.Ops where
 
-import Data.Comp.Multi.HFunctor
+import Control.Applicative
+import Control.Monad
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HTraversable
 import qualified Data.Comp.Ops as O
-import Control.Monad
-import Control.Applicative
 
 import Data.Comp.SubsumeCommon
 
@@ -34,7 +44,7 @@
 
 -- |Data type defining coproducts.
 data (f :+: g) (h :: * -> *) e = Inl (f h e)
-                    | Inr (g h e)
+                               | Inr (g h e)
 
 {-| Utility function to case on a higher-order functor sum, without exposing the
   internal representation of sums. -}
@@ -76,7 +86,7 @@
 type family Elem (f :: (* -> *) -> * -> *)
                  (g :: (* -> *) -> * -> *) :: Emb where
     Elem f f = Found Here
-    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g) 
+    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g)
     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
     Elem f g = NotFound
 
@@ -111,7 +121,7 @@
 
 instance Subsume (Found p) f g => Subsume (Found (Le p)) f (g :+: g') where
     inj' _ = Inl . inj' (P :: Proxy (Found p))
-    
+
     prj' _ (Inl x) = prj' (P :: Proxy (Found p)) x
     prj' _ _       = Nothing
 
@@ -120,8 +130,8 @@
 
     prj' _ (Inr x) = prj' (P :: Proxy (Found p)) x
     prj' _ _       = Nothing
-              
-instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) 
+
+instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g)
     => Subsume (Found (Sum p1 p2)) (f1 :+: f2) g where
     inj' _ (Inl x) = inj' (P :: Proxy (Found p1)) x
     inj' _ (Inr x) = inj' (P :: Proxy (Found p2)) x
@@ -145,12 +155,12 @@
 proj :: forall f g a . (f :<: g) => NatM Maybe (g a) (f a)
 proj = prj' (P :: Proxy (ComprEmb (Elem f g)))
 
-type f :=: g = (f :<: g, g :<: f) 
+type f :=: g = (f :<: g, g :<: f)
 
 
 
 spl :: (f :=: f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
-spl f1 f2 x = case inj x of 
+spl f1 f2 x = case inj x of
             Inl y -> f1 y
             Inr y -> f2 y
 
@@ -173,9 +183,9 @@
 
 -- | This data type adds a constant product to a
 -- signature. Alternatively, this could have also been defined as
--- 
+--
 -- @data (f :&: a) (g ::  * -> *) e = f g e :&: a e@
--- 
+--
 -- This is too general, however, for example for 'productHHom'.
 
 data (f :&: a) (g ::  * -> *) e = f g e :&: a
diff --git a/src/Data/Comp/Multi/Ordering.hs b/src/Data/Comp/Multi/Ordering.hs
--- a/src/Data/Comp/Multi/Ordering.hs
+++ b/src/Data/Comp/Multi/Ordering.hs
@@ -1,5 +1,8 @@
-{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
-  UndecidableInstances, IncoherentInstances, GADTs #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Ordering
@@ -19,11 +22,10 @@
      OrdHF(..)
     ) where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Sum
-import Data.Comp.Multi.Ops
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.Equality
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Ops
+import Data.Comp.Multi.Term
 
 class KEq f => KOrd f where
     kcompare :: f i -> f j -> Ordering
diff --git a/src/Data/Comp/Multi/Show.hs b/src/Data/Comp/Multi/Show.hs
--- a/src/Data/Comp/Multi/Show.hs
+++ b/src/Data/Comp/Multi/Show.hs
@@ -1,6 +1,9 @@
-{-# LANGUAGE TypeOperators, GADTs, FlexibleContexts,
-  ScopedTypeVariables, UndecidableInstances, FlexibleInstances,
-  TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Show
@@ -20,11 +23,11 @@
     ( ShowHF(..)
     ) where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Annotation
 import Data.Comp.Multi.Algebra
-import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Annotation
 import Data.Comp.Multi.Derive
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Term
 
 instance KShow (K String) where
     kshow = id
diff --git a/src/Data/Comp/Multi/Sum.hs b/src/Data/Comp/Multi/Sum.hs
--- a/src/Data/Comp/Multi/Sum.hs
+++ b/src/Data/Comp/Multi/Sum.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE TypeOperators, GADTs, ScopedTypeVariables,
-  Rank2Types, FlexibleContexts, TemplateHaskell, ConstraintKinds #-}
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Sum
@@ -41,11 +45,11 @@
 --     substHoles'
     ) where
 
+import Data.Comp.Multi.Algebra
 import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HTraversable
 import Data.Comp.Multi.Ops
 import Data.Comp.Multi.Term
-import Data.Comp.Multi.Algebra
 
 
 -- |Project the outermost layer of a term to a sub signature. If the signature
diff --git a/src/Data/Comp/Multi/Term.hs b/src/Data/Comp/Multi/Term.hs
--- a/src/Data/Comp/Multi/Term.hs
+++ b/src/Data/Comp/Multi/Term.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, RankNTypes,
-  TypeOperators, ScopedTypeVariables, IncoherentInstances #-}
+{-# LANGUAGE EmptyDataDecls      #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Term
@@ -15,7 +19,7 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Multi.Term 
+module Data.Comp.Multi.Term
     (Cxt (..),
      Hole,
      NoHole,
@@ -28,13 +32,13 @@
      simpCxt
      ) where
 
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HTraversable
 import Data.Monoid
 
-import Control.Monad
 import Control.Applicative hiding (Const)
+import Control.Monad
 
 import Unsafe.Coerce
 
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -1,5 +1,13 @@
-{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances,
-  OverlappingInstances, TypeOperators, KindSignatures, FlexibleContexts, ScopedTypeVariables, RankNTypes, TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances  #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeOperators         #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Variables
@@ -31,14 +39,14 @@
      getBoundVars
     ) where
 
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Ordering
-import Data.Comp.Multi.Number
-import Data.Comp.Multi.Ops
 import Data.Comp.Multi.Algebra
 import Data.Comp.Multi.Derive
-import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HFoldable
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Number
+import Data.Comp.Multi.Ops
+import Data.Comp.Multi.Ordering
+import Data.Comp.Multi.Term
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Set (Set)
@@ -66,7 +74,7 @@
     -- default implementation returns @Nothing@.
     isVar :: f a :=> Maybe v
     isVar _ = Nothing
-    
+
     -- | Indicates the set of variables bound by the @f@ constructor
     -- for each argument of the constructor. For example for a
     -- non-recursive let binding:
@@ -89,10 +97,10 @@
     bindsVars _ = Map.empty
 
 $(derive [liftSum] [''HasVars])
-    
+
 -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
 -- @v@ is contained in the given set of variables.
-    
+
 isVar' :: (HasVars f v, Ord v) => Set v -> f a :=> Maybe v
 isVar' b t = do v <- isVar t
                 if v `Set.member` b
@@ -108,11 +116,11 @@
                      m :: Map (E (Numbered a)) (Set v)
                      m = bindsVars n
                      trans :: Numbered a :-> (a :*: K (Set v))
-                     trans x = unNumbered x :*: (K (Map.findWithDefault Set.empty (E x) m))
+                     trans x = unNumbered x :*: K (Map.findWithDefault Set.empty (E x) m)
                  in hfmap trans n
-                    
+
 -- | This combinator combines 'getBoundVars' with the 'mfmap' function.
-hfmapBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) 
+hfmapBoundVars :: forall f a b v i . (HasVars f v, HTraversable f)
                   => (Set v -> a :-> b) -> f a i -> f b i
 hfmapBoundVars f t = let n :: f (Numbered a) i
                          n = number t
@@ -121,9 +129,9 @@
                          trans :: Numbered a :-> b
                          trans x = f (Map.findWithDefault Set.empty (E x) m) (unNumbered x)
                      in hfmap trans n
-                        
--- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.   
-hfoldlBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) 
+
+-- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.
+hfoldlBoundVars :: forall f a b v i . (HasVars f v, HTraversable f)
                   => (b -> Set v ->  a :=> b) -> b -> f a i -> b
 hfoldlBoundVars f e t = let n :: f (Numbered a) i
                             n = number t
@@ -145,17 +153,17 @@
           alg t = C $ \vars -> case isVar t of
             Just v | not (v `Set.member` vars) -> Hole $ K v
             _  -> Term $ hfmapBoundVars run t
-              where 
+              where
                 run :: Set v -> C (Set v) (Context f (K v))  :-> Context f (K v)
                 run newVars f = f `unC` (newVars `Set.union` vars)
-                
+
 -- | Convert variables to holes, except those that are bound.
 containsVarAlg :: forall v f . (Ord v, HasVars f v, HTraversable f) => v -> Alg f (K Bool)
 containsVarAlg v t = K $ hfoldlBoundVars run local t
     where local = case isVar t of
                     Just v' -> v == v'
                     Nothing -> False
-          run :: Bool -> Set v -> (K Bool i) -> Bool
+          run :: Bool -> Set v -> K Bool i -> Bool
           run acc vars (K b) = acc || (not (v `Set.member` vars) && b)
 
 {-| This function checks whether a variable is contained in a context. -}
@@ -203,14 +211,14 @@
     substVars subst = doSubst Set.empty
       where doSubst :: Set v -> Cxt h f a :-> Cxt h f a
             doSubst _ (Hole a) = Hole a
-            doSubst b (Term t) = case isVar' b t >>= subst . K of 
+            doSubst b (Term t) = case isVar' b t >>= subst . K of
               Just new -> new
               Nothing  -> Term $ hfmapBoundVars run t
                 where run :: Set v -> Cxt h f a :-> Cxt h f a
-                      run vars s = doSubst (b `Set.union` vars) s
+                      run vars = doSubst (b `Set.union` vars)
 
 instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
-    substVars subst = hfmap (substVars subst) 
+    substVars subst = hfmap (substVars subst)
 
 {-| This function composes two substitutions @s1@ and @s2@. That is,
 applying the resulting substitution is equivalent to first applying
@@ -218,5 +226,4 @@
 
 compSubst :: (Ord v, HasVars f v, HTraversable f)
           => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
-compSubst s1 s2 = Map.map f s2
-    where f (A t) = A (appSubst s1 t)
+compSubst s1 = Map.map (\ (A t) -> A (appSubst s1 t))
diff --git a/src/Data/Comp/Number.hs b/src/Data/Comp/Number.hs
--- a/src/Data/Comp/Number.hs
+++ b/src/Data/Comp/Number.hs
@@ -6,13 +6,13 @@
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
 -- Portability :  non-portable (GHC Extensions)
--- 
+--
 -- This module provides functionality to number the components of a
 -- functorial value with consecutive integers.
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Number 
+module Data.Comp.Number
     ( Numbered (..)
     , unNumbered
     , number
@@ -39,7 +39,7 @@
 -- | This function numbers the components of the given functorial
 -- value with consecutive integers starting at 0.
 number :: Traversable f => f a -> f (Numbered a)
-number x = fst $ runState (mapM run x) 0 where
+number x = evalState (mapM run x) 0 where
   run b = do n <- get
              put (n+1)
              return $ Numbered (n,b)
diff --git a/src/Data/Comp/Ops.hs b/src/Data/Comp/Ops.hs
--- a/src/Data/Comp/Ops.hs
+++ b/src/Data/Comp/Ops.hs
@@ -1,7 +1,16 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses,
-             FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
-             ScopedTypeVariables, FunctionalDependencies, UndecidableInstances,
-             TypeFamilies, DataKinds, ConstraintKinds, PolyKinds #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE TypeSynonymInstances   #-}
+{-# LANGUAGE UndecidableInstances   #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -22,11 +31,11 @@
 import Data.Traversable
 
 import Control.Applicative
-import Control.Monad hiding (sequence, mapM)
+import Control.Monad hiding (mapM, sequence)
 import Data.Comp.SubsumeCommon
 
 
-import Prelude hiding (foldl, mapM, sequence, foldl1, foldr1, foldr)
+import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)
 
 
 -- Sums
@@ -42,7 +51,7 @@
 fromInl = caseF Just (const Nothing)
 
 fromInr :: (f :+: g) e -> Maybe (g e)
-fromInr = caseF (const Nothing) Just 
+fromInr = caseF (const Nothing) Just
 
 {-| Utility function to case on a functor sum, without exposing the internal
   representation of sums. -}
@@ -85,7 +94,7 @@
 
 type family Elem (f :: * -> *) (g :: * -> *) :: Emb where
     Elem f f = Found Here
-    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g) 
+    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g)
     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
     Elem f g = NotFound
 
@@ -119,7 +128,7 @@
 
 instance Subsume (Found p) f g => Subsume (Found (Le p)) f (g :+: g') where
     inj' _ = Inl . inj' (P :: Proxy (Found p))
-    
+
     prj' _ (Inl x) = prj' (P :: Proxy (Found p)) x
     prj' _ _       = Nothing
 
@@ -128,8 +137,8 @@
 
     prj' _ (Inr x) = prj' (P :: Proxy (Found p)) x
     prj' _ _       = Nothing
-              
-instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) 
+
+instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g)
     => Subsume (Found (Sum p1 p2)) (f1 :+: f2) g where
     inj' _ (Inl x) = inj' (P :: Proxy (Found p1)) x
     inj' _ (Inr x) = inj' (P :: Proxy (Found p2)) x
@@ -152,12 +161,12 @@
 proj :: forall f g a . (f :<: g) => g a -> Maybe (f a)
 proj = prj' (P :: Proxy (ComprEmb (Elem f g)))
 
-type f :=: g = (f :<: g, g :<: f) 
+type f :=: g = (f :<: g, g :<: f)
 
 
 
 spl :: (f :=: f1 :+: f2) => (f1 a -> b) -> (f2 a -> b) -> f a -> b
-spl f1 f2 x = case inj x of 
+spl f1 f2 x = case inj x of
             Inl y -> f1 y
             Inr y -> f2 y
 
diff --git a/src/Data/Comp/Ordering.hs b/src/Data/Comp/Ordering.hs
--- a/src/Data/Comp/Ordering.hs
+++ b/src/Data/Comp/Ordering.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeOperators, GADTs, TemplateHaskell #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators   #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Ordering
@@ -17,12 +19,11 @@
      OrdF(..)
     ) where
 
-import Data.Comp.Term
-import Data.Comp.Sum
-import Data.Comp.Ops
-import Data.Comp.Equality ()
 import Data.Comp.Derive
 import Data.Comp.Derive.Utils
+import Data.Comp.Equality ()
+import Data.Comp.Ops
+import Data.Comp.Term
 
 {-|
   From an 'OrdF' functor an 'Ord' instance of the corresponding
@@ -38,7 +39,7 @@
     compareF Hole{} Term{} = GT
 
 -- instance (OrdF f, Ord p) => OrdF (f :*: p) where
---     compareF (v1 :*: p1) (v2 :*: p2) = 
+--     compareF (v1 :*: p1) (v2 :*: p2) =
 --         case compareF v1 v2 of
 --           EQ ->  compare p1 p2
 --           res -> res
diff --git a/src/Data/Comp/Render.hs b/src/Data/Comp/Render.hs
--- a/src/Data/Comp/Render.hs
+++ b/src/Data/Comp/Render.hs
@@ -1,12 +1,13 @@
-{-# LANGUAGE TemplateHaskell, TypeSynonymInstances #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 module Data.Comp.Render where
 
-import Data.Foldable (toList)
-import Data.Tree (Tree (..))
-import Data.Tree.View
 import Data.Comp
 import Data.Comp.Derive
 import Data.Comp.Show ()
+import Data.Foldable (toList)
+import Data.Tree (Tree (..))
+import Data.Tree.View
 
 -- | The 'stringTree' algebra of a functor. The default instance creates a tree
 -- with the same structure as the term.
diff --git a/src/Data/Comp/Show.hs b/src/Data/Comp/Show.hs
--- a/src/Data/Comp/Show.hs
+++ b/src/Data/Comp/Show.hs
@@ -1,4 +1,7 @@
-{-# LANGUAGE TypeOperators, GADTs, TemplateHaskell, TypeSynonymInstances #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Show
@@ -17,12 +20,12 @@
     ( ShowF(..)
     ) where
 
-import Data.Comp.Term
-import Data.Comp.Annotation
 import Data.Comp.Algebra
+import Data.Comp.Annotation
 import Data.Comp.Derive (liftSum)
-import Data.Comp.Derive.Utils (derive)
 import Data.Comp.Derive.Show
+import Data.Comp.Derive.Utils (derive)
+import Data.Comp.Term
 
 instance (Functor f, ShowF f) => ShowF (Cxt h f) where
     showF (Hole s) = s
diff --git a/src/Data/Comp/SubsumeCommon.hs b/src/Data/Comp/SubsumeCommon.hs
--- a/src/Data/Comp/SubsumeCommon.hs
+++ b/src/Data/Comp/SubsumeCommon.hs
@@ -1,4 +1,7 @@
-{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -33,18 +36,18 @@
 data Emb = Found Pos | NotFound | Ambiguous
 
 -- | This type family takes a position type and compresses it. That
--- means it replaces each nested occurrence of 
--- 
+-- means it replaces each nested occurrence of
+--
 -- @
 --   Sum (prefix (Le Here)) (prefix (Ri Here))@
 -- @
 ---
--- with 
--- 
+-- with
+--
 -- @
 --   prefix Here@
 -- @
--- 
+--
 -- where @prefix@ is some composition of @Le@ and @Ri@. The rational
 -- behind this type family is that it provides a more compact proof
 -- term of a subsumption, and thus yields more efficient
@@ -54,8 +57,17 @@
     ComprPos Here = Here
     ComprPos (Le p) = Le (ComprPos p)
     ComprPos (Ri p) = Ri (ComprPos p)
-    ComprPos (Sum l r) = CombineMaybe (Sum l r) (Combine (ComprPos l) (ComprPos r))
+    ComprPos (Sum l r) = CombineRec (ComprPos l) (ComprPos r)
 
+
+-- | Helper type family for 'ComprPos'. Note that we could have
+-- defined this as a type synonym. But if we do that, performance
+-- becomes abysmal. I presume that the reason for this huge impact on
+-- performance lies in the fact that right-hand side of the defining
+-- equation duplicates the two arguments @l@ and @r@.
+type family CombineRec l r where
+    CombineRec l r = CombineMaybe (Sum l r) (Combine l r)
+
 -- | Helper type family for 'ComprPos'.
 type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where
     CombineMaybe p (Just p') = p'
@@ -86,7 +98,7 @@
 -- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If
 -- (1) finds no duplicates, @Found (ComprPos p)@ is returned;
 -- otherwise @Ambiguous@ is returned.
--- 
+--
 -- For (1) it is assumed that @p@ does not contain 'Sum' nested
 -- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a
 -- 'Sum'). We will refer to such positions below as /atomic position/.
diff --git a/src/Data/Comp/Sum.hs b/src/Data/Comp/Sum.hs
--- a/src/Data/Comp/Sum.hs
+++ b/src/Data/Comp/Sum.hs
@@ -1,6 +1,12 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, OverlappingInstances,
-  FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
-  ScopedTypeVariables, TemplateHaskell, ConstraintKinds, Rank2Types #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Sum
@@ -47,17 +53,17 @@
      substHoles'
     ) where
 
-import Data.Comp.Term
 import Data.Comp.Algebra
 import Data.Comp.Ops
+import Data.Comp.Term
 
-import Control.Monad hiding (mapM,sequence)
-import Prelude hiding (mapM,sequence)
+import Control.Monad hiding (mapM, sequence)
+import Prelude hiding (mapM, sequence)
 
-import Data.Maybe
-import Data.Traversable
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Maybe
+import Data.Traversable
 
 
 -- |Project the outermost layer of a term to a sub signature. If the signature
@@ -67,7 +73,7 @@
 
 -- |Project the outermost layer of a term to a sub signature. If the signature
 -- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.
-project_ :: (SigFunM Maybe f g) -> Cxt h f a -> Maybe (g (Cxt h f a))
+project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
 project_ _ (Hole _) = Nothing
 project_ f (Term t) = f t
 
@@ -84,7 +90,7 @@
 -- @deepProject@/n/ instead.
 deepProject_ :: (Traversable g) => (SigFunM Maybe f g) -> CxtFunM Maybe f g
 {-# INLINE deepProject_ #-}
-deepProject_ f = appSigFunM' f
+deepProject_ = appSigFunM'
 
 
 -- |Inject a term where the outermost layer is a sub signature. If the signature
@@ -94,7 +100,7 @@
 
 -- |Inject a term where the outermost layer is a sub signature. If the signature
 -- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
-inject_ :: (SigFun g f) -> g (Cxt h f a) -> Cxt h f a
+inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
 inject_ f = Term . f
 
 
@@ -110,7 +116,7 @@
 -- instead.
 deepInject_ :: (Functor g) => SigFun g f -> CxtFun g f
 {-# INLINE deepInject_ #-}
-deepInject_ f = appSigFun f
+deepInject_ = appSigFun
 
 
 split :: (f :=: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
@@ -156,5 +162,5 @@
 
 instance (Eq (f a), Eq (g a)) => Eq ((f :+: g) a) where
     (Inl x) == (Inl y) = x == y
-    (Inr x) == (Inr y) = x == y                   
+    (Inr x) == (Inr y) = x == y
     _ == _ = False
diff --git a/src/Data/Comp/Term.hs b/src/Data/Comp/Term.hs
--- a/src/Data/Comp/Term.hs
+++ b/src/Data/Comp/Term.hs
@@ -1,4 +1,9 @@
-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types, TypeSynonymInstances, FlexibleInstances #-}
+{-# LANGUAGE EmptyDataDecls       #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE Rank2Types           #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Term
@@ -30,11 +35,11 @@
 import Control.Applicative hiding (Const)
 import Control.Monad hiding (mapM, sequence)
 
-import Data.Traversable
 import Data.Foldable
+import Data.Traversable
 import Unsafe.Coerce
 
-import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
+import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)
 
 
 {-|  -}
@@ -124,11 +129,11 @@
     traverse f = run
         where run (Hole a) = Hole <$> f a
               run (Term t) = Term <$> traverse run t
-                          
+
     sequenceA (Hole a) = Hole <$> a
     sequenceA (Term t) = Term <$> traverse sequenceA t
 
-    mapM f = run 
+    mapM f = run
         where run (Hole a) = liftM Hole $ f a
               run (Term t) = liftM Term $ mapM run t
 
diff --git a/src/Data/Comp/TermRewriting.hs b/src/Data/Comp/TermRewriting.hs
--- a/src/Data/Comp/TermRewriting.hs
+++ b/src/Data/Comp/TermRewriting.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE Rank2Types, GADTs #-}
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE Rank2Types #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.TermRewriting
@@ -17,16 +18,16 @@
 
 import Prelude hiding (any)
 
-import Data.Comp.Term
-import Data.Comp.Sum
 import Data.Comp.Algebra
 import Data.Comp.Equality
 import Data.Comp.Matching
+import Data.Comp.Sum
+import Data.Comp.Term
+import Data.Foldable
 import Data.Map (Map)
 import qualified Data.Map as Map
-import qualified Data.Set as Set
 import Data.Maybe
-import Data.Foldable
+import qualified Data.Set as Set
 
 import Control.Monad
 
@@ -84,7 +85,7 @@
 
 appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
           => Rule f f v -> Step (Cxt h f a)
-appRule rule t = do 
+appRule rule t = do
   (res, subst) <- matchRule rule t
   return $ substHoles' res subst
 
@@ -134,10 +135,10 @@
 parallelStep _ Hole{} = Nothing
 parallelStep trs c@(Term t) =
     case matchRules trs c of
-      Nothing 
+      Nothing
           | anyBelow -> Just $ Term $ fmap fst below
           | otherwise -> Nothing
-        where below = fmap (bStep $ parallelStep trs) t 
+        where below = fmap (bStep $ parallelStep trs) t
               anyBelow = any snd below
       Just (rhs,subst) -> Just $ substHoles' rhs substBelow
           where rhsVars = Set.fromList $ toList rhs
@@ -145,7 +146,7 @@
                 apply v t
                     | Set.member v rhsVars = Just $ fst $ bStep (parallelStep trs) t
                     | otherwise = Nothing
-                
+
 
 {-| This function applies the given reduction step repeatedly until a
 normal form is reached. -}
diff --git a/src/Data/Comp/Thunk.hs b/src/Data/Comp/Thunk.hs
--- a/src/Data/Comp/Thunk.hs
+++ b/src/Data/Comp/Thunk.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, ScopedTypeVariables, ConstraintKinds #-}
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -36,20 +40,20 @@
     ,strict
     ,strictAt) where
 
-import Data.Comp.Term
-import Data.Comp.Equality
 import Data.Comp.Algebra
-import Data.Comp.Ops ((:+:)(..), fromInr)
-import Data.Comp.Sum
+import Data.Comp.Equality
 import Data.Comp.Number
+import Data.Comp.Ops ((:+:) (..), fromInr)
+import Data.Comp.Sum
+import Data.Comp.Term
 import Data.Foldable hiding (and)
 
 import qualified Data.Set as Set
 
+import Control.Monad hiding (mapM, sequence)
 import Data.Traversable
-import Control.Monad hiding (sequence,mapM)
 
-import Prelude hiding (foldr, foldl,foldr1, foldl1,sequence,mapM)
+import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)
 
 
 -- | This type represents terms with thunks.
@@ -98,7 +102,7 @@
 -- (using 'whnf') according to the given function.
 eval2 :: Monad m => (f (TermT m f) -> f (TermT m f) -> TermT m f)
                  -> TermT m f -> TermT m f -> TermT m f
-eval2 cont x y = (\ x' -> cont x' `eval` y) `eval` x 
+eval2 cont x y = (\ x' -> cont x' `eval` y) `eval` x
 
 -- | This function evaluates all thunks.
 nf :: (Monad m, Traversable f) => TermT m f -> m (Term f)
@@ -112,11 +116,11 @@
 
 -- | This function inspects a term (using 'nf') according to the
 -- given function.
-deepEval :: (Traversable f, Monad m) => 
+deepEval :: (Traversable f, Monad m) =>
             (Term f -> TermT m f) -> TermT m f -> TermT m f
-deepEval cont v = case deepProject_ fromInr v of 
+deepEval cont v = case deepProject_ fromInr v of
                     Just v' -> cont v'
-                    _ -> thunk $ liftM cont $ nf v 
+                    _ -> thunk $ liftM cont $ nf v
 
 infixl 1 #>>
 
diff --git a/src/Data/Comp/Unification.hs b/src/Data/Comp/Unification.hs
--- a/src/Data/Comp/Unification.hs
+++ b/src/Data/Comp/Unification.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 -------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Unification
@@ -15,9 +16,9 @@
 
 module Data.Comp.Unification where
 
+import Data.Comp.Decompose
 import Data.Comp.Term
 import Data.Comp.Variables
-import Data.Comp.Decompose
 
 import Control.Monad.Error
 import Control.Monad.State
@@ -87,12 +88,12 @@
 withNextEq :: Monad m
            => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()
 withNextEq m = do eqs <- gets usEqs
-                  case eqs of 
+                  case eqs of
                     [] -> return ()
                     x : xs -> modify (\s -> s {usEqs = xs})
                            >> m x
 
-putEqs :: Monad m 
+putEqs :: Monad m
        => Equations f -> UnifyM f v m ()
 putEqs eqs = modify addEqs
     where addEqs s = s {usEqs = eqs ++ usEqs s}
@@ -108,7 +109,7 @@
          => UnifyM f v m ()
 runUnify = withNextEq (\ e -> unifyStep e >> runUnify)
 
-unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) 
+unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)
           => Equation f -> UnifyM f v m ()
 unifyStep (s,t) = case decompose s of
                     Var v1 -> case decompose t of
diff --git a/src/Data/Comp/Variables.hs b/src/Data/Comp/Variables.hs
--- a/src/Data/Comp/Variables.hs
+++ b/src/Data/Comp/Variables.hs
@@ -1,5 +1,9 @@
-{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances,
-  OverlappingInstances, TypeOperators, TemplateHaskell #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances  #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeOperators         #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -32,17 +36,17 @@
      getBoundVars
     ) where
 
-import Data.Comp.Term
-import Data.Comp.Number
 import Data.Comp.Algebra
 import Data.Comp.Derive
+import Data.Comp.Number
+import Data.Comp.Term
 import Data.Foldable hiding (elem, notElem)
+import Data.Map (Map)
+import qualified Data.Map as Map
 import Data.Maybe
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Map (Map)
-import qualified Data.Map as Map
-import Prelude hiding (or, foldl)
+import Prelude hiding (foldl, or)
 
 -- | This type represents substitutions of contexts, i.e. finite
 -- mappings from variables to contexts.
@@ -60,7 +64,7 @@
     -- default implementation returns @Nothing@.
     isVar :: f a -> Maybe v
     isVar _ = Nothing
-    
+
     -- | Indicates the set of variables bound by the @f@ constructor
     -- for each argument of the constructor. For example for a
     -- non-recursive let binding:
@@ -87,13 +91,13 @@
 
 -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
 -- @v@ is contained in the given set of variables.
-    
+
 isVar' :: (HasVars f v, Ord v) => Set v -> f a -> Maybe v
 isVar' b t = do v <- isVar t
                 if v `Set.member` b
                    then Nothing
                    else return v
-   
+
 -- | This combinator pairs every argument of a given constructor with
 -- the set of (newly) bound variables according to the corresponding
 -- 'HasVars' type class instance.
@@ -102,19 +106,19 @@
                      m = bindsVars n
                      trans x = (Map.findWithDefault Set.empty x m, unNumbered x)
                  in fmap trans n
-                    
+
 -- | This combinator combines 'getBoundVars' with the generic 'fmap' function.
 fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b
 fmapBoundVars f t = let n = number t
                         m = bindsVars n
                         trans x = f (Map.findWithDefault Set.empty x m) (unNumbered x)
-                    in fmap trans n                    
-                    
--- | This combinator combines 'getBoundVars' with the generic 'foldl' function.   
+                    in fmap trans n
+
+-- | This combinator combines 'getBoundVars' with the generic 'foldl' function.
 foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b
 foldlBoundVars f e t = let n = number t
                            m = bindsVars n
-                           trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y) 
+                           trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y)
                        in foldl trans e n
 
 -- | Convert variables to holes, except those that are bound.
@@ -124,7 +128,7 @@
           alg t vars = case isVar t of
             Just v | not (v `Set.member` vars) -> Hole v
             _  -> Term $ fmapBoundVars run t
-              where 
+              where
                 run newVars f = f $ newVars `Set.union` vars
 
 -- |Algebra for checking whether a variable is contained in a term, except those
@@ -181,13 +185,13 @@
         -- subst f = free (substAlg f) Hole
   substVars subst = doSubst Set.empty
     where doSubst _ (Hole a) = Hole a
-          doSubst b (Term t) = case isVar' b t >>= subst of 
+          doSubst b (Term t) = case isVar' b t >>= subst of
             Just new -> new
             Nothing  -> Term $ fmapBoundVars run t
-              where run vars s = doSubst (b `Set.union` vars) s
+              where run vars = doSubst (b `Set.union` vars)
 
 instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where
-    substVars f = fmap (substVars f) 
+    substVars f = fmap (substVars f)
 
 {-| This function composes two substitutions @s1@ and @s2@. That is,
 applying the resulting substitution is equivalent to first applying
diff --git a/testsuite/tests/Data/Comp/Subsume_Test.hs b/testsuite/tests/Data/Comp/Subsume_Test.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Subsume_Test.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies #-}
+
+-- | This module exports a dummy test to force type checking of this
+-- module. In this module we test the subtyping system.
+
+module Data.Comp.Subsume_Test where
+
+import Data.Comp
+import Data.Comp.Ops
+import Data.Comp.SubsumeCommon
+
+
+import Test.Framework
+import Test.Framework.Providers.QuickCheck2
+
+
+data S1 a = S1 a
+data S2 a = S2 a
+data S3 a = S3 a
+data S4 a = S4 a
+
+type TA = S1 :+: S2
+type TB = S3 :+: S4
+type T1 = TA :+: TB
+type T2 = TB :+: TA
+type T3 = S2 :+: TB
+
+test1 :: ComprEmb (Elem T1 T1) ~ (Found Here) => Int
+test1 = 1
+
+test2 :: ComprEmb (Elem T1 T2) ~ (Found (Sum (Ri Here) (Le Here))) => Int
+test2 = 1
+
+test3 :: ComprEmb (Elem (T1 :+: S1) T2) ~ Ambiguous => Int
+test3 = 1
+
+test4 :: ComprEmb (Elem T1 (T2 :+: S1)) ~ Ambiguous => Int
+test4 = 1
+
+test5 :: ComprEmb (Elem T1 T3) ~ NotFound => Int
+test5 = 1
+
+test6 :: ComprEmb (Elem TB T1) ~ (Found (Ri Here)) => Int
+test6 = 1
+
+test7 :: ComprEmb (Elem T3 T1) ~ (Found (Sum (Le (Ri Here))(Ri Here))) => Int
+test7 = 1
+
+main = defaultMain [tests]
+
+tests = testGroup "Subsume" [
+         testProperty "prop_typecheck" prop_typecheck
+        ]
+
+-- dummy test
+prop_typecheck = True
diff --git a/testsuite/tests/Data/Comp_Test.hs b/testsuite/tests/Data/Comp_Test.hs
--- a/testsuite/tests/Data/Comp_Test.hs
+++ b/testsuite/tests/Data/Comp_Test.hs
@@ -6,6 +6,7 @@
 import qualified Data.Comp.Examples_Test
 import qualified Data.Comp.Variables_Test
 import qualified Data.Comp.Multi_Test
+import qualified Data.Comp.Subsume_Test
 
 --------------------------------------------------------------------------------
 -- Test Suits
@@ -17,7 +18,8 @@
          Data.Comp.Equality_Test.tests,
          Data.Comp.Examples_Test.tests,
          Data.Comp.Variables_Test.tests,
-         Data.Comp.Multi_Test.tests
+         Data.Comp.Multi_Test.tests,
+         Data.Comp.Subsume_Test.tests
         ]
 
 --------------------------------------------------------------------------------