diff --git a/examples/realworld.hs b/examples/realworld.hs
new file mode 100644
--- /dev/null
+++ b/examples/realworld.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, ConstraintKinds, TypeOperators, FlexibleContexts, GeneralizedNewtypeDeriving #-}
+
+import Generics.OneLiner
+
+import Data.Monoid
+import Control.Lens (Traversal')
+import Data.Typeable
+import Control.DeepSeq
+import Test.SmallCheck.Series
+import Control.Monad.Logic.Class
+import Control.Applicative
+import Control.Monad
+import Data.Hashable
+import Data.Functor.Contravariant
+import Data.Functor.Contravariant.Divisible
+import Data.Void
+
+
+-- http://hackage.haskell.org/package/lens-4.3.3/docs/Generics-Deriving-Lens.html
+whenCastableOrElse :: forall a b f. (Typeable a, Typeable b) => (b -> f b) -> (a -> f a) -> a -> f a
+whenCastableOrElse f g = maybe g (\Refl -> f) (eqT :: Maybe (a :~: b))
+
+tinplate :: forall t b. (Typeable b, Deep Typeable t) => Traversal' t b
+tinplate f
+  | isAtom (Proxy :: Proxy t) = f `whenCastableOrElse` pure
+  | otherwise = gtraverse (For :: For (Deep Typeable)) $ f `whenCastableOrElse` tinplate f
+
+
+-- http://hackage.haskell.org/package/deepseq-generics-0.1.1.1/docs/src/Control-DeepSeq-Generics.html
+grnf :: (ADT t, Constraints t NFData) => t -> ()
+grnf = gfoldMap (For :: For NFData) rnf
+
+
+-- http://hackage.haskell.org/package/smallcheck-1.1.1/docs/src/Test-SmallCheck-Series.html
+newtype Fair m a = Fair { runFair :: Series m a } deriving Functor
+instance MonadLogic m => Applicative (Fair m) where
+  pure a = Fair $ pure a
+  Fair fs <*> Fair as = Fair $ fs <~> as
+
+gseries :: forall t m. (ADT t, Constraints t (Serial m), MonadLogic m) => Series m t
+gseries = foldr ((\/) . decDepth . runFair) mzero $ createA (For :: For (Serial m)) (Fair series)
+
+newtype CoSeries m a = CoSeries { runCoSeries :: forall r. Series m r -> Series m (a -> r) }
+instance Contravariant (CoSeries m) where
+  contramap f (CoSeries g) = CoSeries $ fmap (. f) . g
+instance MonadLogic m => Divisible (CoSeries m) where
+  divide f (CoSeries g) (CoSeries h) = CoSeries $ \rs -> do
+    rs' <- fixDepth rs
+    f2 <- decDepthChecked (constM $ constM rs') (g $ h rs')
+    return $ uncurry f2 . f
+  conquer = CoSeries constM
+instance MonadLogic m => Decidable (CoSeries m) where
+  choose f (CoSeries g) (CoSeries h) = CoSeries $ \rs ->
+    (\br cr -> either br cr . f) <$> g rs <~> h rs
+  lose f = CoSeries $ \_ ->
+    return $ absurd . f
+
+gcoseries :: forall t m r. (ADT t, Constraints t (CoSerial m), MonadLogic m)
+          => Series m r -> Series m (t -> r)
+gcoseries = runCoSeries $ createD (For :: For (CoSerial m)) (CoSeries coseries)
+
+
+-- http://hackage.haskell.org/package/hashable-1.2.2.0/docs/src/Data-Hashable-Generic.html
+ghashWithSalt :: (ADT t, Constraints t Hashable) => Int -> t -> Int
+ghashWithSalt = flip $ \t -> flip hashWithSalt (ctorIndex t) .
+  appEndo (gfoldMap (For :: For Hashable) (Endo . flip hashWithSalt) t)
diff --git a/one-liner.cabal b/one-liner.cabal
--- a/one-liner.cabal
+++ b/one-liner.cabal
@@ -1,5 +1,5 @@
 Name:                 one-liner
-Version:              0.3.1
+Version:              0.4
 Synopsis:             Constraint-based generics
 Description:          Write short and concise generic instances of type classes.
                       .
@@ -36,6 +36,7 @@
   Build-depends:
       base         >= 4.5 && < 5
     , transformers >= 0.3 && < 0.5
+    , contravariant >= 1.2 && < 1.3
     , ghc-prim
 
 source-repository head
diff --git a/src/Generics/OneLiner.hs b/src/Generics/OneLiner.hs
--- a/src/Generics/OneLiner.hs
+++ b/src/Generics/OneLiner.hs
@@ -13,13 +13,16 @@
 --
 -----------------------------------------------------------------------------
 {-# LANGUAGE
-    RankNTypes
+    GADTs
+  , RankNTypes
   , TypeFamilies
   , TypeOperators
   , ConstraintKinds
   , FlexibleContexts
   , FlexibleInstances
   , ScopedTypeVariables
+  , UndecidableInstances
+  , MultiParamTypeClasses
   #-}
 module Generics.OneLiner (
   -- * Producing values
@@ -28,10 +31,12 @@
   gmap, gfoldMap, gtraverse,
   -- * Combining values
   gzipWith, mzipWith, zipWithA,
+  -- * Consuming values
+  consume,
   -- * Single constructor functions
   op0, op1, op2,
   -- * Types
-  ADT, ADTRecord, Constraints, For(..)
+  ADT, ADTRecord, Constraints, For(..), Deep, DeepConstraint, isAtom
 ) where
 
 import GHC.Generics
@@ -39,6 +44,9 @@
 import Control.Applicative
 import Data.Functor.Identity
 import Data.Monoid
+import Data.Typeable
+import Data.Functor.Contravariant
+import Data.Functor.Contravariant.Divisible
 
 type family Constraints' (t :: * -> *) (c :: * -> Constraint) :: Constraint
 type instance Constraints' V1 c = ()
@@ -59,12 +67,15 @@
      => for c -> (forall s. c s => s -> f s) -> t x -> f (t x)
   f2 :: (Constraints' t c, Applicative f)
      => for c -> (forall s. c s => s -> s -> f s) -> t x -> t x -> Maybe (f (t x))
+  c0 :: (Constraints' t c, Decidable f)
+     => for c -> (forall s. c s => f s) -> f (t ())
 
 instance ADT' V1 where
   ctorCount _ = 0
   f0 _ _ = []
   f1 _ _ = pure
   f2 _ _ _ = Just . pure
+  c0 _ _ = lose (\v -> v `seq` undefined)
 
 instance (ADT' f, ADT' g) => ADT' (f :+: g) where
   ctorIndex' (L1 l) = ctorIndex' l
@@ -76,21 +87,27 @@
   f2 for f (L1 a) (L1 b) = fmap (fmap L1) (f2 for f a b)
   f2 for f (R1 a) (R1 b) = fmap (fmap R1) (f2 for f a b)
   f2 _ _ _ _ = Nothing
+  c0 for f = choose h (c0 for f) (c0 for f) where
+    h (L1 l) = Left l
+    h (R1 r) = Right r
 
 instance ADT' U1 where
   f0 _ _ = [pure U1]
   f1 _ _ = pure
   f2 _ _ _ = Just . pure
+  c0 _ _ = conquer
 
 instance (ADT' f, ADT' g) => ADT' (f :*: g) where
   f0 for f = [(:*:) <$> head (f0 for f) <*> head (f0 for f)]
   f1 for f (l :*: r) = (:*:) <$> f1 for f l <*> f1 for f r
   f2 for f (al :*: ar) (bl :*: br) = liftA2 (:*:) <$> f2 for f al bl <*> f2 for f ar br
+  c0 for f = divide (\(l :*: r) -> (l, r)) (c0 for f) (c0 for f)
 
 instance ADT' (K1 i v) where
   f0 _ f = [K1 <$> f]
   f1 _ f (K1 v) = K1 <$> f v
   f2 _ f (K1 l) (K1 r) = Just $ K1 <$> f l r
+  c0 _ f = contramap unK1 f
 
 instance ADT' f => ADT' (M1 i t f) where
   ctorIndex' = ctorIndex' . unM1
@@ -98,7 +115,7 @@
   f0 for f = map (fmap M1) (f0 for f)
   f1 for f = fmap M1 . f1 for f . unM1
   f2 for f (M1 l) (M1 r) = fmap (fmap M1) (f2 for f l r)
-
+  c0 for f = contramap unM1 (c0 for f)
 
 class ADTRecord' (f :: * -> *) where
 instance ADTRecord' U1
@@ -126,6 +143,27 @@
 -- Where @Show@ can be any class.
 data For (c :: * -> Constraint) = For
 
+-- | @Deep c@ recursively requires all parts of the datatype to be an instance of `c` and of `Generic`.
+class DeepConstraint c t => Deep (c :: * -> Constraint) t where
+instance DeepConstraint c t => Deep c t
+
+-- http://stackoverflow.com/questions/14133121/can-i-constrain-a-type-family
+-- | A trick to avoid GHC from detecting a cycle.
+type family DeepConstraint (c :: * -> Constraint) t :: Constraint
+type instance DeepConstraint c t = (c t, ADT t, Constraints t (Deep c), Constraints t c)
+
+-- | For primitive values like `Int`, `Float`, `Double` and `Char`, the generic representation
+-- of a value contains itself. If you use generics recursively (f.e. using `Deep`),
+-- use `isAtom` to detect primitive values and prevent an infinite loop.
+isAtom :: forall t proxy. (ADT t, Typeable t, Constraints t Typeable) => proxy t -> Bool
+isAtom pt = case createA (For :: For Typeable) f :: [Const [Bool] t] of
+  [Const [True]] -> True
+  _ -> False
+  where
+    f :: forall a. Typeable a => Const [Bool] a
+    f = Const [tRep == typeRep (undefined :: [a])]
+    tRep = typeRep pt
+
 -- | Create a value (one for each constructor), given how to construct the components.
 --
 -- @
@@ -146,6 +184,12 @@
 createA :: (ADT t, Constraints t c, Applicative f)
         => for c -> (forall s. c s => f s) -> [f t]
 createA for f = map (fmap to) (f0 for f)
+
+-- | Generate ways to consume values of type `t`. This is the contravariant version of `createA`.
+consume :: (ADT t, Constraints t c, Decidable f)
+        => for c -> (forall s. c s => f s) -> f t
+consume for f = contramap from (c0 for f)
+
 
 -- | Get the index in the lists returned by `create` and `createA` of the constructor of the given value.
 --