diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Change Log
 
+## 0.3
+
+* Cleanup, GHC 8.6
+
 ## 0.2
 
 * Add `embed` and `restrict` to convert between expression languages
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.2
+version:             0.3
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
@@ -75,7 +75,7 @@
                        containers >=0.5.7 && <0.7,
                        free >=4.2 && <5.2,
                        lattices >=1.6 && <1.8,
-                       singletons >=2.2 && <2.5,
+                       singletons >=2.2 && <2.6,
                        text >=1.2 && <1.3,
                        transformers >=0.5.2 && <0.6
   hs-source-dirs:      src
diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs
--- a/src/Data/Expression.hs
+++ b/src/Data/Expression.hs
@@ -2,6 +2,7 @@
            , FlexibleContexts
            , FlexibleInstances
            , GADTs
+           , InstanceSigs
            , MultiParamTypeClasses
            , OverloadedStrings
            , RankNTypes
@@ -78,6 +79,7 @@
 
                        -- Smart expression constructors
                        , var
+                       , dynvar
                        , true
                        , false
                        , and
@@ -101,6 +103,9 @@
                        , vars
                        , freevars
 
+                       -- Utilities
+                       , freenames
+
                        -- Predicates
                        , MaybeQuantified
                        , isQuantified
@@ -126,6 +131,7 @@
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State
+import Data.Coerce
 import Data.Functor.Identity
 import Data.List hiding (and, or, union)
 import Data.Map hiding (map, drop, foldl, foldr, mapMaybe, partition)
@@ -278,7 +284,7 @@
             var''' n s
 
         var''' :: VariableName -> DynamicSort -> Parser (DynamicallySorted f)
-        var''' n (DynamicSort (s :: Sing s)) = return $ DynamicallySorted s (inject (Var n s))
+        var''' n (DynamicSort (s :: Sing s)) = return $ dynvar n s
 
 -- | A smart constructor for variables of any sort in any language
 -- Takes the variable name and infers the target language and sort from context.
@@ -289,11 +295,15 @@
 var :: forall f s. ( VarF :<: f, SingI s ) => VariableName -> IFix f s
 var n = inject (Var n (sing :: Sing s))
 
+-- | Like @var@ except it hides the sort inside @DynamicallySorted@
+dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySorted f
+dynvar n s = DynamicallySorted s $ withSort s $ var n
+
 -- | Collects a list of all variables occurring in an expression (bound or free).
 vars :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted VarF]
 vars = nub . F.getConst . icata vars' where
     vars' a = case prj a of
-        Just (Var n s) -> F.Const [DynamicallySorted s . inject $ Var n s]
+        Just (Var n s) -> F.Const [dynvar n s]
         Nothing -> ifold a
 
 -- | Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.
@@ -352,10 +362,12 @@
     index Not {} = SBooleanSort
 
 instance IFoldable ConjunctionF where
-    ifold (And as) = F.Const . mconcat . map F.getConst $ as
+    ifold :: forall m (s :: Sort). Monoid m => ConjunctionF (F.Const m) s -> F.Const m s
+    ifold (And as) = coerce (mconcat :: [m] -> m) as
 
 instance IFoldable DisjunctionF where
-    ifold (Or os) = F.Const . mconcat . map F.getConst $ os
+    ifold :: forall m (s :: Sort). Monoid m => DisjunctionF (F.Const m) s -> F.Const m s
+    ifold (Or os) = coerce (mconcat :: [m] -> m) os
 
 instance IFoldable NegationF where
     ifold (Not n) = n
@@ -370,15 +382,15 @@
     itraverse f (Not n) = Not <$> f n
 
 instance IShow ConjunctionF where
-    ishow (And []) = F.Const $ "true"
-    ishow (And as) = F.Const $ "(and " ++ intercalate " " (map F.getConst as) ++ ")"
+    ishow (And []) = coerce ("true" :: String)
+    ishow (And as) = coerce $ "(and " ++ intercalate " " (coerce as) ++ ")"
 
 instance IShow DisjunctionF where
-    ishow (Or []) = F.Const $ "false"
-    ishow (Or os) = F.Const $ "(or "  ++ intercalate " " (map F.getConst os) ++ ")"
+    ishow (Or []) = coerce ("false" :: String)
+    ishow (Or os) = coerce $ "(or "  ++ intercalate " " (coerce os) ++ ")"
 
 instance IShow NegationF where
-    ishow (Not n)  = F.Const $ "(not " ++ F.getConst n ++ ")"
+    ishow (Not n)  = coerce $ "(not " ++ coerce n ++ ")"
 
 instance ConjunctionF :<: f => Parseable ConjunctionF f where
     parser _ r = choice [ true',  and' ] <?> "Conjunction" where
@@ -545,10 +557,10 @@
     itraverse f (Exists vs b) = Exists vs <$> f b
 
 instance IShow (UniversalF v) where
-    ishow (Forall vs phi) = F.Const $ "(forall (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"
+    ishow (Forall vs phi) = coerce $ "(forall (" ++ intercalate " " (map show vs) ++ ") " ++ coerce phi ++ ")"
 
 instance IShow (ExistentialF v) where
-    ishow (Exists vs phi) = F.Const $ "(exists (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"
+    ishow (Exists vs phi) = coerce $ "(exists (" ++ intercalate " " (map show vs) ++ ") " ++ coerce phi ++ ")"
 
 instance ( UniversalF v :<: f, SingI v ) => Parseable (UniversalF v) f where
     parser _ r = forall' <?> "Universal" where
@@ -603,16 +615,16 @@
     freevars' :: f (F.Const [DynamicallySorted VarF]) s -> F.Const [DynamicallySorted VarF] s
 
 instance MaybeQuantified VarF where
-    isQuantified' _ = F.Const (Any False)
-    freevars' (Var n s) = F.Const [DynamicallySorted s . inject $ Var n s]
+    isQuantified' _ = coerce False
+    freevars' (Var n s) = coerce [dynvar n s]
 
 instance MaybeQuantified (UniversalF v) where
-    isQuantified' _ = F.Const (Any True)
-    freevars' (Forall vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a
+    isQuantified' _ = coerce True
+    freevars' (Forall vs a) = coerce (P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs)) a
 
 instance MaybeQuantified (ExistentialF v) where
-    isQuantified' _ = F.Const (Any True)
-    freevars' (Exists vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a
+    isQuantified' _ = coerce True
+    freevars' (Exists vs a) = coerce (P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs)) a
 
 instance ( MaybeQuantified f, MaybeQuantified g ) => MaybeQuantified (f :+: g) where
     isQuantified' (InL fa) = isQuantified' fa
@@ -626,7 +638,7 @@
 
 -- | Test whether an expression contains a quantifier.
 isQuantified :: MaybeQuantified f => IFix f s -> Bool
-isQuantified = getAny . F.getConst . isQuantified' . unIFix
+isQuantified = coerce . isQuantified' . unIFix
 
 -- | Tests whether an expression is free of any quantifier.
 isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool
@@ -634,7 +646,7 @@
 
 -- | Collects a list of all free variables occurring in an expression.
 freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted VarF]
-freevars = nub . F.getConst . icata freevars'
+freevars = nub . coerce . icata freevars'
 
 -- | A smart constructor for universally quantified formulae
 forall :: UniversalF v :<: f => [Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort
diff --git a/src/Data/Expression/Arithmetic.hs b/src/Data/Expression/Arithmetic.hs
--- a/src/Data/Expression/Arithmetic.hs
+++ b/src/Data/Expression/Arithmetic.hs
@@ -29,6 +29,7 @@
                                   , (.<=.)
                                   , (.>=.) ) where
 
+import Data.Coerce
 import Data.List
 import Data.Maybe
 import Data.Monoid
@@ -77,11 +78,11 @@
     index LessThan {} = SBooleanSort
 
 instance IFoldable ArithmeticF where
-    ifold (Const _) = F.Const $ mempty
-    ifold (Add as)  = F.Const . mconcat . map F.getConst $ as
-    ifold (Mul ms)  = F.Const . mconcat . map F.getConst $ ms
-    ifold (_ `Divides` a)  = F.Const . F.getConst $ a
-    ifold (a `LessThan` b) = F.Const (F.getConst a) <> F.Const (F.getConst b)
+    ifold (Const _) = mempty
+    ifold (Add as)  = mconcat as
+    ifold (Mul ms)  = mconcat ms
+    ifold (_ `Divides` a)  = coerce a
+    ifold (a `LessThan` b) = coerce a <> coerce b
 
 instance ITraversable ArithmeticF where
     itraverse _ (Const c) = pure (Const c)
@@ -91,11 +92,11 @@
     itraverse f (a `LessThan` b) = LessThan <$> f a <*> f b
 
 instance IShow ArithmeticF where
-    ishow (Const c)        = F.Const $ show c
-    ishow (Add as)         = F.Const $ "(+ " ++ intercalate " " (map F.getConst as) ++ ")"
-    ishow (Mul ms)         = F.Const $ "(* " ++ intercalate " " (map F.getConst ms) ++ ")"
-    ishow (c `Divides`  a) = F.Const $ "(" ++ show c ++ "| " ++ F.getConst a ++ ")"
-    ishow (a `LessThan` b) = F.Const $ "(< " ++ F.getConst a ++ " " ++ F.getConst b ++ ")"
+    ishow (Const c)        = coerce $ show c
+    ishow (Add as)         = coerce $ "(+ " ++ intercalate " " (coerce as) ++ ")"
+    ishow (Mul ms)         = coerce $ "(* " ++ intercalate " " (coerce ms) ++ ")"
+    ishow (c `Divides`  a) = coerce $ "(" ++ show c ++ "| " ++ coerce a ++ ")"
+    ishow (a `LessThan` b) = coerce $ "(< " ++ coerce a ++ " " ++ coerce b ++ ")"
 
 instance ArithmeticF :<: f => Parseable ArithmeticF f where
     parser _ r = choice [ cnst', add', mul', divides', lessThan' ] <?> "Arithmetic" where
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
@@ -21,6 +21,7 @@
                              , select
                              , store ) where
 
+import Data.Coerce
 import Data.Functor.Const
 import Data.Singletons
 import Data.Singletons.Decide
@@ -54,16 +55,16 @@
     index (Store  is es _ _ _) = SArraySort is es
 
 instance IFoldable ArrayF where
-    ifold (Select _ _ a i)   = Const (getConst a) <> Const (getConst i)
-    ifold (Store  _ _ a i e) = Const (getConst a) <> Const (getConst i) <> Const (getConst e)
+    ifold (Select _ _ a i)   = coerce a <> coerce i
+    ifold (Store  _ _ a i e) = coerce a <> coerce i <> coerce e
 
 instance ITraversable ArrayF where
     itraverse f (Select is es a i)   = Select is es <$> f a <*> f i
     itraverse f (Store  is es a i e) = Store  is es <$> f a <*> f i <*> f e
 
 instance IShow ArrayF where
-    ishow (Select _ _ a i)   = Const $ "(select " ++ getConst a ++ " " ++ getConst i ++ ")"
-    ishow (Store  _ _ a i v) = Const $ "(store " ++ getConst a ++ " " ++ getConst i ++ " " ++ getConst v ++ ")"
+    ishow (Select _ _ a i)   = coerce $ "(select " ++ coerce a ++ " " ++ coerce i ++ ")"
+    ishow (Store  _ _ a i v) = coerce $ "(store " ++ coerce a ++ " " ++ coerce i ++ " " ++ coerce v ++ ")"
 
 instance ArrayF :<: f => Parseable ArrayF f where
     parser _ r = choice [ select', store' ] <?> "Array" where
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
@@ -20,6 +20,7 @@
 module Data.Expression.Equality ( EqualityF(..)
                                 , (.=.) ) where
 
+import Data.Coerce
 import Data.Functor.Const
 import Data.Singletons
 import Data.Singletons.Decide
@@ -47,13 +48,13 @@
     index (Equals _ _ _) = SBooleanSort
 
 instance IFoldable EqualityF where
-    ifold (Equals _ a b) = Const (getConst a) <> Const (getConst b)
+    ifold (Equals _ a b) = coerce a <> coerce b
 
 instance ITraversable EqualityF where
     itraverse f (Equals s a b) = Equals s <$> f a <*> f b
 
 instance IShow EqualityF where
-    ishow (Equals _ a b) = Const $ "(= " ++ getConst a ++ " " ++ getConst b ++ ")"
+    ishow (Equals _ a b) = coerce $ "(= " ++ coerce a ++ " " ++ coerce b ++ ")"
 
 instance EqualityF :<: f => Parseable EqualityF f where
     parser _ r = do
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
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleContexts
            , FlexibleInstances
            , GADTs
+           , InstanceSigs
            , MultiParamTypeClasses
            , OverloadedStrings
            , RankNTypes
@@ -20,6 +21,7 @@
 module Data.Expression.IfThenElse ( IfThenElseF(..)
                                   , ite ) where
 
+import Data.Coerce
 import Data.Functor.Const
 import Data.Singletons
 import Data.Singletons.Decide
@@ -47,13 +49,14 @@
     index (IfThenElse s _ _ _) = s
 
 instance IFoldable IfThenElseF where
-    ifold (IfThenElse _ i t e) = Const $ getConst i <> getConst t <> getConst e
+    ifold :: forall m (s :: Sort). Monoid m => IfThenElseF (Const m) s -> Const m s
+    ifold (IfThenElse _ i t e) = coerce ((coerce i <> coerce t <> coerce e) :: m)
 
 instance ITraversable IfThenElseF where
     itraverse f (IfThenElse s i t e) = IfThenElse s <$> f i <*> f t <*> f e
 
 instance IShow IfThenElseF where
-    ishow (IfThenElse _ i t e) = Const $ "(ite " ++ getConst i ++ " " ++ getConst t ++ " " ++ getConst e ++ ")"
+    ishow (IfThenElse _ i t e) = coerce $ "(ite " ++ coerce i ++ " " ++ coerce t ++ " " ++ coerce e ++ ")"
 
 instance IfThenElseF :<: f => Parseable IfThenElseF f where
     parser _ r = do
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 EmptyCase
-           , DataKinds
+{-# LANGUAGE DataKinds
+           , EmptyCase
+           , FlexibleInstances
            , GADTs
            , KindSignatures
            , OverloadedStrings
@@ -25,6 +26,7 @@
 
 module Data.Expression.Sort ( Sort(..)
                             , Sing(..)
+                            , withSort
                             , DynamicSort(..)
                             , DynamicallySorted(..)
                             , parseSort
@@ -34,7 +36,6 @@
 
 import Data.Attoparsec.Text
 import Data.Functor
-import Data.Kind
 import Data.Singletons
 import Data.Singletons.Decide
 import Data.Singletons.TH
@@ -51,6 +52,12 @@
 
 genSingletons [''Sort]
 singDecideInstance ''Sort
+
+-- | Turn implicit sort parameter into explicit one
+withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a
+withSort SBooleanSort     a = a
+withSort SIntegralSort    a = a
+withSort (SArraySort i e) a = withSort i $ withSort e $ a
 
 show' :: Sort -> String
 show' BooleanSort     = "bool"
diff --git a/src/Data/Expression/Utils/Indexed/Eq.hs b/src/Data/Expression/Utils/Indexed/Eq.hs
--- a/src/Data/Expression/Utils/Indexed/Eq.hs
+++ b/src/Data/Expression/Utils/Indexed/Eq.hs
@@ -12,8 +12,6 @@
 
 module Data.Expression.Utils.Indexed.Eq where
 
-import Data.Kind
-
 -- | Indexed types that can be equated
 class IEq (a :: i -> *) where
     ieq :: forall j. a j -> a j -> Bool
diff --git a/src/Data/Expression/Utils/Indexed/Foldable.hs b/src/Data/Expression/Utils/Indexed/Foldable.hs
--- a/src/Data/Expression/Utils/Indexed/Foldable.hs
+++ b/src/Data/Expression/Utils/Indexed/Foldable.hs
@@ -13,7 +13,6 @@
 module Data.Expression.Utils.Indexed.Foldable (IFoldable(..)) where
 
 import Data.Functor.Const
-import Data.Kind
 
 -- | Type constructors (usually functors) that can be folded
 class IFoldable (f :: (i -> *) -> (i -> *)) where
diff --git a/src/Data/Expression/Utils/Indexed/Functor.hs b/src/Data/Expression/Utils/Indexed/Functor.hs
--- a/src/Data/Expression/Utils/Indexed/Functor.hs
+++ b/src/Data/Expression/Utils/Indexed/Functor.hs
@@ -14,7 +14,6 @@
 module Data.Expression.Utils.Indexed.Functor (IFix(..), IFunctor(..), icata) where
 
 import Data.Functor.Const
-import Data.Kind
 import Data.Singletons
 
 import Data.Expression.Utils.Indexed.Eq
diff --git a/src/Data/Expression/Utils/Indexed/Sum.hs b/src/Data/Expression/Utils/Indexed/Sum.hs
--- a/src/Data/Expression/Utils/Indexed/Sum.hs
+++ b/src/Data/Expression/Utils/Indexed/Sum.hs
@@ -56,10 +56,6 @@
     emb :: f a i -> g a i
     res :: g a i -> Maybe (f a i)
 
-instance IFunctor f => f :<<: f where
-    emb = id
-    res = Just
-
 instance (IFunctor f, IFunctor g) => f :<<: (g :+: f) where
     emb = InR
     res (InL _) = Nothing
diff --git a/src/Data/Expression/Utils/Indexed/Traversable.hs b/src/Data/Expression/Utils/Indexed/Traversable.hs
--- a/src/Data/Expression/Utils/Indexed/Traversable.hs
+++ b/src/Data/Expression/Utils/Indexed/Traversable.hs
@@ -14,7 +14,6 @@
 module Data.Expression.Utils.Indexed.Traversable where
 
 import Control.Monad
-import Data.Kind
 
 import Data.Expression.Utils.Indexed.Functor