diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Change Log
 
+## 0.1.6
+
+* GHC 8.4 compatibility
+
 ## 0.1.5
 
 * Bump dependencies, fix equality, tweak readme
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.1.5
+version:             0.1.6
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
@@ -71,15 +71,16 @@
                        TypeSynonymInstances,
                        UndecidableInstances
   build-depends:       attoparsec >=0.13 && <0.14,
-                       base >=4.9 && <4.12,
+                       base >=4.11 && <4.13,
                        containers >=0.5.7 && <0.6,
+                       free >=4.2 && <5.1,
                        lattices >=1.6 && <1.8,
                        singletons >=2.2 && <2.5,
                        text >=1.2 && <1.3,
                        transformers >=0.5.2 && <0.6
   hs-source-dirs:      src
   default-language:    Haskell2010
-  ghc-options:         -Wall
+  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
 
 test-suite test
   type:                exitcode-stdio-1.0
@@ -90,4 +91,4 @@
   hs-source-dirs:      test
   main-is:             Main.hs
   default-language:    Haskell2010
-  ghc-options:         -Wall
+  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs
--- a/src/Data/Expression.hs
+++ b/src/Data/Expression.hs
@@ -121,14 +121,17 @@
 
 import Algebra.Lattice
 import Control.Applicative hiding (Const)
+import Control.Comonad.Trans.Coiter
 import Control.Monad
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State
+import Data.Functor.Identity
 import Data.List hiding (and, or, union)
-import Data.Map hiding (map, drop, foldr, mapMaybe, partition)
+import Data.Map hiding (map, drop, foldl, foldr, mapMaybe, partition)
 import Data.Maybe
-import Data.Monoid
+import Data.Monoid hiding ((<>))
+import Data.Semigroup hiding (First, getFirst)
 import Data.Singletons
 import Data.Singletons.Decide
 import Prelude hiding (and, or, not)
@@ -308,9 +311,12 @@
     Just b -> b
     Nothing -> IFix . imap (flip substitute s) . unIFix $ a
 
+instance Semigroup (Substitution f) where
+    (Substitution f) <> (Substitution g) = Substitution $ \a -> getFirst (mconcat ([First . f, First . g] <*> [a]))
+
 instance Monoid (Substitution f) where
     mempty  = Substitution (const Nothing)
-    (Substitution f) `mappend` (Substitution g) = Substitution $ \a -> getFirst (mconcat ([First . f, First . g] <*> [a]))
+    mappend = (<>)
 
 -- | A functor representing a logical connective for conjunction
 data ConjunctionF a (s :: Sort) where
@@ -691,24 +697,28 @@
 
     pool = [ [x] | x <- ['a'..'z'] ] ++ [ x ++ [y] | x <- pool, y <- ['a'..'z'] ]
 
-freenames :: forall f (s :: Sort). ( VarF :<: f, IFunctor f, IFoldable f ) => IFix f s -> [String]
-freenames a = map (\n -> freename a ++ show n) ([0..] :: [Int])
+type VariableNamePool = Coiter String
 
-pushQuantifier' :: ( VarF :<: f, IEq1 f ) => ([Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort) -> [Var v] -> IFix f 'BooleanSort -> State ([String], IFix f 'BooleanSort -> IFix f 'BooleanSort) (IFix f 'BooleanSort)
+rename :: VariableNamePool -> [Var v] -> ([Var v], VariableNamePool)
+rename pool = foldl (\(vs, ns) (IFix (Var _ s)) -> let (n', ns') = runCoiter ns in (IFix (Var n' s) : vs, ns')) ([], pool)
+
+freenames :: forall f (s :: Sort). ( VarF :<: f, IFunctor f, IFoldable f ) => IFix f s -> VariableNamePool
+freenames a = fmap (\n -> freename a ++ show n) $ unfold (succ . runIdentity) (Identity (0 :: Int))
+
+pushQuantifier' :: ( VarF :<: f, IEq1 f ) => ([Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort) -> [Var v] -> IFix f 'BooleanSort -> State (VariableNamePool, IFix f 'BooleanSort -> IFix f 'BooleanSort) (IFix f 'BooleanSort)
 pushQuantifier' c vs a = do
     (ns, q) <- get
 
-    let vs' = zipWith (\(IFix (Var _ s)) n' -> IFix (Var n' s)) vs ns
-        ns' = drop (length vs) ns
-        q'  = c vs' . q
-        sub = mconcat $ zipWith (\(IFix (Var n s)) n' -> inject (Var n' s) `for` inject (Var n s)) vs ns
+    let (vs', ns') = rename ns vs
+        q'         = c vs' . q
+        sub        = mconcat $ zipWith (\(IFix (Var n s)) (IFix (Var n' _)) -> inject (Var n' s) `for` inject (Var n s)) vs vs'
 
     put (ns', q')
 
     return $ a `substitute` sub
 
 class MaybeQuantified f => MaybeQuantified' f g where
-    pushQuantifier :: f (IFix g) s -> State ([String], IFix g 'BooleanSort -> IFix g 'BooleanSort) (IFix g s)
+    pushQuantifier :: f (IFix g) s -> State (VariableNamePool, IFix g 'BooleanSort -> IFix g 'BooleanSort) (IFix g s)
 
 instance ( VarF :<: g, UniversalF v :<: g, IEq1 g ) => MaybeQuantified' (UniversalF v) g where
     pushQuantifier (Forall vs a) = pushQuantifier' forall vs a
@@ -731,29 +741,33 @@
 prenex f = let (a, (_, q)) = runState (imapM (pushQuantifier . unIFix) (nnf f)) (freenames f, id) in q a
 
 class Bind f g where
-    bind :: Proxy f -> IFix g s -> Maybe (Bool, State ([String], [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
+    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
 
 instance forall g v. ( VarF :<: g, EqualityF :<: g, NegationF :<: g, DisjunctionF :<: g, UniversalF v :<: g, MaybeQuantified g, SingI v ) => Bind (UniversalF v) g where
     bind _ a = case index (unIFix a) %~ (sing :: Sing v) of
         Proved Refl -> Just . (\s -> (False, s)) $ do
-            (n : ns, q) <- get
+            (ns, q) <- get
 
             let x :: forall f. VarF :<: f => IFix f v
                 x = var n
 
-            put (ns, (freevars a, forall [x] . (x .=. a .->.)) : q)
+                (n, ns') = runCoiter ns
+
+            put (ns', (freevars a, forall [x] . (x .=. a .->.)) : q)
             return x
         Disproved _ -> Nothing
 
 instance forall g v. ( VarF :<: g, EqualityF :<: g, ConjunctionF :<: g, ExistentialF v :<: g, MaybeQuantified g, SingI v ) => Bind (ExistentialF v) g where
     bind _ a = case index (unIFix a) %~ (sing :: Sing v) of
         Proved Refl -> Just . (\s -> (True, s)) $ do
-            (n : ns, q) <- get
+            (ns, q) <- get
 
             let x :: forall f. VarF :<: f => IFix f v
                 x = var n
 
-            put (ns, (freevars a, exists [x] . (x .=. a .&.)) : q)
+                (n, ns') = runCoiter ns
+
+            put (ns', (freevars a, exists [x] . (x .=. a .&.)) : q)
             return x
         Disproved _ -> Nothing
 
@@ -773,7 +787,7 @@
     bind _ _ = Nothing
 
 class Bind' f g where
-    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State ([String], [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
+    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
 
 instance VarF :<: g => Bind' VarF g where
     bind' v = Just (True, return . inject $ v)
@@ -797,11 +811,11 @@
 instance {-# OVERLAPPABLE #-} f :<: g => Bind' f g where
     bind' a = bind (Proxy :: Proxy g) (inject a)
 
-bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State ([String], [([DynamicallySorted VarF], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s)
+bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s)
 bind'' a = fromMaybe (return a) . fmap snd . bind' . unIFix $ a
 
 class MaybeQuantified'' f g where
-    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State ([String], [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)
+    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)
 
 instance ArrayF :<: g => MaybeQuantified'' ArrayF g where
     flatten' (Select is es a i) = do
@@ -870,18 +884,20 @@
     quantify _ _ = Nothing
 
 class Axiomatized f g where
-    instantiate :: Forall g g => IFix g s -> f (IFix g) s -> Maybe (State [String] (IFix g 'BooleanSort))
+    instantiate :: Forall g g => IFix g s -> f (IFix g) s -> Maybe (State VariableNamePool (IFix g 'BooleanSort))
 
 instance ( VarF :<: g, ConjunctionF :<: g, DisjunctionF :<: g, NegationF :<: g, EqualityF :<: g, ArrayF :<: g ) => Axiomatized ArrayF g where
     instantiate a' (Store (is :: Sing is) es a i e) = case quantify (Proxy :: Proxy g) is of
         Just q -> Just $ do
-            (n : ns) <- get
+            ns <- get
 
             let j :: forall f. VarF :<: f => IFix f is
                 j = inject $ Var n is
 
-            put ns
+                (n, ns') = runCoiter ns
 
+            put ns'
+
             return $ inject (Equals es (inject (Select is es a' i)) e) .&. q [j] (not (inject (Equals is i j)) .->. inject (Equals es (inject (Select is es a' j)) (inject (Select is es a j))))
         Nothing -> Nothing
     instantiate _ _ = Nothing
@@ -899,5 +915,5 @@
 -- | Replaces `store` with an instance of its axiomatization.
 unstore :: forall f. Unstore f => IFix f 'BooleanSort -> IFix f 'BooleanSort
 unstore a = let a' = flatten a in evalState (imapM unstore' a') (freenames a') where
-    unstore' :: IFix f s -> State [String] (IFix f s)
+    unstore' :: IFix f s -> State VariableNamePool (IFix f s)
     unstore' a' = fromMaybe (return a') (match a' >>= \(Equals _ l r) -> instantiate l (unIFix r) <|> instantiate r (unIFix l))
diff --git a/src/Data/Expression/Array.hs b/src/Data/Expression/Array.hs
--- a/src/Data/Expression/Array.hs
+++ b/src/Data/Expression/Array.hs
@@ -22,7 +22,6 @@
                              , store ) where
 
 import Data.Functor.Const
-import Data.Monoid
 import Data.Singletons
 import Data.Singletons.Decide
 
diff --git a/src/Data/Expression/Equality.hs b/src/Data/Expression/Equality.hs
--- a/src/Data/Expression/Equality.hs
+++ b/src/Data/Expression/Equality.hs
@@ -21,7 +21,6 @@
                                 , (.=.) ) where
 
 import Data.Functor.Const
-import Data.Monoid
 import Data.Singletons
 import Data.Singletons.Decide
 
diff --git a/src/Data/Expression/IfThenElse.hs b/src/Data/Expression/IfThenElse.hs
--- a/src/Data/Expression/IfThenElse.hs
+++ b/src/Data/Expression/IfThenElse.hs
@@ -21,7 +21,6 @@
                                   , ite ) where
 
 import Data.Functor.Const
-import Data.Monoid
 import Data.Singletons
 import Data.Singletons.Decide
 
diff --git a/src/Data/Expression/Sort.hs b/src/Data/Expression/Sort.hs
--- a/src/Data/Expression/Sort.hs
+++ b/src/Data/Expression/Sort.hs
@@ -1,7 +1,8 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
 
-{-# LANGUAGE GADTs
+{-# LANGUAGE EmptyCase
            , DataKinds
+           , GADTs
            , KindSignatures
            , OverloadedStrings
            , RankNTypes
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -32,16 +32,26 @@
 main :: IO ()
 main = guard (P.and props) where
 
-    props = [ e1 == (parseJust "(a : int)"                                                                   :: ALia 'IntegralSort)
-            , e2 /= (parseJust "(+ (a : int) 3)"                                                             :: ALia 'IntegralSort)
-            , e3 == (parseJust "(+ (a : int) 1)"                                                             :: ALia 'IntegralSort)
-            , e4 == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"                   :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))
-            , e5 == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)
-            , e6 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"          :: Lia 'BooleanSort) ]
+    props = [ e1 == parseJust "(a : int)"
+            , e2 /= parseJust "(+ (a : int) 3)"
+            , e3 == parseJust "(+ (a : int) 1)"
+            , e4 == parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"
+            , e5 == parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))"
+            , e6 == parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"
+            , e7 == e8 ]
 
+    e1, e2, e3 :: ALia 'IntegralSort
     e1 = a
     e2 = a
     e3 = a .+. c1
+
+    e4 :: QFALia ('ArraySort 'IntegralSort 'BooleanSort)
     e4 = select a (b .+. c3)
+
+    e5, e6 :: Lia 'BooleanSort
     e5 = forall [x :: Var 'IntegralSort] (exists [y :: Var 'IntegralSort] (and [true, b .=. (x .<. y)]))
     e6 = forall [x :: Var 'IntegralSort, y] (x .<. y .+. z) .&. z .=. c3
+
+    e7, e8 :: Lia 'IntegralSort
+    e7 = a .*. (a .+. c3) `substitute` (c3 `for` (a .+. c3))
+    e8 = inject (Mul [a, c3])