diff --git a/examples/aeson.hs b/examples/aeson.hs
new file mode 100644
--- /dev/null
+++ b/examples/aeson.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeOperators, DataKinds, FlexibleContexts, FlexibleInstances, UndecidableInstances, PolyKinds, TemplateHaskell #-}
+import Data.Aeson (FromJSON(..), withObject)
+import Data.Extensible (Record, Field(..), KeyValue, AssocKey, Forall, hgenerateFor)
+import GHC.TypeLits (KnownSymbol, symbolVal)
+import Data.Proxy
+import Data.String (fromString)
+import qualified Data.HashMap.Strict as HM
+
+keyProxy :: proxy kv -> Proxy (AssocKey kv)
+keyProxy _ = Proxy
+
+instance Forall (KeyValue KnownSymbol FromJSON) xs => FromJSON (Record xs) where
+  parseJSON = withObject "Object" $ \v -> hgenerateFor (Proxy :: Proxy (KeyValue KnownSymbol FromJSON))
+    $ \m -> let k = symbolVal (keyProxy m) in case HM.lookup (fromString k) v of
+      Just a -> Field <$> return <$> parseJSON a
+      Nothing -> fail $ "Missing key: " ++ k
diff --git a/examples/records.hs b/examples/records.hs
--- a/examples/records.hs
+++ b/examples/records.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE TemplateHaskell, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts #-}
-import Data.Extensible.Record
 import Data.Extensible
 import Control.Lens
 
@@ -14,12 +13,12 @@
   , "quantity" :> Int]
 
 s0 :: Num c => Stock c
-s0 = Field "DA-192H"
-  <: Field 260
-  <: Field 120
-  <: Field True
-  <: Field "High-quality (24bit 192kHz), lightweight portable DAC"
-  <: Field 20
+s0 = name @= "DA-192H"
+  <: weight @= 260
+  <: price @= 120
+  <: featured @= True
+  <: description @= "High-quality (24bit 192kHz), lightweight portable DAC"
+  <: quantity @= 20
   <: Nil
 
 -- Use shrinkAssoc to permute elements
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.3.3
+version:             0.3.4
 synopsis:            Extensible, efficient, lens-friendly data types
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
@@ -31,15 +31,18 @@
     Data.Extensible
     Data.Extensible.Class
     Data.Extensible.Dictionary
+    Data.Extensible.Field
     Data.Extensible.Inclusion
     Data.Extensible.Internal
     Data.Extensible.Internal.Rig
     Data.Extensible.Match
+    Data.Extensible.Nullable
     Data.Extensible.Plain
     Data.Extensible.Product
-    Data.Extensible.Record
     Data.Extensible.Sum
     Data.Extensible.Union
+    Data.Extensible.Wrapper
+    Data.Extensible.TH
   default-extensions: TypeOperators
     , DeriveDataTypeable
     , KindSignatures
@@ -51,7 +54,7 @@
     , FlexibleInstances
     , PolyKinds
     , CPP
-  build-depends:       base >= 4.7 && <5, template-haskell, constraints, profunctors
+  build-depends:       base >= 4.7 && <5, template-haskell, constraints, profunctors, tagged, transformers
   hs-source-dirs:      src
   ghc-options: -Wall
   default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Safe #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible
@@ -8,39 +9,33 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- This package defines an extensible type-indexed product type and a union type.
--- 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.
---
--- >>> let t = K0 (42 :: Int) <:* K0 "foo" <:* K0 (Just "bar") <:* Nil
--- >>> t
--- K0 42 <:* K0 "foo" <:* K0 (Just "bar") <:* Nil
--- >>> :t t
--- t :: K0 :* '[Int, [Char], Maybe [Char]]
--- >>> pluck t :: Int
--- 42
+-- This module just reexports everything.
 -----------------------------------------------------------------------------
 module Data.Extensible (
-  -- * Reexport
   module Data.Extensible.Class
   , module Data.Extensible.Dictionary
+  , module Data.Extensible.Field
   , module Data.Extensible.Inclusion
   , module Data.Extensible.Match
+  , module Data.Extensible.Nullable
   , module Data.Extensible.Plain
-  , module Data.Extensible.Record
   , module Data.Extensible.Product
   , module Data.Extensible.Sum
-  , Comp(..)
-  , comp
+  , module Data.Extensible.TH
+  , module Data.Extensible.Union
+  , module Data.Extensible.Wrapper
   ) where
 
 import Data.Extensible.Class
 import Data.Extensible.Dictionary
+import Data.Extensible.Field
 import Data.Extensible.Inclusion
-import Data.Extensible.Internal.Rig
 import Data.Extensible.Match
+import Data.Extensible.Nullable
 import Data.Extensible.Plain
 import Data.Extensible.Product
-import Data.Extensible.Record
 import Data.Extensible.Sum
+import Data.Extensible.TH
+import Data.Extensible.Union
+import Data.Extensible.Wrapper
+
diff --git a/src/Data/Extensible/Class.hs b/src/Data/Extensible/Class.hs
--- a/src/Data/Extensible/Class.hs
+++ b/src/Data/Extensible/Class.hs
@@ -1,9 +1,24 @@
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Class
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  MPTCs
+--
+-----------------------------------------------------------------------------
 module Data.Extensible.Class (
   -- * Class
    Extensible(..)
   , piece
   , pieceAssoc
+  , itemAt
+  , item
+  , itemAssoc
   -- * Membership
   , Membership
   , mkMembership
@@ -21,17 +36,37 @@
   , Elaborated(..)
   ) where
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig (Optic')
+import Data.Extensible.Wrapper
+import Data.Profunctor
 
 -- | This class allows us to use 'pieceAt' for both sums and products.
-class Extensible f p q (t :: (k -> *) -> [k] -> *) where
-  pieceAt :: Membership xs x -> p (h x) (f (h x)) -> q (t h xs) (f (t h xs))
+class (Functor f, Profunctor p) => Extensible f p (t :: (k -> *) -> [k] -> *) where
+  pieceAt :: Membership xs x -> Optic' p f (t h xs) (h x)
 
 -- | Accessor for an element.
-piece :: (x ∈ xs, Extensible f p q t) => p (h x) (f (h x)) -> q (t h xs) (f (t h xs))
+piece :: (x ∈ xs, Extensible f p t) => Optic' p f (t h xs) (h x)
 piece = pieceAt membership
 {-# INLINE piece #-}
 
 -- | Like 'piece', but reckon membership from its key.
-pieceAssoc :: (Associate k v xs, Extensible f p q t) => p (h (k ':> v)) (f (h (k ':> v))) -> q (t h xs) (f (t h xs))
+pieceAssoc :: (Associate k v xs, Extensible f p t) => Optic' p f (t h xs) (h (k ':> v))
 pieceAssoc = pieceAt association
 {-# INLINE pieceAssoc #-}
+
+itemAt :: (Wrapper h, Extensible f p t) => Membership xs x -> Optic' p f (t h xs) (Repr h x)
+itemAt m = pieceAt m . _Wrapper
+{-# INLINE itemAt #-}
+
+item :: (Wrapper h, Extensible f p t, x ∈ xs) => proxy x -> Optic' p f (t h xs) (Repr h x)
+item p = piece . _WrapperAs p
+{-# INLINE item #-}
+
+itemAssoc :: (Wrapper h, Extensible f p t, Associate k v xs)
+  => proxy k -> Optic' p f (t h xs) (Repr h (k ':> v))
+itemAssoc p = pieceAssoc . _WrapperAs (proxyKey p)
+{-# INLINE itemAssoc #-}
+
+proxyKey :: proxy k -> Proxy (k ':> v)
+proxyKey _ = Proxy
+{-# INLINE proxyKey #-}
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
--- a/src/Data/Extensible/Dictionary.hs
+++ b/src/Data/Extensible/Dictionary.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE PolyKinds, TypeFamilies, InstanceSigs, UndecidableInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -----------------------------------------------------------------------
 --
@@ -10,9 +12,10 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- Reifying classes to make instances for (':*') and (':|')
+-- Reification of constraints using extensible data types.
+-- Also includes orphan instances.
 -----------------------------------------------------------------------
-module Data.Extensible.Dictionary where
+module Data.Extensible.Dictionary (library, WrapForall, Instance1) where
 import Data.Monoid
 import Data.Extensible.Class
 import Data.Extensible.Product
@@ -20,12 +23,25 @@
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Constraint
+import Data.Extensible.Wrapper
+import Data.Profunctor.Unsafe
 
 -- | Reify a collection of dictionaries, as you wish.
 library :: forall c xs. Forall c xs => Comp Dict c :* xs
 library = htabulateFor (Proxy :: Proxy c) $ const (Comp Dict)
 {-# INLINE library #-}
 
+newtype MergeList a = MergeList { getMerged :: [a] }
+
+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 #-}
+
 instance WrapForall Show h xs => Show (h :* xs) where
   showsPrec d = showParen (d > 0)
     . (.showString "Nil")
@@ -35,7 +51,7 @@
     . hzipWith (\(Comp Dict) h -> Const' $ MergeList [showsPrec 0 h . showString " <: "]) (library :: Comp Dict (Instance1 Show h) :* xs)
 
 instance WrapForall Eq h xs => Eq (h :* xs) where
-  xs == ys = getAll $ hfoldMap (All . getConst')
+  xs == ys = getAll $ hfoldMap (All #. getConst')
     $ hzipWith3 (\(Comp Dict) x y -> Const' $ x == y) (library :: Comp Dict (Instance1 Eq h) :* xs) xs ys
   {-# INLINE (==) #-}
 
diff --git a/src/Data/Extensible/Field.hs b/src/Data/Extensible/Field.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Field.hs
@@ -0,0 +1,155 @@
+#if MIN_VERSION_base(4,8,0)
+{-# LANGUAGE Safe #-}
+#else
+{-# LANGUAGE Trustworthy #-}
+#endif
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Record
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Flexible records and variants
+-- Example: <https://github.com/fumieval/extensible/blob/master/examples/records.hs>
+------------------------------------------------------------------------
+module Data.Extensible.Field (
+  Field(..)
+  , (@=)
+  , (<@=>)
+  , FieldOptic
+  , FieldName
+  -- * Records and variants
+  , RecordOf
+  , Record
+  , emptyRecord
+  , VariantOf
+  , Variant
+  -- * Constraint
+  , AssocKey
+  , AssocValue
+  , KeyValue
+  -- * Internal
+  , LabelPhantom
+  , Labelling
+  , Inextensible
+  ) where
+import Data.Extensible.Class
+import Data.Extensible.Sum
+import Data.Extensible.Product
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+import Data.Profunctor.Unsafe
+import Data.Constraint
+import Data.Extensible.Wrapper
+import Data.Functor.Identity
+import GHC.TypeLits hiding (Nat)
+
+type family AssocKey (kv :: Assoc k v) :: k where
+  AssocKey (k ':> v) = k
+
+type family AssocValue (kv :: Assoc k v) :: v where
+  AssocValue (k ':> v) = v
+
+class (pk (AssocKey kv), pv (AssocValue kv)) => KeyValue pk pv kv where
+
+instance (pk k, pv v) => KeyValue pk pv (k ':> v)
+
+-- | A @'Field' h (k ':> v)@ is @h v@, but is along with the index @k@.
+--
+-- @'Field' :: (v -> *) -> Assoc k v -> *@
+--
+newtype Field (h :: v -> *) (kv :: Assoc k v) = Field (h (AssocValue kv))
+
+instance Wrapper h => Wrapper (Field h) where
+  type Repr (Field h) kv = Repr h (AssocValue kv)
+  _Wrapper = dimap (\(Field v) -> v) (fmap Field) . _Wrapper
+  {-# INLINE _Wrapper #-}
+
+-- | Shows in @field \@= value@ style instead of the derived one.
+instance (KnownSymbol k, Wrapper h, Show (Repr h v)) => Show (Field h (k ':> v)) where
+  showsPrec d (Field a) = showParen (d >= 1) $ showString (symbolVal (Proxy :: Proxy k))
+    . showString " @= "
+    . showsPrec 1 (view _Wrapper a)
+
+-- | The type of records which contain several fields.
+--
+-- @RecordOf :: (v -> *) -> [Assoc k v] -> *@
+--
+type RecordOf h = (:*) (Field h)
+
+-- | The dual of 'RecordOf'
+--
+-- @VariantOf :: (v -> *) -> [Assoc k v] -> *@
+--
+type VariantOf h = (:|) (Field h)
+
+-- | Simple record
+type Record = RecordOf Identity
+
+-- | Simple variant
+type Variant = VariantOf Identity
+
+-- | An empty 'Record'.
+emptyRecord :: Record '[]
+emptyRecord = Nil
+{-# INLINE emptyRecord #-}
+
+-- | @FieldOptic s@ is a type of optics that points a field/constructor named @s@.
+--
+-- The yielding fields can be
+-- <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Lens Lens>es
+-- for 'Record's and
+-- <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Prism Prism>s
+-- for 'Variant's.
+--
+-- @
+-- 'FieldOptic' "foo" = Associate "foo" a xs => Lens' ('Record' xs) a
+-- 'FieldOptic' "foo" = Associate "foo" a xs => Prism' ('Variant' xs) a
+-- @
+--
+-- 'FieldOptic's can be generated using 'mkField' defined in the "Data.Extensible.TH" module.
+--
+type FieldOptic k = forall f p t xs (h :: kind -> *) (v :: kind). (Extensible f p t
+  , Associate k v xs
+  , Labelling k p
+  , Wrapper h)
+  => p (Repr h v) (f (Repr h v)) -> p (t (Field h) xs) (f (t (Field h) xs))
+
+-- | The trivial inextensible data type
+data Inextensible (h :: k -> *) (xs :: [k])
+
+instance Functor f => Extensible f (LabelPhantom s) Inextensible where
+  pieceAt _ _ = error "Impossible"
+
+-- | When you see this type as an argument, it expects a 'FieldLens'.
+-- This type is used to resolve the name of the field internally.
+type FieldName k = forall v. LabelPhantom k () (Proxy ())
+  -> LabelPhantom k (Inextensible (Field Proxy) '[k ':> v]) (Proxy (Inextensible (Field Proxy) '[k ':> v]))
+
+type family Labelling s p :: Constraint where
+  Labelling s (LabelPhantom t) = s ~ t
+  Labelling s p = ()
+
+-- | A ghostly type which spells the field name
+data LabelPhantom s a b
+
+instance Profunctor (LabelPhantom s) where
+  dimap _ _ _ = error "Impossible"
+
+-- | Annotate a value by the field name.
+(@=) :: Wrapper h => FieldName k -> Repr h v -> Field h (k ':> v)
+(@=) _ = Field #. review _Wrapper
+{-# INLINE (@=) #-}
+infix 1 @=
+
+-- | Lifted ('@=')
+(<@=>) :: (Functor f, Wrapper h) => FieldName k -> f (Repr h v) -> Comp f (Field h) (k ':> v)
+(<@=>) k = Comp #. fmap (k @=)
+{-# INLINE (<@=>) #-}
+infix 1 <@=>
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,6 +1,7 @@
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Inclusion
 -- Copyright   :  (c) Fumiaki Kinoshita 2015
@@ -24,13 +25,6 @@
   , inclusionAssoc
   , shrinkAssoc
   , spreadAssoc
-  -- * Inverse
-  , coinclusion
-  , wrench
-  , retrench
-  , Nullable(..)
-  , nullable
-  , mapNullable
   ) where
 
 import Data.Extensible.Class
@@ -38,7 +32,6 @@
 import Data.Extensible.Sum
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
-import Data.Monoid
 
 -- | Unicode alias for 'Include'
 type xs ⊆ ys = Include ys xs
@@ -60,23 +53,6 @@
 spread :: (xs ⊆ ys) => h :| xs -> h :| ys
 spread (EmbedAt i h) = views (pieceAt i) EmbedAt inclusion h
 {-# INLINE spread #-}
-
--- | The inverse of 'inclusion'.
-coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys
-coinclusion = flip appEndo (htabulate (const Null))
-  $ hfoldMap getConst'
-  $ hmapWithIndex (\src dst -> Const' $ Endo $ pieceAt 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 = mapNullable (flip hlookup xs) `hmap` coinclusion
-{-# INLINE wrench #-}
-
--- | Narrow the range of the sum, if possible.
-retrench :: (Generate ys, xs ⊆ ys) => h :| ys -> Nullable ((:|) h) xs
-retrench (EmbedAt i h) = views (pieceAt i) (mapNullable (`EmbedAt`h)) coinclusion
-{-# INLINE retrench #-}
 
 ------------------------------------------------------------------
 
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,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FunctionalDependencies #-}
@@ -48,8 +49,6 @@
   , Half
   , Head
   , Tail
-  , lemmaHalfTail
-  , lemmaMerging
   , (++)()
   , Map
   , Merge
@@ -236,15 +235,6 @@
 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 #-}
-
--- | GHC can't prove this
-lemmaMerging :: p (Merge (Half xs) (Half (Tail xs))) -> p xs
-lemmaMerging = unsafeCoerce
 
 -- | Type level map
 type family Map (f :: k -> k) (xs :: [k]) :: [k] where
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,4 @@
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# LANGUAGE Trustworthy #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Rig
@@ -7,88 +7,56 @@
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
 -- Stability   :  experimental
--- Portability :  non-portable
+-- Portability :  portable
 --
--- Miscellaneous utilities
+-- Re-implementation of lens combinators
 ------------------------------------------------------------------------
-module Data.Extensible.Internal.Rig where
-import Unsafe.Coerce
-import Data.Typeable
+module Data.Extensible.Internal.Rig (
+  Optic
+  , Optic'
+  , view
+  , views
+  , over
+  , withIso
+  , Exchange(..)
+  , review
+  )
+where
 import Control.Applicative
-#if !MIN_VERSION_base(4,8,0)
-import Data.Monoid
-import Data.Foldable (Foldable)
-import Data.Traversable (Traversable)
-#endif
 import Data.Profunctor
+import Data.Functor.Identity
+import Data.Tagged
+import Data.Coerce
 
--- | A type synonym for lenses
-type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
+type Optic p f s t a b = p a (f b) -> p s (f t)
+type Optic' p f s a = p a (f a) -> p s (f s)
 
--- | @'view' :: Lens' s a -> (a -> a) -> (s -> s)@
-view :: ((a -> Const a a) -> s -> Const a s) -> s -> a
+-- | @'view' :: Getter s a -> s -> a@
+view :: Optic' (->) (Const a) s a -> 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
+-- | @'views' :: Getter s a -> (a -> r) -> (s -> r)@
+views :: Optic' (->) (Const r) s a -> (a -> r) -> s -> r
+views = coerce
 {-# INLINE views #-}
 
--- | Just a value.
-newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable, Functor, Foldable, Traversable)
-
-_K0 :: (Functor f, Profunctor p) => p a (f b) -> p (K0 a) (f (K0 b))
-_K0 = dimap getK0 (fmap K0)
-
-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
+-- | @'over' :: Setter s t a b -> (a -> b) -> (s -> t)@
+over :: Optic (->) Identity s t a b -> (a -> b) -> s -> t
+over = coerce
 {-# INLINE over #-}
 
--- | Poly-kinded Const
-newtype Const' a x = Const' { getConst' :: a } deriving Show
-
-newtype Comp f g a = Comp { getComp :: f (g a) }
-
-comp :: Functor f => (a -> g b) -> f a -> Comp f g b
-comp f = Comp . fmap f
-{-# INLINE comp #-}
-
--- | 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 #-}
+data Exchange a b s t = Exchange (s -> a) (b -> t)
 
--- | 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 #-}
+instance Profunctor (Exchange a b) where
+  dimap f g (Exchange sa bt) = Exchange (sa . f) (g . bt)
+  {-# INLINE dimap #-}
 
--- A list, but with Monoid instance based on merging
-newtype MergeList a = MergeList { getMerged :: [a] } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+withIso :: Optic (Exchange a b) Identity s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+withIso l r = case l (Exchange id Identity) of
+  Exchange f g -> r f (coerce g)
+{-# INLINE withIso #-}
 
-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 #-}
+review :: Optic' Tagged Identity s a -> a -> s
+review = coerce
+{-# INLINE review #-}
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,3 +1,5 @@
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.League
@@ -13,7 +15,6 @@
 module Data.Extensible.Match (
   matchWith
   , Match(..)
-  , _Match
   , match
   , mapMatch
   , caseOf) where
@@ -22,8 +23,9 @@
 import Data.Extensible.Class
 import Data.Extensible.Product
 import Data.Extensible.Sum
-import Data.Profunctor
-import Data.Typeable
+import Data.Extensible.Wrapper
+import Data.Typeable (Typeable)
+import Data.Profunctor.Unsafe
 
 -- | Retrieve the contents so that they matches and pass both to the given function.
 matchWith :: (forall x. f x -> g x -> r) -> f :* xs -> g :| xs -> r
@@ -46,8 +48,10 @@
 {-# INLINE caseOf #-}
 infix 0 `caseOf`
 
--- | Turn a wrapper type into one clause that returns @a@.
-newtype Match h a x = Match { runMatch :: h x -> a } deriving Typeable
+-- | Turn a wrapper type into a clause for it.
+newtype Match h r x = Match { runMatch :: h x -> r } deriving Typeable
 
-_Match :: (Profunctor p, Functor f) => p (g x -> a) (f (h y -> b)) -> p (Match g a x) (f (Match h b y))
-_Match = dimap runMatch (fmap Match)
+instance Wrapper h => Wrapper (Match h r) where
+  type Repr (Match h r) x = Repr h x -> r
+  _Wrapper = withIso _Wrapper $ \f g -> dimap ((. g) .# runMatch) (fmap (Match #. (. f)))
+  {-# INLINE _Wrapper #-}
diff --git a/src/Data/Extensible/Nullable.hs b/src/Data/Extensible/Nullable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Nullable.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE LambdaCase, TypeFamilies #-}
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Nullable
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Nullable (
+  coinclusion
+  , wrench
+  , retrench
+  , Nullable(..)
+  , mapNullable) where
+
+import Data.Extensible.Class
+import Data.Extensible.Product
+import Data.Extensible.Sum
+import Data.Extensible.Inclusion
+import Data.Extensible.Internal.Rig
+import Data.Typeable (Typeable)
+import Data.Monoid
+import Data.Extensible.Wrapper
+import Data.Profunctor.Unsafe
+
+-- | Poly-kinded Maybe
+newtype Nullable h x = Nullable { getNullable :: Maybe (h x) } deriving (Show, Eq, Ord, Typeable)
+
+instance Wrapper h => Wrapper (Nullable h) where
+  type Repr (Nullable h) x = Maybe (Repr h x)
+  _Wrapper = withIso _Wrapper $ \f g -> dimap (fmap f . getNullable) (fmap (Nullable . fmap g))
+
+-- | Apply a function to its content.
+mapNullable :: (g x -> h y) -> Nullable g x -> Nullable h y
+mapNullable f = Nullable #. fmap f .# getNullable
+{-# INLINE mapNullable #-}
+
+-- | The inverse of 'inclusion'.
+coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys
+coinclusion = flip appEndo (htabulate $ const $ Nullable Nothing)
+  $ hfoldMap getConst'
+  $ hmapWithIndex (\src dst -> Const' $ Endo $ pieceAt dst `over` const (Nullable $ Just src))
+  $ inclusion
+
+-- | Extend a product and fill missing fields by 'Null'.
+wrench :: (Generate ys, xs ⊆ ys) => h :* xs -> Nullable h :* ys
+wrench xs = mapNullable (flip hlookup xs) `hmap` coinclusion
+{-# INLINE wrench #-}
+
+-- | Narrow the range of the sum, if possible.
+retrench :: (Generate ys, xs ⊆ ys) => h :| ys -> Nullable ((:|) h) xs
+retrench (EmbedAt i h) = views (pieceAt i) (mapNullable (`EmbedAt`h)) coinclusion
+{-# INLINE retrench #-}
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,5 @@
-{-# LANGUAGE LambdaCase, TemplateHaskell #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE LambdaCase #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Plain
@@ -11,94 +12,52 @@
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Plain (
-  K0(..)
-  , _K0
-  , AllOf
+    AllOf
   , OneOf
   , (<%)
   , pluck
   , bury
   , (<%|)
   , accessing
-  , decFields
-  , decFieldsDeriving
   ) where
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Class
 import Data.Extensible.Product
 import Data.Extensible.Sum
-import Unsafe.Coerce
-import Language.Haskell.TH hiding (Match(..))
-import Data.Char
+import Data.Functor.Identity
+import Data.Extensible.Wrapper
 import Data.Coerce
+import Data.Profunctor.Unsafe
 
 -- | Alias for plain products
-type AllOf xs = K0 :* xs
+type AllOf xs = Identity :* xs
 
 -- | Alias for plain sums
-type OneOf xs = K0 :| xs
+type OneOf xs = Identity :| xs
 
 -- | /O(log n)/ Add a plain value to a product.
 (<%) :: x -> AllOf xs -> AllOf (x ': xs)
-(<%) = unsafeCoerce (<:*)
+(<%) = (<:) .# Identity
 {-# INLINE (<%) #-}
 infixr 5 <%
 
 -- | Extract a plain value.
 pluck :: (x ∈ xs) => AllOf xs -> x
-pluck = views piece getK0
+pluck = views piece runIdentity
 {-# INLINE pluck #-}
 
 -- | Embed a plain value.
 bury :: (x ∈ xs) => x -> OneOf xs
-bury = embed . K0
+bury = embed .# Identity
 {-# INLINE bury #-}
 
 -- | Naive pattern matching for a plain value.
 (<%|) :: (x -> r) -> (OneOf xs -> r) -> OneOf (x ': xs) -> r
-(<%|) = unsafeCoerce (<:|)
+(<%|) = (<:|) . (.# runIdentity)
 infixr 1 <%|
 
 -- | An accessor for newtype constructors.
-accessing :: (Coercible b a, b ∈ xs) => (a -> b) -> Lens' (AllOf xs) a
-accessing c f = piece (_K0 (fmap c . f . coerce))
+accessing :: (Coercible x a, x ∈ xs, Extensible f p t) => (a -> x) -> Optic' p f (t Identity xs) a
+accessing c = piece . _Wrapper . dimap coerce (fmap c)
 {-# INLINE accessing #-}
-
--- | Generate newtype wrappers and lenses from type synonyms.
---
--- @
--- decFields [d|type Foo = Int|]
--- @
---
--- Generates:
---
--- @
--- newtype Foo = Foo Int
--- foo :: (Foo ∈ xs) => Lens' (AllOf xs) Int
--- foo = accessing Foo
--- @
---
-decFields :: DecsQ -> DecsQ
-decFields = decFieldsDeriving []
-
--- | 'decFields' with additional deriving clauses
-decFieldsDeriving :: [Name] -> DecsQ -> DecsQ
-decFieldsDeriving drv' ds = ds >>= fmap concat . mapM mkBody
-  where
-    mkBody (NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) drv) = do
-      let name = let (x:xs) = nameBase name_ in mkName (toLower x : xs)
-      xs <- newName "xs"
-      sequence [return $ NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) (drv' ++ drv)
-        ,sigD name
-#if MIN_VERSION_template_haskell(2,10,0)
-          $ forallT (PlainTV xs : tvs) (sequence [conT ''Member `appT` varT xs `appT` conT name_])
-#else
-          $ forallT (PlainTV xs : tvs) (sequence [classP ''Member [varT xs, conT name_]])
-#endif
-          $ conT ''Lens' `appT` (conT ''AllOf `appT` varT xs) `appT` return ty
-        , valD (varP name) (normalB $ varE 'accessing `appE` conE nc) []
-        , return $ PragmaD $ InlineP name Inline FunLike AllPhases
-        ]
-    mkBody (TySynD name_ tvs ty) = mkBody (NewtypeD [] name_ tvs (NormalC (mkName (nameBase name_)) [(NotStrict, ty)]) [])
-    mkBody _ = fail "Unsupported declaration: genField handles newtype declarations or type synonyms"
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,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
@@ -50,10 +51,16 @@
 import Control.Applicative
 #endif
 import Data.Monoid
-import Data.Typeable
+import Data.Typeable (Typeable)
 import Data.Extensible.Class
+import Data.Functor.Identity
+import Data.Extensible.Wrapper
+import Data.Profunctor.Unsafe
 
 -- | The type of extensible products.
+--
+-- @(:*) :: (k -> *) -> [k] -> *@
+--
 data (h :: k -> *) :* (s :: [k]) where
   Nil :: h :* '[]
   Tree :: !(h x)
@@ -68,7 +75,7 @@
 hhead (Tree a _ _) = a
 {-# INLINE hhead #-}
 
--- | /O(n)/ Extract the tail of the product.
+-- | /O(log 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
@@ -183,7 +190,7 @@
   go _ Nil = pure Nil
 {-# INLINE htraverseWithIndex #-}
 
-instance Functor f => Extensible f (->) (->) (:*) where
+instance Functor f => Extensible f (->) (:*) where
   -- | /O(log n)/ A lens for a value in a known position.
   pieceAt = pieceAt_
   {-# INLINE pieceAt #-}
@@ -230,7 +237,7 @@
 -- 'hindex' ('htabulate' k) ≡ k
 -- @
 htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
-htabulate f = getK0 (hgenerate (K0 . f))
+htabulate f = runIdentity (hgenerate (Identity #. f))
 {-# INLINE htabulate #-}
 
 -- | Guarantees the all elements satisfies the predicate.
@@ -251,5 +258,10 @@
 
 -- | Pure version of 'hgenerateFor'.
 htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
-htabulateFor p f = getK0 (hgenerateFor p (K0 . f))
+htabulateFor p f = runIdentity (hgenerateFor p (Identity #. f))
 {-# INLINE htabulateFor #-}
+
+-- | GHC can't prove this
+lemmaHalfTail :: proxy xs -> h :* (x ': Half (Tail xs)) -> h :* (Half (x ': xs))
+lemmaHalfTail _ = unsafeCoerce
+{-# INLINE lemmaHalfTail #-}
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
deleted file mode 100644
--- a/src/Data/Extensible/Record.hs
+++ /dev/null
@@ -1,139 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies, FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.Record
--- Copyright   :  (c) Fumiaki Kinoshita 2015
--- License     :  BSD3
---
--- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Flexible records and variants
--- Example: <https://github.com/fumieval/extensible/blob/master/examples/records.hs>
-------------------------------------------------------------------------
-module Data.Extensible.Record (
-   module Data.Extensible.Class
-  , module Data.Extensible.Inclusion
-  , (@=)
-  , (<@=>)
-  , mkField
-  , Field(..)
-  , getField
-  , FieldOptic
-  , FieldName
-  , fieldOptic
-  -- * Records and variants
-  , Record
-  , (<:)
-  , (:*)(Nil)
-  , Variant
-  -- * Internal
-  , LabelPhantom
-  , Labelling
-  ) where
-import Data.Extensible.Class
-import Data.Extensible.Sum
-import Data.Extensible.Product
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Language.Haskell.TH
-import GHC.TypeLits hiding (Nat)
-import Data.Extensible.Inclusion
-import Data.Extensible.Dictionary ()
-import Control.Monad
-import Data.Profunctor
-import Data.Constraint
-
--- | The type of fields.
-data Field kv where
-  Field :: v -> Field (k ':> v)
-
--- | Get a value of a field.
-getField :: Field (k ':> v) -> v
-getField (Field v) = v
-{-# INLINE getField #-}
-
--- | The type of records which contain several fields.
-type Record = (:*) Field
-
--- | The dual of 'Record'
-type Variant = (:|) Field
-
--- | Shows in @field \@= value@ style instead of the derived one.
-instance (KnownSymbol k, Show v) => Show (Field (k ':> v)) where
-  showsPrec d (Field a) = showParen (d >= 1) $ showString (symbolVal (Proxy :: Proxy k))
-    . showString " @= "
-    . showsPrec 1 a
-
--- | @FieldOptic s@ is a type of optics that points a field/constructor named @s@.
---
--- The yielding fields can be
--- <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Lens Lens>es
--- for 'Record's and
--- <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Prism Prism>s
--- for 'Variant's.
---
--- @
--- 'FieldOptic' "foo" = Associate "foo" a xs => Lens' ('Record' xs) a
--- 'FieldOptic' "foo" = Associate "foo" a xs => Prism' ('Variant' xs) a
--- @
---
-type FieldOptic k = forall f p q t xs v. (Functor f
-  , Profunctor p
-  , Extensible f p q t
-  , Associate k v xs
-  , Labelling k p)
-  => p v (f v) -> q (t Field xs) (f (t Field xs))
-
--- | When you see this type as an argument, it expects a 'FieldLens'.
--- This type is used to resolve the name of the field internally.
-type FieldName k = forall v. LabelPhantom k v (Proxy v)
-  -> Record '[k ':> v] -> Proxy (Record '[k ':> v])
-
-type family Labelling s p :: Constraint where
-  Labelling s (LabelPhantom t) = s ~ t
-  Labelling s p = ()
-
--- | A ghostly type which spells the field name
-data LabelPhantom s a b
-
-instance Profunctor (LabelPhantom s) where
-  dimap _ _ _ = error "Impossible"
-
-instance Extensible f (LabelPhantom s) q t where
-  pieceAt _ _ = error "Impossible"
-
--- | Annotate a value by the field name.
-(@=) :: FieldName k -> v -> Field (k ':> v)
-(@=) _ = Field
-{-# INLINE (@=) #-}
-infix 1 @=
-
--- | Lifted ('@=')
-(<@=>) :: Functor f => FieldName k -> f v -> Comp f Field (k ':> v)
-(<@=>) _ = comp Field
-{-# INLINE (<@=>) #-}
-infix 1 <@=>
-
--- | Generate a field optic from the given name.
-fieldOptic :: forall proxy k. proxy k -> FieldOptic k
-fieldOptic _ = pieceAssoc . dimap getField (fmap (Field :: v -> Field (k ':> v)))
-{-# INLINE fieldOptic #-}
-
--- | Generate fields using 'fieldOptic'.
--- @'mkField' "foo bar"@ defines:
---
--- @
--- foo :: FieldOptic "foo"
--- bar :: FieldOptic "bar"
--- @
---
-mkField :: String -> DecsQ
-mkField str = fmap concat $ forM (words str) $ \s -> do
-  let st = litT (strTyLit s)
-  let lbl = conE 'Proxy `sigE` (conT ''Proxy `appT` st)
-  sequence [sigD (mkName s) $ conT ''FieldOptic `appT` st
-    , valD (varP (mkName s)) (normalB $ varE 'fieldOptic `appE` lbl) []
-    , 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
@@ -1,5 +1,5 @@
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
@@ -36,6 +36,9 @@
 import Data.Profunctor
 
 -- | The extensible sum type
+--
+-- @(:|) :: (k -> *) -> [k] -> *@
+--
 data (h :: k -> *) :| (s :: [k]) where
   EmbedAt :: !(Membership xs x) -> h x -> h :| xs
 deriving instance Typeable (:|)
@@ -90,7 +93,8 @@
   _ -> pure u
 {-# INLINE picked #-}
 
-instance (Applicative f, Choice p) => Extensible f p p (:|) where
-  pieceAt m p = dimap (\t@(EmbedAt i h) -> case compareMembership i m of
+instance (Applicative f, Choice p) => Extensible f p (:|) where
+  pieceAt m = dimap (\t@(EmbedAt i h) -> case compareMembership i m of
     Right Refl -> Right h
-    Left _ -> Left t) (either pure (fmap (EmbedAt m))) (right' p)
+    Left _ -> Left t) (either pure (fmap (EmbedAt m))) . right'
+  {-# INLINABLE pieceAt #-}
diff --git a/src/Data/Extensible/TH.hs b/src/Data/Extensible/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/TH.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE Trustworthy, TemplateHaskell #-}
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.TH
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.TH (mkField, decFields, decFieldsDeriving) where
+
+import Data.Proxy
+import Data.Extensible.Class (Member, Extensible, itemAssoc)
+import Data.Extensible.Field (FieldOptic)
+import Data.Extensible.Plain (accessing)
+import Language.Haskell.TH
+import Control.Monad (forM)
+import Data.Char (toLower)
+import Data.Functor.Identity
+
+-- | Generate fields using 'itemAssoc'.
+-- @'mkField' "foo bar"@ defines:
+--
+-- @
+-- foo :: FieldOptic "foo"
+-- foo = itemAssoc (Proxy :: Proxy "foo")
+-- bar :: FieldOptic "bar"
+-- bar = itemAssoc (Proxy :: Proxy "bar")
+-- @
+--
+mkField :: String -> DecsQ
+mkField str = fmap concat $ forM (words str) $ \s -> do
+  let st = litT (strTyLit s)
+  let lbl = conE 'Proxy `sigE` (conT ''Proxy `appT` st)
+  sequence [sigD (mkName s) $ conT ''FieldOptic `appT` st
+    , valD (varP (mkName s)) (normalB $ varE 'itemAssoc `appE` lbl) []
+    , return $ PragmaD $ InlineP (mkName s) Inline FunLike AllPhases
+    ]
+
+-- | Generate newtype wrappers and lenses from type synonyms.
+--
+-- @
+-- decFields [d|type Foo = Int|]
+-- @
+--
+-- Generates:
+--
+-- @
+-- newtype Foo = Foo Int
+-- foo :: (Foo ∈ xs) => Lens' (AllOf xs) Int
+-- foo = accessing Foo
+-- @
+--
+decFields :: DecsQ -> DecsQ
+decFields = decFieldsDeriving []
+
+-- | 'decFields' with additional deriving clauses
+decFieldsDeriving :: [Name] -> DecsQ -> DecsQ
+decFieldsDeriving drv' ds = ds >>= fmap concat . mapM mkBody
+  where
+    mkBody (NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) drv) = do
+      let name = let (x:xs) = nameBase name_ in mkName (toLower x : xs)
+          xs_ = mkName "xs"
+          f_ = mkName "f"
+          p_ = mkName "p"
+          q_ = mkName "q"
+          t_ = mkName "t"
+          ext = varT t_ `appT` conT ''Identity `appT` varT xs_
+          tvs' = PlainTV xs_ : PlainTV f_ : PlainTV p_ : PlainTV q_ : PlainTV t_ : tvs
+      sequence [return $ NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) (drv' ++ drv)
+
+        ,sigD name
+#if MIN_VERSION_template_haskell(2,10,0)
+          $ forallT tvs' (sequence [conT ''Member `appT` varT xs_ `appT` conT name_
+            , conT ''Extensible `appT` varT f_ `appT` varT p_ `appT` varT q_ `appT` varT t_])
+#else
+          $ forallT tvs' (sequence [classP ''Member [varT xs_, conT name_]
+            , classP ''Extensible [varT f_, varT p_, varT q_, varT t_]])
+#endif
+          $ arrowT
+            `appT` (varT p_ `appT` return ty `appT` (varT f_ `appT` return ty))
+            `appT` (varT q_ `appT` ext `appT` (varT f_ `appT` ext))
+
+        , valD (varP name) (normalB $ varE 'accessing `appE` conE nc) []
+        , return $ PragmaD $ InlineP name Inline FunLike AllPhases
+        ]
+    mkBody (TySynD name_ tvs ty) = mkBody (NewtypeD [] name_ tvs (NormalC (mkName (nameBase name_)) [(NotStrict, ty)]) [])
+    mkBody _ = fail "Unsupported declaration: genField handles newtype declarations or type synonyms"
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,5 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Union
@@ -11,17 +12,24 @@
 --
 -- Polymorphic open unions
 ------------------------------------------------------------------------
-module Data.Extensible.Union where
+module Data.Extensible.Union (K1(..), Union(..), Gondola(..), reunion, rung, runGondolas) where
 
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Class
 import Data.Extensible.Sum
 import Data.Extensible.Product
-import Data.Typeable
+import Data.Extensible.Wrapper
+import Data.Profunctor
+import Data.Typeable (Typeable)
 
 -- | Wrap a type that has a kind @* -> *@.
 newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
+
+instance Wrapper (K1 a) where
+  type Repr (K1 a) f = f a
+  _Wrapper = dimap getK1 (fmap K1)
+  {-# INLINE _Wrapper #-}
 
 newtype Union xs a = Union { getUnion :: K1 a :| xs }
 
diff --git a/src/Data/Extensible/Wrapper.hs b/src/Data/Extensible/Wrapper.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Wrapper.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# LANGUAGE TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Wrapper
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+module Data.Extensible.Wrapper (
+  Wrapper(..)
+  , _WrapperAs
+  , Const'(..)
+  , Comp(..)
+  , comp
+  ) where
+
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(..))
+import Data.Profunctor.Unsafe (Profunctor(..))
+import Data.Functor.Identity (Identity(..))
+import Data.Extensible.Internal.Rig (Optic', withIso)
+
+#if !MIN_VERSION_base(4,8,0)
+import Data.Monoid
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+#endif
+
+-- | The extensible data types should take @k -> *@ as a parameter.
+-- This class allows us to take a shortcut for direct representation.
+class Wrapper (h :: k -> *) where
+  -- | @'Repr' h v@ is the actual representation of @h v@.
+  type Repr h (v :: k) :: *
+
+  -- | This is an isomorphism between @h v@ and @'Repr' h v@.
+  --
+  -- @_Wrapper :: Iso' (h v) (Repr h v)@
+  --
+  _Wrapper :: (Functor f, Profunctor p) => Optic' p f (h v) (Repr h v)
+
+-- | Restricted version of '_Wrapper'.
+-- It is useful for eliminating ambiguousness.
+_WrapperAs :: (Functor f, Profunctor p, Wrapper h) => proxy v -> Optic' p f (h v) (Repr h v)
+_WrapperAs _ = _Wrapper
+{-# INLINE _WrapperAs #-}
+
+instance Wrapper Identity where
+  type Repr Identity a = a
+  _Wrapper = dimap runIdentity (fmap Identity)
+  {-# INLINE _Wrapper #-}
+
+-- | Poly-kinded composition
+newtype Comp (f :: j -> *) (g :: i -> j) (a :: i) = Comp { getComp :: f (g a) } deriving (Show, Eq, Ord, Typeable)
+
+comp :: Functor f => (a -> g b) -> f a -> Comp f g b
+comp f = Comp #. fmap f
+{-# INLINE comp #-}
+
+instance (Functor f, Wrapper g) => Wrapper (Comp f g) where
+  type Repr (Comp f g) x = f (Repr g x)
+  _Wrapper = withIso _Wrapper $ \f g -> dimap (fmap f .# getComp) (fmap (Comp #. fmap g))
+  {-# INLINE _Wrapper #-}
+
+-- | Poly-kinded Const
+newtype Const' a x = Const' { getConst' :: a } deriving (Show, Eq, Ord, Typeable)
+
+instance Wrapper (Const' a) where
+  type Repr (Const' a) b = a
+  _Wrapper = dimap getConst' (fmap Const')
+  {-# INLINE _Wrapper #-}
+
+instance Wrapper Proxy where
+  type Repr Proxy x = ()
+  _Wrapper = dimap (const ()) (fmap (const Proxy))
+  {-# INLINE _Wrapper #-}