diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,54 @@
+# 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-2017, Renzo Carbonara
 
 All rights reserved.
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
 # exinst
 
+[![Build Status](https://travis-ci.org/k0001/exinst.svg?branch=master)](https://travis-ci.org/k0001/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.
 
@@ -50,7 +52,7 @@
 `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`. 
+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
@@ -182,7 +184,7 @@
 Note: this code won't work yet. Keep reading.
 
 ```
-> import Exinst.Singletons (some1)
+> import Exinst (some1)
 > import Exinst.Instances.Base ()
 > :t some1 Glass
 :t some1 Glass :: Some1 Receptacle
@@ -218,7 +220,7 @@
 type.
 
 ```haskell
--- The Exinst.Singletons.Dict1 class
+-- The Exinst.Dict1 class
 class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) where
   dict1 :: Sing (a1 :: k1) -> Dict (c (f1 a1))
 ```
@@ -282,25 +284,21 @@
 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:
+The `Exinst` module exports ready-made instances for `Some1`, `Some2`, `Some3`
+and `Some4` (they can be enabled with some cabal flags).
 
-* Package `exinst`, module `Exinst.Instances.Base`: Instances for various
-  type-classes found in the `base` package: `Eq`, `Ord`, `Show`.
+* `Eq`, `Ord`, `Show` from the `base` package.
 
-* Package `exinst-aeson`, module `Exinst.Instances.Aeson`: Instances for
-  `FromJSON` and `ToJSON` from the `aeson` package.
+* `FromJSON` and `ToJSON` from the `aeson` package.
 
-* Package `exinst-bytes`, module `Exinst.Instances.Bytes`: Instances for
-  `Serial` from the `bytes` package.
+* `Serial` from the `bytes` package.
 
-* Package `exinst-hashable`, module `Exinst.Instances.Hashable`: Instances for
-  `Hashable` from the `hashable` package.
+* `Hashable` from the `hashable` package.
 
-* Package `exinst-deepseq`, module `Exinst.Instances.DeepSeq`: Instances for
-  `NFData` from the `deepseq` package.
+* `NFData` from the `deepseq` package.
 
+* `Arbitrary` from the `QuickCheck` 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
@@ -309,10 +307,6 @@
 (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`:
 
@@ -332,7 +326,7 @@
 import qualified Data.Aeson as Ae
 import           Data.Constraint (Dict(Dict))
 import qualified Data.Singletons.TH
-import           Exinst.Singletons (Dict1(dict1))
+import           Exinst (Dict1(dict1))
 
 -----
 
@@ -536,30 +530,3 @@
 using `Read`.
 
 
-# Related work on Generic instances for GADTs
-
-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).
-
-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/exinst.cabal b/exinst.cabal
--- a/exinst.cabal
+++ b/exinst.cabal
@@ -1,8 +1,8 @@
 name:                exinst
-version:             0.2
+version:             0.3
 author:              Renzo Carbonara
 maintainer:          renzoλcarbonara.com.ar
-copyright:           Renzo Carbonara 2015-2016
+copyright:           Renzo Carbonara 2015-2017
 license:             BSD3
 license-file:        LICENSE.txt
 extra-source-files:  README.md CHANGELOG.md
@@ -18,12 +18,74 @@
   hs-source-dirs: src/lib
   default-language: Haskell2010
   exposed-modules:
-      Exinst.Singletons
+      Exinst
+  other-modules:
+      Exinst.Internal
       Exinst.Instances.Base
   build-depends:
       base >=4.9 && <5.0
-    , constraints >=0.4 && <0.9
-    , profunctors >=5.0 && <6.0
-    , singletons >=2.2 && <2.3
+    , constraints >=0.4
+    , profunctors >=5.0
+    , singletons >=2.2
   ghcjs-options: -Wall -O3
   ghc-options: -Wall -O2
+
+  if flag(aeson)
+    build-depends: aeson
+    other-modules: Exinst.Instances.Aeson
+  if flag(bytes)
+    build-depends: bytes >=0.15 && <0.16
+    other-modules: Exinst.Instances.Bytes
+  if flag(deepseq)
+    build-depends: deepseq
+    other-modules: Exinst.Instances.DeepSeq
+  if flag(hashable)
+    build-depends: hashable
+    other-modules: Exinst.Instances.Hashable
+  if flag(quickcheck)
+    build-depends: QuickCheck
+    other-modules: Exinst.Instances.QuickCheck
+
+
+test-suite tests
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+  hs-source-dirs: tests
+  main-is: Main.hs
+  build-depends:
+     aeson
+   , base
+   , bytes
+   , constraints
+   , deepseq
+   , exinst
+   , generic-random >=0.4
+   , hashable
+   , profunctors
+   , QuickCheck
+   , singletons
+   , tasty
+   , tasty-hunit
+   , tasty-quickcheck
+
+
+flag aeson
+  description: Provide instances for @aeson@
+  default: True
+  manual: True
+flag bytes
+  description: Provide instances for @bytes@
+  default: True
+  manual: True
+flag deepseq
+  description: Provide instances for @deepseq@
+  default: True
+  manual: True
+flag hashable
+  description: Provide instances for @hashable@
+  default: True
+  manual: True
+flag quickcheck
+  description: Provide instances for @QuickCheck@
+  default: True
+  manual: True
diff --git a/src/lib/Exinst.hs b/src/lib/Exinst.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE CPP #-}
+
+-- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme
+module Exinst
+ ( -- * 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)
+
+   -- * Miscellaneous
+ , Dict0(dict0)
+
+   -- * Re-exports
+ , Constraint
+ , Dict(Dict)
+ ) where
+
+import Data.Constraint (Constraint, Dict(Dict))
+
+import Exinst.Internal
+
+#ifdef VERSION_aeson
+import Exinst.Instances.Aeson ()
+#endif
+
+#ifdef VERSION_bytes
+import Exinst.Instances.Bytes ()
+#endif
+
+#ifdef VERSION_bytes
+import Exinst.Instances.Base ()
+#endif
+
+#ifdef VERSION_bytes
+import Exinst.Instances.DeepSeq ()
+#endif
+
+#ifdef VERSION_bytes
+import Exinst.Instances.Hashable ()
+#endif
+
+#ifdef VERSION_QuickCheck
+import Exinst.Instances.QuickCheck ()
+#endif
diff --git a/src/lib/Exinst/Instances/Aeson.hs b/src/lib/Exinst/Instances/Aeson.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Instances/Aeson.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'Ae.FromJSON' and 'Ae.ToJSON' 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.Instances.Aeson () where
+
+import qualified Data.Aeson as Ae
+import Data.Constraint
+import Data.Singletons
+import Prelude
+
+import Exinst.Internal
+
+--------------------------------------------------------------------------------
+
+instance forall (f1 :: k1 -> *)
+  . ( SingKind k1
+    , Ae.ToJSON (DemoteRep k1)
+    , Dict1 Ae.ToJSON f1
+    ) => Ae.ToJSON (Some1 f1)
+  where
+    {-# INLINABLE toJSON #-}
+    toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->
+       case dict1 sa1 :: Dict (Ae.ToJSON (f1 a1)) of
+          Dict -> Ae.toJSON (fromSing sa1, x)
+
+instance forall (f2 :: k2 -> k1 -> *)
+  . ( SingKind k2
+    , SingKind k1
+    , Ae.ToJSON (DemoteRep k2)
+    , Ae.ToJSON (DemoteRep k1)
+    , Dict2 Ae.ToJSON f2
+    ) => Ae.ToJSON (Some2 f2)
+  where
+    {-# INLINABLE toJSON #-}
+    toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f2 a2 a1)) of
+          Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x)
+
+instance forall (f3 :: k3 -> k2 -> k1 -> *)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Ae.ToJSON (DemoteRep k3)
+    , Ae.ToJSON (DemoteRep k2)
+    , Ae.ToJSON (DemoteRep k1)
+    , Dict3 Ae.ToJSON f3
+    ) => Ae.ToJSON (Some3 f3)
+  where
+    {-# INLINABLE toJSON #-}
+    toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f3 a3 a2 a1)) of
+          Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x)
+
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Ae.ToJSON (DemoteRep k4)
+    , Ae.ToJSON (DemoteRep k3)
+    , Ae.ToJSON (DemoteRep k2)
+    , Ae.ToJSON (DemoteRep k1)
+    , Dict4 Ae.ToJSON f4
+    ) => Ae.ToJSON (Some4 f4)
+  where
+    {-# INLINABLE toJSON #-}
+    toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f4 a4 a3 a2 a1)) of
+          Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x)
+
+--------------------------------------------------------------------------------
+
+instance forall (f1 :: k1 -> *)
+  . ( SingKind k1
+    , Ae.FromJSON (DemoteRep k1)
+    , Dict1 Ae.FromJSON f1
+    ) => Ae.FromJSON (Some1 f1)
+  where
+    {-# INLINABLE parseJSON #-}
+    parseJSON = \v -> do
+      (rsa1, v') <- Ae.parseJSON v
+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+         case dict1 sa1 :: Dict (Ae.FromJSON (f1 a1)) of
+            Dict -> do
+               x :: f1 a1 <- Ae.parseJSON v'
+               return (some1 x)
+
+instance forall (f2 :: k2 -> k1 -> *)
+  . ( SingKind k2
+    , SingKind k1
+    , Ae.FromJSON (DemoteRep k2)
+    , Ae.FromJSON (DemoteRep k1)
+    , Dict2 Ae.FromJSON f2
+    ) => Ae.FromJSON (Some2 f2)
+  where
+    {-# INLINABLE parseJSON #-}
+    parseJSON = \v -> do
+      ((rsa2, rsa1), v') <- Ae.parseJSON v
+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+            case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f2 a2 a1)) of
+               Dict -> do
+                  x :: f2 a2 a1 <- Ae.parseJSON v'
+                  return (some2 x)
+
+instance forall (f3 :: k3 -> k2 -> k1 -> *)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Ae.FromJSON (DemoteRep k3)
+    , Ae.FromJSON (DemoteRep k2)
+    , Ae.FromJSON (DemoteRep k1)
+    , Dict3 Ae.FromJSON f3
+    ) => Ae.FromJSON (Some3 f3)
+  where
+    {-# INLINABLE parseJSON #-}
+    parseJSON = \v -> do
+      ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v
+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $
+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+               case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f3 a3 a2 a1)) of
+                  Dict -> do
+                     x :: f3 a3 a2 a1 <- Ae.parseJSON v'
+                     return (some3 x)
+
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Ae.FromJSON (DemoteRep k4)
+    , Ae.FromJSON (DemoteRep k3)
+    , Ae.FromJSON (DemoteRep k2)
+    , Ae.FromJSON (DemoteRep k1)
+    , Dict4 Ae.FromJSON f4
+    ) => Ae.FromJSON (Some4 f4)
+  where
+    {-# INLINABLE parseJSON #-}
+    parseJSON = \v -> do
+      ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v
+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> withSingI sa4 $
+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $
+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f4 a4 a3 a2 a1)) of
+                     Dict -> do
+                        x :: f4 a4 a3 a2 a1 <- Ae.parseJSON v'
+                        return (some4 x)
diff --git a/src/lib/Exinst/Instances/Base.hs b/src/lib/Exinst/Instances/Base.hs
--- a/src/lib/Exinst/Instances/Base.hs
+++ b/src/lib/Exinst/Instances/Base.hs
@@ -6,13 +6,14 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# 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
+-- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.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
@@ -21,14 +22,19 @@
 import Data.Constraint
 import Data.Kind (Type)
 import Data.Singletons
+import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound))
 import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))
+import qualified Data.Singletons.Prelude.List as List
+import Data.Singletons.Prelude.Tuple (Tuple2Sym1)
 import Data.Singletons.Decide
 import Data.Type.Equality
-import Exinst.Singletons
-  hiding (Some1(..), Some2(..), Some3(..), Some4(..))
-import qualified Exinst.Singletons as Exinst
+import qualified GHC.Generics as G
 import Prelude
 
+import Exinst.Internal
+  hiding (Some1(..), Some2(..), Some3(..), Some4(..))
+import qualified Exinst.Internal as Exinst
+
 --------------------------------------------------------------------------------
 
 -- Internal wrappers used to avoid writing the string manipulation in 'Show'
@@ -276,10 +282,254 @@
                      Dict -> Just (compare x y)
 
 --------------------------------------------------------------------------------
+-- Generic
+
+type Eithers1 (f :: k1 -> Type) =
+  Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f
+
+-- | TODO: Mak1e this logarithmic.
+type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where
+  Eithers1' (x ': '[]) f = f x
+  Eithers1' (x ': xs)  f = Either (f x) (Eithers1' xs f)
+
+instance forall k1 (f :: k1 -> Type)
+  . ( SingKind k1
+    , PEnum ('Proxy :: Proxy k1)
+    , PBounded ('Proxy :: Proxy k1)
+    , G.Generic (DemoteRep k1)
+    , Dict1 G.Generic f
+    , Dict1 (Inj (Eithers1 f)) f
+    ) => G.Generic (Exinst.Some1 f)
+  where
+    type Rep (Exinst.Some1 (f :: k1 -> Type)) =
+      G.Rep (DemoteRep k1, Eithers1 f)
+    {-# INLINABLE from #-}
+    from = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) ->
+      case dict1 sa1 :: Dict (G.Generic (f a1)) of
+        Dict -> case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of
+          Dict -> G.from (fromSing sa1, inj x)
+    {-# INLINABLE to #-}
+    to = \(G.M1 (G.M1 (G.M1 (G.K1 da1) G.:*: G.M1 (G.K1 ex)))) ->
+      withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+        case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of
+          Dict -> case prj ex of
+            Just x -> Exinst.Some1 sa1 (x :: f a1)
+            Nothing -> error "Generic Some1: Malformed Rep"
+
+---
+type Eithers2 (f :: k2 -> k1 -> Type) =
+  Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f
+
+-- | TODO: Mak1e this logarithmic.
+type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where
+  Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1
+  Eithers2' ( '(x2, x1) ': xs)  f = Either (f x2 x1) (Eithers2' xs f)
+
+type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where
+  Cartesian2 '[] xs1 = '[]
+  Cartesian2 (x2 ': xs2) xs1 =
+    List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1]
+
+
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
+  . ( SingKind k2
+    , SingKind k1
+    , PEnum ('Proxy :: Proxy k2)
+    , PEnum ('Proxy :: Proxy k1)
+    , PBounded ('Proxy :: Proxy k2)
+    , PBounded ('Proxy :: Proxy k1)
+    , G.Generic (DemoteRep k2)
+    , G.Generic (DemoteRep k1)
+    , Dict2 G.Generic f
+    , Dict2 (Inj (Eithers2 f)) f
+    ) => G.Generic (Exinst.Some2 f)
+  where
+    type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) =
+      G.Rep ((DemoteRep k2, DemoteRep k1), Eithers2 f)
+    {-# INLINABLE from #-}
+    from = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) ->
+      case dict2 sa2 sa1 :: Dict (G.Generic (f a2 a1)) of
+        Dict -> case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of
+          Dict -> G.from ((fromSing sa2, fromSing sa1), inj x)
+    {-# INLINABLE to #-}
+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->
+      withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->
+        withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+          case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of
+            Dict -> case prj ex of
+              Just x -> Exinst.Some2 sa2 sa1 (x :: f a2 a1)
+              Nothing -> error "Generic Some2: Malformed Rep"
+
+
+---
+type Eithers3 (f :: k3 -> k2 -> k1 -> Type) =
+  Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3))
+                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f
+
+-- | TODO: Mak1e this logarithmic.
+type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where
+  Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1
+  Eithers3' ( '(x3, '(x2, x1)) ': xs)  f = Either (f x3 x2 x1) (Eithers3' xs f)
+
+-- | We use nested 2-tuples instead of 3-tuples because it's easier to implement.
+type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where
+  Cartesian3 '[] xs2 xs1 = '[]
+  Cartesian3 (x3 ': xs3) xs2 xs1 =
+    List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1)
+                , Cartesian3 xs3 xs2 xs1 ]
+
+
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , PEnum ('Proxy :: Proxy k3)
+    , PEnum ('Proxy :: Proxy k2)
+    , PEnum ('Proxy :: Proxy k1)
+    , PBounded ('Proxy :: Proxy k3)
+    , PBounded ('Proxy :: Proxy k2)
+    , PBounded ('Proxy :: Proxy k1)
+    , G.Generic (DemoteRep k3)
+    , G.Generic (DemoteRep k2)
+    , G.Generic (DemoteRep k1)
+    , Dict3 G.Generic f
+    , Dict3 (Inj (Eithers3 f)) f
+    ) => G.Generic (Exinst.Some3 f)
+  where
+    type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) =
+      G.Rep ((DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers3 f)
+    {-# INLINABLE from #-}
+    from = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->
+      case dict3 sa3 sa2 sa1 :: Dict (G.Generic (f a3 a2 a1)) of
+        Dict -> case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of
+          Dict -> G.from ((fromSing sa3, fromSing sa2, fromSing sa1), inj x)
+    {-# INLINABLE to #-}
+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->
+      withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->
+        withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->
+          withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->
+            case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of
+              Dict -> case prj ex of
+                Just x -> Exinst.Some3 sa3 sa2 sa1 (x :: f a3 a2 a1)
+                Nothing -> error "Generic Some3: Malformed Rep"
+
+
+---
+type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) =
+  Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4))
+                        (EnumFromTo (MinBound :: k3) (MaxBound :: k3))
+                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f
+
+-- | TODO: Mak1e this logarithmic.
+type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where
+  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1
+  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs)  f = Either (f x4 x3 x2 x1) (Eithers4' xs f)
+
+-- | We use nested 2-tuples instead of 4-tuples because it's easier to implement.
+type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where
+  Cartesian4 '[] xs3 xs2 xs1 = '[]
+  Cartesian4 (x4 ': xs4) xs3 xs2 xs1 =
+    List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1)
+                , Cartesian4 xs4 xs3 xs2 xs1 ]
+
+
+instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , PEnum ('Proxy :: Proxy k4)
+    , PEnum ('Proxy :: Proxy k3)
+    , PEnum ('Proxy :: Proxy k2)
+    , PEnum ('Proxy :: Proxy k1)
+    , PBounded ('Proxy :: Proxy k4)
+    , PBounded ('Proxy :: Proxy k3)
+    , PBounded ('Proxy :: Proxy k2)
+    , PBounded ('Proxy :: Proxy k1)
+    , G.Generic (DemoteRep k4)
+    , G.Generic (DemoteRep k3)
+    , G.Generic (DemoteRep k2)
+    , G.Generic (DemoteRep k1)
+    , Dict4 G.Generic f
+    , Dict4 (Inj (Eithers4 f)) f
+    ) => G.Generic (Exinst.Some4 f)
+  where
+    type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) =
+      G.Rep ((DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers4 f)
+    {-# INLINABLE from #-}
+    from = \s4x -> withSome4Sing s4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->
+      case dict4 sa4 sa3 sa2 sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of
+        Dict -> case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of
+          Dict -> G.from ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), inj x)
+    {-# INLINABLE to #-}
+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da4, da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->
+      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 (Inj (Eithers4 f) (f a4 a3 a2 a1)) of
+                Dict -> case prj ex of
+                  Just x -> Exinst.Some4 sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1)
+                  Nothing -> error "Generic Some4: Malformed Rep"
+
 --------------------------------------------------------------------------------
--- Out of the box 'Dict1' instances for some @base@ types
+--------------------------------------------------------------------------------
+-- Out of the box 'DictX' instances for some @base@ types
 
-instance (c (f 'True), c (f 'False)) => Dict1 c (f :: Bool -> k0) where
-  dict1 = \case
-    STrue -> Dict
-    SFalse -> Dict
+instance
+  (c 'False, c 'True
+  ) => Dict0 (c :: Bool -> Constraint) where
+  {-# INLINABLE dict0 #-}
+  dict0 = \case { SFalse -> Dict; STrue -> Dict }
+
+instance
+  ( c (f 'False), c (f 'True)
+  ) => Dict1 c (f :: Bool -> k0) where
+  {-# INLINABLE dict1 #-}
+  dict1 = \case { SFalse -> Dict; STrue -> Dict }
+
+instance
+  ( Dict1 c (f 'False), Dict1 c (f 'True)
+  ) => Dict2 c (f :: Bool -> k1 -> k0) where
+  {-# INLINABLE dict2 #-}
+  dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 }
+
+instance
+  ( Dict2 c (f 'False), Dict2 c (f 'True)
+  ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where
+  {-# INLINABLE dict3 #-}
+  dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 }
+
+instance
+  ( Dict3 c (f 'False), Dict3 c (f 'True)
+  ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where
+  {-# INLINABLE dict4 #-}
+  dict4 = \x -> case x of { SFalse -> dict3; STrue -> dict3 }
+
+--------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+-- Misc
+
+class Inj b a where
+  inj :: a -> b
+  prj :: b -> Maybe a
+instance Inj a a where
+  {-# INLINE inj #-}
+  inj = id
+  {-# INLINE prj #-}
+  prj = Just
+instance Inj (Either a b) a where
+  {-# INLINE inj #-}
+  inj = Left
+  {-# INLINE prj #-}
+  prj = either Just (const Nothing)
+-- | TODO: Make this logarithmic.
+instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where
+  {-# INLINE inj #-}
+  inj = Right . inj
+  {-# INLINE prj #-}
+  prj = either (const Nothing) prj
+
diff --git a/src/lib/Exinst/Instances/Bytes.hs b/src/lib/Exinst/Instances/Bytes.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Instances/Bytes.hs
@@ -0,0 +1,118 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | This module exports 'By.Serial' 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.Instances.Bytes () where
+
+import qualified Data.Bytes.Serial as By
+import Data.Constraint
+import Data.Singletons
+import Prelude
+
+import Exinst.Internal
+
+--------------------------------------------------------------------------------
+
+instance forall (f1 :: k1 -> *)
+  . ( SingKind k1
+    , By.Serial (DemoteRep k1)
+    , Dict1 By.Serial f1
+    ) => By.Serial (Some1 f1)
+  where
+    {-# INLINABLE serialize #-}
+    serialize = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->
+       case dict1 sa1 :: Dict (By.Serial (f1 a1)) of
+          Dict -> do By.serialize (fromSing sa1)
+                     By.serialize x
+    {-# INLINABLE deserialize #-}
+    deserialize = do
+      rsa1 <- By.deserialize
+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+         case dict1 sa1 :: Dict (By.Serial (f1 a1)) of
+            Dict -> do x :: f1 a1 <- By.deserialize
+                       return (some1 x)
+
+instance forall (f2 :: k2 -> k1 -> *)
+  . ( SingKind k2
+    , SingKind k1
+    , By.Serial (DemoteRep k2)
+    , By.Serial (DemoteRep k1)
+    , Dict2 By.Serial f2
+    ) => By.Serial (Some2 f2)
+  where
+    {-# INLINABLE serialize #-}
+    serialize = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (By.Serial (f2 a2 a1)) of
+          Dict -> do By.serialize (fromSing sa2, fromSing sa1)
+                     By.serialize x
+    {-# INLINABLE deserialize #-}
+    deserialize = do
+      (rsa2, rsa1) <- By.deserialize
+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+            case dict2 sa2 sa1 :: Dict (By.Serial (f2 a2 a1)) of
+               Dict -> do x :: f2 a2 a1 <- By.deserialize
+                          return (some2 x)
+
+instance forall (f3 :: k3 -> k2 -> k1 -> *)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , By.Serial (DemoteRep k3)
+    , By.Serial (DemoteRep k2)
+    , By.Serial (DemoteRep k1)
+    , Dict3 By.Serial f3
+    ) => By.Serial (Some3 f3)
+  where
+    {-# INLINABLE serialize #-}
+    serialize = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 a3 a2 a1)) of
+          Dict -> do By.serialize (fromSing sa3, fromSing sa2, fromSing sa1)
+                     By.serialize x
+    {-# INLINABLE deserialize #-}
+    deserialize = do
+      (rsa3, rsa2, rsa1) <- By.deserialize
+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $
+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+               case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 a3 a2 a1)) of
+                  Dict -> do x :: f3 a3 a2 a1 <- By.deserialize
+                             return (some3 x)
+
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , By.Serial (DemoteRep k4)
+    , By.Serial (DemoteRep k3)
+    , By.Serial (DemoteRep k2)
+    , By.Serial (DemoteRep k1)
+    , Dict4 By.Serial f4
+    ) => By.Serial (Some4 f4)
+  where
+    {-# INLINABLE serialize #-}
+    serialize = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 a4 a3 a2 a1)) of
+          Dict -> do By.serialize (fromSing sa4, fromSing sa3,
+                                   fromSing sa2, fromSing sa1)
+                     By.serialize x
+    {-# INLINABLE deserialize #-}
+    deserialize = do
+      (rsa4, rsa3, rsa2, rsa1) <- By.deserialize
+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> withSingI sa4 $
+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $
+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $
+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $
+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 a4 a3 a2 a1)) of
+                     Dict -> do x :: f4 a4 a3 a2 a1 <- By.deserialize
+                                return (some4 x)
diff --git a/src/lib/Exinst/Instances/DeepSeq.hs b/src/lib/Exinst/Instances/DeepSeq.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Instances/DeepSeq.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# 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.Instances.DeepSeq () where
+
+import Control.DeepSeq (NFData(rnf))
+import Data.Constraint
+import Prelude
+
+import Exinst.Internal
+
+--------------------------------------------------------------------------------
+
+instance forall (f1 :: k1 -> *).
+  ( Dict1 NFData f1
+  ) => NFData (Some1 f1) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some1x) ->
+    withSome1Sing some1x $ \ !sa1 !(x :: f1 a1) ->
+       case dict1 sa1 :: Dict (NFData (f1 a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall (f2 :: k2 -> k1 -> *).
+  ( Dict2 NFData f2
+  ) => NFData (Some2 f2) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some2x) ->
+    withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f2 a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (NFData (f2 a2 a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall (f3 :: k3 -> k2 -> k1 -> *).
+  ( Dict3 NFData f3
+  ) => NFData (Some3 f3) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some3x) ->
+    withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f3 a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (NFData (f3 a3 a2 a1)) of
+          Dict -> rnf x `seq` ()
+
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *).
+  ( Dict4 NFData f4
+  ) => NFData (Some4 f4) where
+  {-# INLINABLE rnf #-}
+  rnf = \(!some4x) ->
+    withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f4 a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f4 a4 a3 a2 a1)) of
+          Dict -> rnf x `seq` ()
+
diff --git a/src/lib/Exinst/Instances/Hashable.hs b/src/lib/Exinst/Instances/Hashable.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Instances/Hashable.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# 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.Instances.Hashable () where
+
+import Data.Hashable (Hashable(hashWithSalt))
+import Data.Constraint
+import Data.Singletons
+import Prelude
+
+import Exinst.Internal
+
+--------------------------------------------------------------------------------
+
+-- | Some salt we add to hashes calculated in this module.
+salt0 :: Int
+salt0 = 6700417
+
+--------------------------------------------------------------------------------
+
+instance forall (f1 :: k1 -> *)
+  . ( SingKind k1
+    , Hashable (DemoteRep k1)
+    , Dict1 Hashable f1
+    ) => Hashable (Some1 f1)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f1 a1) ->
+       case dict1 sa1 :: Dict (Hashable (f1 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall (f2 :: k2 -> k1 -> *)
+  . ( SingKind k2
+    , SingKind k1
+    , Hashable (DemoteRep k2)
+    , Hashable (DemoteRep k1)
+    , Dict2 Hashable f2
+    ) => Hashable (Some2 f2)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->
+       case dict2 sa2 sa1 :: Dict (Hashable (f2 a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall (f3 :: k3 -> k2 -> k1 -> *)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Hashable (DemoteRep k3)
+    , Hashable (DemoteRep k2)
+    , Hashable (DemoteRep k1)
+    , Dict3 Hashable f3
+    ) => Hashable (Some3 f3)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->
+       case dict3 sa3 sa2 sa1 :: Dict (Hashable (f3 a3 a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa3
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
+
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Hashable (DemoteRep k4)
+    , Hashable (DemoteRep k3)
+    , Hashable (DemoteRep k2)
+    , Hashable (DemoteRep k1)
+    , Dict4 Hashable f4
+    ) => Hashable (Some4 f4)
+  where
+    {-# INLINABLE hashWithSalt #-}
+    hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->
+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f4 a4 a3 a2 a1)) of
+          Dict -> salt `hashWithSalt` salt0
+                       `hashWithSalt` fromSing sa4
+                       `hashWithSalt` fromSing sa3
+                       `hashWithSalt` fromSing sa2
+                       `hashWithSalt` fromSing sa1
+                       `hashWithSalt` x
diff --git a/src/lib/Exinst/Instances/QuickCheck.hs b/src/lib/Exinst/Instances/QuickCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Instances/QuickCheck.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+
+{-# 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.Instances.QuickCheck () where
+
+import Data.Constraint
+import Data.Kind (Type)
+import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing)
+import qualified Test.QuickCheck as QC
+
+import Exinst.Internal
+
+--------------------------------------------------------------------------------
+
+instance
+  forall k1 (f :: k1 -> Type).
+  ( SingKind k1
+  , QC.Arbitrary (DemoteRep 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 (DemoteRep k2)
+  , QC.Arbitrary (DemoteRep 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 (DemoteRep k3)
+  , QC.Arbitrary (DemoteRep k2)
+  , QC.Arbitrary (DemoteRep 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 (DemoteRep k4)
+  , QC.Arbitrary (DemoteRep k3)
+  , QC.Arbitrary (DemoteRep k2)
+  , QC.Arbitrary (DemoteRep 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
+
diff --git a/src/lib/Exinst/Internal.hs b/src/lib/Exinst/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Exinst/Internal.hs
@@ -0,0 +1,361 @@
+{-# 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
+ , 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)
+
+   -- * 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 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 #-}
+
+--------------------------------------------------------------------------------
+
+-- | '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/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' #-}
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,182 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where
+
+import Control.DeepSeq (NFData(rnf))
+import qualified Data.Aeson as Aeson
+import qualified Data.Bytes.Get as Bytes
+import qualified Data.Bytes.Put as Bytes
+import qualified Data.Bytes.Serial as Bytes
+import Data.Hashable (Hashable(hash))
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+import Generic.Random.Generic (genericArbitrary, uniform)
+import qualified GHC.Generics as G
+import qualified Test.Tasty as Tasty
+import qualified Test.Tasty.Runners as Tasty
+import Test.Tasty.QuickCheck ((===))
+import qualified Test.Tasty.QuickCheck as QC
+
+import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing)
+
+import Exinst
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = Tasty.defaultMainWithIngredients
+  [ Tasty.consoleTestReporter
+  , Tasty.listingTests
+  ] tt
+
+--------------------------------------------------------------------------------
+
+tt :: Tasty.TestTree
+tt =
+  Tasty.testGroup "main"
+  [ tt_id "Identity through GHC's Generic" id_generic
+  , tt_id "Identity through Aeson's FromJSON/ToJSON" id_aeson
+  , tt_id "Identity through Bytes's Serial" id_bytes
+  , tt_nfdata
+  ]
+
+tt_id
+  :: String
+  -> (forall a.
+        ( G.Generic a, Aeson.FromJSON a, Aeson.ToJSON a, Bytes.Serial a
+        ) => a -> Maybe a
+     ) -- ^ It's easier to put all the constraints here.
+  -> Tasty.TestTree
+tt_id = \title id' -> Tasty.testGroup title
+  [ QC.testProperty "Some1" $
+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> Just x === id' x
+  , QC.testProperty "Some2" $
+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> Just x === id' x
+  , QC.testProperty "Some3" $
+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> Just x === id' x
+  , QC.testProperty "Some4" $
+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> Just x === id' x
+  ]
+
+tt_nfdata :: Tasty.TestTree
+tt_nfdata = Tasty.testGroup "NFData"
+  [ QC.testProperty "Some1" $
+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === rnf x
+  , QC.testProperty "Some2" $
+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === rnf x
+  , QC.testProperty "Some3" $
+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === rnf x
+  , QC.testProperty "Some4" $
+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === rnf x
+  ]
+
+tt_hashable :: Tasty.TestTree
+tt_hashable = Tasty.testGroup "Hashable"
+  [ QC.testProperty "Some1" $
+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === (hash x `seq` ())
+  , QC.testProperty "Some2" $
+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === (hash x `seq` ())
+  , QC.testProperty "Some3" $
+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === (hash x `seq` ())
+  , QC.testProperty "Some4" $
+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === (hash x `seq` ())
+  ]
+
+--------------------------------------------------------------------------------
+
+id_generic :: G.Generic a => a -> Maybe a
+id_generic = Just . G.to . G.from
+
+id_aeson :: (Aeson.FromJSON a, Aeson.ToJSON a) => a -> Maybe a
+id_aeson = Aeson.decode . Aeson.encode
+
+id_bytes :: Bytes.Serial a => a -> Maybe a
+id_bytes = \a ->
+  let bs = Bytes.runPutS (Bytes.serialize a)
+  in case Bytes.runGetS Bytes.deserialize bs of
+       Left _ -> Nothing
+       Right a' -> Just a'
+
+--------------------------------------------------------------------------------
+
+data family Foo1 :: Bool -> Type
+data instance Foo1 'False = F1 | F2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo1 'True = T1 | T2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+
+data family Foo2 :: Bool -> Bool -> Type
+data instance Foo2 'False 'False = FF1 | FF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo2 'False 'True = FT1 | FT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo2 'True 'False = TF1 | TF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo2 'True 'True = TT1 | TT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+
+data family Foo3 :: Bool -> Bool -> Bool -> Type
+data instance Foo3 'False 'False 'False = FFF1 | FFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'False 'False 'True = FFT1 | FFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'False 'True 'False = FTF1 | FTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'False 'True 'True = FTT1 | FTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'True 'False 'False = TFF1 | TFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'True 'False 'True = TFT1 | TFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'True 'True 'False = TTF1 | TTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo3 'True 'True 'True = TTT1 | TTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+
+data family Foo4 :: Bool -> Bool -> Bool -> Bool -> Type
+data instance Foo4 'False 'False 'False 'False = FFFF1 | FFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'False 'False 'True = FFFT1 | FFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'False 'True 'False = FFTF1 | FFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'False 'True 'True = FFTT1 | FFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'True 'False 'False = FTFF1 | FTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'True 'False 'True = FTFT1 | FTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'True 'True 'False = FTTF1 | FTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'False 'True 'True 'True = FTTT1 | FTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'False 'False 'False = TFFF1 | TFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'False 'False 'True = TFFT1 | TFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'False 'True 'False = TFTF1 | TFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'False 'True 'True = TFTT1 | TFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'True 'False 'False = TTFF1 | TTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'True 'False 'True = TTFT1 | TTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'True 'True 'False = TTTF1 | TTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+data instance Foo4 'True 'True 'True 'True = TTTT1 | TTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)
+
+--------------------------------------------------------------------------------
+-- Arbitrary instances
+
+instance QC.Arbitrary (Foo1 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo1 'True) where arbitrary = genericArbitrary uniform
+
+instance QC.Arbitrary (Foo2 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo2 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo2 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo2 'True 'True) where arbitrary = genericArbitrary uniform
+
+instance QC.Arbitrary (Foo3 'False 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'False 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'False 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'False 'True 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'True 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'True 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'True 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo3 'True 'True 'True) where arbitrary = genericArbitrary uniform
+
+instance QC.Arbitrary (Foo4 'False 'False 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'False 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'False 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'False 'True 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'True 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'True 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'True 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'False 'True 'True 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'False 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'False 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'False 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'False 'True 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'True 'False 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'True 'False 'True) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'True 'True 'False) where arbitrary = genericArbitrary uniform
+instance QC.Arbitrary (Foo4 'True 'True 'True 'True) where arbitrary = genericArbitrary uniform
+