diff --git a/Data/Yoko.hs b/Data/Yoko.hs
--- a/Data/Yoko.hs
+++ b/Data/Yoko.hs
@@ -36,8 +36,10 @@
 -}
 
 module Data.Yoko
-  (module Data.YokoRaw, module Data.Yoko.SmartPreciseCase)
-  where
+  (module Data.YokoRaw, module Data.Yoko.SmartPreciseCase, module Data.Yoko.TH) where
 
-import Data.YokoRaw hiding (precise_case)
+import Data.YokoRaw hiding (precise_case0)
 import Data.Yoko.SmartPreciseCase
+import Data.Yoko.TH
+
+import Data.Yoko.Prelude ()
diff --git a/Data/Yoko/Each.hs b/Data/Yoko/Each.hs
deleted file mode 100644
--- a/Data/Yoko/Each.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# LANGUAGE KindSignatures, ConstraintKinds, MultiParamTypeClasses,
-  Rank2Types, FlexibleInstances, UndecidableInstances, TypeOperators #-}
-
-{- |
-
-Module      :  Data.Yoko.Each
-Copyright   :  (c) The University of Kansas 2012
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Basic support for folding through type-level sums.
-
--}
-
-module Data.Yoko.Each (Each, each) where
-
-import Data.Yoko.TypeBasics
-import Data.Yoko.Representation
-
-
--- | The constraint @Each con sum@ corresponds to the constraing @forall dc in
--- sum. con dc@.
-type Each = Each_
-
--- | Fold through a type-level sum.
-each :: Each cxt sum => Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b
-each = each_
-
-
-
-
-
-
-class Each_ cxt sum where
-  each_ :: Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b
-
-
-
-instance cxt a => Each_ cxt (N a) where each_ _ f (N x) = f x
-
-instance (Each_ cxt a, Each_ cxt b) => Each_ cxt (a :+: b) where
-  each_ c f = foldPlus (each c f) (each c f)
-
---instance Each_ cxt sum => Each_ cxt (DCsOf t sum) where
---  each_ c f = each c f . unDCsOf
-
-
-
-
-
-_ex = putStrLn $ each (Proxy :: Proxy Show) show $
-       L (N 'n') `asTypeOf` R (N True)
diff --git a/Data/Yoko/HCompos.hs b/Data/Yoko/HCompos.hs
--- a/Data/Yoko/HCompos.hs
+++ b/Data/Yoko/HCompos.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
   FlexibleContexts, FlexibleInstances, UndecidableInstances,
-  ScopedTypeVariables, DataKinds  #-}
+  ScopedTypeVariables, DataKinds, PolyKinds  #-}
 
 {-# OPTIONS_GHC -fcontext-stack=250 #-}
 
@@ -23,6 +23,7 @@
 module Data.Yoko.HCompos where
 
 import Data.Yoko.TypeBasics
+import Data.Yoko.W
 import Data.Yoko
 
 import Control.Applicative
@@ -36,15 +37,15 @@
 
 
 -- | The applicative functor required by the conversion.
-type family Idiom cnv :: * -> *
+type family Idiom (cnv :: *) :: * -> *
 
 -- | Use the conversion @cnv@ to convert from @a@ to @b@.
-class Applicative (Idiom cnv) => Convert cnv a b where
-  convert :: cnv -> a -> Idiom cnv b
+class Applicative (Idiom cnv) => Convert0 cnv a b where
+  convert0 :: cnv -> a -> Idiom cnv b
 
 -- | The generic version of @convert@; operates on /disbanded data types/.
-class Applicative (Idiom cnv) => HCompos cnv a t where
-  hcompos :: cnv -> a -> Idiom cnv t
+class Applicative (Idiom cnv) => HCompos0 cnv a t where
+  hcompos0 :: cnv -> a p1 p0 -> Idiom cnv t
 
 
 
@@ -52,45 +53,45 @@
 -- these two instances make functions work directly for singly-recursive data
 -- types
 type instance Idiom (a -> i b) = i
-instance (Applicative i, a ~ x, b ~ y) => Convert (a -> i b) x y where convert = ($)
+instance (Applicative i, a ~ x, b ~ y) => Convert0 (a -> i b) x y where convert0 = ($)
 
 
 
 
 
-data FoundDC star = NoCorrespondingConstructorFor_In_ star star | Match star
+data FoundDC (k :: *) (l :: *) = NoCorrespondingConstructorFor_In_ k k | Match l
 
-type family WithMessage (dcA :: *) (b :: *) (dcB :: Maybe *) :: FoundDC *
+type family WithMessage (dcA :: k) (b :: k) (dcB :: Maybe l) :: FoundDC k l
 type instance WithMessage dcA b (Just x) = Match x
 type instance WithMessage dcA b Nothing  = NoCorrespondingConstructorFor_In_ dcA b
 
 
 -- | @FindDCs dcA dcBs@ returns a type-level @Maybe@. @Just dcB@ is a fields
 -- type @dcB@ where @'Tag' dcA ~ dcB@.
-type family FindDCs (s :: Digit) (dcBs :: *) :: Maybe *
+type family FindDCs (s :: Digit) (dcBs :: * -> * -> *) :: Maybe (* -> * -> *)
 type instance FindDCs s (N dc) =
-  If   (Equal s (Tag dc))   (Just dc)   Nothing
+  If   (Equal s (Tag dc))   (Just (N dc))   Nothing
 type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)
 
 
 
 
 
-instance (HCompos cnv a t, HCompos cnv b t
-         ) => HCompos cnv (a :+: b) t where
-  hcompos cnv = foldPlus (hcompos cnv) (hcompos cnv)
+instance (HCompos0 cnv a t, HCompos0 cnv b t
+         ) => HCompos0 cnv (a :+: b) t where
+  hcompos0 cnv = foldPlus (hcompos0 cnv) (hcompos0 cnv)
 
 -- NB only works if there's exactly one matching constructor
-instance (Generic dcA, Match dcB ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),
-          MapRs cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB),
+instance (Generic dcA, Match (N dcB) ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),
+          MapRs0 cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB),
           DC dcB, Codomain dcB ~ b, DT b
-         ) => HCompos cnv (N dcA) b where
-  hcompos cnv =
-    foldN $ liftA (rejoin . (id :: dcB -> dcB) . obj) . mapRs cnv msgp p1 p2 . rep
+         ) => HCompos0 cnv (N dcA) b where
+  hcompos0 cnv =
+    foldN0 $ liftA (unSym0 rejoin . (id :: dcB -> dcB) . unW'0 obj) . mapRs0 cnv msgp p1 p2 . unW0 rep
     where p1 :: Proxy dcA; p1 = Proxy; p2 :: Proxy dcB; p2 = Proxy
           msgp = ResultsInIncompatibleFields :: ResultsInIncompatibleFields dcA dcB
 
-data ResultsInIncompatibleFields (dcA :: *) (dcB :: *) = ResultsInIncompatibleFields
+data ResultsInIncompatibleFields (dcA :: k) (dcB :: k) = ResultsInIncompatibleFields
 
 
 
@@ -100,25 +101,29 @@
 
 -- | Same as @compos@ semantics, but with a generalized type and just for
 -- converting between product representations.
-class Applicative (Idiom cnv) => MapRs cnv msg dc dc' prod prod' where
-  mapRs :: cnv -> msg -> Proxy dc -> Proxy dc' -> prod -> Idiom cnv prod'
+class Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' prod prod' where
+  mapRs0 :: cnv -> msg -> Proxy dc -> Proxy dc' -> prod p1 p0 -> Idiom cnv (prod' p1 p0)
 
-instance Convert cnv a b => MapRs cnv msg dc dc' (Rec a) (Rec b) where
-  mapRs cnv _ _ _ (Rec x) = Rec <$> convert cnv x
+instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' U       U       where
+  mapRs0 _ _ _ _ = pure
 
-instance Applicative (Idiom cnv) => MapRs cnv msg dc dc' (Dep a) (Dep a) where
-  mapRs _ _ _ _ = pure
-instance Applicative (Idiom cnv) => MapRs cnv msg dc dc' U       U       where
-  mapRs _ _ _ _ = pure
+instance (MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'
+         ) => MapRs0 cnv msg dc dc' (a :*: b) (a' :*: b') where
+  mapRs0 cnv msgp p1 p2 (a :*: b) = (:*:) <$> mapRs0 cnv msgp p1 p2 a <*> mapRs0 cnv msgp p1 p2 b
 
-instance (MapRs cnv msg dc dc' a a', MapRs cnv msg dc dc' b b'
-         ) => MapRs cnv msg dc dc' (a :*: b) (a' :*: b') where
-  mapRs cnv msgp p1 p2 (a :*: b) = (:*:) <$> mapRs cnv msgp p1 p2 a <*> mapRs cnv msgp p1 p2 b
+instance MapRs0 cnv msg dc dc' a a' => MapRs0 cnv msg dc dc' (C dcA a) (C dcB a') where
+  mapRs0 cnv msgp p1 p2 (C x) = C <$> mapRs0 cnv msgp p1 p2 x
 
-instance (Traversable f, MapRs cnv msg dc dc' a a'
-         ) => MapRs cnv msg dc dc' (Par1 f a) (Par1 f a') where
-  mapRs cnv msgp p1 p2 (Par1 x) = Par1 <$> traverse (mapRs cnv msgp p1 p2) x
+instance Convert0 cnv a b => MapRs0 cnv msg dc dc' (T0 (Rec lbl) a) (T0 (Rec lbl') b) where
+  mapRs0 cnv _ _ _ (T0 x) = T0 <$> convert0 cnv x
 
-instance (Bitraversable f, MapRs cnv msg dc dc' a a', MapRs cnv msg dc dc' b b'
-         ) => MapRs cnv msg dc dc' (Par2 f a b) (Par2 f a' b') where
-  mapRs cnv msgp p1 p2 (Par2 x) = Par2 <$> bitraverse (mapRs cnv msgp p1 p2) (mapRs cnv msgp p1 p2) x
+instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' (T0 Dep a) (T0 Dep a) where
+  mapRs0 _ _ _ _ = pure
+
+instance (Traversable f, MapRs0 cnv msg dc dc' a a'
+         ) => MapRs0 cnv msg dc dc' (T1 Dep f a) (T1 Dep f a') where
+  mapRs0 cnv msgp p1 p2 (T1 x) = T1 <$> traverse (mapRs0 cnv msgp p1 p2) x
+
+instance (Bitraversable f, MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'
+         ) => MapRs0 cnv msg dc dc' (T2 Dep f a b) (T2 Dep f a' b') where
+  mapRs0 cnv msgp p1 p2 (T2 x) = T2 <$> bitraverse (mapRs0 cnv msgp p1 p2) (mapRs0 cnv msgp p1 p2) x
diff --git a/Data/Yoko/Invariant.hs b/Data/Yoko/Invariant.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Invariant.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE TypeOperators, LambdaCase, FlexibleContexts, UndecidableInstances, PolyKinds #-}
+
+module Data.Yoko.Invariant
+  (module Data.Yoko.Invariant, module Data.Functor.Invariant) where
+
+import Data.Yoko.W
+import Data.YokoRaw
+
+import Data.Functor.Invariant
+
+
+
+
+
+gen_invmap :: (Invariant2 (DCs t), DT t, AreDCsOf t (DCs t)) =>
+              (a -> b) -> (b -> a) -> t a -> t b
+gen_invmap f f' = unW'1 band . invmap2 id id f f' . unW1 disband
+
+gen_invmap2 :: (Invariant2 (DCs t), DT t, AreDCsOf t (DCs t)) =>
+               (a -> c) -> (c -> a) -> (b -> d) -> (d -> b) -> t a b -> t c d
+gen_invmap2 f f' g g' = unW'2 band . invmap2 f f' g g' . unW2 disband
+
+
+
+
+
+instance Invariant2 U where
+  invmap2 _ _ _ _ _ = U
+
+instance (Invariant2 l, Invariant2 r) => Invariant2 (l :*: r) where
+  invmap2 f f' g g' (l :*: r) = invmap2 f f' g g' l :*: invmap2 f f' g g' r
+
+instance (Invariant2 r) => Invariant2 (C dc r) where
+  invmap2 f f' g g' (C x) = C $ invmap2 f f' g g' x
+
+
+-- can optimize for * and * -> *, but I'm favoring terseness
+instance (WN dc, Invariant2 (Rep dc), Generic dc) => Invariant2 (N dc) where
+  invmap2 f f' g g'  = unSym nN obj . invmap2 f f' g g' . unSym rep unN
+
+instance (Invariant2 l, Invariant2 r) => Invariant2 (l :+: r) where
+  invmap2 f f' g g' = \case
+    L x -> L $ invmap2 f f' g g' x
+    R x -> R $ invmap2 f f' g g' x
+
+instance Invariant2 Void where invmap2 = error "invmap2 @Void"
+
+
+
+instance Invariant2 (T0 v t) where
+  invmap2 _ _ _ _ (T0 x) = T0 x
+
+instance (Invariant t, Invariant2 r) => Invariant2 (T1 v t r) where
+  invmap2 f f' g g' (T1 x) = T1 $ invmap (invmap2 f f' g g') (invmap2 f' f g' g) x
+
+instance (Invariant2 t, Invariant2 r, Invariant2 s) => Invariant2 (T2 v t r s) where
+  invmap2 f f' g g' (T2 x) = T2 $ invmap2 (invmap2 f f' g g') (invmap2 f' f g' g) (invmap2 f f' g g') (invmap2 f' f g' g) x
+
+
+
+instance Invariant2 Par1 where invmap2 f _ _ _ (Par1 x) = Par1 (f x)
+instance Invariant2 Par0 where invmap2 _ _ g _ (Par0 x) = Par0 (g x)
diff --git a/Data/Yoko/MinCtors.hs b/Data/Yoko/MinCtors.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MinCtors.hs
@@ -0,0 +1,373 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, UndecidableInstances,
+  DefaultSignatures, ViewPatterns, FlexibleContexts, FlexibleInstances,
+  PolyKinds, MultiParamTypeClasses, Rank2Types #-}
+
+module Data.Yoko.MinCtors (MinCtors(..), gen_minCtors, nCtors) where
+
+import Data.Yoko
+
+import Data.Semigroup (Min(..))
+import qualified Data.Yoko.MinCtors.MMap as MMap
+import Data.Yoko.MinCtors.Minima
+
+import Data.Monoid (mappend)
+
+import qualified GHC.Real
+
+--------------------
+-- miscellaneous
+
+pDisband :: Proxy t -> Proxy (DCs t)
+pDisband _ = Proxy
+
+pRep :: Proxy t -> Proxy (Rep t)
+pRep _ = Proxy
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+--------------------
+-- the internal classes
+
+class MinInfoRec (t :: k) (ts :: [k1]) where
+  minInfoRec :: Proxy t -> Proxy ts -> SiblingInT ts
+
+class MinInfoNonRec (t :: k) where minInfoNonRec :: Proxy t -> Minima2
+
+minima1ToSiblingInT :: VRepeat ts => Minima2 -> SiblingInT ts
+minima1ToSiblingInT =
+  MMap.mapWithMonoKeys (\(np1, np0) -> (cvRepeat 0, np1, np0)) id
+
+void :: Minima2
+void = MMap.singleton (0, 0) $ Min 0
+
+nCtors :: MinCtorsTrim t => Int -> Proxy t -> MinCtorsT t
+nCtors n p = minCtorsTrim p $ nCtors' n p
+
+nCtors' :: Int -> Proxy t -> Minima2
+nCtors' n _ = MMap.singleton (0, 0) $ Min n
+
+
+
+
+
+
+
+deApp :: Proxy (T1 v f r) -> (Proxy f, Proxy r)
+deApp _ = (Proxy, Proxy)
+
+instance (Ord (CVec ts NRec), MinCtors f, MinInfoRec r ts) => MinInfoRec (T1 Dep f r) ts where
+  minInfoRec (deApp -> (pf, pr)) pts = minCtors pf `plug0` minInfoRec pr pts
+
+instance (MinCtors f, MinInfoNonRec r) => MinInfoNonRec (T1 Dep f r) where
+  minInfoNonRec (deApp -> (pf, pr)) = minCtors pf `plug0'` minInfoNonRec pr
+
+deApp2 :: Proxy (T2 v ff r1 r0) -> (Proxy ff, Proxy r1, Proxy r0)
+deApp2 _ = (Proxy, Proxy, Proxy)
+
+instance (Ord (CVec ts NRec), MinCtors ff, MinInfoRec rB ts, MinInfoRec rA ts) => MinInfoRec (T2 Dep ff rB rA) ts where
+  minInfoRec (deApp2 -> (ff, rB, rA)) pts =
+    plug10 (minCtors ff) (minInfoRec rB pts) (minInfoRec rA pts)
+
+instance (MinCtors ff, MinInfoNonRec rB, MinInfoNonRec rA) => MinInfoNonRec (T2 Dep ff rB rA) where
+  minInfoNonRec (deApp2 -> (ff, rB, rA)) = plug10' (minCtors ff) (minInfoNonRec rB) (minInfoNonRec rA)
+
+
+
+instance (VRepeat ts) => MinInfoRec (Void t) ts where minInfoRec _ _ = minima1ToSiblingInT void
+instance MinInfoNonRec (Void t) where minInfoNonRec = nCtors' 0
+
+
+
+deN :: Proxy (N dc) -> Proxy dc
+deN _ = Proxy
+
+instance MinInfoRec (Rep dc) ts => MinInfoRec (N dc) ts where
+  minInfoRec = minInfoRec . pRep . deN
+instance MinInfoNonRec (Rep dc) => MinInfoNonRec (N dc) where
+  minInfoNonRec = minInfoNonRec . pRep . deN
+
+
+
+
+
+deC :: Proxy (C t r) -> Proxy r
+deC _ = Proxy
+
+instance MinInfoRec r ts => MinInfoRec (C dc r) ts where
+  minInfoRec = (MMap.map (fmap succ) .) . minInfoRec . deC
+instance MinInfoNonRec r => MinInfoNonRec (C dc r) where
+  minInfoNonRec = MMap.map (fmap succ) . minInfoNonRec . deC
+
+
+
+dePlus :: Proxy (l :+: r) -> (Proxy l, Proxy r)
+dePlus _ = (Proxy, Proxy)
+
+instance (Ord (CVec ts NRec), MinInfoRec l ts, MinInfoRec r ts) => MinInfoRec (l :+: r) ts where
+  minInfoRec (dePlus -> (l, r)) pts = minInfoRec l pts `mappend` minInfoRec r pts
+instance (MinInfoNonRec l, MinInfoNonRec r) => MinInfoNonRec (l :+: r) where
+  minInfoNonRec (dePlus -> (l, r)) = minInfoNonRec l `mappend` minInfoNonRec r
+
+
+
+instance MinInfoNonRec U where minInfoNonRec = nCtors' 0
+instance (VRepeat ts) => MinInfoRec U ts where minInfoRec _ _ = minima1ToSiblingInT void
+
+deTimes :: Proxy (l :*: r) -> (Proxy l, Proxy r)
+deTimes _ = (Proxy, Proxy)
+
+instance (Ord (CVec ts NRec), VRepeat ts, MinInfoRec l ts, MinInfoRec r ts) => MinInfoRec (l :*: r) ts where
+  minInfoRec (deTimes -> (l, r)) pts =
+    addSiblingInTs (minInfoRec l pts) (minInfoRec r pts)
+instance (MinInfoNonRec l, MinInfoNonRec r) => MinInfoNonRec (l :*: r) where
+  minInfoNonRec (deTimes -> (l, r)) = addMinima2 (minInfoNonRec l) (minInfoNonRec r)
+
+
+
+instance MinInfoNonRec Par1 where minInfoNonRec _ = MMap.singleton (1, 0) $ Min 0
+instance MinInfoNonRec Par0 where minInfoNonRec _ = MMap.singleton (0, 1) $ Min 0
+instance (VRepeat ts, MinInfoNonRec Par1) => MinInfoRec Par1 ts where
+  minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p
+instance (VRepeat ts, MinInfoNonRec Par0) => MinInfoRec Par0 ts where
+  minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p
+
+
+
+deRec0 :: Proxy (T0 (Rec lbl) t) -> Proxy lbl
+deRec0 _ = Proxy
+
+instance (IndexInto lbl ts, VRepeat ts) => MinInfoRec (T0 (Rec lbl) t) ts where
+  minInfoRec (deRec0 -> plbl) pts =
+    MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0
+
+deRec1 :: Proxy (T1 (Rec lbl) t r) -> Proxy lbl
+deRec1 _ = Proxy
+
+-- TODO: how to support non-regular data types?
+
+-- NB only supports regular data types for now
+instance (IndexInto lbl ts, VRepeat ts) => MinInfoRec (T1 (Rec lbl) t Par0) ts where
+  minInfoRec (deRec1 -> plbl) pts =
+    MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0
+
+deRec2 :: Proxy (T2 (Rec lbl) t r s) -> Proxy lbl
+deRec2 _ = Proxy
+
+class Regularish r s where
+  regularish :: ((r ~ Par1, s ~ Par0) => a) -> ((r ~ Par0, s ~ Par1) => a) -> a
+instance Regularish Par1 Par0 where regularish x _ = x
+instance Regularish Par0 Par1 where regularish _ y = y
+-- NB no other instances!
+
+-- NB only supports regularish data types for now
+instance (Regularish r s, IndexInto lbl ts, VRepeat ts) => MinInfoRec (T2 (Rec lbl) t r s) ts where
+  minInfoRec (deRec2 -> plbl) pts =
+    MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0
+
+
+
+deDep0 :: Proxy (T0 v t) -> Proxy t
+deDep0 _ = Proxy
+
+instance (VRepeat ts, MinInfoNonRec (T0 Dep t)) => MinInfoRec (T0 Dep t) ts where
+  minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p
+
+instance MinCtors t => MinInfoNonRec (T0 Dep t) where
+  minInfoNonRec = maybe MMap.empty (MMap.singleton (0, 0) . Min) . minCtors . deDep0
+
+
+
+
+
+pDTs :: Proxy t -> Proxy (DTs t)
+pDTs _ = Proxy
+
+class MinCtorsTrim t where minCtorsTrim :: Proxy t -> Minima2 -> MinCtorsT t
+instance MinCtorsTrim (t :: *) where
+  minCtorsTrim _ m = getMin `fmap` MMap.lookup (0, 0) m
+instance MinCtorsTrim (t :: * -> *) where
+  minCtorsTrim _ = MMap.mapWithMonoKeys (\(_, nP0) -> nP0) id
+instance MinCtorsTrim (t :: * -> * -> *) where minCtorsTrim _ = id
+
+gen_minCtors :: (MinCtorsTrim t, MinCtorsWorker t (DTs t)) => Proxy t -> MinCtorsT t
+gen_minCtors p = minCtorsTrim p $ method p (pDTs p)
+
+type family MinCtorsT (t :: k) :: *
+type instance MinCtorsT (t :: *) = Maybe Int
+type instance MinCtorsT (t :: * -> *) = Minima1
+type instance MinCtorsT (t :: * -> * -> *) = Minima2
+
+class MinCtors t where
+  minCtors :: Proxy t -> MinCtorsT t
+  default minCtors :: (MinCtorsTrim t, MinCtorsWorker t (DTs t)) => Proxy t -> MinCtorsT t
+  minCtors = gen_minCtors
+
+class MinCtorsWorker t dpos where method :: Proxy t -> Proxy dpos -> Minima2
+
+pSiblingDTs :: Proxy t -> Proxy (SiblingDTs t)
+pSiblingDTs _ = Proxy
+
+instance MinInfoNonRec (DCs t) => MinCtorsWorker t NonRecDT where method pt _ = minInfoNonRec (pDisband pt)
+
+pIndex :: Proxy (RecDT l r) -> Proxy (Length l)
+pIndex _ = Proxy
+
+instance (IndexInto (Length l) (SiblingDTs t),
+          VInitialize (MinInfo__ (SiblingDTs t)) (SiblingDTs t),
+          VFunctor (SiblingInC (SiblingDTs t)) (SiblingDTs t),
+          VRepeat (SiblingDTs t),
+          VEnum (SiblingDTs t),
+          Eq (CVec (SiblingDTs t) Minima2),
+          MinInfoRec (DCs t) (SiblingDTs t)) => MinCtorsWorker t (RecDT l r) where
+  method pt pdpos = (`cvAt` indexInto (pIndex pdpos) psibs) $ solve_sibling_set' $
+                    cvInitialize (pcon psibs) minInfo__
+    where psibs = pSiblingDTs pt
+          pcon :: Proxy ts -> Proxy (MinInfo__ ts)
+          pcon _ = Proxy
+
+class    (MinInfoRec (DCs t) ts, ts ~ SiblingDTs t) => MinInfo__ ts t
+instance (MinInfoRec (DCs t) ts, ts ~ SiblingDTs t) => MinInfo__ ts t
+
+minInfo__ :: MinInfo__ ts t => Proxy t -> SiblingInT ts
+minInfo__ p = minInfoRec (pDisband p) (pSiblingDTs p)
+
+
+
+
+
+
+
+
+
+{-
+
+-- T tests support for interesting structures as well as avoiding the recursive
+-- branch
+data T a = One a | Branch (T a, [T a]) Int
+
+yokoTH ''T
+
+
+
+
+
+-- S tests one interesting way that the final answer depends on the parameter
+data S a = OneS a | BranchS Int Int
+
+yokoTH ''S
+
+
+
+-- M1 and M2 exercise the erroneous definition for Recs
+data M1 = M1C Int Int Int Int | M1D M2
+data M2 = M2C M1
+
+yokoTH ''M1
+yokoTH ''M2
+
+
+
+
+yokoTH ''Nat
+
+
+
+data Inf = Inf Inf
+
+yokoTH ''Inf
+
+
+
+
+
+data X a = X a a a a
+
+yokoTH ''X
+
+data Y a = Y (X (X a))
+
+yokoTH ''Y
+
+
+
+data Stream a = SCons a (Stream a)
+type instance DTs Stream = RecDT '[] '[]
+
+yokoTH ''Stream
+
+data Even a = ENil | ECons a (Odd  a)
+data Odd  a =        OCons a (Even a)
+
+yokoTH ''Even
+yokoTH ''Odd
+
+
+
+
+instance MinCtors X
+instance MinCtors a => MinCtors (X a)
+
+instance MinCtors Y
+instance MinCtors a => MinCtors (Y a)
+
+instance MinCtors Stream
+instance MinCtors a => MinCtors (Stream a)
+
+instance MinCtors T
+instance MinCtors a => MinCtors (T a)
+instance MinCtors S
+instance MinCtors a => MinCtors (S a)
+instance MinCtors M1
+instance MinCtors M2
+instance MinCtors Inf
+
+instance MinCtors Nat
+
+
+instance MinCtors Even
+instance MinCtors Odd
+instance MinCtors a => MinCtors (Even a)
+instance MinCtors a => MinCtors (Odd  a)
+
+-}
+
+
+
+
+
+--------------------
+-- usages
+instance MinCtors Bool
+instance MinCtors ()
+
+instance MinCtors (,)
+instance MinCtors a => MinCtors ((,) a)
+instance (MinCtors a, MinCtors b) => MinCtors ((,) a b)
+
+instance MinCtors a => MinCtors ((,,) a)
+instance (MinCtors a, MinCtors b) => MinCtors ((,,) a b)
+instance (MinCtors a, MinCtors b, MinCtors c) => MinCtors ((,,) a b c)
+
+instance MinCtors Maybe
+instance MinCtors a => MinCtors (Maybe a)
+
+instance MinCtors []
+instance MinCtors a => MinCtors [a]
+
+instance MinCtors Either
+instance MinCtors a => MinCtors (Either a)
+instance (MinCtors a, MinCtors b) => MinCtors (Either a b)
+
+instance MinCtors GHC.Real.Ratio
+instance MinCtors a => MinCtors (GHC.Real.Ratio a)
diff --git a/Data/Yoko/MinCtors/MMap.hs b/Data/Yoko/MinCtors/MMap.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MinCtors/MMap.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
+
+-- | Like 'Map' but with a 'Monoid' instance that respects the value type's
+-- 'Semigroup' instance.
+
+module Data.Yoko.MinCtors.MMap where
+
+import Data.Monoid
+
+import Data.Semigroup (Semigroup)
+import qualified Data.Semigroup as Semigroup
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import qualified Data.Foldable as F
+
+
+
+newtype MMap k f v = MMap {unMMap :: Map k (f v)}
+
+deriving instance Eq (Map k (f v)) => Eq (MMap k f v)
+deriving instance Show (Map k (f v)) => Show (MMap k f v)
+
+map f (MMap m) = MMap $ Map.map f m
+
+singleton k v = MMap $ Map.singleton k v
+
+null (MMap m) = Map.null m
+
+empty :: MMap k f v
+empty = MMap Map.empty
+
+instance (Ord k, Semigroup (f v)) => Monoid (MMap k f v) where
+  mempty = MMap Map.empty
+  MMap x `mappend` MMap y = MMap $ Map.unionWith (Semigroup.<>) x y
+
+foldMap :: Monoid m => (k -> f v -> m) -> MMap k f v -> m
+foldMap f (MMap m) = F.foldMap (uncurry f) $ Map.toList m
+
+mapWithMonoKeys :: (k -> k1) -> (f v -> g v1) -> MMap k f v -> MMap k1 g v1
+mapWithMonoKeys fk fv (MMap m) =
+  MMap $ Map.mapKeysMonotonic fk $ Map.map fv m
+
+lookup :: Ord k => k -> MMap k f v -> Maybe (f v)
+lookup k (MMap m) = Map.lookup k m
diff --git a/Data/Yoko/MinCtors/Minima.hs b/Data/Yoko/MinCtors/Minima.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MinCtors/Minima.hs
@@ -0,0 +1,165 @@
+{-# LANGUAGE ScopedTypeVariables, PolyKinds, DataKinds, MultiParamTypeClasses,
+  TypeFamilies, UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
+
+module Data.Yoko.MinCtors.Minima
+  (NCtor, NRec, NP1, NP0, Minima2, Minima1, Minimum,
+   DTsCVec, SumInfo, SC_SumInfo,
+   SiblingInT, SiblingInC, addMinima2, addSiblingInTs,
+   solve_sibling_set, solve_sibling_set',
+   plug10, plug0, plug10', plug0') where
+
+import Data.Yoko.TypeBasics
+
+import Data.Yoko.View
+
+import Data.Yoko.MinCtors.MMap (MMap)
+import qualified Data.Yoko.MinCtors.MMap as MMap
+
+import qualified Data.Foldable as F
+
+import Data.Semigroup (Min(..))
+
+import Data.Traversable (traverse)
+import Data.Maybe (catMaybes)
+
+
+
+instance Functor Min where fmap f (Min a) = Min (f a)
+
+
+
+--------------------
+-- an appropriate abstraction for the MinCtors question
+type NCtor = Int
+type NRec  = Int
+type NP1   = Int
+type NP0   = Int
+
+type Minima2 = MMap (NP1, NP0) Min NCtor
+type Minima1 = MMap NP0        Min NCtor
+type Minimum = MMap ()         Min NCtor
+
+-- scale each coordinate
+scale :: Int -> Minima2 -> Minima2
+scale i = MMap.mapWithMonoKeys (\(np1, np0) -> (i * np1, i * np0)) (fmap (i *))
+
+-- take Cartesian product, add coordinates point-wise, and re\"normalize\"
+addMinima2 :: Minima2 -> Minima2 -> Minima2
+addMinima2 m m' = flip MMap.foldMap m $ \(np1, np0) (Min k) ->
+  flip MMap.foldMap m' $ \(np1', np0') (Min k') ->
+    MMap.singleton (np1 + np1', np0 + np0') (Min $ k + k')
+
+-- product and sum info
+type DTsCVec t = CVec (SiblingDTs t)
+
+type SumInfo t = MMap (DTsCVec t NRec, NP1, NP0) Min NCtor
+
+scaleSiblingInTs :: Int -> SiblingInT ts -> SiblingInT ts
+scaleSiblingInTs i = MMap.mapWithMonoKeys (\(r, np1, np0) -> (fmap (i *) r, i * np1, i * np0)) (fmap (i *))
+
+addSiblingInTs :: Ord (CVec ts NRec) => SiblingInT ts -> SiblingInT ts -> SiblingInT ts
+addSiblingInTs m m' = flip MMap.foldMap m $ \(rs, np1, np0) (Min k) ->
+  flip MMap.foldMap m' $ \(rs', np1', np0') (Min k') ->
+    MMap.singleton (cvZipWith (+) rs rs', np1 + np1', np0 + np0') (Min $ k + k')
+
+
+
+
+
+--------------------
+-- solve a sibling set
+
+-- let cnv x = ($ x) $ MMap . Map.fromList . map (\(recs, np1, np0, k) -> ((recs, np1, np0), k))
+
+-- TODO Put an interface around 'solve' so it can also be applied to
+-- non-recursive data types -- this might involve a token type representing the
+-- entire "sibling set", even for non-recursive types
+
+-- TODO how to memoize the sibling set analysis as a CAF with all siblings'
+-- MinCtors dictionaries sharing the CAF's elements?
+
+-- | @type instance 'App' SC_SumInfo t = 'SumInfo' t@
+data SC_SumInfo t = SC_SumInfo
+type instance App SC_SumInfo t = SumInfo t
+
+solve_sibling_set ::
+  (Eq (CVec ts Minima2), VRepeat ts,
+   VFunctor (SiblingInC ts) ts, VEnum ts) => Vec ts SC_SumInfo -> Work ts
+solve_sibling_set = solve_sibling_set' . homogenize
+
+solve_sibling_set' ::
+  (Eq (CVec ts Minima2), VRepeat ts, VEnum ts) => CVec ts (SiblingInT ts) -> Work ts
+solve_sibling_set' table = chaotic (step table) $ initialize table
+
+-- 1) start with the smallest non-recursive ctors
+
+-- 2) build up only from those, so we're maintaining a correct answer the
+-- entire time
+
+-- 3) codata siblings end up as MMap.empty.
+
+-- the work set holds the sofar determined answers -- only the ones that are
+-- gauranteed to be minimal. Codata siblings never get changed from MMap.empty.
+type Work ts = CVec ts Minima2
+
+-- like SC_SumInfo except parameterized over the sibling set instead of just a
+-- single sibling
+type SiblingInT ts = MMap (CVec ts NRec, NP1, NP0) Min NCtor
+
+-- switch to a 'CVec', since all of the 'DTs' instances are compatible...
+homogenize :: forall ts. VFunctor (SiblingInC ts) ts =>
+              Vec ts SC_SumInfo -> CVec ts (SiblingInT ts)
+homogenize = (CVec .) $ vMap (Proxy :: Proxy (SiblingInC ts)) $ \_ -> id
+
+-- ...in this way
+class    (ts ~ SiblingDTs t) => SiblingInC (ts :: [k]) (t :: k)
+instance (ts ~ SiblingDTs t) => SiblingInC  ts          t
+
+-- the initial work set is the siblings' smallest non-recursive constructors
+initialize :: CVec ts (SiblingInT ts) -> Work ts
+initialize = fmap $ \ctors -> flip MMap.foldMap ctors $ \(recs, np1, np0) k ->
+  if F.all (0 ==) recs -- non-recursive ctor iff no recursive occurrences
+  then MMap.singleton (np1, np0) k
+  else MMap.empty
+
+-- extend the working set with the unsolved siblings that are now soluble
+step :: VEnum ts => CVec ts (SiblingInT ts) -> Work ts -> Work ts
+step table sofar = cvZipWith leftbias sofar $ flip fmap table $
+  MMap.foldMap $ \(recs, np1, np0) k -> -- fold over products in this sibling
+    -- if all of its non-zero NRecs are solved...
+    let all_answered = flip traverse (cvAddIndexes recs) $ \(idx, times) ->
+          if times <= 0 then Just Nothing -- omit without failing
+          else let answer = sofar `cvAt` idx
+               in if MMap.null answer then Nothing -- fail
+                  else Just $ Just $ scale times answer -- emit
+    in ($ all_answered) $ maybe MMap.empty $
+         foldl addMinima2 (MMap.singleton (np1, np0) k) . catMaybes . cvec2list
+
+leftbias m1 m2 = if MMap.null m1 then m2 else m1
+
+-- rinse and repeat until clean
+chaotic :: Eq a => (a -> a) -> a -> a
+chaotic f = w where w x = let x' = f x in if x == x' then x else w x'
+
+
+
+
+
+--------------------
+-- combining minima
+
+plug0 :: Ord (CVec ts NRec) => Minima1 -> SiblingInT ts -> SiblingInT ts
+plug0 f s0 = flip MMap.foldMap f $ \np0 (Min k) ->
+  MMap.map (fmap (+k)) $ scaleSiblingInTs np0 s0
+
+plug10 :: Ord (CVec ts NRec) => Minima2 -> SiblingInT ts -> SiblingInT ts -> SiblingInT ts
+plug10 f s1 s0 = flip MMap.foldMap f $ \(np1, np0) (Min k) ->
+  MMap.map (fmap (+k)) $ scaleSiblingInTs np1 s1 `addSiblingInTs` scaleSiblingInTs np0 s0
+
+plug0' :: Minima1 -> Minima2 -> Minima2
+plug0' f s0 = flip MMap.foldMap f $ \np0 (Min k) ->
+  MMap.map (fmap (+k)) $ scale np0 s0
+
+plug10' :: Minima2 -> Minima2 -> Minima2 -> Minima2
+plug10' f s1 s0 = flip MMap.foldMap f $ \(np1, np0) (Min k) ->
+  MMap.map (fmap (+k)) $ scale np1 s1 `addMinima2` scale np0 s0
diff --git a/Data/Yoko/MinCtors/Prims0.hs b/Data/Yoko/MinCtors/Prims0.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MinCtors/Prims0.hs
@@ -0,0 +1,16 @@
+module Data.Yoko.MinCtors.Prims0 where
+
+import qualified GHC.Word
+import qualified GHC.ForeignPtr
+
+import Data.Yoko.MinCtors
+
+
+
+instance MinCtors Int     where minCtors = nCtors 0
+instance MinCtors Integer where minCtors = nCtors 0
+instance MinCtors Char    where minCtors = nCtors 0
+instance MinCtors Float   where minCtors = nCtors 0
+instance MinCtors Double  where minCtors = nCtors 0
+instance MinCtors GHC.Word.Word8 where minCtors = nCtors 0
+instance MinCtors GHC.ForeignPtr.ForeignPtr where minCtors = nCtors 0
diff --git a/Data/Yoko/MinCtors/Prims1.hs b/Data/Yoko/MinCtors/Prims1.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MinCtors/Prims1.hs
@@ -0,0 +1,16 @@
+module Data.Yoko.MinCtors.Prims1 where
+
+import qualified GHC.Word
+import qualified GHC.ForeignPtr
+
+import Data.Yoko.MinCtors
+
+
+
+instance MinCtors Int     where minCtors = nCtors 1
+instance MinCtors Integer where minCtors = nCtors 1
+instance MinCtors Char    where minCtors = nCtors 1
+instance MinCtors Float   where minCtors = nCtors 1
+instance MinCtors Double  where minCtors = nCtors 1
+instance MinCtors GHC.Word.Word8 where minCtors = nCtors 1
+instance MinCtors GHC.ForeignPtr.ForeignPtr where minCtors = nCtors 1
diff --git a/Data/Yoko/Prelude.hs b/Data/Yoko/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Prelude.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators,
+  UndecidableInstances, DataKinds, LambdaCase #-}
+
+module Data.Yoko.Prelude where
+
+import qualified GHC.Real
+
+import Data.Yoko.TH
+import Data.Yoko.W
+import Data.YokoRaw
+
+import Type.Spine (spineType_d)
+import Type.Serialize (serializeTypeAsHash_data)
+
+
+yokoTH ''Bool
+
+
+yokoTH ''()
+
+type instance DTs (,,) = NonRecDT
+
+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''GHC.Real.Ratio
+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''(,)
+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''(,,)
+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''Maybe
+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''Either
+
+data Nil_  (p0 :: *) = Nil_
+data Cons_ (p0 :: *) = Cons_ p0 [p0]
+
+spineType_d ''Nil_
+spineType_d ''Cons_
+
+serializeTypeAsHash_data ''Nil_
+serializeTypeAsHash_data ''Cons_
+
+type instance Codomain Nil_  = []
+type instance Codomain Cons_ = []
+
+type instance Codomain (Nil_ a)  = [a]
+type instance Codomain (Cons_ a) = [a]
+
+type instance Rep (Nil_ a)  = Subst0 Nil_ a
+instance Generic (Nil_ a) where
+  rep = W0  $ \_ -> C U
+  obj = W'0 $ \_ -> Nil_
+
+type instance Rep Nil_  = C Nil_ U
+instance Generic Nil_ where
+  rep = W1  $ \_ -> C U
+  obj = W'1 $ \_ -> Nil_
+
+type instance Rep (Cons_ a) = Subst0 Cons_ a
+instance Generic (Cons_ a) where
+  rep = W0  $ \(Cons_ a as)         -> C (T0 a :*: T0 as)
+  obj = W'0 $ \(C (T0 a :*: T0 as)) -> Cons_ a as
+
+type instance Rep Cons_ = C Cons_ (Par0 :*: T1 (Rec 'Z) [] Par0)
+instance Generic Cons_ where
+  rep = W1  $ \(Cons_ a as)           -> C (Par0 a :*: T1 (map Par0 as))
+  obj = W'1 $ \(C (Par0 a :*: T1 as)) -> Cons_ a (map unPar0 as)
+
+type instance DTs []  = RecDT '[] '[]
+type instance DCs []  = N Nil_     :+: N Cons_
+type instance DTs [a] = RecDT '[] '[]
+type instance DCs [a] = N (Nil_ a) :+: N (Cons_ a)
+
+instance (EQ ~ SpineCompare a a) => DT [a] where
+  disband = W0 $ \case
+    []     -> L $ N0 $ Nil_
+    a : as -> R $ N0 $ Cons_ a as
+
+instance DT [] where
+  disband = W1 $ \case
+    []     -> L $ N1 $ Nil_
+    a : as -> R $ N1 $ Cons_ a as
diff --git a/Data/Yoko/Representation.hs b/Data/Yoko/Representation.hs
--- a/Data/Yoko/Representation.hs
+++ b/Data/Yoko/Representation.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, TemplateHaskell,
-  UndecidableInstances, EmptyDataDecls, DataKinds #-}
+  UndecidableInstances, EmptyDataDecls, DataKinds, PolyKinds,
+  MultiParamTypeClasses, FlexibleInstances #-}
 
 {- |
 
@@ -19,88 +20,143 @@
   (-- * Representation
    -- ** Sums
    Void(..), N(..), (:+:)(..),
+   C(..),
    -- ** Products
    U(..), (:*:)(..),
    -- ** Fields
-   Rec(..), Dep(..), Par1(..), Par2(..),
+   T0(..), T1(..), T2(..), Variety(..),
+   Par1(..), Par0(..),
    -- ** Conversions to and from fields-of-products structure
    Rep, Generic(..),
    -- ** Auxilliaries
-   unN, foldN, mapN,
-   foldPlus, mapPlus,
+   unC, foldC, mapC,
+   WN(..),
+   unN0, foldN0, mapN0,
+   unN1, foldN1, mapN1,
+   unN2, foldN2, mapN2,
+   foldPlus, FoldPlusW'(..), mapPlus,
    foldTimes, mapTimes,
-   unRec, mapRec, unDep, unPar1, unPar2,
+   unT0, mapT0,
+   unT1, mapT1,
+   unT2, mapT2,
+   unPar0, mapPar0,
+   unPar1, mapPar1,
    DistMaybePlus
    ) where
 
+import Data.Yoko.W
 import Data.Yoko.TypeBasics
 
 
 
+data Variety = Rec Nat | Dep
+
+
+
+-- | Wrapper around productus
+newtype C dc r (p1 :: *) (p0 :: *) = C (r p1 p0)
+
 -- | The empty product.
-data U = U
+data U (p1 :: *) (p0 :: *) = U
 
 infixr 6 :*:
 -- | Product union.
-data a :*: b = a :*: b
+data (:*:) a b (p1 :: *) (p0 :: *) = a p1 p0 :*: b p1 p0
 
 -- | The empty sum. Used as an error type instead of a represention type, since
 -- data types with no constructors are uninteresting from a generic programming
 -- perspective -- there's just not much to be done generically.
-data Void
+data Void (p1 :: *) (p0 :: *)
 
 -- | The singleton sum.
-newtype N a = N a
+data family N (dc :: k) :: * -> * -> *
+newtype instance N dc (p1 :: *) (p0 :: *) = N0  dc
+newtype instance N dc (p1 :: *) (p0 :: *) = N1 (dc    p0)
+newtype instance N dc (p1 :: *) (p0 :: *) = N2 (dc p1 p0)
 
 infixl 6 :+:
 -- | Sum union.
-data a :+: b = L a | R b deriving (Eq, Show, Ord, Read)
+data (:+:) a b (p1 :: *) (p0 :: *) = L (a p1 p0) | R (b p1 p0) deriving (Eq, Show, Ord, Read)
 
 
--- | Representation of unary type application. @f@ is a genuine @*->*@ type,
--- not a representation. @a@ is a representation.
-newtype Par1 f a = Par1 (f a)
 
--- | Representation of binary type application. @f@ is a genuine @*->*->*@
--- type, not a representation. @a@ and @b@ are representations.
-newtype Par2 f a b = Par2 (f a b)
+-- | An occurrence of the 1st parameter.
+newtype Par1 (p1 :: *) (p0 :: *) = Par1 p1
 
+-- | An occurrence of the zeroth parameter.
+newtype Par0 (p1 :: *) (p0 :: *) = Par0 p0
 
--- | A non-recursive occurrence.
-newtype Dep a = Dep a
 
--- | A recursive occurrence.
-newtype Rec a = Rec a
 
+newtype T0 (v :: Variety) t                      (p1 :: *) (p0 :: *) = T0  t
+newtype T1 (v :: Variety) (t :: * -> *)        a (p1 :: *) (p0 :: *) = T1 (t           (a p1 p0))
+newtype T2 (v :: Variety) (t :: * -> * -> *) b a (p1 :: *) (p0 :: *) = T2 (t (b p1 p0) (a p1 p0))
 
 
+
 -- | A mapping to the structural representation of a fields type: just products
 -- of fields, no sums -- fields types have just one constructor.
-type family Rep a
+type family Rep (t :: k) :: * -> * -> *
 
 
 
 -- | Converts between a fields type and its product-of-fields structure.
-class Generic a where rep :: a -> Rep a; obj :: Rep a -> a
+class Generic dc where
+  rep :: W dc (Rep dc) p1 p0; obj :: W' dc (Rep dc) p1 p0
 
 
 
-unDep (Dep x) = x
 
-unRec (Rec x) = x
-mapRec f (Rec x) = Rec (f x)
+class ComposeW dc => WN dc where
+  nN  :: W  dc (N dc) p1 p0
+  unN :: W' dc (N dc) p1 p0
+instance WN (dc :: *)           where nN = W0 N0; unN = W'0 unN0
+instance WN (dc :: * -> *)      where nN = W1 N1; unN = W'1 unN1
+instance WN (dc :: * -> * -> *) where nN = W2 N2; unN = W'2 unN2
 
+unT0 (T0 x) = x
+mapT0 f (T0 x) = T0 (f x)
+
+unT1 (T1 x) = x
+mapT1 f (T1 x) = T1 (f x)
+
+unT2 (T2 x) = x
+mapT2 f (T2 x) = T2 (f x)
+
+unPar0 (Par0 x) = x
+mapPar0 f (Par0 x) = Par0 (f x)
+
 unPar1 (Par1 x) = x
-unPar2 (Par2 x) = x
+mapPar1 f (Par1 x) = Par1 (f x)
 
-unN (N x) = x
-foldN f = f . unN
 
-mapN f = N . foldN f
 
+unC (C x) = x
+foldC f = f . unC
+mapC f = foldC (C . f)
+
+unN0 (N0 x) = x
+foldN0 f = f . unN0
+
+unN1 (N1 x) = x
+foldN1 f = f . unN1
+
+unN2 (N2 x) = x
+foldN2 f = f . unN2
+
+mapN0 f = N0 . foldN0 f
+mapN1 f = N1 . foldN1 f
+mapN2 f = N2 . foldN2 f
+
 foldPlus f g x = case x of
   L x -> f x   ;   R x -> g x
 
+class FoldPlusW' (s :: k) where
+  foldPlusW' :: W' s l p1 p0 -> W' s r p1 p0 -> W' s (l :+: r) p1 p0
+instance FoldPlusW' (s :: *) where foldPlusW' (W'0 f) (W'0 g) = W'0 $ foldPlus f g
+instance FoldPlusW' (s :: * -> *) where foldPlusW' (W'1 f) (W'1 g) = W'1 $ foldPlus f g
+instance FoldPlusW' (s :: * -> * -> *) where foldPlusW' (W'2 f) (W'2 g) = W'2 $ foldPlus f g
+
 mapPlus f g = foldPlus (L . f) (R . g)
 
 mapTimes f g (a :*: b) = f a :*: g b
@@ -112,26 +168,28 @@
 -- | We avoid empty sums with a type-level @Maybe@. @DistMaybePlus@ performs
 -- sum union on lifted sums, only introducing @:+:@ when both arguments are
 -- @Just@s.
-type family DistMaybePlus (a :: Maybe *) (b :: Maybe *) :: Maybe *
+type family DistMaybePlus (a :: Maybe (* -> * -> *)) (b :: Maybe (* -> * -> *)) :: Maybe (* -> * -> *)
 type instance DistMaybePlus Nothing b = b
 type instance DistMaybePlus (Just a) Nothing = Just a
 type instance DistMaybePlus (Just a) (Just b) = Just (a :+: b)
 
 
-
-data Z; data S n
-type family Add n m
+{-
+data Nat = Z | S Nat
+type family Add (n :: Nat) (m :: Nat) :: Nat
 type instance Add Z m = m
 type instance Add (S n) m = S (Add n m)
 
-type family CountRs rep
+type family CountRs (rep :: * -> * -> *) :: Nat
 type instance CountRs (Dep a) = Z
 type instance CountRs (Rec a) = S Z
 type instance CountRs U = Z
 type instance CountRs (a :*: b) = Add (CountRs a) (CountRs b)
+-}
 
 
 
 
 
-concat `fmap` mapM derive_data [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]
+concat `fmap` mapM derive_data [''Variety, ''T0, ''T1, ''T2, ''Par1, ''Par0, ''C, ''U, ''(:*:), ''N, ''(:+:)]
+concat `fmap` mapM derive_pro ['Rec, 'Dep, 'Z, 'S]
diff --git a/Data/Yoko/SmartPreciseCase.hs b/Data/Yoko/SmartPreciseCase.hs
--- a/Data/Yoko/SmartPreciseCase.hs
+++ b/Data/Yoko/SmartPreciseCase.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances, Rank2Types #-}
 
 {- |
 
@@ -25,16 +25,16 @@
 
 -}
 
-module Data.Yoko.SmartPreciseCase where
+module Data.Yoko.SmartPreciseCase (precise_case0, Default(..)) where
 
-import Data.YokoRaw hiding (precise_case)
+import Data.YokoRaw hiding (precise_case0)
 import qualified Data.YokoRaw as Raw
 
 
 class Error_precise_case_requires_at_least_1_special_case a
 
-data AdHoc dcs dt r = AdHoc dt (dcs -> r)
-newtype Default a = Default a
+data AdHoc dcs dt r = AdHoc dt (forall p1 p0. dcs p1 p0 -> r)
+newtype Default a r = Default (forall p1 p0. a p1 p0 -> r)
 
 
 
@@ -43,7 +43,7 @@
 class Builder adhoc bldr where
   precise_case_ :: adhoc -> bldr
 
-instance Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a -> b) where
+instance Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a final -> b) where
   precise_case_ = error "precise_case_ requires at least 1 special case"
 
 newtype Start dt = Start dt
@@ -53,20 +53,20 @@
   Builder (Start dt) ((dc -> r) -> bldr) where
   precise_case_ (Start dt) f = precise_case_ $ AdHoc dt $ one f
 
-instance (dt ~ Codomain dc, dt ~ Codomain dcs, r ~ r', -- False ~ Elem dc dcs,
+instance (dt ~ Codomain dc, dt ~ Codomain0 dcs, r ~ r', -- False ~ Elem dc dcs,
           Builder (AdHoc (dcs :+: N dc) dt r) bldr) =>
   Builder (AdHoc dcs dt r) ((dc -> r') -> bldr) where
   precise_case_ (AdHoc dt adhoc) f = precise_case_ $ AdHoc dt $ adhoc ||. f
 
-instance (DT dt, dt ~ Codomain dcs, dt ~ Codomain (DCs dt),
+instance (DT dt, dt ~ Codomain0 dcs, dt ~ Codomain0 (DCs dt),
           Partition (DCs dt) dcs (DCs dt :-: dcs),
-          x ~ (DCs dt :-: dcs -> r),
-          final ~ r) =>
-  Builder (AdHoc dcs dt r) (Default x -> final) where
-  precise_case_ (AdHoc dt adhoc) (Default dflt) = Raw.precise_case dflt dt adhoc
+          x ~ (DCs dt :-: dcs),
+          final ~ r, final' ~ r) =>
+  Builder (AdHoc dcs dt r) (Default x final -> final') where
+  precise_case_ (AdHoc dt adhoc) (Default dflt) = Raw.precise_case0 dflt dt adhoc
 
-precise_case :: Builder (Start dt) bldr => dt -> bldr
-precise_case = precise_case_ . Start
+precise_case0 :: Builder (Start dt) bldr => dt -> bldr
+precise_case0 = precise_case_ . Start
 
 
 
diff --git a/Data/Yoko/TH.hs b/Data/Yoko/TH.hs
--- a/Data/Yoko/TH.hs
+++ b/Data/Yoko/TH.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards, DataKinds #-}
+{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards,
+  DataKinds, LambdaCase #-}
 
 {- |
 
@@ -21,7 +22,7 @@
 
 Each 'Mapping' specifies a representation type, its constructor, and a
 structure-preserving mapping function. The default options handle applications
-of @*->*@ and @*->*->*@ types with the 'Par1' and 'Par2' types from
+of @*->*@ and @*->*->*@ types with the 'T1' and 'T2' types from
 "Data.Yoko.Representation" and uses the 'invmap' and 'invmap2' mapping
 functions from the @invariant@ package.
 
@@ -29,7 +30,7 @@
 is applied at kind @*->*->*@. It can, however handle @data U = C0 | C1 (Int, U,
 U)@, since @(,,) Int@ is applied at kind @*->*->*@ -- the kind of the
 application is determined by the leftmost argument with a recursive
-occurrence. In this case, @yokoTH@ uses the default @Mapping ''Par2 'Par2
+occurrence. In this case, @yokoTH@ uses the default @Mapping ''T2 'T2
 'invmap2@.
 
 The following invocation of @yokoTH_with@ can handle @T@, since it provides an
@@ -66,10 +67,13 @@
 import Type.Serialize (serializeTypeAsHash_data)
 import qualified Type.Ord as Ord
 
-import Data.Yoko.TypeBasics (encode)
+import Data.Yoko.TypeBasics (encode, Nat(..))
+import Data.Yoko.W
 import Data.Yoko.Representation
 import Data.Yoko.View
 
+import Data.Yoko.Invariant
+
 import Language.Haskell.TH as TH hiding (Codomain)
 import Language.Haskell.TH.Syntax as TH hiding (Codomain)
 import qualified Language.Haskell.TH.SCCs as SCCs
@@ -77,17 +81,20 @@
 import qualified Data.Yoko.TH.Internal as Int
 import Data.Yoko.TH.Internal (tvbName, peelApp, peelAppAcc, expandSyn)
 
-import Data.Functor.Invariant (invmap, invmap2)
-
 import qualified Control.Monad.Writer as Writer
 import qualified Control.Monad.Trans as Trans
+import Control.Monad (liftM, when, foldM)
 
 import qualified Control.Arrow as Arrow
 
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
 import qualified Data.List as List
 
+import Data.Maybe (catMaybes)
+
 import Data.Kind (KindStar(..))
 import Data.TypeFun
 import Data.Record hiding (convert, Name)
@@ -98,32 +105,50 @@
 
 
 
+w0' :: (t p1 p0 -> s      ) -> W' s t p1 p0; w0' = W'0
+w1' :: (t p1 p0 -> s    p0) -> W' s t p1 p0; w1' = W'1
+w2' :: (t p1 p0 -> s p1 p0) -> W' s t p1 p0; w2' = W'2
 
+
+
+
+
 convert r = R.convert $ R.withStyle r (Id KindStar)
 
-data Target = Target deriving Show
-data Renamer = Renamer deriving Show
+data Target   = Target   deriving Show
+data Renamer  = Renamer  deriving Show
 data Mappings = Mappings deriving Show
+data InvInsts = InvInsts deriving Show
+data DCInsts = DCInsts deriving Show
 data BindingGroup = BindingGroup deriving Show
-data TargetData = TargetData deriving Show
-data TargetType = TargetType deriving Show
-data TargetKind = TargetKind deriving Show
-instance R.Name Target where name = Target
-instance R.Name Renamer where name = Renamer
+data TargetData   = TargetData   deriving Show
+data TargetType   = TargetType   deriving Show
+data TargetCxt    = TargetCxt    deriving Show
+data TargetTVBs   = TargetTVBs   deriving Show
+data TargetPars   = TargetPars   deriving Show
+data ConName      = ConName      deriving Show
+data ConFields    = ConFields    deriving Show
+instance R.Name Target   where name = Target
+instance R.Name Renamer  where name = Renamer
 instance R.Name Mappings where name = Mappings
+instance R.Name InvInsts where name = InvInsts
+instance R.Name DCInsts  where name = DCInsts
 instance R.Name BindingGroup where name = BindingGroup
-instance R.Name TargetData where name = TargetData
-instance R.Name TargetType where name = TargetType
-instance R.Name TargetKind where name = TargetKind
+instance R.Name TargetData   where name = TargetData
+instance R.Name TargetType   where name = TargetType
+instance R.Name TargetCxt    where name = TargetCxt
+instance R.Name TargetTVBs   where name = TargetTVBs
+instance R.Name TargetPars   where name = TargetPars
+instance R.Name ConName      where name = ConName
+instance R.Name ConFields    where name = ConFields
 
 
 
 -- | A 'Mapping' identifies the representation type, its constructor, and the
--- associated mapping function. For example, 'Par1' is represented with
--- @Mapping ''Par1 'Par1 'invmap@.
+-- associated mapping function. For example, 'T1' is represented with @Mapping
+-- ''T1 'T1 'invmap@.
 data Mapping = Mapping
-  {containerTypeName :: Name, containerCtor :: Name,
-   methodName :: Name}
+  {containerTypeName :: Name, containerCtor :: Name, methodName :: Name}
 
 -- | The default @yoko@ derivations can be customised.
 data YokoOptions = YokoOptions
@@ -131,12 +156,19 @@
     -- @(++ \"_\")@.
    renamer :: (String -> String) -> (String -> String),
     -- | How applications of higher-rank data types are represented. Defaults
-    -- to @[(1, 'Mapping' ''Par1 'Par1 'invmap), (2, 'Mapping' ''Par2 'Par2 'invmap2)]@.
-   mappings :: [(Int, Mapping)] -> [(Int, Mapping)]}
+    -- to @[(1, 'Mapping' ''T1 'T1 'invmap), (2, 'Mapping' ''T2 'T2
+    -- 'invmap2)]@.
+   mappings :: [(Int, Mapping)] -> [(Int, Mapping)],
+    -- | Should instances of 'Invariant' also be automatically derived for this
+    -- type? Defaults to @True@.
+   invInsts :: Bool -> Bool,
+    -- | For which constructors should instances of 'Rep' and 'Generic' be
+    -- automatically derived? Defaults to the set of all constructors.
+   dcInsts :: [Name] -> [Name]}
 
--- | The default options. @yokoDefaults = YokoOptions id id@.
+-- | The default options. @yokoDefaults = YokoOptions id id id@.
 yokoDefaults :: YokoOptions
-yokoDefaults = YokoOptions id id
+yokoDefaults = YokoOptions id id id id
 
 type M r = Writer.WriterT [Dec] Q
 
@@ -151,6 +183,11 @@
 
 
 
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f = liftM concat . mapM f
+
+
+
 -- | Derive fields types and all @yoko@ instances for a given data type.
 yokoTH :: Name -> Q [Dec]
 yokoTH n = yokoTH_with yokoDefaults n
@@ -159,36 +196,34 @@
 yokoTH_with :: YokoOptions -> Name -> Q [Dec]
 yokoTH_with options n = runM $ yoko0 $ X :&
   Target := n :& Renamer := (mkName . renamer options (++ "_") . TH.nameBase)
-         :& Mappings := mappings options [(1, Mapping ''Par1 'Par1 'invmap),
-                                          (2, Mapping ''Par2 'Par2 'invmap2)]
+         :& Mappings := mappings options [(1, Mapping ''T1 'T1 'invmap),
+                                          (2, Mapping ''T2 'T2 'invmap2)]
+         :& InvInsts := invInsts options True
+         :& DCInsts := dcInsts options
 
 
 
 
 -- gather reflective information about the target type
 yoko0 r@(convert -> X :& Target := n) = do
-  names <- liftQ $ SCCs.binding_group n
-  datatype@(Int.DataType tvbs _) <- liftQ $ Int.dataType n
-
-  let ty = applyConT2TVBs n tvbs
+  datatype <- liftQ $ Int.dataType n
 
-  -- get the kind of the target type; each fields type has the same kind
-  cxt <- flip mapM tvbs $ \tvb -> liftQ $
-    EqualP (PromotedT 'EQ) `fmap` do
-      let tv = [t| Spine $(return $ tvbType tvb) |]
-      [t| Ord.Compare $tv $tv |]
+  scc      <- do
+    scc <- liftQ $ SCCs.scc n
+    case scc of
+      Left n   -> return $ Left n
+      Right ns -> fmap (Right . fst) $ foldM snoc (Map.empty, 0) $ Set.toAscList ns
+        where snoc (m, acc) n = liftQ (reify n) >>= return . \case
+                TyConI TySynD{} -> (Map.insert n Nothing    m, acc)
+                _               -> (Map.insert n (Just acc) m, acc + 1)
 
-  yoko1 $ r :&
-    BindingGroup := names :&
-    TargetData := datatype :&
-    TargetType := ty :&
-    TargetKind := (map tvbKind tvbs, cxt)
+  yoko1 $ r :& TargetData := datatype :& BindingGroup := scc
 
 -- generate fields types
 conName :: Con -> Name
-conName (NormalC n _) = n
-conName (RecC n _) = n
-conName (InfixC _ n _) = n
+conName (NormalC  n _)  = n
+conName (RecC     n _)  = n
+conName (InfixC _ n _)  = n
 conName (ForallC _ _ c) = conName c
 
 renameCon :: (Name -> Name) -> Con -> Con
@@ -204,6 +239,12 @@
 tvbType :: TyVarBndr -> Type
 tvbType = VarT . tvbName
 
+compose :: Exp -> Exp -> Exp
+compose l r = VarE '(.) `AppE` l `AppE` r
+
+postConE :: Name -> Exp -> Exp
+postConE n inj = compose (ConE n) inj
+
 applyConT2TVBs :: Name -> [TyVarBndr] -> Type
 applyConT2TVBs n tvbs = foldl ((. tvbType) . AppT) (ConT n) tvbs
 
@@ -218,145 +259,263 @@
                    foldl ((. VarE) . AppE) (ConE ne) ns) where
   ns = [ mkName $ "x" ++ show i | i <- [0..k - 1] ]
 
-simpleClause pats exp = Clause pats (NormalB exp) []
+simpleVal n exp = ValD (VarP n) (NormalB exp) []
 
 halves :: [a] -> b -> (b -> b -> b) -> (a -> b) -> b
-halves as nil app each = w (length as) as where
+halves as nil appnd single = w (length as) as where
   w _ []  = nil
-  w _ [a] = each a
-  w k as  = w lk l `app` w rk r
+  w _ [a] = single a
+  w k as  = w lk l `appnd` w rk r
     where lk = k `div` 2   ;   rk = k - lk
           (l, r) = List.splitAt lk as
 
+toNat 0 = PromotedT 'Z
+toNat n = PromotedT 'S `AppT` toNat (n - 1)
+
 data FieldRO = FieldRO {repF :: Exp, objF :: Exp}
 
-fieldRO :: [(Int, Mapping)] -> Set Name -> Type -> Q (Type, FieldRO)
-fieldRO maps bg = w' where
+namesIn :: Type -> Set Name
+namesIn (ForallT tvbs _ ty) = namesIn ty `Set.difference` Set.fromList (map tvbName tvbs)
+namesIn (AppT ty1 ty2) = namesIn ty1 `Set.union` namesIn ty2
+namesIn (SigT ty _) = namesIn ty
+namesIn (VarT n) = Set.singleton n
+namesIn (ConT n) = Set.singleton n
+namesIn _ = Set.empty
+
+fieldRO :: [(Int, Mapping)] -> Either Name (Map Name (Maybe Int)) ->
+           [Name] -> -- just the represented parameters (ie Par1 and Par0)
+           Type -> Q (Type, FieldRO)
+fieldRO maps bg parNs = w' where
   w' = uncurry w . peelApp
 
-  isRec n = Set.member n bg
+  isRec = case bg of
+    Left _   -> const False
+    Right bg -> \n -> Map.member n bg
+  isPar n = n `elem` parNs
+  isImportant n = isRec n || isPar n
 
-  simple b ty tys = return $ (ConT tyn `AppT` foldl AppT ty tys,
-    if b then FieldRO (ConE 'Rec) (VarE 'unRec)
-         else FieldRO (ConE 'Dep) (VarE 'unDep))
-    where tyn = if b then ''Rec else ''Dep
+  (nRecTy, nRecCtor) = case length parNs of
+    0 -> (''T0, 'T0)
+    1 -> (''T1, 'T1)
+    2 -> (''T2, 'T2)
 
   w ty tys = case ty of
-    AppT{}              -> Int.thFail $ "impossible: AppT is guarded by peelApp."
-    SigT ty _           -> uncurry w $ peelAppAcc tys ty
-    ForallT{}           -> Int.thFail $ "no support for ForallT."
-    ConT n | isRec n -> do
-      rhs <- expandSyn ty tys
-      case rhs of
+    PromotedT{}      -> Int.thFail $ "no support for promoted types."
+    PromotedTupleT{} -> Int.thFail $ "no support for promoted types."
+    PromotedNilT{}   -> Int.thFail $ "no support for promoted types."
+    PromotedConsT{}  -> Int.thFail $ "no support for promoted types."
+    StarT{}          -> Int.thFail $ "no support for kinds."
+    ConstraintT{}    -> Int.thFail $ "no support for constraint kinds."
+    LitT{}           -> Int.thFail $ "no support for type literals."
+    AppT{}           -> Int.thFail $ "impossible: AppT is guarded by peelApp."
+    ForallT{}        -> Int.thFail $ "no support for ForallT."
+    UnboxedTupleT{}  -> Int.thFail $ "no support for unboxed tuples."
+
+    SigT ty _        -> uncurry w $ peelAppAcc tys ty
+
+    VarT n | Just k <- List.findIndex (== n) $ reverse parNs ->
+      if null tys then return $
+        let (tyn, ctor, dtor) = case k of
+              0 -> (''Par0, 'Par0, 'unPar0)
+              1 -> (''Par1, 'Par1, 'unPar1)
+        in (ConT tyn, FieldRO (ConE ctor) (VarE dtor))
+      else Int.thFail $ "no support for poly- or higher-kinded parameters."
+
+    ConT n | Just lbl <- case bg of Left _ -> Nothing; Right bg -> Map.lookup n bg -> case lbl of
+      Nothing -> expandSyn ty tys >>= \case
         Just (ty, tys) -> w ty tys
-        Nothing ->
-          if not (null recs) then Int.thFail "no support for nested recursion."
-          else simple True ty tys
-    _
-      | not (null recs) -> case lookup (length recs) maps of
-        Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length recs) ++ " arguments."
-        Just (Mapping {containerTypeName = tyn, containerCtor = ctor,
-                       methodName = mn}) -> do
-          recs <- mapM w' recs
-          let snoc (tyL, fROL) (tyR, fROR) =
-                (tyL `AppT` tyR, fROL `appRO` fROR)
-              appRO l r = FieldRO {repF = repF l `AppE` repF r `AppE` objF r,
-                                   objF = objF l `AppE` objF r `AppE` repF r}
-              post fRO = FieldRO {repF = ConE ctor `compose` repF fRO,
-                                  objF = objF fRO `compose` dtor}
-          return $ Arrow.second post $ foldl snoc
-            (ConT tyn `AppT` container,
-             FieldRO {repF = VarE mn, objF = VarE mn}) recs
-          where dtor = LamE [ConP ctor [VarP x]] (VarE x)
-                  where x = mkName "x"
-      | otherwise -> simple False ty tys
-    where (foldl AppT ty -> container, recs) =
-            List.break (any isRec . Set.toList . SCCs.type_dependencies) tys
+        Nothing -> Int.thFail "impossible: expandSyn is guarded by yoko0."
+      Just lbl -> appliedRec lbl container tys'
+        where (foldl AppT ty -> container, tys') =
+                List.splitAt (length tys - length parNs) tys
 
+    -- NB cannot be recursive ... TODO unless we're operating on []
+    _ -> appliedDep container importants
+      where (foldl AppT ty -> container, importants) =
+              List.break (any isImportant . Set.toList . namesIn) tys
+
+  appliedRec lbl container tys = case null tys of
+    True -> return (ConT ''T0 `AppT` (PromotedT 'Rec `AppT` toNat lbl) `AppT` container, FieldRO (ConE 'T0) (VarE 'unT0))
+    False -> case lookup (length tys) maps of
+      Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length tys) ++ " arguments."
+      Just (Mapping {methodName = mn}) -> appliedType (ConT nRecTy `AppT` (PromotedT 'Rec `AppT` toNat lbl), nRecCtor, mn) container tys
+
+  appliedDep container tys = case null tys of
+    True -> return (ConT ''T0 `AppT` PromotedT 'Dep `AppT` container, FieldRO (ConE 'T0) (VarE 'unT0))
+    False -> case lookup (length tys) maps of
+      Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length tys) ++ " arguments."
+      Just (Mapping {containerTypeName = tyn, containerCtor = ctor, methodName = mn}) ->
+        appliedType (ConT tyn `AppT` PromotedT 'Dep, ctor, mn) container tys
+
+  appliedType (rTy, nCtor, nMap) ty tys = do
+    tys <- mapM w' tys
+    let snoc (tyL, fROL) (tyR, fROR) = (tyL `AppT` tyR, fROL `appRO` fROR)
+        appRO l r = FieldRO {repF = repF l `AppE` repF r `AppE` objF r,
+                             objF = objF l `AppE` objF r `AppE` repF r}
+        post fRO = FieldRO {repF = ConE nCtor `compose` repF fRO,
+                            objF = objF fRO `compose` dtor}
+          where dtor = let x = mkName "x" in LamE [ConP nCtor [VarP x]] (VarE x)
+    return $ Arrow.second post $ foldl snoc
+      (rTy `AppT` ty,
+       FieldRO {repF = VarE nMap, objF = VarE nMap}) tys
+
 data ConRO = ConRO {repP :: [Pat], repE :: Exp, objP :: Pat, objE :: [Exp]}
 
 yoko1 r@(convert -> X :&
-  Renamer := rn :&
-  Mappings := maps :&
-  BindingGroup := bg :&
-  TargetData := Int.DataType tvbs cons :&
-  TargetType := ty :&
-  TargetKind := (ks, cxt)
+  Target       := tyn :&
+  Renamer      := rn :&
+  Mappings     := maps :&
+  TargetData   := Int.DataType tvbs cons :&
+  DCInsts      := dcInsts
         ) = do
-  loc <- liftQ TH.location
+  let activated = dcInsts $ either ((:[]) . conName) (map conName) cons
 
   -- make a name into a NameG for a type in the current module; NB the fields
   -- types need not be declared in the same module as the target type
+  loc <- liftQ TH.location
   let mkG n = Name (mkOccName $ nameBase n) $
               NameG TcClsName (mkPkgName $ loc_package loc)
                       (mkModName $ loc_module loc)
 
-  liftQ (sequence [do
+  -- extract the ctors' fields and declare the fields types
+  nAndFieldss <- flip mapM (either (:[]) id cons) $ \con -> do
     let n = conName con
         n' = rn n
-        fd = applyConT2TVBs n' tvbs
+    generate [Int.dataType2Dec n' $ Int.DataType tvbs $ Right [renameCon rn con]]
+    (>>= generate) $ liftQ $ serializeTypeAsHash_data (mkG n')
+    fmap ((,) n)   $ liftQ $ conFields con
 
-    fields <- conFields con
+  let tvbSplits = [ List.splitAt k tvbs
+         | k <- [length (drop 2 tvbs)..length tvbs] ]
+  -- eg tvbs = [a,b,c]: [   ([a,b,c], []),   ([a,b], [c]),   ([a], [b,c])   ]
+  -- eg tvbs = [a,b]:   [   ([a,b]  , []),   ([a]  , [b]),   ([] , [a,b])   ]
+  -- eg tvbs = [a]:     [   ([a]    , []),   ([]   , [a])                   ]
+  -- eg tvbs = []:      [   ([]     , [])                                   ]
 
-    -- declare the fields type and its Codomain/Tag/DC instances
-    let yokoD = 
-          [Int.dataType2Dec n' (Int.DataType tvbs (Right [renameCon rn con])),
-           TySynInstD ''Codomain [fd] ty,
-           TySynInstD ''Tag   [fd] $ encode $ TH.nameBase n,
-           InstanceD cxt (ConT ''DC `AppT` fd)
-             [let (pat, exp) = pat_exp n' n $ length fields
-              in FunD 'rejoin [simpleClause [pat] exp]]
-          ]
+  (>>= generate) $ liftQ $ spineType_d_ tyn $ map tvbKind tvbs
+  (>>= generate) $ liftQ $ serializeTypeAsHash_data tyn
 
-    -- declare the Rep and Generic instances
-    (repTy, (conRO, _)) <- Arrow.second ($ 0) `fmap` halves fields
-          (return (ConT ''U, \s ->
-                   (ConRO {repP = [], repE = ConE 'U,
-                           objP = WildP, objE = []}, s)))
-          (\l r -> l >>= \(tyL, roL) -> r >>= \(tyR, roR) -> return $
-            (ConT ''(:*:) `AppT` tyL `AppT` tyR,
-             \s -> case roL s of
-               (roL, s) -> case roR s of
-                 (roR, s) ->
-                   (ConRO {repP = repP roL ++ repP roR,
-                           repE = ConE '(:*:) `AppE` repE roL `AppE` repE roR,
-                           objP = ConP '(:*:) [objP roL, objP roR],
-                           objE = objE roL ++ objE roR}, s)))
-          (\(_, ty) ->
-             let post fRO s =
-                   (ConRO {repP = [VarP n], repE = repF fRO `AppE` VarE n,
-                           objP = VarP n, objE = [objF fRO `AppE` VarE n]},
-                    s + 1)
-                   where n = mkName $ "x" ++ show s
-             in Arrow.second post `fmap` fieldRO maps bg ty)
+  flip mapM_ tvbSplits $ \(tvbs, pars) ->
+    (flip mapM (either (:[]) id cons) $ \con -> do
+      let n = conName con
+          n' = rn n
+      ((>>= generate) $ liftQ $ spineType_d_ (mkG n') $ map tvbKind tvbs)) >>
 
-    let genD = [TySynInstD ''Rep [fd] repTy,
-                InstanceD cxt (ConT ''Generic `AppT` fd)
-                 [FunD 'rep [simpleClause [ConP n' (repP conRO)] $ repE conRO],
-                  FunD 'obj [simpleClause [objP conRO] $
-                               foldl AppE (ConE n') $ objE conRO]]]
+    case filter ((/= StarT) . tvbKind) pars of
+    offenders@(_:_) -> liftQ $ Int.thWarn $ "not representing " ++ nameBase tyn ++ " with " ++ msg (length pars) ++ " because [" ++ List.intercalate "," (map (nameBase . tvbName) offenders) ++ "] involves poly- or higher-kinds."
+      where msg 1 = "1 parameter"
+            msg n = show n ++ " parameters"
+    [] -> do
+      -- the pervasive context of the reflective Compare constraints
+      cxt <- liftQ $ flip mapM tvbs $ \tvb ->
+        EqualP (PromotedT 'EQ) `fmap` do
+          let tv = [t| Spine $(return $ tvbType tvb) |]
+          [t| Ord.Compare $tv $tv |]
 
-    -- integrate with type-spine and type-cereal
-    spineD <- spineType_d_ (mkG n') ks
-    cerealD <- serializeTypeAsHash_data (mkG n')
+      -- for every fields type, generate the fields types instances
+      flip mapM_ nAndFieldss $ \(n, fields) -> do
+        yoko2 (n `elem` activated) $ r :&
+          TargetTVBs := tvbs :&
+          TargetPars := pars :&
+          TargetType := applyConT2TVBs tyn tvbs :&
+          TargetCxt  := cxt :&
+          ConName    := n :&
+          ConFields  := fields
 
-    return $ yokoD ++ spineD ++ cerealD ++ genD
-       | con <- either (:[]) id cons ]) >>= generate . concat
+      -- generate the DCs, DTs, DT instances
+      yoko3 $ r :&
+          TargetTVBs := tvbs :&
+          TargetPars := pars :&
+          TargetType := applyConT2TVBs tyn tvbs :&
+          TargetCxt  := cxt
 
-  yoko2 r
 
--- generate DCs/DT instances
-compose l r = VarE '(.) `AppE` l `AppE` r
+yoko2 activated (convert -> X :&
+  Renamer      := rn :&
+  Mappings     := maps :&
+  BindingGroup := bg :&
+  TargetType   := ty :&
+  TargetPars   := pars :&
+  TargetTVBs   := tvbs :&
+  TargetCxt    := cxt :&
+  ConName      := n :&
+  ConFields    := fields
+        ) = do
+  let nW_rejoin = case length pars of
+        0 -> 'Sym0
+        1 -> 'Sym1
+        2 -> 'Sym2
 
-postConE :: Name -> Exp -> Exp
-postConE n inj = compose (ConE n) inj
+  let (nW_rep, nW_obj) = case length pars of
+        0 -> ('W0, 'w0')
+        1 -> ('W1, 'w1')
+        2 -> ('W2, 'w2')
 
-yoko2 r@(convert -> X :&
-  Renamer := rn :&
-  TargetData := Int.DataType tvbs cons :&
-  TargetType := ty :&
-  TargetKind := (_, cxt)
+  let n' = rn n   ;   fd = applyConT2TVBs n' tvbs
+
+  -- declare the fields type's Codomain/Tag/DC instances
+  generate
+    [TySynInstD ''Codomain [fd] ty,
+     TySynInstD ''Tag   [fd] $ encode $ TH.nameBase n,
+     InstanceD cxt (ConT ''DC `AppT` fd)
+       [let (pat, exp) = pat_exp n' n $ length fields
+        in simpleVal 'rejoin $ ConE nW_rejoin `AppE` LamE [pat] exp]
+    ]
+
+  -- declare the Rep and Generic RHSs
+  when activated $ (>>= generate) $ do
+    (repTy, (conRO, _)) <- liftQ $ Arrow.second ($ 0) `fmap` halves fields
+      (return (ConT ''U, \s ->
+               (ConRO {repP = [], repE = ConE 'U,
+                       objP = WildP, objE = []}, s)))
+
+      (\l r -> l >>= \(tyL, roL) -> r >>= \(tyR, roR) -> return $
+       (ConT ''(:*:) `AppT` tyL `AppT` tyR,
+        \s -> case roL s of
+          (roL, s) -> case roR s of
+            (roR, s) ->
+              (ConRO {repP = repP roL ++ repP roR,
+                      repE = ConE '(:*:) `AppE` repE roL `AppE` repE roR,
+                      objP = ConP '(:*:) [objP roL, objP roR],
+                      objE = objE roL ++ objE roR}, s)))
+
+      (\(_, ty) ->
+         let post fRO s =
+               (ConRO {repP = [VarP n], repE = repF fRO `AppE` VarE n,
+                       objP = VarP n, objE = [objF fRO `AppE` VarE n]},
+                s + 1)
+               where n = mkName $ "x" ++ show s
+         in Arrow.second post `fmap`
+            fieldRO maps bg (map tvbName pars) ty)
+
+    return
+      [ TySynInstD ''Rep [fd] (ConT ''C `AppT` fd `AppT` repTy),
+        InstanceD cxt (ConT ''Generic `AppT` fd)
+        [simpleVal 'rep $ (ConE nW_rep `AppE`) $ LamE [ConP n' (repP conRO)] $ ConE 'C `AppE` repE conRO,
+         simpleVal 'obj $ (VarE nW_obj `AppE`) $ LamE [ConP 'C [objP conRO]] $ foldl AppE (ConE n') $ objE conRO]]
+
+-- generate DCs/DT instances
+yoko3 r@(convert -> X :&
+  Target       := tyn :&
+  Renamer      := rn :&
+  InvInsts     := invInsts :&
+  TargetData   := Int.DataType _ cons :&
+  BindingGroup := bg :&
+  TargetType   := ty :&
+  TargetPars   := pars :&
+  TargetTVBs   := tvbs :&
+  TargetCxt    := cxt
         ) = do
+  let (nW_disband, nNCtor) = case length pars of
+        0 -> ('W0, 'N0)
+        1 -> ('W1, 'N1)
+        2 -> ('W2, 'N2)
+
+  let invInst = case length pars of
+        0 -> Nothing
+        1 -> Just (''Invariant, 'invmap, 'gen_invmap)
+        2 -> Just (''Invariant2, 'invmap2, 'gen_invmap2)
+
   (dcs, cases) <- liftQ $ halves (either (:[]) id cons)
     (Int.thFail $ "`" ++ show (r !!! Target :: Name) ++ "' must have constructors.")
     (\l r -> do
@@ -369,10 +528,28 @@
        fields <- length `fmap` conFields con
        return $ let n = conName con
                 in (ConT ''N `AppT` applyConT2TVBs (rn n) tvbs,
-                    [(ConE 'N, (n, fields))]))
+                    [(ConE nNCtor, (n, fields))]))
 
-  cases <- return $ flip map cases $ \(inj, (n, fds)) ->
+  matches <- return $ flip map cases $ \(inj, (n, fds)) ->
     let (pat, exp) = pat_exp n (rn n) fds
-    in simpleClause [pat] $ inj `AppE` exp
+    in Match pat (NormalB $ inj `AppE` exp) []
   generate $ [TySynInstD ''DCs [ty] dcs,
-              InstanceD cxt (ConT ''DT `AppT` ty) [FunD 'disband cases]]
+              InstanceD cxt (ConT ''DT `AppT` ty)
+                [simpleVal 'disband $ (ConE nW_disband `AppE`) $ LamCaseE matches]]
+
+  when invInsts $ flip (maybe (return ())) invInst $ \(cls, method, rhs) ->
+    generate [InstanceD cxt (ConT cls `AppT` ty) [ValD (VarP method) (NormalB (VarE rhs)) []]]
+
+  (>>= generate) $ do
+    rhs <- case fmap (Set.toAscList . Map.keysSet) bg of
+      Left  _  -> return $ PromotedT 'NonRecDT
+      Right ns -> do
+        -- filter out the type synonyms
+        ns <- fmap catMaybes $ flip mapM ns $ \n -> liftQ (reify n) >>= \case
+          TyConI TySynD{} -> return Nothing
+          _               -> return $ Just n
+        let (l, _:r) = List.break (== tyn) ns
+            promo = foldr cons PromotedNilT where
+              cons n sofar = PromotedConsT `AppT` foldl AppT (ConT n) (map (VarT . tvbName) tvbs) `AppT` sofar
+        return $ PromotedT 'RecDT `AppT` promo l `AppT` promo r
+    return [TySynInstD ''DTs [ty] rhs]
diff --git a/Data/Yoko/TH/Internal.hs b/Data/Yoko/TH/Internal.hs
--- a/Data/Yoko/TH/Internal.hs
+++ b/Data/Yoko/TH/Internal.hs
@@ -27,7 +27,11 @@
 thFail s = fail $ "yokoTH: " ++ s
 
 
+thWarn :: String -> Q ()
+thWarn s = reportWarning $ "yokoTH: " ++ s
 
+
+
 data DataType = DataType [TyVarBndr] (Either Con [Con])
 
 
@@ -35,10 +39,13 @@
 dataType :: Name -> Q DataType
 dataType n = do
   i <- reify n
+  let refine = map $ \tvb -> case tvb of
+        PlainTV n -> KindedTV n StarT
+        _ -> tvb
   case i of
     TyConI d -> case d of
-      DataD _ _ tvbs cons _   -> return $ DataType tvbs $ Right cons
-      NewtypeD _ _ tvbs con _ -> return $ DataType tvbs $ Left con
+      DataD _ _ tvbs cons _   -> return $ DataType (refine tvbs) $ Right cons
+      NewtypeD _ _ tvbs con _ -> return $ DataType (refine tvbs) $ Left con
       _ -> thFail $ "expecting name of newtype or data type, not: " ++ show d
     _ -> thFail $ "expecting name of newtype or data type, not: " ++ show i
 
diff --git a/Data/Yoko/TypeBasics.hs b/Data/Yoko/TypeBasics.hs
--- a/Data/Yoko/TypeBasics.hs
+++ b/Data/Yoko/TypeBasics.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds, GADTs,
+  FlexibleInstances, TypeOperators, Rank2Types, ScopedTypeVariables,
+  InstanceSigs, ConstraintKinds, MultiParamTypeClasses #-}
 
 {- |
 
@@ -16,10 +18,24 @@
 
 module Data.Yoko.TypeBasics (
   Proxy(..), Equal, derive_data, derive_pro,
+  Nat(..), SingNat(..),
+  Length, Length', Append,
+  App, Constant(..),
+  Vec(..), vCarrying,
+  VFunctor(..), TrivCon, trivCon,
+  VInitialize(..),
+  CVec(..), cvec2list,
+  VRepeat(..), Diag_(..), VZip(..), cvZipWith,
+  Idx(..), IndexInto(..), cvAt, cvUpd, VEnum(..), cvAddIndexes,
   -- ** Re-exports
-  module Data.Yoko.MaybeKind, encode
+  module Data.Yoko.MaybeKind, encode, SpineCompare
   ) where
 
+import Data.Monoid
+import qualified Data.Foldable as F
+import qualified Data.Traversable as T
+import qualified Control.Applicative as I
+
 import Data.Yoko.MaybeKind
 
 import Type.Spine
@@ -49,3 +65,172 @@
 derive_pro n = do
   d <- spineType_pro n
   (d ++) `fmap` serializeTypeAsHash_pro n
+
+
+
+-- naturals
+data Nat = Z | S Nat
+
+data SingNat :: Nat -> * where
+  SZ ::              SingNat 'Z
+  SN :: SingNat n -> SingNat ('S n)
+
+-- lists
+type family Append (x :: [k]) (y :: [k]) :: [k]
+type instance Append '[] y       = y
+type instance Append (t ': ts) y = t ': Append ts y
+
+
+type Length list = Length' Z list
+
+type family Length' (acc :: Nat) (list :: [k]) :: Nat
+type instance Length' acc '[]         = acc
+type instance Length' acc (t ': list) = Length' (S acc) list
+
+-- indexed vectors
+type family App (fn :: k -> *) (t :: k) :: *
+
+newtype Constant a (t :: k) = Constant a
+type instance App (Constant a) k = a
+
+data Vec :: [k] -> (k -> *) -> * where
+  VNil  ::                        Vec '[]       f
+  VCons :: App f t -> Vec ts f -> Vec (t ': ts) f
+
+instance Eq (Vec '[] f) where _ == _ = True
+instance (Eq (App f t), Eq (Vec ts f)) => Eq (Vec (t ': ts) f) where
+  VCons a as == VCons b bs = a == b && as == bs
+
+instance Ord (Vec '[] f) where compare _ _ = EQ
+instance (Ord (App f t), Ord (Vec ts f)) => Ord (Vec (t ': ts) f) where
+  VCons a as `compare` VCons b bs = compare (a, as) (b, bs)
+
+vCarrying :: Proxy f -> Vec ts f -> Vec ts f
+vCarrying _ = id
+
+class VFunctor c ts where
+  vMap :: Proxy c -> (forall t. c t => Proxy t -> App f t -> App g t) -> Vec ts f -> Vec ts g
+
+instance VFunctor c '[] where
+  vMap _ _ VNil         = VNil
+instance (c t, VFunctor c ts) => VFunctor c (t ': ts) where
+  vMap c f (VCons x xs) = VCons (f (Proxy :: Proxy t) x) $ vMap c f xs
+
+class TrivCon a; instance TrivCon a
+trivCon :: Proxy TrivCon
+trivCon = Proxy
+
+instance Monoid (Vec '[] f) where
+  mempty = VNil; mappend _ _ = VNil
+instance (Monoid (App f t), Monoid (Vec ts f)) => Monoid (Vec (t ': ts) f) where
+  mempty = VCons mempty mempty
+  VCons x xs `mappend` VCons y ys = mappend x y `VCons` mappend xs ys
+
+
+
+newtype CVec ts a = CVec {unCVec :: Vec ts (Constant a)}
+
+instance Eq  (Vec ts (Constant a)) => Eq  (CVec ts a) where CVec x == CVec y = x == y
+instance Ord (Vec ts (Constant a)) => Ord (CVec ts a) where CVec x `compare` CVec y = compare x y
+
+instance Monoid (Vec ts (Constant a)) => Monoid (CVec ts a) where
+  mempty = CVec mempty
+  CVec x `mappend` CVec y = CVec $ mappend x y
+
+instance Functor (CVec ts) where fmap = T.fmapDefault
+instance F.Foldable (CVec ts) where foldMap = T.foldMapDefault
+
+instance T.Traversable (CVec ts) where
+  traverse :: forall a i b. I.Applicative i => (a -> i b) -> CVec ts a -> i (CVec ts b)
+  traverse f (CVec v) = CVec I.<$> w v where
+    w :: forall ts. Vec ts (Constant a) -> i (Vec ts (Constant b))
+    w x = case x of
+      VNil       -> I.pure VNil
+      VCons a as -> VCons I.<$> f a I.<*> w as
+
+cvec2list :: CVec ts a -> [a]
+cvec2list = F.toList
+
+class VRepeat ts where cvRepeat :: a -> CVec ts a
+
+instance VRepeat '[]                     where cvRepeat _ = CVec VNil
+instance VRepeat ts => VRepeat (t ': ts) where
+  cvRepeat a = CVec $ VCons a $ unCVec $ cvRepeat a
+
+data Diag_ (f :: k -> *) (g :: k -> *) (t :: k) = Diag_
+type instance App (Diag_ f g) t = (App f t, App g t)
+
+class VZip ts where vZip :: Vec ts f -> Vec ts g -> Vec ts (Diag_ f g)
+
+instance VZip '[] where vZip _ _ = VNil
+instance VZip ts => VZip (t ': ts) where
+  vZip (VCons a as) (VCons b bs) = VCons (a, b) $ vZip as bs
+
+cvZipWith :: forall a b c ts. (a -> b -> c) -> CVec ts a -> CVec ts b -> CVec ts c
+cvZipWith f (CVec x) (CVec y) = CVec $ w x y where
+  w :: forall ts. Vec ts (Constant a) -> Vec ts (Constant b) -> Vec ts (Constant c)
+  w VNil         VNil         = VNil
+  w (VCons a as) (VCons b bs) = VCons (f a b) $ w as bs
+
+data Idx :: [k] -> * where
+  ZIdx :: Idx (t ': ts)
+  SIdx :: Idx ts -> Idx (t ': ts)
+type instance App Idx ts = Idx ts
+
+class IndexInto (n :: Nat) (ts :: [k]) where
+  indexInto :: Proxy n -> Proxy ts -> Idx ts
+
+instance IndexInto Z (t ': ts) where indexInto _ _ = ZIdx
+instance IndexInto n ts => IndexInto (S n) (t ': ts) where
+  indexInto _ _ = SIdx $ indexInto (Proxy :: Proxy n) (Proxy :: Proxy ts)
+
+instance Show (Idx ts) where
+  showsPrec _ ZIdx = showString "ZIdx"
+  showsPrec p (SIdx x) = showParen (p > 10) $
+    showString "SIdx" . showChar ' ' . showsPrec 11 x
+
+instance Eq (Idx ts) where
+  ZIdx == ZIdx = True
+  SIdx a == SIdx b = a == b
+  _ == _ = False
+
+instance Ord (Idx ts) where
+  ZIdx   `compare` ZIdx   = EQ
+  ZIdx   `compare` _      = LT
+  SIdx _ `compare` ZIdx   = GT
+  SIdx a `compare` SIdx b = compare a b
+
+cvAt :: forall ts a. CVec ts a -> Idx ts -> a
+cvAt (CVec v) = flip w v where
+  w :: forall ts. Idx ts -> Vec ts (Constant a) -> a
+  w ZIdx       (VCons a _ ) = a
+  w (SIdx idx) (VCons _ as) = w idx as
+
+cvUpd :: forall ts a. CVec ts a -> Idx ts -> (a -> a) -> CVec ts a
+cvUpd (CVec v) idx f = CVec $ w idx v where
+  w :: forall ts. Idx ts -> Vec ts (Constant a) -> Vec ts (Constant a)
+  w ZIdx       (VCons a as) = VCons (f a) as
+  w (SIdx idx) (VCons a as) = VCons a $ w idx as
+
+class VEnum ts where cvEnum :: CVec ts (Idx ts)
+instance VEnum '[] where cvEnum = CVec VNil
+instance VEnum ts => VEnum (t ': ts) where
+  cvEnum = CVec $ VCons ZIdx $ unCVec $ fmap SIdx cvEnum
+
+cvAddIndexes :: VEnum ts => CVec ts a -> CVec ts (Idx ts, a)
+cvAddIndexes = cvZipWith (,) cvEnum
+
+
+
+type instance App Proxy t = Proxy t
+
+class VInitialize c ts where
+  vInitialize  :: Proxy c -> Proxy f -> (forall t. c t => Proxy t -> App f t) -> Vec  ts f
+  cvInitialize :: Proxy c ->            (forall t. c t => Proxy t -> a) ->       CVec ts a
+instance VInitialize c '[] where
+  vInitialize  _ _ _ = VNil
+  cvInitialize _   _ = CVec VNil
+instance (c t, VInitialize c ts) => VInitialize c (t ': ts) where
+  vInitialize  pc pf x = VCons (x (Proxy :: Proxy t)) (vInitialize  pc pf x)
+  cvInitialize pc    x = CVec $
+                         VCons (x (Proxy :: Proxy t)) (unCVec $ cvInitialize pc    x)
diff --git a/Data/Yoko/TypeSums.hs b/Data/Yoko/TypeSums.hs
--- a/Data/Yoko/TypeSums.hs
+++ b/Data/Yoko/TypeSums.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators,
-  NoPolyKinds, DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators, PolyKinds, DataKinds #-}
 
 {-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
   ScopedTypeVariables, EmptyDataDecls #-}
@@ -21,8 +20,8 @@
 -}
 
 module Data.Yoko.TypeSums (DistMaybePlus, (:-:),
-                           Embed, embed, inject,
-                           Partition, project, partition) where
+                           Embed, embed, inject0, inject1, inject2,
+                           Partition, project0, project1, project2, partition) where
 
 import Data.Yoko.TypeBasics
 import Data.Yoko.Representation
@@ -34,39 +33,49 @@
 
 
 
-class Embed sub sup where embed_ :: sub -> sup
+class Embed sub sup where embed_ :: sub (p1 :: *) (p0 :: *) -> sup p1 p0
 
-embed :: Embed sub sup => sub -> sup
+embed :: Embed sub sup => sub p1 p0 -> sup p1 p0
 embed = embed_
 
-inject :: Embed (N a) sum => a -> sum
-inject = embed . N
+inject0 :: Embed (N a) sum => a -> sum p1 p0
+inject0 = embed . N0
 
+inject1 :: Embed (N a) sum => a p0 -> sum p1 p0
+inject1 = embed . N1
 
+inject2 :: Embed (N a) sum => a p1 p0 -> sum p1 p0
+inject2 = embed . N2
 
-class Partition sup subL subR where partition_ :: sup -> Either subL subR
 
+
+class Partition sup subL subR where partition_ :: sup (p1 :: *) (p0 :: *) -> Either (subL p1 p0) (subR p1 p0)
+
 partition :: Partition sup sub (sup :-: sub) =>
-             sup -> Either sub (sup :-: sub)
+             sup p1 p0 -> Either (sub p1 p0) ((sup :-: sub) p1 p0)
 partition = partition_
 
-project :: Partition sum (N a) (sum :-: N a) => sum -> Either a (sum :-: N a)
-project = left unN . partition_
+project0 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either a ((sum :-: N a) p1 p0)
+project0 = left unN0 . partition_
 
+project1 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either (a p0) ((sum :-: N a) p1 p0)
+project1 = left unN1 . partition_
 
+project2 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either (a p1 p0) ((sum :-: N a) p1 p0)
+project2 = left unN2 . partition_
 
 
 
-data Here a
-data TurnLeft path
-data TurnRight path
 
-type family Locate a sum :: Maybe *
-type instance Locate a (N x) = If (Equal x a) (Just (Here a)) Nothing
+
+data Path k = Here k | TurnLeft (Path k) | TurnRight (Path k)
+
+type family Locate (a :: k) (sum :: * -> * -> *) :: Maybe (Path k)
+type instance Locate a (N x)     = If (Equal x a) (Just (Here a)) Nothing
 type instance Locate a (l :+: r) =
   MaybeMap TurnLeft (Locate a l) `MaybePlus1`
   MaybeMap TurnRight (Locate a r)
-type instance Locate a Void = Nothing
+type instance Locate a Void  = Nothing
 
 type Elem a sum = IsJust (Locate a sum)
 
@@ -74,8 +83,8 @@
 
 
 
-class InjectAt path a sum where injectAt :: Proxy path -> a -> sum
-instance InjectAt (Here a) a (N a) where injectAt _ = N
+class InjectAt path n sum where injectAt :: Proxy path -> n (p1 :: *) (p0 :: *) -> sum p1 p0
+instance InjectAt (Here a) (N a) (N a) where injectAt _ = id
 instance InjectAt path a l => InjectAt (TurnLeft path) a (l :+: r) where
   injectAt _ = L . injectAt (Proxy :: Proxy path)
 instance InjectAt path a r => InjectAt (TurnRight path) a (l :+: r) where
@@ -85,8 +94,8 @@
 
 
 
-instance (Locate x sup ~ Just path, InjectAt path x sup) => Embed (N x) sup where
-  embed_ = injectAt (Proxy :: Proxy path) . unN
+instance (Locate x sup ~ Just path, InjectAt path (N x) sup) => Embed (N x) sup where
+  embed_ = injectAt (Proxy :: Proxy path)
 instance (Embed l sup, Embed r sup) => Embed (l :+: r) sup where
   embed_ = foldPlus embed embed
 
@@ -95,12 +104,12 @@
 
 
 infixl 6 :-:
-type family (:-:) sum sum2
-type instance (:-:) (N x) sum2 = If (Elem x sum2) Void (N x)
+type family (:-:) (sum :: * -> * -> *) (sum2 :: * -> * -> *) :: * -> * -> *
+type instance (:-:) (N x)    sum2 = If (Elem x sum2) Void (N x)
 type instance (:-:) (l :+: r) sum2 = Combine (l :-: sum2) (r :-: sum2)
 
 
-type family Combine sum sum2
+type family Combine (sum :: * -> * -> *) (sum2 :: * -> * -> *) :: * -> * -> *
 type instance Combine Void x = x
 type instance Combine (N x) Void = N x
 type instance Combine (N x) (N y) = N x :+: N y
@@ -112,9 +121,9 @@
 
 
 class Partition_N (bn :: Bool) x subL subR where
-  partition_N :: Proxy bn -> N x -> Either subL subR
+  partition_N :: Proxy bn -> x (p1 :: *) (p0 :: *) -> Either (subL p1 p0) (subR p1 p0)
 
-instance (Partition_N (Elem x subL) x subL subR
+instance (Partition_N (Elem x subL) (N x) subL subR
          ) => Partition (N x) subL subR where
   partition_ = partition_N (Proxy :: Proxy (Elem x subL))
 
@@ -124,7 +133,7 @@
 
 
 
-instance Embed (N x) subR => Partition_N False x subL subR where
+instance Embed x subR => Partition_N False x subL subR where
   partition_N _ = Right . embed
-instance Embed (N x) subL => Partition_N True  x subL subR where
+instance Embed x subL => Partition_N True  x subL subR where
   partition_N _ = Left  . embed
diff --git a/Data/Yoko/View.hs b/Data/Yoko/View.hs
--- a/Data/Yoko/View.hs
+++ b/Data/Yoko/View.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
-  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds #-}
+  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds,
+  PolyKinds, GADTs #-}
 
 {- |
 
@@ -16,42 +17,124 @@
 -}
 
 module Data.Yoko.View
-  (-- * Reflection
+{-  (-- * Reflection
    -- ** Fields types
-   Tag, Codomain, DC(..),
+   Tag, Codomain0, Codi, DC(..),
+   -- ** Substitution
+   Subst, Subst0, Subst1,
    -- ** Disbanded data types
    DCs, DT(..)
-  ) where
+  ) -} where
 
+import Data.Yoko.W
+import Data.Yoko.TypeBasics
 import Data.Yoko.Representation
-import Data.Yoko.TypeSums (Embed, Partition, (:-:))
-import Data.Yoko.Each
+--import Data.Yoko.TypeSums (Embed, Partition, (:-:))
+--import Data.Yoko.Each
 
 import Type.Digits (Digit)
 
 
 
+
+
 -- | @Tag@ returns a simulated type-level string that is the name of the
 -- constructor that the @dc@ fields type represents.
-type family Tag dc :: Digit
+type family Tag (dc :: k) :: Digit
 
 -- | @Codomain@ is the data type that contains the constructor that the fields
 -- type @dc@ represents.  It can also be applied to sums of fields types, in
 -- which case it just uses the left-most.
-type family Codomain dc
-type instance Codomain (N dc) = Codomain dc
-type instance Codomain (l :+: r) = Codomain l
+type family Codomain (dc :: k) :: k
 
+type family Codomain0 (dcs :: * -> * -> *) :: *
+type family Codomain1 (dcs :: * -> * -> *) :: * -> *
+type family Codomain2 (dcs :: * -> * -> *) :: * -> * -> *
+type instance Codomain0 (N dc)    = Codomain dc
+type instance Codomain1 (N dc)    = Codomain dc
+type instance Codomain2 (N dc)    = Codomain dc
+type instance Codomain0 (l :+: r) = Codomain0 l
+type instance Codomain1 (l :+: r) = Codomain1 l
+type instance Codomain2 (l :+: r) = Codomain2 l
+
+
+
+data DTPos k = NonRecDT | RecDT [k] [k]
+
+-- | Maps a type to its mutually recursive siblings.
+type family DTs (t :: k) :: DTPos k
+
+
+type NumDTs t = NumDTs' (DTs t)
+type family NumDTs' (t :: DTPos k) :: Nat
+type instance NumDTs' NonRecDT    = Z
+type instance NumDTs' (RecDT l r) = S (Length' (Length r) l)
+
+type SiblingDTs t = SiblingDTs' t (DTs t)
+type family SiblingDTs' (t :: k) (dpos :: DTPos k) :: [k]
+type instance SiblingDTs' t NonRecDT    = '[]
+type instance SiblingDTs' t (RecDT l r) = Append l (t ': r)
+
+
+
 -- | Any fields type can be further represented as a product-of-fields and can
 -- be injected back into the original data type.
-class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: dc -> Codomain dc
+class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: Sym dc (Codomain dc) p1 p0
 
 -- | The @DCs@ of a data type is sum of all of its fields types.
-type family DCs t
--- | @DT@ disbands a data type if all of its fields types have @DC@ instances.
-class Each IsDCOf (DCs t) => DT t where disband :: t -> DCs t
+type family DCs (t :: k) :: * -> * -> *
+-- | @DT@ disbands a data type.@
+class DT t where disband :: W t (DCs t) p1 p0
 
-class (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),
-       Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc
-instance (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),
-          Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc
+
+
+-- take a representation, C or above and excluding Recs/Pars, to an actual *
+-- type
+type family Eval (r :: * -> * -> *) :: *
+type instance Eval (T0 Dep t)       = t
+--type instance Eval Void           = ???
+type instance Eval (l :+: r)        = Eval l -- equivalently, Eval r
+type instance Eval (C  (dc :: *) r) = Codomain dc
+type instance Eval (N dc)           = Codomain dc
+
+
+
+data SubstSpec star = Sub0 star | Sub1 star | Sub10 star star
+
+
+
+type family Subst (spec :: SubstSpec *) (r :: * -> * -> *) :: * -> * -> *
+--type instance Subst spec Void  = ???
+type instance Subst spec (N dc)   = N dc
+type instance Subst spec (l :+: r) = Subst spec l :+: Subst spec r
+
+type instance Subst spec (C dc r) = C dc (Subst spec r)
+type instance Subst spec U         = U
+type instance Subst spec (l :*: r) = Subst spec l :*: Subst spec r
+
+type instance Subst (Sub0  par0     ) Par0 = T0 Dep par0
+type instance Subst (Sub1  par1     ) Par0 = Par0
+type instance Subst (Sub10 par1 par0) Par0 = T0 Dep par0
+type instance Subst (Sub1  par1     ) Par1 = T0 Dep par1
+type instance Subst (Sub10 par1 par0) Par1 = T0 Dep par1
+
+type instance Subst (Sub0 par0) (T1 (Rec lbl) t a) = T0 (Rec lbl) (t (Eval (Subst (Sub0 par0) a)))
+--type instance Subst (Sub1 par1) (Rec0 lbl t) = undefined
+--type instance Subst (Sub10 par1 par0) (Rec1 lbl t a) = undefined
+
+--type instance Subst (Sub0 par0 (Rec2 lbl t b a) = undefined
+type instance Subst (Sub1 par1) (T2 (Rec lbl) t b a) =
+  T1 (Rec lbl)    (t (Eval (Subst (Sub1 par1) b)))    (Subst (Sub1 par1) a)
+type instance Subst (Sub10 par1 par0) (T2 (Rec lbl) t b a) =
+  T0 (Rec lbl)    (t (Eval (Subst (Sub10 par1 par0) b))    (Eval (Subst (Sub10 par1 par0) a)))
+
+type instance Subst spec (T0 Dep t)  = T0 Dep t
+
+type instance Subst spec (T1 Dep f x  ) = T1 Dep f (Subst spec x)
+type instance Subst spec (T2 Dep f x y) = T2 Dep f (Subst spec x) (Subst spec y)
+
+
+
+type Subst0  t    p0 = Subst (Sub0 p0)     (Rep t)
+type Subst1  t p1    = Subst (Sub1 p1)     (Rep t)
+type Subst10 t p1 p0 = Subst (Sub10 p1 p0) (Rep t)
diff --git a/Data/Yoko/W.hs b/Data/Yoko/W.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/W.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, RankNTypes, ConstraintKinds #-}
+
+{-# LANGUAGE FlexibleInstances #-}
+
+module Data.Yoko.W where
+
+
+
+data family W (t :: k) :: (* -> * -> *) -> * -> * -> *
+
+newtype instance W (t :: *)           s p1 p0 = W0 (t       -> s p1 p0)
+newtype instance W (t :: * -> *)      s p1 p0 = W1 (t    p0 -> s p1 p0)
+newtype instance W (t :: * -> * -> *) s p1 p0 = W2 (t p1 p0 -> s p1 p0)
+
+unW0 (W0 f) = f
+unW1 (W1 f) = f
+unW2 (W2 f) = f
+
+data family W' (s :: k) :: (* -> * -> *) -> * -> * -> *
+
+newtype instance W' (s :: *)           t p1 p0 = W'0 (t p1 p0 -> s      )
+newtype instance W' (s :: * -> *)      t p1 p0 = W'1 (t p1 p0 -> s    p0)
+newtype instance W' (s :: * -> * -> *) t p1 p0 = W'2 (t p1 p0 -> s p1 p0)
+
+unW'0 (W'0 f) = f
+unW'1 (W'1 f) = f
+unW'2 (W'2 f) = f
+
+data family Sym (t :: k) :: k ->  * -> * -> *
+
+newtype instance Sym (t :: *)           s p1 p0 = Sym0 (t       -> s      )
+newtype instance Sym (t :: * -> *)      s p1 p0 = Sym1 (t    p0 -> s    p0)
+newtype instance Sym (t :: * -> * -> *) s p1 p0 = Sym2 (t p1 p0 -> s p1 p0)
+
+unSym0 (Sym0 f) = f
+unSym1 (Sym1 f) = f
+unSym2 (Sym2 f) = f
+
+
+class ComposeW (t :: k) where
+  composeW  :: (s p1 p0 -> s' p1 p0) -> W t s p1 p0 -> W t s' p1 p0
+  composeW' :: W' t s' p1 p0 -> (s p1 p0 -> s' p1 p0) -> W' t s p1 p0
+  sym ::   W' t' s  p1 p0 -> W  t s p1 p0 -> Sym t t' p1 p0
+  unSym :: W  t  s' p1 p0 -> W' t s p1 p0 -> s p1 p0 -> s' p1 p0
+  composeSymW' :: Sym t t' p1 p0 -> W' t s p1 p0 -> W' t' s p1 p0
+  composeWSym  :: W t' s p1 p0 -> Sym t t' p1 p0 -> W t s p1 p0
+instance ComposeW (t :: *) where
+  composeW       f  (W0  g) = W0  (f . g)
+  composeW' (W'0 f)      g  = W'0 (f . g)
+  sym       (W'0 f) (W0  g) = Sym0 (f . g)
+  unSym     (W0  f) (W'0 g) = f . g
+  composeSymW' (Sym0 f) (W'0 g) = W'0 (f . g)
+  composeWSym  (W0 f) (Sym0 g) = W0 (f . g)
+instance ComposeW (t :: * -> *) where
+  composeW       f  (W1  g) = W1 (f . g)
+  composeW' (W'1 f)      g  = W'1 (f . g)
+  sym       (W'1 f) (W1  g) = Sym1 (f . g)
+  unSym     (W1  f) (W'1 g) = f . g
+  composeSymW' (Sym1 f) (W'1 g) = W'1 (f . g)
+  composeWSym  (W1 f) (Sym1 g) = W1 (f . g)
+instance ComposeW (t :: * -> * -> *) where
+  composeW       f  (W2  g) = W2 (f . g)
+  composeW' (W'2 f)      g = W'2 (f . g)
+  sym       (W'2 f) (W2  g) = Sym2 (f . g)
+  unSym     (W2  f) (W'2 g) = f . g
+  composeSymW' (Sym2 f) (W'2 g) = W'2 (f . g)
+  composeWSym  (W2 f) (Sym2 g) = W2 (f . g)
diff --git a/Data/YokoRaw.hs b/Data/YokoRaw.hs
--- a/Data/YokoRaw.hs
+++ b/Data/YokoRaw.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
   MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables,
-  UndecidableInstances #-}
+  UndecidableInstances, PolyKinds #-}
 
 {- |
 
@@ -20,39 +20,37 @@
 module Data.YokoRaw
   (module Data.Yoko.Representation,
    module Data.Yoko.View,
+   module Data.Yoko.TypeBasics,
+   module Data.Yoko.W,
    -- * Building fields type consumers
    one, (|||), (||.), (.||), (.|.),
    -- * Operations on disbanded data types
-   disbanded, band, ConDCOf, precise_case,
+   disbanded, AreDCsOf, band, precise_case0,
    -- * Operations on sums of fields types
    (:-:), Embed, Partition,
    embed, inject, partition, project,
    -- * Forgetting @yoko@'s extra structure
-   reps, EachGeneric, EachRep, ig_from,
-   Equal,
-   -- * Bundled Template Haskell
-   module Data.Yoko.TH) where
+   reps, EachGeneric, EachRep, ig_from) where
 
+import Data.Yoko.W
 import Data.Yoko.TypeBasics
 import Data.Yoko.Representation
 import Data.Yoko.View
 import Data.Yoko.TypeSums (Embed, Partition, (:-:))
 import qualified Data.Yoko.TypeSums as TypeSums
-import Data.Yoko.Each
-
-import Data.Yoko.TH
+--import Data.Yoko.Each
 
 
 
 -- | @one@ extends a function that consumes a fields type to a function that
 -- consumes a disbanded data type containing just that fields type.
-one :: (dc -> a) -> N dc -> a
-one = foldN
+one :: (dc -> a) -> N dc p1 p0 -> a
+one = foldN0
 
 infixl 6 |||
 -- | Combines two functions that consume disbanded data types into a function
 -- that consumes their union. All fields types must be from the same data type.
-(|||) :: (Codomain sumL ~ Codomain sumR) => (sumL -> a) -> (sumR -> a) -> sumL :+: sumR -> a
+(|||) :: (Codomain0 sumL ~ Codomain0 sumR) => (sumL p1 p0 -> a) -> (sumR p1 p0 -> a) -> (sumL :+: sumR) p1 p0 -> a
 (|||) = foldPlus
 
 infixl 9 .|.
@@ -69,56 +67,54 @@
 
 
 -- | @disbanded@ injects a fields type into its disbanded range
-disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc)
-disbanded = TypeSums.inject
+disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc) p1 p0
+disbanded = TypeSums.inject0
 
 -- | @band@s a disbanded data type back into its normal data type.
 --
--- Since 'Disbanded' is a type family, the range of @band@ determines the @t@
--- type variable.
-band :: forall t. Each (ConDCOf t) (DCs t) => DCs t -> t
-band = each (Proxy :: Proxy (ConDCOf t)) rejoin
+-- Since 'DCs' is a type family, it's the range of @band@ that determines the
+-- @t@ type variable.
+class AreDCsOf (t :: k) (dcs :: * -> * -> *) where band_ :: W' t dcs p1 p0
+instance (WN dc, Codomain dc ~ t, DC dc) => AreDCsOf t (N dc) where
+  band_ = composeSymW' rejoin unN
+instance (FoldPlusW' t, AreDCsOf t l, AreDCsOf t r) => AreDCsOf t (l :+: r) where band_ = foldPlusW' band_ band_
 
-class (Codomain dc ~ t, DC dc) => ConDCOf t dc
-instance (Codomain dc ~ t, DC dc) => ConDCOf t dc
+band :: (AreDCsOf (t :: k) (DCs t)) => W' t (DCs t) p1 p0
+band = band_
 
-embed :: (Codomain sub ~ Codomain sup, Embed sub sup) => sub -> sup
+embed :: (Codomain0 sub ~ Codomain0 sup, Embed sub sup) => sub p1 p0 -> sup p1 p0
 embed = TypeSums.embed
 
 
 -- | @inject@s a fields type into a sum of fields types.
-inject :: Embed (N dc) sum => dc -> sum
-inject = TypeSums.inject
+inject :: Embed (N dc) sum => dc -> sum p1 p0
+inject = TypeSums.inject0
 
 -- | @partition@s a sum of fields type into a specified sum of fields types and
 -- the remaining sum.
-partition :: (Codomain sum ~ Codomain sub, Partition sum sub (sum :-: sub)) =>
-             sum -> Either sub (sum :-: sub)
+partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) =>
+             sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0)
 partition = TypeSums.partition
 
 -- | @project@s a single fields type out of a disbanded data type.
-project :: (Codomain sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>
-           sum -> Either dc (sum :-: N dc)
-project = TypeSums.project
+project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>
+           sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)
+project = TypeSums.project0
 
 
 
 -- TODO need a MapSum just like MapRs, use a RPV for rep
 
 -- | @reps@ maps a disbanded data type to its sum-of-products representation.
-reps :: EachGeneric sum => sum -> EachRep sum
+reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0
 reps = repEach
 
-type family EachRep sum
+type family EachRep (sum :: * -> * -> *) :: * -> * -> *
 type instance EachRep (N a) = Rep a
 type instance EachRep (a :+: b) = EachRep a :+: EachRep b
-class EachGeneric sum where
-  repEach :: sum -> EachRep sum   ;   objEach :: EachRep sum -> sum
-instance Generic a => EachGeneric (N a) where
-  repEach (N x) = rep x   ;   objEach = N . obj
-instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where
-  repEach = mapPlus repEach repEach
-  objEach = mapPlus objEach objEach
+class EachGeneric sum where repEach :: sum p1 p0 -> EachRep sum p1 p0
+instance (WN dc, Generic dc) => EachGeneric (N dc) where repEach = unSym rep unN
+instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where repEach = mapPlus repEach repEach
 
 
 
@@ -136,12 +132,12 @@
 --
 -- In this example, @C0_@, @C1_@, and @C2_@ are fields types. The other fields
 -- types for the same data type are handled with the @default@ function.
-precise_case :: (Codomain dcs ~ t, Codomain (DCs t) ~ t, DT t,
-               Partition (DCs t) dcs (DCs t :-: dcs)) =>
-  (DCs t :-: dcs -> a) -> t -> (dcs -> a) -> a
-precise_case g x f = either f g $ partition $ disband x
+precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t,
+                 Partition (DCs t) dcs (DCs t :-: dcs)) =>
+  ((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> a
+precise_case0 g x f = either f g $ partition $ unW0 disband x
 
 -- | @ig_from x =@ 'reps $ disband' @x@ is a convenience. It approximates the
 -- @instant-generics@ view, less the @CEq@ annotations.
-ig_from :: (DT t, EachGeneric (DCs t)) => t -> EachRep (DCs t)
-ig_from x = reps $ disband x
+ig_from :: (ComposeW t, DT t, EachGeneric (DCs t)) => W t (EachRep (DCs t)) p1 p0
+ig_from = reps `composeW` disband
diff --git a/Examples/LambdaLift/Common.hs b/Examples/LambdaLift/Common.hs
--- a/Examples/LambdaLift/Common.hs
+++ b/Examples/LambdaLift/Common.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TemplateHaskell, DataKinds, TypeFamilies #-}
+
 {- |
 
 Module      :  LambdaLift.Common
@@ -14,4 +16,10 @@
 
 module LambdaLift.Common where
 
+import Data.Yoko
+
+
+
 data Type = TyUnit | TyInt | TyFun Type Type deriving Show
+
+yokoTH ''Type
diff --git a/Examples/LambdaLift/DeepSeq.hs b/Examples/LambdaLift/DeepSeq.hs
--- a/Examples/LambdaLift/DeepSeq.hs
+++ b/Examples/LambdaLift/DeepSeq.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
-  UndecidableInstances #-}
+  UndecidableInstances, DefaultSignatures, PolyKinds, DataKinds, TypeFamilies #-}
 
 {- |
 
@@ -18,31 +18,54 @@
 module LambdaLift.DeepSeq where
 
 import Data.Yoko
+import Data.Bifunctor
 
 
 
-class DeepSeq a where rnf :: a -> ()
-instance DeepSeq a => DeepSeq [a] where
-  rnf [] = ()
-  rnf (x : xs) = rnf x `seq` rnf xs
-instance DeepSeq a => DeepSeq (N a) where rnf = rnf . unN
-instance (DeepSeq a, DeepSeq b) => DeepSeq (a :+: b) where
-  rnf = foldPlus rnf rnf
---instance DeepSeq sum => DeepSeq (DCsOf a sum) where rnf = rnf . unDCsOf
-instance (DeepSeq a, DeepSeq b) => DeepSeq (a :*: b) where
-  rnf = foldTimes seq rnf rnf
-instance DeepSeq a => DeepSeq (Rec a) where rnf = rnf . unRec
-instance DeepSeq a => DeepSeq (Dep a) where rnf = rnf . unDep
-instance DeepSeq (f a) => DeepSeq (Par1 f a) where rnf = rnf . unPar1
-instance DeepSeq U where rnf U = ()
+class DeepSeq0 a where
+  rnf0 :: a       -> ()
+  default rnf0 :: (DeepSeq2 (DCs a), DT a) => a -> ()
+  rnf0 = rnf2 . unW0 disband
+class DeepSeq1 a where
+  rnf1 :: a    () -> ()
+  default rnf1 :: (DeepSeq2 (DCs a), DT a) => a () -> ()
+  rnf1 = rnf2 . unW1 disband
+class DeepSeq2 a where
+  rnf2 :: a () () -> ()
+  default rnf2 :: (DeepSeq2 (DCs a), DT a) => a () () -> ()
+  rnf2 = rnf2 . unW2 disband
 
-instance DeepSeq Int where rnf = (`seq` ())
-instance (DeepSeq a, DeepSeq b) => DeepSeq (Either a b) where
-  rnf = either rnf rnf
+instance (WN a, DeepSeq2 (Rep a), Generic a) => DeepSeq2 (N a) where
+  rnf2 = rnf2 . unSym rep unN
+instance (DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (a :+: b) where
+  rnf2 = foldPlus rnf2 rnf2
 
-instance (DeepSeq a, DeepSeq b, DeepSeq c) =>
-  DeepSeq (a, b, c) where
-  rnf (a, b, c) = rnf a `seq` rnf b `seq` rnf c
-instance (DeepSeq a, DeepSeq b, DeepSeq c, DeepSeq d) =>
-  DeepSeq (a, b, c, d) where
-  rnf (a, b, c, d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
+instance DeepSeq2 U where rnf2 U = ()
+instance (DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (a :*: b) where
+  rnf2 = foldTimes seq rnf2 rnf2
+instance DeepSeq2 a => DeepSeq2 (C dc a) where rnf2 = rnf2 . unC
+
+instance DeepSeq0 a => DeepSeq2 (T0 v a) where rnf2 = rnf0 . unT0
+instance (Functor f, DeepSeq1 f, DeepSeq2 a) => DeepSeq2 (T1 v f a) where
+  rnf2 = rnf1 . fmap rnf2 . unT1
+instance (Bifunctor f, DeepSeq2 f, DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (T2 (Rec lbl) f a b) where
+  rnf2 = rnf2 . bimap rnf2 rnf2 . unT2
+
+instance DeepSeq2 Par0 where rnf2 (Par0 ()) = ()
+instance DeepSeq2 Par1 where rnf2 (Par1 ()) = ()
+
+
+
+instance (EQ ~ SpineCompare a a, DeepSeq0 a) => DeepSeq0 [a]
+instance DeepSeq1 []
+
+instance DeepSeq0 Int where rnf0 = (`seq` ())
+instance (DeepSeq0 a, DeepSeq0 b) => DeepSeq0 (Either a b) where
+  rnf0 = either rnf0 rnf0
+
+instance (DeepSeq0 a, DeepSeq0 b, DeepSeq0 c) =>
+  DeepSeq0 (a, b, c) where
+  rnf0 (a, b, c) = rnf0 a `seq` rnf0 b `seq` rnf0 c
+instance (DeepSeq0 a, DeepSeq0 b, DeepSeq0 c, DeepSeq0 d) =>
+  DeepSeq0 (a, b, c, d) where
+  rnf0 (a, b, c, d) = rnf0 a `seq` rnf0 b `seq` rnf0 c `seq` rnf0 d
diff --git a/Examples/LambdaLift/FreeVars.hs b/Examples/LambdaLift/FreeVars.hs
--- a/Examples/LambdaLift/FreeVars.hs
+++ b/Examples/LambdaLift/FreeVars.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances, KindSignatures, DataKinds, FlexibleInstances #-}
 
 {- |
 
@@ -42,33 +42,35 @@
 
 
 class FreeVars a where freeVars :: a -> Frees
+class FreeVars2 a where freeVars2 :: a (p1 :: *) (p0 :: *) -> Frees
 
 instance FreeVars ULC where
   freeVars = w where
-    w tm = case partition $ disband tm of
+    w tm = case partition $ unW0 disband tm of
       Left x -> ($ x) $
         (\(Lam_ _ty tm) -> bump 1 $ w tm) .||
         (\(Var_ i) -> IS.singleton i) .|.
         (\(Let_ ds tm) ->
           foldr (\(Decl _ tm) -> IS.union (w tm) . bump 1) (w tm) ds)
-      Right x -> freeVars x
+      Right x -> freeVars2 x
 
 -- through sums
 --instance FreeVars sum => FreeVars (DCsOf t sum) where
 --  freeVars = freeVars . unDCsOf
-instance (FreeVars a, FreeVars b) => FreeVars (a :+: b) where
-  freeVars = foldPlus freeVars freeVars
-instance (Generic a, FreeVars (Rep a)) => FreeVars (N a) where
-  freeVars = freeVars . rep . unN
+instance (FreeVars2 a, FreeVars2 b) => FreeVars2 (a :+: b) where
+  freeVars2 = foldPlus freeVars2 freeVars2
+instance (WN dc, Generic dc, FreeVars2 (Rep dc)) => FreeVars2 (N dc) where
+  freeVars2 = freeVars2 . unSym rep unN
 
 -- through products
-instance FreeVars U where freeVars = const IS.empty
-instance (FreeVars a, FreeVars b) => FreeVars (a :*: b) where
-  freeVars = foldTimes IS.union freeVars freeVars
+instance FreeVars2 U where freeVars2 = const IS.empty
+instance (FreeVars2 a, FreeVars2 b) => FreeVars2 (a :*: b) where
+  freeVars2 = foldTimes IS.union freeVars2 freeVars2
+instance FreeVars2 a => FreeVars2 (C dc a) where freeVars2 = freeVars2 . unC
 
 -- through fields
-instance FreeVars a => FreeVars (Rec a) where
-  freeVars = freeVars . unRec
-instance FreeVars (Dep a) where freeVars = const IS.empty
-instance (Foldable f, FreeVars a) => FreeVars (Par1 f a) where
-  freeVars = foldMap freeVars . unPar1
+instance FreeVars a => FreeVars2 (T0 (Rec lbl) a) where
+  freeVars2 = freeVars . unT0
+instance FreeVars2 (T0 Dep a) where freeVars2 = const IS.empty
+instance (Foldable f, FreeVars2 a) => FreeVars2 (T1 v f a) where
+  freeVars2 = foldMap freeVars2 . unT1
diff --git a/Examples/LambdaLift/LambdaLift.hs b/Examples/LambdaLift/LambdaLift.hs
--- a/Examples/LambdaLift/LambdaLift.hs
+++ b/Examples/LambdaLift/LambdaLift.hs
@@ -28,7 +28,7 @@
 
 import LambdaLift.LLBasics
 import LambdaLift.FreeVars (freeVars)
-import LambdaLift.DeepSeq (DeepSeq(..))
+import LambdaLift.DeepSeq (DeepSeq0(..), rnf2)
 
 
 
@@ -42,12 +42,12 @@
 
 data Cnv = Cnv
 type instance Idiom Cnv = M
-instance Convert Cnv ULC TLF where convert Cnv = ll
+instance Convert0 Cnv ULC TLF where convert0 Cnv = ll
 
 
 
 ll :: ULC -> M TLF
-ll tm = precise_case tm llLam llVar llLet (Default $ hcompos Cnv)
+ll tm = precise_case0 tm llLam llVar llLet (Default $ hcompos0 Cnv)
 
 llLam lams@(Lam_ tyTop tmTop) = do
   -- get the body; count formals; determine captives
@@ -55,7 +55,7 @@
         peel (acc, ty') (Lam ty tm) = peel (ty' : acc, ty) tm
         peel acc tm = (acc, tm)
   let nLocals = 1 + length tys -- NB "1 +" is for ty
-  let captives = IS.toAscList $ freeVars $ rejoin lams
+  let captives = IS.toAscList $ freeVars $ unSym0 rejoin lams
       captives' = reverse captives
 
   (rho, rn) <- ask
@@ -117,12 +117,12 @@
 
 
 
-instance DeepSeq Type where rnf = (`seq` ())
-instance DeepSeq Occ  where
-  rnf (Par x) = rnf x
-  rnf (Env x) = rnf x
-instance DeepSeq Prog where rnf (Prog decs tm) = rnf decs `seq` rnf tm
-instance DeepSeq TLF  where rnf = rnf . reps . disband
+instance DeepSeq0 Type where rnf0 = (`seq` ())
+instance DeepSeq0 Occ  where
+  rnf0 (Par x) = rnf0 x
+  rnf0 (Env x) = rnf0 x
+instance DeepSeq0 Prog where rnf0 (Prog decs tm) = rnf0 decs `seq` rnf0 tm
+instance DeepSeq0 TLF  where rnf0 = rnf2 . unW0 ig_from
 
 
 
@@ -130,4 +130,4 @@
 -- this should evaluate without an exception if things are working; NB doesn't
 -- actually test correctness -- currently asking you to do that by
 -- investigating the value of each lambda-lifted term
-all_exs = rnf [ex0', ex1', ex2', ex3', ex4', ex5']
+all_exs = rnf0 [ex0', ex1', ex2', ex3', ex4', ex5']
diff --git a/Examples/LambdaLift/TLF.hs b/Examples/LambdaLift/TLF.hs
--- a/Examples/LambdaLift/TLF.hs
+++ b/Examples/LambdaLift/TLF.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators, DataKinds #-}
 
 {- |
 
@@ -34,7 +34,7 @@
 
 
 
-concat `fmap` mapM yokoTH [''TLF]
+concat `fmap` mapM yokoTH [''Occ, ''TLF, ''Prog]
 
 {-
 data Top_ = Top_ Int [Occ]
diff --git a/Examples/LambdaLift/ULC.hs b/Examples/LambdaLift/ULC.hs
--- a/Examples/LambdaLift/ULC.hs
+++ b/Examples/LambdaLift/ULC.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators, DataKinds #-}
 
 {- |
 
diff --git a/Examples/MinCtors.hs b/Examples/MinCtors.hs
new file mode 100644
--- /dev/null
+++ b/Examples/MinCtors.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds #-}
+
+module Examples.MinCtors where
+
+import Data.Yoko
+import Data.Yoko.MinCtors
+import Data.Yoko.MinCtors.Prims0 ()
+
+data I = I Int
+
+data H = H I
+
+data D = D0 H
+       | D1 D
+       | D2 D D
+
+concat `fmap` mapM yokoTH [''I, ''H, ''D]
+
+instance MinCtors I
+instance MinCtors H
+instance MinCtors D
+
+{-
+
+  *MinCtorsExample> minCtors (Proxy :: Proxy D)
+  Just 3
+
+This means that the minimal value uses three constructors.
+
+@* -> *@ and @* -> * -> *@ kinded types have different result types. Consider
+the minimal @(forall p1 p0. (p1, p0))@ value: it uses both of its parameters
+once, and has its own single constructor.
+
+  *MinCtorsExample> minCtors (Proxy :: Proxy (,))
+  MMap {unMMap = fromList [((1,1),Min {getMin = 1})]}
+
+Accordingly, the minimal @[]@ value uses its single parameter zero times.
+
+  *MinCtorsExample> minCtors (Proxy :: Proxy [])
+  MMap {unMMap = fromList [(0,Min {getMin = 1})]}
+
+And there are two minimal @Either@ values, each which uses one of the
+parameters. We track both because which one is ultimately minimal depends on
+the instantiation of @Either@'s parameters, and their minimal counts.
+
+  *MinCtorsExample> minCtors (Proxy :: Proxy Either)
+  MMap {unMMap = fromList [((0,1),Min {getMin = 1}),((1,0),Min {getMin = 1})]}
+
+These might not be necessary for your uses, but they are used by my generic
+definitions in order to handle types like @T@ below that have internal
+applications.
+
+-}
+
+data T = T (Either D ((Int, Int), (Bool, Bool)))
+
+yokoTH ''T
+
+instance MinCtors T
diff --git a/yoko.cabal b/yoko.cabal
--- a/yoko.cabal
+++ b/yoko.cabal
@@ -1,5 +1,5 @@
 name: yoko
-version: 0.9
+version: 2.0
 synopsis: Generic Programming with Disbanded Data Types
 
 description:
@@ -97,12 +97,12 @@
 
   build-depends: th-sccs, invariant
 
-  build-depends: type-equality, bifunctors
+  build-depends: type-equality, bifunctors, semigroups
 
   build-depends: kinds >= 0.0.1.5, type-functions >= 0.2.0.3, records >= 0.1.1.6
 
   build-depends:
-    type-spine >= 0.2, type-digits >= 0.2, type-cereal >= 0.2, type-ord >= 0.2, type-ord-spine-cereal >= 0.2
+    type-spine >= 0.2.0.20120924, type-digits >= 0.2, type-cereal >= 0.2, type-ord >= 0.2, type-ord-spine-cereal >= 0.2
 
   exposed-modules:
     Data.Yoko,
@@ -111,7 +111,16 @@
 
     Data.YokoRaw, Data.Yoko.HCompos, Data.Yoko.TH,
 
-    Data.Yoko.TypeBasics, Data.Yoko.Each
+    Data.Yoko.Invariant,
+
+    Data.Yoko.TypeBasics, Data.Yoko.W,
+
+    Data.Yoko.Prelude,
+
+    Data.Yoko.MinCtors,
+    Data.Yoko.MinCtors.Prims0, Data.Yoko.MinCtors.Prims1,
+    Data.Yoko.MinCtors.Minima,
+    Data.Yoko.MinCtors.MMap
 
   other-modules:
     Data.Yoko.View,