diff --git a/.travis.yml b/.travis.yml
new file mode 100644
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,10 @@
+language: haskell
+
+env:
+  - GHCVER=7.8.3
+
+before_install:
+  - sudo add-apt-repository -y ppa:hvr/ghc
+  - sudo apt-get update
+  - sudo apt-get install -y -qq cabal-install-1.20 ghc-$GHCVER
+  - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/1.20/bin:$PATH
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,12 @@
+extensible
+======================
+
+[![Build Status](https://travis-ci.org/fumieval/extensible.svg?branch=master)](https://travis-ci.org/fumieval/extensible)
+
+This package provides extensible poly-kinded data types, including records and polymorphic open unions.
+
+While most rival packages takes O(n) for looking up, this package provides O(log n) access.
+
+Extensible products can be applied to first-class pattern matching. It is potentially faster than the ordinary pattern matching, since accessing to an element is O(log n).
+
+Bug reports and contributions are welcome.
diff --git a/examples/records.hs b/examples/records.hs
new file mode 100644
--- /dev/null
+++ b/examples/records.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TemplateHaskell, DataKinds, TypeOperators, KindSignatures, TypeFamilies, FlexibleContexts #-}
+import Data.Extensible.Record
+import Data.Extensible
+import Control.Lens
+
+mkField "name" [t|String|]
+mkField "weight" [t|Float|]
+mkField "price" [t|Int|]
+mkField "description" [t|String|]
+mkField "featured" [t|Bool|]
+mkField "quantity" [t|Int|]
+
+type Stock = Record '["name", "weight", "price", "featured", "description", "quantity"]
+
+s0 :: Stock
+s0 = Field "DA-192H"
+  <: Field 260
+  <: Field 120
+  <: Field True
+  <: Field "High-quality (24bit 192kHz), lightweight portable DAC"
+  <: Field 20
+  <: Nil
+
+-- Use shrink to permute elements
+s1 :: Stock
+s1 = shrink
+   $ name @= "HHP-150"
+  <: featured @= False
+  <: description @= "Premium wooden headphone"
+  <: weight @= 150
+  <: price @= 330
+  <: quantity @= 55
+  <: Nil
+
+-- If "quantity" is missing,
+--    Couldn't match type ‘Missing "quantity"’ with ‘Expecting one’
+--
+-- If there are duplicate "quantity",
+--    Couldn't match type ‘Ambiguous "quantity"’ with ‘Expecting one’
+
+printSummary :: ("name" ∈ s, "description" ∈ s) => Record s -> IO ()
+printSummary s = putStrLn $ view name s ++ ": " ++ view description s
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,17 +1,23 @@
 name:                extensible
-version:             0.2.4
-synopsis:            Poly-kinded, extensible ADTs
+version:             0.2.5
+synopsis:            Extensible, efficient, lens-friendly data types
 homepage:            https://github.com/fumieval/extensible
-description:         Extensible Products/Unions
+bug-reports:         http://github.com/fumieval/extensible/issues
+description:         Combinators and types for extensible product and sum
 license:             BSD3
 license-file:        LICENSE
 author:              Fumiaki Kinoshita
 maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
 copyright:           Copyright (C) 2015 Fumiaki Kinoshita
-category:            Data
+category:            Data, Records
 build-type:          Simple
+stability:           provisional
+
 extra-source-files:
+  examples/*.hs
   .gitignore
+  .travis.yml
+  README.md
 cabal-version:       >=1.10
 
 source-repository head
@@ -24,6 +30,8 @@
     Data.Extensible.Inclusion
     Data.Extensible.Internal
     Data.Extensible.Internal.Rig
+    Data.Extensible.Internal.HList
+    Data.Extensible.Dictionary
     Data.Extensible.League
     Data.Extensible.Match
     Data.Extensible.Plain
@@ -31,7 +39,16 @@
     Data.Extensible.Sum
     Data.Extensible.Union
     Data.Extensible.Record
-  default-extensions: TypeOperators, DeriveDataTypeable
+  default-extensions: TypeOperators
+    , DeriveDataTypeable
+    , KindSignatures
+    , ConstraintKinds
+    , DataKinds
+    , GADTs
+    , Rank2Types
+    , FlexibleContexts
+    , FlexibleInstances
+    , PolyKinds
   build-depends:       base >= 4.7 && <5, template-haskell
   hs-source-dirs:      src
   ghc-options: -Wall
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -24,16 +24,23 @@
 module Data.Extensible (
   -- * Reexport
   module Data.Extensible.Inclusion
+  , module Data.Extensible.League
   , module Data.Extensible.Match
   , module Data.Extensible.Plain
   , module Data.Extensible.Product
+  , module Data.Extensible.Record
   , module Data.Extensible.Sum
+  , module Data.Extensible.Union
   ) where
 import Data.Extensible.Inclusion
 import Data.Extensible.Match
 import Data.Extensible.Plain
 import Data.Extensible.Product
 import Data.Extensible.Sum
+import Data.Extensible.League
+import Data.Extensible.Union
+import Data.Extensible.Record
+import Data.Extensible.Dictionary ()
 
 -------------------------------------------------------------
 
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Dictionary.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-----------------------------------------------------------------------
+--
+-- Module      :  Data.Extensible.Dictionary
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Reifying some classes to make instances for (':*') and (':|')
+-----------------------------------------------------------------------
+module Data.Extensible.Dictionary where
+import Data.Monoid
+import Data.Extensible.Product
+import Data.Extensible.Sum
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+
+type DictOf c g h = forall xs. WrapForall c g xs => h :* xs
+
+dictShow :: forall h. DictOf Show h (Match h (Int -> ShowS))
+dictShow = generateFor (Proxy :: Proxy (Instance1 Show h)) $ const $ Match (flip showsPrec)
+
+dictEq :: forall h. DictOf Eq h (Wrap2 h Bool)
+dictEq = generateFor (Proxy :: Proxy (Instance1 Eq h)) $ const $ Wrap2 (==)
+
+dictOrd :: forall h. DictOf Ord h (Wrap2 h Ordering)
+dictOrd = generateFor (Proxy :: Proxy (Instance1 Ord h)) $ const $ Wrap2 compare
+
+data WrapMonoid h x = WrapMonoid { unwrapEmpty :: h x, unwrapAppend :: h x -> h x -> h x }
+
+dictMonoid :: forall h. DictOf Monoid h (WrapMonoid h)
+dictMonoid = generateFor (Proxy :: Proxy (Instance1 Monoid h)) $ const $ WrapMonoid mempty mappend
+
+instance WrapForall Show h xs => Show (h :* xs) where
+  showsPrec d = showParen (d > 0)
+    . (.showString "Nil")
+    . foldr (.) id
+    . getMerged
+    . hfoldMap getConst'
+    . hzipWith (\(Match f) h -> Const' $ MergeList [f h 0 . showString " <:* "]) dictShow
+
+instance WrapForall Eq h xs => Eq (h :* xs) where
+  xs == ys = getAll $ hfoldMap (All . getConst')
+    $ hzipWith3 (\(Wrap2 f) x y -> Const' (f x y)) dictEq xs ys
+  {-# INLINE (==) #-}
+
+instance (Eq (h :* xs), WrapForall Ord h xs) => Ord (h :* xs) where
+  compare xs ys = hfoldMap getConst'
+    $ hzipWith3 (\(Wrap2 f) x y -> Const' (f x y)) dictOrd xs ys
+  {-# INLINE compare #-}
+
+instance WrapForall Monoid h xs => Monoid (h :* xs) where
+  mempty = hmap unwrapEmpty dictMonoid
+  {-# INLINE mempty #-}
+  mappend xs ys = hzipWith3 unwrapAppend dictMonoid xs ys
+  {-# INLINE mappend #-}
+
+instance WrapForall Show h xs => Show (h :| xs) where
+  showsPrec d (UnionAt pos h) = showParen (d > 10) $ showString "embed "
+    . runMatch (hlookup pos dictShow) h 11
+
+instance WrapForall Eq h xs => Eq (h :| xs) where
+  UnionAt p g == UnionAt q h = case comparePosition p q of
+    Left _ -> False
+    Right Refl -> unwrap2 (hlookup p dictEq) g h
+  {-# INLINE (==) #-}
+
+instance (Eq (h :| xs), WrapForall Ord h xs) => Ord (h :| xs) where
+  UnionAt p g `compare` UnionAt q h = case comparePosition p q of
+    Left x -> x
+    Right Refl -> unwrap2 (hlookup p dictOrd) g h
+  {-# INLINE compare #-}
+
+type WrapForall c h = Forall (Instance1 c h)
+
+-- | Composition for a class and a wrapper
+class c (h x) => Instance1 c h x
+instance c (h x) => Instance1 c h x
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,4 @@
-{-# LANGUAGE PolyKinds, Rank2Types, ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}
-{-# LANGUAGE DataKinds, GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Inclusion
@@ -26,6 +25,7 @@
   , Include
   , inclusion
   , shrink
+  , subset
   , spread
   -- * Inverse
   , coinclusion
@@ -40,7 +40,6 @@
 import Data.Extensible.Sum
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
-import Data.Proxy
 import Data.Monoid
 
 -- | Unicode alias for 'Include'
@@ -58,6 +57,12 @@
 shrink h = hmap (\pos -> hlookup pos h) inclusion
 {-# INLINE shrink #-}
 
+subset :: (xs ⊆ ys, Functor f) => (h :* xs -> f (h :* xs)) -> h :* ys -> f (h :* ys)
+subset f ys = fmap (write ys) $ f (shrink ys) where
+  write y xs = flip appEndo y
+    $ hfoldMap getConst'
+    $ hzipWith (\dst src -> Const' $ Endo $ sectorAt dst `over` const src) inclusion xs
+
 -- | /O(log n)/ Embed to a larger union.
 spread :: (xs ⊆ ys) => h :| xs -> h :| ys
 spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
@@ -72,8 +77,8 @@
 
 -- | 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
+wrench xs = mapNullable (flip hlookup xs) `hmap` 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
+retrench (UnionAt pos h) = flip UnionAt h `mapNullable` hlookup 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
@@ -1,8 +1,19 @@
-{-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, PolyKinds #-}
-{-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
 {-# LANGUAGE TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Inclusion
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- A bunch of combinators that contains magic
+------------------------------------------------------------------------
 module Data.Extensible.Internal (Position
   , runPosition
   , comparePosition
@@ -23,13 +34,17 @@
   , Half
   , Tail
   , lemmaHalfTail
+  , lemmaMerging
   , (++)()
   , Map
   , Merge
+  , Concat
   , Check
   , Expecting
   , Missing
   , Ambiguous
+  , module Data.Type.Equality
+  , module Data.Proxy
   ) where
 import Data.Type.Equality
 import Data.Proxy
@@ -39,7 +54,7 @@
 import Data.Typeable
 import Language.Haskell.TH
 
--- | Generates 'Position' for an ordinal (0-origin).
+-- | Generates a 'Position' that corresponds to the given ordinal (0-origin).
 ord :: Int -> Q Exp
 ord n = do
   let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
@@ -59,10 +74,10 @@
 runPosition (Position n) = Right (Position (n - 1))
 {-# INLINE runPosition #-}
 
-comparePosition :: Position xs x -> Position xs y -> Maybe (x :~: y)
-comparePosition (Position m) (Position n)
-  | m == n = Just (unsafeCoerce Refl)
-  | otherwise = Nothing
+comparePosition :: Position xs x -> Position xs y -> Either Ordering (x :~: y)
+comparePosition (Position m) (Position n) = case compare m n of
+  EQ -> Right (unsafeCoerce Refl)
+  x -> Left x
 {-# INLINE comparePosition #-}
 
 navigate :: Position xs x -> Nav xs x
@@ -170,6 +185,9 @@
 lemmaHalfTail _ = unsafeCoerce
 {-# INLINE lemmaHalfTail #-}
 
+lemmaMerging :: p (Merge (Half xs) (Half (Tail xs))) -> p xs
+lemmaMerging = unsafeCoerce
+
 type family Map (f :: k -> k) (xs :: [k]) :: [k] where
   Map f '[] = '[]
   Map f (x ': xs) = f x ': Map f xs
@@ -177,6 +195,10 @@
 type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
   '[] ++ ys = ys
   (x ': xs) ++ ys = x ': xs ++ ys
+
+type family Concat (xs :: [[k]]) :: [k] where
+  Concat '[] = '[]
+  Concat (x ': xs) = x ++ Concat xs
 
 type family Merge (xs :: [k]) (ys :: [k]) :: [k] where
   Merge (x ': xs) (y ': ys) = x ': y ': Merge xs ys
diff --git a/src/Data/Extensible/Internal/HList.hs b/src/Data/Extensible/Internal/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Internal/HList.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+-----------------------------------------------------------------------
+--
+-- Module      :  Data.Extensible.Internal.HList
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+--
+-----------------------------------------------------------------------
+module Data.Extensible.Internal.HList where
+
+import Data.Extensible.Internal
+
+data HList (h :: k -> *) (s :: [k]) where
+  HNil :: HList h '[]
+  HCons :: h x -> HList h xs -> HList h (x ': xs)
+
+infixr 5 `HCons`
+
+merge :: HList h xs -> HList h ys -> HList h (Merge xs ys)
+merge (HCons x xs) (HCons y ys) = x `HCons` y `HCons` merge xs ys
+merge HNil ys = ys
+merge xs HNil = xs
+
+split :: forall h xs. HList h xs -> (HList h (Half xs), HList h (Half (Tail xs)))
+split (HCons x (HCons y ys)) = let (a, b) = split ys
+  in (HCons x a, lemmaHalfTail (Proxy :: Proxy (Tail (Tail xs))) $ HCons y b)
+split (HCons x HNil) = (HCons x HNil, HNil)
+split HNil = (HNil, HNil)
diff --git a/src/Data/Extensible/Internal/Rig.hs b/src/Data/Extensible/Internal/Rig.hs
--- a/src/Data/Extensible/Internal/Rig.hs
+++ b/src/Data/Extensible/Internal/Rig.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE PolyKinds, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, FlexibleInstances, DeriveFunctor #-}
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable#-}
 -----------------------------------------------------------------------------
 -- |
@@ -16,6 +15,7 @@
 import Unsafe.Coerce
 import Control.Applicative
 import Data.Typeable
+import Data.Monoid
 import Data.Foldable (Foldable)
 import Data.Traversable (Traversable)
 
@@ -51,9 +51,16 @@
 -- | Poly-kinded Const
 newtype Const' a x = Const' { getConst' :: a } deriving Show
 
+-- | Turn a wrapper type into one clause that returns @a@.
+newtype Match h a x = Match { runMatch :: h x -> a } deriving Typeable
+
+newtype Wrap2 h a x = Wrap2 { unwrap2 :: h x -> h x -> a }
+
 -- | Poly-kinded Maybe
 data Nullable h x = Null | Eine (h x) deriving (Show, Eq, Ord, Typeable)
 
+data Pair g h x = Pair (g x) (h x)
+
 -- | Destruct 'Nullable'.
 nullable :: r -> (h x -> r) -> Nullable h x -> r
 nullable r _ Null = r
@@ -66,6 +73,13 @@
 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
+newtype MergeList a = MergeList { getMerged :: [a] } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+
+instance Monoid (MergeList a) where
+  mempty = MergeList []
+  {-# INLINE mempty #-}
+  mappend (MergeList a) (MergeList b) = MergeList $ merge a b where
+    merge (x:xs) (y:ys) = x : y : merge xs ys
+    merge xs [] = xs
+    merge [] ys = ys
+  {-# INLINE mappend #-}
diff --git a/src/Data/Extensible/League.hs b/src/Data/Extensible/League.hs
--- a/src/Data/Extensible/League.hs
+++ b/src/Data/Extensible/League.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Rank2Types, DataKinds #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.League
@@ -47,6 +46,6 @@
 
 -- | Prepend a clause for @'Match' ('Fuse' x)@ as well as ('<?!').
 (<?~) :: (f x -> a) -> Match (Fuse x) a :* fs -> Match (Fuse x) a :* (f ': fs)
-(<?~) f = (<:*) (Match (f . meltdown))
+(<?~) f = (<:) (Match (f . meltdown))
 {-# INLINE (<?~) #-}
 infixr 1 <?~
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
@@ -1,4 +1,3 @@
-{-# LANGUAGE PolyKinds #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.League
@@ -19,12 +18,9 @@
   , caseOf) where
 
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
 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)
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,3 @@
-{-# LANGUAGE DataKinds #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Plain
@@ -28,7 +27,6 @@
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Product
 import Data.Extensible.Sum
-import Data.Extensible.Match
 import Data.Typeable
 import Unsafe.Coerce
 
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
@@ -1,8 +1,6 @@
-{-# LANGUAGE Rank2Types, GADTs #-}
-{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Product
@@ -17,6 +15,7 @@
 module Data.Extensible.Product (
   -- * Product
   (:*)(..)
+  , (<:)
   , (<:*)
   , (*++*)
   , hhead
@@ -32,10 +31,13 @@
   , sector
   , sectorAt
   , Generate(..)
-  , Forall(..)) where
+  , Forall(..)
+  , fromHList
+  , toHList) where
 
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
+import Data.Extensible.Internal.HList
 import Unsafe.Coerce
 import Data.Typeable
 import Control.Applicative
@@ -51,40 +53,40 @@
 
 deriving instance Typeable (:*)
 
-instance Show (h :* '[]) where
-  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 > 0) $
-     showsPrec 0 x
-    . showString " <:* "
-    . showsPrec 0 xs
-
 -- | /O(1)/ Extract the head element.
 hhead :: h :* (x ': xs) -> h x
 hhead (Tree a _ _) = a
+{-# INLINE hhead #-}
 
 -- | /O(n)/ Extract the tail of the product.
+-- FIXME: unsafeCoerce
 htail :: h :* (x ': xs) -> h :* xs
 htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
-htail _ = unsafeCoerce Nil
+htail (Tree _ Nil _) = unsafeCoerce Nil
 
 -- | Split a product to the head and the tail.
 huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
 huncons t@(Tree a _ _) = (a, htail t)
+{-# INLINE huncons #-}
 
--- | /O(log n)/ Add an element to a product.
+-- | An alias for ('<:').
 (<:*) :: 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 <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $ b <: d) c
 a <:* Nil = Tree a Nil Nil
 infixr 0 <:*
 
+-- | /O(log n)/ Add an element to a product.
+(<:) :: h x -> h :* xs -> h :* (x ': xs)
+(<:) = (<:*)
+{-# INLINE (<:) #-}
+infixr 0 <:
+
 -- | 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.
+-- | Combine products.
 (*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
 (*++*) Nil ys = ys
 (*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
@@ -124,24 +126,7 @@
   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))
-    (generateFor c id) where
-      dic = generateFor c $ const $ WrapEq (==)
-      aggr = getAll . hfoldMap (All . getConst')
-      c = Proxy :: Proxy (ClassComp Eq h)
-
-instance (Forall (ClassComp Eq h) xs, Forall (ClassComp Ord h) xs) => Ord (h :* xs) where
-  compare = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapOrd (view (sectorAt pos) dic))
-    (generateFor c id) where
-      dic = generateFor c $ const $ WrapOrd compare
-      aggr = hfoldMap getConst'
-      c = Proxy :: Proxy (ClassComp Ord h)
-
-newtype WrapEq h x = WrapEq { unwrapEq :: h x -> h x -> Bool }
-
-newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }
+{-# INLINE htabulate #-}
 
 -- | /O(log n)/ A lens for a specific element.
 sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
@@ -161,6 +146,7 @@
 
 -- | Given a function that maps types to values, we can "collect" entities all you want.
 class Generate (xs :: [k]) where
+  -- | /O(n)/ generates a product with the given function.
   generate :: (forall x. Position xs x -> h x) -> h :* xs
 
 instance Generate '[] where
@@ -169,9 +155,11 @@
 
 instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
   generate f = Tree (f here) (generate (f . navL)) (generate (f . navR))
+  {-# INLINE generate #-}
 
 -- | Guarantees the all elements satisfies the predicate.
 class Forall c (xs :: [k]) where
+  -- | /O(n)/ Analogous to 'generate', but it also supplies a context @c x@ for every elements in @xs@.
   generateFor :: proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs
 
 instance Forall c '[] where
@@ -180,3 +168,14 @@
 
 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))
+  {-# INLINE generateFor #-}
+
+-- | Turn a product into 'HList'.
+toHList :: h :* xs -> HList h xs
+toHList (Tree h a b) = HCons h $ lemmaMerging $ toHList a `merge` toHList b
+toHList Nil = HNil
+
+-- | Build a product from 'HList'.
+fromHList :: HList h xs -> h :* xs
+fromHList (HCons x xs) = let (a, b) = split xs in Tree x (fromHList a) (fromHList b)
+fromHList HNil = Nil
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
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell, PolyKinds, TypeFamilies, DataKinds, KindSignatures, FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances, Rank2Types #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Record
@@ -15,6 +15,7 @@
 module Data.Extensible.Record (
    module Data.Extensible.Inclusion
   , Record
+  , (<:)
   , (<:*)
   , (:*)(Nil)
   , (@=)
@@ -32,7 +33,7 @@
 import Language.Haskell.TH
 import GHC.TypeLits hiding (Nat)
 import Data.Extensible.Inclusion
-import Data.Proxy
+import Data.Extensible.Dictionary ()
 
 -- | Associates names with concrete types.
 type family FieldValue (s :: Symbol) :: *
@@ -40,9 +41,10 @@
 -- | The type of fields.
 data Field (s :: Symbol) = Field { getField :: FieldValue s }
 
--- | The type of records which contain several fields
+-- | The type of records which contain several fields.
 type Record = (:*) Field
 
+-- | Shows in @field \@= value@ style instead of the derived one.
 instance (KnownSymbol s, Show (FieldValue s)) => Show (Field s) where
   showsPrec d f@(Field a) = showParen (d >= 1) $ showString (symbolVal f)
     . showString " @= "
@@ -58,11 +60,11 @@
   => 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.
+-- This type is used to resolve the name of the field internally.
 type FieldName s = LabelPhantom s (FieldValue s) (Proxy (FieldValue s))
   -> Record '[s] -> Proxy (Record '[s])
 
--- | A ghostly type used to reify field names
+-- | A ghostly type which reifies the field name
 data LabelPhantom s a b
 
 -- | An internal class to characterize 'FieldLens'
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
@@ -1,7 +1,5 @@
-{-# LANGUAGE Rank2Types, GADTs #-}
-{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
@@ -24,7 +22,6 @@
   ) where
 
 import Data.Extensible.Internal
-import Data.Type.Equality
 import Control.Applicative
 import Data.Typeable
 
@@ -43,13 +40,6 @@
 embed = UnionAt membership
 {-# INLINE embed #-}
 
-instance Show (h :| '[]) where
-  show = exhaust
-
-instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where
-  showsPrec d = (\h -> showParen (d > 10) $ showString "embed " . showsPrec 11 h)
-    <:| showsPrec d
-
 -- | /O(1)/ Naive pattern match
 (<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r
 (<:|) r c = \(UnionAt pos h) -> case runPosition pos of
@@ -65,6 +55,6 @@
 -- | A traversal that tries to point a specific element.
 picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)
 picked f u@(UnionAt pos h) = case comparePosition (membership :: Position xs x) pos of
-  Just Refl -> fmap (UnionAt pos) (f h)
-  Nothing -> pure u
+  Right Refl -> fmap (UnionAt pos) (f h)
+  _ -> pure u
 {-# INLINE picked #-}
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
@@ -1,4 +1,3 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, Rank2Types #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Union
@@ -48,6 +47,6 @@
 
 -- | Prepend a clause for @'Match' ('Flux' x)@ as well as ('<?!').
 (<$?~) :: (forall b. f b -> (b -> x) -> a) -> Match (Flux x) a :* fs -> Match (Flux x) a :* (f ': fs)
-(<$?~) f = (<:*) $ Match $ \(Flux g m) -> f m g
+(<$?~) f = (<:) $ Match $ \(Flux g m) -> f m g
 {-# INLINE (<$?~) #-}
 infixr 1 <$?~