diff --git a/atp-haskell.cabal b/atp-haskell.cabal
--- a/atp-haskell.cabal
+++ b/atp-haskell.cabal
@@ -1,5 +1,5 @@
 Name:             atp-haskell
-Version:          1.10
+Version:          1.13
 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code
 Description:      This package is a liberal translation from OCaml to Haskell of
                   the automated theorem prover written in OCaml in
diff --git a/src/Data/Logic/ATP/Resolution.hs b/src/Data/Logic/ATP/Resolution.hs
--- a/src/Data/Logic/ATP/Resolution.hs
+++ b/src/Data/Logic/ATP/Resolution.hs
@@ -79,10 +79,11 @@
             _ -> solve <$> get
       _ -> solve <$> get
 
-unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),
+unifiable :: forall lit term atom v.
+             (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),
               atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
              lit -> lit -> Bool
-unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty)
+unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty :: Failing (Map v term))
 
 -- -------------------------------------------------------------------------
 -- Rename a clause.
diff --git a/src/Data/Logic/ATP/Unif.hs b/src/Data/Logic/ATP/Unif.hs
--- a/src/Data/Logic/ATP/Unif.hs
+++ b/src/Data/Logic/ATP/Unif.hs
@@ -9,9 +9,11 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Data.Logic.ATP.Unif
-    ( Unify(unify, UTermOf)
+    ( Unify(unify', UTermOf)
+    , unify
     , unify_terms
     , unify_literals
     , unify_atoms
@@ -52,8 +54,11 @@
 -- EqualityT a) b)@.
 class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where
     type UTermOf a
-    unify :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
+    unify' :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
 
+unify :: (Unify a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a))
+unify a mp0 = execStateT (unify' a) mp0
+
 unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) =>
                [(term,term)] -> StateT (Map v term) m ()
 unify_terms = mapM_ (uncurry unify_term_pair)
@@ -75,19 +80,19 @@
           then mapM_ (uncurry unify_term_pair) (zip fargs gargs)
           else fail "impossible unification"
 
-istriv :: forall term v m. (IsTerm term, v ~ TVarOf term, Monad m) =>
+istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>
           v -> term -> StateT (Map v term) m Bool
 istriv x t =
     foldTerm vr fn t
     where
       vr :: v -> StateT (Map v term) m Bool
       vr y | x == y = return True
-      vr y = (Map.lookup y <$> get) >>= maybe (return False) (istriv x)
+      vr y = (Map.lookup y <$> get) >>= \(mt :: Maybe term) -> maybe (return False) (istriv x) mt
       fn :: f -> [term] -> StateT (Map v term) m Bool
       fn _ args = mapM (istriv x) args >>= bool (return False) (fail "cyclic") . or
 
 -- | Solve to obtain a single instantiation.
-solve :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>
+solve :: (IsTerm term, v ~ TVarOf term) =>
          Map v term -> Map v term
 solve env =
     if env' == env then env else solve env'
@@ -108,7 +113,8 @@
 -- variable type.  Note that only one needs to be 'JustLiteral', if
 -- the unification succeeds the other must have been too, if it fails,
 -- who cares.
-unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
+unify_literals :: forall lit1 lit2 atom1 atom2 v term m.
+                  (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
                    JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2,
                    Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, Monad m) =>
                   lit1 -> lit2 -> StateT (Map v term) m ()
@@ -117,8 +123,9 @@
     where
       ho _ _ = Nothing
       ne p q = Just $ unify_literals p q
-      tf p q = if p == q then Just (unify_terms []) else Nothing
-      at a1 a2 = Just (unify (a1, a2))
+      -- tf :: Bool -> Bool -> Maybe (StateT (Map v term) m ())
+      tf p q = if p == q then Just (unify_terms ([] :: [(term, term)])) else Nothing
+      at a1 a2 = Just (unify' (a1, a2))
 
 unify_atoms :: (JustApply atom1, term ~ TermOf atom1,
                 JustApply atom2, term ~ TermOf atom2,
@@ -144,7 +151,7 @@
 
 instance Unify (SkAtom, SkAtom) where
     type UTermOf (SkAtom, SkAtom) = TermOf SkAtom
-    unify = uncurry unify_atoms_eq
+    unify' = uncurry unify_atoms_eq
 
 test01, test02, test03, test04 :: Test
 test01 = TestCase (assertEqual "Unify test 1"