diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Revision history for expressions-z3
 
+## 0.4
+
+* Bump dependencies
+
 ## 0.3
 
 * Bump dependencies
diff --git a/expressions-z3.cabal b/expressions-z3.cabal
--- a/expressions-z3.cabal
+++ b/expressions-z3.cabal
@@ -1,5 +1,5 @@
 name:                expressions-z3
-version:             0.3
+version:             0.4
 synopsis:            Encode and Decode expressions from Z3 ASTs
 description:
   A simple interface for converting expressions back and forth between pure
@@ -64,7 +64,7 @@
   exposed-modules:     Data.Expression.Z3
   build-depends:       base >=4.9 && <4.13,
                        containers >=0.5 && <0.7,
-                       expressions >=0.1.7 && <0.4,
+                       expressions >=0.4 && <0.5,
                        singletons >=2.2 && <2.6,
                        transformers >=0.5.2 && <0.6,
                        list-t >=1.0 && <1.1,
diff --git a/src/Data/Expression/Z3.hs b/src/Data/Expression/Z3.hs
--- a/src/Data/Expression/Z3.hs
+++ b/src/Data/Expression/Z3.hs
@@ -47,7 +47,7 @@
 import qualified Data.Map as M
 import qualified Z3.Monad as Z3
 
-type Cache g = M.Map Z3.AST (DynamicallySorted g)
+type Cache g = M.Map Z3.AST (DynamicallySortedFix g)
 
 newtype Decoder g a b = Decoder { unwrap :: StateT (Cache g) (ListT a) b } deriving ( Functor, Applicative, Alternative, Monad, MonadIO )
 
@@ -120,9 +120,9 @@
 toZ3 = F.getConst . icata itoZ3
 
 class IFromZ3Into (f :: (Sort -> *) -> Sort -> *) (g :: (Sort -> *) -> Sort -> *) where
-    ifromZ3App        :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> String -> Z3.App           -> Decoder g z3 (DynamicallySorted g)
-    ifromZ3Quantifier :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Bool -> [Z3.AST] -> Z3.AST -> Decoder g z3 (DynamicallySorted g)
-    ifromZ3Numeral    :: Z3.MonadZ3 z3 => Proxy f ->                                                   Int                        -> Decoder g z3 (DynamicallySorted g)
+    ifromZ3App        :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> String -> Z3.App           -> Decoder g z3 (DynamicallySortedFix g)
+    ifromZ3Quantifier :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> Bool -> [Z3.AST] -> Z3.AST -> Decoder g z3 (DynamicallySortedFix g)
+    ifromZ3Numeral    :: Z3.MonadZ3 z3 => Proxy f ->                                                   Int                           -> Decoder g z3 (DynamicallySortedFix g)
 
     ifromZ3App        _ _ _ _   = empty
     ifromZ3Quantifier _ _ _ _ _ = empty
@@ -183,7 +183,7 @@
             _ -> empty
     ifromZ3App _ _ _ _ = empty
 
-varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted VarF)
+varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted Var)
 varFromZ3 = ifromZ3 (Proxy :: Proxy (VarF :: (Sort -> *) -> Sort -> *)) varFromZ3
 
 local :: Z3.MonadZ3 z3 => Decoder VarF z3 a -> Decoder g z3 a
@@ -207,8 +207,8 @@
                 _ -> empty
         where
 
-            isVSorted :: DynamicallySorted VarF -> Bool
-            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )
+            isVSorted :: DynamicallySorted Var -> Bool
+            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted Var -> Maybe (IFix VarF v) )
 
     ifromZ3Quantifier _ _ _ _ _ = empty
 
@@ -230,8 +230,8 @@
                 _ -> empty
         where
 
-            isVSorted :: DynamicallySorted VarF -> Bool
-            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )
+            isVSorted :: DynamicallySorted Var -> Bool
+            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted Var -> Maybe (IFix VarF v) )
 
     ifromZ3Quantifier _ _ _ _ _ = empty
 
@@ -244,7 +244,7 @@
 
         where
 
-            ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySorted g] -> Decoder g z3 (DynamicallySorted g)
+            ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySortedFix g] -> Decoder g z3 (DynamicallySortedFix g)
             ifromZ3'' [DynamicallySorted s1 a, DynamicallySorted s2 b] = case s1 %~ s2 of
                 Proved Refl -> return . toDynamicallySorted . inject $ Equals s1 a b
                 Disproved _ -> empty
@@ -357,7 +357,7 @@
                   (g :: (Sort -> *) -> Sort -> *)
                   z3.
            ( IFromZ3Into f g, Z3.MonadZ3 z3 )
-         => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Z3.AST -> Decoder g z3 (DynamicallySorted g)
+         => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> Z3.AST -> Decoder g z3 (DynamicallySortedFix g)
 ifromZ3 p r a = do
     c <- Decoder $ get
     if a `M.member` c then do