diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,36 @@
+# optics-core-0.4 (2021-02-22)
+* See [migration-guide-0.4.md](https://github.com/well-typed/optics/blob/master/migration-guide-0.4.md) for more details
+* Add support for GHC-9.0
+* Drop support for GHC-8.0
+* The `FunctorWithIndex`, `FoldableWithIndex` and `TraversableWithIndex` type
+  classes have been migrated to a new package,
+  [`indexed-traversable`](https://hackage.haskell.org/package/indexed-traversable)
+  ([#370](https://github.com/well-typed/optics/pull/370))
+* Add `adjoin`, `iadjoin` and `both` to `Optics.[Ix]Traversal`
+  ([#332](https://github.com/well-typed/optics/pull/332),
+   [#372](https://github.com/well-typed/optics/pull/372))
+* Add `ifst` and `isnd` to `Optics.IxLens`
+  ([#389](https://github.com/well-typed/optics/pull/389))
+* Generalize types of `generic`
+  ([#376](https://github.com/well-typed/optics/pull/376))
+* Make `chosen` an indexed lens to see which value is traversed
+  ([#335](https://github.com/well-typed/optics/pull/335))
+* Remove `GeneralLabelOptic` extensibility mechanism
+  ([#361](https://github.com/well-typed/optics/pull/361))
+* Add `gfield`, `gafield`, `gconstructor`, `gposition` and `gplate` for
+  generics-based data access
+  ([#358](https://github.com/well-typed/optics/pull/358),
+   [#361](https://github.com/well-typed/optics/pull/361))
+* Add support for generics-based field lenses and constructor prisms (`gfield`
+  and `gconstructor`) to `LabelOptic` so they can be used via `OverloadedLabels`
+  ([#361](https://github.com/well-typed/optics/pull/361))
+* Remove unnecessary INLINE pragmas to reduce compile times
+  ([#394](https://github.com/well-typed/optics/pull/394))
+* Simplify the type of `(%)` using new `JoinKinds` and `AppendIndices` classes
+  in place of the `Join` and `Append` type families
+  ([#397](https://github.com/well-typed/optics/pull/397),
+   [#399](https://github.com/well-typed/optics/pull/399))
+
 # optics-core-0.3.0.1 (2020-08-05)
 * Add INLINE pragmas to `atraverseOf_`, `iaTraverseOf_` and `ignored`
 * Improve error message in catch-all `GeneralLabelOptic` instance
diff --git a/optics-core.cabal b/optics-core.cabal
--- a/optics-core.cabal
+++ b/optics-core.cabal
@@ -1,12 +1,12 @@
 name:          optics-core
-version:       0.3.0.1
+version:       0.4
 license:       BSD3
 license-file:  LICENSE
 build-type:    Simple
 cabal-version: 1.24
 maintainer:    optics@well-typed.com
 author:        Adam Gundry, Andres Löh, Andrzej Rybczak, Oleg Grenrus
-tested-with:   GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.3 || ==8.10.1, GHCJS ==8.4
+tested-with:   GHC ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.4 || ==8.10.3, GHCJS ==8.4
 synopsis:      Optics as an abstract interface: core definitions
 category:      Data, Optics, Lenses
 description:
@@ -27,16 +27,25 @@
   location: https://github.com/well-typed/optics.git
   subdir:   optics-core
 
+flag explicit-generic-labels
+  default: False
+  manual:  True
+  description: Require explicit GenericLabelOptics instances in order to use generics-based labels
+
 library
   default-language: Haskell2010
   hs-source-dirs:   src
   ghc-options:      -Wall
 
-  build-depends: base                   >= 4.9        && <5
-               , array                  >= 0.5.1.1    && <0.6
-               , containers             >= 0.5.7.1    && <0.7
+  if flag(explicit-generic-labels)
+    cpp-options: -DEXPLICIT_GENERIC_LABELS
+
+  build-depends: base                   >= 4.10       && <5
+               , array                  >= 0.5.2.0    && <0.6
+               , containers             >= 0.5.10.2   && <0.7
                , indexed-profunctors    >= 0.1        && <0.2
                , transformers           >= 0.5        && <0.6
+               , indexed-traversable    >= 0.1        && <0.2
 
   exposed-modules: Optics.Core
 
@@ -71,6 +80,7 @@
                    Optics.Cons.Core
                    Optics.Each.Core
                    Optics.Empty.Core
+                   Optics.Generic
                    Optics.Indexed.Core
                    Optics.Mapping
                    Optics.Label
@@ -97,11 +107,14 @@
                    -- internal modules
                    Optics.Internal.Bi
                    Optics.Internal.Fold
+                   Optics.Internal.Generic
+                   Optics.Internal.Generic.TypeLevel
                    Optics.Internal.Indexed
                    Optics.Internal.Indexed.Classes
                    Optics.Internal.IxFold
                    Optics.Internal.IxSetter
                    Optics.Internal.IxTraversal
+                   Optics.Internal.Magic
                    Optics.Internal.Optic
                    Optics.Internal.Optic.Subtyping
                    Optics.Internal.Optic.TypeLevel
diff --git a/src/Data/IntMap/Optics.hs b/src/Data/IntMap/Optics.hs
--- a/src/Data/IntMap/Optics.hs
+++ b/src/Data/IntMap/Optics.hs
@@ -43,7 +43,8 @@
   , ge
   ) where
 
-import Data.IntMap as IntMap
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
 
 import Optics.IxAffineTraversal
 import Optics.IxFold
@@ -82,7 +83,7 @@
 -- Nothing
 lt :: Int -> IxAffineTraversal' Int (IntMap v) v
 lt k = iatraversalVL $ \point f s ->
-  case lookupLT k s of
+  case IntMap.lookupLT k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> IntMap.insert k' v' s
 {-# INLINE lt #-}
@@ -97,7 +98,7 @@
 -- Just (2,'y')
 gt :: Int -> IxAffineTraversal' Int (IntMap v) v
 gt k = iatraversalVL $ \point f s ->
-  case lookupGT k s of
+  case IntMap.lookupGT k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> IntMap.insert k' v' s
 {-# INLINE gt #-}
@@ -112,7 +113,7 @@
 -- Just (1,'x')
 le :: Int -> IxAffineTraversal' Int (IntMap v) v
 le k = iatraversalVL $ \point f s ->
-  case lookupLE k s of
+  case IntMap.lookupLE k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> IntMap.insert k' v' s
 {-# INLINE le #-}
@@ -127,7 +128,7 @@
 -- Just (3,'y')
 ge :: Int -> IxAffineTraversal' Int (IntMap v) v
 ge k = iatraversalVL $ \point f s ->
-  case lookupGE k s of
+  case IntMap.lookupGE k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> IntMap.insert k' v' s
 {-# INLINE ge #-}
diff --git a/src/Data/IntSet/Optics.hs b/src/Data/IntSet/Optics.hs
--- a/src/Data/IntSet/Optics.hs
+++ b/src/Data/IntSet/Optics.hs
@@ -10,7 +10,8 @@
   , setOf
   ) where
 
-import Data.IntSet as IntSet
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
 
 import Optics.Fold
 import Optics.Optic
@@ -32,7 +33,7 @@
 -- but you can manipulate it by reading using 'Optics.Fold.folded' and
 -- reindexing it via 'setmapped'.
 --
--- >>> over setmapped (+1) (fromList [1,2,3,4])
+-- >>> over setmapped (+1) (IntSet.fromList [1,2,3,4])
 -- fromList [2,3,4,5]
 setmapped :: Setter' IntSet Int
 setmapped = sets IntSet.map
diff --git a/src/Data/Map/Optics.hs b/src/Data/Map/Optics.hs
--- a/src/Data/Map/Optics.hs
+++ b/src/Data/Map/Optics.hs
@@ -50,7 +50,8 @@
   , ge
   ) where
 
-import Data.Map as Map
+import Data.Map (Map)
+import qualified Data.Map as Map
 
 import Optics.IxAffineTraversal
 import Optics.IxFold
@@ -89,7 +90,7 @@
 -- Nothing
 lt :: Ord k => k -> IxAffineTraversal' k (Map k v) v
 lt k = iatraversalVL $ \point f s ->
-  case lookupLT k s of
+  case Map.lookupLT k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> Map.insert k' v' s
 {-# INLINE lt #-}
@@ -104,7 +105,7 @@
 -- Just ('b','y')
 gt :: Ord k => k -> IxAffineTraversal' k (Map k v) v
 gt k = iatraversalVL $ \point f s ->
-  case lookupGT k s of
+  case Map.lookupGT k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> Map.insert k' v' s
 {-# INLINE gt #-}
@@ -119,7 +120,7 @@
 -- Just ('a','x')
 le :: Ord k => k -> IxAffineTraversal' k (Map k v) v
 le k = iatraversalVL $ \point f s ->
-  case lookupLE k s of
+  case Map.lookupLE k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> Map.insert k' v' s
 {-# INLINE le #-}
@@ -134,7 +135,7 @@
 -- Just ('c','y')
 ge :: Ord k => k -> IxAffineTraversal' k (Map k v) v
 ge k = iatraversalVL $ \point f s ->
-  case lookupGE k s of
+  case Map.lookupGE k s of
     Nothing      -> point s
     Just (k', v) -> f k' v <&> \v' -> Map.insert k' v' s
 {-# INLINE ge #-}
diff --git a/src/Data/Sequence/Optics.hs b/src/Data/Sequence/Optics.hs
--- a/src/Data/Sequence/Optics.hs
+++ b/src/Data/Sequence/Optics.hs
@@ -10,7 +10,8 @@
   , seqOf
   ) where
 
-import Data.Sequence as Seq
+import Data.Sequence (Seq, ViewL (..), ViewR (..), (><))
+import qualified Data.Sequence as Seq
 
 import Optics.Internal.Indexed
 import Optics.Fold
@@ -34,10 +35,10 @@
 -- >>> EmptyL ^. re viewL
 -- fromList []
 --
--- >>> review viewL $ 1 Seq.:< fromList [2,3]
+-- >>> review viewL $ 1 Seq.:< Seq.fromList [2,3]
 -- fromList [1,2,3]
 viewL :: Iso (Seq a) (Seq b) (ViewL a) (ViewL b)
-viewL = iso viewl $ \xs -> case xs of
+viewL = iso Seq.viewl $ \xs -> case xs of
   EmptyL      -> mempty
   a Seq.:< as -> a Seq.<| as
 {-# INLINE viewL #-}
@@ -55,23 +56,23 @@
 -- >>> EmptyR ^. re viewR
 -- fromList []
 --
--- >>> review viewR $ fromList [1,2] Seq.:> 3
+-- >>> review viewR $ Seq.fromList [1,2] Seq.:> 3
 -- fromList [1,2,3]
 viewR :: Iso (Seq a) (Seq b) (ViewR a) (ViewR b)
-viewR = iso viewr $ \xs -> case xs of
+viewR = iso Seq.viewr $ \xs -> case xs of
   EmptyR      -> mempty
   as Seq.:> a -> as Seq.|> a
 {-# INLINE viewR #-}
 
 -- | Traverse the first @n@ elements of a 'Seq'
 --
--- >>> fromList [1,2,3,4,5] ^.. slicedTo 2
+-- >>> Seq.fromList [1,2,3,4,5] ^.. slicedTo 2
 -- [1,2]
 --
--- >>> fromList [1,2,3,4,5] & slicedTo 2 %~ (*10)
+-- >>> Seq.fromList [1,2,3,4,5] & slicedTo 2 %~ (*10)
 -- fromList [10,20,3,4,5]
 --
--- >>> fromList [1,2,4,5,6] & slicedTo 10 .~ 0
+-- >>> Seq.fromList [1,2,4,5,6] & slicedTo 10 .~ 0
 -- fromList [0,0,0,0,0]
 slicedTo :: Int -> IxTraversal' Int (Seq a) a
 slicedTo n = conjoined noix ix
@@ -85,13 +86,13 @@
 
 -- | Traverse all but the first @n@ elements of a 'Seq'
 --
--- >>> fromList [1,2,3,4,5] ^.. slicedFrom 2
+-- >>> Seq.fromList [1,2,3,4,5] ^.. slicedFrom 2
 -- [3,4,5]
 --
--- >>> fromList [1,2,3,4,5] & slicedFrom 2 %~ (*10)
+-- >>> Seq.fromList [1,2,3,4,5] & slicedFrom 2 %~ (*10)
 -- fromList [1,2,30,40,50]
 --
--- >>> fromList [1,2,3,4,5] & slicedFrom 10 .~ 0
+-- >>> Seq.fromList [1,2,3,4,5] & slicedFrom 10 .~ 0
 -- fromList [1,2,3,4,5]
 slicedFrom :: Int -> IxTraversal' Int (Seq a) a
 slicedFrom n = conjoined noix ix
@@ -105,13 +106,13 @@
 
 -- | Traverse all the elements numbered from @i@ to @j@ of a 'Seq'
 --
--- >>> fromList [1,2,3,4,5] & sliced 1 3 %~ (*10)
+-- >>> Seq.fromList [1,2,3,4,5] & sliced 1 3 %~ (*10)
 -- fromList [1,20,30,4,5]
 --
--- >>> fromList [1,2,3,4,5] ^.. sliced 1 3
+-- >>> Seq.fromList [1,2,3,4,5] ^.. sliced 1 3
 -- [2,3]
 --
--- >>> fromList [1,2,3,4,5] & sliced 1 3 .~ 0
+-- >>> Seq.fromList [1,2,3,4,5] & sliced 1 3 .~ 0
 -- fromList [1,0,0,4,5]
 sliced :: Int -> Int -> IxTraversal' Int (Seq a) a
 sliced i j = conjoined noix ix
diff --git a/src/Data/Set/Optics.hs b/src/Data/Set/Optics.hs
--- a/src/Data/Set/Optics.hs
+++ b/src/Data/Set/Optics.hs
@@ -9,7 +9,8 @@
   , setOf
   ) where
 
-import Data.Set as Set
+import Data.Set (Set)
+import qualified Data.Set as Set
 
 import Optics.Fold
 import Optics.Optic
@@ -22,7 +23,7 @@
 -- you can manipulate it by reading using 'Optics.Fold.folded' and reindexing it
 -- via 'setmapped'.
 --
--- >>> over setmapped (+1) (fromList [1,2,3,4])
+-- >>> over setmapped (+1) (Set.fromList [1,2,3,4])
 -- fromList [2,3,4,5]
 setmapped :: Ord b => Setter (Set a) (Set b) a b
 setmapped = sets Set.map
diff --git a/src/Data/Tree/Optics.hs b/src/Data/Tree/Optics.hs
--- a/src/Data/Tree/Optics.hs
+++ b/src/Data/Tree/Optics.hs
@@ -9,7 +9,7 @@
   , branches
   ) where
 
-import Data.Tree
+import Data.Tree (Tree (..))
 
 import Optics.Lens
 
diff --git a/src/Data/Tuple/Optics.hs b/src/Data/Tuple/Optics.hs
--- a/src/Data/Tuple/Optics.hs
+++ b/src/Data/Tuple/Optics.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 -- |
 -- Module: Data.Tuple.Optics
 -- Description: 'Lens'es for tuple types.
@@ -13,18 +14,21 @@
 -- >>> set _3 True ('a','b','c')
 -- ('a','b',True)
 --
--- If a single-constructor datatype has a 'Generic' instance, the corresponding
--- @FieldN@ instances can be defined using their default methods:
+-- If a datatype has a 'Generic' instance, the corresponding @FieldN@ instances
+-- can be defined using their default methods:
 --
 -- >>> :set -XDeriveGeneric
--- >>> data T a = MkT Int a deriving (Generic, Show)
--- >>> instance Field1 (T a) (T a) Int Int
--- >>> instance Field2 (T a) (T b) a b
+-- >>> import GHC.Generics (Generic)
+-- >>> data T a b = MkT a Int b deriving (Generic, Show)
+-- >>> instance Field1 (T a c) (T b c) a b
+-- >>> instance Field2 (T a b) (T a b) Int Int
+-- >>> instance Field3 (T c a) (T c b) a b
 --
--- >>> set _2 'x' (MkT 1 False)
--- MkT 1 'x'
+-- >>> set _3 'x' (MkT False 1 ())
+-- MkT False 1 'x'
 --
-{-# LANGUAGE UndecidableInstances   #-}
+-- For a generalization of this pattern see 'GPosition'.
+--
 module Data.Tuple.Optics
   (
   -- * Tuples
@@ -43,11 +47,9 @@
 
 import Data.Functor.Identity
 import Data.Functor.Product
-import Data.Kind
-import Data.Proxy
-import GHC.Generics ((:*:)(..), Generic(..), K1, M1, U1)
+import GHC.Generics ((:*:)(..))
 
-import GHC.Generics.Optics
+import Optics.Generic
 import Optics.Lens
 import Optics.Optic
 
@@ -70,9 +72,8 @@
   -- >>> (1,2,3,4,5) & _1 %~ (+41)
   -- (42,2,3,4,5)
   _1 :: Lens s t a b
-  default _1 :: (Generic s, Generic t, GIxed N0 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _1 = ix proxyN0
+  default _1 :: GPosition 1 s t a b => Lens s t a b
+  _1 = gposition @1
   {-# INLINE[1] _1 #-}
 
 instance Field1 (Identity a) (Identity b) a b where
@@ -133,9 +134,8 @@
   -- 2
   -- (1,())
   _2 :: Lens s t a b
-  default _2 :: (Generic s, Generic t, GIxed N1 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _2 = ix proxyN1
+  default _2 :: GPosition 2 s t a b => Lens s t a b
+  _2 = gposition @2
   {-# INLINE[1] _2 #-}
 
 instance Field2 (Product f g a) (Product f g' a) (g a) (g' a) where
@@ -182,9 +182,8 @@
 class Field3 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 3rd field of a tuple.
   _3 :: Lens s t a b
-  default _3 :: (Generic s, Generic t, GIxed N2 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _3 = ix proxyN2
+  default _3 :: GPosition 3 s t a b => Lens s t a b
+  _3 = gposition @3
   {-# INLINE[1] _3 #-}
 
 instance Field3 (a,b,c) (a,b,c') c c' where
@@ -219,9 +218,8 @@
 class Field4 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 4th field of a tuple.
   _4 :: Lens s t a b
-  default _4 :: (Generic s, Generic t, GIxed N3 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _4 = ix proxyN3
+  default _4 :: GPosition 4 s t a b => Lens s t a b
+  _4 = gposition @4
   {-# INLINE[1] _4 #-}
 
 instance Field4 (a,b,c,d) (a,b,c,d') d d' where
@@ -252,9 +250,8 @@
 class Field5 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 5th field of a tuple.
   _5 :: Lens s t a b
-  default _5 :: (Generic s, Generic t, GIxed N4 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _5 = ix proxyN4
+  default _5 :: GPosition 5 s t a b => Lens s t a b
+  _5 = gposition @5
   {-# INLINE[1] _5 #-}
 
 instance Field5 (a,b,c,d,e) (a,b,c,d,e') e e' where
@@ -281,9 +278,8 @@
 class Field6 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 6th field of a tuple.
   _6 :: Lens s t a b
-  default _6 :: (Generic s, Generic t, GIxed N5 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _6 = ix proxyN5
+  default _6 :: GPosition 6 s t a b => Lens s t a b
+  _6 = gposition @6
   {-# INLINE[1] _6 #-}
 
 instance Field6 (a,b,c,d,e,f) (a,b,c,d,e,f') f f' where
@@ -306,9 +302,8 @@
 class Field7 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 7th field of a tuple.
   _7 :: Lens s t a b
-  default _7 :: (Generic s, Generic t, GIxed N6 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _7 = ix proxyN6
+  default _7 :: GPosition 7 s t a b => Lens s t a b
+  _7 = gposition @7
   {-# INLINE[1] _7 #-}
 
 instance Field7 (a,b,c,d,e,f,g) (a,b,c,d,e,f,g') g g' where
@@ -327,9 +322,8 @@
 class Field8 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 8th field of a tuple.
   _8 :: Lens s t a b
-  default _8 :: (Generic s, Generic t, GIxed N7 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _8 = ix proxyN7
+  default _8 :: GPosition 8 s t a b => Lens s t a b
+  _8 = gposition @8
   {-# INLINE[1] _8 #-}
 
 instance Field8 (a,b,c,d,e,f,g,h) (a,b,c,d,e,f,g,h') h h' where
@@ -344,9 +338,8 @@
 class Field9 s t a b | s -> a, t -> b, s b -> t, t a -> s where
   -- | Access the 9th field of a tuple.
   _9 :: Lens s t a b
-  default _9 :: (Generic s, Generic t, GIxed N8 (Rep s) (Rep t) a b)
-             => Lens s t a b
-  _9 = ix proxyN8
+  default _9 :: GPosition 9 s t a b => Lens s t a b
+  _9 = gposition @9
   {-# INLINE[1] _9 #-}
 
 instance Field9 (a,b,c,d,e,f,g,h,i) (a,b,c,d,e,f,g,h,i') i i' where
@@ -399,122 +392,6 @@
 _9' :: Field9 s t a b => Lens s t a b
 _9' = equality' % _9
 {-# INLINE _9' #-}
-
-ix :: (Generic s, Generic t, GIxed n (Rep s) (Rep t) a b) => f n -> Lens s t a b
-ix n = generic % gix n
-{-# INLINE ix #-}
-
--- TODO: this can be replaced by generic-optics position
-type family GSize (f :: Type -> Type)
-type instance GSize U1 = Z
-type instance GSize (K1 i c) = S Z
-type instance GSize (M1 i c f) = GSize f
-type instance GSize (a :*: b) = Add (GSize a) (GSize b)
-
-class GIxed n s t a b | n s -> a, n t -> b, n s b -> t, n t a -> s where
-  gix :: f n -> Lens (s x) (t x) a b
-
-instance GIxed N0 (K1 i a) (K1 i b) a b where
-  gix _ = castOptic _K1
-  {-# INLINE gix #-}
-
-instance GIxed n s t a b => GIxed n (M1 i c s) (M1 i c t) a b where
-  gix n = _M1 % gix n
-  {-# INLINE gix #-}
-
-instance (p ~ GT (GSize s) n,
-          p ~ GT (GSize t) n,
-          GIxed' p n s s' t t' a b)
-      => GIxed n (s :*: s') (t :*: t') a b where
-  gix = gix' (Proxy @p)
-  {-# INLINE gix #-}
-
-class (p ~ GT (GSize s) n,
-       p ~ GT (GSize t) n)
-   => GIxed' p n s s' t t' a b | p n s s' -> a
-                               , p n t t' -> b
-                               , p n s s' b -> t t'
-                               , p n t t' a -> s s' where
-  gix' :: f p -> g n -> Lens ((s :*: s') x) ((t :*: t') x) a b
-
-instance (GT (GSize s) n ~ T,
-          GT (GSize t) n ~ T,
-          GIxed n s t a b)
-      => GIxed' T n s s' t s' a b where
-  gix' _ n = _1 % gix n
-  {-# INLINE gix' #-}
-
-instance (GT (GSize s) n ~ F,
-          n' ~ Subtract (GSize s) n,
-          GIxed n' s' t' a b)
-      => GIxed' F n s s' s t' a b where
-  gix' _ _ = _2 % gix (Proxy @n')
-  {-# INLINE gix' #-}
-
-data Z
-data S a
-
-data T
-data F
-
-type family Add x y
-type instance Add Z y = y
-type instance Add (S x) y = S (Add x y)
-
-type family Subtract x y
-type instance Subtract Z x = x
-type instance Subtract (S x) (S y) = Subtract x y
-
-type family GT x y
-type instance GT Z x = F
-type instance GT (S x) Z = T
-type instance GT (S x) (S y) = GT x y
-
-type N0 = Z
-type N1 = S N0
-type N2 = S N1
-type N3 = S N2
-type N4 = S N3
-type N5 = S N4
-type N6 = S N5
-type N7 = S N6
-type N8 = S N7
-
-proxyN0 :: Proxy N0
-proxyN0 = Proxy
-{-# INLINE proxyN0 #-}
-
-proxyN1 :: Proxy N1
-proxyN1 = Proxy
-{-# INLINE proxyN1 #-}
-
-proxyN2 :: Proxy N2
-proxyN2 = Proxy
-{-# INLINE proxyN2 #-}
-
-proxyN3 :: Proxy N3
-proxyN3 = Proxy
-{-# INLINE proxyN3 #-}
-
-proxyN4 :: Proxy N4
-proxyN4 = Proxy
-{-# INLINE proxyN4 #-}
-
-proxyN5 :: Proxy N5
-proxyN5 = Proxy
-{-# INLINE proxyN5 #-}
-
-proxyN6 :: Proxy N6
-proxyN6 = Proxy
-{-# INLINE proxyN6 #-}
-
-proxyN7 :: Proxy N7
-proxyN7 = Proxy
-{-# INLINE proxyN7 #-}
-
-proxyN8 :: Proxy N8
-proxyN8 = Proxy
-{-# INLINE proxyN8 #-}
 
 -- $setup
 -- >>> import Optics.Core
diff --git a/src/GHC/Generics/Optics.hs b/src/GHC/Generics/Optics.hs
--- a/src/GHC/Generics/Optics.hs
+++ b/src/GHC/Generics/Optics.hs
@@ -1,13 +1,12 @@
-{-# LANGUAGE PolyKinds #-}
 -- |
 -- Module: GHC.Generics.Optics
 -- Description: Optics for types defined in "GHC.Generics".
 --
--- Note: "GHC.Generics" exports a number of names that collide with "Optics"
+-- /Note:/ "GHC.Generics" exports a number of names that collide with "Optics"
 -- (at least 'GHC.Generics.to').
 --
--- You can use hiding or imports to mitigate this to an extent, and the
--- following imports, represent a fair compromise for user code:
+-- You can use hiding of imports to mitigate this to an extent. The following
+-- imports represent a fair compromise for user code:
 --
 -- @
 -- import "Optics"
@@ -31,66 +30,4 @@
   , _R1
   ) where
 
-import qualified GHC.Generics as GHC (to, from, to1, from1)
-import GHC.Generics (Generic, Rep, Generic1, Rep1, (:+:) (..), V1, U1 (..),
-                     K1 (..), M1 (..), Par1 (..), Rec1 (..))
-
-import Optics.Iso
-import Optics.Lens
-import Optics.Prism
-
--- | Convert from the data type to its representation (or back)
---
--- >>> view (generic % re generic) "hello" :: String
--- "hello"
---
-generic :: (Generic a, Generic b) => Iso a b (Rep a c) (Rep b c)
-generic = iso GHC.from GHC.to
-{-# INLINE generic #-}
-
--- | Convert from the data type to its representation (or back)
-generic1 :: (Generic1 f, Generic1 g) => Iso (f a) (g b) (Rep1 f a) (Rep1 g b)
-generic1 = iso GHC.from1 GHC.to1
-{-# INLINE generic1 #-}
-
-_V1 :: Lens (V1 s) (V1 t) a b
-_V1 = lens absurd absurd where
-  absurd !_a = undefined
-{-# INLINE _V1 #-}
-
-_U1 :: Iso (U1 p) (U1 q) () ()
-_U1 = iso (const ()) (const U1)
-{-# INLINE _U1 #-}
-
-_Par1 :: Iso (Par1 p) (Par1 q) p q
-_Par1 = iso unPar1 Par1
-{-# INLINE _Par1 #-}
-
-_Rec1 :: Iso (Rec1 f p) (Rec1 g q) (f p) (g q)
-_Rec1 = iso unRec1 Rec1
-{-# INLINE _Rec1 #-}
-
-_K1 :: Iso (K1 i c p) (K1 j d q) c d
-_K1 = iso unK1 K1
-{-# INLINE _K1 #-}
-
-_M1 :: Iso (M1 i c f p) (M1 j d g q) (f p) (g q)
-_M1 = iso unM1 M1
-{-# INLINE _M1 #-}
-
-_L1 :: Prism ((a :+: c) t) ((b :+: c) t) (a t) (b t)
-_L1 = prism L1 reviewer
-  where
-  reviewer (L1 v) = Right v
-  reviewer (R1 v) = Left (R1 v)
-{-# INLINE _L1 #-}
-
-_R1 :: Prism ((c :+: a) t) ((c :+: b) t) (a t) (b t)
-_R1 = prism R1 reviewer
-  where
-  reviewer (R1 v) = Right v
-  reviewer (L1 v) = Left (L1 v)
-{-# INLINE _R1 #-}
-
--- $setup
--- >>> import Optics.Core
+import Optics.Internal.Generic
diff --git a/src/Optics/At/Core.hs b/src/Optics/At/Core.hs
--- a/src/Optics/At/Core.hs
+++ b/src/Optics/At/Core.hs
@@ -42,19 +42,26 @@
   , Contains(..)
   ) where
 
-import Data.Array.IArray as Array
-import Data.Array.Unboxed
-import Data.Complex
-import Data.Functor.Identity
-import Data.IntMap as IntMap
-import Data.IntSet as IntSet
+import qualified Data.Array.IArray as Array
+import Data.Array.Unboxed (UArray)
+import Data.Complex (Complex (..))
+import Data.Ix (Ix (..))
+import Data.Functor.Identity (Identity (..))
 import Data.Kind (Type)
-import Data.List.NonEmpty as NonEmpty
-import Data.Map as Map
-import Data.Sequence as Seq
-import Data.Set as Set
-import Data.Tree
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Tree (Tree (..))
 
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+import Data.Set (Set)
+import qualified Data.Set as Set
+
 import Data.Maybe.Optics
 import Optics.AffineTraversal
 import Optics.Iso
@@ -239,7 +246,7 @@
 -- @
 instance Ix i => Ixed (Array.Array i e) where
   ix i = atraversalVL $ \point f arr ->
-    if inRange (bounds arr) i
+    if inRange (Array.bounds arr) i
     then f (arr Array.! i) <&> \e -> arr Array.// [(i,e)]
     else point arr
   {-# INLINE ix #-}
@@ -250,9 +257,9 @@
 -- arr 'Array.!' i ≡ arr 'Optics.Operators.^.' 'ix' i
 -- arr '//' [(i,e)] ≡ 'ix' i 'Optics.Operators..~' e '$' arr
 -- @
-instance (IArray UArray e, Ix i) => Ixed (UArray i e) where
+instance (Array.IArray UArray e, Ix i) => Ixed (UArray i e) where
   ix i = atraversalVL $ \point f arr ->
-    if inRange (bounds arr) i
+    if inRange (Array.bounds arr) i
     then f (arr Array.! i) <&> \e -> arr Array.// [(i,e)]
     else point arr
   {-# INLINE ix #-}
@@ -437,27 +444,11 @@
   {-# INLINE at #-}
 
 instance At (IntMap a) where
-#if MIN_VERSION_containers(0,5,8)
   at k = lensVL $ \f -> IntMap.alterF f k
-#else
-  at k = lensVL $ \f m ->
-    let mv = IntMap.lookup k m
-    in f mv <&> \r -> case r of
-      Nothing -> maybe m (const (IntMap.delete k m)) mv
-      Just v' -> IntMap.insert k v' m
-#endif
   {-# INLINE at #-}
 
 instance Ord k => At (Map k a) where
-#if MIN_VERSION_containers(0,5,8)
   at k = lensVL $ \f -> Map.alterF f k
-#else
-  at k = lensVL $ \f m ->
-    let mv = Map.lookup k m
-    in f mv <&> \r -> case r of
-      Nothing -> maybe m (const (Map.delete k m)) mv
-      Just v' -> Map.insert k v' m
-#endif
   {-# INLINE at #-}
 
 instance At IntSet where
diff --git a/src/Optics/Core.hs b/src/Optics/Core.hs
--- a/src/Optics/Core.hs
+++ b/src/Optics/Core.hs
@@ -56,6 +56,7 @@
 import Optics.Cons.Core                        as P
 import Optics.Each.Core                        as P
 import Optics.Empty.Core                       as P
+import Optics.Generic                          as P
 import Optics.Mapping                          as P
 import Optics.Operators                        as P
 import Optics.Re                               as P
diff --git a/src/Optics/Each/Core.hs b/src/Optics/Each/Core.hs
--- a/src/Optics/Each/Core.hs
+++ b/src/Optics/Each/Core.hs
@@ -16,16 +16,22 @@
     Each(..)
   ) where
 
-import Data.Array
-import Data.Complex
-import Data.Functor.Identity
-import Data.IntMap as IntMap
-import Data.List.NonEmpty
-import Data.Map as Map
-import Data.Sequence as Seq
-import Data.Tree as Tree
+import Data.Complex (Complex (..))
+import Data.Functor.Identity (Identity (..))
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Tree (Tree (..))
+import Data.Ix (Ix)
 
+import Data.Array (Array)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Sequence (Seq)
+
+import Optics.IxLens
 import Optics.IxTraversal
+import Optics.Optic
 
 -- | Extract 'each' element of a (potentially monomorphic) container.
 --
@@ -148,9 +154,7 @@
 instance
   (a ~ a', b ~ b'
   ) => Each (Either () ()) (Either a a') (Either b b') a b where
-  each = itraversalVL $ \f -> \case
-    Left  a -> Left  <$> f (Left ())  a
-    Right a -> Right <$> f (Right ()) a
+  each = castOptic chosen
   {-# INLINE[1] each #-}
 
 -- | @'each' :: ('RealFloat' a, 'RealFloat' b) => 'IxTraversal' (Either () ())
diff --git a/src/Optics/Empty/Core.hs b/src/Optics/Empty/Core.hs
--- a/src/Optics/Empty/Core.hs
+++ b/src/Optics/Empty/Core.hs
@@ -24,12 +24,17 @@
   ) where
 
 import Control.Applicative (ZipList(..))
-import Data.IntMap as IntMap
-import Data.IntSet as IntSet
-import Data.Map as Map
-import Data.Maybe
-import Data.Monoid
-import Data.Set as Set
+import Data.Maybe (isNothing)
+import Data.Monoid (Any (..), All (..), Product (..), Sum (..), Last (..), First (..), Dual (..))
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import Data.Map (Map)
+import qualified Data.Map as Map
 import qualified Data.Sequence as Seq
 
 import Data.Profunctor.Indexed
@@ -43,7 +48,7 @@
 import Optics.Review
 
 #if !defined(mingw32_HOST_OS) && !defined(ghcjs_HOST_OS)
-import GHC.Event
+import GHC.Event (Event)
 #endif
 
 -- | Class for types that may be '_Empty'.
diff --git a/src/Optics/Fold.hs b/src/Optics/Fold.hs
--- a/src/Optics/Fold.hs
+++ b/src/Optics/Fold.hs
@@ -75,8 +75,8 @@
   , pre
   , backwards_
 
-  -- * Monoid structures
-  -- | 'Fold' admits (at least) two monoid structures: #monoids#
+  -- * Monoid structures #monoids#
+  -- | 'Fold' admits (at least) two monoid structures:
   --
   -- * 'summing' concatenates results from both folds.
   --
@@ -267,6 +267,7 @@
 -- >>> toListOf (_1 % ix 0 `summing` _2 % ix 1) ([1,2], [4,7,1])
 -- [1,7]
 --
+-- For the traversal version see 'Optics.Traversal.adjoin'.
 summing
   :: (Is k A_Fold, Is l A_Fold)
   => Optic' k is s a
diff --git a/src/Optics/Generic.hs b/src/Optics/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Generic.hs
@@ -0,0 +1,385 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- |
+-- Module: Optics.Generic
+-- Description: Data access via the 'Generic' type class.
+--
+-- This module provides, for data types having a 'Generic' instance, a way to
+-- focus on:
+--
+-- - their named total fields via 'gfield',
+--
+-- - their named partial fields via 'gafield',
+--
+-- - their constructors via 'gconstructor',
+--
+-- - their fields at a specific position via 'gposition',
+--
+-- - their fields of a specific type via 'gplate'.
+--
+-- /Note:/ 'gfield' and 'gconstructor' are supported by
+-- 'Optics.Label.labelOptic' and can be used with a consise syntax via
+-- @OverloadedLabels@.
+--
+-- If you're looking for optics for working with a generic representation of a
+-- data type, there's "GHC.Generics.Optics".
+--
+module Optics.Generic
+  (
+  -- * Fields
+    GField(..)
+  , GAffineField(..)
+
+  -- * Positions
+  , GPosition(..)
+
+  -- * Constructors
+  , GConstructor(..)
+
+  -- * Types
+  , GPlate(..)
+  ) where
+
+import Data.Type.Bool
+import GHC.Generics (Generic, Rep)
+import GHC.TypeLits
+
+import Optics.AffineTraversal
+import Optics.Internal.Generic
+import Optics.Internal.Magic
+import Optics.Internal.Optic
+import Optics.Lens
+import Optics.Prism
+import Optics.Traversal
+
+-- | Hidden type for preventing GHC from solving constraints too early.
+data Void0
+
+-- | Focus on a field @name@ of type @a@ within a type @s@ using its 'Generic'
+-- instance.
+--
+-- >>> :{
+-- data User a
+--   = User { name :: String
+--          , age  :: a
+--          }
+--   | LazyUser { name :: String
+--              , age  :: a
+--              , lazy :: Bool
+--              }
+--   deriving (Show, Generic)
+-- :}
+--
+-- >>> let user = User "Tom" 32 :: User Int
+--
+-- >>> user ^. gfield @"name"
+-- "Tom"
+--
+-- >>> user ^. gfield @"age"
+-- 32
+--
+-- >>> user ^. gfield @"salary"
+-- ...
+-- ...Data constructor ‘User’ doesn't have a field named ‘salary’
+-- ...In the...
+-- ...
+--
+-- Only total fields are accessible (for partial ones see 'gafield'):
+--
+-- >>> user ^. gfield @"lazy"
+-- ...
+-- ...Data constructor ‘User’ doesn't have a field named ‘lazy’
+-- ...In the...
+-- ...
+--
+-- Type changing updates are supported:
+--
+-- >>> user & gfield @"age" .~ ()
+-- User {name = "Tom", age = ()}
+--
+-- Types without a 'Generic' instance are not supported:
+--
+-- >>> NoG 'x' ^. gfield @"any"
+-- ...
+-- ...Type ‘NoG’ doesn't have a Generic instance
+-- ...In the...
+-- ...
+--
+-- /Note:/ 'gfield' is supported by 'Optics.Label.labelOptic' and can be used
+-- with a concise syntax via @OverloadedLabels@.
+--
+-- >>> user ^. #name
+-- "Tom"
+--
+-- >>> user & #age %~ (+1)
+-- User {name = "Tom", age = 33}
+--
+-- @since 0.4
+--
+class GField (name :: Symbol) s t a b | name s -> t a b
+                                      , name t -> s a b where
+  gfield :: Lens s t a b
+
+instance GFieldContext name s t a b => GField name s t a b where
+  gfield = gfieldImpl @name
+
+-- | Hide implementation from haddock.
+type GFieldContext name s t a b =
+  ( s `HasShapeOf` t
+  , t `HasShapeOf` s
+  , Unless (Defined (Rep s)) (NoGenericError s)
+  , Unless (Defined (Rep t)) (NoGenericError t)
+  , GFieldImpl name s t a b
+  , Dysfunctional name () s t a b
+  )
+
+-- | Hidden instance.
+instance (a ~ Void0, b ~ Void0) => GField name Void0 Void0 a b where
+  gfield = lensVL id
+
+-- | Focus on a possibly partial field @name@ of type @a@ within a type @s@
+-- using its 'Generic' instance.
+--
+-- >>> :{
+-- data Fish = Herring { name :: String }
+--           | Tuna    { name :: String, sleeping :: Bool }
+--   deriving Generic
+-- :}
+--
+-- >>> let herring = Herring { name = "Henry" }
+-- >>> let tuna    = Tuna { name = "Tony", sleeping = True }
+--
+-- >>> herring ^? gafield @"name"
+-- Just "Henry"
+--
+-- >>> herring ^? gafield @"sleeping"
+-- Nothing
+--
+-- >>> tuna ^? gafield @"sleeping"
+-- Just True
+--
+-- Types without a 'Generic' instance are not supported:
+--
+-- >>> NoG 'x' ^? gafield @"any"
+-- ...
+-- ...Type ‘NoG’ doesn't have a Generic instance
+-- ...In the...
+-- ...
+--
+-- /Note:/ trying to access a field that doesn't exist in any data constructor
+-- results in an error:
+--
+-- >>> tuna ^? gafield @"salary"
+-- ...
+-- ...Type ‘Fish’ doesn't have a field named ‘salary’
+-- ...In the...
+-- ...
+--
+-- @since 0.4
+--
+class GAffineField (name :: Symbol) s t a b | name s -> t a b
+                                            , name t -> s a b where
+  gafield :: AffineTraversal s t a b
+
+instance GAFieldContext repDefined name s t a b => GAffineField name s t a b where
+  gafield = gafieldImpl @repDefined @name
+
+-- | Hide implementation from haddock.
+type GAFieldContext repDefined name s t a b =
+  ( s `HasShapeOf` t
+  , t `HasShapeOf` s
+  , repDefined ~ (Defined (Rep s) && Defined (Rep t))
+  , Unless (Defined (Rep s)) (NoGenericError s)
+  , Unless (Defined (Rep t)) (NoGenericError t)
+  , GAffineFieldImpl repDefined name s t a b
+  , Dysfunctional name () s t a b
+  )
+
+-- | Hidden instance.
+instance (a ~ Void0, b ~ Void0) => GAffineField name Void0 Void0 a b where
+  gafield = atraversalVL (\_ _ -> \case {})
+
+-- | Focus on a field at position @n@ of type @a@ within a type @s@ using its
+-- 'Generic' instance.
+--
+-- >>> ('a', 'b', 'c') ^. gposition @2
+-- 'b'
+--
+-- >>> ('a', 'b') & gposition @1 .~ "hi" & gposition @2 .~ "there"
+-- ("hi","there")
+--
+-- >>> ('a', 'b', 'c') ^. gposition @4
+-- ...
+-- ...Data constructor ‘(,,)’ has 3 fields, 4th requested
+-- ...In the...
+-- ...
+--
+-- >>> () ^. gposition @1
+-- ...
+-- ...Data constructor ‘()’ has no fields, 1st requested
+-- ...In the...
+-- ...
+--
+-- Types without a 'Generic' instance are not supported:
+--
+-- >>> NoG 'x' ^. gposition @1
+-- ...
+-- ...Type ‘NoG’ doesn't have a Generic instance
+-- ...In the...
+-- ...
+--
+-- /Note:/ Positions start from @1@:
+--
+-- >>> ('a', 'b') ^. gposition @0
+-- ...
+-- ...There is no 0th position
+-- ...In the...
+-- ...
+--
+-- @since 0.4
+--
+class GPosition (n :: Nat) s t a b | n s -> t a b
+                                   , n t -> s a b where
+  gposition :: Lens s t a b
+
+instance GPositionContext repDefined n s t a b => GPosition n s t a b where
+  gposition = gpositionImpl @repDefined @n
+
+-- | Hide implementation from haddock.
+type GPositionContext repDefined n s t a b =
+  ( s `HasShapeOf` t
+  , t `HasShapeOf` s
+  , repDefined ~ (Defined (Rep s) && Defined (Rep t))
+  , Unless (Defined (Rep s)) (NoGenericError s)
+  , Unless (Defined (Rep t)) (NoGenericError t)
+  , GPositionImpl repDefined n s t a b
+  , Dysfunctional n () s t a b
+  )
+
+-- | Hidden instance.
+instance (a ~ Void0, b ~ Void0) => GPosition name Void0 Void0 a b where
+  gposition = lensVL id
+
+-- | Focus on a constructor @name@ of a type @s@ using its 'Generic' instance.
+--
+-- >>> :{
+-- data Animal = Dog { name :: String, age :: Int }
+--             | Cat { name :: String, purrs :: Bool }
+--   deriving (Show, Generic)
+-- :}
+--
+-- >>> let dog = Dog "Sparky" 2
+-- >>> let cat = Cat "Cuddly" True
+--
+-- >>> dog ^? gconstructor @"Dog"
+-- Just ("Sparky",2)
+--
+-- >>> dog ^? gconstructor @"Cat"
+-- Nothing
+--
+-- >>> cat & gconstructor @"Cat" % _2 %~ not
+-- Cat {name = "Cuddly", purrs = False}
+--
+-- >>> dog & gconstructor @"Cat" % _1 .~ "Merry"
+-- Dog {name = "Sparky", age = 2}
+--
+-- >>> cat ^? gconstructor @"Parrot"
+-- ...
+-- ...Type ‘Animal’ doesn't have a constructor named ‘Parrot’
+-- ...In the...
+-- ...
+--
+-- Types without a 'Generic' instance are not supported:
+--
+-- >>> NoG 'x' ^. gconstructor @"NoG"
+-- ...
+-- ...Type ‘NoG’ doesn't have a Generic instance
+-- ...In the...
+-- ...
+--
+-- /Note:/ 'gconstructor' is supported by 'Optics.Label.labelOptic' and can be
+-- used with a concise syntax via @OverloadedLabels@.
+--
+-- >>> dog ^? #_Dog
+-- Just ("Sparky",2)
+--
+-- >>> cat & #_Cat % _1 .~ "Merry"
+-- Cat {name = "Merry", purrs = True}
+--
+-- @since 0.4
+--
+class GConstructor (name :: Symbol) s t a b | name s -> t a b
+                                            , name t -> s a b where
+  gconstructor :: Prism s t a b
+
+instance GConstructorContext repDefined name s t a b => GConstructor name s t a b where
+  gconstructor = gconstructorImpl @repDefined @name
+
+-- | Hide implementation from haddock.
+type GConstructorContext repDefined name s t a b =
+  ( s `HasShapeOf` t
+  , t `HasShapeOf` s
+  , repDefined ~ (Defined (Rep s) && Defined (Rep t))
+  , Unless (Defined (Rep s)) (NoGenericError s)
+  , Unless (Defined (Rep t)) (NoGenericError t)
+  , GConstructorImpl repDefined name s t a b
+  , Dysfunctional name () s t a b
+  )
+-- | Hidden instance.
+instance (a ~ Void0, b ~ Void0) => GConstructor name Void0 Void0 a b where
+  gconstructor = prism id (\case {})
+
+-- | Traverse occurrences of a type @a@ within a type @s@ using its 'Generic'
+-- instance.
+--
+-- >>> toListOf (gplate @Char) ('h', ((), 'e', Just 'l'), "lo")
+-- "hello"
+--
+-- If @a@ occurs recursively in its own definition, only outermost occurrences
+-- of @a@ within @s@ will be traversed:
+--
+-- >>> toListOf (gplate @String) ("one","two")
+-- ["one","two"]
+--
+-- /Note:/ types without a 'Generic' instance in scope when 'GPlate' class
+-- constraint is resolved will not be entered during the traversal.
+--
+-- >>> let noG = (NoG 'n', (Just 'i', "c"), 'e')
+--
+-- >>> toListOf (gplate @Char) noG
+-- "ice"
+--
+-- >>> deriving instance Generic NoG
+--
+-- >>> toListOf (gplate @Char) noG
+-- "nice"
+--
+-- @since 0.4
+--
+class GPlate a s where
+  gplate :: Traversal' s a
+
+instance GPlateContext a s => GPlate a s where
+  gplate = traversalVL (gplateInner @'True)
+  {-# INLINE gplate #-}
+
+-- | Hide implementation from haddock.
+type GPlateContext a s =
+  ( Generic s
+  , GPlateImpl (Rep s) a
+  )
+
+-- | Hidden instance.
+instance GPlate a Void0 where
+  gplate = error "unreachable"
+-- | Hidden instance.
+instance GPlate Void0 a where
+  gplate = error "unreachable"
+
+-- $setup
+-- >>> :set -XDataKinds -XDeriveGeneric -XStandaloneDeriving -XOverloadedLabels
+-- >>> import Optics.Core
+-- >>> newtype NoG = NoG { fromNoG :: Char }
diff --git a/src/Optics/Indexed/Core.hs b/src/Optics/Indexed/Core.hs
--- a/src/Optics/Indexed/Core.hs
+++ b/src/Optics/Indexed/Core.hs
@@ -75,8 +75,7 @@
 --
 infixl 9 <%>
 (<%>)
-  :: (m ~ Join k l, Is k m, Is l m, IxOptic m s t a b,
-      is `HasSingleIndex` i, js `HasSingleIndex` j)
+  :: (JoinKinds k l m, IxOptic m s t a b, is `HasSingleIndex` i, js `HasSingleIndex` j)
   => Optic k is              s t u v
   -> Optic l js              u v a b
   -> Optic m (WithIx (i, j)) s t a b
@@ -91,7 +90,7 @@
 --
 infixl 9 %>
 (%>)
-  :: (m ~ Join k l, Is k m, Is l m, IxOptic k s t u v, NonEmptyIndices is)
+  :: (JoinKinds k l m, IxOptic k s t u v, NonEmptyIndices is)
   => Optic k is s t u v
   -> Optic l js u v a b
   -> Optic m js s t a b
@@ -106,7 +105,7 @@
 --
 infixl 9 <%
 (<%)
-  :: (m ~ Join k l, Is l m, Is k m, IxOptic l u v a b, NonEmptyIndices js)
+  :: (JoinKinds k l m, IxOptic l u v a b, NonEmptyIndices js)
   => Optic k is s t u v
   -> Optic l js u v a b
   -> Optic m is s t a b
diff --git a/src/Optics/Internal/Bi.hs b/src/Optics/Internal/Bi.hs
--- a/src/Optics/Internal/Bi.hs
+++ b/src/Optics/Internal/Bi.hs
@@ -21,9 +21,6 @@
   bimap  _f g = Tagged #. g .# unTagged
   first  _f   = coerce
   second    g = Tagged #. g .# unTagged
-  {-# INLINE bimap #-}
-  {-# INLINE first #-}
-  {-# INLINE second #-}
 
 -- | Class for contravariant bifunctors.
 class Bicontravariant p where
@@ -35,33 +32,21 @@
   contrabimap  f _g (Forget k) = Forget (k . f)
   contrafirst  f    (Forget k) = Forget (k . f)
   contrasecond   _g (Forget k) = Forget k
-  {-# INLINE contrabimap #-}
-  {-# INLINE contrafirst #-}
-  {-# INLINE contrasecond #-}
 
 instance Bicontravariant (ForgetM r) where
   contrabimap  f _g (ForgetM k) = ForgetM (k . f)
   contrafirst  f    (ForgetM k) = ForgetM (k . f)
   contrasecond   _g (ForgetM k) = ForgetM k
-  {-# INLINE contrabimap #-}
-  {-# INLINE contrafirst #-}
-  {-# INLINE contrasecond #-}
 
 instance Bicontravariant (IxForget r) where
   contrabimap  f _g (IxForget k) = IxForget (\i -> k i . f)
   contrafirst  f    (IxForget k) = IxForget (\i -> k i . f)
   contrasecond   _g (IxForget k) = IxForget k
-  {-# INLINE contrabimap #-}
-  {-# INLINE contrafirst #-}
-  {-# INLINE contrasecond #-}
 
 instance Bicontravariant (IxForgetM r) where
   contrabimap  f _g (IxForgetM k) = IxForgetM (\i -> k i . f)
   contrafirst  f    (IxForgetM k) = IxForgetM (\i -> k i . f)
   contrasecond   _g (IxForgetM k) = IxForgetM k
-  {-# INLINE contrabimap #-}
-  {-# INLINE contrafirst #-}
-  {-# INLINE contrasecond #-}
 
 ----------------------------------------
 
@@ -69,10 +54,8 @@
 -- phantom.
 lphantom :: (Profunctor p, Bifunctor p) => p i a c -> p i b c
 lphantom = first absurd . lmap absurd
-{-# INLINE lphantom #-}
 
 -- | If @p@ is a 'Profunctor' and 'Bicontravariant' then its right parameter
 -- must be phantom.
 rphantom :: (Profunctor p, Bicontravariant p) => p i c a -> p i c b
 rphantom = rmap absurd . contrasecond absurd
-{-# INLINE rphantom #-}
diff --git a/src/Optics/Internal/Fold.hs b/src/Optics/Internal/Fold.hs
--- a/src/Optics/Internal/Fold.hs
+++ b/src/Optics/Internal/Fold.hs
@@ -64,8 +64,6 @@
 instance Monoid (Leftmost a) where
   mempty  = LPure
   mappend = (SG.<>)
-  {-# INLINE mempty #-}
-  {-# INLINE mappend #-}
 
 -- | Extract the 'Leftmost' element. This will fairly eagerly determine that it
 -- can return 'Just' the moment it sees any element at all.
@@ -98,8 +96,6 @@
 instance Monoid (Rightmost a) where
   mempty  = RPure
   mappend = (SG.<>)
-  {-# INLINE mempty #-}
-  {-# INLINE mappend #-}
 
 -- | Extract the 'Rightmost' element. This will fairly eagerly determine that it
 -- can return 'Just' the moment it sees any element at all.
diff --git a/src/Optics/Internal/Generic.hs b/src/Optics/Internal/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Internal/Generic.hs
@@ -0,0 +1,556 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+-- This module is intended for internal use only, and may change without warning
+-- in subsequent releases.
+module Optics.Internal.Generic
+  ( generic
+  , generic1
+  , _V1
+  , _U1
+  , _Par1
+  , _Rec1
+  , _K1
+  , _M1
+  , _L1
+  , _R1
+  -- * Fields
+  , GFieldImpl(..)
+  , GSetFieldSum(..)
+  , GSetFieldProd(..)
+  , GAffineFieldImpl(..)
+  , GAffineFieldSum(..)
+  , GFieldProd(..)
+  -- * Positions
+  , GPositionImpl(..)
+  , GPositionSum(..)
+  -- * Constructors
+  , GConstructorImpl(..)
+  , GConstructorSum(..)
+  , GConstructorTuple(..)
+  -- * Types
+  , GPlateImpl(..)
+  , GPlateInner(..)
+  -- * Re-export
+  , module Optics.Internal.Generic.TypeLevel
+  ) where
+
+import Data.Type.Bool
+import GHC.Generics
+import GHC.Records
+import GHC.TypeLits
+
+import Optics.AffineTraversal
+import Optics.Internal.Generic.TypeLevel
+import Optics.Internal.Magic
+import Optics.Internal.Optic
+import Optics.Iso
+import Optics.Lens
+import Optics.Prism
+import Optics.Traversal
+
+----------------------------------------
+-- GHC.Generics
+
+-- | Convert from the data type to its representation (or back)
+--
+-- >>> view (generic % re generic) "hello" :: String
+-- "hello"
+--
+generic :: (Generic a, Generic b) => Iso a b (Rep a x) (Rep b y)
+generic = iso from to
+
+-- | Convert from the data type to its representation (or back)
+generic1 :: (Generic1 f, Generic1 g) => Iso (f x) (g y) (Rep1 f x) (Rep1 g y)
+generic1 = iso from1 to1
+
+_V1 :: Lens (V1 s) (V1 t) a b
+_V1 = lensVL (\_ -> \case {})
+
+_U1 :: Iso (U1 p) (U1 q) () ()
+_U1 = iso (const ()) (const U1)
+
+_Par1 :: Iso (Par1 p) (Par1 q) p q
+_Par1 = coerced
+
+_Rec1 :: Iso (Rec1 f p) (Rec1 g q) (f p) (g q)
+_Rec1 = coerced
+
+_K1 :: Iso (K1 i c p) (K1 j d q) c d
+_K1 = coerced
+
+_M1 :: Iso (M1 i c f p) (M1 j d g q) (f p) (g q)
+_M1 = coerced
+
+_L1 :: Prism ((a :+: c) t) ((b :+: c) t) (a t) (b t)
+_L1 = prism L1 reviewer
+  where
+    reviewer (L1 v) = Right v
+    reviewer (R1 v) = Left (R1 v)
+
+_R1 :: Prism ((c :+: a) t) ((c :+: b) t) (a t) (b t)
+_R1 = prism R1 reviewer
+  where
+    reviewer (R1 v) = Right v
+    reviewer (L1 v) = Left (L1 v)
+
+----------------------------------------
+-- Field
+
+class GFieldImpl (name :: Symbol) s t a b | name s -> a
+                                       {- These hold morally, but we can't prove it.
+                                          , name t -> b
+                                          , name s b -> t
+                                          , name t a -> s -} where
+  gfieldImpl :: Lens s t a b
+
+instance
+  ( Generic s
+  , Generic t
+  , path ~ GetFieldPaths s name (Rep s)
+  , HasField name s a
+  , GSetFieldSum path (Rep s) (Rep t) b
+  ) => GFieldImpl name s t a b where
+  gfieldImpl = lens (getField @name) (\s -> to . gsetFieldSum @path (from s))
+  {-# INLINE gfieldImpl #-}
+
+----------------------------------------
+
+class GSetFieldSum (path :: PathTree Symbol) g h b | path h -> b
+                                                   , path g b -> h where
+  gsetFieldSum :: g x -> b -> h x
+
+instance
+  ( GSetFieldSum path g h b
+  ) => GSetFieldSum path (M1 D m g) (M1 D m h) b where
+  gsetFieldSum (M1 x) = M1 . gsetFieldSum @path x
+
+instance
+  ( GSetFieldSum path1 g1 h1 b
+  , GSetFieldSum path2 g2 h2 b
+  ) => GSetFieldSum ('PathTree path1 path2) (g1 :+: g2) (h1 :+: h2) b where
+  gsetFieldSum (L1 x) = L1 . gsetFieldSum @path1 x
+  gsetFieldSum (R1 y) = R1 . gsetFieldSum @path2 y
+  {-# INLINE gsetFieldSum #-}
+
+instance
+  ( path ~ GSetFieldPath con epath
+  , When (IsLeft epath) (HideReps g h)
+  , GSetFieldProd path g h b
+  ) => GSetFieldSum ('PathLeaf epath) (M1 C ('MetaCons con fix hs) g)
+                                      (M1 C ('MetaCons con fix hs) h) b where
+  gsetFieldSum (M1 x) = M1 . gsetFieldProd @path x
+
+type family GSetFieldPath (con :: Symbol) (e :: Either Symbol [Path]) :: [Path] where
+  GSetFieldPath _   ('Right path) = path
+  GSetFieldPath con ('Left name)  = TypeError
+    ('Text "Data constructor " ':<>: QuoteSymbol con ':<>:
+     'Text " doesn't have a field named " ':<>: QuoteSymbol name)
+
+class GSetFieldProd (path :: [Path]) g h b | path h -> b
+                                           , path g b -> h where
+  gsetFieldProd :: g x -> b -> h x
+
+-- fast path left
+instance {-# OVERLAPPING #-}
+  ( GSetFieldProd path g1 h1 b
+  ) => GSetFieldProd ('PathLeft : path) (g1 :*: g2) (h1 :*: g2) b where
+  gsetFieldProd (x :*: y) = (:*: y) . gsetFieldProd @path x
+
+-- slow path left
+instance
+  ( GSetFieldProd path g1 h1 b
+  , g2 ~ h2
+  ) => GSetFieldProd ('PathLeft : path) (g1 :*: g2) (h1 :*: h2) b where
+  gsetFieldProd (x :*: y) = (:*: y) . gsetFieldProd @path x
+
+-- fast path right
+instance {-# OVERLAPPING #-}
+  ( GSetFieldProd path g2 h2 b
+  ) => GSetFieldProd ('PathRight : path) (g1 :*: g2) (g1 :*: h2) b where
+  gsetFieldProd (x :*: y) = (x :*:) . gsetFieldProd @path y
+
+-- slow path right
+instance
+  ( GSetFieldProd path g2 h2 b
+  , g1 ~ h1
+  ) => GSetFieldProd ('PathRight : path) (g1 :*: g2) (h1 :*: h2) b where
+  gsetFieldProd (x :*: y) = (x :*:) . gsetFieldProd @path y
+
+instance
+  ( r ~ b
+  ) => GSetFieldProd '[] (M1 S m (Rec0 a)) (M1 S m (Rec0 b)) r where
+  gsetFieldProd _ = M1 . K1
+
+----------------------------------------
+-- Affine field
+
+class GAffineFieldImpl (repDefined :: Bool)
+                       (name :: Symbol) s t a b | name s -> a
+                                             {- These hold morally, but we can't prove it.
+                                                , name t -> b
+                                                , name s b -> t
+                                                , name t a -> s -} where
+
+  gafieldImpl :: AffineTraversal s t a b
+
+instance
+  ( Generic s
+  , Generic t
+  , path ~ GetFieldPaths s name (Rep s)
+  , HasField name s a -- require the field to be in scope
+  , Unless (AnyHasPath path)
+    (TypeError
+      ('Text "Type " ':<>: QuoteType s ':<>:
+       'Text " doesn't have a field named " ':<>: QuoteSymbol name))
+  , GAffineFieldSum path (Rep s) (Rep t) a b
+  ) => GAffineFieldImpl 'True name s t a b where
+  gafieldImpl = withAffineTraversal
+    (atraversalVL (\point f s -> to <$> gafieldSum @path point f (from s)))
+    (\match update -> atraversalVL $ \point f s ->
+        either point (fmap (update s) . f) (match s))
+  {-# INLINE gafieldImpl #-}
+
+----------------------------------------
+
+class GAffineFieldSum (path :: PathTree Symbol) g h a b where
+  gafieldSum :: AffineTraversalVL (g x) (h x) a b
+
+instance
+  ( GAffineFieldSum path g h a b
+  ) => GAffineFieldSum path (M1 D m g) (M1 D m h) a b where
+  gafieldSum point f (M1 x) = M1 <$> gafieldSum @path point f x
+
+instance
+  ( GAffineFieldSum path1 g1 h1 a b
+  , GAffineFieldSum path2 g2 h2 a b
+  ) => GAffineFieldSum ('PathTree path1 path2) (g1 :+: g2) (h1 :+: h2) a b where
+  gafieldSum point f (L1 x) = L1 <$> gafieldSum @path1 point f x
+  gafieldSum point f (R1 y) = R1 <$> gafieldSum @path2 point f y
+  {-# INLINE gafieldSum #-}
+
+instance
+  ( GAffineFieldMaybe epath g h a b
+  ) => GAffineFieldSum ('PathLeaf epath) (M1 C m g) (M1 C m h) a b where
+  gafieldSum point f (M1 x) = M1 <$> gafieldMaybe @epath point f x
+
+class GAffineFieldMaybe (epath :: Either Symbol [Path]) g h a b where
+  gafieldMaybe :: AffineTraversalVL (g x) (h x) a b
+
+instance
+  ( g ~ h
+  ) => GAffineFieldMaybe ('Left name) g h a b where
+  gafieldMaybe point _ g = point g
+
+instance
+  ( GFieldProd prodPath g h a b
+  ) => GAffineFieldMaybe ('Right prodPath) g h a b where
+  gafieldMaybe _ f g = gfieldProd @prodPath f g
+
+----------------------------------------
+
+class GFieldProd (path :: [Path]) g h a b | path g -> a
+                                          , path h -> b
+                                          , path g b -> h
+                                          , path h a -> g where
+  gfieldProd :: LensVL (g x) (h x) a b
+
+-- fast path left
+instance {-# OVERLAPPING #-}
+  ( GFieldProd path g1 h1 a b
+  ) => GFieldProd ('PathLeft : path) (g1 :*: g2) (h1 :*: g2) a b where
+  gfieldProd f (x :*: y) = (:*: y) <$> gfieldProd @path f x
+
+-- slow path left
+instance
+  ( GFieldProd path g1 h1 a b
+  , g2 ~ h2
+  ) => GFieldProd ('PathLeft : path) (g1 :*: g2) (h1 :*: h2) a b where
+  gfieldProd f (x :*: y) = (:*: y) <$> gfieldProd @path f x
+
+-- fast path right
+instance {-# OVERLAPPING #-}
+  ( GFieldProd path g2 h2 a b
+  ) => GFieldProd ('PathRight : path) (g1 :*: g2) (g1 :*: h2) a b where
+  gfieldProd f (x :*: y) = (x :*:) <$> gfieldProd @path f y
+
+-- slow path right
+instance
+  ( GFieldProd path g2 h2 a b
+  , g1 ~ h1
+  ) => GFieldProd ('PathRight : path) (g1 :*: g2) (h1 :*: h2) a b where
+  gfieldProd f (x :*: y) = (x :*:) <$> gfieldProd @path f y
+
+instance
+  ( r ~ a
+  , s ~ b
+  ) => GFieldProd '[] (M1 S m (Rec0 a)) (M1 S m (Rec0 b)) r s where
+  gfieldProd f (M1 (K1 x)) = M1 . K1 <$> f x
+
+----------------------------------------
+-- Position
+
+class GPositionImpl (repDefined :: Bool)
+                    (n :: Nat) s t a b | n s -> a
+                                    {- These hold morally, but we can't prove it.
+                                       , n t -> b
+                                       , n s b -> t
+                                       , n t a -> s -} where
+
+  gpositionImpl :: Lens s t a b
+
+instance
+  ( Generic s
+  , Generic t
+  , path ~ If (n <=? 0)
+              (TypeError ('Text "There is no 0th position"))
+              (GetPositionPaths s n (Rep s))
+  , When (n <=? 0) (HideReps (Rep s) (Rep t))
+  , GPositionSum path (Rep s) (Rep t) a b
+  ) => GPositionImpl 'True n s t a b where
+  gpositionImpl = withLens
+    (lensVL (\f s -> to <$> gpositionSum @path f (from s)))
+    (\get set -> lensVL $ \f s -> set s <$> f (get s))
+  {-# INLINE gpositionImpl #-}
+
+----------------------------------------
+
+class GPositionSum (path :: PathTree (Nat, Nat)) g h a b | path g -> a
+                                                         , path h -> b
+                                                         , path g b -> h
+                                                         , path h a -> g where
+  gpositionSum :: LensVL (g x) (h x) a b
+
+instance
+  ( GPositionSum path g h a b
+  ) => GPositionSum path (M1 D m g) (M1 D m h) a b where
+  gpositionSum f (M1 x) = M1 <$> gpositionSum @path f x
+
+instance
+  ( GPositionSum path1 g1 h1 a b
+  , GPositionSum path2 g2 h2 a b
+  ) => GPositionSum ('PathTree path1 path2) (g1 :+: g2) (h1 :+: h2) a b where
+  gpositionSum f (L1 x) = L1 <$> gpositionSum @path1 f x
+  gpositionSum f (R1 y) = R1 <$> gpositionSum @path2 f y
+  {-# INLINE gpositionSum #-}
+
+instance
+  ( path ~ GPositionPath con epath
+  , When (IsLeft epath) (HideReps g h)
+  , GFieldProd path g h a b
+  ) => GPositionSum ('PathLeaf epath) (M1 C ('MetaCons con fix hs) g)
+                                      (M1 C ('MetaCons con fix hs) h) a b where
+  gpositionSum f (M1 x) = M1 <$> gfieldProd @path f x
+
+type family GPositionPath con (e :: Either (Nat, Nat) [Path]) :: [Path] where
+  GPositionPath _   ('Right path)   = path
+  GPositionPath con ('Left '(n, k)) = TypeError
+    ('Text "Data constructor " ':<>: QuoteSymbol con ':<>:
+     'Text " has " ':<>: ShowFieldNumber k ':<>: 'Text ", " ':<>:
+     ToOrdinal n ':<>: 'Text " requested")
+
+type family ShowFieldNumber (k :: Nat) :: ErrorMessage where
+  ShowFieldNumber 0 = 'Text "no fields"
+  ShowFieldNumber 1 = 'Text "1 field"
+  ShowFieldNumber k = 'ShowType k ':<>: 'Text " fields"
+
+----------------------------------------
+-- Constructor
+
+class GConstructorImpl (repDefined :: Bool)
+                       (name :: Symbol) s t a b | name s -> a
+                                             {- These hold morally, but we can't prove it.
+                                                , name t -> b
+                                                , name s b -> t
+                                                , name t a -> s -} where
+
+  gconstructorImpl :: Prism s t a b
+
+instance
+  ( Generic s
+  , Generic t
+  , epath ~ GetNamePath name (Rep s) '[]
+  , path ~ FromRight
+    (TypeError
+      ('Text "Type " ':<>: QuoteType s ':<>:
+       'Text " doesn't have a constructor named " ':<>: QuoteSymbol name))
+    epath
+  , When (IsLeft epath) (HideReps (Rep s) (Rep t))
+  , GConstructorSum path (Rep s) (Rep t) a b
+  ) => GConstructorImpl 'True name s t a b where
+  gconstructorImpl = withPrism (generic % gconstructorSum @path) prism
+  {-# INLINE gconstructorImpl #-}
+
+----------------------------------------
+
+class GConstructorSum (path :: [Path]) g h a b | path g -> a
+                                               , path h -> b
+                                               , path g b -> h
+                                               , path h a -> g where
+  gconstructorSum :: Prism (g x) (h x) a b
+
+instance
+  ( GConstructorSum path g h a b
+  ) => GConstructorSum path (M1 D m g) (M1 D m h) a b where
+  gconstructorSum = _M1 % gconstructorSum @path
+
+-- fast path left
+instance {-# OVERLAPPING #-}
+  ( GConstructorSum path g1 h1 a b
+  ) => GConstructorSum ('PathLeft : path) (g1 :+: g2) (h1 :+: g2) a b where
+  gconstructorSum = _L1 % gconstructorSum @path
+
+-- slow path left
+instance
+  ( GConstructorSum path g1 h1 a b
+  , g2 ~ h2
+  ) => GConstructorSum ('PathLeft : path) (g1 :+: g2) (h1 :+: h2) a b where
+  gconstructorSum = _L1 % gconstructorSum @path
+
+-- fast path right
+instance {-# OVERLAPPING #-}
+  ( GConstructorSum path g2 h2 a b
+  ) => GConstructorSum ('PathRight : path) (g1 :+: g2) (g1 :+: h2) a b where
+  gconstructorSum = _R1 % gconstructorSum @path
+
+-- slow path right
+instance
+  ( GConstructorSum path g2 h2 a b
+  , g1 ~ h1
+  ) => GConstructorSum ('PathRight : path) (g1 :+: g2) (h1 :+: h2) a b where
+  gconstructorSum = _R1 % gconstructorSum @path
+
+instance
+  ( GConstructorTuple g h a b
+  ) => GConstructorSum '[] (M1 C m g) (M1 C m h) a b where
+  gconstructorSum = _M1 % gconstructorTuple
+
+class GConstructorTuple g h a b | g -> a
+                                , h -> b
+                                , g b -> h
+                                , h a -> g where
+  gconstructorTuple :: Prism (g x) (h x) a b
+
+-- Fon uncluttering types in below instances a bit.
+type F m a = M1 S m (Rec0 a)
+
+instance {-# OVERLAPPABLE #-}
+  ( Dysfunctional () () g h a b
+  , TypeError
+    ('Text "Generic based access supports constructors" ':$$:
+     'Text "containing up to 5 fields. Please generate" ':$$:
+     'Text "PrismS with Template Haskell if you need more.")
+  ) => GConstructorTuple g h a b where
+  gconstructorTuple = error "unreachable"
+
+instance
+  ( a ~ ()
+  , b ~ ()
+  ) => GConstructorTuple U1 U1 a b where
+  gconstructorTuple = castOptic _U1
+  {-# INLINE gconstructorTuple #-}
+
+instance
+  ( r ~ a
+  , s ~ b
+  ) => GConstructorTuple (F m a) (F m b) r s where
+  gconstructorTuple = castOptic coerced
+  {-# INLINE gconstructorTuple #-}
+
+instance
+  ( r ~ (a1, a2)
+  , s ~ (b1, b2)
+  ) => GConstructorTuple
+         (F m1 a1 :*: F m2 a2)
+         (F m1 b1 :*: F m2 b2) r s where
+  gconstructorTuple = castOptic $ iso
+    (\(M1 (K1 a1) :*: M1 (K1 a2)) -> (a1, a2))
+    (\(b1, b2) -> M1 (K1 b1) :*: M1 (K1 b2))
+  {-# INLINE gconstructorTuple #-}
+
+-- | Only for a derived balanced representation.
+instance
+  ( r ~ (a1, a2, a3)
+  , s ~ (b1, b2, b3)
+  ) => GConstructorTuple
+         (F m1 a1 :*: F m2 a2 :*: F m3 a3)
+         (F m1 b1 :*: F m2 b2 :*: F m3 b3) r s where
+  gconstructorTuple = castOptic $ iso
+    (\(M1 (K1 a1) :*: M1 (K1 a2) :*: M1 (K1 a3)) -> (a1, a2, a3))
+    (\(b1, b2, b3) -> M1 (K1 b1) :*: M1 (K1 b2) :*: M1 (K1 b3))
+  {-# INLINE gconstructorTuple #-}
+
+-- | Only for a derived balanced representation.
+instance
+  ( r ~ (a1, a2, a3, a4)
+  , s ~ (b1, b2, b3, b4)
+  ) => GConstructorTuple
+         ((F m1 a1 :*: F m2 a2) :*: (F m3 a3 :*: F m4 a4))
+         ((F m1 b1 :*: F m2 b2) :*: (F m3 b3 :*: F m4 b4)) r s where
+  gconstructorTuple = castOptic $ iso
+    (\((M1 (K1 a1) :*: M1 (K1 a2)) :*: (M1 (K1 a3) :*: M1 (K1 a4))) -> (a1, a2, a3, a4))
+    (\(b1, b2, b3, b4) -> (M1 (K1 b1) :*: M1 (K1 b2)) :*: (M1 (K1 b3) :*: M1 (K1 b4)))
+  {-# INLINE gconstructorTuple #-}
+
+-- | Only for a derived balanced representation.
+instance
+  ( r ~ (a1, a2, a3, a4, a5)
+  , s ~ (b1, b2, b3, b4, b5)
+  ) => GConstructorTuple
+         ((F m1 a1 :*: F m2 a2) :*: (F m3 a3 :*: F m4 a4 :*: F m5 a5))
+         ((F m1 b1 :*: F m2 b2) :*: (F m3 b3 :*: F m4 b4 :*: F m5 b5)) r s where
+  gconstructorTuple = castOptic $ iso
+    (\((M1 (K1 a1) :*: M1 (K1 a2)) :*: (M1 (K1 a3) :*: M1 (K1 a4) :*: M1 (K1 a5))) ->
+       (a1, a2, a3, a4, a5))
+    (\(b1, b2, b3, b4, b5) ->
+       (M1 (K1 b1) :*: M1 (K1 b2)) :*: (M1 (K1 b3) :*: M1 (K1 b4) :*: M1 (K1 b5)))
+  {-# INLINE gconstructorTuple #-}
+
+----------------------------------------
+-- Types
+
+class GPlateImpl g a where
+  gplateImpl :: TraversalVL' (g x) a
+
+instance GPlateImpl f a => GPlateImpl (M1 i c f) a where
+  gplateImpl f (M1 x) = M1 <$> gplateImpl f x
+
+instance (GPlateImpl f a, GPlateImpl g a) => GPlateImpl (f :+: g) a where
+  gplateImpl f (L1 x) = L1 <$> gplateImpl f x
+  gplateImpl f (R1 x) = R1 <$> gplateImpl f x
+
+instance (GPlateImpl f a, GPlateImpl g a) => GPlateImpl (f :*: g) a where
+  gplateImpl f (x :*: y) = (:*:) <$> gplateImpl f x <*> gplateImpl f y
+  {-# INLINE gplateImpl #-}
+
+-- | Matching type.
+instance {-# OVERLAPPING #-} GPlateImpl (K1 i a) a where
+  gplateImpl f (K1 a) = K1 <$> f a
+
+-- | Recurse into the inner type if it has a 'Generic' instance.
+instance GPlateInner (Defined (Rep b)) b a => GPlateImpl (K1 i b) a where
+  gplateImpl f (K1 b) = K1 <$> gplateInner @(Defined (Rep b)) f b
+
+instance GPlateImpl U1 a where
+  gplateImpl _ = pure
+
+instance GPlateImpl V1 a where
+  gplateImpl _ = \case {}
+
+instance GPlateImpl (URec b) a where
+  gplateImpl _ = pure
+
+class GPlateInner (repDefined :: Bool) s a where
+  gplateInner :: TraversalVL' s a
+
+instance (Generic s, GPlateImpl (Rep s) a) => GPlateInner 'True s a where
+  gplateInner f = fmap to . gplateImpl f . from
+
+instance {-# INCOHERENT #-} GPlateInner repNotDefined s a where
+  gplateInner _ = pure
+
+-- $setup
+-- >>> import Optics.Core
diff --git a/src/Optics/Internal/Generic/TypeLevel.hs b/src/Optics/Internal/Generic/TypeLevel.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Internal/Generic/TypeLevel.hs
@@ -0,0 +1,131 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+-- | This module is intended for internal use only, and may change without
+-- warning in subsequent releases.
+module Optics.Internal.Generic.TypeLevel
+  ( -- * Pathing
+    PathTree(..)
+  , Path(..)
+  -- ** Names
+  , GetFieldPaths
+  , GetNamePath
+  -- ** Positions
+  , GetPositionPaths
+  , GetPositionPath
+  -- * Misc
+  , HideReps
+  , AnyHasPath
+  , NoGenericError
+  ) where
+
+import Data.Kind
+import Data.Type.Bool
+import Data.Type.Equality
+import GHC.Generics
+import GHC.TypeLits
+
+import Optics.Internal.Optic.TypeLevel
+
+-- | A map that allows reaching a specific field in a generic representation of
+-- a data type. Computed up front by generic optics for early error reporting
+-- and efficient data traversal.
+data PathTree e
+  = PathTree (PathTree e) (PathTree e)
+  | PathLeaf (Either e [Path])
+
+data Path = PathLeft | PathRight
+
+----------------------------------------
+-- Paths to a field
+
+-- | Compute paths to a field with a specific name.
+type family GetFieldPaths s (name :: Symbol) g :: PathTree Symbol where
+  GetFieldPaths s name (M1 D _ g)  = GetFieldPaths s name g
+  GetFieldPaths s name (g1 :+: g2) = 'PathTree (GetFieldPaths s name g1)
+                                               (GetFieldPaths s name g2)
+  GetFieldPaths s name (M1 C _ g)  = 'PathLeaf (GetNamePath name g '[])
+
+  GetFieldPaths s name V1 = TypeError ('Text "Type " ':<>: QuoteType s ':<>:
+                                       'Text " has no data constructors")
+
+-- | Compute path to a constructor in a sum or a field in a product with a
+-- specific name.
+type family GetNamePath (name :: Symbol) g (acc :: [Path]) :: Either Symbol [Path] where
+  GetNamePath name (M1 D _ g) acc = GetNamePath name g acc
+
+  -- Find path to a constructor in a sum type.
+  GetNamePath name (M1 C ('MetaCons name _ _) _) acc = 'Right (Reverse acc '[])
+  GetNamePath name (g1 :+: g2) acc = FirstRight (GetNamePath name g1 ('PathLeft  : acc))
+                                                (GetNamePath name g2 ('PathRight : acc))
+
+  -- Find path to a field in a product type.
+  GetNamePath name (M1 S ('MetaSel ('Just name) _ _ _) _) acc = 'Right (Reverse acc '[])
+  GetNamePath name (g1 :*: g2) acc = FirstRight (GetNamePath name g1 ('PathLeft  : acc))
+                                                (GetNamePath name g2 ('PathRight : acc))
+
+  GetNamePath name _ _ = 'Left name
+
+----------------------------------------
+-- Paths to a position
+
+-- | Compute paths to a field at a specific position.
+type family GetPositionPaths s (pos :: Nat) g :: PathTree (Nat, Nat) where
+  GetPositionPaths s pos (M1 D _ g)  = GetPositionPaths s pos g
+  GetPositionPaths s pos (g1 :+: g2) = 'PathTree (GetPositionPaths s pos g1)
+                                                 (GetPositionPaths s pos g2)
+  GetPositionPaths s pos (M1 C _ g)  = 'PathLeaf (GetPositionPath pos g 0 '[])
+
+  GetPositionPaths s pos V1 = TypeError ('Text "Type " ':<>: QuoteType s ':<>:
+                                         'Text " has no data constructors")
+
+-- | Compute path to a constructor in a sum or a field in a product at a
+-- specific position.
+type family GetPositionPath (pos :: Nat) g (k :: Nat) (acc :: [Path])
+  :: Either (Nat, Nat) [Path] where
+  GetPositionPath pos (M1 D _ g) k acc = GetPositionPath pos g k acc
+
+  -- Find field at a position in a sum type.
+  GetPositionPath pos (M1 C _ _) k acc =
+    If (pos == k + 1) ('Right (Reverse acc '[])) ('Left '(pos, k + 1))
+  GetPositionPath pos (g1 :+: g2) k acc =
+    ContinueWhenLeft (GetPositionPath pos g1 k ('PathLeft : acc)) g2 acc
+
+  -- Find field at a position in a product type.
+  GetPositionPath pos (M1 S _ _) k acc =
+    If (pos == k + 1) ('Right (Reverse acc '[])) ('Left '(pos, k + 1))
+  GetPositionPath pos (g1 :*: g2) k acc =
+    ContinueWhenLeft (GetPositionPath pos g1 k ('PathLeft : acc)) g2 acc
+
+  -- The second element is the number of fields in the data constructor.
+  GetPositionPath pos _ k _ = 'Left '(pos, k)
+
+-- | If the left branch had the position we're looking for, return it. Otherwise
+-- continue with the right branch.
+type family ContinueWhenLeft (r :: Either (Nat, Nat) [Path]) g acc
+  :: Either (Nat, Nat) [Path] where
+  ContinueWhenLeft ('Right path) _ _ = 'Right path
+  ContinueWhenLeft ('Left '(pos, k)) g acc = GetPositionPath pos g k ('PathRight : acc)
+
+----------------------------------------
+-- Misc
+
+data Void1 a
+-- | Generate bogus equality constraints that attempt to unify generic
+-- representations with this type in case there is an error such as missing
+-- field, constructor etc. so these huge types don't leak into error messages.
+type family HideReps (g :: Type -> Type) (h :: Type -> Type) :: Constraint where
+  HideReps g h = (g ~ Void1, h ~ Void1)
+
+-- | Check if any leaf in the tree has a '[Path]'.
+type family AnyHasPath (path :: PathTree e) :: Bool where
+  AnyHasPath ('PathTree path1 path2) = AnyHasPath path1 || AnyHasPath path2
+  AnyHasPath ('PathLeaf ('Right _))  = 'True
+  AnyHasPath ('PathLeaf ('Left _ ))  = 'False
+
+type family NoGenericError t where
+  NoGenericError t = TypeError
+    ('Text "Type " ':<>: QuoteType t ':<>:
+     'Text " doesn't have a Generic instance")
diff --git a/src/Optics/Internal/Indexed.hs b/src/Optics/Internal/Indexed.hs
--- a/src/Optics/Internal/Indexed.hs
+++ b/src/Optics/Internal/Indexed.hs
@@ -110,15 +110,12 @@
 instance Functor f => Functor (Indexing f) where
   fmap f (Indexing m) = Indexing $ \i -> case m i of
     IntT j x -> IntT j (fmap f x)
-  {-# INLINE fmap #-}
 
 instance Applicative f => Applicative (Indexing f) where
   pure x = Indexing $ \i -> IntT i (pure x)
-  {-# INLINE pure #-}
   Indexing mf <*> Indexing ma = Indexing $ \i -> case mf i of
     IntT j ff -> case ma j of
        IntT k fa -> IntT k (ff <*> fa)
-  {-# INLINE (<*>) #-}
 
 -- | Index a traversal by position of visited elements.
 indexing
@@ -126,7 +123,6 @@
   -> ((Int -> a -> f b) -> s -> f t)
 indexing l iafb s =
   unIntT $ runIndexing (l (\a -> Indexing (\i -> IntT (i + 1) (iafb i a))) s) 0
-{-# INLINE indexing #-}
 
 ----------------------------------------
 
@@ -142,4 +138,3 @@
   -> Optic k is   s t a b
   -> Optic k is   s t a b
 conjoined (Optic f) (Optic g) = Optic (conjoined__ f g)
-{-# INLINE conjoined #-}
diff --git a/src/Optics/Internal/Indexed/Classes.hs b/src/Optics/Internal/Indexed/Classes.hs
--- a/src/Optics/Internal/Indexed/Classes.hs
+++ b/src/Optics/Internal/Indexed/Classes.hs
@@ -6,509 +6,12 @@
 --
 -- This module is intended for internal use only, and may change without warning
 -- in subsequent releases.
-module Optics.Internal.Indexed.Classes where
-
-import Control.Applicative
-import Control.Applicative.Backwards
-import Control.Monad.Trans.Identity
-import Control.Monad.Trans.Reader
-import Data.Functor.Constant
-import Data.Functor.Compose
-import Data.Functor.Identity
-import Data.Functor.Product
-import Data.Functor.Reverse
-import Data.Functor.Sum
-import Data.Ix
-import Data.List.NonEmpty
-import Data.Monoid hiding (Product, Sum)
-import Data.Proxy
-import Data.Tree
-import Data.Void
-import GHC.Generics
-import qualified Data.Array as Array
-import qualified Data.IntMap as IntMap
-import qualified Data.Map as Map
-import qualified Data.Sequence as Seq
-
-import Optics.Internal.Utils
-
--- | Class for 'Functor's that have an additional read-only index available.
-class Functor f => FunctorWithIndex i f | f -> i where
-  imap :: (i -> a -> b) -> f a -> f b
-  default imap
-    :: TraversableWithIndex i f => (i -> a -> b) -> f a -> f b
-  imap f = runIdentity #. itraverse (\i a -> Identity (f i a))
-  {-# INLINE imap #-}
-
--- | Class for 'Foldable's that have an additional read-only index available.
-class (FunctorWithIndex i f, Foldable f
-      ) => FoldableWithIndex i f | f -> i where
-  ifoldMap :: Monoid m => (i -> a -> m) -> f a -> m
-  default ifoldMap
-    :: (TraversableWithIndex i f, Monoid m) => (i -> a -> m) -> f a -> m
-  ifoldMap f = getConst #. itraverse (\i a -> Const (f i a))
-  {-# INLINE ifoldMap #-}
-
-  ifoldr :: (i -> a -> b -> b) -> b -> f a -> b
-  ifoldr iabb b0 = (\e -> appEndo e b0) . ifoldMap (\i -> Endo #. iabb i)
-  {-# INLINE ifoldr #-}
-
-  ifoldl' :: (i -> b -> a -> b) -> b -> f a -> b
-  ifoldl' ibab b0 s = ifoldr (\i a bb b -> bb $! ibab i b a) id s b0
-  {-# INLINE ifoldl' #-}
-
--- | Traverse 'FoldableWithIndex' ignoring the results.
-itraverse_ :: (FoldableWithIndex i t, Applicative f) => (i -> a -> f b) -> t a -> f ()
-itraverse_ f = runTraversed . ifoldMap (\i -> Traversed #. f i)
-{-# INLINE itraverse_ #-}
-
--- | Flipped 'itraverse_'.
-ifor_ :: (FoldableWithIndex i t, Applicative f) => t a -> (i -> a -> f b) -> f ()
-ifor_ = flip itraverse_
-{-# INLINE ifor_ #-}
-
--- | List of elements of a structure with an index, from left to right.
-itoList :: FoldableWithIndex i f => f a -> [(i, a)]
-itoList = ifoldr (\i c -> ((i, c) :)) []
-{-# INLINE itoList #-}
-
--- | Class for 'Traversable's that have an additional read-only index available.
-class (FoldableWithIndex i t, Traversable t
-      ) => TraversableWithIndex i t | t -> i where
-  itraverse :: Applicative f => (i -> a -> f b) -> t a -> f (t b)
-
--- | Flipped 'itraverse'
-ifor :: (TraversableWithIndex i t, Applicative f) => t a -> (i -> a -> f b) -> f (t b)
-ifor = flip itraverse
-{-# INLINE ifor #-}
-
-----------------------------------------
--- Instances
-
--- Identity
-
-instance FunctorWithIndex () Identity where
-  imap f (Identity a) = Identity (f () a)
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex () Identity where
-  ifoldMap f (Identity a) = f () a
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex () Identity where
-  itraverse f (Identity a) = Identity <$> f () a
-  {-# INLINE itraverse #-}
-
--- Const
-
--- | @since 0.3
-instance FunctorWithIndex Void (Const e) where
-  imap _ (Const a) = Const a
-  {-# INLINE imap #-}
-
--- | @since 0.3
-instance FoldableWithIndex Void (Const e) where
-  ifoldMap _ _ = mempty
-  {-# INLINE ifoldMap #-}
-
--- | @since 0.3
-instance TraversableWithIndex Void (Const e) where
-  itraverse _ (Const a) = pure (Const a)
-  {-# INLINE itraverse #-}
-
--- Constant
-
--- | @since 0.3
-instance FunctorWithIndex Void (Constant e) where
-  imap _ (Constant a) = Constant a
-  {-# INLINE imap #-}
-
--- | @since 0.3
-instance FoldableWithIndex Void (Constant e) where
-  ifoldMap _ _ = mempty
-  {-# INLINE ifoldMap #-}
-
--- | @since 0.3
-instance TraversableWithIndex Void (Constant e) where
-  itraverse _ (Constant a) = pure (Constant a)
-  {-# INLINE itraverse #-}
-
--- (,) k
-
-instance FunctorWithIndex k ((,) k) where
-  imap f (k, a) = (k, f k a)
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex k ((,) k) where
-  ifoldMap = uncurry'
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex k ((,) k) where
-  itraverse f (k, a) = (,) k <$> f k a
-  {-# INLINE itraverse #-}
-
--- (->) r
-
-instance FunctorWithIndex r ((->) r) where
-  imap f g x = f x (g x)
-  {-# INLINE imap #-}
-
--- []
-
-instance FunctorWithIndex Int []
-instance FoldableWithIndex Int []
-instance TraversableWithIndex Int [] where
-  -- Faster than @indexing traverse@, also best for folds and setters.
-  itraverse f = traverse (uncurry' f) . Prelude.zip [0..]
-  {-# INLINE itraverse #-}
-
--- ZipList
-
-instance FunctorWithIndex Int ZipList
-instance FoldableWithIndex Int ZipList
-instance TraversableWithIndex Int ZipList where
-  itraverse f (ZipList xs) = ZipList <$> itraverse f xs
-  {-# INLINE itraverse #-}
-
--- NonEmpty
-
-instance FunctorWithIndex Int NonEmpty
-instance FoldableWithIndex Int NonEmpty
-instance TraversableWithIndex Int NonEmpty where
-  itraverse f ~(a :| as) =
-    (:|) <$> f 0 a <*> traverse (uncurry' f) (Prelude.zip [1..] as)
-  {-# INLINE itraverse #-}
-
--- Maybe
-
-instance FunctorWithIndex () Maybe where
-  imap f = fmap (f ())
-  {-# INLINE imap #-}
-instance FoldableWithIndex () Maybe where
-  ifoldMap f = foldMap (f ())
-  {-# INLINE ifoldMap #-}
-instance TraversableWithIndex () Maybe where
-  itraverse f = traverse (f ())
-  {-# INLINE itraverse #-}
-
--- Seq
-
--- | The position in the 'Seq.Seq' is available as the index.
-instance FunctorWithIndex Int Seq.Seq where
-  imap = Seq.mapWithIndex
-  {-# INLINE imap #-}
-instance FoldableWithIndex Int Seq.Seq where
-#if MIN_VERSION_containers(0,5,8)
-  ifoldMap = Seq.foldMapWithIndex
-#else
-  ifoldMap f = ifoldr (\i -> mappend . f i) mempty
-#endif
-  {-# INLINE ifoldMap #-}
-
-  ifoldr = Seq.foldrWithIndex
-  {-# INLINE ifoldr #-}
-
-instance TraversableWithIndex Int Seq.Seq where
-#if MIN_VERSION_containers(0,6,0)
-  itraverse = Seq.traverseWithIndex
-#else
-  -- Much faster than Seq.traverseWithIndex for containers < 0.6.0, see
-  -- https://github.com/haskell/containers/issues/603.
-  itraverse f = sequenceA . Seq.mapWithIndex f
-#endif
-  {-# INLINE itraverse #-}
-
--- IntMap
-
-instance FunctorWithIndex Int IntMap.IntMap where
-  imap = IntMap.mapWithKey
-  {-# INLINE imap #-}
-instance FoldableWithIndex Int IntMap.IntMap where
-  ifoldMap = IntMap.foldMapWithKey
-  ifoldr   = IntMap.foldrWithKey
-  ifoldl'  = IntMap.foldlWithKey' . flip
-  {-# INLINE ifoldMap #-}
-  {-# INLINE ifoldr #-}
-  {-# INLINE ifoldl' #-}
-instance TraversableWithIndex Int IntMap.IntMap where
-  itraverse = IntMap.traverseWithKey
-  {-# INLINE itraverse #-}
-
--- Map
-
-instance FunctorWithIndex k (Map.Map k) where
-  imap = Map.mapWithKey
-  {-# INLINE imap #-}
-instance FoldableWithIndex k (Map.Map k) where
-  ifoldMap = Map.foldMapWithKey
-  ifoldr   = Map.foldrWithKey
-  ifoldl'  = Map.foldlWithKey' . flip
-  {-# INLINE ifoldMap #-}
-  {-# INLINE ifoldr #-}
-  {-# INLINE ifoldl' #-}
-instance TraversableWithIndex k (Map.Map k) where
-  itraverse = Map.traverseWithKey
-  {-# INLINE itraverse #-}
-
--- Array
-
-instance Ix i => FunctorWithIndex i (Array.Array i) where
-  imap f arr = Array.listArray (Array.bounds arr)
-    . fmap (uncurry' f) $ Array.assocs arr
-  {-# INLINE imap #-}
-
-instance Ix i => FoldableWithIndex i (Array.Array i) where
-  ifoldMap f = foldMap (uncurry' f) . Array.assocs
-  {-# INLINE ifoldMap #-}
-
-instance Ix i => TraversableWithIndex i (Array.Array i) where
-  itraverse f arr = Array.listArray (Array.bounds arr)
-    <$> traverse (uncurry' f) (Array.assocs arr)
-  {-# INLINE itraverse #-}
-
--- Compose
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (i, j) (Compose f g) where
-  imap f (Compose fg) = Compose $ imap (\k -> imap (f . (,) k)) fg
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (i, j) (Compose f g) where
-  ifoldMap f (Compose fg) = ifoldMap (\k -> ifoldMap (f . (,) k)) fg
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (i, j) (Compose f g) where
-  itraverse f (Compose fg) =
-    Compose <$> itraverse (\k -> itraverse (f . (,) k)) fg
-  {-# INLINE itraverse #-}
-
--- Sum
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (Either i j) (Sum f g) where
-  imap q (InL fa) = InL (imap (q . Left)  fa)
-  imap q (InR ga) = InR (imap (q . Right) ga)
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (Either i j) (Sum f g) where
-  ifoldMap q (InL fa) = ifoldMap (q . Left)  fa
-  ifoldMap q (InR ga) = ifoldMap (q . Right) ga
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (Either i j) (Sum f g) where
-  itraverse q (InL fa) = InL <$> itraverse (q . Left)  fa
-  itraverse q (InR ga) = InR <$> itraverse (q . Right) ga
-  {-# INLINE itraverse #-}
-
--- Product
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (Either i j) (Product f g) where
-  imap f (Pair a b) = Pair (imap (f . Left) a) (imap (f . Right) b)
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (Either i j) (Product f g) where
-  ifoldMap f (Pair a b) =
-    ifoldMap (f . Left) a `mappend` ifoldMap (f . Right) b
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (Either i j) (Product f g) where
-  itraverse f (Pair a b) =
-    Pair <$> itraverse (f . Left) a <*> itraverse (f . Right) b
-  {-# INLINE itraverse #-}
-
--- Tree
-
-instance FunctorWithIndex [Int] Tree where
-  imap f (Node a as) = Node (f [] a) $ imap (\i -> imap (f . (:) i)) as
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex [Int] Tree where
-  ifoldMap f (Node a as) =
-    f [] a `mappend` ifoldMap (\i -> ifoldMap (f . (:) i)) as
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex [Int] Tree where
-  itraverse f (Node a as) =
-    Node <$> f [] a <*> itraverse (\i -> itraverse (f . (:) i)) as
-  {-# INLINE itraverse #-}
-
--- Proxy
-
-instance FunctorWithIndex Void Proxy where
-  imap _ Proxy = Proxy
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex Void Proxy where
-  ifoldMap _ _ = mempty
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex Void Proxy where
-  itraverse _ _ = pure Proxy
-  {-# INLINE itraverse #-}
-
--- Backwards
-
-instance FunctorWithIndex i f => FunctorWithIndex i (Backwards f) where
-  imap f  = Backwards . imap f . forwards
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex i f => FoldableWithIndex i (Backwards f) where
-  ifoldMap f = ifoldMap f . forwards
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex i f => TraversableWithIndex i (Backwards f) where
-  itraverse f = fmap Backwards . itraverse f . forwards
-  {-# INLINE itraverse #-}
-
--- Reverse
-
-instance FunctorWithIndex i f => FunctorWithIndex i (Reverse f) where
-  imap f = Reverse . imap f . getReverse
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex i f => FoldableWithIndex i (Reverse f) where
-  ifoldMap f = getDual . ifoldMap (\i -> Dual #. f i) . getReverse
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex i f => TraversableWithIndex i (Reverse f) where
-  itraverse f =
-    fmap Reverse . forwards . itraverse (\i -> Backwards . f i) . getReverse
-  {-# INLINE itraverse #-}
-
--- IdentityT
-
-instance FunctorWithIndex i m => FunctorWithIndex i (IdentityT m) where
-  imap f (IdentityT m) = IdentityT $ imap f m
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex i m => FoldableWithIndex i (IdentityT m) where
-  ifoldMap f (IdentityT m) = ifoldMap f m
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex i m => TraversableWithIndex i (IdentityT m) where
-  itraverse f (IdentityT m) = IdentityT <$> itraverse f m
-  {-# INLINE itraverse #-}
-
--- ReaderT
-
-instance FunctorWithIndex i m => FunctorWithIndex (e, i) (ReaderT e m) where
-  imap f (ReaderT m) = ReaderT $ \k -> imap (f . (,) k) (m k)
-  {-# INLINE imap #-}
-
--- Generics
-
-instance FunctorWithIndex Void V1 where
-  imap _ v = v `seq` undefined
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex Void V1 where
-  ifoldMap _ v = v `seq` undefined
-
-instance TraversableWithIndex Void V1 where
-  itraverse _ v = v `seq` undefined
-
-instance FunctorWithIndex Void U1 where
-  imap _ U1 = U1
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex Void U1 where
-  ifoldMap _ _ = mempty
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex Void U1 where
-  itraverse _ U1 = pure U1
-  {-# INLINE itraverse #-}
-
-instance FunctorWithIndex () Par1 where
-  imap f = fmap (f ())
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex () Par1 where
-  ifoldMap f (Par1 a) = f () a
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex () Par1 where
-  itraverse f (Par1 a) = Par1 <$> f () a
-  {-# INLINE itraverse #-}
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (i, j) (f :.: g) where
-  imap q (Comp1 fga) = Comp1 (imap (\k -> imap (q . (,) k)) fga)
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (i, j) (f :.: g) where
-  ifoldMap q (Comp1 fga) = ifoldMap (\k -> ifoldMap (q . (,) k)) fga
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (i, j) (f :.: g) where
-  itraverse q (Comp1 fga) =
-    Comp1 <$> itraverse (\k -> itraverse (q . (,) k)) fga
-  {-# INLINE itraverse #-}
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (Either i j) (f :*: g) where
-  imap q (fa :*: ga) = imap (q . Left) fa :*: imap (q . Right) ga
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (Either i j) (f :*: g) where
-  ifoldMap q (fa :*: ga) =
-    ifoldMap (q . Left) fa `mappend` ifoldMap (q . Right) ga
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (Either i j) (f :*: g) where
-  itraverse q (fa :*: ga) =
-    (:*:) <$> itraverse (q . Left) fa <*> itraverse (q . Right) ga
-  {-# INLINE itraverse #-}
-
-instance (FunctorWithIndex i f, FunctorWithIndex j g
-         ) => FunctorWithIndex (Either i j) (f :+: g) where
-  imap q (L1 fa) = L1 (imap (q . Left) fa)
-  imap q (R1 ga) = R1 (imap (q . Right) ga)
-  {-# INLINE imap #-}
-
-instance (FoldableWithIndex i f, FoldableWithIndex j g
-         ) => FoldableWithIndex (Either i j) (f :+: g) where
-  ifoldMap q (L1 fa) = ifoldMap (q . Left) fa
-  ifoldMap q (R1 ga) = ifoldMap (q . Right) ga
-  {-# INLINE ifoldMap #-}
-
-instance (TraversableWithIndex i f, TraversableWithIndex j g
-         ) => TraversableWithIndex (Either i j) (f :+: g) where
-  itraverse q (L1 fa) = L1 <$> itraverse (q . Left) fa
-  itraverse q (R1 ga) = R1 <$> itraverse (q . Right) ga
-  {-# INLINE itraverse #-}
-
-instance FunctorWithIndex i f => FunctorWithIndex i (Rec1 f) where
-  imap q (Rec1 f) = Rec1 (imap q f)
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex i f => FoldableWithIndex i (Rec1 f) where
-  ifoldMap q (Rec1 f) = ifoldMap q f
-  {-# INLINE ifoldMap #-}
-
-instance TraversableWithIndex i f => TraversableWithIndex i (Rec1 f) where
-  itraverse q (Rec1 f) = Rec1 <$> itraverse q f
-  {-# INLINE itraverse #-}
-
-instance FunctorWithIndex Void (K1 i c) where
-  imap _ (K1 c) = K1 c
-  {-# INLINE imap #-}
-
-instance FoldableWithIndex Void (K1 i c) where
-  ifoldMap _ _ = mempty
-  {-# INLINE ifoldMap #-}
+module Optics.Internal.Indexed.Classes (
+   module Data.Functor.WithIndex,
+   module Data.Foldable.WithIndex,
+   module Data.Traversable.WithIndex,
+) where
 
-instance TraversableWithIndex Void (K1 i c) where
-  itraverse _ (K1 a) = pure (K1 a)
-  {-# INLINE itraverse #-}
+import Data.Functor.WithIndex
+import Data.Foldable.WithIndex
+import Data.Traversable.WithIndex
diff --git a/src/Optics/Internal/Magic.hs b/src/Optics/Internal/Magic.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Internal/Magic.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+-- | This module is intended for internal use only, and may change without
+-- warning in subsequent releases.
+module Optics.Internal.Magic where
+
+-- | How about a magic trick? I'm gonna make the coverage condition disappear.
+class Dysfunctional field k s t a b | field s -> k t a b
+                                    , field t -> k s a b
+
+-- | Show something useful when type inference goes into a loop and stops with
+-- "reduction stack overflow" message (sometimes happens when trying to infer
+-- types of local bindings when monomorphism restriction is enabled).
+instance
+  ( TypeInferenceLoop
+    "Type inference for the local binding failed. Write the type"
+    "signature yourself or disable monomorphism restriction with"
+    "NoMonomorphismRestriction LANGUAGE pragma so GHC infers it."
+    field k s t a b
+  ) => Dysfunctional field k s t a b
+
+class TypeInferenceLoop msg1 msg2 msg3 field k s t a b | field s -> k t a b
+                                                       , field t -> k s a b
+
+-- | Including the instance head in the context lifts the coverage condition for
+-- all type variables in the instance. A dirty trick until we have
+-- https://github.com/ghc-proposals/ghc-proposals/pull/374 and can do it
+-- properly.
+instance
+  ( TypeInferenceLoop msg1 msg2 msg3 field k s t a b
+  ) => TypeInferenceLoop msg1 msg2 msg3 field k s t a b
diff --git a/src/Optics/Internal/Optic.hs b/src/Optics/Internal/Optic.hs
--- a/src/Optics/Internal/Optic.hs
+++ b/src/Optics/Internal/Optic.hs
@@ -1,9 +1,5 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeInType #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_HADDOCK not-home #-}
 
 -- | Core optic types and subtyping machinery.
@@ -27,10 +23,6 @@
   , (%)
   , (%%)
   , (%&)
-  -- * Labels
-  , LabelOptic(..)
-  , LabelOptic'
-  , GeneralLabelOptic(..)
   -- * Re-exports
   , module Optics.Internal.Optic.Subtyping
   , module Optics.Internal.Optic.Types
@@ -38,12 +30,6 @@
   ) where
 
 import Data.Function ((&))
-import Data.Kind (Type)
-import Data.Proxy (Proxy (..))
-import Data.Type.Equality
-import GHC.Generics (Rep)
-import GHC.OverloadedLabels
-import GHC.TypeLits
 
 import Data.Profunctor.Indexed
 
@@ -51,9 +37,6 @@
 import Optics.Internal.Optic.TypeLevel
 import Optics.Internal.Optic.Types
 
--- to make %% simpler
-import Unsafe.Coerce (unsafeCoerce)
-
 -- | Wrapper newtype for the whole family of optics.
 --
 -- The first parameter @k@ identifies the particular optic kind (e.g. 'A_Lens'
@@ -123,7 +106,6 @@
       .  Optic_ srcKind  p i (Curry is i) s t a b
       -> Optic_ destKind p i (Curry is i) s t a b
     cast x = implies @srcKind @destKind @p x
-{-# INLINE castOptic #-}
 
 -- | Compose two optics of compatible flavours.
 --
@@ -131,34 +113,37 @@
 -- indexed, the composition preserves all the indices.
 --
 infixl 9 %
-(%) :: (Is k m, Is l m, m ~ Join k l, ks ~ Append is js)
+(%) :: forall k l m is js ks s t u v a b. (JoinKinds k l m, AppendIndices is js ks)
     => Optic k is s t u v
     -> Optic l js u v a b
     -> Optic m ks s t a b
-o % o' = castOptic o %% castOptic o'
-{-# INLINE (%) #-}
+Optic k % Optic l = Optic m
+  where
+    km :: forall p i. Profunctor p => Optic_ m p i (Curry is i) s t u v
+    km = joinKinds @k @l @m @p k
 
+    lm :: forall p i. Profunctor p => Optic_ m p i (Curry js i) u v a b
+    lm = joinKinds @k @l @m @p l
+
+    m :: forall p i. (Profunctor p, Constraints m p)
+      => Optic__ p i (Curry ks i) s t a b
+    m | IxEq <- appendIndices @is @js @ks @i = km . lm
+
 -- | Compose two optics of the same flavour.
 --
 -- Normally you can simply use ('%') instead, but this may be useful to help
 -- type inference if the type of one of the optics is otherwise
 -- under-constrained.
 infixl 9 %%
-(%%) :: forall k is js ks s t u v a b. ks ~ Append is js
+(%%) :: forall k is js ks s t u v a b. AppendIndices is js ks
      => Optic k is s t u v
      -> Optic k js u v a b
      -> Optic k ks s t a b
 Optic o %% Optic o' = Optic oo
   where
-    -- unsafeCoerce to the rescue, for a proof see below.
-    oo :: forall p i. (Profunctor p, Constraints k p) => Optic__ p i (Curry ks i) s t a b
-    oo = (unsafeCoerce
-           :: Optic__ p i (Curry is (Curry js i)) s t a b
-           -> Optic__ p i (Curry ks i           ) s t a b)
-      ( (o  :: Optic__ p (Curry js i) (Curry is (Curry js i)) s t u v)
-      . (o' :: Optic__ p i            (Curry js i)            u v a b)
-      )
-{-# INLINE (%%) #-}
+    oo :: forall p i. (Profunctor p, Constraints k p)
+       => Optic__ p i (Curry ks i) s t a b
+    oo | IxEq <- appendIndices @is @js @ks @i = o . o'
 
 -- | Flipped function application, specialised to optics and binding tightly.
 --
@@ -172,109 +157,6 @@
      -> (Optic k is s t a b -> Optic l js s' t' a' b')
      -> Optic l js s' t' a' b'
 (%&) = (&)
-{-# INLINE (%&) #-}
-
-
--- |
---
--- 'AppendProof' is a very simple class which provides a witness
---
--- @
--- foldr f (foldr f init xs) ys = foldr f init (ys ++ xs)
---    where f = (->)
--- @
---
--- It shows that usage of 'unsafeCoerce' in '(%%)' is, in fact, safe.
---
-class Append xs ys ~ zs => AppendProof (xs :: [Type]) (ys :: [Type]) (zs :: [Type])
-  | xs ys -> zs, zs xs -> ys {- , zs ys -> xs -} where
-  appendProof :: Proxy i -> Curry xs (Curry ys i) :~: Curry zs i
-
-instance ys ~ zs => AppendProof '[] ys zs where
-  appendProof _ = Refl
-
-instance
-  (Append (x : xs) ys ~ (x : zs), AppendProof xs ys zs
-  ) => AppendProof (x ': xs) ys (x ': zs) where
-  appendProof
-    :: forall i. Proxy i
-    -> Curry (x ': xs) (Curry ys i) :~: Curry (x ': zs) i
-  appendProof i = case appendProof @xs @ys @zs i of
-    Refl -> Refl
-
-----------------------------------------
--- Labels
-
--- | Support for overloaded labels as optics. An overloaded label @#foo@ can be
--- used as an optic if there is an instance of @'LabelOptic' "foo" k s t a b@.
-class LabelOptic (name :: Symbol) k s t a b | name s -> k a
-                                            , name t -> k b
-                                            , name s b -> t
-                                            , name t a -> s where
-  -- | Used to interpret overloaded label syntax.  An overloaded label @#foo@
-  -- corresponds to @'labelOptic' \@"foo"@.
-  labelOptic :: Optic k NoIx s t a b
-
--- | Type synonym for a type-preserving optic as overloaded label.
-type LabelOptic' name k s a = LabelOptic name k s s a a
-
--- | Implements fallback behaviour in case there is no explicit 'LabelOptic'
--- instance. This has a catch-all incoherent instance that merely yields an
--- error message.  However, a downstream module can give a more specific
--- instance that uses 'Generic' to construct an optic automatically.
---
--- To support this, the last parameter will be instantiated to 'RepDefined' if
--- at least one of @s@ or @t@ has a 'Generic' instance.
-class GeneralLabelOptic (name :: Symbol) k s t a b (repDefined :: RepDefined) where
-  -- | Used to interpret overloaded label syntax in the absence of an explicit
-  -- 'LabelOptic' instance.
-  generalLabelOptic :: Optic k NoIx s t a b
-
-data Void0
--- | If for an overloaded label @#label@ there is no instance starting with
--- @LabelOptic "label"@, using it in the context of optics makes GHC immediately
--- pick the overlappable instance defined below (since no other instance could
--- match). If at this point GHC has no information about @s@ or @t@, it ends up
--- picking incoherent instance of GeneralLabelOptic defined below. Prevent that
--- (if only to be able to inspect most polymorphic types of @#foo % #bar@ or
--- @view #foo@ in GHCi) by defining a dummy instance that matches all names,
--- thus postponing instance resolution.
-instance
-  ( k ~ An_Iso, a ~ Void0, b ~ Void0
-  ) => LabelOptic name k Void0 Void0 a b where
-  labelOptic = Optic id
-
--- | If no instance matches, fall back on 'GeneralLabelOptic'.
-instance {-# OVERLAPPABLE #-}
-  ( LabelOptic name k s t a b -- Needed to satisfy functional dependencies
-  , GeneralLabelOptic name k s t a b (AnyHasRep (Rep s) (Rep t))
-  ) => LabelOptic name k s t a b where
-  labelOptic = generalLabelOptic @name @k @s @t @a @b @(AnyHasRep (Rep s) (Rep t))
-
--- | If no instance matches, GHC tends to bury error messages "No instance for
--- LabelOptic..." within a ton of other error messages about ambiguous type
--- variables and overlapping instances which are irrelevant and confusing. Use
--- incoherent instance providing a custom type error to cut its efforts short.
-instance {-# INCOHERENT #-}
-  TypeError
-   ('Text "No instance for LabelOptic " ':<>: 'ShowType name
-    ':<>: 'Text " " ':<>: QuoteType k
-    ':<>: 'Text " " ':<>: QuoteType s
-    ':<>: 'Text " " ':<>: QuoteType t
-    ':<>: 'Text " " ':<>: QuoteType a
-    ':<>: 'Text " " ':<>: QuoteType b
-    ':$$: 'Text "Perhaps you forgot to define it or misspelled its name?")
-   => GeneralLabelOptic name k s t a b repDefined where
-  generalLabelOptic = error "unreachable"
-
-instance
-  (LabelOptic name k s t a b, is ~ NoIx
-  ) => IsLabel name (Optic k is s t a b) where
-#if __GLASGOW_HASKELL__ >= 802
-  fromLabel = labelOptic @name @k @s @t @a @b
-#else
-  fromLabel _ = labelOptic @name @k @s @t @a @b
-#endif
 
 -- $setup
 -- >>> import Optics.Core
diff --git a/src/Optics/Internal/Optic/Subtyping.hs b/src/Optics/Internal/Optic/Subtyping.hs
--- a/src/Optics/Internal/Optic/Subtyping.hs
+++ b/src/Optics/Internal/Optic/Subtyping.hs
@@ -147,174 +147,293 @@
 
 -- | Computes the least upper bound of two optics kinds.
 --
--- @Join k l@ represents the least upper bound of an @Optic k@ and an @Optic
--- l@. This means in particular that composition of an @Optic k@ and an @Optic
--- k@ will yield an @Optic (Join k l)@.
+-- In presence of a @JoinKinds k l m@ constraint @Optic m@ represents the least
+-- upper bound of an @Optic k@ and an @Optic l@. This means in particular that
+-- composition of an @Optic k@ and an @Optic k@ will yield an @Optic m@.
 --
-type family Join (k :: OpticKind) (l :: OpticKind) where
-  -- BEGIN GENERATED CONTENT
-  -- An_Iso-----
-  Join An_Iso             A_ReversedLens     = A_ReversedLens
-  Join An_Iso             A_ReversedPrism    = A_ReversedPrism
-  Join An_Iso             A_Prism            = A_Prism
-  Join An_Iso             A_Review           = A_Review
-  Join An_Iso             A_Lens             = A_Lens
-  Join An_Iso             A_Getter           = A_Getter
-  Join An_Iso             An_AffineTraversal = An_AffineTraversal
-  Join An_Iso             An_AffineFold      = An_AffineFold
-  Join An_Iso             A_Traversal        = A_Traversal
-  Join An_Iso             A_Fold             = A_Fold
-  Join An_Iso             A_Setter           = A_Setter
+-- @since 0.4
+--
+class JoinKinds k l m | k l -> m where
+  joinKinds :: ((Constraints k p, Constraints l p) => r) -> (Constraints m p => r)
 
-  -- A_ReversedLens-----
-  Join A_ReversedLens     An_Iso             = A_ReversedLens
-  -- no Join with         A_ReversedPrism
-  Join A_ReversedLens     A_Prism            = A_Review
-  Join A_ReversedLens     A_Review           = A_Review
-  -- no Join with         A_Lens
-  -- no Join with         A_Getter
-  -- no Join with         An_AffineTraversal
-  -- no Join with         An_AffineFold
-  -- no Join with         A_Traversal
-  -- no Join with         A_Fold
-  -- no Join with         A_Setter
+-- BEGIN GENERATED CONTENT
 
-  -- A_ReversedPrism-----
-  Join A_ReversedPrism    An_Iso             = A_ReversedPrism
-  -- no Join with         A_ReversedLens
-  Join A_ReversedPrism    A_Prism            = An_AffineFold
-  -- no Join with         A_Review
-  Join A_ReversedPrism    A_Lens             = A_Getter
-  Join A_ReversedPrism    A_Getter           = A_Getter
-  Join A_ReversedPrism    An_AffineTraversal = An_AffineFold
-  Join A_ReversedPrism    An_AffineFold      = An_AffineFold
-  Join A_ReversedPrism    A_Traversal        = A_Fold
-  Join A_ReversedPrism    A_Fold             = A_Fold
-  -- no Join with         A_Setter
+-- An_Iso -----
+instance JoinKinds An_Iso             An_Iso             An_Iso             where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_ReversedLens     A_ReversedLens     where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_ReversedPrism    A_ReversedPrism    where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Prism            A_Prism            where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Review           A_Review           where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Lens             A_Lens             where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Getter           A_Getter           where
+  joinKinds r = r
+instance JoinKinds An_Iso             An_AffineTraversal An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds An_Iso             An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Traversal        A_Traversal        where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds An_Iso             A_Setter           A_Setter           where
+  joinKinds r = r
 
-  -- A_Prism-----
-  Join A_Prism            An_Iso             = A_Prism
-  Join A_Prism            A_ReversedLens     = A_Review
-  Join A_Prism            A_ReversedPrism    = An_AffineFold
-  Join A_Prism            A_Review           = A_Review
-  Join A_Prism            A_Lens             = An_AffineTraversal
-  Join A_Prism            A_Getter           = An_AffineFold
-  Join A_Prism            An_AffineTraversal = An_AffineTraversal
-  Join A_Prism            An_AffineFold      = An_AffineFold
-  Join A_Prism            A_Traversal        = A_Traversal
-  Join A_Prism            A_Fold             = A_Fold
-  Join A_Prism            A_Setter           = A_Setter
+-- A_ReversedLens -----
+instance JoinKinds A_ReversedLens     A_ReversedLens     A_ReversedLens     where
+  joinKinds r = r
+instance JoinKinds A_ReversedLens     An_Iso             A_ReversedLens     where
+  joinKinds r = r
+--    no JoinKinds A_ReversedLens     A_ReversedPrism
+instance JoinKinds A_ReversedLens     A_Prism            A_Review           where
+  joinKinds r = r
+instance JoinKinds A_ReversedLens     A_Review           A_Review           where
+  joinKinds r = r
+--    no JoinKinds A_ReversedLens     A_Lens
+--    no JoinKinds A_ReversedLens     A_Getter
+--    no JoinKinds A_ReversedLens     An_AffineTraversal
+--    no JoinKinds A_ReversedLens     An_AffineFold
+--    no JoinKinds A_ReversedLens     A_Traversal
+--    no JoinKinds A_ReversedLens     A_Fold
+--    no JoinKinds A_ReversedLens     A_Setter
 
-  -- A_Review-----
-  Join A_Review           An_Iso             = A_Review
-  Join A_Review           A_ReversedLens     = A_Review
-  -- no Join with         A_ReversedPrism
-  Join A_Review           A_Prism            = A_Review
-  -- no Join with         A_Lens
-  -- no Join with         A_Getter
-  -- no Join with         An_AffineTraversal
-  -- no Join with         An_AffineFold
-  -- no Join with         A_Traversal
-  -- no Join with         A_Fold
-  -- no Join with         A_Setter
+-- A_ReversedPrism -----
+instance JoinKinds A_ReversedPrism    A_ReversedPrism    A_ReversedPrism    where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    An_Iso             A_ReversedPrism    where
+  joinKinds r = r
+--    no JoinKinds A_ReversedPrism    A_ReversedLens
+instance JoinKinds A_ReversedPrism    A_Prism            An_AffineFold      where
+  joinKinds r = r
+--    no JoinKinds A_ReversedPrism    A_Review
+instance JoinKinds A_ReversedPrism    A_Lens             A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    A_Getter           A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    An_AffineTraversal An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    A_Traversal        A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_ReversedPrism    A_Fold             A_Fold             where
+  joinKinds r = r
+--    no JoinKinds A_ReversedPrism    A_Setter
 
-  -- A_Lens-----
-  Join A_Lens             An_Iso             = A_Lens
-  -- no Join with         A_ReversedLens
-  Join A_Lens             A_ReversedPrism    = A_Getter
-  Join A_Lens             A_Prism            = An_AffineTraversal
-  -- no Join with         A_Review
-  Join A_Lens             A_Getter           = A_Getter
-  Join A_Lens             An_AffineTraversal = An_AffineTraversal
-  Join A_Lens             An_AffineFold      = An_AffineFold
-  Join A_Lens             A_Traversal        = A_Traversal
-  Join A_Lens             A_Fold             = A_Fold
-  Join A_Lens             A_Setter           = A_Setter
+-- A_Prism -----
+instance JoinKinds A_Prism            A_Prism            A_Prism            where
+  joinKinds r = r
+instance JoinKinds A_Prism            An_Iso             A_Prism            where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_ReversedLens     A_Review           where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_ReversedPrism    An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Review           A_Review           where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Lens             An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Getter           An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Prism            An_AffineTraversal An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds A_Prism            An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Traversal        A_Traversal        where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Prism            A_Setter           A_Setter           where
+  joinKinds r = r
 
-  -- A_Getter-----
-  Join A_Getter           An_Iso             = A_Getter
-  -- no Join with         A_ReversedLens
-  Join A_Getter           A_ReversedPrism    = A_Getter
-  Join A_Getter           A_Prism            = An_AffineFold
-  -- no Join with         A_Review
-  Join A_Getter           A_Lens             = A_Getter
-  Join A_Getter           An_AffineTraversal = An_AffineFold
-  Join A_Getter           An_AffineFold      = An_AffineFold
-  Join A_Getter           A_Traversal        = A_Fold
-  Join A_Getter           A_Fold             = A_Fold
-  -- no Join with         A_Setter
+-- A_Review -----
+instance JoinKinds A_Review           A_Review           A_Review           where
+  joinKinds r = r
+instance JoinKinds A_Review           An_Iso             A_Review           where
+  joinKinds r = r
+instance JoinKinds A_Review           A_ReversedLens     A_Review           where
+  joinKinds r = r
+--    no JoinKinds A_Review           A_ReversedPrism
+instance JoinKinds A_Review           A_Prism            A_Review           where
+  joinKinds r = r
+--    no JoinKinds A_Review           A_Lens
+--    no JoinKinds A_Review           A_Getter
+--    no JoinKinds A_Review           An_AffineTraversal
+--    no JoinKinds A_Review           An_AffineFold
+--    no JoinKinds A_Review           A_Traversal
+--    no JoinKinds A_Review           A_Fold
+--    no JoinKinds A_Review           A_Setter
 
-  -- An_AffineTraversal-----
-  Join An_AffineTraversal An_Iso             = An_AffineTraversal
-  -- no Join with         A_ReversedLens
-  Join An_AffineTraversal A_ReversedPrism    = An_AffineFold
-  Join An_AffineTraversal A_Prism            = An_AffineTraversal
-  -- no Join with         A_Review
-  Join An_AffineTraversal A_Lens             = An_AffineTraversal
-  Join An_AffineTraversal A_Getter           = An_AffineFold
-  Join An_AffineTraversal An_AffineFold      = An_AffineFold
-  Join An_AffineTraversal A_Traversal        = A_Traversal
-  Join An_AffineTraversal A_Fold             = A_Fold
-  Join An_AffineTraversal A_Setter           = A_Setter
+-- A_Lens -----
+instance JoinKinds A_Lens             A_Lens             A_Lens             where
+  joinKinds r = r
+instance JoinKinds A_Lens             An_Iso             A_Lens             where
+  joinKinds r = r
+--    no JoinKinds A_Lens             A_ReversedLens
+instance JoinKinds A_Lens             A_ReversedPrism    A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_Lens             A_Prism            An_AffineTraversal where
+  joinKinds r = r
+--    no JoinKinds A_Lens             A_Review
+instance JoinKinds A_Lens             A_Getter           A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_Lens             An_AffineTraversal An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds A_Lens             An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Lens             A_Traversal        A_Traversal        where
+  joinKinds r = r
+instance JoinKinds A_Lens             A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Lens             A_Setter           A_Setter           where
+  joinKinds r = r
 
-  -- An_AffineFold-----
-  Join An_AffineFold      An_Iso             = An_AffineFold
-  -- no Join with         A_ReversedLens
-  Join An_AffineFold      A_ReversedPrism    = An_AffineFold
-  Join An_AffineFold      A_Prism            = An_AffineFold
-  -- no Join with         A_Review
-  Join An_AffineFold      A_Lens             = An_AffineFold
-  Join An_AffineFold      A_Getter           = An_AffineFold
-  Join An_AffineFold      An_AffineTraversal = An_AffineFold
-  Join An_AffineFold      A_Traversal        = A_Fold
-  Join An_AffineFold      A_Fold             = A_Fold
-  -- no Join with         A_Setter
+-- A_Getter -----
+instance JoinKinds A_Getter           A_Getter           A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_Getter           An_Iso             A_Getter           where
+  joinKinds r = r
+--    no JoinKinds A_Getter           A_ReversedLens
+instance JoinKinds A_Getter           A_ReversedPrism    A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_Getter           A_Prism            An_AffineFold      where
+  joinKinds r = r
+--    no JoinKinds A_Getter           A_Review
+instance JoinKinds A_Getter           A_Lens             A_Getter           where
+  joinKinds r = r
+instance JoinKinds A_Getter           An_AffineTraversal An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Getter           An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds A_Getter           A_Traversal        A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Getter           A_Fold             A_Fold             where
+  joinKinds r = r
+--    no JoinKinds A_Getter           A_Setter
 
-  -- A_Traversal-----
-  Join A_Traversal        An_Iso             = A_Traversal
-  -- no Join with         A_ReversedLens
-  Join A_Traversal        A_ReversedPrism    = A_Fold
-  Join A_Traversal        A_Prism            = A_Traversal
-  -- no Join with         A_Review
-  Join A_Traversal        A_Lens             = A_Traversal
-  Join A_Traversal        A_Getter           = A_Fold
-  Join A_Traversal        An_AffineTraversal = A_Traversal
-  Join A_Traversal        An_AffineFold      = A_Fold
-  Join A_Traversal        A_Fold             = A_Fold
-  Join A_Traversal        A_Setter           = A_Setter
+-- An_AffineTraversal -----
+instance JoinKinds An_AffineTraversal An_AffineTraversal An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal An_Iso             An_AffineTraversal where
+  joinKinds r = r
+--    no JoinKinds An_AffineTraversal A_ReversedLens
+instance JoinKinds An_AffineTraversal A_ReversedPrism    An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal A_Prism            An_AffineTraversal where
+  joinKinds r = r
+--    no JoinKinds An_AffineTraversal A_Review
+instance JoinKinds An_AffineTraversal A_Lens             An_AffineTraversal where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal A_Getter           An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal A_Traversal        A_Traversal        where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds An_AffineTraversal A_Setter           A_Setter           where
+  joinKinds r = r
 
-  -- A_Fold-----
-  Join A_Fold             An_Iso             = A_Fold
-  -- no Join with         A_ReversedLens
-  Join A_Fold             A_ReversedPrism    = A_Fold
-  Join A_Fold             A_Prism            = A_Fold
-  -- no Join with         A_Review
-  Join A_Fold             A_Lens             = A_Fold
-  Join A_Fold             A_Getter           = A_Fold
-  Join A_Fold             An_AffineTraversal = A_Fold
-  Join A_Fold             An_AffineFold      = A_Fold
-  Join A_Fold             A_Traversal        = A_Fold
-  -- no Join with         A_Setter
+-- An_AffineFold -----
+instance JoinKinds An_AffineFold      An_AffineFold      An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      An_Iso             An_AffineFold      where
+  joinKinds r = r
+--    no JoinKinds An_AffineFold      A_ReversedLens
+instance JoinKinds An_AffineFold      A_ReversedPrism    An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      A_Prism            An_AffineFold      where
+  joinKinds r = r
+--    no JoinKinds An_AffineFold      A_Review
+instance JoinKinds An_AffineFold      A_Lens             An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      A_Getter           An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      An_AffineTraversal An_AffineFold      where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      A_Traversal        A_Fold             where
+  joinKinds r = r
+instance JoinKinds An_AffineFold      A_Fold             A_Fold             where
+  joinKinds r = r
+--    no JoinKinds An_AffineFold      A_Setter
 
-  -- A_Setter-----
-  Join A_Setter           An_Iso             = A_Setter
-  -- no Join with         A_ReversedLens
-  -- no Join with         A_ReversedPrism
-  Join A_Setter           A_Prism            = A_Setter
-  -- no Join with         A_Review
-  Join A_Setter           A_Lens             = A_Setter
-  -- no Join with         A_Getter
-  Join A_Setter           An_AffineTraversal = A_Setter
-  -- no Join with         An_AffineFold
-  Join A_Setter           A_Traversal        = A_Setter
-  -- no Join with         A_Fold
+-- A_Traversal -----
+instance JoinKinds A_Traversal        A_Traversal        A_Traversal        where
+  joinKinds r = r
+instance JoinKinds A_Traversal        An_Iso             A_Traversal        where
+  joinKinds r = r
+--    no JoinKinds A_Traversal        A_ReversedLens
+instance JoinKinds A_Traversal        A_ReversedPrism    A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Traversal        A_Prism            A_Traversal        where
+  joinKinds r = r
+--    no JoinKinds A_Traversal        A_Review
+instance JoinKinds A_Traversal        A_Lens             A_Traversal        where
+  joinKinds r = r
+instance JoinKinds A_Traversal        A_Getter           A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Traversal        An_AffineTraversal A_Traversal        where
+  joinKinds r = r
+instance JoinKinds A_Traversal        An_AffineFold      A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Traversal        A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Traversal        A_Setter           A_Setter           where
+  joinKinds r = r
 
-  -- END GENERATED CONTENT
+-- A_Fold -----
+instance JoinKinds A_Fold             A_Fold             A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             An_Iso             A_Fold             where
+  joinKinds r = r
+--    no JoinKinds A_Fold             A_ReversedLens
+instance JoinKinds A_Fold             A_ReversedPrism    A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             A_Prism            A_Fold             where
+  joinKinds r = r
+--    no JoinKinds A_Fold             A_Review
+instance JoinKinds A_Fold             A_Lens             A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             A_Getter           A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             An_AffineTraversal A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             An_AffineFold      A_Fold             where
+  joinKinds r = r
+instance JoinKinds A_Fold             A_Traversal        A_Fold             where
+  joinKinds r = r
+--    no JoinKinds A_Fold             A_Setter
 
-  -- Every optic kinds can be joined with itself.
-  Join k k = k
+-- A_Setter -----
+instance JoinKinds A_Setter           A_Setter           A_Setter           where
+  joinKinds r = r
+instance JoinKinds A_Setter           An_Iso             A_Setter           where
+  joinKinds r = r
+--    no JoinKinds A_Setter           A_ReversedLens
+--    no JoinKinds A_Setter           A_ReversedPrism
+instance JoinKinds A_Setter           A_Prism            A_Setter           where
+  joinKinds r = r
+--    no JoinKinds A_Setter           A_Review
+instance JoinKinds A_Setter           A_Lens             A_Setter           where
+  joinKinds r = r
+--    no JoinKinds A_Setter           A_Getter
+instance JoinKinds A_Setter           An_AffineTraversal A_Setter           where
+  joinKinds r = r
+--    no JoinKinds A_Setter           An_AffineFold
+instance JoinKinds A_Setter           A_Traversal        A_Setter           where
+  joinKinds r = r
+--    no JoinKinds A_Setter           A_Fold
 
-  -- Everything else is a type error.
-  Join k l = TypeError ('ShowType k
-                        ':<>: 'Text " cannot be composed with "
-                        ':<>: 'ShowType l)
+-- END GENERATED CONTENT
+
+instance {-# OVERLAPPABLE #-}
+  ( JoinKinds k l m
+  , TypeError ('ShowType k ':<>: 'Text " cannot be composed with " ':<>: 'ShowType l)
+  ) => JoinKinds k l m where
+  joinKinds _ = error "unreachable"
diff --git a/src/Optics/Internal/Optic/TypeLevel.hs b/src/Optics/Internal/Optic/TypeLevel.hs
--- a/src/Optics/Internal/Optic/TypeLevel.hs
+++ b/src/Optics/Internal/Optic/TypeLevel.hs
@@ -1,13 +1,14 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_HADDOCK not-home #-}
 
 -- | This module is intended for internal use only, and may change without
 -- warning in subsequent releases.
 module Optics.Internal.Optic.TypeLevel where
 
-import Data.Kind (Type)
+import Data.Kind
 import GHC.TypeLits
 
 -- | A list of index types, used for indexed optics.
@@ -21,14 +22,6 @@
 -- | Singleton index list
 type WithIx i = ('[i] :: IxList)
 
--- | Show a type surrounded by quote marks.
-type family QuoteType (x :: Type) :: ErrorMessage where
-  QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’"
-
--- | Show a symbol surrounded by quote marks.
-type family QuoteSymbol (x :: Symbol) :: ErrorMessage where
-  QuoteSymbol x = 'Text "‘" ':<>: 'Text x ':<>: 'Text "’"
-
 ----------------------------------------
 -- Elimination forms in error messages
 
@@ -60,14 +53,12 @@
     ShowSymbolsWithOrigin fs ':$$: 'Text "  " ':<>: ShowOperators ops
 
 ----------------------------------------
+-- Lists
 
-data RepDefined = RepDefined
--- | This type family should be called with applications of 'Rep' on both sides,
--- and will reduce to 'RepDefined' if at least one of them is defined; otherwise
--- it is stuck.
-type family AnyHasRep (s :: Type -> Type) (t :: Type -> Type) :: RepDefined
-type instance AnyHasRep (s x) t = 'RepDefined
-type instance AnyHasRep s (t x) = 'RepDefined
+-- | Reverse a type-level list.
+type family Reverse (xs :: [k]) (acc :: [k]) :: [k] where
+  Reverse '[]      acc = acc
+  Reverse (x : xs) acc = Reverse xs (x : acc)
 
 -- | Curry a type-level list.
 --
@@ -96,8 +87,94 @@
 
 instance CurryCompose '[] where
   composeN = id
-  {-# INLINE composeN #-}
 
 instance CurryCompose xs => CurryCompose (x ': xs) where
   composeN ij f = composeN @xs ij . f
-  {-# INLINE composeN #-}
+
+----------------------------------------
+-- Indices
+
+-- | Tagged version of 'Data.Type.Equality.(:~:)' for carrying evidence that two
+-- index lists in a curried form are equal.
+data IxEq i is js where
+  IxEq :: IxEq i is is
+
+-- | In pseudo (dependent-)Haskell, provide a witness
+--
+-- @
+-- foldr f (foldr f init xs) ys = foldr f init (ys ++ xs)
+--    where f = (->)
+-- @
+--
+-- @since 0.4
+--
+class AppendIndices xs ys ks | xs ys -> ks where
+  appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)
+
+-- | If the second list is empty, we can shortcircuit and pick the first list
+-- immediately.
+instance {-# INCOHERENT #-} AppendIndices xs '[] xs where
+  appendIndices = IxEq
+
+instance AppendIndices '[] ys ys where
+  appendIndices = IxEq
+
+instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where
+  appendIndices :: forall i. IxEq i (Curry (x ': xs) (Curry ys i)) (Curry (x ': ks) i)
+  appendIndices | IxEq <- appendIndices @xs @ys @ks @i = IxEq
+
+----------------------------------------
+-- Either
+
+-- | If lhs is 'Right', return it. Otherwise check rhs.
+type family FirstRight (m1 :: Either e a) (m2 :: Either e a) :: Either e a where
+  FirstRight ('Right a) _ = 'Right a
+  FirstRight          _ b = b
+
+type family FromRight (def :: b) (e :: Either a b) :: b where
+  FromRight _   ('Right b) = b
+  FromRight def ('Left  _) = def
+
+type family IsLeft (e :: Either a b) :: Bool where
+  IsLeft ('Left _)  = 'True
+  IsLeft ('Right _) = 'False
+
+----------------------------------------
+-- Errors
+
+-- | Show a custom type error if @p@ is true.
+type family When (p :: Bool) (err :: Constraint) :: Constraint where
+  When 'True  err = err
+  When 'False _   = ()
+
+-- | Show a custom type error if @p@ is false (or stuck).
+type family Unless (p :: Bool) (err :: Constraint) :: Constraint where
+  Unless 'True  _   = ()
+  Unless 'False err = err
+
+-- | Use with 'Unless' to detect stuck (undefined) type families.
+type family Defined (f :: k) :: Bool where
+  Defined (f _) = Defined f
+  Defined _     = 'True
+
+-- | Show a type surrounded by quote marks.
+type family QuoteType (x :: t) :: ErrorMessage where
+  QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’"
+
+-- | Show a symbol surrounded by quote marks.
+type family QuoteSymbol (x :: Symbol) :: ErrorMessage where
+  QuoteSymbol x = 'Text "‘" ':<>: 'Text x ':<>: 'Text "’"
+
+type family ToOrdinal (n :: Nat) :: ErrorMessage where
+  ToOrdinal 1 = 'Text "1st"
+  ToOrdinal 2 = 'Text "2nd"
+  ToOrdinal 3 = 'Text "3rd"
+  ToOrdinal n = 'ShowType n ':<>: 'Text "th"
+
+----------------------------------------
+-- Misc
+
+-- | Derive the shape of @a@ from the shape of @b@.
+class HasShapeOf (a :: k) (b :: k)
+instance {-# OVERLAPPING #-} (fa ~ f a, HasShapeOf f g) => HasShapeOf fa (g b)
+instance (a ~ b) => HasShapeOf a b
diff --git a/src/Optics/Internal/Utils.hs b/src/Optics/Internal/Utils.hs
--- a/src/Optics/Internal/Utils.hs
+++ b/src/Optics/Internal/Utils.hs
@@ -31,25 +31,18 @@
 
 instance Applicative Identity' where
   pure a = Identity' () a
-  {-# INLINE pure #-}
   Identity' () f <*> Identity' () x = Identity' () (f x)
-  {-# INLINE (<*>) #-}
 
 instance Mapping (Star Identity') where
   roam  f (Star k) = Star $ wrapIdentity' . f (unwrapIdentity' . k)
   iroam f (Star k) = Star $ wrapIdentity' . f (\_ -> unwrapIdentity' . k)
-  {-# INLINE roam #-}
-  {-# INLINE iroam #-}
 
 instance Mapping (IxStar Identity') where
   roam  f (IxStar k) =
     IxStar $ \i -> wrapIdentity' . f (unwrapIdentity' . k i)
   iroam f (IxStar k) =
     IxStar $ \ij -> wrapIdentity' . f (\i -> unwrapIdentity' . k (ij i))
-  {-# INLINE roam #-}
-  {-# INLINE iroam #-}
 
-
 -- | Mark a value for evaluation to whnf.
 --
 -- This allows us to, when applying a setter to a structure, evaluate only the
@@ -59,11 +52,9 @@
 --
 wrapIdentity' :: a -> Identity' a
 wrapIdentity' a = Identity' (a `seq` ()) a
-{-# INLINE wrapIdentity' #-}
 
 unwrapIdentity' :: Identity' a -> a
 unwrapIdentity' (Identity' () a) = a
-{-# INLINE unwrapIdentity' #-}
 
 ----------------------------------------
 
@@ -75,17 +66,13 @@
 
 runTraversed :: Functor f => Traversed f a -> f ()
 runTraversed (Traversed fa) = () <$ fa
-{-# INLINE runTraversed #-}
 
 instance Applicative f => SG.Semigroup (Traversed f a) where
   Traversed ma <> Traversed mb = Traversed (ma *> mb)
-  {-# INLINE (<>) #-}
 
 instance Applicative f => Monoid (Traversed f a) where
   mempty = Traversed (pure (error "Traversed: value used"))
   mappend = (SG.<>)
-  {-# INLINE mempty #-}
-  {-# INLINE mappend #-}
 
 ----------------------------------------
 
@@ -96,18 +83,14 @@
 instance Applicative f => Applicative (OrT f) where
   pure = OrT False . pure
   OrT a f <*> OrT b x = OrT (a || b) (f <*> x)
-  {-# INLINE pure #-}
-  {-# INLINE (<*>) #-}
 
 -- | Wrap the applicative action in 'OrT' so that we know later that it was
 -- executed.
 wrapOrT :: f a -> OrT f a
 wrapOrT = OrT True
-{-# INLINE wrapOrT #-}
 
 -- | 'uncurry' with no lazy pattern matching for more efficient code.
 --
 -- @since 0.3
 uncurry' :: (a -> b -> c) -> (a, b) -> c
 uncurry' f (a, b) = f a b
-{-# INLINE uncurry' #-}
diff --git a/src/Optics/IxAffineTraversal.hs b/src/Optics/IxAffineTraversal.hs
--- a/src/Optics/IxAffineTraversal.hs
+++ b/src/Optics/IxAffineTraversal.hs
@@ -120,8 +120,9 @@
 -- no substructures.
 --
 -- This is the identity element when a 'Optics.Fold.Fold',
--- 'Optics.AffineFold.AffineFold', 'Optics.IxFold.IxFold' or
--- 'Optics.IxAffineFold.IxAffineFold' is viewed as a monoid.
+-- 'Optics.AffineFold.AffineFold', 'Optics.IxFold.IxFold',
+-- 'Optics.IxAffineFold.IxAffineFold', 'Optics.Traversal.Traversal' or
+-- 'Optics.IxTraversal.IxTraversal' is viewed as a monoid.
 --
 -- >>> 6 & ignored %~ absurd
 -- 6
diff --git a/src/Optics/IxFold.hs b/src/Optics/IxFold.hs
--- a/src/Optics/IxFold.hs
+++ b/src/Optics/IxFold.hs
@@ -44,7 +44,7 @@
   , ifiltered
   , ibackwards_
 
-  -- * Monoid structures
+  -- * Monoid structures #monoids#
   -- | 'IxFold' admits (at least) two monoid structures:
   --
   -- * 'isumming' concatenates results from both folds.
@@ -246,6 +246,7 @@
 -- >>> itoListOf (ifolded `isumming` ibackwards_ ifolded) ["a","b"]
 -- [(0,"a"),(1,"b"),(1,"b"),(0,"a")]
 --
+-- For the traversal version see 'Optics.IxTraversal.iadjoin'.
 isumming
   :: (Is k A_Fold, Is l A_Fold,
       is1 `HasSingleIndex` i, is2 `HasSingleIndex` i)
diff --git a/src/Optics/IxLens.hs b/src/Optics/IxLens.hs
--- a/src/Optics/IxLens.hs
+++ b/src/Optics/IxLens.hs
@@ -29,7 +29,10 @@
   -- @
 
   -- * Additional introduction forms
+  , chosen
   , devoid
+  , ifst
+  , isnd
 
   -- * Subtyping
   , A_Lens
@@ -97,6 +100,13 @@
 ----------------------------------------
 -- Lenses
 
+-- | Focus on both sides of an 'Either'.
+chosen :: IxLens (Either () ()) (Either a a) (Either b b) a b
+chosen = ilensVL $ \f -> \case
+  Left  a -> Left  <$> f (Left ())  a
+  Right a -> Right <$> f (Right ()) a
+{-# INLINE chosen #-}
+
 -- | There is an indexed field for every type in the 'Void'.
 --
 -- >>> set (mapped % devoid) 1 []
@@ -108,6 +118,32 @@
 devoid :: IxLens' i Void a
 devoid = ilens absurd const
 {-# INLINE devoid #-}
+
+-- | Indexed '_1' with other half of a pair as an index.
+--
+-- See 'isnd' for examples.
+--
+-- @since 0.4
+--
+ifst :: IxLens i (a, i) (b, i) a b
+ifst = ilens (\(a, i) -> (i, a)) (\(_,i) b -> (b, i))
+
+-- | Indexed '_2' with other half of a pair as an index.
+-- Specialized version of 'itraversed' to pairs, which can be 'IxLens'.
+--
+-- >>> iview isnd ('a', True)
+-- ('a',True)
+--
+-- That is not possible with 'itraversed', because it is an 'IxTraversal'.
+--
+-- >>> :t itraversed :: IxTraversal i (i, a) (i, b) a b
+-- itraversed :: IxTraversal i (i, a) (i, b) a b
+--   :: IxTraversal i (i, a) (i, b) a b
+--
+-- @since 0.4
+--
+isnd :: IxLens i (i, a) (i, b) a b
+isnd = ilens id (\(i,_) b -> (i, b))
 
 -- $setup
 -- >>> import Optics.Core
diff --git a/src/Optics/IxTraversal.hs b/src/Optics/IxTraversal.hs
--- a/src/Optics/IxTraversal.hs
+++ b/src/Optics/IxTraversal.hs
@@ -60,6 +60,23 @@
   , ipartsOf
   , isingular
 
+  -- * Monoid structure
+  -- | 'IxTraversal' admits a (partial) monoid structure where 'iadjoin'
+  -- combines non-overlapping indexed traversals, and the identity element is
+  -- 'ignored' (which traverses no elements).
+  --
+  -- If you merely need an 'IxFold', you can use indexed traversals as indexed
+  -- folds and combine them with one of the monoid structures on indexed folds
+  -- (see "Optics.IxFold#monoids"). In particular, 'isumming' can be used to
+  -- concatenate results from two traversals, and 'ifailing' will returns
+  -- results from the second traversal only if the first returns no results.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'IxTraversal', because
+  -- there is not a unique choice of monoid to use that works for all optics,
+  -- and the ('<>') operator could not be used to combine optics of different
+  -- kinds.
+  , iadjoin
+
   -- * Subtyping
   , A_Traversal
 
@@ -338,6 +355,122 @@
       Just a' -> put Nothing >> pure a'
       Nothing ->                pure a
 {-# INLINE isingular #-}
+
+-- | Combine two disjoint indexed traversals into one.
+--
+-- >>> iover (_1 % itraversed `iadjoin` _2 % itraversed) (+) ([0, 0, 0], (3, 5))
+-- ([0,1,2],(3,8))
+--
+-- /Note:/ if the argument traversals are not disjoint, the result will not
+-- respect the 'IxTraversal' laws, because it will visit the same element multiple
+-- times.  See section 7 of
+-- <https://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf Understanding Idiomatic Traversals Backwards and Forwards>
+-- by Bird et al. for why this is illegal.
+--
+-- >>> iview (ipartsOf (each `iadjoin` each)) ("x","y")
+-- ([0,1,0,1],["x","y","x","y"])
+-- >>> iset (ipartsOf (each `iadjoin` each)) (const ["a","b","c","d"]) ("x","y")
+-- ("c","d")
+--
+-- For the 'IxFold' version see 'Optics.IxFold.isumming'.
+--
+-- @since 0.4
+--
+iadjoin
+  :: (Is k A_Traversal, Is l A_Traversal, is `HasSingleIndex` i)
+  => Optic' k is s a
+  -> Optic' l is s a
+  -> IxTraversal' i s a
+iadjoin o1 o2 = conjoined (adjoin o1 o2) (combined % traversed % itraversed)
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+         in s2
+      )
+      <$> f (itoListOf (castOptic @A_Traversal o1) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o2) s0)
+
+    update a = get >>= \case
+      (_, a') : as' -> put as' >> pure a'
+      []            ->            pure a
+infixr 6 `iadjoin` -- Same as (<>)
+{-# INLINE [1] iadjoin #-}
+
+{-# RULES
+
+"iadjoin_12_3" forall o1 o2 o3. iadjoin o1 (iadjoin o2 o3) = iadjoin3 o1 o2 o3
+"iadjoin_21_3" forall o1 o2 o3. iadjoin (iadjoin o1 o2) o3 = iadjoin3 o1 o2 o3
+
+"iadjoin_13_4" forall o1 o2 o3 o4. iadjoin o1 (iadjoin3 o2 o3 o4) = iadjoin4 o1 o2 o3 o4
+"iadjoin_31_4" forall o1 o2 o3 o4. iadjoin (iadjoin3 o1 o2 o3) o4 = iadjoin4 o1 o2 o3 o4
+
+#-}
+
+-- | Triple 'iadjoin' for optimizing multiple 'iadjoin's with rewrite rules.
+iadjoin3
+  :: (Is k1 A_Traversal, Is k2 A_Traversal, Is k3 A_Traversal, is `HasSingleIndex` i )
+  => Optic' k1 is s a
+  -> Optic' k2 is s a
+  -> Optic' k3 is s a
+  -> IxTraversal' i s a
+iadjoin3 o1 o2 o3 = conjoined (o1 `adjoin` o2 `adjoin` o3)
+                              (combined % traversed % itraversed)
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 r3 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+             s3 = evalState (traverseOf o3 update s2) r3
+         in s3
+      )
+      <$> f (itoListOf (castOptic @A_Traversal o1) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o2) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o3) s0)
+
+    update a = get >>= \case
+      (_, a') : as' -> put as' >> pure a'
+      []            ->            pure a
+{-# INLINE [1] iadjoin3 #-}
+
+{-# RULES
+
+"iadjoin_211_4" forall o1 o2 o3 o4. iadjoin3 (iadjoin o1 o2) o3 o4 = iadjoin4 o1 o2 o3 o4
+"iadjoin_121_4" forall o1 o2 o3 o4. iadjoin3 o1 (iadjoin o2 o3) o4 = iadjoin4 o1 o2 o3 o4
+"iadjoin_112_4" forall o1 o2 o3 o4. iadjoin3 o1 o2 (iadjoin o3 o4) = iadjoin4 o1 o2 o3 o4
+
+#-}
+
+-- | Quadruple 'iadjoin' for optimizing multiple 'iadjoin's with rewrite rules.
+iadjoin4
+  :: ( Is k1 A_Traversal, Is k2 A_Traversal, Is k3 A_Traversal, Is k4 A_Traversal
+     , is `HasSingleIndex` i)
+  => Optic' k1 is s a
+  -> Optic' k2 is s a
+  -> Optic' k3 is s a
+  -> Optic' k4 is s a
+  -> IxTraversal' i s a
+iadjoin4 o1 o2 o3 o4 = conjoined (o1 `adjoin` o2 `adjoin` o3 `adjoin` o4)
+                                 (combined % traversed % itraversed)
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 r3 r4 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+             s3 = evalState (traverseOf o3 update s2) r3
+             s4 = evalState (traverseOf o4 update s3) r4
+         in s4
+      )
+      <$> f (itoListOf (castOptic @A_Traversal o1) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o2) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o3) s0)
+      <*> f (itoListOf (castOptic @A_Traversal o4) s0)
+
+    update a = get >>= \case
+      (_, a') : as' -> put as' >> pure a'
+      []            ->            pure a
+{-# INLINE [1] iadjoin4 #-}
 
 -- $setup
 -- >>> import Data.Void
diff --git a/src/Optics/Label.hs b/src/Optics/Label.hs
--- a/src/Optics/Label.hs
+++ b/src/Optics/Label.hs
@@ -1,6 +1,13 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 -- |
 -- Module: Optics.Label
--- Description: Overloaded labels as optics
+-- Description: Overloaded labels as optics.
 --
 -- Overloaded labels are a solution to Haskell's namespace problem for records.
 -- The @-XOverloadedLabels@ extension allows a new expression syntax for labels,
@@ -27,65 +34,55 @@
     -- ** 'LabelOptic' type class
     LabelOptic(..)
   , LabelOptic'
+  , GenericLabelOptics(..)
 
     -- ** Structure of 'LabelOptic' instances
     -- $instanceStructure
 
-    -- ** Limitations arising from functional dependencies
-    -- $fundepLimitations
+    -- ** Explanation of functional dependencies
+    -- $fundepExplanation
   ) where
 
+import Data.Type.Bool
+import Data.Type.Equality
+import GHC.Generics
+import GHC.OverloadedLabels
+import GHC.TypeLits
+
+import Optics.Internal.Generic
+import Optics.Internal.Magic
 import Optics.Internal.Optic
 
 -- $sampleUsage
 --
 -- #usage#
--- An example showing how overloaded labels can be used as optics.
 --
--- >>> :set -XDataKinds
+-- An example showing how overloaded labels can be used as optics for fields of
+-- types having a 'Generic' instance.
+--
+-- >>> :set -XDeriveAnyClass
+-- >>> :set -XDeriveGeneric
 -- >>> :set -XDuplicateRecordFields
--- >>> :set -XFlexibleInstances
--- >>> :set -XMultiParamTypeClasses
 -- >>> :set -XOverloadedLabels
--- >>> :set -XTypeFamilies
--- >>> :set -XUndecidableInstances
+-- >>> import GHC.Generics (Generic)
 -- >>> :{
 -- data Human = Human
 --   { name :: String
 --   , age  :: Integer
 --   , pets :: [Pet]
---   } deriving Show
+--   } deriving (Show, Generic)
 -- data Pet
 --   = Cat  { name :: String, age :: Int, lazy :: Bool }
---   | Fish { name :: String, age :: Int }
---   deriving Show
+--   | Fish { name :: String, age :: Int, lazy :: Bool }
+--   deriving (Show, Generic)
 -- :}
 --
--- The following instances can be generated by @makeFieldLabelsWith
--- noPrefixFieldLabels@ from
--- @<https://hackage.haskell.org/package/optics-th/docs/Optics-TH.html Optics.TH>@
--- in the @<https://hackage.haskell.org/package/optics-th optics-th>@ package:
---
--- >>> :{
--- instance (k ~ A_Lens, a ~ String, b ~ String) => LabelOptic "name" k Human Human a b where
---   labelOptic = lensVL $ \f (Human name age pets) -> (\name' -> Human name' age pets) <$> f name
--- instance (k ~ A_Lens, a ~ Integer, b ~ Integer) => LabelOptic "age" k Human Human a b where
---   labelOptic = lensVL $ \f (Human name age pets) -> (\age' -> Human name age' pets) <$> f age
--- instance (k ~ A_Lens, a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" k Human Human a b where
---   labelOptic = lensVL $ \f (Human name age pets) -> (\pets' -> Human name age pets') <$> f pets
--- instance (k ~ A_Lens, a ~ String, b ~ String) => LabelOptic "name" k Pet Pet a b where
---   labelOptic = lensVL $ \f s -> case s of
---     Cat  name age lazy -> (\name' -> Cat  name' age lazy) <$> f name
---     Fish name age      -> (\name' -> Fish name' age     ) <$> f name
--- instance (k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "age" k Pet Pet a b where
---   labelOptic = lensVL $ \f s -> case s of
---     Cat  name age lazy -> (\age' -> Cat  name age' lazy) <$> f age
---     Fish name age      -> (\age' -> Fish name age'     ) <$> f age
--- instance (k ~ An_AffineTraversal, a ~ Bool, b ~ Bool) => LabelOptic "lazy" k Pet Pet a b where
---   labelOptic = atraversalVL $ \point f s -> case s of
---     Cat name age lazy -> (\lazy' -> Cat name age lazy') <$> f lazy
---     _                 -> point s
--- :}
+-- /Note:/ Generic deriving of optics works well on a moderate scale, but for
+-- ubiquitous usage (and in production in general) we recommend generating them
+-- with Template Haskell as it scales better in terms of compilation time. For
+-- more details see @makeFieldLabelsNoPrefix@ from
+-- <https://hackage.haskell.org/package/optics-th/docs/Optics-TH.html Optics.TH>
+-- in the <https://hackage.haskell.org/package/optics-th optics-th> package.
 --
 -- Here is some test data:
 --
@@ -95,6 +92,7 @@
 --               , age  = 13
 --               , pets = [ Fish { name = "Goldie"
 --                               , age  = 1
+--                               , lazy = False
 --                               }
 --                        , Cat { name = "Loopy"
 --                              , age  = 3
@@ -110,12 +108,12 @@
 --
 -- Now we can ask for Peter's name:
 --
--- >>> view #name peter
+-- >>> peter ^. #name
 -- "Peter"
 --
 -- or for names of his pets:
 --
--- >>> toListOf (#pets % folded % #name) peter
+-- >>> peter ^.. #pets % folded % #name
 -- ["Goldie","Loopy","Sparky"]
 --
 -- We can check whether any of his pets is lazy:
@@ -125,12 +123,12 @@
 --
 -- or how things might be be a year from now:
 --
--- >>> peter & over #age (+1) & over (#pets % mapped % #age) (+1)
--- Human {name = "Peter", age = 14, pets = [Fish {name = "Goldie", age = 2},Cat {name = "Loopy", age = 4, lazy = False},Cat {name = "Sparky", age = 3, lazy = True}]}
+-- >>> peter & #age %~ (+1) & #pets % mapped % #age %~ (+1)
+-- Human {name = "Peter", age = 14, pets = [Fish {name = "Goldie", age = 2, lazy = False},Cat {name = "Loopy", age = 4, lazy = False},Cat {name = "Sparky", age = 3, lazy = True}]}
 --
 -- Perhaps Peter is going on vacation and needs to leave his pets at home:
 --
--- >>> peter & set #pets []
+-- >>> peter & #pets .~ []
 -- Human {name = "Peter", age = 13, pets = []}
 
 -- $problem
@@ -199,23 +197,31 @@
 --                    }
 -- @
 --
--- Then appropriate 'LabelOptic' instances can be either written by hand or
--- generated using Template Haskell functions (defined in
--- @<https://hackage.haskell.org/package/optics-th/docs/Optics-TH.html Optics.TH>@
--- module from @<https://hackage.haskell.org/package/optics-th optics-th>@ package)
--- with
+-- Then appropriate 'LabelOptic' instances can be either written by hand,
+-- seamlessly derived via generic representation (see the
+-- <Optics-Label.html#usage Sample usage> section for more details)
+-- or generated with Template Haskell functions
+-- (defined in
+-- <https://hackage.haskell.org/package/optics-th/docs/Optics-TH.html Optics.TH>
+-- module from <https://hackage.haskell.org/package/optics-th optics-th>
+-- package) with
 --
 -- @
--- makeFieldLabelsWith noPrefixFieldLabels ''User
--- makeFieldLabelsWith noPrefixFieldLabels ''Movie
+-- makeFieldLabelsNoPrefix ''User
+-- makeFieldLabelsNoPrefix ''Movie
 -- @
 --
+-- For production software the recommended approach is generation with Template
+-- Haskell as it scales well in terms of compilation time and provides the best
+-- performance in general.
+--
 -- /Note:/ there exists a similar approach that involves prefixing field names
--- with the underscore and generation of lenses as ordinary functions so that
--- @_field@ is the ordinary field name and @field@ is the lens referencing
--- it. The drawback of such solution is inability to get working
--- jump-to-definition for field names, which makes navigation in unfamiliar code
--- bases significantly harder, so it's not recommended.
+-- (either with the underscore or name of the data type) and generation of
+-- lenses as ordinary functions so that @prefixField@ is the ordinary field name
+-- and @field@ is the lens referencing it. The drawback of such solution is
+-- inability to get working jump-to-definition for field names, which makes
+-- navigation in unfamiliar code bases significantly harder, so it's not
+-- recommended.
 --
 -- === Emulation of @NoFieldSelectors@
 --
@@ -253,7 +259,7 @@
 --                  , name :: String
 --                  }
 --
--- makeFieldLabelsWith noPrefixFieldLabels ''User
+-- makeFieldLabelsNoPrefix ''User
 --
 -- ...
 -- @
@@ -332,99 +338,119 @@
 --
 -- (3) The full power of optics at our disposal, should we ever need it.
 
--- $instanceStructure
+-- $instanceStructure #structure#
 --
--- You might wonder why instances above are written in form
+-- You might wonder why instances generated with Template Haskell have the
+-- following form:
 --
 -- @
 -- instance (k ~ A_Lens, a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" k Human Human a b where
+--   ...
 -- @
 --
 -- instead of
 --
 -- @
 -- instance LabelOptic "pets" A_Lens Human Human [Pet] [Pet] where
+--   ...
 -- @
 --
 -- The reason is that using the first form ensures that it is enough for GHC to
--- match on the instance if either @s@ or @t@ is known (as type equalities are
--- verified after the instance matches), which not only makes type inference
+-- match on the instance if either @s@ or @t@ is known (as equality constraints
+-- are solved after the instance matches), which not only makes type inference
 -- better, but also allows it to generate better error messages.
 --
--- For example, if you try to write @peter & set #pets []@ with the appropriate
--- 'LabelOptic' instance in the second form, you get the following:
+-- >>> :set -XDataKinds
+-- >>> :set -XFlexibleInstances
+-- >>> :set -XMultiParamTypeClasses
+-- >>> :set -XTypeFamilies
+-- >>> :set -XUndecidableInstances
+-- >>> :{
+-- data Pet = Dog { name :: String }
+--          | Cat { name :: String }
+--   deriving Show
+-- :}
 --
--- @
--- <interactive>:16:1: error:
---    • No instance for LabelOptic "pets" ‘A_Lens’ ‘Human’ ‘()’ ‘[Pet]’ ‘[a0]’
---        (maybe you forgot to define it or misspelled a name?)
---    • In the first argument of ‘print’, namely ‘it’
---      In a stmt of an interactive GHCi command: print it
--- @
+-- >>> :{
+-- data Human1 = Human1 { pets :: [Pet] }
+--   deriving Show
+-- instance LabelOptic "pets" A_Lens Human1 Human1 [Pet] [Pet] where
+--   labelOptic = lensVL $ \f (Human1 pets) -> Human1 <$> f pets
+-- :}
 --
--- That's because empty list doesn't have type @[Pet]@, it has type @[r]@ and
--- GHC doesn't have enough information to match on the instance we
--- provided. We'd need to either annotate the list: @peter & set #pets
--- ([]::[Pet])@ or the result type: @peter & set #pets [] :: Human@, which is
--- suboptimal.
+-- >>> :{
+-- data Human2 = Human2 { pets :: [Pet] }
+--  deriving Show
+-- instance (k ~ A_Lens, a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" k Human2 Human2 a b where
+--   labelOptic = lensVL $ \f (Human2 pets) -> Human2 <$> f pets
+-- :}
 --
--- Here are more examples of confusing error messages if the instance for
--- @LabelOptic "age"@ is written without type equalities:
+-- >>> let human1 = Human1 [Dog "Lucky"]
+-- >>> let human2 = Human2 [Cat "Sleepy"]
 --
--- @
--- λ> view #age peter :: Char
+-- Let's have a look how these two instance definitions differ.
 --
--- <interactive>:28:6: error:
---     • No instance for LabelOptic "age" ‘k0’ ‘Human’ ‘Human’ ‘Char’ ‘Char’
---         (maybe you forgot to define it or misspelled a name?)
---     • In the first argument of ‘view’, namely ‘#age’
---       In the expression: view #age peter :: Char
---       In an equation for ‘it’: it = view #age peter :: Char
--- λ> peter & set #age "hi"
+-- >>> human1 & #pets .~ []
+-- ...
+-- ...No instance for LabelOptic "pets" ‘A_Lens’ ‘Human1’ ‘()’ ‘[Pet]’ ‘[a0]’
+-- ...
 --
--- <interactive>:29:1: error:
---     • No instance for LabelOptic "age" ‘k’ ‘Human’ ‘b’ ‘a’ ‘[Char]’
---         (maybe you forgot to define it or misspelled a name?)
---     • When checking the inferred type
---         it :: forall k b a. ((TypeError ...), Is k A_Setter) => b
+-- >>> human2 & #pets .~ []
+-- Human2 {pets = []}
 --
--- λ> age = #age :: Iso' Human Int
+-- That's because an empty list doesn't have a type @[Pet]@, it has a type @[r]@
+-- and GHC doesn't have enough information to match on the instance we
+-- provided. We'd need to either annotate the list:
 --
--- <interactive>:7:7: error:
---     • No instance for LabelOptic "age" ‘An_Iso’ ‘Human’ ‘Human’ ‘Int’ ‘Int’
---         (maybe you forgot to define it or misspelled a name?)
---     • In the expression: #age :: Iso' Human Int
---       In an equation for ‘age’: age = #age :: Iso' Human Int
--- @
+-- >>> human1 & #pets .~ ([] :: [Pet])
+-- Human1 {pets = []}
 --
--- If we use the first form, error messages become more accurate:
+-- or the result type:
 --
--- @
--- λ> view #age peter :: Char
--- <interactive>:31:6: error:
---     • Couldn't match type ‘Char’ with ‘Integer’
---         arising from the overloaded label ‘#age’
---     • In the first argument of ‘view’, namely ‘#age’
---       In the expression: view #age peter :: Char
---       In an equation for ‘it’: it = view #age peter :: Char
--- λ> peter & set #age "hi"
+-- >>> human1 & #pets .~ [] :: Human1
+-- Human1 {pets = []}
 --
--- <interactive>:32:13: error:
---     • Couldn't match type ‘[Char]’ with ‘Integer’
---         arising from the overloaded label ‘#age’
---     • In the first argument of ‘set’, namely ‘#age’
---       In the second argument of ‘(&)’, namely ‘set #age "hi"’
---       In the expression: peter & set #age "hi"
--- λ> age = #age :: Iso' Human Int
+-- both of which are a nuisance.
 --
--- <interactive>:9:7: error:
---     • Couldn't match type ‘An_Iso’ with ‘A_Lens’
---         arising from the overloaded label ‘#age’
---     • In the expression: #age :: Iso' Human Int
---       In an equation for ‘age’: age = #age :: Iso' Human Int
--- @
+-- Here are more examples of confusing error messages if the instance for
+-- @LabelOptic "pets"@ is written without type equalities:
+--
+-- >>> human1 ^. #pets :: Char
+-- ...
+-- ...No instance for LabelOptic "pets" ‘A_Lens’ ‘Human1’ ‘Human1’ ‘Char’ ‘Char’
+-- ...
+--
+-- >>> human1 & #pets .~ 'x'
+-- ...
+-- ...No instance for LabelOptic "pets" ‘A_Lens’ ‘Human1’ ‘Human1’ ‘[Pet]’ ‘Char’
+-- ...
+--
+-- >>> let pets = #pets :: Iso' Human1 [Pet]
+-- ...
+-- ...No instance for LabelOptic "pets" ‘An_Iso’ ‘Human1’ ‘Human1’ ‘[Pet]’ ‘[Pet]’
+-- ...
+--
+-- If we use the second form, error messages become much more accurate:
+--
+-- >>> human2 ^. #pets :: Char
+-- ...
+-- ...Couldn't match type ‘Char’ with ‘[Pet]’
+-- ...  arising from the overloaded label ‘#pets’
+-- ...
+--
+-- >>> human2 & #pets .~ 'x'
+-- ...
+-- ...Couldn't match type ‘Char’ with ‘[Pet]’
+-- ...  arising from the overloaded label ‘#pets’
+-- ...
+--
+-- >>> let pets = #pets :: Iso' Human2 [Pet]
+-- ...
+-- ...Couldn't match type ‘An_Iso’ with ‘A_Lens’
+-- ...  arising from the overloaded label ‘#pets’
+-- ...
 
--- $fundepLimitations #limitations#
+-- $fundepExplanation
 --
 -- 'LabelOptic' uses the following functional dependencies to guarantee good
 -- type inference:
@@ -440,19 +466,142 @@
 -- 4. @name t a -> s@ (replacing the field @name@ in @t@ with @a@ yields @s@)
 --
 -- Dependencies (1) and (2) ensure that when we compose two optics, the middle
--- type is unambiguous. The consequence is that it's not possible to create
--- label optics with @a@ or @b@ referencing type variables not referenced in @s@
--- or @t@, i.e. getters for fields of rank 2 type or reviews for constructors
--- with existentially quantified types inside.
+-- type is unambiguous.
 --
 -- Dependencies (3) and (4) ensure that when we perform a chain of updates, the
--- middle type is unambiguous. The consequence is that it's not possible to
--- define label optics that:
+-- middle type is unambiguous.
+
+----------------------------------------
+-- Definitions
+
+-- | Support for overloaded labels as optics.
 --
--- - Modify phantom type parameters of type @s@ or @t@.
+-- An overloaded label @#foo@ can be used as an optic if there is an instance
+-- @'LabelOptic' "foo" k s t a b@.
 --
--- - Modify type parameters of type @s@ or @t@ if @a@ or @b@ contain ambiguous
---   applications of type families to these type parameters.
+-- Alternatively, if both @s@ and @t@ have a 'Generic' ('GenericLabelOptics' if
+-- @explicit-generic-labels@ flag is enabled) instance, a total field of @s@ is
+-- accessible by a label @#field@ of kind 'A_Lens', whereas its constructor by a
+-- label @#_Constructor@ of kind 'A_Prism'.
+class LabelOptic (name :: Symbol) k s t a b | name s -> k a
+                                            , name t -> k b
+                                            , name s b -> t
+                                            , name t a -> s where
+  -- | Used to interpret overloaded label syntax.  An overloaded label @#foo@
+  -- corresponds to @'labelOptic' \@"foo"@.
+  labelOptic :: Optic k NoIx s t a b
+
+-- | Type synonym for a type-preserving optic as overloaded label.
+type LabelOptic' name k s a = LabelOptic name k s s a a
+
+data Void0
+-- | If for an overloaded label @#label@ there is no instance starting with
+-- @LabelOptic "label"@ in scope, using it in the context of optics makes GHC
+-- immediately pick the overlappable instance defined below (since no other
+-- instance could match). If at this point GHC has no information about @s@ or
+-- @t@, it ends up picking incoherent instance of 'GenericLabelOptic' defined
+-- below. Prevent that (if only to be able to inspect most polymorphic types of
+-- @#foo % #bar@ or @view #foo@ in GHCi) by defining a dummy instance that
+-- matches all names, thus postponing instance resolution until @s@ or @t@ is
+-- known.
+instance
+  ( k ~ An_Iso, a ~ Void0, b ~ Void0
+  ) => LabelOptic name k Void0 Void0 a b where
+  labelOptic = Optic id
+
+-- | If no instance matches, try to use 'Generic' machinery for field access.
+--
+-- For more information have a look at 'Optics.Generic.gfield' and
+-- 'Optics.Generic.gconstructor'.
+--
+-- @since 0.4
+instance {-# OVERLAPPABLE #-}
+  ( GenericLabelOpticContext repDefined name k s t a b
+  ) => LabelOptic name k s t a b where
+  labelOptic = genericOptic @repDefined @name
+
+-- | Hide implementation from haddock.
+type GenericLabelOpticContext repDefined name k s t a b =
+  ( s `HasShapeOf` t
+  , t `HasShapeOf` s
+#ifdef EXPLICIT_GENERIC_LABELS
+  , repDefined ~ (HasGenericLabelOptics s && HasGenericLabelOptics t)
+#else
+  , repDefined ~ (Defined (Rep s) && Defined (Rep t))
+#endif
+  , Unless repDefined (NoLabelOpticError name k s t a b)
+  , k ~ If (CmpSymbol "_@" name == 'LT && CmpSymbol "_[" name == 'GT)
+           A_Prism
+           A_Lens
+  , GenericOptic repDefined name k s t a b
+  , Dysfunctional name k s t a b
+  )
+
+-- | If there is no specific 'LabelOptic' instance, display a custom type error.
+type family NoLabelOpticError name k s t a b where
+  NoLabelOpticError name k s t a b = TypeError
+    ('Text "No instance for LabelOptic " ':<>: 'ShowType name
+     ':<>: 'Text " " ':<>: QuoteType k
+     ':<>: 'Text " " ':<>: QuoteType s
+     ':<>: 'Text " " ':<>: QuoteType t
+     ':<>: 'Text " " ':<>: QuoteType a
+     ':<>: 'Text " " ':<>: QuoteType b
+     ':$$: 'Text "Possible solutions:"
+     ':$$: 'Text "- Check and correct spelling of the label"
+     ':$$: 'Text "- Define the LabelOptic instance by hand or via Template Haskell"
+#ifdef EXPLICIT_GENERIC_LABELS
+     ':$$: 'Text "- Derive a GenericLabelOptics instance for " ':<>: QuoteType s
+#else
+     ':$$: 'Text "- Derive a Generic instance for " ':<>: QuoteType s
+#endif
+    )
+
+----------------------------------------
+
+-- | If the @explicit-generic-labels@ Cabal flag is enabled, only types with
+-- this instance (which can be trivially derived with @DeriveAnyClass@
+-- extension) will be able to use labels as generic optics with a specific type.
+--
+-- It's an option for application developers to disable implicit fallback to
+-- generic optics for more control.
+--
+-- Libraries using generic labels with their data types should derive this
+-- instance for compatibility with the @explicit-generic-labels@ flag.
+--
+-- /Note:/ the flag @explicit-generic-labels@ is disabled by default. Enabling
+-- it is generally unsupported as it might lead to compilation errors of
+-- dependencies relying on implicit fallback to generic optics.
+--
+-- @since 0.4
+class Generic a => GenericLabelOptics a where
+  type HasGenericLabelOptics a :: Bool
+  type HasGenericLabelOptics a = 'True
+
+----------------------------------------
+
+class GenericOptic (repDefined :: Bool) name k s t a b where
+  genericOptic :: Optic k NoIx s t a b
+
+instance
+  ( -- We always let GHC enter the GFieldImpl instance because doing so doesn't
+    -- generate any additional error messages and we might get type improvements
+    -- from the HasField constraint to show in the error message.
+    GFieldImpl name s t a b
+  ) => GenericOptic repDefined name A_Lens s t a b where
+  genericOptic = gfieldImpl @name
+
+instance
+  ( GConstructorImpl repDefined name s t a b
+  , _name ~ AppendSymbol "_" name
+  ) => GenericOptic repDefined _name A_Prism s t a b where
+  genericOptic = gconstructorImpl @repDefined @name
+
+----------------------------------------
+
+instance
+  (LabelOptic name k s t a b, is ~ NoIx
+  ) => IsLabel name (Optic k is s t a b) where
+  fromLabel = labelOptic @name
 
 -- $setup
 -- >>> import Optics.Core
diff --git a/src/Optics/Lens.hs b/src/Optics/Lens.hs
--- a/src/Optics/Lens.hs
+++ b/src/Optics/Lens.hs
@@ -90,8 +90,9 @@
 
   -- * Additional introduction forms
   -- | See "Data.Tuple.Optics" for 'Lens'es for tuples.
+  --
+  -- If you're looking for 'Optics.IxLens.chosen', it was moved to "Optics.IxLens".
   , equality'
-  , chosen
   , alongside
   , united
 
@@ -192,11 +193,6 @@
 equality' :: Lens a b a b
 equality' = lensVL ($!)
 {-# INLINE equality' #-}
-
--- | Focus on both sides of an 'Either'.
-chosen :: Lens (Either a a) (Either b b) a b
-chosen = lensVL $ \f -> either (fmap Left . f) (fmap Right . f)
-{-# INLINE chosen #-}
 
 -- | Make a 'Lens' from two other lenses by executing them on their respective
 -- halves of a product.
diff --git a/src/Optics/Optic.hs b/src/Optics/Optic.hs
--- a/src/Optics/Optic.hs
+++ b/src/Optics/Optic.hs
@@ -31,7 +31,7 @@
   -- * Subtyping
   , castOptic
   , Is
-  , Join
+  , JoinKinds
 
   -- * Composition
   -- | The usual operator for composing optics is ('%'), which allows different
@@ -60,12 +60,12 @@
   , IxList
   , NoIx
   , WithIx
-  , Append
+  , AppendIndices
   , NonEmptyIndices
   , HasSingleIndex
   , AcceptsEmptyIndices
   , Curry
-  , CurryCompose
+  , CurryCompose(..)
 
     -- * Base re-exports
   , (&)
diff --git a/src/Optics/ReadOnly.hs b/src/Optics/ReadOnly.hs
--- a/src/Optics/ReadOnly.hs
+++ b/src/Optics/ReadOnly.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeInType #-}
 -- |
 -- Module: Optics.ReadOnly
 -- Description: Converting read-write optics into their read-only counterparts.
@@ -16,6 +18,7 @@
 
 -- | Class for read-write optics that have their read-only counterparts.
 class ToReadOnly k s t a b where
+  type ReadOnlyOptic k :: OpticKind
   -- | Turn read-write optic into its read-only counterpart (or leave read-only
   -- optics as-is).
   --
@@ -35,41 +38,50 @@
   --
   -- >>> :t view (getting fstIntToChar)
   -- view (getting fstIntToChar) :: (Int, r) -> Int
-  getting :: Optic k is s t a b -> Optic' (Join A_Getter k) is s a
+  getting :: Optic k is s t a b -> Optic' (ReadOnlyOptic k) is s a
 
 instance ToReadOnly An_Iso s t a b where
+  type ReadOnlyOptic An_Iso = A_Getter
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance ToReadOnly A_Lens s t a b where
+  type ReadOnlyOptic A_Lens = A_Getter
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance ToReadOnly A_Prism s t a b where
+  type ReadOnlyOptic A_Prism = An_AffineFold
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance ToReadOnly An_AffineTraversal s t a b where
+  type ReadOnlyOptic An_AffineTraversal = An_AffineFold
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance ToReadOnly A_Traversal s t a b where
+  type ReadOnlyOptic A_Traversal = A_Fold
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance ToReadOnly A_ReversedPrism s t a b where
+  type ReadOnlyOptic A_ReversedPrism = A_Getter
   getting o = Optic (getting__ o)
   {-# INLINE getting #-}
 
 instance (s ~ t, a ~ b) => ToReadOnly A_Getter s t a b where
+  type ReadOnlyOptic A_Getter = A_Getter
   getting = id
   {-# INLINE getting #-}
 
 instance (s ~ t, a ~ b) => ToReadOnly An_AffineFold s t a b where
+  type ReadOnlyOptic An_AffineFold = An_AffineFold
   getting = id
   {-# INLINE getting #-}
 
 instance (s ~ t, a ~ b) => ToReadOnly A_Fold s t a b where
+  type ReadOnlyOptic A_Fold = A_Fold
   getting = id
   {-# INLINE getting #-}
 
diff --git a/src/Optics/Traversal.hs b/src/Optics/Traversal.hs
--- a/src/Optics/Traversal.hs
+++ b/src/Optics/Traversal.hs
@@ -1,3 +1,7 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
 -- |
 -- Module: Optics.Traversal
 -- Description: Lifts an effectful operation on elements to act on structures.
@@ -46,6 +50,7 @@
 
   -- * Additional introduction forms
   , traversed
+  , both
 
   -- * Additional elimination forms
   , forOf
@@ -63,6 +68,22 @@
   , partsOf
   , singular
 
+  -- * Monoid structure
+  -- | 'Traversal' admits a (partial) monoid structure where 'adjoin' combines
+  -- non-overlapping traversals, and the identity element is
+  -- 'Optics.IxAffineTraversal.ignored' (which traverses no elements).
+  --
+  -- If you merely need a 'Fold', you can use traversals as folds and combine
+  -- them with one of the monoid structures on folds (see
+  -- "Optics.Fold#monoids"). In particular, 'summing' can be used to concatenate
+  -- results from two traversals, and 'failing' will returns results from the
+  -- second traversal only if the first returns no results.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'Traversal', because there
+  -- is not a unique choice of monoid to use that works for all optics, and the
+  -- ('<>') operator could not be used to combine optics of different kinds.
+  , adjoin
+
   -- * Subtyping
   , A_Traversal
   -- | <<diagrams/Traversal.png Traversal in the optics hierarchy>>
@@ -79,10 +100,10 @@
 import Control.Applicative
 import Control.Applicative.Backwards
 import Control.Monad.Trans.State
+import Data.Bitraversable
 import Data.Functor.Identity
 
 import Data.Profunctor.Indexed
-
 import Optics.AffineTraversal
 import Optics.Fold
 import Optics.Internal.Optic
@@ -274,6 +295,27 @@
 traversed = Optic traversed__
 {-# INLINE traversed #-}
 
+-- | Traverse both parts of a 'Bitraversable' container with matching types.
+--
+-- /Note:/ for traversing a pair or an 'Either' it's better to use
+-- 'Optics.Each.Core.each' and 'Optics.IxLens.chosen' respectively to reduce
+-- potential for bugs due to too much polymorphism.
+--
+-- >>> (1,2) & both %~ (*10)
+-- (10,20)
+--
+-- >>> over both length ("hello","world")
+-- (5,5)
+--
+-- >>> foldOf both ("hello","world")
+-- "helloworld"
+--
+-- @since 0.4
+--
+both :: Bitraversable r => Traversal (r a a) (r b b) a b
+both = traversalVL $ \f -> bitraverse f f
+{-# INLINE both #-}
+
 ----------------------------------------
 -- Traversal combinators
 
@@ -342,6 +384,119 @@
       Just a' -> put Nothing >> pure a'
       Nothing ->                pure a
 {-# INLINE singular #-}
+
+-- | Combine two disjoint traversals into one.
+--
+-- >>> over (_1 % _Just `adjoin` _2 % _Right) not (Just True, Right False)
+-- (Just False,Right True)
+--
+-- /Note:/ if the argument traversals are not disjoint, the result will not
+-- respect the 'Traversal' laws, because it will visit the same element multiple
+-- times.  See section 7 of
+-- <https://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf Understanding Idiomatic Traversals Backwards and Forwards>
+-- by Bird et al. for why this is illegal.
+--
+-- >>> view (partsOf (each `adjoin` _1)) ('x','y')
+-- "xyx"
+-- >>> set (partsOf (each `adjoin` _1)) "abc" ('x','y')
+-- ('c','b')
+--
+-- For the 'Fold' version see 'Optics.Fold.summing'.
+--
+-- @since 0.4
+--
+adjoin
+  :: (Is k A_Traversal, Is l A_Traversal)
+  => Optic' k is s a
+  -> Optic' l js s a
+  -> Traversal' s a
+adjoin o1 o2 = combined % traversed
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+         in s2
+      )
+      <$> f (toListOf (castOptic @A_Traversal o1) s0)
+      <*> f (toListOf (castOptic @A_Traversal o2) s0)
+
+    update a = get >>= \case
+      a' : as' -> put as' >> pure a'
+      []       ->            pure a
+infixr 6 `adjoin` -- Same as (<>)
+{-# INLINE [1] adjoin #-}
+
+{-# RULES
+
+"adjoin_12_3" forall o1 o2 o3. adjoin o1 (adjoin o2 o3) = adjoin3 o1 o2 o3
+"adjoin_21_3" forall o1 o2 o3. adjoin (adjoin o1 o2) o3 = adjoin3 o1 o2 o3
+
+"adjoin_13_4" forall o1 o2 o3 o4. adjoin o1 (adjoin3 o2 o3 o4) = adjoin4 o1 o2 o3 o4
+"adjoin_31_4" forall o1 o2 o3 o4. adjoin (adjoin3 o1 o2 o3) o4 = adjoin4 o1 o2 o3 o4
+
+#-}
+
+-- | Triple 'adjoin' for optimizing multiple 'adjoin's with rewrite rules.
+adjoin3
+  :: (Is k1 A_Traversal, Is k2 A_Traversal, Is k3 A_Traversal)
+  => Optic' k1 is1 s a
+  -> Optic' k2 is2 s a
+  -> Optic' k3 is3 s a
+  -> Traversal' s a
+adjoin3 o1 o2 o3 = combined % traversed
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 r3 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+             s3 = evalState (traverseOf o3 update s2) r3
+         in s3
+      )
+      <$> f (toListOf (castOptic @A_Traversal o1) s0)
+      <*> f (toListOf (castOptic @A_Traversal o2) s0)
+      <*> f (toListOf (castOptic @A_Traversal o3) s0)
+
+    update a = get >>= \case
+      a' : as' -> put as' >> pure a'
+      []       ->            pure a
+{-# INLINE [1] adjoin3 #-}
+
+{-# RULES
+
+"adjoin_211_4" forall o1 o2 o3 o4. adjoin3 (adjoin o1 o2) o3 o4 = adjoin4 o1 o2 o3 o4
+"adjoin_121_4" forall o1 o2 o3 o4. adjoin3 o1 (adjoin o2 o3) o4 = adjoin4 o1 o2 o3 o4
+"adjoin_112_4" forall o1 o2 o3 o4. adjoin3 o1 o2 (adjoin o3 o4) = adjoin4 o1 o2 o3 o4
+
+#-}
+
+-- | Quadruple 'adjoin' for optimizing multiple 'adjoin's with rewrite rules.
+adjoin4
+  :: (Is k1 A_Traversal, Is k2 A_Traversal, Is k3 A_Traversal, Is k4 A_Traversal)
+  => Optic' k1 is1 s a
+  -> Optic' k2 is2 s a
+  -> Optic' k3 is3 s a
+  -> Optic' k4 is4 s a
+  -> Traversal' s a
+adjoin4 o1 o2 o3 o4 = combined % traversed
+  where
+    combined = traversalVL $ \f s0 ->
+      (\r1 r2 r3 r4 ->
+         let s1 = evalState (traverseOf o1 update s0) r1
+             s2 = evalState (traverseOf o2 update s1) r2
+             s3 = evalState (traverseOf o3 update s2) r3
+             s4 = evalState (traverseOf o4 update s3) r4
+         in s4
+      )
+      <$> f (toListOf (castOptic @A_Traversal o1) s0)
+      <*> f (toListOf (castOptic @A_Traversal o2) s0)
+      <*> f (toListOf (castOptic @A_Traversal o3) s0)
+      <*> f (toListOf (castOptic @A_Traversal o4) s0)
+
+    update a = get >>= \case
+      a' : as' -> put as' >> pure a'
+      []       ->            pure a
+{-# INLINE [1] adjoin4 #-}
 
 -- $setup
 -- >>> import Data.List