diff --git a/rest-rewrite.cabal b/rest-rewrite.cabal
--- a/rest-rewrite.cabal
+++ b/rest-rewrite.cabal
@@ -1,6 +1,6 @@
 name:               rest-rewrite
 build-type:         Simple
-version:            0.4.0
+version:            0.4.1
 cabal-version:      2.0
 category:           Rewriting
 maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>
@@ -53,12 +53,12 @@
   hs-source-dirs: src
   build-depends:  base                 >= 4.7 && < 5
                 , containers           >= 0.6.2 && < 0.7
-                , hashable             >= 1.3.0 && < 1.4
+                , hashable             >= 1.3.0 && < 1.5
                 , process              >= 1.6.9 && < 1.7
                 , parsec               >= 3.1.14 && < 3.2
-                , mtl                  >= 2.2.2 && < 2.3
+                , mtl                  >= 2.2.2 && < 2.4
                 , unordered-containers >= 0.2.13 && < 0.3
-                , text                 >= 1.2.4 && < 1.3
+                , text                 >= 1.2.4 && < 2.1
 
 library testlib
   default-language:  Haskell2010
@@ -72,8 +72,8 @@
                 , mtl
                 , monad-loops >= 0.4.3 && < 0.5
                 , unordered-containers >= 0.2.11
-                , text >= 1.2.2
-                , time >= 1.9.3 && < 1.10
+                , text
+                , time >= 1.9.3 && < 1.13
   exposed-modules:
       Arith
       DSL
@@ -123,8 +123,8 @@
                 , mtl
                 , unordered-containers >= 0.2.11
                 , testlib
-                , text >= 1.2.2
-                , time >= 1.9.3 && < 1.10
+                , text
+                , time
                 -- , liquidhaskell
                 -- , liquid-base
   other-modules:
diff --git a/src/Language/REST/Dot.hs b/src/Language/REST/Dot.hs
--- a/src/Language/REST/Dot.hs
+++ b/src/Language/REST/Dot.hs
@@ -37,7 +37,7 @@
   deriving (Read)
 
 -- | A GraphViz node
-data Node = Node 
+data Node = Node
     { nodeID     :: NodeID
     , label      :: String
     , nodeStyle  :: String
@@ -60,9 +60,9 @@
 
 edgeString :: Edge -> String
 edgeString (Edge efrom eto elabel color esubLabel style) =
-    let 
+    let
         sub = escape esubLabel
-        escape xs = concatMap go xs
+        escape = concatMap go
             where
                 go '\\' = "\\"
                 go '\n' = "<br />"
@@ -77,8 +77,8 @@
         printf "\t%s -> %s [label = <%s<br/>%s>\ncolor=\"%s\"\nstyle=\"%s\"];" efrom eto labelPart sub color style
 
 graphString :: DiGraph -> String
-graphString (DiGraph name nodes edges) = 
-    printf "digraph %s {\n%s\n\n%s\n}" name (nodesString) (edgesString)
+graphString (DiGraph name nodes edges) =
+    printf "digraph %s {\n%s\n\n%s\n}" name nodesString edgesString
     where
         nodesString :: String
         nodesString = intercalate "\n" (map nodeString (S.toList nodes))
diff --git a/src/Language/REST/ExploredTerms.hs b/src/Language/REST/ExploredTerms.hs
--- a/src/Language/REST/ExploredTerms.hs
+++ b/src/Language/REST/ExploredTerms.hs
@@ -50,7 +50,7 @@
 -- | A mapping of terms, to the rewritten terms that need to be fully explored
 -- | in order for this term to be fully explored
 data ExploredTerms term c m =
-  ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs term c m) ExploreStrategy
+  ET (M.HashMap term (c, S.HashSet term)) (ExploreFuncs term c m) ExploreStrategy
 
 size :: ExploredTerms term c m -> Int
 size (ET m _ _) = M.size m
@@ -64,9 +64,9 @@
 insert :: (Eq term, Hashable term) => term -> c -> S.HashSet term -> ExploredTerms term c m -> ExploredTerms term c m
 insert t oc s (ET etMap ef@(EF union _ _) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy
   where
-    go (oc1, s1) (oc2, s2) = (union oc1 oc2, S.union s1 s2)
+    go (oc1, s1) (oc2, s2) = (oc1 `union` oc2, S.union s1 s2)
 
-lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, (S.HashSet term))
+lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, S.HashSet term)
 lookup t (ET etMap _ _) = M.lookup t etMap
 
 -- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is
@@ -97,14 +97,14 @@
                           -- would allow exploration of each t in trms,
                           -- at the constraints generated by the step from h to t
                           trms' = S.map (\t -> (t, exRefine oc' h t)) trms
-                          ts    = (S.union trms' (S.fromList rest)) `S.difference` seen'
+                          ts    = S.union trms' (S.fromList rest) `S.difference` seen'
                         in
                           go seen' (S.toList ts)
                   where
                     seen' = S.insert (h, oc') seen
 
   -- There exists a reachable term that has never previously been seen; not fully explored
-  go _ _        | otherwise = return False
+  go _ _         = return False
 
 -- | @'shouldExplore' t c et@ determines if rewrites originating from term @t@ at
 --   constraints @c@ should be considered, given the already explored terms of @et@
diff --git a/src/Language/REST/Internal/ListT.hs b/src/Language/REST/Internal/ListT.hs
--- a/src/Language/REST/Internal/ListT.hs
+++ b/src/Language/REST/Internal/ListT.hs
@@ -5,14 +5,13 @@
 import           Control.Applicative
 import           Control.Monad.Trans
 
-data ListT m a = ListT {
+newtype ListT m a = ListT {
   runListT :: m [a]
 }
 
 instance (Monad m) => Functor (ListT m) where
   fmap f (ListT mxs) = ListT $ do
-    xs <- mxs
-    return $ map f xs
+    map f <$> mxs
 
 instance (Monad m) => Applicative (ListT m) where
   pure x                    = ListT (return [x])
diff --git a/src/Language/REST/Internal/MultiSet.hs b/src/Language/REST/Internal/MultiSet.hs
--- a/src/Language/REST/Internal/MultiSet.hs
+++ b/src/Language/REST/Internal/MultiSet.hs
@@ -26,7 +26,7 @@
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
 
-data MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord)
+newtype MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord)
 
 instance Show a => Show (MultiSet a) where
   show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}"
@@ -42,7 +42,7 @@
 deleteMany :: (Hashable a, Eq a) => a -> Int -> MultiSet a -> MultiSet a
 deleteMany k v (MultiSet ms) | Just c <- M.lookup k ms
                              , c > v = MultiSet $ M.insert k (c - v) ms
-deleteMany k _ (MultiSet ms) | otherwise = MultiSet $ M.delete k ms
+deleteMany k _ (MultiSet ms)  = MultiSet $ M.delete k ms
 
 distinctElems :: MultiSet a -> [a]
 distinctElems (MultiSet ms) = M.keys ms
@@ -69,12 +69,12 @@
 toList :: MultiSet a -> [a]
 toList ms = concatMap go (toOccurList ms)
   where
-    go (k, num) = take num $ repeat k
+    go (k, num) = replicate num k
 
 insert :: (Eq a, Hashable a) => a -> MultiSet a -> MultiSet a
 insert k (MultiSet ms) | Just c <- M.lookup k ms
                        = MultiSet $ M.insert k (c + 1) ms
-insert k (MultiSet ms) | otherwise
+insert k (MultiSet ms)
                        = MultiSet $ M.insert k 1 ms
 
 singleton :: (Eq a, Hashable a) => a -> MultiSet a
diff --git a/src/Language/REST/Internal/MultisetOrder.hs b/src/Language/REST/Internal/MultisetOrder.hs
--- a/src/Language/REST/Internal/MultisetOrder.hs
+++ b/src/Language/REST/Internal/MultisetOrder.hs
@@ -25,10 +25,10 @@
 trace' _ x = x
 
 removeEQs :: (Eq x, Ord x, Hashable x) => MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)
-removeEQs ts0 us0 = go (M.toList ts0) M.empty us0 where
+removeEQs ts0 = go (M.toList ts0) M.empty where
   go []       ts us                   = (ts, us)
   go (x : xs) ts us | x `M.member` us = go xs ts (M.delete x us)
-  go (x : xs) ts us | otherwise       = go xs (M.insert x ts) us
+  go (x : xs) ts us        = go xs (M.insert x ts) us
 
 data Replace a =
     ReplaceOne a a
@@ -40,8 +40,8 @@
 powerset (x:xs) = [x:ps | ps <- powerset xs] ++ powerset xs
 
 possibilities :: (Hashable a, Eq a) => Relation -> [a] -> [a] -> S.HashSet (S.HashSet (Replace a))
-possibilities r []     []    = if r == GT then S.empty else S.singleton (S.empty)
-possibilities r xs     []    = if r == EQ then S.empty else S.singleton (S.fromList $ map (flip Replace S.empty)  xs)
+possibilities r []     []    = if r == GT then S.empty else S.singleton S.empty
+possibilities r xs     []    = if r == EQ then S.empty else S.singleton (S.fromList $ map (`Replace` S.empty)  xs)
 possibilities _ []     (_:_) = S.empty
 possibilities r (x:xs) ys    = if r == EQ then eqs else S.union eqs doms where
   eqs = S.unions $ map go ys where
@@ -60,7 +60,7 @@
      ConstraintGen oc base lifted m
   -> ConstraintGen oc base (MultiSet lifted) m
 multisetOrder _          impl _ oc _   _   | oc == unsatisfiable impl = return $ unsatisfiable impl
-multisetOrder underlying impl r oc ts0 us0 = (uncurry go) (removeEQs ts0 us0) where
+multisetOrder underlying impl r oc ts0 us0 = uncurry go (removeEQs ts0 us0) where
   go :: MultiSet lifted -> MultiSet lifted -> m (oc base)
   go ts us | M.null ts && M.null us             = return $ if r == GT then unsatisfiable impl else oc
   go ts us | not (M.null ts) && M.null us       = return $ if r == EQ then unsatisfiable impl else oc
@@ -71,7 +71,7 @@
       pos = possibilities r (M.toList ts) (M.toList us)
 
       result =
-        trace' ("There are " ++ (show $ S.size pos) ++ " possibilities") $
+        trace' ("There are " ++ show (S.size pos) ++ " possibilities") $
         unionAll impl <$> mapM posConstraints (S.toList pos)
 
       posConstraints pos1 = L.foldl' apply (return oc) (S.toList pos1) where
@@ -82,4 +82,4 @@
           oc' <- moc
           if S.null ts'
             then return oc'
-            else intersectAll impl <$> (mapM (underlying impl GT oc' t) (S.toList ts'))
+            else intersectAll impl <$> mapM (underlying impl GT oc' t) (S.toList ts')
diff --git a/src/Language/REST/Internal/OpOrdering.hs b/src/Language/REST/Internal/OpOrdering.hs
--- a/src/Language/REST/Internal/OpOrdering.hs
+++ b/src/Language/REST/Internal/OpOrdering.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE DeriveAnyClass #-}
+
+
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+
 
 -- | This module defines an interface for 'WQO's on 'Op'erators,
 --   for example, that are used as the precedence for an [RPQO]("Language.REST.RPO").
diff --git a/src/Language/REST/Internal/PartialOrder.hs b/src/Language/REST/Internal/PartialOrder.hs
--- a/src/Language/REST/Internal/PartialOrder.hs
+++ b/src/Language/REST/Internal/PartialOrder.hs
@@ -82,7 +82,7 @@
     result = PartialOrder $ M.insertWith S.union f decs $ M.mapWithKey go m
 
     go k old | S.member k ascs = S.union old decs
-    go _ v   | otherwise       = v
+    go _ v          = v
 
     ascs = ascendants f o
     decs = S.insert g $ descendents g o
@@ -125,7 +125,7 @@
 
   descs = S.unions (map (`descendents` po) froms)
 
-  filtered = M.filterWithKey (\k _ -> not $ k `elem` froms) m
+  filtered = M.filterWithKey (\k _ -> k `notElem` froms) m
   m' =
     if S.null descs
     then filtered
@@ -134,6 +134,6 @@
   result = PartialOrder $ M.map go m'
 
   go s | hasFrom s = S.insert to $ S.union descs $ S.difference s from'
-  go s | otherwise = s
+  go s  = s
 
   hasFrom set = any (`S.member` set) froms
diff --git a/src/Language/REST/Internal/Rewrite.hs b/src/Language/REST/Internal/Rewrite.hs
--- a/src/Language/REST/Internal/Rewrite.hs
+++ b/src/Language/REST/Internal/Rewrite.hs
@@ -13,6 +13,7 @@
 
 import GHC.Generics (Generic)
 
+import           Data.Maybe (isNothing)
 import           Data.Hashable
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
@@ -61,7 +62,7 @@
 unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
 unify (MT.Var s) term su | M.lookup s su == Just term
   = Just su
-unify (MT.Var s) term su | M.lookup s su == Nothing
+unify (MT.Var s) term su | isNothing (M.lookup s su)
   = Just $ M.insert s term su
 unify (MT.RWApp o1 xs) (App o2 ys) su | o1 == o2 && length xs == length ys =
   unifyAll su (zip xs ys)
@@ -71,4 +72,4 @@
   apply t (Rewrite left right _) = return $ S.unions $ map go (subTerms t)
     where
       go (t', tf) | Just su <- unify left t' M.empty = S.singleton (tf $ subst su right)
-      go _        | otherwise                        = S.empty
+      go _                                = S.empty
diff --git a/src/Language/REST/Internal/WQO.hs b/src/Language/REST/Internal/WQO.hs
--- a/src/Language/REST/Internal/WQO.hs
+++ b/src/Language/REST/Internal/WQO.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
 
 module Language.REST.Internal.WQO (
       empty
@@ -86,10 +87,8 @@
     show (WQO ecs po) = L.intercalate " ∧ " (map show ecs' ++ po')
         where
             ecs'          = filter (not . EC.isSingleton) $ S.toList ecs
-            po'           = 
-                if PO.isEmpty po 
-                    then []
-                    else [show po]
+            po'           =
+                [show po | not (PO.isEmpty po)]
             --         else [show $ PO.mapUnsafe ecHead po]
             -- ecHead (x, y) = (EC.head x, EC.head y)
 
@@ -100,7 +99,7 @@
 empty = WQO S.empty PO.empty
 
 singleton :: (Ord a, Eq a, Hashable a) => (a, a, QORelation) -> Maybe (WQO a)
-singleton t = insertMaybe empty t
+singleton = insertMaybe empty
 
 {-# INLINE elems #-}
 elems :: (Ord a) => WQO a -> S.Set a
@@ -133,7 +132,7 @@
     t <- L.find (EC.isMember source) classes'
     if EC.isMember target t
       then return (t, t)
-      else ((,) t) <$> L.find (EC.isMember target) classes'
+      else (t,) <$> L.find (EC.isMember target) classes'
   where
     classes' = S.toList classes
 
@@ -142,12 +141,12 @@
 {-# INLINE getRelation #-}
 getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation
 getRelation _ f g | f == g = Just QEQ
-getRelation wqo@(WQO _ po) source target 
+getRelation wqo@(WQO _ po) source target
     | Just (s, t) <- getEquivalenceClasses' wqo source target
     = if s == t
         then Just QEQ
-        else 
-            if PO.gt po s t 
+        else
+            if PO.gt po s t
                 then Just QGT
                 else Nothing
     | otherwise = Nothing
@@ -192,7 +191,7 @@
     let
       Just ec' = M.lookup ec ecsMap
     in
-      descs `S.isSubsetOf` (PO.descendents ec' po')
+      descs `S.isSubsetOf` PO.descendents ec' po'
 
 
 
@@ -211,16 +210,16 @@
 merge :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a)
 merge lhs@(WQO ecs po) rhs@(WQO ecs' po') | S.disjoint (elems lhs) (elems rhs)
   = Just $ WQO (S.union ecs ecs') (PO.unionDisjointUnsafe po po')
-merge lhs rhs | otherwise =
+merge lhs rhs  =
   if S.size (elems lhs) >= S.size (elems rhs)
   then merge' lhs rhs
   else merge' rhs lhs
 
 {-# SPECIALISE merge' :: WQO Op -> WQO Op -> Maybe (WQO Op) #-}
 merge' :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a)
-merge' lhs rhs@(WQO ecs po) = trace' message $ result where
+merge' lhs rhs@(WQO ecs po) = trace' message result where
 
-    message = "Merge " ++ (show $ hash lhs) ++ " " ++ (show $ hash rhs)
+    message = "Merge " ++ show (hash lhs) ++ " " ++ show (hash rhs)
 
     withEQs' = go lhs ecsFacts
 
@@ -235,10 +234,10 @@
         let
             xs = EC.toList ec
         in
-            map (\(a, b) -> (a, b, QEQ)) (zip xs (tail xs))
+            zipWith (\ a b -> (a, b, QEQ)) xs (tail xs)
 
     poFacts :: [(a, a, QORelation)]
-    poFacts = 
+    poFacts =
         map (\(a, b) -> (head (EC.toList a), head (EC.toList b), QGT)) (PO.toList po)
 
     go r []       = Just r
@@ -276,7 +275,7 @@
   go wqo ((f, g) : xs) | Just r  <- getRelation wqo0 g f
                        , wqo'    <- get wqo $ insert wqo (g, f, r)
                        = go wqo' xs
-  go wqo (_ : xs)      | otherwise = go wqo xs
+  go wqo (_ : xs)       = go wqo xs
 
 {-# INLINE insertMaybe #-}
 {-# SPECIALISE insertMaybe :: WQO Op -> (Op, Op, QORelation) -> Maybe (WQO Op) #-}
@@ -291,13 +290,13 @@
 {-# SPECIALISE insert :: WQO Op -> (Op, Op, QORelation) -> ExtendOrderingResult Op #-}
 insert :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
 insert _   (f, g, QGT)  | f == g = Contradicts
-insert wqo (f, g, r)    | Just r' <- getRelation wqo f g 
+insert wqo (f, g, r)    | Just r' <- getRelation wqo f g
                         = if r == r' then AlreadyImplied else Contradicts
 insert wqo (f, g, _)    | isJust $ getRelation wqo g f = Contradicts
 
 insert wqo@(WQO ecs po) (f, g, QEQ) = ValidExtension $
     case getEquivalenceClasses wqo f g of
-        (Nothing, Nothing) -> 
+        (Nothing, Nothing) ->
             let
                 ecs' = S.insert (EC.fromList [f, g]) ecs
             in
@@ -308,7 +307,7 @@
 
 insert wqo@(WQO ecs po) (f, g, QGT) = ValidExtension $
     case getEquivalenceClasses wqo f g of
-        (Nothing, Nothing) -> 
+        (Nothing, Nothing) ->
             let
                 f'       = EC.singleton f
                 g'       = EC.singleton g
@@ -316,7 +315,7 @@
                 Just po' = PO.insert po f' g'
             in
                 WQO ecs' po'
-        (Just ec, Nothing)   -> 
+        (Just ec, Nothing)   ->
             let
                 g'       = EC.singleton g
                 ecs'     = S.insert g' ecs
@@ -324,14 +323,14 @@
             in
                 WQO ecs' po'
 
-        (Nothing, Just ec) -> 
+        (Nothing, Just ec) ->
             let
                 f'       = EC.singleton f
                 ecs'     = S.insert f' ecs
                 Just po' = PO.insert po f' ec
             in
                 WQO ecs' po'
-        (Just ec1, Just ec2) -> 
+        (Just ec1, Just ec2) ->
             WQO ecs (PO.insertUnsafe po ec1 ec2)
 
 -- | Generates all the possible orderings of the elements in the given set.
diff --git a/src/Language/REST/KBO.hs b/src/Language/REST/KBO.hs
--- a/src/Language/REST/KBO.hs
+++ b/src/Language/REST/KBO.hs
@@ -12,7 +12,7 @@
 import qualified Data.Map as M
 
 termOps :: RuntimeTerm -> [Op]
-termOps (App f xs) = f:(concatMap termOps xs)
+termOps (App f xs) = f:concatMap termOps xs
 
 arityConstraints :: RuntimeTerm -> SMTExpr Bool
 arityConstraints t = toExpr $ go M.empty t where
@@ -22,7 +22,7 @@
   go m (App f ts)  = foldl go (M.insert f 0 m) ts
 
   toExpr m = And $ map toConstraint (M.toList m)
-  toConstraint (sym, n) = toSMT sym `smtGTE` (Const n)
+  toConstraint (sym, n) = toSMT sym `smtGTE` Const n
 
 
 -- | @kboGTE t u@ returns the SMT expression describing constraints
diff --git a/src/Language/REST/LPO.hs b/src/Language/REST/LPO.hs
--- a/src/Language/REST/LPO.hs
+++ b/src/Language/REST/LPO.hs
@@ -1,11 +1,11 @@
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE DeriveAnyClass #-}
+
+
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ImplicitParams #-}
 
+
+
+
 module Language.REST.LPO (lpo, lpoStrict) where
 
 import Prelude hiding (EQ, GT, lex)
@@ -50,7 +50,7 @@
 lpo' False oc EQ cs (App f ts) (App g us) =
   let
     cs'  = intersect oc cs (singleton oc $ f =. g)
-    subs = map (uncurry $ lpo' False oc EQ cs') (zip ts us)
+    subs = zipWith (lpo' False oc EQ cs') ts us
   in
     intersectAll oc (cs' : subs)
 
@@ -74,12 +74,12 @@
     case3 =
       if strict && f /= g
       then unsatisfiable oc
-      else intersectAll oc ([tDominatesUs, (lex oc (r == GT) cs (lpo' strict) ts us)] ++ symEQ) where
-        symEQ = if f == g then [] else [singleton oc (f =. g)]
+      else intersectAll oc ([tDominatesUs, lex oc (r == GT) cs (lpo' strict) ts us] ++ symEQ) where
+        symEQ = [singleton oc (f =. g) | f /= g]
 
 
     tDominatesUs = intersectAll oc (map go us) where
-      go ui = lpo' strict oc GT cs t ui
+      go = lpo' strict oc GT cs t
 
 
 -- | Constraint generator for a quasi-order extension to the Lexicographic path ordering
diff --git a/src/Language/REST/OCAlgebra.hs b/src/Language/REST/OCAlgebra.hs
--- a/src/Language/REST/OCAlgebra.hs
+++ b/src/Language/REST/OCAlgebra.hs
@@ -23,7 +23,7 @@
   where
     isSat'  c             = return $ c >= 0
     refine' c _ _         = c - 1
-    union'  c c'          = max c c'
+    union'                = max
     notStrongerThan' c c' = return $ c >= c'
 
 -- | @contramap f oca@ transforms an OCA of terms of type @a@ terms of type @b@,
diff --git a/src/Language/REST/OCToAbstract.hs b/src/Language/REST/OCToAbstract.hs
--- a/src/Language/REST/OCToAbstract.hs
+++ b/src/Language/REST/OCToAbstract.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -32,7 +31,7 @@
   }
   where
     isSat' :: impl base -> m Bool
-    isSat' aoc = OC.isSatisfiable oc aoc
+    isSat' = OC.isSatisfiable oc
 
     top' :: impl base
     top' = OC.noConstraints oc
diff --git a/src/Language/REST/RESTDot.hs b/src/Language/REST/RESTDot.hs
--- a/src/Language/REST/RESTDot.hs
+++ b/src/Language/REST/RESTDot.hs
@@ -39,7 +39,7 @@
 rejectedNodes :: forall rule term a . (Hashable rule, Hashable term, Hashable a) =>
   GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Node
 rejectedNodes _ pp _ | showRejects pp == HideRejects = S.empty
-rejectedNodes gt pp p@(_steps, (PathTerm {rejected})) = S.fromList $ map go (HS.toList rejected)
+rejectedNodes gt pp p@(_steps, PathTerm {rejected}) = S.fromList $ map go (HS.toList rejected)
     where
         go :: (term, rule) -> Node
         go (rejTerm, _r) = Node (rejNodeID gt p rejTerm) (printTerm pp rejTerm) "dashed" "red"
@@ -62,7 +62,7 @@
 
 toEdges :: forall rule term a . (Hashable rule, Hashable term, Hashable a) =>
   GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Edge
-toEdges gt pp path = allRej `S.union` (S.fromList $ map toEdge (zip subs (tail subs)))
+toEdges gt pp path = allRej `S.union` S.fromList (zipWith (curry toEdge) subs (tail subs))
     where
         subs = subPaths path
 
@@ -86,7 +86,7 @@
         toEdge (p0, p1@(ts, _)) =
             let
                 step        = last ts
-                color       = if (fromPLE step) then "brown" else "darkgreen"
+                color       = if fromPLE step then "brown" else "darkgreen"
                 esubLabel    = printOrd pp (ordering step)
                 startNodeID = nodeID (endNode gt pp p0)
                 endNodeID   = nodeID (endNode gt pp p1)
diff --git a/src/Language/REST/RPO.hs b/src/Language/REST/RPO.hs
--- a/src/Language/REST/RPO.hs
+++ b/src/Language/REST/RPO.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ImplicitParams #-}
 
 -- | This module contains the implementation of the Recursive Path Quasi-Ordering,
@@ -47,7 +46,7 @@
 isSubtermOf :: RuntimeTerm -> RuntimeTerm -> Bool
 isSubtermOf t u@(App _ us) = t == u || any (t `isSubtermOf`) (MS.distinctElems us)
 
-type CacheKey oc = ((oc Op), Relation, RuntimeTerm, RuntimeTerm)
+type CacheKey oc = (oc Op, Relation, RuntimeTerm, RuntimeTerm)
 
 type Cache oc = M.HashMap (CacheKey oc) (oc Op)
 
@@ -95,7 +94,7 @@
 rpo' oc r cs t@(App f ts) u@(App g us) = incDepth result
   where
     cs'    = noConstraints oc
-    result = cached (cs, r, t, u) $ (intersect oc cs <$> result')
+    result = cached (cs, r, t, u) (intersect oc cs <$> result')
     result' = cached (cs', r, t, u) $
       if r == EQ
       then rpoMul oc r (addConstraint oc (f =. g) cs') ts us
@@ -122,7 +121,7 @@
   -> RT.RuntimeTerm
   -> RT.RuntimeTerm
   -> Identity (oc Op)
-rpoGTE' impl oc t u = rpo impl GTE oc t u
+rpoGTE' impl = rpo impl GTE
 
 
 -- Non symbolic version
diff --git a/src/Language/REST/Rest.hs b/src/Language/REST/Rest.hs
--- a/src/Language/REST/Rest.hs
+++ b/src/Language/REST/Rest.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE DeriveAnyClass #-}
+
+
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ImplicitParams #-}
+
 {-# LANGUAGE NamedFieldPuns #-}
 {-# OPTIONS_GHC -Wno-error=deprecations #-}
 
@@ -97,7 +97,7 @@
   , RESTResult rtype)
   => RESTParams m rule term oc rtype
   -> term
-  -> m ((rtype rule term oc), Maybe (Path rule term oc))
+  -> m (rtype rule term oc, Maybe (Path rule term oc))
 rest RESTParams{re,ru,ocImpl,workStrategy,initRes,target,etStrategy} t =
   rest' (RESTState initRes [([], PathTerm t S.empty)] initET Nothing)
   where
@@ -141,8 +141,8 @@
               t'  <- ListT $ S.toList <$> apply ptTerm r
               return (t', r)
 
-        accepted :: (S.HashSet (term, rule)) -> m (M.HashMap term oc)
-        accepted userRWs = M.fromList <$> (runListT $ do
+        accepted :: S.HashSet (term, rule) -> m (M.HashMap term oc)
+        accepted userRWs = M.fromList <$> runListT (do
           t' <- liftSet $ S.map fst userRWs
           guard $ L.notElem t' tsTerms
           let ord = refine ocImpl lastOrdering ptTerm t'
diff --git a/src/Language/REST/RuntimeTerm.hs b/src/Language/REST/RuntimeTerm.hs
--- a/src/Language/REST/RuntimeTerm.hs
+++ b/src/Language/REST/RuntimeTerm.hs
@@ -38,10 +38,10 @@
 -- term where @s@ is replaced with @s'@ in @t@. Also includes the pair (t, id),
 -- representing the term itself.
 -- TODO: Consider more efficient implementations
-subTerms :: RuntimeTerm -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]
+subTerms :: RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
 subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1]
   where
-    st :: Int -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]
+    st :: Int -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
     st i =
       let
         ti = ts !! i
diff --git a/src/Language/REST/SMT.hs b/src/Language/REST/SMT.hs
--- a/src/Language/REST/SMT.hs
+++ b/src/Language/REST/SMT.hs
@@ -6,10 +6,10 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
+
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
+
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | This module contains functionality for creating SMTLIB expressions and interacting
@@ -142,8 +142,8 @@
   go _ (And [])         = "⊤"
   go p (And ts)         = eparens p $ T.intercalate " ∧ " $ map (go (not p)) ts
   go p (Add ts)         = eparens p $ T.intercalate " + " $ map (go (not p)) ts
-  go p (GTE t u)        = eparens p $ T.intercalate " ≥ " $ map (go True) $ [t, u]
-  go p (Greater t u)    = eparens p $ T.intercalate " > " $ map (go True) $ [t, u]
+  go p (GTE t u)        = eparens p $ T.intercalate " ≥ " $ map (go True) [t, u]
+  go p (Greater t u)    = eparens p $ T.intercalate " > " $ map (go True) [t, u]
   go _ (Var (SMTVar v)) = v
   go _ (Const c)        = T.pack (show c)
   go _ _e               = undefined
@@ -186,10 +186,10 @@
 -- | `smtGTE t u` returns an SMT expression \( t \geqslant u \). If @t == u@, returns 'smtTrue'.
 smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
 smtGTE t u | t == u    = smtTrue
-smtGTE t u | otherwise = GTE t u
+smtGTE t u  = GTE t u
 
 app :: T.Text -> [SMTExpr a] -> T.Text
-app op trms = T.concat $ ["(", op, " ", (T.intercalate " " (map exprString trms)), ")"]
+app op trms = T.concat ["(", op, " ", T.intercalate " " (map exprString trms), ")"]
 
 exprString :: SMTExpr a -> T.Text
 exprString (And [])           = "true"
@@ -207,7 +207,7 @@
 
 commandString :: SMTCommand -> T.Text
 commandString (SMTAssert expr) = app "assert" [expr]
-commandString (DeclareVar var) = T.concat $ ["(declare-const ", var,  " Int)"]
+commandString (DeclareVar var) = T.concat ["(declare-const ", var,  " Int)"]
 commandString CheckSat = "(check-sat)"
 commandString Push     = "(push)"
 commandString Pop      = "(pop)"
@@ -234,7 +234,7 @@
 withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b
 withZ3 f =
   do
-    z3     <- liftIO $ spawnZ3
+    z3     <- liftIO spawnZ3
     result <- f z3
     liftIO $ killZ3 z3
     return result
@@ -263,7 +263,7 @@
   return sat
   where
     sendCommands cmds = do
-      hPutStr stdIn $ (T.unpack (T.intercalate "\n" (map commandString cmds))) ++ "\n"
+      hPutStr stdIn $ T.unpack (T.intercalate "\n" (map commandString cmds)) ++ "\n"
       hFlush stdIn
 
 -- | @checkSat expr@ launches Z3, to checks satisfiability of @expr@, terminating Z3
diff --git a/src/Language/REST/Types.hs b/src/Language/REST/Types.hs
--- a/src/Language/REST/Types.hs
+++ b/src/Language/REST/Types.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE GADTs #-}
@@ -50,7 +50,7 @@
 
   replace s | Just (from, to) <- L.find ((`T.isPrefixOf` s) . fst) substs
             = T.append to $ T.drop (T.length from) s
-  replace s | otherwise = s
+  replace s  = s
 
   replaceAll :: MT.MetaTerm -> MT.MetaTerm
   replaceAll (MT.Var x)            = MT.Var x
@@ -67,9 +67,9 @@
   go (MT.RWApp (Op op) xs)       = T.concat [op, "(" , T.intercalate ", " (map go xs) , ")"]
 
   goParens mt | needsParens mt = T.pack $ printf "(%s)" (go mt)
-  goParens mt | otherwise      = go mt
+  goParens mt       = go mt
 
-  needsParens (MT.RWApp (Op op) _) = op `elem` (map fst infixOps)
+  needsParens (MT.RWApp (Op op) _) = op `elem` map fst infixOps
   needsParens _                    = False
 
 data Relation = GT | GTE | EQ deriving (Eq, Generic, Hashable)
diff --git a/src/Language/REST/WQOConstraints/ADT.hs b/src/Language/REST/WQOConstraints/ADT.hs
--- a/src/Language/REST/WQOConstraints/ADT.hs
+++ b/src/Language/REST/WQOConstraints/ADT.hs
@@ -62,9 +62,7 @@
 #ifdef OPTIMIZE_WQO
 -- Optimization
 intersect (Sat t) (Sat u) =
-  case WQO.merge t u of
-    Just t' -> Sat t'
-    Nothing -> Unsat
+  maybe Unsat Sat (WQO.merge t u)
 #endif
 
 intersect (Sat w) v            | w == WQO.empty = v
@@ -76,19 +74,19 @@
 #ifdef OPTIMIZE_WQO
 intersect (Sat w1) (Intersect (Sat w2) t2) =
   case WQO.merge w1 w2 of
-    Just w' -> intersect (Sat w') t2
+    Just w' -> Sat w' `intersect` t2
     Nothing -> Unsat
 intersect (Sat w1) (Intersect t2 (Sat w2)) =
   case WQO.merge w1 w2 of
-    Just w' -> intersect (Sat w') t2
+    Just w' -> Sat w' `intersect` t2
     Nothing -> Unsat
 intersect (Intersect t1 (Sat w1)) (Sat w2) =
   case WQO.merge w1 w2 of
-    Just w' -> intersect t1 (Sat w')
+    Just w' -> t1 `intersect` Sat w'
     Nothing -> Unsat
 intersect (Intersect (Sat w1) t1) (Sat w2) =
   case WQO.merge w1 w2 of
-    Just w' -> intersect t1 (Sat w')
+    Just w' -> t1 `intersect` Sat w'
     Nothing -> Unsat
 #endif
 intersect t1 t2            = Intersect t1 t2
@@ -108,7 +106,7 @@
 -- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@
 addConstraint
  :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a
-addConstraint o c = intersect (Sat o) c
+addConstraint o = intersect (Sat o)
 
 notStrongerThan
   :: (Eq a, ToSMTVar a Int)
@@ -117,10 +115,10 @@
   -> SMTExpr Bool
 notStrongerThan t1 t2 | t1 == t2            = smtTrue
 notStrongerThan t1 _  | t1 == noConstraints = smtTrue
-notStrongerThan t1 t2 | otherwise           = Implies (toSMT t2) (toSMT t1)
+notStrongerThan t1 t2            = Implies (toSMT t2) (toSMT t1)
 
 noConstraints :: ConstraintsADT a
-noConstraints = Sat (WQO.empty)
+noConstraints = Sat WQO.empty
 
 unsatisfiable :: ConstraintsADT a
 unsatisfiable = Unsat
@@ -143,8 +141,8 @@
 cached key thunk = do
   cache <- gets cs
   case M.lookup key cache of
-    Just result -> trace'' ("ADT Cache hit") $ return result
-    Nothing     -> trace'' ("ADT Cache miss") $ do
+    Just result -> trace'' "ADT Cache hit" $ return result
+    Nothing     -> trace'' "ADT Cache miss" $ do
       result <- trace'' "Do thunk" thunk
       trace'' "Done" $ modify (\st -> st{cs = M.insert key result (cs st)})
       return result
@@ -156,7 +154,7 @@
 cached' (lhs, rhs) thunk = do
   cache <- gets ms
   case M.lookup (lhs, rhs) cache of
-    Just result -> trace'' ("WQO Cache hit") $ return result
+    Just result -> trace'' "WQO Cache hit" $ return result
     Nothing     -> trace'' ("WQO Cache miss" ++ show (lhs, rhs)) $ do
       trace'' "Done" $ modify (\st -> st{ms = M.insert (rhs, lhs) thunk $ M.insert (lhs, rhs) thunk (ms st)})
       return thunk
@@ -181,15 +179,15 @@
   c1' <- cached c1 $ getConstraints' c1
   if null c1'
     then return []
-    else (cached c2 $ getConstraints' c2) >>= go c1'
+    else cached c2 (getConstraints' c2) >>= go c1'
   where
       go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
       go c1' c2' = flatten <$>
-        (sequence $ do
+        sequence (do
           wqo1 <- c1'
           wqo2 <- c2'
           return (cached' (wqo1, wqo2) $ WQO.merge wqo1 wqo2))
-      flatten = concatMap Mb.maybeToList
+      flatten = Mb.catMaybes
       (c1, c2) =
         if cost lhs > cost rhs
         then (lhs, rhs)
@@ -203,7 +201,7 @@
 permits adt wqo = any (`WQO.notStrongerThan` wqo) (getConstraints adt)
 
 isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool
-isSatisfiable s = toSMT s
+isSatisfiable = toSMT
 
 instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where
   show (Sat w)         = show w
@@ -226,3 +224,4 @@
   union
   unsatisfiable
   undefined
+
diff --git a/src/Language/REST/WQOConstraints/Lazy.hs b/src/Language/REST/WQOConstraints/Lazy.hs
--- a/src/Language/REST/WQOConstraints/Lazy.hs
+++ b/src/Language/REST/WQOConstraints/Lazy.hs
@@ -54,9 +54,9 @@
     (Sat c1 t1', Sat c2 t2') ->
       let
         rest =
-          (ADT.intersect (ADT.Sat c1) t2') `ADT.union`
-          (ADT.intersect (ADT.Sat c2) t1') `ADT.union`
-          (ADT.intersect t1' t2')
+          ADT.intersect (ADT.Sat c1) t2' `ADT.union`
+          ADT.intersect (ADT.Sat c2) t1' `ADT.union`
+          ADT.intersect t1' t2'
       in
         case WQO.merge c1 c2 of
           Just c' -> Sat c' rest
@@ -74,7 +74,7 @@
 
 -- | Returns a new instance of 'LazyOC' permitting all WQOs
 noConstraints :: LazyOC a
-noConstraints = Sat (WQO.empty) ADT.Unsat
+noConstraints = Sat WQO.empty ADT.Unsat
 
 unsatisfiable :: LazyOC a
 unsatisfiable = Unsat
diff --git a/src/Language/REST/WQOConstraints/Strict.hs b/src/Language/REST/WQOConstraints/Strict.hs
--- a/src/Language/REST/WQOConstraints/Strict.hs
+++ b/src/Language/REST/WQOConstraints/Strict.hs
@@ -46,7 +46,7 @@
 --   2. Related, calculating the entire set @ws@ is computationally expensive,
 --      and often unnecessary for RESTs use-case, where continuing the path only
 --      requires knowing if /any/ WQO is permitted.
-data StrictOC a = StrictOC (S.Set (WQO a))
+newtype StrictOC a = StrictOC (S.Set (WQO a))
   deriving (Eq, Ord, Generic, Hashable)
 
 instance (Show a, Eq a, Ord a, Hashable a) => Show (StrictOC a) where
@@ -61,7 +61,7 @@
 -- | Constraints that permit any 'WQO'. In this case implemented by
 --   a singleton set containing an empty WQO.
 noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a
-noConstraints = StrictOC (S.singleton (WQO.empty))
+noConstraints = StrictOC (S.singleton WQO.empty)
 
 unsatisfiable :: StrictOC a
 unsatisfiable = StrictOC S.empty
diff --git a/test/BagExample.hs b/test/BagExample.hs
--- a/test/BagExample.hs
+++ b/test/BagExample.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE ImplicitParams #-}
+
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 
+
 module BagExample (mkBagGraph) where
 
 import Prelude hiding (EQ, GT)
@@ -31,7 +31,7 @@
 import GHC.Generics (Generic)
 import           Data.Hashable
 
-data PChar = PChar Char deriving (Eq, Ord, Generic, Hashable)
+newtype PChar = PChar Char deriving (Eq, Ord, Generic, Hashable)
 
 instance ToSMTVar PChar Int where
   toSMTVar c = SMTVar $ T.pack $ "char_" ++ show c
@@ -39,7 +39,7 @@
 instance Show PChar where
   show (PChar c) = return c
 
-data Bag = Bag String
+newtype Bag = Bag String
   deriving (Eq, Ord, Generic, Hashable)
 
 instance Show Bag where
@@ -62,12 +62,12 @@
 
 instance RewriteRule IO Rewrite Bag where
   apply bag1 (Rewrite bag' result) | bag1 == bag' = return result
-  apply _ _ | otherwise                           = return S.empty
+  apply _ _                            = return S.empty
 
 
 fromPath :: [String] -> S.HashSet Rewrite
 fromPath [] = S.empty
-fromPath xs = S.fromList $ map go (zip xs (tail xs))
+fromPath xs = S.fromList $ zipWith (curry go) xs (tail xs)
   where
     go :: (String, String) -> Rewrite
     go (x, y) = Rewrite (bag x) (S.singleton $ bag y)
@@ -80,13 +80,13 @@
 start = "AAB"
 
 rules :: S.HashSet Rewrite
-rules = fromPaths $
+rules = fromPaths
   [  start ~> "ACD" ~> "AAAA" ~> "ABDD" ~> []
   ,  start ~> "ABD" ~> "AB"  ~> "BBD" ~> []
   ]
 
 showBag :: Bag -> String
-showBag (Bag bag1) = "{ " ++ (L.intercalate ", " $ map return bag1) ++ " }"
+showBag (Bag bag1) = "{ " ++ L.intercalate ", " (map return bag1) ++ " }"
 
 showRule :: Rewrite -> String
 showRule _ = ""
diff --git a/test/Group.hs b/test/Group.hs
--- a/test/Group.hs
+++ b/test/Group.hs
@@ -21,6 +21,6 @@
       [
           x #+ zero'    ~> x
         , zero'    #+ x ~> x
-        , (neg x) #+ x  ~> zero'
+        , neg x #+ x  ~> zero'
         , (x #+ y) #+ v ~> x #+ (y #+ v)
       ]
diff --git a/test/Lists.hs b/test/Lists.hs
--- a/test/Lists.hs
+++ b/test/Lists.hs
@@ -35,6 +35,6 @@
 
 userRWs :: S.HashSet Rewrite
 userRWs = S.fromList [
-    reverse (xs .++ ys) ~> (reverse ys) .++ (reverse xs)
-  , (reverse ys) .++ (reverse xs) ~> reverse (xs .++ ys)
+    reverse (xs .++ ys) ~> reverse ys .++ reverse xs
+  , reverse ys .++ reverse xs ~> reverse (xs .++ ys)
   ]
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ImplicitParams #-}
+
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 
@@ -20,7 +20,7 @@
 import Language.REST.Internal.WorkStrategy
 import DSL
 import Nat
-import Set as Set
+import Set
 import qualified Multiset as MS
 import NonTerm as NT
 import qualified Lists as Li
@@ -77,7 +77,7 @@
       do
         mapM_ (explain (refine impl (top impl))) pairs
         printf "Result:\n%s\n" (show $ orient impl ts)
-        (isSatisfiable SC.strictOC (orient impl ts)) >>= print
+        isSatisfiable SC.strictOC (orient impl ts) >>= print
     where
       impl :: OCAlgebra (SC.StrictOC Op) RuntimeTerm Identity
       impl = lift SC.strictOC lpo
@@ -142,9 +142,9 @@
 mkRESTGraph' impl evalRWs0 userRWs0 name term0 params =
   do
     let pr (Rewrite t u _) = printf "%s → %s" (pp t) (pp u)
-    liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList userRWs0
-    liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList evalRWs0
-    start <- liftIO $ getCurrentTime
+    liftIO $ mapM_ (putStrLn . pr) $ S.toList userRWs0
+    liftIO $ mapM_ (putStrLn . pr) $ S.toList evalRWs0
+    start <- liftIO getCurrentTime
     (PathsResult paths, targetPath) <- rest
       RESTParams
         { re           = evalRWs0
@@ -155,7 +155,7 @@
         , initRes      = pathsResult
         , etStrategy   = if gUseETOpt params then ExploreWhenNeeded else ExploreAlways
         } (parseTerm term0)
-    end <- liftIO $ getCurrentTime
+    end <- liftIO getCurrentTime
     liftIO $ printf "REST run completed, in %s\n" $ show $ diffUTCTime end start
     liftIO $ putStrLn "Drawing graph"
     let showCons = if gShowConstraints params then show else const ""
@@ -189,5 +189,5 @@
 main :: IO ()
 main = do
   mkRESTGraph RPO S.empty (S.insert (s1 /\ s0 ~> emptyset) challengeRulesNoCommute) "fig4" "f(intersect(union(s₀,s₁), s₀))" (withNoETOpt defaultParams)
-  mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-noopt" "a + (b + a)" (withNoETOpt defaultParams)
-  mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-opt" "a + (b + a)" defaultParams
+  mkRESTGraph RPO S.empty (S.fromList $ (x #+ y ~> y #+ x) : ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-noopt" "a + (b + a)" (withNoETOpt defaultParams)
+  mkRESTGraph RPO S.empty (S.fromList $ (x #+ y ~> y #+ x) : ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-opt" "a + (b + a)" defaultParams
diff --git a/test/Multiset.hs b/test/Multiset.hs
--- a/test/Multiset.hs
+++ b/test/Multiset.hs
@@ -37,17 +37,17 @@
 expandM xs0 = multisetOf xs0 ~> ite (isEmpty xs0) empty (singleton (hd xs0) \/ multisetOf (tl xs0))
 
 userRWs :: S.HashSet Rewrite
-userRWs = S.fromList $
+userRWs = S.fromList
   [
     commutes (\/) `named` "mpComm"
   , assocL (\/) `named` "mpAssoc"
   , assocR (\/) `named` "mpAssoc"
-  , (singleton x) \/ (multisetOf y) ~> multisetOf (cons x y)
+  , singleton x \/ multisetOf y ~> multisetOf (cons x y)
   ]
 
 evalRWs :: S.HashSet Rewrite
 evalRWs = S.fromList
-  [ multisetOf (cons x y) ~> (singleton x) \/ (multisetOf y)
+  [ multisetOf (cons x y) ~> singleton x \/ multisetOf y
   , expandM xs
   , expandM ys
   ]
diff --git a/test/MultisetOrder.hs b/test/MultisetOrder.hs
--- a/test/MultisetOrder.hs
+++ b/test/MultisetOrder.hs
@@ -31,7 +31,7 @@
 tests :: [(String, Bool)]
 tests = [
     ("Constraints",
-     (SC.noConstraints /=
-     (runIdentity $ ms SC.noConstraints (M.fromList "bc") (M.fromList "aa"))))
+     SC.noConstraints /=
+     runIdentity (ms SC.noConstraints (M.fromList "bc") (M.fromList "aa")))
   , ("Unsat", SC.isUnsatisfiable $ runIdentity unsat)
   ]
diff --git a/test/NonTerm.hs b/test/NonTerm.hs
--- a/test/NonTerm.hs
+++ b/test/NonTerm.hs
@@ -16,7 +16,7 @@
 d' x1 = RWApp (Op "d") [x1]
 
 userRWs :: S.HashSet Rewrite
-userRWs = S.fromList $
+userRWs = S.fromList
   [
     a' (b' x) ~> a' (d' x)
   , d' (b' x) ~> b' (d' x)
diff --git a/test/OpOrdering.hs b/test/OpOrdering.hs
--- a/test/OpOrdering.hs
+++ b/test/OpOrdering.hs
@@ -22,11 +22,11 @@
   ) ]
         where
 
-        Just wqo = mergeAll [ ("cons" =. "z")
-                , ("g" =. "nil")
-                , ("h" =. "s")
-                , ("cons" >. "g")
-                , ("cons" >. "h")
-                , ("h" >. "f")
-                , ("h" >. "g")
+        Just wqo = mergeAll [ "cons" =. "z"
+                , "g" =. "nil"
+                , "h" =. "s"
+                , "cons" >. "g"
+                , "cons" >. "h"
+                , "h" >. "f"
+                , "h" >. "g"
                 ]
diff --git a/test/QuickCheckTests.hs b/test/QuickCheckTests.hs
--- a/test/QuickCheckTests.hs
+++ b/test/QuickCheckTests.hs
@@ -54,7 +54,7 @@
       let po' = fromMaybe po $ PO.insert po f g
       go po' (n - 1)
 
-gen_wqo_steps :: Gen ([(Op, Op, WQO.QORelation)])
+gen_wqo_steps :: Gen [(Op, Op, WQO.QORelation)]
 gen_wqo_steps =
   do
     numOps <- choose (0, 10)
@@ -83,7 +83,7 @@
   where
     go :: Int -> Gen RuntimeTerm
     go sz = do
-      (op, arity) <- oneof $ map return $ (filter ((<= sz) . snd) syms)
+      (op, arity) <- oneof $ map return $ filter ((<= sz) . snd) syms
       args        <- vectorOf arity (go (sz `div` (arity + 1)))
       return $ App (Op op) args
 
@@ -134,7 +134,7 @@
     ordering    = Mb.fromJust (OC.getOrdering impl constraints)
 
 prop_permits :: [(Op, Op, WQO.QORelation)] -> Bool
-prop_permits steps = SC.permits (SC.noConstraints) (toWQO steps)
+prop_permits steps = SC.permits SC.noConstraints (toWQO steps)
 
 -- Should fail
 -- If this prop was true, we'd only ever need to check each term once
diff --git a/test/RPO.hs b/test/RPO.hs
--- a/test/RPO.hs
+++ b/test/RPO.hs
@@ -47,7 +47,7 @@
   :: (?impl::WQOConstraints impl m, Show (impl Op), Eq (impl Op), Hashable (impl Op))
   => [RuntimeTerm]
   -> impl Op
-rpoSeq xs = go (OC.noConstraints ?impl) xs where
+rpoSeq = go (OC.noConstraints ?impl) where
   go c (t:u:_xss) = OC.intersect ?impl c (rpoGTE t u)
   go c _        = c
 
@@ -59,7 +59,7 @@
     g = Op "g"
     h = Op "h"
   in
-    [ ("RPO1",   return $ (rpoGTE "f(z)" "g(s(z))")
+    [ ("RPO1",   return $ rpoGTE "f(z)" "g(s(z))"
               == OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (f >. s)))
     , ("RPO2", isUnsatisfiable ?impl $
          OC.intersect ?impl
@@ -73,8 +73,8 @@
     , ("SynGTE", return $ synGTE OpOrdering.empty (App s [App s [App g [App (Op "+") [App h [App s [App z []]],App z []],App s [App s [App g [App z [],App z []]]]]]]) (App z []))
     , ("SynGTE2",
         return $ synGTE (Mb.fromJust $ mergeAll [
-          ("cons" >. g)
-        , (f >. s)
-        , (h >. g)
-        , (h >. "nil")]) "s(cons(h(h(z)), f(nil, nil, z)))"  "g(z, cons(g(nil, nil), s(s(z))))")
+          "cons" >. g
+        , f >. s
+        , h >. g
+        , h >. "nil"]) "s(cons(h(h(z)), f(nil, nil, z)))"  "g(z, cons(g(nil, nil), s(s(z))))")
     ]
diff --git a/test/StrictOC.hs b/test/StrictOC.hs
--- a/test/StrictOC.hs
+++ b/test/StrictOC.hs
@@ -13,11 +13,11 @@
     ("permits", permits noConstraints wqo)
   , ("permits2", permits noConstraints $ fromJust $ parseOO "+ = f = nil = s ∧ + > g ∧ + > h ∧ cons > + ∧ cons > g")
   ] where
-  Just wqo = mergeAll [ ("cons" =. "z")
-                      , ("g" =. "nil")
-                      , ("h" =. "s")
-                      , ("cons" >. "g")
-                      , ("cons" >. "h")
-                      , ("h" >. "f")
-                      , ("h" >. "g")
+  Just wqo = mergeAll [ "cons" =. "z"
+                      , "g" =. "nil"
+                      , "h" =. "s"
+                      , "cons" >. "g"
+                      , "cons" >. "h"
+                      , "h" >. "f"
+                      , "h" >. "g"
                       ]
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -8,22 +9,25 @@
 
 import qualified Data.List as L
 import Data.Hashable
+#if MIN_VERSION_mtl(2,3,0)
+import Control.Monad (guard)
+#endif
 import Control.Monad.Identity
 import qualified Arith as A
 
 import qualified Data.HashMap.Strict as M
-import qualified ExploredTerms as ExploredTerms
+import qualified ExploredTerms
 import OpOrdering
 import DSL
-import WQO as WQO
-import MultisetOrder as MultisetOrder
+import WQO
+import MultisetOrder
 import Nat
-import RPO as RPO
-import KBO as KBO
-import StrictOC as StrictOC
-import LazyOC as LazyOC
-import SMT as SMT
-import qualified QuickCheckTests as QuickCheckTests
+import RPO
+import KBO
+import StrictOC
+import LazyOC
+import SMT
+import qualified QuickCheckTests
 import System.IO
 
 import Language.REST.ExploredTerms
@@ -56,13 +60,13 @@
 canOrient terms = isSat ?impl (orient ?impl terms)
 
 diverges :: (Show oc) => OCAlgebra oc RuntimeTerm IO -> [RuntimeTerm] -> IO Bool
-diverges impl ts = not <$> (isSat impl $ orient impl ts)
+diverges impl ts = not <$> isSat impl (orient impl ts)
 
 rewrites :: (Show oc, Hashable oc, Eq oc)
   => OCAlgebra oc RuntimeTerm IO
   -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm)
 rewrites impl evalRWs userRWs t0 =
-  resultTerms <$> fst <$> rest
+  resultTerms . fst <$> rest
     RESTParams
       { re           = evalRWs
       , ru           = userRWs
@@ -104,9 +108,9 @@
 orderingTests :: (Hashable (oc Op), Show (oc Op), Ord (oc Op)) => (?impl :: WQOConstraints oc IO) => [(String, IO Bool)]
 orderingTests =
   [
-    ("simple1", return $ not $ (rpoGTE "f(t1)" "g(t2)") `permits'` (t1Op =. t2Op))
-  , ("simple2", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op =. t2Op)))
-  , ("simple3", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op >. t2Op)))
+    ("simple1", return $ not $ rpoGTE "f(t1)" "g(t2)" `permits'` (t1Op =. t2Op))
+  , ("simple2", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op =. t2Op)))
+  , ("simple3", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op >. t2Op)))
   , ("subterm", return $ rpoGTE "f(g)" "f" == noConstraints ?impl)
   , ("intersect", OC.isUnsatisfiable ?impl $ OC.intersect ?impl (OC.singleton ?impl (f  >. g)) (OC.singleton ?impl (g >. f)))
   ]
@@ -119,8 +123,8 @@
   -> RuntimeTerm -> RuntimeTerm -> IO Bool
 proveEQ impl evalRWs userRWs have want =
   do
-    rw1 <- (rewrites impl evalRWs userRWs have)
-    rw2 <- (rewrites impl evalRWs userRWs want)
+    rw1 <- rewrites impl evalRWs userRWs have
+    rw2 <- rewrites impl evalRWs userRWs want
     return $ not $ disjoint rw1 rw2
   where
     disjoint s1 s2 = S.null $ s1 `S.intersection` s2
@@ -137,15 +141,13 @@
 arithTests impl =
   [
     ("Contains", return $ contains (intToTerm 2) (intToTerm 1))
-  , ("Diverge", not <$> (diverges impl [ (intToTerm 2) .+ t1
-                               , (intToTerm 1) .+ t1
-                               ]
-                    ))
-  , ("Diverge3", not <$> (diverges impl [ (t1 .+ t2) .+ t3
+  , ("Diverge", not <$> diverges impl [ intToTerm 2 .+ t1
+                               , intToTerm 1 .+ t1
+                               ])
+  , ("Diverge3", not <$> diverges impl [ (t1 .+ t2) .+ t3
                                , t1 .+ (t2 .+ t3)
                                , (t2 .+ t3) .+ t1
-                               ]
-                    ))
+                               ])
   , ("Eval1", arithEQ (intToTerm 2 .+ intToTerm 3) 5)
   , ("Eval2", arithEQ (ack (intToTerm 3) (intToTerm 2)) 29)
   , ("Subst1", return $ subst (M.fromList [("X", intToTerm 1), ("Y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2))
@@ -184,7 +186,7 @@
     termTest2 = proveEQ impl evalRWs userRWs (App f1 [zero]) (App g1 [zero])
       where
         evalRWs = S.union termEvalRWs A.evalRWs
-        userRWs = S.insert (MT.RWApp f1 [x] ~> MT.RWApp g1 [(suc' (suc' x))]) A.userRWs
+        userRWs = S.insert (MT.RWApp f1 [x] ~> MT.RWApp g1 [suc' (suc' x)]) A.userRWs
         termEvalRWs = S.fromList
           [  MT.RWApp f1 [suc' x] ~> MT.RWApp g1 [suc' x]
           ,  MT.RWApp f1 [zero']  ~> zero'
@@ -201,7 +203,7 @@
 completeTests impl =
   [ ("CompleteDiverges", not <$> diverges impl [App start [], App mid [], App finish []])
   , ("Complete1"     , eq (App start []) (App finish []))
-  , ("EvalComplete2" , (== (App finish [])) <$> eval completeUserRWs (App start' [App s1 []]) )
+  , ("EvalComplete2" , (== App finish []) <$> eval completeUserRWs (App start' [App s1 []]) )
   , ("Complete2"     , eq (App start' [App s1 []]) (App finish []))
   ]
   where
diff --git a/test/WQO.hs b/test/WQO.hs
--- a/test/WQO.hs
+++ b/test/WQO.hs
@@ -1,6 +1,7 @@
 module WQO where
 
 import Language.REST.Internal.WQO as WQO
+import Data.Maybe (isNothing)
 
 basicInvalid :: Maybe (WQO Char)
 basicInvalid = do
@@ -14,5 +15,5 @@
     ValidExtension fgyz = insert fg ("y", "z", QGT)
   in
     [ ("NotStrongerThan", fg `notStrongerThan` fgyz)
-    , ("RejectInvalid", basicInvalid == Nothing)
+    , ("RejectInvalid", isNothing basicInvalid)
     ]
diff --git a/testlib/Arith.hs b/testlib/Arith.hs
--- a/testlib/Arith.hs
+++ b/testlib/Arith.hs
@@ -24,11 +24,11 @@
 evalRWs =
     S.fromList
       [
-        (suc' x) <# (suc' y) ~> x <# y
-      , (suc' x) #+ y ~> suc' (x #+ y)
+        suc' x <# suc' y ~> x <# y
+      , suc' x #+ y ~> suc' (x #+ y)
       , zero'    #+ x ~> x
 
-      , (suc' x) #* y ~> y #+ (x #* y)
+      , suc' x #* y ~> y #+ (x #* y)
       , zero'     #* y ~> zero'
 
       , ack' zero' x           ~> suc' x
@@ -46,7 +46,7 @@
       , x #* y        ~> y #* x
 
       , (x #+ y) #* v ~> (x #* v) #+ (y #* v)
-      , (neg x) #+ x ~> zero'
+      , neg x #+ x ~> zero'
       -- , (x #* v) #+ (y #* v) ~> (x #+ y) #* v
 
       --  , x ~> x #+ zero'
diff --git a/testlib/Language/REST/ConcreteOC.hs b/testlib/Language/REST/ConcreteOC.hs
--- a/testlib/Language/REST/ConcreteOC.hs
+++ b/testlib/Language/REST/ConcreteOC.hs
@@ -13,7 +13,7 @@
 import GHC.Generics (Generic)
 import qualified Data.Set as S
 
-data ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))
+newtype ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))
   deriving (Eq, Ord, Generic, Hashable)
 
 instance Show ConcreteOC where
diff --git a/testlib/Language/REST/ProofGen.hs b/testlib/Language/REST/ProofGen.hs
--- a/testlib/Language/REST/ProofGen.hs
+++ b/testlib/Language/REST/ProofGen.hs
@@ -28,23 +28,20 @@
 
 toLH _ (App op [])   = opToLH op
 toLH parens (App op args) =
-  withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args)
+  withParens parens $ printf "%s %s" (opToLH op) (unwords $ map (toLH True) args)
 
 toProof :: Path Rewrite RuntimeTerm a -> String
-toProof (steps, PathTerm result _) = "    " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED"
+toProof (steps, PathTerm result _) = "    " ++ L.intercalate "\n=== " (proofSteps ++ [toLH False result]) ++ "\n*** QED"
   where
     proofSteps :: [String]
-    proofSteps = map proofStep $ zip steps [0..]
+    proofSteps = zipWith (curry proofStep) steps [0..]
 
-    proofStep ((Step (PathTerm t _) _ _ True), _)     = toLH False t
-    proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma
+    proofStep (Step (PathTerm t _) _ _ True, _)                       = toLH False t
+    proofStep (Step (PathTerm t _) (Rewrite lhs rhs name) _ False, i) = toLH False t ++ " ? " ++ toLemma lemma
       where
         lemma = go (subTerms t)
 
-        lemmaName =
-          case name of
-            Just n  -> T.pack n
-            Nothing -> "lemma"
+        lemmaName = maybe "lemma" T.pack name
 
         toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s))
 
diff --git a/testlib/MultisetOrdering.hs b/testlib/MultisetOrdering.hs
--- a/testlib/MultisetOrdering.hs
+++ b/testlib/MultisetOrdering.hs
@@ -15,7 +15,7 @@
   | Replace a [a]
   deriving (Show)
 
-data MultisetGE a = MultisetGE [Replace a] deriving (Show)
+newtype MultisetGE a = MultisetGE [Replace a] deriving (Show)
 
 type GTE a = a -> a -> Bool
 
@@ -31,14 +31,14 @@
 
     go :: [Replace a] -> [a] -> [a] -> Maybe (MultisetGE a)
     go rs (t : ts) us | Just u <- L.find (equiv t) us
-      = go ((ReplaceOne t u):rs) ts (L.delete u us)
+      = go (ReplaceOne t u:rs) ts (L.delete u us)
 
-    go rs (t : ts) us | otherwise =
+    go rs (t : ts) us  =
         let
           (lts, us') = L.partition (t `gt`)  us
         in
-          go ((Replace t lts) : rs) ts us'
-    go rs ts [] = Just $ MultisetGE $ (map ((flip Replace) []) ts) ++ rs
+          go (Replace t lts : rs) ts us'
+    go rs ts [] = Just $ MultisetGE $ map (`Replace` []) ts ++ rs
     go _  [] _  = Nothing
 
 
@@ -78,13 +78,13 @@
       from edge == nodeID node || to edge == nodeID node
 
     edges :: S.HashSet Edge
-    edges = S.fromList $ topEdges ++ (map snd $ replEdges pairs)
+    edges = S.fromList $ topEdges ++ map snd (replEdges pairs)
 
     topEdges = map go (M.toList (fst $ head indexed)) where
       go (_, index) =
         mkEdge "⊤" (nodeName (index,  0))
 
-    botNodes = S.fromList $ concatMap Mb.maybeToList $ map fst $ replEdges pairs
+    botNodes = S.fromList $ Mb.mapMaybe fst (replEdges pairs)
 
     nodeName :: (Int,  Int) -> String
     nodeName (elemIndex,  msIndex) =
@@ -92,7 +92,7 @@
 
     replEdges = toEdges Mp.empty
 
-    toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> ([(Maybe Node, Edge)])
+    toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> [(Maybe Node, Edge)]
     toEdges _ [] = []
     toEdges mp (((ts, tsIndex), (us, usIndex)) : mss) =
         concatMap redges repls ++ toEdges mp' mss
@@ -100,9 +100,7 @@
         Just (MultisetGE repls) = multisetGE (\t u -> gte (fst t) (fst u)) ts us
 
         lookupTIndex :: Int -> (Int, Int)
-        lookupTIndex tindex = case Mp.lookup (tindex, tsIndex) mp of
-          Just t  -> t
-          Nothing -> (tindex, tsIndex)
+        lookupTIndex tindex = Mb.fromMaybe (tindex, tsIndex) (Mp.lookup (tindex, tsIndex) mp)
 
         mp' = go mp repls where
           go mpi [] = mpi
diff --git a/testlib/Nat.hs b/testlib/Nat.hs
--- a/testlib/Nat.hs
+++ b/testlib/Nat.hs
@@ -46,7 +46,7 @@
                   ] showInt)
   where
     showInt :: MT.MetaTerm -> Maybe Text
-    showInt t = fmap (pack . show) $ termToInt t
+    showInt t = pack . show <$> termToInt t
 
 op :: GenParser Char st Op
 op = fmap (Op . pack) (many (alphaNum <|> char '\''))
diff --git a/testlib/Set.hs b/testlib/Set.hs
--- a/testlib/Set.hs
+++ b/testlib/Set.hs
@@ -24,7 +24,7 @@
 isSubset mt1 mt2 = mt1 \/ mt2 ~> mt2
 
 userRWs :: S.HashSet Rewrite
-userRWs = S.union A.evalRWs $ S.fromList $
+userRWs = S.union A.evalRWs $ S.fromList
   [
     distribL (/\) (\/)
   , distribR (/\) (\/)