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.13
+Version:          1.14
 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
@@ -26,6 +26,7 @@
     applicative-extras,
     base >= 4.8 && < 5,
     containers,
+    extra,
     HUnit,
     mtl,
     parsec,
diff --git a/src/Data/Logic/ATP/Meson.hs b/src/Data/Logic/ATP/Meson.hs
--- a/src/Data/Logic/ATP/Meson.hs
+++ b/src/Data/Logic/ATP/Meson.hs
@@ -176,7 +176,7 @@
 -- -------------------------------------------------------------------------
 
 mexpand1 :: (JustLiteral lit, Ord lit,
-             HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),
+             HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
            Set (PrologRule lit)
         -> Set lit
@@ -206,7 +206,7 @@
 -- -------------------------------------------------------------------------
 
 puremeson1 :: forall fof atom term v function.
-              (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,
+              (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof,
                atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
                v ~ VarOf fof, v ~ TVarOf term) =>
               Maybe Depth -> fof -> Failing Depth
@@ -219,7 +219,7 @@
       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)
 
 meson1 :: forall m fof atom predicate term function v.
-          (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
+          (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
            atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
 meson1 maxdl fm =
@@ -230,7 +230,7 @@
 -- With repetition checking and divide-and-conquer search.
 -- -------------------------------------------------------------------------
 
-equal :: (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
+equal :: (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
           atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
          Map v term -> lit -> lit -> Bool
 equal env fm1 fm2 =
@@ -257,7 +257,7 @@
                                    (e1,n2+r1,k1))
                  (env,n1,k)
 
-mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),
+mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
            Set (PrologRule lit)
         -> Set lit
@@ -284,7 +284,7 @@
             mexpand2' = mexpands rules (Set.insert g ancestors) asm cont
             (Prolog asm c, k') = renamerule k rule
 
-mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
+mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (PrologRule lit)
          -> Set lit
@@ -317,7 +317,7 @@
 puremeson2 :: forall fof atom term v.
              (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
               IsFirstOrder fof,
-              Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof
+              Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof
              ) => Maybe Depth -> fof -> Failing Depth
 puremeson2 maxdl fm =
     snd <$> deepen f (Depth 0) maxdl
@@ -328,7 +328,7 @@
       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)
 
 meson2 :: forall m fof atom term function v.
-          (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,
+          (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof,
            HasSkolem function, Monad m,
            atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
@@ -336,7 +336,7 @@
     askolemize ((.~.)(generalize fm)) >>=
     return . Set.map (puremeson2 maxdl . list_conj) . (simpdnf' :: fof -> Set (Set fof))
 
-meson :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
+meson :: (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
           atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
          Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
 meson = meson2
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
@@ -68,7 +68,7 @@
 
 -- | MGU of a set of literals.
 mgu :: forall lit atom term v.
-       (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
+       (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
         atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
        Set lit -> StateT (Map v term) Failing (Map v term)
 mgu l =
@@ -80,7 +80,7 @@
       _ -> solve <$> get
 
 unifiable :: forall lit term atom v.
-             (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),
+             (JustLiteral lit, IsTerm term, HasApply atom, Unify Failing (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 :: Failing (Map v term))
@@ -101,7 +101,7 @@
 -- General resolution rule, incorporating factoring as in Robinson's paper.
 -- -------------------------------------------------------------------------
 
-resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
+resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
                atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
               Set lit -> Set lit -> lit -> Set lit -> Set lit
 resolvents cl1 cl2 p acc =
@@ -118,7 +118,7 @@
       -- ps2 :: Set fof
       ps2 = Set.filter (unifiable ((.~.) p)) cl2
 
-resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
+resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
                     atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                    Set lit -> Set lit -> Set lit
 resolve_clauses cls1 cls2 =
@@ -130,7 +130,7 @@
 -- Basic "Argonne" loop.
 -- -------------------------------------------------------------------------
 
-resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),
+resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 resloop1 used unused =
@@ -146,13 +146,13 @@
 pure_resolution1 :: forall fof atom term v.
                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,
                      IsFirstOrder fof,
-                     Unify (atom, atom), term ~ UTermOf (atom, atom),
+                     Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
                      Ord fof, Pretty fof
                     ) => fof -> Failing Bool
 pure_resolution1 fm = resloop1 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))
 
 resolution1 :: forall m fof atom term v function.
-               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
+               (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof))
@@ -221,7 +221,7 @@
 
 -- | With deletion of tautologies and bi-subsumption with "unused".
 resolution2 :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
+               (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof))
@@ -229,13 +229,13 @@
 pure_resolution2 :: forall fof atom term v.
                     (IsFirstOrder fof, Ord fof, Pretty fof,
                      HasApply atom, IsTerm term,
-                     Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
+                     Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) =>
                     fof -> Failing Bool
 pure_resolution2 fm = resloop2 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))
 
 resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
-             Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
+             Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 resloop2 used unused =
@@ -296,20 +296,20 @@
 
 -- | Positive (P1) resolution.
 presolution :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,
+               (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 presolution fm =
     askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_presolution . list_conj) . (simpdnf' :: fof -> Set (Set fof))
 
 pure_presolution :: forall fof atom term v.
-                    (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof,
+                    (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof,
                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) =>
                     fof -> Failing Bool
 pure_presolution fm = presloop Set.empty (simpcnf id (specialize id (pnf fm :: fof) ::  PFormula atom) :: Set (Set (LFormula atom)))
 
 presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
-             Match (atom, atom) v term, Unify (atom, atom), term ~ UTermOf (atom, atom),
+             Match (atom, atom) v term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 presloop used unused =
@@ -324,7 +324,7 @@
           then Success True
           else presloop used' (Set.fold (incorporate cl) ros news)
 
-presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),
+presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
                      atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                     Set lit -> Set lit -> Set lit
 presolve_clauses cls1 cls2 =
@@ -334,7 +334,7 @@
 
 -- | Introduce a set-of-support restriction.
 resolution3 :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
+               (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution3 fm =
@@ -343,7 +343,7 @@
 pure_resolution3 :: forall fof atom term v.
                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
                      IsFirstOrder fof,
-                     Unify (atom, atom), term ~ UTermOf (atom, atom),
+                     Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
                      Match (atom, atom) v term,
                      Ord fof, Pretty fof) => fof -> Failing Bool
 pure_resolution3 fm =
diff --git a/src/Data/Logic/ATP/Tableaux.hs b/src/Data/Logic/ATP/Tableaux.hs
--- a/src/Data/Logic/ATP/Tableaux.hs
+++ b/src/Data/Logic/ATP/Tableaux.hs
@@ -46,20 +46,20 @@
 
 -- | Unify complementary literals.
 unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
-                      Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,
+                      Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,
                       atom1 ~ AtomOf lit1, term ~ TermOf atom1,
                       atom2 ~ AtomOf lit2, term ~ TermOf atom2) =>
-                     lit1 -> lit2 -> StateT (Map v term) Failing ()
+                     lit1 -> lit2 -> StateT (Map v term) m ()
 unify_complements p q = unify_literals p ((.~.) q)
 
 -- | Unify and refute a set of disjuncts.
 unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
-                 Unify (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,
+                 Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,
                  atom ~ AtomOf lit, term ~ TermOf atom) =>
                 Set (Set lit) -> Map v term -> Failing (Map v term)
 unify_refute djs env =
     case Set.minView djs of
-      Nothing -> Success env
+      Nothing -> pure env
       Just (d, odjs) ->
           settryfind (\ (p, n) -> execStateT (unify_complements p n) env >>= unify_refute odjs) pairs
           where
@@ -68,7 +68,7 @@
 
 -- | Hence a Prawitz-like procedure (using unification on DNF).
 prawitz_loop :: forall lit atom v term.
-                (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),
+                (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
                  atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                 Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
 prawitz_loop djs0 fvs djs n =
@@ -81,7 +81,7 @@
       newvar k = vt (fromString ("_" ++ show (n * length fvs + k)))
 
 prawitz :: forall formula atom term function v.
-           (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
+           (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
             v ~ TVarOf term, v ~ SVarOf function) =>
            formula -> Int
@@ -110,7 +110,7 @@
 -- Comparison of number of ground instances.
 -- -------------------------------------------------------------------------
 
-compare :: (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
+compare :: (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
             v ~ TVarOf term, v ~ SVarOf function) =>
            formula -> (Int, Int)
@@ -178,7 +178,7 @@
 
 -- | More standard tableau procedure, effectively doing DNF incrementally.  (p. 177)
 tableau :: forall formula atom term v function.
-           (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),
+           (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
            [formula] -> Depth -> RWS () () () (Failing (K, Map v term))
 tableau fms n0 =
@@ -214,14 +214,14 @@
             tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
             tryLit fm' l = failing (return . Failure) (\env' -> cont (k, env')) (execStateT (unify_complements fm' l) env)
 
-tabrefute :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),
+tabrefute :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
               atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
              Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
 tabrefute limit fms =
     let r = deepen (\n -> (,n) <$> evalRS (tableau fms n) () ()) (Depth 0) limit in
     failing Failure (Success . fst) r
 
-tab :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
+tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
         atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
         v ~ TVarOf term, v ~ SVarOf function) =>
        Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
@@ -288,7 +288,7 @@
 -- Try to split up the initial formula first; often a big improvement.
 -- -------------------------------------------------------------------------
 splittab :: forall formula atom term v function.
-            (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,
+            (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,
              atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
              v ~ TVarOf term, v ~ SVarOf function) =>
             formula -> [Failing ((K, Map v term), Depth)]
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
@@ -52,11 +52,11 @@
 -- single type contains both - for example, in template-haskell we
 -- want to unify a and b in a predicate such as this: @(AppT (AppT
 -- EqualityT a) b)@.
-class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where
+class (Monad m, IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify m a where
     type UTermOf a
-    unify' :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
+    unify' :: 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 :: (Unify m 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) =>
@@ -116,7 +116,7 @@
 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) =>
+                   Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) =>
                   lit1 -> lit2 -> StateT (Map v term) m ()
 unify_literals f1 f2 =
     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)
@@ -149,7 +149,7 @@
 --        where
 --          app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2)
 
-instance Unify (SkAtom, SkAtom) where
+instance Monad m => Unify m (SkAtom, SkAtom) where
     type UTermOf (SkAtom, SkAtom) = TermOf SkAtom
     unify' = uncurry unify_atoms_eq