diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,247 @@
+0.14.4 [2026.01.26]
+-------------------
+* Depend on `ghc-bignum` instead of `integer-gmp` on recent versions GHC.
+
+0.14.3 [2026.01.10]
+-------------------
+* Remove unused `ghc-prim` dependency.
+
+0.14.2 [2024.05.12]
+-------------------
+* Re-export `Log2` from `Data.Constraint.Nat`.
+* Add `log2Nat` and `log2Pow` to `Data.Constraint.Nat`.
+
+0.14.1 [2024.04.29]
+-------------------
+* Remove an unused dependency on the `type-equality` library.
+
+0.14 [2023.10.11]
+-----------------
+* Drop support for GHCs older than 8.6.
+* The `forall` function in `Data.Constraint.Forall` has been renamed to
+  `forall_`, since a future version of GHC will make the use of `forall` as
+  an identifier an error.
+* Implement `Data.Constraint.Forall` using `QuantifiedConstraints`.
+* Remove `Lifting` instances for `ErrorT` and `ListT`, which were removed
+  in `transformers-0.6.*`.
+* Add a `c => Boring (Dict c)` instance.
+* Add the `Data.Constraint.Char` module, which contains utilities for working
+  with `KnownChar` constraints. This module is only available on GHC 9.2 or
+  later.
+* Add `unsafeAxiom` to `Data.Constraint.Unsafe`.
+* Add `unsafeSChar`, `unsafeSNat`, and `unsafeSSymbol` to
+  `Data.Constraint.Unsafe` when building with `base-4.18` (GHC 9.6) or later.
+
+0.13.4 [2022.05.19]
+-------------------
+* Correct the CPP introduced in `constraints-0.13.3` such that it works when
+  building with `mtl-2.3.*` or later combined with `transformers < 0.6`.
+
+0.13.3 [2022.01.31]
+-------------------
+* Allow building with `transformers-0.6.*` and `mtl-2.3.*`.
+
+0.13.2 [2021.11.10]
+-------------------
+* Allow building on GHC HEAD.
+
+0.13.1 [2021.10.31]
+-------------------
+* Allow building with GHC 9.2.
+
+0.13 [2021.02.17]
+-----------------
+* `Data.Constraint.Symbol` now reexports the `GHC.TypeLits.AppendSymbol` type
+  family from recent versions of `base` (or, on old versions of `base`, it
+  defines a backwards-compatibile version of `AppendSymbol`). The existing
+  `(++)` type family for `Data.Constraint.Symbol` is now a synonym for
+  `AppendSymbol`.
+
+  This is technically a breaking change, as `(++)` was previously defined like
+  so:
+
+  ```hs
+  type family (++) :: Symbol -> Symbol -> Symbol
+  ```
+
+  This meant that `(++)` could be partially applied. However, for compatibility
+  with the way that `AppendSymbol` is defined, `(++)` is now defined like so:
+
+  ```hs
+  type m ++ n = AppendSymbol m n
+  ```
+
+  As a result, `(++)` can no longer be partially applied.
+* Make the `(++)` type family in `Data.Constraint.Symbol` be `infixr 5`.
+* Add `implied :: (a => b) -> (a :- b)` to `Data.Constraint`, which converts
+  a quantified constraint into an entailment. This is only available when
+  compiled with GHC 8.6 or later.
+
+0.12 [2020.02.03]
+-----------------
+* Relax the type signature for `divideTimes`:
+
+  ```diff
+  -dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)
+  +dividesTimes ::  Divides a b               :- Divides a (b * c)
+  ```
+
+* Simplify the type signature of `dividesDef`:
+
+  ```diff
+  -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)
+  +dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
+  ```
+
+  The original type of `diviesDef` can be (partially) recovered by defining
+  it in terms of the new `dividesDef`:
+
+  ```hs
+  dividesDef' :: forall a b. (1 <= a, Divides a b) :- ((a * Div b a) ~ b)
+  dividesDef' = Sub $ case (dividesDef @a @b, euclideanNat @a @b) of
+    (Sub Dict, Sub Dict) -> Dict
+  ```
+
+0.11.2 [2019.09.06]
+-------------------
+* Depend on the `type-equality` compatibility library so that `(:~~:)` may be
+  used when compiling this library with GHC 8.0. This avoids having to redefine
+  `(:~~:)` directly in the internals of `constraints` itself.
+
+0.11.1 [2019.08.27]
+-------------------
+* Make `Data.Constraint.Deferrable.UnsatisfiedConstraint` a newtype.
+
+0.11 [2019.05.10]
+-----------------
+* Introduce a `HasDict` type class for types that witness evidence of
+  constraints, such as `Dict`, `(:-)`, `Coercion`, `(:~:)`, `(:~~:)`, and
+  `TypeRep`.
+* Generalize the types of `withDict` and `(\\)` to be polymorphic over
+  any `HasDict` instance.
+* Add `type (⊢) = (:-)`.
+* Fix unsafe mistakes in the statements of `dividesDef` and `timesDiv` in
+  `Data.Constraint.Nat`.
+* Make the implementations of `Min` and `Max` reduce on more inputs in
+  `Data.Constraint.Nat`.
+* Add `minusNat` and `minusZero` functions to `Data.Constraint.Nat`.
+* Support `hashable-1.3.*` and `semigroups-0.19.*`.
+
+0.10.1 [2018.07.02]
+-------------------
+* Allow building with GHC 8.6.
+* Add three axioms about `(+)` and `(-)` to `Data.Constraint.Nat`.
+
+0.10
+----
+* Adapt to the `Semigroup`–`Monoid` Proposal (introduced in `base-4.11`):
+  * Add a `Semigroup` instance for `Dict`
+  * Add the appropriate `(:=>)` instances involving `Semigroup`, and change the
+    `Class () (Monoid a)` instance to `Class (Semigroup a) (Monoid a)` when
+    `base` is recent enough
+  * Add the appropriate `Lifting(2)` instances involving `Semigroup`
+* `Data.Constraint.Nat` now reexports the `Div` and `Mod` type families from
+  `GHC.TypeLits` on `base-4.11` or later
+* Fix the type signature of `maxCommutes`
+* Export the `no` method of `Bottom`
+* Add `NFData` instances for `Dict` and `(:-)`
+
+0.9.1
+-----
+* Correct an improper use of `unsafeCoerce` in the internals of
+  `Data.Constraint.Nat` and `Data.Constraint.Symbol`
+* Correctly identify the mismatched types when you defer an unsatisfiable
+  equality constraint through `Data.Constraint.Deferrable`
+* Re-export the `(:~~:)` defined in `base` from `Data.Constraint.Deferred` with
+  GHC 8.2 or later
+* Add several new `(:=>)` instances for `Bits`, `Identity`, `Const`, `Natural`,
+  `IO`, and `Word`.
+* Modernize some existing `Class` and `(:=>)` instances to reflect the fact
+  that `Applicative` is now a superclass of `Monad` on recent versions of
+  `base`.
+
+0.9
+---
+* Changes to `Data.Constraint`:
+  * Add `strengthen1` and `strengthen2`
+* Changes to `Data.Constraint.Deferrable`:
+  * Add a `Deferrable ()` instance
+  * The `Deferrable (a ~ b)` instance now shows the `TypeRep`s of `a` and `b`
+    when a type mismatch error is thrown
+  * Add `defer_` and `deferEither_`, counterparts to `defer` and `deferEither`
+    which do not require proxy arguments
+  * Enable `PolyKinds`. This allows the `Deferrable (a ~ b)` instance to be
+    polykinded on all supported versions of GHC _except_ 7.10, where the kinds
+    must be `*` due to an old GHC bug
+  * Introduce a heterogeneous equality type `(:~~:)`, and use it to define a
+    `Deferrable (a ~~ b)` instance on GHC 8.0 or later
+* Changes to `Data.Constraint.Forall`:
+  * Implement `ForallF` and `ForallT` in terms of `Forall`
+  * Add `ForallV` and `InstV` (supporting a variable number of parameters)
+  * Add a `forall` combinator
+* Introduce `Data.Constraint.Nat` and `Data.Constraint.Symbol`, which contain
+  utilities for working with `KnownNat` and `KnownSymbol` constraints,
+  respectively. These modules are only available on GHC 8.0 or later.
+
+0.8
+-----
+* GHC 8 compatibility
+* `transformers` 0.5 compatibility
+* `binary` 0.8 compatibility
+* Dropped support for GHC 7.6 in favor of a nicer Bottom representation.
+
+0.7
+---
+* Found a nicer encoding of the initial object in the category of constraints using a [nullary constraint](https://ghc.haskell.org/trac/ghc/ticket/7642).
+
+0.6.1
+-----
+* Remove the need for closed type families from the new `Forall`.
+
+0.6
+---
+* Completely redesigned `Data.Constraint.Forall`. The old design is unsound and can be abused to define `unsafeCoerce`!
+  The new design requires closed type families, so this module now requires GHC 7.8+
+
+0.5.1
+-----
+* Added `Data.Constraint.Deferrable`.
+
+0.5
+-----
+* Added `Data.Constraint.Lifting`.
+
+0.4.1.3
+-------
+* Acknowledge we actually need at least base 4.5
+
+0.4.1.2
+-------
+* Restore support for building on older GHCs
+
+0.4.1.1
+-------
+* Minor documentation fixes.
+
+0.4.1
+-----
+* Added `mapDict` and `unmapDict`.
+* Added a lot of documentation.
+
+0.4
+---
+* `Typeable` and `Data`. The `Data` instance for `(:-)` is a conservative approximation that avoids having to turn (:-) into a cartesian closed category.
+  If it becomes a pain point for users, I know how to do that, and have done so in other libraries -- see [hask](http://github.com/ekmett/hask), but I'm hesitant to bring such heavy machinery to bear and it isn't clear how to do it in a way that is compatible with those other libraries.
+
+0.3.5
+-----
+* Explicit role annotations
+
+0.3.4.1
+-------
+* Fixed build failures.
+* Fixed an unused import warning on older GHCs.
+
+0.3.4
+-----
+* Added `bottom`
diff --git a/Data/Constraint.hs b/Data/Constraint.hs
deleted file mode 100644
--- a/Data/Constraint.hs
+++ /dev/null
@@ -1,359 +0,0 @@
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE RoleAnnotations #-}
-#endif
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Constraint
--- Copyright   :  (C) 2011-2013 Edward Kmett,
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
-----------------------------------------------------------------------------
-
-
-module Data.Constraint
-  (
-  -- * Constraints
-    Constraint
-  -- * Dictionary
-  , Dict(Dict)
-  -- * Entailment
-  , (:-)(Sub)
-  , (\\)
-  , weaken1, weaken2, contract
-  , (&&&), (***)
-  , trans, refl
-  , top, bottom
-  -- * Reflection
-  , Class(..)
-  , (:=>)(..)
-  ) where
-import Control.Monad
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-import Control.Category
-#endif
-import Control.Applicative
-import Data.Monoid
-import Data.Complex
-import Data.Ratio
-import GHC.Prim (Constraint)
-
--- | Capture a dictionary for a given constraint
-data Dict :: Constraint -> * where
-  Dict :: a => Dict a
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-type role Dict nominal
-#endif
-
-deriving instance Eq (Dict a)
-deriving instance Ord (Dict a)
-deriving instance Show (Dict a)
-
-infixr 9 :-
-newtype a :- b = Sub (a => Dict b)
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-type role (:-) nominal nominal
-#endif
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-instance Category (:-) where
-  id  = refl
-  (.) = trans
-#endif
-
-instance Eq (a :- b) where
-  _ == _ = True
-
-instance Ord (a :- b) where
-  compare _ _ = EQ
-
-instance Show (a :- b) where
-  showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"
-
-infixl 1 \\ -- required comment
-
--- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
-(\\) :: a => (b => r) -> (a :- b) -> r
-r \\ Sub Dict = r
-
--- | due to the hack for the kind of (,) in the current version of GHC we can't actually
--- make instances for (,) :: Constraint -> Constraint -> Constraint
-(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
-f *** g = Sub $ Dict \\ f \\ g
-
--- | Weakening a constraint product
-weaken1 :: (a, b) :- a
-weaken1 = Sub Dict
-
--- | Weakening a constraint product
-weaken2 :: (a, b) :- b
-weaken2 = Sub Dict
-
--- | Contracting a constraint / diagonal morphism
-contract :: a :- (a, a)
-contract = Sub Dict
-
--- | Constraint product
---
--- > trans weaken1 (f &&& g) = f
--- > trans weaken2 (f &&& g) = g
-(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)
-f &&& g = Sub $ Dict \\ f \\ g
-
---    ?
---   / \
--- (#)  ??  ???
---     /  \ / \
---    #    *  Constraint
-
--- | Transitivity of entailment
---
--- If we view '(:-)' as a Constraint-indexed category, then this is '(.)'
-trans :: (b :- c) -> (a :- b) -> a :- c
-trans f g = Sub $ Dict \\ f \\ g
-
--- | Reflexivity of entailment
--- 
--- If we view '(:-)' as a Constraint-indexed category, then this is 'id'
-refl :: a :- a
-refl = Sub Dict
-
--- | Every constraint implies truth
---
--- These are the terminal arrows of the category, and () is the terminal object.
-top :: a :- ()
-top = Sub Dict
-
-type family Ex (a :: *) (c :: Constraint) :: Constraint
-type instance Ex () c = ()
-type instance Ex Bool c = c
-
-falso :: (() ~ a) :- Ex a c
-falso = Sub Dict
-
--- |
--- A bad type coercion lets you derive any type you want.
---
--- These are the initial arrows of the category and (() ~ Bool) is the initial object
---
--- This demonstrates the law of classical logical <http://en.wikipedia.org/wiki/Principle_of_explosion ex falso quodlibet>
-bottom :: (() ~ Bool) :- c
-bottom = falso
-
--- | Reify the relationship between a class and its superclass constraints as a class
-class Class b h | h -> b where
-  cls :: h :- b
-
-infixr 9 :=>
--- | Reify the relationship between an instance head and its body as a class
-class b :=> h | h -> b where
-  ins :: b :- h
-
-instance Class () (Class b a) where cls = Sub Dict
-instance Class () (b :=> a) where cls = Sub Dict
-
-instance Class b a => () :=> Class b a where ins = Sub Dict
-instance (b :=> a) => () :=> b :=> a where ins = Sub Dict
-
-instance Class () () where cls = Sub Dict
-instance () :=> () where ins = Sub Dict
-
--- Local, Prelude, Applicative, C.M.I and Data.Monoid instances
-
--- Eq
-instance Class () (Eq a) where cls = Sub Dict
-instance () :=> Eq () where ins = Sub Dict
-instance () :=> Eq Int where ins = Sub Dict
-instance () :=> Eq Bool where ins = Sub Dict
-instance () :=> Eq Integer where ins = Sub Dict
-instance () :=> Eq Float where ins = Sub Dict
-instance () :=> Eq Double where ins = Sub Dict
-instance Eq a :=> Eq [a] where ins = Sub Dict
-instance Eq a :=> Eq (Maybe a) where ins = Sub Dict
-instance Eq a :=> Eq (Complex a) where ins = Sub Dict
-instance Eq a :=> Eq (Ratio a) where ins = Sub Dict
-instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict
-instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict
-instance () :=> Eq (Dict a) where ins = Sub Dict
-instance () :=> Eq (a :- b) where ins = Sub Dict
-
--- Ord
-instance Class (Eq a) (Ord a) where cls = Sub Dict
-instance () :=> Ord () where ins = Sub Dict
-instance () :=> Ord Bool where ins = Sub Dict
-instance () :=> Ord Int where ins = Sub Dict
-instance ():=> Ord Integer where ins = Sub Dict
-instance () :=> Ord Float where ins = Sub Dict
-instance ():=> Ord Double where ins = Sub Dict
-instance () :=> Ord Char where ins = Sub Dict
-instance Ord a :=> Ord (Maybe a) where ins = Sub Dict
-instance Ord a :=> Ord [a] where ins = Sub Dict
-instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict
-instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict
-instance Integral a :=> Ord (Ratio a) where ins = Sub Dict
-instance () :=> Ord (Dict a) where ins = Sub Dict
-instance () :=> Ord (a :- b) where ins = Sub Dict
-
-instance Class () (Show a) where cls = Sub Dict
-instance () :=> Show () where ins = Sub Dict
-instance () :=> Show Bool where ins = Sub Dict
-instance () :=> Show Ordering where ins = Sub Dict
-instance () :=> Show Char where ins = Sub Dict
-instance Show a :=> Show (Complex a) where ins = Sub Dict
-instance Show a :=> Show [a] where ins = Sub Dict
-instance Show a :=> Show (Maybe a) where ins = Sub Dict
-instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict
-instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict
-instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict
-instance () :=> Show (Dict a) where ins = Sub Dict
-instance () :=> Show (a :- b) where ins = Sub Dict
-
-instance Class () (Read a) where cls = Sub Dict
-instance () :=> Read () where ins = Sub Dict
-instance () :=> Read Bool where ins = Sub Dict
-instance () :=> Read Ordering where ins = Sub Dict
-instance () :=> Read Char where ins = Sub Dict
-instance Read a :=> Read (Complex a) where ins = Sub Dict
-instance Read a :=> Read [a] where ins = Sub Dict
-instance Read a :=> Read (Maybe a) where ins = Sub Dict
-instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict
-instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict
-instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict
-
-instance Class () (Enum a) where cls = Sub Dict
-instance () :=> Enum () where ins = Sub Dict
-instance () :=> Enum Bool where ins = Sub Dict
-instance () :=> Enum Ordering where ins = Sub Dict
-instance () :=> Enum Char where ins = Sub Dict
-instance () :=> Enum Int where ins = Sub Dict
-instance () :=> Enum Integer where ins = Sub Dict
-instance () :=> Enum Float where ins = Sub Dict
-instance () :=> Enum Double where ins = Sub Dict
-instance Integral a :=> Enum (Ratio a) where ins = Sub Dict
-
-instance Class () (Bounded a) where cls = Sub Dict
-instance () :=> Bounded () where ins = Sub Dict
-instance () :=> Bounded Ordering where ins = Sub Dict
-instance () :=> Bounded Bool where ins = Sub Dict
-instance () :=> Bounded Int where ins = Sub Dict
-instance () :=> Bounded Char where ins = Sub Dict
-instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict
-
-instance Class () (Num a) where cls = Sub Dict
-instance () :=> Num Int where ins = Sub Dict
-instance () :=> Num Integer where ins = Sub Dict
-instance () :=> Num Float where ins = Sub Dict
-instance () :=> Num Double where ins = Sub Dict
-instance RealFloat a :=> Num (Complex a) where ins = Sub Dict
-instance Integral a :=> Num (Ratio a) where ins = Sub Dict
-
-instance Class (Num a, Ord a) (Real a) where cls = Sub Dict
-instance () :=> Real Int where ins = Sub Dict
-instance () :=> Real Integer where ins = Sub Dict
-instance () :=> Real Float where ins = Sub Dict
-instance () :=> Real Double where ins = Sub Dict
-instance Integral a :=> Real (Ratio a) where ins = Sub Dict
-
-instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict
-instance () :=> Integral Int where ins = Sub Dict
-instance () :=> Integral Integer where ins = Sub Dict
-
-instance Class (Num a) (Fractional a) where cls = Sub Dict
-instance () :=> Fractional Float where ins = Sub Dict
-instance () :=> Fractional Double where ins = Sub Dict
-instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict
-instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict
-
-instance Class (Fractional a) (Floating a) where cls = Sub Dict
-instance () :=> Floating Float where ins = Sub Dict
-instance () :=> Floating Double where ins = Sub Dict
-instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict
-
-instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict
-instance () :=> RealFrac Float where ins = Sub Dict
-instance () :=> RealFrac Double where ins = Sub Dict
-instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict
-
-instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict
-instance () :=> RealFloat Float where ins = Sub Dict
-instance () :=> RealFloat Double where ins = Sub Dict
-
-instance Class () (Monoid a) where cls = Sub Dict
-instance () :=> Monoid () where ins = Sub Dict
-instance () :=> Monoid Ordering where ins = Sub Dict
-instance () :=> Monoid [a] where ins = Sub Dict
-instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict
-instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict
-
-instance Class () (Functor f) where cls = Sub Dict
-instance () :=> Functor [] where ins = Sub Dict
-instance () :=> Functor Maybe where ins = Sub Dict
-instance () :=> Functor (Either a) where ins = Sub Dict
-instance () :=> Functor ((->) a) where ins = Sub Dict
-instance () :=> Functor ((,) a) where ins = Sub Dict
-instance () :=> Functor IO where ins = Sub Dict
-instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict
-
-instance Class (Functor f) (Applicative f) where cls = Sub Dict
-instance () :=> Applicative [] where ins = Sub Dict
-instance () :=> Applicative Maybe where ins = Sub Dict
-instance () :=> Applicative (Either a) where ins = Sub Dict
-instance () :=> Applicative ((->)a) where ins = Sub Dict
-instance () :=> Applicative IO where ins = Sub Dict
-instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict
-instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict
-
-instance Class (Applicative f) (Alternative f) where cls = Sub Dict
-instance () :=> Alternative [] where ins = Sub Dict
-instance () :=> Alternative Maybe where ins = Sub Dict
-instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict
-
-instance Class () (Monad f) where cls = Sub Dict
-instance () :=> Monad [] where ins = Sub Dict
-instance () :=> Monad ((->) a) where ins = Sub Dict
-instance () :=> Monad (Either a) where ins = Sub Dict
-instance () :=> Monad IO where ins = Sub Dict
-
-instance Class (Monad f) (MonadPlus f) where cls = Sub Dict
-instance () :=> MonadPlus [] where ins = Sub Dict
-instance () :=> MonadPlus Maybe where ins = Sub Dict
-
--- UndecidableInstances
-instance a :=> Enum (Dict a) where ins = Sub Dict
-instance a => Enum (Dict a) where
-  toEnum _ = Dict
-  fromEnum Dict = 0
-
-instance a :=> Bounded (Dict a) where ins = Sub Dict
-instance a => Bounded (Dict a) where
-  minBound = Dict
-  maxBound = Dict
-
-instance a :=> Read (Dict a) where ins = Sub Dict
-deriving instance a => Read (Dict a)
-
-instance a :=> Monoid (Dict a) where ins = Sub Dict
-instance a => Monoid (Dict a) where
-  mappend Dict Dict = Dict
-  mempty = Dict
-
diff --git a/Data/Constraint/Forall.hs b/Data/Constraint/Forall.hs
deleted file mode 100644
--- a/Data/Constraint/Forall.hs
+++ /dev/null
@@ -1,69 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE Trustworthy #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-{-# LANGUAGE RoleAnnotations #-}
-#endif
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Constraint.Forall
--- Copyright   :  (C) 2011-2013 Edward Kmett,
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
-----------------------------------------------------------------------------
-
-module Data.Constraint.Forall
-  ( Forall, inst
-  , ForallF, instF
-  , Forall1, inst1
-  , ForallT, instT
-  ) where
-
-import Data.Constraint
-import Data.Constraint.Unsafe
-
--- skolem variables, do not export!
-data A
-data B
--- | A quantified constraint
-type Forall (p :: * -> Constraint) = (p A, p B)
-
-type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B))
-
-data F a
-data M a
-
-type Forall1 (p :: (* -> *) -> Constraint) = (p F, p M)
-
-type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B))
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-type role F nominal
-type role M nominal
-#endif
-
-
--- | instantiate a quantified constraint on kind @*@
-inst :: forall p a. Forall p :- p a
-inst = trans (unsafeCoerceConstraint :: p A :- p a) weaken1
-
-instF :: forall p f a. ForallF p f :- p (f a)
-instF = trans (unsafeCoerceConstraint :: p (f A) :- p (f a)) weaken1
-
--- | instantiate a quantified constraint on kind @* -> *@
-inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall1 p :- p f
-inst1 = trans (unsafeCoerceConstraint :: p F :- p f) weaken1
-
-instT :: forall (p :: * -> Constraint) (t :: (* -> *) -> * -> *) (f :: * -> *) a. ForallT p t :- p (t f a)
-instT = trans (unsafeCoerceConstraint :: p (t F A) :- p (t f a)) weaken1
-
diff --git a/Data/Constraint/Unsafe.hs b/Data/Constraint/Unsafe.hs
deleted file mode 100644
--- a/Data/Constraint/Unsafe.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE Unsafe #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Constraint.Unsafe
--- Copyright   :  (C) 2011-2013 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
-----------------------------------------------------------------------------
-module Data.Constraint.Unsafe
-  ( unsafeCoerceConstraint
-  , unsafeDerive
-  , unsafeUnderive
-  -- * Sugar
-  , unsafeApplicative
-  , unsafeAlternative
-  ) where
-
-import Control.Applicative
-import Control.Monad
-import Control.Newtype
-import Data.Constraint
-import Unsafe.Coerce
-
--- | Coerce a dictionary unsafely from one type to another
-unsafeCoerceConstraint :: a :- b
-unsafeCoerceConstraint = unsafeCoerce refl
-
--- | Coerce a dictionary unsafely from one type to a newtype of that type
-unsafeDerive :: Newtype n o => (o -> n) -> t o :- t n
-unsafeDerive _ = unsafeCoerceConstraint
-
--- | Coerce a dictionary unsafely from a newtype of a type to the base type
-unsafeUnderive :: Newtype n o => (o -> n) -> t n :- t o
-unsafeUnderive _ = unsafeCoerceConstraint
-
--- | Construct an Applicative instance from a Monad
-unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a
-unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins
-
--- | Construct an Alternative instance from a MonadPlus
-unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a
-unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2011-2013 Edward Kmett
+Copyright 2011-2015 Edward Kmett
 
 All rights reserved.
 
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,6 +1,8 @@
 constraints
 ===========
 
+[![Hackage](https://img.shields.io/hackage/v/constraints.svg)](https://hackage.haskell.org/package/constraints) [![Build Status](https://github.com/ekmett/constraints/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/constraints/actions?query=workflow%3AHaskell-CI)
+
 This package provides data types and classes for manipulating the 'ConstraintKinds' exposed by GHC in 7.4.
 
 Contact Information
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,28 +1,48 @@
+cabal-version: 2.4
 name:          constraints
 category:      Constraints
-version:       0.3.5
-license:       BSD3
-cabal-version: >= 1.10
+version:       0.14.4
+license:       BSD-2-Clause
 license-file:  LICENSE
 author:        Edward A. Kmett
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
 stability:     experimental
 homepage:      http://github.com/ekmett/constraints/
 bug-reports:   http://github.com/ekmett/constraints/issues
-copyright:     Copyright (C) 2011-2013 Edward A. Kmett
+copyright:     Copyright (C) 2011-2021 Edward A. Kmett
 synopsis:      Constraint manipulation
-description:   Constraint manipulation
+description:
+  GHC 7.4 gave us the ability to talk about @ConstraintKinds@. They stopped crashing the compiler in GHC 7.6.
+  .
+  This package provides a vocabulary for working with them.
+
 build-type:    Simple
-tested-with:   GHC == 7.7.20131027, GHC == 7.7.20131025, GHC == 7.6.3
+
+tested-with:
+  GHC == 9.14.1
+  GHC == 9.12.2
+  GHC == 9.10.3
+  GHC == 9.8.4
+  GHC == 9.6.7
+  GHC == 9.4.8
+  GHC == 9.2.8
+  GHC == 9.0.2
+  GHC == 8.10.7
+  GHC == 8.8.4
+  GHC == 8.6.5
+
 extra-source-files: README.markdown
+                  , CHANGELOG.markdown
 
 source-repository head
   type: git
-  location: git://github.com/ekmett/constraints.git
+  location: https://github.com/ekmett/constraints.git
 
 library
+  hs-source-dirs: src
+
   default-language: Haskell2010
-  other-extensions
+  other-extensions:
     FunctionalDependencies,
     ScopedTypeVariables,
     StandaloneDeriving,
@@ -35,12 +55,45 @@
     GADTs
 
   build-depends:
-    base >= 4.4 && < 5,
-    newtype >= 0.2 && < 0.3,
-    ghc-prim
+    , base           >= 4.12  && < 5
+    , binary         >= 0.7.1 && < 0.9
+    , boring         >= 0.2   && < 0.3
+    , deepseq        >= 1.3   && < 1.6
+    , hashable       >= 1.2   && < 1.6
+    , mtl            >= 2.2   && < 2.4
+    , transformers   >= 0.5   && < 0.7
+  if impl(ghc >= 9.15)
+    build-depends:
+      ghc-bignum
+  elif impl(ghc < 9.0)
+    build-depends:
+      integer-gmp
+
   exposed-modules:
     Data.Constraint
+    Data.Constraint.Deferrable
     Data.Constraint.Forall
+    Data.Constraint.Lifting
+    Data.Constraint.Nat
+    Data.Constraint.Symbol
     Data.Constraint.Unsafe
 
-  ghc-options: -Wall
+  if impl(ghc >= 9.2)
+    exposed-modules:
+      Data.Constraint.Char
+
+  ghc-options: -Wall -Wno-star-is-type
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  hs-source-dirs: tests
+  main-is: Spec.hs
+  other-modules: GH55Spec
+                 GH117Spec
+  ghc-options: -Wall -threaded -rtsopts
+  build-tool-depends: hspec-discover:hspec-discover >= 2
+  build-depends:
+    , base
+    , constraints
+    , hspec >= 2
diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint.hs
@@ -0,0 +1,747 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+-- |
+-- Copyright   :  (C) 2011-2015 Edward Kmett,
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- @ConstraintKinds@ made type classes into types of a new kind, @Constraint@.
+--
+-- @
+-- 'Eq' :: * -> 'Constraint'
+-- 'Ord' :: * -> 'Constraint'
+-- 'Monad' :: (* -> *) -> 'Constraint'
+-- @
+--
+-- The need for this extension was first publicized in the paper
+--
+-- <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/gmap3.pdf Scrap your boilerplate with class: extensible generic functions>
+--
+-- by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the
+-- things they needed into a custom 'Sat' typeclass.
+--
+-- With @ConstraintKinds@ we can put into code a lot of tools for manipulating
+-- these new types without such awkward workarounds.
+
+module Data.Constraint
+  (
+  -- * The Kind of Constraints
+    Constraint
+  -- * Dictionary
+  , Dict(Dict)
+  , HasDict(..)
+  , withDict
+  , (\\)
+  -- * Entailment
+  , (:-)(Sub)
+  , type (⊢)
+  , type (|-)
+  , type (&)
+  , weaken1, weaken2, contract
+  , strengthen1, strengthen2
+  , (&&&), (***)
+  , trans, refl
+  , implied
+  , Bottom(no)
+  , top, bottom
+  -- * Dict is fully faithful
+  , mapDict
+  , unmapDict
+  -- * Reflection
+  , Class(..)
+  , (:=>)(..)
+  ) where
+import Control.Applicative
+import Control.Category
+import Control.DeepSeq
+import Control.Monad
+import Data.Complex
+import Data.Ratio
+import Data.Data hiding (TypeRep)
+import qualified GHC.Exts as Exts (Any)
+import GHC.Exts (Constraint)
+import Data.Bits (Bits)
+import Data.Functor.Identity (Identity)
+import Numeric.Natural (Natural)
+import Data.Coerce (Coercible)
+import Data.Type.Coercion(Coercion(..))
+import Data.Type.Equality (type (~~))
+import qualified Data.Type.Equality as Hetero
+import Type.Reflection (TypeRep, typeRepKind, withTypeable)
+import Data.Boring (Boring (..))
+
+-- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@.
+--
+-- e.g.
+--
+-- @
+-- 'Dict' :: 'Dict' ('Eq' 'Int')
+-- @
+--
+-- captures a dictionary that proves we have an:
+--
+-- @
+-- instance 'Eq' 'Int'
+-- @
+--
+-- Pattern matching on the 'Dict' constructor will bring this instance into scope.
+--
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+deriving stock instance (Typeable p, p) => Data (Dict p)
+deriving stock instance Eq (Dict a)
+deriving stock instance Ord (Dict a)
+deriving stock instance Show (Dict a)
+
+instance c => Boring (Dict c) where
+    boring = Dict
+
+{-
+instance (Typeable p, p) => Data (Dict p) where
+  gfoldl _ z Dict = z Dict
+  toConstr _ = dictConstr
+  gunfold _ z c = case constrIndex c of
+    1 -> z Dict
+    _ -> error "gunfold"
+  dataTypeOf _ = dictDataType
+
+dictConstr :: Constr
+dictConstr = mkConstr dictDataType "Dict" [] Prefix
+
+dictDataType :: DataType
+dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]
+-}
+
+
+instance NFData (Dict c) where
+  rnf Dict = ()
+
+-- | Witnesses that a value of type @e@ contains evidence of the constraint @c@.
+--
+-- Mainly intended to allow ('\\') to be overloaded, since it's a useful operator.
+class HasDict c e | e -> c where
+  evidence :: e -> Dict c
+
+instance HasDict a (Dict a) where
+  evidence = Prelude.id
+
+instance a => HasDict b (a :- b) where
+  evidence (Sub x) = x
+
+instance HasDict (Coercible a b) (Coercion a b) where
+  evidence Coercion = Dict
+
+instance HasDict (a ~ b) (a :~: b) where
+  evidence Refl = Dict
+
+instance HasDict (a ~~ b) (a Hetero.:~~: b) where
+  evidence Hetero.HRefl = Dict
+
+instance HasDict (Typeable k, Typeable a) (TypeRep (a :: k)) where
+  evidence tr = withTypeable tr $ withTypeable (typeRepKind tr) Dict
+
+-- | From a 'Dict', takes a value in an environment where the instance
+-- witnessed by the 'Dict' is in scope, and evaluates it.
+--
+-- Essentially a deconstruction of a 'Dict' into its continuation-style
+-- form.
+--
+-- Can also be used to deconstruct an entailment, @a ':-' b@, using a context @a@.
+--
+-- @
+-- withDict :: 'Dict' c -> (c => r) -> r
+-- withDict :: a => (a ':-' c) -> (c => r) -> r
+-- @
+withDict :: HasDict c e => e -> (c => r) -> r
+withDict d r = case evidence d of
+                 Dict -> r
+
+infixl 1 \\ -- required comment
+
+-- | Operator version of 'withDict', with the arguments flipped
+(\\) :: HasDict c e => (c => r) -> e -> r
+r \\ d = withDict d r
+
+infixr 9 :-
+infixr 9 ⊢
+
+-- | Type entailment, as written with a single character.
+type (⊢) = (:-)
+
+-- | This is the type of entailment.
+--
+-- @a ':-' b@ is read as @a@ \"entails\" @b@.
+--
+-- With this we can actually build a category for 'Constraint' resolution.
+--
+-- e.g.
+--
+-- Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@
+-- entails @'Eq' a@.
+--
+-- Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@
+-- entails @'Ord' [a]@ as well.
+--
+-- This relationship is captured in the ':-' entailment type here.
+--
+-- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a
+-- 'Category' of constraints. However, 'Category' only became sufficiently
+-- general to support this instance in GHC 7.8, so prior to 7.8 this instance
+-- is unavailable.
+--
+-- But due to the coherence of instance resolution in Haskell, this 'Category'
+-- has some very interesting properties. Notably, in the absence of
+-- @IncoherentInstances@, this category is \"thin\", which is to say that
+-- between any two objects (constraints) there is at most one distinguishable
+-- arrow.
+--
+-- This means that for instance, even though there are two ways to derive
+-- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by
+-- construction be equal. This is a property that Haskell offers that is
+-- pretty much unique in the space of languages with things they call \"type
+-- classes\".
+--
+-- What are the two ways?
+--
+-- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the
+-- superclass relationship, and then from @'Eq' a ':-' 'Eq' [a]@ via the
+-- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance
+-- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship
+-- and this diagram by definition must \"commute\".
+--
+-- Diagrammatically,
+--
+-- >                    Ord a
+-- >                ins /     \ cls
+-- >                   v       v
+-- >             Ord [a]     Eq a
+-- >                cls \     / ins
+-- >                     v   v
+-- >                    Eq [a]
+--
+-- This safety net ensures that pretty much anything you can write with this
+-- library is sensible and can't break any assumptions on the behalf of
+-- library authors.
+newtype a :- b = Sub (a => Dict b)
+
+type role (:-) nominal nominal
+
+instance (Typeable p, Typeable q, p => q) => Data (p :- q) where
+  gfoldl _ z d = z d
+  gunfold _ z c = case constrIndex c of
+     1 -> z (Sub Dict)
+     _ -> error "Data.Data.Data: Data.Constraint.:- constructor out of bounds"
+  toConstr _ = subCon
+  dataTypeOf _ = subTy
+
+subCon :: Constr
+subCon = mkConstr subTy "Sub Dict" [] Prefix
+{-# noinline subCon #-}
+subTy :: DataType
+subTy = mkDataType "Data.Constraint.:-" [subCon]
+{-# noinline subTy #-}
+
+-- | Possible since GHC 7.8, when 'Category' was made polykinded.
+instance Category (:-) where
+  id  = refl
+  (.) = trans
+
+-- | Assumes 'IncoherentInstances' doesn't exist.
+instance Eq (a :- b) where
+  _ == _ = True
+
+-- | Assumes 'IncoherentInstances' doesn't exist.
+instance Ord (a :- b) where
+  compare _ _ = EQ
+
+instance Show (a :- b) where
+  showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"
+
+instance a => NFData (a :- b) where
+  rnf (Sub Dict) = ()
+
+--------------------------------------------------------------------------------
+-- Constraints form a Category
+--------------------------------------------------------------------------------
+
+-- | Transitivity of entailment
+--
+-- If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@
+trans :: (b :- c) -> (a :- b) -> a :- c
+trans f g = Sub $ Dict \\ f \\ g
+
+-- | Reflexivity of entailment
+--
+-- If we view @(':-')@ as a Constraint-indexed category, then this is 'id'
+refl :: a :- a
+refl = Sub Dict
+
+--------------------------------------------------------------------------------
+-- QuantifiedConstraints
+--------------------------------------------------------------------------------
+
+-- | Convert a quantified constraint into an entailment.
+implied :: forall a b. (a => b) => a :- b
+implied = Sub (Dict :: Dict b)
+
+-- | The internal hom for the category of constraints.
+--
+-- This version can be passed around inside Dict, whereas (a => b) is impredicative
+--
+-- @
+-- foo :: Dict (Ord a => Eq a)
+-- foo = Dict
+-- @
+--
+-- fails to typecheck due to the lack of impredicative polymorphism, but
+--
+-- @
+-- foo :: Dict (Ord a |- Eq a)
+-- foo = Dict
+-- @
+--
+-- typechecks just fine.
+
+class (p => q) => p |- q
+instance (p => q) => p |- q
+
+
+--------------------------------------------------------------------------------
+-- (,) is a Bifunctor
+--------------------------------------------------------------------------------
+
+-- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually
+-- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but we can define
+-- an equivalent type, that converts back and forth to @(,)@, and lets you hang instances.
+class (p,q) => p & q
+instance (p,q) => p & q
+
+-- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually
+-- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a
+-- bifunctor on the category of constraints. This lets us map over both sides.
+(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
+f *** g = Sub $ Dict \\ f \\ g
+
+--------------------------------------------------------------------------------
+-- Constraints are Cartesian
+--------------------------------------------------------------------------------
+
+-- | Weakening a constraint product
+--
+-- The category of constraints is Cartesian. We can forget information.
+weaken1 :: (a, b) :- a
+weaken1 = Sub Dict
+
+-- | Weakening a constraint product
+--
+-- The category of constraints is Cartesian. We can forget information.
+weaken2 :: (a, b) :- b
+weaken2 = Sub Dict
+
+strengthen1 :: Dict b -> a :- c -> a :- (b,c)
+strengthen1 d e = unmapDict (const d) &&& e
+
+strengthen2 :: Dict b -> a :- c -> a :- (c,b)
+strengthen2 d e = e &&& unmapDict (const d)
+
+-- | Contracting a constraint / diagonal morphism
+--
+-- The category of constraints is Cartesian. We can reuse information.
+contract :: a :- (a, a)
+contract = Sub Dict
+
+-- | Constraint product
+--
+-- > trans weaken1 (f &&& g) = f
+-- > trans weaken2 (f &&& g) = g
+(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)
+f &&& g = Sub $ Dict \\ f \\ g
+
+--------------------------------------------------------------------------------
+-- Initial and terminal morphisms
+--------------------------------------------------------------------------------
+
+-- | Every constraint implies truth
+--
+-- These are the terminal arrows of the category, and @()@ is the terminal object.
+--
+-- Given any constraint there is a unique entailment of the @()@ constraint from that constraint.
+top :: a :- ()
+top = Sub Dict
+
+-- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance.
+class Exts.Any => Bottom where
+  no :: a
+
+-- |
+-- This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">
+bottom :: Bottom :- a
+bottom = Sub no
+
+--------------------------------------------------------------------------------
+-- Dict is fully faithful
+--------------------------------------------------------------------------------
+
+-- | Apply an entailment to a dictionary.
+--
+-- From a category theoretic perspective 'Dict' is a functor that maps from the category
+-- of constraints (with arrows in ':-') to the category Hask of Haskell data types.
+mapDict :: (a :- b) -> Dict a -> Dict b
+mapDict p Dict = case p of Sub q -> q
+
+-- |
+-- This functor is fully faithful, which is to say that given any function you can write
+-- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints
+-- that you can build.
+unmapDict :: (Dict a -> Dict b) -> a :- b
+unmapDict f = Sub (f Dict)
+
+type role Dict nominal
+
+--------------------------------------------------------------------------------
+-- Reflection
+--------------------------------------------------------------------------------
+
+-- | Reify the relationship between a class and its superclass constraints as a class
+--
+-- Given a definition such as
+--
+-- @
+-- class Foo a => Bar a
+-- @
+--
+-- you can capture the relationship between 'Bar a' and its superclass 'Foo a' with
+--
+-- @
+-- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict'
+-- @
+--
+-- Now the user can use 'cls :: Bar a :- Foo a'
+class Class b h | h -> b where
+  cls :: h :- b
+
+infixr 9 :=>
+-- | Reify the relationship between an instance head and its body as a class
+--
+-- Given a definition such as
+--
+-- @
+-- instance Foo a => Foo [a]
+-- @
+--
+-- you can capture the relationship between the instance head and its body with
+--
+-- @
+-- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict'
+-- @
+class b :=> h | h -> b where
+  ins :: b :- h
+
+-- Bootstrapping
+
+instance Class () (Class b a) where cls = Sub Dict
+instance Class () (b :=> a) where cls = Sub Dict
+
+instance Class b a => () :=> Class b a where ins = Sub Dict
+instance (b :=> a) => () :=> (b :=> a) where ins = Sub Dict
+
+instance Class () () where cls = Sub Dict
+instance () :=> () where ins = Sub Dict
+
+-- Local, Prelude, Applicative, C.M.I and Data.Monoid instances
+
+-- Eq
+instance Class () (Eq a) where cls = Sub Dict
+instance () :=> Eq () where ins = Sub Dict
+instance () :=> Eq Int where ins = Sub Dict
+instance () :=> Eq Bool where ins = Sub Dict
+instance () :=> Eq Integer where ins = Sub Dict
+instance () :=> Eq Float where ins = Sub Dict
+instance () :=> Eq Double where ins = Sub Dict
+instance Eq a :=> Eq [a] where ins = Sub Dict
+instance Eq a :=> Eq (Maybe a) where ins = Sub Dict
+instance Eq a :=> Eq (Complex a) where ins = Sub Dict
+instance Eq a :=> Eq (Ratio a) where ins = Sub Dict
+instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict
+instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict
+instance () :=> Eq (Dict a) where ins = Sub Dict
+instance () :=> Eq (a :- b) where ins = Sub Dict
+instance () :=> Eq Word where ins = Sub Dict
+instance Eq a :=> Eq (Identity a) where ins = Sub Dict
+instance Eq a :=> Eq (Const a b) where ins = Sub Dict
+instance () :=> Eq Natural where ins = Sub Dict
+
+-- Ord
+instance Class (Eq a) (Ord a) where cls = Sub Dict
+instance () :=> Ord () where ins = Sub Dict
+instance () :=> Ord Bool where ins = Sub Dict
+instance () :=> Ord Int where ins = Sub Dict
+instance ():=> Ord Integer where ins = Sub Dict
+instance () :=> Ord Float where ins = Sub Dict
+instance ():=> Ord Double where ins = Sub Dict
+instance () :=> Ord Char where ins = Sub Dict
+instance Ord a :=> Ord (Maybe a) where ins = Sub Dict
+instance Ord a :=> Ord [a] where ins = Sub Dict
+instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict
+instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict
+instance Integral a :=> Ord (Ratio a) where ins = Sub Dict
+instance () :=> Ord (Dict a) where ins = Sub Dict
+instance () :=> Ord (a :- b) where ins = Sub Dict
+instance () :=> Ord Word where ins = Sub Dict
+instance Ord a :=> Ord (Identity a) where ins = Sub Dict
+instance Ord a :=> Ord (Const a b) where ins = Sub Dict
+instance () :=> Ord Natural where ins = Sub Dict
+
+-- Show
+instance Class () (Show a) where cls = Sub Dict
+instance () :=> Show () where ins = Sub Dict
+instance () :=> Show Bool where ins = Sub Dict
+instance () :=> Show Ordering where ins = Sub Dict
+instance () :=> Show Char where ins = Sub Dict
+instance () :=> Show Int where ins = Sub Dict
+instance Show a :=> Show (Complex a) where ins = Sub Dict
+instance Show a :=> Show [a] where ins = Sub Dict
+instance Show a :=> Show (Maybe a) where ins = Sub Dict
+instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict
+instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict
+instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict
+instance () :=> Show (Dict a) where ins = Sub Dict
+instance () :=> Show (a :- b) where ins = Sub Dict
+instance () :=> Show Word where ins = Sub Dict
+instance Show a :=> Show (Identity a) where ins = Sub Dict
+instance Show a :=> Show (Const a b) where ins = Sub Dict
+instance () :=> Show Natural where ins = Sub Dict
+
+-- Read
+instance Class () (Read a) where cls = Sub Dict
+instance () :=> Read () where ins = Sub Dict
+instance () :=> Read Bool where ins = Sub Dict
+instance () :=> Read Ordering where ins = Sub Dict
+instance () :=> Read Char where ins = Sub Dict
+instance () :=> Read Int where ins = Sub Dict
+instance Read a :=> Read (Complex a) where ins = Sub Dict
+instance Read a :=> Read [a] where ins = Sub Dict
+instance Read a :=> Read (Maybe a) where ins = Sub Dict
+instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict
+instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict
+instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict
+instance () :=> Read Word where ins = Sub Dict
+instance Read a :=> Read (Identity a) where ins = Sub Dict
+instance Read a :=> Read (Const a b) where ins = Sub Dict
+instance () :=> Read Natural where ins = Sub Dict
+
+-- Enum
+instance Class () (Enum a) where cls = Sub Dict
+instance () :=> Enum () where ins = Sub Dict
+instance () :=> Enum Bool where ins = Sub Dict
+instance () :=> Enum Ordering where ins = Sub Dict
+instance () :=> Enum Char where ins = Sub Dict
+instance () :=> Enum Int where ins = Sub Dict
+instance () :=> Enum Integer where ins = Sub Dict
+instance () :=> Enum Float where ins = Sub Dict
+instance () :=> Enum Double where ins = Sub Dict
+instance Integral a :=> Enum (Ratio a) where ins = Sub Dict
+instance () :=> Enum Word where ins = Sub Dict
+instance Enum a :=> Enum (Identity a) where ins = Sub Dict
+instance Enum a :=> Enum (Const a b) where ins = Sub Dict
+instance () :=> Enum Natural where ins = Sub Dict
+
+-- Bounded
+instance Class () (Bounded a) where cls = Sub Dict
+instance () :=> Bounded () where ins = Sub Dict
+instance () :=> Bounded Ordering where ins = Sub Dict
+instance () :=> Bounded Bool where ins = Sub Dict
+instance () :=> Bounded Int where ins = Sub Dict
+instance () :=> Bounded Char where ins = Sub Dict
+instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict
+instance () :=> Bounded Word where ins = Sub Dict
+instance Bounded a :=> Bounded (Identity a) where ins = Sub Dict
+instance Bounded a :=> Bounded (Const a b) where ins = Sub Dict
+
+-- Num
+instance Class () (Num a) where cls = Sub Dict
+instance () :=> Num Int where ins = Sub Dict
+instance () :=> Num Integer where ins = Sub Dict
+instance () :=> Num Float where ins = Sub Dict
+instance () :=> Num Double where ins = Sub Dict
+instance RealFloat a :=> Num (Complex a) where ins = Sub Dict
+instance Integral a :=> Num (Ratio a) where ins = Sub Dict
+instance () :=> Num Word where ins = Sub Dict
+instance Num a :=> Num (Identity a) where ins = Sub Dict
+instance Num a :=> Num (Const a b) where ins = Sub Dict
+instance () :=> Num Natural where ins = Sub Dict
+
+-- Real
+instance Class (Num a, Ord a) (Real a) where cls = Sub Dict
+instance () :=> Real Int where ins = Sub Dict
+instance () :=> Real Integer where ins = Sub Dict
+instance () :=> Real Float where ins = Sub Dict
+instance () :=> Real Double where ins = Sub Dict
+instance Integral a :=> Real (Ratio a) where ins = Sub Dict
+instance () :=> Real Word where ins = Sub Dict
+instance Real a :=> Real (Identity a) where ins = Sub Dict
+instance Real a :=> Real (Const a b) where ins = Sub Dict
+instance () :=> Real Natural where ins = Sub Dict
+
+-- Integral
+instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict
+instance () :=> Integral Int where ins = Sub Dict
+instance () :=> Integral Integer where ins = Sub Dict
+instance () :=> Integral Word where ins = Sub Dict
+instance Integral a :=> Integral (Identity a) where ins = Sub Dict
+instance Integral a :=> Integral (Const a b) where ins = Sub Dict
+instance () :=> Integral Natural where ins = Sub Dict
+
+-- Bits
+instance Class (Eq a) (Bits a) where cls = Sub Dict
+instance () :=> Bits Bool where ins = Sub Dict
+instance () :=> Bits Int where ins = Sub Dict
+instance () :=> Bits Integer where ins = Sub Dict
+instance () :=> Bits Word where ins = Sub Dict
+instance Bits a :=> Bits (Identity a) where ins = Sub Dict
+instance Bits a :=> Bits (Const a b) where ins = Sub Dict
+instance () :=> Bits Natural where ins = Sub Dict
+
+-- Fractional
+instance Class (Num a) (Fractional a) where cls = Sub Dict
+instance () :=> Fractional Float where ins = Sub Dict
+instance () :=> Fractional Double where ins = Sub Dict
+instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict
+instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict
+instance Fractional a :=> Fractional (Identity a) where ins = Sub Dict
+instance Fractional a :=> Fractional (Const a b) where ins = Sub Dict
+
+-- Floating
+instance Class (Fractional a) (Floating a) where cls = Sub Dict
+instance () :=> Floating Float where ins = Sub Dict
+instance () :=> Floating Double where ins = Sub Dict
+instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict
+instance Floating a :=> Floating (Identity a) where ins = Sub Dict
+instance Floating a :=> Floating (Const a b) where ins = Sub Dict
+
+-- RealFrac
+instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict
+instance () :=> RealFrac Float where ins = Sub Dict
+instance () :=> RealFrac Double where ins = Sub Dict
+instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict
+instance RealFrac a :=> RealFrac (Identity a) where ins = Sub Dict
+instance RealFrac a :=> RealFrac (Const a b) where ins = Sub Dict
+
+-- RealFloat
+instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict
+instance () :=> RealFloat Float where ins = Sub Dict
+instance () :=> RealFloat Double where ins = Sub Dict
+instance RealFloat a :=> RealFloat (Identity a) where ins = Sub Dict
+instance RealFloat a :=> RealFloat (Const a b) where ins = Sub Dict
+
+-- Semigroup
+instance Class () (Semigroup a) where cls = Sub Dict
+instance () :=> Semigroup () where ins = Sub Dict
+instance () :=> Semigroup Ordering where ins = Sub Dict
+instance () :=> Semigroup [a] where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Maybe a) where ins = Sub Dict
+instance (Semigroup a, Semigroup b) :=> Semigroup (a, b) where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Const a b) where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Identity a) where ins = Sub Dict
+instance Semigroup a :=> Semigroup (IO a) where ins = Sub Dict
+
+-- Monoid
+instance Class (Semigroup a) (Monoid a) where cls = Sub Dict
+instance () :=> Monoid () where ins = Sub Dict
+instance () :=> Monoid Ordering where ins = Sub Dict
+instance () :=> Monoid [a] where ins = Sub Dict
+instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict
+instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict
+instance Monoid a :=> Monoid (Const a b) where ins = Sub Dict
+instance Monoid a :=> Monoid (Identity a) where ins = Sub Dict
+instance Monoid a :=> Monoid (IO a) where ins = Sub Dict
+
+-- Functor
+instance Class () (Functor f) where cls = Sub Dict
+instance () :=> Functor [] where ins = Sub Dict
+instance () :=> Functor Maybe where ins = Sub Dict
+instance () :=> Functor (Either a) where ins = Sub Dict
+instance () :=> Functor ((->) a) where ins = Sub Dict
+instance () :=> Functor ((,) a) where ins = Sub Dict
+instance () :=> Functor IO where ins = Sub Dict
+instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict
+instance () :=> Functor Identity where ins = Sub Dict
+instance () :=> Functor (Const a) where ins = Sub Dict
+
+-- Applicative
+instance Class (Functor f) (Applicative f) where cls = Sub Dict
+instance () :=> Applicative [] where ins = Sub Dict
+instance () :=> Applicative Maybe where ins = Sub Dict
+instance () :=> Applicative (Either a) where ins = Sub Dict
+instance () :=> Applicative ((->)a) where ins = Sub Dict
+instance () :=> Applicative IO where ins = Sub Dict
+instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict
+instance Monoid a :=> Applicative (Const a) where ins = Sub Dict
+instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict
+
+-- Alternative
+instance Class (Applicative f) (Alternative f) where cls = Sub Dict
+instance () :=> Alternative [] where ins = Sub Dict
+instance () :=> Alternative Maybe where ins = Sub Dict
+instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict
+
+-- Monad
+instance Class (Applicative f) (Monad f) where cls = Sub Dict
+instance () :=> Monad [] where ins = Sub Dict
+instance () :=> Monad ((->) a) where ins = Sub Dict
+instance () :=> Monad (Either a) where ins = Sub Dict
+instance () :=> Monad IO where ins = Sub Dict
+instance () :=> Monad Identity where ins = Sub Dict
+
+-- MonadPlus
+instance Class (Monad f, Alternative f) (MonadPlus f) where cls = Sub Dict
+instance () :=> MonadPlus [] where ins = Sub Dict
+instance () :=> MonadPlus Maybe where ins = Sub Dict
+
+--------------------------------------------------------------------------------
+-- UndecidableInstances
+--------------------------------------------------------------------------------
+
+instance a :=> Enum (Dict a) where ins = Sub Dict
+instance a => Enum (Dict a) where
+  toEnum _ = Dict
+  fromEnum Dict = 0
+
+instance a :=> Bounded (Dict a) where ins = Sub Dict
+instance a => Bounded (Dict a) where
+  minBound = Dict
+  maxBound = Dict
+
+instance a :=> Read (Dict a) where ins = Sub Dict
+deriving instance a => Read (Dict a)
+
+instance () :=> Semigroup (Dict a) where ins = Sub Dict
+instance Semigroup (Dict a) where
+  Dict <> Dict = Dict
+
+instance a :=> Monoid (Dict a) where ins = Sub Dict
+instance a => Monoid (Dict a) where
+  mempty = Dict
diff --git a/src/Data/Constraint/Char.hs b/src/Data/Constraint/Char.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Char.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE CPP #-}
+-- | Utilities for working with 'KnownChar' constraints.
+--
+-- This module is only available on GHC 9.2 or later.
+module Data.Constraint.Char
+  ( CharToNat
+  , NatToChar
+  , charToNat
+  , natToChar
+  ) where
+
+import Data.Char
+import Data.Constraint
+import Data.Proxy
+import GHC.TypeLits
+#if MIN_VERSION_base(4,18,0)
+import Data.Constraint.Unsafe
+import qualified GHC.TypeNats as TN
+#else
+import Unsafe.Coerce
+#endif
+
+-- implementation details
+
+#if !MIN_VERSION_base(4,18,0)
+newtype Magic c = Magic (KnownChar c => Dict (KnownChar c))
+#endif
+
+magicCN :: forall c n. (Char -> Int) -> KnownChar c :- KnownNat n
+#if MIN_VERSION_base(4,18,0)
+magicCN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (charVal (Proxy @c))))) Dict
+#else
+magicCN f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral @Int @Natural (f (charVal (Proxy @c))))
+#endif
+
+magicNC :: forall n c. (Int -> Char) -> KnownNat n :- KnownChar c
+#if MIN_VERSION_base(4,18,0)
+magicNC f = Sub $ withKnownChar (unsafeSChar @c (f (fromIntegral (natVal (Proxy @n))))) Dict
+#else
+magicNC f = Sub $ unsafeCoerce (Magic Dict) (f (fromIntegral (natVal (Proxy @n))))
+#endif
+
+-- operations
+
+charToNat :: forall c. KnownChar c :- KnownNat (CharToNat c)
+charToNat = magicCN ord
+
+-- NB: 0x10FFFF the maximum value for a Unicode code point. Calling `chr` on
+-- anything greater will throw an exception.
+natToChar :: forall n. (n <= 0x10FFFF, KnownNat n) :- KnownChar (NatToChar n)
+natToChar = Sub $ case magicNC @n @(NatToChar n) chr of Sub r -> r
diff --git a/src/Data/Constraint/Deferrable.hs b/src/Data/Constraint/Deferrable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Deferrable.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- |
+-- Copyright   :  (C) 2015-2021 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- The idea for this trick comes from Dimitrios Vytiniotis.
+
+module Data.Constraint.Deferrable
+  ( UnsatisfiedConstraint(..)
+  , Deferrable(..)
+  , defer
+  , deferred
+  , (:~~:)(HRefl)
+  , (:~:)(Refl)
+  ) where
+
+import Control.Exception
+import Control.Monad
+import Data.Constraint
+import Data.Proxy
+import Data.Typeable (Typeable, cast, typeRep)
+import Data.Type.Equality ((:~:)(Refl))
+
+import Data.Type.Equality (type (~~), (:~~:)(HRefl))
+
+newtype UnsatisfiedConstraint = UnsatisfiedConstraint String
+  deriving Show
+
+instance Exception UnsatisfiedConstraint
+
+-- | Allow an attempt at resolution of a constraint at a later time
+class Deferrable p where
+  -- | Resolve a 'Deferrable' constraint with observable failure.
+  deferEither :: (p => r) -> Either String r
+
+deferred :: forall p. Deferrable p :- p
+deferred = Sub $ defer @p Dict
+
+defer :: forall p r. Deferrable p => (p => r) -> r
+defer r = either (throw . UnsatisfiedConstraint) id $ deferEither @p r
+
+showTypeRep :: forall t. Typeable t => String
+showTypeRep = show $ typeRep (Proxy @t)
+
+instance Deferrable () where
+  deferEither r = Right r
+
+-- | Deferrable homogeneous equality constraints.
+--
+-- Note that due to a GHC bug (https://ghc.haskell.org/trac/ghc/ticket/10343),
+-- using this instance on GHC 7.10 will only work with @*@-kinded types.
+instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where
+  deferEither r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of
+    Just Refl -> Right r
+    Nothing   -> Left $
+      "deferred type equality: type mismatch between `" ++ showTypeRep @a ++ "’ and `"  ++ showTypeRep @b ++ "'"
+
+-- | Deferrable heterogenous equality constraints.
+--
+-- Only available on GHC 8.0 or later.
+instance (Typeable i, Typeable j, Typeable (a :: i), Typeable (b :: j)) => Deferrable (a ~~ b) where
+  deferEither r = case cast (HRefl :: a :~~: a) :: Maybe (a :~~: b) of
+    Just HRefl -> Right r
+    Nothing   -> Left $
+      "deferred type equality: type mismatch between `" ++ showTypeRep @a ++ "’ and `"  ++ showTypeRep @b ++ "'"
+
+instance (Deferrable a, Deferrable b) => Deferrable (a, b) where
+  deferEither r = join $ deferEither @a $ deferEither @b r
+
+instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where
+  deferEither r = join $ deferEither @a $ join $ deferEither @b $ deferEither @c r
diff --git a/src/Data/Constraint/Forall.hs b/src/Data/Constraint/Forall.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Forall.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE GADTs #-}
+
+-- |
+-- Copyright   :  (C) 2011-2021 Edward Kmett,
+--                (C) 2015 Ørjan Johansen,
+--                (C) 2016 David Feuer
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module uses a trick to provide quantification over constraints.
+
+module Data.Constraint.Forall
+  ( Forall, inst
+  , ForallF, instF
+  , Forall1, inst1
+  , ForallT, instT
+  , ForallV, InstV (instV)
+  , forall_
+  ) where
+
+import Data.Constraint
+import Unsafe.Coerce (unsafeCoerce)
+
+class (forall a. p a) => Forall (p :: k -> Constraint)
+instance (forall a. p a) => Forall (p :: k -> Constraint)
+
+-- | Instantiate a quantified @'Forall' p@ constraint at type @a@.
+inst :: forall p a. Forall p :- p a
+inst = Sub Dict
+
+data Dict1 p where
+  Dict1 :: (forall a. p a) => Dict1 p
+
+forallish :: forall p. Dict1 p -> Dict (Forall p)
+forallish Dict1 = Dict
+
+forall_ :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
+forall_ d = forallish (unsafeCoerce d)
+
+-- | Composition for constraints.
+class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)
+instance p (f a) => ComposeC p f a
+
+-- | A representation of the quantified constraint @forall a. p (f a)@.
+class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
+instance Forall (ComposeC p f) => ForallF p f
+
+-- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@.
+instF :: forall p f a . ForallF p f :- p (f a)
+instF = Sub $
+  case inst :: Forall (ComposeC p f) :- ComposeC p f a of
+    Sub Dict -> Dict
+
+-- Classes building up to ForallT
+class p (t a b) => R (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1) (b :: k2)
+instance p (t a b) => R p t a b
+class Forall (R p t a) => Q (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1)
+instance Forall (R p t a) => Q p t a
+
+-- | A representation of the quantified constraint @forall f a. p (t f a)@.
+class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
+instance Forall (Q p t) => ForallT p t
+
+-- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.
+instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
+instT = Sub $
+  case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->
+  case inst :: Forall (R p t f) :- R p t f a of
+    Sub Dict -> Dict }
+
+type Forall1 p = Forall p
+-- | Instantiate a quantified constraint on kind @* -> *@.
+-- This is now redundant since @'inst'@ became polykinded.
+inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
+inst1 = inst
+
+-- | A representation of the quantified constraint
+-- @forall a1 a2 ... an . p a1 a2 ... an@, supporting a variable number of
+-- parameters.
+type family ForallV :: k -> Constraint
+type instance ForallV = ForallV_
+
+class ForallV' p => ForallV_ (p :: k)
+instance ForallV' p => ForallV_ p
+
+-- | Instantiate a quantified @'ForallV' p@ constraint as @c@, where
+-- @c ~ p a1 a2 ... an@.
+class InstV (p :: k) c | k c -> p where
+  type ForallV' (p :: k) :: Constraint
+  instV :: ForallV p :- c
+
+instance p ~ c => InstV (p :: Constraint) c where
+  type ForallV' (p :: Constraint) = p
+  instV = Sub Dict
+
+-- Treating 1 argument specially rather than recursing as a bit of (premature?)
+-- optimization
+instance p a ~ c => InstV (p :: k -> Constraint) c where
+  type ForallV' (p :: k -> Constraint) = Forall p
+  instV = Sub $ case inst :: Forall p :- c of
+    Sub Dict -> Dict
+
+instance InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c where
+  type ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p
+  instV = Sub $ case instF :: ForallF ForallV p :- ForallV (p a) of
+    Sub Dict -> case instV :: ForallV (p a) :- c of
+      Sub Dict -> Dict
+
diff --git a/src/Data/Constraint/Lifting.hs b/src/Data/Constraint/Lifting.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Lifting.hs
@@ -0,0 +1,404 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Data.Constraint.Lifting
+  ( Lifting(..)
+  , Lifting2(..)
+  ) where
+
+import Control.Applicative
+import Control.Applicative.Backwards
+import Control.Applicative.Lift
+import Control.DeepSeq
+import Control.Monad
+import Control.Monad.Cont.Class
+import Control.Monad.Error.Class
+import Control.Monad.Fix
+import Control.Monad.IO.Class
+import Control.Monad.RWS.Class
+import Control.Monad.Trans.Cont
+import Control.Monad.Trans.Except
+import Control.Monad.Trans.Identity
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.RWS.Lazy as Lazy
+import Control.Monad.Trans.RWS.Strict as Strict
+import Control.Monad.Trans.State.Lazy as Lazy
+import Control.Monad.Trans.State.Strict as Strict
+import Control.Monad.Trans.Writer.Lazy as Lazy
+import Control.Monad.Trans.Writer.Strict as Strict
+import Data.Binary
+import Data.Complex
+import Data.Constraint
+import Data.Functor.Classes
+import Data.Functor.Compose as Functor
+import Data.Functor.Identity
+import Data.Functor.Product as Functor
+import Data.Functor.Reverse as Functor
+import Data.Functor.Sum as Functor
+import Data.Hashable
+import Data.Ratio
+import GHC.Arr
+
+class Lifting p f where
+  lifting :: p a :- p (f a)
+
+instance Lifting Eq [] where lifting = Sub Dict
+instance Lifting Ord [] where lifting = Sub Dict
+instance Lifting Show [] where lifting = Sub Dict
+instance Lifting Read [] where lifting = Sub Dict
+instance Lifting Hashable [] where lifting = Sub Dict
+instance Lifting Binary [] where lifting = Sub Dict
+instance Lifting NFData [] where lifting = Sub Dict
+
+instance Lifting Eq Maybe where lifting = Sub Dict
+instance Lifting Ord Maybe where lifting = Sub Dict
+instance Lifting Show Maybe where lifting = Sub Dict
+instance Lifting Read Maybe where lifting = Sub Dict
+instance Lifting Hashable Maybe where lifting = Sub Dict
+instance Lifting Binary Maybe where lifting = Sub Dict
+instance Lifting NFData Maybe where lifting = Sub Dict
+instance Lifting Semigroup Maybe where lifting = Sub Dict
+instance Lifting Monoid Maybe where lifting = Sub Dict
+
+instance Lifting Eq Ratio where lifting = Sub Dict
+-- instance Lifting Show Ratio where lifting = Sub Dict -- requires 7.10
+
+instance Lifting Eq Complex where lifting = Sub Dict
+instance Lifting Read Complex where lifting = Sub Dict
+instance Lifting Show Complex where lifting = Sub Dict
+instance Lifting Semigroup ((->) a) where lifting = Sub Dict
+instance Lifting Monoid ((->) a) where lifting = Sub Dict
+
+instance Eq a => Lifting Eq (Either a) where lifting = Sub Dict
+instance Ord a => Lifting Ord (Either a) where lifting = Sub Dict
+instance Show a => Lifting Show (Either a) where lifting = Sub Dict
+instance Read a => Lifting Read (Either a) where lifting = Sub Dict
+instance Hashable a => Lifting Hashable (Either a) where lifting = Sub Dict
+instance Binary a => Lifting Binary (Either a) where lifting = Sub Dict
+instance NFData a => Lifting NFData (Either a) where lifting = Sub Dict
+
+instance Eq a => Lifting Eq ((,) a) where lifting = Sub Dict
+instance Ord a => Lifting Ord ((,) a) where lifting = Sub Dict
+instance Show a => Lifting Show ((,) a) where lifting = Sub Dict
+instance Read a => Lifting Read ((,) a) where lifting = Sub Dict
+instance Hashable a => Lifting Hashable ((,) a) where lifting = Sub Dict
+instance Binary a => Lifting Binary ((,) a) where lifting = Sub Dict
+instance NFData a => Lifting NFData ((,) a) where lifting = Sub Dict
+instance Semigroup a => Lifting Semigroup ((,) a) where lifting = Sub Dict
+instance Monoid a => Lifting Monoid ((,) a) where lifting = Sub Dict
+instance Bounded a => Lifting Bounded ((,) a) where lifting = Sub Dict
+instance Ix a => Lifting Ix ((,) a) where lifting = Sub Dict
+
+instance Functor f => Lifting Functor (Compose f) where lifting = Sub Dict
+instance Foldable f => Lifting Foldable (Compose f) where lifting = Sub Dict
+instance Traversable f => Lifting Traversable (Compose f) where lifting = Sub Dict
+instance Applicative f => Lifting Applicative (Compose f) where lifting = Sub Dict
+instance Alternative f => Lifting Alternative (Compose f) where lifting = Sub Dict -- overconstrained
+
+instance Show1 f => Lifting Show1 (Compose f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq1 (Compose f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord1 (Compose f) where lifting = Sub Dict
+instance Read1 f => Lifting Read1 (Compose f) where lifting = Sub Dict
+instance (Eq1 f, Eq1 g) => Lifting Eq (Compose f g) where lifting = Sub Dict
+instance (Ord1 f, Ord1 g) => Lifting Ord (Compose f g) where lifting = Sub Dict
+instance (Read1 f, Read1 g) => Lifting Read (Compose f g) where lifting = Sub Dict
+instance (Show1 f, Show1 g) => Lifting Show (Compose f g) where lifting = Sub Dict
+
+instance Functor f => Lifting Functor (Functor.Product f) where lifting = Sub Dict
+instance Foldable f => Lifting Foldable (Functor.Product f) where lifting = Sub Dict
+instance Traversable f => Lifting Traversable (Functor.Product f) where lifting = Sub Dict
+instance Applicative f => Lifting Applicative (Functor.Product f) where lifting = Sub Dict
+instance Alternative f => Lifting Alternative (Functor.Product f) where lifting = Sub Dict
+instance Monad f => Lifting Monad (Functor.Product f) where lifting = Sub Dict
+instance MonadFix f => Lifting MonadFix (Functor.Product f) where lifting = Sub Dict
+instance MonadPlus f => Lifting MonadPlus (Functor.Product f) where lifting = Sub Dict
+instance Show1 f => Lifting Show1 (Functor.Product f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq1 (Functor.Product f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord1 (Functor.Product f) where lifting = Sub Dict
+instance Read1 f => Lifting Read1 (Functor.Product f) where lifting = Sub Dict
+instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Product f g) where lifting = Sub Dict
+instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Product f g) where lifting = Sub Dict
+instance (Read1 f, Read1 g) => Lifting Read (Functor.Product f g) where lifting = Sub Dict
+instance (Show1 f, Show1 g) => Lifting Show (Functor.Product f g) where lifting = Sub Dict
+
+instance Functor f => Lifting Functor (Functor.Sum f) where lifting = Sub Dict
+instance Foldable f => Lifting Foldable (Functor.Sum f) where lifting = Sub Dict
+instance Traversable f => Lifting Traversable (Functor.Sum f) where lifting = Sub Dict
+instance Show1 f => Lifting Show1 (Functor.Sum f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq1 (Functor.Sum f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord1 (Functor.Sum f) where lifting = Sub Dict
+instance Read1 f => Lifting Read1 (Functor.Sum f) where lifting = Sub Dict
+instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Sum f g) where lifting = Sub Dict
+instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Sum f g) where lifting = Sub Dict
+instance (Read1 f, Read1 g) => Lifting Read (Functor.Sum f g) where lifting = Sub Dict
+instance (Show1 f, Show1 g) => Lifting Show (Functor.Sum f g) where lifting = Sub Dict
+
+instance Lifting Functor (Strict.StateT s) where lifting = Sub Dict
+instance Lifting Monad (Strict.StateT s) where lifting = Sub Dict
+instance Lifting MonadFix (Strict.StateT s) where lifting = Sub Dict
+instance Lifting MonadIO (Strict.StateT s) where lifting = Sub Dict
+instance Lifting MonadPlus (Strict.StateT s) where lifting = Sub Dict
+
+instance Lifting Functor (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting Monad (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting MonadFix (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting MonadIO (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting MonadPlus (Lazy.StateT s) where lifting = Sub Dict
+
+instance Lifting Functor (Lazy.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting Monad (Lazy.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadFix (Lazy.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadPlus (Lazy.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadIO (Lazy.RWST r w s) where lifting = Sub Dict
+
+instance Lifting Functor (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting Monad (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadFix (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadPlus (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadIO (Strict.RWST r w s) where lifting = Sub Dict
+
+instance Lifting Functor (ReaderT e) where lifting = Sub Dict
+instance Lifting Applicative (ReaderT e) where lifting = Sub Dict
+instance Lifting Alternative (ReaderT e) where lifting = Sub Dict
+instance Lifting Monad (ReaderT e) where lifting = Sub Dict
+instance Lifting MonadPlus (ReaderT e) where lifting = Sub Dict
+instance Lifting MonadFix (ReaderT e) where lifting = Sub Dict
+instance Lifting MonadIO (ReaderT e) where lifting = Sub Dict
+
+instance Lifting Functor (ExceptT e) where lifting = Sub Dict
+instance Lifting Foldable (ExceptT e) where lifting = Sub Dict
+instance Lifting Traversable (ExceptT e) where lifting = Sub Dict
+instance Lifting Monad (ExceptT e) where lifting = Sub Dict
+instance Lifting MonadFix (ExceptT e) where lifting = Sub Dict
+instance Monoid e => Lifting MonadPlus (ExceptT e) where lifting = Sub Dict -- overconstrained!
+instance Lifting MonadIO (ExceptT e) where lifting = Sub Dict
+instance Show e => Lifting Show1 (ExceptT e) where lifting = Sub Dict
+instance Eq e => Lifting Eq1 (ExceptT e) where lifting = Sub Dict
+instance Ord e => Lifting Ord1 (ExceptT e) where lifting = Sub Dict
+instance Read e => Lifting Read1 (ExceptT e) where lifting = Sub Dict
+instance (Show e, Show1 m) => Lifting Show (ExceptT e m) where lifting = Sub Dict
+instance (Eq e, Eq1 m) => Lifting Eq (ExceptT e m) where lifting = Sub Dict
+instance (Ord e, Ord1 m) => Lifting Ord (ExceptT e m) where lifting = Sub Dict
+instance (Read e, Read1 m) => Lifting Read (ExceptT e m) where lifting = Sub Dict
+
+instance Lifting Functor (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Applicative (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Alternative (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Monad (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadFix (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadPlus (Strict.WriterT w) where lifting = Sub Dict
+instance Lifting Foldable (Strict.WriterT w) where lifting = Sub Dict
+instance Lifting Traversable (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadIO (Strict.WriterT w) where lifting = Sub Dict
+instance Show w => Lifting Show1 (Strict.WriterT w) where lifting = Sub Dict
+instance Eq w => Lifting Eq1 (Strict.WriterT w) where lifting = Sub Dict
+instance Ord w => Lifting Ord1 (Strict.WriterT w) where lifting = Sub Dict
+instance Read w => Lifting Read1 (Strict.WriterT w) where lifting = Sub Dict
+instance (Show w, Show1 m) => Lifting Show (Strict.WriterT w m) where lifting = Sub Dict
+instance (Eq w, Eq1 m) => Lifting Eq (Strict.WriterT w m) where lifting = Sub Dict
+instance (Ord w, Ord1 m) => Lifting Ord (Strict.WriterT w m) where lifting = Sub Dict
+instance (Read w, Read1 m) => Lifting Read (Strict.WriterT w m) where lifting = Sub Dict
+
+instance Lifting Functor (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Applicative (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Alternative (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting Monad (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadFix (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadPlus (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting Foldable (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting Traversable (Lazy.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadIO (Lazy.WriterT w) where lifting = Sub Dict
+instance Show w => Lifting Show1 (Lazy.WriterT w) where lifting = Sub Dict
+instance Eq w => Lifting Eq1 (Lazy.WriterT w) where lifting = Sub Dict
+instance Ord w => Lifting Ord1 (Lazy.WriterT w) where lifting = Sub Dict
+instance Read w => Lifting Read1 (Lazy.WriterT w) where lifting = Sub Dict
+instance (Show w, Show1 m) => Lifting Show (Lazy.WriterT w m) where lifting = Sub Dict
+instance (Eq w, Eq1 m) => Lifting Eq (Lazy.WriterT w m) where lifting = Sub Dict
+instance (Ord w, Ord1 m) => Lifting Ord (Lazy.WriterT w m) where lifting = Sub Dict
+instance (Read w, Read1 m) => Lifting Read (Lazy.WriterT w m) where lifting = Sub Dict
+
+instance Lifting Functor (ContT r) where lifting = Sub Dict -- overconstrained
+instance Lifting Applicative (ContT r) where lifting = Sub Dict -- overconstrained
+instance Lifting Monad (ContT r) where lifting = Sub Dict -- overconstrained
+instance Lifting MonadIO (ContT r) where lifting = Sub Dict
+
+instance Lifting Functor IdentityT where lifting = Sub Dict
+instance Lifting Applicative IdentityT where lifting = Sub Dict
+instance Lifting Alternative IdentityT where lifting = Sub Dict
+instance Lifting Monad IdentityT where lifting = Sub Dict
+instance Lifting MonadPlus IdentityT where lifting = Sub Dict
+instance Lifting MonadFix IdentityT where lifting = Sub Dict
+instance Lifting Foldable IdentityT where lifting = Sub Dict
+instance Lifting Traversable IdentityT where lifting = Sub Dict
+instance Lifting MonadIO IdentityT where lifting = Sub Dict
+instance Lifting Show1 IdentityT where lifting = Sub Dict
+instance Lifting Read1 IdentityT where lifting = Sub Dict
+instance Lifting Ord1 IdentityT where lifting = Sub Dict
+instance Lifting Eq1 IdentityT where lifting = Sub Dict
+instance Show1 m => Lifting Show (IdentityT m) where lifting = Sub Dict
+instance Read1 m => Lifting Read (IdentityT m) where lifting = Sub Dict
+instance Ord1 m => Lifting Ord (IdentityT m) where lifting = Sub Dict
+instance Eq1 m => Lifting Eq (IdentityT m) where lifting = Sub Dict
+
+instance Lifting Functor MaybeT where lifting = Sub Dict
+instance Lifting Monad MaybeT where lifting = Sub Dict
+-- instance Lifting MonadFix MaybeT where lifting = Sub Dict
+instance Lifting MonadPlus MaybeT where lifting = Sub Dict -- overconstrained
+instance Lifting Foldable MaybeT where lifting = Sub Dict
+instance Lifting Traversable MaybeT where lifting = Sub Dict
+instance Lifting MonadIO MaybeT where lifting = Sub Dict
+instance Lifting Show1 MaybeT where lifting = Sub Dict
+instance Lifting Read1 MaybeT where lifting = Sub Dict
+instance Lifting Ord1 MaybeT where lifting = Sub Dict
+instance Lifting Eq1 MaybeT where lifting = Sub Dict
+instance Show1 m => Lifting Show (MaybeT m) where lifting = Sub Dict
+instance Read1 m => Lifting Read (MaybeT m) where lifting = Sub Dict
+instance Ord1 m => Lifting Ord (MaybeT m) where lifting = Sub Dict
+instance Eq1 m => Lifting Eq (MaybeT m) where lifting = Sub Dict
+
+instance Lifting Functor Reverse where lifting = Sub Dict
+instance Lifting Applicative Reverse where lifting = Sub Dict
+instance Lifting Alternative Reverse where lifting = Sub Dict
+instance Lifting Foldable Reverse where lifting = Sub Dict
+instance Lifting Traversable Reverse where lifting = Sub Dict
+instance Lifting Show1 Reverse where lifting = Sub Dict
+instance Lifting Read1 Reverse where lifting = Sub Dict
+instance Lifting Ord1 Reverse where lifting = Sub Dict
+instance Lifting Eq1 Reverse where lifting = Sub Dict
+instance Show1 f => Lifting Show (Reverse f) where lifting = Sub Dict
+instance Read1 f => Lifting Read (Reverse f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord (Reverse f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq (Reverse f) where lifting = Sub Dict
+
+instance Lifting Functor Backwards where lifting = Sub Dict
+instance Lifting Foldable Backwards where lifting = Sub Dict
+instance Lifting Traversable Backwards where lifting = Sub Dict
+instance Lifting Applicative Backwards where lifting = Sub Dict
+instance Lifting Alternative Backwards where lifting = Sub Dict
+instance Lifting Show1 Backwards where lifting = Sub Dict
+instance Lifting Read1 Backwards where lifting = Sub Dict
+instance Lifting Ord1 Backwards where lifting = Sub Dict
+instance Lifting Eq1 Backwards where lifting = Sub Dict
+instance Show1 f => Lifting Show (Backwards f) where lifting = Sub Dict
+instance Read1 f => Lifting Read (Backwards f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord (Backwards f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq (Backwards f) where lifting = Sub Dict
+
+instance Lifting Functor Lift where lifting = Sub Dict
+instance Lifting Foldable Lift where lifting = Sub Dict
+instance Lifting Traversable Lift where lifting = Sub Dict
+instance Lifting Applicative Lift where lifting = Sub Dict
+instance Lifting Alternative Lift where lifting = Sub Dict
+instance Lifting Show1 Lift where lifting = Sub Dict
+instance Lifting Read1 Lift where lifting = Sub Dict
+instance Lifting Ord1 Lift where lifting = Sub Dict
+instance Lifting Eq1 Lift where lifting = Sub Dict
+instance Show1 f => Lifting Show (Lift f) where lifting = Sub Dict
+instance Read1 f => Lifting Read (Lift f) where lifting = Sub Dict
+instance Ord1 f => Lifting Ord (Lift f) where lifting = Sub Dict
+instance Eq1 f => Lifting Eq (Lift f) where lifting = Sub Dict
+
+instance Lifting Eq Identity where lifting = Sub Dict
+instance Lifting Ord Identity where lifting = Sub Dict
+instance Lifting Show Identity where lifting = Sub Dict
+instance Lifting Read Identity where lifting = Sub Dict
+
+instance Lifting MonadCont MaybeT where lifting = Sub Dict
+instance Lifting MonadCont IdentityT where lifting = Sub Dict
+instance Monoid w => Lifting MonadCont (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting MonadCont (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting MonadCont (ExceptT w) where lifting = Sub Dict
+instance Lifting MonadCont (Strict.StateT s) where lifting = Sub Dict
+instance Lifting MonadCont (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting MonadCont (ReaderT e) where lifting = Sub Dict
+instance Monoid w => Lifting MonadCont (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting MonadCont (Lazy.RWST r w s) where lifting = Sub Dict
+
+instance Lifting (MonadError e) MaybeT where lifting = Sub Dict
+instance Lifting (MonadError e) IdentityT where lifting = Sub Dict
+instance Monoid w => Lifting (MonadError e) (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting (MonadError e) (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting (MonadError e) (Strict.StateT s) where lifting = Sub Dict
+instance Lifting (MonadError e) (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting (MonadError e) (ReaderT r) where lifting = Sub Dict
+instance Monoid w => Lifting (MonadError e) (Strict.RWST r w s) where lifting = Sub Dict
+instance Monoid w => Lifting (MonadError e) (Lazy.RWST r w s) where lifting = Sub Dict
+
+instance Lifting (MonadRWS r w s) MaybeT where lifting = Sub Dict
+instance Lifting (MonadRWS r w s) IdentityT where lifting = Sub Dict
+instance Lifting (MonadRWS r w s) (ExceptT e) where lifting = Sub Dict
+
+instance Lifting (MonadReader r) MaybeT where lifting = Sub Dict
+instance Lifting (MonadReader r) IdentityT where lifting = Sub Dict
+instance Monoid w => Lifting (MonadReader r) (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting (MonadReader r) (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting (MonadReader r) (Strict.StateT s) where lifting = Sub Dict
+instance Lifting (MonadReader r) (Lazy.StateT s) where lifting = Sub Dict
+instance Lifting (MonadReader r) (ExceptT e) where lifting = Sub Dict
+instance Lifting (MonadReader r) (ContT r') where lifting = Sub Dict
+
+instance Lifting (MonadState s) MaybeT where lifting = Sub Dict
+instance Lifting (MonadState s) IdentityT where lifting = Sub Dict
+instance Monoid w => Lifting (MonadState s) (Strict.WriterT w) where lifting = Sub Dict
+instance Monoid w => Lifting (MonadState s) (Lazy.WriterT w) where lifting = Sub Dict
+instance Lifting (MonadState s) (ReaderT r) where lifting = Sub Dict
+instance Lifting (MonadState s) (ExceptT e) where lifting = Sub Dict
+instance Lifting (MonadState s) (ContT r') where lifting = Sub Dict
+
+class Lifting2 p f where
+  lifting2 :: p a :- Lifting p (f a) -- (p a, p b) :- p (f a b)
+
+instance Lifting2 Eq Either where lifting2 = Sub Dict
+instance Lifting2 Ord Either where lifting2 = Sub Dict
+instance Lifting2 Show Either where lifting2 = Sub Dict
+instance Lifting2 Read Either where lifting2 = Sub Dict
+instance Lifting2 Hashable Either where lifting2 = Sub Dict
+instance Lifting2 Binary Either where lifting2 = Sub Dict
+instance Lifting2 NFData Either where lifting2 = Sub Dict
+
+instance Lifting2 Eq (,) where lifting2 = Sub Dict
+instance Lifting2 Ord (,) where lifting2 = Sub Dict
+instance Lifting2 Show (,) where lifting2 = Sub Dict
+instance Lifting2 Read (,) where lifting2 = Sub Dict
+instance Lifting2 Hashable (,) where lifting2 = Sub Dict
+instance Lifting2 Binary (,) where lifting2 = Sub Dict
+instance Lifting2 NFData (,) where lifting2 = Sub Dict
+instance Lifting2 Semigroup (,) where lifting2 = Sub Dict
+instance Lifting2 Monoid (,) where lifting2 = Sub Dict
+instance Lifting2 Bounded (,) where lifting2 = Sub Dict
+instance Lifting2 Ix (,) where lifting2 = Sub Dict
+
+instance Lifting2 Functor Compose where lifting2 = Sub Dict
+instance Lifting2 Foldable Compose where lifting2 = Sub Dict
+instance Lifting2 Traversable Compose where lifting2 = Sub Dict
+instance Lifting2 Applicative Compose where lifting2 = Sub Dict
+instance Lifting2 Alternative Compose where lifting2 = Sub Dict -- overconstrained
+
+instance Lifting2 Functor Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Foldable Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Traversable Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Applicative Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Alternative Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Monad Functor.Product where lifting2 = Sub Dict
+instance Lifting2 MonadPlus Functor.Product where lifting2 = Sub Dict
+instance Lifting2 MonadFix Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Show1 Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Eq1 Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Ord1 Functor.Product where lifting2 = Sub Dict
+instance Lifting2 Read1 Functor.Product where lifting2 = Sub Dict
+
+instance Lifting2 Functor Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Foldable Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Traversable Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Show1 Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Eq1 Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Ord1 Functor.Sum where lifting2 = Sub Dict
+instance Lifting2 Read1 Functor.Sum where lifting2 = Sub Dict
diff --git a/src/Data/Constraint/Nat.hs b/src/Data/Constraint/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Nat.hs
@@ -0,0 +1,396 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NoStarIsType #-}
+-- | Utilities for working with 'KnownNat' constraints.
+--
+-- This module is only available on GHC 8.0 or later.
+module Data.Constraint.Nat
+  ( Min, Max, Lcm, Gcd, Divides, Div, Mod, Log2
+  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat, log2Nat
+  , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne
+  , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates
+  , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes
+  , plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm
+  , minDistributesOverPlus, minDistributesOverTimes, minDistributesOverPow1, minDistributesOverPow2, minDistributesOverMax
+  , maxDistributesOverPlus, maxDistributesOverTimes, maxDistributesOverPow1, maxDistributesOverPow2, maxDistributesOverMin
+  , gcdDistributesOverLcm, lcmDistributesOverGcd
+  , minIsIdempotent, maxIsIdempotent, lcmIsIdempotent, gcdIsIdempotent
+  , plusIsCancellative, timesIsCancellative
+  , dividesPlus, dividesTimes, dividesMin, dividesMax, dividesPow, dividesGcd, dividesLcm
+  , plusMonotone1, plusMonotone2
+  , timesMonotone1, timesMonotone2
+  , powMonotone1, powMonotone2
+  , minMonotone1, minMonotone2
+  , maxMonotone1, maxMonotone2
+  , divMonotone1, divMonotone2
+  , euclideanNat
+  , plusMod, timesMod
+  , modBound
+  , log2Pow
+  , dividesDef
+  , timesDiv
+  , eqLe, leEq, leId, leTrans
+  , leZero, zeroLe
+  , plusMinusInverse1, plusMinusInverse2, plusMinusInverse3
+  ) where
+
+import Data.Constraint
+import Data.Constraint.Unsafe
+import Data.Proxy
+import Data.Type.Bool
+import GHC.TypeNats
+import qualified Numeric.Natural as Nat
+
+#if MIN_VERSION_base(4,15,0)
+import GHC.Num.Natural (naturalLog2)
+#else
+import GHC.Exts (Int(..))
+import GHC.Integer.Logarithms (integerLog2#)
+#endif
+
+#if !MIN_VERSION_base(4,18,0)
+import Unsafe.Coerce
+#endif
+
+type family Min (m::Nat) (n::Nat) :: Nat where
+    Min m n = If (n <=? m) n m
+type family Max (m::Nat) (n::Nat) :: Nat where
+    Max m n = If (n <=? m) m n
+type family Gcd (m::Nat) (n::Nat) :: Nat where
+    Gcd m m = m
+type family Lcm (m::Nat) (n::Nat) :: Nat where
+   Lcm m m = m
+
+type Divides n m = n ~ Gcd n m
+
+#if !MIN_VERSION_base(4,18,0)
+newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
+#endif
+
+magicNNN :: forall n m o. (Nat.Natural -> Nat.Natural -> Nat.Natural) -> (KnownNat n, KnownNat m) :- KnownNat o
+#if MIN_VERSION_base(4,18,0)
+magicNNN f = Sub $ withKnownNat @o (unsafeSNat (natVal (Proxy @n) `f` natVal (Proxy @m))) Dict
+#else
+magicNNN f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))
+#endif
+
+magicNN :: forall n m. (Nat.Natural -> Nat.Natural) -> KnownNat n :- KnownNat m
+#if MIN_VERSION_base(4,18,0)
+magicNN f = Sub $ withKnownNat @m (unsafeSNat (f (natVal (Proxy @n)))) Dict
+#else
+magicNN f = Sub $ unsafeCoerce (Magic Dict) (f (natVal (Proxy :: Proxy n)))
+#endif
+
+axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
+axiomLe = unsafeAxiom
+
+eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
+eqLe = Sub Dict
+
+dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
+dividesGcd = Sub unsafeAxiom
+
+dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c
+dividesLcm = Sub unsafeAxiom
+
+gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)
+gcdCommutes = unsafeAxiom
+
+lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)
+lcmCommutes = unsafeAxiom
+
+gcdZero :: forall a. Dict (Gcd 0 a ~ a)
+gcdZero = unsafeAxiom
+
+gcdOne :: forall a. Dict (Gcd 1 a ~ 1)
+gcdOne = unsafeAxiom
+
+lcmZero :: forall a. Dict (Lcm 0 a ~ 0)
+lcmZero = unsafeAxiom
+
+lcmOne :: forall a. Dict (Lcm 1 a ~ a)
+lcmOne = unsafeAxiom
+
+gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
+gcdNat = magicNNN gcd
+
+lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
+lcmNat = magicNNN lcm
+
+plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
+plusNat = magicNNN (+)
+
+minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
+minusNat = Sub $ case magicNNN @n @m (-) of Sub r -> r
+
+minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
+minNat = magicNNN min
+
+maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
+maxNat = magicNNN max
+
+timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
+timesNat = magicNNN (*)
+
+powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
+powNat = magicNNN (^)
+
+divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
+divNat = Sub $ case magicNNN @n @m div of Sub r -> r
+
+modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
+modNat = Sub $ case magicNNN @n @m mod of Sub r -> r
+
+log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
+log2Nat = Sub $ case magicNN @n log2 of Sub r -> r
+  where
+    log2 :: Nat.Natural -> Nat.Natural
+#if MIN_VERSION_base(4,15,0)
+    log2 n = fromIntegral (naturalLog2 n)
+#else
+    log2 n = fromIntegral (I# (integerLog2# (toInteger n)))
+#endif
+
+plusZero :: forall n. Dict ((n + 0) ~ n)
+plusZero = Dict
+
+minusZero :: forall n. Dict ((n - 0) ~ n)
+minusZero = Dict
+
+timesZero :: forall n. Dict ((n * 0) ~ 0)
+timesZero = Dict
+
+timesOne :: forall n. Dict ((n * 1) ~ n)
+timesOne = Dict
+
+minZero :: forall n. Dict (Min n 0 ~ 0)
+#if MIN_VERSION_base(4,16,0)
+minZero = unsafeAxiom
+#else
+minZero = Dict
+#endif
+
+maxZero :: forall n. Dict (Max n 0 ~ n)
+#if MIN_VERSION_base(4,16,0)
+maxZero = unsafeAxiom
+#else
+maxZero = Dict
+#endif
+
+powZero :: forall n. Dict ((n ^ 0) ~ 1)
+powZero = Dict
+
+leZero :: forall a. (a <= 0) :- (a ~ 0)
+leZero = Sub unsafeAxiom
+
+zeroLe :: forall (a :: Nat). Dict (0 <= a)
+#if MIN_VERSION_base(4,16,0)
+zeroLe = unsafeAxiom
+#else
+zeroLe = Dict
+#endif
+
+plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
+plusMinusInverse1 = unsafeAxiom
+
+plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)
+plusMinusInverse2 = Sub unsafeAxiom
+
+plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)
+plusMinusInverse3 = Sub unsafeAxiom
+
+plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)
+plusMonotone1 = Sub unsafeAxiom
+
+plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)
+plusMonotone2 = Sub unsafeAxiom
+
+powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))
+powMonotone1 = Sub unsafeAxiom
+
+powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))
+powMonotone2 = Sub unsafeAxiom
+
+divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)
+divMonotone1 = Sub unsafeAxiom
+
+divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)
+divMonotone2 = Sub unsafeAxiom
+
+timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)
+timesMonotone1 = Sub unsafeAxiom
+
+timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)
+timesMonotone2 = Sub unsafeAxiom
+
+minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)
+minMonotone1 = Sub unsafeAxiom
+
+minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)
+minMonotone2 = Sub unsafeAxiom
+
+maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)
+maxMonotone1 = Sub unsafeAxiom
+
+maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)
+maxMonotone2 = Sub unsafeAxiom
+
+powOne :: forall n. Dict ((n ^ 1) ~ n)
+powOne = unsafeAxiom
+
+plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
+plusMod = Sub unsafeAxiom
+
+timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
+timesMod = Sub unsafeAxiom
+
+modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
+modBound = Sub unsafeAxiom
+
+log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)
+log2Pow = unsafeAxiom
+
+euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))
+euclideanNat = Sub unsafeAxiom
+
+plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
+plusCommutes = unsafeAxiom
+
+timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
+timesCommutes = unsafeAxiom
+
+minCommutes :: forall n m. Dict (Min m n ~ Min n m)
+minCommutes = unsafeAxiom
+
+maxCommutes :: forall n m. Dict (Max m n ~ Max n m)
+maxCommutes = unsafeAxiom
+
+plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
+plusAssociates = unsafeAxiom
+
+timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
+timesAssociates = unsafeAxiom
+
+minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))
+minAssociates = unsafeAxiom
+
+maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))
+maxAssociates = unsafeAxiom
+
+gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))
+gcdAssociates = unsafeAxiom
+
+lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
+lcmAssociates = unsafeAxiom
+
+minIsIdempotent :: forall n. Dict (Min n n ~ n)
+minIsIdempotent = Dict
+
+maxIsIdempotent :: forall n. Dict (Max n n ~ n)
+maxIsIdempotent = Dict
+
+gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
+gcdIsIdempotent = Dict
+
+lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
+lcmIsIdempotent = Dict
+
+minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
+minDistributesOverPlus = unsafeAxiom
+
+minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
+minDistributesOverTimes = unsafeAxiom
+
+minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
+minDistributesOverPow1 = unsafeAxiom
+
+minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
+minDistributesOverPow2 = unsafeAxiom
+
+minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
+minDistributesOverMax = unsafeAxiom
+
+maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
+maxDistributesOverPlus = unsafeAxiom
+
+maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
+maxDistributesOverTimes = unsafeAxiom
+
+maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
+maxDistributesOverPow1 = unsafeAxiom
+
+maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
+maxDistributesOverPow2 = unsafeAxiom
+
+maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
+maxDistributesOverMin = unsafeAxiom
+
+plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))
+plusDistributesOverTimes = unsafeAxiom
+
+timesDistributesOverPow  :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))
+timesDistributesOverPow = unsafeAxiom
+
+timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
+timesDistributesOverGcd = unsafeAxiom
+
+timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
+timesDistributesOverLcm = unsafeAxiom
+
+plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
+plusIsCancellative = Sub unsafeAxiom
+
+timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
+timesIsCancellative = Sub unsafeAxiom
+
+gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
+gcdDistributesOverLcm = unsafeAxiom
+
+lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
+lcmDistributesOverGcd = unsafeAxiom
+
+dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
+dividesPlus = Sub unsafeAxiom
+
+dividesTimes :: Divides a b :- Divides a (b * c)
+dividesTimes = Sub unsafeAxiom
+
+dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
+dividesMin = Sub unsafeAxiom
+
+dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
+dividesMax = Sub unsafeAxiom
+
+-- This `dividesDef` is simpler and more convenient than Divides a b :- ((a * Div b a) ~ b)
+-- because the latter can be easily derived via 'euclideanNat', but not vice versa.
+
+dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
+dividesDef = Sub unsafeAxiom
+
+dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)
+dividesPow = Sub unsafeAxiom
+
+timesDiv :: forall a b. Dict ((a * Div b a) <= b)
+timesDiv = unsafeAxiom
+
+-- (<=) is an internal category in the category of constraints.
+
+leId :: forall (a :: Nat). Dict (a <= a)
+leId = Dict
+
+leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
+leEq = Sub unsafeAxiom
+
+leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)
+leTrans = Sub (axiomLe @a @c)
diff --git a/src/Data/Constraint/Symbol.hs b/src/Data/Constraint/Symbol.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Symbol.hs
@@ -0,0 +1,138 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE CPP #-}
+-- | Utilities for working with 'KnownSymbol' constraints.
+module Data.Constraint.Symbol
+  ( type AppendSymbol
+  , type (++)
+  , type Take
+  , type Drop
+  , type Length
+  , appendSymbol
+  , appendUnit1
+  , appendUnit2
+  , appendAssociates
+  , takeSymbol
+  , dropSymbol
+  , takeAppendDrop
+  , lengthSymbol
+  , takeLength
+  , take0
+  , takeEmpty
+  , dropLength
+  , drop0
+  , dropEmpty
+  , lengthTake
+  , lengthDrop
+  , dropDrop
+  , takeTake
+  ) where
+
+import Data.Constraint
+import Data.Constraint.Nat
+import Data.Constraint.Unsafe
+import Data.Proxy
+import GHC.TypeLits
+#if MIN_VERSION_base(4,18,0)
+import qualified GHC.TypeNats as TN
+#else
+import Unsafe.Coerce
+#endif
+
+-- | An infix synonym for 'AppendSymbol'.
+type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n
+infixr 5 ++
+
+type family Take :: Nat -> Symbol -> Symbol where
+type family Drop :: Nat -> Symbol -> Symbol where
+type family Length :: Symbol -> Nat where
+
+-- implementation details
+
+#if !MIN_VERSION_base(4,18,0)
+newtype Magic n = Magic (KnownSymbol n => Dict (KnownSymbol n))
+#endif
+
+magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
+#if MIN_VERSION_base(4,18,0)
+magicNSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))) Dict
+#else
+magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))
+#endif
+
+magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
+#if MIN_VERSION_base(4,18,0)
+magicSSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))) Dict
+#else
+magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))
+#endif
+
+magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n
+#if MIN_VERSION_base(4,18,0)
+magicSN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (symbolVal (Proxy :: Proxy a))))) Dict
+#else
+magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy @a))))
+#endif
+
+-- operations
+
+appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
+appendSymbol = magicSSS (++)
+
+appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)
+appendUnit1 = Dict
+
+appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)
+appendUnit2 = Dict
+
+appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
+appendAssociates = unsafeAxiom
+
+takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
+takeSymbol = magicNSS take
+
+dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
+dropSymbol = magicNSS drop
+
+takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
+takeAppendDrop = unsafeAxiom
+
+lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)
+lengthSymbol = magicSN length
+
+takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)
+takeLength = Sub unsafeAxiom
+
+take0 :: forall a. Dict (Take 0 a ~ "")
+take0 = unsafeAxiom
+
+takeEmpty :: forall n. Dict (Take n "" ~ "")
+takeEmpty = unsafeAxiom
+
+dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")
+dropLength = Sub unsafeAxiom
+
+drop0 :: forall a. Dict (Drop 0 a ~ a)
+drop0 = unsafeAxiom
+
+dropEmpty :: forall n. Dict (Drop n "" ~ "")
+dropEmpty = unsafeAxiom
+
+lengthTake :: forall n a. Dict (Length (Take n a) <= n)
+lengthTake = unsafeAxiom
+
+lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))
+lengthDrop = unsafeAxiom
+
+dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)
+dropDrop = unsafeAxiom
+
+takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)
+takeTake = unsafeAxiom
diff --git a/src/Data/Constraint/Unsafe.hs b/src/Data/Constraint/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraint/Unsafe.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Unsafe #-}
+{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+-- |
+-- Copyright   :  (C) 2011-2021 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Unsafe utilities used throughout @constraints@. As the names suggest, these
+-- functions are unsafe in general and can cause your program to segfault if
+-- used improperly. Handle with care.
+
+module Data.Constraint.Unsafe
+  ( Coercible
+  , unsafeAxiom
+  , unsafeCoerceConstraint
+  , unsafeDerive
+  , unsafeUnderive
+
+#if MIN_VERSION_base(4,18,0)
+    -- * Unsafely creating @GHC.TypeLits@ singleton values
+  , unsafeSChar
+  , unsafeSNat
+  , unsafeSSymbol
+#endif
+  ) where
+
+import Data.Coerce
+import Data.Constraint
+import Unsafe.Coerce
+
+#if MIN_VERSION_base(4,18,0)
+import GHC.TypeLits (SChar, SNat, SSymbol)
+import Numeric.Natural (Natural)
+#endif
+
+-- | Unsafely create a dictionary for any constraint.
+unsafeAxiom :: Dict c
+unsafeAxiom = unsafeCoerce (Dict :: Dict ())
+
+-- | Coerce a dictionary unsafely from one type to another
+unsafeCoerceConstraint :: a :- b
+unsafeCoerceConstraint = unsafeCoerce refl
+
+-- | Coerce a dictionary unsafely from one type to a newtype of that type
+unsafeDerive :: Coercible n o => (o -> n) -> t o :- t n
+unsafeDerive _ = unsafeCoerceConstraint
+
+-- | Coerce a dictionary unsafely from a newtype of a type to the base type
+unsafeUnderive :: Coercible n o => (o -> n) -> t n :- t o
+unsafeUnderive _ = unsafeCoerceConstraint
+
+#if MIN_VERSION_base(4,18,0)
+-- NB: if https://gitlab.haskell.org/ghc/ghc/-/issues/23478 were implemented,
+-- then we could avoid using 'unsafeCoerce' in the definitions below.
+
+-- | Unsafely create an 'SChar' value directly from a 'Char'. Use this function
+-- with care:
+--
+-- * The 'Char' value must match the 'Char' @c@ encoded in the return type
+--   @'SChar' c@.
+--
+-- * Be wary of using this function to create multiple values of type
+--   @'SChar' T@, where @T@ is a type family that does not reduce (e.g.,
+--   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
+--   the values and replace it with the other during a common subexpression
+--   elimination pass. If the two values have different underlying 'Char'
+--   values, this could be disastrous.
+unsafeSChar :: Char -> SChar c
+unsafeSChar = unsafeCoerce
+
+-- | Unsafely create an 'SNat' value directly from a 'Natural'. Use this
+-- function with care:
+--
+-- * The 'Natural' value must match the 'Nat' @n@ encoded in the return type
+--   @'SNat' n@.
+--
+-- * Be wary of using this function to create multiple values of type
+--   @'SNat' T@, where @T@ is a type family that does not reduce (e.g.,
+--   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
+--   the values and replace it with the other during a common subexpression
+--   elimination pass. If the two values have different underlying 'Natural'
+--   values, this could be disastrous.
+unsafeSNat :: Natural -> SNat n
+unsafeSNat = unsafeCoerce
+
+-- | Unsafely create an 'SSymbol' value directly from a 'String'. Use this
+-- function with care:
+--
+-- * The 'String' value must match the 'Symbol' @s@ encoded in the return type
+--   @'SSymbol' s@.
+--
+-- * Be wary of using this function to create multiple values of type
+--   @'SSymbol' T@, where @T@ is a type family that does not reduce (e.g.,
+--   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
+--   the values and replace it with the other during a common subexpression
+--   elimination pass. If the two values have different underlying 'String'
+--   values, this could be disastrous.
+unsafeSSymbol :: String -> SSymbol s
+unsafeSSymbol = unsafeCoerce
+#endif
diff --git a/tests/GH117Spec.hs b/tests/GH117Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/GH117Spec.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module GH117Spec (main, spec) where
+
+import Test.Hspec
+
+#if __GLASGOW_HASKELL__ >= 902
+import Data.Constraint
+import Data.Constraint.Char
+import Data.Proxy
+import GHC.TypeLits
+
+spec :: Spec
+spec =
+  describe "GH #117" $ do
+    it "should evaluate `charToNat @'a'` to 97" $
+      case charToNat @'a' of
+        Sub (Dict :: Dict (KnownNat n)) ->
+          natVal (Proxy @n) `shouldBe` 97
+    it "should evaluate `natToChar @97` to 'a'" $
+      case natToChar @97 of
+        Sub (Dict :: Dict (KnownChar c)) ->
+          charVal (Proxy @c) `shouldBe` 'a'
+#else
+spec :: Spec
+spec = return ()
+#endif
+
+main :: IO ()
+main = hspec spec
diff --git a/tests/GH55Spec.hs b/tests/GH55Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/GH55Spec.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module GH55Spec (main, spec) where
+
+import Data.Constraint
+import Data.Constraint.Nat
+import GHC.TypeLits
+import Test.Hspec
+
+newtype GF (n :: Nat) = GF Integer deriving (Eq, Show)
+
+instance KnownNat n => Num (GF n) where
+  xf@(GF a) + GF b = GF $ (a+b) `mod` (natVal xf)
+  xf@(GF a) - GF b = GF $ (a-b) `mod` (natVal xf)
+  xf@(GF a) * GF b = GF $ (a*b) `mod` (natVal xf)
+  abs = id
+  signum xf@(GF a) | a==0 = xf
+                   | otherwise = GF 1
+  fromInteger = GF
+
+x :: GF 5
+x = GF 3
+
+y :: GF 5
+y = GF 4
+
+foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
+foo m@(GF a) n@(GF b) = GF $ (a*b) `mod` (lcm (natVal m) (natVal n))
+
+bar :: (KnownNat m) => GF m -> GF m -> GF m
+bar (a :: GF m) b = foo a b - foo b a \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m
+
+z :: GF 5
+z = bar x y
+
+spec :: Spec
+spec = describe "GH #53" $
+         it "should normalize Lcm m m" $
+           z `shouldBe` (GF 0 :: GF (Lcm 5 5))
+
+main :: IO ()
+main = hspec spec
diff --git a/tests/Spec.hs b/tests/Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}