diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,2 @@
+Copyright Louis Wasserman 2010
+BSD license
diff --git a/Language/Haskell/TH/KindInference.hs b/Language/Haskell/TH/KindInference.hs
new file mode 100644
--- /dev/null
+++ b/Language/Haskell/TH/KindInference.hs
@@ -0,0 +1,208 @@
+
+-- | A module to infer the kind of a given type within Template Haskell.
+-- Warning: this implements its own kind inference system, and is therefore
+-- not guaranteed to work on all esoteric types.  (That said, I have no examples
+-- where it doesn't work.)
+module Language.Haskell.TH.KindInference (inferKind) where
+
+-- import Control.Monad
+import Control.Monad.Trans
+import Data.Ord
+import Debug.Trace
+import Data.Map((!))
+import Data.Set
+import Control.Monad.State
+import Text.ParserCombinators.ReadP hiding (get)
+
+import Language.Haskell.TH hiding (AppE)
+import Language.Haskell.TH.Unification
+import Language.Haskell.TH.PprLib hiding (empty, char)
+import qualified Language.Haskell.TH.PprLib as Ppr
+
+type KindUTerm = Term KindFunc Type KindAtom
+type KindUT = UnifT KindFunc Type KindAtom
+
+instance Ord Type where
+	compare = comparing show
+
+type LoopKillerT = StateT (Set Name)
+data KindFunc = KindArrow deriving (Eq, Show)
+data KindAtom = Star deriving (Eq, Show)
+
+-- | Returns either an error message or the 'Kind' of the type referred to by the specified name.
+-- Works with datas, newtypes, type synonyms, type classes, data families, and type families.
+-- 
+-- Note: There has been a bug observed in Template Haskell relating to the parsing of types.  This
+-- assumes that bug is still present, and fixes it.
+inferKind :: Name -> Q (Either String Kind)
+inferKind name = do
+	ans <- solveUnification (evalStateT (infer (ConT name)) empty)
+	either (return . Left) (\ (x, sol) -> return (Right $ termToK (subTerm sol x))) ans
+
+termToK :: Explicit KindFunc KindAtom -> Kind
+termToK (AppE ~KindArrow t1 t2) = termToK t1 `ArrowK` termToK t2
+termToK (AtomE ~Star) = StarK
+
+infer :: Type -> LoopKillerT (KindUT Q) KindUTerm
+infer (TupleT n) = return (tupleKind n star)
+infer ArrowT = return (tupleKind 2 star)
+infer ListT = return (tupleKind 1 star)
+infer (AppT f x) = do
+	fK <- infer f
+	xK <- infer x
+	let var = Var (AppT f x)
+	lift $ unify fK (xK `kindArrow` var)
+	return var
+infer (SigT t k) = do
+	tK <- infer t
+	lift $ unify tK (kToTerm k)
+	return tK
+infer (ForallT bdrs cxt t) = do
+	mapM_ handleBdr bdrs
+	mapM_ handleCxt cxt
+	infer t
+infer t@VarT{} = return $ Var t
+infer (ConT t) = do
+	examine (Just t) t
+	return (tyCon t)
+
+matchUnboxedTuple :: ReadP Int
+matchUnboxedTuple = do
+	string "(#"
+	munchComma 1
+	where	munchComma k = k `seq` ((do
+			char ','
+			munchComma (k+1)) <++ (do
+			string "#)"
+			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)
+	_	-> 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 ()
+	
+mUnify :: Maybe Name -> KindUTerm -> LoopKillerT (KindUT Q) ()
+mUnify name0 k = case name0 of 
+	Just name0	-> lift $ unify (tyCon name0) k
+	_		-> return ()
+
+examineDec :: Maybe Name -> Dec -> LoopKillerT (KindUT Q) ()
+examineDec name0 (DataD cxt name bdrs cons _) = do
+	visited <- get
+	unless (name `member` visited) $ do
+	  modify (insert name)
+	  mapM_ handleCxt cxt
+	  args <- mapM handleBdr bdrs
+	  lift $ unify (tyCon name) (foldr kindArrow star args)
+	  mUnify name0 (tyCon name)
+	  mapM_ handleCon cons
+examineDec name0 (NewtypeD cxt name bdrs con _) = do
+	visited <- get
+	unless (name `member` visited) $ do
+	  modify (insert name)
+	  mapM_ handleCxt cxt
+	  args <- mapM handleBdr bdrs
+	  lift $ unify (tyCon name) (foldr kindArrow star args)
+	  mUnify name0 (tyCon name)
+	  handleCon con
+examineDec name0 (ClassD cxt name bdrs _ _) = do
+	visited <- get
+	unless (name `member` visited) $ do
+	  modify (insert name)
+	  mapM_ handleCxt cxt
+	  args <- mapM handleBdr bdrs
+	  lift $ unify (tyCon name) (foldr kindArrow 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)
+	  mUnify name0 (tyCon name)
+examineDec name0 (TySynD name bdrs typ) = do
+	visited <- get
+	unless (name `member` visited) $ do
+	  modify (insert name)
+	  args <- mapM handleBdr bdrs
+	  kind <- infer typ
+	  lift $ unify (tyCon name) (foldr kindArrow 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 (InfixC (_, t1) _ (_, t2)) = do
+	k1 <- infer t1
+	k2 <- infer t2
+	lift $ unify k1 star
+	lift $ unify k2 star
+handleCon (ForallC bdrs cxt con) = do
+	mapM_ handleBdr bdrs
+	mapM_ handleCxt cxt
+	handleCon con
+
+tyCon :: Name -> KindUTerm
+tyCon = Var . ConT
+
+tyVar :: Name -> KindUTerm
+tyVar = Var . VarT
+
+handleBdr :: TyVarBndr -> LoopKillerT (KindUT Q) KindUTerm
+handleBdr (PlainTV n) = return (tyVar n)
+handleBdr (KindedTV n k) = do
+	lift $ 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)
+	examine (Just name) name
+handleCxt (EqualP t1 t2) = do
+	k1 <- infer t1
+	k2 <- infer t2
+	lift $ 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)
+
+kindArrow :: KindUTerm -> KindUTerm -> KindUTerm
+kindArrow = App KindArrow
+
+star :: KindUTerm
+star = Atom Star
+
+tupleKind :: Int -> KindUTerm -> KindUTerm
+tupleKind n k = foldr kindArrow k (replicate n star)
+
+instance (Ppr a, Ppr b) => Ppr (Either a b) where
+	ppr (Left x) = text "Left" <+> parens (ppr x)
+	ppr (Right x) = text "Right" <+> parens (ppr x)
+instance Ppr Char where
+	ppr = Ppr.char
diff --git a/Language/Haskell/TH/Unification.hs b/Language/Haskell/TH/Unification.hs
new file mode 100644
--- /dev/null
+++ b/Language/Haskell/TH/Unification.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module Language.Haskell.TH.Unification (subTerm, Term(..), UnifT, Explicit(..), unify, solveUnification) where
+
+import Control.Monad
+import Data.Map hiding (map)
+import Control.Monad.State.Strict
+import Control.Monad.Error
+
+data Term f v a = App f (Term f v a) (Term f v a) | Atom a | Var v deriving (Eq, Show)
+data Explicit f a = AppE f (Explicit f a) (Explicit f a) | AtomE a deriving (Eq, Show)
+type Solution f v a = Map v (Explicit f a)
+
+data Constraint f v a = Term f v a :==: Term f v a
+type Constraints f v a = [Constraint f v a]
+
+newtype UnifT f v a m x = UnifT (StateT (Constraints f v a) (ErrorT String m) x)
+deriving instance (Monad m) => Monad (UnifT f v a m)
+deriving instance (Monad m) => MonadState (Constraints f v a) (UnifT f v a m)
+
+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 [])
+
+solveUnification :: (Ord v, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (x, Solution f v a))
+solveUnification (UnifT m) = runErrorT (evalStateT m' [])
+	where	m' = do	x <- m
+			ans <- solve =<< get
+			return (x, ans)
+
+solve :: (Ord v, Eq f, Eq a, Monad m) => Constraints f v a -> m (Solution f v a)
+solve (constr:constrs) = case constr of
+	Var x :==: Var y
+		| x == y	-> solve constrs
+	Var x :==: t
+		-> subSol x t `liftM` solve (substitute x t constrs)
+	t :==: Var y
+		-> subSol y t `liftM` solve (substitute y t constrs)
+	Atom a :==: Atom b
+		| a == b	-> solve constrs
+		| otherwise	-> fail "Mismatched atoms"
+	App f1 x1 y1 :==: App f2 x2 y2
+		| f1 /= f2	-> fail "Mismatched functions"
+		| otherwise	-> solve ([x1 :==: x2, y1 :==: y2] ++ constrs)
+	_	-> fail "Function matched to atom"
+solve [] = return empty
+
+substitute :: (Ord v, Eq f, Eq a) => v -> Term f v a -> Constraints f v a -> Constraints f v a
+substitute v t = map (\ (x :==: y) -> sub x :==: sub y) where
+	sub (Var v')
+		| v == v'	= t
+	sub (App f x y) = App f (sub x) (sub y)
+	sub t' = t'
+
+subTerm :: Ord v => Solution f v a -> Term f v a -> Explicit f a
+subTerm sol (Var v) = sol ! v
+subTerm sol (App f x y) = AppE f (subTerm sol x) (subTerm sol y)
+subTerm _ (Atom a) = AtomE a
+
+subSol :: (Ord v, Eq f, Eq a) => v -> Term f v a -> Solution f v a -> Solution f v a
+subSol v t sol = insert v (subTerm 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/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/th-kinds.cabal b/th-kinds.cabal
new file mode 100644
--- /dev/null
+++ b/th-kinds.cabal
@@ -0,0 +1,17 @@
+Name:		th-kinds
+Version:	0.0.0
+Category:	Template Haskell
+Author:		Louis Wasserman
+License:	BSD3
+License-file:	LICENSE
+Stability:	experimental
+Synopsis:	Automated kind inference in Template Haskell.
+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
+
+exposed-modules:
+      Language.Haskell.TH.KindInference
+other-modules:
+      Language.Haskell.TH.Unification