diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,14 @@
+0.4 -> 0.9
+===============
+
+* I integrated all of the changes made during writing up my dissertation --
+  mostly superficial/renamings, though I did realize that the DCsOf wrapper was
+  superfluous.
+
+* In particular, I renamed @exact_case@ to @precise_case@, which is
+  polyvariadic in the ad-hoc cases. This makes for code that very much
+  resembles a normal case expression.
+
 0.2 -> 0.4
 ===============
 
diff --git a/Data/Yoko.hs b/Data/Yoko.hs
--- a/Data/Yoko.hs
+++ b/Data/Yoko.hs
@@ -1,11 +1,7 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
-  MultiParamTypeClasses, FlexibleInstances, ConstraintKinds,
-  ScopedTypeVariables, UndecidableInstances #-}
-
 {- |
 
 Module      :  Data.Yoko
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -15,142 +11,33 @@
 This omnibus module is the only necessary import for using the @yoko@ generic
 programming library.
 
-However, some sophisticated functions' types might need to import the
-"Data.Yoko.TypeBasics" or "Data.Yoko.Each" modules.
+(Some sophisticated functions' types might require the import of the
+"Data.Yoko.TypeBasics" or "Data.Yoko.Each" modules.)
 
-The "Data.Yoko.HCompos" function defines the generic homomorphism; see the
-paper \"A Pattern for Almost Homomorphic Functions\" at
-<http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf>, submitted to ICFP 2012.
+The "Data.Yoko.HCompos" module defines the generic homomorphism; see the paper
+\"A Pattern for Almost Homomorphic Functions\" at
+<http://www.ittc.ku.edu/~nfrisby/frisby-wgp-2012.pdf>, published at the
+Workshop on Generic Programming 2012. Much more details in my dissertation:
+<http://www.ittc.ku.edu/~nfrisby/frisby-dissertation.pdf>.
 
 @dc@ type variables abstract over /fields types/.
 
 @dcs@ and @sum@ type variables abstract over sums of /fields types/.
 
-Types of the form @'DCsOf' t dcs@ are /disbanded data types/; for each fields
-type @dc@ in @dcs@, @'Range' dc ~ t@.
+Types of the form @'DC' t@ are /disbanded data types/; for each fields type
+@dc@ in the resulting sum, @'Codomain' dc ~ t@. That means they all correspond
+to constructors from @t@.
 
-A Template Haskell deriver is provided in the "Data.Yoko.TH" module.
+A complete Template Haskell deriver is provided in the "Data.Yoko.TH" module.
 
+It works for the data types that `instant-generics` works on, excluding indexed
+data types. Yell loudly if you need that... then send me an email :) HTH!
+
 -}
 
 module Data.Yoko
-  (module Data.Yoko.Representation,
-   module Data.Yoko.View,
-   -- * Building fields type consumers
-   one, (||.), (.||), (.|.),
-   -- * Operations on disbanded data types
-   disbanded, band, ConDCOf, exact_case,
-   -- * Operations on sums of fields types
-   (:-:), Embed, Partition,
-   inject, partition, project,
-   -- * Forgetting @yoko@'s extra structure
-   reps, EachGeneric, EachRep, ig_from,
-   Equal,
-   -- * Bundled Template Haskell
-   module Data.Yoko.TH) where
-
-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 Control.Arrow (right, (+++))
-
-
-
--- | @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) -> DCsOf (Range dc) (N dc) -> a
-one = (. unDCsOf) . foldN
-
-infixl 9 .|.
-infixr 8 .||, ||.
--- | @f .|. g = one f '|||' one g@
-f .|. g = one f ||| one g
--- | @f .|| g = one f '|||' g@
-f .|| g = one f ||| g
--- | @f ||. g = f '|||' one g@
-f ||. g = f ||| one g
-
-
-
-
-
--- | @disbanded@ injects a fields type into its disbanded range
-disbanded :: Embed (N dc) (DCs (Range dc)) => dc -> Disbanded (Range dc)
-disbanded = DCsOf . TypeSums.inject
-
--- | @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) => Disbanded t -> t
-band = each (Proxy :: Proxy (ConDCOf t)) rejoin
-
-class (Range dc ~ t, DC dc) => ConDCOf t dc
-instance (Range dc ~ t, DC dc) => ConDCOf t dc
-
-
--- | @inject@s a fields type into a sum of fields types.
-inject :: Embed (N dc) sum => dc -> sum
-inject = TypeSums.inject
-
--- | @partition@s a sum of fields type into a specified sum of fields types and
--- the remaining sum.
-partition :: Partition sum sub (sum :-: sub) =>
-             DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))
-partition = (DCsOf +++ DCsOf) . TypeSums.partition . unDCsOf
-
--- | @project@s a single fields type out of a disbanded data type.
-project :: Partition sum (N dc) (sum :-: N dc) =>
-           DCsOf (Range dc) sum -> Either dc (DCsOf (Range dc) (sum :-: N dc))
-project = right DCsOf . TypeSums.project . unDCsOf
-
-
-
--- 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 => DCsOf t sum -> EachRep sum
-reps = repEach . unDCsOf
-
-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
-
-
-
-
--- | @exact_case@ is an exactly-typed case: the second argument is the
--- discriminant, the first argument is the default case, and the third argument
--- approximates a list of alternatives.
---
--- @
--- exact_case default x $
---   (\(C0_ ...) -> ...) '.||'
---   (\(C1_ ...) -> ...) '.|.'
---   (\(C2_ ...) -> ...)
--- @
---
--- 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.
-exact_case :: (DT t, Partition (DCs t) dcs (DCs t :-: dcs)) =>
-  (DCsOf t (DCs t :-: dcs) -> a) -> t -> (DCsOf t dcs -> a) -> a
-exact_case g x f =
-  either f g $ partition $ disband x
+  (module Data.YokoRaw, module Data.Yoko.SmartPreciseCase)
+  where
 
--- | @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
+import Data.YokoRaw hiding (precise_case)
+import Data.Yoko.SmartPreciseCase
diff --git a/Data/Yoko/Each.hs b/Data/Yoko/Each.hs
--- a/Data/Yoko/Each.hs
+++ b/Data/Yoko/Each.hs
@@ -4,7 +4,7 @@
 {- |
 
 Module      :  Data.Yoko.Each
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -44,12 +44,12 @@
 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
+--instance Each_ cxt sum => Each_ cxt (DCsOf t sum) where
+--  each_ c f = each c f . unDCsOf
 
 
 
 
 
-ex = putStrLn $ each (Proxy :: Proxy Show) show $
+_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,13 +1,13 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
   FlexibleContexts, FlexibleInstances, UndecidableInstances,
-  ScopedTypeVariables  #-}
+  ScopedTypeVariables, DataKinds  #-}
 
 {-# OPTIONS_GHC -fcontext-stack=250 #-}
 
 {- |
 
 Module      :  Data.Yoko.HCompos
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -16,72 +16,109 @@
 
 The generic homomorphism or \"heterogenous compos\".
 
-See the paper \"A Pattern for Almost Homomorphic Functions\" at <http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf>, submitted to ICFP 2012.
+See the paper \"A Pattern for Almost Homomorphic Functions\" at <http://www.ittc.ku.edu/~nfrisby/frisby-2012-wgp.pdf>, presented at the Workshop on Generic Programming 2012.
 
 -}
 
-module Data.Yoko.HCompos (Idiom, HCompos(..), FindDCs) where
+module Data.Yoko.HCompos where
 
 import Data.Yoko.TypeBasics
 import Data.Yoko
 
 import Control.Applicative
+import Data.Traversable (Traversable, traverse)
+import Data.Bitraversable (Bitraversable, bitraverse)
 
+import Type.Digits (Digit)
 
 
 
 
-instance HCompos cnv sum t => HCompos cnv (DCsOf a sum) t where
-  hcompos cnv = hcompos cnv . unDCsOf
 
-
-
-
 -- | The applicative functor required by the conversion.
 type family Idiom cnv :: * -> *
--- | The conversion @cnv@ can convert from @a@ to @t@.
+
+-- | 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
+
+-- | 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
 
 
 
 
+-- 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 = ($)
 
+
+
+
+
+data FoundDC star = NoCorrespondingConstructorFor_In_ star star | Match star
+
+type family WithMessage (dcA :: *) (b :: *) (dcB :: Maybe *) :: FoundDC *
+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 instance FindDCs s (N dc) =
+  If   (Equal s (Tag dc))   (Just 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)
 
 -- NB only works if there's exactly one matching constructor
-instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
-          HComposRs cnv (Rep dc) (Rep dc'),
-          DC dc', Range dc' ~ t, DT t
-         ) => HCompos cnv (N dc) t where
-  hcompos cnv = 
-    foldN $ liftA (rejoin . (id :: dc' -> dc') . obj) . mapRs cnv . rep
+instance (Generic dcA, Match dcB ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),
+          MapRs 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
+    where p1 :: Proxy dcA; p1 = Proxy; p2 :: Proxy dcB; p2 = Proxy
+          msgp = ResultsInIncompatibleFields :: ResultsInIncompatibleFields dcA dcB
 
+data ResultsInIncompatibleFields (dcA :: *) (dcB :: *) = ResultsInIncompatibleFields
 
 
--- | @FindDCs s sum@ returns a type-level @Maybe@. @Just dc@ is a fields type
--- @dc@ where @'Tag' dc ~ s@.
-type family FindDCs s sum
-type instance FindDCs s (N dc) =
-  If (Equal s (Tag dc)) (Just (N dc)) Nothing
-type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)
 
+-- applies cnv to every Rec in a product; identity on other factors; the dc and
+-- dc' parameters are just for error messages: all instances treat them
+-- parametrically
 
+-- | 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'
 
--- applies cnv to every Rec in a product; identity on other factors
-class Applicative (Idiom cnv) => HComposRs cnv prod prod' where
-  mapRs :: cnv -> prod -> Idiom cnv prod'
+instance Convert cnv a b => MapRs cnv msg dc dc' (Rec a) (Rec b) where
+  mapRs cnv _ _ _ (Rec x) = Rec <$> convert cnv x
 
-instance HCompos cnv a b => HComposRs cnv (Rec a) (Rec b) where
-  mapRs cnv (Rec x) = Rec <$> hcompos cnv x
+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 Applicative (Idiom cnv) => HComposRs cnv (Dep a) (Dep a) where
-  mapRs _ = pure
-instance Applicative (Idiom cnv) => HComposRs cnv U       U       where
-  mapRs _ = pure
+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 (HComposRs cnv a a', HComposRs cnv b b'
-         ) => HComposRs cnv (a :*: b) (a' :*: b') where
-  mapRs cnv (a :*: b) = (:*:) <$> mapRs cnv a <*> mapRs cnv b
+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 (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
diff --git a/Data/Yoko/MaybeKind.hs b/Data/Yoko/MaybeKind.hs
--- a/Data/Yoko/MaybeKind.hs
+++ b/Data/Yoko/MaybeKind.hs
@@ -1,27 +1,40 @@
-{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
 
+{- |
+
+Module      :  Data.Yoko.MaybeKind
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+Some interface functions for type-level @Maybe@ (and @Bool@s). These functions
+are probably ripe for the @promotion@ library of Eisenberg, Weirich, et alia?
+
+-}
+
 module Data.Yoko.MaybeKind
   (-- ** Type-level @Maybe@
-   Nothing, Just,
-   IsJust, MaybePlus1, MaybeMap
+   IsJust, MaybePlus1, MaybeMap, If
    ) where
 
-import Type.Booleans
-
-data Nothing
-data Just (x :: *)
+type family If (c :: Bool) (a :: k) (b :: k) :: k
+type instance If True  a b = a
+type instance If False a b = b
 
 -- | Returns a type-level boolean from @type-booleans@.
-type family IsJust (x :: *) :: * -- returns Bool, ideally
+type family IsJust (x :: Maybe k) :: Bool
 type instance IsJust Nothing = False
 type instance IsJust (Just x) = True
 
 -- | Type-level @mplus@ for @Maybe@.
-type family MaybePlus1 (x :: *) (y :: *) :: *
+type family MaybePlus1 (x :: Maybe k) (y :: Maybe k) :: Maybe k
 type instance MaybePlus1 Nothing y = y
 type instance MaybePlus1 (Just x) Nothing = Just x
 
 -- | Type-level @fmap@ for @Maybe@.
-type family MaybeMap (f :: * -> *) (x :: *) :: *
+type family MaybeMap (f :: k -> l) (x :: Maybe k) :: Maybe l
 type instance MaybeMap f (Just x) = Just (f x)
 type instance MaybeMap f Nothing = Nothing
diff --git a/Data/Yoko/Representation.hs b/Data/Yoko/Representation.hs
--- a/Data/Yoko/Representation.hs
+++ b/Data/Yoko/Representation.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, TemplateHaskell,
-  UndecidableInstances, EmptyDataDecls #-}
+  UndecidableInstances, EmptyDataDecls, DataKinds #-}
 
 {- |
 
 Module      :  Data.Yoko.Representation
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -18,17 +18,15 @@
 module Data.Yoko.Representation
   (-- * Representation
    -- ** Sums
-   Void(..), N(..), (:+:)(..), DCsOf(..),
+   Void(..), N(..), (:+:)(..),
    -- ** Products
    U(..), (:*:)(..),
    -- ** Fields
    Rec(..), Dep(..), Par1(..), Par2(..),
    -- ** Conversions to and from fields-of-products structure
    Rep, Generic(..),
-   -- ** Building disbanded data type consumers
-   (|||),
    -- ** Auxilliaries
-   unDCsOf, unN, foldN, mapN,
+   unN, foldN, mapN,
    foldPlus, mapPlus,
    foldTimes, mapTimes,
    unRec, mapRec, unDep, unPar1, unPar2,
@@ -114,7 +112,7 @@
 -- | 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 b
+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)
@@ -136,21 +134,4 @@
 
 
 
--- | A disbanded data type is an application of @DCsOf t@ to a sum of fields
--- types all of which have @t@ as their range. The use of @DCsOf@'s first
--- parameter throughout the API (e.g. in '|||') supplants many ascriptions.
-newtype DCsOf t sum = DCsOf sum   ;   unDCsOf (DCsOf x) = x
-instance Functor (DCsOf t) where fmap f = DCsOf . f . unDCsOf
-
-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.
-(|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) ->
-         DCsOf t (sumL :+: sumR) -> a
-(|||) f g = foldPlus f g . mapPlus DCsOf DCsOf . unDCsOf
-
-
-
-
-
-concat `fmap` mapM derive [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]
+concat `fmap` mapM derive_data [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]
diff --git a/Data/Yoko/SmartPreciseCase.hs b/Data/Yoko/SmartPreciseCase.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/SmartPreciseCase.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances #-}
+
+{- |
+
+Module      :  Data.Yoko.SmartPreciseCase
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+Using some McBride \"Faking It\" style trickery to make @precise_case@
+polyvariadic in the ad-hoc cases.
+
+E.g.
+
+> precise_case x (\(C_ a b) -> special_case a b) (Default $ \x -> generic_function x)
+
+and
+
+> precise_case x (\(C_ a b) -> special_case a b) (\(D_ x) -> special_case2 x) (Default $ \x -> generic_function x)
+
+both work.
+
+-}
+
+module Data.Yoko.SmartPreciseCase where
+
+import Data.YokoRaw hiding (precise_case)
+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
+
+
+
+
+
+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
+  precise_case_ = error "precise_case_ requires at least 1 special case"
+
+newtype Start dt = Start dt
+
+instance (dt ~ Codomain dc,
+          Builder (AdHoc (N dc) (Codomain dc) r) bldr) =>
+  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,
+          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),
+          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
+
+precise_case :: Builder (Start dt) bldr => dt -> bldr
+precise_case = precise_case_ . Start
+
+
+
+
+{-
+
+data T = A | B Int | C Bool
+
+yokoTH ''T
+
+
+
+
+*PreciseCase> precise_case A (\(B_ i) -> i) (Default $ const 0)
+0
+*PreciseCase> precise_case (B 3) (\(B_ i) -> i) (Default $ const 0)
+3
+*PreciseCase> precise_case (B 3) (\(B_ i) -> i) (\A_ -> 1) (Default $ const 0)
+3
+*PreciseCase> precise_case A (\(B_ i) -> i) (\A_ -> 1) (Default $ const 0)
+1
+
+-}
diff --git a/Data/Yoko/TH.hs b/Data/Yoko/TH.hs
--- a/Data/Yoko/TH.hs
+++ b/Data/Yoko/TH.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards #-}
+{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards, DataKinds #-}
 
 {- |
 
 Module      :  Data.Yoko.TH
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -13,7 +13,7 @@
 This bundled Template Haskell derives all fields types and @yoko@ instances for
 users' data types.
 
-'yokoTH' is the prinicpal deriver, but it can be customized in two ways via
+'yokoTH' is the principal deriver, but it can be customized in two ways via
 'yokoTH_with'. First, the user can specify how to derive the names of fields
 types from the original constructor name -- the default is @(++ \"_\")@.
 Second, the user can specify how to represent composite fields that include
@@ -62,16 +62,16 @@
    YokoOptions(..), Mapping(..), yokoDefaults
   ) where
 
-import Type.Spine.Stage0 (Spine, spineType_, kTypeG)
-import Type.Serialize (serializeTypeAsHash_)
+import Type.Spine (Spine, spineType_d_)
+import Type.Serialize (serializeTypeAsHash_data)
 import qualified Type.Ord as Ord
 
 import Data.Yoko.TypeBasics (encode)
 import Data.Yoko.Representation
 import Data.Yoko.View
 
-import Language.Haskell.TH as TH hiding (Range)
-import Language.Haskell.TH.Syntax as TH hiding (Range)
+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
 
 import qualified Data.Yoko.TH.Internal as Int
@@ -174,8 +174,8 @@
 
   -- get the kind of the target type; each fields type has the same kind
   cxt <- flip mapM tvbs $ \tvb -> liftQ $
-    EqualP (ConT ''Ord.EQ) `fmap` do
-      let tv = [t| Spine ($(kTypeG (tvbKind tvb)) $(return $ tvbType tvb)) |]
+    EqualP (PromotedT 'EQ) `fmap` do
+      let tv = [t| Spine $(return $ tvbType tvb) |]
       [t| Ord.Compare $tv $tv |]
 
   yoko1 $ r :&
@@ -198,7 +198,7 @@
 renameCon f (ForallC tvbs cxt c) = ForallC tvbs cxt $ renameCon f c
 
 tvbKind :: TyVarBndr -> Kind
-tvbKind (PlainTV _) = StarK
+tvbKind (PlainTV _) = StarT
 tvbKind (KindedTV _ k) = k
 
 tvbType :: TyVarBndr -> Type
@@ -252,7 +252,7 @@
         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,
@@ -298,10 +298,10 @@
 
     fields <- conFields con
 
-    -- declare the fields type and its Range/Tag/DC instances
+    -- declare the fields type and its Codomain/Tag/DC instances
     let yokoD = 
           [Int.dataType2Dec n' (Int.DataType tvbs (Right [renameCon rn con])),
-           TySynInstD ''Range [fd] ty,
+           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
@@ -337,8 +337,8 @@
                                foldl AppE (ConE n') $ objE conRO]]]
 
     -- integrate with type-spine and type-cereal
-    spineD <- spineType_ (mkG n') ks StarK
-    cerealD <- serializeTypeAsHash_ (mkG n') ks StarK
+    spineD <- spineType_d_ (mkG n') ks
+    cerealD <- serializeTypeAsHash_data (mkG n')
 
     return $ yokoD ++ spineD ++ cerealD ++ genD
        | con <- either (:[]) id cons ]) >>= generate . concat
@@ -373,6 +373,6 @@
 
   cases <- return $ flip map cases $ \(inj, (n, fds)) ->
     let (pat, exp) = pat_exp n (rn n) fds
-    in simpleClause [pat] $ postConE 'DCsOf inj `AppE` exp
+    in simpleClause [pat] $ inj `AppE` exp
   generate $ [TySynInstD ''DCs [ty] dcs,
               InstanceD cxt (ConT ''DT `AppT` ty) [FunD 'disband cases]]
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
@@ -1,5 +1,19 @@
 {-# LANGUAGE ViewPatterns #-}
 
+{- |
+
+Module      :  Data.Yoko.TH.Internal
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+Some bits and pieces for the Template Haskell deriver.
+
+-}
+
 module Data.Yoko.TH.Internal where
 
 import Data.Maybe (fromMaybe)
@@ -45,6 +59,7 @@
 peelApp :: Type -> (Type, [Type])
 peelApp = peelAppAcc []
 
+peelAppAcc :: [Type] -> Type -> (Type, [Type])
 peelAppAcc acc (AppT ty0 ty1) = peelAppAcc (ty1 : acc) ty0
 peelAppAcc acc ty             = (ty, acc)
 
diff --git a/Data/Yoko/TypeBasics.hs b/Data/Yoko/TypeBasics.hs
--- a/Data/Yoko/TypeBasics.hs
+++ b/Data/Yoko/TypeBasics.hs
@@ -3,7 +3,7 @@
 {- |
 
 Module      :  Data.Yoko.TypeBasics
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -15,18 +15,17 @@
 -}
 
 module Data.Yoko.TypeBasics (
-  Proxy(..), Equal, derive,
+  Proxy(..), Equal, derive_data, derive_pro,
   -- ** Re-exports
-  module Data.Yoko.MaybeKind, module Type.Booleans, encode
+  module Data.Yoko.MaybeKind, encode
   ) where
 
-import Type.Booleans
 import Data.Yoko.MaybeKind
 
 import Type.Spine
 import Type.Ord (IsEQ)
 import Type.Serialize
-import Type.Ord.SpineSerialize (Compare)
+import Type.Ord.SpineSerialize (SpineCompare)
 
 
 
@@ -35,14 +34,18 @@
 
 
 
--- | Convenient synonym. @type Equal a b = 'IsEQ' ('Compare' a b)@
-type Equal a b = IsEQ (Compare a b)
+-- | Convenient synonym. @type Equal a b = 'IsEQ' ('SpineCompare' a b)@
+type Equal a b = IsEQ (SpineCompare a b)
 
 
 
 -- | Template Haskell derivation for the @type-spine@ and @type-cereal@
 -- packages' 'Spine' and 'Serialize' type families, which support generic
 -- instances of 'Compare'.
-derive n = do
-  d <- spineType n
-  (d ++) `fmap` serializeTypeAsHash n
+derive_data n = do
+  d <- spineType_d n
+  (d ++) `fmap` serializeTypeAsHash_data n
+
+derive_pro n = do
+  d <- spineType_pro n
+  (d ++) `fmap` serializeTypeAsHash_pro n
diff --git a/Data/Yoko/TypeSums.hs b/Data/Yoko/TypeSums.hs
--- a/Data/Yoko/TypeSums.hs
+++ b/Data/Yoko/TypeSums.hs
@@ -6,6 +6,20 @@
 
 {-# OPTIONS_GHC -fcontext-stack=250 #-}
 
+{- |
+
+Module      :  Data.Yoko.TypeSums
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+This is the technical core of @yoko@'s cheap constructor subsets.
+
+-}
+
 module Data.Yoko.TypeSums (DistMaybePlus, (:-:),
                            Embed, embed, inject,
                            Partition, project, partition) where
@@ -15,7 +29,6 @@
 
 import Control.Arrow (left)
 
-import Data.Yoko.TypeSumsAux (Partition_N(..))
 
 
 
@@ -48,7 +61,7 @@
 data TurnLeft path
 data TurnRight path
 
-type family Locate a sum
+type family Locate a sum :: Maybe *
 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`
@@ -90,7 +103,7 @@
 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 
+type instance Combine (N x) (N y) = N x :+: N y
 type instance Combine (N x) (l :+: r) = N x :+: (l :+: r)
 type instance Combine (l :+: r) Void = l :+: r
 type instance Combine (l :+: r) (N y) = (l :+: r) :+: N y
@@ -98,6 +111,8 @@
 
 
 
+class Partition_N (bn :: Bool) x subL subR where
+  partition_N :: Proxy bn -> N x -> Either subL subR
 
 instance (Partition_N (Elem x subL) x subL subR
          ) => Partition (N x) subL subR where
diff --git a/Data/Yoko/TypeSumsAux.hs b/Data/Yoko/TypeSumsAux.hs
deleted file mode 100644
--- a/Data/Yoko/TypeSumsAux.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, KindSignatures #-}
-
-module Data.Yoko.TypeSumsAux where
-
-import Data.Yoko.TypeBasics
-import Data.Yoko.Representation
-
-
-
--- this * is Bool, ideally
-class Partition_N (bn :: *) x subL subR where
-  partition_N :: Proxy bn -> N x -> Either subL subR
diff --git a/Data/Yoko/View.hs b/Data/Yoko/View.hs
--- a/Data/Yoko/View.hs
+++ b/Data/Yoko/View.hs
@@ -1,11 +1,10 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
-  MultiParamTypeClasses, FlexibleInstances, ConstraintKinds,
-  UndecidableInstances #-}
+  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds #-}
 
 {- |
 
 Module      :  Data.Yoko.View
-Copyright   :  (c) The University of Kansas 2011
+Copyright   :  (c) The University of Kansas 2012
 License     :  BSD3
 
 Maintainer  :  nicolas.frisby@gmail.com
@@ -19,38 +18,40 @@
 module Data.Yoko.View
   (-- * Reflection
    -- ** Fields types
-   Tag, Range, DC(..),
+   Tag, Codomain, DC(..),
    -- ** Disbanded data types
-   DCs, Disbanded, DT(..)
+   DCs, DT(..)
   ) where
 
 import Data.Yoko.Representation
 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
+type family Tag dc :: Digit
 
--- | @Range@ is the data type that contains the constructor that the fields
--- type @dc@ represents.
-type family Range dc
+-- | @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
 
 -- | 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 (Range dc)) => DC dc where rejoin :: dc -> Range dc
+class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: dc -> Codomain dc
 
 -- | The @DCs@ of a data type is sum of all of its fields types.
 type family DCs t
--- | A disbanded data type is the data type's @DCs@ annotated with it.
-type Disbanded t = DCsOf t (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 -> Disbanded t
+class Each IsDCOf (DCs t) => DT t where disband :: t -> DCs t
 
-class (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),
-       Embed (N dc) (DCs (Range dc))) => IsDCOf dc
-instance (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),
-          Embed (N dc) (DCs (Range dc))) => IsDCOf dc
+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
diff --git a/Data/YokoRaw.hs b/Data/YokoRaw.hs
new file mode 100644
--- /dev/null
+++ b/Data/YokoRaw.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
+  MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables,
+  UndecidableInstances #-}
+
+{- |
+
+Module      :  Data.YokoRaw
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+This is the entire library, excluding the fancy builder of precise cases from
+"Data.Yoko.SmartPreciseCase".
+
+-}
+
+module Data.YokoRaw
+  (module Data.Yoko.Representation,
+   module Data.Yoko.View,
+   -- * Building fields type consumers
+   one, (|||), (||.), (.||), (.|.),
+   -- * Operations on disbanded data types
+   disbanded, band, ConDCOf, precise_case,
+   -- * 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
+
+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
+
+
+
+-- | @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
+
+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
+(|||) = foldPlus
+
+infixl 9 .|.
+infixr 8 .||, ||.
+-- | @f .|. g = one f '|||' one g@
+f .|. g = one f ||| one g
+-- | @f .|| g = one f '|||' g@
+f .|| g = one f ||| g
+-- | @f ||. g = f '|||' one g@
+f ||. g = f ||| one g
+
+
+
+
+
+-- | @disbanded@ injects a fields type into its disbanded range
+disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc)
+disbanded = TypeSums.inject
+
+-- | @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
+
+class (Codomain dc ~ t, DC dc) => ConDCOf t dc
+instance (Codomain dc ~ t, DC dc) => ConDCOf t dc
+
+embed :: (Codomain sub ~ Codomain sup, Embed sub sup) => sub -> sup
+embed = TypeSums.embed
+
+
+-- | @inject@s a fields type into a sum of fields types.
+inject :: Embed (N dc) sum => dc -> sum
+inject = TypeSums.inject
+
+-- | @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 = 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
+
+
+
+-- 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 = repEach
+
+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
+
+
+
+
+-- | @precise_case@ is an exactly-typed case: the second argument is the
+-- discriminant, the first argument is the default case, and the third argument
+-- approximates a list of alternatives.
+--
+-- @
+-- precise_case default x $
+--   (\(C0_ ...) -> ...) '.||'
+--   (\(C1_ ...) -> ...) '.|.'
+--   (\(C2_ ...) -> ...)
+-- @
+--
+-- 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
+
+-- | @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
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,17 @@
+{- |
+
+Module      :  LambdaLift.Common
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.Common where
 
 data Type = TyUnit | TyInt | TyFun Type Type deriving Show
diff --git a/Examples/LambdaLift/DeepSeq.hs b/Examples/LambdaLift/DeepSeq.hs
--- a/Examples/LambdaLift/DeepSeq.hs
+++ b/Examples/LambdaLift/DeepSeq.hs
@@ -1,6 +1,20 @@
 {-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
   UndecidableInstances #-}
 
+{- |
+
+Module      :  LambdaLift.DeepSeq
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.DeepSeq where
 
 import Data.Yoko
@@ -14,7 +28,7 @@
 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 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
diff --git a/Examples/LambdaLift/FreeVars.hs b/Examples/LambdaLift/FreeVars.hs
--- a/Examples/LambdaLift/FreeVars.hs
+++ b/Examples/LambdaLift/FreeVars.hs
@@ -1,5 +1,19 @@
 {-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances #-}
 
+{- |
+
+Module      :  LambdaLift.FreeVars
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.FreeVars where
 
 import LambdaLift.ULC
@@ -33,15 +47,15 @@
   freeVars = w where
     w tm = case partition $ disband tm of
       Left x -> ($ x) $
-        (\(Lam_ ty tm) -> bump 1 $ w tm) .||
+        (\(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
 
 -- through sums
-instance FreeVars sum => FreeVars (DCsOf t sum) where
-  freeVars = freeVars . unDCsOf
+--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
diff --git a/Examples/LambdaLift/LLBasics.hs b/Examples/LambdaLift/LLBasics.hs
--- a/Examples/LambdaLift/LLBasics.hs
+++ b/Examples/LambdaLift/LLBasics.hs
@@ -1,6 +1,20 @@
 {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies,
   UndecidableInstances #-}
 
+{- |
+
+Module      :  LambdaLift.LLBasics
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.LLBasics where
 
 import LambdaLift.Common
diff --git a/Examples/LambdaLift/LambdaLift.hs b/Examples/LambdaLift/LambdaLift.hs
--- a/Examples/LambdaLift/LambdaLift.hs
+++ b/Examples/LambdaLift/LambdaLift.hs
@@ -1,5 +1,19 @@
 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
 
+{- |
+
+Module      :  LambdaLift.LambdaLift
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.LambdaLift where
 
 import LambdaLift.Common
@@ -28,12 +42,12 @@
 
 data Cnv = Cnv
 type instance Idiom Cnv = M
-instance HCompos Cnv ULC TLF where hcompos Cnv = ll
+instance Convert Cnv ULC TLF where convert Cnv = ll
 
 
 
 ll :: ULC -> M TLF
-ll tm = exact_case (hcompos Cnv) tm $ llLam .|| llVar .|. llLet
+ll tm = precise_case tm llLam llVar llLet (Default $ hcompos Cnv)
 
 llLam lams@(Lam_ tyTop tmTop) = do
   -- get the body; count formals; determine captives
@@ -41,23 +55,26 @@
         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 = freeVars $ rejoin lams
-      captives' = IS.toAscList captives
-      captives'' = reverse captives'
+  let captives = IS.toAscList $ freeVars $ rejoin lams
+      captives' = reverse captives
 
   (rho, rn) <- ask
 
   -- generate a top-level function from the body
-  do let m = IM.fromDistinctAscList $ zip captives' [0..]
+  do let m = IM.fromDistinctAscList $ zip captives [0..]
      tlf <- ignoreEmissions $
             local (const (ty : tys ++ rho, (nLocals, m))) $ ll ulc
-     emit (map (rho !!) captives'', reverse tys, ty, tlf)
+     emit (map (rho !!) $ captives', reverse tys, ty, tlf)
 
   -- replace lambdas with an invocation of tlf
   sh <- intermediates
 
-  return $ Top (sh - 1) $ map (lookupRN rn) $ captives''
+  return $ Top sh $ map (lookupRN rn) $ captives'
+
+-- just look up a variables new location (ie now from new closure's environment or parameters)
 llVar (Var_ i) = ask >>= \(_, rn) -> return $ Occ $ lookupRN rn i
+
+-- also simultaneously elaborate lets
 llLet (Let_ ds tm) = ll $ foldr (\(Decl ty tm) x -> A.App (Lam ty tm) x) tm ds
 
 
@@ -91,50 +108,15 @@
 ex4 = Lam (TyFun TyInt TyInt) (Var 0) @@ Lam TyInt (Var 0)
 ex4' = lambdaLift [] ex4
 
+-- note, ill-typed, but the types don't really matter as long as the LL
+-- preserves them
 ex5 = Lam (TyFun (TyFun TyInt TyInt) (TyFun TyInt TyInt)) (Var 0) @@
       Lam (TyFun TyInt TyInt)
           (Lam TyUnit (Var 1) @@ Var 1)
 ex5' = lambdaLift [TyUnit] ex5
 
--- TODO can I make the Tops use scoped instead of global indices?
 
-{-
-ex0' ==
-Prog [([],[],TyInt,Var 0)
-     ] (Top 0 [])
 
-ex1' ==
-Prog [([],[TyFun TyInt (TyFun TyInt TyInt),TyFun TyInt TyInt],TyInt,
-         App (App (Var 2) (Var 0)) (App (Var 1) (Var 0))),
-      ([],[TyInt],TyInt,Var 0),
-      ([TyFun TyInt TyInt,TyInt],[],TyUnit,App (Var ^1) (Var ^0))
-     ] (App (App (Top 0 []) (Top 1 [])) (Top 2 [1,0]))
-
-ex2' ==
-Prog [([TyFun TyInt TyInt],[],TyInt,App (Var ^0) (Var 0)),
-      ([],[TyFun (TyFun TyInt TyInt) TyUnit],TyFun TyInt TyInt,
-         App (Var 1) (Top 0 [0]))
-     ] (Top 1 [])
-
-ex3' ==
-Prog [([TyUnit],[],TyInt,Var ^0),
-      ([TyUnit],[],TyUnit,App (Var ^0) (Top 0 [0])),
-      ([],[TyUnit,TyUnit],TyUnit,App (Var 1) (Top 1 [2]))
-     ] (Top 2 [])
-
-ex4' ==
-Prog [([],[],TyFun TyInt TyInt,Var 0),
-      ([],[],TyInt,Var 0)
-     ] (App (Top 0 []) (Top 1 []))
-
-ex5' ==
-Prog [([],[],TyFun (TyFun TyInt TyInt) (TyFun TyInt TyInt),Var 0),
-      ([TyFun TyInt TyInt],[],TyUnit,Var ^0),
-      ([TyUnit],[],TyFun TyInt TyInt,App (Top 1 [0]) (Var ^0))
-     ] (App (Top 0 []) (Top 2 [0]))
-
--}
-
 instance DeepSeq Type where rnf = (`seq` ())
 instance DeepSeq Occ  where
   rnf (Par x) = rnf x
@@ -142,4 +124,10 @@
 instance DeepSeq Prog where rnf (Prog decs tm) = rnf decs `seq` rnf tm
 instance DeepSeq TLF  where rnf = rnf . reps . disband
 
+
+
+
+-- 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']
diff --git a/Examples/LambdaLift/TLF.hs b/Examples/LambdaLift/TLF.hs
--- a/Examples/LambdaLift/TLF.hs
+++ b/Examples/LambdaLift/TLF.hs
@@ -1,8 +1,21 @@
 {-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
 
+{- |
+
+Module      :  LambdaLift.TLF
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.TLF where
 
-import Data.Yoko.TypeBasics (encode, derive)
 import Data.Yoko
 
 import LambdaLift.Common
@@ -21,23 +34,24 @@
 
 
 
-
+concat `fmap` mapM yokoTH [''TLF]
 
+{-
 data Top_ = Top_ Int [Occ]
 data Occ_ = Occ_ Occ
 data App_  = App_ TLF TLF
 
 
 
-type instance Range Top_ = TLF
-type instance Range Occ_  = TLF
-type instance Range App_  = TLF
+type instance Codomain Top_ = TLF
+type instance Codomain Occ_  = TLF
+type instance Codomain App_  = TLF
 
 type instance Tag Top_ = $(return $ encode "Top")
 type instance Tag Occ_ = $(return $ encode "Occ")
 type instance Tag App_  = $(return $ encode "App")
 
-concat `fmap` mapM derive [''TLF, ''Top_, ''Occ_, ''App_]
+concat `fmap` mapM derive_data [''TLF, ''Top_, ''Occ_, ''App_]
 
 
 
@@ -58,9 +72,10 @@
 
 type instance DCs TLF = (N Top_ :+: N Occ_) :+: N App_
 instance DT TLF where
-  disband (Top i os )   = DCsOf . inject $ Top_ i os
-  disband (Occ o)       = DCsOf . inject $ Occ_ o
-  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
+  disband (Top i os )   = inject $ Top_ i os
+  disband (Occ o)       = inject $ Occ_ o
+  disband (App tm1 tm2) = inject $ App_ tm1 tm2
 instance DC Top_ where rejoin (Top_ i os)    = Top i os
 instance DC Occ_ where rejoin (Occ_  o)      = Occ o
 instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2
+-}
diff --git a/Examples/LambdaLift/ULC.hs b/Examples/LambdaLift/ULC.hs
--- a/Examples/LambdaLift/ULC.hs
+++ b/Examples/LambdaLift/ULC.hs
@@ -1,9 +1,22 @@
 {-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
 
+{- |
+
+Module      :  LambdaLift.ULC
+Copyright   :  (c) The University of Kansas 2012
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+An example lambba lifter using @hcompos@.
+
+-}
+
 module LambdaLift.ULC where
 
 import Data.Yoko
-import Data.Yoko.TypeBasics (encode, derive)
 import LambdaLift.Common
 
 
@@ -15,6 +28,9 @@
 data Decl = Decl Type ULC deriving Show
 
 
+concat `fmap` mapM yokoTH [''ULC, ''Decl]
+
+{-
 data Lam_ = Lam_ Type ULC
 data Var_ = Var_ Int
 data Let_ = Let_ [Decl] ULC
@@ -24,12 +40,12 @@
 
 
 
-type instance Range Lam_ = ULC
-type instance Range Var_ = ULC
-type instance Range Let_ = ULC
-type instance Range App_ = ULC
+type instance Codomain Lam_ = ULC
+type instance Codomain Var_ = ULC
+type instance Codomain Let_ = ULC
+type instance Codomain App_ = ULC
 
-type instance Range Decl_ = Decl
+type instance Codomain Decl_ = Decl
 
 type instance Tag Lam_ = $(return $ encode "Lam")
 type instance Tag Var_ = $(return $ encode "Var")
@@ -38,7 +54,7 @@
 
 type instance Tag Decl_ = $(return $ encode "Decl")
 
-concat `fmap` mapM derive [''ULC, ''Decl, ''Lam_, ''Var_, ''Let_, ''App_, ''Decl_]
+concat `fmap` mapM derive_data [''ULC, ''Decl, ''Lam_, ''Var_, ''Let_, ''App_, ''Decl_]
 
 
 
@@ -69,10 +85,10 @@
 type instance DCs ULC =
   (N Lam_ :+: N Var_) :+: (N Let_ :+: N App_)
 instance DT ULC where
-  disband (Lam ty tm)   = DCsOf . inject $ Lam_ ty tm
-  disband (Var i)       = DCsOf . inject $ Var_ i
-  disband (Let ds tm)   = DCsOf . inject $ Let_ ds tm
-  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
+  disband (Lam ty tm)   = inject $ Lam_ ty tm
+  disband (Var i)       = inject $ Var_ i
+  disband (Let ds tm)   = inject $ Let_ ds tm
+  disband (App tm1 tm2) = inject $ App_ tm1 tm2
 instance DC Lam_ where rejoin (Lam_ ty tm)   = Lam ty tm
 instance DC Var_ where rejoin (Var_ i)       = Var i
 instance DC Let_ where rejoin (Let_ ds tm)   = Let ds tm
@@ -80,5 +96,6 @@
 
 type instance DCs Decl = N Decl_
 instance DT Decl where
-  disband (Decl ty tm) = DCsOf . N $ Decl_ ty tm
+  disband (Decl ty tm) = N $ Decl_ ty tm
 instance DC Decl_ where rejoin (Decl_ ty tm) = Decl ty tm
+-}
diff --git a/Examples/Test.hs b/Examples/Test.hs
--- a/Examples/Test.hs
+++ b/Examples/Test.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies, TemplateHaskell, UndecidableInstances #-}
 
 {-# OPTIONS_GHC -ddump-splices #-}
 
@@ -13,7 +13,7 @@
 data X = X
 
 
-concat `fmap` mapM derive [''T, ''X]
+concat `fmap` mapM yokoTH [''T, ''X, ''Maybe]
 
 
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2011, University of Kansas
+Copyright (c) 2012, University of Kansas
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/README b/README
--- a/README
+++ b/README
@@ -1,1 +1,1 @@
-Read the paper at http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf
+Read the paper at http://www.ittc.ku.edu/~nfrisby/papers/frisby-wgp-2012.pdf
diff --git a/yoko.cabal b/yoko.cabal
--- a/yoko.cabal
+++ b/yoko.cabal
@@ -1,9 +1,12 @@
 name: yoko
-version: 0.3.2.2
+version: 0.9
 synopsis: Generic Programming with Disbanded Data Types
 
 description:
-  Based off of the paper \"A Pattern for Almost Homomorphic Functions\" at <http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf>, submitted to ICFP 2012.
+  Based off of the paper \"A Pattern for Almost Homomorphic Functions\"
+  at <http://www.ittc.ku.edu/~nfrisby/frisby-wgp-2012.pdf>, presented at the
+  Workshop on Generic Programming 2012. Also, my
+  dissertation <http://www.ittc.ku.edu/~nfrisby/frisby-dissertation.pdf>
   .
   @yoko@ views a nominal datatype as a /band/ of constructors, each
   a nominal type in its own right. Such datatypes can be disbanded via the
@@ -19,7 +22,7 @@
   @
   .
   This type can of course be understood as a sum of the individual
-  /constructor types/.
+  /fields types/.
   .
   @
     data John   = John   ...
@@ -33,10 +36,11 @@
   and sibling constructors.
   .
   As a generic programming library, @yoko@ extends @instant-generics@ with
-  support for constructor-centric generic programming. The @Examples/LambdaLift/@
-  file distributed with the @yoko@ source demonstrates defining a
-  lambda-lifting conversion between the two types @ULC@, which has lambdas,
-  and @Prog@, which has top-level function declarations instead.
+  support for constructor-centric generic programming. The
+  @Examples\/LambdaLift\/LambdaLift.hs@ file distributed with the @yoko@ source
+  demonstrates defining a lambda-lifting conversion between the two types
+  @ULC@, which has lambdas, and @Prog@, which has top-level function
+  declarations instead.
   .
   @
     data ULC = Lam Type ULC | Var Int | Let [Decl] ULC | App ULC ULC
@@ -59,9 +63,13 @@
   work for any new @ULC@ constructors (e.g. syntax for tuples or mutable
   references) as long as constructors with the same names and analogous fields
   were added to @TLF@ and the semantics of those constructors doesn't involve
-  binding. This default behavior of the lambda-lifter is specified in about ten
-  lines of user code.
+  binding. This default /generic/ behavior of the lambda-lifter is specified in
+  about ten lines of user code.
   .
+  The non-generic code is much more complicated. This is intentional: I wanted
+  to show that sometimes shoehorning an algorithm into the requisite type (/ie/
+  @a -> m a'@) can be difficult and require subtleties like backwards state.
+  .
   Existing generic libraries don't use constructor names to the degree that
   @yoko@ does, and so cannot accomodate generic /conversions/ as well.
 
@@ -85,32 +93,24 @@
 
 
 library
-  build-depends: base >= 4 && < 5,
-                 template-haskell > 2.7 && < 2.8,
-                 containers >= 0.4 && < 0.5,
-                 mtl >= 2.0 && < 2.1
+  build-depends: base >= 4 && < 5, template-haskell, containers, mtl
 
-  build-depends: th-sccs < 0.1, invariant < 0.2
+  build-depends: th-sccs, invariant
 
-  build-depends: type-equality < 0.2
+  build-depends: type-equality, bifunctors
 
-  build-depends:
-    kinds >= 0.0.1.5 && < 0.1,
-    type-functions >= 0.2.0.3 && < 0.3,
-    records >= 0.1.1.6 && < 0.2
+  build-depends: kinds >= 0.0.1.5, type-functions >= 0.2.0.3, records >= 0.1.1.6
 
   build-depends:
-    type-booleans < 0.2,
-    type-spine >= 0.1.1 && < 0.2,
-    tagged-th < 0.2,
-    type-digits < 0.2,
-    type-cereal >= 0.1.1 && < 0.2,
-    type-ord < 0.2,
-    type-ord-spine-cereal < 0.2
+    type-spine >= 0.2, type-digits >= 0.2, type-cereal >= 0.2, type-ord >= 0.2, type-ord-spine-cereal >= 0.2
 
   exposed-modules:
-    Data.Yoko, Data.Yoko.HCompos, Data.Yoko.TH
+    Data.Yoko,
 
+    Data.Yoko.SmartPreciseCase,
+
+    Data.YokoRaw, Data.Yoko.HCompos, Data.Yoko.TH,
+
     Data.Yoko.TypeBasics, Data.Yoko.Each
 
   other-modules:
@@ -118,10 +118,4 @@
     Data.Yoko.MaybeKind,
     Data.Yoko.Representation,
     Data.Yoko.TypeSums,
-    Data.Yoko.TypeSumsAux,
     Data.Yoko.TH.Internal
-
-    -- under development
---    Data.Yoko.Fold,
---    Data.Yoko.Map,
---    Data.Yoko.OnRs