diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,130 @@
+# Version 0.9
+
+* BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: The `Show`, `Read`,
+  `Eq`, `Ord` and `Generic` instances now live in the `exinst-base` package.
+  This is so that `exinst` doesn't need to depend on the large
+  `singletons-base`. Users wanting access to those instances need to import
+  `Exinst.Base` explicitly.
+
+* Builds with GHC 9.4.
+
+* The tests for `exinst` now live in `exinst-base`.
+
+# Version 0.8
+
+* Builds with GHC 8.10 and `singletons-2.7`.
+
+# Version 0.7
+
+* BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: All of the cabal flags
+  for turning on and off instances were removed.  The `hashable` are now
+  always exported from the `exinst`, and the `aeson`, `bytes`,
+  `cereal` and `serialise` instances  are now exported from new
+  packages `exinst-aeson`, `exinst-bytes`, `exinst-cereal` and
+  `exinst-serialise`. The instances exported from those packages are
+  the same as the ones exported with `exinst-0.6`.
+
+
+# Version 0.6
+
+* The `binary` and `deepseq` Cabal flags were removed since these two packages
+  are always included with the GHC distribution, so it doesn't make sense to
+  make them optional.
+
+* The optional dependencies hidden behind Cabal flags now apply to the test
+  suite as well.
+
+* Builds with GHC 8.4.
+
+
+# Version 0.5
+
+* BREAKING: Depend on `singletons == 2.3.*`.
+
+* Add `same{1,2,3,4}`.
+
+* Add dependencies on `cborg` and `serialise`
+
+* Add instances for `serialise` (binary CBOR encoding/decoding)
+
+
+# Version 0.4
+
+* BREAKING: Decouple `binary` and `cereal` instances from `bytes`. This
+  introduces a slight backwards incompatible change if you were using some
+  `Serial` instances that depended on host endianness (such as `Int`).
+
+* Add `P1`, `P2`, `P3`, `P4`.
+
+* Add `S1`, `S2`, `S3`, `S4`.
+
+* Add `Read` instances for `Some{1,2,3,4}`.
+
+* Moved documentation from `README.md` into the top-level `Exinst` module.
+
+
+# Version 0.3.0.1
+
+* Removed dependency on `generic-random`.
+
+* Correctly deal with cabal flags for `deepseq` and `hashable`.
+
+* Add `binary`'s `Data.Binary.Binary` and `cereal`'s `Data.Serialize.Serialize`
+  instances for `Some{1,2,3,4}`. These instances are compatible with each other
+  and rely on the `Data.Bytes.Serial` instances.
+
+
+# Version 0.3
+
+* BREAKING: Renamed module `Exinst.Singletons` to  `Exinst`.
+
+* BREAKING: The `Exinst.Instances.Base` module is gone. The `base` instances are
+  now exported from `Exinst`.
+
+* Add `Dict0`.
+
+* Re-export `Constraint` from `base`.
+
+* Add `Dict{0,2,3,4}` instances for `Bool`.
+
+* Add `GHC.Generics.Generic` support for `Some{1,2,3,4}`. This only works for
+  indexes with `PEnum` and `PBounded` instances.
+
+* Added tests.
+
+* Added `Test.QuickCheck.Arbitrary` instances for `Some{1,2,3,4}` in
+  `Exinst.Instances.QuickCheck`. These instances and their dependency on
+  `QuickCheck` can be toggled with the `quickcheck` Cabal flag.
+
+* Added `Data.Aeson.{FromJSON,ToJSON}` instances for `Some{1,2,3,4}` in
+  `Exinst.Instances.Aeson`. These instances and their dependency on
+  `aeson` can be toggled with the `aeson` Cabal flag. These instances used to
+  exist in now-deprecated the `exinst-aeson` package, and are compatible with
+  them.
+
+* Added `Bytes.Serial.Serial` instances for `Some{1,2,3,4}` in
+  `Exinst.Instances.Bytes`. These instances and their dependency on `bytes` can
+  be toggled with the `bytes` Cabal flag. These instances used to exist in
+  now-deprecated the `exinst-bytes` package, and are compatible with them.
+
+* Added `Control.DeepSeq.NFData` instances for `Some{1,2,3,4}` in
+  `Exinst.Instances.DeepSeq`. These instances and their dependency on `deepseq`
+  can be toggled with the `deepseq` Cabal flag. These instances used to exist in
+  now-deprecated the `exinst-deepseq` package, and are compatible with them.
+
+* Added `Data.Hashable.Hashable` instances for `Some{1,2,3,4}` in
+  `Exinst.Instances.DeepSeq`. These instances and their dependency on `hashable`
+  can be toggled with the `hashable` Cabal flag. These instances used to exist
+  in now-deprecated the `exinst-hashable` package, and are compatible with them.
+
+
 # Version 0.2
 
 * Depend on `singletons-2.2`, which means `KProxy` is gone.
 
 * Add `_Some{1,2,3,4}` prisms.
 
-* Add `Dict` instance for `Bool`.
+* Add `Dict1` instance for `Bool`.
 
 * Add `some{1,2,3,4}SingRep`.
 
diff --git a/LICENSE.txt b/LICENSE.txt
--- a/LICENSE.txt
+++ b/LICENSE.txt
@@ -1,4 +1,4 @@
-Copyright (c) 2015-2016, Renzo Carbonara
+Copyright (c) 2015-2018, Renzo Carbonara
 
 All rights reserved.
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,565 +1,9 @@
 # exinst
 
-> See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt)
-> file to learn about the legal terms and conditions for this library.
-
-Exinst is a library providing you with tools to automatically derive instances for
-type-indexed types whose type-indexes have been existentialized. Currently it only
-supports using [`singleton`](https://hackage.haskell.org/package/singletons) types as
-type-indexes.
-
-> TODO: Support for non-singleton-types types with kind `*` using `Typeable` should
-> be possible, but I haven't worked on that yet. It's on the roadmap.
-
-In short, what `exinst` currently gives you is: For any type ``t :: k -> *``,
-if `k` is a singleton type and `c (t k) :: Constraint` is satisfied, then you can
-existentialize away the `k` parameter with `Some1 t`, and have `c (Some1 t)`
-automatically satisfied. Currently, up to 4 type indexes can be existentialized
-using `Some1`, `Some2`, `Some3` and `Some4` respectively.
-
-> NOTE: This tutorial asumes some familiarity with singleton types as implemented
-> by the [`singleton`](https://hackage.haskell.org/package/singletons) library.
-> A singleton type is, in very rough terms, a type inhabited by a single term,
-> which allows one to go from its term-level representation to its type-level
-> representation and back without much trouble. A bit like the term `()`, which
-> is of type `()`: whenever you have the type `()` you know what that its
-> term-level representation must be `()`, and whenever you have the term `()`
-> you know that its type must be `()`.
-
-## Motivation
-
-As a motivation, let's consider the following example:
-
-```haskell
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE StandaloneDeriving #-}
-
-data Size = Big | Small
-
-data Receptacle (a :: Size) :: * where
-  Vase :: Receptacle 'Small
-  Glass :: Receptacle 'Small
-  Barrel :: Receptacle 'Big
-
-deriving instance Show (Receptacle a)
-```
-
-`Receptacle` can describe three types of receptacles (`Vase`, `Glass` and
-`Barrel`), while at the same time being able to indicate, at the type level,
-whether the size of the receptacle is `Big` or `Small`. Additionally, we've
-provided `Show` instances for `Receptacle`. 
-
-Now, if we want to put `Receptacle`s in a container, for example in `[]`, we can
-do so only as long as the `Receptacle` type is fully applied and monomorphic. That is, we can
-have `[Receptacle 'Small]` and `[Receptacle 'Big]`, but we can't have
-`[Receptacle]` nor `[forall a. Receptacle a]`. So, if we want to have `Receptacle`s of different sizes in a
-container like `[]`, we need a different solution.
-
-At this point we need to ask ourselves why we need to put `Receptacle`s of
-different sizes in a same container. If the answer is something like “because we
-want to show all of them, no matter what size they are”, then we should realize
-that what we are actually asking for is that no matter what `Size` our
-`Receptable` has, we need to be able to find a `Show` instance for that
-`Receptacle`. In Haskell, we can express just that using existential types
-and constraints hidden behind a data constructor.
-
-```haskell
---We need to add these language extensions to the ones in the previous example
---{-# LANGUAGE ExistentialQuantification #-}
---{-# LANGUAGE FlexibleContexts #-}
-
-data ReceptacleOfAnySizeThatCanBeShown
-  = forall a. (Show (Receptacle a))
-      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)
-```
-
-We can construct values of type `ReceptacleOfAnySizeThatCanBeShown` only as long
-as there exist a `Show` instance for the `Receptacle a` we give to the
-`MkReceptacleOfAnySizeThatCanBeShown` constructor. In our case, both `Receptacle
-'Small` and `Receptacle 'Big` have `Show` instances, so all of `Vase`, `Glass` and
-`Barrel` can be used successfully with `MkReceptacleOfAnySizeThatCanBeShown`.
-
-Now, `ReceptacleOfAnySizeThatCanBeShown` on itself doesn't yet have a `Show`
-instance, and we can't derive one automatically using the `deriving` mechanism,
-but we can give an explicit `Show` instance that just forwards the work to the
-`Show` instance of the underlying `Receptacle a`.
-
-```haskell
-instance Show ReceptacleOfAnySizeThatCanBeShown where
-  show (MkReceptacleOfAnySizeThatCanBeShown a) = show a
-```
-
-That works as intended:
-
-```
-> show (MkReceptacleOfAnySizeThatCanBeShown Vase)
-"Vase"
-> show (MkReceptacleOfAnySizeThatCanBeShown Barrel)
-"Barrel"
-```
-
-And now, as we wanted, we can put `Receptacle`s of different sizes in a `[]` and
-show them (as long as we wrap each of them as
-`ReceptacleOfAnySizeThatCanBeShown`, that is).
-
-```
-> map show [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel]
-["Vase", "Barrel"]
-```
-
-However, the above solution is unsatisfying for various reasons: For one, the
-`Show` instance for `ReceptacleOfAnySizeThatCanBeShown` works only as long as
-the `ReceptacleOfAnySizeThatCanBeShown` itself carries a witness that the `Show`
-constraint for `Receptacle a` is satisfied, which means that if we want to write
-yet another instance for `ReceptacleOfAnySizeThatCanBeShown` that simply forwards
-its implementation to the underlying `Receptacle a`, say `Eq`, then the
-`MkReceptacleOfAnySizeThatCanBeShown` constructor would need to be modified to witness
-the `Eq (Receptacle a)` instance too:
-
-```haskell
-data ReceptacleOfAnySizeThatCanBeShown
-  = forall a. (Show (Receptacle a), Eq (Receptacle a))
-      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)
-```
-
-With that in place we can provide an `Eq` instance for
-`ReceptacleOfAnySizeThatCanBeShown` as we did for `Show` before, but if we pay
-close attention, we can see how the implementation of
-`ReceptacleOfAnySizeThatCanBeShown` starts to become a bottleneck: Every
-instance we want to provide for `ReceptacleOfAnySizeThatCanBeShown` that simply
-forwards its work to the underlying `Receptacle a` needs to be witnessed by
-`MkReceptacleOfAnySizeThatCanBeShown` itself, it is not enough that there exists
-an instance for `Receptacle a`. Moreover, even the name
-`ReceptacleOfAnySizeThatCanBeShown` that we chose before isn't completely
-accurate anymore, and will become less and less accurate as we continue adding
-constraints to `MkReceptacleOfAnySizeThatCanBeShown`.
-
-Additionally, everywhere we use the `MkReceptacleOfAnySizeThatCanBeShown`
-constructor we need to witness that the existentialized `Receptacle a` satisfies
-all the required constraints, which means that, if the `Receptacle a` we pass to
-`MkReceptacleOfAnySizeThatCanBeShown` is being received, say, as a parameter to
-a function, then the type of that function will also require that its caller
-satisfies all of the same constraints, even though it is obvious to us,
-statically, that the instances exist. We can now see how all of this becomes
-unmanegeable, or at least very *boilerplatey*, as those constraints start to
-propagate through our code base.
-
-What we need is a way for instances such as the `Show` instance for
-`ReceptacleOfAnySizeThatCanBeShown` to find the `Show` instance for `Receptacle
-a` without it being explicitely witnessed by the
-`MkReceptacleOfAnySizeThatCanBeShown` constructor. That is exactly the problem
-that `exinst` solves: allowing *exi*stentials to find their *inst*ances.
-
-
-## Usage
-
-Given the code for `Size`, `Receptacle` and its `Show` instances above, we can
-achieve the same functionality as our initial `ReceptacleOfAnySizeThatCanBeShown` by
-existentializing the type indexes of `Receptacle 'Small` and `Receptacle 'Big`
-as `Some1 Receptacle`. In order to do that, we must first ensure that `Size` and its
-constructors can be used as singleton types (as supported by the `singletons` library),
-for which we can use some TH provided by `Data.Singletons.TH`:
-
-```haskell
-import Data.Singletons.TH
-
-Data.Singletons.TH.genSingletons [''Size]
-```
-
-And we'll also need a `Show` instance for `Size` for reasons that will become
-apparent later:
-
-```haskell
-deriving instance Show Size
-```
-
-Now we can construct a `Show1 Size` and `show` achieving the same results as we
-did with `ReceptacleOfAnySizeThatCanBeShown` before.
-
-Note: this code won't work yet. Keep reading.
-
-```
-> import Exinst.Singletons (some1)
-> import Exinst.Instances.Base ()
-> :t some1 Glass
-:t some1 Glass :: Some1 Receptacle
-> show (some1 Glass)
-"Some1 Small Glass"
-```
-
-Well, actually, the default `Show` instance for `Some1` shows a bit more of
-information, as it permits this string to be `Read` back into a `Some1
-Receptacle` if needed, but displaying just `"Glass"` would be possible too, if
-desired.
-
-> TODO: Implement said `Read` instance.
-
-The important thing to notice in the example above is that `some1` does not
-require us to satisfy a `Show (Receptacle 'Small)` constraint, it just requires
-that the type index for the type-indexed type we give it as argument is a
-singleton type:
-
-```haskell
-some1 :: forall (f1 :: k1 -> *) (a1 :: k1). SingI a1 => f1 a1 -> Some1 f1
-```
-
-It is the application of `show` to `some1 Glass` which will fail to compile if
-there isn't a `Show` instance for `Receptacle 'Small`, complaining that a `Show`
-instance for `Some1 Receptable` can't be found. The reason for this is that even
-if `Show` instances for `Some1` are derived for free, they are only derived for
-`Some1 (t :: k1 -> *)` where a `Show (t a)` for a specific but statically
-unknown `a` can be found at runtime (mostly, there are other minor requirements too).
-The mechanism through which instances are found at runtime relies on `Dict` from the
-[`constraints`](https://hackage.haskell.org/package/constraints) library, which
-`exinst` wraps in a `Dict1` typeclass to be instantiated once per singleton
-type.
-
-```haskell
--- The Exinst.Singletons.Dict1 class
-class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) where
-  dict1 :: Sing (a1 :: k1) -> Dict (c (f1 a1))
-```
-
-What `Dict1` says is that: for a type-indexed type `f1`, given a term-level
-representation of the singleton type that indexes said `f1`, we can obtain a
-witness that the constraint `c` is satisfied by `f1` applied to the singleton
-type.
-
-That class seems to be a bit too abstract, but the instances we as users need to
-write for it are quite silly and straightforward. Even *boilerplatey* if you
-will; they could even be generated using TH
-
-> TODO: Write the TH for deriving the `Dict{1,2,3,4}` implementation.
-
-Here's an example of how to provide `Show` support for `Some1 Receptacle` via
-`Dict1`:
-
-```
-instance (Show (Receptacle 'Small), Show (Receptacle 'Big)) => Dict1 Show Receptacle where
-  dict1 = \x -> case x of
-    SSmall -> Dict
-    SBig -> Dict
-```
-
-The implementation of `dict1` looks quite silly, but it has to look like that as
-it is only by pattern-matching on each of the `Sing Size` constructors that we
-learn about the type level representation of a singleton type, which we then use
-to select the proper `Show` instance among all of those listed in the instance head.
-
-Given this `Dict1` instance, we can proceed to excecute the REPL example mentioned before
-and it will work just fine.
-
-However, that `Dict1` instance is still a bit insatisfactory: If we wanted,
-again, to provide `Eq` support for our `Some1 Receptacle` type, we would need to
-write yet another `Dict1` instance like the one above, but mentioning `Eq`
-instead of `Show`. We can do better.
-
-The trick, when writing `Dict1` instances such as the one above, is to leave `c`
-and `f1 :: k1 -> *` completely polymorphic, and instead only talk concretely
-about the singleton type with kind `k1`. This might sound strange at first, as
-`c` and `f1` are the only two type parameters to `Dict1`. But as it often happens
-when working with singleton types, we are not particularly interested in the
-types involved, but in their kinds instead. So, this is the `Dict1` instance
-you often want to write:
-
-```haskell
-instance (c (f1 'Small), c (f1 'Big)) => Dict1 c f1 where
-  dict1 = \x -> case x of
-    SSmall -> Dict
-    SBig -> Dict
-```
-
-That instance says that for any choice of `c` and `f1 :: Size -> *`, if an
-instance for `c (f1 a)` exists for a specific choice of `a`, then, given a term
-level representation for that `a` and the aid of `dict1`, said instance can be
-looked up at runtime.
-
-Notice that `Some1` itself doesn't have any requirements about `Dict1`, it's the
-various instances for `Some1` who rely on `Dict1`. `Dict1` has nothing to do
-with `Some1`, nor with the choice of `f` nor with the choice of `c`; it is only
-related to the singleton type used as a type-index for `f`.
-
-As of this writing, we can find some ready-made instances for `Some1`, `Some2`,
-`Some3` and `Some4` in the following modules, which you need to import so as to
-bring to scope the desired instances at their usage site:
-
-* Package `exinst`, module `Exinst.Instances.Base`: Instances for various
-  type-classes found in the `base` package: `Eq`, `Ord`, `Show`.
-
-* Package `exinst-aeson`, module `Exinst.Instances.Aeson`: Instances for
-  `FromJSON` and `ToJSON` from the `aeson` package.
-
-* Package `exinst-bytes`, module `Exinst.Instances.Bytes`: Instances for
-  `Serial` from the `bytes` package.
-
-* Package `exinst-hashable`, module `Exinst.Instances.Hashable`: Instances for
-  `Hashable` from the `hashable` package.
-
-* Package `exinst-deepseq`, module `Exinst.Instances.DeepSeq`: Instances for
-  `NFData` from the `deepseq` package.
-
-You are invited to read the instance heads for said instances so as to understand
-what you need to provide in order to get those instances “for free”. As a rule of
-thumb, most instances will require this: If you expect to have an instance for
-`class Y => Z a` satisfied for `Some1 (f :: k -> *)`, then make sure an instance
-for `Z` is available for the `DemoteRep ('KProxy :: KProxy k)`, that a `Dict1 Z
-(f :: k -> *)` or more general instance exists, and that the `Y` instance for
-`Some1 (f :: k -> *)` exists too.
-
-> TODO: Have something similar to `Dict1` and friends for working with
-> non-singleton types, possibly integrating with 'Data.Constraint.Forall.ForallT'
-> if it made sense to do so.
-
-Here is the full code needed to have, say, the `Eq`, `Show`, `ToJSON` and
-`FromJSON` instances available for `Some1 Receptacle`:
-
-```haskell
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-import qualified Data.Aeson as Ae
-import           Data.Constraint (Dict(Dict))
-import qualified Data.Singletons.TH
-import           Exinst.Singletons (Dict1(dict1))
-
------
-
-data Size = Big | Small
-  deriving (Eq, Show)
-
-Data.Singletons.TH.genSingletons [''Size]
-Data.Singletons.TH.singDecideInstances [''Size]
-
-instance Ae.ToJSON Size where
-  toJSON = \x -> case x of
-    Small -> Ae.toJSON ("Small" :: String)
-    Big -> Ae.toJSON ("Big" :: String)
-
-instance Ae.FromJSON Size where
-  parseJSON = Ae.withText "Size" $ \t -> case t of
-     "Big" -> return Big
-     "Small" -> return Small
-     _ -> fail "Unknown"
-
-
-instance (c (f 'Big), c (f 'Small)) => Dict1 c f where
-  dict1 = \x -> case x of
-    SBig -> Dict
-    SSmall -> Dict
-
------
-
-data Receptacle (a :: Size) :: * where
-  Vase :: Receptacle 'Small
-  Glass :: Receptacle 'Small
-  Barrel :: Receptacle 'Big
-
-deriving instance Eq (Receptacle a)
-deriving instance Show (Receptacle a)
-
-instance Ae.ToJSON (Receptacle a) where
-  toJSON = \x -> case x of
-    Vase -> Ae.toJSON ("Vase" :: String)
-    Glass -> Ae.toJSON ("Glass" :: String)
-    Barrel -> Ae.toJSON ("Barrel" :: String)
-
-instance Ae.FromJSON (Receptacle 'Small) where
-  parseJSON = Ae.withText "Receptacle 'Small" $ \t -> case t of
-     "Vase" -> return Vase
-     "Glass" -> return Glass
-     _ -> fail "Unknown"
-
-instance Ae.FromJSON (Receptacle 'Big) where
-  parseJSON = Ae.withText "Receptacle 'Big" $ \t -> case t of
-     "Barrel" -> return Barrel
-     _ -> fail "Unknown"
-```
-
-Now, provided that we import `Exinst.Instances.Base` and
-`Exinst.Instances.Aeson`, `Some1 Receptacle` will have `Eq`, `Show`, `FromJSON`
-and `FromJSON` instances:
-
-```
-> import Exinst.Instances.Base ()
-> import Exinst.Instances.Aeson ()
-
-> -- Trying `fromSome1`.
-> fromSome1 (some1 Vase) == Just Vase
-True
-> fromSome1 (some1 Vase) == Just Glass
-False
-> fromSome1 (some1 Vase) == Just Barrel
-False
-
-> -- Trying `withSome1`
-> withSome1 (some1 Vase) show
-"Vase"
-> withSome1 (some1 Vase) (== Vase)    -- This will fail, use `fromSome1`
-                                      -- if you know you are expecting
-                                      -- a `Receptacle 'Small`
-
-> -- Trying the `Eq` instance.
-> some1 Vase == some1 Vase
-True
-> some1 Vase == some1 Glass
-False
-> some1 Vase == some1 Barrel
-False
-
-> -- Trying the `Show` instance.
-> show (some1 Vase)
-"Some1 Small Vase"
-> map show [some1 Vase, some1 Glass, some1 Barrel]
-["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"]
-
-> -- Trying the `ToJSON` and `FromJSON` instances.
-> Ae.encode (some1 Vase)
-"[\"Small\",\"Vase\"]"  -- Just like in Show, the ToJSON adds some information
-                        -- about the Size type-index. That's why we require
-                        -- Size to provide a ToJSON instance too.
-> Ae.decode (Ae.encode (some1 Vase)) == Just (some1 Vase)
-True
-> Ae.decode (Ae.encode (some1 Vase)) == Just (some1 Glass)
-False
-```
-
-
-## About `Some2`, `Some3` and `Some4`.
-
-Just like `Some1` hides the last singleton type index from fully applied
-type-indexed type, `Some2` hides the last two type indexes, `Some3` hides the
-last three, and `Some3` hides the last four. They can be used in the same way as
-`Some1`.
-
-Like as most instances for `Some1` require `Dict1` instances to be present for
-their singleton type-index, most instances for `Some2`, `Some3` and `Some4` will
-require that `Dict2`, `Dict3` or `Dict4` instances exist, respectively. Writing
-these instances is very straightforward. Supposing you have a type `X :: T4 ->
-T3 -> T2 -> T1 -> *` and want to existentialize all of the four type indexes yet
-be able to continue using all of its instances, we can write something like
-this:
-
-```haskell
-instance (c (f1 'T1a), c (f1 'T1b)) => Dict1 c (f1 :: T1 -> *) where
-  dict1 = \x -> case x of { ST1a -> Dict; ST1b -> Dict }
-instance (Dict1 c (f2 'T2a), Dict1 c (f2 'T2b)) => Dict2 c (f2 :: T2 -> k1 -> *) where
-  dict2 = \x -> case x of { ST2a -> dict1; ST2b -> dict1 }
-instance (Dict2 c (f3 'T3a), Dict2 c (f3 'T3b)) => Dict3 c (f3 :: T3 -> k2 -> k1 -> *) where
-  dict3 = \x -> case x of { ST3a -> dict2; ST3b -> dict2 }
-instance (Dict3 c (f4 'T4a), Dict3 c (f4 'T4b)) => Dict4 c (f4 :: T4 -> k3 -> k2 -> k1 -> *) where
-  dict4 = \x -> case x of { ST4a -> dict3; ST4b -> dict3 }
-```
-
-That is, assuming the following `T1`, `T2`, `T3` and `T4`:
-
-```haskell
-data T4 = T4a | T4b
-data T3 = T3a | T3b
-data T2 = T2a | T2b
-data T1 = T1a | T1b
-```
-
-Effectively, we wrote just one instance per singleton type per type-index
-position, each of them promoting a term-level representation of a singleton
-type to its type-level representation and forwarding the rest of the work to
-a “smaller” dict. That is, `dict4` reifies the type of the fourth-to-last
-type-index of `X` and then calls `dict3` to do the same for the third-to-last
-type-index of `X` and so on. Notice, however, how we didn't need to mention `X`
-in none of the instances above: As we said before, these instances are
-intended to work for any choice of `c`, `f4`, `f3`, `f2` and `f1`.
-
-> TODO: See if instead of having `Some1`, `Some2`, `Some3`, `Some4`, and their
-> respective `Dict1`, `Dict2`, `Dict3` and `Dict4`, etc., we can have a single
-> `SomeN` and a single `DictN` working out the number of parameters using
-> type-level natural numbers.
-
-## Converting `Some1 (f :: k -> *)` to `f (a :: k)`.
-
-If you have a `Some1 (f :: k -> *)` and you know, statically, that you need an
-specific `f (a :: k)`, then you can use `fromSome1` which will give you an
-`f (a :: k)` only if `a` was the type that was existentialized by `Some1`.
-Using `fromSome1` requires that the singleton type-index implements
-`Data.Singletons.Decide.SDecide`, which can be derived mechanically with TH by
-means of `Data.Singletons.TH.singInstance`.
-
-If you don't know, statically, the type of `f (a :: k)`, then you can use
-`withSome1Sing` or `withSome1` to work with `f (a :: k)` as long as `a` never
-leaves their scope (don't worry, the compiler will yell at you if you try to do
-that).
-
-
-# Library implementors: Writing instances for `Some1` and friends.
-
-Instances for `Some1` seem to come out of thin air, but the truth is that they
-need to be written at least once by library authors so that, provided all its
-requirements are satisfied, they are made available.
-
-When we imported `Exinst.Instances.Base` before, we brought to scope, among
-other things, the `Show` instance for `Some1`, which is defined as this:
-
-```haskell
--- Internal wrapper so that we don't have to write the string manipulation parts
--- in the 'Show' instance by hand.
-data Some1'Show r1 x = Some1 r1 x deriving (Show)
-
-instance forall (f1 :: k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k1)
-    , Show (DemoteRep ('KProxy :: KProxy k1))
-    , Dict1 Show f1
-    ) => Show (Some1 f1)
-  where
-    showsPrec n = \some1 -> withSome1Sing some1 $ \sa1 (x :: f1 a1) ->
-       case dict1 sa1 :: Dict (Show (f1 a1)) of
-          Dict -> showsPrec n (Some1 (fromSing sa1) x)
-```
-
-This code should be relatively straightforward if you are familiar with uses of
-the `singletons` and `constraints` libraries. We are simply reifying singleton
-types from their term-level representation to their type-level representation,
-and afterwards using the `Dict1` mechanism to lookup the required instances
-during runtime. Additionaly, this instance requires that the term level
-representation of the singleton type implements `Show` too, as, like we saw in a
-previous example, the type index itself is shown in this `Show` implementation,
-in the hope that it can be later recovered and reified to the type level when
-using `Read`.
-
-
-# Related work on Generic instances for GADTs
+See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/exinst/LICENSE.txt)
+file to learn about the legal terms and conditions for this library.
 
-One of the most appealing applications of `exinst` is to reduce the boilerplate
-associated with manually writing instances for existentialized GADTs. However,
-quite often, writing instances for said GADTs on its own is very cumbersome
-due to the lack of generic instance deriving mechanisms for GADTs. There exists,
-however, at the time of this writing, at least one library able to derive
-generic representations for some GADTs using TH:
-[`instant-generics`](https://hackage.haskell.org/package/instant-generics).
+Find documentation for this library in the top-level
+[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/lib/Exinst.hs)
+module.
 
-Combining [`instant-generics`](https://hackage.haskell.org/package/instant-generics) (and
-[`instant-aeson`](https://hackage.haskell.org/package/instant-aeson),
-[`instant-hashable`](https://hackage.haskell.org/package/instant-hashable),
-[`instant-bytes`](https://hackage.haskell.org/package/instant-bytes) and
-[`instant-deepseq`](https://hackage.haskell.org/package/instant-deepseq))
-with [`exinst`](https://hackage.haskell.org/package/exinst) (and
-[`exinst-aeson`](https://hackage.haskell.org/package/exinst-aeson),
-[`exinst-hashable`](https://hackage.haskell.org/package/exinst-hashable),
-[`exinst-bytes`](https://hackage.haskell.org/package/exinst-bytes) and
-[`exinst-deepseq`](https://hackage.haskell.org/package/exinst-deepseq)),
-you can reduce a lot of the boilerplate associated with working with GADTs, in
-particular when it comes to the serialization and deserialization of them (i.e.,
-`Show` and `Read`, or `ToJSON` and `FromJSON`) or puting GADTs in monomorphic
-containers (i.e., `[]` or `HashMap`), which become straightforward things to do
-once you are able able to both generically derive the instances for your GADT
-and then existentialize away the type-index while keeping the underlying
-instances available.
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/exinst.cabal b/exinst.cabal
--- a/exinst.cabal
+++ b/exinst.cabal
@@ -1,29 +1,40 @@
 name:                exinst
-version:             0.2
+version:             0.9
 author:              Renzo Carbonara
-maintainer:          renzoλcarbonara.com.ar
-copyright:           Renzo Carbonara 2015-2016
+maintainer:          renλren!zone
+copyright:           Renzo Carbonara 2015
 license:             BSD3
 license-file:        LICENSE.txt
 extra-source-files:  README.md CHANGELOG.md
 category:            Data
 build-type:          Simple
-cabal-version:       >=1.18
-synopsis:            Derive instances for your existential types.
+cabal-version:       1.18
+synopsis:            Dependent pairs and their instances.
 homepage:            https://github.com/k0001/exinst
 bug-reports:         https://github.com/k0001/exinst/issues
 
 
 library
-  hs-source-dirs: src/lib
+  hs-source-dirs: lib
   default-language: Haskell2010
   exposed-modules:
-      Exinst.Singletons
-      Exinst.Instances.Base
+      Exinst
+  other-modules:
+      Exinst.Internal
+      Exinst.Internal.Product
+      Exinst.Internal.Sum
+      Exinst.Binary
+      Exinst.DeepSeq
+      Exinst.Hashable
+      Exinst.QuickCheck
   build-depends:
       base >=4.9 && <5.0
-    , constraints >=0.4 && <0.9
-    , profunctors >=5.0 && <6.0
-    , singletons >=2.2 && <2.3
+    , binary
+    , constraints >=0.4
+    , deepseq
+    , hashable
+    , profunctors >=5.0
+    , singletons >= 3.0
+    , QuickCheck
   ghcjs-options: -Wall -O3
   ghc-options: -Wall -O2
diff --git a/lib/Exinst.hs b/lib/Exinst.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst.hs
@@ -0,0 +1,669 @@
+{-# LANGUAGE CPP #-}
+
+{- |
+
+Exinst is a library providing you with tools to recover type-indexed types whose
+type-indexes have been existentialized, as well as automatically deriving
+instances for them, as long as said type indexes are singleton types
+(see [singleton](https://hackage.haskell.org/package/singletons)).
+
+In short, what @exinst@ currently gives you is: For any type @t :: k -> *@, if
+@k@ is a singleton type and @c (t a) :: 'Constraint'@ is satisfied, then you can
+existentialize away the @a@ parameter with @'Some1' t@, recover it later, and
+have @c ('Some1' t)@ automatically satisfied. Currently, up to 4 type indexes
+can be existentialized using 'Some1', 'Some2', 'Some3' and 'Some4' respectively.
+
+NOTE: This tutorial asumes some familiarity with singleton types as implemented
+by the [singleton](https://hackage.haskell.org/package/singletons) library.
+A singleton type is, in very rough terms, a type inhabited by a single term,
+which allows one to go from its term-level representation to its type-level
+representation and back without much trouble. A bit like the term @()@, which
+is of type @()@. Whenever you have the type @()@ you know what that its
+term-level representation must be @()@, and whenever you have the term @()@
+you know that its type must be @()@.
+
+-}
+
+module Exinst
+ ( -- * Tutorial
+   -- $motivation
+
+   -- *** Usage
+   -- $usage
+
+   -- *** Recovering
+   -- $recovering
+
+   -- *** Many indexes
+   -- $manyIndexes
+
+   -- *** Writing instances
+   -- $writingInstances
+
+   -- *** Products and sums
+   -- $prodsums
+
+   -- * 1 type index
+   Some1(Some1)
+ , some1
+ , fromSome1
+ , _Some1
+ , withSome1
+ , withSome1Sing
+ , some1SingRep
+ , same1
+ , Dict1(dict1)
+
+   -- * 2 type indexes
+ , Some2(Some2)
+ , some2
+ , fromSome2
+ , _Some2
+ , withSome2
+ , withSome2Sing
+ , some2SingRep
+ , same2
+ , Dict2(dict2)
+
+   -- * 3 type indexes
+ , Some3(Some3)
+ , some3
+ , fromSome3
+ , _Some3
+ , withSome3
+ , withSome3Sing
+ , some3SingRep
+ , same3
+ , Dict3(dict3)
+
+   -- * 4 type indexes
+ , Some4(Some4)
+ , some4
+ , fromSome4
+ , _Some4
+ , withSome4
+ , withSome4Sing
+ , some4SingRep
+ , same4
+ , Dict4(dict4)
+
+   -- * Miscellaneous
+ , Dict0(dict0)
+
+   -- * Products
+ , P1(P1)
+ , P2(P2)
+ , P3(P3)
+ , P4(P4)
+
+   -- * Sums
+ , S1(S1L,S1R)
+ , S2(S2L,S2R)
+ , S3(S3L,S3R)
+ , S4(S4L,S4R)
+
+   -- * Re-exports
+ , Constraint
+ , Dict(Dict)
+ , Sing
+ , SingI
+ ) where
+
+import Data.Constraint (Constraint, Dict(Dict))
+
+import Data.Singletons (Sing, SingI)
+
+import Exinst.Internal
+import Exinst.Internal.Product
+import Exinst.Internal.Sum
+
+import Exinst.Binary ()
+import Exinst.DeepSeq ()
+import Exinst.Hashable ()
+import Exinst.QuickCheck ()
+
+{- $motivation
+
+As a motivation, let's consider the following example:
+
+@
+\{\-\# LANGUAGE GADTs \#\-\}
+\{\-\# LANGUAGE DataKinds \#\-\}
+\{\-\# LANGUAGE KindSignatures \#\-\}
+\{\-\# LANGUAGE FlexibleInstances \#\-\}
+\{\-\# LANGUAGE StandaloneDeriving \#\-\}
+
+data Size = Big | Small
+
+data Receptacle (a :: Size) :: * where
+  Vase :: Receptacle 'Small
+  Glass :: Receptacle 'Small
+  Barrel :: Receptacle 'Big
+
+deriving instance 'Show' (Receptacle a)
+@
+
+@Receptacle@ can describe three types of receptacles (@Vase@, @Glass@ and
+@Barrel@), while at the same time being able to indicate, at the type level,
+whether the size of the receptacle is @Big@ or @Small@. Additionally, we've
+provided 'Show' instances for @Receptacle@.
+
+Now, if we want to put @Receptacle@s in a container, for example in @[]@, we can
+do so only as long as the @Receptacle@ type is fully applied and monomorphic.
+That is, we can have @[Receptacle 'Small]@ and @[Receptacle 'Big]@, but we
+can't have @[Receptacle]@ nor @[forall a. Receptacle a]@. So, if we want to
+have @Receptacle@s of different sizes in a container like @[]@, we need a
+different solution.
+
+At this point we need to ask ourselves why we need to put @Receptacle@s of
+different sizes in a same container. If the answer is something like “because we
+want to show all of them, no matter what size they are”, then we should realize
+that what we are actually asking for is that no matter what @Size@ our
+@Receptable@ has, we need to be able to find a 'Show' instance for that
+@Receptacle@. In Haskell, we can express just that using existential types
+and constraints hidden behind a data constructor.
+
+@
+-- We need to add these language extensions to the ones in the previous example
+\{\-\# LANGUAGE ExistentialQuantification \#\-\}
+\{\-\# LANGUAGE FlexibleContexts \#\-\}
+
+data ReceptacleOfAnySizeThatCanBeShown
+  = forall a. ('Show' (Receptacle a))
+      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)
+@
+
+We can construct values of type @ReceptacleOfAnySizeThatCanBeShown@ only as long
+as there exist a 'Show' instance for the @Receptacle a@ we give to the
+@MkReceptacleOfAnySizeThatCanBeShown@ constructor. In our case, both @Receptacle
+'Small@ and @Receptacle 'Big@ have 'Show' instances, so all of @Vase@, @Glass@ and
+@Barrel@ can be used successfully with @MkReceptacleOfAnySizeThatCanBeShown@.
+
+Now, @ReceptacleOfAnySizeThatCanBeShown@ on itself doesn't yet have a 'Show'
+instance, and we can't derive one automatically using the @deriving@ mechanism,
+but we can give an explicit 'Show' instance that just forwards the work to the
+'Show' instance of the underlying @Receptacle a@.
+
+@
+instance 'Show' ReceptacleOfAnySizeThatCanBeShown where
+  'show' (MkReceptacleOfAnySizeThatCanBeShown a) = 'show' a
+@
+
+That works as intended:
+
+@
+> 'show' (MkReceptacleOfAnySizeThatCanBeShown Vase)
+"Vase"
+> 'show' (MkReceptacleOfAnySizeThatCanBeShown Barrel)
+"Barrel"
+@
+
+And now, as we wanted, we can put @Receptacle@s of different sizes in a @[]@ and
+show them (as long as we wrap each of them as
+@ReceptacleOfAnySizeThatCanBeShown@, that is).
+
+@
+> 'map' 'show' [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel]
+["Vase", "Barrel"]
+@
+
+However, the above solution is unsatisfying for various reasons: For one, the
+'Show' instance for @ReceptacleOfAnySizeThatCanBeShown@ works only as long as
+the @ReceptacleOfAnySizeThatCanBeShown@ itself carries a witness that the 'Show'
+constraint for @Receptacle a@ is satisfied, which means that if we want to write
+yet another instance for @ReceptacleOfAnySizeThatCanBeShown@ that simply forwards
+its implementation to the underlying @Receptacle a@, say 'Eq', then the
+@MkReceptacleOfAnySizeThatCanBeShown@ constructor would need to be modified to witness
+the @Eq (Receptacle a)@ instance too:
+
+@
+data ReceptacleOfAnySizeThatCanBeShown
+  = forall a. ('Show' (Receptacle a), 'Eq' (Receptacle a))
+      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)
+@
+
+With that in place we can provide an 'Eq' instance for
+@ReceptacleOfAnySizeThatCanBeShown@ as we did for 'Show' before, but if we pay
+close attention, we can see how the implementation of
+@ReceptacleOfAnySizeThatCanBeShown@ starts to become a bottleneck: Every
+instance we want to provide for @ReceptacleOfAnySizeThatCanBeShown@ that simply
+forwards its work to the underlying @Receptacle a@ needs to be witnessed by
+@MkReceptacleOfAnySizeThatCanBeShown@ itself, it is not enough that there exists
+an instance for @Receptacle a@. Moreover, even the name
+@ReceptacleOfAnySizeThatCanBeShown@ that we chose before isn't completely
+accurate anymore, and will become less and less accurate as we continue adding
+constraints to @MkReceptacleOfAnySizeThatCanBeShown@.
+
+Additionally, everywhere we use the @MkReceptacleOfAnySizeThatCanBeShown@
+constructor we need to witness that the existentialized @Receptacle a@ satisfies
+all the required constraints, which means that, if the @Receptacle a@ we pass to
+@MkReceptacleOfAnySizeThatCanBeShown@ is being received, say, as a parameter to
+a function, then the type of that function will also require that its caller
+satisfies all of the same constraints, even though it is obvious to us,
+statically, that the instances exist. We can now see how all of this becomes
+unmanegeable, or at least very *boilerplatey*, as those constraints start to
+propagate through our code base.
+
+What we need is a way for instances such as the 'Show' instance for
+@ReceptacleOfAnySizeThatCanBeShown@ to find the 'Show' instance for @Receptacle
+a@ without it being explicitely witnessed by the
+@MkReceptacleOfAnySizeThatCanBeShown@ constructor. That is exactly the problem
+that @exinst@ solves: allowing /exi/stentials to find their /inst/ances. Thus,
+the name of this library.
+
+-}
+
+{- $usage
+
+Given the code for @Size@, @Receptacle@ and its 'Show' instances above, we can
+achieve the same functionality as our initial @ReceptacleOfAnySizeThatCanBeShown@ by
+existentializing the type indexes of @Receptacle 'Small@ and @Receptacle 'Big@
+as @'Some1' Receptacle@. In order to do that, we must first ensure that @Size@ and its
+constructors can be used as singleton types (as supported by the @singletons@ library),
+for which we can use some @TemplateHaskell@ provided by @Data.Singletons.TH@:
+
+@
+import qualified "Data.Singletons.TH"
+
+Data.Singletons.TH.genSingletons [''Size]
+@
+
+And we'll also need a 'Show' instance for @Size@ for reasons that will become
+apparent later:
+
+@
+deriving instance 'Show' Size
+@
+
+Now we can construct a @Show1 Size@ and 'show' achieving the same results as we
+did with @ReceptacleOfAnySizeThatCanBeShown@ before.
+
+Note: this code won't work yet. Keep reading.
+
+@
+> import "Exinst" ('Some1', 'some1')
+> :t 'some1' Glass
+:t 'some1' Glass :: 'Some1' Receptacle
+> 'show' ('some1' Glass)
+"Some1 Small Glass"
+@
+
+Well, actually, the default 'Show' instance for 'Some1' shows a bit more of
+information, as it permits this string to be 'Read' back into a @'Some1'
+Receptacle@ if needed, but displaying just @"Glass"@ would be possible too, if
+desired.
+
+The important thing to notice in the example above is that @some1@ does not
+require us to satisfy a @'Show' (Receptacle 'Small)@ constraint, it just requires
+that the type index for the type-indexed type we give it as argument is a
+singleton type:
+
+@
+'some1' :: forall (f1 :: k1 -> *) (a1 :: k1). 'SingI' a1 => f1 a1 -> 'Some1' f1
+@
+
+It is the application of 'show' to @'some1' Glass@ which will fail to compile if
+there isn't a 'Show' instance for @Receptacle 'Small@, complaining that a 'Show'
+instance for @'Some1' Receptable@ can't be found. The reason for this is that even
+if 'Show' instances for 'Some1' are derived for free, they are only derived for
+@'Some1' (t :: k1 -> *)@ where a @'Show' (t a)@ for a specific but statically
+unknown @a@ can be found at runtime (mostly, there are other minor requirements too).
+The mechanism through which instances are found at runtime relies on 'Dict' from
+the [constraints](https://hackage.haskell.org/package/constraints) library, which
+@exinst@ wraps in a 'Dict1' typeclass to be instantiated once per singleton
+type.
+
+@
+-- The "Exinst.Dict1" class
+class 'Dict1' (c :: k0 -> 'Constraint') (f1 :: k1 -> k0) where
+  'dict1' :: 'Sing' (a1 :: k1) -> 'Dict' (c (f1 a1))
+@
+
+What 'Dict1' says is that: for a type-indexed type @f1@, given a term-level
+representation of the singleton type that indexes said @f1@, we can obtain a
+witness that the constraint @c@ is satisfied by @f1@ applied to the singleton
+type.
+
+That class seems to be a bit too abstract, but the instances we as users need to
+write for it are quite silly and straightforward.
+
+Here's an example of how to provide 'Show' support for @'Some1' Receptacle@ via
+'Dict1':
+
+@
+instance ('Show' (Receptacle 'Small), 'Show' (Receptacle 'Big)) => 'Dict1' 'Show' Receptacle where
+  'dict1' = \x -> case x of
+    SSmall -> 'Dict'
+    SBig -> 'Dict'
+@
+
+The implementation of @dict1@ looks quite silly, but it has to look like that as
+it is only by pattern-matching on each of the @'Sing' Size@ constructors that we
+learn about the type level representation of a singleton type, which we then use
+to select the proper 'Show' instance among all of those listed in the instance head.
+
+Given this 'Dict1' instance, we can proceed to excecute the REPL example mentioned before
+and it will work just fine.
+
+However, that 'Dict1' instance is still a bit insatisfactory: If we wanted,
+again, to provide 'Eq' support for our @'Some1' Receptacle@ type, we would need to
+write yet another 'Dict1' instance like the one above, but mentioning 'Eq'
+instead of 'Show'. We can do better.
+
+The trick, when writing 'Dict1' instances such as the one above, is to leave @c@
+and @f1 :: k1 -> k0@ completely polymorphic, and instead only talk concretely
+about the singleton type with kind @k1@. This might sound strange at first, as
+@c@ and @f1@ are the only two type parameters to 'Dict1'. But as it often happens
+when working with singleton types, we are not particularly interested in the
+types involved, but in their kinds instead. So, this is the 'Dict1' instance
+you often want to write:
+
+@
+instance (c (f1 'Small), c (f1 'Big)) => 'Dict1' c (f1 :: Size -> k0) where
+  'dict1' = \x -> case x of
+    SSmall -> 'Dict'
+    SBig -> 'Dict'
+@
+
+That instance says that for any choice of @c@ and @f1 :: Size -> k0@, if an
+instance for @c (f1 a)@ exists for a specific choice of @a@, then, given a term
+level representation for that @a@ and the aid of @dict1@, said instance can be
+looked up at runtime.
+
+Notice that 'Some1' itself doesn't have any requirements about 'Dict1', it's the
+various instances for 'Some1' who rely on 'Dict1'. 'Dict1' has nothing to do
+with 'Some1', nor with the choice of @f@ nor with the choice of @c@; it is only
+related to the singleton type used as a type-index for @f@.
+
+The @Exinst@ module exports ready-made instances for 'Some1', 'Some2', 'Some3'
+and 'Some4'.
+
+* 'Data.Binary.Binary' from the @binary@ package.
+
+* 'Data.Hashable.Hashable' from the @hashable@ package.
+
+* 'Control.DeepSeq.NFData' from the @deepseq@ package.
+
+* 'Test.QuickCheck.Arbitrary' from the @QuickCheck@ package.
+
+Furthermore, other libraries export other orphan instances for the datatypes
+exported by 'exinst':
+
+* [exinst-base](https://hackage.haskell.org/package/exinst-aeson) exports
+instances for 'Show', 'Read', 'Eq', 'Ord' and 'Generic' from the @base@
+package. Depends on the large @singleton-base@ package, that's why
+these instances are not in the @exinst@ package itself.
+
+* [exinst-aeson](https://hackage.haskell.org/package/exinst-aeson) exports
+instances for 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@
+package.
+
+* [exinst-bytes](https://hackage.haskell.org/package/exinst-bytes) exports
+instances for 'Data.Bytes.Serial' from the @bytes@ package.
+
+* [exinst-cereal](https://hackage.haskell.org/package/exinst-cereal) exports
+instances for 'Cereal.Serialize.Serialize' from the @cereal@ package.
+
+* [exinst-serialise](https://hackage.haskell.org/package/exinst-serialise)
+exports instances for 'Codec.Serialise.Serialise' from the @serialise@ package.
+
+
+You are invited to read the instance heads for said instances so as to understand
+what you need to provide in order to get those instances “for free”. As a rule of
+thumb, most instances will require this: If you expect to have an instance for
+@class Y => Z a@ satisfied for @'Some1' (f :: k1 -> *)@, then make sure an instance
+for @Z@ is available for the @DemoteRep k1@, that a @'Dict1' Z (f :: k1 -> k0)@ or
+more general instance exists, and that the @Y@ instance for @'Some1' (f :: k1 ->
+*)@ exists too.
+
+Here is the full code needed to have, say, the 'Eq' and 'Show' instances
+available for @'Some1' Receptacle@:
+
+@
+\{\-\# LANGUAGE ConstraintKinds \#\-\}
+\{\-\# LANGUAGE DataKinds \#\-\}
+\{\-\# LANGUAGE FlexibleInstances \#\-\}
+\{\-\# LANGUAGE GADTs \#\-\}
+\{\-\# LANGUAGE KindSignatures \#\-\}
+\{\-\# LANGUAGE MultiParamTypeClasses \#\-\}
+\{\-\# LANGUAGE OverloadedStrings \#\-\}
+\{\-\# LANGUAGE StandaloneDeriving \#\-\}
+\{\-\# LANGUAGE TemplateHaskell \#\-\}
+\{\-\# LANGUAGE TypeFamilies \#\-\}
+\{\-\# LANGUAGE UndecidableInstances \#\-\}
+
+import qualified "Data.Singletons.TH"
+import           "Exinst" ('Dict'('Dict'), 'Dict1'('dict1'))
+
+data Size = Big | Small
+  deriving ('Eq', 'Show')
+
+Data.Singletons.TH.genSingletons [''Size]
+Data.Singletons.TH.singDecideInstances [''Size]
+
+instance (c (f 'Big), c (f 'Small)) => 'Dict1' c f where
+  'dict1' = \x -> case x of
+    SBig -> 'Dict'
+    SSmall -> 'Dict'
+
+
+data Receptacle (a :: Size) :: * where
+  Vase :: Receptacle 'Small
+  Glass :: Receptacle 'Small
+  Barrel :: Receptacle 'Big
+
+deriving instance 'Eq' (Receptacle a)
+deriving instance 'Show' (Receptacle a)
+@
+
+Now, @'Some1' Receptacle@ will have 'Eq' and 'Show' instances:
+
+@
+> -- Trying 'fromSome1'.
+> 'fromSome1' ('some1' Vase) == 'Just' Vase
+'True'
+> 'fromSome1' ('some1' Vase) == 'Just' Glass
+'False'
+> 'fromSome1' ('some1' Vase) == 'Just' Barrel
+'False'
+
+> -- Trying 'withSome1'
+> 'withSome1' ('some1' Vase) 'show'
+"Vase"
+> 'withSome1' ('some1' Vase) (== Vase)    -- This will fail, use 'fromSome1'
+                                      -- if you know you are expecting
+                                      -- a @Receptacle 'Small@
+
+> -- Trying the 'Eq' instance.
+> 'some1' Vase == 'some1' Vase
+'True'
+> 'some1' Vase == 'some1' Glass
+'False'
+> 'some1' Vase == 'some1' Barrel
+'False'
+
+> -- Trying the 'Show' instance.
+> 'show' ('some1' Vase)
+"Some1 Small Vase"
+> 'map' 'show' ['some1' Vase, 'some1' Glass, 'some1' Barrel]
+["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"]
+@
+
+-}
+
+{- $manyIndexes
+
+Just like 'Some1' hides the last singleton type index from fully applied
+type-indexed type, 'Some2' hides the last two type indexes, 'Some3' hides the
+last three, and 'Some3' hides the last four. They can be used in the same way as
+'Some1'.
+
+Like as most instances for 'Some1' require 'Dict1' instances to be present for
+their singleton type-index, most instances for 'Some2', 'Some3' and 'Some4' will
+require that 'Dict2', 'Dict3' or 'Dict4' instances exist, respectively. Writing
+these instances is very straightforward. Supposing you have a type @X :: T4 ->
+T3 -> T2 -> T1 -> *@ and want to existentialize all of the four type indexes yet
+be able to continue using all of its instances, we can write something like
+this:
+
+@
+instance (c (f1 'T1a), c (f1 'T1b)) => 'Dict1' c (f1 :: T1 -> k0) where
+  'dict1' = \x -> case x of { ST1a -> 'Dict'; ST1b -> 'Dict' }
+instance ('Dict1' c (f2 'T2a), 'Dict1' c (f2 'T2b)) => 'Dict2' c (f2 :: T2 -> k1 -> k0) where
+  'dict2' = \x -> case x of { ST2a -> 'dict1'; ST2b -> 'dict1' }
+instance ('Dict2' c (f3 'T3a), 'Dict2' c (f3 'T3b)) => 'Dict3' c (f3 :: T3 -> k2 -> k1 -> k0) where
+  'dict3' = \x -> case x of { ST3a -> 'dict2'; ST3b -> 'dict2' }
+instance ('Dict3' c (f4 'T4a), 'Dict3' c (f4 'T4b)) => 'Dict4' c (f4 :: T4 -> k3 -> k2 -> k1 -> k0) where
+  'dict4' = \x -> case x of { ST4a -> 'dict3'; ST4b -> 'dict3' }
+@
+
+That is, assuming the following @T1@, @T2@, @T3@ and @T4@:
+
+@
+data T4 = T4a | T4b
+data T3 = T3a | T3b
+data T2 = T2a | T2b
+data T1 = T1a | T1b
+@
+
+Effectively, we wrote just one instance per singleton type per type-index
+position, each of them promoting a term-level representation of a singleton
+type to its type-level representation and forwarding the rest of the work to
+a “smaller” dict. That is, 'dict4' reifies the type of the fourth-to-last
+type-index of @X@ and then calls 'dict3' to do the same for the third-to-last
+type-index of @X@ and so on. Notice, however, how we didn't need to mention @X@
+in none of the instances above: As we said before, these instances are
+intended to work for any choice of @c@, @f4@, @f3@, @f2@ and @f1@.
+
+-}
+
+{- $recovering
+
+If you have a @'Some1' (f :: k -> *)@ and you know, statically, that you need an
+specific @f (a :: k)@, then you can use 'fromSome1' which will give you an
+@f (a :: k)@ only if @a@ was the type that was existentialized by 'Some1'.
+Using 'fromSome1' requires that the singleton type-index implements
+'Data.Singletons.Decide.SDecide', which can be derived mechanically with
+`TemplateHaskell` by means of 'Data.Singletons.TH.singInstance'.
+
+If you don't know, statically, the type of @f (a :: k)@, then you can use
+'withSome1Sing' or 'withSome1' to work with @f (a :: k)@ as long as @a@ never
+leaves their scope (don't worry, the compiler will yell at you if you try to do
+that).
+
+-}
+
+
+{- $prodsums
+
+Consider the following types and constructors:
+
+@
+data X (a :: 'Bool') where
+  XT :: X ''True'
+  XF :: X ''False'
+
+data Y (a :: 'Bool') where
+  YT :: Y ''True'
+  YF :: Y ''False'
+@
+
+You can use '(,)' to create a product for values of this type, and 'Either' to
+create a sum. However, see what happens if we try to existentialize the type
+index when using that approach:
+
+@
+> :t ('some1' XT, 'some1' YT)
+('some1' XT, 'some1' YT) :: ('Some1' X, 'Some1' Y)
+> :t ('some1' XT, 'some1' YF)
+('some1' XT, 'some1' YF) :: ('Some1' X, 'Some1' Y)
+@
+
+It works, but there is no type level guarantee that the type index taken by @X@
+and @Y@ is the same. If you do want to enforce that restriction, then you can
+use @P1@ instead:
+
+@
+> :t 'P1'
+'P1' :: l a -> r a -> 'P1' l r (a :: k)
+> :t 'P1' XT YT
+'P1' XT YT :: 'P1' X Y ''True'
+> :t 'P1' XT YT
+'P1' XT YT :: 'P1' X Y ''True'
+> :t 'some1' ('P1' XT YT)
+'some1' ('P1' XT YT) :: 'Some1' ('P1' X Y)
+@
+
+Trying to mix @XT@ with @YF@ fails, of course, since they have different type
+indexes:
+
+@
+> :t 'P1' XT YF
+\<interactive\>:1:7: error:
+    • Couldn't match type ‘''False'’ with ‘''True'’
+      Expected type: Y ''True'
+        Actual type: Y ''False'
+    • In the second argument of ‘'P1'’, namely ‘YF’
+      In the expression: 'P1' XT YF
+@
+
+Moreover, 'P1' supports many common instances from @base@, @hashable@,
+@deepseq@, @aeson@, @bytes@, @cereal@, @binary@ and @quickcheck@ out of the
+box, so you can benefit from them as well.
+
+There's also 'P2', 'P3' and 'P4' for product types taking a different number of
+indexes, and also 'S1', 'S2', 'S3' and 'S4' for sum types:
+
+@
+> :t 'S1L'
+'S1L' :: l a -> 'S1' l r (a :: k)
+> :t 'S1R'
+'S1R' :: r a -> 'S1' l r (a :: k)
+> :t 'S1L' XT
+'S1L' XT :: 'S1' X r ''True'
+> :t 'S1R' YT
+'S1R' YT :: 'S1' l Y ''True'
+> :t 'some1' ('S1L' XT)
+'some1' ('S1L' XT) :: 'Some1' ('S1' X r)
+> :t 'some1' ('S1R' YT)
+'some1' ('S1R' YT) :: 'Some1' ('S1' l Y)
+@
+
+-}
+
+
+{- $writingInstances
+
+Instances for 'Some1' seem to come out of thin air, but the truth is that they
+need to be written at least once by library authors so that, provided all its
+requirements are satisfied, they are made available.
+
+For example, when we imported "Exinst" before, we also brought to scope, among
+other things, the 'Eq' instance for 'Some1', which is defined as this:
+
+@
+instance forall (f :: k1 -> *).
+  ( 'Data.Singletons.Decide.SDecide' k1
+  , 'Dict1' 'Eq' f
+  ) => 'Eq' ('Some1' f)
+  where
+  (==) = \\som1x som1y ->
+     'withSome1Sing' som1x $ \\sa1x (x :: f a1x) ->
+        'withSome1Sing' som1y $ \\sa1y (y :: f a1y) ->
+           'maybe' 'False' 'id' $ do
+              'Data.Type.Equality.Refl' <- 'Data.Type.Equality.testEquality' sa1x sa1y
+              case 'dict1' sa1x :: 'Dict' ('Eq' (f a1x)) of
+                 'Dict' -> 'Just' (x == y)
+@
+
+This code should be relatively straightforward if you are familiar with uses of
+the @singletons@ and @constraints@ libraries. We are simply reifying singleton
+types from their term-level representation to their type-level representation,
+and afterwards using the 'Dict1' mechanism to lookup the required instances
+during runtime. Additionaly, this instance requires that the term level
+representation of the singleton type implements 'Show' too, as, like we saw in a
+previous example, the type index itself is shown in this 'Show' implementation,
+in the hope that it can be later recovered and reified to the type level when
+using 'Read'.
+
+-}
diff --git a/lib/Exinst/Binary.hs b/lib/Exinst/Binary.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/Binary.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'Bin.Binary' instances for 'Some1', 'Some2', 'Some3'
+-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2',
+-- 'Dict3' and 'Dict4' instances are available.
+--
+-- See the README file in the @exinst@ package for more general documentation:
+-- https://hackage.haskell.org/package/exinst#readme
+module Exinst.Binary () where
+
+import qualified Data.Binary as Bin
+import Data.Constraint
+import Data.Kind (Type)
+import Data.Singletons
+import Prelude
+
+import Exinst.Internal
+import Exinst.Internal.Sum
+import Exinst.Internal.Product
+
+--------------------------------------------------------------------------------
+
+-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
+-- fully applied @f@ instances are compatible as well.
+instance forall k1 (f :: k1 -> Type).
+  ( SingKind k1
+  , Bin.Binary (Demote k1)
+  , Dict1 Bin.Binary f
+  ) => Bin.Binary (Some1 f) where
+  {-# INLINABLE put #-}
+  put = \some1x ->
+    withSome1Sing some1x $ \sa1 (x :: f a1) ->
+      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of
+        Dict -> do
+          Bin.put (fromSing sa1)
+          Bin.put x
+  {-# INLINABLE get #-}
+  get = do
+    rsa1 <- Bin.get
+    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->
+      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of
+        Dict -> do
+          x :: f a1 <- Bin.get
+          pure (Some1 sa1 x)
+
+-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
+-- fully applied @f@ instances are compatible as well.
+instance forall k2 k1 (f :: k2 -> k1 -> Type).
+  ( SingKind k2
+  , SingKind k1
+  , Bin.Binary (Demote k2)
+  , Bin.Binary (Demote k1)
+  , Dict2 Bin.Binary f
+  ) => Bin.Binary (Some2 f) where
+  {-# INLINABLE put #-}
+  put = \some2x ->
+    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->
+      case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of
+        Dict -> do
+          Bin.put (fromSing sa2, fromSing sa1)
+          Bin.put x
+  {-# INLINABLE get #-}
+  get = do
+    (rsa2, rsa1) <- Bin.get
+    withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->
+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->
+        case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of
+          Dict -> do
+            x :: f a2 a1 <- Bin.get
+            pure (Some2 sa2 sa1 x)
+
+-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
+-- fully applied @f@ instances are compatible as well.
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type).
+  ( SingKind k3
+  , SingKind k2
+  , SingKind k1
+  , Bin.Binary (Demote k3)
+  , Bin.Binary (Demote k2)
+  , Bin.Binary (Demote k1)
+  , Dict3 Bin.Binary f
+  ) => Bin.Binary (Some3 f) where
+  {-# INLINABLE put #-}
+  put = \some3x ->
+    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->
+      case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of
+        Dict -> do
+          Bin.put (fromSing sa3, fromSing sa2, fromSing sa1)
+          Bin.put x
+  {-# INLINABLE get #-}
+  get = do
+    (rsa3, rsa2, rsa1) <- Bin.get
+    withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->
+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->
+        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->
+          case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of
+            Dict -> do
+              x :: f a3 a2 a1 <- Bin.get
+              pure (Some3 sa3 sa2 sa1 x)
+
+-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
+-- fully applied @f@ instances are compatible as well.
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type).
+  ( SingKind k4
+  , SingKind k3
+  , SingKind k2
+  , SingKind k1
+  , Bin.Binary (Demote k4)
+  , Bin.Binary (Demote k3)
+  , Bin.Binary (Demote k2)
+  , Bin.Binary (Demote k1)
+  , Dict4 Bin.Binary f
+  ) => Bin.Binary (Some4 f) where
+  {-# INLINABLE put #-}
+  put = \some4x ->
+    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->
+      case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of
+        Dict -> do
+          Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)
+          Bin.put x
+  {-# INLINABLE get #-}
+  get = do
+    (rsa4, rsa3, rsa2, rsa1) <- Bin.get
+    withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->
+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->
+        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->
+          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->
+            case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of
+              Dict -> do
+                x :: f a4 a3 a2 a1 <- Bin.get
+                pure (Some4 sa4 sa3 sa2 sa1 x)
+
+--------------------------------------------------------------------------------
+
+instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1)
+instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1)
+instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1)
+instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1)
+
+--------------------------------------------------------------------------------
+
+instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1)
+instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1)
+instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1)
+instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1)
diff --git a/lib/Exinst/DeepSeq.hs b/lib/Exinst/DeepSeq.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/DeepSeq.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and
+-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3'
+-- and 'Dict4' instances are available.
+--
+-- See the README file in the @exinst@ package for more general documentation:
+-- https://hackage.haskell.org/package/exinst#readme
+module Exinst.DeepSeq () where
+
+import Control.DeepSeq (NFData(rnf))
+import Data.Constraint
+import Data.Kind (Type)
+import Prelude
+
+import Exinst.Internal
+import Exinst.Internal.Sum
+import Exinst.Internal.Product
+
+--------------------------------------------------------------------------------
+
+instance forall k1 (f :: k1 -> Type).
+  ( Dict1 NFData f
+  ) => NFData (Some1 f) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some1x) ->
+    withSome1Sing some1x $ \ !sa1 !(x :: f a1) ->
+       case dict1 sa1 :: Dict (NFData (f a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall k2 k1 (f :: k2 -> k1 -> Type).
+  ( Dict2 NFData f
+  ) => NFData (Some2 f) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some2x) ->
+    withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type).
+  ( Dict3 NFData f
+  ) => NFData (Some3 f) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some3x) ->
+    withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type).
+  ( Dict4 NFData f
+  ) => NFData (Some4 f) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some4x) ->
+    withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of
+          Dict -> rnf x `seq` ()
+
+--------------------------------------------------------------------------------
+
+instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1)
+instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1)
+instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1)
+instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1)
+
+--------------------------------------------------------------------------------
+
+instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1)
+instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1)
+instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1)
+instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1)
+
diff --git a/lib/Exinst/Hashable.hs b/lib/Exinst/Hashable.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/Hashable.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and
+-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3'
+-- and 'Dict4' instances are available.
+--
+-- See the README file in the @exinst@ package for more general documentation:
+-- https://hackage.haskell.org/package/exinst#readme
+module Exinst.Hashable () where
+
+import Data.Hashable (Hashable(hashWithSalt))
+import Data.Constraint
+import Data.Kind (Type)
+import Data.Singletons
+import Prelude
+
+import Exinst.Internal
+import Exinst.Internal.Sum
+import Exinst.Internal.Product
+
+--------------------------------------------------------------------------------
+
+-- | Some salt we add to hashes calculated in this module.
+salt0 :: Int
+salt0 = 6700417
+
+--------------------------------------------------------------------------------
+
+instance forall k1 (f :: k1 -> Type)
+  . ( SingKind k1
+    , Hashable (Demote k1)
+    , Dict1 Hashable f
+    , Eq (Some1 f)
+    ) => Hashable (Some1 f)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) ->
+       case dict1 sa1 :: Dict (Hashable (f a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
+  . ( SingKind k2
+    , SingKind k1
+    , Hashable (Demote k2)
+    , Hashable (Demote k1)
+    , Dict2 Hashable f
+    , Eq (Some2 f)
+    ) => Hashable (Some2 f)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Hashable (Demote k3)
+    , Hashable (Demote k2)
+    , Hashable (Demote k1)
+    , Dict3 Hashable f
+    , Eq (Some3 f)
+    ) => Hashable (Some3 f)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa3
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Hashable (Demote k4)
+    , Hashable (Demote k3)
+    , Hashable (Demote k2)
+    , Hashable (Demote k1)
+    , Eq (Some4 f)
+    , Dict4 Hashable f
+    ) => Hashable (Some4 f)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa4
+                       `hashWithSalt` fromSing sa3
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+--------------------------------------------------------------------------------
+
+instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1)
+instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1)
+instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1)
+instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1)
+
+--------------------------------------------------------------------------------
+
+instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1)
+instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1)
+instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1)
+instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1)
+
diff --git a/lib/Exinst/Internal.hs b/lib/Exinst/Internal.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/Internal.hs
@@ -0,0 +1,446 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+
+
+module Exinst.Internal
+ ( -- * 1 type index
+   Some1(Some1)
+ , some1
+ , fromSome1
+ , _Some1
+ , withSome1
+ , withSome1Sing
+ , some1SingRep
+ , same1
+ , Dict1(dict1)
+
+   -- * 2 type indexes
+ , Some2(Some2)
+ , some2
+ , fromSome2
+ , _Some2
+ , withSome2
+ , withSome2Sing
+ , some2SingRep
+ , same2
+ , Dict2(dict2)
+
+   -- * 3 type indexes
+ , Some3(Some3)
+ , some3
+ , fromSome3
+ , _Some3
+ , withSome3
+ , withSome3Sing
+ , some3SingRep
+ , same3
+ , Dict3(dict3)
+
+   -- * 4 type indexes
+ , Some4(Some4)
+ , some4
+ , fromSome4
+ , _Some4
+ , withSome4
+ , withSome4Sing
+ , some4SingRep
+ , same4
+ , Dict4(dict4)
+
+   -- * Miscellaneous
+ , Dict0(dict0)
+ ) where
+
+import Data.Constraint
+import Data.Kind (Type)
+import Data.Profunctor (dimap, Choice(right'))
+import Data.Singletons
+import Data.Singletons.Decide
+import Prelude
+
+--------------------------------------------------------------------------------
+
+data Some1 (f1 :: k1 -> Type) = forall a1.
+  Some1 !(Sing a1) !(f1 a1)
+
+data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.
+  Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)
+
+data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.
+  Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)
+
+data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.
+  Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)
+
+--------------------------------------------------------------------------------
+
+some1
+  :: forall k1 (f1 :: k1 -> Type) a1
+  .  SingI a1
+  => f1 a1
+  -> Some1 f1 -- ^
+some1 = Some1 (sing :: Sing a1)
+{-# INLINE some1 #-}
+
+some2
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
+  .  (SingI a2, SingI a1)
+  => f2 a2 a1
+  -> Some2 f2 -- ^
+some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)
+{-# INLINE some2 #-}
+
+some3
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+  .  (SingI a3, SingI a2, SingI a1)
+  => f3 a3 a2 a1
+  -> Some3 f3 -- ^
+some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)
+{-# INLINE some3 #-}
+
+some4
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+  .  (SingI a4, SingI a3, SingI a2, SingI a1)
+  => f4 a4 a3 a2 a1
+  -> Some4 f4 -- ^
+some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)
+              (sing :: Sing a2) (sing :: Sing a1)
+{-# INLINE some4 #-}
+
+--------------------------------------------------------------------------------
+
+withSome1
+  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
+   . Some1 f1
+  -> (forall a1. SingI a1 => f1 a1 -> r)
+  -> r -- ^
+withSome1 s1 g = withSome1Sing s1 (\_ -> g)
+{-# INLINABLE withSome1 #-}
+
+withSome2
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
+  .  Some2 f2
+  -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
+  -> r -- ^
+withSome2 s2 g = withSome2Sing s2 (\_ _ -> g)
+{-# INLINABLE withSome2 #-}
+
+withSome3
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
+  .  Some3 f3
+  -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
+  -> r -- ^
+withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g)
+{-# INLINABLE withSome3 #-}
+
+withSome4
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
+  .  Some4 f4
+  -> (forall a4 a3 a2 a1
+        .  (SingI a4, SingI a3, SingI a2, SingI a1)
+        => f4 a4 a3 a2 a1 -> r)
+  -> r -- ^
+withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g)
+{-# INLINABLE withSome4 #-}
+
+--------------------------------------------------------------------------------
+
+-- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.
+withSome1Sing
+  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
+   . Some1 f1
+  -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
+  -> r -- ^
+withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x)
+{-# INLINABLE withSome1Sing #-}
+
+-- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.
+withSome2Sing
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
+  .  Some2 f2
+  -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
+  -> r -- ^
+withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x))
+{-# INLINABLE withSome2Sing #-}
+
+-- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.
+withSome3Sing
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
+  .  Some3 f3
+  -> (forall a3 a2 a1
+         .  (SingI a3, SingI a2, SingI a1)
+         => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
+  -> r -- ^
+withSome3Sing (Some3 sa3 sa2 sa1 x) g =
+  withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x)))
+{-# INLINABLE withSome3Sing #-}
+
+-- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.
+withSome4Sing
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
+  .  Some4 f4
+  -> (forall a4 a3 a2 a1
+        .  (SingI a4, SingI a3, SingI a2, SingI a1)
+        => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
+  -> r -- ^
+withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g =
+  withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1
+     (g sa4 sa3 sa2 sa1 x))))
+{-# INLINABLE withSome4Sing #-}
+
+--------------------------------------------------------------------------------
+
+fromSome1
+   :: forall k1 (f1 :: k1 -> Type) a1
+    . (SingI a1, SDecide k1)
+   => Some1 f1
+   -> Maybe (f1 a1) -- ^
+fromSome1 = \(Some1 sa1' x) -> do
+   Refl <- decideEquality sa1' (sing :: Sing a1)
+   return x
+{-# INLINABLE fromSome1 #-}
+
+fromSome2
+   :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
+    . ( SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
+   => Some2 f2
+   -> Maybe (f2 a2 a1) -- ^
+fromSome2 = \(Some2 sa2' sa1' x) -> do
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
+   return x
+{-# INLINABLE fromSome2 #-}
+
+fromSome3
+   :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+    . ( SingI a3, SDecide k3
+      , SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
+   => Some3 f3
+   -> Maybe (f3 a3 a2 a1) -- ^
+fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do
+   Refl <- decideEquality sa3' (sing :: Sing a3)
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
+   return x
+{-# INLINABLE fromSome3 #-}
+
+fromSome4
+   :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+    . ( SingI a4, SDecide k4
+      , SingI a3, SDecide k3
+      , SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
+   => Some4 f4
+   -> Maybe (f4 a4 a3 a2 a1) -- ^
+fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do
+   Refl <- decideEquality sa4' (sing :: Sing a4)
+   Refl <- decideEquality sa3' (sing :: Sing a3)
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
+   return x
+{-# INLINABLE fromSome4 #-}
+
+--------------------------------------------------------------------------------
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.
+_Some1
+  :: forall k1 (f1 :: k1 -> Type) a1
+  .  (SingI a1, SDecide k1)
+  => Prism' (Some1 f1) (f1 a1)
+_Some1 = prism' some1 fromSome1
+{-# INLINE _Some1 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.
+_Some2
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
+  .  ( SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some2 f2) (f2 a2 a1)
+_Some2 = prism' some2 fromSome2
+{-# INLINE _Some2 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.
+_Some3
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+  .  ( SingI a3, SDecide k3
+     , SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some3 f3) (f3 a3 a2 a1)
+_Some3 = prism' some3 fromSome3
+{-# INLINE _Some3 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.
+_Some4
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+  .  ( SingI a4, SDecide k4
+     , SingI a3, SDecide k3
+     , SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)
+_Some4 = prism' some4 fromSome4
+{-# INLINE _Some4 #-}
+
+--------------------------------------------------------------------------------
+
+some1SingRep
+  :: SingKind k1
+  => Some1 (f1 :: k1 -> Type)
+  -> Demote k1 -- ^
+some1SingRep = \(Some1 sa1 _) -> fromSing sa1
+{-# INLINE some1SingRep #-}
+
+some2SingRep
+  :: (SingKind k2, SingKind k1)
+  => Some2 (f2 :: k2 -> k1 -> Type)
+  -> (Demote k2, Demote k1) -- ^
+some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)
+{-# INLINE some2SingRep #-}
+
+some3SingRep
+  :: (SingKind k3, SingKind k2, SingKind k1)
+  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)
+  -> (Demote k3, Demote k2, Demote k1) -- ^
+some3SingRep = \(Some3 sa3 sa2 sa1 _) ->
+  (fromSing sa3, fromSing sa2, fromSing sa1)
+{-# INLINE some3SingRep #-}
+
+some4SingRep
+  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)
+  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
+  -> (Demote k4, Demote k3, Demote k2, Demote k1) -- ^
+some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->
+  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)
+{-# INLINE some4SingRep #-}
+
+--------------------------------------------------------------------------------
+
+-- | @'same1' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
+-- indexes are equal.
+--
+-- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@
+{-# INLINABLE same1 #-}
+same1
+  :: forall k1 f g x
+  .  SDecide k1
+  => (forall a1. SingI a1 => f a1 -> g a1 -> x)
+  -> Some1 (f :: k1 -> Type)
+  -> Some1 (g :: k1 -> Type)
+  -> Maybe x  -- ^
+same1 z = \s1f s1g ->
+  withSome1Sing s1f $ \sa1 f ->
+    withSome1Sing s1g $ \sa1' g -> do
+       Refl <- decideEquality sa1 sa1'
+       pure (z f g)
+
+-- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
+-- indexes are equal.
+--
+-- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@
+{-# INLINABLE same2 #-}
+same2
+  :: forall k2 k1 f g x
+  .  (SDecide k2, SDecide k1)
+  => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x)
+  -> Some2 (f :: k2 -> k1 -> Type)
+  -> Some2 (g :: k2 -> k1 -> Type)
+  -> Maybe x  -- ^
+same2 z = \s2l s2g ->
+  withSome2Sing s2l $ \sa2 sa1 f ->
+    withSome2Sing s2g $ \sa2' sa1' g -> do
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
+       pure (z f g)
+
+-- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
+-- indexes are equal.
+--
+-- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@
+{-# INLINABLE same3 #-}
+same3
+  :: forall k3 k2 k1 f g x
+  .  (SDecide k3, SDecide k2, SDecide k1)
+  => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1)
+        => f a3 a2 a1 -> g a3 a2 a1 -> x)
+  -> Some3 (f :: k3 -> k2 -> k1 -> Type)
+  -> Some3 (g :: k3 -> k2 -> k1 -> Type)
+  -> Maybe x  -- ^
+same3 z = \s3l s3g ->
+  withSome3Sing s3l $ \sa3 sa2 sa1 f ->
+    withSome3Sing s3g $ \sa3' sa2' sa1' g -> do
+       Refl <- decideEquality sa3 sa3'
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
+       pure (z f g)
+
+-- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
+-- indexes are equal.
+--
+-- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@
+{-# INLINABLE same4 #-}
+same4
+  :: forall k4 k3 k2 k1 f g x
+  .  (SDecide k4, SDecide k3, SDecide k2, SDecide k1)
+  => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1)
+        => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x)
+  -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)
+  -> Some4 (g :: k4 -> k3 -> k2 -> k1 -> Type)
+  -> Maybe x  -- ^
+same4 z = \s4l s4g ->
+  withSome4Sing s4l $ \sa4 sa3 sa2 sa1 f ->
+    withSome4Sing s4g $ \sa4' sa3' sa2' sa1' g -> do
+       Refl <- decideEquality sa4 sa4'
+       Refl <- decideEquality sa3 sa3'
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
+       pure (z f g)
+
+--------------------------------------------------------------------------------
+
+-- | 'Dict0' is a bit different from 'Dict1', 'Dict2', etc. in that it looks up
+-- an instance for the singleton type itself, and not for some other type
+-- indexed by said singleton type.
+class Dict0 (c :: k0 -> Constraint) where
+  -- | Runtime lookup of the @c a0@ instance.
+  dict0 :: Sing a0 -> Dict (c a0)
+
+class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where
+  -- | Runtime lookup of the @c (f1 a1)@ instance.
+  dict1 :: Sing a1 -> Dict (c (f1 a1))
+
+class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f2 a2 a1)@ instance.
+  dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
+
+class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.
+  dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
+
+class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.
+  dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
+
+--------------------------------------------------------------------------------
+-- Miscelaneous @lens@-compatible stuff.
+
+type Prism s t a b
+  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
+
+type Prism' s a = Prism s s a a
+
+prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
+prism bt seta = dimap seta (either pure (fmap bt)) . right'
+{-# INLINE prism #-}
+
+prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
+prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s))
+{-# INLINE prism' #-}
+
diff --git a/lib/Exinst/Internal/Product.hs b/lib/Exinst/Internal/Product.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/Internal/Product.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Exinst.Internal.Product
+ ( P1(P1)
+ , P2(P2)
+ , P3(P3)
+ , P4(P4)
+ ) where
+
+import GHC.Generics (Generic)
+
+--------------------------------------------------------------------------------
+-- Products
+
+-- | Like 'Data.Functor.Product.Product' from "Data.Functor.Product", but
+-- only intended to be used with kinds other than 'Type'.
+--
+-- This type is particularly useful when used in combination with 'Exinst.Some1'
+-- as @'Exinst.Some1' ('P1' l r)@, so as to ensure that @l@ and @r@ are indexed
+-- by the same type. Moreover, 'P1' already supports many common instances from
+-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and
+-- @quickcheck@ out of the box, so you can benefit from them as well.
+data P1 l r (a1 :: k1)
+  = P1 (l a1) (r a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'P1', but for @l@ and @r@ taking two type indexes.
+data P2 l r (a2 :: k2) (a1 :: k1)
+  = P2 (l a2 a1) (r a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'P1', but for @l@ and @r@ taking three type indexes.
+data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)
+  = P3 (l a3 a2 a1) (r a3 a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'P1', but for @l@ and @r@ taking four type indexes.
+data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)
+  = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
diff --git a/lib/Exinst/Internal/Sum.hs b/lib/Exinst/Internal/Sum.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/Internal/Sum.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Exinst.Internal.Sum
+ ( S1(S1L,S1R)
+ , S2(S2L,S2R)
+ , S3(S3L,S3R)
+ , S4(S4L,S4R)
+ ) where
+
+import GHC.Generics (Generic)
+
+--------------------------------------------------------------------------------
+-- Sums
+
+-- | Like 'Data.Functor.Sum.Sum' from "Data.Functor.Sum", but
+-- only intended to be used with kinds other than 'Type'.
+--
+-- This type is particularly useful when used in combination with 'Exinst.Some1'
+-- as @'Exinst.Some1' ('S1' l r)@, so as to ensure that @l@ and @r@ are indexed
+-- by the same type. Moreover, 'S1' already supports many common instances from
+-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and
+-- @quickcheck@ out of the box, so you can benefit from them as well.
+data S1 l r (a1 :: k1)
+  = S1L (l a1) | S1R (r a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'S1', but for @l@ and @r@ taking two type indexes.
+data S2 l r (a2 :: k2) (a1 :: k1)
+  = S2L (l a2 a1) | S2R (r a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'S1', but for @l@ and @r@ taking three type indexes.
+data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)
+  = S3L (l a3 a2 a1) | S3R (r a3 a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
+-- | Like 'S1', but for @l@ and @r@ taking four type indexes.
+data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)
+  = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1)
+  deriving (Eq, Show, Read, Ord, Generic)
+
diff --git a/lib/Exinst/QuickCheck.hs b/lib/Exinst/QuickCheck.hs
new file mode 100644
--- /dev/null
+++ b/lib/Exinst/QuickCheck.hs
@@ -0,0 +1,142 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2',
+-- 'Some3' and 'Some4' from "Exinst", provided situable 'Dict1',
+-- 'Dict2', 'Dict3' and 'Dict4' instances are available.
+--
+-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme
+module Exinst.QuickCheck () where
+
+import Data.Constraint
+import Data.Kind (Type)
+import Data.Singletons (SingKind, Sing, Demote, withSomeSing)
+import qualified Test.QuickCheck as QC
+
+import Exinst.Internal
+import Exinst.Internal.Sum
+import Exinst.Internal.Product
+
+--------------------------------------------------------------------------------
+
+instance
+  forall k1 (f :: k1 -> Type).
+  ( SingKind k1
+  , QC.Arbitrary (Demote k1)
+  , Dict1 QC.Arbitrary f
+  ) => QC.Arbitrary (Some1 f) where
+  arbitrary = do
+    da1 <- QC.arbitrary
+    withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+      case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of
+        Dict -> Some1 sa1 <$> QC.arbitrary
+  shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) ->
+    case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of
+      Dict -> Some1 sa1 <$> QC.shrink x
+
+instance
+  forall k2 k1 (f :: k2 -> k1 -> Type).
+  ( SingKind k2
+  , SingKind k1
+  , QC.Arbitrary (Demote k2)
+  , QC.Arbitrary (Demote k1)
+  , Dict2 QC.Arbitrary f
+  ) => QC.Arbitrary (Some2 f) where
+  arbitrary = do
+    da2 <- QC.arbitrary
+    da1 <- QC.arbitrary
+    withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->
+      withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+        case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of
+          Dict -> Some2 sa2 sa1 <$> QC.arbitrary
+  shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) ->
+    case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of
+      Dict -> Some2 sa2 sa1 <$> QC.shrink x
+
+instance
+  forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type).
+  ( SingKind k3
+  , SingKind k2
+  , SingKind k1
+  , QC.Arbitrary (Demote k3)
+  , QC.Arbitrary (Demote k2)
+  , QC.Arbitrary (Demote k1)
+  , Dict3 QC.Arbitrary f
+  ) => QC.Arbitrary (Some3 f) where
+  arbitrary = do
+    da3 <- QC.arbitrary
+    da2 <- QC.arbitrary
+    da1 <- QC.arbitrary
+    withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->
+      withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->
+        withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+          case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of
+            Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary
+  shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->
+    case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of
+      Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x
+
+instance
+  forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type).
+  ( SingKind k4
+  , SingKind k3
+  , SingKind k2
+  , SingKind k1
+  , QC.Arbitrary (Demote k4)
+  , QC.Arbitrary (Demote k3)
+  , QC.Arbitrary (Demote k2)
+  , QC.Arbitrary (Demote k1)
+  , Dict4 QC.Arbitrary f
+  ) => QC.Arbitrary (Some4 f) where
+  arbitrary = do
+    da4 <- QC.arbitrary
+    da3 <- QC.arbitrary
+    da2 <- QC.arbitrary
+    da1 <- QC.arbitrary
+    withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) ->
+      withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->
+        withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->
+          withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+            case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of
+              Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary
+  shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->
+    case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of
+      Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x
+
+--------------------------------------------------------------------------------
+
+instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where
+  arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ]
+  shrink (S1L l) = S1L <$> QC.shrink l
+  shrink (S1R r) = S1R <$> QC.shrink r
+instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where
+  arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ]
+  shrink (S2L l) = S2L <$> QC.shrink l
+  shrink (S2R r) = S2R <$> QC.shrink r
+instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where
+  arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ]
+  shrink (S3L l) = S3L <$> QC.shrink l
+  shrink (S3R r) = S3R <$> QC.shrink r
+instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where
+  arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ]
+  shrink (S4L l) = S4L <$> QC.shrink l
+  shrink (S4R r) = S4R <$> QC.shrink r
+
+--------------------------------------------------------------------------------
+
+instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where
+  arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary
+  shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y
+instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where
+  arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary
+  shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y
+instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where
+  arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary
+  shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y
+instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where
+  arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary
+  shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y
diff --git a/src/lib/Exinst/Instances/Base.hs b/src/lib/Exinst/Instances/Base.hs
deleted file mode 100644
--- a/src/lib/Exinst/Instances/Base.hs
+++ /dev/null
@@ -1,285 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
--- | This module exports 'Show', 'Eq' and 'Ord' instances for 'Exinst.Some1',
--- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst.Singletons", provided situable
--- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available.
---
--- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme
-module Exinst.Instances.Base () where
-
-import Data.Constraint
-import Data.Kind (Type)
-import Data.Singletons
-import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))
-import Data.Singletons.Decide
-import Data.Type.Equality
-import Exinst.Singletons
-  hiding (Some1(..), Some2(..), Some3(..), Some4(..))
-import qualified Exinst.Singletons as Exinst
-import Prelude
-
---------------------------------------------------------------------------------
-
--- Internal wrappers used to avoid writing the string manipulation in 'Show'
-data Some1'Show r1 x = Some1 r1 x deriving (Show)
-data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show)
-data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show)
-data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show)
-
---------------------------------------------------------------------------------
--- Show
-
-instance forall (f1 :: k1 -> Type)
-  . ( SingKind k1
-    , Show (DemoteRep k1)
-    , Dict1 Show f1
-    ) => Show (Exinst.Some1 f1)
-  where
-    {-# INLINABLE showsPrec #-}
-    showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->
-       case dict1 sa1 :: Dict (Show (f1 a1)) of
-          Dict -> showsPrec n (Some1 (fromSing sa1) x)
-
-instance forall (f2 :: k2 -> k1 -> Type)
-  . ( SingKind k2
-    , SingKind k1
-    , Show (DemoteRep k2)
-    , Show (DemoteRep k1)
-    , Dict2 Show f2
-    ) => Show (Exinst.Some2 f2)
-  where
-    {-# INLINABLE showsPrec #-}
-    showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->
-       case dict2 sa2 sa1 :: Dict (Show (f2 a2 a1)) of
-          Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)
-
-instance forall (f3 :: k3 -> k2 -> k1 -> Type)
-  . ( SingKind k3
-    , SingKind k2
-    , SingKind k1
-    , Show (DemoteRep k3)
-    , Show (DemoteRep k2)
-    , Show (DemoteRep k1)
-    , Dict3 Show f3
-    ) => Show (Exinst.Some3 f3)
-  where
-    {-# INLINABLE showsPrec #-}
-    showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->
-       case dict3 sa3 sa2 sa1 :: Dict (Show (f3 a3 a2 a1)) of
-          Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)
-
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
-  . ( SingKind k4
-    , SingKind k3
-    , SingKind k2
-    , SingKind k1
-    , Show (DemoteRep k4)
-    , Show (DemoteRep k3)
-    , Show (DemoteRep k2)
-    , Show (DemoteRep k1)
-    , Dict4 Show f4
-    ) => Show (Exinst.Some4 f4)
-  where
-    {-# INLINABLE showsPrec #-}
-    showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->
-       case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f4 a4 a3 a2 a1)) of
-          Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3)
-                                     (fromSing sa2) (fromSing sa1) x)
-
---------------------------------------------------------------------------------
--- Read
-
---------------------------------------------------------------------------------
--- Eq
-
-instance forall (f1 :: k1 -> Type)
-  . ( SDecide k1
-    , Dict1 Eq f1
-    ) => Eq (Exinst.Some1 f1)
-  where
-    {-# INLINABLE (==) #-}
-    (==) = \som1x som1y ->
-       withSome1Sing som1x $ \sa1x (x :: f1 a1x) ->
-          withSome1Sing som1y $ \sa1y (y :: f1 a1y) ->
-             maybe False id $ do
-                Refl <- testEquality sa1x sa1y
-                case dict1 sa1x :: Dict (Eq (f1 a1x)) of
-                   Dict -> Just (x == y)
-
-instance forall (f2 :: k2 -> k1 -> Type)
-  . ( SDecide k2
-    , SDecide k1
-    , Dict2 Eq f2
-    ) => Eq (Exinst.Some2 f2)
-  where
-    {-# INLINABLE (==) #-}
-    (==) = \som2x som2y ->
-       withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) ->
-          withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) ->
-             maybe False id $ do
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
-                case dict2 sa2x sa1x :: Dict (Eq (f2 a2x a1x)) of
-                   Dict -> Just (x == y)
-
-instance forall (f3 :: k3 -> k2 -> k1 -> Type)
-  . ( SDecide k3
-    , SDecide k2
-    , SDecide k1
-    , Dict3 Eq f3
-    ) => Eq (Exinst.Some3 f3)
-  where
-    {-# INLINABLE (==) #-}
-    (==) = \som3x som3y ->
-       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) ->
-          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) ->
-             maybe False id $ do
-                Refl <- testEquality sa3x sa3y
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
-                case dict3 sa3x sa2x sa1x :: Dict (Eq (f3 a3x a2x a1x)) of
-                   Dict -> Just (x == y)
-
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
-  . ( SDecide k4
-    , SDecide k3
-    , SDecide k2
-    , SDecide k1
-    , Dict4 Eq f4
-    ) => Eq (Exinst.Some4 f4)
-  where
-    {-# INLINABLE (==) #-}
-    (==) = \som4x som4y ->
-       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) ->
-          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) ->
-             maybe False id $ do
-                Refl <- testEquality sa4x sa4y
-                Refl <- testEquality sa3x sa3y
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
-                case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f4 a4x a3x a2x a1x)) of
-                   Dict -> Just (x == y)
-
---------------------------------------------------------------------------------
--- Ord
-
-instance forall (f1 :: k1 -> Type)
-  . ( SingKind k1
-    , SDecide k1
-    , Ord (DemoteRep k1)
-    , Dict1 Ord f1
-    , Eq (Exinst.Some1 f1)
-    ) => Ord (Exinst.Some1 f1)
-  where
-    {-# INLINABLE compare #-}
-    compare = \som1x som1y ->
-       withSome1Sing som1x $ \sa1x (x :: f1 a1x) ->
-          withSome1Sing som1y $ \sa1y (y :: f1 a1y) ->
-             let termCompare = compare (fromSing sa1x) (fromSing sa1y)
-             in maybe termCompare id $ do
-                  Refl <- testEquality sa1x sa1y
-                  case dict1 sa1x :: Dict (Ord (f1 a1x)) of
-                     Dict -> Just (compare x y)
-
-instance forall (f2 :: k2 -> k1 -> Type)
-  . ( SingKind k2
-    , SingKind k1
-    , SDecide k2
-    , SDecide k1
-    , Ord (DemoteRep k2)
-    , Ord (DemoteRep k1)
-    , Dict2 Ord f2
-    , Eq (Exinst.Some2 f2)
-    ) => Ord (Exinst.Some2 f2)
-  where
-    {-# INLINABLE compare #-}
-    compare = \som2x som2y ->
-       withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) ->
-          withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) ->
-             let termCompare = compare (fromSing sa2x, fromSing sa1x)
-                                       (fromSing sa2y, fromSing sa1y)
-             in maybe termCompare id $ do
-                   Refl <- testEquality sa2x sa2y
-                   Refl <- testEquality sa1x sa1y
-                   case dict2 sa2x sa1x :: Dict (Ord (f2 a2x a1x)) of
-                      Dict -> Just (compare x y)
-
-instance forall (f3 :: k3 -> k2 -> k1 -> Type)
-  . ( SingKind k3
-    , SingKind k2
-    , SingKind k1
-    , SDecide k3
-    , SDecide k2
-    , SDecide k1
-    , Ord (DemoteRep k3)
-    , Ord (DemoteRep k2)
-    , Ord (DemoteRep k1)
-    , Dict3 Ord f3
-    , Eq (Exinst.Some3 f3)
-    ) => Ord (Exinst.Some3 f3)
-  where
-    {-# INLINABLE compare #-}
-    compare = \som3x som3y ->
-       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) ->
-          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) ->
-             let termCompare = compare
-                   (fromSing sa3x, fromSing sa2x, fromSing sa1x)
-                   (fromSing sa3y, fromSing sa2y, fromSing sa1y)
-             in maybe termCompare id $ do
-                  Refl <- testEquality sa3x sa3y
-                  Refl <- testEquality sa2x sa2y
-                  Refl <- testEquality sa1x sa1y
-                  case dict3 sa3x sa2x sa1x :: Dict (Ord (f3 a3x a2x a1x)) of
-                     Dict -> Just (compare x y)
-
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
-  . ( SingKind k4
-    , SingKind k3
-    , SingKind k2
-    , SingKind k1
-    , SDecide k4
-    , SDecide k3
-    , SDecide k2
-    , SDecide k1
-    , Ord (DemoteRep k4)
-    , Ord (DemoteRep k3)
-    , Ord (DemoteRep k2)
-    , Ord (DemoteRep k1)
-    , Dict4 Ord f4
-    , Eq (Exinst.Some4 f4)
-    ) => Ord (Exinst.Some4 f4)
-  where
-    {-# INLINABLE compare #-}
-    compare = \som4x som4y ->
-       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) ->
-          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) ->
-             let termCompare = compare
-                   (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x)
-                   (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y)
-             in maybe termCompare id $ do
-                  Refl <- testEquality sa4x sa4y
-                  Refl <- testEquality sa3x sa3y
-                  Refl <- testEquality sa2x sa2y
-                  Refl <- testEquality sa1x sa1y
-                  case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f4 a4x a3x a2x a1x)) of
-                     Dict -> Just (compare x y)
-
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
--- Out of the box 'Dict1' instances for some @base@ types
-
-instance (c (f 'True), c (f 'False)) => Dict1 c (f :: Bool -> k0) where
-  dict1 = \case
-    STrue -> Dict
-    SFalse -> Dict
diff --git a/src/lib/Exinst/Singletons.hs b/src/lib/Exinst/Singletons.hs
deleted file mode 100644
--- a/src/lib/Exinst/Singletons.hs
+++ /dev/null
@@ -1,353 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
-
--- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme
-module Exinst.Singletons
- ( -- * 1 type index
-   Some1(Some1)
- , some1
- , fromSome1
- , _Some1
- , withSome1
- , withSome1Sing
- , some1SingRep
- , Dict1(dict1)
-
-   -- * 2 type indexes
- , Some2(Some2)
- , some2
- , fromSome2
- , _Some2
- , withSome2
- , withSome2Sing
- , some2SingRep
- , Dict2(dict2)
-
-   -- * 3 type indexes
- , Some3(Some3)
- , some3
- , fromSome3
- , _Some3
- , withSome3
- , withSome3Sing
- , some3SingRep
- , Dict3(dict3)
-
-   -- * 4 type indexes
- , Some4(Some4)
- , some4
- , fromSome4
- , _Some4
- , withSome4
- , withSome4Sing
- , some4SingRep
- , Dict4(dict4)
-
-   -- * Re-exports
- , Dict(Dict)
- ) where
-
-import Data.Constraint
-import Data.Kind (Type)
-import Data.Profunctor (dimap, Choice(right'))
-import Data.Singletons
-import Data.Singletons.Decide
-import Data.Type.Equality
-import Prelude
-
---------------------------------------------------------------------------------
-
-data Some1 (f1 :: k1 -> Type) = forall a1.
-  Some1 !(Sing a1) !(f1 a1)
-
-data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.
-  Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)
-
-data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.
-  Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)
-
-data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.
-  Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)
-
---------------------------------------------------------------------------------
-
-some1
-  :: forall (f1 :: k1 -> Type) a1
-  .  SingI a1
-  => f1 a1
-  -> Some1 f1 -- ^
-some1 = Some1 (sing :: Sing a1)
-{-# INLINE some1 #-}
-
-some2
-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
-  .  (SingI a2, SingI a1)
-  => f2 a2 a1
-  -> Some2 f2 -- ^
-some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)
-{-# INLINE some2 #-}
-
-some3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
-  .  (SingI a3, SingI a2, SingI a1)
-  => f3 a3 a2 a1
-  -> Some3 f3 -- ^
-some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)
-{-# INLINE some3 #-}
-
-some4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
-  .  (SingI a4, SingI a3, SingI a2, SingI a1)
-  => f4 a4 a3 a2 a1
-  -> Some4 f4 -- ^
-some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)
-              (sing :: Sing a2) (sing :: Sing a1)
-{-# INLINE some4 #-}
-
---------------------------------------------------------------------------------
-
-withSome1
-  :: forall (f1 :: k1 -> Type) (r :: Type)
-   . Some1 f1
-  -> (forall a1. SingI a1 => f1 a1 -> r)
-  -> r -- ^
-withSome1 s1 g = withSome1Sing s1 (\_ -> g)
-{-# INLINABLE withSome1 #-}
-
-withSome2
-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
-  .  Some2 f2
-  -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
-  -> r -- ^
-withSome2 s2 g = withSome2Sing s2 (\_ _ -> g)
-{-# INLINABLE withSome2 #-}
-
-withSome3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
-  .  Some3 f3
-  -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
-  -> r -- ^
-withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g)
-{-# INLINABLE withSome3 #-}
-
-withSome4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
-  .  Some4 f4
-  -> (forall a4 a3 a2 a1
-        .  (SingI a4, SingI a3, SingI a2, SingI a1)
-        => f4 a4 a3 a2 a1 -> r)
-  -> r -- ^
-withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g)
-{-# INLINABLE withSome4 #-}
-
---------------------------------------------------------------------------------
-
--- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.
-withSome1Sing
-  :: forall (f1 :: k1 -> Type) (r :: Type)
-   . Some1 f1
-  -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
-  -> r -- ^
-withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x)
-{-# INLINABLE withSome1Sing #-}
-
--- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.
-withSome2Sing
-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
-  .  Some2 f2
-  -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-  -> r -- ^
-withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x))
-{-# INLINABLE withSome2Sing #-}
-
--- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.
-withSome3Sing
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
-  .  Some3 f3
-  -> (forall a3 a2 a1
-         .  (SingI a3, SingI a2, SingI a1)
-         => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-  -> r -- ^
-withSome3Sing (Some3 sa3 sa2 sa1 x) g =
-  withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x)))
-{-# INLINABLE withSome3Sing #-}
-
--- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.
-withSome4Sing
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
-  .  Some4 f4
-  -> (forall a4 a3 a2 a1
-        .  (SingI a4, SingI a3, SingI a2, SingI a1)
-        => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-  -> r -- ^
-withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g =
-  withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1
-     (g sa4 sa3 sa2 sa1 x))))
-{-# INLINABLE withSome4Sing #-}
-
---------------------------------------------------------------------------------
-
-fromSome1
-   :: forall (f1 :: k1 -> Type) a1
-    . (SingI a1, SDecide k1)
-   => Some1 f1
-   -> Maybe (f1 a1) -- ^
-fromSome1 = \(Some1 sa1' x) -> do
-   Refl <- testEquality sa1' (sing :: Sing a1)
-   return x
-{-# INLINABLE fromSome1 #-}
-
-fromSome2
-   :: forall (f2 :: k2 -> k1 -> Type) a2 a1
-    . ( SingI a2, SDecide k2
-      , SingI a1, SDecide k1 )
-   => Some2 f2
-   -> Maybe (f2 a2 a1) -- ^
-fromSome2 = \(Some2 sa2' sa1' x) -> do
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
-   return x
-{-# INLINABLE fromSome2 #-}
-
-fromSome3
-   :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
-    . ( SingI a3, SDecide k3
-      , SingI a2, SDecide k2
-      , SingI a1, SDecide k1 )
-   => Some3 f3
-   -> Maybe (f3 a3 a2 a1) -- ^
-fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do
-   Refl <- testEquality sa3' (sing :: Sing a3)
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
-   return x
-{-# INLINABLE fromSome3 #-}
-
-fromSome4
-   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
-    . ( SingI a4, SDecide k4
-      , SingI a3, SDecide k3
-      , SingI a2, SDecide k2
-      , SingI a1, SDecide k1 )
-   => Some4 f4
-   -> Maybe (f4 a4 a3 a2 a1) -- ^
-fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do
-   Refl <- testEquality sa4' (sing :: Sing a4)
-   Refl <- testEquality sa3' (sing :: Sing a3)
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
-   return x
-{-# INLINABLE fromSome4 #-}
-
---------------------------------------------------------------------------------
-
--- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.
-_Some1
-  :: forall (f1 :: k1 -> Type) a1
-  .  (SingI a1, SDecide k1)
-  => Prism' (Some1 f1) (f1 a1)
-_Some1 = prism' some1 fromSome1
-{-# INLINE _Some1 #-}
-
--- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.
-_Some2
-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
-  .  ( SingI a2, SDecide k2
-     , SingI a1, SDecide k1 )
-  => Prism' (Some2 f2) (f2 a2 a1)
-_Some2 = prism' some2 fromSome2
-{-# INLINE _Some2 #-}
-
--- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.
-_Some3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
-  .  ( SingI a3, SDecide k3
-     , SingI a2, SDecide k2
-     , SingI a1, SDecide k1 )
-  => Prism' (Some3 f3) (f3 a3 a2 a1)
-_Some3 = prism' some3 fromSome3
-{-# INLINE _Some3 #-}
-
--- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.
-_Some4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
-  .  ( SingI a4, SDecide k4
-     , SingI a3, SDecide k3
-     , SingI a2, SDecide k2
-     , SingI a1, SDecide k1 )
-  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)
-_Some4 = prism' some4 fromSome4
-{-# INLINE _Some4 #-}
-
---------------------------------------------------------------------------------
-
-some1SingRep
-  :: SingKind k1
-  => Some1 (f1 :: k1 -> Type)
-  -> DemoteRep k1 -- ^
-some1SingRep = \(Some1 sa1 _) -> fromSing sa1
-{-# INLINE some1SingRep #-}
-
-some2SingRep
-  :: (SingKind k2, SingKind k1)
-  => Some2 (f2 :: k2 -> k1 -> Type)
-  -> (DemoteRep k2, DemoteRep k1) -- ^
-some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)
-{-# INLINE some2SingRep #-}
-
-some3SingRep
-  :: (SingKind k3, SingKind k2, SingKind k1)
-  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)
-  -> (DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^
-some3SingRep = \(Some3 sa3 sa2 sa1 _) ->
-  (fromSing sa3, fromSing sa2, fromSing sa1)
-{-# INLINE some3SingRep #-}
-
-some4SingRep
-  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)
-  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
-  -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^
-some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->
-  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)
-{-# INLINE some4SingRep #-}
-
---------------------------------------------------------------------------------
-
-class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where
-  -- | Runtime lookup of the @c (f1 a1)@ instance.
-  dict1 :: Sing a1 -> Dict (c (f1 a1))
-
-class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where
-  -- Runtime lookup of the @c (f2 a2 a1)@ instance.
-  dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
-
-class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where
-  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.
-  dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
-
-class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where
-  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.
-  dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
-
---------------------------------------------------------------------------------
--- Miscelaneous @lens@-compatible stuff.
-
-type Prism s t a b
-  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
-
-type Prism' s a = Prism s s a a
-
-prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
-prism bt seta = dimap seta (either pure (fmap bt)) . right'
-{-# INLINE prism #-}
-
-prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
-prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s))
-{-# INLINE prism' #-}