diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,11 +1,13 @@
 # This Travis job script has been generated by a script via
 #
-#   runghc make_travis_yml_2.hs 'extensible.cabal'
+#   haskell-ci './extensible.cabal'
 #
-# For more information, see https://github.com/hvr/multi-ghc-travis
+# For more information, see https://github.com/haskell-CI/haskell-ci
 #
+# version: 0.2.1
+#
 language: c
-sudo: false
+dist: xenial
 
 git:
   submodules: false  # whether to recursively clone submodules
@@ -16,71 +18,59 @@
     - $HOME/.cabal/store
 
 before_cache:
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/build-reports.log
   # remove files that are regenerated by 'cabal update'
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.*
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/00-index.*
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/*.json
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.cache
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar.idx
 
-  - rm -rfv $HOME/.cabal/packages/head.hackage
+  - rm -rfv $CABALHOME/packages/head.hackage
 
 matrix:
   include:
-    - compiler: "ghc-8.4.4"
-      env: GHCHEAD=true
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-8.4.4], sources: [hvr-ghc]}}
     - compiler: "ghc-8.6.3"
-      env: GHCHEAD=true
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-8.6.3], sources: [hvr-ghc]}}
-
+      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-2.4,ghc-8.6.3], sources: [hvr-ghc]}}
+    - compiler: "ghc-8.4.4"
+      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-2.4,ghc-8.4.4], sources: [hvr-ghc]}}
 
 before_install:
-  - HC=${CC}
+  - HC=/opt/ghc/bin/${CC}
   - HCPKG=${HC/ghc/ghc-pkg}
   - unset CC
+  - CABAL=/opt/ghc/bin/cabal
+  - CABALHOME=$HOME/.cabal
+  - export PATH="$CABALHOME/bin:$PATH"
   - ROOTDIR=$(pwd)
-  - mkdir -p $HOME/.local/bin
-  - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH"
   - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))
   - echo $HCNUMVER
 
 install:
-  - cabal --version
+  - ${CABAL} --version
   - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
-  - BENCH=${BENCH---enable-benchmarks}
-  - TEST=${TEST---enable-tests}
-  - HADDOCK=${HADDOCK-true}
-  - INSTALLED=${INSTALLED-true}
+  - TEST=--enable-tests
+  - BENCH=--enable-benchmarks
   - GHCHEAD=${GHCHEAD-false}
-  - travis_retry cabal update -v
-  - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config"
+  - travis_retry ${CABAL} update -v
+  - sed -i.bak 's/^jobs:/-- jobs:/' $CABALHOME/config
   - rm -fv cabal.project cabal.project.local
-  # Overlay Hackage Package Index for GHC HEAD: https://github.com/hvr/head.hackage
-  - |
-    if $GHCHEAD; then
-      sed -i.bak 's/-- allow-newer:.*/allow-newer: *:base, *:template-haskell, *:ghc, *:Cabal/' ${HOME}/.cabal/config
-
-      echo 'repository head.hackage'                                                        >> ${HOME}/.cabal/config
-      echo '   url: http://head.hackage.haskell.org/'                                       >> ${HOME}/.cabal/config
-      echo '   secure: True'                                                                >> ${HOME}/.cabal/config
-      echo '   root-keys: 07c59cb65787dedfaef5bd5f987ceb5f7e5ebf88b904bbd4c5cbdeb2ff71b740' >> ${HOME}/.cabal/config
-      echo '              2e8555dde16ebd8df076f1a8ef13b8f14c66bad8eafefd7d9e37d0ed711821fb' >> ${HOME}/.cabal/config
-      echo '              8f79fd2389ab2967354407ec852cbe73f2e8635793ac446d09461ffb99527f6e' >> ${HOME}/.cabal/config
-      echo '   key-threshold: 3'                                                            >> ${HOME}/.cabal.config
-
-      cabal new-update head.hackage -v
-    fi
-  - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$'
-  - "printf 'packages: \".\"\\n' > cabal.project"
-  - cat cabal.project
-  - if [ -f "./configure.ac" ]; then
-      (cd "." && autoreconf -i);
-    fi
+  - grep -Ev -- '^\s*--' $CABALHOME/config | grep -Ev '^\s*$'
+  - rm -f cabal.project
+  - touch cabal.project
+  - "printf 'packages: \".\"\\n' >> cabal.project"
+  - "printf 'write-ghc-environment-files: always\\n' >> cabal.project"
+  - touch cabal.project.local
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(extensible)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
+  - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi
   - rm -f cabal.project.freeze
-  - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all
-  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks --project-file="cabal.project" --dep -j2 all
+  - ${CABAL} new-freeze -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dry
+  - "cat \"cabal.project.freeze\" | sed -E 's/^(constraints: *| *)//' | sed 's/any.//'"
+  - rm  "cabal.project.freeze"
+  - ${CABAL} new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all
+  - ${CABAL} new-build -w ${HC} --disable-tests --disable-benchmarks --project-file="cabal.project" --dep -j2 all
   - rm -rf .ghc.environment.* "."/dist
   - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)
 
@@ -88,28 +78,33 @@
 # any command which exits with a non-zero exit code causes the build to fail.
 script:
   # test that source-distributions can be generated
-  - (cd "." && cabal sdist)
-  - mv "."/dist/extensible-*.tar.gz ${DISTDIR}/
+  - ${CABAL} new-sdist all
+  - mv dist-newstyle/sdist/*.tar.gz ${DISTDIR}/
   - cd ${DISTDIR} || false
   - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \;
-  - "printf 'packages: extensible-*/*.cabal\\n' > cabal.project"
-  - cat cabal.project
+  - rm -f cabal.project
+  - touch cabal.project
+  - "printf 'packages: \"extensible-*/*.cabal\"\\n' >> cabal.project"
+  - "printf 'write-ghc-environment-files: always\\n' >> cabal.project"
+  - touch cabal.project.local
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(extensible)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
   # this builds all libraries and executables (without tests/benchmarks)
-  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks all
-
-  # Build with installed constraints for packages in global-db
-  - if $INSTALLED; then echo cabal new-build -w ${HC} --disable-tests --disable-benchmarks $(${HCPKG} list --global --simple-output --names-only | sed 's/\([a-zA-Z0-9-]\{1,\}\) */--constraint="\1 installed" /g') all | sh; else echo "Not building with installed constraints"; fi
+  - ${CABAL} new-build -w ${HC} --disable-tests --disable-benchmarks all
 
   # build & run tests, build benchmarks
-  - cabal new-build -w ${HC} ${TEST} ${BENCH} all
-  - if [ "x$TEST" = "x--enable-tests" ]; then cabal new-test -w ${HC} ${TEST} ${BENCH} all; fi
+  - ${CABAL} new-build -w ${HC} ${TEST} ${BENCH} all
+  - if [ "x$TEST" = "x--enable-tests" ]; then ${CABAL} new-test -w ${HC} ${TEST} ${BENCH} all; fi
 
   # cabal check
-  - (cd extensible-* && cabal check)
+  - (cd extensible-* && ${CABAL} check)
 
   # haddock
-  - rm -rf ./dist-newstyle
-  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi
+  - ${CABAL} new-haddock -w ${HC} ${TEST} ${BENCH} all
 
-# REGENDATA ["extensible.cabal"]
+  # Build without installed constraints for packages in global-db
+  - rm -f cabal.project.local; ${CABAL} new-build -w ${HC} --disable-tests --disable-benchmarks all;
+
+# REGENDATA ["./extensible.cabal"]
 # EOF
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,12 @@
+0.5.1
+-------------------------------------------------
+* Split `Data.Extensible.HList` and `Data.Extensible.Internal` to the
+  `membership` package
+* `AssocKey`, `AssocValue`, `ValueIs`, `KeyValue` and their related combinators
+  are deprecated. Use ones from `membership`
+* `IsRecord` now has a generic default implementation
+* Deprecated `deriveIsRecord`
+
 0.5
 -------------------------------------------------
 * GHC older than 8.4 is no longer supported
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.5
+version:             0.5.1
 synopsis:            Extensible, efficient, optics-friendly data types and effects
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
@@ -39,9 +39,7 @@
     Data.Extensible.Effect
     Data.Extensible.Effect.Default
     Data.Extensible.GetOpt
-    Data.Extensible.HList
     Data.Extensible.Inclusion
-    Data.Extensible.Internal
     Data.Extensible.Internal.Rig
     Data.Extensible.Label
     Data.Extensible.Match
@@ -77,6 +75,7 @@
     , exceptions
     , ghc-prim
     , hashable
+    , membership
     , monad-skeleton >= 0.1.2
     , mtl
     , prettyprinter
@@ -93,7 +92,7 @@
     , unordered-containers
     , vector
   hs-source-dirs:      src
-  ghc-options: -Wall
+  ghc-options: -Wall -Wcompat
   default-language:    Haskell2010
 
 test-suite effects
diff --git a/src/Data/Extensible/Bits.hs b/src/Data/Extensible/Bits.hs
--- a/src/Data/Extensible/Bits.hs
+++ b/src/Data/Extensible/Bits.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE UndecidableInstances, ScopedTypeVariables, MultiParamTypeClasses, TypeFamilies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving, DeriveGeneric #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
+#endif
 -----------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Bits
@@ -27,11 +30,11 @@
 import Data.Extensible.Class
 import Data.Extensible.Dictionary
 import Data.Extensible.Product
-import Data.Extensible.Internal (getMemberId)
 import Data.Extensible.Field
 import Data.Functor.Identity
 import Data.Hashable
 import Data.Ix
+import Data.Kind (Type)
 import Data.Profunctor.Rep
 import Data.Profunctor.Sieve
 import Data.Proxy
@@ -42,7 +45,7 @@
 import GHC.TypeLits
 
 -- | Bit-vector product. It has similar interface as @(:*)@ but fields are packed into @r@.
-newtype BitProd r (h :: k -> *) (xs :: [k]) = BitProd { unBitProd :: r }
+newtype BitProd r (h :: k -> Type) (xs :: [k]) = BitProd { unBitProd :: r }
   deriving (Eq, Ord, Enum, Bounded, Ix, Generic, Hashable, Storable)
 
 instance (Forall (Instance1 Show h) xs, BitFields r h xs) => Show (BitProd r h xs) where
@@ -135,8 +138,8 @@
   fromBits = Const . fromBits
   toBits = toBits . getConst
 
-instance (Bits r, FromBits r (h (AssocValue x))) => FromBits r (Field h x) where
-  type BitWidth (Field h x) = BitWidth (h (AssocValue x))
+instance (Bits r, FromBits r (h (TargetOf x))) => FromBits r (Field h x) where
+  type BitWidth (Field h x) = BitWidth (h (TargetOf x))
   fromBits = Field . fromBits
   toBits = toBits . getField
 
@@ -183,8 +186,8 @@
     offset = bitOffsetAt (Proxy :: Proxy r) (Proxy :: Proxy h) (Proxy :: Proxy xs) $ getMemberId i
 {-# INLINE bupdate #-}
 
-bitOffsetAt :: forall r h xs. Forall (Instance1 (FromBits r) h) xs
-  => Proxy (r :: *) -> Proxy (h :: k -> *) -> Proxy (xs :: [k]) -> Int -> Int
+bitOffsetAt :: forall k r h xs. Forall (Instance1 (FromBits r) h) xs
+  => Proxy (r :: Type) -> Proxy (h :: k -> Type) -> Proxy (xs :: [k]) -> Int -> Int
 bitOffsetAt _ ph _ = henumerateFor
   (Proxy :: Proxy (Instance1 (FromBits r) h))
   (Proxy :: Proxy xs)
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
@@ -25,7 +25,6 @@
   , leadership
   -- * Member
   , Member(..)
-  , remember
   , type (∈)
   , FindType
   -- * Generation
@@ -35,18 +34,18 @@
   -- * Association
   , Assoc(..)
   , type (>:)
-  , Associate(..)
-  , FindAssoc
-  -- * Sugar
-  , Elaborate
-  , Elaborated(..)
+  , Lookup(..)
+  , Associate
+  -- * Misc
+  , Head
+  , Last
   ) where
 import Data.Constraint
-import Data.Extensible.HList
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig (Optic')
 import Data.Extensible.Wrapper
 import Data.Profunctor
+import Type.Membership
+import Type.Membership.Internal
 
 -- | This class allows us to use 'pieceAt' for both sums and products.
 class (Functor f, Profunctor p) => Extensible f p (t :: (k -> *) -> [k] -> *) where
@@ -60,7 +59,7 @@
 {-# INLINE piece #-}
 
 -- | Like 'piece', but reckon membership from its key.
-pieceAssoc :: (Associate k v xs, Extensible f p t, ExtensibleConstr t h xs (k ':> v)) => Optic' p f (t h xs) (h (k ':> v))
+pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t h xs (k ':> v)) => Optic' p f (t h xs) (h (k ':> v))
 pieceAssoc = pieceAt association
 {-# INLINE pieceAssoc #-}
 
@@ -75,7 +74,7 @@
 {-# INLINE item #-}
 
 -- | Access an element specified by the key type through a wrapper.
-itemAssoc :: (Wrapper h, Extensible f p t, Associate k v xs, ExtensibleConstr t h xs (k ':> v))
+itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t h xs (k ':> v))
   => proxy k -> Optic' p f (t h xs) (Repr h (k ':> v))
 itemAssoc p = pieceAssoc . _WrapperAs (proxyKey p)
 {-# INLINE itemAssoc #-}
@@ -84,52 +83,14 @@
 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
-
-  hcount _ = 0
-
-  hgenerateList _ = pure HNil
-
-instance Generate xs => Generate (x ': xs) where
-  henumerate f r = f here $ henumerate (f . navNext) r
-
-  hcount _ = 1 + hcount (Proxy :: Proxy xs)
-
-  -- | Enumerate 'Membership's and construct an 'HList'.
-  hgenerateList f = HCons <$> f here <*> hgenerateList (f . navNext)
-
--- | 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
-
-  hgenerateListFor _ _ = pure HNil
-
-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
+-- | First element
+type family Head (xs :: [k]) :: k where
+  Head (x ': xs) = x
 
-  hgenerateListFor p f = HCons <$> f here <*> hgenerateListFor p (f . navNext)
+-- | Last element
+type family Last (x :: [k]) :: k where
+  Last '[x] = x
+  Last (x ': xs) = Last xs
 
--- | HACK: Without this, the constraints are not propagated well.
-type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
-  ForallF c '[] = ()
-  ForallF c (x ': xs) = (c x, Forall c xs)
+type Associate k v xs = Lookup xs k v
+{-# DEPRECATED Associate "Use Lookup instead" #-}
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
@@ -26,7 +26,6 @@
 import Data.Extensible.Field
 import Data.Extensible.Product
 import Data.Extensible.Sum
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Nullable
 import Data.Constraint
@@ -41,11 +40,13 @@
 import qualified Data.Vector.Unboxed as U
 import qualified Data.Vector as V
 import qualified Data.Text as T
+import Data.Type.Equality
 import qualified Language.Haskell.TH.Lift as TH
 import Language.Haskell.TH hiding (Type)
 import GHC.TypeLits
 import Test.QuickCheck.Arbitrary
 import Test.QuickCheck.Gen
+import Type.Membership
 
 -- | Reify a collection of dictionaries, as you wish.
 library :: forall c xs. Forall c xs => Comp Dict c :* xs
@@ -94,8 +95,7 @@
 instance (WrapForall Semigroup h xs, WrapForall Monoid h xs) => Monoid (h :* xs) where
   mempty = hrepeatFor (Proxy :: Proxy (Instance1 Monoid h)) mempty
   {-# INLINE mempty #-}
-  mappend = hzipWith3 (\(Comp Dict) -> mappend)
-    (library :: Comp Dict (Instance1 Monoid h) :* xs)
+  mappend = (<>)
   {-# INLINE mappend #-}
 
 instance WrapForall Hashable h xs => Hashable (h :* xs) where
@@ -132,7 +132,7 @@
   basicUnsafeThaw (V_Product v) = fmap MV_Product
     $ hgenerateFor (Proxy :: Proxy (Instance1 U.Unbox h))
     $ \m -> Comp <$> G.basicUnsafeThaw (hlookupC m v)
-  basicLength (V_Product v) = G.basicLength $ getComp $ hindex v here
+  basicLength (V_Product v) = G.basicLength $ getComp $ hindex v leadership
   basicUnsafeSlice i n (V_Product v) = V_Product
     $ htabulateFor (Proxy :: Proxy (Instance1 U.Unbox h))
     $ \m -> Comp $ G.basicUnsafeSlice i n (hlookupC m v)
@@ -142,7 +142,7 @@
     = henumerateFor (Proxy :: Proxy (Instance1 U.Unbox h)) (Proxy :: Proxy (x ': xs)) ((>>) . \i -> G.basicUnsafeCopy (hlookupC i v) (hlookupC i w)) (return ())
 
 instance WrapForall U.Unbox h (x ': xs) => M.MVector U.MVector (h :* (x ': xs)) where
-  basicLength (MV_Product v) = M.basicLength $ getComp $ hindex v here
+  basicLength (MV_Product v) = M.basicLength $ getComp $ hindex v leadership
   basicUnsafeSlice i n (MV_Product v) = MV_Product
     $ htabulateFor (Proxy :: Proxy (Instance1 U.Unbox h))
     $ \m -> Comp $ M.basicUnsafeSlice i n (hlookupC m v)
@@ -190,8 +190,8 @@
   parseRecord rec = hgenerateFor (Proxy :: Proxy (Instance1 Csv.FromField h))
     $ \i -> G.indexM rec (getMemberId i) >>= Csv.parseField
 
-instance Forall (KeyValue KnownSymbol (Instance1 Csv.FromField h)) xs => Csv.FromNamedRecord (Field h :* xs) where
-  parseNamedRecord rec = hgenerateFor (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 Csv.FromField h)))
+instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.FromField h)) xs => Csv.FromNamedRecord (Field h :* xs) where
+  parseNamedRecord rec = hgenerateFor (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 Csv.FromField h)))
     $ \i -> rec Csv..: BC.pack (symbolVal (proxyAssocKey i)) >>= Csv.parseField
 
 instance WrapForall Csv.ToField h xs => Csv.ToRecord (h :* xs) where
@@ -199,33 +199,33 @@
     . hfoldrWithIndexFor (Proxy :: Proxy (Instance1 Csv.ToField h))
       (\_ v -> (:) $ Csv.toField v) []
 
-instance Forall (KeyValue KnownSymbol (Instance1 Csv.ToField h)) xs => Csv.ToNamedRecord (Field h :* xs) where
-  toNamedRecord = hfoldlWithIndexFor (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 Csv.ToField h)))
+instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.ToField h)) xs => Csv.ToNamedRecord (Field h :* xs) where
+  toNamedRecord = hfoldlWithIndexFor (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 Csv.ToField h)))
     (\k m v -> HM.insert (BC.pack (symbolVal (proxyAssocKey k))) (Csv.toField v) m)
     HM.empty
 
 -- | @'parseJSON' 'J.Null'@ is called for missing fields.
-instance Forall (KeyValue KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Field h :* xs) where
   parseJSON = J.withObject "Object" $ \v -> hgenerateFor
-    (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 J.FromJSON h)))
+    (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)))
     $ \m -> let k = symbolVal (proxyAssocKey m)
       in fmap Field $ J.parseJSON $ maybe J.Null id $ HM.lookup (T.pack k) v
 
-instance Forall (KeyValue KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Field h :* xs) where
   toJSON = J.Object . hfoldlWithIndexFor
-    (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 J.ToJSON h)))
+    (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)))
     (\k m v -> HM.insert (T.pack (symbolVal (proxyAssocKey k))) (J.toJSON v) m)
     HM.empty
 
-instance Forall (KeyValue KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Nullable (Field h) :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Nullable (Field h) :* xs) where
   parseJSON = J.withObject "Object" $ \v -> hgenerateFor
-    (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 J.FromJSON h)))
+    (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)))
     $ \m -> let k = symbolVal (proxyAssocKey m)
       in fmap Nullable $ traverse J.parseJSON $ HM.lookup (T.pack k) v
 
-instance Forall (KeyValue KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Nullable (Field h) :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Nullable (Field h) :* xs) where
   toJSON = J.Object . hfoldlWithIndexFor
-    (Proxy :: Proxy (KeyValue KnownSymbol (Instance1 J.ToJSON h)))
+    (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)))
     (\k m (Nullable v) -> maybe id (HM.insert (T.pack $ symbolVal $ proxyAssocKey k) . J.toJSON) v m)
     HM.empty
 
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
@@ -89,37 +89,36 @@
 import Control.Monad.Trans.Cont (ContT(..))
 import Data.Extensible.Field
 import Data.Extensible.Inclusion
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Product
 import Data.Extensible.Class
 import Data.Functor.Identity
 import Data.Profunctor.Unsafe -- Trustworthy since 7.8
-import Data.Typeable (Typeable)
+import Data.Type.Equality
+import Type.Membership
 
 -- | A unit of named effects. This is a variant of @(':|')@ specialised for
 -- 'Type -> Type'.
 data Instruction (xs :: [Assoc k (* -> *)]) a where
-  Instruction :: !(Membership xs kv) -> AssocValue kv a -> Instruction xs a
-  deriving Typeable
+  Instruction :: !(Membership xs kv) -> TargetOf 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 :: forall s t xs a. Lookup xs s t => 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
+liftsEff :: forall s t xs a r. Lookup xs s t
   => 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 :: forall s t xs a. Lookup xs s t => 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
@@ -145,7 +144,7 @@
 peelEff pass ret wrap = go where
   go m = case debone m of
     Return a -> ret a
-    Instruction i t :>>= k -> leadership i
+    Instruction i t :>>= k -> testMembership i
       (\Refl -> wrap t (go . k))
       (\j -> pass (Instruction j t) (go . k))
 {-# INLINE peelEff #-}
@@ -192,13 +191,12 @@
 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 -> leadership i
+  Instruction i t :>>= k -> testMembership i
     (\Refl -> t >>= retractEff . k)
     $ error "Impossible"
 
 -- | Transformation between effects
 newtype Interpreter f g = Interpreter { runInterpreter :: forall a. g a -> f a }
-  deriving Typeable
 
 -- | Process an 'Eff' action using a record of 'Interpreter's.
 handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a
@@ -237,7 +235,7 @@
 peelAction pass ret wrap = go where
   go m = case debone m of
     Return a -> ret a
-    Instruction i t :>>= k -> leadership i
+    Instruction i t :>>= k -> testMembership i
       (\Refl -> case t of
         (_ :: Action ps q x) ->
           let run :: forall t. Function t ((q -> r) -> r) -> Action t q x -> r
@@ -253,7 +251,7 @@
 peelAction0 wrap = go where
   go m = case debone m of
     Return a -> return a
-    Instruction i t :>>= k -> leadership i
+    Instruction i t :>>= k -> testMembership i
       (\Refl -> case t of
         (_ :: Action ps q x) ->
           let run :: forall t. Function t (Eff xs q) -> Action t q x -> Eff xs a
@@ -268,19 +266,19 @@
 type ReaderEff = (:~:)
 
 -- | Fetch the environment.
-askEff :: forall k r xs. Associate k (ReaderEff r) xs
+askEff :: forall k r xs. Lookup xs k (ReaderEff r)
   => 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
+asksEff :: forall k r xs a. Lookup xs k (ReaderEff r)
   => 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
+localEff :: forall k r xs a. Lookup xs k (ReaderEff r)
   => Proxy k -> (r -> r) -> Eff xs a -> Eff xs a
 localEff _ f = go where
   go m = case debone m of
@@ -298,31 +296,31 @@
 {-# INLINE runReaderEff #-}
 
 -- | Get the current state.
-getEff :: forall k s xs. Associate k (State s) xs
+getEff :: forall k s xs. Lookup xs k (State s)
   => 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
+getsEff :: forall k s a xs. Lookup xs k (State s)
   => 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
+putEff :: forall k s xs. Lookup xs k (State s)
   => 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
+modifyEff :: forall k s xs. Lookup xs k (State s)
   => 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
+stateEff :: forall k s xs a. Lookup xs k (State s)
   => Proxy k -> (s -> (a, s)) -> Eff xs a
 stateEff k = liftEff k . state
 {-# INLINE stateEff #-}
@@ -349,19 +347,19 @@
 type WriterEff w = (,) w
 
 -- | Write the second element and return the first element.
-writerEff :: forall k w xs a. (Associate k (WriterEff w) xs)
+writerEff :: forall k w xs a. (Lookup xs k (WriterEff w))
   => 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)
+tellEff :: forall k w xs. (Lookup xs k (WriterEff w))
   => 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)
+listenEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
   => Proxy k -> Eff xs a -> Eff xs (a, w)
 listenEff p = go mempty where
   go w m = case debone m of
@@ -373,7 +371,7 @@
 {-# INLINE listenEff #-}
 
 -- | Modify the output using the function in the result.
-passEff :: forall k w xs a. (Associate k (WriterEff w) xs, Monoid w)
+passEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
   => Proxy k -> Eff xs (a, w -> w) -> Eff xs a
 passEff p = go mempty where
   go w m = case debone m of
@@ -401,7 +399,7 @@
 type MaybeEff = Const ()
 
 -- | Break out of the computation. Similar to 'Nothing'.
-nothingEff :: Associate k MaybeEff xs => Proxy k -> Eff xs a
+nothingEff :: Lookup xs k MaybeEff => Proxy k -> Eff xs a
 nothingEff = flip throwEff ()
 
 -- | Run an effect which may fail in the name of @k@.
@@ -413,12 +411,12 @@
 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 :: Lookup xs k (EitherEff e) => 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)
+catchEff :: forall k e xs a. (Lookup xs k (EitherEff e))
   => Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a
 catchEff _ m0 handler = go m0 where
   go m = case debone m of
@@ -434,7 +432,7 @@
 {-# INLINE runEitherEff #-}
 
 -- | Put a milestone on a computation.
-tickEff :: Associate k Identity xs => Proxy k -> Eff xs ()
+tickEff :: Lookup xs k Identity => Proxy k -> Eff xs ()
 tickEff k = liftEff k $ Identity ()
 {-# INLINE tickEff #-}
 
@@ -443,12 +441,12 @@
   -> Eff xs (Either a (Eff (k >: Identity ': xs) a))
 runIterEff m = case debone m of
   Return a -> return (Left a)
-  Instruction i t :>>= k -> leadership i
+  Instruction i t :>>= k -> testMembership i
     (\Refl -> return $ Right $ k $ runIdentity t)
     $ \j -> boned $ Instruction j t :>>= runIterEff . k
 
 -- | Place a continuation-passing action.
-contEff :: Associate k (ContT r m) xs => Proxy k
+contEff :: Lookup xs k (ContT r m) => Proxy k
   -> ((a -> m r) -> m r) -> Eff xs a
 contEff k = liftEff k . ContT
 
@@ -458,6 +456,6 @@
   -> Eff xs r
 runContEff m cont = case debone m of
   Return a -> cont a
-  Instruction i t :>>= k -> leadership i
+  Instruction i t :>>= k -> testMembership i
     (\Refl -> runContT t (flip runContEff cont . k))
     $ \j -> boned $ Instruction j t :>>= flip runContEff cont . k
diff --git a/src/Data/Extensible/Effect/Default.hs b/src/Data/Extensible/Effect/Default.hs
--- a/src/Data/Extensible/Effect/Default.hs
+++ b/src/Data/Extensible/Effect/Default.hs
@@ -30,7 +30,6 @@
 ) where
 import Control.Applicative
 import Data.Extensible.Effect
-import Data.Extensible.Internal
 import Control.Monad.Except
 import Control.Monad.Catch
 import Control.Monad.Reader.Class
@@ -40,19 +39,21 @@
 import Control.Monad.Trans.Resource
 #endif
 import Control.Monad.Writer.Class
+import Data.Type.Equality
+import Type.Membership
 
-instance (MonadIO m, Associate "IO" m xs) => MonadIO (Eff xs) where
+instance (MonadIO m, Lookup xs "IO" m) => MonadIO (Eff xs) where
   liftIO = liftEff (Proxy :: Proxy "IO") . liftIO
 
 #if MIN_VERSION_resourcet(1,2,0)
-instance (MonadResource m, Associate "IO" m xs) => MonadResource (Eff xs) where
+instance (MonadResource m, Lookup xs "IO" m) => MonadResource (Eff xs) where
   liftResourceT = liftEff (Proxy :: Proxy "IO") . liftResourceT
 #endif
 
-instance (MonadThrow m, Associate "IO" m xs) => MonadThrow (Eff xs) where
+instance (MonadThrow m, Lookup xs "IO" m) => MonadThrow (Eff xs) where
   throwM = liftEff (Proxy :: Proxy "IO") . throwM
 
-instance (MonadCatch m, Associate "IO" m xs) => MonadCatch (Eff xs) where
+instance (MonadCatch m, Lookup xs "IO" m) => MonadCatch (Eff xs) where
   catch m0 h = go m0 where
     go m = case debone m of
       Return a -> return a
@@ -63,7 +64,7 @@
 pReader :: Proxy "Reader"
 pReader = Proxy
 
-instance Associate "Reader" ((:~:) r) xs => MonadReader r (Eff xs) where
+instance Lookup xs "Reader" ((:~:) r) => MonadReader r (Eff xs) where
   ask = askEff pReader
   local = localEff pReader
   reader = asksEff pReader
@@ -71,7 +72,7 @@
 pState :: Proxy "State"
 pState = Proxy
 
-instance Associate "State" (State s) xs => MonadState s (Eff xs) where
+instance Lookup xs "State" (State s) => MonadState s (Eff xs) where
   get = getEff pState
   put = putEff pState
   state = stateEff pState
@@ -79,7 +80,7 @@
 pWriter :: Proxy "Writer"
 pWriter = Proxy
 
-instance (Monoid w, Associate "Writer" ((,) w) xs) => MonadWriter w (Eff xs) where
+instance (Monoid w, Lookup xs "Writer" ((,) w)) => MonadWriter w (Eff xs) where
   writer = writerEff pWriter
   tell = tellEff pWriter
   listen = listenEff pWriter
@@ -88,16 +89,16 @@
 pEither :: Proxy "Either"
 pEither = Proxy
 
-instance (Associate "Either" (Const e) xs) => MonadError e (Eff xs) where
+instance (Lookup xs "Either" (Const e)) => MonadError e (Eff xs) where
   throwError = throwEff pEither
   catchError = catchEff pEither
 
 -- | A bit dubious
-instance (Monoid e, Associate "Either" (Const e) xs) => Alternative (Eff xs) where
+instance (Monoid e, Lookup xs "Either" (Const e)) => 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
+instance (Monoid e, Lookup xs "Either" (Const e)) => MonadPlus (Eff xs) where
   mzero = empty
   mplus = (<|>)
 
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
@@ -35,14 +35,22 @@
   , matchWithField
   , matchField
   -- * Key / value
+  , KeyOf
+  , proxyKeyOf
+  , stringKeyOf
+  , TargetOf
+  , proxyTargetOf
+  , KeyIs
+  , TargetIs
+  , KeyTargetAre
+  -- * deprecated
   , AssocKey
   , AssocValue
+  , ValueIs
   , KeyValue
   , proxyAssocKey
-  , proxyAssocValue
   , stringAssocKey
-  , KeyIs
-  , ValueIs
+  , proxyAssocValue
   -- * Internal
   , LabelPhantom
   , Labelling
@@ -59,7 +67,6 @@
 import Data.Extensible.Sum
 import Data.Extensible.Match
 import Data.Extensible.Product
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Kind
 import Data.Profunctor.Unsafe
@@ -68,7 +75,6 @@
 import Data.Hashable
 import Data.String
 import Data.Text.Prettyprint.Doc
-import Data.Typeable (Typeable)
 import qualified Data.Vector.Generic as G
 import qualified Data.Vector.Generic.Mutable as M
 import qualified Data.Vector.Unboxed as U
@@ -78,54 +84,18 @@
 import Language.Haskell.TH.Lift
 import Language.Haskell.TH (appE, conE)
 import Test.QuickCheck.Arbitrary
-
--- | 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
-
--- | Proxy-level 'AssocValue'.
-proxyAssocValue :: proxy kv -> Proxy (AssocValue kv)
-proxyAssocValue _ = Proxy
-
--- | Get a string from a proxy of @'Assoc' 'Symbol' v@.
-stringAssocKey :: (IsString a, KnownSymbol (AssocKey kv)) => proxy kv -> a
-stringAssocKey = fromString . symbolVal . proxyAssocKey
-{-# INLINE stringAssocKey #-}
-
--- | Take the type of the value
-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)
-
--- | Constraint applied to 'AssocKey'
-class (pk (AssocKey kv)) => KeyIs pk kv where
-
-instance (pk k) => KeyIs pk (k ':> v)
-
--- | Constraint applied to 'AssocValue'
-class (pv (AssocValue kv)) => ValueIs pv kv where
-
-instance (pv v) => ValueIs pv (k ':> v)
-
+import Type.Membership
 
 -- | A @'Field' h (k ':> v)@ is @h v@ annotated with the field name @k@.
 --
 -- @'Field' :: (v -> *) -> Assoc k v -> *@
 --
 newtype Field (h :: v -> Type) (kv :: Assoc k v)
-  = Field { getField :: h (AssocValue kv) }
+  = Field { getField :: h (TargetOf kv) }
 
-  deriving (Typeable, Generic)
+  deriving (Generic)
 
-#define ND_Field(c) deriving instance c (h (AssocValue kv)) => c (Field h kv)
+#define ND_Field(c) deriving instance c (h (TargetOf kv)) => c (Field h kv)
 
 ND_Field(Eq)
 ND_Field(Ord)
@@ -149,10 +119,10 @@
 ND_Field(J.FromJSON)
 ND_Field(J.ToJSON)
 
-newtype instance U.MVector s (Field h x) = MV_Field (U.MVector s (h (AssocValue x)))
-newtype instance U.Vector (Field h x) = V_Field (U.Vector (h (AssocValue x)))
+newtype instance U.MVector s (Field h x) = MV_Field (U.MVector s (h (TargetOf x)))
+newtype instance U.Vector (Field h x) = V_Field (U.Vector (h (TargetOf x)))
 
-instance (U.Unbox (h (AssocValue x))) => M.MVector U.MVector (Field h x) where
+instance (U.Unbox (h (TargetOf x))) => M.MVector U.MVector (Field h x) where
   {-# INLINE basicLength #-}
   {-# INLINE basicUnsafeSlice #-}
   {-# INLINE basicOverlaps #-}
@@ -181,7 +151,7 @@
   basicUnsafeMove (MV_Field v1) (MV_Field v2) = M.basicUnsafeMove v1 v2
   basicUnsafeGrow (MV_Field v) n = MV_Field <$> M.basicUnsafeGrow v n
 
-instance (U.Unbox (h (AssocValue x))) => G.Vector U.Vector (Field h x) where
+instance (U.Unbox (h (TargetOf x))) => G.Vector U.Vector (Field h x) where
   {-# INLINE basicUnsafeFreeze #-}
   {-# INLINE basicUnsafeThaw #-}
   {-# INLINE basicLength #-}
@@ -194,24 +164,24 @@
   basicUnsafeIndexM (V_Field v) i = Field <$> G.basicUnsafeIndexM v i
   basicUnsafeCopy (MV_Field mv) (V_Field v) = G.basicUnsafeCopy mv v
 
-instance (U.Unbox (h (AssocValue x))) => U.Unbox (Field h x)
+instance (U.Unbox (h (TargetOf x))) => U.Unbox (Field h x)
 
-instance Lift (h (AssocValue x)) => Lift (Field h x) where
+instance Lift (h (TargetOf x)) => Lift (Field h x) where
   lift = appE (conE 'Field) . lift . getField
 
 -- | Lift a function for the content.
-liftField :: (g (AssocValue kv) -> h (AssocValue kv)) -> Field g kv -> Field h kv
+liftField :: (g (TargetOf kv) -> h (TargetOf 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))
+liftField2 :: (f (TargetOf kv) -> g (TargetOf kv) -> h (TargetOf 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)
+  type Repr (Field h) kv = Repr h (TargetOf kv)
   _Wrapper = dimap getField (fmap Field) . _Wrapper
   {-# INLINE _Wrapper #-}
 
@@ -277,7 +247,7 @@
 type FieldOptic k = forall kind. forall f p t xs (h :: kind -> Type) (v :: kind).
   (Extensible f p t
   , ExtensibleConstr t (Field h) xs (k ':> v)
-  , Associate k v xs
+  , Lookup xs k v
   , Labelling k p
   , Wrapper h)
   => Optic' p f (t (Field h) xs) (Repr h v)
@@ -340,3 +310,30 @@
 (@==) = (@=)
 {-# INLINE (@==) #-}
 infix 1 @==
+
+type AssocKey kv = KeyOf kv
+{-# DEPRECATED AssocKey "Use KeyOf instead" #-}
+
+type AssocValue kv = TargetOf kv
+{-# DEPRECATED AssocValue "Use TargetOf instead" #-}
+
+type ValueIs = TargetIs
+{-# DEPRECATED ValueIs "Use TargetIs instead" #-}
+
+type KeyValue = KeyTargetAre
+{-# DEPRECATED KeyValue "Use KeyTargetAre instead" #-}
+
+proxyAssocKey :: proxy kv -> Proxy (KeyOf kv)
+proxyAssocKey = proxyKeyOf
+{-# INLINE proxyAssocKey #-}
+{-# DEPRECATED proxyAssocKey "Use proxyKeyOf instead" #-}
+
+proxyAssocValue :: proxy kv -> Proxy (TargetOf kv)
+proxyAssocValue = proxyTargetOf
+{-# INLINE proxyAssocValue #-}
+{-# DEPRECATED proxyAssocValue "Use proxyTargetOf instead" #-}
+
+stringAssocKey :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a
+stringAssocKey = stringKeyOf
+{-# INLINE stringAssocKey #-}
+{-# DEPRECATED stringAssocKey "Use stringKeyOf instead" #-}
diff --git a/src/Data/Extensible/HList.hs b/src/Data/Extensible/HList.hs
deleted file mode 100644
--- a/src/Data/Extensible/HList.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
-{-# LANGUAGE Trustworthy #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.HList
--- Copyright   :  (c) Fumiaki Kinoshita 2018
--- 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
@@ -32,8 +32,8 @@
 import Data.Extensible.Class
 import Data.Extensible.Product
 import Data.Extensible.Sum
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
+import Data.Proxy
 
 -- | Unicode alias for 'Include'
 type xs ⊆ ys = Include ys xs
@@ -59,7 +59,7 @@
 ------------------------------------------------------------------
 
 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) = Lookup xs k v
 
 -- | @'Associated' xs (k ':> v)@ is equivalent to @'Associate' k v xs@
 class Associated' xs t => Associated xs t where
diff --git a/src/Data/Extensible/Internal.hs b/src/Data/Extensible/Internal.hs
deleted file mode 100644
--- a/src/Data/Extensible/Internal.hs
+++ /dev/null
@@ -1,199 +0,0 @@
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.Inclusion
--- Copyright   :  (c) Fumiaki Kinoshita 2018
--- License     :  BSD3
---
--- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
---
--- A bunch of combinators that contains magic
-------------------------------------------------------------------------
-module Data.Extensible.Internal (
-  -- * Membership
-  Membership
-  , getMemberId
-  , mkMembership
-  , reifyMembership
-  , leadership
-  , compareMembership
-  , impossibleMembership
-  , here
-  , navNext
-  -- * Member class
-  , Member(..)
-  , remember
-  , type (∈)
-  , FindType
-  -- * Association
-  , Assoc(..)
-  , type (>:)
-  , Associate(..)
-  , FindAssoc
-  -- * Sugar
-  , Elaborate
-  , Elaborated(..)
-  -- * Miscellaneous
-  , Head
-  , Last
-  , module Data.Type.Equality
-  , module Data.Proxy
-  ) where
-import Control.DeepSeq (NFData)
-import Data.Type.Equality
-import Data.Proxy
-import Control.Monad
-import Unsafe.Coerce
-import Data.Hashable
-import Data.Text.Prettyprint.Doc
-import Data.Typeable
-import Language.Haskell.TH hiding (Pred)
-import Language.Haskell.TH.Lift
-import Data.Semigroup (Semigroup(..))
-import GHC.TypeLits
-
--- | 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 -- ^ get the position as an 'Int'.
-  } deriving (Typeable, NFData)
-
-instance Lift (Membership xs x) where
-  lift (Membership i) = mkMembership i
-
-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, KnownNat pos) => Member xs x where
-  membership = Membership (fromInteger $ natVal (Proxy :: Proxy pos))
-  {-# INLINE membership #-}
-
-instance Hashable (Membership xs x) where
-  hashWithSalt s = hashWithSalt s . getMemberId
-
--- | Make up a 'Membership' from an integer.
-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 0 k xs) ~ 'Expecting (n ':> v), KnownNat n) => Associate k v xs where
-  association = Membership (fromInteger $ natVal (Proxy :: Proxy n))
-
--- | A readable type search result
-data Elaborated k v = Expecting v | Missing k | Duplicate k
-
--- | Make the result more readable
-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
-
--- | Find a type associated to the specified key.
-type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where
-  FindAssoc n k ((k ':> v) ': xs) = (n ':> v) ': FindAssoc (1 + n) k xs
-  FindAssoc n k ((k' ':> v) ': xs) = FindAssoc (1 + n) k xs
-  FindAssoc n k '[] = '[]
-
-instance Show (Membership xs x) where
-  show (Membership n) = "$(mkMembership " ++ show n ++ ")"
-
-instance Pretty (Membership xs x) where
-  pretty (Membership n) = "$(mkMembership " <> pretty n <> ")"
-
-instance Eq (Membership xs x) where
-  _ == _ = True
-
-instance Ord (Membership xs x) where
-  compare _ _ = EQ
-
-instance Semigroup (Membership xs x) where
-  x <> _ = x
-
--- | Embodies a type equivalence to ensure that the 'Membership' points the first element.
-leadership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
-leadership (Membership 0) l _ = l (unsafeCoerce Refl)
-leadership (Membership n) _ r = r (Membership (n - 1))
-{-# INLINE leadership #-}
-
--- | 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"
-
--- | 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
-
--- | First element
-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) = 0 ': FindType x xs
-  FindType x (y ': ys) = MapSucc (FindType x ys)
-  FindType x '[] = '[]
-
--- | Last element
-type family Last (x :: [k]) :: k where
-  Last '[x] = x
-  Last (x ': xs) = Last xs
-
--- | Ideally, it will be 'Map Succ'
-type family MapSucc (xs :: [Nat]) :: [Nat] where
-  MapSucc '[] = '[]
-  MapSucc (x ': xs) = (1 + x) ': MapSucc xs
diff --git a/src/Data/Extensible/Label.hs b/src/Data/Extensible/Label.hs
--- a/src/Data/Extensible/Label.hs
+++ b/src/Data/Extensible/Label.hs
@@ -30,7 +30,7 @@
 訊 = itemAssoc
 
 instance (Extensible f p e
-  , Associate k v xs
+  , Lookup xs k v
   , Labelling k p
   , Wrapper h
   , ExtensibleConstr e (Field h) xs (k ':> v)
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
@@ -41,13 +41,13 @@
   _Wrapper = withIso _Wrapper $ \f g -> dimap (fmap f . getNullable) (fmap (Nullable . fmap g))
 
 instance Semigroup (h x) => Semigroup (Nullable h x) where
-  (<>) = mappend
+  Nullable (Just a) <> Nullable (Just b) = Nullable (Just (a <> b))
+  a@(Nullable (Just _)) <> _ = a
+  _ <> b = b
 
 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
+  mappend = (<>)
 
 instance Lift (h a) => Lift (Nullable h a) where
   lift = appE (conE 'Nullable) . lift . getNullable
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
@@ -18,7 +18,6 @@
   , (<%|)
   , accessing
   ) where
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Class
 import Data.Extensible.Product
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
@@ -61,13 +61,12 @@
   , htabulateFor
   , hrepeatFor) where
 
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig (review)
 import Data.Extensible.Struct
 import Data.Extensible.Sum
 import Data.Extensible.Class
-import qualified Data.Extensible.HList as HList
 import Data.Extensible.Wrapper
+import qualified Type.Membership.HList as HList
 
 -- | O(n) Prepend an element onto a product.
 -- Expressions like @a <: b <: c <: nil@ are transformed to a single 'fromHList'.
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
--- a/src/Data/Extensible/Record.hs
+++ b/src/Data/Extensible/Record.hs
@@ -1,4 +1,8 @@
 {-# LANGUAGE LambdaCase, TemplateHaskell, TypeFamilies #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
 ------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Record
@@ -12,14 +16,15 @@
 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.Generics
 import GHC.TypeLits
+import Type.Membership
+import Type.Membership.HList
 
 -- | The class of types that can be converted to/from a 'Record'.
 class IsRecord a where
@@ -27,11 +32,52 @@
   recordFromList :: HList (Field Identity) (RecFields a) -> a
   recordToList :: a -> HList (Field Identity) (RecFields a)
 
+  type RecFields a = GRecFields (Rep a) '[]
+  default recordFromList :: (Generic a, GIsRecord (Rep a) '[], GRecFields (Rep a) '[] ~ RecFields a) => HList (Field Identity) (RecFields a) -> a
+  recordFromList xs = recordFromList' xs (\x (HNil :: HList (Field Identity) '[]) -> to x)
+
+  default recordToList :: (Generic a, GIsRecord (Rep a) '[], GRecFields (Rep a) '[] ~ RecFields a) => a -> HList (Field Identity) (RecFields a)
+  recordToList x = recordToList' (from x) HNil
+
 instance IsRecord () where
   type RecFields () = '[]
   recordFromList _ = ()
   recordToList _ = HNil
 
+-- | The class of types that can be converted to/from a 'Record'.
+class GIsRecord f r where
+  type GRecFields f (r :: [Assoc Symbol *]) :: [Assoc Symbol *]
+  recordFromList' :: HList (Field Identity) (GRecFields f r) -> (f x -> HList (Field Identity) r -> cont) -> cont
+  recordToList' :: f x -> HList (Field Identity) r -> HList (Field Identity) (GRecFields f r)
+
+instance (GIsRecord f (GRecFields g r), GIsRecord g r) => GIsRecord (f :*: g) r where
+  type GRecFields (f :*: g) r = GRecFields f (GRecFields g r)
+  recordFromList' xs cont = recordFromList' xs $ \l ys -> recordFromList' ys $ \r zs -> cont (l :*: r) zs
+  {-# INLINE recordFromList' #-}
+  recordToList' (f :*: g) = recordToList' f . recordToList' g
+  {-# INLINE recordToList' #-}
+
+instance GIsRecord (S1 ('MetaSel ('Just name) su ss ds) (K1 i a)) r where
+  type GRecFields (S1 ('MetaSel ('Just name) su ss ds) (K1 i a)) r = (name >: a) ': r
+  recordFromList' (HCons (Field (Identity a)) xs) cont = cont (M1 (K1 a)) xs
+  {-# INLINE recordFromList' #-}
+  recordToList' (M1 (K1 a)) = HCons (Field (Identity a))
+  {-# INLINE recordToList' #-}
+
+instance GIsRecord f r => GIsRecord (C1 i f) r where
+  type GRecFields (C1 i f) r = GRecFields f r
+  recordFromList' xs cont = recordFromList' xs $ cont . M1
+  {-# INLINE recordFromList' #-}
+  recordToList' (M1 f) = recordToList' f
+  {-# INLINE recordToList' #-}
+
+instance GIsRecord f r => GIsRecord (D1 i f) r where
+  type GRecFields (D1 i f) r = GRecFields f r
+  recordFromList' xs cont = recordFromList' xs $ cont . M1
+  {-# INLINE recordFromList' #-}
+  recordToList' (M1 f) = recordToList' f
+  {-# INLINE recordToList' #-}
+
 -- | Convert a value into a 'Record'.
 toRecord :: IsRecord a => a -> Record (RecFields a)
 toRecord = fromHList . recordToList
@@ -52,6 +98,7 @@
 tvName (PlainTV n) = n
 tvName (KindedTV n _) = n
 
+{-# DEPRECATED deriveIsRecord "Use the generic default methods instead" #-}
 -- | Create an 'IsRecord' instance for a normal record declaration.
 deriveIsRecord :: Name -> DecsQ
 deriveIsRecord name = reify name >>= \case
diff --git a/src/Data/Extensible/Struct.hs b/src/Data/Extensible/Struct.hs
--- a/src/Data/Extensible/Struct.hs
+++ b/src/Data/Extensible/Struct.hs
@@ -46,26 +46,24 @@
   , toHList) where
 
 import GHC.Prim
+import Control.Comonad
 import Control.Monad
 import Control.Monad.IO.Class
 import Control.Monad.Primitive
 import Control.Monad.ST
 import Data.Constraint
 import Data.Extensible.Class
-import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import Data.Extensible.Wrapper
-import Control.Comonad
 import Data.Profunctor.Rep
 import Data.Profunctor.Sieve
+import Data.Proxy
 import qualified Data.StateVar as V
-import Data.Typeable (Typeable)
-import qualified Data.Extensible.HList as L
 import GHC.Types
+import qualified Type.Membership.HList as L
 
 -- | Mutable type-indexed struct.
 data Struct s (h :: k -> *) (xs :: [k]) = Struct (SmallMutableArray# s Any)
-  deriving Typeable
 
 -- | Write a value in a 'Struct'.
 set :: PrimMonad m => Struct (PrimState m) h xs -> Membership xs x -> h x -> m ()
@@ -137,7 +135,7 @@
   WrappedPointer s i $~! f = liftIO $ void $ atomicModify'_ s i $ over _Wrapper f
 
 -- | Get a 'WrappedPointer' from a name.
-(-$>) :: forall k h xs v s. (Associate k v xs) => Struct s h xs -> Proxy k -> WrappedPointer s h (Repr h (k ':> v))
+(-$>) :: forall k h xs v s. (Lookup xs k v) => Struct s h xs -> Proxy k -> WrappedPointer s h (Repr h (k ':> v))
 s -$> _ = WrappedPointer s (association :: Membership xs (k ':> v))
 {-# INLINE (-$>) #-}
 
@@ -239,6 +237,8 @@
       case copySmallArray# rhs 0# a lhsSz rhsSz s2 of { s3 ->
       case unsafeFreezeSmallArray# a s3 of { (# s4, frz #) ->
       (# s4, HProduct frz #) }}}}
+
+infixr 5 `happend`
 
 unsafeMembership :: Int -> Membership xs x
 unsafeMembership = unsafeCoerce#
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
@@ -23,10 +23,11 @@
   , embedAssoc
   ) where
 
-import Data.Extensible.Internal
-import Data.Typeable
 import Data.Extensible.Class
 import Data.Profunctor
+import Data.Proxy
+import Data.Type.Equality
+import Type.Membership
 
 -- | The extensible sum type
 --
@@ -34,7 +35,6 @@
 --
 data (h :: k -> *) :| (s :: [k]) where
   EmbedAt :: !(Membership xs x) -> h x -> h :| xs
-deriving instance Typeable (:|)
 
 instance Enum (Proxy :| xs) where
   fromEnum (EmbedAt m _) = fromIntegral $ getMemberId m
@@ -71,7 +71,7 @@
     -> (h :| xs -> r)
     -> h :| (x ': xs)
     -> r
-(<:|) r c = \(EmbedAt i h) -> leadership i
+(<:|) r c = \(EmbedAt i h) -> testMembership i
   (\Refl -> r h)
   (\j -> c (EmbedAt j h))
 infixr 1 <:|
@@ -82,7 +82,7 @@
 exhaust _ = error "Impossible"
 
 -- | Embed a value, but focuses on its key.
-embedAssoc :: Associate k a xs => h (k ':> a) -> h :| xs
+embedAssoc :: Lookup xs k a => h (k ':> a) -> h :| xs
 embedAssoc = EmbedAt association
 {-# INLINE embedAssoc #-}
 
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
@@ -15,8 +15,6 @@
   , decEffectSuite
   , customDecEffects) where
 
-import Data.Proxy
-import Data.Extensible.Internal
 import Data.Extensible.Class (itemAssoc)
 import Data.Extensible.Effect
 import Data.Extensible.Field
@@ -24,6 +22,7 @@
 import Language.Haskell.TH
 import Data.Char
 import Control.Monad
+import Type.Membership
 
 -- | Generate fields using 'itemAssoc'.
 -- @'mkField' "foo Bar"@ defines:
@@ -186,7 +185,7 @@
   -> Type -- type
   -> Name -- variable
   -> Type
-associateT nameT t xs = ConT ''Associate `AppT` nameT `AppT` t `AppT` VarT xs
+associateT nameT t xs = ConT ''Lookup `AppT` VarT xs `AppT` nameT `AppT` t
 
 effClause :: Type -- effect key
   -> Int -- number of arguments
diff --git a/src/Data/Extensible/Tangle.hs b/src/Data/Extensible/Tangle.hs
--- a/src/Data/Extensible/Tangle.hs
+++ b/src/Data/Extensible/Tangle.hs
@@ -41,10 +41,10 @@
 
 instance (Monad m, Monoid a) => Monoid (TangleT h xs m a) where
   mempty = pure mempty
-  mappend = liftA2 mappend
+  mappend = (<>)
 
 -- | 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)
+lasso :: forall k v m h xs. (Monad m, Lookup xs k v, Wrapper h)
   => FieldName k -> TangleT h xs m (Repr h (k ':> v))
 lasso _ = view _Wrapper <$> hitchAt (association :: Membership xs (k ':> v))
 {-# INLINE lasso #-}
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
@@ -136,7 +136,7 @@
 
 instance (Monoid (f a), Monoid (g a)) => Monoid (Prod f g a) where
   mempty = Prod mempty mempty
-  Prod a b `mappend` Prod c d = Prod (mappend a c) (mappend b d)
+  mappend = (<>)
 
 instance (Arbitrary (f a), Arbitrary (g a)) => Arbitrary (Prod f g a) where
   arbitrary = Prod <$> arbitrary <*> arbitrary