diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,59 +1,59 @@
-dist
-cabal-dev
-*.o
-*.hi
-*.chi
-*.chs.h
-.virtualenv
-.hsenv
-.cabal-sandbox/
-cabal.sandbox.config
-cabal.config
-.stack-work
-
-# =========================
-# Operating System Files
-# =========================
-
-# OSX
-# =========================
-
-.DS_Store
-.AppleDouble
-.LSOverride
-
-# Thumbnails
-._*
-
-# Files that might appear on external disk
-.Spotlight-V100
-.Trashes
-
-# Directories potentially created on remote AFP share
-.AppleDB
-.AppleDesktop
-Network Trash Folder
-Temporary Items
-.apdisk
-
-# Windows
-# =========================
-
-# Windows image file caches
-Thumbs.db
-ehthumbs.db
-
-# Folder config file
-Desktop.ini
-
-# Recycle Bin used on file shares
-$RECYCLE.BIN/
-
-# Windows Installer files
-*.cab
-*.msi
-*.msm
-*.msp
-
-# Windows shortcuts
-*.lnk
+dist
+cabal-dev
+*.o
+*.hi
+*.chi
+*.chs.h
+.virtualenv
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+cabal.config
+.stack-work
+
+# =========================
+# Operating System Files
+# =========================
+
+# OSX
+# =========================
+
+.DS_Store
+.AppleDouble
+.LSOverride
+
+# Thumbnails
+._*
+
+# Files that might appear on external disk
+.Spotlight-V100
+.Trashes
+
+# Directories potentially created on remote AFP share
+.AppleDB
+.AppleDesktop
+Network Trash Folder
+Temporary Items
+.apdisk
+
+# Windows
+# =========================
+
+# Windows image file caches
+Thumbs.db
+ehthumbs.db
+
+# Folder config file
+Desktop.ini
+
+# Recycle Bin used on file shares
+$RECYCLE.BIN/
+
+# Windows Installer files
+*.cab
+*.msi
+*.msm
+*.msp
+
+# Windows shortcuts
+*.lnk
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,54 +1,79 @@
-# NB: don't set `language: haskell` here
+# This file has been generated -- see https://github.com/hvr/multi-ghc-travis
+language: c
+sudo: false
 
-# See also https://github.com/hvr/multi-ghc-travis for more information
+cache:
+  directories:
+    - $HOME/.cabsnap
+    - $HOME/.cabal/packages
 
-# The following lines enable several GHC versions and/or HP versions
-# to be tested; often it's enough to test only against the last
-# release of a major GHC version. Setting HPVER implictly sets
-# GHCVER. Omit lines with versions you don't need/want testing for.
-env:
- - CABALVER=1.22 GHCVER=7.10.1
+before_cache:
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.tar
 
-# Note: the distinction between `before_install` and `install` is not
-#       important.
+matrix:
+  include:
+    - env: CABALVER=1.22 GHCVER=7.10.3
+      compiler: ": #GHC 7.10.3"
+      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3], sources: [hvr-ghc]}}
+    - env: CABALVER=1.24 GHCVER=8.0.1
+      compiler: ": #GHC 8.0.1"
+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1], sources: [hvr-ghc]}}
+
 before_install:
- - travis_retry sudo add-apt-repository -y ppa:hvr/ghc
- - travis_retry sudo apt-get update
- - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER
+ - unset CC
  - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
 
 install:
  - cabal --version
  - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
- - travis_retry cabal update
- - cabal install --only-dependencies --enable-tests --enable-benchmarks
+ - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
+   then
+     zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
+          $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
+   fi
+ - travis_retry cabal update -v
+ - sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
+ - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt
+ - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
 
-# Here starts the actual work to be performed for the package under
-# test; any command which exits with a non-zero exit code causes the
-# build to fail.
-script:
- - if [ -f configure.ac ]; then autoreconf -i; fi
- # -v2 provides useful information for debugging
- - cabal configure --enable-tests --enable-benchmarks -v2
+# check whether current requested install-plan matches cached package-db snapshot
+ - if diff -u $HOME/.cabsnap/installplan.txt installplan.txt;
+   then
+     echo "cabal build-cache HIT";
+     rm -rfv .ghc;
+     cp -a $HOME/.cabsnap/ghc $HOME/.ghc;
+     cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;
+   else
+     echo "cabal build-cache MISS";
+     rm -rf $HOME/.cabsnap;
+     mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
+     cabal install --only-dependencies --enable-tests --enable-benchmarks;
+   fi
 
- # this builds all libraries and executables
- # (including tests/benchmarks)
- - cabal build
+# snapshot package-db on cache miss
+ - if [ ! -d $HOME/.cabsnap ];
+   then
+      echo "snapshotting package-db to build-cache";
+      mkdir $HOME/.cabsnap;
+      cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
+      cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;
+   fi
 
+# Here starts the actual work to be performed for the package under test;
+# any command which exits with a non-zero exit code causes the build to fail.
+script:
+ - if [ -f configure.ac ]; then autoreconf -i; fi
+ - cabal configure --enable-tests --enable-benchmarks -v2  # -v2 provides useful information for debugging
+ - cabal build   # this builds all libraries and executables (including tests/benchmarks)
  - cabal test
  - cabal check
-
- # tests that a source-distribution can be generated
- - cabal sdist
+ - cabal sdist   # tests that a source-distribution can be generated
 
- # check that the generated source-distribution can be built & installed
- - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;
-   cd dist/;
-   if [ -f "$SRC_TGZ" ]; then
-      cabal install --force-reinstalls "$SRC_TGZ";
-   else
-      echo "expected '$SRC_TGZ' not found";
-      exit 1;
-   fi
+# Check that the resulting source distribution can be built & installed.
+# If there are no other `.tar.gz` files in `dist`, this can be even simpler:
+# `cabal install --force-reinstalls dist/*-*.tar.gz`
+ - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&
+   (cd dist && cabal install --force-reinstalls "$SRC_TGZ")
 
 # EOF
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,26 @@
+0.4
+---------------------------------------------------
+* Added `Data.Extensible.Struct`
+* Changed the representation of `(:*)` to use `SmallArray`
+* Removed `(<:*)`. `hhead`, `htail`, `huncons`, `(*++*)`, `htrans`
+* New functions: `hfoldrWithIndex`, `hrepeat`, `hrepeatFor`, `haccumMap`,
+  `haccum`, `hpartition`, `henumerate`, `hlength`, `hcount`
+* Added various derived instances for `Field`
+* Added `liftField`, `liftField2`
+* Added `Wrapper` instances for `Maybe` and `[]`
+* Added `>:` as a synonym for `:>`
+* `Data.Extensible.Effect`
+  * Refined the API
+  * Added `Data.Extensible.Effect.Default`
+* Added `Data.Extensible.Tangle`
+* Added `record`
+* Type inference aids
+
+0.3.7.1
+----------------------------------------------------
+* `pieceAt` for `(:*)` is now index-preserving
+* Removed `sector`, `sectorAt`, `picked`
+
 0.3.7
 -----------------------------------------------------
 * Support GHC 8.0
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,30 +1,30 @@
-Copyright (c) 2015, Fumiaki Kinoshita
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-    * Redistributions of source code must retain the above copyright
-      notice, this list of conditions and the following disclaimer.
-
-    * Redistributions in binary form must reproduce the above
-      copyright notice, this list of conditions and the following
-      disclaimer in the documentation and/or other materials provided
-      with the distribution.
-
-    * Neither the name of Fumiaki Kinoshita nor the names of other
-      contributors may be used to endorse or promote products derived
-      from this software without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+Copyright (c) 2015, Fumiaki Kinoshita
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Fumiaki Kinoshita nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,2 @@
-import Distribution.Simple
-main = defaultMain
+import Distribution.Simple
+main = defaultMain
diff --git a/benchmarks/eff-comparison.hs b/benchmarks/eff-comparison.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/eff-comparison.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# OPTIONS_GHC -ddump-simpl -dsuppress-all #-}
+import Data.Void
+
+-- extensible-effects
+import qualified Control.Eff as ExtEff
+import qualified Control.Eff.Reader.Strict as ExtEff
+import qualified Control.Eff.Writer.Strict as ExtEff
+import qualified Control.Eff.State.Strict as ExtEff
+
+-- effin
+import qualified Control.Effect as Effin
+import qualified Control.Effect.Reader as Effin
+import qualified Control.Effect.Writer as Effin
+import qualified Control.Effect.State as Effin
+
+-- freer
+import qualified Control.Monad.Freer as Freer
+import qualified Control.Monad.Freer.Reader as Freer
+import qualified Control.Monad.Freer.Writer as Freer
+import qualified Control.Monad.Freer.State as Freer
+
+import Control.Monad.Reader
+import Control.Monad.State.Strict
+import Control.Monad.Writer.Strict
+import Control.Monad.RWS.Strict
+
+import Data.Extensible.Effect
+import Data.Extensible.Effect.Default
+
+import Criterion.Main
+
+testExtEff :: (ExtEff.Member (ExtEff.Reader Int) r
+  , ExtEff.Member (ExtEff.State Int) r
+  , ExtEff.Member (ExtEff.Writer (Sum Int)) r)
+  => ExtEff.Eff r ()
+testExtEff = replicateM_ 100 $ do
+  r :: Int <- ExtEff.ask
+  s <- ExtEff.get
+  ExtEff.tell (Sum s)
+  ExtEff.put $! s + r
+
+runExtEff :: ExtEff.Eff
+  ( ExtEff.Reader Int
+  ExtEff.:> ExtEff.State Int
+  ExtEff.:> ExtEff.Writer (Sum Int)
+  ExtEff.:> Void) a -> (Sum Int, (Int, a))
+runExtEff = ExtEff.run
+  . ExtEff.runMonoidWriter
+  . ExtEff.runState 0
+  . flip ExtEff.runReader 1
+
+testEffin :: (Effin.EffectReader Int l
+  , Effin.EffectState Int l
+  , Effin.EffectWriter (Sum Int) l)
+  => Effin.Effect l ()
+testEffin = replicateM_ 100 $ do
+  r <- Effin.ask
+  s <- Effin.get
+  Effin.tell (Sum s)
+  Effin.put $! s + r
+
+runEffin = Effin.runEffect
+  . Effin.runWriter
+  . Effin.runState 0
+  . Effin.runReader 1
+
+testFreer :: (Freer.Member (Freer.Reader Int) r
+  , Freer.Member (Freer.State Int) r
+  , Freer.Member (Freer.Writer (Sum Int)) r)
+  => Freer.Eff r ()
+testFreer = replicateM_ 100 $ do
+  r :: Int <- Freer.ask
+  s <- Freer.get
+  Freer.tell (Sum s)
+  Freer.put $! s + r
+
+runFreer :: Freer.Eff '[Freer.Reader Int, Freer.State Int, Freer.Writer (Sum Int)] a
+  -> ((a, Int), Sum Int)
+runFreer = Freer.run
+  . Freer.runWriter
+  . flip Freer.runState 0
+  . flip Freer.runReader 1
+
+testMTL :: (MonadReader Int m, MonadState Int m, MonadWriter (Sum Int) m)
+  => m ()
+testMTL = replicateM_ 100 $ do
+  r <- ask
+  s <- get
+  tell (Sum s)
+  put $! s + r
+
+runMTL :: ReaderT Int (StateT Int (Writer (Sum Int))) a -> ((a, Int), Sum Int)
+runMTL = runWriter
+  . flip runStateT 0
+  . flip runReaderT 1
+
+runExtensible :: Eff '[ReaderDef Int, StateDef Int, WriterDef (Sum Int)] a
+  -> ((a, Int), Sum Int)
+runExtensible = leaveEff
+  . runWriterDef
+  . flip runStateDef 0
+  . flip runReaderDef 1
+
+main = defaultMain
+  [ bgroup "rws"
+    [ bench "extensible" $ nf runExtensible testMTL
+    , bench "mtl" $ nf runMTL testMTL
+    , bench "mtl-RWS" $ nf (\m -> runRWS m 0 1) testMTL
+    , bench "exteff" $ nf runExtEff testExtEff
+    , bench "effin" $ nf runEffin testEffin
+    , bench "freer" $ nf runFreer testFreer
+    ]
+  ]
diff --git a/benchmarks/records.hs b/benchmarks/records.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/records.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators, DataKinds, FlexibleContexts #-}
+import Criterion.Main
+import Control.Lens
+import Data.Extensible
+import Data.Monoid
+
+mkField "foo bar baz qux foobar foobaz fooqux barfoo barbaz barqux"
+
+type Fields = ["foo" >: Sum Int
+  , "bar" >: String
+  , "baz" >: First Int
+  , "qux" >: String
+  , "foobar" >: (Sum Int, String)
+  , "foobaz" >: (Sum Int, First Int)
+  , "fooqux" >: (Sum Int, String)
+  , "barfoo" >: (String, Sum Int)
+  , "barbaz" >: (String, First Int)
+  , "barqux" >: (String, String)]
+
+recA :: Record Fields
+recA = foo @= Sum 1 <: bar @= "barA" <: baz @= mempty <: qux @= "qux"
+    <: foobar @= (Sum 1, "foobar")
+    <: foobaz @= (Sum 5, mempty)
+    <: fooqux @= (Sum 6, mempty)
+    <: barfoo @= mempty
+    <: barbaz @= mempty
+    <: barqux @= mempty
+    <: nil
+{-# NOINLINE recA #-}
+
+recB :: Record Fields
+recB = foo @= Sum 2 <: bar @= "barB" <: baz @= pure 42 <: qux @= "qux"
+  <: foobar @= (Sum 1, "foobar")
+  <: foobaz @= (Sum 5, mempty)
+  <: fooqux @= (Sum 7, mempty)
+  <: barfoo @= mempty
+  <: barbaz @= mempty
+  <: barqux @= mempty
+  <: nil
+{-# NOINLINE recB #-}
+
+data HsRec = HsRec { _hsFoo :: !(Sum Int), _hsBar :: !String, _hsBaz :: !(First Int)
+  , _hsQux :: !String
+  , _hsFooBar :: !(Sum Int, String)
+  , _hsFooBaz :: !(Sum Int, First Int)
+  , _hsFooQux :: !(Sum Int, String)
+  , _hsBarFoo :: !(String, Sum Int)
+  , _hsBarBaz :: !(String, First Int)
+  , _hsBarQux :: !(String, String)
+  }
+makeLenses ''HsRec
+
+hsRec = HsRec { _hsFoo = Sum 1, _hsBar = "hsBar"
+  , _hsBaz = mempty, _hsQux = "hsQux"
+  , _hsFooBar = (Sum 1, "foobar")
+  , _hsFooBaz = (Sum 5, mempty)
+  , _hsFooQux = (Sum 6, mempty)
+  , _hsBarFoo = mempty
+  , _hsBarBaz = mempty
+  , _hsBarQux = mempty
+  }
+
+main = defaultMain
+  [ bgroup "basic"
+    [ bench "view" $ whnf (view foo) recA
+    , bench "hsview" $ whnf (view hsFoo) hsRec
+    , bench "set" $ whnf (set foo 3) recB
+    , bench "hsset" $ whnf (set hsFoo 3) hsRec
+    ]
+  , bgroup "instances"
+    [ bench "mappend" $ whnf (uncurry mappend) (recA, recB)
+    , bench "==" $ whnf (uncurry (==)) $! (recA, recB)
+    , bench "compare" $ whnf (uncurry compare) (recA, recB)
+    , bench "show" $ nf show recA
+    ]
+  ]
diff --git a/examples/aeson.hs b/examples/aeson.hs
--- a/examples/aeson.hs
+++ b/examples/aeson.hs
@@ -1,16 +1,27 @@
-{-# 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)
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+import Data.Aeson hiding (KeyValue)
+import Data.Constraint
+import Data.Extensible
+import Data.Monoid
 import Data.Proxy
 import Data.String (fromString)
+import GHC.TypeLits (KnownSymbol, symbolVal)
 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
+    $ \m -> let k = symbolVal (proxyAssocKey m) in case HM.lookup (fromString k) v of
       Just a -> Field <$> return <$> parseJSON a
       Nothing -> fail $ "Missing key: " ++ k
+
+instance Forall (KeyValue KnownSymbol ToJSON) xs => ToJSON (Record xs) where
+  toJSON rec = Object $ HM.fromList $ flip appEndo [] $ hfoldMap getConst'
+    $ hzipWith (\(Comp Dict) v -> Const' $ Endo
+      ((fromString $ symbolVal $ proxyAssocKey v, toJSON $ getField v):))
+    (library :: Comp Dict (KeyValue KnownSymbol ToJSON) :* xs) rec
diff --git a/examples/effect.hs b/examples/effect.hs
--- a/examples/effect.hs
+++ b/examples/effect.hs
@@ -1,20 +1,48 @@
 {-# LANGUAGE TemplateHaskell, DataKinds, FlexibleContexts #-}
 import Data.Extensible
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Writer.Strict
+import Control.Monad.Skeleton
 
-decEffects [d|
-  data Example x where -- the name doesn't matter
-    Foo :: Int -> Example ()
-    Bar :: Example String
-    Baz :: Bool -> Bool -> Example Int
+decEffectSuite [d|
+  data Example x where
+    Reset :: Int -> Example ()
+    PrintString :: String -> Example ()
+    Hello :: Example ()
+    Count :: Example Int
     |]
 
-mkField "Foo Bar Baz"
+mkField "Reset PrintString Hello Count"
 
-test :: (Associate "Foo" (Action '[Int] ()) xs
-  , Associate "Bar" (Action '[] String) xs
-  , Associate "Baz" (Action '[Bool, Bool] Int) xs) => Eff xs Int
+test :: IncludeAssoc xs Example => Eff xs ()
 test = do
-  foo 42
-  s <- bar
-  t <- bar
-  baz (s == "bar") (s == t)
+  hello
+  hello
+  n <- count
+  printString (show n)
+  reset 0
+  n' <- count
+  printString (show n')
+
+-- | Object-like stateful handler
+newtype Methods xs m = Methods
+  { getMethods :: RecordOf (Interpreter (WriterT (Methods xs m) m)) xs }
+
+runMethods :: Monad m => Methods xs m -> Eff xs a -> m (a, Methods xs m)
+runMethods rec eff = case handleEff (getMethods rec) eff of
+  Return a -> return (a, rec)
+  m :>>= k -> do
+    (a, rec') <- runWriterT m
+    runMethods rec' (k a)
+
+example :: Int -> Methods Example IO
+example n = Methods
+  $ _Reset @!? do \n' -> writer ((), example n')
+  <: _PrintString @!? do \str -> WriterT $ ((), example n) <$ putStrLn str
+  <: _Hello @!? do WriterT $ ((), example $ n + 1) <$ putStrLn "Hello!"
+  <: _Count @!? do writer (n, example n)
+  <: nil
+
+takePrintString :: MonadIO (Eff xs) => Eff (PrintString ': xs) a -> Eff xs a
+takePrintString = peelAction rebindEff0 return
+  $ \str cont -> liftIO (putStrLn str) >>= cont
diff --git a/examples/records.hs b/examples/records.hs
--- a/examples/records.hs
+++ b/examples/records.hs
@@ -5,12 +5,12 @@
 mkField "name weight price description featured quantity"
 
 type Stock c = Record '[
-    "name" :> String
-  , "weight" :> Float
-  , "price" :> c
-  , "featured" :> Bool
-  , "description" :> String
-  , "quantity" :> Int]
+    "name" >: String
+  , "weight" >: Float
+  , "price" >: c
+  , "featured" >: Bool
+  , "description" >: String
+  , "quantity" >: Int]
 
 s0 :: Num c => Stock c
 s0 = name @= "DA-192H"
@@ -19,7 +19,7 @@
   <: featured @= True
   <: description @= "High-quality (24bit 192kHz), lightweight portable DAC"
   <: quantity @= 20
-  <: Nil
+  <: emptyRecord
 
 -- Use shrinkAssoc to permute elements
 s1 :: Num c => Stock c
@@ -30,7 +30,7 @@
   <: price @= 330
   <: quantity @= 55
   <: weight @= 200
-  <: Nil
+  <: emptyRecord
 
 -- If "quantity" is missing,
 --    Couldn't match type ‘Missing "quantity"’ with ‘Expecting one’
diff --git a/examples/tangle.hs b/examples/tangle.hs
new file mode 100644
--- /dev/null
+++ b/examples/tangle.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE TemplateHaskell, DataKinds #-}
+import Control.Monad.Trans.Class
+import Data.Extensible
+import Data.Functor.Identity
+import Data.Proxy
+
+mkField "foo bar baz"
+
+type Rec = ["foo" :> String, "bar" :> Int, "baz" :> Double, "qux" :> Bool]
+
+class MakeRec kv where
+  make :: proxy kv -> TangleT (Field Identity) Rec IO (AssocValue kv)
+
+instance MakeRec ("foo" :> String) where
+  make _ = lift getLine
+
+instance MakeRec ("bar" :> Int) where
+  make _ = lift $ length <$> getLine
+
+instance MakeRec ("baz" :> Double) where
+  make _ = lift readLn
+
+instance MakeRec ("qux" :> Bool) where
+  make _ = do
+    str <- lasso foo
+    x <- lasso baz
+    return $ str == show x
+
+makeRec :: IO (Record Rec)
+makeRec = runTangles
+  (htabulateFor (Proxy :: Proxy MakeRec)
+    $ \m -> Comp $ Field . pure <$> make m)
+  (wrench Nil)
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,17 +1,18 @@
 name:                extensible
-version:             0.3.7
-synopsis:            Extensible, efficient, optics-friendly data types
+version:             0.4
+synopsis:            Extensible, efficient, optics-friendly data types and effects
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
-description:         Poly-kinded extensible records and variants
+description:         Poly-kinded extensible records, variants, effects, tangles
 license:             BSD3
 license-file:        LICENSE
 author:              Fumiaki Kinoshita
 maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
-copyright:           Copyright (C) 2016 Fumiaki Kinoshita
-category:            Data, Records
+copyright:           Copyright (c) 2017 Fumiaki Kinoshita
+category:            Data, Records, Monads
 build-type:          Simple
 stability:           experimental
+Tested-With:         GHC == 7.10.3, GHC == 8.0.1
 
 extra-source-files:
   examples/*.hs
@@ -32,15 +33,20 @@
     Data.Extensible.Dictionary
     Data.Extensible.Field
     Data.Extensible.Effect
+    Data.Extensible.Effect.Default
+    Data.Extensible.HList
     Data.Extensible.Inclusion
     Data.Extensible.Internal
     Data.Extensible.Internal.Rig
+    Data.Extensible.Label
     Data.Extensible.Match
     Data.Extensible.Nullable
     Data.Extensible.Plain
     Data.Extensible.Product
     Data.Extensible.Record
+    Data.Extensible.Struct
     Data.Extensible.Sum
+    Data.Extensible.Tangle
     Data.Extensible.Wrapper
     Data.Extensible.TH
   default-extensions: TypeOperators
@@ -57,10 +63,36 @@
   build-depends:       base >= 4.7 && <5
     , template-haskell
     , constraints
+    , ghc-prim
+    , primitive
     , profunctors
+    , semigroups
+    , comonad
+    , deepseq
     , tagged
     , transformers
+    , mtl
     , monad-skeleton >= 0.1.2
   hs-source-dirs:      src
   ghc-options: -Wall
   default-language:    Haskell2010
+
+test-suite effects
+  type: exitcode-stdio-1.0
+  main-is: effects.hs
+  build-depends: base, extensible
+  hs-source-dirs: tests
+
+benchmark records
+  type:           exitcode-stdio-1.0
+  main-is:        records.hs
+  ghc-options:    -O2
+  hs-source-dirs: benchmarks
+  build-depends: base, lens, criterion, extensible
+
+benchmark eff-comparison
+  type:           exitcode-stdio-1.0
+  main-is:        eff-comparison.hs
+  ghc-options:    -O2
+  hs-source-dirs: benchmarks
+  build-depends: base, criterion, extensible, extensible-effects, effin, freer, mtl
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -1,12 +1,10 @@
 ----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 -- This module just reexports everything.
 -----------------------------------------------------------------------------
@@ -16,12 +14,14 @@
   , module Data.Extensible.Effect
   , module Data.Extensible.Field
   , module Data.Extensible.Inclusion
+  , module Data.Extensible.Label
   , module Data.Extensible.Match
   , module Data.Extensible.Nullable
   , module Data.Extensible.Plain
   , module Data.Extensible.Product
   , module Data.Extensible.Record
   , module Data.Extensible.Sum
+  , module Data.Extensible.Tangle
   , module Data.Extensible.TH
   , module Data.Extensible.Wrapper
   ) where
@@ -31,11 +31,13 @@
 import Data.Extensible.Field
 import Data.Extensible.Effect
 import Data.Extensible.Inclusion
+import Data.Extensible.Label
 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.Tangle
 import Data.Extensible.TH
 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,13 +1,14 @@
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables, TypeFamilies #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE UndecidableSuperClasses #-}
+#endif
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Class
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  MPTCs
 --
 -----------------------------------------------------------------------------
 module Data.Extensible.Class (
@@ -30,14 +31,25 @@
   , (∈)()
 #endif
   , FindType
+  -- * Generation
+  , Generate(..)
+  , Forall(..)
+  , ForallF
   -- * Association
   , Assoc(..)
+#if __GLASGOW_HASKELL__ >= 800
+  , type (>:)
+#else
+  , (>:)()
+#endif
   , Associate(..)
   , FindAssoc
   -- * Sugar
   , Elaborate
   , Elaborated(..)
   ) where
+import Data.Constraint
+import Data.Extensible.HList
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig (Optic')
 import Data.Extensible.Wrapper
@@ -57,14 +69,17 @@
 pieceAssoc = pieceAt association
 {-# INLINE pieceAssoc #-}
 
+-- | Access a specified element through a wrapper.
 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 #-}
 
+-- | Access an element through a wrapper.
 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 #-}
 
+-- | Access an element specified by the key type through a wrapper.
 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)
@@ -73,3 +88,62 @@
 proxyKey :: proxy k -> Proxy (k ':> v)
 proxyKey _ = Proxy
 {-# INLINE proxyKey #-}
+
+-- | Every type-level list is an instance of 'Generate'.
+class Generate (xs :: [k]) where
+  -- | Enumerate all possible 'Membership's of @xs@.
+  henumerate :: (forall x. Membership xs x -> r -> r) -> r -> r
+
+  -- | Count the number of memberships.
+  hcount :: proxy xs -> Int
+
+  -- | Enumerate 'Membership's and construct an 'HList'.
+  hgenerateList :: Applicative f
+    => (forall x. Membership xs x -> f (h x)) -> f (HList h xs)
+
+instance Generate '[] where
+  henumerate _ r = r
+  {-# INLINE henumerate #-}
+
+  hcount _ = 0
+  {-# INLINE hcount #-}
+
+  hgenerateList _ = pure HNil
+  {-# INLINE hgenerateList #-}
+
+instance Generate xs => Generate (x ': xs) where
+  henumerate f r = f here $ henumerate (f . navNext) r
+  {-# INLINE henumerate #-}
+
+  hcount _ = 1 + hcount (Proxy :: Proxy xs)
+  {-# INLINE hcount #-}
+
+  -- | Enumerate 'Membership's and construct an 'HList'.
+  hgenerateList f = HCons <$> f here <*> hgenerateList (f . navNext)
+  {-# INLINE hgenerateList #-}
+
+-- | Every element in @xs@ satisfies @c@
+class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where
+  -- | Enumerate all possible 'Membership's of @xs@ with an additional context.
+  henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r
+
+  hgenerateListFor :: Applicative f
+    => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs)
+
+instance Forall c '[] where
+  henumerateFor _ _ _ r = r
+  {-# INLINE henumerateFor #-}
+
+  hgenerateListFor _ _ = pure HNil
+  {-# INLINE hgenerateListFor #-}
+
+instance (c x, Forall c xs) => Forall c (x ': xs) where
+  henumerateFor p _ f r = f here $ henumerateFor p (Proxy :: Proxy xs) (f . navNext) r
+  {-# INLINE henumerateFor #-}
+
+  hgenerateListFor p f = HCons <$> f here <*> hgenerateListFor p (f . navNext)
+  {-# INLINE hgenerateListFor #-}
+
+type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
+  ForallF c '[] = ()
+  ForallF c (x ': xs) = (c x, Forall c xs)
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
@@ -8,18 +8,15 @@
 -----------------------------------------------------------------------
 --
 -- Module      :  Data.Extensible.Dictionary
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 -- Reification of constraints using extensible data types.
 -- Also includes orphan instances.
 -----------------------------------------------------------------------
 module Data.Extensible.Dictionary (library, WrapForall, Instance1) where
-import Data.Monoid
 import Data.Extensible.Class
 import Data.Extensible.Product
 import Data.Extensible.Sum
@@ -27,46 +24,33 @@
 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)
+library = hrepeatFor (Proxy :: Proxy c) $ 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")
-    . foldr (.) id
-    . getMerged
-    . hfoldMap getConst'
-    . hzipWith (\(Comp Dict) h -> Const' $ MergeList [showsPrec 0 h . showString " <: "]) (library :: Comp Dict (Instance1 Show h) :* xs)
+  showsPrec d xs = showParen (d > 0)
+    $ henumerateFor (Proxy :: Proxy (Instance1 Show h)) xs
+    (\i r -> showsPrec 0 (hlookup i xs) . showString " <: " . r)
+    (showString "nil")
 
 instance WrapForall Eq h xs => Eq (h :* xs) where
-  xs == ys = getAll $ hfoldMap (All #. getConst')
-    $ hzipWith3 (\(Comp Dict) x y -> Const' $ x == y) (library :: Comp Dict (Instance1 Eq h) :* xs) xs ys
+  xs == ys = henumerateFor (Proxy :: Proxy (Instance1 Eq h)) xs
+    (\i r -> hlookup i xs == hlookup i ys && r) True
   {-# INLINE (==) #-}
 
 instance (Eq (h :* xs), WrapForall Ord h xs) => Ord (h :* xs) where
-  compare xs ys = hfoldMap getConst'
-    $ hzipWith3 (\(Comp Dict) x y -> Const' $ compare x y) (library :: Comp Dict (Instance1 Ord h) :* xs) xs ys
+  compare xs ys = henumerateFor (Proxy :: Proxy (Instance1 Ord h)) xs
+    (\i r -> (hlookup i xs `compare` hlookup i ys) `mappend` r) mempty
   {-# INLINE compare #-}
 
 instance WrapForall Monoid h xs => Monoid (h :* xs) where
-  mempty = hmap (\(Comp Dict) -> mempty) (library :: Comp Dict (Instance1 Monoid h) :* xs)
+  mempty = hrepeatFor (Proxy :: Proxy (Instance1 Monoid h)) mempty
   {-# INLINE mempty #-}
-  mappend xs ys = hzipWith3 (\(Comp Dict) -> mappend) (library :: Comp Dict (Instance1 Monoid h) :* xs) xs ys
+  mappend = hzipWith3 (\(Comp Dict) -> mappend)
+    (library :: Comp Dict (Instance1 Monoid h) :* xs)
   {-# INLINE mappend #-}
 
 instance WrapForall Show h xs => Show (h :| xs) where
diff --git a/src/Data/Extensible/Effect.hs b/src/Data/Extensible/Effect.hs
--- a/src/Data/Extensible/Effect.hs
+++ b/src/Data/Extensible/Effect.hs
@@ -1,95 +1,373 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
-module Data.Extensible.Effect (Instruction(..)
-  , Eff
-  , liftEff
-  , hoistEff
-  , handleWith
-  , Handler(..)
-  -- * Unnamed actions
-  , Action(..)
-  , Function
-  , receive
-  -- * Successive handling
-  , (!-!!)
-  , squash
-  , nihility) where
-
-import Control.Monad.Skeleton
-import Data.Extensible.Field
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Data.Extensible.Class
-import Data.Profunctor.Unsafe -- Trustworthy since 7.8
-
--- | Unnamed action
-data Action (args :: [*]) a r where
-  AResult :: Action '[] a a
-  AArgument :: x -> Action xs a r -> Action (x ': xs) a r
-
-type family Function args r :: * where
-  Function '[] r = r
-  Function (x ': xs) r = x -> Function xs r
-
--- | Transformation between effects
-newtype Handler f g = Handler { runHandler :: forall a. g a -> f a }
-
-receive :: Functor f => Function xs (f a) -> Handler f (Action xs a)
-receive f0 = Handler (go f0) where
-  go :: Functor f => Function xs (f a) -> Action xs a r -> f r
-  go r AResult = r
-  go f (AArgument x a) = go (f x) a
-
-----------------------------------------------
-
--- | A unit of effects
-data Instruction (xs :: [Assoc k (* -> *)]) a where
-  Instruction :: !(Membership xs kv) -> AssocValue kv a -> Instruction xs a
-
--- | The extensible operational monad
-type Eff xs = Skeleton (Instruction xs)
-
--- | Lift some effect to 'Eff'
-liftEff :: forall proxy s t xs a. Associate s t xs => proxy s -> t a -> Eff xs a
-liftEff _ x = bone (Instruction (association :: Membership xs (s ':> t)) x)
-{-# INLINE liftEff #-}
-
-hoistEff :: forall proxy s t xs a. Associate s t xs => proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a
-hoistEff _ f = hoistSkeleton $ \(Instruction i t) -> case compareMembership (association :: Membership xs (s ':> t)) i of
-  Right Refl -> Instruction i (f t)
-  _ -> Instruction i t
-{-# INLINABLE hoistEff #-}
-
-handleWith :: RecordOf (Handler m) xs -> Eff xs a -> MonadView m (Eff xs) a
-handleWith hs m = case unbone m of
-  Instruction i t :>>= k -> views (pieceAt i) (runHandler .# getField) hs t :>>= k
-  Return a -> Return a
-{-# INLINABLE handleWith #-}
-
-(!-!!) :: Monad m => (forall x. t x -> m x)
-  -> (forall x. Eff xs x -> m x)
-  -> Eff ((s ':> t) ': xs) a -> m a
-f !-!! g = go where
-  go m = case unbone m of
-    Return a -> return a
-    Instruction i t :>>= k -> runMembership i
-      (\Refl -> f t >>= go . k)
-      (\j -> g (bone (Instruction j t)) >>= go . k)
-{-# INLINE (!-!!) #-}
-infixr 0 !-!!
-
-nihility :: Monad m => Eff '[] a -> m a
-nihility m = case unbone m of
-  Return a -> return a
-  Instruction i _ :>>= _ -> impossibleMembership i
-
--- | @'squash' = ('!-!!' 'id')@
-squash :: (forall x. t x -> Eff xs x) -> Eff ((s ':> t) ': xs) a -> Eff xs a
-squash f = go where
-  go m = case unbone m of
-    Return a -> return a
-    Instruction i t :>>= k -> runMembership i
-      (\Refl -> f t >>= go . k)
-      (\j -> boned $ Instruction j t :>>= go . k)
-{-# INLINE squash #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Effect
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Name-based extensible effects
+-----------------------------------------------------------------------------
+module Data.Extensible.Effect (
+  -- * Base
+  Instruction(..)
+  , Eff
+  , liftEff
+  , liftsEff
+  , hoistEff
+  -- * Step-wise handling
+  , Interpreter(..)
+  , handleEff
+  -- * Peeling
+  , peelEff
+  , Rebinder
+  , rebindEff0
+  , rebindEff1
+  , rebindEff2
+  , leaveEff
+  , retractEff
+  -- * Anonymous actions
+  , Action(..)
+  , Function
+  , runAction
+  , (@!?)
+  , peelAction
+  -- * transformers-compatible actions and handlers
+  -- ** Reader
+  , ReaderEff
+  , askEff
+  , asksEff
+  , localEff
+  , runReaderEff
+  -- ** State
+  , State
+  , getEff
+  , getsEff
+  , putEff
+  , modifyEff
+  , stateEff
+  , runStateEff
+  -- ** Writer
+  , WriterEff
+  , writerEff
+  , tellEff
+  , listenEff
+  , passEff
+  , runWriterEff
+  -- ** Maybe
+  , MaybeEff
+  , runMaybeEff
+  -- ** Either
+  , EitherEff
+  , throwEff
+  , catchEff
+  , runEitherEff
+  -- ** Iter
+  , Identity
+  , tickEff
+  , runIterEff
+  ) where
+
+import Control.Applicative
+import Control.Monad.Skeleton
+import Control.Monad.Trans.State.Strict
+import Data.Extensible.Field
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+import Data.Extensible.Class
+import Data.Functor.Identity
+import Data.Profunctor.Unsafe -- Trustworthy since 7.8
+
+-- | A unit of named effects.
+data Instruction (xs :: [Assoc k (* -> *)]) a where
+  Instruction :: !(Membership xs kv) -> AssocValue kv a -> Instruction xs a
+
+-- | The extensible operational monad
+type Eff xs = Skeleton (Instruction xs)
+
+-- | Lift an instruction onto an 'Eff' action.
+liftEff :: forall s t xs a. Associate s t xs => Proxy s -> t a -> Eff xs a
+liftEff p x = liftsEff p x id
+{-# INLINE liftEff #-}
+
+-- | Lift an instruction onto an 'Eff' action and apply a function to the result.
+liftsEff :: forall s t xs a r. Associate s t xs
+  => Proxy s -> t a -> (a -> r) -> Eff xs r
+liftsEff _ x k = boned
+  $ Instruction (association :: Membership xs (s ':> t)) x :>>= return . k
+{-# INLINE liftsEff #-}
+
+-- | Censor a specific type of effects in an action.
+hoistEff :: forall s t xs a. Associate s t xs => Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a
+hoistEff _ f = hoistSkeleton $ \(Instruction i t) -> case compareMembership (association :: Membership xs (s ':> t)) i of
+  Right Refl -> Instruction i (f t)
+  _ -> Instruction i t
+{-# INLINABLE hoistEff #-}
+
+-- | Build a relay-style handler from a triple of functions.
+--
+-- @
+-- runStateEff = peelEff rebindEff1 (\a s -> return (a, s))
+--   (\m k s -> let (a, s') = runState m s in k a s')
+-- @
+--
+peelEff :: forall k t xs a r
+  . Rebinder xs r -- ^ Re-bind an unrelated action
+  -> (a -> r) -- ^ return the result
+  -> (forall x. t x -> (x -> r) -> r) -- ^ Handle the foremost type of an action
+  -> Eff (k >: t ': xs) a -> r
+peelEff pass ret wrap = go where
+  go m = case debone m of
+    Return a -> ret a
+    Instruction i t :>>= k -> runMembership i
+      (\Refl -> wrap t (go . k))
+      (\j -> pass (Instruction j t) (go . k))
+{-# INLINE peelEff #-}
+
+-- | A function to bind an 'Instruction' in 'peelEff'.
+type Rebinder xs r = forall x. Instruction xs x -> (x -> r) -> r
+
+-- | A common value for the second argument of 'peelEff'. Binds an instruction
+-- directly.
+rebindEff0 :: Rebinder xs (Eff xs r)
+rebindEff0 i k = boned (i :>>= k)
+
+-- | A pre-defined value for the second argument of 'peelEff'.
+-- Preserves the argument of the continuation.
+rebindEff1 :: Rebinder xs (a -> Eff xs r)
+rebindEff1 i k a = boned (i :>>= flip k a)
+
+-- | A pre-defined value for the second argument of 'peelEff'.
+-- Preserves two arguments of the continuation.
+rebindEff2 :: Rebinder xs (a -> b -> Eff xs r)
+rebindEff2 i k a b = boned (i :>>= \x -> k x a b)
+
+-- | Reveal the final result of 'Eff'.
+leaveEff :: Eff '[] a -> a
+leaveEff m = case debone m of
+  Return a -> a
+  _ -> error "Impossible"
+
+-- | Tear down an action using the 'Monad' instance of the instruction.
+retractEff :: forall k m a. Monad m => Eff '[k >: m] a -> m a
+retractEff m = case debone m of
+  Return a -> return a
+  Instruction i t :>>= k -> runMembership i
+    (\Refl -> t >>= retractEff . k)
+    (error "Impossible")
+
+-- | Transformation between effects
+newtype Interpreter f g = Interpreter { runInterpreter :: forall a. g a -> f a }
+
+-- | Process an 'Eff' action using a record of 'Interpreter's.
+handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a
+handleEff hs m = case debone m of
+  Instruction i t :>>= k -> views (pieceAt i) (runInterpreter .# getField) hs t :>>= k
+  Return a -> Return a
+
+-- | Anonymous representation of instructions.
+data Action (args :: [*]) a r where
+  AResult :: Action '[] a a
+  AArgument :: x -> Action xs a r -> Action (x ': xs) a r
+
+-- | @'Function' [a, b, c] r@ is @a -> b -> c -> r@
+type family Function args r :: * where
+  Function '[] r = r
+  Function (x ': xs) r = x -> Function xs r
+
+-- | Pass the arguments of 'Action' to the supplied function.
+runAction :: Function xs (f a) -> Action xs a r -> f r
+runAction r AResult = r
+runAction f (AArgument x a) = runAction (f x) a
+
+-- | Create a 'Field' of a 'Interpreter' for an 'Action'.
+(@!?) :: FieldName k -> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a)
+_ @!? f = Field $ Interpreter (runAction f)
+infix 1 @!?
+
+-- | Specialised version of 'peelEff' for 'Action's.
+-- You can pass a function @a -> b -> ... -> (q -> r) -> r@ as a handler for
+-- @'Action' '[a, b, ...] q@.
+peelAction :: forall k ps q xs a r
+  . (forall x. Instruction xs x -> (x -> r) -> r) -- ^ Re-bind an unrelated action
+  -> (a -> r) -- ^ return the result
+  -> Function ps ((q -> r) -> r) -- ^ Handle the foremost action
+  -> Eff (k >: Action ps q ': xs) a -> r
+peelAction pass ret wrap = go where
+  go m = case debone m of
+    Return a -> ret a
+    Instruction i t :>>= k -> runMembership i
+      (\Refl -> case t of
+        (_ :: Action ps q x) ->
+          let run :: forall t. Function t ((q -> r) -> r) -> Action t q x -> r
+              run f AResult = f (go . k)
+              run f (AArgument x a) = run (f x) a
+          in run wrap t)
+      (\j -> pass (Instruction j t) (go . k))
+{-# INLINE peelAction #-}
+
+-- | The reader monad is characterised by a type equality between the result
+-- type and the enviroment type.
+type ReaderEff = (:~:)
+
+-- | Fetch the environment.
+askEff :: forall k r xs. Associate k (ReaderEff r) xs
+  => Proxy k -> Eff xs r
+askEff p = liftEff p Refl
+{-# INLINE askEff #-}
+
+-- | Pass the environment to a function.
+asksEff :: forall k r xs a. Associate k (ReaderEff r) xs
+  => Proxy k -> (r -> a) -> Eff xs a
+asksEff p = liftsEff p Refl
+{-# INLINE asksEff #-}
+
+-- | Modify the enviroment locally.
+localEff :: forall k r xs a. Associate k (ReaderEff r) xs
+  => Proxy k -> (r -> r) -> Eff xs a -> Eff xs a
+localEff _ f = go where
+  go m = case debone m of
+    Return a -> return a
+    Instruction i t :>>= k -> case compareMembership
+      (association :: Membership xs (k >: ReaderEff r)) i of
+        Left _ -> boned $ Instruction i t :>>= go . k
+        Right Refl -> case t of
+          Refl -> boned $ Instruction i t :>>= go . k . f
+{-# INLINE localEff #-}
+
+-- | Run the frontal reader effect.
+runReaderEff :: forall k r xs a. Eff (k >: ReaderEff r ': xs) a -> r -> Eff xs a
+runReaderEff m r = peelEff rebindEff0 return (\Refl k -> k r) m
+{-# INLINE runReaderEff #-}
+
+-- | Get the current state.
+getEff :: forall k s xs. Associate k (State s) xs
+  => Proxy k -> Eff xs s
+getEff k = liftEff k get
+{-# INLINE getEff #-}
+
+-- | Pass the current state to a function.
+getsEff :: forall k s a xs. Associate k (State s) xs
+  => Proxy k -> (s -> a) -> Eff xs a
+getsEff k = liftsEff k get
+{-# INLINE getsEff #-}
+
+-- | Replace the state with a new value.
+putEff :: forall k s xs. Associate k (State s) xs
+  => Proxy k -> s -> Eff xs ()
+putEff k = liftEff k . put
+{-# INLINE putEff #-}
+
+-- | Modify the state.
+modifyEff :: forall k s xs. Associate k (State s) xs
+  => Proxy k -> (s -> s) -> Eff xs ()
+modifyEff k f = liftEff k $ state $ \s -> ((), f s)
+{-# INLINE modifyEff #-}
+
+-- | Lift a state modification function.
+stateEff :: forall k s xs a. Associate k (State s) xs
+  => Proxy k -> (s -> (a, s)) -> Eff xs a
+stateEff k = liftEff k . state
+{-# INLINE stateEff #-}
+
+-- | Run the frontal state effect.
+runStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs (a, s)
+runStateEff = peelEff rebindEff1 (\a s -> return (a, s))
+  (\m k s -> let (a, s') = runState m s in k a $! s')
+{-# INLINE runStateEff #-}
+
+-- | @(,)@ already is a writer monad.
+type WriterEff w = (,) w
+
+-- | Write the second element and return the first element.
+writerEff :: forall k w xs a. (Associate k (WriterEff w) xs)
+  => Proxy k -> (a, w) -> Eff xs a
+writerEff k (a, w) = liftEff k (w, a)
+{-# INLINE writerEff #-}
+
+-- | Write a value.
+tellEff :: forall k w xs. (Associate k (WriterEff w) xs)
+  => Proxy k -> w -> Eff xs ()
+tellEff k w = liftEff k (w, ())
+{-# INLINE tellEff #-}
+
+-- | Squash the outputs into one step and return it.
+listenEff :: forall k w xs a. (Associate k (WriterEff w) xs, Monoid w)
+  => Proxy k -> Eff xs a -> Eff xs (a, w)
+listenEff p = go mempty where
+  go w m = case debone m of
+    Return a -> writerEff p ((a, w), w)
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> (,) w)) i of
+      Left _ -> boned $ Instruction i t :>>= go w . k
+      Right Refl -> let (w', a) = t
+                        !w'' = mappend w w' in go w'' (k a)
+{-# INLINE listenEff #-}
+
+-- | Modify the output using the function in the result.
+passEff :: forall k w xs a. (Associate k (WriterEff w) xs, Monoid w)
+  => Proxy k -> Eff xs (a, w -> w) -> Eff xs a
+passEff p = go mempty where
+  go w m = case debone m of
+    Return (a, f) -> writerEff p (a, f w)
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> (,) w)) i of
+      Left _ -> boned $ Instruction i t :>>= go w . k
+      Right Refl -> let (w', a) = t
+                        !w'' = mappend w w' in go w'' (k a)
+{-# INLINE passEff #-}
+
+-- | Run the frontal writer effect.
+runWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs (a, w)
+runWriterEff = peelEff rebindEff1 (\a w -> return (a, w))
+  (\(w', a) k w -> k a $! mappend w w') `flip` mempty
+{-# INLINE runWriterEff #-}
+
+-- | An effect with no result
+type MaybeEff = Const ()
+
+-- | Run an effect which may fail in the name of @k@.
+runMaybeEff :: forall k xs a. Eff (k >: MaybeEff ': xs) a -> Eff xs (Maybe a)
+runMaybeEff = peelEff rebindEff0 (return . Just)
+  (\_ _ -> return Nothing)
+{-# INLINE runMaybeEff #-}
+
+-- | Throwing an exception
+type EitherEff = Const
+
+-- | Throw an exception @e@, throwing the rest of the computation away.
+throwEff :: Associate k (EitherEff e) xs => Proxy k -> e -> Eff xs a
+throwEff k = liftEff k . Const
+{-# INLINE throwEff #-}
+
+-- | Attach a handler for an exception.
+catchEff :: forall k e xs a. (Associate k (EitherEff e) xs)
+  => Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a
+catchEff _ m0 handler = go m0 where
+  go m = case debone m of
+    Return a -> return a
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> Const e)) i of
+      Left _ -> boned $ Instruction i t :>>= go . k
+      Right Refl -> handler (getConst t)
+{-# INLINE catchEff #-}
+
+-- | Run the frontal Either effect.
+runEitherEff :: forall k e xs a. Eff (k >: EitherEff e ': xs) a -> Eff xs (Either e a)
+runEitherEff = peelEff rebindEff0 (return . Right)
+  (\(Const e) _ -> return $ Left e)
+{-# INLINE runEitherEff #-}
+
+-- | Put a milestone on a computation.
+tickEff :: Associate k Identity xs => Proxy k -> Eff xs ()
+tickEff k = liftEff k (Identity ())
+{-# INLINE tickEff #-}
+
+-- | Run a computation until 'tickEff'.
+runIterEff :: Eff (k >: Identity ': xs) a
+  -> Eff xs (Either a (Eff (k >: Identity ': xs) a))
+runIterEff m = case debone m of
+  Return a -> return (Left a)
+  Instruction i t :>>= k -> runMembership i
+    (\Refl -> return $ Right $ k $ runIdentity t)
+    (\j -> boned $ Instruction j t :>>= runIterEff . k)
diff --git a/src/Data/Extensible/Effect/Default.hs b/src/Data/Extensible/Effect/Default.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Effect/Default.hs
@@ -0,0 +1,107 @@
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Effect.Default
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Default monad runners and 'MonadIO', 'MonadReader', 'MonadWriter',
+-- 'MonadState', 'MonadError' instances
+-----------------------------------------------------------------------------
+module Data.Extensible.Effect.Default (
+  ReaderDef
+  , runReaderDef
+  , StateDef
+  , runStateDef
+  , WriterDef
+  , runWriterDef
+  , MaybeDef
+  , runMaybeDef
+  , EitherDef
+  , runEitherDef
+) where
+import Control.Applicative
+import Data.Extensible.Effect
+import Data.Extensible.Internal
+import Control.Monad.Except
+import Control.Monad.Reader.Class
+import Control.Monad.State.Strict
+import Control.Monad.Writer.Class
+
+instance Associate "IO" IO xs => MonadIO (Eff xs) where
+  liftIO = liftEff (Proxy :: Proxy "IO")
+
+pReader :: Proxy "Reader"
+pReader = Proxy
+
+instance Associate "Reader" ((:~:) r) xs => MonadReader r (Eff xs) where
+  ask = askEff pReader
+  local = localEff pReader
+  reader = asksEff pReader
+
+pState :: Proxy "State"
+pState = Proxy
+
+instance Associate "State" (State s) xs => MonadState s (Eff xs) where
+  get = getEff pState
+  put = putEff pState
+  state = stateEff pState
+
+pWriter :: Proxy "Writer"
+pWriter = Proxy
+
+instance (Monoid w, Associate "Writer" ((,) w) xs) => MonadWriter w (Eff xs) where
+  writer = writerEff pWriter
+  tell = tellEff pWriter
+  listen = listenEff pWriter
+  pass = passEff pWriter
+
+pEither :: Proxy "Either"
+pEither = Proxy
+
+instance (Associate "Either" (Const e) xs) => MonadError e (Eff xs) where
+  throwError = throwEff pEither
+  catchError = catchEff pEither
+
+instance (Monoid e, Associate "Either" (Const e) xs) => Alternative (Eff xs) where
+  empty = throwError mempty
+  p <|> q = catchError p (const q)
+
+instance (Monoid e, Associate "Either" (Const e) xs) => MonadPlus (Eff xs) where
+  mzero = empty
+  mplus = (<|>)
+
+type ReaderDef r = "Reader" >: ReaderEff r
+
+runReaderDef :: Eff (ReaderDef r ': xs) a -> r -> Eff xs a
+runReaderDef = runReaderEff
+{-# INLINE runReaderDef #-}
+
+type StateDef s = "State" >: State s
+
+runStateDef :: Eff (StateDef s ': xs) a -> s -> Eff xs (a, s)
+runStateDef = runStateEff
+{-# INLINE runStateDef #-}
+
+type WriterDef w = "Writer" >: WriterEff w
+
+runWriterDef :: Monoid w => Eff (WriterDef w ': xs) a -> Eff xs (a, w)
+runWriterDef = runWriterEff
+{-# INLINE runWriterDef #-}
+
+type MaybeDef = "Maybe" >: EitherEff ()
+
+runMaybeDef :: Eff (MaybeDef ': xs) a -> Eff xs (Maybe a)
+runMaybeDef = runMaybeEff
+{-# INLINE runMaybeDef #-}
+
+type EitherDef e = "Either" >: EitherEff e
+
+runEitherDef :: Eff (EitherDef e ': xs) a -> Eff xs (Either e a)
+runEitherDef = runEitherEff
+{-# INLINE runEitherDef #-}
diff --git a/src/Data/Extensible/Field.hs b/src/Data/Extensible/Field.hs
--- a/src/Data/Extensible/Field.hs
+++ b/src/Data/Extensible/Field.hs
@@ -1,20 +1,19 @@
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}
+{-# LANGUAGE CPP #-}
 #if __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE UndecidableSuperClasses #-}
 #endif
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Extensible.Record
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Module      :  Data.Extensible.Field
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- 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(..)
@@ -23,6 +22,8 @@
   , (@:>)
   , FieldOptic
   , FieldName
+  , liftField
+  , liftField2
   -- * Records and variants
   , RecordOf
   , Record
@@ -42,6 +43,8 @@
   , Labelling
   , Inextensible
   ) where
+import Control.DeepSeq (NFData)
+import Data.Coerce
 import Data.Extensible.Class
 import Data.Extensible.Sum
 import Data.Extensible.Match
@@ -52,6 +55,8 @@
 import Data.Constraint
 import Data.Extensible.Wrapper
 import Data.Functor.Identity
+import Data.Semigroup
+import Foreign.Storable (Storable)
 import GHC.TypeLits hiding (Nat)
 
 -- | Take the type of the key
@@ -66,6 +71,7 @@
 type family AssocValue (kv :: Assoc k v) :: v where
   AssocValue (k ':> v) = v
 
+-- | Combined constraint for 'Assoc'
 class (pk (AssocKey kv), pv (AssocValue kv)) => KeyValue pk pv kv where
 
 instance (pk k, pv v) => KeyValue pk pv (k ':> v)
@@ -76,6 +82,35 @@
 --
 newtype Field (h :: v -> *) (kv :: Assoc k v) = Field { getField :: h (AssocValue kv) }
 
+#define ND_Field(c) deriving instance c (h (AssocValue kv)) => c (Field h kv)
+
+ND_Field(Eq)
+ND_Field(Ord)
+ND_Field(Num)
+ND_Field(Integral)
+ND_Field(Fractional)
+ND_Field(Floating)
+ND_Field(Real)
+ND_Field(RealFloat)
+ND_Field(RealFrac)
+ND_Field(Semigroup)
+ND_Field(Storable)
+ND_Field(Monoid)
+ND_Field(Enum)
+ND_Field(Bounded)
+ND_Field(NFData)
+
+-- | Lift a function for the content.
+liftField :: (g (AssocValue kv) -> h (AssocValue kv)) -> Field g kv -> Field h kv
+liftField = coerce
+{-# INLINE liftField #-}
+
+-- | Lift a function for the content.
+liftField2 :: (f (AssocValue kv) -> g (AssocValue kv) -> h (AssocValue kv))
+    -> Field f kv -> Field g kv -> Field h kv
+liftField2 = coerce
+{-# INLINE liftField2 #-}
+
 instance Wrapper h => Wrapper (Field h) where
   type Repr (Field h) kv = Repr h (AssocValue kv)
   _Wrapper = dimap getField (fmap Field) . _Wrapper
@@ -87,12 +122,6 @@
     . showString " @= "
     . showsPrec 1 (view _Wrapper a)
 
-instance Monoid (h (AssocValue kv)) => Monoid (Field h kv) where
-  mempty = Field mempty
-  {-# INLINE mempty #-}
-  Field a `mappend` Field b = Field (mappend a b)
-  {-# INLINE mappend #-}
-
 -- | The type of records which contain several fields.
 --
 -- @RecordOf :: (v -> *) -> [Assoc k v] -> *@
@@ -113,7 +142,7 @@
 
 -- | An empty 'Record'.
 emptyRecord :: Record '[]
-emptyRecord = Nil
+emptyRecord = nil
 {-# INLINE emptyRecord #-}
 
 -- | Select a corresponding field of a variant.
@@ -121,6 +150,7 @@
 matchWithField h = matchWith (\(Field x) (Field y) -> h x y)
 {-# INLINE matchWithField #-}
 
+-- | Pattern matching on a 'Variant'
 matchField :: RecordOf (Match h r) xs -> VariantOf h xs -> r
 matchField = matchWithField runMatch
 {-# INLINE matchField #-}
@@ -161,6 +191,7 @@
 -- This type is used to resolve the name of the field internally.
 type FieldName k = Optic' (LabelPhantom k) Proxy (Inextensible (Field Proxy) '[k ':> ()]) ()
 
+-- | Signifies a field name internally
 type family Labelling s p :: Constraint where
   Labelling s (LabelPhantom t) = s ~ t
   Labelling s p = ()
@@ -179,7 +210,7 @@
 
 -- | Lifted ('@=')
 (<@=>) :: (Functor f, Wrapper h) => FieldName k -> f (Repr h v) -> Comp f (Field h) (k ':> v)
-(<@=>) k = Comp #. fmap (k @=)
+(<@=>) k = comp (k @=)
 {-# INLINE (<@=>) #-}
 infix 1 <@=>
 
diff --git a/src/Data/Extensible/HList.hs b/src/Data/Extensible/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/HList.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
+{-# LANGUAGE Trustworthy #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.HList
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Heterogeneous list
+------------------------------------------------------------------------
+module Data.Extensible.HList where
+
+import Data.Extensible.Internal
+import Unsafe.Coerce
+
+data HList (h :: k -> *) (xs :: [k]) where
+  HNil :: HList h '[]
+  HCons :: h x -> HList h xs -> HList h (x ': xs)
+
+infixr 5 `HCons`
+
+htraverse :: Applicative f => (forall x. g x -> f (h x)) -> HList g xs -> f (HList h xs)
+htraverse _ HNil = pure HNil
+htraverse f (HCons h xs) = HCons <$> f h <*> htraverse f xs
+
+htraverseWithIndex :: forall f g h xs. Applicative f
+    => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs)
+htraverseWithIndex f = go 0 where
+  go :: Int -> HList g t -> f (HList h t)
+  go !k (HCons x xs) = HCons <$> f (unsafeCoerce k) x <*> go (k + 1) xs
+  go _ HNil = pure HNil
+{-# INLINE htraverseWithIndex #-}
+
+hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r
+hfoldrWithIndex f r = go 0 where
+  go :: Int -> HList h t -> r
+  go !k (HCons x xs) = f (unsafeCoerce k) x $ go (k + 1) xs
+  go _ HNil = r
+{-# INLINE hfoldrWithIndex #-}
+
+hlength :: HList h xs -> Int
+hlength = go 0 where
+  go :: Int -> HList h xs -> Int
+  go n HNil = n
+  go n (HCons _ xs) = let n' = n + 1 in go n' xs
+{-# INLINE hlength #-}
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,14 +1,17 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE UndecidableSuperClasses #-}
+#endif
 ------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Inclusion
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Inclusion (
@@ -30,6 +33,7 @@
   , spreadAssoc
   ) where
 
+import Data.Constraint
 import Data.Extensible.Class
 import Data.Extensible.Product
 import Data.Extensible.Sum
@@ -44,42 +48,45 @@
 
 -- | Reify the inclusion of type level sets.
 inclusion :: forall xs ys. Include ys xs => Membership ys :* xs
-inclusion = htabulateFor (Proxy :: Proxy (Member ys)) (const membership)
+inclusion = hrepeatFor (Proxy :: Proxy (Member ys)) membership
 {-# INLINABLE inclusion #-}
 
--- | /O(m log n)/ Select some elements.
+-- | /O(n)/ Select some elements.
 shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
 shrink h = hmap (hindex h) inclusion
 {-# INLINE shrink #-}
 
--- | /O(log n)/ Embed to a larger union.
+-- | /O(1)/ Embed to a larger union.
 spread :: (xs ⊆ ys) => h :| xs -> h :| ys
 spread (EmbedAt i h) = views (pieceAt i) EmbedAt inclusion h
 {-# INLINE spread #-}
 
 ------------------------------------------------------------------
 
-class Associated xs t where
+type family Associated' (xs :: [Assoc k v]) (t :: Assoc k v) :: Constraint where
+  Associated' xs (k ':> v) = Associate k v xs
+
+-- | @'Associated' xs (k ':> v)@ is equivalent to @'Associate' k v xs@
+class Associated' xs t => Associated xs t where
   getAssociation :: Membership xs t
 
-instance Associate k v xs => Associated xs (k ':> v) where
+instance (Associated' xs t, t ~ (k ':> v)) => Associated xs t where
   getAssociation = association
-  {-# INLINE getAssociation #-}
 
 -- | Similar to 'Include', but this focuses on keys.
 type IncludeAssoc ys = Forall (Associated ys)
 
 -- | Reify the inclusion of type level sets.
 inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => Membership ys :* xs
-inclusionAssoc = htabulateFor (Proxy :: Proxy (Associated ys)) (const getAssociation)
+inclusionAssoc = hrepeatFor (Proxy :: Proxy (Associated ys)) getAssociation
 {-# INLINABLE inclusionAssoc #-}
 
--- | /O(m log n)/ Select some elements.
+-- | /O(n)/ Select some elements.
 shrinkAssoc :: (IncludeAssoc ys xs) => h :* ys -> h :* xs
 shrinkAssoc h = hmap (hindex h) inclusionAssoc
 {-# INLINE shrinkAssoc #-}
 
--- | /O(log n)/ Embed to a larger union.
+-- | /O(1)/ Embed to a larger union.
 spreadAssoc :: (IncludeAssoc ys xs) => h :| xs -> h :| ys
 spreadAssoc (EmbedAt i h) = views (pieceAt i) EmbedAt inclusionAssoc h
 {-# INLINE spreadAssoc #-}
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,281 +1,220 @@
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FunctionalDependencies #-}
-{-# LANGUAGE ScopedTypeVariables, BangPatterns, StandaloneDeriving #-}
-{-# 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 (
-  -- * Membership
-  Membership
-  , getMemberId
-  , mkMembership
-  , reifyMembership
-  , runMembership
-  , compareMembership
-  , impossibleMembership
-  -- * Member class
-  , Member(..)
-  , remember
-#if __GLASGOW_HASKELL__ >= 800
-  , type (∈)
-#else
-  , (∈)()
-#endif
-  , FindType
-  -- * Association
-  , Assoc(..)
-  , Associate(..)
-  , FindAssoc
-  -- * Sugar
-  , Elaborate
-  , Elaborated(..)
-  -- * Tree navigation
-  , NavHere(..)
-  , navigate
-  , here
-  , navNext
-  , navL
-  , navR
-  -- * Miscellaneous
-  , Nat(..)
-  , KnownPosition(..)
-  , Succ
-  , Half
-  , Head
-  , Tail
-  , Last
-#if __GLASGOW_HASKELL__ >= 800
-  , type (++)
-#else
-  , (++)()
-#endif
-  , Map
-  , Merge
-  , Concat
-  , module Data.Type.Equality
-  , module Data.Proxy
-  ) where
-import Data.Type.Equality
-import Data.Proxy
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative
-import Data.Word
-#endif
-import Control.Monad
-import Unsafe.Coerce
-import Data.Typeable
-import Language.Haskell.TH hiding (Pred)
-import Data.Bits
-
--- | Generates a 'Membership' that corresponds to the given ordinal (0-origin).
-mkMembership :: Int -> Q Exp
-mkMembership n = do
-  let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
-  let rest = mkName "any"
-  let cons x xs = PromotedConsT `AppT` x `AppT` xs
-  let t = foldr cons (VarT rest) (map VarT names)
-  sigE (conE 'Membership `appE` litE (IntegerL $ toInteger n))
-    $ forallT (PlainTV rest : map PlainTV names) (pure [])
-    $ conT ''Membership `appT` pure t `appT` varT (names !! n)
-
--- | The position of @x@ in the type level set @xs@.
-newtype Membership (xs :: [k]) (x :: k) = Membership { getMemberId :: Word } deriving Typeable
-
-newtype Remembrance xs x r = Remembrance (Member xs x => r)
-
--- | Remember that @Member xs x@ from 'Membership'.
-remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
-remember i r = unsafeCoerce (Remembrance r :: Remembrance xs x r) i
-{-# INLINE remember #-}
-
-class Member xs x where
-  membership :: Membership xs x
-
-instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownPosition pos) => Member xs x where
-  membership = Membership (theInt (Proxy :: Proxy pos))
-  {-# INLINE membership #-}
-
-reifyMembership :: Word -> (forall x. Membership xs x -> r) -> r
-reifyMembership n k = k (Membership n)
-
--- | The kind of key-value pairs
-data Assoc k v = k :> v
-infix 0 :>
-
--- | @'Associate' k v xs@ is essentially identical to @(k :> v) ∈ xs@
--- , but the type @v@ is inferred from @k@ and @xs@.
-class Associate k v xs | k xs -> v where
-  association :: Membership xs (k ':> v)
-
-instance (Elaborate k (FindAssoc k xs) ~ 'Expecting (n ':> v), KnownPosition n) => Associate k v xs where
-  association = Membership (theInt (Proxy :: Proxy n))
-
-data Elaborated k v = Expecting v | Missing k | Duplicate k
-
-type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where
-  Elaborate k '[] = 'Missing k
-  Elaborate k '[x] = 'Expecting x
-  Elaborate k xs = 'Duplicate k
-
-type family FindAssoc (key :: k) (xs :: [Assoc k v]) where
-  FindAssoc k ((k ':> v) ': xs) = ('Zero ':> v) ': MapSuccKey (FindAssoc k xs)
-  FindAssoc k ((k' ':> v) ': xs) = MapSuccKey (FindAssoc k xs)
-  FindAssoc k '[] = '[]
-
-type family MapSuccKey (xs :: [Assoc Nat v]) :: [Assoc Nat v] where
-  MapSuccKey '[] = '[]
-  MapSuccKey ((k ':> x) ': xs) = (Succ k ':> x) ': MapSuccKey xs
-
-instance Show (Membership xs x) where
-  show (Membership n) = "$(mkMembership " ++ show n ++ ")"
-
-instance Eq (Membership xs x) where
-  _ == _ = True
-
-instance Ord (Membership xs x) where
-  compare _ _ = EQ
-
--- | Embodies a type equivalence to ensure that the 'Membership' points the first element.
-runMembership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
-runMembership (Membership 0) l _ = l (unsafeCoerce Refl)
-runMembership (Membership n) _ r = r (Membership (n - 1))
-{-# INLINE runMembership #-}
-
--- | Compare two 'Membership's.
-compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
-compareMembership (Membership m) (Membership n) = case compare m n of
-  EQ -> Right (unsafeCoerce Refl)
-  x -> Left x
-{-# INLINE compareMembership #-}
-
-impossibleMembership :: Membership '[] x -> r
-impossibleMembership _ = error "Impossible"
-
--- | PRIVILEGED: Navigate a tree.
-navigate :: (NavHere xs x -> r)
-  -> (Membership (Half (Tail xs)) x -> r)
-  -> (Membership (Half (Tail (Tail xs))) x -> r)
-  -> Membership xs x
-  -> r
-navigate h nl nr = \case
-  Membership 0 -> h (unsafeCoerce Here)
-  Membership n -> if n .&. 1 == 0
-    then nr (Membership (unsafeShiftR (n - 1) 1))
-    else nl (Membership (unsafeShiftR (n - 1) 1))
-{-# INLINE navigate #-}
-
--- | Ensure that the first element of @xs@ is @x@
-data NavHere xs x where
-  Here :: NavHere (x ': xs) x
-
--- | The 'Membership' points the first element
-here :: Membership (x ': xs) x
-here = Membership 0
-{-# INLINE here #-}
-
--- | The next membership
-navNext :: Membership xs y -> Membership (x ': xs) y
-navNext (Membership n) = Membership (n + 1)
-{-# INLINE navNext #-}
-
--- | Describes the relation of 'Membership' within a tree
-navL :: Membership (Half xs) y -> Membership (x ': xs) y
-navL (Membership x) = Membership (x * 2 + 1)
-{-# INLINE navL #-}
-
--- | Describes the relation of 'Membership' within a tree
-navR :: Membership (Half (Tail xs)) y -> Membership (x ': xs) y
-navR (Membership x) = Membership (x * 2 + 2)
-{-# INLINE navR #-}
-
--- | Unicode flipped alias for 'Member'
-type x ∈ xs = Member xs x
-
-type family Head (xs :: [k]) :: k where
-  Head (x ': xs) = x
-
--- | FindType types
-type family FindType (x :: k) (xs :: [k]) :: [Nat] where
-  FindType x (x ': xs) = 'Zero ': FindType x xs
-  FindType x (y ': ys) = MapSucc (FindType x ys)
-  FindType x '[] = '[]
-
--- | Interleaved list
-type family Half (xs :: [k]) :: [k] where
-  Half '[] = '[]
-  Half (x ': y ': zs) = x ': Half zs
-  Half (x ': '[]) = '[x]
-
--- | Type-level tail
-type family Tail (xs :: [k]) :: [k] where
-  Tail (x ': xs) = xs
-  Tail '[] = '[]
-
-type family Last (x :: [k]) :: k where
-  Last '[x] = x
-  Last (x ': xs) = Last xs
-
--- | Type level binary number
-data Nat = Zero | DNat Nat | SDNat Nat
-
--- | Converts type naturals into 'Word'.
-class KnownPosition n where
-  theInt :: proxy n -> Word
-
-instance KnownPosition 'Zero where
-  theInt _ = 0
-  {-# INLINE theInt #-}
-
-instance KnownPosition n => KnownPosition ('DNat n) where
-  theInt _ = theInt (Proxy :: Proxy n) `unsafeShiftL` 1
-  {-# INLINE theInt #-}
-
-instance KnownPosition n => KnownPosition ('SDNat n) where
-  theInt _ = (theInt (Proxy :: Proxy n) `unsafeShiftL` 1) + 1
-  {-# INLINE theInt #-}
-
--- | The successor of the number
-type family Succ (x :: Nat) :: Nat where
-  Succ 'Zero = 'SDNat 'Zero
-  Succ ('DNat n) = 'SDNat n
-  Succ ('SDNat n) = 'DNat (Succ n)
-
--- | Ideally, it will be 'Map Succ'
-type family MapSucc (xs :: [Nat]) :: [Nat] where
-  MapSucc '[] = '[]
-  MapSucc (x ': xs) = Succ x ': MapSucc xs
-
--- | Type level map
-type family Map (f :: k -> k) (xs :: [k]) :: [k] where
-  Map f '[] = '[]
-  Map f (x ': xs) = f x ': Map f xs
-
--- | Type level ++
-type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
-  '[] ++ ys = ys
-  (x ': xs) ++ ys = x ': xs ++ ys
-
-infixr 5 ++
-
--- | Type level concat
-type family Concat (xs :: [[k]]) :: [k] where
-  Concat '[] = '[]
-  Concat (x ': xs) = x ++ Concat xs
-
--- | Type level merging
-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
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FunctionalDependencies #-}
+{-# LANGUAGE ScopedTypeVariables, BangPatterns, StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Inclusion
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- A bunch of combinators that contains magic
+------------------------------------------------------------------------
+module Data.Extensible.Internal (
+  -- * Membership
+  Membership
+  , getMemberId
+  , mkMembership
+  , reifyMembership
+  , runMembership
+  , compareMembership
+  , impossibleMembership
+  -- * Member class
+  , Member(..)
+  , remember
+#if __GLASGOW_HASKELL__ >= 800
+  , type (∈)
+#else
+  , (∈)()
+#endif
+  , FindType
+  -- * Association
+  , Assoc(..)
+#if __GLASGOW_HASKELL__ >= 800
+  , type (>:)
+#else
+  , (>:)()
+#endif
+  , Associate(..)
+  , FindAssoc
+  -- * Sugar
+  , Elaborate
+  , Elaborated(..)
+  -- * Tree navigation
+  , NavHere(..)
+  , here
+  , navNext
+  -- * Miscellaneous
+  , Nat(..)
+  , KnownPosition(..)
+  , Succ
+  , Head
+  , Last
+  , module Data.Type.Equality
+  , module Data.Proxy
+  ) where
+import Data.Type.Equality
+import Data.Proxy
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative
+import Data.Word
+#endif
+import Control.Monad
+import Unsafe.Coerce
+import Data.Typeable
+import Language.Haskell.TH hiding (Pred)
+import Data.Bits
+
+-- | Generates a 'Membership' that corresponds to the given ordinal (0-origin).
+mkMembership :: Int -> Q Exp
+mkMembership n = do
+  let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
+  let rest = mkName "any"
+  let cons x xs = PromotedConsT `AppT` x `AppT` xs
+  let t = foldr cons (VarT rest) (map VarT names)
+  sigE (conE 'Membership `appE` litE (IntegerL $ toInteger n))
+    $ forallT (PlainTV rest : map PlainTV names) (pure [])
+    $ conT ''Membership `appT` pure t `appT` varT (names !! n)
+
+-- | The position of @x@ in the type level set @xs@.
+newtype Membership (xs :: [k]) (x :: k) = Membership { getMemberId :: Int } deriving Typeable
+
+newtype Remembrance xs x r = Remembrance (Member xs x => r)
+
+-- | Remember that @Member xs x@ from 'Membership'.
+remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
+remember i r = unsafeCoerce (Remembrance r :: Remembrance xs x r) i
+{-# INLINE remember #-}
+
+-- | @x@ is a member of @xs@
+class Member xs x where
+  membership :: Membership xs x
+
+instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownPosition pos) => Member xs x where
+  membership = Membership (theInt (Proxy :: Proxy pos))
+  {-# INLINE membership #-}
+
+reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
+reifyMembership n k = k (Membership n)
+
+-- | The kind of key-value pairs
+data Assoc k v = k :> v
+infix 0 :>
+
+-- | A synonym for (':>')
+type (>:) = '(:>)
+
+-- | @'Associate' k v xs@ is essentially identical to @(k :> v) ∈ xs@
+-- , but the type @v@ is inferred from @k@ and @xs@.
+class Associate k v xs | k xs -> v where
+  association :: Membership xs (k ':> v)
+
+instance (Elaborate k (FindAssoc k xs) ~ 'Expecting (n ':> v), KnownPosition n) => Associate k v xs where
+  association = Membership (theInt (Proxy :: Proxy n))
+
+-- | A readable type search result
+data Elaborated k v = Expecting v | Missing k | Duplicate k
+
+type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where
+  Elaborate k '[] = 'Missing k
+  Elaborate k '[x] = 'Expecting x
+  Elaborate k xs = 'Duplicate k
+
+type family FindAssoc (key :: k) (xs :: [Assoc k v]) where
+  FindAssoc k ((k ':> v) ': xs) = ('Zero ':> v) ': MapSuccKey (FindAssoc k xs)
+  FindAssoc k ((k' ':> v) ': xs) = MapSuccKey (FindAssoc k xs)
+  FindAssoc k '[] = '[]
+
+type family MapSuccKey (xs :: [Assoc Nat v]) :: [Assoc Nat v] where
+  MapSuccKey '[] = '[]
+  MapSuccKey ((k ':> x) ': xs) = (Succ k ':> x) ': MapSuccKey xs
+
+instance Show (Membership xs x) where
+  show (Membership n) = "$(mkMembership " ++ show n ++ ")"
+
+instance Eq (Membership xs x) where
+  _ == _ = True
+
+instance Ord (Membership xs x) where
+  compare _ _ = EQ
+
+-- | Embodies a type equivalence to ensure that the 'Membership' points the first element.
+runMembership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
+runMembership (Membership 0) l _ = l (unsafeCoerce Refl)
+runMembership (Membership n) _ r = r (Membership (n - 1))
+{-# INLINE runMembership #-}
+
+-- | Compare two 'Membership's.
+compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
+compareMembership (Membership m) (Membership n) = case compare m n of
+  EQ -> Right (unsafeCoerce Refl)
+  x -> Left x
+{-# INLINE compareMembership #-}
+
+-- | There is no 'Membership' of an empty list.
+impossibleMembership :: Membership '[] x -> r
+impossibleMembership _ = error "Impossible"
+
+-- | Ensure that the first element of @xs@ is @x@
+data NavHere xs x where
+  Here :: NavHere (x ': xs) x
+
+-- | The 'Membership' points the first element
+here :: Membership (x ': xs) x
+here = Membership 0
+{-# INLINE here #-}
+
+-- | The next membership
+navNext :: Membership xs y -> Membership (x ': xs) y
+navNext (Membership n) = Membership (n + 1)
+{-# INLINE navNext #-}
+
+-- | Unicode flipped alias for 'Member'
+type x ∈ xs = Member xs x
+
+type family Head (xs :: [k]) :: k where
+  Head (x ': xs) = x
+
+-- | FindType types
+type family FindType (x :: k) (xs :: [k]) :: [Nat] where
+  FindType x (x ': xs) = 'Zero ': FindType x xs
+  FindType x (y ': ys) = MapSucc (FindType x ys)
+  FindType x '[] = '[]
+
+type family Last (x :: [k]) :: k where
+  Last '[x] = x
+  Last (x ': xs) = Last xs
+
+-- | Type level binary number
+data Nat = Zero | DNat Nat | SDNat Nat
+
+-- | Converts type naturals into 'Word'.
+class KnownPosition n where
+  theInt :: proxy n -> Int
+
+instance KnownPosition 'Zero where
+  theInt _ = 0
+  {-# INLINE theInt #-}
+
+instance KnownPosition n => KnownPosition ('DNat n) where
+  theInt _ = theInt (Proxy :: Proxy n) `unsafeShiftL` 1
+  {-# INLINE theInt #-}
+
+instance KnownPosition n => KnownPosition ('SDNat n) where
+  theInt _ = (theInt (Proxy :: Proxy n) `unsafeShiftL` 1) + 1
+  {-# INLINE theInt #-}
+
+-- | The successor of the number
+type family Succ (x :: Nat) :: Nat where
+  Succ 'Zero = 'SDNat 'Zero
+  Succ ('DNat n) = 'SDNat n
+  Succ ('SDNat n) = 'DNat (Succ n)
+
+-- | Ideally, it will be 'Map Succ'
+type family MapSucc (xs :: [Nat]) :: [Nat] where
+  MapSucc '[] = '[]
+  MapSucc (x ': xs) = Succ x ': MapSucc xs
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,13 +1,11 @@
 {-# LANGUAGE Trustworthy #-}
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Extensible.Rig
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Module      :  Data.Extensible.Internal.Rig
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  portable
 --
 -- Re-implementation of lens combinators
 ------------------------------------------------------------------------
diff --git a/src/Data/Extensible/Label.hs b/src/Data/Extensible/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Label.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE CPP, MultiParamTypeClasses #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Label
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Experimental API for OverloadedLabels. GHC 8.0+ only
+-----------------------------------------------------------------------------
+module Data.Extensible.Label where
+
+#if __GLASGOW_HASKELL__ >= 800
+
+import Data.Extensible.Class
+import Data.Extensible.Field
+import Data.Proxy
+import GHC.OverloadedLabels
+
+instance k ~ l => IsLabel k (Proxy l) where
+  fromLabel _ = Proxy
+
+-- | Specialised version of 'itemAssoc'.
+訊 :: Proxy k -> FieldOptic k
+訊 = itemAssoc
+
+#endif
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
@@ -2,12 +2,10 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.League
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 -- Pattern matching
 ------------------------------------------------------------------------
@@ -36,7 +34,7 @@
 mapMatch f = Match #. (f.) .# runMatch
 {-# INLINE mapMatch #-}
 
--- | /O(log n)/ Perform pattern matching.
+-- | /O(1)/ Perform pattern matching.
 match :: Match h a :* xs -> h :| xs -> a
 match = matchWith runMatch
 {-# INLINE match #-}
diff --git a/src/Data/Extensible/Nullable.hs b/src/Data/Extensible/Nullable.hs
--- a/src/Data/Extensible/Nullable.hs
+++ b/src/Data/Extensible/Nullable.hs
@@ -2,16 +2,15 @@
 ------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Nullable
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Nullable (
-  coinclusion
+  vacancy
+  , coinclusion
   , wrench
   , retrench
   , Nullable(..)
@@ -23,17 +22,24 @@
 import Data.Extensible.Inclusion
 import Data.Extensible.Internal.Rig
 import Data.Typeable (Typeable)
-import Data.Monoid
 import Data.Extensible.Wrapper
+import qualified Data.Extensible.Struct as S
 import Data.Profunctor.Unsafe
+import Data.Semigroup
 
--- | Poly-kinded Maybe
+-- | Wrapped 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))
 
+instance Semigroup (h x) => Monoid (Nullable h x) where
+  mempty = Nullable Nothing
+  mappend (Nullable (Just a)) (Nullable (Just b)) = Nullable (Just (a <> b))
+  mappend a@(Nullable (Just _)) _ = a
+  mappend _ b = b
+
 -- | Apply a function to its content.
 mapNullable :: (g x -> h y) -> Nullable g x -> Nullable h y
 mapNullable f = Nullable #. fmap f .# getNullable
@@ -41,10 +47,14 @@
 
 -- | 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
+coinclusion = S.hfrozen $ do
+  s <- S.newRepeat $ Nullable Nothing
+  hfoldrWithIndex
+    (\i m cont -> S.set s m (Nullable $ Just i) >> cont) (return s) inclusion
+
+-- | A product filled with @'Nullable' 'Nothing'@
+vacancy :: Generate xs => Nullable h :* xs
+vacancy = hrepeat $ Nullable Nothing
 
 -- | Extend a product and fill missing fields by 'Null'.
 wrench :: (Generate ys, xs ⊆ ys) => h :* xs -> Nullable h :* ys
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
@@ -3,12 +3,10 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Plain
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Plain (
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,267 +1,212 @@
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.Product
--- Copyright   :  (c) Fumiaki Kinoshita 2015
--- License     :  BSD3
---
--- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
-------------------------------------------------------------------------
-module Data.Extensible.Product (
-  -- * Basic operations
-  (:*)(..)
-  , (<:)
-  , (<:*)
-  , (*++*)
-  , hhead
-  , htail
-  , huncons
-  , hmap
-  , hmapWithIndex
-  , htrans
-  , hzipWith
-  , hzipWith3
-  , hfoldMap
-  , htraverse
-  , htraverseWithIndex
-  , hsequence
-  , hcollect
-  , hdistribute
-  -- * Lookup
-  , hlookup
-  , hindex
-  , sectorAt
-  , sector
-  -- * Generation
-  , Generate(..)
-  , htabulate
-  , Forall(..)
-  , htabulateFor) where
-
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Unsafe.Coerce
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative
-#endif
-import Data.Monoid
-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)
-    -> h :* Half xs
-    -> h :* Half (Tail xs)
-    -> h :* (x ': xs)
-
-deriving instance Typeable (:*)
-
--- | /O(1)/ Extract the head element.
-hhead :: h :* (x ': xs) -> h x
-hhead (Tree a _ _) = a
-{-# INLINE hhead #-}
-
--- | /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
-
--- | 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 #-}
-
--- | 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 <:* 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' 'id' ≡ 'id'
--- 'hmap' (f . g) ≡ 'hmap' f . 'hmap' g
--- @
-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
-
--- | Transform every elements in a product, preserving the order.
-htrans :: (forall x. g x -> h (t x)) -> g :* xs -> h :* Map t xs
-htrans t (Tree h a b) = unsafeCoerce (Tree (t h)) (htrans t a) (htrans t b)
-htrans _ Nil = Nil
-
--- | Combine 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)
-hzipWith _ Nil _ = Nil
-hzipWith _ _ Nil = Nil
-
--- | 'zipWith3' for heterogeneous product
-hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
-hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
-hzipWith3 _ Nil _ _ = Nil
-hzipWith3 _ _ Nil _ = Nil
-hzipWith3 _ _ _ Nil = Nil
-
--- | Map elements to a monoid and combine the results.
---
--- @'hfoldMap' f . 'hmap' g ≡ 'hfoldMap' (f . g)@
-hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
-hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
-hfoldMap _ Nil = mempty
-
--- | Traverse all elements and combine the result sequentially.
--- @
--- htraverse (fmap f . g) ≡ fmap (hmap f) . htraverse g
--- htraverse pure ≡ pure
--- htraverse (Comp . fmap g . f) ≡ Comp . fmap (htraverse g) . htraverse f
--- @
-htraverse :: Applicative f => (forall x. g x -> f (h x)) -> g :* xs -> f (h :* xs)
-htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
-htraverse _ Nil = pure Nil
-
--- | 'sequence' analog for extensible products
-hsequence :: Applicative f => Comp f h :* xs -> f (h :* xs)
-hsequence = htraverse getComp
-{-# INLINE hsequence #-}
-
--- | The dual of 'htraverse'
-hcollect :: (Functor f, Generate xs) => (a -> h :* xs) -> f a -> Comp f h :* xs
-hcollect f m = htabulate $ \i -> Comp $ fmap (hlookup i . f) m
-{-# INLINABLE hcollect #-}
-
--- | The dual of 'hsequence'
-hdistribute :: (Functor f, Generate xs) => f (h :* xs) -> Comp f h :* xs
-hdistribute = hcollect id
-{-# INLINE hdistribute #-}
-
--- | /O(log n)/ Pick up an elemtnt.
-hlookup :: Membership xs x -> h :* xs -> h x
-hlookup = view . pieceAt
-{-# INLINABLE hlookup #-}
-
--- | Flipped 'hlookup'
-hindex :: h :* xs -> Membership xs x -> h x
-hindex = flip hlookup
-{-# INLINE hindex #-}
-
--- | 'hmap' with 'Membership's.
-hmapWithIndex :: forall g h xs. (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
-hmapWithIndex f = go id where
-  go :: (forall x. Membership t x -> Membership 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
-{-# INLINE hmapWithIndex #-}
-
--- | 'htraverse' with 'Membership's.
-htraverseWithIndex :: forall f g h xs. Applicative f
-  => (forall x. Membership xs x -> g x -> f (h x)) -> g :* xs -> f (h :* xs)
-htraverseWithIndex f = go id where
-  go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> f (h :* t)
-  go k (Tree g a b) = Tree <$> f (k here) g <*> go (k . navL) a <*> go (k . navR) b
-  go _ Nil = pure Nil
-{-# INLINE htraverseWithIndex #-}
-
-instance Functor f => Extensible f (->) (:*) where
-  -- | /O(log n)/ A lens for a value in a known position.
-  pieceAt = pieceAt_
-  {-# INLINE pieceAt #-}
-
-pieceAt_ :: forall (xs :: [k]) (x :: k) (h :: k -> *) (f :: * -> *). Functor f
-  => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-pieceAt_ i f = flip go i where
-  go :: forall t. h :* t -> Membership t x -> f (h :* t)
-  go (Tree h a b) = navigate
-    (\Here -> fmap (\h' -> Tree h' a b) (f h))
-    (fmap (\a' -> Tree h a' b) . go a)
-    (fmap (\b' -> Tree h a b') . go b)
-  go Nil = error "Impossible"
-{-# INLINE pieceAt_ #-}
-
-{-# DEPRECATED sectorAt "Use pieceAt" #-}
--- | The legacy name for 'pieceAt'
-sectorAt :: Functor f => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sectorAt = pieceAt
-
-{-# DEPRECATED sector "Use piece" #-}
--- | The legacy name for 'piece'
-sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sector = piece
-
--- | Given a function that maps types to values, we can "collect" entities all you want.
-class Generate (xs :: [k]) where
-  -- | /O(n)/ Generate a product with the given function.
-  hgenerate :: Applicative f => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
-
-instance Generate '[] where
-  hgenerate _ = pure Nil
-  {-# INLINE hgenerate #-}
-
-instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
-  hgenerate f = Tree <$> f here <*> hgenerate (f . navL) <*> hgenerate (f . navR)
-  {-# INLINE hgenerate #-}
-
--- | Pure version of 'hgenerate'.
---
--- @
--- 'hmap' f ('htabulate' g) ≡ 'htabulate' (f . g)
--- 'htabulate' ('hindex' m) ≡ m
--- 'hindex' ('htabulate' k) ≡ k
--- @
-htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
-htabulate f = runIdentity (hgenerate (Identity #. f))
-{-# INLINE htabulate #-}
-
--- | Guarantees the all elements satisfies the predicate.
-class Forall c (xs :: [k]) where
-  -- | /O(n)/ Analogous to 'hgenerate', but it also supplies a context @c x@ for every elements in @xs@.
-  hgenerateFor :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
-
-instance Forall c '[] where
-  hgenerateFor _ _ = pure Nil
-  {-# INLINE hgenerateFor #-}
-
-instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
-  hgenerateFor proxy f = Tree
-    <$> f here
-    <*> hgenerateFor proxy (f . navL)
-    <*> hgenerateFor proxy (f . navR)
-  {-# INLINE hgenerateFor #-}
-
--- | Pure version of 'hgenerateFor'.
-htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
-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 #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE ViewPatterns, ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Product
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+------------------------------------------------------------------------
+module Data.Extensible.Product (
+  -- * Basic operations
+  (:*)
+  , nil
+  , (<:)
+  , hlength
+  , hmap
+  , hmapWithIndex
+  , hzipWith
+  , hzipWith3
+  , hfoldMap
+  , hfoldMapWithIndex
+  , hfoldrWithIndex
+  , htraverse
+  , htraverseWithIndex
+  , hsequence
+  -- * Update
+  , haccumMap
+  , haccum
+  , hpartition
+  -- * Lookup
+  , hlookup
+  , hindex
+  -- * Generation
+  , Generate(..)
+  , hgenerate
+  , htabulate
+  , hrepeat
+  , hcollect
+  , hdistribute
+  , fromHList
+  , toHList
+  , Forall(..)
+  , hgenerateFor
+  , htabulateFor
+  , hrepeatFor) where
+
+import Data.Extensible.Internal
+import Data.Extensible.Struct
+import Data.Extensible.Sum
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative
+#endif
+import Data.Extensible.Class
+import qualified Data.Extensible.HList as HList
+import Data.Extensible.Wrapper
+
+-- | O(n) Prepend an element onto a product.
+-- Expressions like @a <: b <: c <: nil@ are transformed to a single 'fromHList'.
+(<:) :: h x -> h :* xs -> h :* (x ': xs)
+(<:) x = fromHList . HList.HCons x . toHList
+{-# INLINE (<:) #-}
+infixr 0 <:
+
+-- | An empty product.
+nil :: h :* '[]
+nil = hfrozen $ new $ error "Impossible"
+{-# NOINLINE nil #-}
+{-# RULES "toHList/nil" toHList nil = HList.HNil #-}
+
+-- | Convert 'L.HList' into a product.
+fromHList :: HList.HList h xs -> h :* xs
+fromHList xs = hfrozen (newFromHList xs)
+{-# NOINLINE fromHList #-}
+{-# RULES "toHList/fromHList" forall x. toHList (fromHList x) = x #-}
+
+-- | Flipped 'hlookup'
+hindex :: h :* xs -> Membership xs x ->  h x
+hindex = flip hlookup
+{-# INLINE hindex #-}
+
+-- | Map a function to every element of a product.
+hmapWithIndex :: (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
+hmapWithIndex t p = hfrozen (newFrom p t)
+{-# INLINE hmapWithIndex #-}
+
+-- | Transform every element in a product, preserving the order.
+--
+-- @
+-- 'hmap' 'id' ≡ 'id'
+-- 'hmap' (f . g) ≡ 'hmap' f . 'hmap' g
+-- @
+hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
+hmap f = hmapWithIndex (const f)
+{-# INLINE hmap #-}
+
+-- | 'zipWith' for heterogeneous product
+hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
+hzipWith t xs = hmapWithIndex (\i -> t (hlookup i xs))
+{-# INLINE hzipWith #-}
+
+-- | 'zipWith3' for heterogeneous product
+hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
+hzipWith3 t xs ys = hmapWithIndex (\i -> t (hlookup i xs) (hlookup i ys))
+{-# INLINE hzipWith3 #-}
+
+-- | Map elements to a monoid and combine the results.
+--
+-- @'hfoldMap' f . 'hmap' g ≡ 'hfoldMap' (f . g)@
+hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
+hfoldMap f = hfoldMapWithIndex (const f)
+{-# INLINE hfoldMap #-}
+
+-- | 'hfoldMap' with the membership of elements.
+hfoldMapWithIndex :: Monoid a
+  => (forall x. Membership xs x -> g x -> a) -> g :* xs -> a
+hfoldMapWithIndex f = hfoldrWithIndex (\i -> mappend . f i) mempty
+{-# INLINE hfoldMapWithIndex #-}
+
+-- | Traverse all elements and combine the result sequentially.
+-- @
+-- htraverse (fmap f . g) ≡ fmap (hmap f) . htraverse g
+-- htraverse pure ≡ pure
+-- htraverse (Comp . fmap g . f) ≡ Comp . fmap (htraverse g) . htraverse f
+-- @
+htraverse :: Applicative f => (forall x. g x -> f (h x)) -> g :* xs -> f (h :* xs)
+htraverse f = fmap fromHList . HList.htraverse f . toHList
+{-# INLINE htraverse #-}
+
+-- | 'sequence' analog for extensible products
+hsequence :: Applicative f => Comp f h :* xs -> f (h :* xs)
+hsequence = htraverse getComp
+{-# INLINE hsequence #-}
+
+-- | The dual of 'htraverse'
+hcollect :: (Functor f, Generate xs) => (a -> h :* xs) -> f a -> Comp f h :* xs
+hcollect f m = htabulate $ \i -> Comp $ fmap (hlookup i . f) m
+{-# INLINABLE hcollect #-}
+
+-- | The dual of 'hsequence'
+hdistribute :: (Functor f, Generate xs) => f (h :* xs) -> Comp f h :* xs
+hdistribute = hcollect id
+{-# INLINE hdistribute #-}
+
+-- | 'htraverse' with 'Membership's.
+htraverseWithIndex :: Applicative f
+  => (forall x. Membership xs x -> g x -> f (h x)) -> g :* xs -> f (h :* xs)
+htraverseWithIndex f = fmap fromHList . HList.htraverseWithIndex f . toHList
+{-# INLINE htraverseWithIndex #-}
+
+-- | A product filled with the specified value.
+hrepeat :: Generate xs => (forall x. h x) -> h :* xs
+hrepeat x = hfrozen $ newRepeat x
+{-# INLINE hrepeat #-}
+
+-- | Construct a product using a function which takes a 'Membership'.
+--
+-- @
+-- 'hmap' f ('htabulate' g) ≡ 'htabulate' (f . g)
+-- 'htabulate' ('hindex' m) ≡ m
+-- 'hindex' ('htabulate' k) ≡ k
+-- @
+htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
+htabulate f = hfrozen $ new f
+{-# INLINE htabulate #-}
+
+-- | 'Applicative' version of 'htabulate'.
+hgenerate :: (Generate xs, Applicative f)
+  => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
+hgenerate f = fmap fromHList $ hgenerateList f
+{-# INLINE hgenerate #-}
+
+-- | Pure version of 'hgenerateFor'.
+htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
+htabulateFor p f = hfrozen $ newFor p f
+{-# INLINE htabulateFor #-}
+
+-- | A product filled with the specified value.
+hrepeatFor :: Forall c xs => proxy c -> (forall x. c x => h x) -> h :* xs
+hrepeatFor p f = htabulateFor p (const f)
+{-# INLINE hrepeatFor #-}
+
+-- | 'Applicative' version of 'htabulateFor'.
+hgenerateFor :: (Forall c xs, Applicative f)
+  => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
+hgenerateFor p f = fmap fromHList $ hgenerateListFor p f
+{-# INLINE hgenerateFor #-}
+
+-- | Accumulate sums on a product.
+haccumMap :: Foldable f
+  => (a -> g :| xs)
+  -> (forall x. Membership xs x -> g x -> h x -> h x)
+  -> h :* xs -> f a -> h :* xs
+haccumMap f g p0 xs = hfrozen $ do
+  s <- thaw p0
+  mapM_ (\x -> case f x of EmbedAt i v -> get s i >>= set s i . g i v) xs
+  return s
+
+-- | @haccum = 'haccumMap' 'id'@
+haccum :: Foldable f
+  => (forall x. Membership xs x -> g x -> h x -> h x)
+  -> h :* xs -> f (g :| xs) -> h :* xs
+haccum = haccumMap id
+{-# INLINE haccum #-}
+
+-- | Group sums by type.
+hpartition :: (Foldable f, Generate xs) => (a -> h :| xs) -> f a -> Comp [] h :* xs
+hpartition f = haccumMap f (\_ x (Comp xs) -> Comp (x:xs)) $ hrepeat $ Comp []
+{-# INLINE hpartition #-}
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,23 +1,58 @@
 {-# LANGUAGE LambdaCase, TemplateHaskell, TypeFamilies, DeriveFunctor #-}
-module Data.Extensible.Record (IsRecord(..), deriveIsRecord) where
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Record
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Bidirectional conversion from/to records
+------------------------------------------------------------------------
+module Data.Extensible.Record (IsRecord(..), toRecord, fromRecord, record, deriveIsRecord) where
 
 import Language.Haskell.TH
 import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+import Data.Extensible.HList
 import Data.Extensible.Product
 import Data.Extensible.Field
 import Data.Functor.Identity
+import Data.Profunctor
 import GHC.TypeLits
 
 -- | The class of types that can be converted to/from a 'Record'.
 class IsRecord a where
   type RecFields a :: [Assoc Symbol *]
-  fromRecord :: Record (RecFields a) -> a
-  toRecord :: a -> Record (RecFields a)
+  recordFromList :: HList (Field Identity) (RecFields a) -> a
+  recordToList :: a -> HList (Field Identity) (RecFields a)
 
+instance IsRecord () where
+  type RecFields () = '[]
+  recordFromList _ = ()
+  recordToList _ = HNil
+
+-- | Convert a value into a 'Record'.
+toRecord :: IsRecord a => a -> Record (RecFields a)
+toRecord = fromHList . recordToList
+{-# INLINE toRecord #-}
+
+-- | Convert a 'Record' to a value.
+fromRecord :: IsRecord a => Record (RecFields a) -> a
+fromRecord = recordFromList . toHList
+{-# INLINE fromRecord #-}
+
+-- | @record :: IsRecord a => Iso' a (Record (RecFields a)) @
+record :: (IsRecord a, Functor f, Profunctor p)
+  => Optic' p f a (Record (RecFields a))
+record = dimap toRecord (fmap fromRecord)
+{-# INLINE record #-}
+
 tvName :: TyVarBndr -> Name
 tvName (PlainTV n) = n
 tvName (KindedTV n _) = n
 
+-- | Create an 'IsRecord' instance for a normal record declaration.
 deriveIsRecord :: Name -> DecsQ
 deriveIsRecord name = reify name >>= \case
 #if MIN_VERSION_template_haskell(2,11,0)
@@ -43,16 +78,14 @@
             (\(v, _, t) r -> PromotedConsT `AppT` (PromotedT '(:>) `AppT` LitT (StrTyLit $ nameBase v) `AppT` refineTV t) `AppT` r)
             PromotedNilT
             vst
-        , FunD 'fromRecord [Clause
-            [shape2Pat $ fmap (\x -> ConP 'Field [ConP 'Identity [VarP x]]) $ foldr consShape SNil newNames]
+        , FunD 'recordFromList [Clause
+            [shape2Pat $ fmap (\x -> ConP 'Field [ConP 'Identity [VarP x]]) newNames]
             (NormalB $ RecConE conName [(n, VarE n') | (n, n') <- zip names newNames])
             []
             ]
-        , FunD 'toRecord [Clause
+        , FunD 'recordToList [Clause
             [VarP rec]
-            (NormalB $ shape2Exp
-              $ foldr consShape SNil
-              [AppE (ConE 'Field)
+            (NormalB $ shape2Exp [AppE (ConE 'Field)
                 $ AppE (ConE 'Identity)
                 $ VarE n `AppE` VarE rec
               | n <- names])
@@ -62,18 +95,10 @@
       ]
   info -> fail $ "deriveAsRecord: Unsupported " ++ show info
 
-shape2Pat :: Shape Pat -> Pat
-shape2Pat SNil = ConP 'Nil []
-shape2Pat (STree p l r) = ConP 'Tree [p, shape2Pat l, shape2Pat r]
-
-shape2Exp :: Shape Exp -> Exp
-shape2Exp SNil = ConE 'Nil
-shape2Exp (STree e l r) = ConE 'Tree `AppE` e `AppE` shape2Exp l `AppE` shape2Exp r
-
-data Shape a = SNil
-    | STree a (Shape a) (Shape a)
-    deriving Functor
+shape2Pat :: [Pat] -> Pat
+shape2Pat [] = ConP 'HNil []
+shape2Pat (x : xs) = ConP 'HCons [x, shape2Pat xs]
 
-consShape :: a -> Shape a -> Shape a
-consShape a SNil = STree a SNil SNil
-consShape a (STree b l r) = STree a (consShape b r) l
+shape2Exp :: [Exp] -> Exp
+shape2Exp [] = ConE 'HNil
+shape2Exp (x : xs) = ConE 'HCons `AppE` x `AppE` shape2Exp xs
diff --git a/src/Data/Extensible/Struct.hs b/src/Data/Extensible/Struct.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Struct.hs
@@ -0,0 +1,211 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns, BangPatterns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MagicHash, UnboxedTuples #-}
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Struct
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Mutable structs
+------------------------------------------------------------------------
+module Data.Extensible.Struct (
+  -- * Mutable struct
+  Struct
+  , set
+  , get
+  , new
+  , newRepeat
+  , newFor
+  , newFromHList
+  -- * Immutable product
+  , (:*)
+  , unsafeFreeze
+  , newFrom
+  , hlookup
+  , hlength
+  , hfoldrWithIndex
+  , thaw
+  , hfrozen
+  , toHList) where
+
+import GHC.Prim
+import Control.Monad.Primitive
+import Control.Monad.ST
+import Data.Constraint
+import Data.Extensible.Class
+import Data.Extensible.Internal
+import Control.Comonad
+import Data.Profunctor.Rep
+import Data.Profunctor.Sieve
+import qualified Data.Extensible.HList as L
+import GHC.Types
+
+-- | Mutable type-indexed struct.
+data Struct s (h :: k -> *) (xs :: [k]) = Struct (SmallMutableArray# s Any)
+
+-- | Write a value in a 'Struct'.
+set :: PrimMonad m => Struct (PrimState m) h xs -> Membership xs x -> h x -> m ()
+set (Struct m) (getMemberId -> I# i) e = primitive
+  $ \s -> case unsafeCoerce# writeSmallArray# m i e s of
+    s' -> (# s', () #)
+{-# INLINE set #-}
+
+-- | Read a value from a 'Struct'.
+get :: PrimMonad m => Struct (PrimState m) h xs -> Membership xs x -> m (h x)
+get (Struct m) (getMemberId -> I# i) = primitive $ unsafeCoerce# readSmallArray# m i
+{-# INLINE get #-}
+
+-- | Create a new 'Struct' using the supplied initializer.
+new :: forall h m xs. (PrimMonad m, Generate xs)
+  => (forall x. Membership xs x -> h x)
+  -> m (Struct (PrimState m) h xs)
+new = newDict Dict
+{-# INLINE new #-}
+
+newDict :: PrimMonad m
+  => Dict (Generate xs)
+  -> (forall x. Membership xs x -> h x)
+  -> m (Struct (PrimState m) h xs)
+newDict Dict k = do
+  m <- newRepeat undefined
+  henumerate (\i cont -> set m i (k i) >> cont) $ return m
+{-# NOINLINE[0] newDict #-}
+
+-- | Create a 'Struct' full of the specified value.
+newRepeat :: forall h m xs. (PrimMonad m, Generate xs)
+  => (forall x. h x)
+  -> m (Struct (PrimState m) h xs)
+newRepeat x = do
+  let !(I# n) = hcount (Proxy :: Proxy xs)
+  primitive $ \s -> case newSmallArray# n (unsafeCoerce# x) s of
+    (# s', a #) -> (# s', Struct a #)
+{-# INLINE newRepeat #-}
+
+-- | Create a new 'Struct' using the supplied initializer with a context.
+newFor :: forall proxy c h m xs. (PrimMonad m, Forall c xs)
+  => proxy c
+  -> (forall x. c x => Membership xs x -> h x)
+  -> m (Struct (PrimState m) h xs)
+newFor = newForDict Dict
+{-# INLINE newFor #-}
+
+newForDict :: forall proxy c h m xs. (PrimMonad m)
+  => Dict (Forall c xs)
+  -> proxy c
+  -> (forall x. c x => Membership xs x -> h x)
+  -> m (Struct (PrimState m) h xs)
+newForDict Dict p k = do
+  m <- newRepeat undefined
+  henumerateFor p (Proxy :: Proxy xs) (\i cont -> set m i (k i) >> cont) $ return m
+{-# NOINLINE[0] newForDict #-}
+
+-- | Create a new 'Struct' from an 'HList'.
+newFromHList :: forall h m xs. PrimMonad m => L.HList h xs -> m (Struct (PrimState m) h xs)
+newFromHList l = do
+  let !(I# size) = L.hlength l
+  m <- primitive $ \s -> case newSmallArray# size undefined s of
+    (# s', a #) -> (# s', Struct a #)
+
+  let go :: Int -> L.HList h t -> m ()
+      go _ L.HNil = return ()
+      go i (L.HCons x xs) = set m (unsafeMembership i) x >> go (i + 1) xs
+
+  go 0 l
+  return m
+
+-- | The type of extensible products.
+--
+-- @(:*) :: (k -> *) -> [k] -> *@
+--
+data (h :: k -> *) :* (s :: [k]) = HProduct (SmallArray# Any)
+
+-- | Turn 'Struct' into an immutable product. The original 'Struct' may not be used.
+unsafeFreeze :: PrimMonad m => Struct (PrimState m) h xs -> m (h :* xs)
+unsafeFreeze (Struct m) = primitive $ \s -> case unsafeFreezeSmallArray# m s of
+  (# s', a #) -> (# s', HProduct a #)
+{-# INLINE unsafeFreeze #-}
+
+-- | Create a new 'Struct' from a product.
+thaw :: PrimMonad m => h :* xs -> m (Struct (PrimState m) h xs)
+thaw (HProduct ar) = primitive $ \s -> case thawSmallArray# ar 0# (sizeofSmallArray# ar) s of
+  (# s', m #) -> (# s', Struct m #)
+
+-- | The size of a product.
+hlength :: h :* xs -> Int
+hlength (HProduct ar) = I# (sizeofSmallArray# ar)
+{-# INLINE hlength #-}
+
+unsafeMembership :: Int -> Membership xs x
+unsafeMembership = unsafeCoerce#
+
+-- | Right-associative fold of a product.
+hfoldrWithIndex :: (forall x. Membership xs x -> h x -> r -> r) -> r -> h :* xs -> r
+hfoldrWithIndex f r p = foldr
+  (\i -> let m = unsafeMembership i in f m (hlookup m p)) r [0..hlength p - 1]
+{-# INLINE hfoldrWithIndex #-}
+
+-- | Convert a product into an 'HList'.
+toHList :: forall h xs. h :* xs -> L.HList h xs
+toHList p = go 0 where
+  go :: Int -> L.HList h xs
+  go i
+    | i == hlength p = unknownHList L.HNil
+    | otherwise = unknownHList $ L.HCons (hlookup (unsafeMembership i) p) (go (i + 1))
+
+  unknownHList :: L.HList h ys -> L.HList h zs
+  unknownHList = unsafeCoerce#
+{-# NOINLINE toHList #-}
+
+-- | Create a new 'Struct' using the contents of a product.
+newFrom :: forall g h m xs. (PrimMonad m)
+  => g :* xs
+  -> (forall x. Membership xs x -> g x -> h x)
+  -> m (Struct (PrimState m) h xs)
+newFrom hp@(HProduct ar) k = do
+  let !n = sizeofSmallArray# ar
+  st <- primitive $ \s -> case newSmallArray# n undefined s of
+    (# s', a #) -> (# s', Struct a #)
+  let go i
+        | i == I# n = return st
+        | otherwise = do
+          let !m = unsafeMembership i
+          set st m $ k m (hlookup m hp)
+          go (i + 1)
+  go 0
+{-# NOINLINE newFrom #-}
+
+{-# RULES "newFrom/newFrom" forall p (f :: forall x. Membership xs x -> f x -> g x)
+ (g :: forall x. Membership xs x -> g x -> h x)
+  . newFrom (hfrozen (newFrom p f)) g = newFrom p (\i x -> g i (f i x)) #-}
+
+{-# RULES "newFrom/newDict" forall d (f :: forall x. Membership xs x -> g x)
+ (g :: forall x. Membership xs x -> g x -> h x)
+  . newFrom (hfrozen (newDict d f)) g = newDict d (\i -> g i (f i)) #-}
+
+{-# RULES "newFrom/newForDict" forall d p (f :: forall x. Membership xs x -> g x)
+ (g :: forall x. Membership xs x -> g x -> h x)
+  . newFrom (hfrozen (newForDict d p f)) g = newForDict d p (\i -> g i (f i)) #-}
+
+-- | Get an element in a product.
+hlookup :: Membership xs x -> h :* xs -> h x
+hlookup (getMemberId -> I# i) (HProduct ar) = case indexSmallArray# ar i of
+  (# a #) -> unsafeCoerce# a
+{-# INLINE hlookup #-}
+
+-- | Create a product from an 'ST' action which returns a 'Struct'.
+hfrozen :: (forall s. ST s (Struct s h xs)) -> h :* xs
+hfrozen m = runST $ m >>= unsafeFreeze
+{-# NOINLINE[0] hfrozen #-}
+
+instance (Corepresentable p, Comonad (Corep p), Functor f) => Extensible f p (:*) where
+  -- | A lens for a value in a known position.
+  pieceAt i pafb = cotabulate $ \ws -> sbt (extract ws) <$> cosieve pafb (hlookup i <$> ws) where
+    sbt xs x = hfrozen $ do
+      s <- thaw xs
+      set s i x
+      return s
+  {-# INLINE pieceAt #-}
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
@@ -6,12 +6,10 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Sum
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Sum (
@@ -22,7 +20,6 @@
   , strikeAt
   , (<:|)
   , exhaust
-  , picked
   , embedAssoc
   ) where
 
@@ -88,14 +85,6 @@
 embedAssoc :: Associate k a xs => h (k ':> a) -> h :| xs
 embedAssoc = EmbedAt association
 {-# INLINE embedAssoc #-}
-
-{-# DEPRECATED picked "Use piece instead" #-}
--- | 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@(EmbedAt i h) = case compareMembership (membership :: Membership xs x) i of
-  Right Refl -> fmap (EmbedAt i) (f h)
-  _ -> pure u
-{-# INLINE picked #-}
 
 instance (Applicative f, Choice p) => Extensible f p (:|) where
   pieceAt m = dimap (\t@(EmbedAt i h) -> case compareMembership i m of
diff --git a/src/Data/Extensible/TH.hs b/src/Data/Extensible/TH.hs
--- a/src/Data/Extensible/TH.hs
+++ b/src/Data/Extensible/TH.hs
@@ -2,21 +2,24 @@
 ------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.TH
--- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
 -- License     :  BSD3
 --
 -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
 --
 ------------------------------------------------------------------------
-module Data.Extensible.TH (mkField, decEffects) where
+module Data.Extensible.TH (mkField
+  , decEffects
+  , decEffectSet
+  , decEffectSuite
+  , customDecEffects) where
 
 import Data.Proxy
 import Data.Extensible.Internal
 import Data.Extensible.Class (itemAssoc)
 import Data.Extensible.Effect
 import Data.Extensible.Field
+import Data.List (nub)
 import Language.Haskell.TH
 import Data.Char
 import Control.Monad
@@ -46,91 +49,151 @@
     ]
 
 -- | Generate named effects from a GADT declaration.
+--
+-- @
+-- decEffects [d|
+--  data Blah a b x where
+--    Blah :: Int -> a -> Blah a b b
+--  |]
+-- @
+--
+-- generates
+--
+-- @
+-- type Blah a b = \"Blah\" >: Action '[Int, a] b
+-- blah :: forall xs a b
+--   . Associate \"Blah\" (Action '[Int, a] b) xs
+--   => Int -> a -> Eff xs b
+-- blah a0 a1
+--   = liftEff
+--     (Data.Proxy.Proxy :: Data.Proxy.Proxy \"Blah\")
+--     (AArgument a0 (AArgument a1 AResult))
+-- @
 decEffects :: DecsQ -> DecsQ
-decEffects decs = decs >>= \ds -> fmap concat $ forM ds $ \case
+decEffects = customDecEffects False True
+
+-- | Instead of making a type synonym for individual actions, it defines a list
+-- of actions.
+decEffectSet :: DecsQ -> DecsQ
+decEffectSet = customDecEffects True False
+
+-- | Generates type synonyms for the set of actions and also individual actions.
+decEffectSuite :: DecsQ -> DecsQ
+decEffectSuite = customDecEffects True True
+
+customDecEffects :: Bool -- ^ generate a synonym of the set of actions
+    -> Bool -- ^ generate synonyms for individual actions
+    -> DecsQ -> DecsQ
+customDecEffects synSet synActions decs = decs >>= \ds -> fmap concat $ forM ds $ \case
 #if MIN_VERSION_template_haskell(2,11,0)
-  DataD _ _ (fmap getTV -> tyvars) _ cs _
+  DataD _ dataName tparams _ cs _
 #else
-  DataD _ _ (fmap getTV -> tyvars) cs _
+  DataD _ dataName tparams cs _
 #endif
-    | not (null tyvars) -> fmap concat $ forM cs $ \case
-      NormalC con st -> mk tyvars [] con st
-      ForallC _ eqs (NormalC con st) -> mk tyvars eqs con st
-      p -> do
-        runIO (print p)
-        fail "Unsupported constructor"
+    -> do
+      (cxts, dcs) <- fmap unzip $ traverse (con2Eff tparams) cs
+
+      let vars = map PlainTV $ nub $ concatMap (varsT . snd) cxts
+      return $ [TySynD dataName vars (typeListT $ map snd cxts) | synSet]
+          ++ [ TySynD k (map PlainTV $ nub $ varsT t) t | synActions, (k, t) <- cxts]
+          ++ concat dcs
   _ -> fail "mkEffects accepts GADT declaration"
-  where
-    mk tyvars eqs con (fmap snd -> argTypes) = do
-#if MIN_VERSION_template_haskell(2,10,0)
-      let dic_ = [(v, t) | AppT (AppT EqualityT (VarT v)) t <- eqs]
-#else
-      let dic_ = [(v, t) | EqualP (VarT v) t <- eqs]
+
+con2Eff :: [TyVarBndr] -> Con -> Q ((Name, Type), [Dec])
+#if MIN_VERSION_template_haskell(2,11,0)
+con2Eff _ (GadtC [name] st (AppT _ resultT))
+  = return $ effectFunD name (map snd st) resultT
 #endif
-      let dic = dic_ ++ [(t, VarT v) | (v, VarT t) <- dic_]
+con2Eff tparams (ForallC _ eqs (NormalC name st))
+  = return $ fromMangledGADT tparams eqs name st
+con2Eff tparams (ForallC _ _ c) = con2Eff tparams c
+con2Eff _ p = do
+  runIO (print p)
+  fail "Unsupported constructor"
 
-      let tvs = map mkName $ concatMap (flip replicateM ['a'..'z']) [1..]
+fromMangledGADT :: [TyVarBndr] -> [Type] -> Name -> [(Strict, Type)] -> ((Name, Type), [Dec])
+fromMangledGADT tyvars_ eqs con fieldTypes
+  = effectFunD con argumentsT result
+  where
+    getTV (PlainTV n) = n
+    getTV (KindedTV n _) = n
 
-      let params' = do
-            (t, v) <- zip tyvars tvs
-            case lookup t dic of
-              Just (VarT p) -> return (t, p)
-              _ -> return (t, v)
+    tyvars = map getTV tyvars_
 
-      let (_, fts) = foldMap (\(p, t) -> maybe ([VarT t], [t]) (\case
-              VarT _ -> ([VarT t], [t])
-              x -> ([x], [])) (lookup p dic)) (init params')
+    dic_ = [(v, t) | AppT (AppT EqualityT (VarT v)) t <- eqs]
+    dic = dic_ ++ [(t, VarT v) | (v, VarT t) <- dic_]
 
-      let argTypes' = map (\case
-            VarT n -> maybe (VarT n) VarT $ lookup n params'
-            x -> x) argTypes
+    params' = do
+      (t, v) <- zip tyvars uniqueNames
+      case lookup t dic of
+        Just (VarT p) -> return (t, p)
+        _ -> return (t, v)
 
-      let (extra, result) = case lookup (last tyvars) dic of
-            Just (VarT v) -> (id, case lookup v params' of
-              Just p -> VarT p
-              Nothing -> VarT v)
-            Just t -> (id, t)
-            Nothing -> ((PlainTV (mkName "x"):), VarT $ mkName "x")
+    argumentsT = map (\case
+      (_, VarT n) -> maybe (VarT n) VarT $ lookup n params'
+      (_, x) -> x) fieldTypes
 
-      -- Eff xs R
-      let rt = ConT ''Eff `AppT` VarT (mkName "xs") `AppT` result
+    result = case lookup (last tyvars) dic of
+      Just (VarT v) -> case lookup v params' of
+        Just p -> VarT p
+        Nothing -> VarT v
+      Just t -> t
+      Nothing -> VarT $ mkName "x"
 
-      -- a -> B -> C -> Eff xs R
-      let fun = foldr (\x y -> ArrowT `AppT` x `AppT` y) rt argTypes'
+varsT :: Type -> [Name]
+varsT (VarT v) = [v]
+varsT (AppT s t) = varsT s ++ varsT t
+varsT _ = []
 
-      -- Action [a, B, C] R
-      let eff = ConT ''Action
-            `AppT` foldr (\x y -> PromotedConsT `AppT` x `AppT` y) PromotedNilT argTypes'
-            `AppT` result
+effectFunD :: Name
+  -> [Type]
+  -> Type
+  -> ((Name, Type), [Dec])
+effectFunD key argumentsT resultT = ((key, PromotedT '(:>) `AppT` nameT `AppT` actionT)
+  , [SigD fName typ, FunD fName [effClause nameT (length argumentsT)]]) where
 
-      -- "Foo"
-      let nameT = LitT $ StrTyLit $ nameBase con
+    varList = mkName "xs"
 
-      -- Associate "Foo" (Foo a B C) xs
-#if MIN_VERSION_template_haskell(2,10,0)
-      let cx = ConT ''Associate
-            `AppT` nameT
-            `AppT` eff
-            `AppT` VarT (mkName "xs")
-#else
-      let cx = ClassP ''Associate [nameT, eff, VarT (mkName "xs")]
-#endif
+    fName = let (ch : rest) = nameBase key in mkName $ toLower ch : rest
 
-      let typ = ForallT (PlainTV (mkName "xs") : extra (map PlainTV fts)) [cx] fun
+    typ = ForallT (map PlainTV $ varList : varsT resultT ++ concatMap varsT argumentsT)
+        [associateT nameT actionT varList]
+        $ effectFunT varList argumentsT resultT
 
-      -- liftEff (Proxy :: Proxy "Foo")
-      let lifter = VarE 'liftEff `AppE` (ConE 'Proxy `SigE` AppT (ConT ''Proxy) nameT)
+    -- Action [a, B, C] R
+    actionT = ConT ''Action `AppT` typeListT argumentsT `AppT` resultT
 
-      let argNames = map (mkName . ("a" ++) . show) [0..length argTypes-1]
+    nameT = LitT $ StrTyLit $ nameBase key
 
-      let ex = lifter
-            `AppE` foldr (\x y -> ConE 'AArgument `AppE` x `AppE` y)
-                         (ConE 'AResult)
-                         (map VarE argNames)
+effectFunT :: Name
+  -> [Type]
+  -> Type
+  -> Type
+effectFunT varList argumentsT resultT
+  = foldr (\x y -> ArrowT `AppT` x `AppT` y) rt argumentsT where
+    rt = ConT ''Eff `AppT` VarT varList `AppT` resultT
 
-      let fName = let (ch : rest) = nameBase con in mkName $ toLower ch : rest
-      return [SigD fName typ
-        , FunD fName [Clause (map VarP argNames) (NormalB ex) []]]
+uniqueNames :: [Name]
+uniqueNames = map mkName $ concatMap (flip replicateM ['a'..'z']) [1..]
 
-    getTV (PlainTV n) = n
-    getTV (KindedTV n _) = n
+typeListT :: [Type] -> Type
+typeListT = foldr (\x y -> PromotedConsT `AppT` x `AppT` y) PromotedNilT
+
+associateT :: Type -- key
+  -> Type -- type
+  -> Name -- variable
+  -> Type
+associateT nameT t xs = ConT ''Associate `AppT` nameT `AppT` t `AppT` VarT xs
+
+effClause :: Type -- effect key
+  -> Int -- number of arguments
+  -> Clause
+effClause nameT n = Clause (map VarP argNames) (NormalB rhs) [] where
+  -- liftEff (Proxy :: Proxy "Foo")
+  lifter = VarE 'liftEff `AppE` (ConE 'Proxy `SigE` AppT (ConT ''Proxy) nameT)
+
+  argNames = map (mkName . ("a" ++) . show) [0..n-1]
+
+  rhs = lifter `AppE` foldr (\x y -> ConE 'AArgument `AppE` x `AppE` y)
+    (ConE 'AResult)
+    (map VarE argNames)
diff --git a/src/Data/Extensible/Tangle.hs b/src/Data/Extensible/Tangle.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Tangle.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE PolyKinds, KindSignatures, TypeOperators, DataKinds, Rank2Types, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Struct
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Extensible tangles
+------------------------------------------------------------------------
+module Data.Extensible.Tangle where
+
+import Control.Monad.Trans.RWS.Strict
+import Control.Monad.Trans.Class
+import Data.Extensible.Class
+import Data.Extensible.Field
+import Data.Extensible.Product
+import Data.Extensible.Internal.Rig
+import Data.Extensible.Nullable
+import Data.Extensible.Wrapper
+
+-- | @'TangleT' h xs m@ is the monad of computations that may depend on the elements in 'xs'.
+newtype TangleT h xs m a = TangleT
+  { unTangleT :: RWST (Comp (TangleT h xs m) h :* xs) () (Nullable h :* xs) m a }
+  deriving (Functor, Applicative, Monad)
+
+instance MonadTrans (TangleT h xs) where
+  lift = TangleT . lift
+
+-- | Hitch an element associated to the 'FieldName' through a wrapper.
+lasso :: forall k v m h xs. (Monad m, Associate k v xs, Wrapper h)
+    => FieldName k -> TangleT h xs m (Repr h (k ':> v))
+lasso _ = view _Wrapper <$> hitchAt (association :: Membership xs (k ':> v))
+{-# INLINE lasso #-}
+
+-- | Take a value from the tangles. The result is memoized.
+hitchAt :: Monad m => Membership xs x -> TangleT h xs m (h x)
+hitchAt k = TangleT $ do
+  mem <- get
+  case getNullable $ hlookup k mem of
+    Just a -> return a
+    Nothing -> do
+      tangles <- ask
+      a <- unTangleT $ getComp $ hlookup k tangles
+      modify $ over (pieceAt k) $ const $ Nullable $ Just a
+      return a
+
+-- | Run a 'TangleT' action and return the result and the calculated values.
+runTangleT :: Monad m
+  => Comp (TangleT h xs m) h :* xs -- ^ tangle matrix
+  -> Nullable h :* xs -- ^ pre-calculated values
+  -> TangleT h xs m a
+  -> m (a, Nullable h :* xs)
+runTangleT tangles rec0 (TangleT m) = (\(a, s, _) -> (a, s))
+  <$> runRWST m tangles rec0
+{-# INLINE runTangleT #-}
+
+-- | Run a 'TangleT' action.
+evalTangleT :: Monad m
+  => Comp (TangleT h xs m) h :* xs -- ^ tangle matrix
+  -> Nullable h :* xs -- ^ pre-calculated values
+  -> TangleT h xs m a
+  -> m a
+evalTangleT tangles rec0 (TangleT m) = fst <$> evalRWST m tangles rec0
+{-# INLINE evalTangleT #-}
+
+-- | Run tangles and collect all the results as a 'Record'.
+runTangles :: Monad m
+  => Comp (TangleT h xs m) h :* xs -- ^ tangle matrix
+  -> Nullable h :* xs -- ^ pre-calculated values
+  -> m (h :* xs)
+runTangles ts vs = evalTangleT ts vs $ htraverseWithIndex (const . hitchAt) vs
+{-# INLINE runTangles #-}
diff --git a/src/Data/Extensible/Wrapper.hs b/src/Data/Extensible/Wrapper.hs
--- a/src/Data/Extensible/Wrapper.hs
+++ b/src/Data/Extensible/Wrapper.hs
@@ -1,74 +1,81 @@
-{-# 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)
-
--- | 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 #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# LANGUAGE TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Wrapper
+-- Copyright   :  (c) Fumiaki Kinoshita 2017
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-----------------------------------------------------------------------------
+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)
+
+-- | 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 #-}
+
+instance Wrapper Maybe where
+    type Repr Maybe a = Maybe a
+    _Wrapper = id
+
+instance Wrapper [] where
+    type Repr [] a = [a]
+    _Wrapper = id
+
+-- | Poly-kinded composition
+newtype Comp (f :: j -> *) (g :: i -> j) (a :: i) = Comp { getComp :: f (g a) } deriving (Show, Eq, Ord, Typeable)
+
+-- | Wrap a result of 'fmap'
+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 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 #-}
diff --git a/tests/effects.hs b/tests/effects.hs
new file mode 100644
--- /dev/null
+++ b/tests/effects.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, DataKinds, FlexibleContexts, TemplateHaskell #-}
+{-# OPTIONS_GHC -ddump-splices #-}
+import Data.Extensible
+
+decEffects [d|
+  data Example a b x where
+    Concrete :: Int -> Example a b ()
+    PolyArg :: a -> Example a b ()
+    PolyRes :: Example a b b
+    PolyArgRes :: a -> Example a b b
+    UnboundArg :: x -> Example a b ()
+    UnboundRes :: Example a b x
+--    ExtArg :: Show s => s -> Example a b ()
+--    ExtRes :: Read s => Example a b s
+  |]
+
+decEffects [d|
+  data Simple x where
+    Simple :: Simple ()
+  |]
+
+main = return ()