diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
 
 "Data.Diverse.Which" polymorphic variant of possibilities encoded as (Int, Any).
 
-Provides getters, setters, projection, injection, fold, and catamorphisms;
-accessed by type or index.
+Provides getters, setters, projection, injection, folds, and catamorphisms;
+accessed by type or index or label.
 
 Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages.
diff --git a/data-diverse.cabal b/data-diverse.cabal
--- a/data-diverse.cabal
+++ b/data-diverse.cabal
@@ -1,10 +1,10 @@
 name:                data-diverse
-version:             0.4.0.0
+version:             0.5.0.0
 synopsis:            Extensible records and polymorphic variants.
 description:         "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Int, Map Int Any).
                      "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any).
-                     Provides getters, setters, projection, injection, fold, and catamorphisms;
-                     accessed by type or index.
+                     Provides getters, setters, projection, injection, folds, and catamorphisms;
+                     accessed by type, index or label.
                      Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages.
 homepage:            https://github.com/louispan/data-diverse#readme
 license:             BSD3
@@ -16,7 +16,7 @@
 build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
-tested-with:         GHC == 8.0.1
+tested-with:         GHC == 8.0.2
 
 library
   hs-source-dirs:      src
@@ -29,10 +29,10 @@
                        Data.Diverse.Many.Internal
                        Data.Diverse.Reduce
                        Data.Diverse.Reiterate
-                       Data.Diverse.Type
+                       Data.Diverse.TypeLevel
+                       Data.Diverse.TypeLevel.Internal
                        Data.Diverse.Which
                        Data.Diverse.Which.Internal
-  other-modules:       Data.Diverse.Type.Internal
   build-depends:       base >= 4.7 && < 5
                      , containers >= 0.5 && < 0.6
                      , ghc-prim >= 0.5 && < 1
diff --git a/src/Data/Diverse.hs b/src/Data/Diverse.hs
--- a/src/Data/Diverse.hs
+++ b/src/Data/Diverse.hs
@@ -6,7 +6,7 @@
     , module Data.Diverse.Many
     , module Data.Diverse.Reduce
     , module Data.Diverse.Reiterate
-    , module Data.Diverse.Type
+    , module Data.Diverse.TypeLevel
     , module Data.Diverse.Which
     ) where
 
@@ -17,5 +17,5 @@
 import Data.Diverse.Many
 import Data.Diverse.Reduce
 import Data.Diverse.Reiterate
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Diverse.Which
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
@@ -6,7 +6,7 @@
 
 module Data.Diverse.Case where
 
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 
 -- | This class allows defining handlers that can handle the 'Head' type in the @xs@ typelist.
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
@@ -9,7 +9,7 @@
 
 import Data.Diverse.Case
 import Data.Diverse.Reiterate
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 import Data.Typeable
 
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
@@ -21,7 +21,7 @@
 import Data.Diverse.Case
 import Data.Diverse.Many
 import Data.Diverse.Reiterate
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 import Data.Proxy
 import GHC.TypeLits
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
@@ -103,7 +103,7 @@
 import Data.Diverse.AFoldable
 import Data.Diverse.Case
 import Data.Diverse.Reiterate
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 import qualified Data.Map.Strict as M
 import Data.Proxy
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,12 +1,9 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
 module Data.Diverse.Reduce where
 
-import Data.Kind
-
--- | Reduce a polymorphic variant @v xs@ into @r@ using handlers.
+-- | 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 (xs :: [Type]) r where
-    reduce :: handler xs r -> v xs -> r
+class Reduce v handler r where
+    reduce :: handler r -> v -> r
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
@@ -6,7 +6,7 @@
 
 module Data.Diverse.Reiterate where
 
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 import GHC.TypeLits
 
diff --git a/src/Data/Diverse/Type.hs b/src/Data/Diverse/Type.hs
deleted file mode 100644
--- a/src/Data/Diverse/Type.hs
+++ /dev/null
@@ -1,145 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeInType #-}
-
-module Data.Diverse.Type where
-
-import Data.Diverse.Type.Internal
-import Data.Kind
-import GHC.TypeLits
-
--- | 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))
-
--- | 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)
-
--- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.
-type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs))
-
--- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natVal' can be used.
-type MaybeUniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ PositionOf x xs)
-
--- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natVal' can be used.
-type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs)
-
--- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used.
-type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)
-
--- | Ensures x is a unique member in @xs@ iff it exists in @ys@
-type family UniqueIfExists ys x xs :: Constraint where
-    UniqueIfExists '[] x xs = ()
-    UniqueIfExists (y ': ys) y xs = Unique y xs
-    UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs
-
--- | Ensures that the type list contain unique types
-type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs
-
--- | Return the list of distinct types in a typelist
-type family Nub (xs :: [k]) :: [k] where
-    Nub '[] = '[]
-    Nub (x ': xs) = NubImpl xs x xs
-
--- | Ensures that @x@ only ever appears once in @xs@
-type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs
-
--- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.
-type UniqueLabel (l :: k1) (xs :: [k]) = UniqueLabelImpl xs l xs
-
--- | Ensures that the @label@ list all 'UniqueLabel's
-type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where
-    UniqueLabels '[] xs = ()
-    UniqueLabels (l ': ls) xs = (UniqueLabel l xs, UniqueLabels ls xs)
-
--- | Get the first index of a type (Indexed by 0)
--- Will result in type error if x doesn't exist in xs.
-type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs
-
--- | Get the first index of a type (Indexed by 1)
--- Will return 0 if x doesn't exists in xs.
-type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs
-
--- | Get the type at an index
-type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs
-
--- | Get the type at a label
-type KindAtLabel (l :: k1) (xs :: [k]) = KindAtLabelImpl l xs xs
-
--- | It's actually ok for the position to be zero, but if it's not zero then the types must match
-type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where
-    KindAtPositionIs 0 x xs = ()
-    KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs)
-
--- | Get the types at an list of index
-type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where
-    KindsAtIndices '[] xs = '[]
-    KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs
-
-type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where
-    KindsAtLabels '[] xs = '[]
-    KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs
-
--- | The typelist @xs@ without first @x@. It is okay for @x@ not to exist in @xs@
-type family Without (x :: k) (xs :: [k]) :: [k] where
-    Without x '[] = '[]
-    Without x (x ': xs) = xs
-    Without x (y ': xs) = y ': Without x xs
-
--- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@
-type Replace (x :: k) (y :: k) (xs :: [k]) = ReplaceImpl x y xs
-
--- | The typelist @zs@ with the first @xs@ replaced by @ys@.
--- @xs@ must be the same size as @ys@
-type Replaces (xs :: [k]) (ys :: [k]) (zs :: [k]) = ReplacesImpl xs ys xs ys zs
-
--- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@
-type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs
-
--- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@
-type ReplaceIndex (n :: Nat) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n y xs
-
--- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@
-type ReplacesIndex (ns :: [Nat]) (ys :: [k]) (xs :: [k]) = ReplacesIndexImpl 0 ns ys xs
-
--- | Get the typelist without the 'Head' type
-type family Tail (xs :: [k]) :: [k] where
-    Tail '[] = TypeError ('Text "Tail error: empty type list")
-    Tail (x ': xs) = xs
-
--- | Get the first type in a typelist
-type family Head (xs :: [k]) :: k where
-    Head '[] = TypeError ('Text "Head error: empty type list")
-    Head (x ': xs) = x
-
--- | Get the last type in a typelist
-type family Last (xs :: [k]) :: k where
-    Last '[] = TypeError ('Text "Last error: empty type list")
-    Last (x ': x' ': xs) = Last (x' ': xs)
-    Last '[x] = x
-
--- | Ensures two typelists are the same length
-type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys
-
--- | Set complement. Returns the set of things in @xs@ that are not in @ys@.
-type family Complement (xs :: [k]) (ys :: [k]) :: [k] where
-    Complement xs '[] = xs
-    Complement xs (y ': ys)  = Complement (Without y xs) ys
-
--- | Returns a @xs@ appended with @ys@
-type family Append (xs :: [k]) (ys :: [k]) :: [k] where
-    Append '[] ys = ys
-    Append (x ': xs) ys = x ': Append xs ys
-
--- | Returns the typelist without the 'Last' type
-type family Init (xs :: [k]) :: [k] where
-    Init '[]  = TypeError ('Text "Init error: empty type list")
-    Init '[x] = '[]
-    Init (x ': xs) = x ': Init xs
-
--- | 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
diff --git a/src/Data/Diverse/Type/Internal.hs b/src/Data/Diverse/Type/Internal.hs
deleted file mode 100644
--- a/src/Data/Diverse/Type/Internal.hs
+++ /dev/null
@@ -1,194 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Data.Diverse.Type.Internal where
-
-import Data.Kind
-import GHC.TypeLits
-
--- | Get the first position of a type (indexed by 1)
--- Will return 0 if @x@ doesn't exists in @xs@.
-type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where
-   PositionOfImpl i x (x ': xs) = i + 1
-   PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs
-   PositionOfImpl i x '[] = 0
-
--- | Get the first index of a type from a list
-type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where
-   IndexOfImpl ctx x (x ': xs) = 0
-   IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs
-   IndexOfImpl ctx y '[] = TypeError ('Text "IndexOf error: ‘"
-                                      ':<>: 'ShowType y
-                                      ':<>: 'Text "’"
-                                      ':<>: 'Text " is not a member of "
-                                      ':<>: 'Text "‘"
-                                      ':<>: 'ShowType ctx
-                                      ':<>: 'Text "’")
-
--- | Searches for y in ys
--- if not found, than use y, and repeat search with next (y ': ys) in ctx
--- else if found, then don't use y, then repeat search with next (y ': ys) in ctx
-type family NubImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where
-    NubImpl '[] y '[] = y ': '[]
-    NubImpl '[] y (y ': xs) = '[]
-    NubImpl (x ': xs) y '[] = y ': NubImpl xs x xs
-    NubImpl (x ': xs) y (y ': ys) = NubImpl xs x xs
-    NubImpl ctx y (x ': xs) = NubImpl ctx y xs
-
--- | Errors if a type exists in a typelist
-type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where
-    MissingImpl ctx y '[] = ()
-    MissingImpl ctx x (x ': xs) = TypeError ('Text "Not unique error: ‘"
-                                             ':<>: 'ShowType x
-                                             ':<>: 'Text "’"
-                                             ':<>: 'Text " is a duplicate in "
-                                             ':<>: 'Text "‘"
-                                             ':<>: 'ShowType ctx
-                                             ':<>: 'Text "’")
-    MissingImpl ctx y (x ': xs) = (MissingImpl ctx y xs)
-
--- | Errors if a label exists in a typelist
-type family MissingLabelImpl (ctx :: [k]) (l :: k2) (xs :: [k]) :: Constraint where
-    MissingLabelImpl ctx y '[] = ()
-    MissingLabelImpl ctx l (tagged l x ': xs) = TypeError ('Text "Not unique label error: ‘"
-                                             ':<>: 'ShowType l
-                                             ':<>: 'Text "’"
-                                             ':<>: 'Text " is a duplicate in "
-                                             ':<>: 'Text "‘"
-                                             ':<>: 'ShowType ctx
-                                             ':<>: 'Text "’")
-    MissingLabelImpl ctx l (x ': xs) = (MissingLabelImpl ctx l xs)
-
--- | Ensures that the type list contain unique types.
--- Not implemented as @(xs ~ Nub xs)@ for better type error messages.
-type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where
-    IsDistinctImpl ctx '[] = ()
-    IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs)
-
--- | Ensures that @x@ only ever appears once in @xs@
-type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where
-    UniqueImpl ctx x '[] = ()
-    UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs
-    UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs
-
--- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.
-type family UniqueLabelImpl (ctx :: [k]) (l :: k1) (xs :: [k]) :: Constraint where
-    UniqueLabelImpl ctx l '[] = ()
-    UniqueLabelImpl ctx l (tagged l x ': xs) = MissingLabelImpl ctx l xs
-    UniqueLabelImpl ctx l (y ': xs) = UniqueLabelImpl ctx l xs
-
--- | Indexed access into the list
-type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where
-    KindAtIndexImpl i ctx 0 '[] = TypeError ('Text "KindAtIndex error: Index ‘"
-                                       ':<>: 'ShowType i
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " is out of bounds of "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ctx
-                                       ':<>: 'Text "’")
-    KindAtIndexImpl i ctx 0 (x ': xs) = x
-    KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs
-
--- | Labelled access into the list
-type family KindAtLabelImpl (l :: k1) (ctx :: [k]) (xs :: [k]) :: k where
-    KindAtLabelImpl l ctx '[] = TypeError ('Text "KindAtLabel error: Label ‘"
-                                       ':<>: 'ShowType l
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " is not found in "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ctx
-                                       ':<>: 'Text "’")
-    KindAtLabelImpl l ctx (tagged l x ': xs) = tagged l x
-    KindAtLabelImpl l ctx (x ': xs) = KindAtLabelImpl l ctx xs
-
--- | Ensures two typelists are the same length
-type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where
-    SameLengthImpl as bs '[] '[] = ()
-    SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys
-    SameLengthImpl as bs xs ys = TypeError ('Text "SameLength error: ‘"
-                                            ':<>: 'ShowType as
-                                            ':<>: 'Text "’"
-                                            ':<>: 'Text " is not the same length as "
-                                            ':<>: 'Text "‘"
-                                            ':<>: 'ShowType bs
-                                            ':<>: 'Text "’")
-
--- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@
-type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where
-    WithoutIndexImpl i ctx n '[] = TypeError ('Text "WithoutIndex error: Index ‘"
-                                       ':<>: 'ShowType i
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " is out of bounds of "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ctx
-                                       ':<>: 'Text "’")
-    WithoutIndexImpl i ctx 0 (x ': xs) = xs
-    WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs
-
--- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@
-type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where
-    ReplaceIndexImpl i ctx n y '[] = TypeError ('Text "ReplaceIndex error: Index ‘"
-                                       ':<>: 'ShowType i
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " is out of bounds of "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ctx
-                                       ':<>: 'Text "’")
-    ReplaceIndexImpl i ctx 0 y (x ': xs) = y ': xs
-    ReplaceIndexImpl i ctx n y (x ': xs) = x ': ReplaceIndexImpl i ctx (n - 1) y xs
-
--- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@
-type family ReplaceImpl (x :: k) (y :: k) (xs :: [k]) :: [k] where
-    ReplaceImpl x y '[] = '[]
-    ReplaceImpl x y (x ': xs) = y ': xs
-    ReplaceImpl x y (z ': xs) = z ': ReplaceImpl x y xs
-
--- | The typelist @zs@ with the first @xs@ replaced by @ys@.
--- @xs@ must be the same size as @ys@
-type family ReplacesImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where
-    ReplacesImpl xs' ys' xs ys '[] = '[]
-    ReplacesImpl xs' ys' '[] '[] (z ': zs) = z ': ReplacesImpl xs' ys' xs' ys' zs
-    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (x ': zs) = y ': ReplacesImpl xs' ys' xs' ys' zs
-    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (z ': zs) = ReplacesImpl xs' ys' xs ys (z ': zs)
-    ReplacesImpl xs' ys' xs ys zs = TypeError ('Text "Replaces error: ‘"
-                                       ':<>: 'ShowType xs'
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " must be the same size as "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ys'
-                                       ':<>: 'Text "’")
-
--- | The type @x@ replaced by an @y@ if an @n@ matches @i@.
-type family ReplaceIfIndex (ns :: [Nat]) (ys :: [k]) (i :: Nat) (x :: k) :: k where
-    ReplaceIfIndex '[] ys i x = x
-    ReplaceIfIndex ns '[] i x = x
-    ReplaceIfIndex (n ': ns) (y ': ys) n x = y
-    ReplaceIfIndex (n ': ns) (y ': ys) i x = ReplaceIfIndex ns ys i x
-
--- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@
-type family ReplacesIndexImpl (i :: Nat) (ns :: [Nat]) (ys :: [k]) (xs :: [k]) :: [k] where
-    ReplacesIndexImpl i ns ys '[] = '[]
-    ReplacesIndexImpl i '[] '[] xs = xs
-    ReplacesIndexImpl i ns ys (x ': xs) = ReplaceIfIndex ns ys i x ': ReplacesIndexImpl (i + 1) ns ys xs
-    ReplacesIndexImpl i ns ys xs = TypeError ('Text "ReplacesIndex error: ‘"
-                                       ':<>: 'ShowType ns
-                                       ':<>: 'Text "’"
-                                       ':<>: 'Text " must be the same size as "
-                                       ':<>: 'Text "‘"
-                                       ':<>: 'ShowType ys
-                                       ':<>: 'Text "’")
-
--- | Zips up @xs@ and @ys@, which must be the same length
-type family ZipImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) :: [k] where
-    ZipImpl xs' ys' '[] '[] = '[]
-    ZipImpl xs' ys' (x ': xs) (y ': ys) = (x, y) ': ZipImpl xs' ys' xs ys
-    ZipImpl xs' ys' xs ys = TypeError ('Text "Zip error: ‘"
-                              ':<>: 'ShowType xs'
-                              ':<>: 'Text "’"
-                              ':<>: 'Text " must be the same size as "
-                              ':<>: 'Text "‘"
-                              ':<>: 'ShowType ys'
-                              ':<>: 'Text "’")
diff --git a/src/Data/Diverse/TypeLevel.hs b/src/Data/Diverse/TypeLevel.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Diverse/TypeLevel.hs
@@ -0,0 +1,145 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeInType #-}
+
+module Data.Diverse.TypeLevel where
+
+import Data.Diverse.TypeLevel.Internal
+import Data.Kind
+import GHC.TypeLits
+
+-- | 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))
+
+-- | 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)
+
+-- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.
+type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs))
+
+-- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natVal' can be used.
+type MaybeUniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ PositionOf x xs)
+
+-- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natVal' can be used.
+type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs)
+
+-- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used.
+type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)
+
+-- | Ensures x is a unique member in @xs@ iff it exists in @ys@
+type family UniqueIfExists ys x xs :: Constraint where
+    UniqueIfExists '[] x xs = ()
+    UniqueIfExists (y ': ys) y xs = Unique y xs
+    UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs
+
+-- | Ensures that the type list contain unique types
+type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs
+
+-- | Return the list of distinct types in a typelist
+type family Nub (xs :: [k]) :: [k] where
+    Nub '[] = '[]
+    Nub (x ': xs) = NubImpl xs x xs
+
+-- | Ensures that @x@ only ever appears once in @xs@
+type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs
+
+-- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.
+type UniqueLabel (l :: k1) (xs :: [k]) = UniqueLabelImpl xs l xs
+
+-- | Ensures that the @label@ list all 'UniqueLabel's
+type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where
+    UniqueLabels '[] xs = ()
+    UniqueLabels (l ': ls) xs = (UniqueLabel l xs, UniqueLabels ls xs)
+
+-- | Get the first index of a type (Indexed by 0)
+-- Will result in type error if x doesn't exist in xs.
+type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs
+
+-- | Get the first index of a type (Indexed by 1)
+-- Will return 0 if x doesn't exists in xs.
+type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs
+
+-- | Get the type at an index
+type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs
+
+-- | Get the type at a label
+type KindAtLabel (l :: k1) (xs :: [k]) = KindAtLabelImpl l xs xs
+
+-- | It's actually ok for the position to be zero, but if it's not zero then the types must match
+type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where
+    KindAtPositionIs 0 x xs = ()
+    KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs)
+
+-- | Get the types at an list of index
+type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where
+    KindsAtIndices '[] xs = '[]
+    KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs
+
+type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where
+    KindsAtLabels '[] xs = '[]
+    KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs
+
+-- | The typelist @xs@ without first @x@. It is okay for @x@ not to exist in @xs@
+type family Without (x :: k) (xs :: [k]) :: [k] where
+    Without x '[] = '[]
+    Without x (x ': xs) = xs
+    Without x (y ': xs) = y ': Without x xs
+
+-- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@
+type Replace (x :: k) (y :: k) (xs :: [k]) = ReplaceImpl x y xs
+
+-- | The typelist @zs@ with the first @xs@ replaced by @ys@.
+-- @xs@ must be the same size as @ys@
+type Replaces (xs :: [k]) (ys :: [k]) (zs :: [k]) = ReplacesImpl xs ys xs ys zs
+
+-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@
+type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs
+
+-- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@
+type ReplaceIndex (n :: Nat) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n y xs
+
+-- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@
+type ReplacesIndex (ns :: [Nat]) (ys :: [k]) (xs :: [k]) = ReplacesIndexImpl 0 ns ys xs
+
+-- | Get the typelist without the 'Head' type
+type family Tail (xs :: [k]) :: [k] where
+    Tail '[] = TypeError ('Text "Tail error: empty type list")
+    Tail (x ': xs) = xs
+
+-- | Get the first type in a typelist
+type family Head (xs :: [k]) :: k where
+    Head '[] = TypeError ('Text "Head error: empty type list")
+    Head (x ': xs) = x
+
+-- | Get the last type in a typelist
+type family Last (xs :: [k]) :: k where
+    Last '[] = TypeError ('Text "Last error: empty type list")
+    Last (x ': x' ': xs) = Last (x' ': xs)
+    Last '[x] = x
+
+-- | Ensures two typelists are the same length
+type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys
+
+-- | Set complement. Returns the set of things in @xs@ that are not in @ys@.
+type family Complement (xs :: [k]) (ys :: [k]) :: [k] where
+    Complement xs '[] = xs
+    Complement xs (y ': ys)  = Complement (Without y xs) ys
+
+-- | Returns a @xs@ appended with @ys@
+type family Append (xs :: [k]) (ys :: [k]) :: [k] where
+    Append '[] ys = ys
+    Append (x ': xs) ys = x ': Append xs ys
+
+-- | Returns the typelist without the 'Last' type
+type family Init (xs :: [k]) :: [k] where
+    Init '[]  = TypeError ('Text "Init error: empty type list")
+    Init '[x] = '[]
+    Init (x ': xs) = x ': Init xs
+
+-- | 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
diff --git a/src/Data/Diverse/TypeLevel/Internal.hs b/src/Data/Diverse/TypeLevel/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Diverse/TypeLevel/Internal.hs
@@ -0,0 +1,194 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Diverse.TypeLevel.Internal where
+
+import Data.Kind
+import GHC.TypeLits
+
+-- | Get the first position of a type (indexed by 1)
+-- Will return 0 if @x@ doesn't exists in @xs@.
+type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where
+   PositionOfImpl i x (x ': xs) = i + 1
+   PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs
+   PositionOfImpl i x '[] = 0
+
+-- | Get the first index of a type from a list
+type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where
+   IndexOfImpl ctx x (x ': xs) = 0
+   IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs
+   IndexOfImpl ctx y '[] = TypeError ('Text "IndexOf error: ‘"
+                                      ':<>: 'ShowType y
+                                      ':<>: 'Text "’"
+                                      ':<>: 'Text " is not a member of "
+                                      ':<>: 'Text "‘"
+                                      ':<>: 'ShowType ctx
+                                      ':<>: 'Text "’")
+
+-- | Searches for y in ys
+-- if not found, than use y, and repeat search with next (y ': ys) in ctx
+-- else if found, then don't use y, then repeat search with next (y ': ys) in ctx
+type family NubImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where
+    NubImpl '[] y '[] = y ': '[]
+    NubImpl '[] y (y ': xs) = '[]
+    NubImpl (x ': xs) y '[] = y ': NubImpl xs x xs
+    NubImpl (x ': xs) y (y ': ys) = NubImpl xs x xs
+    NubImpl ctx y (x ': xs) = NubImpl ctx y xs
+
+-- | Errors if a type exists in a typelist
+type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where
+    MissingImpl ctx y '[] = ()
+    MissingImpl ctx x (x ': xs) = TypeError ('Text "Not unique error: ‘"
+                                             ':<>: 'ShowType x
+                                             ':<>: 'Text "’"
+                                             ':<>: 'Text " is a duplicate in "
+                                             ':<>: 'Text "‘"
+                                             ':<>: 'ShowType ctx
+                                             ':<>: 'Text "’")
+    MissingImpl ctx y (x ': xs) = (MissingImpl ctx y xs)
+
+-- | Errors if a label exists in a typelist
+type family MissingLabelImpl (ctx :: [k]) (l :: k2) (xs :: [k]) :: Constraint where
+    MissingLabelImpl ctx y '[] = ()
+    MissingLabelImpl ctx l (tagged l x ': xs) = TypeError ('Text "Not unique label error: ‘"
+                                             ':<>: 'ShowType l
+                                             ':<>: 'Text "’"
+                                             ':<>: 'Text " is a duplicate in "
+                                             ':<>: 'Text "‘"
+                                             ':<>: 'ShowType ctx
+                                             ':<>: 'Text "’")
+    MissingLabelImpl ctx l (x ': xs) = (MissingLabelImpl ctx l xs)
+
+-- | Ensures that the type list contain unique types.
+-- Not implemented as @(xs ~ Nub xs)@ for better type error messages.
+type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where
+    IsDistinctImpl ctx '[] = ()
+    IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs)
+
+-- | Ensures that @x@ only ever appears once in @xs@
+type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where
+    UniqueImpl ctx x '[] = ()
+    UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs
+    UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs
+
+-- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.
+type family UniqueLabelImpl (ctx :: [k]) (l :: k1) (xs :: [k]) :: Constraint where
+    UniqueLabelImpl ctx l '[] = ()
+    UniqueLabelImpl ctx l (tagged l x ': xs) = MissingLabelImpl ctx l xs
+    UniqueLabelImpl ctx l (y ': xs) = UniqueLabelImpl ctx l xs
+
+-- | Indexed access into the list
+type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where
+    KindAtIndexImpl i ctx 0 '[] = TypeError ('Text "KindAtIndex error: Index ‘"
+                                       ':<>: 'ShowType i
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " is out of bounds of "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ctx
+                                       ':<>: 'Text "’")
+    KindAtIndexImpl i ctx 0 (x ': xs) = x
+    KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs
+
+-- | Labelled access into the list
+type family KindAtLabelImpl (l :: k1) (ctx :: [k]) (xs :: [k]) :: k where
+    KindAtLabelImpl l ctx '[] = TypeError ('Text "KindAtLabel error: Label ‘"
+                                       ':<>: 'ShowType l
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " is not found in "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ctx
+                                       ':<>: 'Text "’")
+    KindAtLabelImpl l ctx (tagged l x ': xs) = tagged l x
+    KindAtLabelImpl l ctx (x ': xs) = KindAtLabelImpl l ctx xs
+
+-- | Ensures two typelists are the same length
+type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where
+    SameLengthImpl as bs '[] '[] = ()
+    SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys
+    SameLengthImpl as bs xs ys = TypeError ('Text "SameLength error: ‘"
+                                            ':<>: 'ShowType as
+                                            ':<>: 'Text "’"
+                                            ':<>: 'Text " is not the same length as "
+                                            ':<>: 'Text "‘"
+                                            ':<>: 'ShowType bs
+                                            ':<>: 'Text "’")
+
+-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@
+type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where
+    WithoutIndexImpl i ctx n '[] = TypeError ('Text "WithoutIndex error: Index ‘"
+                                       ':<>: 'ShowType i
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " is out of bounds of "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ctx
+                                       ':<>: 'Text "’")
+    WithoutIndexImpl i ctx 0 (x ': xs) = xs
+    WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs
+
+-- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@
+type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where
+    ReplaceIndexImpl i ctx n y '[] = TypeError ('Text "ReplaceIndex error: Index ‘"
+                                       ':<>: 'ShowType i
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " is out of bounds of "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ctx
+                                       ':<>: 'Text "’")
+    ReplaceIndexImpl i ctx 0 y (x ': xs) = y ': xs
+    ReplaceIndexImpl i ctx n y (x ': xs) = x ': ReplaceIndexImpl i ctx (n - 1) y xs
+
+-- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@
+type family ReplaceImpl (x :: k) (y :: k) (xs :: [k]) :: [k] where
+    ReplaceImpl x y '[] = '[]
+    ReplaceImpl x y (x ': xs) = y ': xs
+    ReplaceImpl x y (z ': xs) = z ': ReplaceImpl x y xs
+
+-- | The typelist @zs@ with the first @xs@ replaced by @ys@.
+-- @xs@ must be the same size as @ys@
+type family ReplacesImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where
+    ReplacesImpl xs' ys' xs ys '[] = '[]
+    ReplacesImpl xs' ys' '[] '[] (z ': zs) = z ': ReplacesImpl xs' ys' xs' ys' zs
+    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (x ': zs) = y ': ReplacesImpl xs' ys' xs' ys' zs
+    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (z ': zs) = ReplacesImpl xs' ys' xs ys (z ': zs)
+    ReplacesImpl xs' ys' xs ys zs = TypeError ('Text "Replaces error: ‘"
+                                       ':<>: 'ShowType xs'
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " must be the same size as "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ys'
+                                       ':<>: 'Text "’")
+
+-- | The type @x@ replaced by an @y@ if an @n@ matches @i@.
+type family ReplaceIfIndex (ns :: [Nat]) (ys :: [k]) (i :: Nat) (x :: k) :: k where
+    ReplaceIfIndex '[] ys i x = x
+    ReplaceIfIndex ns '[] i x = x
+    ReplaceIfIndex (n ': ns) (y ': ys) n x = y
+    ReplaceIfIndex (n ': ns) (y ': ys) i x = ReplaceIfIndex ns ys i x
+
+-- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@
+type family ReplacesIndexImpl (i :: Nat) (ns :: [Nat]) (ys :: [k]) (xs :: [k]) :: [k] where
+    ReplacesIndexImpl i ns ys '[] = '[]
+    ReplacesIndexImpl i '[] '[] xs = xs
+    ReplacesIndexImpl i ns ys (x ': xs) = ReplaceIfIndex ns ys i x ': ReplacesIndexImpl (i + 1) ns ys xs
+    ReplacesIndexImpl i ns ys xs = TypeError ('Text "ReplacesIndex error: ‘"
+                                       ':<>: 'ShowType ns
+                                       ':<>: 'Text "’"
+                                       ':<>: 'Text " must be the same size as "
+                                       ':<>: 'Text "‘"
+                                       ':<>: 'ShowType ys
+                                       ':<>: 'Text "’")
+
+-- | Zips up @xs@ and @ys@, which must be the same length
+type family ZipImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) :: [k] where
+    ZipImpl xs' ys' '[] '[] = '[]
+    ZipImpl xs' ys' (x ': xs) (y ': ys) = (x, y) ': ZipImpl xs' ys' xs ys
+    ZipImpl xs' ys' xs ys = TypeError ('Text "Zip error: ‘"
+                              ':<>: 'ShowType xs'
+                              ':<>: 'Text "’"
+                              ':<>: 'Text " must be the same size as "
+                              ':<>: 'Text "‘"
+                              ':<>: 'ShowType ys'
+                              ':<>: '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
@@ -70,7 +70,7 @@
 import Data.Diverse.Case
 import Data.Diverse.Reduce
 import Data.Diverse.Reiterate
-import Data.Diverse.Type
+import Data.Diverse.TypeLevel
 import Data.Kind
 import Data.Proxy
 import qualified GHC.Generics as G
@@ -322,7 +322,7 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversify'.
-type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce Which (Switch (CaseDiversify tree branch)) branch (Which tree)
+type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce (Which branch) (Switch (CaseDiversify tree branch) 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@.
@@ -378,7 +378,9 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'diversifyN'.
-type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) = (Reduce Which (SwitchN (CaseDiversifyN indices) 0) (KindsAtIndices indices tree) (Which tree), KindsAtIndices indices tree ~ branch)
+type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) =
+    ( Reduce (Which branch) (SwitchN (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
 --
@@ -410,7 +412,7 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpret'.
-type Reinterpret branch tree = Reduce Which (Switch (CaseReinterpret branch tree)) tree (Either (Which (Complement tree branch)) (Which branch))
+type Reinterpret branch tree = Reduce (Which tree) (Switch (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.
@@ -472,7 +474,9 @@
 ------------------------------------------------------------------
 
 -- | A friendlier constraint synonym for 'reinterpretN'.
-type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) = (Reduce Which (SwitchN (CaseReinterpretN indices) 0) tree (Maybe (Which (KindsAtIndices indices tree))), KindsAtIndices indices tree ~ branch)
+type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
+    ( Reduce (Which tree) (SwitchN (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
 --
@@ -571,24 +575,26 @@
 
 -- | '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 (Switch c) (x' ': xs) r, Reiterate c (x : x' : xs)) =>
-         Reduce Which (Switch c) (x ': x' ': xs) r where
+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 =
         case trial0 v of
             Right a -> case' c a
             Left v' -> reduce (Switch (reiterate c)) v'
     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types
-    {-# NOINLINE reduce #-}
+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement
+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877
+    {-# INLINEABLE reduce #-}
 
 -- | 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 (Switch c) '[x] r where
+instance (Case c '[x] r) => Reduce (Which '[x]) (Switch c '[x]) r where
     reduce (Switch c) v = case obvious v of
             a -> case' c a
 
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@.
-which :: Reduce Which (Switch case') xs r => case' xs r -> Which xs -> r
+which :: Reduce (Which xs) (Switch case' xs) r => case' xs r -> Which xs -> r
 which = reduce . Switch
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@
@@ -611,7 +617,7 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switch :: Reduce Which (Switch case') xs r => Which xs -> case' xs r -> r
+switch :: Reduce (Which xs) (Switch case' xs) r => Which xs -> case' xs r -> r
 switch = flip which
 
 ------------------------------------------------------------------
@@ -622,24 +628,26 @@
 
 -- | '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 (SwitchN c (n + 1)) (x' ': xs) r, ReiterateN c n (x : x' : xs)) =>
-         Reduce Which (SwitchN c n) (x ': x' ': xs) r where
+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 =
         case trial0 v of
             Right a -> case' c a
             Left v' -> reduce (SwitchN (reiterateN c)) v'
     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types
-    {-# NOINLINE reduce #-}
+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement
+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877
+    {-# INLINEABLE reduce #-}
 
 -- | 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 (SwitchN c n) '[x] r where
+instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitchN c n '[x]) r where
     reduce (SwitchN c) v = case obvious v of
             a -> case' c a
 
 -- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@.
-whichN :: Reduce Which (SwitchN case' n) xs r => case' n xs r -> Which xs -> r
+whichN :: Reduce (Which xs) (SwitchN case' n xs) r => case' n xs r -> Which xs -> r
 whichN = reduce . SwitchN
 
 -- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@
@@ -658,13 +666,13 @@
 -- @
 --
 -- Or you may use your own custom instance of 'Case'.
-switchN :: Reduce Which (SwitchN case' n) xs r => Which xs -> case' n xs r -> r
+switchN :: Reduce (Which xs) (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 (Switch CaseEqWhich) (x ': xs) Bool) => Eq (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool) => Eq (Which (x ': xs)) where
     l@(Which i _) == (Which j u) =
         if i /= j
             then False
@@ -687,7 +695,10 @@
 -----------------------------------------------------------------
 
 -- | A 'Which' with a type at smaller type index is considered smaller.
-instance (Reduce Which (Switch CaseEqWhich) (x ': xs) Bool, Reduce Which (Switch CaseOrdWhich) (x ': xs) Ordering) => Ord (Which (x ': xs)) where
+instance ( Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool
+         , Reduce (Which (x ': xs)) (Switch CaseOrdWhich (x ': xs)) Ordering
+         ) =>
+         Ord (Which (x ': xs)) where
     compare l@(Which i _) (Which j u) =
         if i /= j
             then compare i j
@@ -710,7 +721,7 @@
 ------------------------------------------------------------------
 
 -- | @show ('pick'' \'A') == "pick \'A'"@
-instance (Reduce Which (Switch CaseShowWhich) (x ': xs) ShowS) => Show (Which (x ': xs)) where
+instance (Reduce (Which (x ': xs)) (Switch CaseShowWhich (x ': xs)) ShowS) => Show (Which (x ': xs)) where
     showsPrec d v = showParen (d > app_prec) (which (CaseShowWhich 0) v)
       where app_prec = 10
 
@@ -750,7 +761,9 @@
     whichReadPrec i j = readWhich_ i j
                <|> (diversify0' <$> (whichReadPrec i (j + 1) :: ReadPrec (Which_ (x' ': xs))))
     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types
-    {-# NOINLINE whichReadPrec #-}
+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement
+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877
+    {-# INLINEABLE whichReadPrec #-}
 
 
 -- | This 'Read' instance tries to read using the each type in the typelist, using the first successful type read.
diff --git a/test/Data/Diverse/TypeSpec.hs b/test/Data/Diverse/TypeSpec.hs
--- a/test/Data/Diverse/TypeSpec.hs
+++ b/test/Data/Diverse/TypeSpec.hs
@@ -29,7 +29,7 @@
             fromIntegral (natVal @(PositionOf Int '[Bool, String, Char]) Proxy) `shouldBe` (0 :: Int)
 
         it "ComplementOf" $ do
-            let complementTest :: (Complement xs ys ~ comp) => Proxy xs -> Proxy ys -> Proxy comp -> Proxy comp
+            let complementTest :: Proxy xs -> Proxy ys -> Proxy (Complement xs ys) -> Proxy (Complement xs ys)
                 complementTest _ _ comp = comp
 
             complementTest (Proxy @[String, Int]) (Proxy @[Bool, Int]) (Proxy @'[String]) `shouldBe` Proxy