diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -12,42 +12,24 @@
 
 Iso, Lens and Prisms are provided in [data-diverse-lens](http://hackage.haskell.org/package/data-diverse-lens)
 
-
 # Changelog
 
-* 0.1.0.0
-  - Initial version represented as (Int, Data.Map Int Any)
-
-* 0.4.0.0
-  - Removed Emit typeclass, breaking renames. Added label accessors.
-
-* 0.5.0.0
-  - Renamed type level functions module from Type to TypeLevel
-
-* 0.6.0.0
-  - Moved lens to data-diverse-lens
-
-* 0.7.0.0
-  - Removed NOINLINE pragmas.
-  - Changed internal representation to (Int, Data.IntMap Any) for a 2.5x append speedup.
-
-* 0.8.0.0
-  - Changed internal representation to (Data.Seq Any) for a further 2x append speedup.
-  - Added NFData instance for Many.
-
-* 0.8.1.0
-  - Added NFData instance for Which.
-  - Forgot to expose Many.sliceL and Many.sliceR.
-
-* 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)
+* 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.9.0.1
-  - Fixed GHC 8.2.1 test failure due to changed TypeRep show instance.
+* 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
@@ -63,10 +45,36 @@
     so the type variable ordering is consistently smaller to larger, ie. 'x', 'xs', 'branch', 'tree'
   - Added `diversify'` for allowing rearranging the types only.
 
-* 0.11.0.0
-  - Fixed https://github.com/louispan/data-diverse/issues/4
-  - Added `impossible` modelled after `Data.Void.absurd`
-  - 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.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:             0.11.0.0
+version:             1.0.0.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).
@@ -26,6 +26,7 @@
   hs-source-dirs:      src
   exposed-modules:     Data.Diverse
                        Data.Diverse.AFoldable
+                       Data.Diverse.AFunctor
                        Data.Diverse.Case
                        Data.Diverse.Cases
                        Data.Diverse.CaseTypeable
diff --git a/src/Data/Diverse.hs b/src/Data/Diverse.hs
--- a/src/Data/Diverse.hs
+++ b/src/Data/Diverse.hs
@@ -1,5 +1,6 @@
 module Data.Diverse
     ( module Data.Diverse.AFoldable
+    , module Data.Diverse.AFunctor
     , module Data.Diverse.Case
     , module Data.Diverse.Cases
     , module Data.Diverse.CaseTypeable
@@ -11,6 +12,7 @@
     ) where
 
 import Data.Diverse.AFoldable
+import Data.Diverse.AFunctor
 import Data.Diverse.Case
 import Data.Diverse.Cases
 import Data.Diverse.CaseTypeable
diff --git a/src/Data/Diverse/AFunctor.hs b/src/Data/Diverse/AFunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Diverse/AFunctor.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Data.Diverse.AFunctor where
+
+import Data.Diverse.TypeLevel
+
+-- | Given a 'Data.Diverse.Case' that transforms each type in the
+-- typelist, convert a @f xs@ to @f (CasesResult2 c xs)@
+class AFunctor f c xs where
+    afmap :: c xs -> f xs -> f (CaseResults c xs)
diff --git a/src/Data/Diverse/Case.hs b/src/Data/Diverse/Case.hs
--- a/src/Data/Diverse/Case.hs
+++ b/src/Data/Diverse/Case.hs
@@ -14,6 +14,6 @@
 -- the types in the @xs@ typelist.
 --
 -- See "Data.Diverse.CaseTypeable" and "Data.Diverse.Cases".
-class Case c (xs :: [Type]) r where
+class Case c (xs :: [Type]) where
     -- | Return the handler/continuation when x is observed.
-    case' :: c xs r -> Head xs -> r
+    case' :: c xs -> Head xs -> CaseResult c (Head xs)
diff --git a/src/Data/Diverse/CaseTypeable.hs b/src/Data/Diverse/CaseTypeable.hs
--- a/src/Data/Diverse/CaseTypeable.hs
+++ b/src/Data/Diverse/CaseTypeable.hs
@@ -4,6 +4,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Data.Diverse.CaseTypeable where
 
@@ -25,10 +27,12 @@
 -- 'Data.Diverse.AFoldable.afoldr' (:) [] ('Data.Diverse.Many.forMany' ('CaseTypeable' (show . typeRep . (pure @Proxy))) x) \`shouldBe`
 --     [\"Int", \"Bool", \"Char", \"Maybe Char", \"Int", \"Maybe Char"]
 -- @
-newtype CaseTypeable (xs :: [Type]) r = CaseTypeable (forall x. Typeable x => x -> r)
+newtype CaseTypeable r (xs :: [Type]) = CaseTypeable (forall x. Typeable x => x -> r)
 
-instance Reiterate CaseTypeable xs where
+type instance CaseResult (CaseTypeable r) x = r
+
+instance Reiterate (CaseTypeable r) xs where
     reiterate (CaseTypeable f) = CaseTypeable f
 
-instance Typeable (Head xs) => Case CaseTypeable xs r where
+instance Typeable x => Case (CaseTypeable r) (x ': xs) where
     case' (CaseTypeable f) = f
diff --git a/src/Data/Diverse/Cases.hs b/src/Data/Diverse/Cases.hs
--- a/src/Data/Diverse/Cases.hs
+++ b/src/Data/Diverse/Cases.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -32,13 +33,15 @@
 -- This uses __'fetch'__ to get the unique handler for the type at the 'Head' of @xs@.
 --
 -- Use 'cases' to construct this with 'SameLength' constraint to reduce programming confusion.
-newtype Cases (fs :: [Type]) (xs :: [Type]) r = Cases (Many fs)
+newtype Cases (fs :: [Type]) r (xs :: [Type]) = Cases (Many fs)
 
-instance Reiterate (Cases fs) xs where
+type instance CaseResult (Cases fs r) x = r
+
+instance Reiterate (Cases fs r) xs where
     reiterate (Cases s) = Cases s
 
 -- | UndecidableInstances because @fs@ appers more often.
-instance UniqueMember (Head xs -> r) fs => Case (Cases fs) xs r where
+instance UniqueMember (Head xs -> r) fs => Case (Cases fs r) xs where
     case' (Cases s) = fetch @(Head xs -> r) s
 
 -- | Create an instance of 'Case' for either handling 'Data.Diverse.Which.switch'ing a 'Which'.
@@ -63,26 +66,41 @@
 -- This function imposes additional @SameLength@ constraints than when using the 'Cases' constructor directly.
 -- It is better practice to use 'cases' to prevent programming confusion with dead code.
 -- However, the 'Cases' constructor is still exported to allow creating a master-of-all-'Case'.
-cases :: forall r xs fs. (CasesResult fs ~ r, SameLength fs (Nub xs)) => Many fs -> Cases fs xs r
+cases
+    :: forall r xs fs.
+       (IsAll r (CaseResults (Cases fs r) fs), SameLength fs (Nub xs))
+    => Many fs -> Cases fs r xs
 cases = Cases
 
 -- | A variation of 'cases' without the @SameLength@ constraint to allow creating a master-of-all-'Case'.
-cases' :: forall r xs fs. (CasesResult fs ~ r) => Many fs -> Cases fs xs r
+cases'
+    :: forall r xs fs.
+       (IsAll r (CaseResults (Cases fs r) fs))
+    => Many fs -> Cases fs r xs
 cases' = Cases
 
+-- -- | Create a partially appliable contraint :: [Type] -> Constraint
+-- -- Idea from https://hackage.haskell.org/package/constraint-manip-0.1.0.0/docs/src/Control.ConstraintManip.html
+-- -- type MyC f xs = (f xs)
+-- class (f xs) => MyC f xs
+-- instance (f xs) => MyC f xs
+
+
 -----------------------------------------------
 
 -- | A variation of 'Cases' which uses __'fetchN'__ to get the handler by index.
 -- There may be different handlers for the same type, but the handlers must be in the same order
 -- as the input @xs@ typelist.
 -- Use 'casesN' to construct this safely ensuring @n@ starts at 0.
-newtype CasesN (fs :: [Type]) (n :: Nat) (xs :: [Type]) r = CasesN (Many fs)
+newtype CasesN (fs :: [Type]) r (n :: Nat) (xs :: [Type]) = CasesN (Many fs)
 
-instance ReiterateN (CasesN fs) n xs where
+type instance CaseResult (CasesN fs r n) x = r
+
+instance ReiterateN (CasesN fs r) n xs where
     reiterateN (CasesN s) = CasesN s
 
 -- | UndecidableInstances because @fs@ appears more often.
-instance (MemberAt n (Head xs -> r) fs) => Case (CasesN fs n) xs r where
+instance (MemberAt n (Head xs -> r) fs) => Case (CasesN fs r n) xs where
     case' (CasesN s) = fetchN (Proxy @n) s
 
 -- | Safe Constructor for 'CasesN' ensuring that the @n@ Nat starts at 0.
@@ -106,9 +124,15 @@
 -- 'Data.Diverse.AFoldable.afoldr' (:) [] ('collectN' x ('casesN' y)) \`shouldBe`
 --     [\"5", \"False", \"'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-casesN :: forall r xs fs. SameLength fs xs => Many fs -> CasesN fs 0 xs r
+casesN
+    :: forall r xs fs.
+       (IsAll r (CaseResults (CasesN fs r 0) fs), SameLength fs xs)
+    => Many fs -> CasesN fs r 0 xs
 casesN = CasesN
 
 -- | A variation of 'casesN' without the @SameLength@ constraint to allow creating a master-of-all-'Case'.
-casesN' :: forall r xs fs. (CasesResult fs ~ r) => Many fs -> CasesN fs 0 xs r
+casesN'
+    :: forall r xs fs.
+       (IsAll r (CaseResults (CasesN fs r 0) fs))
+    => Many fs -> CasesN fs r 0 xs
 casesN' = CasesN
diff --git a/src/Data/Diverse/Many.hs b/src/Data/Diverse/Many.hs
--- a/src/Data/Diverse/Many.hs
+++ b/src/Data/Diverse/Many.hs
@@ -62,9 +62,13 @@
 
     -- * Destruction
     -- ** By type
+    , Collect
+    , Collector
     , forMany
     , collect
     -- ** By Nat index offset
+    , CollectN
+    , CollectorN
     , forManyN
     , collectN
     ) where
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
@@ -79,9 +79,13 @@
 
     -- * Destruction
     -- ** By type
+    , Collect
+    , Collector
     , forMany
     , collect
     -- ** By Nat index offset
+    , CollectN
+    , CollectorN
     , forManyN
     , collectN
     ) where
@@ -90,6 +94,7 @@
 import Control.DeepSeq
 import Data.Bool
 import Data.Diverse.AFoldable
+import Data.Diverse.AFunctor
 import Data.Diverse.Case
 import Data.Diverse.Reiterate
 import Data.Diverse.TypeLevel
@@ -129,7 +134,7 @@
 -- * getter/setter for multiple fields: 'selectN' and 'amendN'
 -- * folds: 'forManyN' or 'collectN'
 --
--- Encoding: The record is encoded as (Offset, Map Int Any).
+-- Encoding: The record is encoded as (S.Seq Any).
 -- This encoding should reasonabily efficient for any number of fields.
 --
 -- The map Key is index + offset of the type in the typelist.
@@ -139,7 +144,7 @@
 --
 -- The constructor will guarantee the correct number and types of the elements.
 -- The constructor is only exported in the "Data.Diverse.Many.Internal" module
-data Many (xs :: [Type]) = Many (S.Seq Any)
+newtype Many (xs :: [Type]) = Many (S.Seq Any)
 
 -- Inferred role is phantom which is incorrect
 -- representational means:
@@ -150,7 +155,7 @@
 
 -- | Many stored as a list. This is useful when folding over 'Many' efficienty
 -- so that the conversion to List is only done once
-data Many_ (xs :: [Type]) = Many_ [Any]
+newtype Many_ (xs :: [Type]) = Many_ { runMany_ :: [Any] }
 
 type role Many_ representational
 
@@ -520,22 +525,23 @@
 
 ------------------------------------------------------------------------
 
-class CaseAny c (xs :: [Type]) r where
+class CaseAny c (xs :: [Type]) where
     -- | Return the handler/continuation when x is observed.
-    caseAny :: c xs r -> Any -> r
+    caseAny :: c xs -> Any -> CaseResult c Any
 
 -----------------------------------------------------------------------
 
 -- | Variation of 'Collector' which uses 'CaseAny' instead of 'Case'
-data CollectorAny c (xs :: [Type]) r = CollectorAny (c xs r) [Any]
+data CollectorAny c (xs :: [Type]) r = CollectorAny (c r xs) [Any]
 
 -- | nill case that doesn't even use 'caseAny', so that an instance of @CaseAny '[]@ is not needed.
 instance AFoldable (CollectorAny c '[]) r where
     afoldr _ z _ = z
 
-instance ( CaseAny c (x ': xs) r
-         , Reiterate c (x ': xs)
+instance ( CaseAny (c r) (x ': xs)
+         , Reiterate (c r) (x ': xs)
          , AFoldable (CollectorAny c xs) r
+         , r ~ CaseResult (c r) Any
          ) =>
          AFoldable (CollectorAny c (x ': xs)) r where
     afoldr f z (CollectorAny c xs) = f (caseAny c x) (afoldr f z (CollectorAny (reiterate c) xs'))
@@ -545,21 +551,22 @@
        xs' = Partial.tail xs
     {-# INLINABLE afoldr #-} -- This makes compiling tests a little faster than with no pragma
 
-forMany' :: c xs r -> Many xs -> CollectorAny c xs r
+forMany' :: c r xs -> Many xs -> CollectorAny c xs r
 forMany' c (Many xs) = CollectorAny c (toList xs)
 
 -----------------------------------------------------------------------
 
 -- | A variation of 'CollectorN' which uses 'CaseAny' instead of 'Case'
-data CollectorAnyN c n (xs :: [Type]) r = CollectorAnyN (c n xs r) [Any]
+data CollectorAnyN c n (xs :: [Type]) r = CollectorAnyN (c r n xs) [Any]
 
 -- | nill case that doesn't even use 'caseAnyN', so that an instance of @CaseAnyN '[]@ is not needed.
 instance AFoldable (CollectorAnyN c n '[]) r where
     afoldr _ z _ = z
 
-instance ( CaseAny (c n) (x ': xs) r
-         , ReiterateN c n (x ': xs)
+instance ( CaseAny (c r n) (x ': xs)
+         , ReiterateN (c r) n (x ': xs)
          , AFoldable (CollectorAnyN c (n + 1) xs) r
+         , r ~ CaseResult (c r n) Any
          ) =>
          AFoldable (CollectorAnyN c n (x ': xs)) r where
     afoldr f z (CollectorAnyN c xs) = f (caseAny c x) (afoldr f z (CollectorAnyN (reiterateN c) xs'))
@@ -569,7 +576,7 @@
        xs' = Partial.tail xs
     {-# INLINABLE afoldr #-} -- This makes compiling tests a little faster than with no pragma
 
-forManyN' :: c n xs r -> Many xs -> CollectorAnyN c n xs r
+forManyN' :: c r n xs -> Many xs -> CollectorAnyN c n xs r
 forManyN' c (Many xs) = CollectorAnyN c (toList xs)
 
 -----------------------------------------------------------------------
@@ -580,16 +587,17 @@
 --  Internally, this holds the left-over [(k, v)] from the original 'Many' for the remaining typelist @xs@.
 --
 -- That is, the first v in the (k, v) is of type @x@, and the length of the list is equal to the length of @xs@.
-data Collector c (xs :: [Type]) r = Collector (c xs r) [Any]
+data Collector c (xs :: [Type]) r = Collector (c r xs) [Any]
 
 -- | nill case that doesn't even use 'case'', so that an instance of @Case '[]@ is not needed.
 instance AFoldable (Collector c '[]) r where
     afoldr _ z _ = z
 
 -- | Folds values by 'reiterate'ing 'Case's through the @xs@ typelist.
-instance ( Case c (x ': xs) r
-         , Reiterate c (x ': xs)
+instance ( Case (c r) (x ': xs)
+         , Reiterate (c r) (x ': xs)
          , AFoldable (Collector c xs) r
+         , r ~ CaseResult (c r) x
          ) =>
          AFoldable (Collector c (x ': xs)) r where
     afoldr f z (Collector c xs) = f (case' c v) (afoldr f z (Collector (reiterate c) xs'))
@@ -601,6 +609,39 @@
 
 -----------------------------------------------------------------------
 
+-- | Terminating AFunctor instance for empty type list
+instance AFunctor Many_ c '[] where
+    afmap _ = id
+
+-- | Recursive AFunctor instance for non empty type list
+-- delegate afmap'ing the remainder to an instance of Collector' with one less type in the type list
+instance ( Reiterate c (a ': as)
+         , AFunctor Many_ c as
+         , Case c (a ': as)
+         ) =>
+         AFunctor Many_ c (a ': as) where
+    afmap c (Many_ as) =
+        Many_ $
+        unsafeCoerce (case' c a) :
+        runMany_
+            (afmap
+                 (reiterate c)
+                 (Many_ as' :: Many_ as))
+      where
+        a = unsafeCoerce (Partial.head as)
+        as' = Partial.tail as
+    {-# INLINABLE afmap #-}
+    -- This makes compiling tests a little faster than with no pragma
+
+-- | Given a 'Data.Diverse.Case' that transforms each type in the
+-- typelist, convert a @Many xs@ to @Many (CaseResults c xs)@
+instance AFunctor Many_ c as => AFunctor Many c as where
+    afmap c m = fromMany_ (afmap 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)
+
 -- | Folds any 'Many', even with indistinct types.
 -- Given __distinct__ handlers for the fields in 'Many', create 'AFoldable'
 -- of the results of running the handlers over the fields in 'Many'.
@@ -611,7 +652,7 @@
 -- 'afoldr' (:) [] ('forMany' ('Data.Diverse.Cases.cases' y) x) \`shouldBe`
 --     [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-forMany :: (t ~ Collector c xs, AFoldable t r, Case c xs r) => c xs r -> Many xs -> t r
+forMany :: Collect c r xs => c r xs -> Many xs -> Collector c xs r
 forMany c (Many xs) = Collector c (toList xs)
 
 -- | This is @flip 'forMany'@
@@ -622,22 +663,23 @@
 -- 'afoldr' (:) [] ('collect' x ('Data.Diverse.Cases.cases' y)) \`shouldBe`
 --     [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-collect :: (t ~ Collector c xs, AFoldable t r, Case c xs r) => Many xs -> c xs r -> t r
+collect :: (Collect c r xs) => Many xs -> c r xs -> Collector c xs r
 collect = flip forMany
 
 -----------------------------------------------------------------------
 
 -- | A variation of 'Collector' which uses 'ReiterateN' instead of 'Reiterate'
-data CollectorN c (n :: Nat) (xs :: [Type]) r = CollectorN (c n xs r) [Any]
+data CollectorN c (n :: Nat) (xs :: [Type]) r = CollectorN (c r n xs) [Any]
 
 -- | nill case that doesn't even use 'case'', so that an instance of @Case '[]@ is not needed.
 instance AFoldable (CollectorN c n '[]) r where
     afoldr _ z _ = z
 
 -- | Folds values by 'reiterate'ing 'Emit'ters through the @xs@ typelist.
-instance ( Case (c n) (x ': xs) r
-         , ReiterateN c n (x ': xs)
+instance ( Case (c r n) (x ': xs)
+         , ReiterateN (c r) n (x ': xs)
          , AFoldable (CollectorN c (n + 1) xs) r
+         , r ~ CaseResult (c r n) x
          ) =>
          AFoldable (CollectorN c n (x ': xs)) r where
     afoldr f z (CollectorN c xs) = f (case' c v) (afoldr f z (CollectorN (reiterateN c) xs'))
@@ -647,6 +689,9 @@
        xs' = Partial.tail xs
     {-# INLINABLE afoldr #-} -- This makes compiling tests a little faster than with no pragma
 
+-- | A friendlier type constraint synomyn for 'collect' and 'forMany'
+type CollectN c r (n :: Nat) (xs :: [Type]) = (AFoldable (CollectorN c n xs) r, Case (c r n) xs)
+
 -- | Folds any 'Many', even with indistinct types.
 -- Given __index__ handlers for the fields in 'Many', create 'AFoldable'
 -- of the results of running the handlers over the fields in 'Many'.
@@ -657,7 +702,7 @@
 -- 'afoldr' (:) [] ('forManyN' ('Data.Diverse.Cases.casesN' y) x) \`shouldBe`
 --     [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-forManyN :: (t ~ CollectorN c n xs, AFoldable t r, Case (c n) xs r) => c n xs r -> Many xs -> t r
+forManyN :: CollectN c r n xs => c r n xs -> Many xs -> CollectorN c n xs r
 forManyN c (Many xs) = CollectorN c (toList xs)
 
 -- | This is @flip 'forManyN'@
@@ -668,7 +713,7 @@
 -- 'afoldr' (:) [] ('collectN' x ('Data.Diverse.Cases.casesN' y)) \`shouldBe`
 --     [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-collectN :: (t ~ CollectorN c n xs, AFoldable t r, Case (c n) xs r) => Many xs -> c n xs r -> t r
+collectN :: CollectN c r n xs  => Many xs -> c r n xs -> CollectorN c n xs r
 collectN = flip forManyN
 
 -----------------------------------------------------------------------
@@ -676,7 +721,7 @@
 -- | A friendlier type constraint synomyn for 'select'
 type Select (smaller :: [Type]) (larger :: [Type]) =
     (AFoldable
-        ( CollectorAny (CaseSelect smaller larger) larger) (Maybe (Int, WrappedAny)))
+        (CollectorAny (CaseSelect smaller larger) larger) (Maybe (Int, WrappedAny)))
 
 -- | Construct a 'Many' with a smaller number of fields than the original.
 -- Analogous to 'fetch' getter but for multiple fields.
@@ -690,17 +735,19 @@
 select :: forall smaller larger. Select smaller larger => Many larger -> Many smaller
 select t = Many (fromList' xs')
   where
-    xs' = afoldr (\a z -> maybe z (: z) a) [] (forMany' (CaseSelect @smaller @larger @larger) t)
+    xs' = afoldr (\a z -> maybe z (: z) a) [] (forMany' (CaseSelect @smaller @larger @_ @larger) t)
 
 -- | For each type x in @larger@, generate the (k, v) in @smaller@ (if it exists)
-data CaseSelect (smaller :: [Type]) (larger :: [Type]) (xs :: [Type]) r = CaseSelect
+data CaseSelect (smaller :: [Type]) (larger :: [Type]) r (xs :: [Type]) = CaseSelect
 
-instance Reiterate (CaseSelect smaller larger) (x ': xs) where
+type instance CaseResult (CaseSelect smaller larger r) x = r
+
+instance Reiterate (CaseSelect smaller larger r) (x ': xs) where
     reiterate = coerce
 
 -- | For each type x in larger, find the index in ys, and create a (key, value)
 instance forall smaller larger x xs n. (UniqueIfExists smaller x larger, MaybeUniqueMemberAt n x smaller) =>
-         CaseAny (CaseSelect smaller larger) (x ': xs) (Maybe (Int, WrappedAny)) where
+    CaseAny (CaseSelect smaller larger (Maybe (Int, WrappedAny))) (x ': xs) where
     caseAny _ v =
         case i of
             0 -> Nothing
@@ -753,16 +800,18 @@
     => proxy ns -> Many larger -> Many smaller
 selectN _ xs = Many (fromList' xs')
   where
-    xs' = afoldr (\a z -> maybe z (: z) a) [] (forManyN' (CaseSelectN @ns @smaller @0 @larger) xs)
+    xs' = afoldr (\a z -> maybe z (: z) a) [] (forManyN' (CaseSelectN @ns @smaller @_ @0 @larger) xs)
 
-data CaseSelectN (indices :: [Nat]) (smaller :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseSelectN
+data CaseSelectN (indices :: [Nat]) (smaller :: [Type]) r (n :: Nat) (xs :: [Type]) = CaseSelectN
 
-instance ReiterateN (CaseSelectN indices smaller) n (x ': xs) where
+type instance CaseResult (CaseSelectN indices smaller r n) x = r
+
+instance ReiterateN (CaseSelectN indices smaller r) n (x ': xs) where
     reiterateN CaseSelectN = CaseSelectN
 
 -- | For each type x in @larger@, find the index in ys, and create an (incrementing key, value)
 instance forall indices smaller n x xs n'. (MaybeMemberAt n' x smaller, n' ~ PositionOf n indices) =>
-         CaseAny (CaseSelectN indices smaller n) (x ': xs) (Maybe (Int, WrappedAny)) where
+    CaseAny (CaseSelectN indices smaller (Maybe (Int, WrappedAny)) n) (x ': xs) where
     caseAny _ v =
         case i of
             0 -> Nothing
@@ -773,8 +822,7 @@
 -----------------------------------------------------------------------
 
 -- | A friendlier type constraint synomyn for 'amend'
-type Amend smaller larger = (AFoldable (CollectorAny (CaseAmend larger) smaller) (Int, WrappedAny)
-       , IsDistinct smaller)
+type Amend smaller larger = (AFoldable (CollectorAny (CaseAmend larger) smaller) (Int, WrappedAny), IsDistinct smaller)
 
 -- | Sets the subset of 'Many' in the larger 'Many'.
 -- Analogous to 'replace' setter but for multiple fields.
@@ -787,15 +835,18 @@
 amend :: forall smaller larger. Amend smaller larger => Many larger -> Many smaller -> Many larger
 amend (Many ls) t = Many $ foldr (\(i, WrappedAny v) ys -> S.update i v ys) ls xs'
   where
-    xs' = afoldr (:) [] (forMany' (CaseAmend @larger @smaller) t)
+    xs' = afoldr (:) [] (forMany' (CaseAmend @larger @_ @smaller) t)
 
-data CaseAmend (larger :: [Type]) (xs :: [Type]) r = CaseAmend
+data CaseAmend (larger :: [Type]) r (xs :: [Type]) = CaseAmend
 
-instance Reiterate (CaseAmend larger) (x ': xs) where
+type instance CaseResult (CaseAmend larger r) x = r
+
+instance Reiterate (CaseAmend larger r) (x ': xs) where
     reiterate = coerce
 
 -- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @Many larger@
-instance UniqueMemberAt n x larger => CaseAny (CaseAmend larger) (x ': xs) (Int, WrappedAny) where
+instance UniqueMemberAt n x larger =>
+         CaseAny (CaseAmend larger (Int, WrappedAny)) (x ': xs) where
     caseAny _ v = (i, WrappedAny v)
       where
         i = fromInteger (natVal @n Proxy)
@@ -831,18 +882,21 @@
     => proxy smaller -> Many larger -> Many smaller' -> Many (Replaces smaller smaller' larger)
 amend' _ (Many ls) t = Many $ foldr (\(i, WrappedAny v) ys -> S.update i v ys) ls xs'
   where
-    xs' = afoldr (:) [] (forMany'' @smaller Proxy (CaseAmend' @larger @(Zip smaller smaller')) t)
+    xs' = afoldr (:) [] (forMany'' @smaller Proxy (CaseAmend' @larger @_ @(Zip smaller smaller')) t)
 
-forMany'' :: Proxy xs -> c (Zip xs ys) r -> Many ys -> CollectorAny c (Zip xs ys) r
+forMany'' :: Proxy xs -> c r (Zip xs ys) -> Many ys -> CollectorAny c (Zip xs ys) r
 forMany'' _ c (Many ys) = CollectorAny c (toList ys)
 
-data CaseAmend' (larger :: [Type]) (zs :: [Type]) r = CaseAmend'
+data CaseAmend' (larger :: [Type]) r (zs :: [Type]) = CaseAmend'
 
-instance Reiterate (CaseAmend' larger) (z ': zs) where
+type instance CaseResult (CaseAmend' larger r) x = r
+
+instance Reiterate (CaseAmend' larger r) (z ': zs) where
     reiterate = coerce
 
 -- | for each y in @smaller@, convert it to a (k, v) to insert into the x in @Many larger@
-instance (UniqueMemberAt n x larger) => CaseAny (CaseAmend' larger) ((x, y) ': zs) (Int, WrappedAny) where
+instance (UniqueMemberAt n x larger) =>
+         CaseAny (CaseAmend' larger (Int, WrappedAny)) ((x, y) ': zs) where
     caseAny _ v = (i, WrappedAny v)
       where
         i = fromInteger (natVal @n Proxy)
@@ -897,16 +951,18 @@
     => proxy ns -> Many larger -> Many smaller -> Many larger
 amendN _ (Many ls) t = Many $ foldr (\(i, WrappedAny v) ys -> S.update i v ys) ls xs'
   where
-    xs' = afoldr (:) [] (forManyN' (CaseAmendN @ns @larger @0 @smaller) t)
+    xs' = afoldr (:) [] (forManyN' (CaseAmendN @ns @larger @_ @0 @smaller) t)
 
-data CaseAmendN (indices :: [Nat]) (larger :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseAmendN
+data CaseAmendN (indices :: [Nat]) (larger :: [Type]) r (n :: Nat) (xs :: [Type]) = CaseAmendN
 
-instance ReiterateN (CaseAmendN indices larger) n (x ': xs) where
+type instance CaseResult (CaseAmendN indices larger r n) x = r
+
+instance ReiterateN (CaseAmendN indices larger r) n (x ': xs) where
     reiterateN = coerce
 
 -- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @larger@
 instance (MemberAt n' x larger, n' ~ KindAtIndex n indices) =>
-         CaseAny (CaseAmendN indices larger n) (x ': xs) (Int, WrappedAny) where
+         CaseAny (CaseAmendN indices larger (Int, WrappedAny) n) (x ': xs) where
     caseAny _ v = (i, WrappedAny v)
       where
         i = fromInteger (natVal @n' Proxy)
@@ -925,19 +981,21 @@
     => proxy ns -> Many larger -> Many smaller' -> Many (ReplacesIndex ns smaller' larger)
 amendN' _ (Many ls) t = Many $ foldr (\(i, WrappedAny v) ys -> S.update i v ys) ls xs'
   where
-    xs' = afoldr (:) [] (forManyN'' @smaller Proxy (CaseAmendN' @ns @larger @0 @(Zip smaller smaller')) t)
+    xs' = afoldr (:) [] (forManyN'' @smaller Proxy (CaseAmendN' @ns @larger @_ @0 @(Zip smaller smaller')) t)
 
-forManyN'' :: Proxy xs -> c n (Zip xs ys) r -> Many ys -> CollectorAnyN c n (Zip xs ys) r
+forManyN'' :: Proxy xs -> c r n (Zip xs ys) -> Many ys -> CollectorAnyN c n (Zip xs ys) r
 forManyN'' _ c (Many ys) = CollectorAnyN c (toList ys)
 
-data CaseAmendN' (indices :: [Nat]) (larger :: [Type]) (n :: Nat) (zs :: [Type]) r = CaseAmendN'
+data CaseAmendN' (indices :: [Nat]) (larger :: [Type]) r (n :: Nat) (zs :: [Type]) = CaseAmendN'
 
-instance ReiterateN (CaseAmendN' indices larger) n (z ': zs) where
+type instance CaseResult (CaseAmendN' indices larger r n) x = r
+
+instance ReiterateN (CaseAmendN' indices larger r) n (z ': zs) where
     reiterateN = coerce
 
 -- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @larger@
 instance (MemberAt n' x larger, n' ~ KindAtIndex n indices) =>
-         CaseAny (CaseAmendN' indices larger n) ((x, y) ': zs) (Int, WrappedAny) where
+         CaseAny (CaseAmendN' indices larger (Int, WrappedAny) n) ((x, y) ': zs) where
     caseAny _ v = (i, WrappedAny v)
       where
         i = fromInteger (natVal @n' Proxy)
diff --git a/src/Data/Diverse/Reiterate.hs b/src/Data/Diverse/Reiterate.hs
--- a/src/Data/Diverse/Reiterate.hs
+++ b/src/Data/Diverse/Reiterate.hs
@@ -13,9 +13,9 @@
 -- | Allows iterating over the types in a typelist
 class Reiterate c (xs :: [Type]) where
     -- | Return the next iteration without the 'Head' type x in (x ': xs)
-    reiterate :: c xs r -> c (Tail xs) r
+    reiterate :: c xs -> c (Tail xs)
 
 -- | Allows iterating over the types in a typelist, whilst also incrementing an Nat index
 class ReiterateN c (n :: Nat) (xs :: [Type]) where
     -- | Return the next iteration without the 'Head' type x in (x ': xs)
-    reiterateN :: c n xs r -> c (n + 1) (Tail xs) r
+    reiterateN :: c n xs -> c (n + 1) (Tail 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
@@ -164,9 +164,12 @@
 -- | Takes two lists which must be the same length and returns a list of corresponding pairs.
 type Zip (xs :: [k]) (ys :: [k]) = ZipImpl xs ys xs ys
 
-type family CasesResult (fs :: [k1]) :: k2 where
-    CasesResult ((a -> r) ': fs) = CasesResultImpl ((a -> r) ': fs) r fs
-    CasesResult fs = TypeError ('Text "CasesResult error: ‘"
-                              ':<>: 'ShowType fs
-                              ':<>: 'Text "’"
-                              ':<>: 'Text " doesn't return anything")
+-- | Tests if all the types in a typelist is all a specified type.
+type IsAll (x :: k) (xs :: [k]) = IsAllImpl xs x xs
+
+type family CaseResult (c ::[k1] -> k2) (x :: k1) :: k2
+
+-- | Return a list of results from applying 'CaseResult' to every type in the @xs@ typelist.
+type family CaseResults (c ::[k1] -> k2) (xs :: [k1]) :: [k2] where
+    CaseResults c '[] = '[]
+    CaseResults c (x ': xs) = CaseResult c x ': CaseResults c xs
diff --git a/src/Data/Diverse/TypeLevel/Internal.hs b/src/Data/Diverse/TypeLevel/Internal.hs
--- a/src/Data/Diverse/TypeLevel/Internal.hs
+++ b/src/Data/Diverse/TypeLevel/Internal.hs
@@ -193,13 +193,13 @@
                               ':<>: 'ShowType ys'
                               ':<>: 'Text "’")
 
-type family CasesResultImpl (ctx :: [k1]) (r :: k2) (fs :: [k1]) :: k2 where
-    CasesResultImpl ctx r '[] = r
-    CasesResultImpl ctx r ((a -> r) ': fs) = CasesResultImpl ctx r fs
-    CasesResultImpl ctx r fs = TypeError ('Text "CasesResult error: ‘"
-                                  ':<>: 'ShowType ctx
-                                  ':<>: 'Text "’"
-                                  ':<>: 'Text " doesn't all return "
-                                  ':<>: 'Text "‘"
-                                  ':<>: 'ShowType r
-                                  ':<>: 'Text "’")
+-- | Tests if all the types in a typelist is all a specified type.
+type family IsAllImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where
+    IsAllImpl ctx x '[] = ()
+    IsAllImpl ctx x (x ': xs) = IsAllImpl ctx x xs
+    IsAllImpl ctx x xs = TypeError ('Text "IsAll error: ‘"
+                              ':<>: 'ShowType ctx
+                              ':<>: 'Text "’"
+                              ':<>: 'Text " must only contain ‘"
+                              ':<>: 'ShowType x
+                              ':<>: 'Text "’")
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
@@ -332,7 +332,7 @@
 -----------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversify'.
-type Diversify (branch :: [Type]) (tree :: [Type]) = Reduce (Which branch) (Switcher (CaseDiversify branch tree) branch (Which tree))
+type Diversify (branch :: [Type]) (tree :: [Type]) = Reduce (Which branch) (Switcher (CaseDiversify branch tree) (Which tree) branch)
 
 -- | Convert a 'Which' to another 'Which' that may include other possibilities.
 -- That is, @branch@ is equal or is a subset of @tree@.
@@ -349,16 +349,18 @@
 --     c = 'diversify' \@_ \@[Bool, Int] b :: 'Which' '[Bool, Int]
 -- @
 diversify :: forall branch tree. Diversify branch tree => Which branch -> Which tree
-diversify = which (CaseDiversify @branch @tree @branch)
+diversify = which (CaseDiversify @branch @tree @_ @branch)
 
-data CaseDiversify (branch :: [Type]) (tree :: [Type]) (branch' :: [Type]) r = CaseDiversify
+data CaseDiversify (branch :: [Type]) (tree :: [Type]) r (branch' :: [Type]) = CaseDiversify
 
-instance Reiterate (CaseDiversify branch tree) branch' where
+type instance CaseResult (CaseDiversify branch tree r) x = r
+
+instance Reiterate (CaseDiversify r branch tree) branch' where
     reiterate CaseDiversify = CaseDiversify
 
 -- | The @Unique x branch@ is important to get a compile error if the from @branch@ doesn't have a unique x
 instance (UniqueMember x tree, Unique x branch) =>
-         Case (CaseDiversify branch tree) (x ': branch') (Which tree) where
+         Case (CaseDiversify branch tree (Which tree)) (x ': branch') where
     case' CaseDiversify = pick
 
 -- | A simple version of 'diversify' which add another type to the front of the typelist.
@@ -387,13 +389,13 @@
        , IsDistinct ls
        )
     => proxy ls -> Which branch -> Which tree
-diversifyL _ = which (CaseDiversify @branch @tree @branch)
+diversifyL _ = which (CaseDiversify @branch @tree @_ @branch)
 
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversifyN'.
 type DiversifyN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
-    ( Reduce (Which branch) (SwitcherN (CaseDiversifyN indices) 0 branch (Which tree))
+    ( Reduce (Which branch) (SwitcherN (CaseDiversifyN indices) (Which tree) 0 branch)
     , KindsAtIndices indices tree ~ branch)
 
 -- | A variation of 'diversify' which uses a Nat list @indices@ to specify how to reorder the fields, where
@@ -412,21 +414,23 @@
 -- 'switch' y'' ('Data.Diverse.CaseTypeable.CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Int"
 -- @
 diversifyN :: forall indices branch tree proxy. (DiversifyN indices branch tree) => proxy indices -> Which branch -> Which tree
-diversifyN _ = whichN (CaseDiversifyN @indices @0 @branch)
+diversifyN _ = whichN (CaseDiversifyN @indices @_ @0 @branch)
 
-data CaseDiversifyN (indices :: [Nat]) (n :: Nat) (branch' :: [Type]) r = CaseDiversifyN
+data CaseDiversifyN (indices :: [Nat]) r (n :: Nat) (branch' :: [Type]) = CaseDiversifyN
 
-instance ReiterateN (CaseDiversifyN indices) n branch' where
+type instance CaseResult (CaseDiversifyN indices r n) x = r
+
+instance ReiterateN (CaseDiversifyN indices r) n branch' where
     reiterateN CaseDiversifyN = CaseDiversifyN
 
 instance MemberAt (KindAtIndex n indices) x tree =>
-         Case (CaseDiversifyN indices n) (x ': branch') (Which tree) where
+         Case (CaseDiversifyN indices (Which tree) n) (x ': branch') where
     case' CaseDiversifyN v = pickN (Proxy @(KindAtIndex n indices)) v
 
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpret'.
-type Reinterpret branch tree = Reduce (Which tree) (Switcher (CaseReinterpret branch tree) tree (Either (Which (Complement tree branch)) (Which branch)))
+type Reinterpret branch tree = Reduce (Which tree) (Switcher (CaseReinterpret branch tree) (Either (Which (Complement tree branch)) (Which branch)) tree)
 
 -- | Convert a 'Which' into possibly another 'Which' with a totally different typelist.
 -- Returns either a 'Which' with the 'Right' value, or a 'Which' with the 'Left'over @compliment@ types.
@@ -443,11 +447,13 @@
 --     c \`shouldBe` Right ('pick' (5 :: Int)) :: 'Which' '[String, Int]
 -- @
 reinterpret :: forall branch tree. Reinterpret branch tree => Which tree -> Either (Which (Complement tree branch)) (Which branch)
-reinterpret = which (CaseReinterpret @branch @tree @tree)
+reinterpret = which (CaseReinterpret @branch @tree @_ @tree)
 
-data CaseReinterpret (branch :: [Type]) (tree :: [Type]) (tree' :: [Type]) r = CaseReinterpret
+data CaseReinterpret (branch :: [Type]) (tree :: [Type]) r (tree' :: [Type]) = CaseReinterpret
 
-instance Reiterate (CaseReinterpret branch tree) tree' where
+type instance CaseResult (CaseReinterpret branch tree r) x = r
+
+instance Reiterate (CaseReinterpret branch tree r) tree' where
     reiterate CaseReinterpret = CaseReinterpret
 
 instance ( MaybeUniqueMemberAt n x branch
@@ -455,7 +461,7 @@
          , MaybeUniqueMemberAt n' x comp
          , Unique x tree -- Compile error to ensure reinterpret only works with unique fields
          ) =>
-         Case (CaseReinterpret branch tree) (x ': tree') (Either (Which comp) (Which branch)) where
+         Case (CaseReinterpret branch tree (Either (Which comp) (Which branch))) (x ': tree') where
     case' CaseReinterpret a =
         case fromInteger (natVal @n Proxy) of
             0 -> let j = fromInteger (natVal @n' Proxy)
@@ -466,15 +472,17 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpret''.
-type Reinterpret' branch tree = Reduce (Which tree) (Switcher (CaseReinterpret' branch tree) tree (Maybe (Which branch)))
+type Reinterpret' branch tree = Reduce (Which tree) (Switcher (CaseReinterpret' branch tree) (Maybe (Which branch)) tree)
 
 -- | Variation of 'reinterpret' which returns a Maybe.
 reinterpret' :: forall branch tree. Reinterpret' branch tree => Which tree -> Maybe (Which branch)
-reinterpret' = which (CaseReinterpret' @branch @tree @tree)
+reinterpret' = which (CaseReinterpret' @branch @tree @_ @tree)
 
-data CaseReinterpret' (branch :: [Type]) (tree :: [Type]) (tree' :: [Type]) r = CaseReinterpret'
+data CaseReinterpret' (branch :: [Type]) (tree :: [Type]) r (tree' :: [Type]) = CaseReinterpret'
 
-instance Reiterate (CaseReinterpret' branch tree) tree' where
+type instance CaseResult (CaseReinterpret' branch tree r) x = r
+
+instance Reiterate (CaseReinterpret' branch tree r) tree' where
     reiterate CaseReinterpret' = CaseReinterpret'
 
 instance ( MaybeUniqueMemberAt n x branch
@@ -482,7 +490,7 @@
          -- , MaybeUniqueMemberAt n' x comp
          , Unique x tree -- Compile error to ensure reinterpret only works with unique fields
          ) =>
-         Case (CaseReinterpret' branch tree) (x ': tree') (Maybe (Which branch)) where
+         Case (CaseReinterpret' branch tree (Maybe (Which branch))) (x ': tree') where
     case' CaseReinterpret' a =
         case fromInteger (natVal @n Proxy) of
             0 -> Nothing
@@ -508,7 +516,7 @@
     => proxy ls
     -> Which tree
     -> Either (Which (Complement tree branch)) (Which branch)
-reinterpretL _ = which (CaseReinterpret @branch @tree @tree)
+reinterpretL _ = which (CaseReinterpret @branch @tree @_ @tree)
 
 -- | Variation of 'reinterpretL' which returns a Maybe.
 reinterpretL'
@@ -521,13 +529,13 @@
     => proxy ls
     -> Which tree
     -> Maybe (Which branch)
-reinterpretL' _ = which (CaseReinterpret' @branch @tree @tree)
+reinterpretL' _ = which (CaseReinterpret' @branch @tree @_ @tree)
 
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpretN'.
 type ReinterpretN' (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
-    ( Reduce (Which tree) (SwitcherN (CaseReinterpretN' indices) 0 tree (Maybe (Which branch)))
+    ( Reduce (Which tree) (SwitcherN (CaseReinterpretN' indices) (Maybe (Which branch)) 0 tree)
     , KindsAtIndices indices tree ~ branch)
 
 -- | A limited variation of 'reinterpret' which uses a Nat list @n@ to specify how to reorder the fields, where
@@ -545,14 +553,17 @@
 --
 -- This is so that the same @indices@ can be used in 'narrowN'.
 reinterpretN' :: forall (indices :: [Nat]) branch tree proxy. (ReinterpretN' indices branch tree) => proxy indices -> Which tree -> Maybe (Which branch)
-reinterpretN' _ = whichN (CaseReinterpretN' @indices @0 @tree)
+reinterpretN' _ = whichN (CaseReinterpretN' @indices @_ @0 @tree)
 
-data CaseReinterpretN' (indices :: [Nat]) (n :: Nat) (tree' :: [Type]) r = CaseReinterpretN'
+data CaseReinterpretN' (indices :: [Nat]) r (n :: Nat) (tree' :: [Type]) = CaseReinterpretN'
 
-instance ReiterateN (CaseReinterpretN' indices) n tree' where
+type instance CaseResult (CaseReinterpretN' indices r n) x = r
+
+instance ReiterateN (CaseReinterpretN' indices r) n tree' where
     reiterateN CaseReinterpretN' = CaseReinterpretN'
 
-instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) => Case (CaseReinterpretN' indices n) (x ': tree) (Maybe (Which branch)) where
+instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) =>
+         Case (CaseReinterpretN' indices (Maybe (Which branch)) n) (x ': tree) where
     case' CaseReinterpretN' a =
         case fromInteger (natVal @n' Proxy) of
             0 -> Nothing
@@ -562,40 +573,46 @@
 
 -- | 'Switcher' is an instance of 'Reduce' for which __'reiterate'__s through the possibilities in a 'Which',
 -- delegating handling to 'Case', ensuring termination when 'Which' only contains one type.
-newtype Switcher c (xs :: [Type]) r = Switcher (c xs r)
-type instance Reduced (Switcher c xs r) = r
+newtype Switcher c r (xs :: [Type]) = Switcher (c r xs)
 
+type instance Reduced (Switcher c r xs) = r
+
 -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterate'__
 -- trying the next type in the type list.
-instance (Case c (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (Switcher c (x' ': xs) r), Reiterate c (x : x' : xs)) =>
-         Reduce (Which (x ': x' ': xs)) (Switcher c (x ': x' ': xs) r) where
+instance ( Case (c r) (x ': x' ': xs)
+         , Reduce (Which (x' ': xs)) (Switcher c r (x' ': xs))
+         , Reiterate (c r) (x : x' : xs)
+         , r ~ CaseResult (c r) x -- This means all @r@ for all typelist must be the same @r@
+         ) =>
+         Reduce (Which (x ': x' ': xs)) (Switcher c r (x ': x' ': xs)) where
     reduce (Switcher c) v =
         case trial0 v of
             Right a -> case' c a
             Left v' -> reduce (Switcher (reiterate c)) v'
-    -- Ghc 8.2.1 can optimize to single case statement. See https://ghc.haskell.org/trac/ghc/ticket/12877
-    {-# INLINABLE reduce #-} -- This makes compiling tests a little faster than with no pragma
+    -- GHC 8.2.1 can optimize to single case statement. See https://ghc.haskell.org/trac/ghc/ticket/12877
+    {-# INLINABLE reduce #-}
+     -- This makes compiling tests a little faster than with no pragma
 
 -- | Terminating case of the loop, ensuring that a instance of @Case '[]@
 -- with an empty typelist is not required.
 -- You can't reduce 'zilch'
-instance (Case c '[x] r) => Reduce (Which '[x]) (Switcher c '[x] r) where
+instance (Case (c r) '[x], r ~ CaseResult (c r) x) => Reduce (Which '[x]) (Switcher c r '[x]) where
     reduce (Switcher c) v = case obvious v of
             a -> case' c a
 
 -- | Allow 'Which \'[]' to be 'reinterpret''ed or 'diversify'ed into anything else
 -- This is safe because @Which '[]@ is uninhabited, and this is already something that
 -- can be done with 'impossible'
-instance Reduce (Which '[]) (Switcher c '[] r) where
+instance Reduce (Which '[]) (Switcher c r '[]) where
     reduce _ = impossible
 
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'switch'.
-type Switch case' xs r = Reduce (Which xs) (Switcher case' xs r)
+type Switch c r xs = Reduce (Which xs) (Switcher c r xs)
 
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@.
-which :: Switch case' xs r => case' xs r -> Which xs -> r
+which :: Switch c r xs => c r xs -> Which xs -> r
 which = reduce . Switcher
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@
@@ -618,39 +635,45 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switch :: Switch case' xs r => Which xs -> case' xs r -> r
+switch :: Switch c r xs => Which xs -> c r xs -> r
 switch = flip which
 
 ------------------------------------------------------------------
 
 -- | 'SwitcherN' is a variation of 'Switcher' which __'reiterateN'__s through the possibilities in a 'Which',
 -- delegating work to 'CaseN', ensuring termination when 'Which' only contains one type.
-newtype SwitcherN c (n :: Nat) (xs :: [Type]) r = SwitcherN (c n xs r)
-type instance Reduced (SwitcherN c n xs r) = r
+newtype SwitcherN c r (n :: Nat) (xs :: [Type]) = SwitcherN (c r n xs)
 
+type instance Reduced (SwitcherN c r n xs) = r
+
 -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterateN'__
 -- trying the next type in the type list.
-instance (Case (c n) (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (SwitcherN c (n + 1) (x' ': xs) r), ReiterateN c n (x : x' : xs)) =>
-         Reduce (Which (x ': x' ': xs)) (SwitcherN c n (x ': x' ': xs) r) where
+instance ( Case (c r n) (x ': x' ': xs)
+         , Reduce (Which (x' ': xs)) (SwitcherN c r (n + 1) (x' ': xs))
+         , ReiterateN (c r) n (x : x' : xs)
+         , r ~ CaseResult (c r n) x -- This means all @r@ for all typelist must be the same @r@
+         ) =>
+         Reduce (Which (x ': x' ': xs)) (SwitcherN c r n (x ': x' ': xs)) where
     reduce (SwitcherN c) v =
         case trial0 v of
             Right a -> case' c a
             Left v' -> reduce (SwitcherN (reiterateN c)) v'
     -- Ghc 8.2.1 can optimize to single case statement. See https://ghc.haskell.org/trac/ghc/ticket/12877
-    {-# INLINABLE reduce #-} -- This makes compiling tests a little faster than with no pragma
+    {-# INLINABLE reduce #-}
+ -- This makes compiling tests a little faster than with no pragma
 
 -- | Terminating case of the loop, ensuring that a instance of @Case '[]@
 -- with an empty typelist is not required.
 -- You can't reduce 'zilch'
-instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitcherN c n '[x] r) where
+instance (Case (c r n) '[x], r ~ CaseResult (c r n) x) => Reduce (Which '[x]) (SwitcherN c r n '[x]) where
     reduce (SwitcherN c) v = case obvious v of
             a -> case' c a
 
 -- | A friendlier constraint synonym for 'switch'.
-type SwitchN case' n xs r = Reduce (Which xs) (SwitcherN case' n xs r)
+type SwitchN c r n xs = Reduce (Which xs) (SwitcherN c r n xs)
 
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@.
-whichN :: SwitchN case' n xs r => case' n xs r -> Which xs -> r
+whichN :: SwitchN c r n xs => c r n xs -> Which xs -> r
 whichN = reduce . SwitcherN
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@
@@ -669,13 +692,14 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switchN :: SwitchN case' n xs r => Which xs -> case' n xs r -> r
+switchN :: SwitchN c r n xs => Which xs -> c r n xs -> r
 switchN = flip whichN
 
 -----------------------------------------------------------------
 
 -- | Two 'Which'es are only equal iff they both contain the equivalnet value at the same type index.
-instance (Reduce (Which (x ': xs)) (Switcher CaseEqWhich (x ': xs) Bool)) => Eq (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switcher CaseEqWhich Bool (x ': xs))) =>
+         Eq (Which (x ': xs)) where
     l@(Which i _) == (Which j u) =
         if i /= j
             then False
@@ -687,19 +711,21 @@
 
 -- | Do not export constructor
 -- Stores the right Any to be compared when the correct type is discovered
-newtype CaseEqWhich (xs :: [Type]) r = CaseEqWhich Any
+newtype CaseEqWhich r (xs :: [Type]) = CaseEqWhich Any
 
-instance Reiterate CaseEqWhich (x ': xs) where
+type instance CaseResult (CaseEqWhich r) x = r
+
+instance Reiterate (CaseEqWhich r) (x ': xs) where
     reiterate (CaseEqWhich r) = CaseEqWhich r
 
-instance (Eq x) => Case CaseEqWhich (x ': xs) Bool where
+instance Eq x => Case (CaseEqWhich Bool) (x ': xs) where
     case' (CaseEqWhich r) l = l == unsafeCoerce r
 
 -----------------------------------------------------------------
 
 -- | A 'Which' with a type at smaller type index is considered smaller.
-instance ( Reduce (Which (x ': xs)) (Switcher CaseEqWhich (x ': xs) Bool)
-         , Reduce (Which (x ': xs)) (Switcher CaseOrdWhich (x ': xs) Ordering)
+instance ( Reduce (Which (x ': xs)) (Switcher CaseEqWhich Bool (x ': xs))
+         , Reduce (Which (x ': xs)) (Switcher CaseOrdWhich Ordering (x ': xs))
          ) =>
          Ord (Which (x ': xs)) where
     compare l@(Which i _) (Which j u) =
@@ -713,30 +739,36 @@
 
 -- | Do not export constructor
 -- Stores the right Any to be compared when the correct type is discovered
-newtype CaseOrdWhich (xs :: [Type]) r = CaseOrdWhich Any
+newtype CaseOrdWhich r (xs :: [Type]) = CaseOrdWhich Any
 
-instance Reiterate CaseOrdWhich (x ': xs) where
+type instance CaseResult (CaseOrdWhich r) x = r
+
+instance Reiterate (CaseOrdWhich r) (x ': xs) where
     reiterate (CaseOrdWhich r) = CaseOrdWhich r
 
-instance (Ord x) => Case CaseOrdWhich (x ': xs) Ordering where
+instance Ord x => Case (CaseOrdWhich Ordering) (x ': xs) where
     case' (CaseOrdWhich r) l = compare l (unsafeCoerce r)
 
 ------------------------------------------------------------------
 
 -- | @show ('pick'' \'A') == "pick \'A'"@
-instance (Reduce (Which (x ': xs)) (Switcher CaseShowWhich (x ': xs) ShowS)) => Show (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switcher CaseShowWhich ShowS (x ': xs))) =>
+         Show (Which (x ': xs)) where
     showsPrec d v = showParen (d > app_prec) (which (CaseShowWhich 0) v)
-      where app_prec = 10
+      where
+        app_prec = 10
 
 instance Show (Which '[]) where
     showsPrec _ = impossible
 
-newtype CaseShowWhich (xs :: [Type]) r = CaseShowWhich Int
+newtype CaseShowWhich r (xs :: [Type]) = CaseShowWhich Int
 
-instance Reiterate CaseShowWhich (x ': xs) where
+type instance CaseResult (CaseShowWhich r) x = r
+
+instance Reiterate (CaseShowWhich r) (x ': xs) where
     reiterate (CaseShowWhich i) = CaseShowWhich (i + 1)
 
-instance Show x => Case CaseShowWhich (x ': xs) ShowS where
+instance Show x => Case (CaseShowWhich ShowS) (x ': xs) where
     case' (CaseShowWhich i) v = showString "pickN @" . showString (show i) . showString " Proxy " . showsPrec (app_prec + 1) v
       where app_prec = 10
 
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
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -10,15 +11,46 @@
 module Data.Diverse.ManySpec (main, spec) where
 
 import Data.Diverse
+import Data.Int
+import Data.Kind
 import Data.Tagged
 import Data.Typeable
 import Test.Hspec
 
+
 -- `main` is here so that this module can be run from GHCi on its own.  It is
--- not needed for automatic spec discovery.
+-- not needed for automatic spec dicovery.
 main :: IO ()
 main = hspec spec
 
+--------------------------------
+
+-- | Create an instance of 'Case' that can handle all 'Num'
+newtype CaseNum' (xs :: [Type]) = CaseNum' (forall x. Num x => x -> x)
+
+type instance CaseResult CaseNum' x = x
+
+instance Reiterate CaseNum' (x ': xs) where
+    reiterate (CaseNum' f) = CaseNum' f
+
+instance Num x => Case CaseNum' (x ': xs) where
+    case' (CaseNum' f) = f
+
+--------------------------------
+
+-- | Create an instance of 'Case' that can handle all 'Show' and convert to a specified type
+newtype CaseShow r (xs :: [Type]) = CaseShow (forall x. Show x => x -> r)
+
+type instance CaseResult (CaseShow r) x = r
+
+instance Reiterate (CaseShow r) (x ': xs) where
+    reiterate (CaseShow f) = CaseShow f
+
+instance Show x => Case (CaseShow r) (x ': xs) where
+    case' (CaseShow f) = f
+
+--------------------------------
+
 data Foo
 data Bar
 
@@ -310,3 +342,10 @@
                 ret = ["5", "False", "'X'", "Just 'O'", "6", "Just 'A'"]
             afoldr (:) [] (collectN x (casesN y)) `shouldBe` ret
             afoldr (:) [] (forManyN (casesN y) x) `shouldBe` ret
+
+        it "every item can be mapped into a different type in a Functor-like fashion with using 'afmap'" $ do
+            let x = (5 :: Int) ./ (6 :: Int8) ./ (7 :: Int16) ./ (8 :: Int32) ./ nil
+                y = (15 :: Int) ./ (16 :: Int8) ./ (17 :: Int16) ./ (18 :: Int32) ./ nil
+                z = ("5" :: String) ./ ("6" :: String) ./ ("7" :: String) ./ ("8" :: String) ./ nil
+            afmap (CaseNum' (+10)) x `shouldBe` y
+            afmap (CaseShow show) x `shouldBe` z