diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,15 @@
 Changelog
 =========
 
+Version 0.1.2.1
+---------------
+
+*February 23, 2023*
+
+<https://github.com/mstksg/functor-products/releases/tag/v0.1.2.1>
+
+*   Bump upper version bounds, reformat, fix warnings on ghc 9.6
+
 Version 0.1.2.0
 ---------------
 
diff --git a/functor-products.cabal b/functor-products.cabal
--- a/functor-products.cabal
+++ b/functor-products.cabal
@@ -1,7 +1,7 @@
 cabal-version: 1.12
 
 name:           functor-products
-version:        0.1.2.0
+version:        0.1.2.1
 synopsis:       General functor products for various Foldable instances
 description:    Generalizes the Rec type in vinyl to work over various different Foldable
                 instances, instead of just lists.  Provides a unifying abstraction for all
@@ -38,7 +38,7 @@
       base >=4.16 && <5,
       microlens           < 0.5,
       singletons          >= 3.0 && < 3.1,
-      singletons-base     < 3.2,
+      singletons-base     < 3.4,
       text                < 1.3,
       vinyl               < 0.15
   default-language: Haskell2010
diff --git a/src/Data/Type/Functor/Product.hs b/src/Data/Type/Functor/Product.hs
--- a/src/Data/Type/Functor/Product.hs
+++ b/src/Data/Type/Functor/Product.hs
@@ -1,1005 +1,1058 @@
-{-# LANGUAGE AllowAmbiguousTypes      #-}
-{-# LANGUAGE ConstraintKinds          #-}
-{-# LANGUAGE DeriveGeneric            #-}
-{-# LANGUAGE DeriveTraversable        #-}
-{-# LANGUAGE EmptyCase                #-}
-{-# LANGUAGE FlexibleContexts         #-}
-{-# LANGUAGE FlexibleInstances        #-}
-{-# LANGUAGE FunctionalDependencies   #-}
-{-# LANGUAGE GADTs                    #-}
-{-# LANGUAGE InstanceSigs             #-}
-{-# LANGUAGE KindSignatures           #-}
-{-# LANGUAGE LambdaCase               #-}
-{-# LANGUAGE MultiParamTypeClasses    #-}
-{-# LANGUAGE RankNTypes               #-}
-{-# LANGUAGE ScopedTypeVariables      #-}
-{-# LANGUAGE StandaloneDeriving       #-}
-{-# LANGUAGE TypeApplications         #-}
-{-# LANGUAGE TypeFamilyDependencies   #-}
-{-# LANGUAGE TypeInType               #-}
-{-# LANGUAGE TypeOperators            #-}
-{-# LANGUAGE UndecidableInstances     #-}
-{-# LANGUAGE ViewPatterns             #-}
-
--- |
--- Module      : Data.Type.Functor.Product
--- Copyright   : (c) Justin Le 2018
--- License     : BSD3
---
--- Maintainer  : justin@jle.im
--- Stability   : experimental
--- Portability : non-portable
---
--- Generalized functor products based on lifted 'Foldable's.
---
--- For example, @'Rec' f '[a,b,c]@ from /vinyl/ contains an @f a@, @f b@,
--- and @f c@.
---
--- @'PMaybe' f ('Just a)@ contains an @f a@ and @'PMaybe' f 'Nothing@
--- contains nothing.
---
--- Also provide data types for "indexing" into each foldable.
-
-module Data.Type.Functor.Product (
-  -- * Classes
-    FProd(..), Shape
-  , PureProd(..), pureShape
-  , PureProdC(..), ReifyConstraintProd(..)
-  , AllConstrainedProd
-  -- ** Functions
-  , indexProd, mapProd, foldMapProd, hmap, zipProd
-  , imapProd, itraverseProd, ifoldMapProd
-  , generateProd, generateProdA
-  , selectProd, indices
-  , eqProd, compareProd
-  -- *** Over singletons
-  , indexSing, singShape
-  , foldMapSing, ifoldMapSing
-  -- * Instances
-  , Rec(..), Index(..), withPureProdList
-  , PMaybe(..), IJust(..)
-  , PEither(..), IRight(..)
-  , NERec(..), NEIndex(..), withPureProdNE
-  , PTup(..), ISnd(..)
-  , PIdentity(..), IIdentity(..)
-  , sameIndexVal, sameNEIndexVal
-  -- ** Interfacing with vinyl
-  , rElemIndex, indexRElem, toCoRec
-  -- * Singletons
-  , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIIdentity(..)
-  -- * Defunctionalization symbols
-  , ElemSym0, ElemSym1, ElemSym2
-  , ProdSym0, ProdSym1, ProdSym2
-  ) where
-
-import           Control.Applicative
-import           Data.Either.Singletons
-import           Data.Foldable.Singletons hiding  (Elem, ElemSym0, ElemSym1, ElemSym2)
-import           Data.Function.Singletons
-import           Data.Functor.Classes
-import           Data.Functor.Identity
-import           Data.Functor.Identity.Singletons
-import           Data.Functor.Singletons
-import           Data.Kind
-import           Data.List.NonEmpty               (NonEmpty(..))
-import           Data.List.Singletons hiding      (Elem, ElemSym0, ElemSym1, ElemSym2)
-import           Data.Maybe
-import           Data.Maybe.Singletons
-import           Data.Semigroup
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Tuple.Singletons
-import           Data.Vinyl hiding                ((:~:))
-import           Data.Vinyl.CoRec
-import           GHC.Generics                     ((:*:)(..))
-import           Lens.Micro hiding                ((%~))
-import           Lens.Micro.Extras
-import           Text.Show.Singletons
-import           Unsafe.Coerce
-import qualified Data.List.NonEmpty.Singletons    as NE
-import qualified Data.Text                        as T
-import qualified Data.Vinyl.Functor               as V
-import qualified Data.Vinyl.TypeLevel             as V
-
-fmapIdent :: Fmap IdSym0 as :~: as
-fmapIdent = unsafeCoerce Refl
-
--- | Simply witness the /shape/ of an argument (ie, @'Shape' [] as@
--- witnesses the length of @as@, and @'Shape' Maybe as@ witnesses whether
--- or not @as@ is 'Just' or 'Nothing').
-type Shape f = (Prod f Proxy :: f k -> Type)
-
--- | Unify different functor products over a Foldable @f@.
-class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where
-    type Elem  f = (i :: f k -> k -> Type) | i -> f
-    type Prod  f = (p :: (k -> Type) -> f k -> Type) | p -> f
-
-    -- | You can convert a singleton of a foldable value into a foldable product of
-    -- singletons.  This essentially "breaks up" the singleton into its
-    -- individual items.  Should be an inverse with 'prodSing'.
-    singProd :: Sing as -> Prod f Sing as
-
-    -- | Collect a collection of singletons back into a single singleton.
-    -- Should be an inverse with 'singProd'.
-    prodSing :: Prod f Sing as -> Sing as
-
-    -- | Pair up each item in a foldable product with its index.
-    withIndices
-        :: Prod f g as
-        -> Prod f (Elem f as :*: g) as
-
-    -- | Traverse a foldable functor product with a RankN applicative function,
-    -- mapping over each value and sequencing the effects.
-    --
-    -- This is the generalization of 'rtraverse'.
-    traverseProd
-        :: forall g h as m. Applicative m
-        => (forall a. g a -> m (h a))
-        -> Prod f g as
-        -> m (Prod f h as)
-    traverseProd = case fmapIdent @as of
-      Refl -> htraverse (sing @IdSym0)
-
-    -- | Zip together two foldable functor products with a Rank-N function.
-    zipWithProd
-        :: (forall a. g a -> h a -> j a)
-        -> Prod f g as
-        -> Prod f h as
-        -> Prod f j as
-    zipWithProd f xs ys = imapProd (\i x -> f x (indexProd i ys)) xs
-
-    -- | Traverse a foldable functor product with a type-changing function.
-    htraverse
-        :: Applicative m
-        => Sing ff
-        -> (forall a. g a -> m (h (ff @@ a)))
-        -> Prod f g as
-        -> m (Prod f h (Fmap ff as))
-
-    -- | A 'Lens' into an item in a foldable functor product, given its
-    -- index.
-    --
-    -- This roughly generalizes 'rlens'.
-    ixProd
-        :: Elem f as a
-        -> Lens' (Prod f g as) (g a)
-
-    -- | Fold a functor product into a 'Rec'.
-    toRec :: Prod f g as -> Rec g (ToList as)
-
-    -- | Get a 'PureProd' instance from a foldable functor product
-    -- providing its shape.
-    withPureProd
-        :: Prod f g as
-        -> (PureProd f as => r)
-        -> r
-
--- | Create @'Prod' f@ if you can give a @g a@ for every slot.
-class PureProd f as where
-    pureProd :: (forall a. g a) -> Prod f g as
-
--- | Create @'Prod' f@ if you can give a @g a@ for every slot, given some
--- constraint.
-class PureProdC f c as where
-    pureProdC :: (forall a. c a => g a) -> Prod f g as
-
--- | Pair up each item in a @'Prod' f@ with a witness that @f a@ satisfies
--- some constraint.
-class ReifyConstraintProd f c g as where
-    reifyConstraintProd :: Prod f g as -> Prod f (Dict c V.:. g) as
-
-data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
-data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
-type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
-
-type instance Apply (ElemSym0 f) as = ElemSym1 f as
-type instance Apply (ElemSym1 f as) a = Elem f as a
-
-data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> f k ~> Type
-data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type
-type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as
-
-type instance Apply (ProdSym0 f) g = ProdSym1 f g
-type instance Apply (ProdSym1 f g) as = Prod f g as
-
--- | A convenient wrapper over 'V.AllConstrained' that works for any
--- Foldable @f@.
-type AllConstrainedProd c as = V.AllConstrained c (ToList as)
-
--- | Create a 'Shape' given an instance of 'PureProd'.
-pureShape :: PureProd f as => Shape f as
-pureShape = pureProd Proxy
-
--- | Generate a 'Prod' of indices for an @as@.
-indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
-indices = imapProd const pureShape
-
--- | Convert a @'Sing' as@ into a @'Shape' f as@, witnessing the shape of
--- of @as@ but dropping all of its values.
-singShape
-    :: FProd f
-    => Sing as
-    -> Shape f as
-singShape = mapProd (const Proxy) . singProd
-
--- | Map a RankN function over a 'Prod'.  The generalization of 'rmap'.
-mapProd
-    :: FProd f
-    => (forall a. g a -> h a)
-    -> Prod f g as
-    -> Prod f h as
-mapProd f = runIdentity . traverseProd (Identity . f)
-
--- | Zip together the values in two 'Prod's.
-zipProd
-    :: FProd f
-    => Prod f g as
-    -> Prod f h as
-    -> Prod f (g :*: h) as
-zipProd = zipWithProd (:*:)
-
--- | Map a type-changing function over every item in a 'Prod'.
-hmap
-    :: FProd f
-    => Sing ff
-    -> (forall a. g a -> h (ff @@ a))
-    -> Prod f g as
-    -> Prod f h (Fmap ff as)
-hmap ff f = runIdentity . htraverse ff (Identity . f)
-
--- | 'mapProd', but with access to the index at each element.
-imapProd
-    :: FProd f
-    => (forall a. Elem f as a -> g a -> h a)
-    -> Prod f g as
-    -> Prod f h as
-imapProd f = mapProd (\(i :*: x) -> f i x) . withIndices
-
--- | Extract the item from the container witnessed by the 'Elem'
-indexSing
-    :: forall f as a. FProd f
-    => Elem f as a        -- ^ Witness
-    -> Sing as            -- ^ Collection
-    -> Sing a
-indexSing i = indexProd i . singProd
-
--- | Use an 'Elem' to index a value out of a 'Prod'.
-indexProd
-    :: FProd f
-    => Elem f as a
-    -> Prod f g as
-    -> g a
-indexProd i = view (ixProd i)
-
--- | 'traverseProd', but with access to the index at each element.
-itraverseProd
-    :: (FProd f, Applicative m)
-    => (forall a. Elem f as a -> g a -> m (h a))
-    -> Prod f g as
-    -> m (Prod f h as)
-itraverseProd f = traverseProd (\(i :*: x) -> f i x) . withIndices
-
--- | 'foldMapProd', but with access to the index at each element.
-ifoldMapProd
-    :: (FProd f, Monoid m)
-    => (forall a. Elem f as a -> g a -> m)
-    -> Prod f g as
-    -> m
-ifoldMapProd f = getConst . itraverseProd (\i -> Const . f i)
-
--- | Map a RankN function over a 'Prod' and collect the results as
--- a 'Monoid'.
-foldMapProd
-    :: (FProd f, Monoid m)
-    => (forall a. g a -> m)
-    -> Prod f g as
-    -> m
-foldMapProd f = ifoldMapProd (const f)
-
--- | 'foldMapSing' but with access to the index.
-ifoldMapSing
-    :: forall f k (as :: f k) m. (FProd f, Monoid m)
-    => (forall a. Elem f as a -> Sing a -> m)
-    -> Sing as
-    -> m
-ifoldMapSing f = ifoldMapProd f . singProd
-
--- | A 'foldMap' over all items in a collection.
-foldMapSing
-    :: forall f k (as :: f k) m. (FProd f, Monoid m)
-    => (forall (a :: k). Sing a -> m)
-    -> Sing as
-    -> m
-foldMapSing f = ifoldMapSing (const f)
-
--- | Rearrange or permute the items in a 'Prod' based on a 'Prod' of
--- indices.
---
--- @
--- 'selectProd' ('IS' 'IZ' ':&' IZ :& 'RNil') ("hi" :& "bye" :& "ok" :& RNil)
---      == "bye" :& "hi" :& RNil
--- @
-selectProd
-    :: FProd f
-    => Prod f (Elem f as) bs
-    -> Prod f g as
-    -> Prod f g bs
-selectProd is xs = mapProd (`indexProd` xs) is
-
--- | An implementation of equality testing for all 'FProd' instances, as
--- long as each of the items are instances of 'Eq'.
-eqProd
-    :: (FProd f, ReifyConstraintProd f Eq g as)
-    => Prod f g as
-    -> Prod f g as
-    -> Bool
-eqProd xs = getAll
-          . foldMapProd getConst
-          . zipWithProd (\(V.Compose (Dict x)) y -> Const (All (x == y)))
-                (reifyConstraintProd @_ @Eq xs)
-
--- | An implementation of order comparison for all 'FProd' instances, as
--- long as each of the items are instances of 'Ord'.
-compareProd
-    :: (FProd f, ReifyConstraintProd f Ord g as)
-    => Prod f g as
-    -> Prod f g as
-    -> Ordering
-compareProd xs = foldMapProd getConst
-            . zipWithProd (\(V.Compose (Dict x)) y -> Const (compare x y))
-                  (reifyConstraintProd @_ @Ord xs)
-
--- | Construct a 'Prod' purely by providing a generating function for each
--- index.
-generateProd
-    :: (FProd f, PureProd f as)
-    => (forall a. Elem f as a -> g a)
-    -> Prod f g as
-generateProd f = mapProd f indices
-
--- | Construct a 'Prod' in an 'Applicative' context by providing
--- a generating function for each index.
-generateProdA
-    :: (FProd f, PureProd f as, Applicative m)
-    => (forall a. Elem f as a -> m (g a))
-    -> m (Prod f g as)
-generateProdA f = traverseProd f indices
-
-
--- | Witness an item in a type-level list by providing its index.
---
--- The number of 'IS's correspond to the item's position in the list.
---
--- @
--- 'IZ'         :: 'Index' '[5,10,2] 5
--- 'IS' 'IZ'      :: 'Index' '[5,10,2] 10
--- 'IS' ('IS' 'IZ') :: 'Index' '[5,10,2] 2
--- @
-data Index :: [k] -> k -> Type where
-    IZ :: Index (a ': as) a
-    IS :: Index bs a -> Index (b ': bs) a
-
-deriving instance Show (Index as a)
-deriving instance Eq (Index as a)
-deriving instance Ord (Index as a)
-
--- | Kind-indexed singleton for 'Index'.
-data SIndex (as :: [k]) (a :: k) :: Index as a -> Type where
-    SIZ :: SIndex (a ': as) a 'IZ
-    SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)
-
-deriving instance Show (SIndex as a i)
-
-type instance Sing = SIndex as a :: Index as a -> Type
-
-instance SingI 'IZ where
-    sing = SIZ
-
-instance SingI i => SingI ('IS i) where
-    sing = SIS sing
-
-instance SingKind (Index as a) where
-    type Demote (Index as a) = Index as a
-    fromSing = \case
-       SIZ   -> IZ
-       SIS j -> IS (fromSing j)
-    toSing i = go i SomeSing
-      where
-        go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
-        go = \case
-          IZ   -> ($ SIZ)
-          IS j -> \f -> go j (f . SIS)
-
-instance SDecide (Index as a) where
-    (%~) = \case
-      SIZ -> \case
-        SIZ   -> Proved Refl
-        SIS _ -> Disproved $ \case {}
-      SIS i' -> \case
-        SIZ   -> Disproved $ \case {}
-        SIS j' -> case i' %~ j' of
-          Proved Refl -> Proved Refl
-          Disproved v -> Disproved $ \case Refl -> v Refl
-
-instance FProd [] where
-    type Elem [] = Index
-    type Prod [] = Rec
-
-    singProd = \case
-      SNil         -> RNil
-      x `SCons` xs -> x :& singProd xs
-
-    prodSing = \case
-      RNil    -> SNil
-      x :& xs -> x `SCons` prodSing xs
-
-    traverseProd
-        :: forall g h m as. Applicative m
-        => (forall a. g a -> m (h a))
-        -> Prod [] g as
-        -> m (Prod [] h as)
-    traverseProd f = go
-      where
-        go :: Prod [] g bs -> m (Prod [] h bs)
-        go = \case
-          RNil    -> pure RNil
-          x :& xs -> (:&) <$> f x <*> go xs
-
-    zipWithProd
-        :: forall g h j as. ()
-        => (forall a. g a -> h a -> j a)
-        -> Prod [] g as
-        -> Prod [] h as
-        -> Prod [] j as
-    zipWithProd f = go
-      where
-        go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
-        go = \case
-          RNil -> \case
-            RNil -> RNil
-          x :& xs -> \case
-            y :& ys -> f x y :& go xs ys
-
-    htraverse
-        :: forall ff g h as m. Applicative m
-        => Sing ff
-        -> (forall a. g a -> m (h (ff @@ a)))
-        -> Prod [] g as
-        -> m (Prod [] h (Fmap ff as))
-    htraverse _ f = go
-      where
-        go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
-        go = \case
-          RNil    -> pure RNil
-          x :& xs -> (:&) <$> f x <*> go xs
-
-    withIndices = \case
-        RNil    -> RNil
-        x :& xs -> (IZ :*: x) :& mapProd (\(i :*: y) -> IS i :*: y) (withIndices xs)
-
-    ixProd
-        :: forall g as a. ()
-        => Elem [] as a
-        -> Lens' (Prod [] g as) (g a)
-    ixProd i0 (f :: g a -> h (g a)) = go i0
-      where
-        go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
-        go = \case
-          IZ -> \case
-            x :& xs -> (:& xs) <$> f x
-          IS i -> \case
-            x :& xs -> (x :&) <$> go i xs
-
-    toRec = id
-
-    withPureProd = withPureProdList
-
--- | A stronger version of 'withPureProd' for 'Rec', providing
--- a 'RecApplicative' instance as well.
-withPureProdList
-    :: Rec f as
-    -> ((RecApplicative as, PureProd [] as) => r)
-    -> r
-withPureProdList = \case
-    RNil    -> id
-    _ :& xs -> withPureProdList xs
-
-instance RecApplicative as => PureProd [] as where
-    pureProd = rpure
-
-instance RPureConstrained c as => PureProdC [] c as where
-    pureProdC = rpureConstrained @c
-
-instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where
-    reifyConstraintProd = reifyConstraint @c
-
--- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
--- 'Just'.
-data IJust :: Maybe k -> k -> Type where
-    IJust :: IJust ('Just a) a
-
-deriving instance Show (IJust as a)
-deriving instance Read (IJust ('Just a) a)
-deriving instance Eq (IJust as a)
-deriving instance Ord (IJust as a)
-
--- | Kind-indexed singleton for 'IJust'.
-data SIJust (as :: Maybe k) (a :: k) :: IJust as a -> Type where
-    SIJust :: SIJust ('Just a) a 'IJust
-
-deriving instance Show (SIJust as a i)
-
-type instance Sing = SIJust as a :: IJust as a -> Type
-
-instance SingI 'IJust where
-    sing = SIJust
-
-instance SingKind (IJust as a) where
-    type Demote (IJust as a) = IJust as a
-    fromSing SIJust = IJust
-    toSing IJust = SomeSing SIJust
-
-instance SDecide (IJust as a) where
-    SIJust %~ SIJust = Proved Refl
-
--- | A @'PMaybe' f 'Nothing@ contains nothing, and a @'PMaybe' f ('Just a)@
--- contains an @f a@.
---
--- In practice this can be useful to write polymorphic
--- functions/abstractions that contain an argument that can be "turned off"
--- for different instances.
-data PMaybe :: (k -> Type) -> Maybe k -> Type where
-    PNothing :: PMaybe f 'Nothing
-    PJust    :: f a -> PMaybe f ('Just a)
-
-instance ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) where
-    showsPrec d xs = case reifyConstraintProd @_ @Show xs of
-      PNothing                   -> showString "PNothing"
-      PJust (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PJust" d x
-instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
-    (==) = eqProd
-instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where
-    compare = compareProd
-
-instance FProd Maybe where
-    type instance Elem Maybe = IJust
-    type instance Prod Maybe = PMaybe
-
-    singProd = \case
-      SNothing -> PNothing
-      SJust x  -> PJust x
-    prodSing = \case
-      PNothing -> SNothing
-      PJust x  -> SJust x
-    withIndices = \case
-      PNothing -> PNothing
-      PJust x  -> PJust (IJust :*: x)
-    traverseProd f = \case
-      PNothing -> pure PNothing
-      PJust x  -> PJust <$> f x
-    zipWithProd f = \case
-      PNothing -> \case
-        PNothing -> PNothing
-      PJust x -> \case
-        PJust y -> PJust (f x y)
-    htraverse _ f = \case
-      PNothing -> pure PNothing
-      PJust x  -> PJust <$> f x
-    ixProd = \case
-      IJust -> \f -> \case
-        PJust x -> PJust <$> f x
-    toRec = \case
-      PNothing -> RNil
-      PJust x  -> x :& RNil
-    withPureProd = \case
-      PNothing -> id
-      PJust _  -> id
-
-instance PureProd Maybe 'Nothing where
-    pureProd _ = PNothing
-instance PureProd Maybe ('Just a) where
-    pureProd x = PJust x
-
-instance PureProdC Maybe c 'Nothing where
-    pureProdC _ = PNothing
-instance c a => PureProdC Maybe c ('Just a) where
-    pureProdC x = PJust x
-
-instance ReifyConstraintProd Maybe c g 'Nothing where
-    reifyConstraintProd PNothing = PNothing
-instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where
-    reifyConstraintProd (PJust x) = PJust (V.Compose (Dict x))
-
--- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
--- is 'Right'.
-data IRight :: Either j k -> k -> Type where
-    IRight :: IRight ('Right a) a
-
-deriving instance Show (IRight as a)
-deriving instance Read (IRight ('Right a) a)
-deriving instance Eq (IRight as a)
-deriving instance Ord (IRight as a)
-
--- | Kind-indexed singleton for 'IRight'.
-data SIRight (as :: Either j k) (a :: k) :: IRight as a -> Type where
-    SIRight :: SIRight ('Right a) a 'IRight
-
-deriving instance Show (SIRight as a i)
-
-type instance Sing = SIRight as a :: IRight as a -> Type
-
-instance SingI 'IRight where
-    sing = SIRight
-
-instance SingKind (IRight as a) where
-    type Demote (IRight as a) = IRight as a
-    fromSing SIRight = IRight
-    toSing IRight = SomeSing SIRight
-
-instance SDecide (IRight as a) where
-    SIRight %~ SIRight = Proved Refl
-
--- | A @'PEither' f ('Left e)@ contains @'Sing' e@, and a @'PMaybe' f ('Right a)@
--- contains an @f a@.
---
--- In practice this can be useful in the same situatinos that 'PMaybe' can,
--- but with an extra value in the case where value @f@ is "turned off" with
--- 'Left'.
-data PEither :: (k -> Type) -> Either j k -> Type where
-    PLeft  :: Sing e -> PEither f ('Left e)
-    PRight :: f a -> PEither f ('Right a)
-
-instance (SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as) where
-    showsPrec d xs = case reifyConstraintProd @_ @Show xs of
-        PLeft e                     -> showsUnaryWith go         "PLeft" d e
-        PRight (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PRight" d x
-      where
-        go (fromIntegral->FromSing i) x (T.pack->FromSing str) = T.unpack . fromSing $ sShowsPrec i x str
-
-instance FProd (Either j) where
-    type instance Elem (Either j) = IRight
-    type instance Prod (Either j) = PEither
-
-    singProd = \case
-      SLeft  e -> PLeft e
-      SRight x -> PRight x
-    prodSing = \case
-      PLeft e  -> SLeft e
-      PRight x -> SRight x
-    withIndices = \case
-      PLeft e  -> PLeft e
-      PRight x -> PRight (IRight :*: x)
-    traverseProd f = \case
-      PLeft e  -> pure (PLeft e)
-      PRight x -> PRight <$> f x
-    zipWithProd f = \case
-      PLeft e -> \case
-        PLeft _ -> PLeft e
-      PRight x -> \case
-        PRight y -> PRight (f x y)
-    htraverse _ f = \case
-      PLeft e  -> pure (PLeft e)
-      PRight x -> PRight <$> f x
-    ixProd = \case
-      IRight -> \f -> \case
-        PRight x -> PRight <$> f x
-    toRec = \case
-      PLeft _  -> RNil
-      PRight x -> x :& RNil
-    withPureProd = \case
-      PLeft Sing -> id
-      PRight _   -> id
-
-instance SingI e => PureProd (Either j) ('Left e) where
-    pureProd _ = PLeft sing
-instance PureProd (Either j) ('Right a) where
-    pureProd x = PRight x
-
-instance SingI e => PureProdC (Either j) c ('Left e) where
-    pureProdC _ = (PLeft sing)
-instance c a => PureProdC (Either j) c ('Right a) where
-    pureProdC x = PRight x
-
-instance ReifyConstraintProd (Either j) c g ('Left e) where
-    reifyConstraintProd (PLeft e) = PLeft e
-instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where
-    reifyConstraintProd (PRight x) = PRight (V.Compose (Dict x))
-
--- | Witness an item in a type-level 'NonEmpty' by either indicating that
--- it is the "head", or by providing an index in the "tail".
-data NEIndex :: NonEmpty k -> k -> Type where
-    NEHead :: NEIndex (a ':| as) a
-    NETail :: Index as a -> NEIndex (b ':| as) a
-
-deriving instance Show (NEIndex as a)
-deriving instance Eq (NEIndex as a)
-deriving instance Ord (NEIndex as a)
-
--- | Kind-indexed singleton for 'NEIndex'.
-data SNEIndex (as :: NonEmpty k) (a :: k) :: NEIndex as a -> Type where
-    SNEHead :: SNEIndex (a ':| as) a 'NEHead
-    SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
-
-deriving instance Show (SNEIndex as a i)
-
-type instance Sing = SNEIndex as a :: NEIndex as a -> Type
-
-instance SingI 'NEHead where
-    sing = SNEHead
-
-instance SingI i => SingI ('NETail i) where
-    sing = SNETail sing
-
-instance SingKind (NEIndex as a) where
-    type Demote (NEIndex as a) = NEIndex as a
-    fromSing = \case
-      SNEHead   -> NEHead
-      SNETail i -> NETail $ fromSing i
-    toSing = \case
-      NEHead   -> SomeSing SNEHead
-      NETail i -> withSomeSing i $ SomeSing . SNETail
-
-instance SDecide (NEIndex as a) where
-    (%~) = \case
-      SNEHead -> \case
-        SNEHead   -> Proved Refl
-        SNETail _ -> Disproved $ \case {}
-      SNETail i -> \case
-        SNEHead -> Disproved $ \case {}
-        SNETail j -> case i %~ j of
-          Proved Refl -> Proved Refl
-          Disproved v -> Disproved $ \case Refl -> v Refl
-
--- | A non-empty version of 'Rec'.
-data NERec :: (k -> Type) -> NonEmpty k -> Type where
-    (:&|) :: f a -> Rec f as -> NERec f (a ':| as)
-infixr 5 :&|
-
-deriving instance (Show (f a), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a ':| as))
-deriving instance (Eq (f a), Eq (Rec f as)) => Eq (NERec f (a ':| as))
-deriving instance (Ord (f a), Ord (Rec f as)) => Ord (NERec f (a ':| as))
-
-instance FProd NonEmpty where
-    type instance Elem NonEmpty = NEIndex
-    type instance Prod NonEmpty = NERec
-
-    singProd (x NE.:%| xs) = x :&| singProd xs
-    prodSing (x :&| xs) = x NE.:%| prodSing xs
-    withIndices (x :&| xs) =
-          (NEHead :*: x)
-      :&| mapProd (\(i :*: y) -> NETail i :*: y) (withIndices xs)
-    traverseProd f (x :&| xs) =
-        (:&|) <$> f x <*> traverseProd f xs
-    zipWithProd f (x :&| xs) (y :&| ys) = f x y :&| zipWithProd f xs ys
-    htraverse ff f (x :&| xs) =
-        (:&|) <$> f x <*> htraverse ff f xs
-    ixProd = \case
-      NEHead -> \f -> \case
-        x :&| xs -> (:&| xs) <$> f x
-      NETail i -> \f -> \case
-        x :&| xs -> (x :&|) <$> ixProd i f xs
-    toRec (x :&| xs) = x :& xs
-    withPureProd (x :&| xs) = withPureProdNE x xs
-
--- | A stronger version of 'withPureProd' for 'NERec', providing
--- a 'RecApplicative' instance as well.
-withPureProdNE
-    :: f a
-    -> Rec f as
-    -> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-    -> r
-withPureProdNE _ xs = withPureProdList xs
-
-instance RecApplicative as => PureProd NonEmpty (a ':| as) where
-    pureProd x = x :&| pureProd x
-
-instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where
-    pureProdC x = x :&| pureProdC @_ @c x
-
-instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where
-    reifyConstraintProd (x :&| xs) = V.Compose (Dict x)
-                                 :&| reifyConstraintProd @_ @c xs
-
--- | Test if two indices point to the same item in a list.
---
--- We have to return a 'Maybe' here instead of a 'Decision', because it
--- might be the case that the same item might be duplicated in a list.
--- Therefore, even if two indices are different, we cannot prove that the
--- values they point to are different.
-sameIndexVal
-    :: Index as a
-    -> Index as b
-    -> Maybe (a :~: b)
-sameIndexVal = \case
-    IZ -> \case
-      IZ   -> Just Refl
-      IS _ -> Nothing
-    IS i -> \case
-      IZ   -> Nothing
-      IS j -> sameIndexVal i j <&> \case Refl -> Refl
-
-
--- | Test if two indices point to the same item in a non-empty list.
---
--- We have to return a 'Maybe' here instead of a 'Decision', because it
--- might be the case that the same item might be duplicated in a list.
--- Therefore, even if two indices are different, we cannot prove that the
--- values they point to are different.
-sameNEIndexVal
-    :: NEIndex as a
-    -> NEIndex as b
-    -> Maybe (a :~: b)
-sameNEIndexVal = \case
-    NEHead -> \case
-      NEHead   -> Just Refl
-      NETail _ -> Nothing
-    NETail i -> \case
-      NEHead   -> Nothing
-      NETail j -> sameIndexVal i j <&> \case Refl -> Refl
-
--- | Trivially witness an item in the second field of a type-level tuple.
-data ISnd :: (j, k) -> k -> Type where
-    ISnd :: ISnd '(a, b) b
-
-deriving instance Show (ISnd as a)
-deriving instance Read (ISnd '(a, b) b)
-deriving instance Eq (ISnd as a)
-deriving instance Ord (ISnd as a)
-
--- | Kind-indexed singleton for 'ISnd'.
-data SISnd (as :: (j, k)) (a :: k) :: ISnd as a -> Type where
-    SISnd :: SISnd '(a, b) b 'ISnd
-
-deriving instance Show (SISnd as a i)
-
-type instance Sing = SISnd as a :: ISnd as a -> Type
-
-instance SingI 'ISnd where
-    sing = SISnd
-
-instance SingKind (ISnd as a) where
-    type Demote (ISnd as a) = ISnd as a
-    fromSing SISnd = ISnd
-    toSing ISnd = SomeSing SISnd
-
-instance SDecide (ISnd as a) where
-    SISnd %~ SISnd = Proved Refl
-
--- | A 'PTup' tuples up some singleton with some value; a @'PTup' f '(w,
--- a)@ contains a @'Sing' w@ and an @f a@.
---
--- This can be useful for carrying along some witness aside a functor
--- value.
-data PTup :: (k -> Type) -> (j, k) -> Type where
-    PTup :: Sing w -> f a -> PTup f '(w, a)
-
-deriving instance (Show (Sing w), Show (f a)) => Show (PTup f '(w, a))
-deriving instance (Read (Sing w), Read (f a)) => Read (PTup f '(w, a))
-deriving instance (Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a))
-deriving instance (Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a))
-
-instance FProd ((,) j) where
-    type instance Elem ((,) j) = ISnd
-    type instance Prod ((,) j) = PTup
-
-    singProd (STuple2 w x) = PTup w x
-    prodSing (PTup w x) = STuple2 w x
-    withIndices (PTup w x) = PTup w (ISnd :*: x)
-    traverseProd f (PTup w x) = PTup w <$> f x
-    zipWithProd f (PTup w x) (PTup _ y) = PTup w (f x y)
-    htraverse _ f (PTup w x) = PTup w <$> f x
-    ixProd ISnd f (PTup w x) = PTup w <$> f x
-    toRec (PTup _ x) = x :& RNil
-    withPureProd (PTup Sing _) x = x
-
-instance SingI w => PureProd ((,) j) '(w, a) where
-    pureProd x = PTup sing x
-
-instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
-    pureProdC x = PTup sing x
-
-instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where
-    reifyConstraintProd (PTup w x) = PTup w $ V.Compose (Dict x)
-
--- | Trivially witness the item held in an 'Identity'.
---
--- @since 0.1.3.0
-data IIdentity :: Identity k -> k -> Type where
-    IId :: IIdentity ('Identity x) x
-
-deriving instance Show (IIdentity as a)
-deriving instance Read (IIdentity ('Identity a) a)
-deriving instance Eq (IIdentity as a)
-deriving instance Ord (IIdentity as a)
-
--- | Kind-indexed singleton for 'IIdentity'.
---
--- @since 0.1.5.0
-data SIIdentity (as :: Identity k) (a :: k) :: IIdentity as a -> Type where
-    SIId :: SIIdentity ('Identity a) a 'IId
-
-deriving instance Show (SIIdentity as a i)
-
-type instance Sing = SIIdentity as a :: IIdentity as a -> Type
-
-instance SingI 'IId where
-    sing = SIId
-
-instance SingKind (IIdentity as a) where
-    type Demote (IIdentity as a) = IIdentity as a
-    fromSing SIId = IId
-    toSing IId = SomeSing SIId
-
-instance SDecide (IIdentity as a) where
-    SIId %~ SIId = Proved Refl
-
--- | A 'PIdentity' is a trivial functor product; it is simply the functor,
--- itself, alone.  @'PIdentity' f ('Identity' a)@ is simply @f a@.  This
--- may be useful in conjunction with other combinators.
-data PIdentity :: (k -> Type) -> Identity k -> Type where
-    PIdentity :: f a -> PIdentity f ('Identity a)
-
-deriving instance Show (f a) => Show (PIdentity f ('Identity a))
-deriving instance Read (f a) => Read (PIdentity f ('Identity a))
-deriving instance Eq (f a) => Eq (PIdentity f ('Identity a))
-deriving instance Ord (f a) => Ord (PIdentity f ('Identity a))
-
-instance FProd Identity where
-    type Elem Identity = IIdentity
-    type Prod Identity = PIdentity
-
-    singProd (SIdentity x) = PIdentity x
-    prodSing (PIdentity x) = SIdentity x
-    withIndices (PIdentity x) = PIdentity (IId :*: x)
-    traverseProd f (PIdentity x) = PIdentity <$> f x
-    zipWithProd f (PIdentity x) (PIdentity y) = PIdentity (f x y)
-    htraverse _ f (PIdentity x) = PIdentity <$> f x
-    ixProd IId f (PIdentity x) = PIdentity <$> f x
-    toRec (PIdentity x) = x :& RNil
-    withPureProd (PIdentity _) x = x
-
-instance PureProd Identity ('Identity a) where
-    pureProd x = PIdentity x
-
-instance c a => PureProdC Identity c ('Identity a) where
-    pureProdC x = PIdentity x
-
-instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where
-    reifyConstraintProd (PIdentity x) = PIdentity $ V.Compose (Dict x)
-
--- | Produce an 'Index' from an 'RElem' constraint.
-rElemIndex
-    :: forall r rs i. (RElem r rs i, PureProd [] rs)
-    => Index rs r
-rElemIndex = rgetC indices
-
--- | Use an 'Index' to inject an @f a@ into a 'CoRec'.
-toCoRec
-    :: forall k (as :: [k]) a f. (RecApplicative as, FoldRec as as)
-    => Index as a
-    -> f a
-    -> CoRec f as
-toCoRec = \case
-    IZ   -> CoRec
-    IS i -> \x -> fromJust . firstField $ mapProd (go i x) indices
-  where
-    go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c
-    go i x j = case sameIndexVal (IS i) j of
-      Just Refl -> V.Compose (Just x)
-      Nothing  ->  V.Compose  Nothing
-
--- | If we have @'Index' as a@, we should also be able to create an item
--- that would require @'RElem' a as ('V.RIndex' as a)@.  Along with
--- 'rElemIndex', this essentially converts between the indexing system in
--- this library and the indexing system of /vinyl/.
-indexRElem
-    :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as)
-    => Index as a
-    -> (RElem a as (V.RIndex a as) => r)
-    -> r
-indexRElem i = case toCoRec i x of
-    CoRec y -> case x %~ y of
-      Proved Refl -> id
-      Disproved _ -> \_ -> errorWithoutStackTrace "why :|"
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- |
+-- Module      : Data.Type.Functor.Product
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Generalized functor products based on lifted 'Foldable's.
+--
+-- For example, @'Rec' f '[a,b,c]@ from /vinyl/ contains an @f a@, @f b@,
+-- and @f c@.
+--
+-- @'PMaybe' f ('Just a)@ contains an @f a@ and @'PMaybe' f 'Nothing@
+-- contains nothing.
+--
+-- Also provide data types for "indexing" into each foldable.
+module Data.Type.Functor.Product (
+  -- * Classes
+  FProd (..),
+  Shape,
+  PureProd (..),
+  pureShape,
+  PureProdC (..),
+  ReifyConstraintProd (..),
+  AllConstrainedProd,
+
+  -- ** Functions
+  indexProd,
+  mapProd,
+  foldMapProd,
+  hmap,
+  zipProd,
+  imapProd,
+  itraverseProd,
+  ifoldMapProd,
+  generateProd,
+  generateProdA,
+  selectProd,
+  indices,
+  eqProd,
+  compareProd,
+
+  -- *** Over singletons
+  indexSing,
+  singShape,
+  foldMapSing,
+  ifoldMapSing,
+
+  -- * Instances
+  Rec (..),
+  Index (..),
+  withPureProdList,
+  PMaybe (..),
+  IJust (..),
+  PEither (..),
+  IRight (..),
+  NERec (..),
+  NEIndex (..),
+  withPureProdNE,
+  PTup (..),
+  ISnd (..),
+  PIdentity (..),
+  IIdentity (..),
+  sameIndexVal,
+  sameNEIndexVal,
+
+  -- ** Interfacing with vinyl
+  rElemIndex,
+  indexRElem,
+  toCoRec,
+
+  -- * Singletons
+  SIndex (..),
+  SIJust (..),
+  SIRight (..),
+  SNEIndex (..),
+  SISnd (..),
+  SIIdentity (..),
+
+  -- * Defunctionalization symbols
+  ElemSym0,
+  ElemSym1,
+  ElemSym2,
+  ProdSym0,
+  ProdSym1,
+  ProdSym2,
+) where
+
+import Control.Applicative
+import Data.Either.Singletons
+import Data.Foldable.Singletons hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
+import Data.Function.Singletons
+import Data.Functor.Classes
+import Data.Functor.Identity
+import Data.Functor.Identity.Singletons
+import Data.Functor.Singletons
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty.Singletons as NE
+import Data.List.Singletons hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
+import Data.Maybe
+import Data.Maybe.Singletons
+import Data.Semigroup
+import Data.Singletons
+import Data.Singletons.Decide
+import qualified Data.Text as T
+import Data.Tuple.Singletons
+import Data.Vinyl hiding ((:~:))
+import Data.Vinyl.CoRec
+import qualified Data.Vinyl.Functor as V
+import qualified Data.Vinyl.TypeLevel as V
+import GHC.Generics ((:*:) (..))
+import Lens.Micro hiding ((%~))
+import Lens.Micro.Extras
+import Text.Show.Singletons
+import Unsafe.Coerce
+
+fmapIdent :: Fmap IdSym0 as :~: as
+fmapIdent = unsafeCoerce Refl
+
+-- | Simply witness the /shape/ of an argument (ie, @'Shape' [] as@
+-- witnesses the length of @as@, and @'Shape' Maybe as@ witnesses whether
+-- or not @as@ is 'Just' or 'Nothing').
+type Shape f = (Prod f Proxy :: f k -> Type)
+
+-- | Unify different functor products over a Foldable @f@.
+class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where
+  type Elem f = (i :: f k -> k -> Type) | i -> f
+  type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f
+
+  -- | You can convert a singleton of a foldable value into a foldable product of
+  -- singletons.  This essentially "breaks up" the singleton into its
+  -- individual items.  Should be an inverse with 'prodSing'.
+  singProd :: Sing as -> Prod f Sing as
+
+  -- | Collect a collection of singletons back into a single singleton.
+  -- Should be an inverse with 'singProd'.
+  prodSing :: Prod f Sing as -> Sing as
+
+  -- | Pair up each item in a foldable product with its index.
+  withIndices ::
+    Prod f g as ->
+    Prod f (Elem f as :*: g) as
+
+  -- | Traverse a foldable functor product with a RankN applicative function,
+  -- mapping over each value and sequencing the effects.
+  --
+  -- This is the generalization of 'rtraverse'.
+  traverseProd ::
+    forall g h as m.
+    Applicative m =>
+    (forall a. g a -> m (h a)) ->
+    Prod f g as ->
+    m (Prod f h as)
+  traverseProd = case fmapIdent @as of
+    Refl -> htraverse (sing @IdSym0)
+
+  -- | Zip together two foldable functor products with a Rank-N function.
+  zipWithProd ::
+    (forall a. g a -> h a -> j a) ->
+    Prod f g as ->
+    Prod f h as ->
+    Prod f j as
+  zipWithProd f xs ys = imapProd (\i x -> f x (indexProd i ys)) xs
+
+  -- | Traverse a foldable functor product with a type-changing function.
+  htraverse ::
+    Applicative m =>
+    Sing ff ->
+    (forall a. g a -> m (h (ff @@ a))) ->
+    Prod f g as ->
+    m (Prod f h (Fmap ff as))
+
+  -- | A 'Lens' into an item in a foldable functor product, given its
+  -- index.
+  --
+  -- This roughly generalizes 'rlens'.
+  ixProd ::
+    Elem f as a ->
+    Lens' (Prod f g as) (g a)
+
+  -- | Fold a functor product into a 'Rec'.
+  toRec :: Prod f g as -> Rec g (ToList as)
+
+  -- | Get a 'PureProd' instance from a foldable functor product
+  -- providing its shape.
+  withPureProd ::
+    Prod f g as ->
+    (PureProd f as => r) ->
+    r
+
+-- | Create @'Prod' f@ if you can give a @g a@ for every slot.
+class PureProd f as where
+  pureProd :: (forall a. g a) -> Prod f g as
+
+-- | Create @'Prod' f@ if you can give a @g a@ for every slot, given some
+-- constraint.
+class PureProdC f c as where
+  pureProdC :: (forall a. c a => g a) -> Prod f g as
+
+-- | Pair up each item in a @'Prod' f@ with a witness that @f a@ satisfies
+-- some constraint.
+class ReifyConstraintProd f c g as where
+  reifyConstraintProd :: Prod f g as -> Prod f (Dict c V.:. g) as
+
+data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
+data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
+type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
+
+type instance Apply (ElemSym0 f) as = ElemSym1 f as
+type instance Apply (ElemSym1 f as) a = Elem f as a
+
+data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> f k ~> Type
+data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type
+type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as
+
+type instance Apply (ProdSym0 f) g = ProdSym1 f g
+type instance Apply (ProdSym1 f g) as = Prod f g as
+
+-- | A convenient wrapper over 'V.AllConstrained' that works for any
+-- Foldable @f@.
+type AllConstrainedProd c as = V.AllConstrained c (ToList as)
+
+-- | Create a 'Shape' given an instance of 'PureProd'.
+pureShape :: PureProd f as => Shape f as
+pureShape = pureProd Proxy
+
+-- | Generate a 'Prod' of indices for an @as@.
+indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
+indices = imapProd const pureShape
+
+-- | Convert a @'Sing' as@ into a @'Shape' f as@, witnessing the shape of
+-- of @as@ but dropping all of its values.
+singShape ::
+  FProd f =>
+  Sing as ->
+  Shape f as
+singShape = mapProd (const Proxy) . singProd
+
+-- | Map a RankN function over a 'Prod'.  The generalization of 'rmap'.
+mapProd ::
+  FProd f =>
+  (forall a. g a -> h a) ->
+  Prod f g as ->
+  Prod f h as
+mapProd f = runIdentity . traverseProd (Identity . f)
+
+-- | Zip together the values in two 'Prod's.
+zipProd ::
+  FProd f =>
+  Prod f g as ->
+  Prod f h as ->
+  Prod f (g :*: h) as
+zipProd = zipWithProd (:*:)
+
+-- | Map a type-changing function over every item in a 'Prod'.
+hmap ::
+  FProd f =>
+  Sing ff ->
+  (forall a. g a -> h (ff @@ a)) ->
+  Prod f g as ->
+  Prod f h (Fmap ff as)
+hmap ff f = runIdentity . htraverse ff (Identity . f)
+
+-- | 'mapProd', but with access to the index at each element.
+imapProd ::
+  FProd f =>
+  (forall a. Elem f as a -> g a -> h a) ->
+  Prod f g as ->
+  Prod f h as
+imapProd f = mapProd (\(i :*: x) -> f i x) . withIndices
+
+-- | Extract the item from the container witnessed by the 'Elem'
+indexSing ::
+  forall f as a.
+  FProd f =>
+  -- | Witness
+  Elem f as a ->
+  -- | Collection
+  Sing as ->
+  Sing a
+indexSing i = indexProd i . singProd
+
+-- | Use an 'Elem' to index a value out of a 'Prod'.
+indexProd ::
+  FProd f =>
+  Elem f as a ->
+  Prod f g as ->
+  g a
+indexProd i = view (ixProd i)
+
+-- | 'traverseProd', but with access to the index at each element.
+itraverseProd ::
+  (FProd f, Applicative m) =>
+  (forall a. Elem f as a -> g a -> m (h a)) ->
+  Prod f g as ->
+  m (Prod f h as)
+itraverseProd f = traverseProd (\(i :*: x) -> f i x) . withIndices
+
+-- | 'foldMapProd', but with access to the index at each element.
+ifoldMapProd ::
+  (FProd f, Monoid m) =>
+  (forall a. Elem f as a -> g a -> m) ->
+  Prod f g as ->
+  m
+ifoldMapProd f = getConst . itraverseProd (\i -> Const . f i)
+
+-- | Map a RankN function over a 'Prod' and collect the results as
+-- a 'Monoid'.
+foldMapProd ::
+  (FProd f, Monoid m) =>
+  (forall a. g a -> m) ->
+  Prod f g as ->
+  m
+foldMapProd f = ifoldMapProd (const f)
+
+-- | 'foldMapSing' but with access to the index.
+ifoldMapSing ::
+  forall f k (as :: f k) m.
+  (FProd f, Monoid m) =>
+  (forall a. Elem f as a -> Sing a -> m) ->
+  Sing as ->
+  m
+ifoldMapSing f = ifoldMapProd f . singProd
+
+-- | A 'foldMap' over all items in a collection.
+foldMapSing ::
+  forall f k (as :: f k) m.
+  (FProd f, Monoid m) =>
+  (forall (a :: k). Sing a -> m) ->
+  Sing as ->
+  m
+foldMapSing f = ifoldMapSing (const f)
+
+-- | Rearrange or permute the items in a 'Prod' based on a 'Prod' of
+-- indices.
+--
+-- @
+-- 'selectProd' ('IS' 'IZ' ':&' IZ :& 'RNil') ("hi" :& "bye" :& "ok" :& RNil)
+--      == "bye" :& "hi" :& RNil
+-- @
+selectProd ::
+  FProd f =>
+  Prod f (Elem f as) bs ->
+  Prod f g as ->
+  Prod f g bs
+selectProd is xs = mapProd (`indexProd` xs) is
+
+-- | An implementation of equality testing for all 'FProd' instances, as
+-- long as each of the items are instances of 'Eq'.
+eqProd ::
+  (FProd f, ReifyConstraintProd f Eq g as) =>
+  Prod f g as ->
+  Prod f g as ->
+  Bool
+eqProd xs =
+  getAll
+    . foldMapProd getConst
+    . zipWithProd
+      (\(V.Compose (Dict x)) y -> Const (All (x == y)))
+      (reifyConstraintProd @_ @Eq xs)
+
+-- | An implementation of order comparison for all 'FProd' instances, as
+-- long as each of the items are instances of 'Ord'.
+compareProd ::
+  (FProd f, ReifyConstraintProd f Ord g as) =>
+  Prod f g as ->
+  Prod f g as ->
+  Ordering
+compareProd xs =
+  foldMapProd getConst
+    . zipWithProd
+      (\(V.Compose (Dict x)) y -> Const (compare x y))
+      (reifyConstraintProd @_ @Ord xs)
+
+-- | Construct a 'Prod' purely by providing a generating function for each
+-- index.
+generateProd ::
+  (FProd f, PureProd f as) =>
+  (forall a. Elem f as a -> g a) ->
+  Prod f g as
+generateProd f = mapProd f indices
+
+-- | Construct a 'Prod' in an 'Applicative' context by providing
+-- a generating function for each index.
+generateProdA ::
+  (FProd f, PureProd f as, Applicative m) =>
+  (forall a. Elem f as a -> m (g a)) ->
+  m (Prod f g as)
+generateProdA f = traverseProd f indices
+
+-- | Witness an item in a type-level list by providing its index.
+--
+-- The number of 'IS's correspond to the item's position in the list.
+--
+-- @
+-- 'IZ'         :: 'Index' '[5,10,2] 5
+-- 'IS' 'IZ'      :: 'Index' '[5,10,2] 10
+-- 'IS' ('IS' 'IZ') :: 'Index' '[5,10,2] 2
+-- @
+data Index :: [k] -> k -> Type where
+  IZ :: Index (a ': as) a
+  IS :: Index bs a -> Index (b ': bs) a
+
+deriving instance Show (Index as a)
+deriving instance Eq (Index as a)
+deriving instance Ord (Index as a)
+
+-- | Kind-indexed singleton for 'Index'.
+data SIndex (as :: [k]) (a :: k) :: Index as a -> Type where
+  SIZ :: SIndex (a ': as) a 'IZ
+  SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)
+
+deriving instance Show (SIndex as a i)
+
+type instance Sing = SIndex as a :: Index as a -> Type
+
+instance SingI 'IZ where
+  sing = SIZ
+
+instance SingI i => SingI ('IS i) where
+  sing = SIS sing
+
+instance SingKind (Index as a) where
+  type Demote (Index as a) = Index as a
+  fromSing = \case
+    SIZ -> IZ
+    SIS j -> IS (fromSing j)
+  toSing i = go i SomeSing
+    where
+      go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
+      go = \case
+        IZ -> ($ SIZ)
+        IS j -> \f -> go j (f . SIS)
+
+instance SDecide (Index as a) where
+  (%~) = \case
+    SIZ -> \case
+      SIZ -> Proved Refl
+      SIS _ -> Disproved $ \case {}
+    SIS i' -> \case
+      SIZ -> Disproved $ \case {}
+      SIS j' -> case i' %~ j' of
+        Proved Refl -> Proved Refl
+        Disproved v -> Disproved $ \case Refl -> v Refl
+
+instance FProd [] where
+  type Elem [] = Index
+  type Prod [] = Rec
+
+  singProd = \case
+    SNil -> RNil
+    x `SCons` xs -> x :& singProd xs
+
+  prodSing = \case
+    RNil -> SNil
+    x :& xs -> x `SCons` prodSing xs
+
+  traverseProd ::
+    forall g h m as.
+    Applicative m =>
+    (forall a. g a -> m (h a)) ->
+    Prod [] g as ->
+    m (Prod [] h as)
+  traverseProd f = go
+    where
+      go :: Prod [] g bs -> m (Prod [] h bs)
+      go = \case
+        RNil -> pure RNil
+        x :& xs -> (:&) <$> f x <*> go xs
+
+  zipWithProd ::
+    forall g h j as.
+    () =>
+    (forall a. g a -> h a -> j a) ->
+    Prod [] g as ->
+    Prod [] h as ->
+    Prod [] j as
+  zipWithProd f = go
+    where
+      go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
+      go = \case
+        RNil -> \case
+          RNil -> RNil
+        x :& xs -> \case
+          y :& ys -> f x y :& go xs ys
+
+  htraverse ::
+    forall ff g h as m.
+    Applicative m =>
+    Sing ff ->
+    (forall a. g a -> m (h (ff @@ a))) ->
+    Prod [] g as ->
+    m (Prod [] h (Fmap ff as))
+  htraverse _ f = go
+    where
+      go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
+      go = \case
+        RNil -> pure RNil
+        x :& xs -> (:&) <$> f x <*> go xs
+
+  withIndices = \case
+    RNil -> RNil
+    x :& xs -> (IZ :*: x) :& mapProd (\(i :*: y) -> IS i :*: y) (withIndices xs)
+
+  ixProd ::
+    forall g as a.
+    () =>
+    Elem [] as a ->
+    Lens' (Prod [] g as) (g a)
+  ixProd i0 (f :: g a -> h (g a)) = go i0
+    where
+      go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
+      go = \case
+        IZ -> \case
+          x :& xs -> (:& xs) <$> f x
+        IS i -> \case
+          x :& xs -> (x :&) <$> go i xs
+
+  toRec = id
+
+  withPureProd = withPureProdList
+
+-- | A stronger version of 'withPureProd' for 'Rec', providing
+-- a 'RecApplicative' instance as well.
+withPureProdList ::
+  Rec f as ->
+  ((RecApplicative as, PureProd [] as) => r) ->
+  r
+withPureProdList = \case
+  RNil -> id
+  _ :& xs -> withPureProdList xs
+
+instance RecApplicative as => PureProd [] as where
+  pureProd = rpure
+
+instance RPureConstrained c as => PureProdC [] c as where
+  pureProdC = rpureConstrained @c
+
+instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where
+  reifyConstraintProd = reifyConstraint @c
+
+-- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
+-- 'Just'.
+data IJust :: Maybe k -> k -> Type where
+  IJust :: IJust ('Just a) a
+
+deriving instance Show (IJust as a)
+deriving instance Read (IJust ('Just a) a)
+deriving instance Eq (IJust as a)
+deriving instance Ord (IJust as a)
+
+-- | Kind-indexed singleton for 'IJust'.
+data SIJust (as :: Maybe k) (a :: k) :: IJust as a -> Type where
+  SIJust :: SIJust ('Just a) a 'IJust
+
+deriving instance Show (SIJust as a i)
+
+type instance Sing = SIJust as a :: IJust as a -> Type
+
+instance SingI 'IJust where
+  sing = SIJust
+
+instance SingKind (IJust as a) where
+  type Demote (IJust as a) = IJust as a
+  fromSing SIJust = IJust
+  toSing IJust = SomeSing SIJust
+
+instance SDecide (IJust as a) where
+  SIJust %~ SIJust = Proved Refl
+
+-- | A @'PMaybe' f 'Nothing@ contains nothing, and a @'PMaybe' f ('Just a)@
+-- contains an @f a@.
+--
+-- In practice this can be useful to write polymorphic
+-- functions/abstractions that contain an argument that can be "turned off"
+-- for different instances.
+data PMaybe :: (k -> Type) -> Maybe k -> Type where
+  PNothing :: PMaybe f 'Nothing
+  PJust :: f a -> PMaybe f ('Just a)
+
+instance ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) where
+  showsPrec d xs = case reifyConstraintProd @_ @Show xs of
+    PNothing -> showString "PNothing"
+    PJust (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PJust" d x
+instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
+  (==) = eqProd
+instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where
+  compare = compareProd
+
+instance FProd Maybe where
+  type Elem Maybe = IJust
+  type Prod Maybe = PMaybe
+
+  singProd = \case
+    SNothing -> PNothing
+    SJust x -> PJust x
+  prodSing = \case
+    PNothing -> SNothing
+    PJust x -> SJust x
+  withIndices = \case
+    PNothing -> PNothing
+    PJust x -> PJust (IJust :*: x)
+  traverseProd f = \case
+    PNothing -> pure PNothing
+    PJust x -> PJust <$> f x
+  zipWithProd f = \case
+    PNothing -> \case
+      PNothing -> PNothing
+    PJust x -> \case
+      PJust y -> PJust (f x y)
+  htraverse _ f = \case
+    PNothing -> pure PNothing
+    PJust x -> PJust <$> f x
+  ixProd = \case
+    IJust -> \f -> \case
+      PJust x -> PJust <$> f x
+  toRec = \case
+    PNothing -> RNil
+    PJust x -> x :& RNil
+  withPureProd = \case
+    PNothing -> id
+    PJust _ -> id
+
+instance PureProd Maybe 'Nothing where
+  pureProd _ = PNothing
+instance PureProd Maybe ('Just a) where
+  pureProd = PJust
+
+instance PureProdC Maybe c 'Nothing where
+  pureProdC _ = PNothing
+instance c a => PureProdC Maybe c ('Just a) where
+  pureProdC = PJust
+
+instance ReifyConstraintProd Maybe c g 'Nothing where
+  reifyConstraintProd PNothing = PNothing
+instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where
+  reifyConstraintProd (PJust x) = PJust (V.Compose (Dict x))
+
+-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
+-- is 'Right'.
+data IRight :: Either j k -> k -> Type where
+  IRight :: IRight ('Right a) a
+
+deriving instance Show (IRight as a)
+deriving instance Read (IRight ('Right a) a)
+deriving instance Eq (IRight as a)
+deriving instance Ord (IRight as a)
+
+-- | Kind-indexed singleton for 'IRight'.
+data SIRight (as :: Either j k) (a :: k) :: IRight as a -> Type where
+  SIRight :: SIRight ('Right a) a 'IRight
+
+deriving instance Show (SIRight as a i)
+
+type instance Sing = SIRight as a :: IRight as a -> Type
+
+instance SingI 'IRight where
+  sing = SIRight
+
+instance SingKind (IRight as a) where
+  type Demote (IRight as a) = IRight as a
+  fromSing SIRight = IRight
+  toSing IRight = SomeSing SIRight
+
+instance SDecide (IRight as a) where
+  SIRight %~ SIRight = Proved Refl
+
+-- | A @'PEither' f ('Left e)@ contains @'Sing' e@, and a @'PMaybe' f ('Right a)@
+-- contains an @f a@.
+--
+-- In practice this can be useful in the same situatinos that 'PMaybe' can,
+-- but with an extra value in the case where value @f@ is "turned off" with
+-- 'Left'.
+data PEither :: (k -> Type) -> Either j k -> Type where
+  PLeft :: Sing e -> PEither f ('Left e)
+  PRight :: f a -> PEither f ('Right a)
+
+instance (SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as) where
+  showsPrec d xs = case reifyConstraintProd @_ @Show xs of
+    PLeft e -> showsUnaryWith go "PLeft" d e
+    PRight (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PRight" d x
+    where
+      go (fromIntegral -> FromSing i) x (T.pack -> FromSing str) = T.unpack . fromSing $ sShowsPrec i x str
+
+instance FProd (Either j) where
+  type Elem (Either j) = IRight
+  type Prod (Either j) = PEither
+
+  singProd = \case
+    SLeft e -> PLeft e
+    SRight x -> PRight x
+  prodSing = \case
+    PLeft e -> SLeft e
+    PRight x -> SRight x
+  withIndices = \case
+    PLeft e -> PLeft e
+    PRight x -> PRight (IRight :*: x)
+  traverseProd f = \case
+    PLeft e -> pure (PLeft e)
+    PRight x -> PRight <$> f x
+  zipWithProd f = \case
+    PLeft e -> \case
+      PLeft _ -> PLeft e
+    PRight x -> \case
+      PRight y -> PRight (f x y)
+  htraverse _ f = \case
+    PLeft e -> pure (PLeft e)
+    PRight x -> PRight <$> f x
+  ixProd = \case
+    IRight -> \f -> \case
+      PRight x -> PRight <$> f x
+  toRec = \case
+    PLeft _ -> RNil
+    PRight x -> x :& RNil
+  withPureProd = \case
+    PLeft Sing -> id
+    PRight _ -> id
+
+instance SingI e => PureProd (Either j) ('Left e) where
+  pureProd _ = PLeft sing
+instance PureProd (Either j) ('Right a) where
+  pureProd = PRight
+
+instance SingI e => PureProdC (Either j) c ('Left e) where
+  pureProdC _ = PLeft sing
+instance c a => PureProdC (Either j) c ('Right a) where
+  pureProdC = PRight
+
+instance ReifyConstraintProd (Either j) c g ('Left e) where
+  reifyConstraintProd (PLeft e) = PLeft e
+instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where
+  reifyConstraintProd (PRight x) = PRight (V.Compose (Dict x))
+
+-- | Witness an item in a type-level 'NonEmpty' by either indicating that
+-- it is the "head", or by providing an index in the "tail".
+data NEIndex :: NonEmpty k -> k -> Type where
+  NEHead :: NEIndex (a ':| as) a
+  NETail :: Index as a -> NEIndex (b ':| as) a
+
+deriving instance Show (NEIndex as a)
+deriving instance Eq (NEIndex as a)
+deriving instance Ord (NEIndex as a)
+
+-- | Kind-indexed singleton for 'NEIndex'.
+data SNEIndex (as :: NonEmpty k) (a :: k) :: NEIndex as a -> Type where
+  SNEHead :: SNEIndex (a ':| as) a 'NEHead
+  SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
+
+deriving instance Show (SNEIndex as a i)
+
+type instance Sing = SNEIndex as a :: NEIndex as a -> Type
+
+instance SingI 'NEHead where
+  sing = SNEHead
+
+instance SingI i => SingI ('NETail i) where
+  sing = SNETail sing
+
+instance SingKind (NEIndex as a) where
+  type Demote (NEIndex as a) = NEIndex as a
+  fromSing = \case
+    SNEHead -> NEHead
+    SNETail i -> NETail $ fromSing i
+  toSing = \case
+    NEHead -> SomeSing SNEHead
+    NETail i -> withSomeSing i $ SomeSing . SNETail
+
+instance SDecide (NEIndex as a) where
+  (%~) = \case
+    SNEHead -> \case
+      SNEHead -> Proved Refl
+      SNETail _ -> Disproved $ \case {}
+    SNETail i -> \case
+      SNEHead -> Disproved $ \case {}
+      SNETail j -> case i %~ j of
+        Proved Refl -> Proved Refl
+        Disproved v -> Disproved $ \case Refl -> v Refl
+
+-- | A non-empty version of 'Rec'.
+data NERec :: (k -> Type) -> NonEmpty k -> Type where
+  (:&|) :: f a -> Rec f as -> NERec f (a ':| as)
+
+infixr 5 :&|
+
+deriving instance
+  (Show (f a), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a ':| as))
+deriving instance (Eq (f a), Eq (Rec f as)) => Eq (NERec f (a ':| as))
+deriving instance (Ord (f a), Ord (Rec f as)) => Ord (NERec f (a ':| as))
+
+instance FProd NonEmpty where
+  type Elem NonEmpty = NEIndex
+  type Prod NonEmpty = NERec
+
+  singProd (x NE.:%| xs) = x :&| singProd xs
+  prodSing (x :&| xs) = x NE.:%| prodSing xs
+  withIndices (x :&| xs) =
+    (NEHead :*: x)
+      :&| mapProd (\(i :*: y) -> NETail i :*: y) (withIndices xs)
+  traverseProd f (x :&| xs) =
+    (:&|) <$> f x <*> traverseProd f xs
+  zipWithProd f (x :&| xs) (y :&| ys) = f x y :&| zipWithProd f xs ys
+  htraverse ff f (x :&| xs) =
+    (:&|) <$> f x <*> htraverse ff f xs
+  ixProd = \case
+    NEHead -> \f -> \case
+      x :&| xs -> (:&| xs) <$> f x
+    NETail i -> \f -> \case
+      x :&| xs -> (x :&|) <$> ixProd i f xs
+  toRec (x :&| xs) = x :& xs
+  withPureProd (x :&| xs) = withPureProdNE x xs
+
+-- | A stronger version of 'withPureProd' for 'NERec', providing
+-- a 'RecApplicative' instance as well.
+withPureProdNE ::
+  f a ->
+  Rec f as ->
+  ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r) ->
+  r
+withPureProdNE _ = withPureProdList
+
+instance RecApplicative as => PureProd NonEmpty (a ':| as) where
+  pureProd x = x :&| pureProd x
+
+instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where
+  pureProdC x = x :&| pureProdC @_ @c x
+
+instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where
+  reifyConstraintProd (x :&| xs) =
+    V.Compose (Dict x)
+      :&| reifyConstraintProd @_ @c xs
+
+-- | Test if two indices point to the same item in a list.
+--
+-- We have to return a 'Maybe' here instead of a 'Decision', because it
+-- might be the case that the same item might be duplicated in a list.
+-- Therefore, even if two indices are different, we cannot prove that the
+-- values they point to are different.
+sameIndexVal ::
+  Index as a ->
+  Index as b ->
+  Maybe (a :~: b)
+sameIndexVal = \case
+  IZ -> \case
+    IZ -> Just Refl
+    IS _ -> Nothing
+  IS i -> \case
+    IZ -> Nothing
+    IS j -> sameIndexVal i j <&> \case Refl -> Refl
+
+-- | Test if two indices point to the same item in a non-empty list.
+--
+-- We have to return a 'Maybe' here instead of a 'Decision', because it
+-- might be the case that the same item might be duplicated in a list.
+-- Therefore, even if two indices are different, we cannot prove that the
+-- values they point to are different.
+sameNEIndexVal ::
+  NEIndex as a ->
+  NEIndex as b ->
+  Maybe (a :~: b)
+sameNEIndexVal = \case
+  NEHead -> \case
+    NEHead -> Just Refl
+    NETail _ -> Nothing
+  NETail i -> \case
+    NEHead -> Nothing
+    NETail j -> sameIndexVal i j <&> \case Refl -> Refl
+
+-- | Trivially witness an item in the second field of a type-level tuple.
+data ISnd :: (j, k) -> k -> Type where
+  ISnd :: ISnd '(a, b) b
+
+deriving instance Show (ISnd as a)
+deriving instance Read (ISnd '(a, b) b)
+deriving instance Eq (ISnd as a)
+deriving instance Ord (ISnd as a)
+
+-- | Kind-indexed singleton for 'ISnd'.
+data SISnd (as :: (j, k)) (a :: k) :: ISnd as a -> Type where
+  SISnd :: SISnd '(a, b) b 'ISnd
+
+deriving instance Show (SISnd as a i)
+
+type instance Sing = SISnd as a :: ISnd as a -> Type
+
+instance SingI 'ISnd where
+  sing = SISnd
+
+instance SingKind (ISnd as a) where
+  type Demote (ISnd as a) = ISnd as a
+  fromSing SISnd = ISnd
+  toSing ISnd = SomeSing SISnd
+
+instance SDecide (ISnd as a) where
+  SISnd %~ SISnd = Proved Refl
+
+-- | A 'PTup' tuples up some singleton with some value; a @'PTup' f '(w,
+-- a)@ contains a @'Sing' w@ and an @f a@.
+--
+-- This can be useful for carrying along some witness aside a functor
+-- value.
+data PTup :: (k -> Type) -> (j, k) -> Type where
+  PTup :: Sing w -> f a -> PTup f '(w, a)
+
+deriving instance (Show (Sing w), Show (f a)) => Show (PTup f '(w, a))
+deriving instance (Read (Sing w), Read (f a)) => Read (PTup f '(w, a))
+deriving instance (Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a))
+deriving instance (Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a))
+
+instance FProd ((,) j) where
+  type Elem ((,) j) = ISnd
+  type Prod ((,) j) = PTup
+
+  singProd (STuple2 w x) = PTup w x
+  prodSing (PTup w x) = STuple2 w x
+  withIndices (PTup w x) = PTup w (ISnd :*: x)
+  traverseProd f (PTup w x) = PTup w <$> f x
+  zipWithProd f (PTup w x) (PTup _ y) = PTup w (f x y)
+  htraverse _ f (PTup w x) = PTup w <$> f x
+  ixProd ISnd f (PTup w x) = PTup w <$> f x
+  toRec (PTup _ x) = x :& RNil
+  withPureProd (PTup Sing _) x = x
+
+instance SingI w => PureProd ((,) j) '(w, a) where
+  pureProd = PTup sing
+
+instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
+  pureProdC = PTup sing
+
+instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where
+  reifyConstraintProd (PTup w x) = PTup w $ V.Compose (Dict x)
+
+-- | Trivially witness the item held in an 'Identity'.
+--
+-- @since 0.1.3.0
+data IIdentity :: Identity k -> k -> Type where
+  IId :: IIdentity ('Identity x) x
+
+deriving instance Show (IIdentity as a)
+deriving instance Read (IIdentity ('Identity a) a)
+deriving instance Eq (IIdentity as a)
+deriving instance Ord (IIdentity as a)
+
+-- | Kind-indexed singleton for 'IIdentity'.
+--
+-- @since 0.1.5.0
+data SIIdentity (as :: Identity k) (a :: k) :: IIdentity as a -> Type where
+  SIId :: SIIdentity ('Identity a) a 'IId
+
+deriving instance Show (SIIdentity as a i)
+
+type instance Sing = SIIdentity as a :: IIdentity as a -> Type
+
+instance SingI 'IId where
+  sing = SIId
+
+instance SingKind (IIdentity as a) where
+  type Demote (IIdentity as a) = IIdentity as a
+  fromSing SIId = IId
+  toSing IId = SomeSing SIId
+
+instance SDecide (IIdentity as a) where
+  SIId %~ SIId = Proved Refl
+
+-- | A 'PIdentity' is a trivial functor product; it is simply the functor,
+-- itself, alone.  @'PIdentity' f ('Identity' a)@ is simply @f a@.  This
+-- may be useful in conjunction with other combinators.
+data PIdentity :: (k -> Type) -> Identity k -> Type where
+  PIdentity :: f a -> PIdentity f ('Identity a)
+
+deriving instance Show (f a) => Show (PIdentity f ('Identity a))
+deriving instance Read (f a) => Read (PIdentity f ('Identity a))
+deriving instance Eq (f a) => Eq (PIdentity f ('Identity a))
+deriving instance Ord (f a) => Ord (PIdentity f ('Identity a))
+
+instance FProd Identity where
+  type Elem Identity = IIdentity
+  type Prod Identity = PIdentity
+
+  singProd (SIdentity x) = PIdentity x
+  prodSing (PIdentity x) = SIdentity x
+  withIndices (PIdentity x) = PIdentity (IId :*: x)
+  traverseProd f (PIdentity x) = PIdentity <$> f x
+  zipWithProd f (PIdentity x) (PIdentity y) = PIdentity (f x y)
+  htraverse _ f (PIdentity x) = PIdentity <$> f x
+  ixProd IId f (PIdentity x) = PIdentity <$> f x
+  toRec (PIdentity x) = x :& RNil
+  withPureProd (PIdentity _) x = x
+
+instance PureProd Identity ('Identity a) where
+  pureProd = PIdentity
+
+instance c a => PureProdC Identity c ('Identity a) where
+  pureProdC = PIdentity
+
+instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where
+  reifyConstraintProd (PIdentity x) = PIdentity $ V.Compose (Dict x)
+
+-- | Produce an 'Index' from an 'RElem' constraint.
+rElemIndex ::
+  forall r rs i.
+  (RElem r rs i, PureProd [] rs) =>
+  Index rs r
+rElemIndex = rgetC indices
+
+-- | Use an 'Index' to inject an @f a@ into a 'CoRec'.
+toCoRec ::
+  forall k (as :: [k]) a f.
+  (RecApplicative as, FoldRec as as) =>
+  Index as a ->
+  f a ->
+  CoRec f as
+toCoRec = \case
+  IZ -> CoRec
+  IS i -> \x -> fromJust . firstField $ mapProd (go i x) indices
+  where
+    go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c
+    go i x j = case sameIndexVal (IS i) j of
+      Just Refl -> V.Compose (Just x)
+      Nothing -> V.Compose Nothing
+
+-- | If we have @'Index' as a@, we should also be able to create an item
+-- that would require @'RElem' a as ('V.RIndex' as a)@.  Along with
+-- 'rElemIndex', this essentially converts between the indexing system in
+-- this library and the indexing system of /vinyl/.
+indexRElem ::
+  (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as) =>
+  Index as a ->
+  (RElem a as (V.RIndex a as) => r) ->
+  r
+indexRElem i = case toCoRec i x of
+  CoRec y -> case x %~ y of
+    Proved Refl -> id
+    Disproved _ -> \_ -> errorWithoutStackTrace "why :|"
   where
     x = sing
diff --git a/src/Data/Type/Functor/XProduct.hs b/src/Data/Type/Functor/XProduct.hs
--- a/src/Data/Type/Functor/XProduct.hs
+++ b/src/Data/Type/Functor/XProduct.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE PatternSynonyms     #-}
-{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Functor.XProduct
@@ -26,34 +26,50 @@
 -- provides an alternative interface that may be more convenient in some
 -- situations, in the same way that 'XRec' can be more convenient than
 -- 'Rec' in some situations.
---
 module Data.Type.Functor.XProduct (
-    XProd
-  , fromXProd
-  , toXProd
+  XProd,
+  fromXProd,
+  toXProd,
+
   -- * Functions
-  , mapProdX, mapProdXEndo
-  , imapProdX, zipWithProdX
-  , ixProdX, traverseProdX, traverseProdXEndo, itraverseProdX
-  , foldMapProdX, ifoldMapProdX
+  mapProdX,
+  mapProdXEndo,
+  imapProdX,
+  zipWithProdX,
+  ixProdX,
+  traverseProdX,
+  traverseProdXEndo,
+  itraverseProdX,
+  foldMapProdX,
+  ifoldMapProdX,
+
   -- * Instances
-  , XRec, pattern (::&), pattern XRNil
-  , XMaybe, pattern XNothing, pattern XJust
-  , XEither, pattern XLeft, pattern XRight
-  , XNERec, pattern (::&|)
-  , XTup, pattern XTup
-  , XIdentity, pattern XIdentity
-  ) where
+  XRec,
+  pattern (::&),
+  pattern XRNil,
+  XMaybe,
+  pattern XNothing,
+  pattern XJust,
+  XEither,
+  pattern XLeft,
+  pattern XRight,
+  XNERec,
+  pattern (::&|),
+  XTup,
+  pattern XTup,
+  XIdentity,
+  pattern XIdentity,
+) where
 
-import           Data.Functor.Identity
-import           Data.Kind
-import           Data.List.NonEmpty        (NonEmpty(..))
-import           Data.Singletons
-import           Data.Type.Functor.Product
-import           Data.Vinyl
-import           Data.Vinyl.XRec
-import           Lens.Micro
-import qualified Data.Vinyl.Functor        as V
+import Data.Functor.Identity
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Singletons
+import Data.Type.Functor.Product
+import Data.Vinyl
+import qualified Data.Vinyl.Functor as V
+import Data.Vinyl.XRec
+import Lens.Micro
 
 -- | Generalize 'XRec' to work over any foldable @f@ that implements
 -- 'FProd'.  See 'Prod' and 'FProd' for more information.
@@ -61,116 +77,129 @@
 
 -- | Convert an 'XProd' back into a regular ol' 'Prod'.
 fromXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => XProd f g as -> Prod f g as
-fromXProd = zipWithProd (\(V.Lift u) x -> u x)
-              (pureProdC @_ @(IsoHKD g) (V.Lift (unHKD . unX)))
+fromXProd =
+  zipWithProd
+    (\(V.Lift u) x -> u x)
+    (pureProdC @_ @(IsoHKD g) (V.Lift (unHKD . unX)))
 
 -- | Convert a 'Prod' into a fancy 'XProd'.
 toXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => Prod f g as -> XProd f g as
-toXProd = zipWithProd (\(V.Lift u) x -> u x)
-              (pureProdC @_ @(IsoHKD g) (V.Lift (XData . toHKD)))
+toXProd =
+  zipWithProd
+    (\(V.Lift u) x -> u x)
+    (pureProdC @_ @(IsoHKD g) (V.Lift (XData . toHKD)))
 
 -- | Convenient wrapper over 'mapProd' that lets you deal with the
 -- "simplified" inner types.  Generalizes 'rmapX'.
-mapProdX
-    :: forall f g h as. FProd f
-    => (forall a. HKD g a -> HKD h a)
-    -> XProd f g as
-    -> XProd f h as
+mapProdX ::
+  forall f g h as.
+  FProd f =>
+  (forall a. HKD g a -> HKD h a) ->
+  XProd f g as ->
+  XProd f h as
 mapProdX f = mapProd $ \(XData x :: XData g a) -> XData (f @a x)
 
 -- | A version of 'mapProdX' that doesn't change the context @g@; this can
 -- be easier for type inference in some situations.  Generalizes
 -- 'rmapXEndo'.
-mapProdXEndo
-    :: forall f g as. FProd f
-    => (forall a. HKD g a -> HKD g a)
-    -> XProd f g as
-    -> XProd f g as
+mapProdXEndo ::
+  forall f g as.
+  FProd f =>
+  (forall a. HKD g a -> HKD g a) ->
+  XProd f g as ->
+  XProd f g as
 mapProdXEndo f = mapProd $ \(XData x :: XData g a) -> XData (f @a x)
 
 -- | A version of 'mapProdX' that passes along the index 'Elem' with each
 -- value.  This can help with type inference in some situations.
-imapProdX
-    :: forall f g h as. FProd f
-    => (forall a. Elem f as a -> HKD g a -> HKD h a)
-    -> XProd f g as
-    -> XProd f h as
+imapProdX ::
+  forall f g h as.
+  FProd f =>
+  (forall a. Elem f as a -> HKD g a -> HKD h a) ->
+  XProd f g as ->
+  XProd f h as
 imapProdX f = imapProd $ \i -> XData . f i . unX
 
 -- | Zip two 'XProd's together by supplying a function that works on their
 -- simplified 'HKD' values.
-zipWithProdX
-    :: forall f g h j as. FProd f
-    => (forall a. HKD g a -> HKD h a -> HKD j a)
-    -> XProd f g as
-    -> XProd f h as
-    -> XProd f j as
+zipWithProdX ::
+  forall f g h j as.
+  FProd f =>
+  (forall a. HKD g a -> HKD h a -> HKD j a) ->
+  XProd f g as ->
+  XProd f h as ->
+  XProd f j as
 zipWithProdX f = zipWithProd $ \(XData x :: XData g a) (XData y) -> XData (f @a x y)
 
 -- | Given an index into an 'XProd', provides a lens into the simplified
 -- item that that index points to.
-ixProdX
-    :: FProd f
-    => Elem f as a
-    -> Lens' (XProd f g as) (HKD g a)
+ixProdX ::
+  FProd f =>
+  Elem f as a ->
+  Lens' (XProd f g as) (HKD g a)
 ixProdX i = ixProd i . (\f (XData x) -> XData <$> f x)
 
 -- | Convenient wrapper over 'traverseProd' that lets you deal with the
 -- "simplified" inner types.
-traverseProdX
-    :: forall f g h m as. (FProd f, Applicative m)
-    => (forall a. HKD g a -> m (HKD h a))
-    -> XProd f g as
-    -> m (XProd f h as)
+traverseProdX ::
+  forall f g h m as.
+  (FProd f, Applicative m) =>
+  (forall a. HKD g a -> m (HKD h a)) ->
+  XProd f g as ->
+  m (XProd f h as)
 traverseProdX f = traverseProd $ \(XData x :: XData g a) -> XData <$> f @a x
 
 -- | A version of 'traverseProdX' that doesn't change the context @g@; this can
 -- be easier for type inference in some situations.
-traverseProdXEndo
-    :: forall f g m as. (FProd f, Applicative m)
-    => (forall a. HKD g a -> m (HKD g a))
-    -> XProd f g as
-    -> m (XProd f g as)
+traverseProdXEndo ::
+  forall f g m as.
+  (FProd f, Applicative m) =>
+  (forall a. HKD g a -> m (HKD g a)) ->
+  XProd f g as ->
+  m (XProd f g as)
 traverseProdXEndo f = traverseProd $ \(XData x :: XData g a) -> XData <$> f @a x
 
 -- | A version of 'traverseProdX' that passes along the index 'Elem' with
 -- each value.  This can help with type inference in some situations.
-itraverseProdX
-    :: forall f g h m as. (FProd f, Applicative m)
-    => (forall a. Elem f as a -> HKD g a -> m (HKD h a))
-    -> XProd f g as
-    -> m (XProd f h as)
+itraverseProdX ::
+  forall f g h m as.
+  (FProd f, Applicative m) =>
+  (forall a. Elem f as a -> HKD g a -> m (HKD h a)) ->
+  XProd f g as ->
+  m (XProd f h as)
 itraverseProdX f = itraverseProd $ \i -> fmap XData . f i . unX
 
 -- | Convenient wrapper over 'foldMapProd' that lets you deal with the
 -- "simplified" inner types.
-foldMapProdX
-    :: forall f g m as. (FProd f, Monoid m)
-    => (forall a. HKD g a -> m)
-    -> XProd f g as
-    -> m
+foldMapProdX ::
+  forall f g m as.
+  (FProd f, Monoid m) =>
+  (forall a. HKD g a -> m) ->
+  XProd f g as ->
+  m
 foldMapProdX f = foldMapProd $ \(XData x :: XData g a) -> f @a x
 
 -- | A version of 'foldMapProdX' that passes along the index 'Elem' with
 -- each value.  This can help with type inference in some situations.
-ifoldMapProdX
-    :: forall f g m as. (FProd f, Monoid m)
-    => (forall a. Elem f as a -> HKD g a -> m)
-    -> XProd f g as
-    -> m
+ifoldMapProdX ::
+  forall f g m as.
+  (FProd f, Monoid m) =>
+  (forall a. Elem f as a -> HKD g a -> m) ->
+  XProd f g as ->
+  m
 ifoldMapProdX f = ifoldMapProd $ \i -> f i . unX
 
 -- | 'PMaybe' over 'HKD'-d types.
-type XMaybe f    = PMaybe (XData f)
+type XMaybe f = PMaybe (XData f)
 
 -- | 'PEither' over 'HKD'-d types.
-type XEither f   = PEither (XData f)
+type XEither f = PEither (XData f)
 
 -- | 'NERec' over 'HKD'-d types.
-type XNERec f    = NERec (XData f)
+type XNERec f = NERec (XData f)
 
 -- | 'PTup' over 'HKD'-d types.
-type XTup f      = PTup (XData f)
+type XTup f = PTup (XData f)
 
 -- | 'PIdentity' over 'HKD'-d types.
 type XIdentity f = PIdentity (XData f)
@@ -206,11 +235,10 @@
 pattern XIdentity :: HKD f a -> XIdentity f ('Identity a)
 pattern XIdentity x = PIdentity (XData x)
 
-{-# COMPLETE (::&|)    #-}
+{-# COMPLETE (::&|) #-}
 {-# COMPLETE XIdentity #-}
-{-# COMPLETE XJust     #-}
-{-# COMPLETE XLeft     #-}
-{-# COMPLETE XNothing  #-}
-{-# COMPLETE XRight    #-}
-{-# COMPLETE XTup      #-}
-
+{-# COMPLETE XJust #-}
+{-# COMPLETE XLeft #-}
+{-# COMPLETE XNothing #-}
+{-# COMPLETE XRight #-}
+{-# COMPLETE XTup #-}