diff --git a/Type/Spine.hs b/Type/Spine.hs
--- a/Type/Spine.hs
+++ b/Type/Spine.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TemplateHaskell, EmptyDataDecls, TypeOperators #-}
+{-# LANGUAGE TypeFamilies, TemplateHaskell, PolyKinds #-}
 
 {- |
 
@@ -13,40 +13,13 @@
 The spine-view on types.
 
 -}
-module Type.Spine (qK, Spine, TypeName, (:@), spineType) where
-
-import Type.Spine.Kinds (parseK_, forallAppsK)
-import Type.Spine.Stage0
-
-import Language.Haskell.TH (Kind(ArrowK), tySynInstD, varT, mkName)
-import Language.Haskell.TH.Quote (QuasiQuoter(..))
-
-import Control.Monad ((<=<))
-
-
-
--- | @[qK|...|]@ is the a type that takes one parameter of the corresponding
--- kind. (The name is an encoding of that parameter's kind based on prefix
--- notation for application.)
-qK :: QuasiQuoter
-qK = QuasiQuoter (error "Type.Spine.qK Exp")
-     (error "Type.Spine.qK Pat")
-     (kTypeG <=< parseK_) (error "Type.Spine.qK Dec")
-
-infixl 9 :@
--- | A type-level application.
-data tc :@ t
-
-fmap concat $ forallAppsK $ \ak k ->
-  let kq = kTypeG k; aq = kTypeG ak; fq = kTypeG $ ArrowK ak k
-      [f, a] = map (varT . mkName) ["f", "a"]
-  in (:[]) `fmap` tySynInstD ''Spine [[t| $kq ($f $a) |]] [t| $fq $f :@ $aq $a |]
-
+module Type.Spine (Spine, Atom, (:@), spineType_d, spineType_d_, spineType_pro, spineType_pro_) where
 
+import Type.Spine.Base
 
 
 
-fmap concat $ mapM spineType
+fmap concat $ mapM spineType_d
   [''Bool, ''Char, ''Double, ''Float, ''Int, ''Integer, ''Ordering,
    ''(), ''(,), ''(,,), ''(,,,), ''(,,,,),
    ''IO, ''[], ''Maybe, ''(->), ''Either]
diff --git a/Type/Spine/Base.hs b/Type/Spine/Base.hs
new file mode 100644
--- /dev/null
+++ b/Type/Spine/Base.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE EmptyDataDecls, TypeFamilies, PolyKinds, TemplateHaskell, TypeOperators #-}
+
+module Type.Spine.Base where
+
+import Language.Haskell.TH
+
+import Type.Spine.TH (tyConSignature)
+
+
+
+--type family Reify (t :: k)
+type family Spine (t :: k)
+
+
+
+data Atom (t :: k) :: *
+infixl 9 :@
+data (tc :: k) :@ (t :: l) :: *
+
+
+
+-- works in 7.4, but not in 7.6 :(
+--type instance Spine ((tc :: k -> l) (t :: k)) = Spine tc :@ Spine t
+
+-- | @spineType_d n@ generates the @Spine@ instance for the type named @n@.
+spineType_d :: Name -> Q [Dec]
+spineType_d n = tyConSignature n >>= spineType_d_ n . fst
+
+
+-- | @spineType_d_ n ks@ generates the @Spine@ instance for the type named @n@
+-- that has parameters with kinds @ks@.
+spineType_d_ :: Name -> [Kind] -> Q [Dec]
+spineType_d_ = spineType_gen_ . ConT
+
+
+
+
+-- | @spineType_pro n@ generates the @Spine@ instance for the promoted data constructor named @n@.
+spineType_pro :: Name -> Q [Dec]
+spineType_pro n = tyConSignature n >>= spineType_d_ n . fst
+
+-- | @spineType_pro_ n ks@ generates the @Spine@ instance for the promoted data
+-- constructor named @n@ that has parameters with kinds @ks@.
+spineType_pro_ :: Name -> [Kind] -> Q [Dec]
+spineType_pro_ = spineType_gen_ . PromotedT
+
+
+
+-- | @spineType_gen_ ty ks@ generates the @Spine@ instance for the type @ty@
+-- that has parameters with kinds @ks@.
+spineType_gen_ :: Type -> [Kind] -> Q [Dec]
+spineType_gen_ t ks = do
+  let rhs = ConT ''Atom `AppT` t
+      vars = [VarT $ mkName $ "t" ++ show i | i <- [0..]]
+  let snoc ty1 ty2 = ConT ''(:@) `AppT` ty1 `AppT` ty2
+  return $ TySynInstD ''Spine [t] rhs :
+    [ case take n vars of
+        vars -> TySynInstD ''Spine [foldl AppT t vars] $ foldl snoc t $ vars
+      | n <- [1..length ks] ]
diff --git a/Type/Spine/Kinds.hs b/Type/Spine/Kinds.hs
deleted file mode 100644
--- a/Type/Spine/Kinds.hs
+++ /dev/null
@@ -1,106 +0,0 @@
-{-# LANGUAGE ViewPatterns #-}
-
-{- |
-
-Module      :  Type.Spine.Kinds
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Kinds for the spine-view on types.
-
--}
-module Type.Spine.Kinds where
-
-import Language.Haskell.TH
-import Language.Haskell.TH.Quote
-
-import Control.Monad ((<=<), liftM)
-
-import qualified Control.Arrow as Arrow
-
-
--- | The set of kinds that this library will initially support as type
--- parameters.
-parameterKinds :: [Kind]
-parameterKinds =
-  [StarK, ArrowK StarK StarK, ArrowK StarK (ArrowK StarK StarK)]
-
--- | The default number of parameters that this library will initially support.
-maxParameters = 5 :: Int
-
--- | The kinds consequent from @parameterKinds@ and @maxParameters@.
-allKinds = [ k | n <- [0..maxParameters], k <- generateK parameterKinds n ]
-
-
-
--------------------- parsing kinds
-badParseK s = fail $ "Data.Proxy.TH.Aux could not parse: " ++ s
-
-parseK_ :: Monad m => String -> m Kind
-parseK_ s = parseK s >>= \(k, s) -> case trim s of
-  "" -> return k
-  _ -> badParseK s
-
-trim = dropWhile (==' ')
-
-parseK :: Monad m => String -> m (Kind, String)
-parseK s = w s where
-  bad = badParseK s
-
-  w s = w1 s >>= \p@(k, s) -> case trim s of
-    '-' : '>' : s -> Arrow.first (ArrowK k) `liftM` w s
-    _ -> return p
-
-  w1 (' ' : s) = w1 s
-  w1 ('(' : s) = w s >>= \(k, s) -> case trim s of
-   ')' : s -> return (k, s)
-   _ -> bad
-  w1 ('*' : s) = return (StarK, s)
-  w1 _ = bad
-
--------------------- serializing kind as Haskell identifier
-stringK = w where
-  w StarK = "S"
-  w (ArrowK k1 k2) = 'T' : w k1 ++ w k2
-
-nameK = mkName . ('K' :) . stringK where
-
-typeK = conT . nameK
-
-declareK k = do
-  let n = nameK k
-  let dec = DataD [] n [KindedTV (mkName "t") k] [] []
-  i <- recover (return Nothing) $ Just `fmap` reify n
-  case i of
-    Nothing -> return [dec]
-    Just (TyConI (DataD [] _ [PlainTV _] [] [])) | StarK == k -> return []
-    Just (TyConI (DataD [] _ [KindedTV _ ((== k) -> True)] [] [])) -> return []
-    _ -> fail $ "Data.Proxy.TH.Aux: " ++ show n ++ " is already declared (and not equivalently)"
-
--- | @[qK|...|]@ is either the declaration of a type that takes one parameter
--- of the corresponding kind, or an occurrence of that type constructor. (The
--- name is an encoding of that parameter's kind based on prefix notation for
--- application.)
-qK :: QuasiQuoter
-qK = QuasiQuoter (error "Type.Spine.Kinds.qK Exp")
-     (error "Type.Spine.Kinds.qK Pat")
-     (typeK <=< parseK_) (declareK <=< parseK_)
-
-
--- | @generateK pks n@ generates all 'Kind's with @0@ to @n@ parameters taken
--- from @pks@.
-generateK pks 0 = [StarK]
-generateK pks n = concatMap (\k ->
-  (map (flip ArrowK k) pks)) (generateK pks (n - 1))
-
-
--- | Calls its argument once for each parameter and kind pair implied by
--- @maxParameters@ and @parameterKinds@.
-forallAppsK :: (Kind -> Kind -> Q a) -> Q [a]
-forallAppsK w = mapM (uncurry w) [ (ak, k)
-  | n <- [0..maxParameters - 1], k <- generateK parameterKinds n,
-    ak <- parameterKinds]
diff --git a/Type/Spine/Stage0.hs b/Type/Spine/Stage0.hs
deleted file mode 100644
--- a/Type/Spine/Stage0.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-{-# LANGUAGE TypeFamilies, TemplateHaskell, KindSignatures, EmptyDataDecls #-}
-
-{- |
-
-Module      :  Type.Spine.Stage0
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Declares the type wrappers (mappings @k -> *@) for 'allKinds' and then defines
-functions for referencing them. Also provides a Template Haskell function for
-generating the @Spine@ type instances for user-defined datatypes.
-
--}
-module Type.Spine.Stage0 where
-
-import Language.Haskell.TH
-
-import Type.Spine.TH (liftNameG, tyConSignature)
-import Type.Spine.Kinds (allKinds, declareK, nameK)
-
-import Control.Monad ((<=<))
-
-
--- | The @Spine@ type family represents its argument as either a 'TypeName' or
--- an application via ':@'.
-type family Spine t
-
--- | @TypeName@ represents an occurrence of totally unapplied type name.
-data TypeName x
-
-
-
-fmap concat $ mapM declareK allKinds
-
--- | @kNameG k@ returns the globally unique name (i.e. TH's @NameG@) of the
--- declared wrapper for types of kind @k@.
-kNameG :: Kind -> Q Name
-kNameG k = $(caseE [| k |] $ [
-  let n = nameK k in
-  match (let p StarK = conP 'StarK []
-             p (ArrowK k1 k2) = conP 'ArrowK [p k1, p k2] in p k)
-  (normalB $ [| return $(liftNameG n) |]) []
-    | k <- allKinds ] ++
-  [match wildP (normalB [| fail $ show k ++ " is not supported by type-kinds" |]) []])
-
--- | @kTypeG = conT <=< kNameG@.
-kTypeG :: Kind -> Q Type
-kTypeG = conT <=< kNameG
-
-
-
-
--- | @spineType n@ generates the @Spine@ instance for the type named @n@.
-spineType :: Name -> Q [Dec]
-spineType n = do
-  (ks, k) <- tyConSignature n
-  spineType_ n ks k
-
-
--- | @spineType_ n ks k@ generates the @Spine@ instance for the type named @n@
--- with parameter kind @ks@ and range kind @k@.
-spineType_ :: Name -> [Kind] -> Kind -> Q [Dec]
-spineType_ n ks k = do
-  let kq = kTypeG $ foldr ArrowK k ks
-      t = [t| $kq $(conT n) |]
-  (:[]) `fmap` tySynInstD ''Spine [t] [t| TypeName $t |]
diff --git a/Type/Spine/TH.hs b/Type/Spine/TH.hs
--- a/Type/Spine/TH.hs
+++ b/Type/Spine/TH.hs
@@ -20,30 +20,80 @@
 
 
 
--- | A TemplateHaskell-lifter for 'NameG's.
-liftNameG :: Name -> Q Exp
-liftNameG n = do
-  TyConI (DataD _ (Name occ (NameG _ pkg mod)) _ _ _) <- reify n
-  [| mkNameG_tc $(stringE $ pkgString pkg) $(stringE $ modString mod) $(stringE $ occString occ) |]
 
+toNameG :: Name -> Q Name
+toNameG n = do
+  info <- reify n
+  let err = error "liftNameG expects a top-level named thing"
+      onDec dec = case dec of
+        FunD n _ -> n
+        ValD (VarP n) _ _ -> n
+        ValD (AsP n _) _ _ -> n
+        ValD {} -> err
+        DataD _ n _ _ _ -> n
+        NewtypeD _ n _ _ _ -> n
+        TySynD n _ _ -> n
+        ClassD _ n _ _ _ -> n
+        InstanceD {} -> err
+        SigD n _ -> n
+        ForeignD (ImportF _ _ _ n _) -> n
+        ForeignD (ExportF _ _ n _) -> n
+        InfixD _ n -> n
+        PragmaD {} -> err
+        FamilyD _ n _ _ -> n
+        DataInstD {} -> err
+        NewtypeInstD {} -> err
+        TySynInstD {} -> err
+  return $ case info of
+    ClassI dec _ -> onDec dec
+    ClassOpI n _ _ _ -> n
+    TyConI dec -> onDec dec
+    FamilyI dec _ -> onDec dec
+    PrimTyConI n _ _ -> n
+    DataConI n _ _ _ -> n
+    VarI {} -> err
+    TyVarI {} -> err
 
--- | Returns the kinds of a type constructor's type paratemers and range.
+-- | A Template Haskell-lifter for data constructors' 'NameG's.
+liftNameG_d :: Name -> Q Exp
+liftNameG_d n = do
+  Name occ (NameG _ pkg mod) <- toNameG n
+  [| mkNameG_d $(stringE $ pkgString pkg) $(stringE $ modString mod) $(stringE $ occString occ) |]
+
+
+-- | Returns the kinds of a type constructor's type parameters and range.
 tyConSignature :: Name -> Q ([Kind], Kind)
 tyConSignature n = do
   let bad = fail "Type.Spine.TH.tyConSignature expects the name of a data/newtype/data family"
   i <- reify n
   case i of
+    DataConI _ tys n _ -> return (getArgTypes tys, PromotedT n)
+      where -- NB first, drop quantification over the data types' parameters
+            getArgTypes (ForallT _ _ ty) = loop ty
+            getArgTypes ty = loop ty
+            -- TODO check that it's promotable...
+            loop (AppT (AppT ArrowT x) y) = promote x : loop y
+              where promote (VarT n) = VarT n
+                    promote (ConT n)
+                      | n == '[] = PromotedNilT
+                      | n == '(:) = PromotedConsT
+                      | otherwise = PromotedT n
+                    promote (AppT ty1 ty2) = AppT (promote ty1) (promote ty2)
+                    promote (TupleT i) = PromotedTupleT i
+                    promote ty =
+                      error $ "type-spine:tyConSignature: cannot promote" ++ show ty
+            loop _ = [] -- this is the ctor's codomain, so ignore it
     TyConI dec -> case dec of
-      DataD _ _ tvbs _ _ -> return (map tvb_kind tvbs, StarK)
-      NewtypeD _ _ tvbs _ _ -> return (map tvb_kind tvbs, StarK)
-      FamilyD DataFam _ tvbs mk -> return (map tvb_kind tvbs, maybe StarK (peel tvbs) mk)
+      DataD _ _ tvbs _ _ -> return (map tvb_kind tvbs, StarT)
+      NewtypeD _ _ tvbs _ _ -> return (map tvb_kind tvbs, StarT)
+      FamilyD DataFam _ tvbs mk -> return (map tvb_kind tvbs, maybe StarT (peel tvbs) mk)
         where peel [] k = k
-              peel (_ : l) (ArrowK _ r) = peel l r
+              peel (_ : l) (AppT (AppT ArrowT _) r) = peel l r
               peel _ _ = error "Type.Spine.TH: bad FamilyD kind"
       _ -> bad
-    PrimTyConI _ i _ -> return (replicate i StarK, StarK)
+    PrimTyConI _ i _ -> return (replicate i StarT, StarT)
     _ -> bad
 
 tvb_kind :: TyVarBndr -> Kind
-tvb_kind (PlainTV _) = StarK
+tvb_kind (PlainTV _) = StarT
 tvb_kind (KindedTV _ k) = k
diff --git a/type-spine.cabal b/type-spine.cabal
--- a/type-spine.cabal
+++ b/type-spine.cabal
@@ -1,5 +1,5 @@
 Name:           type-spine
-Version:        0.1.2
+Version:        0.2
 License:        BSD3
 License-File:   LICENSE
 Author:         Nicolas Frisby <nicolas.frisby@gmail.com>
@@ -9,16 +9,12 @@
 
 Synopsis:       A spine-view on types
 
-Description: Until
-  <http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf>
-  reaches the mainline, this is a surprisingly effective workaround. We support
-  a limited number of kinds out-of-the-box, but it can be extended by the
-  power-user. Also, quasiquotation makes the code rather legible. Given a
-  finite set of kinds to support, generic type families can be defined that
-  will work for an infinite number of types. It is very much a \"bumping up\"
-  of the term-level /spine view/.
+Description:
+  This is very much a \"bumping up\" of the term-level /spine view/,
+  c.f. Hinze's work and Emil Axelsson's hackage package @syntactic@.
   .
-  See the @type-cereal@ package for a use case.
+  See the @type-cereal@ and @type-ord@ packages for use cases (ultimately
+  supporting the @yoko@ package).
 
 Cabal-Version: >= 1.6.0.1
 
@@ -28,4 +24,4 @@
 Library
   Build-Depends: base >= 4 && < 5, template-haskell
 
-  Exposed-Modules: Type.Spine, Type.Spine.Kinds, Type.Spine.Stage0, Type.Spine.TH
+  Exposed-Modules: Type.Spine, Type.Spine.Base, Type.Spine.TH