diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,7 @@
 .cabal-sandbox/
 cabal.sandbox.config
 cabal.config
+.stack-work
 
 # =========================
 # Operating System Files
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,55 +1,54 @@
-# NB: don't set `language: haskell` here
-
-# See also https://github.com/hvr/multi-ghc-travis for more information
-
-# 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.18 GHCVER=7.8.4
- - CABALVER=1.22 GHCVER=7.10.1
-
-# Note: the distinction between `before_install` and `install` is not
-#       important.
-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
- - 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
-
-# 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
-
- # this builds all libraries and executables
- # (including tests/benchmarks)
- - cabal build
-
- - cabal test
- - cabal check
-
- # tests that a source-distribution can be generated
- - cabal sdist
-
- # 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
-
-# EOF
+# NB: don't set `language: haskell` here
+
+# See also https://github.com/hvr/multi-ghc-travis for more information
+
+# 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
+
+# Note: the distinction between `before_install` and `install` is not
+#       important.
+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
+ - 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
+
+# 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
+
+ # this builds all libraries and executables
+ # (including tests/benchmarks)
+ - cabal build
+
+ - cabal test
+ - cabal check
+
+ # tests that a source-distribution can be generated
+ - cabal sdist
+
+ # 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
+
+# EOF
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,16 @@
+0.3.7
+-----------------------------------------------------
+* Support GHC 8.0
+* Added a `Monoid` instance for `Field`
+* Added `Data.Extensible.Record`
+* Added `Enum` and `Bounded` instances for `Proxy :| xs`
+* Removed `Data.Extensible.Union`
+
+0.3.6
+-----------------------------------------------------
+* Added `(@:>)`
+* Added `(!-!!)`, `nihility`, `squash`
+
 0.3.5
 -----------------------------------------------------
 * Added `Data.Extensible.Effect`
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,10 +4,6 @@
 [![Build Status](https://travis-ci.org/fumieval/extensible.svg?branch=master)](https://travis-ci.org/fumieval/extensible)
 [![Hackage](https://budueba.com/hackage/extensible)](https://hackage.haskell.org/package/extensible)
 
-This package provides extensible poly-kinded data types, including records and polymorphic open unions.
-
-It focuses on being neat and fast.
-
-![Benchmark](benchmark-accessing.png)
+This package provides extensible poly-kind records and variants.
 
 Bug reports and contributions are welcome!
diff --git a/benchmarks/AtoZ.hs b/benchmarks/AtoZ.hs
deleted file mode 100644
--- a/benchmarks/AtoZ.hs
+++ /dev/null
@@ -1,108 +0,0 @@
-{-# LANGUAGE DataKinds, TypeOperators, GADTs, BangPatterns #-}
-module AtoZ where
-import Data.Extensible
-import Data.HList hiding (K(..))
-import Data.Coerce
-data A = A Int deriving Show
-data B = B Int deriving Show
-data C = C Int deriving Show
-data D = D Int deriving Show
-data E = E Int deriving Show
-data F = F Int deriving Show
-data G = G Int deriving Show
-data H = H Int deriving Show
-data I = I Int deriving Show
-data J = J Int deriving Show
-data K = K Int deriving Show
-data L = L Int deriving Show
-data M = M Int deriving Show
-data N = N Int deriving Show
-data O = O Int deriving Show
-data P = P Int deriving Show
-data Q = Q Int deriving Show
-data R = R Int deriving Show
-data S = S Int deriving Show
-data T = T Int deriving Show
-data U = U Int deriving Show
-data V = V Int deriving Show
-data W = W Int deriving Show
-data X = X Int deriving Show
-data Y = Y Int deriving Show
-data Z = Z Int deriving Show
-
-type AtoZ = [A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z]
-
-extensible26 :: K0 :* AtoZ
-extensible26 = A 0 <% B 1 <% C 2 <% D 3 <% E 4 <% F 5 <% G 6
-  <% H 7 <% I 8 <% J 9 <% K 10 <% L 11 <% M 12 <% N 13
-  <% O 14 <% P 15 <% Q 16 <% R 17 <% S 18 <% T 19 <% U 20
-  <% V 21 <% W 22 <% X 23 <% Y 24 <% Z 25 <% Nil
-
-data Data26 = Data26
-  { getA :: A
-  , getB :: B
-  , getC :: C
-  , getD :: D
-  , getE :: E
-  , getF :: F
-  , getG :: G
-  , getH :: H
-  , getI :: I
-  , getJ :: J
-  , getK :: K
-  , getL :: L
-  , getM :: M
-  , getN :: N
-  , getO :: O
-  , getP :: P
-  , getQ :: Q
-  , getR :: R
-  , getS :: S
-  , getT :: T
-  , getU :: U
-  , getV :: V
-  , getW :: W
-  , getX :: X
-  , getY :: Y
-  , getZ :: Z
-  }
-
-data26 :: Data26
-data26 = Data26 (A 0) (B 1) (C 2) (D 3) (E 4) (F 5) (G 6) (H 7) (I 8) (J 9) (K 10)
-  (L 11) (M 12) (N 13) (O 14) (P 15) (Q 16) (R 17) (S 18) (T 19) (U 20) (V 21)
-  (W 22) (X 23) (Y 24) (Z 25)
-
-hlist26 :: HList AtoZ
-hlist26 = A 0 `HCons` B 1 `HCons` C 2 `HCons` D 3 `HCons` E 4 `HCons` F 5 `HCons` G 6
-  `HCons` H 7 `HCons` I 8 `HCons` J 9 `HCons` K 10 `HCons` L 11 `HCons` M 12 `HCons` N 13
-  `HCons` O 14 `HCons` P 15 `HCons` Q 16 `HCons` R 17 `HCons` S 18 `HCons` T 19 `HCons` U 20
-  `HCons` V 21 `HCons` W 22 `HCons` X 23 `HCons` Y 24 `HCons` Z 25 `HCons` HNil
-
-match26 :: Match K0 Int :* AtoZ
-match26 = (\(A n) -> n)
-  <?% (\(B n) -> n)
-  <?% (\(C n) -> n)
-  <?% (\(D n) -> n)
-  <?% (\(E n) -> n)
-  <?% (\(F n) -> n)
-  <?% (\(G n) -> n)
-  <?% (\(H n) -> n)
-  <?% (\(I n) -> n)
-  <?% (\(J n) -> n)
-  <?% (\(K n) -> n)
-  <?% (\(L n) -> n)
-  <?% (\(M n) -> n)
-  <?% (\(N n) -> n)
-  <?% (\(O n) -> n)
-  <?% (\(P n) -> n)
-  <?% (\(Q n) -> n)
-  <?% (\(R n) -> n)
-  <?% (\(S n) -> n)
-  <?% (\(T n) -> n)
-  <?% (\(U n) -> n)
-  <?% (\(V n) -> n)
-  <?% (\(W n) -> n)
-  <?% (\(X n) -> n)
-  <?% (\(Y n) -> n)
-  <?% (\(Z n) -> n)
-  <?% Nil
diff --git a/benchmarks/membership.hs b/benchmarks/membership.hs
deleted file mode 100644
--- a/benchmarks/membership.hs
+++ /dev/null
@@ -1,112 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, ViewPatterns, TypeFamilies, TypeOperators, GADTs, Rank2Types, ScopedTypeVariables, DataKinds #-}
-import Data.Extensible
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Control.Applicative
-import Criterion.Main
-import AtoZ
-import Data.HList hiding (K(..))
-import Unsafe.Coerce
-
-data Sum = C0 A|C1 B|C2 C|C3 D|C4 E|C5 F|C6 G|C7 H|C8 I|C9 J|C10 K |C11 L|C12 M
-  |C13 N|C14 O|C15 P|C16 Q|C17 R|C18 S|C19 T|C20 U|C21 V|C22 W|C23 X|C24 Y|C25 Z
-
-testNaive :: Sum -> Int
-testNaive (C0 (A n)) = n
-testNaive (C1 (B n)) = n
-testNaive (C2 (C n)) = n
-testNaive (C3 (D n)) = n
-testNaive (C4 (E n)) = n
-testNaive (C5 (F n)) = n
-testNaive (C6 (G n)) = n
-testNaive (C7 (H n)) = n
-testNaive (C8 (I n)) = n
-testNaive (C9 (J n)) = n
-testNaive (C10 (K n)) = n
-testNaive (C11 (L n)) = n
-testNaive (C12 (M n)) = n
-testNaive (C13 (N n)) = n
-testNaive (C14 (O n)) = n
-testNaive (C15 (P n)) = n
-testNaive (C16 (Q n)) = n
-testNaive (C17 (R n)) = n
-testNaive (C18 (S n)) = n
-testNaive (C19 (T n)) = n
-testNaive (C20 (U n)) = n
-testNaive (C21 (V n)) = n
-testNaive (C22 (W n)) = n
-testNaive (C23 (X n)) = n
-testNaive (C24 (Y n)) = n
-testNaive (C25 (Z n)) = n
-
-testExt :: K0 :| AtoZ -> Int
-testExt = match match26
-
-main = defaultMain [
-   bgroup "product" [
-     bench "Data"  $ whnf (\(getZ -> Z x) -> x) data26
-    , bench "A" $ whnf (\(pluck -> A x) -> x) extensible26
-    , bench "B"  $ whnf (\(pluck -> B x) -> x) extensible26
-    , bench "C"  $ whnf (\(pluck -> C x) -> x) extensible26
-    , bench "D"  $ whnf (\(pluck -> D x) -> x) extensible26
-    , bench "E"  $ whnf (\(pluck -> E x) -> x) extensible26
-    , bench "F"  $ whnf (\(pluck -> F x) -> x) extensible26
-    , bench "G"  $ whnf (\(pluck -> G x) -> x) extensible26
-    , bench "H"  $ whnf (\(pluck -> H x) -> x) extensible26
-    , bench "I"  $ whnf (\(pluck -> I x) -> x) extensible26
-    , bench "J"  $ whnf (\(pluck -> J x) -> x) extensible26
-    , bench "K"  $ whnf (\(pluck -> K x) -> x) extensible26
-    , bench "L"  $ whnf (\(pluck -> L x) -> x) extensible26
-    , bench "M"  $ whnf (\(pluck -> M x) -> x) extensible26
-    , bench "N"  $ whnf (\(pluck -> N x) -> x) extensible26
-    , bench "O"  $ whnf (\(pluck -> O x) -> x) extensible26
-    , bench "P"  $ whnf (\(pluck -> P x) -> x) extensible26
-    , bench "Q"  $ whnf (\(pluck -> Q x) -> x) extensible26
-    , bench "R"  $ whnf (\(pluck -> R x) -> x) extensible26
-    , bench "S"  $ whnf (\(pluck -> S x) -> x) extensible26
-    , bench "T"  $ whnf (\(pluck -> T x) -> x) extensible26
-    , bench "U"  $ whnf (\(pluck -> U x) -> x) extensible26
-    , bench "V"  $ whnf (\(pluck -> V x) -> x) extensible26
-    , bench "W"  $ whnf (\(pluck -> W x) -> x) extensible26
-    , bench "X"  $ whnf (\(pluck -> X x) -> x) extensible26
-    , bench "Y"  $ whnf (\(pluck -> Y x) -> x) extensible26
-    , bench "Z"  $ whnf (\(pluck -> Z x) -> x) extensible26
-    , bench "A"  $ whnf (\(hOccursFst -> A x) -> x) hlist26
-    , bench "B"  $ whnf (\(hOccursFst -> B x) -> x) hlist26
-    , bench "C"  $ whnf (\(hOccursFst -> C x) -> x) hlist26
-    , bench "D"  $ whnf (\(hOccursFst -> D x) -> x) hlist26
-    , bench "E"  $ whnf (\(hOccursFst -> E x) -> x) hlist26
-    , bench "F"  $ whnf (\(hOccursFst -> F x) -> x) hlist26
-    , bench "G"  $ whnf (\(hOccursFst -> G x) -> x) hlist26
-    , bench "H"  $ whnf (\(hOccursFst -> H x) -> x) hlist26
-    , bench "I"  $ whnf (\(hOccursFst -> I x) -> x) hlist26
-    , bench "J"  $ whnf (\(hOccursFst -> J x) -> x) hlist26
-    , bench "K"  $ whnf (\(hOccursFst -> K x) -> x) hlist26
-    , bench "L"  $ whnf (\(hOccursFst -> L x) -> x) hlist26
-    , bench "M"  $ whnf (\(hOccursFst -> M x) -> x) hlist26
-    , bench "N"  $ whnf (\(hOccursFst -> N x) -> x) hlist26
-    , bench "O"  $ whnf (\(hOccursFst -> O x) -> x) hlist26
-    , bench "P"  $ whnf (\(hOccursFst -> P x) -> x) hlist26
-    , bench "Q"  $ whnf (\(hOccursFst -> Q x) -> x) hlist26
-    , bench "R"  $ whnf (\(hOccursFst -> R x) -> x) hlist26
-    , bench "S"  $ whnf (\(hOccursFst -> S x) -> x) hlist26
-    , bench "T"  $ whnf (\(hOccursFst -> T x) -> x) hlist26
-    , bench "U"  $ whnf (\(hOccursFst -> U x) -> x) hlist26
-    , bench "V"  $ whnf (\(hOccursFst -> V x) -> x) hlist26
-    , bench "W"  $ whnf (\(hOccursFst -> W x) -> x) hlist26
-    , bench "X"  $ whnf (\(hOccursFst -> X x) -> x) hlist26
-    , bench "Y"  $ whnf (\(hOccursFst -> Y x) -> x) hlist26
-    , bench "Z"  $ whnf (\(hOccursFst -> Z x) -> x) hlist26
-    ]
-  , bgroup "sum" [
-     bench "A" $ whnf testExt (bury (A 0))
-    , bench "M" $ whnf testExt (bury (M 0))
-    , bench "T" $ whnf testExt (bury (T 0))
-    , bench "Z" $ whnf testExt (bury (Z 0))
-    , bench "A_" $ whnf testNaive  (C0 (A 0))
-    , bench "M_" $ whnf testNaive (C12 (M 0))
-    , bench "T_" $ whnf testNaive (C19 (T 0))
-    , bench "Z_" $ whnf testNaive (C25 (Z 0))
-    ]
-
-  ]
diff --git a/examples/effect.hs b/examples/effect.hs
--- a/examples/effect.hs
+++ b/examples/effect.hs
@@ -2,10 +2,19 @@
 import Data.Extensible
 
 decEffects [d|
-  data Example x where
+  data Example x where -- the name doesn't matter
     Foo :: Int -> Example ()
     Bar :: Example String
     Baz :: Bool -> Bool -> Example Int
     |]
 
 mkField "Foo Bar Baz"
+
+test :: (Associate "Foo" (Action '[Int] ()) xs
+  , Associate "Bar" (Action '[] String) xs
+  , Associate "Baz" (Action '[Bool, Bool] Int) xs) => Eff xs Int
+test = do
+  foo 42
+  s <- bar
+  t <- bar
+  baz (s == "bar") (s == t)
diff --git a/examples/records-plain.hs b/examples/records-plain.hs
deleted file mode 100644
--- a/examples/records-plain.hs
+++ /dev/null
@@ -1,43 +0,0 @@
-{-# LANGUAGE TemplateHaskell, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts #-}
-
-import Data.Extensible
-import Control.Lens
-decFieldsDeriving [''Show, ''Eq, ''Ord] [d|
-  type Name = String
-  type Weight = Float
-  type Price = Int
-  type Description = String
-  type Featured = Bool
-  type Quantity = Int
-  |]
-
-type Stock = AllOf '[Name, Weight, Price, Featured, Description, Quantity]
-
-s0 :: Stock
-s0 = Name "DA-192H"
-  <% Weight 260
-  <% Price 120
-  <% Featured True
-  <% Description "High-quality (24bit 192kHz), lightweight portable DAC"
-  <% Quantity 20
-  <% Nil
-
--- Use shrink to permute elements
-s1 :: Stock
-s1 = shrink
-   $ Name "HHP-150"
-  <% Featured False
-  <% Description "Premium wooden headphone"
-  <% Weight 150
-  <% Price 330
-  <% Quantity 55
-  <% Nil
-
--- If Quantity is missing,
---    Couldn't match type ‘Missing Quantity’ with ‘Expecting one’
---
--- If there are duplicate Quantity,
---    Couldn't match type ‘Ambiguous Quantity’ with ‘Expecting one’
-
-printSummary :: (Name ∈ s, Description ∈ s) => AllOf s -> IO ()
-printSummary s = putStrLn $ view name s ++ ": " ++ view description s
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,21 +1,20 @@
 name:                extensible
-version:             0.3.5
-synopsis:            Extensible, efficient, lens-friendly data types
+version:             0.3.7
+synopsis:            Extensible, efficient, optics-friendly data types
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
-description:         Combinators and types for extensible product and sum
+description:         Poly-kinded extensible records and variants
 license:             BSD3
 license-file:        LICENSE
 author:              Fumiaki Kinoshita
 maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
-copyright:           Copyright (C) 2015 Fumiaki Kinoshita
+copyright:           Copyright (C) 2016 Fumiaki Kinoshita
 category:            Data, Records
 build-type:          Simple
-stability:           provisional
+stability:           experimental
 
 extra-source-files:
   examples/*.hs
-  benchmarks/*.hs
   .gitignore
   .travis.yml
   README.md
@@ -40,8 +39,8 @@
     Data.Extensible.Nullable
     Data.Extensible.Plain
     Data.Extensible.Product
+    Data.Extensible.Record
     Data.Extensible.Sum
-    Data.Extensible.Union
     Data.Extensible.Wrapper
     Data.Extensible.TH
   default-extensions: TypeOperators
@@ -55,7 +54,13 @@
     , FlexibleInstances
     , PolyKinds
     , CPP
-  build-depends:       base >= 4.7 && <5, template-haskell, constraints, profunctors, tagged, transformers, monad-skeleton
+  build-depends:       base >= 4.7 && <5
+    , template-haskell
+    , constraints
+    , profunctors
+    , tagged
+    , transformers
+    , monad-skeleton >= 0.1.2
   hs-source-dirs:      src
   ghc-options: -Wall
   default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -20,9 +20,9 @@
   , module Data.Extensible.Nullable
   , module Data.Extensible.Plain
   , module Data.Extensible.Product
+  , module Data.Extensible.Record
   , module Data.Extensible.Sum
   , module Data.Extensible.TH
-  , module Data.Extensible.Union
   , module Data.Extensible.Wrapper
   ) where
 
@@ -35,7 +35,7 @@
 import Data.Extensible.Nullable
 import Data.Extensible.Plain
 import Data.Extensible.Product
+import Data.Extensible.Record
 import Data.Extensible.Sum
 import Data.Extensible.TH
-import Data.Extensible.Union
 import Data.Extensible.Wrapper
diff --git a/src/Data/Extensible/Class.hs b/src/Data/Extensible/Class.hs
--- a/src/Data/Extensible/Class.hs
+++ b/src/Data/Extensible/Class.hs
@@ -24,7 +24,11 @@
   -- * Member
   , Member(..)
   , remember
+#if __GLASGOW_HASKELL__ >= 800
+  , type (∈)
+#else
   , (∈)()
+#endif
   , FindType
   -- * Association
   , Assoc(..)
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
--- a/src/Data/Extensible/Dictionary.hs
+++ b/src/Data/Extensible/Dictionary.hs
@@ -1,5 +1,9 @@
 {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
 {-# LANGUAGE UndecidableInstances, MultiParamTypeClasses #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE UndecidableSuperClasses #-}
+#endif
+
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -----------------------------------------------------------------------
 --
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,64 +1,95 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
-module Data.Extensible.Effect (Instruction(..)
-  , Eff
-  , liftEff
-  , hoistEff
-  , handleWith
-  , Handler(..)
-  -- * Unnamed actions
-  , Action(..)
-  , Function
-  , receive) 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 #-}
+{-# 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 #-}
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,5 +1,8 @@
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE UndecidableSuperClasses #-}
+#endif
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Record
@@ -17,6 +20,7 @@
   Field(..)
   , (@=)
   , (<@=>)
+  , (@:>)
   , FieldOptic
   , FieldName
   -- * Records and variants
@@ -28,10 +32,11 @@
   -- * Matching
   , matchWithField
   , matchField
-  -- * Constraint
+  -- * Key / value
   , AssocKey
   , AssocValue
   , KeyValue
+  , proxyAssocKey
   -- * Internal
   , LabelPhantom
   , Labelling
@@ -49,9 +54,15 @@
 import Data.Functor.Identity
 import GHC.TypeLits hiding (Nat)
 
+-- | Take the type of the key
 type family AssocKey (kv :: Assoc k v) :: k where
   AssocKey (k ':> v) = k
 
+-- | Proxy-level 'AssocKey'. This is useful when using 'symbolVal'.
+proxyAssocKey :: proxy kv -> Proxy (AssocKey kv)
+proxyAssocKey _ = Proxy
+
+-- | Take the type of the value
 type family AssocValue (kv :: Assoc k v) :: v where
   AssocValue (k ':> v) = v
 
@@ -59,7 +70,7 @@
 
 instance (pk k, pv v) => KeyValue pk pv (k ':> v)
 
--- | A @'Field' h (k ':> v)@ is @h v@, but is along with the index @k@.
+-- | A @'Field' h (k ':> v)@ is @h v@ annotated with the field name @k@.
 --
 -- @'Field' :: (v -> *) -> Assoc k v -> *@
 --
@@ -76,6 +87,12 @@
     . 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] -> *@
@@ -99,6 +116,7 @@
 emptyRecord = Nil
 {-# INLINE emptyRecord #-}
 
+-- | Select a corresponding field of a variant.
 matchWithField :: (forall x. f x -> g x -> r) -> RecordOf f xs -> VariantOf g xs -> r
 matchWithField h = matchWith (\(Field x) (Field y) -> h x y)
 {-# INLINE matchWithField #-}
@@ -122,7 +140,12 @@
 --
 -- 'FieldOptic's can be generated using 'mkField' defined in the "Data.Extensible.TH" module.
 --
-type FieldOptic k = forall f p t xs (h :: kind -> *) (v :: kind). (Extensible f p t
+#if __GLASGOW_HASKELL__ >= 800
+type FieldOptic k = forall kind. forall f p t xs (h :: kind -> *) (v :: kind).
+#else
+type FieldOptic k = forall f p t xs (h :: kind -> *) (v :: kind).
+#endif
+  (Extensible f p t
   , Associate k v xs
   , Labelling k p
   , Wrapper h)
@@ -159,3 +182,8 @@
 (<@=>) k = Comp #. fmap (k @=)
 {-# INLINE (<@=>) #-}
 infix 1 <@=>
+
+-- | Annotate a value by the field name without 'Wrapper'.
+(@:>) :: FieldName k -> h v -> Field h (k ':> v)
+(@:>) _ = Field
+infix 1 @:>
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -13,7 +13,11 @@
 ------------------------------------------------------------------------
 module Data.Extensible.Inclusion (
   -- * Inclusion
-   (⊆)()
+#if __GLASGOW_HASKELL__ >= 800
+  type (⊆)
+#else
+  (⊆)()
+#endif
   , Include
   , inclusion
   , shrink
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,260 +1,281 @@
-{-# 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
-  , runMembership
-  , compareMembership
-  -- * Member class
-  , Member(..)
-  , remember
-  , (∈)()
-  , FindType
-  -- * Association
-  , Assoc(..)
-  , Associate(..)
-  , FindAssoc
-  -- * Sugar
-  , Elaborate
-  , Elaborated(..)
-  -- * Tree navigation
-  , NavHere(..)
-  , navigate
-  , here
-  , navNext
-  , navL
-  , navR
-  -- * Miscellaneous
-  , Nat(..)
-  , KnownPosition(..)
-  , Succ
-  , Half
-  , Head
-  , Tail
-  , (++)()
-  , 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 #-}
-
--- | 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 #-}
-
--- | 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 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 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
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Record.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE LambdaCase, TemplateHaskell, TypeFamilies, DeriveFunctor #-}
+module Data.Extensible.Record (IsRecord(..), deriveIsRecord) where
+
+import Language.Haskell.TH
+import Data.Extensible.Internal
+import Data.Extensible.Product
+import Data.Extensible.Field
+import Data.Functor.Identity
+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)
+
+tvName :: TyVarBndr -> Name
+tvName (PlainTV n) = n
+tvName (KindedTV n _) = n
+
+deriveIsRecord :: Name -> DecsQ
+deriveIsRecord name = reify name >>= \case
+#if MIN_VERSION_template_haskell(2,11,0)
+  TyConI (DataD _ _ vars _ [RecC conName vst] _) -> do
+#else
+  TyConI (DataD _ _ vars [RecC conName vst] _) -> do
+#endif
+    rec <- newName "rec"
+    let names = [x | (x, _, _) <- vst]
+    newNames <- traverse (newName . nameBase) names
+    let tvmap = [(tvName tv, VarT (mkName $ "p" ++ show i)) | (i, tv) <- zip [0 :: Int ..] vars]
+    let ty = foldl AppT (ConT name) $ map snd tvmap
+    let refineTV (VarT t) | Just t' <- lookup t tvmap = t'
+        refineTV (AppT a b) = refineTV a `AppT` refineTV b
+        refineTV t = t
+    return
+#if MIN_VERSION_template_haskell(2,11,0)
+      [InstanceD Nothing [] (ConT ''IsRecord `AppT` ty)
+#else
+      [InstanceD [] (ConT ''IsRecord `AppT` ty)
+#endif
+        [ TySynInstD ''RecFields $ TySynEqn [ty] $ foldr
+            (\(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]
+            (NormalB $ RecConE conName [(n, VarE n') | (n, n') <- zip names newNames])
+            []
+            ]
+        , FunD 'toRecord [Clause
+            [VarP rec]
+            (NormalB $ shape2Exp
+              $ foldr consShape SNil
+              [AppE (ConE 'Field)
+                $ AppE (ConE 'Identity)
+                $ VarE n `AppE` VarE rec
+              | n <- names])
+            []
+            ]
+        ]
+      ]
+  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
+
+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
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
@@ -2,6 +2,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Sum
@@ -23,7 +24,6 @@
   , exhaust
   , picked
   , embedAssoc
-  , pattern UnionAt
   ) where
 
 import Data.Extensible.Internal
@@ -42,8 +42,13 @@
   EmbedAt :: !(Membership xs x) -> h x -> h :| xs
 deriving instance Typeable (:|)
 
-{-# DEPRECATED UnionAt "This has renamed to EmbedAt" #-}
-pattern UnionAt a b = EmbedAt a b
+instance Enum (Proxy :| xs) where
+  fromEnum (EmbedAt m _) = fromIntegral $ getMemberId m
+  toEnum i = reifyMembership (fromIntegral i) $ \m -> EmbedAt m Proxy
+
+instance (Last xs ∈ xs) => Bounded (Proxy :| xs) where
+  minBound = reifyMembership 0 $ \m -> EmbedAt m Proxy
+  maxBound = EmbedAt (membership :: Membership xs (Last xs)) Proxy
 
 -- | Change the wrapper.
 hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs
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
@@ -10,18 +10,15 @@
 -- Portability :  non-portable
 --
 ------------------------------------------------------------------------
-module Data.Extensible.TH (mkField, decFields, decFieldsDeriving, decEffects) where
+module Data.Extensible.TH (mkField, decEffects) where
 
 import Data.Proxy
 import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig (Optic')
-import Data.Extensible.Class (Extensible, itemAssoc)
+import Data.Extensible.Class (itemAssoc)
 import Data.Extensible.Effect
 import Data.Extensible.Field
-import Data.Extensible.Plain (accessing)
 import Language.Haskell.TH
 import Data.Char
-import Data.Functor.Identity
 import Control.Monad
 
 #if !MIN_VERSION_base(4,8,0)
@@ -48,57 +45,14 @@
     , return $ PragmaD $ InlineP name Inline FunLike AllPhases
     ]
 
--- | Generate newtype wrappers and lenses from type synonyms.
---
--- @
--- decFields [d|type Foo = Int|]
--- @
---
--- Generates:
---
--- @
--- newtype Foo = Foo Int
--- foo :: (Foo ∈ xs) => Lens' (AllOf xs) Int
--- foo = accessing Foo
--- @
---
-decFields :: DecsQ -> DecsQ
-decFields = decFieldsDeriving []
-
--- | 'decFields' with additional deriving clauses
-decFieldsDeriving :: [Name] -> DecsQ -> DecsQ
-decFieldsDeriving drv' ds = ds >>= fmap concat . mapM mkBody
-  where
-    mkBody (NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) drv) = do
-      let name = let (x:xs) = nameBase name_ in mkName $ toLower x : xs
-          xs_ = mkName "xs"
-          f_ = mkName "f"
-          p_ = mkName "p"
-          t_ = mkName "t"
-          ext = varT t_ `appT` conT ''Identity `appT` varT xs_
-          tvs' = PlainTV xs_ : PlainTV f_ : PlainTV p_ : PlainTV t_ : tvs
-      sequence [return $ NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) (drv' ++ drv)
-
-        ,sigD name
-#if MIN_VERSION_template_haskell(2,10,0)
-          $ forallT tvs' (sequence [conT ''Member `appT` varT xs_ `appT` conT name_
-            , conT ''Extensible `appT` varT f_ `appT` varT p_ `appT` varT t_])
-#else
-          $ forallT tvs' (sequence [classP ''Member [varT xs_, conT name_]
-            , classP ''Extensible [varT f_, varT p_, varT t_]])
-#endif
-          $ conT ''Optic' `appT` varT p_ `appT` varT f_ `appT` ext `appT` return ty
-
-        , valD (varP name) (normalB $ varE 'accessing `appE` conE nc) []
-        , return $ PragmaD $ InlineP name Inline FunLike AllPhases
-        ]
-    mkBody (TySynD name_ tvs ty) = mkBody (NewtypeD [] name_ tvs (NormalC (mkName (nameBase name_)) [(NotStrict, ty)]) [])
-    mkBody _ = fail "Unsupported declaration: genField handles newtype declarations or type synonyms"
-
 -- | Generate named effects from a GADT declaration.
 decEffects :: DecsQ -> DecsQ
 decEffects decs = decs >>= \ds -> fmap concat $ forM ds $ \case
+#if MIN_VERSION_template_haskell(2,11,0)
+  DataD _ _ (fmap getTV -> tyvars) _ cs _
+#else
   DataD _ _ (fmap getTV -> tyvars) 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
diff --git a/src/Data/Extensible/Union.hs b/src/Data/Extensible/Union.hs
deleted file mode 100644
--- a/src/Data/Extensible/Union.hs
+++ /dev/null
@@ -1,51 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.Union
--- Copyright   :  (c) Fumiaki Kinoshita 2015
--- License     :  BSD3
---
--- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Polymorphic open unions
-------------------------------------------------------------------------
-module Data.Extensible.Union (K1(..), Union(..), Gondola(..), reunion, rung, runGondolas) where
-
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Data.Extensible.Class
-import Data.Extensible.Sum
-import Data.Extensible.Product
-import Data.Extensible.Wrapper
-import Data.Profunctor
-import Data.Typeable (Typeable)
-
--- | Wrap a type that has a kind @* -> *@.
-newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
-
-instance Wrapper (K1 a) where
-  type Repr (K1 a) f = f a
-  _Wrapper = dimap getK1 (fmap K1)
-  {-# INLINE _Wrapper #-}
-
-newtype Union xs a = Union { getUnion :: K1 a :| xs }
-
-reunion :: Gondola m :* xs -> Union xs a -> m a
-reunion gs = \(Union (EmbedAt i (K1 f))) -> views (pieceAt i) runGondola gs f
-{-# INLINE reunion #-}
-
--- | Transformation between effects
-newtype Gondola f g = Gondola { runGondola :: forall a. g a -> f a }
-
--- | Add a new transformation.
-rung :: (forall x. f x -> g x) -> Gondola g :* fs -> Gondola g :* (f ': fs)
-rung f = (<:) (Gondola f)
-{-# INLINE rung #-}
-
-infixr 0 `rung`
-
-runGondolas :: (x ∈ xs) => Gondola f :* xs -> x a -> f a
-runGondolas = views piece runGondola
-{-# INLINE runGondolas #-}
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,74 @@
-{-# 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 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 #-}