diff --git a/AUTHORS b/AUTHORS
new file mode 100644
--- /dev/null
+++ b/AUTHORS
@@ -0,0 +1,44 @@
+=== Haskell unification-fd package AUTHORS/THANKS file ===
+
+The unification-fd package was written by wren ng thornton and is
+released under the terms in the LICENSE file.
+
+
+=== Thanks ===
+
+Christopher Anand --- for partially funding this work at McMaster
+    University during the summer of 2011.
+
+Nathaniel W. Filardo --- for helping to figure out the intricacies
+    of unification in Dyna2 (though this code is at best loosely
+    based on that work).
+
+Edward Kmett --- for pointing out the weighted extension to path
+    compression (popular in the union--find literature), and for
+    suggsting the switch to having variables be of kind * rather
+    than *->*
+
+
+=== Related Work ===
+
+The two-level types approach was adapted from Tim Sheard[1]. The
+initial (simple yet naive) implementation of unification was based
+on Sheard's presentation of Cardelli's[2] algorithm in Modula-2.
+Efficient backtracking search via the logict library is described
+by Kiselyov et al.[3] The idea of functional pointers were independently
+discovered by Dijkstra et al.[4] after their apperance in Dyna2.
+
+
+[1] Tim Sheard (2001) /Generic Unification via Two-Level Types and/
+        /Parameterized Modules/, Functional Pearl, ICFP.
+
+[2] Luca Cardelli (1987) /Basic polymorphic typechecking/. Science
+        of Computer Programming, 8(2):147--172.
+
+[3] Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr
+        Sabry (2005) /Backtracking, Interleaving, and Terminating/
+        /Monad Transformers/, ICFP.
+
+[4] Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)
+        /Efficient Functional Unification and Substitution/, Technical
+        Report UU-CS-2008-027, Utrecht University.
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -10,7 +10,7 @@
 
 === unification-fd license ===
 
-Copyright (c) 2007, 2008, 2011, wren ng thornton.
+Copyright (c) 2007, 2008, 2011, 2012, wren ng thornton.
 ALL RIGHTS RESERVED.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,55 @@
+unification-fd
+==============
+
+This is a simple package and should be easy to install. You should
+be able to use one of the following standard methods to install it.
+
+    -- With cabal-install and without the source:
+    $> cabal install unification-fd
+    
+    -- With cabal-install and with the source already:
+    $> cd unification-fd
+    $> cabal install
+    
+    -- Without cabal-install, but with the source already:
+    $> cd unification-fd
+    $> runhaskell Setup.hs configure --user
+    $> runhaskell Setup.hs build
+    $> runhaskell Setup.hs test
+    $> runhaskell Setup.hs haddock --hyperlink-source
+    $> runhaskell Setup.hs install
+
+The test step is optional and currently does nothing. If you see
+some stray lines that look like this:
+
+    mkUsageInfo: internal name? t{tv a7XM}
+
+Feel free to ignore them. They shouldn't cause any problems, even
+though they're unsightly. This should be fixed in newer versions
+of GHC. For more details, see:
+
+    http://hackage.haskell.org/trac/ghc/ticket/3955
+
+If you get a bunch of type errors about there being no MonadLogic
+instance for StateT, this means that your copy of the logict library
+is not compiled against the same mtl that we're using. To fix this,
+update logict to use the same mtl.
+
+
+Portability
+===========
+
+An attempt has been made to keep this library as portable as possible,
+but it does rely on some common language extensions (i.e., ones
+implemented by Hugs as well as GHC) as well as a couple which are
+only known to be supported by GHC. All required language extensions
+are:
+
+    Rank2Types
+    MultiParamTypeClasses
+    FunctionalDependencies -- Alas, necessary for type inference
+    FlexibleContexts       -- Generally necessary for practical use of MPTCs
+    FlexibleInstances      -- Generally necessary for practical use of MPTCs
+    UndecidableInstances   -- Needed for Show instances due to two-level types
+
+----------------------------------------------------------- fin.
diff --git a/VERSION b/VERSION
new file mode 100644
--- /dev/null
+++ b/VERSION
@@ -0,0 +1,16 @@
+0.6.0 (2012-02-17):
+    - Removed the phantom type argument for Variables.
+0.5.0 (2011-07-12):
+    - Moved UnificationFailure to Control.Unification.Types
+    - Renamed NonUnifiable to TermMismatch
+    - Control.Unification: exposed fullprune, semiprune, occursIn
+    - Control.Unification: added unifyOccurs, subsumes
+    - Control.Unification: (re)added symbolic names for binary operators
+0.4.0 (2011-07-07):
+    - Removed heterogeneous unification, and rewrote practically everything.
+    - Added semipruning instead of full pruning.
+    - Added visited-sets instead of occurs-checks.
+    - Added weightedness to path compression (a la union--find).
+    - This is the version emailed for the 2011-07-07 talk at McMaster.
+0.3.6 (2011-06-18):
+    - Forked from the Dyna2 project.
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
@@ -1,4 +1,3 @@
-
 -- The MPTCs and FlexibleInstances are only for
 -- mtl:Control.Monad.Error.MonadError
 {-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-}
@@ -68,41 +67,41 @@
 
 -- | Execute an @EitherK@ and return the concrete @Either@ encoding.
 runEitherK :: EitherK e a -> Either e a
-runEitherK (EK m) = m Right
 {-# INLINE runEitherK #-}
+runEitherK (EK m) = m Right
 
 
 -- | Lift an @Either@ into an @EitherK@.
 toEitherK :: Either e a -> EitherK e a
+{-# INLINE toEitherK #-}
 toEitherK (Left  e) = throwEitherK e
 toEitherK (Right a) = return a
-{-# INLINE toEitherK #-}
 
 
 -- | Throw an error in the @EitherK@ monad. This is identical to
 -- 'throwError'.
 throwEitherK :: e -> EitherK e a
-throwEitherK e = EK (\_ -> Left e)
 {-# INLINE throwEitherK #-}
+throwEitherK e = EK (\_ -> Left e)
 
 
 -- | Handle errors in the @EitherK@ monad. N.B., this type is more
 -- general than that of 'catchError', allowing the type of the
 -- errors to change.
 catchEitherK :: EitherK e a -> (e -> EitherK f a) -> EitherK f a
-catchEitherK m handler = eitherK handler return m
 {-# INLINE catchEitherK #-}
+catchEitherK m handler = eitherK handler return m
 
 
 -- | A version of 'either' on @EitherK@, for convenience. N.B.,
 -- using this function inserts a case match, reducing the range of
 -- short-circuiting.
 eitherK :: (e -> b) -> (a -> b) -> EitherK e a -> b
+{-# INLINE eitherK #-}
 eitherK left right m =
     case runEitherK m of
         Left  e -> left  e
         Right a -> right a
-{-# INLINE eitherK #-}
 
 
 instance Functor (EitherK e) where
@@ -142,36 +141,36 @@
 
 -- | Execute an @EitherKT@ and return the concrete @Either@ encoding.
 runEitherKT :: (Monad m) => EitherKT e m a -> m (Either e a)
-runEitherKT (EKT m) = m (return . Right)
 {-# INLINE runEitherKT #-}
+runEitherKT (EKT m) = m (return . Right)
 
 
 -- | Lift an @Either@ into an @EitherKT@.
 toEitherKT :: (Monad m) => Either e a -> EitherKT e m a
+{-# INLINE toEitherKT #-}
 toEitherKT (Left  e) = throwEitherKT e
 toEitherKT (Right a) = return a
-{-# INLINE toEitherKT #-}
 
 
 -- 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
-liftEitherK = toEitherKT . runEitherK
 {-# INLINE liftEitherK #-}
+liftEitherK = toEitherKT . runEitherK
 
 
 -- TODO: is there a better implementation?
 -- | Lower an @EitherKT@ into an @EitherK@.
 lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a)
-lowerEitherK = liftM toEitherK . runEitherKT
 {-# INLINE lowerEitherK #-}
+lowerEitherK = liftM toEitherK . runEitherKT
 
 
 -- | Throw an error in the @EitherKT@ monad. This is identical to
 -- 'throwError'.
 throwEitherKT :: (Monad m) => e -> EitherKT e m a
-throwEitherKT e = EKT (\_ -> return (Left e))
 {-# INLINE throwEitherKT #-}
+throwEitherKT e = EKT (\_ -> return (Left e))
 
 
 -- | Handle errors in the @EitherKT@ monad. N.B., this type is more
@@ -180,12 +179,12 @@
 catchEitherKT
     :: (Monad m)
     => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a
+{-# INLINE catchEitherKT #-}
 catchEitherKT m handler = EKT $ \k -> do
     ea <- runEitherKT m
     case ea of
         Left  e -> case handler e of EKT m' -> m' k
         Right a -> k a
-{-# INLINE catchEitherKT #-}
 
 
 instance Functor (EitherKT e m) where
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
@@ -59,15 +59,15 @@
 
 -- | Execute the @MaybeK@ and return the concrete @Maybe@ encoding.
 runMaybeK :: MaybeK a -> Maybe a
-runMaybeK (MK m) = m return
 {-# INLINE runMaybeK #-}
+runMaybeK (MK m) = m return
 
 
 -- | Lift a @Maybe@ into @MaybeK@.
 toMaybeK :: Maybe a -> MaybeK a
+{-# INLINE toMaybeK #-}
 toMaybeK Nothing  = mzero
 toMaybeK (Just a) = return a
-{-# INLINE toMaybeK #-}
 
 
 -- | A version of 'maybe' for convenience. This is almost identical
@@ -75,11 +75,11 @@
 -- as well as handling @Nothing@ errors. If you only want to handle
 -- the errors, use 'mplus' instead.
 maybeK :: b -> (a -> b) -> MaybeK a -> b
+{-# INLINE maybeK #-}
 maybeK nothing just m =
     case runMaybeK m of
     Nothing -> nothing
     Just a  -> just a
-{-# INLINE maybeK #-}
 
 
 instance Functor MaybeK where
@@ -116,29 +116,29 @@
 
 -- | Execute a @MaybeKT@ and return the concrete @Maybe@ encoding.
 runMaybeKT :: (Monad m) => MaybeKT m a -> m (Maybe a)
-runMaybeKT (MKT m) = m (return . Just)
 {-# INLINE runMaybeKT #-}
+runMaybeKT (MKT m) = m (return . Just)
 
 
 -- | Lift a @Maybe@ into an @MaybeKT@.
 toMaybeKT :: (Monad m) => Maybe a -> MaybeKT m a
+{-# INLINE toMaybeKT #-}
 toMaybeKT Nothing  = mzero
 toMaybeKT (Just a) = return a
-{-# INLINE toMaybeKT #-}
 
 
 -- 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
-liftMaybeK = toMaybeKT . runMaybeK
 {-# INLINE liftMaybeK #-}
+liftMaybeK = toMaybeKT . runMaybeK
 
 
 -- TODO: is there a better implementation?
 -- | Lower an @MaybeKT@ into an @MaybeK@.
 lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a)
-lowerMaybeK = liftM toMaybeK . runMaybeKT
 {-# INLINE lowerMaybeK #-}
+lowerMaybeK = liftM toMaybeK . runMaybeKT
 
 
 instance Functor (MaybeKT m) where
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
@@ -1,11 +1,10 @@
-
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
 --                                                  ~ 2011.07.05
 -- |
 -- Module      :  Control.Monad.State.UnificationExtras
--- Copyright   :  Copyright (c) 2008--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2008--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  perpetually unstable
@@ -47,20 +46,20 @@
 
 -- | A strict version of 'modify'.
 modify' :: (MonadState s m) => (s -> s) -> m ()
+{-# INLINE modify' #-}
 modify' f = do
     s <- get
     put $! f s
-{-# INLINE modify' #-}
 
 
 -- | Run a state action and undo the state changes at the end.
 localState :: (MonadState s m) => m a -> m a
+{-# INLINE localState #-}
 localState m = do
     s <- get
     x <- m
     put s
     return x
-{-# INLINE localState #-}
 
 ----------------------------------------------------------------
 ----------------------------------------------------------- fin.
diff --git a/src/Control/Unification.hs b/src/Control/Unification.hs
--- a/src/Control/Unification.hs
+++ b/src/Control/Unification.hs
@@ -1,11 +1,10 @@
-
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.11
+--                                                  ~ 2012.02.17
 -- |
 -- Module      :  Control.Unification
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  experimental
@@ -87,7 +86,7 @@
 ----------------------------------------------------------------
 ----------------------------------------------------------------
 
--- BUG: this assumes there are no directly-cyclic chains!
+-- N.B., this assumes there are no directly-cyclic chains!
 --
 -- | Canonicalize a chain of variables so they all point directly
 -- to the term at the end of the chain (or the free variable, if
@@ -108,7 +107,7 @@
                 return finalTerm
 
 
--- BUG: this assumes there are no directly-cyclic chains!
+-- N.B., this assumes there are no directly-cyclic chains!
 --
 -- | Canonicalize a chain of variables so they all point directly
 -- to the last variable in the chain, regardless of whether it is
@@ -140,7 +139,7 @@
 -- 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) -> MutTerm v t -> m Bool
+occursIn :: (BindingMonad v t m) => v -> MutTerm v t -> m Bool
 occursIn v t0 = do
     t <- fullprune t0
     case t of
@@ -157,15 +156,15 @@
         , MonadTrans e
         , MonadError (UnificationFailure v t) (e m)
         )
-    => v (MutTerm v t) -- ^
+    => v               -- ^
     -> MutTerm v t     -- ^
     -> StateT (IM.IntMap (MutTerm v t)) (e m) ()
+{-# INLINE seenAs #-}
 seenAs v t = 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
-{-# INLINE seenAs #-}
 
 ----------------------------------------------------------------
 ----------------------------------------------------------------
@@ -182,7 +181,7 @@
 -- | Walk a term and determine what 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 (MutTerm v t)]
+getFreeVars :: (BindingMonad v t m) => MutTerm v t -> m [v]
 getFreeVars =
     \t -> IM.elems <$> evalStateT (loop t) IS.empty
     where
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
@@ -1,11 +1,13 @@
-
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses
+           , FlexibleInstances
+           , UndecidableInstances
+           #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.06
+--                                                  ~ 2012.02.17
 -- |
 -- Module      :  Control.Unification.IntVar
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  experimental
@@ -54,13 +56,13 @@
 --
 -- N.B., because this implementation is pure, we can use it for
 -- both ranked and unranked monads.
-newtype IntVar t = IntVar Int
+newtype IntVar = IntVar Int
     deriving (Show)
 
 {-
 -- BUG: This part works, but we'd want to change Show IntBindingState too.
 
-instance Show (IntVar t) where
+instance Show IntVar where
     show (IntVar i) = "IntVar " ++ show (boundedInt2Word i)
 
 -- | Convert an integer to a word, via the continuous mapping that
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,11 +1,10 @@
-
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
 --                                                  ~ 2011.07.11
 -- |
 -- Module      :  Control.Unification.Ranked
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  highly experimental
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
@@ -1,11 +1,13 @@
-
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses
+           , FlexibleInstances
+           , UndecidableInstances
+           #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
 --                                                  ~ 2011.07.06
 -- |
 -- Module      :  Control.Unification.Ranked.IntVar
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  highly experimental
@@ -66,7 +68,7 @@
 instance (Functor m) => Functor (IntRBindingT t m) where
     fmap f = IRBT . fmap f . unIRBT
 
--- BUG: can't reduce dependency to Applicative because of StateT's instance.
+-- N.B., it's not possible to reduce the dependency to Applicative.
 instance (Functor m, Monad m) => Applicative (IntRBindingT t m) where
     pure    = IRBT . pure
     x <*> y = IRBT (unIRBT x <*> unIRBT y)
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
@@ -1,16 +1,14 @@
-
 {-# LANGUAGE Rank2Types
            , MultiParamTypeClasses
            , UndecidableInstances
            , FlexibleInstances
            #-}
-
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.06
+--                                                  ~ 2012.02.17
 -- |
 -- Module      :  Control.Unification.Ranked.STVar
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  highly experimental
@@ -41,15 +39,13 @@
 -- addition to the @STRef@ for the term itself, we also track the
 -- variable's ID (to support visited-sets) and rank (to support
 -- weighted path compression).
-data STRVar s t a =
+data STRVar s t =
     STRVar
         {-# UNPACK #-} !Int
         {-# UNPACK #-} !(STRef s Word8)
         {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STRVar s t) t)))
--- BUG: can we actually unpack STRef?
--- BUG: we need a phantom @a@ to get the kinds to work out now...
 
-instance Show (STRVar s t a) where
+instance Show (STRVar s t) where
     show (STRVar i _ _) = "STRVar " ++ show i
 
 instance Variable (STRVar s t) where
@@ -102,7 +98,7 @@
 _newSTRVar
     :: String
     -> Maybe (MutTerm (STRVar s t) t)
-    -> STRBinding s (STRVar s t (MutTerm (STRVar s t) t))
+    -> STRBinding s (STRVar s t)
 _newSTRVar fun mb = STRB $ do
     nr <- ask
     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
@@ -1,16 +1,14 @@
-
 {-# LANGUAGE Rank2Types
            , MultiParamTypeClasses
            , UndecidableInstances
            , FlexibleInstances
            #-}
-
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
 ----------------------------------------------------------------
---                                                  ~ 2011.07.06
+--                                                  ~ 2012.02.17
 -- |
 -- Module      :  Control.Unification.STVar
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  experimental
@@ -40,16 +38,15 @@
 -- | Unification variables implemented by 'STRef's. In addition to
 -- the @STRef@ for the term itself, we also track the variable's
 -- ID (to support visited-sets).
-data STVar s a =
+data STVar s t =
     STVar
         {-# UNPACK #-} !Int
-        {-# UNPACK #-} !(STRef s (Maybe a))
--- BUG: can we actually unpack STRef?
+        {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STVar s t) t)))
 
-instance Show (STVar s a) where
+instance Show (STVar s t) where
     show (STVar i _) = "STVar " ++ show i
 
-instance Variable (STVar s) where
+instance Variable (STVar s t) where
     eqVar (STVar i _) (STVar j _) = i == j
     
     getVarID  (STVar i _) = i
@@ -99,8 +96,8 @@
 
 _newSTVar
     :: String
-    -> Maybe (MutTerm (STVar s) t)
-    -> STBinding s (STVar s (MutTerm (STVar s) t))
+    -> Maybe (MutTerm (STVar s t) t)
+    -> STBinding s (STVar s t)
 _newSTVar fun mb = STB $ do
     nr <- ask
     lift $ do
@@ -111,7 +108,9 @@
                 writeSTRef nr $! n+1
                 STVar n <$> newSTRef mb
 
-instance (Unifiable t) => BindingMonad (STVar s) t (STBinding s) where
+instance (Unifiable t) =>
+    BindingMonad (STVar s t) 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
@@ -4,12 +4,11 @@
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
 
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
-
 ----------------------------------------------------------------
---                                                  ~ 2011.07.11
+--                                                  ~ 2012.02.17
 -- |
 -- Module      :  Control.Unification.Types
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  experimental
@@ -50,11 +49,11 @@
 -- variable type should implement 'Variable'. The 'Show' instance
 -- doesn't show the constructors, for legibility.
 data MutTerm v t
-    = MutVar  !(v (MutTerm v t))
+    = MutVar  !v
     | MutTerm !(t (MutTerm v t))
 
 
-instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) =>
+instance (Show v, Show (t (MutTerm v t))) =>
     Show (MutTerm v t)
     where
     showsPrec p (MutVar  v) = showsPrec p v
@@ -85,7 +84,7 @@
 -- the errors), the extra complexity is not considered worth it.
 data UnificationFailure v t
     
-    = OccursIn (v (MutTerm v t)) (MutTerm v t)
+    = OccursIn v (MutTerm v t)
         -- ^ 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
@@ -117,7 +116,7 @@
 
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show (t (MutTerm v t)), Show (v (MutTerm v t))) =>
+instance (Show (t (MutTerm v t)), Show v) =>
     Show (UnificationFailure v t)
     where
     -- TODO: implement 'showsPrec' instead
@@ -144,10 +143,7 @@
     zipMatch :: t a -> t b -> Maybe (t (a,b))
 
 
--- | An implementation of unification variables. Note that we do
--- not require variables to be functors. Thus, it does not matter
--- whether you give them vacuous functor instances, or use clever
--- tricks like @CoYoneda STRef@ to give them real functor instances.
+-- | An implementation of unification variables.
 class Variable v where
     
     -- | Determine whether two variables are equal /as variables/,
@@ -155,12 +151,12 @@
     -- implementation is:
     --
     -- > eqVar x y = getVarID x == getVarID y
-    eqVar :: v a -> v b -> Bool
+    eqVar :: v -> v -> Bool
     eqVar x y = getVarID x == getVarID y
     
     -- | Return a unique identifier for this variable, in order to
     -- support the use of visited-sets instead of occurs-checks.
-    getVarID :: v a -> Int
+    getVarID :: v -> Int
 
 
 ----------------------------------------------------------------
@@ -181,24 +177,24 @@
     
     -- | Given a variable pointing to @MutTerm v t@, return the
     -- term it's bound to, or @Nothing@ if the variable is unbound.
-    lookupVar :: v (MutTerm v t) -> m (Maybe (MutTerm v t))
+    lookupVar :: v -> m (Maybe (MutTerm v t))
     
     
     -- | Generate a new free variable guaranteed to be fresh in
     -- @m@.
-    freeVar :: m (v (MutTerm v t))
+    freeVar :: m v
     
     
     -- | Generate a new variable (fresh in @m@) bound to the given
     -- term. The default implementation is:
     --
     -- > newVar t = do { v <- freeVar ; bindVar v t ; return v }
-    newVar :: MutTerm v t -> m (v (MutTerm v t))
+    newVar :: MutTerm v t -> 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) -> MutTerm v t -> m ()
+    bindVar :: v -> MutTerm v t -> m ()
 
 
 ----------------------------------------------------------------
@@ -216,7 +212,7 @@
     Rank {-# UNPACK #-} !Word8 !(Maybe (MutTerm v t))
 
 -- Can't derive this because it's an UndecidableInstance
-instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) =>
+instance (Show v, Show (t (MutTerm v t))) =>
     Show (Rank v t)
     where
     show (Rank n mb) = "Rank "++show n++" "++show mb
@@ -240,16 +236,16 @@
 class (BindingMonad v t m) => RankedBindingMonad v t m | m -> v t where
     -- | Given a variable pointing to @MutTerm v t@, return its
     -- rank and the term it's bound to.
-    lookupRankVar :: v (MutTerm v t) -> m (Rank v t)
+    lookupRankVar :: v -> m (Rank v t)
     
     -- | Increase the rank of a variable by one.
-    incrementRank :: v (MutTerm v t) -> m ()
+    incrementRank :: v -> m ()
     
     -- | 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) -> MutTerm v t -> m ()
+    incrementBindVar :: v -> MutTerm v t -> m ()
     incrementBindVar v t = do { incrementRank v ; bindVar v t }
 
 ----------------------------------------------------------------
diff --git a/src/Data/Functor/Fixedpoint.hs b/src/Data/Functor/Fixedpoint.hs
--- a/src/Data/Functor/Fixedpoint.hs
+++ b/src/Data/Functor/Fixedpoint.hs
@@ -1,4 +1,3 @@
-
 -- For the Show (Fix f) instance
 {-# LANGUAGE UndecidableInstances #-}
 -- For 'build' and 'hmap'
@@ -7,12 +6,11 @@
 {-# OPTIONS_GHC -O2 -fglasgow-exts #-}
 
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
-
 ----------------------------------------------------------------
 --                                                    2011.07.11
 -- |
 -- Module      :  Data.Functor.Fixedpoint
--- Copyright   :  Copyright (c) 2007--2011 wren ng thornton
+-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
 -- License     :  BSD
 -- Maintainer  :  wren@community.haskell.org
 -- Stability   :  provisional
@@ -97,9 +95,9 @@
 -- | A higher-order map taking a natural transformation @(f -> g)@
 -- and lifting it to operate on @Fix@.
 hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g
+{-# INLINE [0] hmap #-}
 hmap eps = ana (eps . unFix)
     -- == cata (Fix . eps) -- But the anamorphism is a better producer.
-{-# INLINE [0] hmap #-}
 
 {-# RULES
 "hmap id"
@@ -115,8 +113,8 @@
 hmapM
     :: (Functor f, Traversable g, Monad m)
     => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g)
-hmapM eps = anaM (eps . unFix)
 {-# INLINE [0] hmapM #-}
+hmapM eps = anaM (eps . unFix)
 
 {-# RULES
 "hmapM return"                                  hmapM return = return
@@ -128,8 +126,8 @@
 -- is, this maps the function over the first layer of recursive
 -- structure.
 ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f
-ymap f = Fix . fmap f . unFix
 {-# INLINE [0] ymap #-}
+ymap f = Fix . fmap f . unFix
 
 {-# RULES
 "ymap id"                          ymap id = id
@@ -138,9 +136,10 @@
 
 
 -- | A monadic variant of 'ymap'.
-ymapM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)
-ymapM f = liftM Fix . mapM f . unFix
+ymapM :: (Traversable f, Monad m)
+      => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)
 {-# INLINE ymapM #-}
+ymapM f = liftM Fix . mapM f . unFix
 
 {-# RULES
 "ymapM id"                          ymapM return = return
@@ -154,8 +153,8 @@
 -- | Take a Church encoding of a fixed point into the data
 -- representation of the fixed point.
 build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f
-build g = g Fix
 {-# INLINE [0] build #-}
+build g = g Fix
 
 -- N.B., the signature is required on @g@ in order to be Rank-2.
 -- The signature is required on @phi@ in order to bring @f@ into
@@ -171,10 +170,10 @@
 -- This function applies the @f@-algebra from the bottom up over
 -- @Fix f@ to create some residual value.
 cata :: (Functor f) => (f a -> a) -> (Fix f -> a)
+{-# INLINE [0] cata #-}
 cata phi = self
     where
     self = phi . fmap self . unFix
-{-# INLINE [0] cata #-}
 
 {-# RULES
 "cata-refl"
@@ -200,10 +199,10 @@
 --
 -- N.B., this orders the side effects from the bottom up.
 cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)
+{-# INLINE cataM #-}
 cataM phiM = self
     where
     self = phiM <=< (mapM self . unFix)
-{-# INLINE cataM #-}
 
 -- TODO: other rules for cataM
 {-# RULES
@@ -220,16 +219,16 @@
 -- If you don't like either @fmap@ or @cata@, then maybe this is
 -- what you were thinking?
 ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f
-ycata f = cata (f . Fix)
 {-# INLINE ycata #-}
+ycata f = cata (f . Fix)
 
 
 -- TODO: remove this, or add similar versions for ana* and hylo*?
 -- | Monadic variant of 'ycata'.
 ycataM :: (Traversable f, Monad m)
        => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)
-ycataM f = cataM (f . Fix)
 {-# INLINE ycataM #-}
+ycataM f = cataM (f . Fix)
 
 
 ----------------------------------------------------------------
@@ -237,10 +236,10 @@
 -- functor. This function applies an @f@-coalgebra from the top
 -- down to expand a seed into a @Fix f@.
 ana :: (Functor f) => (a -> f a) -> (a -> Fix f)
+{-# INLINE [0] ana #-}
 ana psi = self
     where
     self = Fix . fmap self . psi
-{-# INLINE [0] ana #-}
 
 
 {-# RULES
@@ -268,10 +267,10 @@
 --
 -- N.B., this orders the side effects from the top down.
 anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))
+{-# INLINE anaM #-}
 anaM psiM = self
     where
     self = (liftM Fix . mapM self) <=< psiM
-{-# INLINE anaM #-}
 
 
 ----------------------------------------------------------------
@@ -283,10 +282,10 @@
 
 -- | @hylo phi psi == cata phi . ana psi@
 hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)
+{-# INLINE hylo #-}
 hylo phi psi = self
     where
     self = phi . fmap self . psi
-{-# INLINE hylo #-}
 
 -- TODO: rules for hylo?
 
@@ -294,10 +293,10 @@
 -- | @hyloM phiM psiM == cataM phiM <=< anaM psiM@
 hyloM :: (Traversable f, Monad m)
       => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)
+{-# INLINE hyloM #-}
 hyloM phiM psiM = self
     where
     self = phiM <=< mapM self <=< psiM
-{-# INLINE hyloM #-}
 
 -- TODO: rules for hyloM?
 
diff --git a/unification-fd.cabal b/unification-fd.cabal
--- a/unification-fd.cabal
+++ b/unification-fd.cabal
@@ -1,24 +1,28 @@
 ----------------------------------------------------------------
--- wren ng thornton <wren@community.haskell.org>    ~ 2011.07.11
+-- wren ng thornton <wren@community.haskell.org>    ~ 2012.02.17
 ----------------------------------------------------------------
 
-Name:           unification-fd
-Version:        0.5.0
 -- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with:
 -- and source-repository:.
 Cabal-Version:  >= 1.6
 Build-Type:     Simple
+
+Name:           unification-fd
+Version:        0.6.0
 Stability:      experimental
-Copyright:      Copyright (c) 2007--2011 wren ng thornton
-License:        BSD3
-License-File:   LICENSE
+Homepage:       http://code.haskell.org/~wren/
 Author:         wren ng thornton
 Maintainer:     wren@community.haskell.org
-Homepage:       http://code.haskell.org/~wren/
+Copyright:      Copyright (c) 2007--2012 wren ng thornton
+License:        BSD3
+License-File:   LICENSE
+
 Category:       Algebra, Algorithms, Compilers/Interpreters, Language, Logic, Unification
 Synopsis:       Simple generic unification algorithms.
 Description:    Simple generic unification algorithms.
 
+Extra-source-files:
+    AUTHORS, README, VERSION
 Source-Repository head
     Type:     darcs
     Location: http://community.haskell.org/~wren/unification-fd