diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,159 @@
+
+# Changelog
+
+* 4.7.0.0
+  - Removed `totally`. Added `CaseFunc1_`
+
+* 4.6.0.0
+  - Renamed `definitely` to `totally`.
+
+* 4.5.0.0
+  - Replaced usages of `KnownNat` with a new `NatToInt` class to avoid inefficient Integer https://github.com/louispan/data-diverse/issues/8.
+
+* 4.4.0.0
+  - Renamed `Unconstrained` to `C0`. Added `C2`, `C3`, `C4`, `C5`, `C6`.
+
+* 4.3.0.0
+  - Renamed `NoConstraint` to `Unconstrained`
+
+* 4.2.0.0
+  - Added `CaseFunc1` to allow `afmap` of with `Functor`, etc.
+  - `Which` is now also an instance of `AFoldable`.
+  - Added `NoConstraint` which is useful for `CaseFunc1` for unused constraints.
+  - Added `definitely`.
+
+* 4.1.0.0
+  - Removed `zilch`.
+
+* 4.0.0.0
+  - Renamed `prefix` to `consMany` and `postfix` to `snocMany`.
+
+* 3.1.0.0
+  - Removed `Read` instance for `Which []` since it is uninhabitable.
+  - `xxxTag` functions only rely on `UniqueMember`, not `UniqueLabelMember`
+
+* 3.0.0.0
+  - Renamed `fetch` to `grab` to avoid conflicting with Haxl.
+  - Removed unused type functions from removed splitting functions (Before,To,After,From,Length)
+  - Added `impossible'` and ability to diversify and reinterpret `Which '[Void]`
+  - Added `zilch`
+  - Removed `CanAppendUnique` (not useful).
+
+* 2.0.1.0
+  - Simplified type synonyms for `Which`. Added `Reinterpreted` constraint synonym.
+
+* 2.0.0.0
+  - Breaking change: the prime (xxx') version of functions are now consistently the simpler or non-polymorphic version.
+    - This is more consistent with `Control.Lens` as well.
+    - This means the following are swapped:
+      - `replace`, `replace'`
+      - `replaceL`, `replaceL'`
+      - `replaceTag`, `replaceTag'`
+      - `replaceN`, `replaceN'`
+      - `amend`, `amend'`
+      - `amendL`, `amendL'`
+      - `amendN`, `amendN'`
+  - Breaking change: Removed proxy argument from `fetchL/Tag/N`, `replaceXXX`, `selectL/Tag/N`, `amendXXX`, `pickL/Tag/N`, `trialL/Tag/N`
+    relying soley on `TypeApplications` and now requiring `AllowAmbiguousTypes`.
+    The `Proxy` is also removed from the Read/Show serialized format.
+  - Rearranged type variables in `fetchL/N`, `replaceL/Tag/N`, `pickL/Tag/N`, `trialL/Tag/N` type parameters,
+    so the type variable ordering is consistently label, orig to change, smaller to larger, ie. `l/n`, `x`, `y`, `xs`
+
+* 1.3.0.0
+  - Removed splitting operations added in 1.2.0.0
+  - added `xxxTag` version of label operations that also automatically untags the field.
+
+* 1.2.0.3
+  - `PolyKinds` for `Which`
+  - Removed cabal upper bounds
+
+* 1.2.0.2
+  - Added `insert`/`remove` for GHC < 8.2
+  - Removed type functions `UniqueMemberAt`, `MaybeUniqueMemberAt`
+
+* 1.2.0.1
+  - `insert`/`remove` is not available in GHC 8.2 onwards.
+
+* 1.2.0.0
+  - Rerranged type variable for xxxL and xxxN functions so that the
+    `x` inferrred from label `l` or index `n` is after `proxy`.
+    - This affects `fetch[L|N]`, `replace[L|N]`, `replace[L|N]'`, `pick[L|N]`
+  - Depends on at least containers-0.5.8.2 for `Data.Sequence.insertAt`
+  - Added splitting operations: `split[Before|After][|L|N]`, `inset[Before|After][|L|N]`,
+    `insert[Before|After][|L|N]`, `remove[Before|After][|L|N]`
+  - Renamed type function `Without` to `Remove` to be consistent with new `remove` method.
+
+* 1.1.0.0
+  - Added `CaseFunc` and `CaseFunc'` which replaces `CaseTypeable` (eg `CaseFunc @Typeable`)
+    <https://github.com/louispan/data-diverse/issues/6>
+  - Replaced `IsAll` constraint with `AllConstrained`.
+
+* 1.0.0.1
+  - Added `CaseTypeable'` as an example of polymorphic `Case` that doesn't change the type.
+
+* 1.0.0.0
+  - The exposed api shouldn't break, but there are a lot of internal changes.
+  - Added `AFunctor` which can map over the types in the 'Many'
+    <https://github.com/louispan/data-diverse/issues/5>.
+  - Added friendlier type synomyns `Collect` and `CollectN` for `collect` and `collectN`
+  - Expose type of 'Collector' and 'CollectorN'
+  - Replace type parameter `r` from `Case` typeclass with `CaseResult` type family.
+  - Replaced `CasesResult` type function with `IsAll` and `CasesResults` type functions.
+  - All `CaseXxx` type variables now end with r xs.
+  - All `CaseXxxN` type variables now end with r n xs.
+
+* 0.11.0.0
+  - Added `impossible` modelled after `Data.Void.absurd`
+    <https://github.com/louispan/data-diverse/issues/4>
+  - Removed `zilch` so `Which '[]` is uninhabited like `Data.Void.Void`, making 'impossible' safe to use.
+  - Removed `Monoid` and changed `Show`, `Read` and `Generic` instances for `Which '[]` to be partial
+    just like Data.Void.Void.
+  - Added `instance Reduce (Which '[]) (Switcher c '[] r)`, which follows from `impossible`.
+
+* 0.10.0.0
+  - Renamed `Switch` to `Switcher`. Switch is now a type synonym for `switch` constraints
+  - Added CasesResult type family to help infer the result of `cases`
+  - Added Semigroup and Monoid instances for all Many xs.
+  - Added Maybe versions of trial, and reinterpret
+  - Renamed `reinterpetN` to `reinterpretN'`
+  - Renamed `impossible` to `zilch`.
+  - Allowed `reintepret`ing and `diversify`ing `zilch` to `zilch`
+  - Removed zipped type variable from `Amend` constraints.
+  - Removed r type variable from `Reduce` typeclass.
+  - Rearranged type variables in `fetch`, `replace`, `pick`, `trial`, `Diversify` type parameters,
+    so the type variable ordering is consistently smaller to larger, ie. `x`, `xs`, `branch`, `tree`
+  - Added `diversify'` for allowing rearranging the types only.
+
+* 0.9.0.1
+  - Fixed GHC 8.2.1 test failure due to changed TypeRep show instance.
+
+* 0.9.0.0
+  - Breaking changes: Renamed Many.sliceL/R to Many.viewf/b
+  - Renamed TypeLevel.Internal.MissingImpl to IsUniqueImpl.
+  - Added postifx' with SnocUnique and append' with AppendUnique.
+  - Added Semigroup & Monoid instances for `Many '[]` and `Which '[]`
+  - Fixed GHC 8.2 compile error with importing GHC.Prim (Any)
+
+* 0.8.1.0
+  - Added NFData instance for Which.
+  - Forgot to expose Many.sliceL and Many.sliceR.
+
+* 0.8.0.0
+  - Changed internal representation to (Data.Seq Any) for a further 2x append speedup.
+  - Added NFData instance for Many.
+
+* 0.7.0.0
+  - Removed NOINLINE pragmas.
+  - Changed internal representation to (Int, Data.IntMap Any) for a 2.5x append speedup.
+
+* 0.6.0.0
+  - Moved lens to data-diverse-lens
+
+* 0.5.0.0
+  - Renamed type level functions module from Type to TypeLevel
+
+* 0.4.0.0
+  - Removed Emit typeclass, breaking renames. Added label accessors.
+
+* 0.1.0.0
+  - Initial version represented as (Int, Data.Map Int Any)
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,30 +1,11 @@
-Copyright Louis Pan (c) 2017
-
-All rights reserved.
+Copyright (c) 2019 Louis Pan. All rights reserved.
 
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
 
-    * Redistributions of source code must retain the above copyright
-      notice, this list of conditions and the following disclaimer.
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
 
-    * Redistributions in binary form must reproduce the above
-      copyright notice, this list of conditions and the following
-      disclaimer in the documentation and/or other materials provided
-      with the distribution.
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
 
-    * Neither the name of Louis Pan nor the names of other
-      contributors may be used to endorse or promote products derived
-      from this software without specific prior written permission.
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
 
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/data-diverse.cabal b/data-diverse.cabal
--- a/data-diverse.cabal
+++ b/data-diverse.cabal
@@ -1,5 +1,5 @@
 name:                data-diverse
-version:             4.6.0.0
+version:             4.7.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).
@@ -15,10 +15,11 @@
 license-file:        LICENSE
 author:              Louis Pan
 maintainer:          louis@pan.me
-copyright:           2017 Louis Pan
+copyright:           2019 Louis Pan
 category:            Data, Records
 build-type:          Simple
 extra-source-files:  README.md
+                   , CHANGELOG.md
 cabal-version:       >=1.10
 tested-with:         GHC == 8.0.1, GHC == 8.2.2
 
diff --git a/src/Data/Diverse/CaseFunc.hs b/src/Data/Diverse/CaseFunc.hs
--- a/src/Data/Diverse/CaseFunc.hs
+++ b/src/Data/Diverse/CaseFunc.hs
@@ -57,7 +57,7 @@
     case' (CaseFunc' f) = f
 
 -- | This handler stores a polymorphic function that work on higher kinds, eg 'Functor'
--- You may want to use @NoContraint for @k@
+-- You may want to use @C0 for @k@
 newtype CaseFunc1 (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r (xs :: [Type]) = CaseFunc1 (forall f x. (k (f x), k1 f, k0 x) => f x -> f r)
 
 type instance CaseResult (CaseFunc1 k k1 k0 r) (f x) = f r
@@ -68,7 +68,18 @@
 instance (k (f x), k1 f, k0 x) => Case (CaseFunc1 k k1 k0 r) (f x ': xs) where
     case' (CaseFunc1 f) = f
 
--- | A varation of 'CaseFunc' that doesn't change the return type
+newtype CaseFunc1_ (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r x (xs :: [Type]) = CaseFunc1_ (forall f. (k (f x), k1 f, k0 x) => f x -> f r)
+
+type instance CaseResult (CaseFunc1_ k k1 k0 r x) (f x) = f r
+
+instance Reiterate (CaseFunc1_ k k1 k0 r x) xs where
+    reiterate (CaseFunc1_ f) = CaseFunc1_ f
+
+instance (k (f x), k1 f, k0 x) => Case (CaseFunc1_ k k1 k0 r x) (f x ': xs) where
+    case' (CaseFunc1_ f) = f
+
+
+-- | A varation of 'CaseFunc1' that doesn't change the return type
 newtype CaseFunc1' (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) (xs :: [Type]) = CaseFunc1' (forall f x. (k (f x), k1 f, k0 x) => f x -> f x)
 
 type instance CaseResult (CaseFunc1' k k1 k0) (f x) = f x
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
@@ -39,7 +39,7 @@
 instance Reiterate (Cases fs r) xs where
     reiterate (Cases s) = Cases s
 
--- | UndecidableInstances because @fs@ appers more often.
+-- | UndecidableInstances because @fs@ appears more often.
 instance UniqueMember (Head xs -> r) fs => Case (Cases fs r) xs where
     case' (Cases s) = grab @(Head xs -> r) s
 
@@ -77,13 +77,6 @@
        (AllConstrained ((~) r) (CaseResults (Cases fs r) fs))
     => Many fs -> Cases fs r xs
 cases' = Cases
-
--- -- | Create a partially appliable contraint :: [Type] -> Constraint
--- -- Idea from https://hackage.haskell.org/package/constraint-manip-0.1.0.0/docs/src/Control.ConstraintManip.html
--- -- type MyC f xs = (f xs)
--- class (f xs) => MyC f xs
--- instance (f xs) => MyC f xs
-
 
 -----------------------------------------------
 
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
@@ -2,8 +2,9 @@
 
 -- | Re-export Many without the constructor
 module Data.Diverse.Many (
-    -- * 'Many' type
-      Many -- Hiding constructor
+      -- * 'Many' type
+      -- | constructor not exported
+      Many
 
       -- * Isomorphism
     , IsMany(..)
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
@@ -196,13 +196,17 @@
 -- https://hackage.haskell.org/package/vinyl-0.6.0/docs/Data-Vinyl-TypeLevel.html#t:AllConstrained
 
 -- | This is useful as a level function for @k@ in 'CaseFunc1'
+-- @C@ stands for constraints.
+-- @C0@ is a type level function of @Type -> Constraint@
 class C0 a where
 instance C0 a where
 
 -- UndecidableSuperInstances :(
+-- @C2@ is a type level function of @(Type -> Constraint) -> (Type -> Constraint) -> (Type -> Constraint)@
 class (c1 a, c2 a) => C2 c1 c2 a where
 instance (c1 a, c2 a) => C2 c1 c2 a where
 
+-- @C3@ is a type level function of @(Type -> Constraint) -> (Type -> Constraint) -> (Type -> Constraint) -> (Type -> Constraint)@
 class (c1 a, c2 a, c3 a) => C3 c1 c2 c3 a where
 instance (c1 a, c2 a, c3 a) => C3 c1 c2 c3 a where
 
diff --git a/src/Data/Diverse/Which.hs b/src/Data/Diverse/Which.hs
--- a/src/Data/Diverse/Which.hs
+++ b/src/Data/Diverse/Which.hs
@@ -1,13 +1,13 @@
 -- | Re-export Which without the constructor
 module Data.Diverse.Which (
       -- * 'Which' type
-      Which -- hiding constructor
-
+      -- | constructor not exported
+      Which
       -- * Single type
       -- ** Construction
     , impossible
     , impossible'
-    , totally
+    -- , totally
     , pick
     , pick0
     , pickOnly
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
@@ -28,7 +28,7 @@
       -- ** Construction
     , impossible
     , impossible'
-    , totally
+    -- , totally
     , pick
     , pick0
     , pickOnly
@@ -188,11 +188,11 @@
 impossible' :: Which '[Void] -> a
 impossible' a = case a of {}
 
--- | This function is useful to type restrict something that returns a polymorphic type
--- to return (Which '[]). Eg. use thishat to prove at compile time that a
--- finished continuation monad has no more unhandled holes.
-totally :: f (Which '[]) -> f (Which '[])
-totally = id
+-- -- | This function is useful to type restrict something that returns a polymorphic type
+-- -- to return (Which '[]). Eg. use this that to prove at compile time that a
+-- -- finished continuation monad has no more unhandled holes.
+-- totally :: f (Which '[]) -> f (Which '[])
+-- totally = id
 
 -- | Lift a value into a 'Which' of possibly other types @xs@.
 -- @xs@ can be inferred or specified with TypeApplications.
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
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
 
 module Data.Diverse.WhichSpec (main, spec) where
 
@@ -208,30 +209,30 @@
         it "can be 'switch'ed with 'Many' handlers in any order" $ do
             let y = pickN @0 (5 :: Int) :: Which '[Int, Bool, Bool, Int]
             switch y (
-                cases (show @Bool
+                cases $ show @Bool
                     ./ show @Int
-                    ./ nil)) `shouldBe` "5"
+                    ./ nil) `shouldBe` "5"
 
         it "can be 'switch'ed with 'Many' handlers with extraneous content" $ do
             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
                     ./ show @(Maybe Char)
                     ./ show @(Maybe Int)
                     ./ nil
-                )) `shouldBe` "5"
+                ) `shouldBe` "5"
 
         it "can be 'switchN'ed with 'Many' handlers in index order" $ do
             let y = pickN @0 (5 :: Int) :: Which '[Int, Bool, Bool, Int]
             switchN y (
-                casesN (show @Int
+                casesN $ show @Int
                     ./ show @Bool
                     ./ show @Bool
                     ./ show @Int
-                    ./ nil)) `shouldBe` "5"
+                    ./ nil) `shouldBe` "5"
 
         it "can be switched with a polymorphic 'CaseFunc' handler" $ do
             let y = pick (5 :: Int) :: Which '[Int, Bool]
@@ -280,7 +281,9 @@
                 mx = pick (Just 5 :: Maybe Int8) :: Which '[Maybe Int, Maybe Int8, Maybe Int16]
                 my = pick (Just 15 :: Maybe Int8) :: Which '[Maybe Int, Maybe Int8, Maybe Int16]
                 mz = pickN @1 (Just "5" :: Maybe String) :: Which '[Maybe String, Maybe String, Maybe String]
+                mz' = pickN @1 (Just ("5", "5") :: Maybe (String, String)) :: Which '[Maybe (String, String), Maybe (String, String), Maybe (String, String)]
             afmap (CaseFunc' @Num (+10)) x `shouldBe` y
             afmap (CaseFunc @Show @String show) x `shouldBe` z
             afmap (CaseFunc1' @C0 @Functor @Num (fmap (+10))) mx `shouldBe` my
             afmap (CaseFunc1 @C0 @Functor @Show @String (fmap show)) mx `shouldBe` mz
+            afmap (CaseFunc1_ @C0 @Functor @C0 @(String, String) (fmap (\i -> (i, i)))) mz `shouldBe` mz'
