diff --git a/README b/README
--- a/README
+++ b/README
@@ -48,8 +48,8 @@
     Rank2Types
     MultiParamTypeClasses
     FunctionalDependencies -- Alas, necessary for type inference
-    FlexibleContexts       -- Generally necessary for practical use of MPTCs
-    FlexibleInstances      -- Generally necessary for practical use of MPTCs
+    FlexibleContexts       -- Necessary for practical use of MPTCs
+    FlexibleInstances      -- Necessary for practical use of MPTCs
     UndecidableInstances   -- Needed for Show instances due to two-level types
 
 ----------------------------------------------------------- fin.
diff --git a/VERSION b/VERSION
--- a/VERSION
+++ b/VERSION
@@ -1,3 +1,9 @@
+0.7.0 (2012-xx-xx):
+    - Control.Unification: changed the type of seenAs to ensure that variables can only be seen as structure.
+    - Renamed MutTerm to UTerm (and MutVar to UVar)
+    - Replaced the Variable.eqVar method by plain old Eq.(==)
+    - Control.Unification: added getFreeVarsAll, applyBindingsAll, freshenAll
+    - Swapped type argument order for MutTerm, so that it can be a functor etc. Also changed BindingMonad, UnificationFailure, Rank, and RankedBindingMonad for consistency.
 0.6.0 (2012-02-17):
     - Removed the phantom type argument for Variables.
 0.5.0 (2011-07-12):
diff --git a/src/Control/Monad/EitherK.hs b/src/Control/Monad/EitherK.hs
--- a/src/Control/Monad/EitherK.hs
+++ b/src/Control/Monad/EitherK.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.06.30
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Monad.EitherK
 -- License     :  BSD
@@ -108,8 +108,10 @@
     fmap f (EK m) = EK (\k -> m (k . f))
 
 instance Applicative (EitherK e) where
-    pure  = return
-    (<*>) = ap
+    pure   = return
+    (<*>)  = ap
+    (*>)   = (>>)
+    x <* y = x >>= \a -> y >> return a
 
 instance Monad (EitherK e) where
     return a   = EK (\k -> k a)
@@ -152,14 +154,29 @@
 toEitherKT (Right a) = return a
 
 
--- TODO: isn't there a better implementation that doesn't lose shortcircuiting?
 -- | Lift an @EitherK@ into an @EitherKT@.
 liftEitherK :: (Monad m) => EitherK e a -> EitherKT e m a
 {-# INLINE liftEitherK #-}
 liftEitherK = toEitherKT . runEitherK
+--
+-- With the above implementation, when @liftEitherK x@ is forced
+-- it will force not only @x = EK m@, but will also force @m@. If
+-- we want to force only @x@ and to defer @m@, then we should use
+-- the following implementation instead:
+--
+-- > liftEitherK (EK m) = EKT (\k -> either (return . Left) k (m Right))
+--
+-- Or if we want to defer both @m@ and @x@, then we could use:
+--
+-- > liftEitherK x = EKT (\k -> either (return . Left) k (runEitherK x))
+--
+-- However, all versions need to reify @m@ at some point, and
+-- therefore will lose short-circuiting. This is necessary since
+-- given some @k :: a -> m (Either e r)@ we have no way of constructing
+-- the needed @k' :: a -> Either e r@ from it without prematurely
+-- executing the side-effects.
 
 
--- TODO: is there a better implementation?
 -- | Lower an @EitherKT@ into an @EitherK@.
 lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a)
 {-# INLINE lowerEitherK #-}
@@ -191,14 +208,17 @@
     fmap f (EKT m) = EKT (\k -> m (k . f))
 
 instance Applicative (EitherKT e m) where
-    pure  = return
-    (<*>) = ap
+    pure   = return
+    (<*>)  = ap
+    (*>)   = (>>)
+    x <* y = x >>= \a -> y >> return a
 
 instance Monad (EitherKT e m) where
     return a    = EKT (\k -> k a)
     EKT m >>= f = EKT (\k -> m (\a -> case f a of EKT n -> n k))
 
--- TODO: is there any way to define catchEitherKT so it only requires Applicative m?
+-- I'm pretty sure it's impossible to define a @(<|>)@ which only
+-- requires @Applicative m@.
 instance (Monad m, Monoid e) => Alternative (EitherKT e m) where
     empty = mzero
     (<|>) = mplus
diff --git a/src/Control/Monad/MaybeK.hs b/src/Control/Monad/MaybeK.hs
--- a/src/Control/Monad/MaybeK.hs
+++ b/src/Control/Monad/MaybeK.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE Rank2Types, MultiParamTypeClasses #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.06.30
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Monad.MaybeK
 -- License     :  BSD
@@ -86,8 +86,10 @@
     fmap f (MK m) = MK (\k -> m (k . f))
 
 instance Applicative MaybeK where
-    pure  = return
-    (<*>) = ap
+    pure   = return
+    (<*>)  = ap
+    (*>)   = (>>)
+    x <* y = x >>= \a -> y >> return a
 
 instance Monad MaybeK where
     return a   = MK (\k -> k a)
@@ -127,14 +129,29 @@
 toMaybeKT (Just a) = return a
 
 
--- TODO: isn't there a better implementation that doesn't lose shortcircuiting?
 -- | Lift an @MaybeK@ into an @MaybeKT@.
 liftMaybeK :: (Monad m) => MaybeK a -> MaybeKT m a
 {-# INLINE liftMaybeK #-}
 liftMaybeK = toMaybeKT . runMaybeK
+--
+-- With the above implementation, when @liftMaybeK x@ is forced it
+-- will force not only @x = MK m@, but will also force @m@. If we
+-- want to force only @x@ and to defer @m@, then we should use the
+-- following implementation instead:
+--
+-- > liftMaybeK (MK m) = MKT (\k -> maybe (return Nothing) k (m Just))
+--
+-- Or if we want to defer both @m@ and @x@, then we could use:
+--
+-- > liftMaybeK x = MKT (\k -> maybe (return Nothing) k (runMaybeK x))
+--
+-- However, all versions need to reify @m@ at some point, and
+-- therefore will lose short-circuiting. This is necessary since
+-- given some @k :: a -> m (Maybe r)@ we have no way of constructing
+-- the needed @k' :: a -> Maybe r@ from it without prematurely
+-- executing the side-effects.
 
 
--- TODO: is there a better implementation?
 -- | Lower an @MaybeKT@ into an @MaybeK@.
 lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a)
 {-# INLINE lowerMaybeK #-}
@@ -145,8 +162,10 @@
     fmap f (MKT m) = MKT (\k -> m (k . f))
 
 instance Applicative (MaybeKT m) where
-    pure  = return
-    (<*>) = ap
+    pure   = return
+    (<*>)  = ap
+    (*>)   = (>>)
+    x <* y = x >>= \a -> y >> return a
 
 instance Monad (MaybeKT m) where
     return a    = MKT (\k -> k a)
diff --git a/src/Control/Monad/State/UnificationExtras.hs b/src/Control/Monad/State/UnificationExtras.hs
--- a/src/Control/Monad/State/UnificationExtras.hs
+++ b/src/Control/Monad/State/UnificationExtras.hs
@@ -35,12 +35,14 @@
 -- | Lift a reader into a state monad. More particularly, this
 -- allows disabling mutability in a local context within @StateT@.
 liftReaderT :: (Monad m) => ReaderT e m a -> StateT e m a
+{-# INLINE liftReaderT #-}
 liftReaderT r = StateT $ \e -> liftM (\a -> (a,e)) (runReaderT r e)
 
 
 -- | Lift a reader into a state monad. More particularly, this
 -- allows disabling mutability in a local context within @State@.
 liftReader :: Reader e a -> State e a
+{-# INLINE liftReader #-}
 liftReader = liftReaderT
 
 
diff --git a/src/Control/Unification.hs b/src/Control/Unification.hs
--- a/src/Control/Unification.hs
+++ b/src/Control/Unification.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
-{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-}
 ----------------------------------------------------------------
---                                                  ~ 2012.02.17
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -27,8 +27,8 @@
 module Control.Unification
     (
     -- * Data types, classes, etc
-    -- ** Mutable terms
-      MutTerm(..)
+    -- ** Unification terms
+      UTerm(..)
     , freeze
     , unfreeze
     -- ** Errors
@@ -60,12 +60,19 @@
     , unifyOccurs
     , subsumes
     
+    -- * Operations on many terms
+    , getFreeVarsAll
+    , applyBindingsAll
+    , freshenAll
+    -- subsumesAll -- to ensure that there's a single coherent substitution allowing the schema to subsume all the terms in some collection. 
+
     -- * Helper functions
     -- | Client code should not need to use these functions, but
     -- they are exposed just in case they are needed.
     , fullprune
     , semiprune
     , occursIn
+    -- TODO: add a post-hoc occurs check in order to have a version of unify which is fast, yet is also guaranteed to fail when it ought to (rather than deferring the failure until later, as the current unify does).
     ) where
 
 import Prelude
@@ -75,6 +82,7 @@
 import qualified Data.IntSet as IS
 import Data.Foldable
 import Data.Traversable
+import Control.Monad.Identity (Identity(..))
 import Control.Applicative
 import Control.Monad       (MonadPlus(..))
 import Control.Monad.Trans (MonadTrans(..))
@@ -93,18 +101,16 @@
 -- the chain is unbound), and return that end.
 --
 -- N.B., this is almost never the function you want. Cf., 'semiprune'.
-fullprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t)
-fullprune t0 =
-    case t0 of
-    MutTerm _ -> return t0
-    MutVar  v -> do
-        mb <- lookupVar v
-        case mb of
-            Nothing -> return t0
-            Just t  -> do
-                finalTerm <- fullprune t
-                v `bindVar` finalTerm
-                return finalTerm
+fullprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)
+fullprune t0@(UTerm _ ) = return t0
+fullprune t0@(UVar  v0) = do
+    mb <- lookupVar v0
+    case mb of
+        Nothing -> return t0
+        Just t  -> do
+            finalTerm <- fullprune t
+            v0 `bindVar` finalTerm
+            return finalTerm
 
 
 -- N.B., this assumes there are no directly-cyclic chains!
@@ -114,24 +120,21 @@
 -- bound or not. This allows detecting many cases where multiple
 -- variables point to the same term, thereby allowing us to avoid
 -- re-unifying the term they point to.
-semiprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t)
-semiprune =
-    \t0 ->
-        case t0 of
-        MutTerm _  -> return t0
-        MutVar  v0 -> loop t0 v0
+semiprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)
+semiprune t0@(UTerm _ ) = return t0
+semiprune t0@(UVar  v0) = loop t0 v0
     where
     -- We pass the @t@ for @v@ in order to add just a little more sharing.
-    loop t v = do
-        mb <- lookupVar v
+    loop t0 v0 = do
+        mb <- lookupVar v0
         case mb of
-            Nothing -> return t
-            Just t' -> 
-                case t' of
-                MutTerm _  -> return t
-                MutVar  v' -> do
-                    finalVar <- loop t' v'
-                    v `bindVar` finalVar
+            Nothing -> return t0
+            Just t  -> 
+                case t  of
+                UTerm _  -> return t0
+                UVar  v  -> do
+                    finalVar <- loop t v
+                    v0 `bindVar` finalVar
                     return finalVar
 
 
@@ -139,32 +142,36 @@
 -- Since occurs checks only make sense when we're about to bind the
 -- variable to the term, we do not bother checking for the possibility
 -- of the variable occuring bound in the term.
-occursIn :: (BindingMonad v t m) => v -> MutTerm v t -> m Bool
-occursIn v t0 = do
-    t <- fullprune t0
-    case t of
-        MutTerm t' -> or <$> mapM (v `occursIn`) t' -- TODO: use foldlM instead
-        MutVar  v' -> return $! v `eqVar` v'
+occursIn :: (BindingMonad t v m) => v -> UTerm t v -> m Bool
+{-# INLINE occursIn #-}
+occursIn v0 t0 = do
+    t0 <- fullprune t0
+    case t0 of
+        UTerm t -> or <$> mapM (v0 `occursIn`) t
+            -- TODO: benchmark the following for shortcircuiting
+            -- > Traversable.foldlM (\b t' -> if b then return True else v0 `occursIn` t') t
+        UVar  v -> return $! v0 == v
 
 
 -- TODO: use IM.insertWith or the like to do this in one pass
+--
 -- | Update the visited-set with a seclaration that a variable has
 -- been seen with a given binding, or throw 'OccursIn' if the
 -- variable has already been seen.
 seenAs
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => v               -- ^
-    -> MutTerm v t     -- ^
-    -> StateT (IM.IntMap (MutTerm v t)) (e m) ()
+    => v -- ^
+    -> t (UTerm t v) -- ^
+    -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^
 {-# INLINE seenAs #-}
-seenAs v t = do
+seenAs v0 t0 = do
     seenVars <- get
-    case IM.lookup (getVarID v) seenVars of
-        Just t' -> lift . throwError $ OccursIn v t'
-        Nothing -> put $! IM.insert (getVarID v) t seenVars
+    case IM.lookup (getVarID v0) seenVars of
+        Just t  -> lift . throwError $ OccursIn v0 (UTerm t)
+        Nothing -> put $! IM.insert (getVarID v0) t0 seenVars
 
 ----------------------------------------------------------------
 ----------------------------------------------------------------
@@ -178,18 +185,41 @@
 -- TODO: Figure out how to abstract the left-catamorphism from these.
 
 
--- | Walk a term and determine what variables are still free. N.B.,
+-- | Walk a term and determine which variables are still free. N.B.,
 -- this function does not detect cyclic terms (i.e., throw errors),
 -- but it will return the correct answer for them in finite time.
-getFreeVars :: (BindingMonad v t m) => MutTerm v t -> m [v]
-getFreeVars =
-    \t -> IM.elems <$> evalStateT (loop t) IS.empty
+getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]
+getFreeVars = getFreeVarsAll . Identity
+
+
+-- TODO: Should we return the IntMap instead?
+--
+-- | Same as 'getFreeVars', but works on several terms simultaneously.
+-- This is more efficient than getting the free variables for each
+-- of the terms separately because we can make use of sharing across
+-- the whole collection. That is, each time we move to the next
+-- term, we still remember the bound variables we've already looked
+-- at (and therefore do not need to traverse, since we've already
+-- seen whatever free variables there are down there); whereas we
+-- would forget between each call to @getFreeVars@.
+--
+-- /Since: 0.7.0/
+getFreeVarsAll
+    :: (BindingMonad t v m, Foldable s)
+    => s (UTerm t v) -> m [v]
+getFreeVarsAll ts0 =
+    IM.elems <$> evalStateT (loopAll ts0) IS.empty
     where
+    -- TODO: is that the most efficient direction/associativity?
+    loopAll = foldrM (\t r -> IM.union r <$> loop t) IM.empty
+    
     loop t0 = do
-        t1 <- lift $ semiprune t0
-        case t1 of
-            MutTerm t -> fold <$> mapM loop t -- TODO: use foldlM instead?
-            MutVar  v -> do
+        t0 <- lift $ semiprune t0
+        case t0 of
+            UTerm t -> fold <$> mapM loop t
+                -- TODO: benchmark using the following instead:
+                -- > foldMapM f = foldlM (\a b -> mappend a <$> f b) mempty
+            UVar  v -> do
                 seenVars <- get
                 let i = getVarID v
                 if IS.member i seenVars
@@ -212,21 +242,38 @@
 -- If any cyclic bindings are detected, then an 'OccursIn' exception
 -- will be thrown.
 applyBindings
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
-applyBindings =
-    \t -> evalStateT (loop t) IM.empty
+    => UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
+applyBindings = fmap runIdentity . applyBindingsAll . Identity
+
+
+-- | Same as 'applyBindings', but works on several terms simultaneously.
+-- This function preserves sharing across the entire collection of
+-- terms, whereas applying the bindings to each term separately
+-- would only preserve sharing within each term.
+--
+-- /Since: 0.7.0/
+applyBindingsAll
+    ::  ( BindingMonad t v m
+        , MonadTrans e
+        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
+        , MonadError (UnificationFailure t v) (e m)
+        , Traversable s
+        )
+    => s (UTerm t v)       -- ^
+    -> e m (s (UTerm t v)) -- ^
+applyBindingsAll ts0 = evalStateT (mapM loop ts0) IM.empty
     where
     loop t0 = do
-        t1 <- lift . lift $ semiprune t0
-        case t1 of
-            MutTerm t -> MutTerm <$> mapM loop t
-            MutVar  v -> do
+        t0 <- lift . lift $ semiprune t0
+        case t0 of
+            UTerm t -> UTerm <$> mapM loop t
+            UVar  v -> do
                 let i = getVarID v
                 mb <- IM.lookup i <$> get
                 case mb of
@@ -235,7 +282,7 @@
                     Nothing -> do
                         mb' <- lift . lift $ lookupVar v
                         case mb' of
-                            Nothing -> return t1
+                            Nothing -> return t0
                             Just t  -> do
                                 modify' . IM.insert i $ Left t
                                 t' <- loop t
@@ -251,21 +298,47 @@
 -- If any cyclic bindings are detected, then an 'OccursIn' exception
 -- will be thrown.
 freshen
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
-freshen =
-    \t -> evalStateT (loop t) IM.empty
+    => UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
+freshen = fmap runIdentity . freshenAll . Identity
+
+
+-- | Same as 'freshen', but works on several terms simultaneously.
+-- This is different from freshening each term separately, because
+-- @freshenAll@ preserves the relationship between the terms. For
+-- instance, the result of
+--
+-- > mapM freshen [UVar 1, UVar 1]
+--
+-- would be @[UVar 2, UVar 3]@ or something alpha-equivalent, whereas
+-- the result of
+--
+-- > freshenAll [UVar 1, UVar 1]
+--
+-- would be @[UVar 2, UVar 2]@ or something alpha-equivalent.
+--
+-- /Since: 0.7.0/
+freshenAll
+    ::  ( BindingMonad t v m
+        , MonadTrans e
+        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
+        , MonadError (UnificationFailure t v) (e m)
+        , Traversable s
+        )
+    => s (UTerm t v)       -- ^
+    -> e m (s (UTerm t v)) -- ^
+freshenAll ts0 = evalStateT (mapM loop ts0) IM.empty
     where
     loop t0 = do
-        t1 <- lift . lift $ semiprune t0
-        case t1 of
-            MutTerm t -> MutTerm <$> mapM loop t
-            MutVar  v -> do
+        t0 <- lift . lift $ semiprune t0
+        case t0 of
+            UTerm t -> UTerm <$> mapM loop t
+            UVar  v -> do
                 let i = getVarID v
                 seenVars <- get
                 case IM.lookup i seenVars of
@@ -275,13 +348,13 @@
                         mb <- lift . lift $ lookupVar v
                         case mb of
                             Nothing -> do
-                                v' <- lift . lift $ MutVar <$> freeVar
+                                v' <- lift . lift $ UVar <$> freeVar
                                 put $! IM.insert i (Right v') seenVars
                                 return v'
                             Just t  -> do
                                 put $! IM.insert i (Left t) seenVars
                                 t' <- loop t
-                                v' <- lift . lift $ MutVar <$> newVar t'
+                                v' <- lift . lift $ UVar <$> newVar t'
                                 modify' $ IM.insert i (Right v')
                                 return v'
 
@@ -291,53 +364,66 @@
 
 -- | 'equals'
 (===)
-    :: (BindingMonad v t m)
-    => MutTerm v t  -- ^
-    -> MutTerm v t  -- ^
-    -> m Bool       -- ^
+    :: (BindingMonad t v m)
+    => UTerm t v  -- ^
+    -> UTerm t v  -- ^
+    -> m Bool     -- ^
 (===) = equals
+{-# INLINE (===) #-}
 infix 4 ===, `equals`
 
 
 -- | 'equiv'
 (=~=)
-    :: (BindingMonad v t m)
-    => MutTerm v t               -- ^
-    -> MutTerm v t               -- ^
+    :: (BindingMonad t v m)
+    => UTerm t v                 -- ^
+    -> UTerm t v                 -- ^
     -> m (Maybe (IM.IntMap Int)) -- ^
 (=~=) = equiv
+{-# INLINE (=~=) #-}
 infix 4 =~=, `equiv`
 
 
 -- | 'unify'
 (=:=)
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
+    => UTerm t v       -- ^
+    -> UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
 (=:=) = unify
+{-# INLINE (=:=) #-}
 infix 4 =:=, `unify`
 
 
 -- | 'subsumes'
 (<:=)
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t -- ^
-    -> MutTerm v t -- ^
-    -> e m Bool
+    => UTerm t v -- ^
+    -> UTerm t v -- ^
+    -> e m Bool  -- ^
 (<:=) = subsumes
+{-# INLINE (<:=) #-}
 infix 4 <:=, `subsumes`
 
 ----------------------------------------------------------------
 
+{- BUG:
+If we don't use anything special, then there's a 2x overhead for
+calling 'equals' (and probably the rest of them too). If we add a
+SPECIALIZE pragma, or if we try to use MaybeT instead of MaybeKT
+then that jumps up to 4x overhead. However, if we add an INLINE
+pragma then it gets faster than the same implementation in the
+benchmark file. I've no idea what's going on here...
+-}
+
 -- TODO: should we offer a variant which gives the reason for failure?
 --
 -- | Determine if two terms are structurally equal. This is essentially
@@ -346,39 +432,45 @@
 -- function does not consider alpha-variance, and thus variables
 -- with different names are considered unequal. Cf., 'equiv'.
 equals
-    :: (BindingMonad v t m)
-    => MutTerm v t  -- ^
-    -> MutTerm v t  -- ^
-    -> m Bool       -- ^
-equals =
-    \tl tr -> do
-        mb <- runMaybeKT (loop tl tr)
-        case mb of
-            Nothing -> return False
-            Just () -> return True
+    :: (BindingMonad t v m)
+    => UTerm t v  -- ^
+    -> UTerm t v  -- ^
+    -> m Bool     -- ^
+equals tl0 tr0 = do
+    mb <- runMaybeKT (loop tl0 tr0)
+    case mb of
+        Nothing -> return False
+        Just () -> return True
     where
     loop tl0 tr0 = do
-        tl <- lift $ semiprune tl0
-        tr <- lift $ semiprune tr0
-        case (tl, tr) of
-            (MutVar vl', MutVar vr')
-                | vl' `eqVar` vr' -> return () -- success
-                | otherwise       -> do
-                    mtl <- lift $ lookupVar vl'
-                    mtr <- lift $ lookupVar vr'
+        tl0 <- lift $ semiprune tl0
+        tr0 <- lift $ semiprune tr0
+        case (tl0, tr0) of
+            (UVar vl, UVar vr)
+                | vl == vr  -> return () -- success
+                | otherwise -> do
+                    mtl <- lift $ lookupVar vl
+                    mtr <- lift $ lookupVar vr
                     case (mtl, mtr) of
-                        (Nothing,  Nothing ) -> mzero
-                        (Nothing,  Just _  ) -> mzero
-                        (Just _,   Nothing ) -> mzero
-                        (Just tl', Just tr') -> loop tl' tr' -- TODO: should just jump to match
-            (MutVar  _,   MutTerm _  ) -> mzero
-            (MutTerm _,   MutVar  _  ) -> mzero
-            (MutTerm tl', MutTerm tr') ->
-                case zipMatch tl' tr' of
-                Nothing  -> mzero
-                Just tlr -> mapM_ (uncurry loop) tlr
+                        (Nothing,         Nothing)         -> mzero
+                        (Nothing,         Just _ )         -> mzero
+                        (Just _,          Nothing)         -> mzero
+                        (Just (UTerm tl), Just (UTerm tr)) -> match tl tr
+                        _ -> error _impossible_equals
+            (UVar  _,  UTerm _ ) -> mzero
+            (UTerm _,  UVar  _ ) -> mzero
+            (UTerm tl, UTerm tr) -> match tl tr
+    
+    match tl tr =
+        case zipMatch tl tr of
+        Nothing  -> mzero
+        Just tlr -> mapM_ (uncurry loop) tlr
 
+_impossible_equals :: String
+{-# NOINLINE _impossible_equals #-}
+_impossible_equals = "equals: the impossible happened"
 
+
 -- TODO: is that the most helpful return type?
 --
 -- | Determine if two terms are structurally equivalent; that is,
@@ -386,20 +478,19 @@
 -- mapping from variable IDs of the left term to variable IDs of
 -- the right term, indicating the renaming used.
 equiv
-    :: (BindingMonad v t m)
-    => MutTerm v t               -- ^
-    -> MutTerm v t               -- ^
+    :: (BindingMonad t v m)
+    => UTerm t v                 -- ^
+    -> UTerm t v                 -- ^
     -> m (Maybe (IM.IntMap Int)) -- ^
-equiv =
-    \tl tr -> runMaybeKT (execStateT (loop tl tr) IM.empty)
+equiv tl0 tr0 = runMaybeKT (execStateT (loop tl0 tr0) IM.empty)
     where
     loop tl0 tr0 = do
-        tl <- lift . lift $ fullprune tl0
-        tr <- lift . lift $ fullprune tr0
-        case (tl, tr) of
-            (MutVar vl',  MutVar  vr') -> do
-                let il = getVarID vl'
-                let ir = getVarID vr'
+        tl0 <- lift . lift $ fullprune tl0
+        tr0 <- lift . lift $ fullprune tr0
+        case (tl0, tr0) of
+            (UVar vl,  UVar  vr) -> do
+                let il = getVarID vl
+                let ir = getVarID vr
                 xs <- get
                 case IM.lookup il xs of
                     Just x
@@ -407,10 +498,10 @@
                         | otherwise -> lift mzero
                     Nothing         -> put $! IM.insert il ir xs
             
-            (MutVar _,    MutTerm _  ) -> lift mzero
-            (MutTerm _,   MutVar  _  ) -> lift mzero
-            (MutTerm tl', MutTerm tr') ->
-                case zipMatch tl' tr' of
+            (UVar  _,  UTerm _ ) -> lift mzero
+            (UTerm _,  UVar  _ ) -> lift mzero
+            (UTerm tl, UTerm tr) ->
+                case zipMatch tl tr of
                 Nothing  -> lift mzero
                 Just tlr -> mapM_ (uncurry loop) tlr
 
@@ -425,14 +516,14 @@
 -- it slow, it's asymptotically slow since it can cause the same
 -- subterm to be traversed multiple times.
 unifyOccurs
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
+    => UTerm t v       -- ^
+    -> UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
 unifyOccurs = loop
     where
     {-# INLINE (=:) #-}
@@ -447,61 +538,70 @@
     
     -- TODO: cf todos in 'unify'
     loop tl0 tr0 = do
-        tl <- lift $ semiprune tl0
-        tr <- lift $ semiprune tr0
-        case (tl, tr) of
-            (MutVar vl', MutVar vr')
-                | vl' `eqVar` vr' -> return tr
-                | otherwise       -> do
-                    mtl <- lift $ lookupVar vl'
-                    mtr <- lift $ lookupVar vr'
+        tl0 <- lift $ semiprune tl0
+        tr0 <- lift $ semiprune tr0
+        case (tl0, tr0) of
+            (UVar vl, UVar vr)
+                | vl == vr  -> return tr0
+                | otherwise -> do
+                    mtl <- lift $ lookupVar vl
+                    mtr <- lift $ lookupVar vr
                     case (mtl, mtr) of
-                        (Nothing,  Nothing ) -> do
-                            vl' =: tr
-                            return tr
-                        (Nothing,  Just _  ) -> do
-                            vl' `acyclicBindVar` tr
-                            return tr
-                        (Just _  , Nothing ) -> do
-                            vr' `acyclicBindVar` tl
-                            return tl
-                        (Just tl', Just tr') -> do
-                            t <- loop tl' tr'
-                            vr' =: t
-                            vl' =: tr
-                            return tr
+                        (Nothing, Nothing) -> do
+                            vl =: tr0
+                            return tr0
+                        (Nothing, Just _ ) -> do
+                            vl `acyclicBindVar` tr0
+                            return tr0
+                        (Just _ , Nothing) -> do
+                            vr `acyclicBindVar` tl0
+                            return tl0
+                        (Just (UTerm tl), Just (UTerm tr)) -> do
+                            t <- match tl tr
+                            vr =: t
+                            vl =: tr0
+                            return tr0
+                        _ -> error _impossible_unifyOccurs
             
-            (MutVar vl', MutTerm _) -> do
-                mtl <- lift $ lookupVar vl'
+            (UVar vl, UTerm tr) -> do
+                mtl <- lift $ lookupVar vl
                 case mtl of
                     Nothing  -> do
-                        vl' `acyclicBindVar` tr
-                        return tl
-                    Just tl' -> do
-                        t <- loop tl' tr
-                        vl' =: t
-                        return tl
+                        vl `acyclicBindVar` tr0
+                        return tl0
+                    Just (UTerm tl) -> do
+                        t <- match tl tr
+                        vl =: t
+                        return tl0
+                    _ -> error _impossible_unifyOccurs
             
-            (MutTerm _, MutVar vr') -> do
-                mtr <- lift $ lookupVar vr'
+            (UTerm tl, UVar vr) -> do
+                mtr <- lift $ lookupVar vr
                 case mtr of
                     Nothing  -> do
-                        vr' `acyclicBindVar` tl
-                        return tr
-                    Just tr' -> do
-                        t <- loop tl tr'
-                        vr' =: t
-                        return tr
+                        vr `acyclicBindVar` tl0
+                        return tr0
+                    Just (UTerm tr) -> do
+                        t <- match tl tr
+                        vr =: t
+                        return tr0
+                    _ -> error _impossible_unifyOccurs
             
-            (MutTerm tl', MutTerm tr') ->
-                case zipMatch tl' tr' of
-                Nothing  -> throwError $ TermMismatch tl' tr'
-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr
+            (UTerm tl, UTerm tr) -> match tl tr
+    
+    match tl tr =
+        case zipMatch tl tr of
+        Nothing  -> throwError $ TermMismatch tl tr
+        Just tlr -> UTerm <$> mapM (uncurry loop) tlr
 
+_impossible_unifyOccurs :: String
+{-# NOINLINE _impossible_unifyOccurs #-}
+_impossible_unifyOccurs = "unifyOccurs: the impossible happened"
 
+
 ----------------------------------------------------------------
 -- TODO: verify correctness, especially for the visited-set stuff.
--- TODO: return Maybe(MutTerm v t) in the loop so we can avoid updating bindings trivially
+-- TODO: return Maybe(UTerm t v) in the loop so we can avoid updating bindings trivially
 -- TODO: figure out why unifyOccurs is so much faster on pure ground terms!! The only difference there is in lifting over StateT...
 -- 
 -- | Unify two terms, or throw an error with an explanation of why
@@ -511,70 +611,78 @@
 -- aggressive opportunistic observable sharing, so it will be more
 -- efficient to use it in future calculations than either argument.
 unify
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
-unify =
-    \tl tr -> evalStateT (loop tl tr) IM.empty
+    => UTerm t v       -- ^
+    -> UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
+unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty
     where
     {-# INLINE (=:) #-}
     v =: t = lift . lift $ v `bindVar` t
     
     -- TODO: would it be beneficial to manually fuse @x <- lift m; y <- lift n@ to @(x,y) <- lift (m;n)@ everywhere we can?
     loop tl0 tr0 = do
-        tl <- lift . lift $ semiprune tl0
-        tr <- lift . lift $ semiprune tr0
-        case (tl, tr) of
-            (MutVar vl', MutVar vr')
-                | vl' `eqVar` vr' -> return tr
-                | otherwise       -> do
-                    mtl <- lift . lift $ lookupVar vl'
-                    mtr <- lift . lift $ lookupVar vr'
+        tl0 <- lift . lift $ semiprune tl0
+        tr0 <- lift . lift $ semiprune tr0
+        case (tl0, tr0) of
+            (UVar vl, UVar vr)
+                | vl == vr  -> return tr0
+                | otherwise -> do
+                    mtl <- lift . lift $ lookupVar vl
+                    mtr <- lift . lift $ lookupVar vr
                     case (mtl, mtr) of
-                        (Nothing,  Nothing ) -> do vl' =: tr ; return tr
-                        (Nothing,  Just _  ) -> do vl' =: tr ; return tr
-                        (Just _  , Nothing ) -> do vr' =: tl ; return tl
-                        (Just tl', Just tr') -> do
+                        (Nothing, Nothing) -> do vl =: tr0 ; return tr0
+                        (Nothing, Just _ ) -> do vl =: tr0 ; return tr0
+                        (Just _ , Nothing) -> do vr =: tl0 ; return tl0
+                        (Just (UTerm tl), Just (UTerm tr)) -> do
                             t <- localState $ do
-                                vl' `seenAs` tl'
-                                vr' `seenAs` tr'
-                                loop tl' tr' -- TODO: should just jump to match
-                            vr' =: t
-                            vl' =: tr
-                            return tr
+                                vl `seenAs` tl
+                                vr `seenAs` tr
+                                match tl tr
+                            vr =: t
+                            vl =: tr0
+                            return tr0
+                        _ -> error _impossible_unify
             
-            (MutVar vl', MutTerm _) -> do
+            (UVar vl, UTerm tr) -> do
                 t <- do
-                    mtl <- lift . lift $ lookupVar vl'
+                    mtl <- lift . lift $ lookupVar vl
                     case mtl of
-                        Nothing  -> return tr
-                        Just tl' -> localState $ do
-                            vl' `seenAs` tl'
-                            loop tl' tr -- TODO: should just jump to match
-                vl' =: t
-                return tl
+                        Nothing         -> return tr0
+                        Just (UTerm tl) -> localState $ do
+                            vl `seenAs` tl
+                            match tl tr
+                        _ -> error _impossible_unify
+                vl =: t
+                return tl0
             
-            (MutTerm _, MutVar vr') -> do
+            (UTerm tl, UVar vr) -> do
                 t <- do
-                    mtr <- lift . lift $ lookupVar vr'
+                    mtr <- lift . lift $ lookupVar vr
                     case mtr of
-                        Nothing  -> return tl
-                        Just tr' -> localState $ do
-                            vr' `seenAs` tr'
-                            loop tl tr' -- TODO: should just jump to match
-                vr' =: t
-                return tr
+                        Nothing         -> return tl0
+                        Just (UTerm tr) -> localState $ do
+                            vr `seenAs` tr
+                            match tl tr
+                        _ -> error _impossible_unify
+                vr =: t
+                return tr0
             
-            (MutTerm tl', MutTerm tr') ->
-                case zipMatch tl' tr' of
-                Nothing  -> lift . throwError $ TermMismatch tl' tr'
-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr
+            (UTerm tl, UTerm tr) -> match tl tr
+    
+    match tl tr =
+        case zipMatch tl tr of
+        Nothing  -> lift . throwError $ TermMismatch tl tr
+        Just tlr -> UTerm <$> mapM (uncurry loop) tlr
 
+_impossible_unify :: String
+{-# NOINLINE _impossible_unify #-}
+_impossible_unify = "unify: the impossible happened"
+
 ----------------------------------------------------------------
 -- TODO: can we find an efficient way to return the bindings directly instead of altering the monadic bindings? Maybe another StateT IntMap taking getVarID to the variable and its pseudo-bound term?
 --
@@ -598,55 +706,61 @@
 -- or else requires specifying too much about the implementation
 -- of variables.
 subsumes
-    ::  ( BindingMonad v t m
+    ::  ( BindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t -- ^
-    -> MutTerm v t -- ^
-    -> e m Bool
-subsumes =
-    \tl tr -> evalStateT (loop tl tr) IM.empty
+    => UTerm t v -- ^
+    -> UTerm t v -- ^
+    -> e m Bool  -- ^
+subsumes tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty
     where
     {-# INLINE (=:) #-}
     v =: t = lift . lift $ do v `bindVar` t ; return True
     
     -- TODO: cf todos in 'unify'
     loop tl0 tr0 = do
-        tl <- lift . lift $ semiprune tl0
-        tr <- lift . lift $ semiprune tr0
-        case (tl, tr) of
-            (MutVar vl', MutVar vr')
-                | vl' `eqVar` vr' -> return True
-                | otherwise       -> do
-                    mtl <- lift . lift $ lookupVar vl'
-                    mtr <- lift . lift $ lookupVar vr'
+        tl0 <- lift . lift $ semiprune tl0
+        tr0 <- lift . lift $ semiprune tr0
+        case (tl0, tr0) of
+            (UVar vl, UVar vr)
+                | vl == vr  -> return True
+                | otherwise -> do
+                    mtl <- lift . lift $ lookupVar vl
+                    mtr <- lift . lift $ lookupVar vr
                     case (mtl, mtr) of
-                        (Nothing,  Nothing ) -> vl' =: tr
-                        (Nothing,  Just _  ) -> vl' =: tr
-                        (Just _  , Nothing ) -> return False
-                        (Just tl', Just tr') ->
+                        (Nothing,         Nothing)         -> vl =: tr0
+                        (Nothing,         Just _ )         -> vl =: tr0
+                        (Just _ ,         Nothing)         -> return False
+                        (Just (UTerm tl), Just (UTerm tr)) ->
                             localState $ do
-                                vl' `seenAs` tl'
-                                vr' `seenAs` tr'
-                                loop tl' tr'
+                                vl `seenAs` tl
+                                vr `seenAs` tr
+                                match tl tr
+                        _ -> error _impossible_subsumes
             
-            (MutVar vl',  MutTerm _  ) -> do
-                mtl <- lift . lift $ lookupVar vl'
+            (UVar vl,  UTerm tr) -> do
+                mtl <- lift . lift $ lookupVar vl
                 case mtl of
-                    Nothing  -> vl' =: tr
-                    Just tl' -> localState $ do
-                        vl' `seenAs` tl'
-                        loop tl' tr
+                    Nothing         -> vl =: tr0
+                    Just (UTerm tl) -> localState $ do
+                        vl `seenAs` tl
+                        match tl tr
+                    _ -> error _impossible_subsumes
             
-            (MutTerm _,   MutVar  _  ) -> return False
+            (UTerm _,  UVar  _ ) -> return False
             
-            (MutTerm tl', MutTerm tr') ->
-                case zipMatch tl' tr' of
-                Nothing  -> return False
-                Just tlr -> and <$> mapM (uncurry loop) tlr
+            (UTerm tl, UTerm tr) -> match tl tr
     
+    match tl tr =
+        case zipMatch tl tr of
+        Nothing  -> return False
+        Just tlr -> and <$> mapM (uncurry loop) tlr -- TODO: use foldlM?
+
+_impossible_subsumes :: String
+{-# NOINLINE _impossible_subsumes #-}
+_impossible_subsumes = "subsumes: the impossible happened"
 
 ----------------------------------------------------------------
 ----------------------------------------------------------- fin.
diff --git a/src/Control/Unification/IntVar.hs b/src/Control/Unification/IntVar.hs
--- a/src/Control/Unification/IntVar.hs
+++ b/src/Control/Unification/IntVar.hs
@@ -4,7 +4,7 @@
            #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2012.02.17
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.IntVar
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -57,7 +57,7 @@
 -- N.B., because this implementation is pure, we can use it for
 -- both ranked and unranked monads.
 newtype IntVar = IntVar Int
-    deriving (Show)
+    deriving (Show, Eq)
 
 {-
 -- BUG: This part works, but we'd want to change Show IntBindingState too.
@@ -74,8 +74,6 @@
 -}
 
 instance Variable IntVar where
-    eqVar (IntVar i) (IntVar j) = i == j
-    
     getVarID (IntVar v) = v
 
 
@@ -83,11 +81,11 @@
 -- | Binding state for 'IntVar'.
 data IntBindingState t = IntBindingState
     { nextFreeVar :: {-# UNPACK #-} !Int
-    , varBindings :: IM.IntMap (MutTerm IntVar t)
+    , varBindings :: IM.IntMap (UTerm t IntVar)
     }
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show (t (MutTerm IntVar t))) =>
+instance (Show (t (UTerm t IntVar))) =>
     Show (IntBindingState t)
     where
     show (IntBindingState nr bs) =
@@ -174,7 +172,7 @@
 ----------------------------------------------------------------
 
 instance (Unifiable t, Applicative m, Monad m) =>
-    BindingMonad IntVar t (IntBindingT t m)
+    BindingMonad t IntVar (IntBindingT t m)
     where
     
     lookupVar (IntVar v) = IBT $ gets (IM.lookup v . varBindings)
diff --git a/src/Control/Unification/Ranked.hs b/src/Control/Unification/Ranked.hs
--- a/src/Control/Unification/Ranked.hs
+++ b/src/Control/Unification/Ranked.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
-{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.11
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.Ranked
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -41,6 +41,12 @@
     , unify
     -- unifyOccurs
     -- subsumes
+    
+    -- * Operations on many terms
+    , getFreeVarsAll
+    , applyBindingsAll
+    , freshenAll
+    -- subsumesAll
     ) where
 
 import Prelude
@@ -60,15 +66,16 @@
 
 -- | 'unify'
 (=:=)
-    ::  ( RankedBindingMonad v t m
+    ::  ( RankedBindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
+    => UTerm t v       -- ^
+    -> UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
 (=:=) = unify
+{-# INLINE (=:=) #-}
 infix 4 =:=, `unify`
 
 
@@ -81,16 +88,15 @@
 -- aggressive opportunistic observable sharing, so it will be more
 -- efficient to use it in future calculations than either argument.
 unify
-    ::  ( RankedBindingMonad v t m
+    ::  ( RankedBindingMonad t v m
         , MonadTrans e
         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)
-        , MonadError (UnificationFailure v t) (e m)
+        , MonadError (UnificationFailure t v) (e m)
         )
-    => MutTerm v t       -- ^
-    -> MutTerm v t       -- ^
-    -> e m (MutTerm v t) -- ^
-unify =
-    \tl tr -> evalStateT (loop tl tr) IM.empty
+    => UTerm t v       -- ^
+    -> UTerm t v       -- ^
+    -> e m (UTerm t v) -- ^
+unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty
     where
     -- TODO: use IM.insertWith or the like to do this in one pass
     {-# INLINE seenAs #-}
@@ -104,33 +110,33 @@
     v =: t = bindVar v t >> return t
     
     loop tl0 tr0 = do
-        tl1 <- lift . lift $ semiprune tl0
-        tr1 <- lift . lift $ semiprune tr0
-        case (tl1, tr1) of
-            (MutVar vl, MutVar vr)
-                | vl `eqVar` vr -> return tr1
-                | otherwise     -> do
+        tl0 <- lift . lift $ semiprune tl0
+        tr0 <- lift . lift $ semiprune tr0
+        case (tl0, tr0) of
+            (UVar vl, UVar vr)
+                | vl == vr  -> return tr0
+                | otherwise -> do
                     Rank rl mtl <- lift . lift $ lookupRankVar vl
                     Rank rr mtr <- lift . lift $ lookupRankVar vr
                     let cmp = compare rl rr
                     case (mtl, mtr) of
                         (Nothing, Nothing) -> lift . lift $
                             case cmp of
-                            LT -> do {                    vl =: tr1 }
-                            EQ -> do { incrementRank vr ; vl =: tr1 }
-                            GT -> do {                    vr =: tl1 }
+                            LT -> do {                    vl =: tr0 }
+                            EQ -> do { incrementRank vr ; vl =: tr0 }
+                            GT -> do {                    vr =: tl0 }
                       
                         (Nothing, Just tr) -> lift . lift $
                             case cmp of
-                            LT -> do {                    vl =: tr1 }
-                            EQ -> do { incrementRank vr ; vl =: tr1 }
-                            GT -> do { vl `bindVar` tr  ; vr =: tl1 }
+                            LT -> do {                    vl =: tr0 }
+                            EQ -> do { incrementRank vr ; vl =: tr0 }
+                            GT -> do { vl `bindVar` tr  ; vr =: tl0 }
                         
                         (Just tl, Nothing) -> lift . lift $
                             case cmp of
-                            LT -> do { vr `bindVar` tl  ; vl =: tr1 }
-                            EQ -> do { incrementRank vl ; vr =: tl1 }
-                            GT -> do {                    vr =: tl1 }
+                            LT -> do { vr `bindVar` tl  ; vl =: tr0 }
+                            EQ -> do { incrementRank vl ; vr =: tl0 }
+                            GT -> do {                    vr =: tl0 }
                         
                         (Just tl, Just tr) -> do
                             t <- localState $ do
@@ -139,38 +145,38 @@
                                 loop tl tr
                             lift . lift $
                                 case cmp of
-                                LT -> do { vr `bindVar` t        ; vl =: tr1 }
-                                EQ -> do { incrementBindVar vl t ; vr =: tl1 }
-                                GT -> do { vl `bindVar` t        ; vr =: tl1 }
+                                LT -> do { vr `bindVar` t        ; vl =: tr0 }
+                                EQ -> do { incrementBindVar vl t ; vr =: tl0 }
+                                GT -> do { vl `bindVar` t        ; vr =: tl0 }
             
-            (MutVar vl, MutTerm _) -> do
+            (UVar vl, UTerm _) -> do
                 t <- do
                     mtl <- lift . lift $ lookupVar vl
                     case mtl of
-                        Nothing -> return tr1
+                        Nothing -> return tr0
                         Just tl -> localState $ do
                             vl `seenAs` tl
-                            loop tl tr1
+                            loop tl tr0
                 lift . lift $ do
                     vl `bindVar` t
-                    return tl1
+                    return tl0
             
-            (MutTerm _, MutVar vr) -> do
+            (UTerm _, UVar vr) -> do
                 t <- do
                     mtr <- lift . lift $ lookupVar vr
                     case mtr of
-                        Nothing -> return tl1
+                        Nothing -> return tl0
                         Just tr -> localState $ do
                             vr `seenAs` tr
-                            loop tl1 tr
+                            loop tl0 tr
                 lift . lift $ do
                     vr `bindVar` t
-                    return tr1
+                    return tr0
             
-            (MutTerm tl, MutTerm tr) ->
+            (UTerm tl, UTerm tr) ->
                 case zipMatch tl tr of
                 Nothing  -> lift . throwError $ TermMismatch tl tr
-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr
+                Just tlr -> UTerm <$> mapM (uncurry loop) tlr
 
 ----------------------------------------------------------------
 ----------------------------------------------------------- fin.
diff --git a/src/Control/Unification/Ranked/IntVar.hs b/src/Control/Unification/Ranked/IntVar.hs
--- a/src/Control/Unification/Ranked/IntVar.hs
+++ b/src/Control/Unification/Ranked/IntVar.hs
@@ -4,7 +4,7 @@
            #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.06
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.Ranked.IntVar
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -40,11 +40,11 @@
 -- | Ranked binding state for 'IntVar'.
 data IntRBindingState t = IntRBindingState
     { nextFreeVar :: {-# UNPACK #-} !Int
-    , varBindings :: IM.IntMap (Rank IntVar t)
+    , varBindings :: IM.IntMap (Rank t IntVar)
     }
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show (t (MutTerm IntVar t))) =>
+instance (Show (t (UTerm t IntVar))) =>
     Show (IntRBindingState t)
     where
     show (IntRBindingState nr bs) =
@@ -131,7 +131,7 @@
 ----------------------------------------------------------------
 
 instance (Unifiable t, Applicative m, Monad m) =>
-    BindingMonad IntVar t (IntRBindingT t m)
+    BindingMonad t IntVar (IntRBindingT t m)
     where
     
     lookupVar (IntVar v) = IRBT $ do
@@ -167,7 +167,7 @@
     
     
 instance (Unifiable t, Applicative m, Monad m) =>
-    RankedBindingMonad IntVar t (IntRBindingT t m)
+    RankedBindingMonad t IntVar (IntRBindingT t m)
     where
     lookupRankVar (IntVar v) = IRBT $ do
         mb <- gets (IM.lookup v . varBindings)
diff --git a/src/Control/Unification/Ranked/STVar.hs b/src/Control/Unification/Ranked/STVar.hs
--- a/src/Control/Unification/Ranked/STVar.hs
+++ b/src/Control/Unification/Ranked/STVar.hs
@@ -5,7 +5,7 @@
            #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2012.02.17
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.Ranked.STVar
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -43,19 +43,20 @@
     STRVar
         {-# UNPACK #-} !Int
         {-# UNPACK #-} !(STRef s Word8)
-        {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STRVar s t) t)))
+        {-# UNPACK #-} !(STRef s (Maybe (UTerm t (STRVar s t))))
 
 instance Show (STRVar s t) where
     show (STRVar i _ _) = "STRVar " ++ show i
 
-instance Variable (STRVar s t) where
-    eqVar (STRVar i _ _) (STRVar j _ _) = i == j
+instance Eq (STRVar s t) where
+    (STRVar i _ _) == (STRVar j _ _) = (i == j)
     
-    getVarID  (STRVar i _ _) = i
+instance Variable (STRVar s t) where
+    getVarID (STRVar i _ _) = i
 
 
 ----------------------------------------------------------------
--- TODO: parameterize this so we can use BacktrackST too. Or course,
+-- TODO: parameterize this so we can use BacktrackST too. Of course,
 -- that means defining another class for STRef-like variables
 --
 -- TODO: parameterize this so we can share the implementation for STVar and STRVar
@@ -97,7 +98,7 @@
 
 _newSTRVar
     :: String
-    -> Maybe (MutTerm (STRVar s t) t)
+    -> Maybe (UTerm t (STRVar s t))
     -> STRBinding s (STRVar s t)
 _newSTRVar fun mb = STRB $ do
     nr <- ask
@@ -113,7 +114,7 @@
                 return (STRVar n rk ptr)
 
 
-instance (Unifiable t) => BindingMonad (STRVar s t) t (STRBinding s) where
+instance (Unifiable t) => BindingMonad t (STRVar s t) (STRBinding s) where
     lookupVar (STRVar _ _ p) = STRB . lift $ readSTRef p
     
     freeVar  = _newSTRVar "freeVar" Nothing
@@ -124,7 +125,7 @@
 
 
 instance (Unifiable t) =>
-    RankedBindingMonad (STRVar s t) t (STRBinding s)
+    RankedBindingMonad t (STRVar s t) (STRBinding s)
     where
     
     lookupRankVar (STRVar _ r p) = STRB . lift $ do
diff --git a/src/Control/Unification/STVar.hs b/src/Control/Unification/STVar.hs
--- a/src/Control/Unification/STVar.hs
+++ b/src/Control/Unification/STVar.hs
@@ -5,7 +5,7 @@
            #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2012.02.17
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.STVar
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -41,15 +41,16 @@
 data STVar s t =
     STVar
         {-# UNPACK #-} !Int
-        {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STVar s t) t)))
+        {-# UNPACK #-} !(STRef s (Maybe (UTerm t (STVar s t))))
 
 instance Show (STVar s t) where
     show (STVar i _) = "STVar " ++ show i
 
+instance Eq (STVar s t) where
+    (STVar i _) == (STVar j _) = (i == j)
+
 instance Variable (STVar s t) where
-    eqVar (STVar i _) (STVar j _) = i == j
-    
-    getVarID  (STVar i _) = i
+    getVarID (STVar i _) = i
 
 
 ----------------------------------------------------------------
@@ -96,7 +97,7 @@
 
 _newSTVar
     :: String
-    -> Maybe (MutTerm (STVar s t) t)
+    -> Maybe (UTerm t (STVar s t))
     -> STBinding s (STVar s t)
 _newSTVar fun mb = STB $ do
     nr <- ask
@@ -109,7 +110,7 @@
                 STVar n <$> newSTRef mb
 
 instance (Unifiable t) =>
-    BindingMonad (STVar s t) t (STBinding s)
+    BindingMonad t (STVar s t) (STBinding s)
     where
 
     lookupVar (STVar _ p) = STB . lift $ readSTRef p
diff --git a/src/Control/Unification/Types.hs b/src/Control/Unification/Types.hs
--- a/src/Control/Unification/Types.hs
+++ b/src/Control/Unification/Types.hs
@@ -5,7 +5,7 @@
 
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2012.02.17
+--                                                  ~ 2012.03.18
 -- |
 -- Module      :  Control.Unification.Types
 -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
@@ -19,8 +19,8 @@
 ----------------------------------------------------------------
 module Control.Unification.Types
     (
-    -- * Mutable terms
-      MutTerm(..)
+    -- * Unification terms
+      UTerm(..)
     , freeze
     , unfreeze
     -- * Errors
@@ -38,40 +38,94 @@
 
 import Data.Word               (Word8)
 import Data.Functor.Fixedpoint (Fix(..))
+import Data.Foldable           (Foldable(..))
 import Data.Traversable        (Traversable(..))
-import Control.Applicative     (Applicative(..), (<$>))
+import Control.Applicative     (Applicative(..), (<$>), Alternative(..))
+import Control.Monad           (MonadPlus(..))
 import Control.Monad.Error     (Error(..))
 ----------------------------------------------------------------
 ----------------------------------------------------------------
 
+-- TODO: incorporate Ed's cheaper free monads, at least as a view.
+
 -- | The type of terms generated by structures @t@ over variables
 -- @v@. The structure type should implement 'Unifiable' and the
--- variable type should implement 'Variable'. The 'Show' instance
--- doesn't show the constructors, for legibility.
-data MutTerm v t
-    = MutVar  !v
-    | MutTerm !(t (MutTerm v t))
+-- variable type should implement 'Variable'.
+--
+-- The 'Show' instance doesn't show the constructors, in order to
+-- improve legibility for large terms.
+--
+-- All the category theoretic instances ('Functor', 'Foldable',
+-- 'Traversable',...) are provided because they are often useful;
+-- however, beware that since the implementations must be pure,
+-- they cannot read variables bound in the current context and
+-- therefore can create incoherent results. Therefore, you should
+-- apply the current bindings before using any of the functions
+-- provided by those classes.
 
+data UTerm t v
+    = UVar  !v               -- ^ A unification variable.
+    | UTerm !(t (UTerm t v)) -- ^ Some structure containing subterms.
 
-instance (Show v, Show (t (MutTerm v t))) =>
-    Show (MutTerm v t)
-    where
-    showsPrec p (MutVar  v) = showsPrec p v
-    showsPrec p (MutTerm t) = showsPrec p t
+instance (Show v, Show (t (UTerm t v))) => Show (UTerm t v) where
+    showsPrec p (UVar  v) = showsPrec p v
+    showsPrec p (UTerm t) = showsPrec p t
 
+instance (Functor t) => Functor (UTerm t) where
+    fmap f (UVar  v) = UVar  (f v)
+    fmap f (UTerm t) = UTerm (fmap (fmap f) t)
 
+instance (Foldable t) => Foldable (UTerm t) where
+    foldMap f (UVar  v) = f v
+    foldMap f (UTerm t) = foldMap (foldMap f) t
+
+instance (Traversable t) => Traversable (UTerm t) where
+    traverse f (UVar  v) = UVar  <$> f v
+    traverse f (UTerm t) = UTerm <$> traverse (traverse f) t
+
+-- Does this even make sense for UTerm? It'd mean (a->b) is a
+-- variable type...
+instance (Functor t) => Applicative (UTerm t) where
+    pure                  = UVar
+    UVar  a  <*> UVar  b  = UVar  (a b)
+    UVar  a  <*> UTerm mb = UTerm (fmap a  <$> mb)
+    UTerm ma <*> b        = UTerm ((<*> b) <$> ma)
+
+-- Does this even make sense for UTerm? It may be helpful for
+-- building terms at least; though bind is inefficient for that.
+-- Should use the cheaper free...
+instance (Functor t) => Monad (UTerm t) where
+    return        = UVar
+    UVar  v >>= f = f v
+    UTerm t >>= f = UTerm ((>>= f) <$> t)
+
+-- This really doesn't make sense for UTerm...
+instance (Alternative t) => Alternative (UTerm t) where
+    empty   = UTerm empty
+    a <|> b = UTerm (pure a <|> pure b)
+
+-- This really doesn't make sense for UTerm...
+instance (Functor t, MonadPlus t) => MonadPlus (UTerm t) where
+    mzero       = UTerm mzero
+    a `mplus` b = UTerm (return a `mplus` return b)
+
+-- There's also MonadTrans, MonadWriter, MonadReader, MonadState,
+-- MonadError, MonadCont; which make even less sense for us. See
+-- Ed Kmett's free package for the implementations.
+
+
 -- | /O(n)/. Embed a pure term as a mutable term.
-unfreeze :: (Functor t) => Fix t -> MutTerm v t
-unfreeze = MutTerm . fmap unfreeze . unFix
+unfreeze :: (Functor t) => Fix t -> UTerm t v
+unfreeze = UTerm . fmap unfreeze . unFix
 
 
 -- | /O(n)/. Extract a pure term from a mutable term, or return
 -- @Nothing@ if the mutable term actually contains variables. N.B.,
 -- this function is pure, so you should manually apply bindings
 -- before calling it.
-freeze :: (Traversable t) => MutTerm v t -> Maybe (Fix t)
-freeze (MutVar  _) = Nothing
-freeze (MutTerm t) = Fix <$> mapM freeze t
+freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)
+freeze (UVar  _) = Nothing
+freeze (UTerm t) = Fix <$> mapM freeze t
 
 
 ----------------------------------------------------------------
@@ -82,9 +136,9 @@
 -- could be given more accurate types if we used ad-hoc combinations
 -- of these constructors (i.e., because they can only throw one of
 -- the errors), the extra complexity is not considered worth it.
-data UnificationFailure v t
+data UnificationFailure t v
     
-    = OccursIn v (MutTerm v t)
+    = OccursIn v (UTerm t v)
         -- ^ A cyclic term was encountered (i.e., the variable
         -- occurs free in a term it would have to be bound to in
         -- order to succeed). Infinite terms like this are not
@@ -102,7 +156,7 @@
         -- we had performed the occurs-check, in order for error
         -- messages to be intelligable.
     
-    | TermMismatch (t (MutTerm v t)) (t (MutTerm v t))
+    | TermMismatch (t (UTerm t v)) (t (UTerm t v))
         -- ^ The top-most level of the terms do not match (according
         -- to 'zipMatch'). In logic programming this should simply
         -- be treated as unification failure; in type checking this
@@ -110,21 +164,36 @@
         -- with inferred type @Bar@\" error.
     
     | UnknownError String
-        -- ^ Required for the @Error@ instance, which in turn is
+        -- ^ Required for the 'Error' instance, which in turn is
         -- required to appease @ErrorT@ in the MTL. We do not use
         -- this anywhere.
 
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show (t (MutTerm v t)), Show v) =>
-    Show (UnificationFailure v t)
+instance (Show (t (UTerm t v)), Show v) =>
+    Show (UnificationFailure t v)
     where
-    -- TODO: implement 'showsPrec' instead
-    show (OccursIn     v  t)  = "OccursIn ("++show v++") ("++show t++")"
-    show (TermMismatch tl tr) = "TermMismatch ("++show tl++") ("++show tr++")"
-    show (UnknownError msg)   = "UnknownError: "++msg
+    showsPrec p (OccursIn v t) =
+        showParen (p > 9)
+            ( showString "OccursIn "
+            . showsPrec 11 v
+            . showString " "
+            . showsPrec 11 t
+            )
+    showsPrec p (TermMismatch tl tr) =
+        showParen (p > 9)
+            ( showString "TermMismatch "
+            . showsPrec 11 tl
+            . showString " "
+            . showsPrec 11 tr
+            )
+    showsPrec p (UnknownError msg) =
+        showParen (p > 9)
+            ( showString "UnknownError: "
+            . showString msg
+            )
 
-instance Error (UnificationFailure v t) where
+instance Error (UnificationFailure t v) where
     noMsg  = UnknownError ""
     strMsg = UnknownError
 
@@ -143,19 +212,19 @@
     zipMatch :: t a -> t b -> Maybe (t (a,b))
 
 
--- | An implementation of unification variables.
-class Variable v where
-    
-    -- | Determine whether two variables are equal /as variables/,
-    -- without considering what they are bound to. The default
-    -- implementation is:
-    --
-    -- > eqVar x y = getVarID x == getVarID y
-    eqVar :: v -> v -> Bool
-    eqVar x y = getVarID x == getVarID y
+-- | An implementation of unification variables. The 'Eq' requirement
+-- is to determine whether two variables are equal /as variables/,
+-- without considering what they are bound to. We use 'Eq' rather
+-- than having our own @eqVar@ method so that clients can make use
+-- of library functions which commonly assume 'Eq'.
+class (Eq v) => Variable v where
     
     -- | Return a unique identifier for this variable, in order to
     -- support the use of visited-sets instead of occurs-checks.
+    -- This function must satisfy the following coherence law with
+    -- respect to the 'Eq' instance:
+    --
+    -- @x == y@ if and only if @getVarID x == getVarID y@
     getVarID :: v -> Int
 
 
@@ -172,12 +241,12 @@
 -- we make the same assumptions everywhere we use @BindingMonad@.
 
 class (Unifiable t, Variable v, Applicative m, Monad m) =>
-    BindingMonad v t m | m -> v t
+    BindingMonad t v m | m -> t v
     where
     
-    -- | Given a variable pointing to @MutTerm v t@, return the
+    -- | Given a variable pointing to @UTerm t v@, return the
     -- term it's bound to, or @Nothing@ if the variable is unbound.
-    lookupVar :: v -> m (Maybe (MutTerm v t))
+    lookupVar :: v -> m (Maybe (UTerm t v))
     
     
     -- | Generate a new free variable guaranteed to be fresh in
@@ -189,12 +258,12 @@
     -- term. The default implementation is:
     --
     -- > newVar t = do { v <- freeVar ; bindVar v t ; return v }
-    newVar :: MutTerm v t -> m v
+    newVar :: UTerm t v -> m v
     newVar t = do { v <- freeVar ; bindVar v t ; return v }
     
     
     -- | Bind a variable to a term, overriding any previous binding.
-    bindVar :: v -> MutTerm v t -> m ()
+    bindVar :: v -> UTerm t v -> m ()
 
 
 ----------------------------------------------------------------
@@ -208,19 +277,17 @@
 -- of variables in the unification problem. Thus, A @Word8@ is
 -- sufficient for @2^(2^8)@ variables, which is far more than can
 -- be indexed by 'getVarID' even on 64-bit architectures.
-data Rank v t =
-    Rank {-# UNPACK #-} !Word8 !(Maybe (MutTerm v t))
+data Rank t v =
+    Rank {-# UNPACK #-} !Word8 !(Maybe (UTerm t v))
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show v, Show (t (MutTerm v t))) =>
-    Show (Rank v t)
-    where
+instance (Show v, Show (t (UTerm t v))) => Show (Rank t v) where
     show (Rank n mb) = "Rank "++show n++" "++show mb
 
--- TODO: flatten the Rank.Maybe.MutTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)?
+-- TODO: flatten the Rank.Maybe.UTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)?
 
 {-
-instance Monoid (Rank v t) where
+instance Monoid (Rank t v) where
     mempty = Rank 0 Nothing
     mappend (Rank l mb) (Rank r _) = Rank (max l r) mb
 -}
@@ -232,11 +299,11 @@
 -- compression is asymptotically optimal, the constant factors may
 -- make it worthwhile to stick with the unweighted path compression
 -- supported by 'BindingMonad'.
-
-class (BindingMonad v t m) => RankedBindingMonad v t m | m -> v t where
-    -- | Given a variable pointing to @MutTerm v t@, return its
+class (BindingMonad t v m) => RankedBindingMonad t v m | m -> t v where
+    
+    -- | Given a variable pointing to @UTerm t v@, return its
     -- rank and the term it's bound to.
-    lookupRankVar :: v -> m (Rank v t)
+    lookupRankVar :: v -> m (Rank t v)
     
     -- | Increase the rank of a variable by one.
     incrementRank :: v -> m ()
@@ -244,8 +311,8 @@
     -- | Bind a variable to a term and increment the rank at the
     -- same time. The default implementation is:
     --
-    -- > incrementBindVar v t = do { incrementRank v ; bindVar v t }
-    incrementBindVar :: v -> MutTerm v t -> m ()
+    -- > incrementBindVar t v = do { incrementRank v ; bindVar v t }
+    incrementBindVar :: v -> UTerm t v -> m ()
     incrementBindVar v t = do { incrementRank v ; bindVar v t }
 
 ----------------------------------------------------------------
diff --git a/unification-fd.cabal b/unification-fd.cabal
--- a/unification-fd.cabal
+++ b/unification-fd.cabal
@@ -1,5 +1,5 @@
 ----------------------------------------------------------------
--- wren ng thornton <wren@community.haskell.org>    ~ 2012.02.17
+-- wren ng thornton <wren@community.haskell.org>    ~ 2012.03.11
 ----------------------------------------------------------------
 
 -- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with:
@@ -8,7 +8,7 @@
 Build-Type:     Simple
 
 Name:           unification-fd
-Version:        0.6.0
+Version:        0.7.0
 Stability:      experimental
 Homepage:       http://code.haskell.org/~wren/
 Author:         wren ng thornton