diff --git a/Language/Haskell/TH/KindInference.hs b/Language/Haskell/TH/KindInference.hs
--- a/Language/Haskell/TH/KindInference.hs
+++ b/Language/Haskell/TH/KindInference.hs
@@ -11,7 +11,7 @@
 import Debug.Trace
 import Data.Map((!))
 import Data.Set
-import Control.Monad.State
+import Control.Monad.State.Strict
 import Text.ParserCombinators.ReadP hiding (get)
 
 import Language.Haskell.TH hiding (AppE)
@@ -54,11 +54,11 @@
 	fK <- infer f
 	xK <- infer x
 	let var = Var (AppT f x)
-	lift $ unify fK (xK `kindArrow` var)
+	unify fK (xK ->- var)
 	return var
 infer (SigT t k) = do
 	tK <- infer t
-	lift $ unify tK (kToTerm k)
+	unify tK (kToTerm k)
 	return tK
 infer (ForallT bdrs cxt t) = do
 	mapM_ handleBdr bdrs
@@ -80,26 +80,24 @@
 			return k))
 
 examine :: Maybe Name -> Name -> LoopKillerT (KindUT Q) ()
-examine name0 name = case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of
-	(n:_)	-> do	lift $ unify (tyVar name) (tupleKind n star)
-			mUnify name0 (tyVar name)
+examine name0 name = do
+     mUnify name0 (tyVar name)
+     case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of
+	(n:_)	-> unify (tyVar name) (tupleKind n star)
 	_	-> do
 	  inf <- lift $ lift $ reify name
 	  case inf of
 		  ClassI dec	-> examineDec name0 dec
 		  TyConI dec	-> examineDec name0 dec
-		  PrimTyConI name n _ -> do
-			  lift $ unify (tyVar name) (tupleKind n star)
-			  mUnify name0 (tyVar name)
-		  TyVarI name typ	-> do
-		  			  kind <- infer typ
-					  lift $ unify (tyVar name) kind
-					  mUnify name0 (tyVar name)
-		  _		-> return ()
+		  PrimTyConI name n _ -> unify (tyVar name) (tupleKind n star)
+		  TyVarI name typ -> do
+		  	kind <- infer typ
+			unify (tyVar name) kind
+		  _ -> return ()
 	
 mUnify :: Maybe Name -> KindUTerm -> LoopKillerT (KindUT Q) ()
 mUnify name0 k = case name0 of 
-	Just name0	-> lift $ unify (tyCon name0) k
+	Just name0	-> unify (tyCon name0) k
 	_		-> return ()
 
 examineDec :: Maybe Name -> Dec -> LoopKillerT (KindUT Q) ()
@@ -109,7 +107,7 @@
 	  modify (insert name)
 	  mapM_ handleCxt cxt
 	  args <- mapM handleBdr bdrs
-	  lift $ unify (tyCon name) (foldr kindArrow star args)
+	  unify (tyCon name) (foldr (->-) star args)
 	  mUnify name0 (tyCon name)
 	  mapM_ handleCon cons
 examineDec name0 (NewtypeD cxt name bdrs con _) = do
@@ -118,7 +116,7 @@
 	  modify (insert name)
 	  mapM_ handleCxt cxt
 	  args <- mapM handleBdr bdrs
-	  lift $ unify (tyCon name) (foldr kindArrow star args)
+	  unify (tyCon name) (foldr (->-) star args)
 	  mUnify name0 (tyCon name)
 	  handleCon con
 examineDec name0 (ClassD cxt name bdrs _ _) = do
@@ -127,14 +125,14 @@
 	  modify (insert name)
 	  mapM_ handleCxt cxt
 	  args <- mapM handleBdr bdrs
-	  lift $ unify (tyCon name) (foldr kindArrow star args)
+	  unify (tyCon name) (foldr (->-) star args)
 	  mUnify name0 (tyCon name)
 examineDec name0 (FamilyD _ name bdrs mK) = do
 	visited <- get
 	unless (name `member` visited) $ do
 	  modify (insert name)
-	  args <- mapM handleBdr bdrs
-	  lift $ unify (tyCon name) (maybe star kToTerm mK)
+	  mapM_ handleBdr bdrs
+	  unify (tyCon name) (maybe star kToTerm mK)
 	  mUnify name0 (tyCon name)
 examineDec name0 (TySynD name bdrs typ) = do
 	visited <- get
@@ -142,22 +140,16 @@
 	  modify (insert name)
 	  args <- mapM handleBdr bdrs
 	  kind <- infer typ
-	  lift $ unify (tyCon name) (foldr kindArrow kind args)
+	  unify (tyCon name) (foldr (->-) kind args)
 	  mUnify name0 (tyCon name)
 examineDec _ _ = return ()
 
 handleCon :: Con -> LoopKillerT (KindUT Q) ()
-handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> do
-	k <- infer t
-	lift $ unify k star) ts
-handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> do
-	k <- infer t
-	lift $ unify k star) ts
+handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> infer t >>= unify star) ts
+handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> infer t >>= unify star) ts
 handleCon (InfixC (_, t1) _ (_, t2)) = do
-	k1 <- infer t1
-	k2 <- infer t2
-	lift $ unify k1 star
-	lift $ unify k2 star
+	infer t1 >>= unify star
+	infer t2 >>= unify star
 handleCon (ForallC bdrs cxt con) = do
 	mapM_ handleBdr bdrs
 	mapM_ handleCxt cxt
@@ -172,37 +164,31 @@
 handleBdr :: TyVarBndr -> LoopKillerT (KindUT Q) KindUTerm
 handleBdr (PlainTV n) = return (tyVar n)
 handleBdr (KindedTV n k) = do
-	lift $ unify (tyVar n) (kToTerm k)
+	unify (tyVar n) (kToTerm k)
 	return (tyVar n)
 
 handleCxt :: Pred -> LoopKillerT (KindUT Q) ()
 handleCxt (ClassP name args) = do
 	kinds <- mapM infer args
-	lift $ unify (Var (ConT name)) (foldr kindArrow star kinds)
+	unify (Var (ConT name)) (foldr (->-) star kinds)
 	examine (Just name) name
 handleCxt (EqualP t1 t2) = do
 	k1 <- infer t1
 	k2 <- infer t2
-	lift $ unify k1 k2
+	unify k1 k2
 
 kToTerm :: Kind -> KindUTerm
-kToTerm = kToTerm' . fixKind where
-	kToTerm' (ArrowK a b) = kToTerm' a `kindArrow` kToTerm' b
-	kToTerm' StarK = star
-
-fixKind :: Kind -> Kind
-fixKind k = loop k StarK where
-	loop StarK k = k
-	loop (ArrowK k1 k2) k = loop k1 (loop k2 StarK `ArrowK` k)
+kToTerm (ArrowK a b) = kToTerm a ->- kToTerm b
+kToTerm StarK = star
 
-kindArrow :: KindUTerm -> KindUTerm -> KindUTerm
-kindArrow = App KindArrow
+(->-) :: KindUTerm -> KindUTerm -> KindUTerm
+(->-) = App KindArrow
 
 star :: KindUTerm
 star = Atom Star
 
 tupleKind :: Int -> KindUTerm -> KindUTerm
-tupleKind n k = foldr kindArrow k (replicate n star)
+tupleKind n k = foldr (->-) k (replicate n star)
 
 instance (Ppr a, Ppr b) => Ppr (Either a b) where
 	ppr (Left x) = text "Left" <+> parens (ppr x)
diff --git a/Language/Haskell/TH/Unification.hs b/Language/Haskell/TH/Unification.hs
--- a/Language/Haskell/TH/Unification.hs
+++ b/Language/Haskell/TH/Unification.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
 
-module Language.Haskell.TH.Unification (subTerm, Term(..), UnifT, Explicit(..), unify, solveUnification) where
+module Language.Haskell.TH.Unification (subTerm, Term(..), MonadUnify(..), UnifT, Explicit(..), solveUnification) where
 
 import Control.Monad
 import Data.Map hiding (map)
@@ -18,12 +18,18 @@
 deriving instance (Monad m) => Monad (UnifT f v a m)
 deriving instance (Monad m) => MonadState (Constraints f v a) (UnifT f v a m)
 
+class Monad m => MonadUnify u m | m -> u where
+	unify :: u -> u -> m ()
+
+instance Monad m => MonadUnify (Term f v a) (UnifT f v a m) where
+	a `unify` b = modify ((a :==: b):)
+
+instance MonadUnify u m => MonadUnify u (StateT s m) where
+	a `unify` b = lift (a `unify` b)
+
 instance MonadTrans (UnifT f v a) where
 	lift = UnifT . lift . lift
 
-unify :: (Monad m) => Term f v a -> Term f v a -> UnifT f v a m ()
-a `unify` b = modify ((a :==: b):)
-
 runUnification :: (Ord v, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (Constraints f v a))
 runUnification (UnifT m) = runErrorT (execStateT m [])
 
@@ -45,8 +51,8 @@
 		| a == b	-> solve def constrs
 		| otherwise	-> fail "Mismatched atoms"
 	App f1 x1 y1 :==: App f2 x2 y2
-		| f1 /= f2	-> fail "Mismatched functions"
-		| otherwise	-> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)
+		| f1 == f2	-> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)
+		| otherwise	-> fail "Mismatched functions"
 	_	-> fail "Function matched to atom"
 solve _ [] = return empty
 
@@ -64,7 +70,3 @@
 
 subSol :: (Ord v, Eq f, Eq a) => Explicit f a -> v -> Term f v a -> Solution f v a -> Solution f v a
 subSol def v t sol = insert v (subTerm def sol t) sol
-	
--- test :: UnifT Char String String IO ()
--- test = do	App 'f' (App 'g' (Var "A") (Var "A")) (Var "A") `unify`
--- 			App 'f' (Var "B") (Atom "xyz")
diff --git a/th-kinds.cabal b/th-kinds.cabal
--- a/th-kinds.cabal
+++ b/th-kinds.cabal
@@ -1,5 +1,5 @@
 Name:		th-kinds
-Version:	0.0.1
+Version:	0.1.0
 Category:	Template Haskell
 Author:		Louis Wasserman
 License:	BSD3
@@ -9,7 +9,7 @@
 Description:	Given the name of a Haskell type, typeclass, type family, or any of the above, determines its kind.
 Maintainer:	Louis Wasserman <wasserman.louis@gmail.com>
 Build-type:	Simple
-build-depends:   template-haskell >= 2.4.0.0 , base >= 4 && < 5, containers >= 0.3, mtl
+build-depends:   template-haskell == 2.4.0.1 , base >= 4 && < 5, containers >= 0.3, mtl
 
 exposed-modules:
       Language.Haskell.TH.KindInference