diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.2.2
+version:             0.2.3
 synopsis:            Poly-kinded, extensible ADTs
 homepage:            https://github.com/fumieval/extensible
 description:         Extensible Products/Unions
@@ -29,6 +29,7 @@
     Data.Extensible.Product
     Data.Extensible.Sum
     Data.Extensible.Union
+    Data.Extensible.Record
   default-extensions: TypeOperators, DeriveDataTypeable
   build-depends:       base >= 4.7 && <5, template-haskell
   hs-source-dirs:      src
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -9,7 +9,7 @@
 -- Portability :  non-portable
 --
 -- This package defines an extensible type-indexed product type and a union type.
--- Both are determined from the type-level list @[k]@
+-- Extensible ADTs provided by this module are determined from a type-level list @[k]@
 -- and a wrapper @k -> *@.
 -- We can define ADTs not only for plain values, but also parameterized ones.
 --
@@ -28,18 +28,12 @@
   , module Data.Extensible.Plain
   , module Data.Extensible.Product
   , module Data.Extensible.Sum
-  -- * Lookup
-  , Position
-  , runPosition
-  , (∈)()
-  , Member(..)
-  , ord
   ) where
-import Data.Extensible.Internal
 import Data.Extensible.Inclusion
 import Data.Extensible.Match
 import Data.Extensible.Plain
 import Data.Extensible.Product
 import Data.Extensible.Sum
+
 -------------------------------------------------------------
 
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,4 +1,5 @@
-{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}
+{-# LANGUAGE PolyKinds, Rank2Types, ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Inclusion
@@ -10,7 +11,21 @@
 -- Portability :  non-portable
 --
 ------------------------------------------------------------------------
-module Data.Extensible.Inclusion where
+module Data.Extensible.Inclusion (
+    Position
+  , runPosition
+  , (∈)()
+  , Member(..)
+  , Expecting
+  , Missing
+  , Ambiguous
+  , ord
+  , (⊆)()
+  , Include
+  , inclusion
+  , shrink
+  , spread
+  ) where
 
 import Data.Extensible.Product
 import Data.Extensible.Sum
@@ -36,3 +51,4 @@
 spread :: (xs ⊆ ys) => h :| xs -> h :| ys
 spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
 {-# INLINE spread #-}
+
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
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, PolyKinds #-}
 {-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}
-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Data.Extensible.Internal (Position
   , runPosition
@@ -10,17 +10,27 @@
   , Nav(..)
   , navigate
   , here
+  , navNext
   , navL
   , navR
   , Member(..)
   , (∈)()
   , Nat(..)
-  , Record(..)
+  , ToInt(..)
   , Lookup
   , Succ
+  , MapSucc
   , Half
   , Tail
-  , lemmaHalfTail) where
+  , lemmaHalfTail
+  , (++)()
+  , Map
+  , Merge
+  , Check
+  , Expecting
+  , Missing
+  , Ambiguous
+  ) where
 import Data.Type.Equality
 import Data.Proxy
 import Control.Applicative
@@ -29,6 +39,7 @@
 import Data.Typeable
 import Language.Haskell.TH
 
+-- | Generates 'Position' for an ordinal (0-origin).
 ord :: Int -> Q Exp
 ord n = do
   let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
@@ -56,7 +67,7 @@
 
 navigate :: Position xs x -> Nav xs x
 navigate (Position 0) = unsafeCoerce Here
-navigate (Position n) = let (m, r) = divMod n 2 in case r of
+navigate (Position n) = let (m, r) = divMod (n - 1) 2 in case r of
   0 -> unsafeCoerce $ NavL $ Position m
   _ -> unsafeCoerce $ NavR $ Position m
 
@@ -69,12 +80,16 @@
 here = Position 0
 {-# INLINE here #-}
 
+navNext :: Position xs y -> Position (x ': xs) y
+navNext (Position n) = Position (n + 1)
+{-# INLINE navNext #-}
+
 navL :: Position (Half xs) y -> Position (x ': xs) y
 navL (Position x) = Position (x * 2 + 1)
 {-# INLINE navL #-}
 
 navR :: Position (Half (Tail xs)) y -> Position (x ': xs) y
-navR (Position x) = Position ((x + 1) * 2)
+navR (Position x) = Position (x * 2 + 2)
 {-# INLINE navR #-}
 
 -- | Unicode flipped alias for 'Member'
@@ -84,8 +99,22 @@
 class Member (xs :: [k]) (x :: k) where
   membership :: Position xs x
 
-instance Record (Lookup x xs) => Member xs x where
-  membership = Position $ theInt (Proxy :: Proxy (Lookup x xs))
+-- | A type sugar to make type error more readable.
+data Expecting a
+
+-- | A type sugar to make type error more readable.
+data Missing a
+
+-- | A type sugar to make type error more readable.
+data Ambiguous a
+
+type family Check x xs where
+  Check x '[n] = Expecting n
+  Check x '[] = Missing x
+  Check x xs = Ambiguous x
+
+instance (Check x (Lookup x xs) ~ Expecting one, ToInt one) => Member xs x where
+  membership = Position $ theInt (Proxy :: Proxy one)
   {-# INLINE membership #-}
 
 type family Half (xs :: [k]) :: [k] where
@@ -97,7 +126,7 @@
   Tail (x ': xs) = xs
   Tail '[] = '[]
 
-data Nat = Zero | DNat Nat | SDNat Nat | NotFound
+data Nat = Zero | DNat Nat | SDNat Nat
 
 retagD :: (Proxy n -> a) -> proxy (DNat n) -> a
 retagD f _ = f Proxy
@@ -107,33 +136,49 @@
 retagSD f _ = f Proxy
 {-# INLINE retagSD #-}
 
-class Record n where
+class ToInt n where
   theInt :: Proxy n -> Int
 
-instance Record Zero where
+instance ToInt Zero where
   theInt _ = 0
   {-# INLINE theInt #-}
 
-instance Record n => Record (DNat n) where
+instance ToInt n => ToInt (DNat n) where
   theInt = (*2) <$> retagD theInt
   {-# INLINE theInt #-}
 
-instance Record n => Record (SDNat n) where
+instance ToInt n => ToInt (SDNat n) where
   theInt = (+1) <$> (*2) <$> retagSD theInt
   {-# INLINE theInt #-}
 
-type family Lookup (x :: k) (xs :: [k]) :: Nat where
-  Lookup x (x ': xs) = Zero
-  Lookup x (y ': ys) = Succ (Lookup x ys)
-  Lookup x '[] = NotFound
+type family Lookup (x :: k) (xs :: [k]) :: [Nat] where
+  Lookup x (x ': xs) = Zero ': Lookup x xs
+  Lookup x (y ': ys) = MapSucc (Lookup x ys)
+  Lookup x '[] = '[]
 
 type family Succ (x :: Nat) :: Nat where
   Succ Zero = SDNat Zero
   Succ (DNat n) = SDNat n
   Succ (SDNat n) = DNat (Succ n)
-  Succ NotFound = NotFound
 
+type family MapSucc (xs :: [Nat]) :: [Nat] where
+  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))
 lemmaHalfTail _ = unsafeCoerce
 {-# INLINE lemmaHalfTail #-}
+
+type family Map (f :: k -> k) (xs :: [k]) :: [k] where
+  Map f '[] = '[]
+  Map f (x ': xs) = f x ': Map f xs
+
+type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
+  '[] ++ ys = ys
+  (x ': xs) ++ ys = x ': xs ++ ys
+
+type family Merge (xs :: [k]) (ys :: [k]) :: [k] where
+  Merge (x ': xs) (y ': ys) = x ': y ': Merge xs ys
+  Merge xs '[] = xs
+  Merge '[] ys = ys
diff --git a/src/Data/Extensible/Match.hs b/src/Data/Extensible/Match.hs
--- a/src/Data/Extensible/Match.hs
+++ b/src/Data/Extensible/Match.hs
@@ -13,16 +13,22 @@
 ------------------------------------------------------------------------
 module Data.Extensible.Match (
   Match(..)
+  , clause
   , match
   , mapMatch
   , caseOf) where
 
+import Data.Extensible.Internal
 import Data.Extensible.Product
 import Data.Extensible.Sum
 import Data.Typeable
 
 -- | Turn a wrapper type into one clause that returns @a@.
 newtype Match h a x = Match { runMatch :: h x -> a } deriving Typeable
+
+-- | A lens for a specific clause.
+clause :: (x ∈ xs, Functor f) => ((h x -> a) -> f (h x -> a)) -> Match h a :* xs -> f (Match h a :* xs)
+clause f = sector (fmap Match . f . runMatch)
 
 -- | Applies a function to the result of 'Match'.
 mapMatch :: (a -> b) -> Match h a x -> Match h b 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
@@ -47,7 +47,10 @@
 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
+
+-- | Alias for plain sums
 type OneOf xs = K0 :| xs
 
 -- | /O(log n)/ Add a plain value to a product.
@@ -69,6 +72,7 @@
 -- | Naive pattern matching for a plain value.
 (<%|) :: (x -> r) -> (OneOf xs -> r) -> OneOf (x ': xs) -> r
 (<%|) = unsafeCoerce (<:|)
+infixr 1 <%|
 
 -- | /O(log n)/ A lens for a plain value in a product.
 record :: (x ∈ xs, Functor f) => (x -> f x) -> (AllOf xs -> f (AllOf 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
@@ -18,6 +18,7 @@
   -- * Product
   (:*)(..)
   , (<:*)
+  , (*++*)
   , hhead
   , htail
   , huncons
@@ -42,7 +43,7 @@
 -- | The extensible product type
 data (h :: k -> *) :* (s :: [k]) where
   Nil :: h :* '[]
-  Tree :: h x
+  Tree :: !(h x)
     -> h :* Half xs
     -> h :* Half (Tail xs)
     -> h :* (x ': xs)
@@ -53,10 +54,10 @@
   show Nil = "Nil"
 
 instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where
-  showsPrec d t = let (x, xs) = huncons t in showParen (d > 10) $
-     showsPrec 6 x
+  showsPrec d t = let (x, xs) = huncons t in showParen (d > 0) $
+     showsPrec 0 x
     . showString " <:* "
-    . showsPrec 6 xs
+    . showsPrec 0 xs
 
 -- | /O(1)/ Extract the head element.
 hhead :: h :* (x ': xs) -> h x
@@ -65,7 +66,7 @@
 -- | /O(n)/ Extract the tail of the product.
 htail :: h :* (x ': xs) -> h :* xs
 htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
-htail (Tree _ Nil _) = unsafeCoerce Nil
+htail _ = unsafeCoerce Nil
 
 -- | Split a product to the head and the tail.
 huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
@@ -75,13 +76,19 @@
 (<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
 a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $! b <:* d) c
 a <:* Nil = Tree a Nil Nil
-infixr 5 <:*
+infixr 0 <:*
 
--- | Transform every elements in a union, preserving the order.
+-- | Transform every elements in a product, preserving the order.
 hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
 hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
 hmap _ Nil = Nil
 
+-- | Serial combination of two products.
+(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
+(*++*) Nil ys = ys
+(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
+infixr 0 *++*
+
 -- | 'zipWith' for heterogeneous product
 hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
 hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
@@ -160,9 +167,11 @@
 
 instance Generate '[] where
   generate _ = Nil
+  {-# 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)) where
+instance (Generate xs) => Generate (x ': xs) where
+  generate f = f here <:* generate (f . navNext)
+  {-# INLINE generate #-}
 
 -- | Guarantees the all elements satisfies the predicate.
 class Forall c (xs :: [k]) where
@@ -170,6 +179,8 @@
 
 instance Forall c '[] where
   generateFor _ _ = Nil
+  {-# 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)) where
+instance (c x, Forall c xs) => Forall c (x ': xs) where
+  generateFor proxy f = f here <:* generateFor proxy (f . navNext)
+  {-# INLINE generateFor #-}
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Record.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE TemplateHaskell, PolyKinds, TypeFamilies, DataKinds, KindSignatures, FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances, Rank2Types #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Record
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Flexible records with well-typed fields.
+-- Example: <https://github.com/fumieval/extensible/blob/master/examples/records.hs>
+------------------------------------------------------------------------
+module Data.Extensible.Record (
+   module Data.Extensible.Inclusion
+  , Record
+  , (<:*)
+  , (:*)(Nil)
+  , (@=)
+  , mkField
+  , Field(..)
+  , FieldValue
+  , FieldLens
+  , FieldName
+  -- * Internal
+  , Labelable(..)
+  , LabelPhantom
+  ) where
+import Data.Extensible.Product
+import Data.Extensible.Internal
+import Language.Haskell.TH
+import GHC.TypeLits hiding (Nat)
+import Data.Extensible.Inclusion
+import Data.Proxy
+
+-- | Associates names with concrete types.
+type family FieldValue (s :: Symbol) :: *
+
+-- | The type of fields.
+data Field (s :: Symbol) = Field { getField :: FieldValue s }
+
+-- | The type of records which contain several fields
+type Record = (:*) Field
+
+instance (KnownSymbol s, Show (FieldValue s)) => Show (Field s) where
+  showsPrec d f@(Field a) = showParen (d >= 1) $ showString (symbolVal f)
+    . showString " @= "
+    . showsPrec 1 a
+
+-- | @FieldLens s@ is a type of lens that points a field named @s@.
+--
+-- @
+-- 'FieldLens' s = (s '∈' xs) => Lens' ('Record' xs) ('FieldValue' s)
+-- @
+--
+type FieldLens s = forall f p xs. (Functor f, Labelable s p, s ∈ xs)
+  => p (FieldValue s) (f (FieldValue s)) -> Record xs -> f (Record xs)
+
+-- | When you see this type as an argument, it expects a 'FieldLens'.
+-- This type hooks the name of 'FieldLens' so that an expression @field \@= value@ has no ambiguousity.
+type FieldName s = LabelPhantom s (FieldValue s) (Proxy (FieldValue s))
+  -> Record '[s] -> Proxy (Record '[s])
+
+-- | A ghostly type used to reify field names
+data LabelPhantom s a b
+
+-- | An internal class to characterize 'FieldLens'
+class Labelable s p where
+  unlabel :: proxy s -> p a b -> a -> b
+
+instance Labelable s (->) where
+  unlabel _ = id
+  {-# INLINE unlabel #-}
+
+instance (s ~ t) => Labelable s (LabelPhantom t) where
+  unlabel _ = error "Impossible"
+
+-- | Annotate a value by the field name.
+(@=) :: FieldName s -> FieldValue s -> Field s
+(@=) _ = Field
+{-# INLINE (@=) #-}
+infix 1 @=
+
+-- | Generate a field.
+-- @'mkField' "foo" [t|Int|]@ defines:
+--
+-- @
+-- type instance FieldValue "foo" = Int
+--
+-- foo :: FieldLens "foo"
+-- @
+--
+-- The yielding field is a <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Lens Lens>.
+mkField :: String -> TypeQ -> DecsQ
+mkField s t = do
+  f <- newName "f"
+  let st = litT (strTyLit s)
+  let vt = conT ''FieldValue `appT` st
+  let fcon = sigE (conE 'Field) $ arrowT `appT` vt `appT` (conT ''Field `appT` st)
+  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)
+    , sigD (mkName s)
+      $ forallT [] (return [])
+      $ conT ''FieldLens `appT` st
+    , funD (mkName s) [clause [varP f] (normalB $ varE 'sector `appE` wf) []]
+    ]
diff --git a/src/Data/Extensible/Union.hs b/src/Data/Extensible/Union.hs
--- a/src/Data/Extensible/Union.hs
+++ b/src/Data/Extensible/Union.hs
@@ -24,8 +24,8 @@
 import Data.Extensible.Product
 import Data.Extensible.Match
 
--- | A much more efficient representation for 'Union' of 'Functor's.
-newtype Union fs a = Union { getLeague :: Flux a :| fs } deriving Typeable
+-- | A union of @* -> *@ types.
+newtype Union fs a = Union { getUnion :: Flux a :| fs } deriving Typeable
 
 -- | fast fmap
 instance Functor (Union fs) where