diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -48,3 +48,17 @@
 
 * 0.9.0.1
   - Fixed GHC 8.2.1 test failure due to changed TypeRep show instance.
+
+* 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.
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.9.0.1
+version:             0.10.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).
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
@@ -12,10 +12,12 @@
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
 module Data.Diverse.Cases
-    ( Cases(..)
+    ( Cases
     , cases
+    , cases'
     , CasesN
     , casesN
+    , casesN'
     ) where
 
 import Data.Diverse.Case
@@ -30,7 +32,6 @@
 -- 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.
--- However, the 'Cases' constructor is still exported to allow creating a master-of-all-'Case'.
 newtype Cases (fs :: [Type]) (xs :: [Type]) r = Cases (Many fs)
 
 instance Reiterate (Cases fs) xs where
@@ -62,9 +63,13 @@
 -- 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 :: SameLength fs (Nub xs) => Many fs -> (Cases fs) xs r
+cases :: forall r xs fs. (CasesResult fs ~ r, SameLength fs (Nub xs)) => Many fs -> Cases fs xs r
 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' = Cases
+
 -----------------------------------------------
 
 -- | A variation of 'Cases' which uses __'fetchN'__ to get the handler by index.
@@ -101,5 +106,9 @@
 -- 'Data.Diverse.AFoldable.afoldr' (:) [] ('collectN' x ('casesN' y)) \`shouldBe`
 --     [\"5", \"False", \"'X'", \"Just \'O'", \"6", \"Just \'A'"]
 -- @
-casesN :: SameLength fs xs => Many fs -> CasesN fs 0 xs r
+casesN :: forall r xs fs. SameLength fs xs => Many fs -> CasesN fs 0 xs r
 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' = 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
@@ -17,7 +17,7 @@
     , postfix'
     , (\.)
     , append
-    , append'
+    , CanAppendUnique(..)
     , (/./)
 
     -- * Simple queries
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
@@ -34,7 +34,7 @@
     , postfix'
     , (\.)
     , append
-    , append'
+    , CanAppendUnique(..)
     , (/./)
 
     -- * Simple queries
@@ -159,6 +159,10 @@
 
 fromMany_ :: Many_ xs -> Many xs
 fromMany_ (Many_ xs) = Many (S.fromList xs)
+
+getMany_ :: Many_ xs -> [Any]
+getMany_ (Many_ xs) = xs
+
 -----------------------------------------------------------------------
 
 instance NFData (Many '[])
@@ -279,13 +283,6 @@
 
 -----------------------------------------------------------------------
 
-instance Semigroup (Many '[]) where
-    _ <> _ = nil
-
-instance Monoid (Many '[]) where
-    mempty = nil
-    mappend = (<>)
-
 -- | Analogous to 'Prelude.null'. Named 'nil' to avoid conflicting with 'Prelude.null'.
 nil :: Many '[]
 nil = Many S.empty
@@ -318,10 +315,10 @@
 
 -- | Add an element to the right of a Many iff the field doesn't already exist.
 postfix'
-    :: forall xs y n.
+    :: forall y xs n.
        MaybeUniqueMemberAt n y xs
     => Many xs -> y -> Many (SnocUnique xs y)
-postfix'(Many ls) y = if i /= 0 then Many ls else Many (ls S.|> (unsafeCoerce y))
+postfix'(Many ls) y = if i /= 0 then Many ls else Many (ls S.|> unsafeCoerce y)
   where
     i = fromInteger (natVal @n Proxy) :: Int
 infixl 5 `postfix'`
@@ -352,7 +349,9 @@
 instance CanAppendUnique xs '[] where
    append' ls _ = ls
 
-instance (MaybeUniqueMemberAt n y xs, CanAppendUnique (SnocUnique xs y) ys) => CanAppendUnique xs (y ': ys) where
+instance ( MaybeUniqueMemberAt n y xs
+         , CanAppendUnique (SnocUnique xs y) ys
+         , AppendUnique (SnocUnique xs y) ys ~ AppendUnique xs (y : ys)) => CanAppendUnique xs (y ': ys) where
    append' ls rs = append' (postfix' ls r) rs'
      where (r, rs') = viewf rs
    {-# INLINABLE append' #-} -- This makes compiling tests a little faster than with no pragma
@@ -427,7 +426,7 @@
 -- 'fetchL' \@Foo Proxy y \`shouldBe` Tagged \@Foo \'X'
 -- 'fetchL' \@"Hi" Proxy y \`shouldBe` Tagged \@"Hi" True
 -- @
-fetchL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x
+fetchL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x
 fetchL _ = fetch_ @x
 
 --------------------------------------------------
@@ -481,7 +480,7 @@
 -- 'replaceL' \@\"Hello" Proxy y (Tagged \@\"Hello" 7) \`shouldBe`
 --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" (7 :: Int) './' 'nil'
 -- @
-replaceL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs
+replaceL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs
 replaceL _ = replace_ @x
 
 -- | Polymorphic setter by unique type. Set the field with type @x@, and replace with type @y@
@@ -493,7 +492,7 @@
 -- replaceL' \@\"Hello" Proxy y (Tagged \@\"Hello" False) \`shouldBe`
 --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" False './' 'nil'
 -- @
-replaceL' :: forall l y xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs)
+replaceL' :: forall l x y xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs)
 replaceL' _ = replace'_ @x Proxy
 
 --------------------------------------------------
@@ -824,16 +823,15 @@
 -----------------------------------------------------------------------
 
 -- | A friendlier type constraint synomyn for 'amend''
-type Amend' smaller smaller' larger zipped =
-    ( AFoldable (CollectorAny (CaseAmend' larger) zipped) (Int, WrappedAny)
-    , IsDistinct smaller
-    , zipped ~ Zip smaller smaller')
+type Amend' smaller smaller' larger =
+    ( AFoldable (CollectorAny (CaseAmend' larger) (Zip smaller smaller')) (Int, WrappedAny)
+    , IsDistinct smaller)
 
-amend' :: forall smaller smaller' larger proxy zipped. Amend' smaller smaller' larger zipped
+amend' :: forall smaller smaller' larger proxy. Amend' smaller smaller' larger
     => 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 @zipped) 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'' _ c (Many ys) = CollectorAny c (toList ys)
@@ -861,8 +859,8 @@
 --     False './' True './' Tagged \@Foo False './' Tagged \@Bar \'X' './' Tagged \@\"Changed" True './' 'nil'
 -- @
 amendL'
-    :: forall ls smaller smaller' larger proxy zipped.
-       ( Amend' smaller smaller' larger zipped
+    :: forall ls smaller smaller' larger proxy.
+       ( Amend' smaller smaller' larger
        , smaller ~ KindsAtLabels ls larger
        , IsDistinct ls
        , UniqueLabels ls larger
@@ -916,19 +914,18 @@
 -----------------------------------------------------------------------
 
 -- | A friendlier type constraint synomyn for 'amendN'
-type AmendN' ns smaller smaller' larger zipped =
-    ( AFoldable (CollectorAnyN (CaseAmendN' ns larger) 0 zipped) (Int, WrappedAny)
+type AmendN' ns smaller smaller' larger =
+    ( AFoldable (CollectorAnyN (CaseAmendN' ns larger) 0 (Zip smaller smaller')) (Int, WrappedAny)
     , smaller ~ KindsAtIndices ns larger
-    , IsDistinct ns
-    , zipped ~ Zip smaller smaller')
+    , IsDistinct ns)
 
 -- | A polymorphic variation of 'amendN'
-amendN' :: forall ns smaller smaller' larger proxy zipped.
-       (AmendN' ns smaller smaller' larger zipped)
+amendN' :: forall ns smaller smaller' larger proxy.
+       (AmendN' ns smaller smaller' larger)
     => 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 @zipped) 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'' _ c (Many ys) = CollectorAnyN c (toList ys)
@@ -975,6 +972,43 @@
 -- | Two 'Many's are ordered by 'compare'ing their fields in index order
 instance Ord (Many_ xs) => Ord (Many xs) where
     compare xs ys = compare (toMany_ xs) (toMany_ ys)
+
+
+-----------------------------------------------------------------------
+
+instance Semigroup (Many_ '[]) where
+    _ <> _ = Many_ []
+
+instance (Semigroup x, Semigroup (Many_ xs)) => Semigroup (Many_ (x ': xs)) where
+    Many_ (a : as) <> Many_ (b : bs) = Many_ (c : cs)
+      where
+        c = unsafeCoerce (unsafeCoerce a <> (unsafeCoerce b :: x))
+        cs = getMany_ (Many_ @xs as <> Many_ @xs bs)
+    _ <> _ = error "invalid Many_ Semigroup"
+
+instance Semigroup (Many_ xs) => Semigroup (Many xs) where
+    as <> bs = fromMany_ (toMany_ as <> toMany_ bs)
+
+-----------------------------------------------------------------------
+
+instance Monoid (Many_ '[]) where
+    mempty = Many_ []
+    mappend = (<>)
+
+instance (Monoid x, Monoid (Many_ xs)) => Monoid (Many_ (x ': xs)) where
+    mempty = Many_ (c : cs)
+      where
+        c = unsafeCoerce (mempty :: x)
+        cs = getMany_ (mempty :: Many_ xs)
+    Many_ (a : as) `mappend` Many_ (b : bs) = Many_ (c : cs)
+      where
+        c = unsafeCoerce (unsafeCoerce a `mappend` (unsafeCoerce b :: x))
+        cs = getMany_ (Many_ @xs as `mappend` Many_ @xs bs)
+    _ `mappend` _ = error "invalid Many_ Monoid"
+
+instance Monoid (Many_ xs) => Monoid (Many xs) where
+    mempty = fromMany_ (mempty :: Many_ xs)
+    as `mappend` bs = fromMany_ (toMany_ as `mappend` toMany_ bs)
 
 -----------------------------------------------------------------------
 
diff --git a/src/Data/Diverse/Reduce.hs b/src/Data/Diverse/Reduce.hs
--- a/src/Data/Diverse/Reduce.hs
+++ b/src/Data/Diverse/Reduce.hs
@@ -1,9 +1,11 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Data.Diverse.Reduce where
 
 -- | Convert something @v@ into @r@ using handlers.
 -- This class is required in order to step through all the different types in a variant.
-class Reduce v handler r where
-    reduce :: handler r -> v -> r
+type family Reduced handler
+class Reduce v handler where
+    reduce :: handler -> v -> Reduced handler
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
@@ -16,6 +16,11 @@
 -- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.
 type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))
 
+-- | Every x in @xs@ is a `UniqueMember x ys`
+type family UniqueMembers (xs :: [k]) (ys :: [k]) :: Constraint where
+    UniqueMembers '[] ys = ()
+    UniqueMembers (x ': xs) ys = (UniqueMember x ys, UniqueMembers xs ys)
+
 -- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.
 type UniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ IndexOf x xs)
 
@@ -39,7 +44,9 @@
 
 -- | For each @y@ in @ys@, snocs them to end of @xs@ if @y@ doesn't already exist in @xs@
 type family AppendUnique (xs :: [k]) (ys :: [k]) :: [k] where
+    AppendUnique '[] xs = xs
     AppendUnique xs '[] = xs
+    AppendUnique xs xs = xs
     AppendUnique xs (y ': ys) = AppendUnique (SnocUnique xs y) ys
 
 -- | Ensures x is a unique member in @xs@ iff it exists in @ys@
@@ -144,6 +151,7 @@
 
 -- | Returns a @xs@ appended with @ys@
 type family Append (xs :: [k]) (ys :: [k]) :: [k] where
+    Append xs '[] = xs
     Append '[] ys = ys
     Append (x ': xs) ys = x ': Append xs ys
 
@@ -155,3 +163,10 @@
 
 -- | 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")
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
@@ -192,3 +192,14 @@
                               ':<>: 'Text "‘"
                               ':<>: '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 "’")
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
@@ -5,7 +5,7 @@
 
       -- * Single type
       -- ** Construction
-    , impossible
+    , zilch
     , pick
     , pick0
     , pickOnly
@@ -14,14 +14,19 @@
       -- ** Destruction
     , obvious
     , trial
+    , trial'
     , trial0
+    , trial0'
     , trialL
+    , trialL'
     , trialN
+    , trialN'
 
       -- * Multiple types
       -- ** Injection
     , Diversify
     , diversify
+    , diversify'
     , diversify0
     , diversifyL
     , DiversifyN
@@ -29,15 +34,20 @@
       -- ** Inverse Injection
     , Reinterpret
     , reinterpret
+    , Reinterpret'
+    , reinterpret'
     , reinterpretL
-    , ReinterpretN
-    , reinterpretN
+    , reinterpretL'
+    , ReinterpretN'
+    , reinterpretN'
 
       -- * Catamorphism
-    , Switch(..)
+    , Switch
+    , Switcher(..)
     , which
     , switch
-    , SwitchN(..)
+    , SwitchN
+    , SwitcherN(..)
     , whichN
     , switchN
     ) where
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
@@ -19,7 +19,7 @@
 
       -- * Single type
       -- ** Construction
-    , impossible
+    , zilch
     , pick
     , pick0
     , pickOnly
@@ -28,14 +28,19 @@
       -- ** Destruction
     , obvious
     , trial
+    , trial'
     , trial0
+    , trial0'
     , trialL
+    , trialL'
     , trialN
+    , trialN'
 
       -- * Multiple types
       -- ** Injection
     , Diversify
     , diversify
+    , diversify'
     , diversify0
     , diversifyL
     , DiversifyN
@@ -43,15 +48,20 @@
       -- ** Inverse Injection
     , Reinterpret
     , reinterpret
+    , Reinterpret'
+    , reinterpret'
     , reinterpretL
-    , ReinterpretN
-    , reinterpretN
+    , reinterpretL'
+    , ReinterpretN'
+    , reinterpretN'
 
       -- * Catamorphism
-    , Switch(..)
+    , Switch
+    , Switcher(..)
     , which
     , switch
-    , SwitchN(..)
+    , SwitchN
+    , SwitcherN(..)
     , whichN
     , switchN
     ) where
@@ -116,12 +126,12 @@
 
 ----------------------------------------------
 
--- | A terminating 'G.Generic' instance for no types encoded as a 'impossible'.
+-- | A terminating 'G.Generic' instance for no types encoded as a 'zilch'.
 -- The 'G.C1' and 'G.S1' metadata are not encoded.
 instance G.Generic (Which '[]) where
   type Rep (Which '[]) = G.U1
   from _ = {- G.U1 -} G.U1
-  to G.U1 = impossible
+  to G.U1 = zilch
 
 -- | A terminating 'G.Generic' instance for one type encoded with 'pick''.
 -- The 'G.C1' and 'G.S1' metadata are not encoded.
@@ -144,27 +154,27 @@
 -----------------------------------------------------------------------
 
 instance Semigroup (Which '[]) where
-    _ <> _ = impossible
+    _ <> _ = zilch
 
 instance Monoid (Which '[]) where
-    mempty = impossible
+    mempty = zilch
     mappend = (<>)
 
--- | A 'Which' with no alternatives. You can't do anything with 'impossible'
+-- | A 'Which' with no alternatives. You can't do anything with 'zilch'
 -- except Eq, Read, and Show it.
--- Using functions like 'switch' and 'trial' with 'impossible' is a compile error.
--- 'impossible' is only useful as a 'Left'-over from 'trial'ing a @Which '[x]@ with one type.
-impossible :: Which '[]
-impossible = Which (-1) (unsafeCoerce ())
+-- Using functions like 'switch' and 'trial' with 'zilch' is a compile error.
+-- 'zilch' is useful as a 'Left'-over from 'trial'ing a @Which '[x]@ with one type.
+zilch :: Which '[]
+zilch = Which (-1) (unsafeCoerce ())
 
 -- | Lift a value into a 'Which' of possibly other types @xs@.
 -- @xs@ can be inferred or specified with TypeApplications.
 -- NB. forall is used to specify @xs@ first, so TypeApplications can be used to specify @xs@ first
 --
 -- @
--- 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: Which '[Int, Bool, Char, Maybe String]
+-- 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: Which '[Int, Bool, Char, Maybe String]
 -- @
-pick :: forall xs x. UniqueMember x xs => x -> Which xs
+pick :: forall x xs. UniqueMember x xs => x -> Which xs
 pick = pick_
 
 pick_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => x -> Which xs
@@ -177,7 +187,7 @@
 --     x = 'trialL' \@Foo Proxy y
 -- x `shouldBe` (Right (Tagged 5))
 -- @
-pickL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> x -> Which xs
+pickL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> x -> Which xs
 pickL _ = pick_ @x
 
 -- | A variation of 'pick' into a 'Which' of a single type.
@@ -201,7 +211,7 @@
 -- @
 -- 'pickN' (Proxy \@4) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char]
 -- @
-pickN :: forall n xs x proxy. MemberAt n x xs => proxy n -> x -> Which xs
+pickN :: forall n x xs proxy. MemberAt n x xs => proxy n -> x -> Which xs
 pickN _ = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce
 
 -- | It is 'obvious' what value is inside a 'Which' of one type.
@@ -227,7 +237,7 @@
 trial = trial_
 
 trial_
-    :: forall x xs n.
+    :: forall n x xs.
        (KnownNat n, n ~ IndexOf x xs)
     => Which xs -> Either (Which (Without x xs)) x
 trial_ (Which n v) = let i = fromInteger (natVal @n Proxy)
@@ -237,6 +247,22 @@
                           then Left (Which (n - 1) v)
                           else Left (Which n v)
 
+-- | Variation of 'trial' which returns a Maybe
+trial'
+    :: forall x xs.
+       (UniqueMember x xs)
+    => Which xs -> Maybe x
+trial' = trial_'
+
+trial_'
+    :: forall n x xs.
+       (KnownNat n, n ~ IndexOf x xs)
+    => Which xs -> Maybe x
+trial_' (Which n v) = let i = fromInteger (natVal @n Proxy)
+                  in if n == i
+                     then Just (unsafeCoerce v)
+                     else Nothing
+
 -- | A variation of 'trial' where x is specified via a label
 --
 -- @
@@ -245,30 +271,43 @@
 -- x `shouldBe` (Right (Tagged 5))
 -- @
 trialL
-    :: forall l xs x proxy.
+    :: forall l x xs proxy.
        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)
     => proxy l -> Which xs -> Either (Which (Without x xs)) x
-trialL _ = trial_ @x
+trialL _ = trial_ @_ @x
 
+-- | Variation of 'trialL' which returns a Maybe
+trialL'
+    :: forall l x xs proxy.
+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)
+    => proxy l -> Which xs -> Maybe x
+trialL' _ = trial_' @_ @x
+
 -- | A variation of a 'Which' 'trial' which 'trial's the first type in the type list.
 --
 -- @
 -- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
 -- 'trial0' x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String]
 -- @
-trial0 :: Which (x ': xs) -> Either (Which xs) x
+trial0 :: forall x xs. Which (x ': xs) -> Either (Which xs) x
 trial0 (Which n v) = if n == 0
            then Right (unsafeCoerce v)
            else Left (Which (n - 1) v)
 
+-- | Variation of 'trial0' which returns a Maybe
+trial0' :: forall x xs.  Which (x ': xs) -> Maybe x
+trial0' (Which n v) = if n == 0
+           then Just (unsafeCoerce v)
+           else Nothing
+
 -- | 'trialN' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities.
 --
 -- @
--- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
--- 'trialN' @1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String]
+-- let x = 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
+-- 'trialN' \@_ \@1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String]
 -- @
 trialN
-    :: forall n xs x proxy.
+    :: forall n x xs proxy.
        (MemberAt n x xs)
     => proxy n -> Which xs -> Either (Which (WithoutIndex n xs)) x
 trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy)
@@ -278,10 +317,20 @@
                           then Left (Which (n - 1) v)
                           else Left (Which n v)
 
+-- | Variation of 'trialN' which returns a Maybe
+trialN'
+    :: forall n x xs proxy.
+       (MemberAt n x xs)
+    => proxy n -> Which xs -> Maybe x
+trialN' _ (Which n v) = let i = fromInteger (natVal @n Proxy)
+                  in if n == i
+                     then Just (unsafeCoerce v)
+                     else Nothing
+
 -----------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversify'.
-type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce (Which branch) (Switch (CaseDiversify tree branch) branch) (Which tree)
+type Diversify (branch :: [Type]) (tree :: [Type]) = Reduce (Which branch) (Switcher (CaseDiversify branch tree) branch (Which tree))
 
 -- | Convert a 'Which' to another 'Which' that may include other possibilities.
 -- That is, @branch@ is equal or is a subset of @tree@.
@@ -297,23 +346,27 @@
 --     b = 'diversify' \@[Int, Bool] a :: 'Which' '[Int, Bool]
 --     c = 'diversify' \@[Bool, Int] b :: 'Which' '[Bool, Int]
 -- @
-diversify :: forall tree branch. Diversify tree branch => Which branch -> Which tree
-diversify = which (CaseDiversify @tree @branch @branch)
+diversify :: forall branch tree. Diversify branch tree => Which branch -> Which tree
+diversify = which (CaseDiversify @branch @tree @branch)
 
-data CaseDiversify (tree :: [Type]) (branch :: [Type]) (branch' :: [Type]) r = CaseDiversify
+data CaseDiversify (branch :: [Type]) (tree :: [Type]) (branch' :: [Type]) r = CaseDiversify
 
-instance Reiterate (CaseDiversify tree branch) branch' where
+instance Reiterate (CaseDiversify 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 tree branch) (x ': branch') (Which tree) where
+         Case (CaseDiversify branch tree) (x ': branch') (Which tree) where
     case' CaseDiversify = pick
 
 -- | A simple version of 'diversify' which add another type to the front of the typelist.
 diversify0 :: forall x xs. Which xs -> Which (x ': xs)
 diversify0 (Which n v) = Which (n + 1) v
 
+-- | A restricted version of 'diversify' which only rearranges the types
+diversify' :: forall branch tree. (Diversify branch tree, SameLength branch tree) => Which branch -> Which tree
+diversify' = diversify
+
 ------------------------------------------------------------------
 
 -- | A variation of 'diversify' where @branch@is additionally specified by a labels list.
@@ -325,20 +378,20 @@
 -- 'switch' y'' ('Data.Diverse.CaseTypeable.CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Tagged * Bar Int"
 -- @
 diversifyL
-    :: forall ls tree branch proxy.
-       ( Diversify tree branch
+    :: forall ls branch tree proxy.
+       ( Diversify branch tree
        , branch ~ KindsAtLabels ls tree
        , UniqueLabels ls tree
        , IsDistinct ls
        )
     => proxy ls -> Which branch -> Which tree
-diversifyL _ = which (CaseDiversify @tree @branch @branch)
+diversifyL _ = which (CaseDiversify @branch @tree @branch)
 
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversifyN'.
-type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) =
-    ( Reduce (Which branch) (SwitchN (CaseDiversifyN indices) 0 branch) (Which tree)
+type DiversifyN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
+    ( Reduce (Which branch) (SwitcherN (CaseDiversifyN indices) 0 branch (Which tree))
     , KindsAtIndices indices tree ~ branch)
 
 -- | A variation of 'diversify' which uses a Nat list @indices@ to specify how to reorder the fields, where
@@ -356,7 +409,7 @@
 --     y'' = 'diversifyN' \@[1,0] \@[Bool, Int] Proxy y'
 -- 'switch' y'' ('Data.Diverse.CaseTypeable.CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Int"
 -- @
-diversifyN :: forall indices tree branch proxy. (DiversifyN indices tree branch) => proxy indices -> Which branch -> Which tree
+diversifyN :: forall indices branch tree proxy. (DiversifyN indices branch tree) => proxy indices -> Which branch -> Which tree
 diversifyN _ = whichN (CaseDiversifyN @indices @0 @branch)
 
 data CaseDiversifyN (indices :: [Nat]) (n :: Nat) (branch' :: [Type]) r = CaseDiversifyN
@@ -371,7 +424,7 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpret'.
-type Reinterpret branch tree = Reduce (Which tree) (Switch (CaseReinterpret branch tree) tree) (Either (Which (Complement tree branch)) (Which branch))
+type Reinterpret branch tree = Reduce (Which tree) (Switcher (CaseReinterpret branch tree) tree (Either (Which (Complement tree branch)) (Which branch)))
 
 -- | 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.
@@ -410,6 +463,31 @@
 
 ------------------------------------------------------------------
 
+-- | A friendlier constraint synonym for 'reinterpret''.
+type Reinterpret' branch tree = Reduce (Which tree) (Switcher (CaseReinterpret' branch tree) tree (Maybe (Which branch)))
+
+-- | 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)
+
+data CaseReinterpret' (branch :: [Type]) (tree :: [Type]) (tree' :: [Type]) r = CaseReinterpret'
+
+instance Reiterate (CaseReinterpret' branch tree) tree' where
+    reiterate CaseReinterpret' = CaseReinterpret'
+
+instance ( MaybeUniqueMemberAt n x branch
+         , comp ~ Complement tree branch
+         -- , 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' a =
+        case fromInteger (natVal @n Proxy) of
+            0 -> Nothing
+            i -> Just $ Which (i - 1) (unsafeCoerce a)
+
+------------------------------------------------------------------
+
 -- | A variation of 'reinterpret' where the @branch@ is additionally specified with a labels list.
 --
 -- @
@@ -430,11 +508,24 @@
     -> Either (Which (Complement tree branch)) (Which branch)
 reinterpretL _ = which (CaseReinterpret @branch @tree @tree)
 
+-- | Variation of 'reinterpretL' which returns a Maybe.
+reinterpretL'
+    :: forall ls branch tree proxy.
+       ( Reinterpret' branch tree
+       , branch ~ KindsAtLabels ls tree
+       , UniqueLabels ls tree
+       , IsDistinct ls
+       )
+    => proxy ls
+    -> Which tree
+    -> Maybe (Which branch)
+reinterpretL' _ = which (CaseReinterpret' @branch @tree @tree)
+
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpretN'.
-type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
-    ( Reduce (Which tree) (SwitchN (CaseReinterpretN indices) 0 tree) (Maybe (Which branch))
+type ReinterpretN' (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
+    ( Reduce (Which tree) (SwitcherN (CaseReinterpretN' indices) 0 tree (Maybe (Which branch)))
     , KindsAtIndices indices tree ~ branch)
 
 -- | A limited variation of 'reinterpret' which uses a Nat list @n@ to specify how to reorder the fields, where
@@ -451,47 +542,63 @@
 -- Also it returns a Maybe instead of Either.
 --
 -- 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' :: forall (indices :: [Nat]) branch tree proxy. (ReinterpretN' indices branch tree) => proxy indices -> Which tree -> Maybe (Which branch)
+reinterpretN' _ = whichN (CaseReinterpretN' @indices @0 @tree)
 
-data CaseReinterpretN (indices :: [Nat]) (n :: Nat) (tree' :: [Type]) r = CaseReinterpretN
+data CaseReinterpretN' (indices :: [Nat]) (n :: Nat) (tree' :: [Type]) r = CaseReinterpretN'
 
-instance ReiterateN (CaseReinterpretN indices) n tree' where
-    reiterateN CaseReinterpretN = CaseReinterpretN
+instance ReiterateN (CaseReinterpretN' indices) 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
-    case' CaseReinterpretN a =
+instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) => Case (CaseReinterpretN' indices n) (x ': tree) (Maybe (Which branch)) where
+    case' CaseReinterpretN' a =
         case fromInteger (natVal @n' Proxy) of
             0 -> Nothing
             i -> Just $ Which (i - 1) (unsafeCoerce a)
 
 ------------------------------------------------------------------
 
--- | 'Switch' is an instance of 'Reduce' for which __'reiterate'__s through the possibilities in a 'Which',
+-- | '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 Switch c (xs :: [Type]) r = Switch (c xs r)
+newtype Switcher c (xs :: [Type]) r = Switcher (c xs r)
+type instance Reduced (Switcher c xs r) = 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)) (Switch c (x' ': xs)) r, Reiterate c (x : x' : xs)) =>
-         Reduce (Which (x ': x' ': xs)) (Switch c (x ': x' ': xs)) r where
-    reduce (Switch c) v =
+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
+    reduce (Switcher c) v =
         case trial0 v of
             Right a -> case' c a
-            Left v' -> reduce (Switch (reiterate c)) v'
+            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
 
 -- | Terminating case of the loop, ensuring that a instance of @Case '[]@
 -- with an empty typelist is not required.
--- You can't reduce 'impossible'
-instance (Case c '[x] r) => Reduce (Which '[x]) (Switch c '[x]) r where
-    reduce (Switch c) v = case obvious v of
+-- You can't reduce 'zilch'
+instance (Case c '[x] r) => Reduce (Which '[x]) (Switcher c '[x] r) where
+    reduce (Switcher c) v = case obvious v of
             a -> case' c a
 
+-- | Allow 'zilch' to be 'reinterpret''ed into 'zilch'
+instance Reduce (Which '[]) (Switcher (CaseReinterpret' '[] '[]) '[] (Maybe (Which '[]))) where
+    reduce _ = Just
+
+-- | Allow 'zilch' to be 'reinterpret'ed into 'zilch'
+instance Reduce (Which '[]) (Switcher (CaseReinterpret '[] '[]) '[] (Either (Which '[]) (Which '[]))) where
+    reduce _ = Right
+
+-- | Allow 'zilch' to be 'diversify'ed into 'zilch'
+instance Reduce (Which '[]) (Switcher (CaseDiversify '[] '[]) '[] (Which '[])) where
+    reduce _ = id
+
+-- | A friendlier constraint synonym for 'switch'.
+type Switch case' xs r = Reduce (Which xs) (Switcher case' xs r)
+
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@.
-which :: Reduce (Which xs) (Switch case' xs) r => case' xs r -> Which xs -> r
-which = reduce . Switch
+which :: Switch case' xs r => case' xs r -> Which xs -> r
+which = reduce . Switcher
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@
 --
@@ -513,36 +620,40 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switch :: Reduce (Which xs) (Switch case' xs) r => Which xs -> case' xs r -> r
+switch :: Switch case' xs r => Which xs -> case' xs r -> r
 switch = flip which
 
 ------------------------------------------------------------------
 
--- | 'SwitchN' is a variation of 'Switch' which __'reiterateN'__s through the possibilities in a '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 SwitchN c (n :: Nat) (xs :: [Type]) r = SwitchN (c n xs r)
+newtype SwitcherN c (n :: Nat) (xs :: [Type]) r = SwitcherN (c n xs r)
+type instance Reduced (SwitcherN c n xs r) = 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)) (SwitchN c (n + 1) (x' ': xs)) r, ReiterateN c n (x : x' : xs)) =>
-         Reduce (Which (x ': x' ': xs)) (SwitchN c n (x ': x' ': xs)) r where
-    reduce (SwitchN c) v =
+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
+    reduce (SwitcherN c) v =
         case trial0 v of
             Right a -> case' c a
-            Left v' -> reduce (SwitchN (reiterateN c)) v'
+            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
 
 -- | Terminating case of the loop, ensuring that a instance of @Case '[]@
 -- with an empty typelist is not required.
--- You can't reduce 'impossible'
-instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitchN c n '[x]) r where
-    reduce (SwitchN c) v = case obvious v of
+-- You can't reduce 'zilch'
+instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitcherN c n '[x] r) 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)
+
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@.
-whichN :: Reduce (Which xs) (SwitchN case' n xs) r => case' n xs r -> Which xs -> r
-whichN = reduce . SwitchN
+whichN :: SwitchN case' n xs r => case' n xs r -> Which xs -> r
+whichN = reduce . SwitcherN
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@
 --
@@ -560,19 +671,19 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switchN :: Reduce (Which xs) (SwitchN case' n xs) r => Which xs -> case' n xs r -> r
+switchN :: SwitchN case' n xs r => Which xs -> case' n xs r -> 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)) (Switch CaseEqWhich (x ': xs)) Bool) => Eq (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switcher CaseEqWhich (x ': xs) Bool)) => Eq (Which (x ': xs)) where
     l@(Which i _) == (Which j u) =
         if i /= j
             then False
             else switch l (CaseEqWhich u)
 
--- | @('impossible' == 'impossible') == True@
+-- | @('zilch' == 'zilch') == True@
 instance Eq (Which '[]) where
     _ == _ = True
 
@@ -589,8 +700,8 @@
 -----------------------------------------------------------------
 
 -- | A 'Which' with a type at smaller type index is considered smaller.
-instance ( Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool
-         , Reduce (Which (x ': xs)) (Switch CaseOrdWhich (x ': xs)) Ordering
+instance ( Reduce (Which (x ': xs)) (Switcher CaseEqWhich (x ': xs) Bool)
+         , Reduce (Which (x ': xs)) (Switcher CaseOrdWhich (x ': xs) Ordering)
          ) =>
          Ord (Which (x ': xs)) where
     compare l@(Which i _) (Which j u) =
@@ -598,7 +709,7 @@
             then compare i j
             else switch l (CaseOrdWhich u)
 
--- | @('compare' 'impossible' 'impossible') == EQ@
+-- | @('compare' 'zilch' 'zilch') == EQ@
 instance Ord (Which '[]) where
     compare _ _ = EQ
 
@@ -615,13 +726,13 @@
 ------------------------------------------------------------------
 
 -- | @show ('pick'' \'A') == "pick \'A'"@
-instance (Reduce (Which (x ': xs)) (Switch CaseShowWhich (x ': xs)) ShowS) => Show (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switcher CaseShowWhich (x ': xs) ShowS)) => Show (Which (x ': xs)) where
     showsPrec d v = showParen (d > app_prec) (which (CaseShowWhich 0) v)
       where app_prec = 10
 
--- | @read "impossible" == 'impossible'@
+-- | @read "zilch" == 'zilch'@
 instance Show (Which '[]) where
-    showsPrec d _ = showParen (d > app_prec) (showString "impossible")
+    showsPrec d _ = showParen (d > app_prec) (showString "zilch")
       where app_prec = 10
 
 newtype CaseShowWhich (xs :: [Type]) r = CaseShowWhich Int
@@ -670,11 +781,11 @@
       where
         app_prec = 10
 
--- | @read "impossible" == 'impossible'@
+-- | @read "zilch" == 'zilch'@
 instance Read (Which '[]) where
     readPrec =
         parens $ prec app_prec $ do
-            lift $ L.expect (Ident "impossible")
-            pure impossible
+            lift $ L.expect (Ident "zilch")
+            pure zilch
       where
         app_prec = 10
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
@@ -40,14 +40,14 @@
             let s = "pickN @0 Proxy 5"
                 x = read s :: Which '[Int, Bool]
             show x `shouldBe` s
-            "impossible" `shouldBe` show impossible
-            "impossible" `shouldBe` show (read "impossible" :: Which '[])
+            "zilch" `shouldBe` show zilch
+            "zilch" `shouldBe` show (read "zilch" :: Which '[])
 
         it "is an Eq" $ do
             let y = pick (5 :: Int) :: Which '[Int, Bool]
             let y' = pick (5 :: Int) :: Which '[Int, Bool]
             y `shouldBe` y'
-            read (show impossible) `shouldBe` impossible
+            read (show zilch) `shouldBe` zilch
 
         it "is an Ord" $ do
             let y5 = pick (5 :: Int) :: Which '[Int, Bool]
@@ -55,7 +55,7 @@
             compare y5 y5 `shouldBe` EQ
             compare y5 y6 `shouldBe` LT
             compare y6 y5 `shouldBe` GT
-            compare impossible impossible `shouldBe` EQ
+            compare zilch zilch `shouldBe` EQ
 
         it "can be constructed by type with 'pick' and destructed with 'trial'" $ do
             let y = pick (5 :: Int) :: Which '[Bool, Int, Char]
@@ -83,10 +83,10 @@
             x `shouldBe` (Just 5)
 
         it "can be 'trial'led until its final 'obvious' value" $ do
-            let a = pick @'[Char, Int, Bool, String] (5 :: Int)
-                b = pick @'[Char, Int, String] (5 :: Int)
-                c = pick @'[Int, String] (5 :: Int)
-                d = pick @'[Int] (5 :: Int)
+            let a = pick @_ @'[Char, Int, Bool, String] (5 :: Int)
+                b = pick @_ @'[Char, Int, String] (5 :: Int)
+                c = pick @_ @'[Int, String] (5 :: Int)
+                d = pick @_ @'[Int] (5 :: Int)
             trial @Int a `shouldBe` Right 5
             trial @Bool a `shouldBe` Left b
             trial @Int b `shouldBe` Right 5
@@ -94,16 +94,16 @@
             trial @Int c `shouldBe` Right 5
             trial @String c `shouldBe` Left d
             trial @Int d `shouldBe` Right 5
-            trial @Int d `shouldNotBe` Left impossible
+            trial @Int d `shouldNotBe` Left zilch
             obvious d `shouldBe` 5
 
         it "can be 'trialN'led until its final 'obvious' value" $ do
-            let a = pickN @2 @'[Char, Bool, Int, Bool, Char, String] Proxy (5 :: Int)
-                b = pickN @2 @'[Char, Bool, Int, Char, String] Proxy (5 :: Int)
-                c = pickN @2 @'[Char, Bool, Int, String] Proxy (5 :: Int)
-                d = pickN @1 @'[Bool, Int, String] Proxy (5 :: Int)
-                e = pickN @1 @'[Bool, Int] Proxy (5 :: Int)
-                f = pickN @0 @'[Int] Proxy (5 :: Int)
+            let a = pickN @2 @_ @'[Char, Bool, Int, Bool, Char, String] Proxy (5 :: Int)
+                b = pickN @2 @_ @'[Char, Bool, Int, Char, String] Proxy (5 :: Int)
+                c = pickN @2 @_ @'[Char, Bool, Int, String] Proxy (5 :: Int)
+                d = pickN @1 @_ @'[Bool, Int, String] Proxy (5 :: Int)
+                e = pickN @1 @_ @'[Bool, Int] Proxy (5 :: Int)
+                f = pickN @0 @_ @'[Int] Proxy (5 :: Int)
             trial @Int a `shouldBe` Right 5
             trialN @2 Proxy a `shouldBe` Right 5
             trialN @3 Proxy a `shouldBe` Left b
@@ -127,14 +127,14 @@
             trial0 e `shouldBe` Left f
 
             trial @Int f `shouldBe` Right 5
-            trial @Int f `shouldNotBe` Left impossible
+            trial @Int f `shouldNotBe` Left zilch
             trial0 f `shouldBe` Right 5
             obvious f `shouldBe` 5
 
         it "can be extended and rearranged by type with 'diversify'" $ do
             let y = pickOnly (5 :: Int)
-                y' = diversify @[Int, Bool] y
-                y'' = diversify @[Bool, Int] y'
+                y' = diversify @_ @[Int, Bool] y
+                y'' = diversify @_ @[Bool, Int] y'
             switch y'' (CaseTypeable (show . typeRep . (pure @Proxy))) `shouldBe` "Int"
 
         it "can be extended and rearranged by type with 'diversify'" $ do
@@ -145,25 +145,25 @@
 
         it "can be extended and rearranged by index with 'diversifyN'" $ do
             let y = pickOnly (5 :: Int)
-                y' = diversifyN @'[0] @[Int, Bool] Proxy y
-                y'' = diversifyN @[1,0] @[Bool, Int] Proxy y'
+                y' = diversifyN @'[0] @_ @[Int, Bool] Proxy y
+                y'' = diversifyN @[1,0] @_ @[Bool, Int] Proxy y'
             switch y'' (CaseTypeable (show . typeRep . (pure @Proxy))) `shouldBe` "Int"
 
         it "the 'diversify'ed type can contain multiple fields if they aren't in the original 'Many'" $ do
-            let y = pick @[Int, Char] (5 :: Int)
-                x = diversify @[String, String, Char, Bool, Int] y
+            let y = pick @_ @[Int, Char] (5 :: Int)
+                x = diversify @_ @[String, String, Char, Bool, Int] y
                 -- Compile error: Char is a duplicate
                 -- z = diversify @[String, String, Char, Bool, Int, Char] y
             x `shouldBe` pick (5 :: Int)
 
         it "the 'diversify'ed type can't use indistinct fields from the original 'Many'" $ do
-            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
+            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
                 -- Compile error: Int is a duplicate
                 -- x = diversify @[String, String, Char, Bool, Int] y
             y `shouldBe` y
 
         it "can be 'reinterpret'ed by type into a totally different Which" $ do
-            let y = pick @[Int, Char] (5 :: Int)
+            let y = pick @_ @[Int, Char] (5 :: Int)
                 a = reinterpret @[String, Bool] y
             a `shouldBe` Left y
             let  b = reinterpret @[String, Char] y
@@ -172,34 +172,34 @@
             c `shouldBe` Right (pick (5 :: Int))
 
         it "can be 'reinterpretL'ed by label into a totally different Which" $ do
-            let y = pick @[Tagged Bar Int, Tagged Foo Bool, Tagged Hi Char, Tagged Bye Bool] (5 :: Tagged Bar Int)
+            let y = pick @_ @[Tagged Bar Int, Tagged Foo Bool, Tagged Hi Char, Tagged Bye Bool] (5 :: Tagged Bar Int)
                 y' = reinterpretL @[Foo, Bar] Proxy y
-                x = pick @[Tagged Foo Bool, Tagged Bar Int] (5 :: Tagged Bar Int)
+                x = pick @_ @[Tagged Foo Bool, Tagged Bar Int] (5 :: Tagged Bar Int)
             y' `shouldBe` Right x
 
         it "the 'reinterpret' type can contain indistinct fields if they aren't in the original 'Many'" $ do
-            let y = pick @[Int, Char] (5 :: Int)
+            let y = pick @_ @[Int, Char] (5 :: Int)
                 x = reinterpret @[String, String, Char, Bool] y
                 -- Compile error: Char is a duplicate
                 -- z = reinterpret @[String, Char, Char, Bool] y
             x `shouldBe` Left (pick (5 :: Int))
 
         it "the 'reinterpret'ed from type can't indistinct fields'" $ do
-            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
+            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
                 -- Compile error: Int is a duplicate
                 -- x = reinterpret @[String, String, Char, Bool] y
             y `shouldBe` y
 
         it "the 'reinterpret' type can't use indistinct fields from the original 'Many'" $ do
-            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
+            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int
                 -- Compile error: Int is a duplicate
                 -- x = reinterpret @[String, String, Char, Bool, Int] y
             y `shouldBe` y
 
         it "can be 'reinterpretN'ed by index into a subset Which" $ do
-            let y = pick @[Char, String, Int, Bool] (5 :: Int)
-                a = reinterpretN @[2, 0] @[Int, Char] Proxy y
-                a' = reinterpretN @[3, 0] @[Bool, Char] Proxy y
+            let y = pick @_ @[Char, String, Int, Bool] (5 :: Int)
+                a = reinterpretN' @[2, 0] @[Int, Char] Proxy y
+                a' = reinterpretN' @[3, 0] @[Bool, Char] Proxy y
             a `shouldBe` Just (pick (5 :: Int))
             a' `shouldBe` Nothing
 
@@ -214,11 +214,11 @@
             let y = pick (5 :: Int) :: Which '[Int, Bool]
             switch y (
                 -- contrast with lowercase 'cases' which disallows extraneous content
-                Cases (show @Int
+                cases' (show @Int
                     ./ show @Bool
                     ./ show @Char
-                    ./ 'X'
-                    ./ False
+                    ./ show @(Maybe Char)
+                    ./ show @(Maybe Int)
                     ./ nil
                 )) `shouldBe` "5"
 
@@ -241,10 +241,18 @@
 #endif
             (show . typeRep . (pure @Proxy) $ y) `shouldBe` expected
 
-        it "is a compile error to 'trial', 'diversify', 'reinterpret 'impossible'" $ do
-            -- let a = diversify @[Int, Bool] impossible
-            -- let a = trial @Int impossible
-            -- let a = trialN (Proxy @0) impossible
-            -- let a = reinterpret @[Int, Bool] impossible
-            -- let a = reinterpretN (Proxy @'[0]) impossible
-            impossible `shouldBe` impossible
+        it "is a compile error to 'trial', 'diversify', 'reinterpret from non-zilch to 'zilch'" $ do
+            -- let a = diversify @[Int, Bool] zilch
+            -- let a = trial @Int zilch
+            -- let a = trialN (Proxy @0) zilch
+            -- let a = reinterpret @[Int, Bool] zilch
+            -- let a = reinterpretN (Proxy @'[0]) zilch
+            zilch `shouldBe` zilch
+
+        it "is ok to 'reinterpret' and 'diversity' into 'zilch'" $ do
+            let x = pick @_ @'[Int] (5 :: Int)
+            reinterpret' @'[] x `shouldBe` Nothing
+            reinterpret' @'[] zilch `shouldBe` Just zilch
+            reinterpret @'[] x `shouldBe` Left x
+            reinterpret @'[] zilch `shouldBe` Right zilch
+            diversify @'[] zilch `shouldBe` zilch