diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,26 @@
+# optics-core-0.3 (2020-04-15)
+* GHC-8.10 support
+* Add `filteredBy` and `unsafeFilteredBy`
+* Add `FunctorWithIndex`, `FoldableWithIndex` and `TraversableWithIndex`
+  instances for `Const` and `Constant`
+* Add `afoldVL` and `iafoldVL` constructors
+* Rename `toAtraversalVL` to `atraverseOf`, and `toIxAtraversalVL` to `iatraverseOf`
+* Generalise `element` and `elementOf` to construct `IxAffineTraversal`s
+  instead of `IxTraversal`s
+* Change `mapping` to work on optic kinds other than `Iso`: it now supports
+  `Lens` and `Prism` degenerating to `Getter` and `Review` respectively
+* Generalise `ignored` to be an `IxAffineTraversal` instead of an `IxTraversal`
+* Add `singular` and `isingular`
+* Add `(^?!)` operator
+* Expose `Curry` and `CurryCompose`
+* Show expected elimination forms on optic kind mismatch
+* Use stricter `uncurry'` for better performance
+* Add hidden `LabelOptic` instance to postpone instance resolution
+* Add `GeneralLabelOptic` for pluggable generic optics as labels
+* Document monoidal structures of `Fold`s
+* Remove proxy argument from `implies`
+* Add `itoList`
+
 # optics-core-0.2 (2019-10-18)
 * Add `non`, `non'` and `anon` to `Optics.Iso`
 * `ix` can produce optic kinds other than `AffineTraversal`
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.2
+version:       0.3
 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.1, GHCJS ==8.4
+tested-with:   GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.3 || ==8.10.1, GHCJS ==8.4
 synopsis:      Optics as an abstract interface: core definitions
 category:      Data, Optics, Lenses
 description:
@@ -72,8 +72,10 @@
                    Optics.Each.Core
                    Optics.Empty.Core
                    Optics.Indexed.Core
+                   Optics.Mapping
                    Optics.Label
                    Optics.Operators
+                   Optics.Operators.Unsafe
                    Optics.Re
                    Optics.ReadOnly
 
@@ -96,6 +98,7 @@
                    Optics.Internal.Bi
                    Optics.Internal.Fold
                    Optics.Internal.Indexed
+                   Optics.Internal.Indexed.Classes
                    Optics.Internal.IxFold
                    Optics.Internal.IxSetter
                    Optics.Internal.IxTraversal
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
@@ -51,7 +51,7 @@
 
 -- | Construct a map from an 'IxFold'.
 --
--- The construction is left-biased (see 'IntMap.union'), i.e. the first occurences of
+-- The construction is left-biased (see 'IntMap.union'), i.e. the first occurrences of
 -- keys in the fold or traversal order are preferred.
 --
 -- >>> toMapOf ifolded ["hello", "world"]
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
@@ -59,7 +59,7 @@
 -- | Construct a map from an 'IxFold'.
 --
 -- The construction is left-biased (see 'Map.union'), i.e. the first
--- occurences of keys in the fold or traversal order are preferred.
+-- occurrences of keys in the fold or traversal order are preferred.
 --
 -- >>> toMapOf ifolded ["hello", "world"]
 -- fromList [(0,"hello"),(1,"world")]
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
@@ -43,6 +43,7 @@
 
 import Data.Functor.Identity
 import Data.Functor.Product
+import Data.Kind
 import Data.Proxy
 import GHC.Generics ((:*:)(..), Generic(..), K1, M1, U1)
 
@@ -404,7 +405,7 @@
 {-# INLINE ix #-}
 
 -- TODO: this can be replaced by generic-optics position
-type family GSize (f :: * -> *)
+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
diff --git a/src/Optics/AffineFold.hs b/src/Optics/AffineFold.hs
--- a/src/Optics/AffineFold.hs
+++ b/src/Optics/AffineFold.hs
@@ -26,12 +26,26 @@
   -- @
 
   -- * Additional introduction forms
+  , afoldVL
   , filtered
 
   -- * Additional elimination forms
+  , atraverseOf_
   , isn't
 
-    -- * Semigroup structure
+  -- * Monoid structure
+  -- | 'AffineFold' admits a monoid structure where 'afailing' combines folds
+  -- (returning a result from the second fold only if the first returns none)
+  -- and the identity element is 'Optics.IxAffineTraversal.ignored' (which
+  -- returns no results).
+  --
+  -- /Note:/ There is no 'Optics.Fold.summing' equivalent that returns an
+  -- 'AffineFold', because it would not need to return more than one result.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'AffineFold', 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.
   , afailing
 
   -- * Subtyping
@@ -49,6 +63,20 @@
 -- | Type synonym for an affine fold.
 type AffineFold s a = Optic' An_AffineFold NoIx s a
 
+-- | Obtain an 'AffineFold' by lifting 'traverse_' like function.
+--
+-- @
+-- 'afoldVL' '.' 'atraverseOf_' ≡ 'id'
+-- 'atraverseOf_' '.' 'afoldVL' ≡ 'id'
+-- @
+--
+-- @since 0.3
+afoldVL
+  :: (forall f. Functor f => (forall r. r -> f r) -> (a -> f u) -> s -> f v)
+  -> AffineFold s a
+afoldVL f = Optic (rphantom . visit f . rphantom)
+{-# INLINE afoldVL #-}
+
 -- | Retrieve the value targeted by an 'AffineFold'.
 --
 -- >>> let _Right = prism Right $ either (Left . Left) Right
@@ -69,6 +97,19 @@
   getOptic (castOptic @An_AffineFold o) $ ForgetM (Just . f)
 {-# INLINE previews #-}
 
+-- | Traverse over the target of an 'AffineFold', computing a 'Functor'-based
+-- answer, but unlike 'Optics.AffineTraversal.atraverseOf' do not construct a
+-- new structure.
+--
+-- @since 0.3
+atraverseOf_
+  :: (Is k An_AffineFold, Functor f)
+  => Optic' k is s a
+  -> (forall r. r -> f r) -> (a -> f u) -> s -> f ()
+atraverseOf_ o point f s = case preview o s of
+  Just a  -> () <$ f a
+  Nothing -> point ()
+
 -- | Create an 'AffineFold' from a partial function.
 --
 -- >>> preview (afolding listToMaybe) "foo"
@@ -80,7 +121,7 @@
 
 -- | Filter result(s) of a fold that don't satisfy a predicate.
 filtered :: (a -> Bool) -> AffineFold a a
-filtered p = Optic (visit (\point f a -> if p a then f a else point a))
+filtered p = afoldVL (\point f a -> if p a then f a else point a)
 {-# INLINE filtered #-}
 
 -- | Try the first 'AffineFold'. If it returns no entry, try the second one.
@@ -90,8 +131,6 @@
 --
 -- >>> preview (ix 42 % re _Left `afailing` ix 2 % re _Right) [0,1,2,3]
 -- Just (Right 2)
---
--- /Note:/ There is no 'Optics.Fold.summing' equivalent, because @asumming = afailing@.
 --
 afailing
   :: (Is k An_AffineFold, Is l An_AffineFold)
diff --git a/src/Optics/AffineTraversal.hs b/src/Optics/AffineTraversal.hs
--- a/src/Optics/AffineTraversal.hs
+++ b/src/Optics/AffineTraversal.hs
@@ -56,7 +56,7 @@
   , AffineTraversalVL
   , AffineTraversalVL'
   , atraversalVL
-  , toAtraversalVL
+  , atraverseOf
   )
   where
 
@@ -143,14 +143,17 @@
 atraversalVL f = Optic (visit f)
 {-# INLINE atraversalVL #-}
 
--- | Convert an affine traversal to its van Laarhoven representation.
-toAtraversalVL
-  :: Is k An_AffineTraversal
+-- | Traverse over the target of an 'AffineTraversal' and compute a
+-- 'Functor'-based answer.
+--
+-- @since 0.3
+atraverseOf
+  :: (Is k An_AffineTraversal, Functor f)
   => Optic k is s t a b
-  -> AffineTraversalVL s t a b
-toAtraversalVL o point =
+  -> (forall r. r -> f r) -> (a -> f b) -> s -> f t
+atraverseOf o point =
   runStarA . getOptic (castOptic @An_AffineTraversal o) . StarA point
-{-# INLINE toAtraversalVL #-}
+{-# INLINE atraverseOf #-}
 
 -- | Retrieve the value targeted by an 'AffineTraversal' or return the original
 -- value while allowing the type to change if it does not match.
diff --git a/src/Optics/Arrow.hs b/src/Optics/Arrow.hs
--- a/src/Optics/Arrow.hs
+++ b/src/Optics/Arrow.hs
@@ -16,6 +16,7 @@
 import Optics.Prism
 import Optics.Setter
 import Optics.Internal.Optic
+import Optics.Internal.Utils
 
 newtype WrappedArrow p i a b = WrapArrow { unwrapArrow :: p a b }
 
@@ -105,7 +106,7 @@
   :: (Is k A_Setter, Arrow arr)
   => Optic k is s t a b
   -> arr s b -> arr s t
-assignA o p = arr (flip $ set o) &&& p >>> arr (uncurry id)
+assignA o p = arr (flip $ set o) &&& p >>> arr (uncurry' id)
 {-# INLINE assignA #-}
 
 ----------------------------------------
diff --git a/src/Optics/Cons/Core.hs b/src/Optics/Cons/Core.hs
--- a/src/Optics/Cons/Core.hs
+++ b/src/Optics/Cons/Core.hs
@@ -38,6 +38,7 @@
 import Optics.AffineFold
 import Optics.AffineTraversal
 import Optics.Coerce
+import Optics.Internal.Utils
 import Optics.Optic
 import Optics.Prism
 import Optics.Review
@@ -86,7 +87,7 @@
   _Cons :: Prism s t (a, s) (b, t)
 
 instance Cons [a] [b] a b where
-  _Cons = prism (uncurry (:)) $ \ aas -> case aas of
+  _Cons = prism (uncurry' (:)) $ \aas -> case aas of
     (a:as) -> Right (a, as)
     []     -> Left  []
   {-# INLINE _Cons #-}
@@ -100,7 +101,7 @@
   {-# INLINE _Cons #-}
 
 instance Cons (Seq a) (Seq b) a b where
-  _Cons = prism (uncurry (Seq.<|)) $ \aas -> case viewl aas of
+  _Cons = prism (uncurry' (Seq.<|)) $ \aas -> case viewl aas of
     a Seq.:< as -> Right (a, as)
     EmptyL  -> Left mempty
   {-# INLINE _Cons #-}
@@ -238,7 +239,7 @@
   {-# INLINE _Snoc #-}
 
 instance Snoc (Seq a) (Seq b) a b where
-  _Snoc = prism (uncurry (Seq.|>)) $ \aas -> case viewr aas of
+  _Snoc = prism (uncurry' (Seq.|>)) $ \aas -> case viewr aas of
     as Seq.:> a -> Right (as, a)
     EmptyR  -> Left mempty
   {-# INLINE _Snoc #-}
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.Mapping                          as P
 import Optics.Operators                        as P
 import Optics.Re                               as P
 import Optics.ReadOnly                         as P
diff --git a/src/Optics/Fold.hs b/src/Optics/Fold.hs
--- a/src/Optics/Fold.hs
+++ b/src/Optics/Fold.hs
@@ -75,7 +75,21 @@
   , pre
   , backwards_
 
-  -- * Semigroup structure
+  -- * Monoid structures
+  -- | 'Fold' admits (at least) two monoid structures: #monoids#
+  --
+  -- * 'summing' concatenates results from both folds.
+  --
+  -- * 'failing' returns results from the second fold only if the first returns
+  --   no results.
+  --
+  -- In both cases, the identity element of the monoid is
+  -- `Optics.IxAffineTraversal.ignored`, which returns no results.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'Fold', because there is
+  -- not a unique choice of monoid to use, and the ('<>') operator could not be
+  -- used to combine optics of different kinds.  When porting code from @lens@
+  -- that uses '<>' to combine folds, use 'summing' instead.
   , summing
   , failing
 
@@ -136,6 +150,9 @@
 {-# INLINE foldlOf' #-}
 
 -- | Fold to a list.
+--
+-- >>> toListOf (_1 % folded % _Right) ([Right 'h', Left 5, Right 'i'], "bye")
+-- "hi"
 toListOf :: Is k A_Fold => Optic' k is s a -> s -> [a]
 toListOf o = foldrOf o (:) []
 {-# INLINE toListOf #-}
@@ -231,6 +248,8 @@
 
 -- | Convert a fold to an 'AffineFold' that visits the first element of the
 -- original fold.
+--
+-- For the traversal version see 'Optics.Traversal.singular'.
 pre :: Is k A_Fold => Optic' k is s a -> AffineFold s a
 pre = afolding . headOf
 {-# INLINE pre #-}
@@ -258,6 +277,12 @@
 {-# INLINE summing #-}
 
 -- | Try the first 'Fold'. If it returns no entries, try the second one.
+--
+-- >>> toListOf (ix 1 `failing` ix 0) [4,7]
+-- [7]
+-- >>> toListOf (ix 1 `failing` ix 0) [4]
+-- [4]
+--
 failing
   :: (Is k A_Fold, Is l A_Fold)
   => Optic' k is s a
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
@@ -41,6 +41,7 @@
   , FoldableWithIndex (..)
   , itraverse_
   , ifor_
+  , itoList
   -- ** Traversable with index
   , TraversableWithIndex (..)
   , ifor
@@ -49,6 +50,7 @@
 import Data.Profunctor.Indexed
 
 import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.Optic
 
 import Optics.AffineFold
@@ -197,7 +199,7 @@
   {-# INLINE noIx #-}
 
 instance IxOptic An_AffineTraversal s t a b where
-  noIx o = atraversalVL (toAtraversalVL o)
+  noIx o = atraversalVL (atraverseOf o)
   {-# INLINE noIx #-}
 
 instance (s ~ t, a ~ b) => IxOptic An_AffineFold s t a b where
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
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -10,33 +9,11 @@
 -- in subsequent releases.
 module Optics.Internal.Indexed where
 
-import Control.Applicative
-import Control.Applicative.Backwards
-import Control.Monad.Trans.Identity
-import Control.Monad.Trans.Reader
-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.Kind (Type)
-import Data.List.NonEmpty
-import Data.Monoid hiding (Product, Sum)
-import Data.Proxy
-import Data.Tree
-import Data.Void
-import GHC.Generics
 import GHC.TypeLits
-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 Data.Profunctor.Indexed
-
 import Optics.Internal.Optic
-import Optics.Internal.Utils
 
 -- | Show useful error message when a function expects optics without indices.
 class is ~ NoIx => AcceptsEmptyIndices (f :: Symbol) (is :: IxList)
@@ -166,447 +143,3 @@
   -> Optic k is   s t a b
 conjoined (Optic f) (Optic g) = Optic (conjoined__ f g)
 {-# INLINE conjoined #-}
-
-----------------------------------------
-
--- | 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 = runIxFunArrow (iwander itraverse (IxFunArrow f)) id
-  {-# 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 = runIxForget (iwander itraverse (IxForget f)) id
-  {-# 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_ #-}
-
--- | 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 #-}
-
--- (,) 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 #-}
-
-instance TraversableWithIndex Void (K1 i c) where
-  itraverse _ (K1 a) = pure (K1 a)
-  {-# INLINE itraverse #-}
diff --git a/src/Optics/Internal/Indexed/Classes.hs b/src/Optics/Internal/Indexed/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Internal/Indexed/Classes.hs
@@ -0,0 +1,514 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+-- | Internal implementation details of indexed optics.
+--
+-- 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 #-}
+
+instance TraversableWithIndex Void (K1 i c) where
+  itraverse _ (K1 a) = pure (K1 a)
+  {-# INLINE itraverse #-}
diff --git a/src/Optics/Internal/IxFold.hs b/src/Optics/Internal/IxFold.hs
--- a/src/Optics/Internal/IxFold.hs
+++ b/src/Optics/Internal/IxFold.hs
@@ -12,7 +12,7 @@
 import Data.Profunctor.Indexed
 
 import Optics.Internal.Bi
-import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.Optic
 import Optics.Internal.Fold
 
diff --git a/src/Optics/Internal/IxSetter.hs b/src/Optics/Internal/IxSetter.hs
--- a/src/Optics/Internal/IxSetter.hs
+++ b/src/Optics/Internal/IxSetter.hs
@@ -8,7 +8,7 @@
 
 import Data.Profunctor.Indexed
 
-import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.Optic
 
 -- | Internal implementation of 'Optics.IxSetter.imapped'.
diff --git a/src/Optics/Internal/IxTraversal.hs b/src/Optics/Internal/IxTraversal.hs
--- a/src/Optics/Internal/IxTraversal.hs
+++ b/src/Optics/Internal/IxTraversal.hs
@@ -9,7 +9,7 @@
 import Data.Profunctor.Indexed
 
 import Optics.Internal.Fold
-import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.IxFold
 import Optics.Internal.IxSetter
 import Optics.Internal.Optic
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
@@ -26,10 +26,10 @@
   , (%)
   , (%%)
   , (%&)
-  , IsProxy(..)
   -- * Labels
   , LabelOptic(..)
   , LabelOptic'
+  , GeneralLabelOptic(..)
   -- * Re-exports
   , module Optics.Internal.Optic.Subtyping
   , module Optics.Internal.Optic.Types
@@ -40,6 +40,7 @@
 import Data.Kind (Type)
 import Data.Proxy (Proxy (..))
 import Data.Type.Equality
+import GHC.Generics (Rep)
 import GHC.OverloadedLabels
 import GHC.TypeLits
 
@@ -87,11 +88,6 @@
 -- | Optic internally as a profunctor transformation.
 type Optic__ p i j s t a b = p i a b -> p j s t
 
--- | Proxy type for use as an argument to 'implies'.
---
-data IsProxy (k :: Type) (l :: Type) (p :: Type -> Type -> Type -> Type) =
-  IsProxy
-
 -- | Explicit cast from one optic flavour to another.
 --
 -- The resulting optic kind is given in the first type argument, so you can use
@@ -110,13 +106,13 @@
   .  Is srcKind destKind
   => Optic srcKind  is s t a b
   -> Optic destKind is s t a b
-castOptic (Optic o) = Optic (implies' o)
+castOptic (Optic o) = Optic (cast o)
   where
-    implies'
+    cast
       :: forall p i
       .  Optic_ srcKind  p i (Curry is i) s t a b
       -> Optic_ destKind p i (Curry is i) s t a b
-    implies' x = implies (IsProxy :: IsProxy srcKind destKind p) x
+    cast x = implies @srcKind @destKind @p x
 {-# INLINE castOptic #-}
 
 -- | Compose two optics of compatible flavours.
@@ -145,11 +141,13 @@
 Optic o %% Optic o' = Optic oo
   where
     -- unsafeCoerce to the rescue, for a proof see below.
-    oo :: forall p i. Profunctor p => Optic_ k p i (Curry ks i) s t a b
+    oo :: forall p i. (Profunctor p, Constraints k p) => Optic__ p i (Curry ks i) s t a b
     oo = (unsafeCoerce
-           :: Optic_ k p i (Curry is (Curry js i)) s t a b
-           -> Optic_ k p i (Curry ks i           ) s t a b)
-      (o . o')
+           :: 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 (%%) #-}
 
 -- | Flipped function application, specialised to optics and binding tightly.
@@ -210,13 +208,48 @@
   -- 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
--- overlappable instance providing a custom type error to cut its efforts short.
-instance {-# OVERLAPPABLE #-}
-  (LabelOptic name k s t a b,
-   TypeError
+-- 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
@@ -224,11 +257,8 @@
     ':<>: 'Text " " ':<>: QuoteType a
     ':<>: 'Text " " ':<>: QuoteType b
     ':$$: 'Text "  (maybe you forgot to define it or misspelled a name?)")
-  ) => LabelOptic name k s t a b where
-  labelOptic = error "unreachable"
-
--- | Type synonym for a type-preserving optic as overloaded label.
-type LabelOptic' name k s a = LabelOptic name k s s a a
+   => GeneralLabelOptic name k s t a b repDefined where
+  generalLabelOptic = error "unreachable"
 
 instance
   (LabelOptic name k s t a b, is ~ NoIx
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
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -11,6 +12,7 @@
 
 import GHC.TypeLits (ErrorMessage(..), TypeError)
 
+import Optics.Internal.Optic.TypeLevel
 import Optics.Internal.Optic.Types
 
 -- | Subtyping relationship between kinds of optics.
@@ -23,69 +25,121 @@
 --
 class Is k l where
   -- | Witness of the subtyping relationship.
-  implies ::
-    proxy k l p -> (Constraints k p => r) -> (Constraints l p => r)
-
--- | Overlappable instance for a custom type error.
-instance {-# OVERLAPPABLE #-} TypeError ('ShowType k
-                                         ':<>: 'Text " cannot be used as "
-                                         ':<>: 'ShowType l
-                                        ) => Is k l where
-  implies = error "unreachable"
+  implies :: (Constraints k p => r) -> (Constraints l p => r)
 
 -- | Every kind of optic can be used as itself.
 instance Is k k where
-  implies _ = id
+  implies r = r
 
+-- | Overlappable instance for a custom type error.
+instance {-# OVERLAPPABLE #-} TypeError
+  ('ShowType k ':<>: 'Text " cannot be used as " ':<>: 'ShowType l
+   ':$$: 'Text "Perhaps you meant one of these:"
+   ':$$: ShowEliminations (EliminationForms k)
+  ) => Is k l where
+  implies _ = error "unreachable"
+
+type family EliminationForms (k :: OpticKind) where
+  EliminationForms An_AffineFold      = AffineFoldEliminations
+  EliminationForms An_AffineTraversal = AffineTraversalEliminations
+  EliminationForms A_Fold             = FoldEliminations
+  EliminationForms A_Getter           = GetterEliminations
+  EliminationForms An_Iso             = IsoEliminations
+  EliminationForms A_Lens             = LensEliminations
+  EliminationForms A_Prism            = PrismEliminations
+  EliminationForms A_ReversedLens     = ReviewEliminations
+  EliminationForms A_ReversedPrism    = GetterEliminations
+  EliminationForms A_Review           = ReviewEliminations
+  EliminationForms A_Setter           = SetterEliminations
+  EliminationForms A_Traversal        = TraversalEliminations
+
+type AffineFoldEliminations = '( '[ '("preview", "Optics.AffineFold") ]
+                               , '[ "(^?)" ])
+
+type AffineTraversalEliminations = AffineFoldEliminations
+              `AppendEliminations` SetterEliminations
+
+type FoldEliminations = '( '[ '("traverseOf_", "Optics.Fold")
+                            , '("foldMapOf",   "Optics.Fold")
+                            , '("toListOf",    "Optics.Fold")
+                            ]
+                         , '[ "(^..)" ])
+
+type GetterEliminations = '( '[ '("view", "Optics.Getter") ]
+                           , '[ "(^.)" ])
+
+type IsoEliminations = GetterEliminations
+  `AppendEliminations` ReviewEliminations
+  `AppendEliminations` SetterEliminations
+
+type LensEliminations = GetterEliminations
+   `AppendEliminations` SetterEliminations
+
+type PrismEliminations = AffineFoldEliminations
+    `AppendEliminations` ReviewEliminations
+    `AppendEliminations` SetterEliminations
+
+type ReviewEliminations = '( '[ '("review", "Optics.Review") ]
+                           , '[ "(#)" ])
+
+type SetterEliminations = '( '[ '("over", "Optics.Setter")
+                              , '("set",  "Optics.Setter")
+                              ]
+                           , '[ "(%~)", "(.~)" ])
+
+type TraversalEliminations = '( '[ '("traverseOf", "Optics.Traversal") ]
+                              , '[]) `AppendEliminations` FoldEliminations
+                                     `AppendEliminations` SetterEliminations
+
 ----------------------------------------
 
 -- BEGIN GENERATED CONTENT
 
 -- An_Iso
-instance Is An_Iso             A_ReversedLens     where implies _ = id
-instance Is An_Iso             A_ReversedPrism    where implies _ = id
-instance Is An_Iso             A_Prism            where implies _ = id
-instance Is An_Iso             A_Review           where implies _ = id
-instance Is An_Iso             A_Lens             where implies _ = id
-instance Is An_Iso             A_Getter           where implies _ = id
-instance Is An_Iso             An_AffineTraversal where implies _ = id
-instance Is An_Iso             An_AffineFold      where implies _ = id
-instance Is An_Iso             A_Traversal        where implies _ = id
-instance Is An_Iso             A_Fold             where implies _ = id
-instance Is An_Iso             A_Setter           where implies _ = id
+instance Is An_Iso             A_ReversedLens     where implies r = r
+instance Is An_Iso             A_ReversedPrism    where implies r = r
+instance Is An_Iso             A_Prism            where implies r = r
+instance Is An_Iso             A_Review           where implies r = r
+instance Is An_Iso             A_Lens             where implies r = r
+instance Is An_Iso             A_Getter           where implies r = r
+instance Is An_Iso             An_AffineTraversal where implies r = r
+instance Is An_Iso             An_AffineFold      where implies r = r
+instance Is An_Iso             A_Traversal        where implies r = r
+instance Is An_Iso             A_Fold             where implies r = r
+instance Is An_Iso             A_Setter           where implies r = r
 -- A_ReversedLens
-instance Is A_ReversedLens     A_Review           where implies _ = id
+instance Is A_ReversedLens     A_Review           where implies r = r
 -- A_ReversedPrism
-instance Is A_ReversedPrism    A_Getter           where implies _ = id
-instance Is A_ReversedPrism    An_AffineFold      where implies _ = id
-instance Is A_ReversedPrism    A_Fold             where implies _ = id
+instance Is A_ReversedPrism    A_Getter           where implies r = r
+instance Is A_ReversedPrism    An_AffineFold      where implies r = r
+instance Is A_ReversedPrism    A_Fold             where implies r = r
 -- A_Prism
-instance Is A_Prism            A_Review           where implies _ = id
-instance Is A_Prism            An_AffineTraversal where implies _ = id
-instance Is A_Prism            An_AffineFold      where implies _ = id
-instance Is A_Prism            A_Traversal        where implies _ = id
-instance Is A_Prism            A_Fold             where implies _ = id
-instance Is A_Prism            A_Setter           where implies _ = id
+instance Is A_Prism            A_Review           where implies r = r
+instance Is A_Prism            An_AffineTraversal where implies r = r
+instance Is A_Prism            An_AffineFold      where implies r = r
+instance Is A_Prism            A_Traversal        where implies r = r
+instance Is A_Prism            A_Fold             where implies r = r
+instance Is A_Prism            A_Setter           where implies r = r
 -- A_Lens
-instance Is A_Lens             A_Getter           where implies _ = id
-instance Is A_Lens             An_AffineTraversal where implies _ = id
-instance Is A_Lens             An_AffineFold      where implies _ = id
-instance Is A_Lens             A_Traversal        where implies _ = id
-instance Is A_Lens             A_Fold             where implies _ = id
-instance Is A_Lens             A_Setter           where implies _ = id
+instance Is A_Lens             A_Getter           where implies r = r
+instance Is A_Lens             An_AffineTraversal where implies r = r
+instance Is A_Lens             An_AffineFold      where implies r = r
+instance Is A_Lens             A_Traversal        where implies r = r
+instance Is A_Lens             A_Fold             where implies r = r
+instance Is A_Lens             A_Setter           where implies r = r
 -- A_Getter
-instance Is A_Getter           An_AffineFold      where implies _ = id
-instance Is A_Getter           A_Fold             where implies _ = id
+instance Is A_Getter           An_AffineFold      where implies r = r
+instance Is A_Getter           A_Fold             where implies r = r
 -- An_AffineTraversal
-instance Is An_AffineTraversal An_AffineFold      where implies _ = id
-instance Is An_AffineTraversal A_Traversal        where implies _ = id
-instance Is An_AffineTraversal A_Fold             where implies _ = id
-instance Is An_AffineTraversal A_Setter           where implies _ = id
+instance Is An_AffineTraversal An_AffineFold      where implies r = r
+instance Is An_AffineTraversal A_Traversal        where implies r = r
+instance Is An_AffineTraversal A_Fold             where implies r = r
+instance Is An_AffineTraversal A_Setter           where implies r = r
 -- An_AffineFold
-instance Is An_AffineFold      A_Fold             where implies _ = id
+instance Is An_AffineFold      A_Fold             where implies r = r
 -- A_Traversal
-instance Is A_Traversal        A_Fold             where implies _ = id
-instance Is A_Traversal        A_Setter           where implies _ = id
+instance Is A_Traversal        A_Fold             where implies r = r
+instance Is A_Traversal        A_Setter           where implies r = r
 
 -- END GENERATED CONTENT
 
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
@@ -25,6 +25,50 @@
 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
+
+type family ShowSymbolWithOrigin symbol origin :: ErrorMessage where
+  ShowSymbolWithOrigin symbol origin = 'Text "  "
+                                 ':<>: QuoteSymbol symbol
+                                 ':<>: 'Text " (from "
+                                 ':<>: 'Text origin
+                                 ':<>: 'Text ")"
+
+type family ShowSymbolsWithOrigin (fs :: [(Symbol, Symbol)]) :: ErrorMessage where
+  ShowSymbolsWithOrigin '[ '(symbol, origin) ] =
+    ShowSymbolWithOrigin symbol origin
+  ShowSymbolsWithOrigin ('(symbol, origin) ': rest) =
+    ShowSymbolWithOrigin symbol origin ':$$: ShowSymbolsWithOrigin rest
+
+type family ShowOperators (ops :: [Symbol]) :: ErrorMessage where
+  ShowOperators '[op] =
+    QuoteSymbol op ':<>: 'Text " (from Optics.Operators)"
+  ShowOperators (op ': rest) =
+    QuoteSymbol op ':<>: 'Text " " ':<>: ShowOperators rest
+
+type family AppendEliminations a b where
+  AppendEliminations '(fs1, ops1) '(fs2, ops2) =
+    '(Append fs1 fs2, Append ops1 ops2)
+
+type family ShowEliminations forms :: ErrorMessage where
+  ShowEliminations '(fs, ops) =
+    ShowSymbolsWithOrigin fs ':$$: 'Text "  " ':<>: ShowOperators ops
+
+----------------------------------------
+
+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
+
 -- | Curry a type-level list.
 --
 -- In pseudo (dependent-)Haskell:
@@ -37,7 +81,7 @@
   Curry (x ': xs) y = x -> Curry xs y
 
 -- | Append two type-level lists together.
-type family Append (xs :: IxList) (ys :: IxList) :: IxList where
+type family Append (xs :: [k]) (ys :: [k]) :: [k] where
   Append '[]       ys  = ys -- needed for (<%>) and (%>)
   Append xs        '[] = xs -- needed for (<%)
   Append (x ': xs) ys  = x ': Append xs ys
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
@@ -15,6 +15,7 @@
 
   , (#.)
   , (.#)
+  , uncurry'
   ) where
 
 import qualified Data.Semigroup as SG
@@ -103,3 +104,10 @@
 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/Iso.hs b/src/Optics/Iso.hs
--- a/src/Optics/Iso.hs
+++ b/src/Optics/Iso.hs
@@ -75,12 +75,14 @@
   , under
 
   -- * Combinators
-  -- | The 'Optics.Re.re' combinator can be used to reverse an 'Iso':
+  -- | The 'Optics.Re.re' combinator can be used to reverse an 'Iso', and the
+  -- 'Optics.Mapping.mapping' combinator to lift an 'Iso' to an 'Iso' on
+  -- functorial values.
   --
   -- @
-  -- 'Optics.Re.re' :: 'Iso' s t a b -> 'Iso' b a t s
+  -- 'Optics.Re.re'      ::                           'Iso' s t a b -> 'Iso' b a t s
+  -- 'Optics.Mapping.mapping' :: (Functor f, Functor g) => 'Iso' s t a b -> 'Iso' (f s) (g t) (f a) (g b)
   -- @
-  , mapping
 
   -- * Subtyping
   , An_Iso
@@ -149,14 +151,6 @@
 
 ----------------------------------------
 -- Isomorphisms
-
--- | This can be used to lift any 'Iso' into an arbitrary 'Functor'.
-mapping
-  :: (Functor f, Functor g)
-  => Iso    s     t     a     b
-  -> Iso (f s) (g t) (f a) (g b)
-mapping k = withIso k $ \sa bt -> iso (fmap sa) (fmap bt)
-{-# INLINE mapping #-}
 
 -- | Capture type constraints as an isomorphism.
 --
diff --git a/src/Optics/IxAffineFold.hs b/src/Optics/IxAffineFold.hs
--- a/src/Optics/IxAffineFold.hs
+++ b/src/Optics/IxAffineFold.hs
@@ -26,7 +26,28 @@
   -- 'ipreview' ('iafolding' f) ≡ f
   -- @
 
-  -- * Semigroup structure
+  -- * Additional introduction forms
+  , iafoldVL
+
+  -- * Additional elimination forms
+  , iatraverseOf_
+
+  -- * Combinators
+  , filteredBy
+
+  -- * Monoid structure
+  -- | 'IxAffineFold' admits a monoid structure where 'iafailing' combines folds
+  -- (returning a result from the second fold only if the first returns none)
+  -- and the identity element is 'Optics.IxAffineTraversal.ignored' (which
+  -- returns no results).
+  --
+  -- /Note:/ There is no 'Optics.IxFold.isumming' equivalent that returns an
+  -- 'IxAffineFold', because it would not need to return more than one result.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'IxAffineFold', 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.
   , iafailing
 
   -- * Subtyping
@@ -39,10 +60,25 @@
 import Optics.Internal.Bi
 import Optics.Internal.Indexed
 import Optics.Internal.Optic
+import Optics.Internal.Utils
 
 -- | Type synonym for an indexed affine fold.
 type IxAffineFold i s a = Optic' An_AffineFold (WithIx i) s a
 
+-- | Obtain an 'IxAffineFold' by lifting 'itraverse_' like function.
+--
+-- @
+-- 'aifoldVL' '.' 'iatraverseOf_' ≡ 'id'
+-- 'aitraverseOf_' '.' 'iafoldVL' ≡ 'id'
+-- @
+--
+-- @since 0.3
+iafoldVL
+  :: (forall f. Functor f => (forall r. r -> f r) -> (i -> a -> f u) -> s -> f v)
+  -> IxAffineFold i s a
+iafoldVL f = Optic (rphantom . ivisit f . rphantom)
+{-# INLINE iafoldVL #-}
+
 -- | Retrieve the value along with its index targeted by an 'IxAffineFold'.
 ipreview
   :: (Is k An_AffineFold, is `HasSingleIndex` i)
@@ -62,16 +98,36 @@
   id
 {-# INLINE ipreviews #-}
 
+-- | Traverse over the target of an 'IxAffineFold', computing a 'Functor'-based
+-- answer, but unlike 'Optics.IxAffineTraversal.iatraverseOf' do not construct a
+-- new structure.
+--
+-- @since 0.3
+iatraverseOf_
+  :: (Is k An_AffineFold, Functor f, is `HasSingleIndex` i)
+  => Optic' k is s a
+  -> (forall r. r -> f r) -> (i -> a -> f u) -> s -> f ()
+iatraverseOf_ o point f s = case ipreview o s of
+  Just (i, a) -> () <$ f i a
+  Nothing     -> point ()
+
 -- | Create an 'IxAffineFold' from a partial function.
 iafolding :: (s -> Maybe (i, a)) -> IxAffineFold i s a
-iafolding g = Optic
-  $ ivisit (\point f s -> maybe (point s) (uncurry f) $ g s)
-  . rphantom
+iafolding g = iafoldVL (\point f s -> maybe (point s) (uncurry' f) $ g s)
 {-# INLINE iafolding #-}
 
+-- | Obtain a potentially empty 'IxAffineFold' by taking the element from
+-- another 'AffineFold' and using it as an index.
+--
+-- @since 0.3
+filteredBy :: Is k An_AffineFold  => Optic' k is a i -> IxAffineFold i a a
+filteredBy p = iafoldVL $ \point f s -> case preview p s of
+  Just i  -> f i s
+  Nothing -> point s
+{-# INLINE filteredBy #-}
+
 -- | Try the first 'IxAffineFold'. If it returns no entry, try the second one.
 --
--- /Note:/ There is no 'Optics.IxFold.isumming' equivalent, because @iasumming = iafailing@.
 iafailing
   :: (Is k An_AffineFold, Is l An_AffineFold,
       is1 `HasSingleIndex` i, is2 `HasSingleIndex` i)
diff --git a/src/Optics/IxAffineTraversal.hs b/src/Optics/IxAffineTraversal.hs
--- a/src/Optics/IxAffineTraversal.hs
+++ b/src/Optics/IxAffineTraversal.hs
@@ -30,6 +30,12 @@
   -- 'Optics.IxSetter.iset'     :: 'IxAffineTraversal' i s t a b -> (i      -> b) -> s -> t
   -- @
 
+  -- * Combinators
+  , unsafeFilteredBy
+
+  -- * Additional introduction forms
+  , ignored
+
   -- * Subtyping
   , An_AffineTraversal
 
@@ -37,13 +43,15 @@
   , IxAffineTraversalVL
   , IxAffineTraversalVL'
   , iatraversalVL
-  , toIxAtraversalVL
+  , iatraverseOf
   ) where
 
 import Data.Profunctor.Indexed
 
+import Optics.AffineFold
 import Optics.Internal.Indexed
 import Optics.Internal.Optic
+import Optics.Internal.Utils
 
 -- | Type synonym for a type-modifying indexed affine traversal.
 type IxAffineTraversal i s t a b = Optic An_AffineTraversal (WithIx i) s t a b
@@ -71,7 +79,7 @@
 -- representation, use 'iatraversalVL'.
 iatraversal :: (s -> Either t (i, a)) -> (s -> b -> t) -> IxAffineTraversal i s t a b
 iatraversal match update = iatraversalVL $ \point f s ->
-  either point (\a -> update s <$> uncurry f a) (match s)
+  either point (\a -> update s <$> uncurry' f a) (match s)
 {-# INLINE iatraversal #-}
 
 -- | Build an indexed affine traversal from the van Laarhoven representation.
@@ -79,11 +87,47 @@
 iatraversalVL f = Optic (ivisit f)
 {-# INLINE iatraversalVL #-}
 
--- | Convert an indexed affine traversal to its van Laarhoven representation.
-toIxAtraversalVL
-  :: (Is k An_AffineTraversal, is `HasSingleIndex` i)
+-- | Traverse over the target of an 'IxAffineTraversal' and compute a
+-- 'Functor'-based answer.
+--
+-- @since 0.3
+iatraverseOf
+  :: (Is k An_AffineTraversal, Functor f, is `HasSingleIndex` i)
   => Optic k is s t a b
-  -> IxAffineTraversalVL i s t a b
-toIxAtraversalVL o point = \f ->
+  -> (forall r. r -> f r) -> (i -> a -> f b) -> s -> f t
+iatraverseOf o point = \f ->
   runIxStarA (getOptic (castOptic @An_AffineTraversal o) (IxStarA point f)) id
-{-# INLINE toIxAtraversalVL #-}
+{-# INLINE iatraverseOf #-}
+
+-- | Obtain a potentially empty 'IxAffineTraversal' by taking the element from
+-- another 'AffineFold' and using it as an index.
+--
+-- -- /Note:/ This is /not/ a legal 'Optics.IxTraversal.IxTraversal', unless you
+-- are very careful not to invalidate the predicate on the target (see
+-- 'Optics.AffineTraversal.unsafeFiltered' for more details).
+--
+-- @since 0.3
+unsafeFilteredBy
+  :: Is k An_AffineFold
+  => Optic' k is a i
+  -> IxAffineTraversal' i a a
+unsafeFilteredBy p = iatraversalVL $ \point f s -> case preview p s of
+  Just i  -> f i s
+  Nothing -> point s
+{-# INLINE unsafeFilteredBy #-}
+
+-- | This is the trivial empty 'IxAffineTraversal', i.e. the optic that targets
+-- 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.
+--
+-- >>> 6 & ignored %~ absurd
+-- 6
+ignored :: IxAffineTraversal i s s a b
+ignored = iatraversalVL $ \point _ -> point
+
+-- $setup
+-- >>> import Optics.Core
+-- >>> import Data.Void (absurd)
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,20 @@
   , ifiltered
   , ibackwards_
 
-  -- * Semigroup structure
+  -- * Monoid structures
+  -- | 'IxFold' admits (at least) two monoid structures:
+  --
+  -- * 'isumming' concatenates results from both folds.
+  --
+  -- * 'ifailing' returns results from the second fold only if the first returns
+  --   no results.
+  --
+  -- In both cases, the identity element of the monoid is
+  -- `Optics.IxAffineTraversal.ignored`, which returns no results.
+  --
+  -- There is no 'Semigroup' or 'Monoid' instance for 'IxFold', because there is
+  -- not a unique choice of monoid to use, and the ('<>') operator could not be
+  -- used to combine optics of different kinds.
   , isumming
   , ifailing
 
@@ -62,6 +75,7 @@
 
 import Optics.Internal.Bi
 import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.Fold
 import Optics.Internal.IxFold
 import Optics.Internal.Optic
@@ -187,6 +201,8 @@
 
 -- | Convert an indexed fold to an 'IxAffineFold' that visits the first element
 -- of the original fold.
+--
+-- For the traversal version see 'Optics.IxTraversal.isingular'.
 ipre
   :: (Is k A_Fold, is `HasSingleIndex` i)
   => Optic' k is s a
@@ -226,6 +242,10 @@
 {-# INLINE ibackwards_ #-}
 
 -- | Return entries of the first 'IxFold', then the second one.
+--
+-- >>> itoListOf (ifolded `isumming` ibackwards_ ifolded) ["a","b"]
+-- [(0,"a"),(1,"b"),(1,"b"),(0,"a")]
+--
 isumming
   :: (Is k A_Fold, Is l A_Fold,
       is1 `HasSingleIndex` i, is2 `HasSingleIndex` i)
@@ -238,6 +258,12 @@
 {-# INLINE isumming #-}
 
 -- | Try the first 'IxFold'. If it returns no entries, try the second one.
+--
+-- >>> itoListOf (_1 % ifolded `ifailing` _2 % ifolded) (["a"], ["b","c"])
+-- [(0,"a")]
+-- >>> itoListOf (_1 % ifolded `ifailing` _2 % ifolded) ([], ["b","c"])
+-- [(0,"b"),(1,"c")]
+--
 ifailing
   :: (Is k A_Fold, Is l A_Fold, is1 `HasSingleIndex` i, is2 `HasSingleIndex` i)
   => Optic' k is1 s a
diff --git a/src/Optics/IxGetter.hs b/src/Optics/IxGetter.hs
--- a/src/Optics/IxGetter.hs
+++ b/src/Optics/IxGetter.hs
@@ -28,6 +28,7 @@
 import Optics.Internal.Bi
 import Optics.Internal.Indexed
 import Optics.Internal.Optic
+import Optics.Internal.Utils
 
 -- | Type synonym for an indexed getter.
 type IxGetter i s a = Optic' A_Getter (WithIx i) s a
@@ -37,7 +38,7 @@
 -- >>> iview (ito id) ('i', 'x')
 -- ('i','x')
 ito :: (s -> (i, a)) -> IxGetter i s a
-ito f = Optic (lmap f . ilinear uncurry . rphantom)
+ito f = Optic (lmap f . ilinear uncurry' . rphantom)
 {-# INLINE ito #-}
 
 -- | Use a value itself as its own index. This is essentially an indexed version
diff --git a/src/Optics/IxLens.hs b/src/Optics/IxLens.hs
--- a/src/Optics/IxLens.hs
+++ b/src/Optics/IxLens.hs
@@ -48,6 +48,7 @@
 
 import Optics.Internal.Indexed
 import Optics.Internal.Optic
+import Optics.Internal.Utils
 
 -- | Type synonym for a type-modifying indexed lens.
 type IxLens i s t a b = Optic A_Lens (WithIx i) s t a b
@@ -67,7 +68,7 @@
 -- If you want to build an 'IxLens' from the van Laarhoven representation, use
 -- 'ilensVL'.
 ilens :: (s -> (i, a)) -> (s -> b -> t) -> IxLens i s t a b
-ilens get set = ilensVL $ \f s -> set s <$> uncurry f (get s)
+ilens get set = ilensVL $ \f s -> set s <$> uncurry' f (get s)
 {-# INLINE ilens #-}
 
 -- | Build an indexed lens from the van Laarhoven representation.
diff --git a/src/Optics/IxSetter.hs b/src/Optics/IxSetter.hs
--- a/src/Optics/IxSetter.hs
+++ b/src/Optics/IxSetter.hs
@@ -60,6 +60,7 @@
 import Data.Profunctor.Indexed
 
 import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.IxSetter
 import Optics.Internal.Optic
 import Optics.Internal.Utils
diff --git a/src/Optics/IxTraversal.hs b/src/Optics/IxTraversal.hs
--- a/src/Optics/IxTraversal.hs
+++ b/src/Optics/IxTraversal.hs
@@ -58,6 +58,7 @@
   , indices
   , ibackwards
   , ipartsOf
+  , isingular
 
   -- * Subtyping
   , A_Traversal
@@ -81,9 +82,11 @@
 import Data.Profunctor.Indexed
 
 import Optics.Internal.Indexed
+import Optics.Internal.Indexed.Classes
 import Optics.Internal.IxTraversal
 import Optics.Internal.Optic
 import Optics.Internal.Utils
+import Optics.IxAffineTraversal
 import Optics.IxLens
 import Optics.IxFold
 import Optics.ReadOnly
@@ -231,13 +234,6 @@
 itraversed = Optic itraversed__
 {-# INLINE itraversed #-}
 
--- | This is the trivial empty 'IxTraversal'.
---
--- >>> 6 & ignored %~ absurd
--- 6
-ignored :: IxTraversal i s s a b
-ignored = itraversalVL $ \_ -> pure
-
 ----------------------------------------
 -- Traversal combinators
 
@@ -288,14 +284,12 @@
 {-# INLINE elements #-}
 
 -- | Traverse the /nth/ element of a 'Traversal' if it exists.
---
--- TODO: the result ideally should be an indexed affine traversal.
 elementOf
   :: Is k A_Traversal
-  => Optic k is s t a a
+  => Optic' k is s a
   -> Int
-  -> IxTraversal Int s t a a
-elementOf o = \i -> elementsOf o (== i)
+  -> IxAffineTraversal' Int s a
+elementOf o = \i -> isingular $ elementsOf o (== i)
 {-# INLINE elementOf #-}
 
 -- | Traverse the /nth/ element of a 'Traversable' container.
@@ -303,7 +297,7 @@
 -- @
 -- 'element' ≡ 'elementOf' 'traversed'
 -- @
-element :: Traversable f => Int -> IxTraversal' Int (f a) a
+element :: Traversable f => Int -> IxAffineTraversal' Int (f a) a
 element = elementOf traversed
 {-# INLINE element #-}
 
@@ -315,12 +309,35 @@
   -> IxLens [i] s t [a] [a]
 ipartsOf o = conjoined (partsOf o) $ ilensVL $ \f s ->
   evalState (traverseOf o update s)
-    <$> uncurry f (unzip $ itoListOf (getting $ castOptic @A_Traversal o) s)
+    <$> uncurry' f (unzip $ itoListOf (getting $ castOptic @A_Traversal o) s)
   where
     update a = get >>= \case
       []       ->            pure a
       a' : as' -> put as' >> pure a'
 {-# INLINE ipartsOf #-}
+
+-- | Convert an indexed traversal to an 'IxAffineTraversal' that visits the
+-- first element of the original traversal.
+--
+-- For the fold version see 'Optics.IxFold.ipre'.
+--
+-- >>> [1,2,3] & iover (isingular itraversed) (-)
+-- [-1,2,3]
+--
+-- @since 0.3
+isingular
+  :: forall k is i s a. (Is k A_Traversal, is `HasSingleIndex` i)
+  => Optic' k is s a
+  -> IxAffineTraversal' i s a
+isingular o = conjoined (singular o) $ iatraversalVL $ \point f s ->
+  case iheadOf (castOptic @A_Traversal o) s of
+    Nothing     -> point s
+    Just (i, a) -> evalState (traverseOf o update s) . Just <$> f i a
+  where
+    update a = get >>= \case
+      Just a' -> put Nothing >> pure a'
+      Nothing ->                pure a
+{-# INLINE isingular #-}
 
 -- $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
@@ -37,17 +37,17 @@
 -- @Optics.TH@ in the @optics-th@ package:
 --
 -- >>> :{
--- instance (a ~ String, b ~ String) => LabelOptic "name" A_Lens Human Human a b where
+-- instance (k ~ A_Lens, a ~ String, b ~ String) => LabelOptic "name" k Human Human a b where
 --   labelOptic = lensVL $ \f s -> (\v -> s { humanName = v }) <$> f (humanName s)
--- instance (a ~ Integer, b ~ Integer) => LabelOptic "age" A_Lens Human Human a b where
+-- instance (k ~ A_Lens, a ~ Integer, b ~ Integer) => LabelOptic "age" k Human Human a b where
 --   labelOptic = lensVL $ \f s -> (\v -> s { humanAge = v }) <$> f (humanAge s)
--- instance (a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" A_Lens Human Human a b where
+-- instance (k ~ A_Lens, a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" k Human Human a b where
 --   labelOptic = lensVL $ \f s -> (\v -> s { humanPets = v }) <$> f (humanPets s)
--- instance (a ~ String, b ~ String) => LabelOptic "name" A_Lens Pet Pet a b where
+-- instance (k ~ A_Lens, a ~ String, b ~ String) => LabelOptic "name" k Pet Pet a b where
 --   labelOptic = lensVL $ \f s -> (\v -> s { petName = v }) <$> f (petName s)
--- instance (a ~ Int, b ~ Int) => LabelOptic "age" A_Lens Pet Pet a b where
+-- instance (k ~ A_Lens, a ~ Int, b ~ Int) => LabelOptic "age" k Pet Pet a b where
 --   labelOptic = lensVL $ \f s -> (\v -> s { petAge = v }) <$> f (petAge s)
--- instance (a ~ Bool, b ~ Bool) => LabelOptic "lazy" An_AffineTraversal Pet Pet a b where
+-- 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
@@ -94,7 +94,7 @@
 -- You might wonder why instances above are written in form
 --
 -- @
--- instance (a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" A_Lens Human Human a b where
+-- instance (k ~ A_Lens, a ~ [Pet], b ~ [Pet]) => LabelOptic "pets" k Human Human a b where
 -- @
 --
 -- instead of
@@ -103,10 +103,10 @@
 -- instance LabelOptic "pets" A_Lens Human Human [Pet] [Pet] where
 -- @
 --
--- The reason is that using the first form ensures that GHC always matches on
--- the instance if either @s@ or @t@ is known and verifies type equalities
--- later, which not only makes type inference better, but also allows it to
--- generate good error messages.
+-- 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
+-- 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:
@@ -144,6 +144,14 @@
 --         (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
+--
+-- λ> age = #age :: Iso' Human Int
+--
+-- <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
 -- @
 --
 -- If we use the first form, error messages become more accurate:
@@ -164,6 +172,13 @@
 --     • 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
+--
+-- <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
 -- @
 --
 -- == Limitations arising from functional dependencies
diff --git a/src/Optics/Mapping.hs b/src/Optics/Mapping.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Mapping.hs
@@ -0,0 +1,91 @@
+-- |
+-- Module: Optics.Mapping
+-- Description: Lifting optics using 'Functor's 'map'.
+--
+-- This module defines 'mapping', which turns an @'Optic'' k 'NoIx' s a@ into an
+-- @'Optic'' ('MappedOptic' k) 'NoIx' (f s) (f a)@, in other words optic operating on values
+-- in a 'Functor'.
+--
+{-# LANGUAGE DataKinds #-}
+module Optics.Mapping
+  ( MappingOptic (..)
+  ) where
+
+import Optics.Getter
+import Optics.Internal.Indexed
+import Optics.Internal.Optic
+import Optics.Iso
+import Optics.Review
+
+-- $setup
+-- >>> import Optics.Core
+-- >>> import Optics.Operators
+
+-- | Class for optics supporting 'mapping' through a 'Functor'.
+--
+-- @since 0.3
+class MappingOptic k f g s t a b where
+  -- | Type family that maps an optic to the optic kind produced by
+  -- 'mapping' using it.
+  type MappedOptic k
+
+  -- | The 'Optics.Mapping.mapping' can be used to lift optic through a 'Functor'.
+  --
+  -- @
+  -- 'mapping' :: 'Iso'    s t a b -> 'Iso'    (f s) (g t) (f a) (g b)
+  -- 'mapping' :: 'Optics.Lens.Lens'   s   a   -> 'Getter' (f s)       (f a)
+  -- 'mapping' :: 'Getter' s   a   -> 'Getter' (f s)       (f a)
+  -- 'mapping' :: 'Optics.Prism.Prism'    t   b -> 'Review'       (g t)       (g b)
+  -- 'mapping' :: 'Review'   t   b -> 'Review'       (g t)       (g b)
+  -- @
+  mapping
+    :: "mapping" `AcceptsEmptyIndices` is
+    => Optic k               is s t a b
+    -> Optic (MappedOptic k) is (f s) (g t) (f a) (g b)
+
+instance (Functor f, Functor g) => MappingOptic An_Iso f g s t a b where
+  type MappedOptic An_Iso = An_Iso
+  mapping k = withIso k $ \sa bt -> iso (fmap sa) (fmap bt)
+  {-# INLINE mapping #-}
+
+-- Getter-y optics
+
+-- | 
+-- >>> [('a', True), ('b', False)] ^. _1 %& mapping
+-- "ab"
+--
+-- >>> let v = [[ (('a', True), "foo"), (('b', False), "bar")], [ (('c', True), "xyz") ] ]
+-- >>> v ^. _1 % _2 %& mapping %& mapping
+-- [[True,False],[True]]
+--
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_Getter f g s t a b where
+  type MappedOptic A_Getter = A_Getter
+  mapping o = to (fmap (view o))
+  {-# INLINE mapping #-}
+
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_ReversedPrism f g s t a b where
+  type MappedOptic A_ReversedPrism = A_Getter
+  mapping o = to (fmap (view o))
+  {-# INLINE mapping #-}
+
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_Lens f g s t a b where
+  type MappedOptic A_Lens = A_Getter
+  mapping o = to (fmap (view o))
+  {-# INLINE mapping #-}
+
+-- Review-y optics
+
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_Review f g s t a b where
+  type MappedOptic A_Review = A_Review
+  mapping o = unto (fmap (review o))
+  {-# INLINE mapping #-}
+
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_Prism f g s t a b where
+  type MappedOptic A_Prism = A_Review
+  mapping o = unto (fmap (review o))
+  {-# INLINE mapping #-}
+
+instance (Functor f, f ~ g, s ~ t, a ~ b) => MappingOptic A_ReversedLens f g s t a b where
+  type MappedOptic A_ReversedLens = A_Review
+  mapping o = unto (fmap (review o))
+  {-# INLINE mapping #-}
diff --git a/src/Optics/Operators.hs b/src/Optics/Operators.hs
--- a/src/Optics/Operators.hs
+++ b/src/Optics/Operators.hs
@@ -50,7 +50,7 @@
 
 infixl 8 ^..
 
--- | Flipped infix version of 'review'.
+-- | Infix version of 'review'.
 (#) :: Is k A_Review => Optic' k is t b -> b -> t
 (#) = review
 {-# INLINE (#) #-}
diff --git a/src/Optics/Operators/Unsafe.hs b/src/Optics/Operators/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Optics/Operators/Unsafe.hs
@@ -0,0 +1,37 @@
+-- |
+-- Module: Optics.Operators.Unsafe
+-- Description: Definitions of unsafe infix operators for optics.
+--
+module Optics.Operators.Unsafe
+  ( (^?!)
+  )
+  where
+
+import Data.Maybe (fromMaybe)
+import GHC.Stack (HasCallStack)
+
+import Optics.AffineFold
+import Optics.Optic
+import Optics.Operators
+
+-- | Perform an *UNSAFE* 'head' of an affine fold assuming that it is there.
+--
+-- >>> Left 4 ^?! _Left
+-- 4
+--
+-- >>> "world" ^?! ix 3
+-- 'l'
+--
+-- >>> [] ^?! _head
+-- *** Exception: (^?!): empty affine fold
+-- ...
+--
+-- @since 0.3
+(^?!) :: (HasCallStack, Is k An_AffineFold) => s -> Optic' k is s a -> a
+s ^?! o = fromMaybe (error "(^?!): empty affine fold") (s ^? o)
+{-# INLINE (^?!) #-}
+
+infixl 8 ^?!
+
+-- $setup
+-- >>> import Optics.Core
diff --git a/src/Optics/Optic.hs b/src/Optics/Optic.hs
--- a/src/Optics/Optic.hs
+++ b/src/Optics/Optic.hs
@@ -34,10 +34,25 @@
   , Join
 
   -- * Composition
+  -- | The usual operator for composing optics is ('%'), which allows different
+  -- optic kinds to be composed, automatically calculating the resulting optic
+  -- kind using 'Join'.
+  --
+  -- The ('.') function composition operator cannot be used to compose optics,
+  -- because /optics are not functions/.  The ('Control.Category..') operator
+  -- from "Control.Category" cannot be used either, because it would not support
+  -- type-changing optics or composing optics of different kinds.
   , (%)
   , (%%)
   , (%&)
 
+  -- * Monoid structures
+  -- | 'Optics.Fold.Fold'-like optics admit various monoid structures (e.g. see
+  -- "Optics.Fold#monoids").  There is no 'Semigroup' or 'Monoid' instance for
+  -- 'Optic', however, because there is not a unique choice of monoid to use,
+  -- and the ('<>') operator could not be used to combine optics of different
+  -- kinds.
+
   -- * Indexed optics
   -- | See the "Indexed optics" section of the overview documentation in the
   -- @Optics@ module of the main @optics@ package for more details on indexed
@@ -49,6 +64,8 @@
   , NonEmptyIndices
   , HasSingleIndex
   , AcceptsEmptyIndices
+  , Curry
+  , 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
@@ -26,19 +26,15 @@
   --
   -- Example:
   --
-  -- @
-  -- λ> let fstIntToChar = _1 :: Lens (Int, r) (Char, r) Int Char
-  -- λ> :t view fstIntToChar
+  -- >>> let fstIntToChar = _1 :: Lens (Int, r) (Char, r) Int Char
   --
-  -- <interactive>:1:6: error:
-  --     • Couldn't match type ‘Char’ with ‘Int’
-  --       Expected type: Optic' A_Lens NoIx (Int, r) Int
-  --         Actual type: Lens (Int, r) (Char, r) Int Char
-  --     • In the first argument of ‘view’, namely ‘fstIntToChar’
-  --       In the expression: view fstIntToChar
-  -- λ> :t view (getting fstIntToChar)
+  -- >>> :t view fstIntToChar
+  -- ...
+  -- ...Couldn't match type ‘Char’ with ‘Int’
+  -- ...
+  --
+  -- >>> :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
 
 instance ToReadOnly An_Iso s t a b where
@@ -84,3 +80,6 @@
   -> Optic__ p i (Curry is i) s s a a
 getting__ (Optic o) = rphantom . o . rphantom
 {-# INLINE getting__ #-}
+
+-- $setup
+-- >>> import Optics.Core
diff --git a/src/Optics/Traversal.hs b/src/Optics/Traversal.hs
--- a/src/Optics/Traversal.hs
+++ b/src/Optics/Traversal.hs
@@ -61,6 +61,7 @@
     -- * Combinators
   , backwards
   , partsOf
+  , singular
 
   -- * Subtyping
   , A_Traversal
@@ -82,6 +83,7 @@
 
 import Data.Profunctor.Indexed
 
+import Optics.AffineTraversal
 import Optics.Fold
 import Optics.Internal.Optic
 import Optics.Internal.Traversal
@@ -317,6 +319,29 @@
       a' : as' -> put as' >> pure a'
       []       ->            pure a
 {-# INLINE partsOf #-}
+
+-- | Convert a traversal to an 'AffineTraversal' that visits the first element
+-- of the original traversal.
+--
+-- For the fold version see 'Optics.Fold.pre'.
+--
+-- >>> "foo" & singular traversed .~ 'z'
+-- "zoo"
+--
+-- @since 0.3
+singular
+  :: forall k is s a. Is k A_Traversal
+  => Optic' k is s a
+  -> AffineTraversal' s a
+singular o = atraversalVL $ \point f s ->
+  case headOf (castOptic @A_Traversal o) s of
+    Nothing -> point s
+    Just a  -> evalState (traverseOf o update s) . Just <$> f a
+  where
+    update a = get >>= \case
+      Just a' -> put Nothing >> pure a'
+      Nothing ->                pure a
+{-# INLINE singular #-}
 
 -- $setup
 -- >>> import Data.List