diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,9 @@
 
 # Changelog
 
+* 4.7.0.1
+  - Added `Hashable` instances for `Many`.
+
 * 4.7.0.0
   - Removed `totally`. Added `CaseFunc1_`
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -11,159 +11,3 @@
 Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages.
 
 Iso, Lens and Prisms are provided in [data-diverse-lens](http://hackage.haskell.org/package/data-diverse-lens)
-
-# Changelog
-
-* 4.6.0.0
-  - Renamed `definitely` to `totally`.
-
-* 4.5.0.0
-  - Replaced usages of `KnownNat` with a new `NatToInt` class to avoid inefficient Integer https://github.com/louispan/data-diverse/issues/8.
-
-* 4.4.0.0
-  - Renamed `Unconstrained` to `C0`. Added `C2`, `C3`, `C4`, `C5`, `C6`.
-
-* 4.3.0.0
-  - Renamed `NoConstraint` to `Unconstrained`
-
-* 4.2.0.0
-  - Added `CaseFunc1` to allow `afmap` of with `Functor`, etc.
-  - `Which` is now also an instance of `AFoldable`.
-  - Added `NoConstraint` which is useful for `CaseFunc1` for unused constraints.
-  - Added `definitely`.
-
-* 4.1.0.0
-  - Removed `zilch`.
-
-* 4.0.0.0
-  - Renamed `prefix` to `consMany` and `postfix` to `snocMany`.
-
-* 3.1.0.0
-  - Removed `Read` instance for `Which []` since it is uninhabitable.
-  - `xxxTag` functions only rely on `UniqueMember`, not `UniqueLabelMember`
-
-* 3.0.0.0
-  - Renamed `fetch` to `grab` to avoid conflicting with Haxl.
-  - Removed unused type functions from removed splitting functions (Before,To,After,From,Length)
-  - Added `impossible'` and ability to diversify and reinterpret `Which '[Void]`
-  - Added `zilch`
-  - Removed `CanAppendUnique` (not useful).
-
-* 2.0.1.0
-  - Simplified type synonyms for `Which`. Added `Reinterpreted` constraint synonym.
-
-* 2.0.0.0
-  - Breaking change: the prime (xxx') version of functions are now consistently the simpler or non-polymorphic version.
-    - This is more consistent with `Control.Lens` as well.
-    - This means the following are swapped:
-      - `replace`, `replace'`
-      - `replaceL`, `replaceL'`
-      - `replaceTag`, `replaceTag'`
-      - `replaceN`, `replaceN'`
-      - `amend`, `amend'`
-      - `amendL`, `amendL'`
-      - `amendN`, `amendN'`
-  - Breaking change: Removed proxy argument from `fetchL/Tag/N`, `replaceXXX`, `selectL/Tag/N`, `amendXXX`, `pickL/Tag/N`, `trialL/Tag/N`
-    relying soley on `TypeApplications` and now requiring `AllowAmbiguousTypes`.
-    The `Proxy` is also removed from the Read/Show serialized format.
-  - Rearranged type variables in `fetchL/N`, `replaceL/Tag/N`, `pickL/Tag/N`, `trialL/Tag/N` type parameters,
-    so the type variable ordering is consistently label, orig to change, smaller to larger, ie. `l/n`, `x`, `y`, `xs`
-
-* 1.3.0.0
-  - Removed splitting operations added in 1.2.0.0
-  - added `xxxTag` version of label operations that also automatically untags the field.
-
-* 1.2.0.3
-  - `PolyKinds` for `Which`
-  - Removed cabal upper bounds
-
-* 1.2.0.2
-  - Added `insert`/`remove` for GHC < 8.2
-  - Removed type functions `UniqueMemberAt`, `MaybeUniqueMemberAt`
-
-* 1.2.0.1
-  - `insert`/`remove` is not available in GHC 8.2 onwards.
-
-* 1.2.0.0
-  - Rerranged type variable for xxxL and xxxN functions so that the
-    `x` inferrred from label `l` or index `n` is after `proxy`.
-    - This affects `fetch[L|N]`, `replace[L|N]`, `replace[L|N]'`, `pick[L|N]`
-  - Depends on at least containers-0.5.8.2 for `Data.Sequence.insertAt`
-  - Added splitting operations: `split[Before|After][|L|N]`, `inset[Before|After][|L|N]`,
-    `insert[Before|After][|L|N]`, `remove[Before|After][|L|N]`
-  - Renamed type function `Without` to `Remove` to be consistent with new `remove` method.
-
-* 1.1.0.0
-  - Added `CaseFunc` and `CaseFunc'` which replaces `CaseTypeable` (eg `CaseFunc @Typeable`)
-    <https://github.com/louispan/data-diverse/issues/6>
-  - Replaced `IsAll` constraint with `AllConstrained`.
-
-* 1.0.0.1
-  - Added `CaseTypeable'` as an example of polymorphic `Case` that doesn't change the type.
-
-* 1.0.0.0
-  - The exposed api shouldn't break, but there are a lot of internal changes.
-  - Added `AFunctor` which can map over the types in the 'Many'
-    <https://github.com/louispan/data-diverse/issues/5>.
-  - Added friendlier type synomyns `Collect` and `CollectN` for `collect` and `collectN`
-  - Expose type of 'Collector' and 'CollectorN'
-  - Replace type parameter `r` from `Case` typeclass with `CaseResult` type family.
-  - Replaced `CasesResult` type function with `IsAll` and `CasesResults` type functions.
-  - All `CaseXxx` type variables now end with r xs.
-  - All `CaseXxxN` type variables now end with r n xs.
-
-* 0.11.0.0
-  - Added `impossible` modelled after `Data.Void.absurd`
-    <https://github.com/louispan/data-diverse/issues/4>
-  - Removed `zilch` so `Which '[]` is uninhabited like `Data.Void.Void`, making 'impossible' safe to use.
-  - Removed `Monoid` and changed `Show`, `Read` and `Generic` instances for `Which '[]` to be partial
-    just like Data.Void.Void.
-  - Added `instance Reduce (Which '[]) (Switcher c '[] r)`, which follows from `impossible`.
-
-* 0.10.0.0
-  - Renamed `Switch` to `Switcher`. Switch is now a type synonym for `switch` constraints
-  - Added CasesResult type family to help infer the result of `cases`
-  - Added Semigroup and Monoid instances for all Many xs.
-  - Added Maybe versions of trial, and reinterpret
-  - Renamed `reinterpetN` to `reinterpretN'`
-  - Renamed `impossible` to `zilch`.
-  - Allowed `reintepret`ing and `diversify`ing `zilch` to `zilch`
-  - Removed zipped type variable from `Amend` constraints.
-  - Removed r type variable from `Reduce` typeclass.
-  - Rearranged type variables in `fetch`, `replace`, `pick`, `trial`, `Diversify` type parameters,
-    so the type variable ordering is consistently smaller to larger, ie. `x`, `xs`, `branch`, `tree`
-  - Added `diversify'` for allowing rearranging the types only.
-
-* 0.9.0.1
-  - Fixed GHC 8.2.1 test failure due to changed TypeRep show instance.
-
-* 0.9.0.0
-  - Breaking changes: Renamed Many.sliceL/R to Many.viewf/b
-  - Renamed TypeLevel.Internal.MissingImpl to IsUniqueImpl.
-  - Added postifx' with SnocUnique and append' with AppendUnique.
-  - Added Semigroup & Monoid instances for `Many '[]` and `Which '[]`
-  - Fixed GHC 8.2 compile error with importing GHC.Prim (Any)
-
-* 0.8.1.0
-  - Added NFData instance for Which.
-  - Forgot to expose Many.sliceL and Many.sliceR.
-
-* 0.8.0.0
-  - Changed internal representation to (Data.Seq Any) for a further 2x append speedup.
-  - Added NFData instance for Many.
-
-* 0.7.0.0
-  - Removed NOINLINE pragmas.
-  - Changed internal representation to (Int, Data.IntMap Any) for a 2.5x append speedup.
-
-* 0.6.0.0
-  - Moved lens to data-diverse-lens
-
-* 0.5.0.0
-  - Renamed type level functions module from Type to TypeLevel
-
-* 0.4.0.0
-  - Removed Emit typeclass, breaking renames. Added label accessors.
-
-* 0.1.0.0
-  - Initial version represented as (Int, Data.Map Int Any)
diff --git a/data-diverse.cabal b/data-diverse.cabal
--- a/data-diverse.cabal
+++ b/data-diverse.cabal
@@ -1,5 +1,5 @@
 name:                data-diverse
-version:             4.7.0.0
+version:             4.7.1.0
 synopsis:            Extensible records and polymorphic variants.
 description:         "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Seq Any).
                      "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any).
@@ -21,15 +21,17 @@
 extra-source-files:  README.md
                    , CHANGELOG.md
 cabal-version:       >=1.10
-tested-with:         GHC == 8.0.1, GHC == 8.2.2
+tested-with:         GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.1
 
 library
   hs-source-dirs:      src
   exposed-modules:     Data.Diverse
                        Data.Diverse.AFoldable
                        Data.Diverse.AFunctor
+                       Data.Diverse.ATraversable
                        Data.Diverse.Case
                        Data.Diverse.CaseFunc
+                       Data.Diverse.CaseIxed
                        Data.Diverse.Cases
                        Data.Diverse.Many
                        Data.Diverse.Many.Internal
@@ -43,6 +45,7 @@
                      , containers >= 0.5
                      , deepseq >= 1.4
                      , ghc-prim >= 0.5
+                     , hashable >= 1.3.0.0
                      , tagged >= 0.8
   ghc-options:         -Wall
   default-language:    Haskell2010
diff --git a/src/Data/Diverse/ATraversable.hs b/src/Data/Diverse/ATraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Diverse/ATraversable.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Data.Diverse.ATraversable where
+
+import Data.Diverse.TypeLevel
+
+-- | Given a 'Data.Diverse.Case' that transforms each type in the typelist within an
+-- 'Applicative' context @m@, convert a @f xs@ to @m (f ('TraverseResults' c m xs))@,
+-- where @('TraverseResults' c m xs)@ corresponds to @('CaseResults' (c m) xs)@ with the
+-- @m@ layer peeled off from each result.
+--
+-- This is primarily meant to be used with 'Data.Diverse.Case.Case's from the
+-- "Data.Diverse.CaseIxed" module.
+class ATraversable f c m xs where
+    atraverse
+        :: ( Applicative m
+           -- Throws a type error when the 'Case' is stuck
+           -- (most likely because the kind does not match).
+           , IsTraversalCase c
+           -- Defers the evaluation of the traversal results, to avoid getting another
+           -- (confusing) type error when the 'Case' is stuck.
+           , xs' ~ (TraverseResults c m xs)
+           )
+        => c m xs
+        -> f xs
+        -> m (f xs')
diff --git a/src/Data/Diverse/CaseIxed.hs b/src/Data/Diverse/CaseIxed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Diverse/CaseIxed.hs
@@ -0,0 +1,213 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Diverse.CaseIxed where
+
+import Data.Diverse.Case
+import Data.Diverse.Reiterate
+import Data.Diverse.TypeLevel
+import Data.Kind
+
+-- | This handler stores a polymorphic function which changes the type of the containers.
+--
+-- >>> let f (x :: f a) = Const @String @a $ show x
+--
+-- >>> let xs = (Just @Int 5) ./ Right @Int False ./ "X" ./ (Left @Int @Bool 6) ./ nil
+--
+-- >>> afmap (CasedIxedFunc @Show f) xs :: Many '[Const String Int, Const String Bool, Const String Char, Const String Bool]
+-- Const "Just 5" ./ Const "Right False" ./ Const "\"X\"" ./ Const "Left 6" ./ nil
+--
+-- >>> atraverse (CasedIxedFunc @Show f) xs :: Const String (Many '[Int, Bool, Char, Bool])
+-- Const "Just 5Right False\"X\"Left 6"
+newtype CaseIxedFunc (k :: Type -> Constraint) r (xs :: [Type]) = CaseIxedFunc (forall f x. k (f x) => f x -> r x)
+
+type instance CaseResult (CaseIxedFunc k r) (f x) = r x
+
+instance Reiterate (CaseIxedFunc k r) xs where
+    reiterate (CaseIxedFunc f) = CaseIxedFunc f
+
+instance k (f x) => Case (CaseIxedFunc k r) (f x ': xs) where
+    case' (CaseIxedFunc f) = f
+
+-- | A variant of 'CaseIxedFunc' for which the type of both containers is fixed.
+newtype CaseIxedFunc_ (k :: Type -> Constraint) f r (xs :: [Type]) = CaseIxedFunc_ (forall x. k (f x) => f x -> r x)
+
+type instance CaseResult (CaseIxedFunc_ k f r) (f x) = r x
+
+instance Reiterate (CaseIxedFunc_ k f r) xs where
+    reiterate (CaseIxedFunc_ f) = CaseIxedFunc_ f
+
+instance k (f x) => Case (CaseIxedFunc_ k f r) (f x ': xs) where
+    case' (CaseIxedFunc_ f) = f
+
+-- | A variant of 'CaseIxedFunc' with more constraints.
+--
+-- >>> let xs = (Just @Int 5) ./ Right @Int False ./ "X" ./ (Left @Int @Bool 6) ./ nil
+--
+-- >>> afmap (CaseIxedFunc1 @C0 @Foldable @C0 toList) xs
+-- [5] ./ [False] ./ "X" ./ [] ./ nil
+--
+-- >>> atraverse (CaseIxedFunc1 @C0 @Foldable @C0 toList) xs
+-- []
+--
+-- >>> let ys = (Just @Int 5) ./ Right @Int False ./ "XYZ" ./ nil
+--
+-- >>> atraverse (CaseIxedFunc1 @C0 @Foldable @C0 toList) ys
+-- [5 ./ False ./ 'X' ./ nil,5 ./ False ./ 'Y' ./ nil,5 ./ False ./ 'Z' ./ nil]
+newtype CaseIxedFunc1 (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r (xs :: [Type]) = CaseIxedFunc1 (forall f x. (k (f x), k1 f, k0 x) => f x -> r x)
+
+type instance CaseResult (CaseIxedFunc1 k k1 k0 r) (f x) = r x
+
+instance Reiterate (CaseIxedFunc1 k k1 k0 r) xs where
+    reiterate (CaseIxedFunc1 f) = CaseIxedFunc1 f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedFunc1 k k1 k0 r) (f x ': xs) where
+    case' (CaseIxedFunc1 f) = f
+
+-- | A variant of 'CaseIxedFunc1' for which the type of both containers is fixed.
+newtype CaseIxedFunc1_ (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) f r (xs :: [Type]) = CaseIxedFunc1_ (forall x. (k (f x), k1 f, k0 x) => f x -> r x)
+
+type instance CaseResult (CaseIxedFunc1_ k k1 k0 f r) (f x) = r x
+
+instance Reiterate (CaseIxedFunc1_ k k1 k0 f r) xs where
+    reiterate (CaseIxedFunc1_ f) = CaseIxedFunc1_ f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedFunc1_ k k1 k0 f r) (f x ': xs) where
+    case' (CaseIxedFunc1_ f) = f
+
+
+-- | A variant of 'CaseIxedFunc' which maps containers within an additional layer.
+--
+-- >>> let f (x :: f a) = Const @String @a $ show x
+--
+-- >>> let xs = (Just @Int 5) ./ Right @Int False ./ "X" ./ (Left @Int @Bool 6) ./ nil
+--
+-- >>> atraverse (CaseIxedFuncM @Show $ \x -> f x <$ print x) xs
+-- Just 5
+-- Right False
+-- "X"
+-- Left 6
+-- Const "Just 5" ./ Const "Right False" ./ Const "\"X\"" ./ Const "Left 6" ./ nil
+newtype CaseIxedFuncM (k :: Type -> Constraint) r m (xs :: [Type]) = CaseIxedFuncM (forall f x. k (f x) => f x -> m (r x))
+
+type instance CaseResult (CaseIxedFuncM k r m) (f x) = m (r x)
+
+instance Reiterate (CaseIxedFuncM k r m) xs where
+    reiterate (CaseIxedFuncM f) = CaseIxedFuncM f
+
+instance k (f x) => Case (CaseIxedFuncM k r m) (f x ': xs) where
+    case' (CaseIxedFuncM f) = f
+
+-- | A variant of 'CaseIxedFuncM' for which the type of both containers is fixed.
+newtype CaseIxedFuncM_ (k :: Type -> Constraint) f r m (xs :: [Type]) = CaseIxedFuncM_ (forall x. k (f x) => f x -> m (r x))
+
+type instance CaseResult (CaseIxedFuncM_ k f r m) (f x) = m (r x)
+
+instance Reiterate (CaseIxedFuncM_ k f r m) xs where
+    reiterate (CaseIxedFuncM_ f) = CaseIxedFuncM_ f
+
+instance k (f x) => Case (CaseIxedFuncM_ k f r m) (f x ': xs) where
+    case' (CaseIxedFuncM_ f) = f
+
+-- | A variant of 'CaseIxedFuncM' with more constraints.
+--
+-- >>> let xs = (Just @Int 5) ./ Right @Int False ./ "XYZ" ./ nil
+--
+-- >>> atraverse (CaseIxedFuncM1 @C0 @Foldable @C0 @[] @Maybe $ Just . toList) xs
+-- Just ([5] ./ [False] ./ "XYZ" ./ nil)
+newtype CaseIxedFuncM1 (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r m (xs :: [Type]) = CaseIxedFuncM1 (forall f x. (k (f x), k1 f, k0 x) => f x -> m (r x))
+
+type instance CaseResult (CaseIxedFuncM1 k k1 k0 r m) (f x) = m (r x)
+
+instance Reiterate (CaseIxedFuncM1 k k1 k0 r m) xs where
+    reiterate (CaseIxedFuncM1 f) = CaseIxedFuncM1 f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedFuncM1 k k1 k0 r m) (f x ': xs) where
+    case' (CaseIxedFuncM1 f) = f
+
+-- | A variant of 'CaseIxedFuncM1' for which the type of both containers is fixed.
+newtype CaseIxedFuncM1_ (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) f r m (xs :: [Type]) = CaseIxedFuncM1_ (forall x. (k (f x), k1 f, k0 x) => f x -> m (r x))
+
+type instance CaseResult (CaseIxedFuncM1_ k k1 k0 f r m) (f x) = m (r x)
+
+instance Reiterate (CaseIxedFuncM1_ k k1 k0 f r m) xs where
+    reiterate (CaseIxedFuncM1_ f) = CaseIxedFuncM1_ f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedFuncM1_ k k1 k0 f r m) (f x ': xs) where
+    case' (CaseIxedFuncM1_ f) = f
+
+
+-- | This handler stores a polymorphic function which maps containers to continuations.
+--
+-- This is especially useful for building 'Data.Diverse.Cases' using 'Data.Diverse.AFunctor.afmap'.
+newtype CaseIxedCont (k :: Type -> Constraint) r (xs :: [Type]) = CaseIxedCont (forall f x. k (f x) => f x -> x -> r)
+
+type instance CaseResult (CaseIxedCont k r) (f x) = x -> r
+
+instance Reiterate (CaseIxedCont k r) xs where
+    reiterate (CaseIxedCont f) = CaseIxedCont f
+
+instance k (f x) => Case (CaseIxedCont k r) (f x ': xs) where
+    case' (CaseIxedCont f) = f
+
+-- | A variant of 'CaseIxedCont' for which the type of both containers is fixed.
+--
+-- >>> let ps = Predicate @Int (> 5) ./ Predicate isLetter ./ Predicate id ./ nil
+--
+-- >>> let ps' = cases $ afmap (CaseIxedCont_ @C0 getPredicate) ps
+--
+-- >>> switch (pick @Int @'[Int, Bool, Char] 5) ps' :: Bool
+-- False
+--
+-- >>> switch (pick @Char @'[Int, Bool, Char] 6) ps' :: Bool
+-- True
+--
+-- >>> switch (pick @Char @'[Int, Bool, Char] '_') ps' :: Bool
+-- False
+--
+-- >>> switch (pick @Int @'[Int, Bool, Char] 'a') ps' :: Bool
+-- True
+--
+-- >>> switch (pick @Bool @'[Int, Bool, Char] False) ps' :: Bool
+-- False
+--
+-- >>> switch (pick @Bool @'[Int, Bool, Char] True) ps' :: Bool
+-- True
+newtype CaseIxedCont_ (k :: Type -> Constraint) f r (xs :: [Type]) = CaseIxedCont_ (forall x. k (f x) => f x -> x -> r)
+
+type instance CaseResult (CaseIxedCont_ k f r) (f x) = x -> r
+
+instance Reiterate (CaseIxedCont_ k f r) xs where
+    reiterate (CaseIxedCont_ f) = CaseIxedCont_ f
+
+instance k (f x) => Case (CaseIxedCont_ k f r) (f x ': xs) where
+    case' (CaseIxedCont_ f) = f
+
+-- | A variant of 'CaseIxedCont' with more constraints.
+newtype CaseIxedCont1 (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r (xs :: [Type]) = CaseIxedCont1 (forall f x. (k (f x), k1 f, k0 x) => f x -> x -> r)
+
+type instance CaseResult (CaseIxedCont1 k k1 k0 r) (f x) = x -> r
+
+instance Reiterate (CaseIxedCont1 k k1 k0 r) xs where
+    reiterate (CaseIxedCont1 f) = CaseIxedCont1 f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedCont1 k k1 k0 r) (f x ': xs) where
+    case' (CaseIxedCont1 f) = f
+
+-- | A variant of 'CaseIxedCont1_' for which the type of both containers is fixed.
+newtype CaseIxedCont1_ (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) f r (xs :: [Type]) = CaseIxedCont1_ (forall x. (k (f x), k1 f, k0 x) => f x -> x -> r)
+
+type instance CaseResult (CaseIxedCont1_ k k1 k0 f r) (f x) = x -> r
+
+instance Reiterate (CaseIxedCont1_ k k1 k0 f r) xs where
+    reiterate (CaseIxedCont1_ f) = CaseIxedCont1_ f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseIxedCont1_ k k1 k0 f r) (f x ': xs) where
+    case' (CaseIxedCont1_ f) = f
diff --git a/src/Data/Diverse/Many/Internal.hs b/src/Data/Diverse/Many/Internal.hs
--- a/src/Data/Diverse/Many/Internal.hs
+++ b/src/Data/Diverse/Many/Internal.hs
@@ -102,6 +102,7 @@
 import Data.Bool
 import Data.Diverse.AFoldable
 import Data.Diverse.AFunctor
+import Data.Diverse.ATraversable
 import Data.Diverse.Case
 import Data.Diverse.Reiterate
 import Data.Diverse.TypeLevel
@@ -118,6 +119,7 @@
 import Text.Read
 import qualified Text.Read.Lex as L
 import Unsafe.Coerce
+import Data.Hashable (Hashable)
 
 -- This module uses the partial 'head', 'tail' from Prelude.
 -- I like to highlight them as partial by using them in the namespace Partial.head
@@ -653,6 +655,29 @@
 instance AFunctor Many_ c as => AFunctor Many c as where
     afmap c m = fromMany_ (afmap c (toMany_ m))
 
+-----------------------------------------------------------------------
+
+instance ATraversable Many_ c m '[] where
+    atraverse _ = pure
+
+instance ( Reiterate (c m) (a ': as)
+         , ATraversable Many_ c m as
+         , Case (c m) (a ': as)
+         ) =>
+         ATraversable Many_ c m (a ': as) where
+    atraverse c (Many_ as) =
+        Many_ <$>
+        liftA2 (:)
+            (unsafeCoerce (case' c a))
+            (runMany_ <$> atraverse (reiterate c) (Many_ as' :: Many_ as))
+      where
+        a = unsafeCoerce (Partial.head as)
+        as' = Partial.tail as
+    {-# INLINABLE atraverse #-}
+
+instance ATraversable Many_ c m as => ATraversable Many c m as where
+    atraverse c m = fromMany_ <$> (atraverse c (toMany_ m))
+
 -- -----------------------------------------------------------------------
 -- | A friendlier type constraint synomyn for 'collect' and 'forMany'
 type Collect c r (xs :: [Type]) = (AFoldable (Collector c xs) r, Case (c r) xs)
@@ -1023,9 +1048,7 @@
     _ == _ = True
 
 instance (Eq x, Eq (Many_ xs)) => Eq (Many_ (x ': xs)) where
-    ls == rs = case front_ ls == front_ rs of
-        False -> False
-        _ -> (aft_ ls) == (aft_ rs)
+    ls == rs = (front_ ls == front_ rs) && (aft_ ls == aft_ rs)
     {-# INLINABLE (==) #-} -- This makes compiling tests a little faster than with no pragma
 
 -- | Two 'Many's are equal if all their fields equal
@@ -1141,6 +1164,12 @@
 
 instance (NFData x, NFData (Many xs)) => NFData (Many (x ': xs)) where
     rnf xs = rnf (front xs) `seq` rnf (aft xs)
+
+-----------------------------------------------------------------------
+
+instance Hashable (Many '[])
+
+instance (Eq (Many_ xs), Hashable x, Hashable (Many xs)) => Hashable (Many (x ': xs))
 
 -----------------------------------------------------------------------
 
diff --git a/src/Data/Diverse/TypeLevel.hs b/src/Data/Diverse/TypeLevel.hs
--- a/src/Data/Diverse/TypeLevel.hs
+++ b/src/Data/Diverse/TypeLevel.hs
@@ -189,6 +189,30 @@
     CaseResults c '[] = '[]
     CaseResults c (x ': xs) = CaseResult c x ': CaseResults c xs
 
+-- | A dummy type whose kind matches the one expected for any 'Data.Diverse.Case.Case'
+-- used with 'Data.Diverse.ATraversable.atraverse'.
+data TraversalCase :: (Type -> Type) -> [Type] -> Type
+
+-- | Throws a custom type error when the given 'Data.Diverse.Case.Case' is stuck.
+--
+-- Based on the solution proposed in this article: https://kcsongor.github.io/report-stuck-families/.
+type family BreakNonTraversalCase (error :: Constraint) (c :: (Type -> Type) -> [Type] -> Type) :: Constraint where
+    BreakNonTraversalCase _ TraversalCase = ((), ())
+    BreakNonTraversalCase _ _  = ()
+
+-- | Throws a relevant type error if a 'Data.Diverse.Case.Case' can not be used with 'Data.Diverse.ATraversable.atraverse'.
+type family IsTraversalCase c where
+    IsTraversalCase c = BreakNonTraversalCase (TypeError ('Text "The chosen `Case' can not be used with atraverse.")) c
+
+-- | Returns a list of results from applying 'CaseResult' to every type in the @xs@ typelist
+-- and peeling off the 'Applicative' layer.
+type family TraverseResults (c :: (Type -> Type) -> [k1] -> k2) (m :: Type -> Type) (xs :: [k1]) :: [k2] where
+    TraverseResults c m xs = TraverseResults' m (CaseResults (c m) xs)
+
+type family TraverseResults' m xs where
+    TraverseResults' m '[] = '[]
+    TraverseResults' m (m x ': xs) = x ': TraverseResults' m xs
+
 -- | Tests if all the types in a typelist satisfy a constraint
 type family AllConstrained (c :: k -> Constraint) (xs :: [k]) :: Constraint where
     AllConstrained c '[] = ()
diff --git a/src/Data/Diverse/Which.hs b/src/Data/Diverse/Which.hs
--- a/src/Data/Diverse/Which.hs
+++ b/src/Data/Diverse/Which.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternSynonyms #-}
 -- | Re-export Which without the constructor
 module Data.Diverse.Which (
       -- * 'Which' type
@@ -26,6 +27,7 @@
     , trialTag'
     , trialN
     , trialN'
+    , pattern W
 
       -- * Multiple types
       -- ** Injection
diff --git a/src/Data/Diverse/Which/Internal.hs b/src/Data/Diverse/Which/Internal.hs
--- a/src/Data/Diverse/Which/Internal.hs
+++ b/src/Data/Diverse/Which/Internal.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RoleAnnotations #-}
@@ -18,6 +19,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Data.Diverse.Which.Internal (
@@ -47,6 +49,7 @@
     , trialTag'
     , trialN
     , trialN'
+    , pattern W
 
       -- * Multiple types
       -- ** Injection
@@ -87,6 +90,7 @@
 import Control.DeepSeq
 import Control.Monad
 import Data.Diverse.AFunctor
+import Data.Diverse.ATraversable
 import Data.Diverse.Case
 import Data.Diverse.CaseFunc
 import Data.Diverse.Reduce
@@ -376,6 +380,21 @@
            then Just (unsafeCoerce v)
            else Nothing
 
+-- | Pattern synonym that makes pattern matching on Which possible.
+--   For example, this will return @Just 5@:
+--
+-- @
+-- let y = pick (5 :: Int) :: Which '[Bool, String, Int]
+-- in  case y of
+--       W (i :: Int) -> Just i
+--       _ -> Nothing
+-- @
+--
+-- Keep in mind, GHC is not smart enough and will always throw a warning about
+-- incomplete pattern matches without a catch-all clause.
+pattern W :: forall x xs. (UniqueMember x xs) => x -> Which xs
+pattern W x <- (trial' -> Just x)
+  where W x = pick x
 -----------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversify'.
@@ -905,3 +924,18 @@
         Left v' -> diversify0 (afmap (reiterate c) v')
     {-# INLINABLE afmap #-}
     -- This makes compiling tests a little faster than with no pragma
+
+------------------------------------------------------------------
+
+instance ATraversable Which c m '[] where
+    atraverse _ = impossible
+
+instance ( Reiterate (c m) (a ': as)
+         , ATraversable Which c m as
+         , Case (c m) (a ': as)
+         ) =>
+         ATraversable Which c m (a ': as) where
+    atraverse c v = case trial0 v of
+        Right a' -> Which 0 <$> unsafeCoerce (case' c a')
+        Left v' -> unsafeCoerce . diversify0 <$> atraverse (reiterate c) v'
+    {-# INLINABLE atraverse #-}
diff --git a/test/Data/Diverse/ManySpec.hs b/test/Data/Diverse/ManySpec.hs
--- a/test/Data/Diverse/ManySpec.hs
+++ b/test/Data/Diverse/ManySpec.hs
@@ -305,7 +305,7 @@
 
         it "with duplicate fields has setter for unique fields 'amend''" $ do
             let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nil
-            amend' @ '[Bool, Char] x (True ./ 'B' ./ nil) `shouldBe`
+            amend' @'[Bool, Char] x (True ./ 'B' ./ nil) `shouldBe`
                 (5 :: Int) ./ True ./ 'B' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nil
 
         it "can be folded with 'Many' handlers using 'forMany' or 'collect'" $ do
diff --git a/test/Data/Diverse/WhichSpec.hs b/test/Data/Diverse/WhichSpec.hs
--- a/test/Data/Diverse/WhichSpec.hs
+++ b/test/Data/Diverse/WhichSpec.hs
@@ -2,7 +2,9 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -79,6 +81,15 @@
             let y = pickOnly (5 :: Int)
                 x = hush $ trial0 y
             x `shouldBe` (Just 5)
+
+        it "can be constructed with 'pick' and destructed with pattern 'W'" $ do
+            let y = pick (5 :: Int) :: Which '[Bool, Int, Char]
+                x = case y of
+                      W (i :: Int) -> i
+                      W (_b :: Bool) -> 0
+                      W (_c :: Char) -> 0
+                      _ -> 0
+            x `shouldBe` 5
 
         it "can be constructed by index with 'pickN' and destructed with 'trialN" $ do
             let y = pickN @4 (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char]