diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,39 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.0.1 -- *2019 Nov 06*
+
+  * Documentation updates
+  * Dependency constraint updates: constraints, lens, th-abstraction, hashable, hashtables, and vector.
+  * Now supports building under GHC 8.8.1.
+  * Added monadic folds and more traversals:
+      * lazy folds: `foldlMF`, `foldrMF`, `foldlMFC`, `foldrMFC`
+      * strict folds: `foldlMF'`, `foldrMF'`, `foldlMFC'`, `foldrMFC'`
+      * `forF`, `forF_`
+      * `forFC`, `forFC_`
+      * `lengthF`
+  * Added monadic folds, ascending or descending list conversions to `Parameterized.Map`:
+      * Added monadic folds: `foldlMWithKey`, `foldrMWithKey`
+      * Added ascending or descending list conversions: `toAscList` (equivalent to existing `toList`) and `toDescList`.
+      * Added `findWithDefault` to lookup a key or return a default value.
+      * Added `traverseMaybeWithKey`.
+      * Fixes traverse to do an in-order rather than a pre-order traversal.
+  * Added the `Data.Parameterized.All` module for universal quantification/parametricity over a type variable.
+  * Additions to `Data.Parameterized.Context`:
+      * Added `IndexView` type and `viewIndex` functions.
+      * Added `addDiff` function to explicitly describe the (flipped) binary operator for the `Diff` instance of the `Category` class from `Control.Category`.
+      * Added `traverseWithIndex_`
+  * Added `Data.Parameterized.DataKind` providing the `PairRepr` type with associated `fst` and `snd` functions.
+  * Added `TypeAp` to `Data.Parameterized.Classes`
+  * Added `runSTNonceGenerator` to `Data.Parameterized.Nonce` for a *global* ST generator.
+  * Added a `Hashable` instance for list `Index l x` types.
+  * Changes in GADT TH code generator:
+      * Added `structuralHashWithSalt` to
+      * Fixed off by one bug in output
+      * Fixed generation and constructor generation to use constructor type arguments, not type parameters.
+  * The `Some` type is now an instance of `FunctorF`, `FoldableF`, and `TraversableF`.
+  * Adjusted `structuralShowsPrec` precedence to match GHC derived `Show` instances.
+  * The `Data.Parameterized.Nonce.Unsafe` module is now deprecated: clients should switch to `Data.Parameterized.Nonce`.
+
 ## 2.0 -- *2019 Apr 03*
 
   * Drop support for GHC versions prior to GHC 8.2
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,5 +1,5 @@
 Name:          parameterized-utils
-Version:       2.0
+Version:       2.0.1.0
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com, kquick@galois.com
 stability:     stable
@@ -11,7 +11,7 @@
 category:      Data Structures, Dependent Types
 Synopsis: Classes and data structures for working with data-kind indexed types
 Description:
-  This packages contains collection classes and type representations
+  This package contains collection classes and type representations
   used for working with values that have a single parameter.  It's
   intended for things like expression libraries where one wishes
   to leverage the Haskell type-checker to improve type-safety by encoding
@@ -36,24 +36,25 @@
 
 library
   build-depends: base >= 4.10 && < 5
-               , th-abstraction >=0.1 && <0.3
-               , constraints == 0.10.*
+               , th-abstraction >=0.3  && <0.4
+               , constraints    >=0.10 && <0.12
                , containers
                , deepseq
                , ghc-prim
-               , hashable == 1.2.*
-               , hashtables == 1.2.*
-               , lens == 4.17.*
+               , hashable       >=1.2  && <1.4
+               , hashtables     ==1.2.*
+               , lens           >=4.16 && <4.19
                , mtl
                , template-haskell
                , text
-               , vector == 0.12.*
+               , vector         ==0.12.*
 
   hs-source-dirs: src
 
   exposed-modules:
     Data.Parameterized
-    Data.Parameterized.BoolRepr                  
+    Data.Parameterized.All
+    Data.Parameterized.BoolRepr
     Data.Parameterized.Classes
     Data.Parameterized.ClassesC
     Data.Parameterized.Compose
@@ -62,6 +63,7 @@
     Data.Parameterized.Context.Unsafe
     Data.Parameterized.Ctx
     Data.Parameterized.Ctx.Proofs
+    Data.Parameterized.DataKind
     Data.Parameterized.DecidableEq
     Data.Parameterized.HashTable
     Data.Parameterized.List
@@ -80,7 +82,7 @@
     Data.Parameterized.Utils.BinTree
     Data.Parameterized.Utils.Endian
     Data.Parameterized.Vector
-    Data.Parameterized.WithRepr                  
+    Data.Parameterized.WithRepr
 
   other-modules:
     Data.Parameterized.NatRepr.Internal
@@ -106,6 +108,7 @@
   build-depends: base
                , hashable
                , hashtables
+               , hedgehog
                , ghc-prim
                , lens
                , mtl
@@ -113,5 +116,4 @@
                , tasty == 1.2.*
                , tasty-ant-xml == 1.1.*
                , tasty-hunit >= 0.9 && < 0.11
-               , tasty-quickcheck >= 0.8.1 && < 0.11
-               , QuickCheck >= 2.7 && < 2.14
+               , tasty-hedgehog
diff --git a/src/Data/Parameterized/All.hs b/src/Data/Parameterized/All.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/All.hs
@@ -0,0 +1,68 @@
+------------------------------------------------------------------------
+-- |
+-- Module           : Data.Parameterized.All
+-- Copyright        : (c) Galois, Inc 2019
+-- Maintainer       : Langston Barrett <langston@galois.com>
+-- Description      : Universal quantification, in a datatype
+--
+-- This module provides 'All', a GADT that encodes universal
+-- quantification/parametricity over a type variable.
+--
+-- The following is an example of a situation in which it might be necessary
+-- to use 'All' (though it is a bit contrived):
+--
+-- @
+--   {-# LANGUAGE FlexibleInstances #-}
+--   {-# LANGUAGE GADTs #-}
+--
+--   data F (x :: Bool) where
+--     FTrue :: F 'True
+--     FFalse :: F 'False
+--     FIndeterminate :: F b
+--
+--   data Value =
+--     VAllF (All F)
+--
+--   class Valuable a where
+--     valuation :: a -> Value
+--
+--   instance Valuable (All F) where
+--     valuation = VAllF
+--
+--   val1 :: Value
+--   val1 = valuation (All FIndeterminate)
+-- @
+--
+-- For a less contrived but more complex example, see this blog
+-- post: http://comonad.com/reader/2008/rotten-bananas/
+------------------------------------------------------------------------
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Data.Parameterized.All
+  ( All(..)
+  , allConst
+  ) where
+
+import Data.Functor.Const (Const(..))
+
+import Data.Parameterized.Classes
+import Data.Parameterized.TraversableF
+
+newtype All (f :: k -> *) = All { getAll :: forall x. f x }
+
+instance FunctorF All where
+  fmapF f (All a) = All (f a)
+
+instance FoldableF All where
+  foldMapF toMonoid (All x) = toMonoid x
+
+instance ShowF f => Show (All f) where
+  show (All fa) = showF fa
+
+instance EqF f => Eq (All f) where
+  (All x) == (All y) = eqF x y
+
+allConst :: a -> All (Const a)
+allConst a = All (Const a)
diff --git a/src/Data/Parameterized/BoolRepr.hs b/src/Data/Parameterized/BoolRepr.hs
--- a/src/Data/Parameterized/BoolRepr.hs
+++ b/src/Data/Parameterized/BoolRepr.hs
@@ -38,15 +38,13 @@
 import           Data.Parameterized.Some
 
 import           Data.Type.Bool
-import           Data.Hashable
 
--- | 
+-- | A Boolean flag
 data BoolRepr (b :: Bool) where
   FalseRepr :: BoolRepr 'False
   TrueRepr  :: BoolRepr 'True
 
-  
--- | conditional 
+-- | conditional
 ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
 ifRepr TrueRepr b _ = b
 ifRepr FalseRepr _ c = c
@@ -56,17 +54,17 @@
 notRepr TrueRepr = FalseRepr
 notRepr FalseRepr = TrueRepr
 
--- | Conjunction 
+-- | Conjunction
 (%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
 FalseRepr %&& _ = FalseRepr
 TrueRepr  %&& a = a
 infixr 3 %&&
 
--- | Disjunction 
+-- | Disjunction
 (%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
 FalseRepr %|| a = a
 TrueRepr  %|| _ = TrueRepr
-infixr 2 %||  
+infixr 2 %||
 
 instance Hashable (BoolRepr n) where
   hashWithSalt i TrueRepr  = hashWithSalt i True
@@ -99,12 +97,11 @@
 instance Show (BoolRepr m) where
   show FalseRepr = "FalseRepr"
   show TrueRepr  = "TrueRepr"
-  
+
 instance ShowF BoolRepr
 
 instance HashableF BoolRepr where
   hashWithSaltF = hashWithSalt
-
 
 ----------------------------------------------------------
 -- * Implicit runtime booleans
diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs
--- a/src/Data/Parameterized/Classes.hs
+++ b/src/Data/Parameterized/Classes.hs
@@ -8,6 +8,7 @@
 "Data.Functor.Classes" types as they work with any kind @k@, and are
 not restricted to '*'.
 -}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -17,6 +18,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 #if MIN_VERSION_base(4,9,0)
@@ -44,6 +46,8 @@
   , showsF
   , HashableF(..)
   , CoercibleF(..)
+    -- * Type function application constructor
+  , TypeAp(..)
     -- * Optics generalizations
   , IndexF
   , IxValueF
@@ -53,11 +57,13 @@
     -- * KnownRepr
   , KnownRepr(..)
     -- * Re-exports
+  , Data.Hashable.Hashable(..)
   , Data.Maybe.isJust
   ) where
 
 import Data.Functor.Const
 import Data.Functor.Compose (Compose(..))
+import Data.Kind
 import Data.Hashable
 import Data.Maybe (isJust)
 import Data.Proxy
@@ -296,6 +302,29 @@
 
 instance Hashable a => HashableF (Const a) where
   hashWithSaltF s (Const x) = hashWithSalt s x
+
+------------------------------------------------------------------------
+-- TypeAp
+
+-- | Captures the value obtained from applying a type to a function so
+-- that we can use parameterized class instance to provide unparameterized
+-- instances for specific types.
+--
+-- This is the same as `Ap` from @Control.Applicative@, but we introduce
+-- our own new type to avoid orphan instances.
+newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)
+
+instance TestEquality f => Eq (TypeAp f tp) where
+  TypeAp x == TypeAp y = isJust $ testEquality x y
+
+instance OrdF f => Ord (TypeAp f tp) where
+  compare (TypeAp x) (TypeAp y) = toOrdering (compareF x y)
+
+instance ShowF f => Show (TypeAp f tp) where
+  showsPrec p (TypeAp x) = showsPrecF p x
+
+instance HashableF f => Hashable (TypeAp f tp) where
+  hashWithSalt s (TypeAp x) = hashWithSaltF s x
 
 ------------------------------------------------------------------------
 -- KnownRepr
diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs
--- a/src/Data/Parameterized/Compose.hs
+++ b/src/Data/Parameterized/Compose.hs
@@ -6,7 +6,8 @@
 Utilities for working with "Data.Functor.Compose".
 
 NB: This module contains an orphan instance. It will be included in GHC 8.10,
-see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273 and also
+https://github.com/haskell-compat/base-orphans/issues/49.
 -}
 
 {-# LANGUAGE GADTs #-}
diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs
--- a/src/Data/Parameterized/Context.hs
+++ b/src/Data/Parameterized/Context.hs
@@ -1,17 +1,26 @@
-------------------------------------------------------------------------
--- |
--- Module           : Data.Parameterized.Context
--- Copyright        : (c) Galois, Inc 2014-2019
--- Maintainer       : Joe Hendrix <jhendrix@galois.com>
---
--- This module reexports either "Data.Parameterized.Context.Safe"
--- or "Data.Parameterized.Context.Unsafe" depending on the
--- the unsafe-operations compile-time flag.
---
--- It also defines some utility typeclasses for transforming
--- between curried and uncurried versions of functions over contexts.
-------------------------------------------------------------------------
+{-|
+Module           : Data.Parameterized.Context
+Copyright        : (c) Galois, Inc 2014-2019
+Maintainer       : Joe Hendrix <jhendrix@galois.com>
 
+This module reexports either "Data.Parameterized.Context.Safe"
+or "Data.Parameterized.Context.Unsafe" depending on the
+the unsafe-operations compile-time flag.
+
+It also defines some utility typeclasses for transforming
+between curried and uncurried versions of functions over contexts.
+
+The 'Assignment' type is isomorphic to the 'Data.Parameterized.List'
+type, except 'Assignment's construct lists from the right-hand side,
+and instead of using type-level @'[]@-style lists, an 'Assignment' is
+indexed by a type-level 'Data.Parameterized.Context.Ctx'. The
+implementation of 'Assignment's is also more efficent than
+'Data.Parameterized.List' for lists of many elements, as it uses a
+balanced binary tree representation rather than a linear-time
+list. For a motivating example, see 'Data.Parameterized.List'.
+
+-}
+
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
@@ -52,6 +61,7 @@
   , generateSomeM
   , fromList
   , traverseAndCollect
+  , traverseWithIndex_
 
     -- * Context extension and embedding utilities
   , CtxEmbedding(..)
@@ -86,6 +96,7 @@
 
 import           Control.Applicative (liftA2)
 import           Control.Lens hiding (Index, (:>), Empty)
+import           Data.Functor (void)
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
 import           GHC.TypeLits (Nat, type (-))
@@ -380,6 +391,14 @@
   m w
 traverseAndCollect f =
   runCollector . traverseWithIndex (\i x -> Collector (f i x))
+
+-- | Visit each of the elements in an @Assignment@ in order
+--   from left to right, executing an action with each.
+traverseWithIndex_ :: Applicative m
+                   => (forall tp . Index ctx tp -> f tp -> m ())
+                   -> Assignment f ctx
+                   -> m ()
+traverseWithIndex_ f = void . traverseAndCollect f
 
 --------------------------------------------------------------------------------
 -- Size and Index values
diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -42,6 +42,8 @@
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS_HADDOCK hide #-}
 module Data.Parameterized.Context.Safe
   ( module Data.Parameterized.Ctx
     -- * Size
@@ -58,6 +60,7 @@
     -- * Diff
   , Diff
   , noDiff
+  , addDiff
   , extendRight
   , appendDiff
   , DiffView(..)
@@ -77,6 +80,8 @@
   , forIndex
   , forIndexRange
   , intIndex
+  , IndexView(..)
+  , viewIndex
     -- * Assignments
   , Assignment
   , size
@@ -127,6 +132,12 @@
   SizeZero :: Size 'EmptyCtx
   SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)
 
+-- | Renders as integer literal
+instance Show (Size ctx) where
+  show = show . sizeInt
+
+instance ShowF Size
+
 -- | Convert a context size to an 'Int'.
 sizeInt :: Size ctx -> Int
 sizeInt SizeZero = 0
@@ -180,10 +191,16 @@
   DiffHere :: Diff ctx ctx
   DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp)
 
--- | The identity difference.
+-- | The identity difference. Identity element of 'Category' instance.
 noDiff :: Diff l l
 noDiff = DiffHere
 
+-- | The addition of differences. Flipped binary operation
+-- of 'Category' instance.
+addDiff :: Diff a b -> Diff b c -> Diff a c
+addDiff x DiffHere = x
+addDiff x (DiffThere y) = DiffThere (addDiff x y)
+
 -- | Extend the difference to a sub-context of the right side.
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight diff = DiffThere diff
@@ -192,13 +209,10 @@
 appendDiff SizeZero = DiffHere
 appendDiff (SizeSucc sz) = DiffThere (appendDiff sz)
 
-composeDiff :: Diff a b -> Diff b c -> Diff a c
-composeDiff x DiffHere = x
-composeDiff x (DiffThere y) = DiffThere (composeDiff x y)
-
+-- | Implemented with 'noDiff' and 'addDiff'
 instance Cat.Category Diff where
   id = DiffHere
-  d1 . d2 = composeDiff d2 d1
+  d1 . d2 = addDiff d2 d1
 
 -- | Extend the size by a given difference.
 extSize :: Size l -> Diff l r -> Size r
@@ -364,10 +378,27 @@
 intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
 intIndex n sz = listToMaybe $ drop n $ indexList sz
 
+-- | Renders as integer literal
 instance Show (Index ctx tp) where
    show = show . indexVal
 
 instance ShowF (Index ctx)
+
+-- | View of indexes as pointing to the last element in the
+-- index range or pointing to an earlier element in a smaller
+-- range.
+data IndexView ctx tp where
+  IndexViewLast :: Size  ctx   -> IndexView (ctx '::> t) t
+  IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t
+
+instance ShowF (IndexView ctx)
+deriving instance Show (IndexView ctx tp)
+
+-- | Project an index
+viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
+viewIndex _ (IndexHere sz) = IndexViewLast sz
+viewIndex _ (IndexThere i) = IndexViewInit i
+-- NB: the unused size parameter is needed in the Unsafe module
 
 ------------------------------------------------------------------------
 -- Assignment
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -13,7 +13,9 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeInType #-}
+{-# OPTIONS_HADDOCK hide #-}
 module Data.Parameterized.Context.Unsafe
   ( module Data.Parameterized.Ctx
   , KnownContext(..)
@@ -30,6 +32,7 @@
     -- * Diff
   , Diff
   , noDiff
+  , addDiff
   , extendRight
   , appendDiff
   , DiffView(..)
@@ -49,6 +52,8 @@
   , forIndex
   , forIndexRange
   , intIndex
+  , IndexView(..)
+  , viewIndex
     -- ** IndexRange
   , IndexRange
   , allRange
@@ -131,6 +136,8 @@
 instance Show (Size ctx) where
   show (Size i) = show i
 
+instance ShowF Size
+
 -- | A context that can be determined statically at compiler time.
 class KnownContext (ctx :: Ctx k) where
   knownSize :: Size ctx
@@ -151,10 +158,17 @@
 
 type role Diff nominal nominal
 
--- | The identity difference.
+-- | The identity difference. Identity element of 'Category' instance.
 noDiff :: Diff l l
 noDiff = Diff 0
+{-# INLINE noDiff #-}
 
+-- | The addition of differences. Flipped binary operation
+-- of 'Category' instance.
+addDiff :: Diff a b -> Diff b c -> Diff a c
+addDiff (Diff x) (Diff y) = Diff (x + y)
+{-# INLINE addDiff #-}
+
 -- | Extend the difference to a sub-context of the right side.
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight (Diff i) = Diff (i+1)
@@ -162,9 +176,10 @@
 appendDiff :: Size r -> Diff l (l <+> r)
 appendDiff (Size r) = Diff r
 
+-- | Implemented with 'noDiff' and 'addDiff'
 instance Cat.Category Diff where
-  id = Diff 0
-  Diff j . Diff i = Diff (i + j)
+  id = noDiff
+  j . i = addDiff i j
 
 -- | Extend the size by a given difference.
 extSize :: Size l -> Diff l r -> Size r
@@ -292,6 +307,24 @@
    show = show . indexVal
 
 instance ShowF (Index ctx)
+
+-- | View of indexes as pointing to the last element in the
+-- index range or pointing to an earlier element in a smaller
+-- range.
+data IndexView ctx tp where
+  IndexViewLast :: !(Size  ctx  ) -> IndexView (ctx '::> t) t
+  IndexViewInit :: !(Index ctx t) -> IndexView (ctx '::> u) t
+
+deriving instance Show (IndexView ctx tp)
+instance ShowF (IndexView ctx)
+
+-- | Project an index
+viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
+viewIndex (Size sz) (Index i)
+  | sz' == i  = unsafeCoerce (IndexViewLast (Size sz'))
+  | otherwise = unsafeCoerce (IndexViewInit (Index i))
+  where
+    sz' = sz-1
 
 ------------------------------------------------------------------------
 -- IndexRange
diff --git a/src/Data/Parameterized/Ctx.hs b/src/Data/Parameterized/Ctx.hs
--- a/src/Data/Parameterized/Ctx.hs
+++ b/src/Data/Parameterized/Ctx.hs
@@ -5,6 +5,10 @@
 
 This module defines type-level lists used for representing the type of
 variables in a context.
+
+A 'Ctx' is never intended to be manipulated at the value level; it is
+used purely as a type-level list, just like @'[]@. To see how it is
+used, see the module header for "Data.Parameterized.Context".
 -}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
diff --git a/src/Data/Parameterized/DataKind.hs b/src/Data/Parameterized/DataKind.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/DataKind.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Data.Parameterized.DataKind
+  ( PairRepr(..), Fst, Snd, fst, snd
+  ) where
+
+import           Data.Parameterized.Classes
+import qualified Data.Parameterized.TH.GADT as TH
+
+import           Prelude hiding ( fst, snd )
+
+data PairRepr (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)) where
+  PairRepr :: f a -> g b -> PairRepr f g '(a, b)
+
+type family Fst (pair :: (k1, k2)) where
+  Fst '(a, _) = a
+type family Snd (pair :: (k1, k2)) where
+  Snd '(_, b) = b
+
+fst :: PairRepr f g p -> f (Fst p)
+fst (PairRepr a _) = a
+
+snd :: PairRepr f g p -> g (Snd p)
+snd (PairRepr _ b) = b
+
+$(return [])
+
+instance ( ShowF f, ShowF g ) => Show (PairRepr f g p) where
+  show (PairRepr a b) = showChar '(' . showsF a . showChar ',' . showsF b $ ")"
+instance ( ShowF f, ShowF g ) => ShowF (PairRepr f g)
+
+deriving instance ( Eq (f a), Eq (g b) ) => Eq (PairRepr f g '(a, b))
+instance ( TestEquality f, TestEquality g ) => TestEquality (PairRepr f g) where
+  testEquality =
+    $(TH.structuralTypeEquality [t|PairRepr|]
+      [
+        ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|testEquality|] )
+      , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|testEquality|] )
+      ])
+
+deriving instance ( Ord (f a), Ord (g b) ) => Ord (PairRepr f g '(a, b))
+instance ( OrdF f, OrdF g ) => OrdF (PairRepr f g) where
+  compareF =
+    $(TH.structuralTypeOrd [t|PairRepr|]
+      [ ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|compareF|] )
+      , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|compareF|] )
+      ])
diff --git a/src/Data/Parameterized/List.hs b/src/Data/Parameterized/List.hs
--- a/src/Data/Parameterized/List.hs
+++ b/src/Data/Parameterized/List.hs
@@ -8,8 +8,117 @@
 second is a list of types with kind @k@ that provide the indices for
 the values in the list.
 
-This type is closely related to the @Context@ type in
-@Data.Parameterized.Context@.
+This type is closely related to the
+'Data.Parameterized.Context.Assignment' type in
+"Data.Parameterized.Context".
+
+= Motivating example - the 'Data.Parameterized.List.List' type
+
+For this example, we need the following extensions:
+
+@
+\{\-\# LANGUAGE DataKinds \#\-\}
+\{\-\# LANGUAGE GADTs \#\-\}
+\{\-\# LANGUAGE KindSignatures \#\-\}
+\{\-\# LANGUAGE TypeOperators \#\-\}
+@
+
+We also require the following imports:
+
+@
+import Data.Parameterized
+import Data.Parameterized.List
+import GHC.TypeLits
+@
+
+Suppose we have a bitvector type:
+
+@
+data BitVector (w :: Nat) :: * where
+  BV :: NatRepr w -> Integer -> BitVector w
+@
+
+This type contains a 'Data.Parameterized.NatRepr.NatRepr', a value-level
+representative of the vector width, and an 'Integer', containing the
+actual value of the bitvector. We can create values of this type as
+follows:
+
+@
+BV (knownNat @8) 0xAB
+@
+
+We can also create a smart constructor to handle the
+'Data.Parameterized.NatRepr.NatRepr' automatically, when the width is known
+from the type context:
+
+@
+bitVector :: KnownNat w => Integer -> BitVector w
+bitVector x = BV knownNat x
+@
+
+Note that this does not check that the value can be represented in the
+given number of bits; that is not important for this example.
+
+If we wish to construct a list of @BitVector@s of a particular length,
+we can do:
+
+@
+[bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8
+@
+
+However, what if we wish to construct a list of 'BitVector's of
+different lengths? We could try:
+
+@
+[bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
+@
+
+However, this gives us an error:
+
+@
+\<interactive\>:3:33: error:
+    • Couldn't match type ‘16’ with ‘8’
+      Expected type: BitVector 8
+        Actual type: BitVector 16
+    • In the expression: bitVector 0x1234 :: BitVector 16
+      In the expression:
+        [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
+      In an equation for ‘it’:
+          it
+            = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
+@
+
+A vanilla Haskell list cannot contain two elements of different types,
+and even though the two elements here are both @BitVector@s, they do
+not have the same type! One solution is to use the
+'Data.Parameterized.Some.Some' type:
+
+@
+[Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]
+@
+
+The type of the above expression is @[Some BitVector]@, which may be
+perfectly acceptable. However, there is nothing in this type that
+tells us what the widths of the bitvectors are, or what the length of
+the overall list is. If we want to actually track that information on
+the type level, we can use the 'List' type from this module.
+
+@
+(bitVector 0xAB :: BitVector 8) :< (bitVector 0x1234 :: BitVector 16) :< Nil
+@
+
+The type of the above expression is @List BitVector '[8, 16]@ -- That
+is, a two-element list of @BitVector@s, where the first element has
+width 8 and the second has width 16.
+
+== Summary
+
+In general, if we have a type constructor @Foo@ of kind @k -> *@ (in
+our example, @Foo@ is just @BitVector@, and we want to create a list
+of @Foo@s where the parameter @k@ varies, /and/ we wish to keep track
+of what each value of @k@ is inside the list at compile time, we can
+use the 'Data.Parameterized.List.List' type for this purpose.
+
 -}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -40,10 +149,10 @@
   ) where
 
 import qualified Control.Lens as Lens
-import Prelude hiding ((!!))
+import           Prelude hiding ((!!))
 
-import Data.Parameterized.Classes
-import Data.Parameterized.TraversableFC
+import           Data.Parameterized.Classes
+import           Data.Parameterized.TraversableFC
 
 -- | Parameterized list of elements.
 data List :: (k -> *) -> [k] -> * where
@@ -137,6 +246,9 @@
         go i (IndexThere x) = seq j $ go j x
           where j = i+1
 
+instance Hashable (Index l x) where
+  hashWithSalt s i = s `hashWithSalt` (indexValue i)
+
 -- | Index 0
 index0 :: Index (x:r) x
 index0 = IndexHere
@@ -172,7 +284,7 @@
     x :< rest -> x :< update rest th upd
 
 -- | Provides a lens for manipulating the element at the given index.
-indexed :: Index l x -> Lens.Simple Lens.Lens (List f l) (f x)
+indexed :: Index l x -> Lens.Lens' (List f l) (f x)
 indexed IndexHere      f (x :< rest) = (:< rest) <$> f x
 indexed (IndexThere i) f (x :< rest) = (x :<) <$> indexed i f rest
 
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -32,6 +32,7 @@
     -- * Query
   , null
   , lookup
+  , findWithDefault
   , member
   , notMember
   , size
@@ -40,6 +41,8 @@
   , elems
   , fromList
   , toList
+  , toAscList
+  , toDescList
   , fromKeys
   , fromKeysM
    -- * Filter
@@ -53,6 +56,8 @@
   , foldrWithKey
   , foldrWithKey'
   , foldMapWithKey
+  , foldlMWithKey
+  , foldrMWithKey
     -- * Traversals
   , map
   , mapWithKey
@@ -60,6 +65,7 @@
   , mapMaybeWithKey
   , traverseWithKey
   , traverseWithKey_
+  , traverseMaybeWithKey
     -- * Complex interface.
   , UpdateRequest(..)
   , Updated(..)
@@ -199,7 +205,8 @@
 -- | Traverse elements in a map
 traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)
 traverse _ Tip = pure Tip
-traverse f (Bin sx kx x l r) = Bin sx kx <$> f x <*> traverse f l <*> traverse f r
+traverse f (Bin sx kx x l r) =
+  (\l' x' r' -> Bin sx kx x' l' r') <$> traverse f l <*> f x <*> traverse f r
 
 -- | Traverse elements in a map
 traverseWithKey
@@ -209,7 +216,7 @@
   -> m (MapF ktp g)
 traverseWithKey _ Tip = pure Tip
 traverseWithKey f (Bin sx kx x l r) =
-   Bin sx kx <$> f kx x <*> traverseWithKey f l <*> traverseWithKey f r
+   (\l' x' r' -> Bin sx kx x' l' r') <$> traverseWithKey f l <*> f kx x <*> traverseWithKey f r
 
 -- | Traverse elements in a map without returning result.
 traverseWithKey_
@@ -217,9 +224,23 @@
   => (forall tp . ktp tp -> f tp -> m ())
   -> MapF ktp f
   -> m ()
-traverseWithKey_ _ Tip = pure ()
-traverseWithKey_ f (Bin _ kx x l r) = f kx x *> traverseWithKey_ f l *> traverseWithKey_ f r
+traverseWithKey_ = \f -> foldrWithKey (\k v r -> f k v *> r) (pure ())
+{-# INLINABLE traverseWithKey_ #-}
 
+-- | Traverse keys\/values and collect the 'Just' results.
+traverseMaybeWithKey :: Applicative f
+                     => (forall tp . k tp -> a tp -> f (Maybe (b tp)))
+                     -> MapF k a -> f (MapF k b)
+traverseMaybeWithKey _ Tip = pure Tip
+traverseMaybeWithKey f (Bin _ kx x Tip Tip) = maybe Tip (\x' -> Bin 1 kx x' Tip Tip) <$> f kx x
+traverseMaybeWithKey f (Bin _ kx x l r) =
+    liftA3 combine (traverseMaybeWithKey f l) (f kx x) (traverseMaybeWithKey f r)
+  where
+    combine l' mx r' = seq l' $ seq r' $
+      case mx of
+        Just x' -> Bin.link (Pair kx x') l' r'
+        Nothing -> Bin.merge l' r'
+{-# INLINABLE traverseMaybeWithKey #-}
 
 type instance IndexF   (MapF k v) = k
 type instance IxValueF (MapF k v) = v
@@ -248,6 +269,20 @@
         EQF -> Just x
 {-# INLINABLE lookup #-}
 
+-- | @findWithDefault d k m@ returns the value bound to @k@ in the map @m@, or @d@
+-- if @k@ is not bound in the map.
+findWithDefault :: OrdF k => a tp -> k tp -> MapF k a -> a tp
+findWithDefault = \def k -> seq k (go def k)
+  where
+    go :: OrdF k => a tp -> k tp -> MapF k a -> a tp
+    go d _ Tip = d
+    go d k (Bin _ kx x l r) =
+      case compareF k kx of
+        LTF -> go d k l
+        GTF -> go d k r
+        EQF -> x
+{-# INLINABLE findWithDefault #-}
+
 -- | Return true if key is bound in map.
 member :: OrdF k => k tp -> MapF k a -> Bool
 member k0 = seq k0 (go k0)
@@ -308,9 +343,7 @@
 foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b
 foldrWithKey _ z Tip = z
 foldrWithKey f z (Bin _ kx x l r) =
-  let rz = foldrWithKey f z r
-      kz = f kx x rz
-   in foldrWithKey f kz l
+  foldrWithKey f (f kx x (foldrWithKey f z r)) l
 
 -- | Perform a strict right fold with the key also provided.
 foldrWithKey' :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b
@@ -325,6 +358,15 @@
 foldMapWithKey _ Tip = mempty
 foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r
 
+-- | A monadic left-to-right fold over keys and values in the map.
+foldlMWithKey :: Monad m => (forall s . b -> k s -> a s -> m b) -> b -> MapF k a -> m b
+foldlMWithKey f z0 m = foldrWithKey (\k a r z ->  f z k a >>= r) pure m z0
+
+-- | A monadic right-to-left fold over keys and values in the map.
+foldrMWithKey :: Monad m => (forall s . k s -> a s -> b -> m b) -> b -> MapF k a -> m b
+foldrMWithKey f z0 m = foldlWithKey (\r k a z ->  f k a z >>= r) pure m z0
+
+-- | Pretty print keys and values in map.
 showMap :: (forall tp . ktp tp -> String)
         -> (forall tp . rtp tp -> String)
         -> MapF ktp rtp
@@ -406,7 +448,10 @@
 {-# INLINABLE delete #-}
 {-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}
 
--- | Union two sets
+-- | Left-biased union of two maps. The resulting map will
+-- contain the union of the keys of the two arguments. When
+-- a key is contained in both maps the value from the first
+-- map will be preserved.
 union :: OrdF k => MapF k a -> MapF k a -> MapF k a
 union t1 t2 = Bin.union comparePairKeys t1 t2
 {-# INLINABLE union #-}
@@ -481,8 +526,17 @@
 fromList :: OrdF k => [Pair k a] -> MapF k a
 fromList = foldl' (\m (Pair k a) -> insert k a m) Data.Parameterized.Map.empty
 
+-- | Return list of key-values pairs in map in ascending order.
+toAscList :: MapF k a -> [Pair k a]
+toAscList = foldrWithKey (\k x l -> Pair k x : l) []
+
+-- | Return list of key-values pairs in map in descending order.
+toDescList :: MapF k a -> [Pair k a]
+toDescList = foldlWithKey (\l k x -> Pair k x : l) []
+
+-- | Return list of key-values pairs in map.
 toList :: MapF k a -> [Pair k a]
-toList = foldrWithKey (\k x m -> Pair k x : m) []
+toList = toAscList
 
 -- | Generate a map from a foldable collection of keys and a
 -- function from keys to values.
@@ -519,6 +573,23 @@
 filterLtMaybe (JustS k) m = filterLt k m
 
 -- | Merge bindings in two maps to get a third.
+--
+-- The first function is used to merge elements that occur under the
+-- same key in both maps. Return Just to add an entry into the
+-- resulting map under this key or Nothing to remove this key from the
+-- resulting map.
+--
+-- The second function will be applied to submaps of the first map argument
+-- where no keys overlap with the second map argument. The result of this
+-- function must be a map with a subset of the keys of its argument.
+-- This means the function can alter the values of its argument and it can
+-- remove key-value pairs from it, but it must not introduce new keys.
+--
+-- Third function is analogous to the second function except that it applies
+-- to the second map argument of 'mergeWithKeyM' instead of the first.
+--
+-- Common examples of the two functions include 'id' when constructing a union
+-- or 'const' 'empty' when constructing an intersection.
 mergeWithKeyM :: forall k a b c m
                . (Applicative m, OrdF k)
               => (forall tp . k tp -> a tp -> b tp -> m (Maybe (c tp)))
@@ -579,7 +650,7 @@
 
 
 
--- Helper function for 'mergeWithKey'. The @'trimLookupLo' lk hk t@ performs both
+-- Helper function for 'mergeWithKeyM'. The @'trimLookupLo' lk hk t@ performs both
 -- @'trim' (JustS lk) hk t@ and @'lookup' lk t@.
 
 -- See Note: Type of local 'go' function
diff --git a/src/Data/Parameterized/Nonce.hs b/src/Data/Parameterized/Nonce.hs
--- a/src/Data/Parameterized/Nonce.hs
+++ b/src/Data/Parameterized/Nonce.hs
@@ -39,6 +39,7 @@
   , newIONonceGenerator
   , withIONonceGenerator
   , withSTNonceGenerator
+  , runSTNonceGenerator
     -- * Global nonce generator
   , withGlobalSTNonceGenerator
   , GlobalNonceGenerator
@@ -103,12 +104,21 @@
 newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))
 newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0)
 
+-- | This combines `runST` and `newSTNonceGenerator` to create a nonce
+-- generator that shares the same phantom type parameter as the @ST@ monad.
+--
+-- This can be used to reduce the number of type parameters when we know a
+-- ST computation only needs a single `NonceGenerator`.
+runSTNonceGenerator :: (forall s . NonceGenerator (ST s) s -> ST s a)
+                    -> a
+runSTNonceGenerator f = runST $ f . STNG =<< newSTRef 0
+
 -- | Create a new nonce generator in the 'ST' monad.
 newIONonceGenerator :: IO (Some (NonceGenerator IO))
 newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0)
 
 -- | Run a 'ST' computation with a new nonce generator in the 'ST' monad.
-withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> (ST t) r) -> ST t r
+withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> ST t r) -> ST t r
 withSTNonceGenerator f = do
   Some r <- newSTNonceGenerator
   f r
diff --git a/src/Data/Parameterized/Nonce/Unsafe.hs b/src/Data/Parameterized/Nonce/Unsafe.hs
--- a/src/Data/Parameterized/Nonce/Unsafe.hs
+++ b/src/Data/Parameterized/Nonce/Unsafe.hs
@@ -1,6 +1,6 @@
 ------------------------------------------------------------------------
 -- |
--- Module           : Data.Parameterized.NonceGenerator
+-- Module           : Data.Parameterized.Nonce.Unsafe
 -- Description      : A counter in the ST monad.
 -- Copyright        : (c) Galois, Inc 2014
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
@@ -19,28 +19,16 @@
 -- Nonces from different origins would allow users to build 'unsafeCoerce'
 -- via the 'testEquality' function.
 --
--- A somewhat safer API would be to brand the generated Nonces with the
--- state type variable of the NonceGenerator whence they came, and to only
--- provide NonceGenerators via a Rank-2 continuation-passing API, similar to
--- 'runST'. This would (via a meta-argument involving parametricity)
--- help to prevent nonces of different origin from being compared.
--- However, this would force us to push the 'ST' type brand into a significant
--- number of other structures and APIs.
---
--- Another alternative would be to use 'unsafePerformIO' magic to make
--- a global nonce generator, and make that the only way to generate nonces.
--- It is not clear that this is actually an improvement from a type safety
--- point of view, but an argument could be made.
---
--- For now, be careful using Nonces, and ensure that you do not mix
--- Nonces from different NonceGenerators.
-------------------------------------------------------------------------
+-- This module is deprecated, and should not be used in new code.
+-- Clients of this module should migrate to use "Data.Parameterized.Nonce".
+-------------------------------------------------------------------------
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE Unsafe #-}
 module Data.Parameterized.Nonce.Unsafe
+  {-# DEPRECATED "Migrate to use Data.Parameterized.Nonce instead, this module will be removed soon." #-}
   ( NonceGenerator
   , newNonceGenerator
   , freshNonce
diff --git a/src/Data/Parameterized/Pair.hs b/src/Data/Parameterized/Pair.hs
--- a/src/Data/Parameterized/Pair.hs
+++ b/src/Data/Parameterized/Pair.hs
@@ -1,5 +1,5 @@
 {-|
-nDescription : A 2-tuple with identically parameterized elements
+Description : A 2-tuple with identically parameterized elements
 Copyright   : (c) Galois, Inc 2017-2019
 
 This module defines a 2-tuple where both elements are parameterized over the
diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs
--- a/src/Data/Parameterized/Peano.hs
+++ b/src/Data/Parameterized/Peano.hs
@@ -45,7 +45,7 @@
      Peano
      , Z , S
 
-     -- * Basic arithmetic 
+     -- * Basic arithmetic
      , Plus, Minus, Mul,  Max, Min
      , plusP, minusP, mulP, maxP, minP
      , zeroP, succP, predP
@@ -53,7 +53,6 @@
      -- * Counting
      , Repeat, CtxSizeP
      , repeatP, ctxSizeP
-     
      -- * Comparisons
      , Le, Lt, Gt, Ge
      , leP, ltP, gtP, geP
@@ -64,7 +63,7 @@
      , PeanoView(..), peanoView, viewRepr
 
      -- * 'Some Peano'
-     , mkPeanoRepr, peanoValue     
+     , mkPeanoRepr, peanoValue
      , somePeano
      , maxPeano
      , minPeano
@@ -88,7 +87,6 @@
 import           Data.Parameterized.Some
 import           Data.Parameterized.Context
 
-import           Data.Hashable
 import           Data.Word
 
 #ifdef UNSAFE_OPS
@@ -185,7 +183,7 @@
 peanoValue ZRepr     = 0
 peanoValue (SRepr m) = 1 + peanoValue m
 #endif
-                                    
+
 -- | When we have optimized the runtime representation,
 -- we need to have a "view" that decomposes the representation
 -- into the standard form.
@@ -227,13 +225,13 @@
   testEquality (PeanoRepr m) (PeanoRepr n)
     | m == n = Just (unsafeCoerce Refl)
     | otherwise = Nothing
-#else 
+#else
   testEquality ZRepr ZRepr = Just Refl
   testEquality (SRepr m1) (SRepr m2)
     | Just Refl <- testEquality m1 m2
     = Just Refl
   testEquality _ _ = Nothing
-  
+
 #endif
 
 instance DecidableEq PeanoRepr where
@@ -418,7 +416,7 @@
 mkPeanoRepr 0 = Some ZRepr
 mkPeanoRepr n = case mkPeanoRepr (n - 1) of
                  Some mr -> Some (SRepr mr)
-#endif                 
+#endif
 
 -- | Turn an @Integral@ value into a 'PeanoRepr'.  Returns @Nothing@
 --   if the given value is negative.
@@ -468,7 +466,7 @@
 -- | Minus distributes over plus
 --
 minusPlusAxiom :: forall n t t'.
-  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->    
+  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->
   Minus n (Plus t' t) :~: Minus (Minus n t') t
 #ifdef UNSAFE_OPS
 minusPlusAxiom _n _t _t' = unsafeCoerce Refl
diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs
--- a/src/Data/Parameterized/Some.hs
+++ b/src/Data/Parameterized/Some.hs
@@ -21,6 +21,7 @@
 
 import Data.Hashable
 import Data.Parameterized.Classes
+import Data.Parameterized.TraversableF
 
 
 data Some (f:: k -> *) = forall x . Some (f x)
@@ -58,3 +59,7 @@
 -- | Modify the inner value.
 traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m ()
 traverseSome_ f (Some x) = (\_ -> ()) `fmap` f x
+
+instance FunctorF     Some where fmapF     = mapSome
+instance FoldableF    Some where foldMapF  = foldMapFDefault
+instance TraversableF Some where traverseF = traverseSome
diff --git a/src/Data/Parameterized/TH/GADT.hs b/src/Data/Parameterized/TH/GADT.hs
--- a/src/Data/Parameterized/TH/GADT.hs
+++ b/src/Data/Parameterized/TH/GADT.hs
@@ -23,6 +23,7 @@
   , structuralTraversal
   , structuralShowsPrec
   , structuralHash
+  , structuralHashWithSalt
   , PolyEq(..)
     -- * Template haskell utilities that may be useful in other contexts.
   , DataD
@@ -91,9 +92,8 @@
     False -> return False
 matchTypePat _ AnyType _ = return True
 matchTypePat tps (DataArg i) tp
-  | i < 0 || i > length tps = error $ "Illegal type pattern index " ++ show i
-  | otherwise = do
-    return $ stripSigT (tps !! i) == tp
+  | i < 0 || i >= length tps = error ("Type pattern index " ++ show i ++ " out of bounds")
+  | otherwise = return (stripSigT (tps !! i) == tp)
   where
     -- th-abstraction can annotate type parameters with their kinds,
     -- we ignore these for matching
@@ -104,11 +104,17 @@
   return (tp' == tp)
 matchTypePat _ _ _ = return False
 
+-- | The dataParamTypes function returns the list of Type arguments
+-- for the constructor.  For example, if passed the DatatypeInfo for a
+-- @newtype Id a = MkId a@ then this would return @['SigT' ('VarT' a)
+-- 'StarT']@.  Note that there may be type *variables* not referenced
+-- in the returned array; this simply returns the type *arguments*.
 dataParamTypes :: DatatypeInfo -> [Type]
-dataParamTypes = datatypeVars
+dataParamTypes = datatypeInstTypes
+ -- see th-abstraction 'dataTypeVars' for the type variables if needed
 
 -- | Find value associated with first pattern that matches given pat if any.
-assocTypePats :: [Type] -> [(TypePat,v)] -> Type -> Q (Maybe v)
+assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)
 assocTypePats _ [] _ = return Nothing
 assocTypePats dTypes ((p,v):pats) tp = do
   r <- matchTypePat dTypes p tp
@@ -141,7 +147,7 @@
 
 matchEqArguments :: [Type]
                     -- ^ Types bound by data arguments.
-                  -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments
+                 -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments
                  -> Name
                      -- ^ Name of constructor.
                  -> Set Name
@@ -193,7 +199,10 @@
       -> Bool -- ^ wildcard case required
       -> ExpQ
 mkEqF d pats con =
-  let dVars = datatypeVars d
+  let dVars = dataParamTypes d  -- the type arguments for the constructor
+      -- bnd is the list of type arguments for this datatype.  Since
+      -- this is Functor equality, ignore the final type since this is
+      -- a higher-kinded equality.
       bnd | null dVars = Set.empty
           | otherwise  = typeVars (init dVars)
   in mkSimpleEqF dVars bnd pats con
@@ -346,16 +355,19 @@
        -> Maybe ExpQ -- ^ optional right constructr index
        -> [Name]
        -> Q [MatchQ]
-mkOrdF d pats = mkSimpleOrdF (datatypeVars d) pats
+mkOrdF d pats = mkSimpleOrdF (datatypeInstTypes d) pats
 
--- | @recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@.
-recurseArg :: (Type -> Q (Maybe ExpQ))
-           -> ExpQ -- ^ Function to apply
-           -> ExpQ
-           -> Type
-           -> Q (Maybe Exp)
-recurseArg m f v tp = do
-  mr <- m tp
+-- | @genTraverseOfType f var tp@ applies @f@ to @var@ where @var@ has type @tp@.
+genTraverseOfType :: [Type]
+                    -- ^ Argument types for the data declaration.
+                 -> [(TypePat, ExpQ)]
+                    -- ^ Patterrns the user provided for overriding type lookup.
+                  -> ExpQ -- ^ Function to apply
+                  -> ExpQ -- ^ Expression denoting value of this constructor field.
+                  -> Type -- ^ Type bound for this constructor field.
+                  -> Q (Maybe Exp)
+genTraverseOfType dataArgs pats f v tp = do
+  mr <- assocTypePats dataArgs pats tp
   case mr of
     Just g ->  Just <$> [| $(g) $(f) $(v) |]
     Nothing ->
@@ -364,16 +376,18 @@
         AppT (VarT _) _ -> Just <$> [| $(f) $(v) |]
         _ -> return Nothing
 
--- | @traverseAppMatch f c@ builds a case statement that matches a term with
+-- | @traverseAppMatch patMatch cexp @ builds a case statement that matches a term with
 -- the constructor @c@ and applies @f@ to each argument.
-traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- ^ Pattern match function
-                 -> ExpQ -- ^ Function to apply to each argument recursively.
+traverseAppMatch :: [Type]
+                    -- ^ Argument types for the data declaration.
+                 -> [(TypePat, ExpQ)]
+                    -- ^ Patterrns the user provided for overriding type lookup.
+                 -> ExpQ -- ^ Function @f@ given to `traverse`
                  -> ConstructorInfo -- ^ Constructor to match.
-                 -> MatchQ -- ^ Match expression that
-traverseAppMatch pats fv c0 = do
+                 -> MatchQ
+traverseAppMatch dataArgs pats fv c0 = do
   (pat,patArgs) <- conPat c0 "p"
-  exprs <- zipWithM (recurseArg pats fv) (varE <$> patArgs) (constructorFields c0)
-
+  exprs <- zipWithM (genTraverseOfType dataArgs pats fv) (varE <$> patArgs) (constructorFields c0)
   let mkRes :: ExpQ -> [(Name, Maybe Exp)] -> ExpQ
       mkRes e [] = e
       mkRes e ((v,Nothing):r) =
@@ -405,28 +419,56 @@
   a <- newName "a"
   lamE [varP f, varP a] $
       caseE (varE a)
-      (traverseAppMatch (assocTypePats (datatypeVars d) pats0) (varE f) <$> datatypeCons d)
+      (traverseAppMatch (datatypeInstTypes d) pats0 (varE f) <$> datatypeCons d)
 
-asTypeCon :: Monad m => String -> Type -> m Name
+asTypeCon :: String -> Type -> Q Name
 asTypeCon _ (ConT nm) = return nm
-asTypeCon fn _ = fail $ fn ++ " expected type constructor."
+asTypeCon fn _ = fail (fn ++ " expected type constructor.")
 
 -- | @structuralHash tp@ generates a function with the type
 -- @Int -> tp -> Int@ that hashes type.
+--
+-- All arguments use `hashable`, and `structuralHashWithSalt` can be
+-- used instead as it allows user-definable patterns to be used at
+-- specific types.
 structuralHash :: TypeQ -> ExpQ
-structuralHash tpq = do
+structuralHash tpq = structuralHashWithSalt tpq []
+{-# DEPRECATED structuralHash "Use structuralHashWithSalt" #-}
+
+-- | @structuralHashWithSalt tp@ generates a function with the type
+-- @Int -> tp -> Int@ that hashes type.
+--
+-- The second arguments is for generating user-defined patterns to replace
+-- `hashWithSalt` for specific types.
+structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
+structuralHashWithSalt tpq pats = do
   d <- reifyDatatype =<< asTypeCon "structuralHash" =<< tpq
   s <- newName "s"
   a <- newName "a"
   lamE [varP s, varP a] $
-    caseE (varE a) (zipWith (matchHashCtor (varE s)) [0..] (datatypeCons d))
+    caseE (varE a) (zipWith (matchHashCtor d pats (varE s)) [0..] (datatypeCons d))
 
-matchHashCtor :: ExpQ -> Integer  -> ConstructorInfo -> MatchQ
-matchHashCtor s0 i c = do
+-- | This matches one of the constructors in a datatype when generating
+-- a `hashWithSalt` function.
+matchHashCtor :: DatatypeInfo
+                 -- ^ Data declaration of type we are hashing.
+              -> [(TypePat, ExpQ)]
+                 -- ^ User provide type patterns
+              -> ExpQ -- ^ Initial salt expression
+              -> Integer -- ^ Index of constructor
+              -> ConstructorInfo -- ^ Constructor information
+              -> MatchQ
+matchHashCtor d pats s0 i c = do
   (pat,vars) <- conPat c "x"
-  let args = [| $(litE (IntegerL i)) :: Int |] : (varE <$> vars)
-  let go s e = [| hashWithSalt $(s) $(e) |]
-  let rhs = foldl go s0 args
+  let go s (e, tp) = do
+        mr <- assocTypePats (datatypeInstTypes d) pats tp
+        case mr of
+          Just f -> do
+            [| $(f) $(s) $(e) |]
+          Nothing ->
+            [| hashWithSalt $(s) $(e) |]
+  let s1 = [| hashWithSalt $(s0) ($(litE (IntegerL i)) :: Int) |]
+  let rhs = foldl go s1 (zip (varE <$> vars) (constructorFields c))
   match (pure pat) (normalB rhs) []
 
 -- | @structuralShow tp@ generates a function with the type
@@ -443,10 +485,10 @@
 showCon p nm n = do
   vars <- newNames "x" n
   let pat = ConP nm (VarP <$> vars)
-  let go s e = [| $(s) . showChar ' ' . showsPrec 10 $(varE e) |]
+  let go s e = [| $(s) . showChar ' ' . showsPrec 11 $(varE e) |]
   let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |]
   let rhs | null vars = ctor
-          | otherwise = [| showParen ($(p) >= 10) $(foldl go ctor vars) |]
+          | otherwise = [| showParen ($(p) >= 11) $(foldl go ctor vars) |]
   match (pure pat) (normalB rhs) []
 
 matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ
diff --git a/src/Data/Parameterized/TraversableF.hs b/src/Data/Parameterized/TraversableF.hs
--- a/src/Data/Parameterized/TraversableF.hs
+++ b/src/Data/Parameterized/TraversableF.hs
@@ -16,12 +16,19 @@
 module Data.Parameterized.TraversableF
   ( FunctorF(..)
   , FoldableF(..)
+  , foldlMF
+  , foldlMF'
+  , foldrMF
+  , foldrMF'
   , TraversableF(..)
   , traverseF_
+  , forF_
+  , forF
   , fmapFDefault
   , foldMapFDefault
   , allF
   , anyF
+  , lengthF
   ) where
 
 import Control.Applicative
@@ -82,6 +89,26 @@
   toListF :: (forall tp . f tp -> a) -> t f -> [a]
   toListF f t = build (\c n -> foldrF (\e v -> c (f e) v) n t)
 
+-- | Monadic fold over the elements of a structure from left to right.
+foldlMF :: (FoldableF t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f -> m b
+foldlMF f z0 xs = foldrF f' return xs z0
+  where f' x k z = f z x >>= k
+
+-- | Monadic strict fold over the elements of a structure from left to right.
+foldlMF' :: (FoldableF t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f -> m b
+foldlMF' f z0 xs = seq z0 (foldrF f' return xs z0)
+  where f' x k z = f z x >>= \r -> seq r (k r)
+
+-- | Monadic fold over the elements of a structure from right to left.
+foldrMF :: (FoldableF t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f -> m b
+foldrMF f z0 xs = foldlF f' return xs z0
+  where f' k x z = f x z >>= k
+
+-- | Monadic strict fold over the elements of a structure from right to left.
+foldrMF' :: (FoldableF t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f -> m b
+foldrMF' f z0 xs = seq z0 $ foldlF f' return xs z0
+  where f' k x z = f x z >>= \r -> seq r (k r)
+
 -- | Return 'True' if all values satisfy the predicate.
 allF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool
 allF p = getAll #. foldMapF (All #. p)
@@ -90,6 +117,10 @@
 anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool
 anyF p = getAny #. foldMapF (Any #. p)
 
+-- | Return number of elements that we fold over.
+lengthF :: FoldableF t => t f -> Int
+lengthF = foldrF (const (+1)) 0
+
 instance FoldableF (Const x) where
   foldMapF _ _ = mempty
 
@@ -105,6 +136,11 @@
 instance TraversableF (Const x) where
   traverseF _ (Const x) = pure (Const x)
 
+-- | Flipped 'traverseF'
+forF :: (TraversableF t, Applicative m) => t e -> (forall s . e s -> m (f s)) -> m (t f)
+forF f x = traverseF x f
+{-# INLINE forF #-}
+
 -- | This function may be used as a value for `fmapF` in a `FunctorF`
 -- instance.
 fmapFDefault :: TraversableF t => (forall s . e s -> f s) -> t e -> t f
@@ -120,6 +156,13 @@
 -- these actions from left to right, and ignore the results.
 traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f ()
 traverseF_ f = foldrF (\e r -> f e *> r) (pure ())
+
+
+-- | Map each element of a structure to an action, evaluate
+-- these actions from left to right, and ignore the results.
+forF_ :: (FoldableF t, Applicative m) => t f -> (forall x. f x -> m a) -> m ()
+forF_ v f = traverseF_ f v
+{-# INLINE forF_ #-}
 
 ------------------------------------------------------------------------
 -- TraversableF (Compose s t)
diff --git a/src/Data/Parameterized/TraversableFC.hs b/src/Data/Parameterized/TraversableFC.hs
--- a/src/Data/Parameterized/TraversableFC.hs
+++ b/src/Data/Parameterized/TraversableFC.hs
@@ -19,9 +19,15 @@
   , HashableFC(..)
   , FunctorFC(..)
   , FoldableFC(..)
+  , foldlMFC
+  , foldlMFC'
+  , foldrMFC
+  , foldrMFC'
   , TraversableFC(..)
   , traverseFC_
   , forMFC_
+  , forFC_
+  , forFC
   , fmapFCDefault
   , foldMapFCDefault
   , allFC
@@ -117,6 +123,26 @@
   toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])
   toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)
 
+-- | Monadic fold over the elements of a structure from left to right.
+foldlMFC :: (FoldableFC t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f c -> m b
+foldlMFC f z0 xs = foldrFC f' return xs z0
+  where f' x k z = f z x >>= k
+
+-- | Monadic strict fold over the elements of a structure from left to right.
+foldlMFC' :: (FoldableFC t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f c -> m b
+foldlMFC' f z0 xs = seq z0 $ foldrFC f' return xs z0
+  where f' x k z = f z x >>= \r -> seq r (k r)
+
+-- | Monadic fold over the elements of a structure from right to left.
+foldrMFC :: (FoldableFC t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f c -> m b
+foldrMFC f z0 xs = foldlFC f' return xs z0
+  where f' k x z = f x z >>= k
+
+-- | Monadic strict fold over the elements of a structure from right to left.
+foldrMFC' :: (FoldableFC t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f c -> m b
+foldrMFC' f z0 xs = seq z0 (foldlFC f' return xs z0)
+  where f' k x z = f x z >>= \r -> seq r (k r)
+
 -- | Return 'True' if all values satisfy predicate.
 allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)
 allFC p = getAll #. foldMapFC (All #. p)
@@ -125,7 +151,7 @@
 anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)
 anyFC p = getAny #. foldMapFC (Any #. p)
 
--- | Return number of elements in list.
+-- | Return number of elements that we fold over.
 lengthFC :: FoldableFC t => t f x -> Int
 lengthFC = foldrFC (const (+1)) 0
 
@@ -160,3 +186,17 @@
 forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
 forMFC_ v f = traverseFC_ f v
 {-# INLINE forMFC_ #-}
+{-# DEPRECATED forMFC_ "Use forFC_" #-}
+
+-- | Map each element of a structure to an action, evaluate
+-- these actions from left to right, and ignore the results.
+forFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
+forFC_ v f = traverseFC_ f v
+{-# INLINE forFC_ #-}
+
+-- | Flipped 'traverseFC'
+forFC ::
+  (TraversableFC t, Applicative m) =>
+  t f x -> (forall y. f y -> m (g y)) -> m (t g x)
+forFC v f = traverseFC f v
+{-# INLINE forFC #-}
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -4,21 +4,22 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 module Test.Context
-( contextTests
-) where
-
-import Test.Tasty
-import Test.QuickCheck
-import Test.Tasty.QuickCheck
-
-import Control.Lens
-import Data.Parameterized.Classes
-import Data.Parameterized.TraversableFC
-import Data.Parameterized.Some
+  ( contextTests
+  )
+where
 
+import           Control.Lens
+import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as C
 import qualified Data.Parameterized.Context.Safe as S
 import qualified Data.Parameterized.Context.Unsafe as U
+import           Data.Parameterized.Some
+import           Data.Parameterized.TraversableFC
+import           Hedgehog
+import qualified Hedgehog.Gen as HG
+import           Hedgehog.Range
+import           Test.Tasty
+import           Test.Tasty.Hedgehog
 
 data Payload (ty :: *) where
   IntPayload    :: Int -> Payload Int
@@ -38,13 +39,17 @@
 
 instance ShowF Payload
 
-instance Arbitrary (Some Payload) where
-  arbitrary = oneof
-    [ Some . IntPayload <$> arbitrary
-    , Some . StringPayload <$> arbitrary
-    , Some . BoolPayload <$> arbitrary
-    ]
+genSomePayload :: Monad m => GenT m (Some Payload)
+genSomePayload = HG.choice [ Some . IntPayload    <$> HG.integral (linearBounded :: Range Int)
+                           , Some . StringPayload <$> HG.string (linear 1 32) HG.ascii
+                           , Some . BoolPayload   <$> HG.element [ True, False ]
+                           ]
 
+-- generate a non-empty list of payload entries
+genSomePayloadList :: Monad m => GenT m [Some Payload]
+genSomePayloadList = HG.list (linear 1 10) genSomePayload
+
+
 type UAsgn = U.Assignment Payload
 type SAsgn = S.Assignment Payload
 
@@ -60,109 +65,120 @@
        go a [] = Some a
        go a (Some x : xs) = go (S.extend a x) xs
 
-instance Arbitrary (Some UAsgn) where
-  arbitrary = mkUAsgn <$> arbitrary
-instance Arbitrary (Some SAsgn) where
-  arbitrary = mkSAsgn <$> arbitrary
 
 twiddle :: Payload a -> Payload a
 twiddle (IntPayload n) = IntPayload (n+1)
 twiddle (StringPayload str) = StringPayload (str++"asdf")
 twiddle (BoolPayload b) = BoolPayload (not b)
 
+
 contextTests :: IO TestTree
 contextTests = testGroup "Context" <$> return
-   [ testProperty "safe_index_eq" $ \v vs i -> ioProperty $ do
-         let vals = v:vs
-         let i' = min (max 0 i) (length vals - 1)
-         Some a <- return $ mkSAsgn vals
-         Just (Some idx) <- return $ S.intIndex i' (S.size a)
-         return (Some (a S.! idx) == vals !! i')
-   , testProperty "unsafe_index_eq" $ \v vs i -> ioProperty $ do
-         let vals = v:vs
-         let i' = min (max 0 i) (length vals - 1)
-         Some a <- return $ mkUAsgn vals
-         Just (Some idx) <- return $ U.intIndex i' (U.size a)
-         return (Some (a U.! idx) == vals !! i')
-   , testProperty "safe_tolist" $ \vals -> ioProperty $ do
-         Some a <- return $ mkSAsgn vals
-         let vals' = toListFC Some a
-         return (vals == vals')
-   , testProperty "unsafe_tolist" $ \vals -> ioProperty $ do
-         Some a <- return $ mkUAsgn vals
-         let vals' = toListFC Some a
-         return (vals == vals')
-   , testProperty "adjust test monadic" $ \v vs i -> ioProperty $ do
-         let vals = v:vs  -- ensures vals is not an empty array
-         Some x <- return $ mkUAsgn vals
-         Some y <- return $ mkSAsgn vals
-         let i' = min (max 0 i) (length vals - 1)
+   [ testProperty "safe_index_eq" $ property $
+     do vals <- forAll genSomePayloadList
+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+        Some a <- return $ mkSAsgn vals
+        Just (Some idx) <- return $ S.intIndex i' (S.size a)
+        Some (a S.! idx) === vals !! i'
 
-         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+   , testProperty "unsafe_index_eq" $ property $
+     do vals <- forAll genSomePayloadList
+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+        Some a <- return $ mkUAsgn vals
+        Just (Some idx) <- return $ U.intIndex i' (U.size a)
+        Some (a U.! idx) === vals !! i'
 
-         x' <- U.adjustM (return . twiddle) idx_x x
-         y' <- S.adjustM (return . twiddle) idx_y y
+   , testProperty "safe_tolist" $ property $
+     do vals <- forAll genSomePayloadList
+        Some a <- return $ mkSAsgn vals
+        let vals' = toListFC Some a
+        vals === vals'
+   , testProperty "unsafe_tolist" $ property $
+     do vals <- forAll genSomePayloadList
+        Some a <- return $ mkUAsgn vals
+        let vals' = toListFC Some a
+        vals === vals'
 
-         return (toListFC Some x' == toListFC Some y')
+   , testProperty "adjust test monadic" $ property $
+     do vals <- forAll genSomePayloadList
+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
 
-   , testProperty "adjust test" $ \v vs i -> ioProperty $ do
-         let vals = v:vs  -- ensures vals is not an empty array
-         Some x <- return $ mkUAsgn vals
-         Some y <- return $ mkSAsgn vals
-         let i' = min (max 0 i) (length vals - 1)
+        Some x <- return $ mkUAsgn vals
+        Some y <- return $ mkSAsgn vals
 
-         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-         let x' = x & ixF idx_x %~ twiddle
-             y' = y & ixF idx_y %~ twiddle
+        x' <- U.adjustM (return . twiddle) idx_x x
+        y' <- S.adjustM (return . twiddle) idx_y y
 
-         return (toListFC Some x' == toListFC Some y' &&
-                 -- adjust actually modified the entry
-                 toListFC Some x /= toListFC Some x' &&
-                 toListFC Some y /= toListFC Some y')
+        toListFC Some x' === toListFC Some y'
 
-   , testProperty "update test" $ \v vs i -> ioProperty $ do
-         let vals = v:vs  -- ensures vals is not an empty array
-         Some x <- return $ mkUAsgn vals
-         Some y <- return $ mkSAsgn vals
-         let i' = min (max 0 i) (length vals - 1)
+   , testProperty "adjust test" $ property $
+     do vals <- forAll genSomePayloadList
+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
 
-         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+        Some x <- return $ mkUAsgn vals
+        Some y <- return $ mkSAsgn vals
 
-         let x' = over (ixF idx_x) twiddle x
-             y' = (ixF idx_y) %~ twiddle $ y
-             updX = x & ixF idx_x .~ x' U.! idx_x
-             updY = y & ixF idx_y .~ y' S.! idx_y
+        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-         return (toListFC Some updX == toListFC Some updY &&
-                 -- update actually modified the entry
-                 toListFC Some x /= toListFC Some updX &&
-                 toListFC Some y /= toListFC Some updY &&
-                 -- update modified the expected entry
-                 toListFC Some x' == toListFC Some updX &&
-                 toListFC Some y' == toListFC Some updY
-                )
+        let x' = x & ixF idx_x %~ twiddle
+            y' = y & ixF idx_y %~ twiddle
 
-   , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do
-         Some x <- return $ mkSAsgn vals1
-         Some y <- return $ mkSAsgn vals2
-         case testEquality x y of
-           Just Refl -> return $ vals1 == vals2
-           Nothing   -> return $ vals1 /= vals2
-   , testProperty "unsafe_eq" $ \vals1 vals2 -> ioProperty $ do
-         Some x <- return $ mkUAsgn vals1
-         Some y <- return $ mkUAsgn vals2
-         case testEquality x y of
-           Just Refl -> return $ vals1 == vals2
-           Nothing   -> return $ vals1 /= vals2
+        toListFC Some x' === toListFC Some y'
+        -- adjust actually modified the entry
+        toListFC Some x /== toListFC Some x'
+        toListFC Some y /== toListFC Some y'
 
-   , testProperty "append_take" $ \vals1 vals2 -> ioProperty $ do
-         Some x <- return $ mkUAsgn vals1
-         Some y <- return $ mkUAsgn vals2
-         let z = x U.<++> y
-         let x' = C.take (U.size x) (U.size y) z
-         return $ isJust $ testEquality x x'
+   , testProperty "update test" $ property $
+     do vals <- forAll genSomePayloadList
+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+
+        Some x <- return $ mkUAsgn vals
+        Some y <- return $ mkSAsgn vals
+
+        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+
+        let x' = over (ixF idx_x) twiddle x
+            y' = (ixF idx_y) %~ twiddle $ y
+            updX = x & ixF idx_x .~ x' U.! idx_x
+            updY = y & ixF idx_y .~ y' S.! idx_y
+
+        toListFC Some updX === toListFC Some updY
+        -- update actually modified the entry
+        toListFC Some x /== toListFC Some updX
+        toListFC Some y /== toListFC Some updY
+        -- update modified the expected entry
+        toListFC Some x' === toListFC Some updX
+        toListFC Some y' === toListFC Some updY
+
+   , testProperty "safe_eq" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        Some x <- return $ mkSAsgn vals1
+        Some y <- return $ mkSAsgn vals2
+        case testEquality x y of
+          Just Refl -> vals1 === vals2
+          Nothing   -> vals1 /== vals2
+   , testProperty "unsafe_eq" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        Some x <- return $ mkUAsgn vals1
+        Some y <- return $ mkUAsgn vals2
+        case testEquality x y of
+          Just Refl -> vals1 === vals2
+          Nothing   -> vals1 /== vals2
+
+   , testProperty "append_take" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        Some x <- return $ mkUAsgn vals1
+        Some y <- return $ mkUAsgn vals2
+        let z = x U.<++> y
+        let x' = C.take (U.size x) (U.size y) z
+        assert $ isJust $ testEquality x x'
+
    ]
diff --git a/test/Test/NatRepr.hs b/test/Test/NatRepr.hs
--- a/test/Test/NatRepr.hs
+++ b/test/Test/NatRepr.hs
@@ -1,18 +1,23 @@
 module Test.NatRepr
-( natTests
-) where
+  ( natTests
+  )
+where
 
-import Test.Tasty
-import Test.Tasty.QuickCheck
+import           Hedgehog
+import qualified Hedgehog.Gen as HG
+import           Hedgehog.Range
+import           Test.Tasty
+import           Test.Tasty.Hedgehog
 
-import Data.Parameterized.NatRepr
-import Data.Parameterized.Some
-import GHC.TypeLits
+import           Data.Parameterized.NatRepr
+import           Data.Parameterized.Some
+import           GHC.TypeLits
 
 natTests :: IO TestTree
 natTests = testGroup "Nat" <$> return
-  [ testProperty "withKnownNat" $ \nInt ->
+  [ testProperty "withKnownNat" $ property $ do
+      nInt <- forAll $ HG.int (linearBounded :: Range Int)
       case someNat nInt of
-        Nothing -> nInt < 0
-        Just (Some r) -> nInt == withKnownNat r (natVal r)
+        Nothing       -> diff nInt (<) 0
+        Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)
   ]
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
--- a/test/Test/Vector.hs
+++ b/test/Test/Vector.hs
@@ -1,70 +1,91 @@
+{-# LANGUAGE TypeApplications #-}
+{-# Language CPP #-}
 {-# Language DataKinds #-}
 {-# Language ExplicitForAll #-}
-{-# Language TypeOperators #-}
-{-# Language TypeFamilies #-}
 {-# Language FlexibleInstances #-}
 {-# Language ScopedTypeVariables #-}
 {-# Language StandaloneDeriving #-}
-{-# Language CPP #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 #if __GLASGOW_HASKELL__ >= 805
 {-# Language NoStarIsType #-}
 #endif
 module Test.Vector
-( vecTests
-) where
-
-import Test.Tasty
-import Test.Tasty.QuickCheck ( Arbitrary(..), testProperty, vectorOf )
+  ( vecTests
+  )
+where
 
-import Data.Parameterized.NatRepr
-import Data.Parameterized.Vector
-import GHC.TypeLits
-import Data.Semigroup
-import Prelude hiding (reverse)
+import           Data.Parameterized.NatRepr
+import           Data.Parameterized.Vector
+import           Data.Semigroup
+import           GHC.TypeLits
+import           Hedgehog
+import qualified Hedgehog.Gen as HG
+import           Hedgehog.Range
+import           Prelude hiding (reverse)
+import           Test.Tasty
+import           Test.Tasty.Hedgehog
 
 
-instance KnownNat n => Arbitrary (NatRepr n) where
-  arbitrary = return knownNat
-
+genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)
+genVector genElem =
+  do let n = knownNat
+         w = widthVal n
+     l <- HG.list (constant w w) genElem
+     case fromList n l of
+       Just v -> return v
+       Nothing -> error ("fromList failure for size " <> show w)
 
-instance forall a n. ( 1 <= n
-                     , Arbitrary a
-                     , KnownNat n) =>
-         Arbitrary (Vector n a) where
-  arbitrary = do
-    n <- arbitrary
-    l <- vectorOf (widthVal n) arbitrary
-    case fromList n l of
-      Just v -> return v
-      Nothing -> error ("fromList failure for size " <> show n)
+genOrdering :: Monad m => GenT m Ordering
+genOrdering = HG.element [ LT, EQ, GT ]
 
 
 instance Show (Int -> Ordering) where
   show _ = "unshowable"
 
+
 -- We use @Ordering@ just because it's simple
 vecTests :: IO TestTree
 vecTests = testGroup "Vector" <$> return
-  [ testProperty "reverse100" $
-      \n v -> fromList (n :: NatRepr 100) (v :: [Ordering]) ==
-              (reverse <$> (reverse <$> (fromList n v)))
-  , testProperty "reverseSingleton" $
-      \n v -> fromList (n :: NatRepr 1) (v :: [Ordering]) ==
-              (reverse <$> (fromList n v))
-  , testProperty "split-join" $
-      \n w v -> (v :: Vector (5 * 5) Ordering) ==
-                (join (n :: NatRepr 5) $ split n (w :: NatRepr 5) $ v)
+  [ testProperty "reverse100" $ property $
+    do v <- forAll $ genVector @100 genOrdering
+       v === (reverse $ reverse v)
+  , testProperty "reverseSingleton" $ property $
+    do l <- (:[]) <$> forAll genOrdering
+       Just v <- return $ fromList (knownNat @1) l
+       v === reverse v
+
+  , testProperty "split-join" $ property $
+    do let n = knownNat @5
+       v <- forAll $ genVector @(5 * 5) genOrdering
+       v === (join n $ split n (knownNat @5) v)
+
   -- @cons@ is the same for vectors or lists
-  , testProperty "cons" $
-      \n v x -> (cons x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==
-                (fromList (incNat n) (x:v))
+  , testProperty "cons" $ property $
+    do let n = knownNat @20
+           w = widthVal n
+       l <- forAll $ HG.list (constant w w) genOrdering
+       x <- forAll genOrdering
+       (cons x <$> fromList n l) === fromList (incNat n) (x:l)
+
   -- @snoc@ is like appending to a list
-  , testProperty "snoc" $
-      \n v x -> (flip snoc x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==
-                (fromList (incNat n) (v ++ [x]))
+  , testProperty "snoc" $ property $
+    do let n = knownNat @20
+           w = widthVal n
+       l <- forAll $ HG.list (constant w w) genOrdering
+       x <- forAll genOrdering
+       (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])
+
   -- @generate@ is like mapping a function over indices
-  , testProperty "generate" $
-      \n f -> Just (generate (n :: NatRepr 55) ((f :: Int -> Ordering) . widthVal)) ==
-              (fromList (incNat n) (map f [0..widthVal n]) :: Maybe (Vector 56 Ordering))
+  , testProperty "generate" $ property $
+    do let n = knownNat @55
+           w = widthVal n
+           funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values
+           funs =  [ const EQ
+                   , \i -> if i < 10 then LT else if i > 15 then GT else EQ
+                   , \i -> if i == 0 then EQ else GT
+                   ]
+       f <- forAll $ HG.element funs
+       Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])
   ]