diff --git a/hell.cabal b/hell.cabal
index 54c85e3..cc980a7 100644
--- a/hell.cabal
+++ b/hell.cabal
@@ -30,6 +30,7 @@ executable hell
     , containers
     , criterion
     , criterion-measurement
+    , data-fix
     , directory
     , ghc-prim
     , haskell-src-exts
@@ -46,7 +47,9 @@ executable hell
     , th-orphans
     , these
     , time
+    , transformers
     , typed-process
+    , unification-fd
     , unliftio
     , vector
     , wai
@@ -70,6 +73,7 @@ test-suite hell-test
     , containers
     , criterion
     , criterion-measurement
+    , data-fix
     , directory
     , ghc-prim
     , haskell-src-exts
@@ -86,7 +90,9 @@ test-suite hell-test
     , th-orphans
     , these
     , time
+    , transformers
     , typed-process
+    , unification-fd
     , unliftio
     , vector
     , wai
diff --git a/package.yaml b/package.yaml
index a427634..5ffb2d7 100644
--- a/package.yaml
+++ b/package.yaml
@@ -34,6 +34,9 @@ dependencies:
 - time
 - warp
 - wai
+- unification-fd
+- transformers
+- data-fix
 - http-types
 - case-insensitive
 
diff --git a/src/Hell.hs b/src/Hell.hs
index 9bfdcf5..36aa46f 100644
--- a/src/Hell.hs
+++ b/src/Hell.hs
@@ -1,9 +1,10 @@
+{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFoldable, DeriveGeneric #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE ExistentialQuantification, DuplicateRecordFields, NoFieldSelectors #-}
@@ -42,10 +43,18 @@
 
 module Main (main, specMain) where
 
+
 #if __GLASGOW_HASKELL__ >= 906
 import Control.Monad
 #endif
 
+import Data.Tuple
+import qualified Control.Unification.Types as FD
+import Control.Monad.Trans.Except
+import qualified Control.Unification as FD
+import qualified Control.Unification.STVar as FD
+import GHC.Generics (Generic1)
+
 -- All modules tend to be imported qualified by their last component,
 -- e.g. 'Data.Graph' becomes 'Graph', and are then exposed to the Hell
 -- guest language as such.
@@ -103,7 +112,6 @@ import Data.Tree (Tree)
 import qualified Data.Tree as Tree
 import Data.Vector (Vector)
 import qualified Data.Vector as Vector
-import Data.Void
 import GHC.TypeLits
 import GHC.Types (Type)
 import qualified Language.Haskell.Exts as HSE
@@ -209,7 +217,7 @@ compileFile stats filePath = do
               case lookup "main" dterms of
                 Nothing -> error "No main declaration!"
                 Just main' -> do
-                  inferred <- inferExp (nestStat stats) main'
+                  inferred <- infer_exp (nestStat stats) main'
                   case inferred of
                     Left err -> error $ prettyString err
                     Right uterm -> do
@@ -1631,43 +1639,29 @@ desugarAll types0 terms0 = do
 -- Infer
 
 data InferError
-  = UnifyError UnifyError
-  | ZonkError ZonkError
+  = ZonkError ZonkError
   | ElabError ElaborateError
-  deriving (Show)
+  | ST_mapping_error
+  | ST_unify_error
+  | ST_apply_bindings_error
+deriving instance Show InferError
 
 -- | Note: All types in the input are free of metavars. There is an
 -- intermediate phase in which there are metavars, but then they're
 -- all eliminated. By the type system, the output contains only
 -- determinate types.
-inferExp ::
+infer_exp ::
   StatsEnabled ->
   UTerm () ->
   IO (Either InferError (UTerm SomeTypeRep))
-inferExp stats uterm = do
+infer_exp stats uterm = do
   t0 <- getTime
   case elaborate uterm of
     Left elabError -> pure $ Left $ ElabError elabError
     Right (iterm, equalities) -> do
       t1 <- getTime
       emitStat stats "elaborate" (t1 - t0)
-      case unify equalities of
-        Left unifyError -> pure $ Left $ UnifyError unifyError
-        Right subs -> do
-          t2 <- getTime
-          emitStat stats "unify" (t2 - t1)
-          case traverse (zonkToStarType subs) iterm of
-            Left zonkError -> pure $ Left $ ZonkError $ zonkError
-            Right !sterm -> do
-              t3 <- getTime
-              emitStat stats "zonk" (t3 - t2)
-              pure $ Right sterm
-
--- | Zonk a type and then convert it to a type: t :: *
-zonkToStarType :: Map IMetaVar (IRep IMetaVar) -> IRep IMetaVar -> Either ZonkError SomeTypeRep
-zonkToStarType subs irep = do
-  zonked <- zonk (substitute subs irep)
-  toSomeTypeRep zonked
+      st_unify stats equalities iterm
 
 --------------------------------------------------------------------------------
 -- Occurs check
@@ -2637,44 +2631,142 @@ process_setWorkingDir :: forall a b c. Text -> ProcessConfig a b c -> ProcessCon
 process_setWorkingDir filepath = Process.setWorkingDir (Text.unpack filepath)
 
 --------------------------------------------------------------------------------
--- Inference type representation
-
-data IRep v
-  = IVar v
-  | IApp (IRep v) (IRep v)
-  | IFun (IRep v) (IRep v)
-  | ICon SomeTypeRep
-  deriving (Functor, Traversable, Foldable, Eq, Ord, Show)
-
-data ZonkError
-  = ZonkKindError
-  | AmbiguousMetavar IMetaVar
-  deriving (Show)
-
--- | A complete implementation of conversion from the inferer's type
+-- unification-fd compatibility layer
+
+data Ty a
+  = TyApp a a
+  | TyFun a a
+  | TyCon SomeTypeRep
+  deriving (Functor, Traversable, Foldable, Eq, Ord, Show, Generic1)
+-- Below: Needed for FD.freeVar (note for myself, not audience)
+deriving instance FD.Unifiable Ty
+
+-- Unify all the constraints in @equalities@, zonk and update the term and return it.
+st_unify :: Traversable t
+  => StatsEnabled
+  -> Set (Equality (IRep IMetaVar))
+  -> t (IRep IMetaVar)
+  -> IO (Either InferError (t SomeTypeRep))
+st_unify stats set term = do
+  t1 <- getTime
+  let result =
+        FD.runSTBinding do
+          -- Thaw the equalities.
+          (equalities, mapping) <- run_stize $ stize_equalities $ Set.toList set
+          -- Unify the mutable equalities into the ambient environment.
+          result' <- runExceptT $ st_unifier_ equalities
+          case result' of
+            Left _err -> pure $ Left ST_unify_error
+            Right () -> do
+              -- Apply bindings, zonk and freeze all the types across the term.
+              runExceptT $
+                for term \irepmv -> do
+                  uterm <- for (irep_to_uterm irepmv) \imv ->
+                    case Map.lookup imv mapping of
+                      Nothing -> throwE $ ST_mapping_error
+                      Just stvar -> pure stvar
+                  uterm' <- withExceptT (const ST_apply_bindings_error) $ st_apply uterm
+                  except $ first ZonkError $
+                    to_sometyperep
+                      mapping
+                      uterm'
+  case result of
+    Left err -> pure $ Left err
+    Right (!term') -> do
+      t2 <- getTime
+      emitStat stats "unify-and-zonk" (t2 - t1)
+      pure $ Right term'
+
+-- Apply bindings; this type signature avoids type inference problems.
+st_apply :: FD.UTerm Ty (FD.STVar s Ty)
+         -> ExceptT (FD.UFailure Ty (FD.STVar s Ty)) (FD.STBinding s) (FD.UTerm Ty (FD.STVar s Ty))
+st_apply = FD.applyBindings
+
+-- Unify all the equality constraints provided.
+st_unifier_ :: [Equality (FD.UTerm Ty (FD.STVar s Ty))]
+            -> ExceptT (FD.UFailure Ty (FD.STVar s Ty)) (FD.STBinding s) ()
+st_unifier_ = traverse_ \(Equality _src a b) -> void $ FD.unify a b
+
+-- Run an ST-izing operation, and return the mapping from the original IMetaVars to the STVars, so that they can be recovered later.
+run_stize :: StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) x -> FD.STBinding s (x, Map IMetaVar (FD.STVar s Ty))
+run_stize = flip runStateT (mempty :: Map IMetaVar (FD.STVar s Ty))
+
+-- ST-ize the metavars in all types in the equality constraints set
+stize_equalities :: [Equality (IRep IMetaVar)] -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) [Equality (FD.UTerm Ty (FD.STVar s Ty))]
+stize_equalities = traverse stize_equality
+
+-- ST-ize the metavars in all types in the equality's types on both sides, it also
+-- is exactly where conversion from IRep to UTerm Ty occurs.
+stize_equality :: Equality (IRep IMetaVar) -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (Equality (FD.UTerm Ty (FD.STVar s Ty)))
+stize_equality (Equality loc a b) = do
+  Equality loc <$> stize_uterm (irep_to_uterm a) <*> stize_uterm (irep_to_uterm b)
+
+-- ST-ize the metavars in a uterm
+stize_uterm :: FD.UTerm Ty IMetaVar -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (FD.UTerm Ty (FD.STVar s Ty))
+stize_uterm = traverse stize_imetavar
+
+-- ST-ize this metavar and remember that it was done
+stize_imetavar :: IMetaVar -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (FD.STVar s Ty)
+stize_imetavar = \v -> do
+  mexisting <- gets (Map.lookup v)
+  case mexisting of
+    Just stv -> pure stv
+    Nothing -> do
+      stv <- lift FD.freeVar
+      modify' (Map.insert v stv)
+      pure stv
+
+irep_to_uterm :: IRep v -> FD.UTerm Ty v
+irep_to_uterm = \case
+  IVar v -> FD.UVar v
+  IApp f x -> FD.UTerm (TyApp (irep_to_uterm f) (irep_to_uterm x))
+  IFun f x -> FD.UTerm (TyFun (irep_to_uterm f) (irep_to_uterm x))
+  ICon t -> FD.UTerm $ TyCon t
+
+-- | (unification-fd edition)
+-- A complete implementation of conversion from the inferer's type
 -- rep to some star type, ready for the type checker.
-toSomeTypeRep :: IRep Void -> Either ZonkError SomeTypeRep
-toSomeTypeRep t = do
+-- Jumps straight from UTerm Ty to SomeTypeRep in one go; handles
+-- ambiguous vars and kind errors here.
+to_sometyperep :: forall v. Eq v => (Map IMetaVar v) ->
+  FD.UTerm Ty v -> Either ZonkError SomeTypeRep
+to_sometyperep mapping t = do
   go t
   where
-    go :: IRep Void -> Either ZonkError SomeTypeRep
+    go :: FD.UTerm Ty v -> Either ZonkError SomeTypeRep
     go = \case
-      IVar v -> pure (absurd v)
-      ICon someTypeRep -> pure someTypeRep
-      IFun a b -> do
+      FD.UVar k -> Left $ ST_ambiguous_var (List.lookup k $ map swap $ Map.toList mapping)
+      FD.UTerm (TyCon someTypeRep) -> pure someTypeRep
+      FD.UTerm (TyFun a b) -> do
         a' <- go a
         b' <- go b
         case (a', b') of
           (StarTypeRep aRep, StarTypeRep bRep) ->
             pure $ StarTypeRep (Type.Fun aRep bRep)
           _ -> Left ZonkKindError
-      IApp f a -> do
+      FD.UTerm (TyApp f a) -> do
         f' <- go f
         a' <- go a
         case applyTypes f' a' of
           Just someTypeRep -> pure someTypeRep
           _ -> Left ZonkKindError
 
+--------------------------------------------------------------------------------
+-- Inference type representation
+
+data IRep v
+  = IVar v
+  | IApp (IRep v) (IRep v)
+  | IFun (IRep v) (IRep v)
+  | ICon SomeTypeRep
+  deriving (Functor, Traversable, Foldable, Eq, Ord, Show)
+
+data ZonkError
+  = ZonkKindError
+  | AmbiguousMetavar IMetaVar
+  | ST_ambiguous_var (Maybe IMetaVar)
+  deriving (Show)
+
 -- | Convert from a type-indexed type to an untyped type.
 fromSomeStarType :: forall void. SomeStarType -> IRep void
 fromSomeStarType (SomeStarType r) = fromSomeType (SomeTypeRep r)
@@ -2791,78 +2883,6 @@ freshIMetaVar srcSpanInfo = do
   modify \elaborate' -> elaborate' {counter = counter + 1}
   pure $ IMetaVar0 counter srcSpanInfo
 
---------------------------------------------------------------------------------
--- Unification
-
-data UnifyError
-  = OccursCheck
-  | TypeMismatch HSE.SrcSpanInfo (IRep IMetaVar) (IRep IMetaVar)
-  deriving (Show)
-
--- | Unification of equality constraints, a ~ b, to substitutions.
-unify :: Set (Equality (IRep IMetaVar)) -> Either UnifyError (Map IMetaVar (IRep IMetaVar))
-unify = foldM update mempty
-  where
-    update existing equality =
-      fmap
-        (`extends` existing)
-        (examine (fmap (substitute existing) equality))
-    examine (Equality l a b)
-      | a == b = pure mempty
-      | IVar ivar <- a = bindMetaVar ivar b
-      | IVar ivar <- b = bindMetaVar ivar a
-      | IFun a1 b1 <- a,
-        IFun a2 b2 <- b =
-          unify (Set.fromList [Equality l a1 a2, Equality l b1 b2])
-      | IApp a1 b1 <- a,
-        IApp a2 b2 <- b =
-          unify (Set.fromList [Equality l a1 a2, Equality l b1 b2])
-      | ICon x <- a,
-        ICon y <- b =
-          if x == y
-            then pure mempty
-            else Left $ TypeMismatch l a b
-      | otherwise = Left $ TypeMismatch l a b
-
--- | Apply new substitutions to the old ones, and expand the set to old+new.
-extends :: Map IMetaVar (IRep IMetaVar) -> Map IMetaVar (IRep IMetaVar) -> Map IMetaVar (IRep IMetaVar)
-extends new old = fmap (substitute new) old <> new
-
--- | Apply any substitutions to the type, where there are metavars.
-substitute :: Map IMetaVar (IRep IMetaVar) -> IRep IMetaVar -> IRep IMetaVar
-substitute subs = go
-  where
-    go = \case
-      IVar v -> case Map.lookup v subs of
-        Nothing -> IVar v
-        Just ty -> ty
-      ICon c -> ICon c
-      IFun a b -> IFun (go a) (go b)
-      IApp a b -> IApp (go a) (go b)
-
--- | Do an occurrs check, if all good, return a binding.
-bindMetaVar ::
-  IMetaVar ->
-  IRep IMetaVar ->
-  Either UnifyError (Map IMetaVar (IRep IMetaVar))
-bindMetaVar var typ
-  | occurs var typ = Left OccursCheck
-  | otherwise = pure $ Map.singleton var typ
-
--- | Occurs check.
-occurs :: IMetaVar -> IRep IMetaVar -> Bool
-occurs ivar = any (== ivar)
-
--- | Remove any metavars from the type.
---
--- <https://stackoverflow.com/questions/31889048/what-does-the-ghc-source-mean-by-zonk>
-zonk :: IRep IMetaVar -> Either ZonkError (IRep Void)
-zonk = \case
-  IVar var -> Left $ AmbiguousMetavar var
-  ICon c -> pure $ ICon c
-  IFun a b -> IFun <$> zonk a <*> zonk b
-  IApp a b -> IApp <$> zonk a <*> zonk b
-
 --------------------------------------------------------------------------------
 -- Parse with #!/shebangs
 
@@ -3083,6 +3103,11 @@ instance (Pretty a) => Pretty (IRep a) where
 instance Pretty ZonkError where
   pretty = \case
     ZonkKindError -> "Kind error."
+    ST_ambiguous_var imetavar -> "(ST) Ambiguous meta variable: "
+        <> maybe "???" pretty imetavar
+        <> "\n"
+        <> "arising from "
+        <> maybe "???" (pretty . (.srcSpanInfo)) imetavar
     AmbiguousMetavar imetavar ->
       "Ambiguous meta variable: "
         <> pretty imetavar
@@ -3096,20 +3121,6 @@ instance Pretty ElaborateError where
     BadInstantiationBug -> "BUG: BadInstantiationBug. Please report."
     VariableNotInScope s -> "Variable not in scope: " <> pretty s
 
-instance Pretty UnifyError where
-  pretty = \case
-    OccursCheck -> "Occurs check failed: Infinite type."
-    TypeMismatch l a b ->
-      mconcat $
-        List.intersperse
-          "\n\n"
-          [ "Couldn't match type",
-            "  " <> pretty a,
-            "against type",
-            "  " <> pretty b,
-            "arising from " <> pretty l
-          ]
-
 instance Pretty HSE.SrcSpanInfo where
   pretty l =
     mconcat
@@ -3155,9 +3166,11 @@ instance Pretty DesugarError where
 
 instance Pretty InferError where
   pretty = \case
-    UnifyError e -> "Unification error: " <> pretty e
     ZonkError e -> "Zonk error: " <> pretty e
     ElabError e -> "Elaboration error: " <> pretty e
+    ST_mapping_error -> "BUG: Unification meta mapping error."
+    ST_unify_error -> "Unification error!"
+    ST_apply_bindings_error -> "Unification apply bindings error."
 
 --------------------------------------------------------------------------------
 -- Generate docs