diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,85 @@
+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/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://secure.travis-ci.org/ekmett/constraints.png?branch=master)](http://travis-ci.org/ekmett/constraints)
+
 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,7 +1,7 @@
 name:          constraints
 category:      Constraints
-version:       0.8
-license:       BSD3
+version:       0.9
+license:       BSD2
 cabal-version: >= 1.10
 license-file:  LICENSE
 author:        Edward A. Kmett
@@ -17,8 +17,9 @@
   This package provides a vocabulary for working with them.
 
 build-type:    Simple
-tested-with:   GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.1, GHC == 7.10.2
+tested-with:   GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2
 extra-source-files: README.markdown
+                  , CHANGELOG.markdown
 
 source-repository head
   type: git
@@ -50,16 +51,16 @@
     transformers >= 0.2 && < 0.6,
     transformers-compat >= 0.4 && < 1
 
-  if impl(ghc < 7.8)
-    build-depends:
-      newtype >= 0.2 && < 0.3,
-      tagged >= 0.2 && < 1
-
   exposed-modules:
     Data.Constraint
     Data.Constraint.Deferrable
     Data.Constraint.Forall
     Data.Constraint.Lifting
     Data.Constraint.Unsafe
+
+  if impl(ghc >= 8)
+    exposed-modules:
+      Data.Constraint.Nat
+      Data.Constraint.Symbol
 
   ghc-options: -Wall
diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs
--- a/src/Data/Constraint.hs
+++ b/src/Data/Constraint.hs
@@ -1,10 +1,13 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeOperators #-}
@@ -13,11 +16,6 @@
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 707
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE RoleAnnotations #-}
-#endif
 #if __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE UndecidableSuperClasses #-}
 #endif
@@ -58,10 +56,12 @@
     Constraint
   -- * Dictionary
   , Dict(Dict)
+  , withDict
   -- * Entailment
   , (:-)(Sub)
   , (\\)
   , weaken1, weaken2, contract
+  , strengthen1, strengthen2
   , (&&&), (***)
   , trans, refl
   , Bottom
@@ -73,25 +73,17 @@
   , Class(..)
   , (:=>)(..)
   ) where
-import Control.Monad
-#if __GLASGOW_HASKELL__ >= 707
-import Control.Category
-#endif
 import Control.Applicative
+import Control.Category
+import Control.Monad
 #if __GLASGOW_HASKELL__ < 710
 import Data.Monoid
 #endif
 import Data.Complex
 import Data.Ratio
-#if __GLASGOW_HASKELL__ >= 707
 import Data.Data
-#endif
-#if __GLASGOW_HASKELL__ <= 710
-import GHC.Prim (Constraint)
-#else
-import GHC.Types (Constraint)
-#endif
-import qualified GHC.Prim as Prim
+import qualified GHC.Exts as Exts (Any)
+import GHC.Exts (Constraint)
 
 -- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@.
 --
@@ -111,7 +103,6 @@
 --
 data Dict :: Constraint -> * where
   Dict :: a => Dict a
-#if __GLASGOW_HASKELL__ >= 707
   deriving Typeable
 
 
@@ -128,12 +119,21 @@
 
 dictDataType :: DataType
 dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]
-#endif
 
 deriving instance Eq (Dict a)
 deriving instance Ord (Dict a)
 deriving instance Show (Dict a)
 
+-- | 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.
+--
+withDict :: Dict a -> (a => r) -> r
+withDict d r = case d of
+                 Dict -> r
+
 infixr 9 :-
 
 -- | This is the type of entailment.
@@ -152,9 +152,10 @@
 --
 -- 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 because sufficiently general to support this
--- instance in GHC 7.8, so prior to 7.8 this instance is unavailable.
+-- 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
@@ -190,7 +191,6 @@
 -- library is sensible and can't break any assumptions on the behalf of
 -- library authors.
 newtype a :- b = Sub (a => Dict b)
-#if __GLASGOW_HASKELL__ >= 707
   deriving Typeable
 
 type role (:-) nominal nominal
@@ -218,7 +218,6 @@
 instance Category (:-) where
   id  = refl
   (.) = trans
-#endif
 
 -- | Assumes 'IncoherentInstances' doesn't exist.
 instance Eq (a :- b) where
@@ -279,6 +278,12 @@
 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.
@@ -305,8 +310,8 @@
 top = Sub Dict
 
 -- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance.
-class Prim.Any => Bottom where
-  no :: Dict a
+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">
@@ -331,9 +336,7 @@
 unmapDict :: (Dict a -> Dict b) -> a :- b
 unmapDict f = Sub (f Dict)
 
-#if __GLASGOW_HASKELL__ >= 707
 type role Dict nominal
-#endif
 
 --------------------------------------------------------------------------------
 -- Reflection
diff --git a/src/Data/Constraint/Deferrable.hs b/src/Data/Constraint/Deferrable.hs
--- a/src/Data/Constraint/Deferrable.hs
+++ b/src/Data/Constraint/Deferrable.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ConstraintKinds #-}
@@ -5,11 +6,18 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE PolyKinds #-}
 
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeInType #-}
+#endif
+
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Constraint.Deferrable
--- Copyright   :  (C) 2015 Edward Kmett
+-- Copyright   :  (C) 2015-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -24,40 +32,98 @@
   , Deferrable(..)
   , defer
   , deferred
+#if __GLASGOW_HASKELL__ >= 800
+  , defer_
+  , deferEither_
+  , (:~~:)(HRefl)
+#endif
+  , (:~:)(Refl)
   ) where
 
 import Control.Exception
 import Control.Monad
 import Data.Constraint
 import Data.Proxy
-import Data.Typeable (Typeable, cast)
+import Data.Typeable (Typeable, cast, typeRep)
+import Data.Type.Equality ((:~:)(Refl))
 
+#if __GLASGOW_HASKELL__ >= 800
+import GHC.Types (type (~~))
+#endif
+
 data UnsatisfiedConstraint = UnsatisfiedConstraint String
   deriving (Typeable, Show)
 
 instance Exception UnsatisfiedConstraint
 
 -- | Allow an attempt at resolution of a constraint at a later time
-class Deferrable (p :: Constraint) where
+class Deferrable p where
   -- | Resolve a 'Deferrable' constraint with observable failure.
   deferEither :: proxy p -> (p => r) -> Either String r
 
 -- | Defer a constraint for later resolution in a context where we want to upgrade failure into an error
-defer :: forall proxy p r. Deferrable p => proxy p -> (p => r) -> r
-defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r 
+defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r
+defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r
 
 deferred :: forall p. Deferrable p :- p
 deferred = Sub $ defer (Proxy :: Proxy p) Dict
 
--- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6.
-data a :~: b where
-  Refl :: a :~: a
+#if __GLASGOW_HASKELL__ >= 800
+-- | A version of 'defer' that uses visible type application in place of a 'Proxy'.
+--
+-- Only available on GHC 8.0 or later.
+defer_ :: forall p r. Deferrable p => (p => r) -> r
+defer_ r = defer @p Proxy r
+
+-- | A version of 'deferEither' that uses visible type application in place of a 'Proxy'.
+--
+-- Only available on GHC 8.0 or later.
+deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r
+deferEither_ r = deferEither @p Proxy r
+#endif
+
+#if __GLASGOW_HASKELL__ >= 800
+-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is
+-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
+--
+-- Only available on GHC 8.0 or later.
+data (a :: i) :~~: (b :: j) where
+  HRefl :: a :~~: a
     deriving Typeable
+#endif
 
+showTypeRep :: Typeable t => Proxy t -> String
+showTypeRep = show . typeRep
+
+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.
+#if __GLASGOW_HASKELL__ >= 800
+instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where
+#elif __GLASGOW_HASKELL__ == 710
+instance (Typeable a, Typeable b) => Deferrable ((a :: *) ~ (b :: *)) where
+#else
 instance (Typeable a, Typeable b) => Deferrable (a ~ b) where
+#endif
   deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of
     Just Refl -> Right r
-    Nothing -> Left "deferred type equality: type mismatch"
+    Nothing   -> Left $
+      "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `"  ++ showTypeRep (Proxy :: Proxy a) ++ "'"
+
+#if __GLASGOW_HASKELL__ >= 800
+-- | 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 (Proxy :: Proxy a) ++ "’ and `"  ++ showTypeRep (Proxy :: Proxy a) ++ "'"
+#endif
 
 instance (Deferrable a, Deferrable b) => Deferrable (a, b) where
   deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r
diff --git a/src/Data/Constraint/Forall.hs b/src/Data/Constraint/Forall.hs
--- a/src/Data/Constraint/Forall.hs
+++ b/src/Data/Constraint/Forall.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -7,6 +8,7 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE PolyKinds #-}
 #if __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE UndecidableSuperClasses #-}
@@ -15,7 +17,8 @@
 -- |
 -- Module      :  Data.Constraint.Forall
 -- Copyright   :  (C) 2011-2015 Edward Kmett,
---                (C) 2015 Ørjan Johansen
+--                (C) 2015 Ørjan Johansen,
+--                (C) 2016 David Feuer
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -30,6 +33,8 @@
   , ForallF, instF
   , Forall1, inst1
   , ForallT, instT
+  , ForallV, InstV (instV)
+  , forall
   ) where
 
 import Data.Constraint
@@ -39,6 +44,14 @@
  - for whether a class predicate holds, and if so assume that it holds for all
  - types, unsafely coercing the typeclass dictionary.
  -
+ - The particular technique used to implement 'Forall' appears to have been
+ - discovered first by Nicolas Frisby and is
+ - <https://csks.wordpress.com/2012/10/22/safe-polykinded-universally-quantified-constraints-part-3-of-3/ discussed in some detail>
+ - on his blog.
+ -
+ - However, his discovery did not directly affect the development of this
+ - module.
+ -
  - A previous version of this module used concrete, unexported types as the
  - skolems. This turned out to be unsound in the presence of type families.
  - There were 3 somewhat distinct issues:
@@ -85,17 +98,14 @@
  - extract it from `Forall p` in order to tie the knot.
  -}
 
--- the `Skolem*` type families represent skolem variables, do not export!
--- if GHC supports it, these might be made closed with no instances.
+-- The `Skolem` type family represents skolem variables; do not export!
+-- If GHC supports it, these might be made closed with no instances.
 
 type family Skolem (p :: k -> Constraint) :: k
-type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1
-type family SkolemT1 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k1
-type family SkolemT2 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k2
 
--- The outer `Forall*` type families prevent GHC from giving a spurious
+-- The outer `Forall` type family prevents GHC from giving a spurious
 -- superclass cycle error.
--- The inner `Forall*_` classes prevent the skolem from leaking to the user,
+-- The inner `Forall_` class prevents the skolem from leaking to the user,
 -- which would be disastrous.
 
 -- | A representation of the quantified constraint @forall a. p a@.
@@ -104,33 +114,78 @@
 class p (Skolem p) => Forall_ (p :: k -> Constraint)
 instance p (Skolem p) => Forall_ (p :: k -> Constraint)
 
--- | A representation of the quantified constraint @forall a. p (f a)@.
-type family ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) :: Constraint
-type instance ForallF p f = ForallF_ p f
-class p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)
-instance p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)
-
-type Forall1 p = Forall p
-
--- | A representation of the quantified constraint @forall f a. p (t f a)@.
-type family ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: Constraint
-type instance ForallT p t = ForallT_ p t
-class p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)
-instance p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)
-
 -- | Instantiate a quantified @'Forall' p@ constraint at type @a@.
 inst :: forall p a. Forall p :- p a
 inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p))
 
+-- | 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 = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f)))
+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 (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
 
--- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.
-instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a)
-instT = unsafeCoerce (Sub Dict :: ForallT p t :- p (t (SkolemT1 p t) (SkolemT2 p t)))
+-- | 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
+
+forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
+forall d = case d :: Dict (p (Skolem p)) of Dict -> 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,323 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE Trustworthy #-}
+-- | 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
+  , plusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat
+  , plusZero, 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
+  , dividesDef
+  , timesDiv
+  , eqLe, leEq, leId, leTrans
+  , leZero, zeroLe
+  ) where
+
+import Data.Constraint
+import Data.Proxy
+import GHC.TypeLits
+import Unsafe.Coerce
+
+type family Min :: Nat -> Nat -> Nat where
+type family Max :: Nat -> Nat -> Nat where
+type family Div :: Nat -> Nat -> Nat where
+type family Mod :: Nat -> Nat -> Nat where
+type family Gcd :: Nat -> Nat -> Nat where
+type family Lcm :: Nat -> Nat -> Nat where
+
+type Divides n m = n ~ Gcd n m
+
+newtype Magic n r = Magic (KnownNat n => r)
+
+magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
+magic f = Sub $ unsafeCoerce (Magic id) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
+
+axiom :: forall a b. Dict (a ~ b)
+axiom = unsafeCoerce (Dict :: Dict (a ~ a))
+
+axiomLe :: forall a b. Dict (a <= b)
+axiomLe = axiom
+
+eqLe :: (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 axiom
+
+dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c
+dividesLcm = Sub axiom
+
+gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)
+gcdCommutes = axiom
+
+lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)
+lcmCommutes = axiom
+
+gcdZero :: forall a. Dict (Gcd 0 a ~ a)
+gcdZero = axiom
+
+gcdOne :: forall a. Dict (Gcd 1 a ~ 1)
+gcdOne = axiom
+
+lcmZero :: forall a. Dict (Lcm 0 a ~ 0)
+lcmZero = axiom
+
+lcmOne :: forall a. Dict (Lcm 1 a ~ a)
+lcmOne = axiom
+
+gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
+gcdNat = magic gcd
+
+lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
+lcmNat = magic lcm
+
+plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
+plusNat = magic (+)
+
+minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
+minNat = magic min
+
+maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
+maxNat = magic max
+
+timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
+timesNat = magic (*)
+
+powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
+powNat = magic (^)
+
+divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
+divNat = Sub $ case magic @n @m div of Sub r -> r
+
+modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
+modNat = Sub $ case magic @n @m mod of Sub r -> r
+
+plusZero :: forall n. Dict ((n + 0) ~ n)
+plusZero = axiom
+
+timesZero :: forall n. Dict ((n * 0) ~ 0)
+timesZero = axiom
+
+timesOne :: forall n. Dict ((n * 1) ~ n)
+timesOne = axiom
+
+minZero :: forall n. Dict (Min n 0 ~ 0)
+minZero = axiom
+
+maxZero :: forall n. Dict (Max n 0 ~ n)
+maxZero = axiom
+
+powZero :: forall n. Dict ((n ^ 0) ~ 1)
+powZero = axiom
+
+leZero :: forall a. (a <= 0) :- (a ~ 0)
+leZero = Sub axiom
+
+zeroLe :: forall a. Dict (0 <= a)
+zeroLe = axiom
+
+plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)
+plusMonotone1 = Sub axiom
+
+plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)
+plusMonotone2 = Sub axiom
+
+powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))
+powMonotone1 = Sub axiom
+
+powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))
+powMonotone2 = Sub axiom
+
+divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)
+divMonotone1 = Sub axiom
+
+divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)
+divMonotone2 = Sub axiom
+
+timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)
+timesMonotone1 = Sub axiom
+
+timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)
+timesMonotone2 = Sub axiom
+
+minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)
+minMonotone1 = Sub axiom
+
+minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)
+minMonotone2 = Sub axiom
+
+maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)
+maxMonotone1 = Sub axiom
+
+maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)
+maxMonotone2 = Sub axiom
+
+powOne :: forall n. Dict ((n ^ 1) ~ n)
+powOne = axiom
+
+plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
+plusMod = Sub axiom
+
+timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
+timesMod = Sub axiom
+
+modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
+modBound = Sub axiom
+
+euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))
+euclideanNat = Sub axiom
+
+plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
+plusCommutes = axiom
+
+timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
+timesCommutes = axiom
+
+minCommutes :: forall n m. Dict (Min m n ~ Min n m)
+minCommutes = axiom
+
+maxCommutes :: forall n m. Dict (Min m n ~ Min n m)
+maxCommutes = axiom
+
+plusAssociates :: forall n m o. Dict (((m + n) + o) ~ (m + (n + o)))
+plusAssociates = axiom
+
+timesAssociates :: forall n m o. Dict (((m * n) * o) ~ (m * (n * o)))
+timesAssociates = axiom
+
+minAssociates :: forall n m o. Dict (Min (Min m n) o ~ Min m (Min n o))
+minAssociates = axiom
+
+maxAssociates :: forall n m o. Dict (Max (Max m n) o ~ Max m (Max n o))
+maxAssociates = axiom
+
+gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))
+gcdAssociates = axiom
+
+lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
+lcmAssociates = axiom
+
+minIsIdempotent :: forall n. Dict (Min n n ~ n)
+minIsIdempotent = axiom
+
+maxIsIdempotent :: forall n. Dict (Max n n ~ n)
+maxIsIdempotent = axiom
+
+gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
+gcdIsIdempotent = axiom
+
+lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
+lcmIsIdempotent = axiom
+
+minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
+minDistributesOverPlus = axiom
+
+minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
+minDistributesOverTimes = axiom
+
+minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
+minDistributesOverPow1 = axiom
+
+minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
+minDistributesOverPow2 = axiom
+
+minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
+minDistributesOverMax = axiom
+
+maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
+maxDistributesOverPlus = axiom
+
+maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
+maxDistributesOverTimes = axiom
+
+maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
+maxDistributesOverPow1 = axiom
+
+maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
+maxDistributesOverPow2 = axiom
+
+maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
+maxDistributesOverMin = axiom
+
+plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))
+plusDistributesOverTimes = axiom
+
+timesDistributesOverPow  :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))
+timesDistributesOverPow = axiom
+
+timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
+timesDistributesOverGcd = axiom
+
+timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
+timesDistributesOverLcm = axiom
+
+plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
+plusIsCancellative = Sub axiom
+
+timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
+timesIsCancellative = Sub axiom
+
+gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
+gcdDistributesOverLcm = axiom
+
+lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
+lcmDistributesOverGcd = axiom
+
+dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
+dividesPlus = Sub axiom
+
+dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)
+dividesTimes = Sub axiom
+
+dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
+dividesMin = Sub axiom
+
+dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
+dividesMax = Sub axiom
+
+dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ a)
+dividesDef = Sub axiom
+
+dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)
+dividesPow = Sub axiom
+
+timesDiv :: forall a b. Dict ((a * Div b a) <= a)
+timesDiv = axiom
+
+-- (<=) is an internal category in the category of constraints.
+
+leId :: forall a. Dict (a <= a)
+leId = Dict
+
+leEq :: forall a b. (a <= b, b <= a) :- (a ~ b)
+leEq = Sub axiom
+
+leTrans :: forall a b c. (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,119 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+-- | Utilities for working with 'KnownSymbol' constraints.
+--
+-- This module is only available on GHC 8.0 or later.
+module Data.Constraint.Symbol
+  ( 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.Proxy
+import GHC.TypeLits
+import Unsafe.Coerce
+
+type family (++) :: Symbol -> Symbol -> Symbol where
+type family Take :: Nat -> Symbol -> Symbol where
+type family Drop :: Nat -> Symbol -> Symbol where
+type family Length :: Symbol -> Nat where
+
+-- implementation details
+
+newtype Magic n r = Magic (KnownSymbol n => r)
+
+magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
+magicNSS f = Sub $ unsafeCoerce (Magic id) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m))
+
+magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
+magicSSS f = Sub $ unsafeCoerce (Magic id) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m))
+
+magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n
+magicSN f = Sub $ unsafeCoerce (Magic id) (toInteger (f (symbolVal (Proxy :: Proxy a))))
+
+axiom :: forall a b. Dict (a ~ b)
+axiom = unsafeCoerce (Dict :: Dict (a ~ a))
+
+-- axioms and operations
+
+appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b)
+appendSymbol = magicSSS (++)
+
+appendUnit1 :: forall a. Dict (("" ++ a) ~ a)
+appendUnit1 = axiom
+
+appendUnit2 :: forall a. Dict ((a ++ "") ~ a)
+appendUnit2 = axiom
+
+appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))
+appendAssociates = axiom
+
+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 (Take n a ++ Drop n a ~ a)
+takeAppendDrop = axiom
+
+lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)
+lengthSymbol = magicSN length
+
+takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)
+takeLength = Sub axiom
+
+take0 :: forall a. Dict (Take 0 a ~ "")
+take0 = axiom
+
+takeEmpty :: forall n. Dict (Take n "" ~ "")
+takeEmpty = axiom
+
+dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")
+dropLength = Sub axiom
+
+drop0 :: forall a. Dict (Drop 0 a ~ a)
+drop0 = axiom
+
+dropEmpty :: forall n. Dict (Drop n "" ~ "")
+dropEmpty = axiom
+
+lengthTake :: forall n a. Dict (Length (Take n a) <= n)
+lengthTake = axiom
+
+lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))
+lengthDrop = axiom
+
+dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)
+dropDrop = axiom
+
+takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)
+takeTake = axiom
diff --git a/src/Data/Constraint/Unsafe.hs b/src/Data/Constraint/Unsafe.hs
--- a/src/Data/Constraint/Unsafe.hs
+++ b/src/Data/Constraint/Unsafe.hs
@@ -32,20 +32,9 @@
 
 import Control.Applicative
 import Control.Monad
+import Data.Coerce
 import Data.Constraint
 import Unsafe.Coerce
-
-#if __GLASGOW_HASKELL__ >= 708
-
-import Data.Coerce
-
-#else
-
-import Control.Newtype
-
-type Coercible = Newtype
-
-#endif
 
 -- | Coerce a dictionary unsafely from one type to another
 unsafeCoerceConstraint :: a :- b