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
@@ -36,8 +36,11 @@
 -- 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
+	ans <- solveUnification defaultKind (evalStateT (infer (ConT name)) empty)
+	either (return . Left) (\ (x, sol) -> return (Right $ termToK (subTerm defaultKind sol x))) ans
+
+defaultKind :: Explicit KindFunc KindAtom
+defaultKind = AtomE Star
 
 termToK :: Explicit KindFunc KindAtom -> Kind
 termToK (AppE ~KindArrow t1 t2) = termToK t1 `ArrowK` termToK t2
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
@@ -27,28 +27,28 @@
 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' [])
+solveUnification :: (Ord v, Eq f, Eq a, Monad m) => Explicit f a -> UnifT f v a m x -> m (Either String (x, Solution f v a))
+solveUnification def (UnifT m) = runErrorT (evalStateT m' [])
 	where	m' = do	x <- m
-			ans <- solve =<< get
+			ans <- solve def =<< 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
+solve :: (Ord v, Eq f, Eq a, Monad m) => Explicit f a -> Constraints f v a -> m (Solution f v a)
+solve def (constr:constrs) = case constr of
 	Var x :==: Var y
-		| x == y	-> solve constrs
+		| x == y	-> solve def constrs
 	Var x :==: t
-		-> subSol x t `liftM` solve (substitute x t constrs)
+		-> subSol def x t `liftM` solve def (substitute x t constrs)
 	t :==: Var y
-		-> subSol y t `liftM` solve (substitute y t constrs)
+		-> subSol def y t `liftM` solve def (substitute y t constrs)
 	Atom a :==: Atom b
-		| a == b	-> solve constrs
+		| a == b	-> solve def 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)
+		| otherwise	-> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)
 	_	-> fail "Function matched to atom"
-solve [] = return empty
+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
@@ -57,13 +57,13 @@
 	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
+subTerm :: Ord v => Explicit f a -> Solution f v a -> Term f v a -> Explicit f a
+subTerm def sol (Var v) = findWithDefault def v sol
+subTerm def sol (App f x y) = AppE f (subTerm def sol x) (subTerm def 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
+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`
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.0
+Version:	0.0.1
 Category:	Template Haskell
 Author:		Louis Wasserman
 License:	BSD3