diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.2.3
+version:             0.2.4
 synopsis:            Poly-kinded, extensible ADTs
 homepage:            https://github.com/fumieval/extensible
 description:         Extensible Products/Unions
@@ -23,6 +23,7 @@
     Data.Extensible
     Data.Extensible.Inclusion
     Data.Extensible.Internal
+    Data.Extensible.Internal.Rig
     Data.Extensible.League
     Data.Extensible.Match
     Data.Extensible.Plain
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE PolyKinds, Rank2Types, ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DataKinds, GADTs #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Inclusion
@@ -12,6 +12,7 @@
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Inclusion (
+  -- * Membership
     Position
   , runPosition
   , (∈)()
@@ -20,17 +21,27 @@
   , Missing
   , Ambiguous
   , ord
+  -- * Inclusion
   , (⊆)()
   , Include
   , inclusion
   , shrink
   , spread
+  -- * Inverse
+  , coinclusion
+  , wrench
+  , retrench
+  , Nullable(..)
+  , nullable
+  , mapNullable
   ) where
 
 import Data.Extensible.Product
 import Data.Extensible.Sum
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
 import Data.Proxy
+import Data.Monoid
 
 -- | Unicode alias for 'Include'
 type xs ⊆ ys = Include ys xs
@@ -52,3 +63,17 @@
 spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
 {-# INLINE spread #-}
 
+-- | The inverse of 'inclusion'.
+coinclusion :: (Include ys xs, Generate ys) => Nullable (Position xs) :* ys
+coinclusion = flip appEndo (generate (const Null))
+  $ hfoldMap getConst'
+  $ htabulate (\src dst -> Const' $ Endo $ sectorAt dst `over` const (Eine src))
+  $ inclusion
+
+-- | Extend a product and fill missing fields by 'Null'.
+wrench :: (Generate ys, xs ⊆ ys) => h :* xs -> Nullable h :* ys
+wrench xs = hmap (mapNullable $ \pos -> view (sectorAt pos) xs) coinclusion
+
+-- | Narrow the range of the sum, if possible.
+retrench :: (Generate ys, xs ⊆ ys) => h :| ys -> Nullable ((:|) h) xs
+retrench (UnionAt pos h) = flip UnionAt h `mapNullable` view (sectorAt pos) coinclusion
diff --git a/src/Data/Extensible/Internal.hs b/src/Data/Extensible/Internal.hs
--- a/src/Data/Extensible/Internal.hs
+++ b/src/Data/Extensible/Internal.hs
@@ -119,8 +119,8 @@
 
 type family Half (xs :: [k]) :: [k] where
   Half '[] = '[]
-  Half (x ': y ': zs) = x ': zs
-  Half (x ': '[]) = x ': '[]
+  Half (x ': y ': zs) = x ': Half zs
+  Half (x ': '[]) = '[x]
 
 type family Tail (xs :: [k]) :: [k] where
   Tail (x ': xs) = xs
@@ -137,7 +137,7 @@
 {-# INLINE retagSD #-}
 
 class ToInt n where
-  theInt :: Proxy n -> Int
+  theInt :: proxy n -> Int
 
 instance ToInt Zero where
   theInt _ = 0
@@ -165,8 +165,8 @@
   MapSucc '[] = '[]
   MapSucc (x ': xs) = Succ x ': MapSucc xs
 
--- GHC can't prove this
-lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))
+-- | GHC can't prove this
+lemmaHalfTail :: proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))
 lemmaHalfTail _ = unsafeCoerce
 {-# INLINE lemmaHalfTail #-}
 
diff --git a/src/Data/Extensible/Internal/Rig.hs b/src/Data/Extensible/Internal/Rig.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Internal/Rig.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE PolyKinds, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, FlexibleInstances, DeriveFunctor #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable#-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Rig
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Miscellaneous utilities
+------------------------------------------------------------------------
+module Data.Extensible.Internal.Rig where
+import Unsafe.Coerce
+import Control.Applicative
+import Data.Typeable
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+
+-- | @'view' :: Lens' s a -> (a -> a) -> (s -> s)@
+view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
+view l = views l id
+{-# INLINE view #-}
+
+-- | @'views' :: Lens' s a -> (a -> r) -> (s -> r)@
+views :: ((a -> Const r a) -> (s -> Const r s)) -> (a -> r) -> s -> r
+views = unsafeCoerce
+{-# INLINE views #-}
+
+-- | Just a value.
+newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable, Functor, Foldable, Traversable)
+
+instance Applicative K0 where
+  pure = K0
+  K0 f <*> K0 a = K0 (f a)
+
+instance Monad K0 where
+  return = K0
+  K0 a >>= k = k a
+
+instance Show a => Show (K0 a) where
+  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a
+
+-- | @'over' :: Lens' s a -> (a -> a) -> (s -> s)@
+over :: ((a -> K0 a) -> s -> K0 s) -> (a -> a) -> s -> s
+over = unsafeCoerce
+{-# INLINE over #-}
+
+-- | Poly-kinded Const
+newtype Const' a x = Const' { getConst' :: a } deriving Show
+
+-- | Poly-kinded Maybe
+data Nullable h x = Null | Eine (h x) deriving (Show, Eq, Ord, Typeable)
+
+-- | Destruct 'Nullable'.
+nullable :: r -> (h x -> r) -> Nullable h x -> r
+nullable r _ Null = r
+nullable _ f (Eine h) = f h
+{-# INLINE nullable #-}
+
+-- | Apply a function to its content.
+mapNullable :: (g x -> h y) -> Nullable g x -> Nullable h y
+mapNullable f (Eine g) = Eine (f g)
+mapNullable _ Null = Null
+{-# INLINE mapNullable #-}
+
+-- | Composition for a class and a wrapper
+class c (h x) => ClassComp c h x
+instance c (h x) => ClassComp c h x
diff --git a/src/Data/Extensible/Plain.hs b/src/Data/Extensible/Plain.hs
--- a/src/Data/Extensible/Plain.hs
+++ b/src/Data/Extensible/Plain.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# LANGUAGE DataKinds #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Plain
@@ -25,27 +25,12 @@
   , (<?!)
   )where
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
 import Data.Extensible.Product
 import Data.Extensible.Sum
 import Data.Extensible.Match
 import Data.Typeable
 import Unsafe.Coerce
-import Data.Foldable (Foldable)
-import Data.Traversable (Traversable)
-import Control.Applicative
--- | Just a value.
-newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable, Functor, Foldable, Traversable)
-
-instance Applicative K0 where
-  pure = K0
-  K0 f <*> K0 a = K0 (f a)
-
-instance Monad K0 where
-  return = K0
-  K0 a >>= k = k a
-
-instance Show a => Show (K0 a) where
-  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a
 
 -- | Alias for plain products
 type AllOf xs = K0 :* xs
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
--- a/src/Data/Extensible/Product.hs
+++ b/src/Data/Extensible/Product.hs
@@ -27,14 +27,15 @@
   , hzipWith3
   , hfoldMap
   , htraverse
+  , htabulate
   , hlookup
   , sector
   , sectorAt
   , Generate(..)
-  , Forall(..)
-  , ClassComp) where
+  , Forall(..)) where
 
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
 import Unsafe.Coerce
 import Data.Typeable
 import Control.Applicative
@@ -44,8 +45,8 @@
 data (h :: k -> *) :* (s :: [k]) where
   Nil :: h :* '[]
   Tree :: !(h x)
-    -> h :* Half xs
-    -> h :* Half (Tail xs)
+    -> !(h :* Half xs)
+    -> !(h :* Half (Tail xs))
     -> h :* (x ': xs)
 
 deriving instance Typeable (:*)
@@ -117,9 +118,12 @@
 hlookup = view . sectorAt
 {-# INLINE hlookup #-}
 
--- | Composition for a class and a wrapper
-class c (h x) => ClassComp c h x
-instance c (h x) => ClassComp c h x
+-- | 'hmap' with its indices.
+htabulate :: forall g h xs. (forall x. Position xs x -> g x -> h x) -> g :* xs -> h :* xs
+htabulate f = go id where
+  go :: (forall x. Position t x -> Position xs x) -> g :* t -> h :* t
+  go k (Tree g a b) = Tree (f (k here) g) (go (k . navL) a) (go (k . navR) b)
+  go _ Nil = Nil
 
 instance Forall (ClassComp Eq h) xs => Eq (h :* xs) where
   (==) = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapEq (view (sectorAt pos) dic))
@@ -135,8 +139,6 @@
       aggr = hfoldMap getConst'
       c = Proxy :: Proxy (ClassComp Ord h)
 
-newtype Const' a x = Const' { getConst' :: a } deriving Show
-
 newtype WrapEq h x = WrapEq { unwrapEq :: h x -> h x -> Bool }
 
 newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }
@@ -146,10 +148,6 @@
 sector = sectorAt membership
 {-# INLINE sector #-}
 
-view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
-view l = unsafeCoerce (l Const)
-{-# INLINE view #-}
-
 -- | /O(log n)/ A lens for a value in a known position.
 sectorAt :: forall h x xs f. (Functor f) => Position xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
 sectorAt pos0 f = go pos0 where
@@ -169,18 +167,16 @@
   generate _ = Nil
   {-# INLINE generate #-}
 
-instance (Generate xs) => Generate (x ': xs) where
-  generate f = f here <:* generate (f . navNext)
-  {-# INLINE generate #-}
+instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
+  generate f = Tree (f here) (generate (f . navL)) (generate (f . navR))
 
 -- | Guarantees the all elements satisfies the predicate.
 class Forall c (xs :: [k]) where
-  generateFor :: Proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs
+  generateFor :: proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs
 
 instance Forall c '[] where
   generateFor _ _ = Nil
   {-# INLINE generateFor #-}
 
-instance (c x, Forall c xs) => Forall c (x ': xs) where
-  generateFor proxy f = f here <:* generateFor proxy (f . navNext)
-  {-# INLINE generateFor #-}
+instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
+  generateFor proxy f = Tree (f here) (generateFor proxy (f . navL)) (generateFor proxy (f . navR))
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
--- a/src/Data/Extensible/Record.hs
+++ b/src/Data/Extensible/Record.hs
@@ -51,7 +51,7 @@
 -- | @FieldLens s@ is a type of lens that points a field named @s@.
 --
 -- @
--- 'FieldLens' s = (s '∈' xs) => Lens' ('Record' xs) ('FieldValue' s)
+-- 'FieldLens' s = (s ∈ xs) => Lens' ('Record' xs) ('FieldValue' s)
 -- @
 --
 type FieldLens s = forall f p xs. (Functor f, Labelable s p, s ∈ xs)
@@ -101,9 +101,10 @@
   let lbl = conE 'Proxy `sigE` (conT ''Proxy `appT` st)
   let wf = varE '(.) `appE` (varE 'fmap `appE` fcon)
         `appE` (varE '(.) `appE` (varE 'unlabel `appE` lbl `appE` varE f) `appE` varE 'getField)
-  sequence $ [tySynInstD ''FieldValue (tySynEqn [litT (strTyLit s)] t)
+  sequence [tySynInstD ''FieldValue (tySynEqn [litT (strTyLit s)] t)
     , sigD (mkName s)
       $ forallT [] (return [])
       $ conT ''FieldLens `appT` st
     , funD (mkName s) [clause [varP f] (normalB $ varE 'sector `appE` wf) []]
+    , return $ PragmaD $ InlineP (mkName s) Inline FunLike AllPhases
     ]
diff --git a/src/Data/Extensible/Sum.hs b/src/Data/Extensible/Sum.hs
--- a/src/Data/Extensible/Sum.hs
+++ b/src/Data/Extensible/Sum.hs
@@ -47,7 +47,7 @@
   show = exhaust
 
 instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where
-  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec 11 h)
+  showsPrec d = (\h -> showParen (d > 10) $ showString "embed " . showsPrec 11 h)
     <:| showsPrec d
 
 -- | /O(1)/ Naive pattern match