diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,138 @@
+# Changelog for the `parameterized-utils` package
+
+## 2.0 -- *2019 Apr 03*
+
+  * Drop support for GHC versions prior to GHC 8.2
+  * Various Haddock and module updates.
+  * Data.Parameterized.Classes
+    - Added function: `ordFCompose`
+    - Added `OrdF` instance for `Compose`
+  * Data.Parameterized.ClassesC
+    - Marked as `Safe` haskell via pragma
+    - Added `OrdC` instance for `Some`
+  * Data.Parameterized.Compose
+    - Update `testEqualityComposeBare` to be more kind-polymorphic.
+    - Marked as `Safe` haskell via pragma
+  * Data.Parameterized.Context
+    - Added `diffIsAppend` function to extract the contextual
+      difference between two `Context`s (as a `Diff`) as an `IsAppend`
+      (new) data value if the left is a sub-context of the right.
+  * Data.Parameterized.NatRepr
+    - Change runtime representation from `Int` to `Natural`
+    - Add function `intValue` to recover an `Int` from a `NatRepr`.
+    - Add constructor function `mkNatRepr` to construct a `NatRepr`
+      from a `Natural`.
+    - Removed awkward backdoor for directly creating `NatRepr` values;
+      the single needed internal usage is now handled internally.
+  * Data.Parameterized.Peano
+    - Newly added module.
+    - Defines a type `Peano` and `PeanoRepr` for representing a
+      type-level natural at runtime.
+    - The runtime representation of `PeanoRepr` is `Word64`
+    - Has both safe and unsafe implementations.
+  * Data.Parameterized.WithRepr
+    - Newly added module.
+    - This module declares a class `IsRepr` with a single method
+      `withRepr` that can be used to derive a 'KnownRepr' constraint
+      from an explicit 'Repr' argument. Clients of this method need
+      only create an empty instance. The default implementation
+      suffices.
+
+## 1.0.8 -- *2019 Feb 01*
+
+  * Data.Parameterized.Map
+    - Fixed `MapF` functions `filter` and `filterWithKey`
+    - Added `MapF` function: `mapWithKey`
+  * Data.Parameterized.NatRepr
+    - Un-deprecate `withKnownNat`
+  * Data.Parameterized.Context
+    - Updated some haddock documentation (esp. `CtxEmbedding` data structure).
+  * Data.Parameterized.Nonce
+    - Fixed `newIONonceGenerator` haddock documentation (IO monad, not ST monad).
+    - Added `countNoncesGenerated` for profiling Nonce usage.
+  * Data.Parameterized.TraversableF
+    - Added `FunctorF`, `FoldableF`, and `TraversableF` instances for
+      `Compose` from Data.Functor.Compose
+  * Data.Parameterized.ClassesC
+    - Newly added module.
+    - Declares `TestEqualityC` and `OrdC` classes for working with
+      types that have kind `(k -> *) -> *` for any `k`.
+  * Data.Parameterized.Compose
+    - Newly added module.
+    - Orphan instance and `testEqualityComposeBare` function for
+      working with Data.Functor.Compose.
+  * Data.Parameterized.TestEquality
+    - Newly added module.
+    - Utilities for working with Data.Type.TestEquality.
+
+## 1.0.7 -- *2018 Nov 17*
+
+  * Data.Parameterized.Map
+    - Added `MapF` functions:
+      - `filter`
+      - `filterWithKey`
+
+## 1.0.6 -- *2018 Nov 19*
+
+  * Add support for GHC 8.6.
+  * Data.Parameterized.Map
+    - Added functions:
+       - `foldlWithKey` and `foldlWithKey'` (strict)
+       - `foldrWithKey` and `foldrWithKey'` (strict)
+       - `mapMaybeWithKey`
+
+## 1.0.5 -- *2018 Sep 04*
+
+  * Data.Parameterized.Context
+      - Add function: `take`, `appendEmbedding`, `appendDiff`
+      - Diff is type role nominal in both parameters.
+
+## 1.0.4 -- *2018 Aug 29*
+
+  * Data.Parameterized.Context
+    - Add `traverseAndCollect`.  Allows traversal of an Assignment in
+      order from left to right, collecting the results of a visitor
+      function monoidically.
+  * Data.Parameterized.DecidableEq
+    - Newly added module.  The `DecidableEq` class represents
+      decideable equality on a type family as a superclass of
+      `TestEquality`, where the latter cannot provide evidence of
+      non-equality.
+  * Data.Parameterized.NatRepr
+    - Add `DecidableEq` instance for NatRepr.
+    - Add functions:
+      - `decideLeq`
+      - `isZeroOrGT1`
+      - `lessThanIrreflexive`
+      - `lessThanAsymmetric`
+      - `natRecStrong`  -- recursor with strong induction
+      - `natRecBounded` -- bounded recursor
+      - `natFromZero`
+  * Data.Parameterized.Vector
+    - Add construction functions: `singleton`, `cons`, `snoc`, `generate`, and `generateM`
+    - Add functions: `splitWithA` (applicative `splitWith`).
+
+## 1.0.3 -- *2018 Aug 24*
+
+  * Move `lemmaMul` from Vector to NatRepr.
+  * Add stricter role annotations:
+    - `NatRepr` is nominal.
+    - `Vector` is nominal in the first parameter and representational in the second.
+  * Data.Parameterized.NatRepr
+    - Provide a backdoor for directly creating `NatRepr` values.  Use carefully.
+  * Data.Parameterized.Vector
+    - Add Show and Eq instances
+    - Add functions: `joinWithM`, `reverse`
+
+## 1.0.2 -- *2018 Aug 23*
+
+  * Allow function passed to `traverseF_`, `traverseFC_`, and
+    `forMFC_` to return a value instead of null (`()`).
+  * Data.Parameterized.Vector
+    - Newly added module.  A fixed-size vector of typed elements.
+  * Data.Parameterized.Utils.Endian
+    - Newly added module.  Used in Vector.
+
+## 1.0.1 -- *2018 Aug 13*
+
+  Baseline for changelog tracking.
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,12 +1,14 @@
 Name:          parameterized-utils
-Version:       1.0.1
+Version:       2.0
 Author:        Galois Inc.
-Maintainer:    jhendrix@galois.com
+Maintainer:    jhendrix@galois.com, kquick@galois.com
+stability:     stable
 Build-type:    Simple
 Cabal-version: >= 1.9.2
-license: BSD3
-license-file: LICENSE
-category: Data Structures, Dependent Types
+Copyright:     ©2016-2019 Galois, Inc.
+License:       BSD3
+License-file:  LICENSE
+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
@@ -14,6 +16,10 @@
   intended for things like expression libraries where one wishes
   to leverage the Haskell type-checker to improve type-safety by encoding
   the object language type system into data kinds.
+extra-source-files: Changelog.md
+homepage:      https://github.com/GaloisInc/parameterized-utils
+bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues
+tested-with:   GHC==8.2.2, GHC==8.4.4, GHC==8.6.4
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -21,7 +27,7 @@
 -- Unsafe.Coerce and Data.Coerce.  These alternate implementations
 -- impose a significant performance hit.
 flag unsafe-operations
-  Description: Use unsafe operations to improve performance
+  Description: Use unsafe operations (e.g. coercions) to improve performance
   Default: True
 
 source-repository head
@@ -29,30 +35,34 @@
   location: https://github.com/GaloisInc/parameterized-utils
 
 library
-  build-depends:
-    base >= 4.7 && < 4.12,
-    th-abstraction >=0.1 && <0.3,
-    containers,
-    deepseq,
-    ghc-prim,
-    hashable,
-    hashtables,
-    lens,
-    mtl,
-    template-haskell,
-    text,
-    vector
+  build-depends: base >= 4.10 && < 5
+               , th-abstraction >=0.1 && <0.3
+               , constraints == 0.10.*
+               , containers
+               , deepseq
+               , ghc-prim
+               , hashable == 1.2.*
+               , hashtables == 1.2.*
+               , lens == 4.17.*
+               , mtl
+               , template-haskell
+               , text
+               , vector == 0.12.*
 
   hs-source-dirs: src
 
   exposed-modules:
     Data.Parameterized
+    Data.Parameterized.BoolRepr                  
     Data.Parameterized.Classes
+    Data.Parameterized.ClassesC
+    Data.Parameterized.Compose
     Data.Parameterized.Context
     Data.Parameterized.Context.Safe
     Data.Parameterized.Context.Unsafe
     Data.Parameterized.Ctx
     Data.Parameterized.Ctx.Proofs
+    Data.Parameterized.DecidableEq
     Data.Parameterized.HashTable
     Data.Parameterized.List
     Data.Parameterized.Map
@@ -60,14 +70,21 @@
     Data.Parameterized.Nonce
     Data.Parameterized.Nonce.Transformers
     Data.Parameterized.Nonce.Unsafe
+    Data.Parameterized.Pair
+    Data.Parameterized.Peano
     Data.Parameterized.Some
     Data.Parameterized.SymbolRepr
-    Data.Parameterized.Pair
     Data.Parameterized.TH.GADT
     Data.Parameterized.TraversableF
     Data.Parameterized.TraversableFC
     Data.Parameterized.Utils.BinTree
+    Data.Parameterized.Utils.Endian
+    Data.Parameterized.Vector
+    Data.Parameterized.WithRepr                  
 
+  other-modules:
+    Data.Parameterized.NatRepr.Internal
+
   ghc-options: -Wall
 
   if flag(unsafe-operations)
@@ -80,21 +97,21 @@
 
   ghc-options: -Wall
 
-  main-is:UnitTest.hs
+  main-is: UnitTest.hs
   other-modules:
     Test.Context
     Test.NatRepr
+    Test.Vector
 
-  build-depends:
-    base,
-    hashable,
-    hashtables,
-    ghc-prim,
-    lens,
-    mtl,
-    parameterized-utils,
-    tasty,
-    tasty-ant-xml,
-    tasty-hunit,
-    tasty-quickcheck >= 0.8.1,
-    QuickCheck >= 2.7
+  build-depends: base
+               , hashable
+               , hashtables
+               , ghc-prim
+               , lens
+               , mtl
+               , parameterized-utils
+               , 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
diff --git a/src/Data/Parameterized/BoolRepr.hs b/src/Data/Parameterized/BoolRepr.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/BoolRepr.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Parameterized.BoolRepr
+  ( module Data.Type.Bool
+  , BoolRepr(..)
+  , ifRepr, notRepr, (%&&), (%||)
+  , KnownBool
+
+  , someBool
+
+  -- * Re-exports
+  , TestEquality(..)
+  , (:~:)(..)
+  , Data.Parameterized.Some.Some
+  )
+where
+
+import           Data.Parameterized.Classes
+import           Data.Parameterized.DecidableEq
+import           Data.Parameterized.Some
+
+import           Data.Type.Bool
+import           Data.Hashable
+
+-- | 
+data BoolRepr (b :: Bool) where
+  FalseRepr :: BoolRepr 'False
+  TrueRepr  :: BoolRepr 'True
+
+  
+-- | conditional 
+ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
+ifRepr TrueRepr b _ = b
+ifRepr FalseRepr _ c = c
+
+-- | negation
+notRepr :: BoolRepr b -> BoolRepr (Not b)
+notRepr TrueRepr = FalseRepr
+notRepr FalseRepr = TrueRepr
+
+-- | Conjunction 
+(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
+FalseRepr %&& _ = FalseRepr
+TrueRepr  %&& a = a
+infixr 3 %&&
+
+-- | Disjunction 
+(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
+FalseRepr %|| a = a
+TrueRepr  %|| _ = TrueRepr
+infixr 2 %||  
+
+instance Hashable (BoolRepr n) where
+  hashWithSalt i TrueRepr  = hashWithSalt i True
+  hashWithSalt i FalseRepr = hashWithSalt i False
+
+
+instance Eq (BoolRepr m) where
+  _ == _ = True
+
+instance TestEquality BoolRepr where
+  testEquality TrueRepr TrueRepr   = Just Refl
+  testEquality FalseRepr FalseRepr = Just Refl
+  testEquality _ _ = Nothing
+
+instance DecidableEq BoolRepr where
+  decEq TrueRepr  TrueRepr  = Left Refl
+  decEq FalseRepr FalseRepr = Left Refl
+  decEq TrueRepr  FalseRepr = Right $ \case {}
+  decEq FalseRepr TrueRepr  = Right $ \case {}
+
+instance OrdF BoolRepr where
+  compareF TrueRepr  TrueRepr  = EQF
+  compareF FalseRepr FalseRepr = EQF
+  compareF TrueRepr  FalseRepr = GTF
+  compareF FalseRepr TrueRepr  = LTF
+
+instance PolyEq (BoolRepr m) (BoolRepr n) where
+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y
+
+instance Show (BoolRepr m) where
+  show FalseRepr = "FalseRepr"
+  show TrueRepr  = "TrueRepr"
+  
+instance ShowF BoolRepr
+
+instance HashableF BoolRepr where
+  hashWithSaltF = hashWithSalt
+
+
+----------------------------------------------------------
+-- * Implicit runtime booleans
+
+type KnownBool = KnownRepr BoolRepr
+
+instance KnownRepr BoolRepr 'True where
+  knownRepr = TrueRepr
+instance KnownRepr BoolRepr 'False where
+  knownRepr = FalseRepr
+
+someBool :: Bool -> Some BoolRepr
+someBool True  = Some TrueRepr
+someBool False = Some FalseRepr
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
@@ -1,6 +1,7 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2015
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : Classes for working with type of kind @k -> *@
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Joe Hendrix <jhendrix@galois.com>
 
 This module declares classes for working with types with the kind
 @k -> *@ for any kind @k@.  These are generalizations of the
@@ -37,6 +38,7 @@
   , orderingF_refl
   , toOrdering
   , fromOrdering
+  , ordFCompose
     -- * Typeclass generalizations
   , ShowF(..)
   , showsF
@@ -55,11 +57,14 @@
   ) where
 
 import Data.Functor.Const
+import Data.Functor.Compose (Compose(..))
 import Data.Hashable
 import Data.Maybe (isJust)
 import Data.Proxy
 import Data.Type.Equality as Equality
 
+import Data.Parameterized.Compose ()
+
 -- We define these type alias here to avoid importing Control.Lens
 -- modules, as this apparently causes problems with the safe Hasekll
 -- checking.
@@ -134,8 +139,8 @@
 fromOrdering EQ = EQF
 fromOrdering GT = GTF
 
--- | `joinOrderingF x y` first compares on x, returning an equivalent
--- value if it is not `EQF`.  If it is EQF, it returns `y`.
+-- | @joinOrderingF x y@ first compares on @x@, returning an
+-- equivalent value if it is not `EQF`.  If it is `EQF`, it returns @y@.
 joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k)
               .  OrderingF a b
               -> (a ~ b => OrderingF c d)
@@ -193,6 +198,23 @@
             -> (a ~ b => OrderingF c d)
             -> OrderingF c d
 lexCompareF x y = joinOrderingF (compareF x y)
+
+-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
+-- for the \"inner\" functor. The type-level evidence of equality is deduced
+-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
+ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y.
+                (forall w z. f w -> f z -> OrderingF w z)
+            -> Compose f g x
+            -> Compose f g y
+            -> OrderingF x y
+ordFCompose ordF_ (Compose x) (Compose y) =
+  case ordF_ x y of
+    LTF -> LTF
+    GTF -> GTF
+    EQF -> EQF
+
+instance OrdF f => OrdF (Compose f g) where
+  compareF x y = ordFCompose compareF x y
 
 ------------------------------------------------------------------------
 -- ShowF
diff --git a/src/Data/Parameterized/ClassesC.hs b/src/Data/Parameterized/ClassesC.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/ClassesC.hs
@@ -0,0 +1,53 @@
+{-|
+Description : Classes for working with type of kind @(k -> *) -> *@
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Langston Barrett <langston@galois.com>
+
+This module declares classes for working with types with the kind
+@(k -> *) -> *@ for any kind @k@.
+
+These classes generally require type-level evidence for operations
+on their subterms, but don't actually provide it themselves (because
+their types are not themselves parameterized, unlike those in
+"Data.Parameterized.TraverableFC").
+
+Note that there is still some ambiguity around naming conventions, see
+<https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.
+-}
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.ClassesC
+  ( TestEqualityC(..)
+  , OrdC(..)
+  ) where
+
+import Data.Type.Equality ((:~:)(..))
+import Data.Maybe (isJust)
+import Data.Parameterized.Classes (OrderingF, toOrdering)
+import Data.Parameterized.Some (Some(..))
+
+class TestEqualityC (t :: (k -> *) -> *) where
+  testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))
+                -> t f
+                -> t f
+                -> Bool
+
+class TestEqualityC t => OrdC (t :: (k -> *) -> *) where
+  compareC :: (forall x y. f x -> g y -> OrderingF x y)
+           -> t f
+           -> t g
+           -> Ordering
+
+-- | This instance demonstrates where the above class is useful: namely, in
+-- types with existential quantification.
+instance TestEqualityC Some where
+  testEqualityC subterms (Some someone) (Some something) =
+    isJust (subterms someone something)
+
+instance OrdC Some where
+  compareC subterms (Some someone) (Some something) =
+    toOrdering (subterms someone something)
diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Compose.hs
@@ -0,0 +1,46 @@
+{-|
+Description : utilities for working with "Data.Functor.Compose"
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Langston Barrett <langston@galois.com>
+
+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.
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Data.Parameterized.Compose
+  ( testEqualityComposeBare
+  ) where
+
+import Data.Functor.Compose
+import Data.Type.Equality
+
+-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
+--
+-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
+testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y.
+                           (forall w z. f w -> f z -> Maybe (w :~: z))
+                        -> Compose f g x
+                        -> Compose f g y
+                        -> Maybe (x :~: y)
+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =
+  case (testEquality_ x y :: Maybe (g x :~: g y)) of
+    Just Refl -> Just (Refl :: x :~: y)
+    Nothing   -> Nothing
+
+testEqualityCompose :: forall (f :: k -> *) (g :: l -> k) x y. (TestEquality f)
+                    => Compose f g x
+                    -> Compose f g y
+                    -> Maybe (x :~: y)
+testEqualityCompose = testEqualityComposeBare testEquality
+
+instance (TestEquality f) => TestEquality (Compose f g) where
+  testEquality = testEqualityCompose
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,7 +1,7 @@
 ------------------------------------------------------------------------
 -- |
 -- Module           : Data.Parameterized.Context
--- Copyright        : (c) Galois, Inc 2014-16
+-- Copyright        : (c) Galois, Inc 2014-2019
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 --
 -- This module reexports either "Data.Parameterized.Context.Safe"
@@ -46,10 +46,13 @@
   , Data.Parameterized.Context.init
   , Data.Parameterized.Context.last
   , Data.Parameterized.Context.view
+  , Data.Parameterized.Context.take
   , forIndexM
   , generateSome
   , generateSomeM
   , fromList
+  , traverseAndCollect
+
     -- * Context extension and embedding utilities
   , CtxEmbedding(..)
   , ExtendContext(..)
@@ -60,6 +63,7 @@
   , extendEmbeddingRightDiff
   , extendEmbeddingRight
   , extendEmbeddingBoth
+  , appendEmbedding
   , ctxeSize
   , ctxeAssignment
 
@@ -80,10 +84,12 @@
   , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6
   ) where
 
+import           Control.Applicative (liftA2)
 import           Control.Lens hiding (Index, (:>), Empty)
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
 import           GHC.TypeLits (Nat, type (-))
+import           Data.Monoid ((<>))
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
@@ -159,7 +165,7 @@
 #endif
 
 --------------------------------------------------------------------------------
--- | Views
+-- Views
 
 -- | Return true if assignment is empty.
 null :: Assignment f ctx -> Bool
@@ -188,10 +194,15 @@
 view :: forall f ctx . Assignment f ctx -> AssignView f ctx
 view = viewAssign
 
+take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
+take sz sz' asgn =
+  let diff = appendDiff sz' in
+  generate sz (\i -> asgn ! extendIndex' diff i)
+
 --------------------------------------------------------------------------------
--- | Context embedding.
+-- Context embedding.
 
--- This datastructure contains a proof that the first context is
+-- | This datastructure contains a proof that the first context is
 -- embeddable in the second.  This is useful if we want to add extend
 -- an existing term under a larger context.
 
@@ -255,6 +266,11 @@
 extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
 extendEmbeddingRight = extendEmbeddingRightDiff knownDiff
 
+appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
+appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))
+  where
+  diff = appendDiff sz'
+
 extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
 extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))
   where
@@ -305,7 +321,7 @@
 
 
 --------------------------------------------------------------------------------
--- CurryAssignment
+-- * CurryAssignment
 
 -- | This type family is used to define currying\/uncurrying operations
 -- on assignments.  It is best understood by seeing its evaluation on
@@ -346,6 +362,24 @@
   where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
         go prev [] = Some prev
         go prev (Some g:next) = (go $! prev `extend` g) next
+
+
+newtype Collector m w a = Collector { runCollector :: m w }
+instance Functor (Collector m w) where
+  fmap _ (Collector x) = Collector x
+instance (Applicative m, Monoid w) => Applicative (Collector m w) where
+  pure _ = Collector (pure mempty)
+  Collector x <*> Collector y = Collector (liftA2 (<>) x y)
+
+-- | Visit each of the elements in an @Assignment@ in order
+--   from left to right and collect the results using the provided @Monoid@.
+traverseAndCollect ::
+  (Monoid w, Applicative m) =>
+  (forall tp. Index ctx tp -> f tp -> m w) ->
+  Assignment f ctx ->
+  m w
+traverseAndCollect f =
+  runCollector . traverseWithIndex (\i x -> Collector (f i x))
 
 --------------------------------------------------------------------------------
 -- 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
@@ -32,7 +32,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE IncoherentInstances #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -60,9 +59,12 @@
   , Diff
   , noDiff
   , extendRight
+  , appendDiff
   , DiffView(..)
   , viewDiff
   , KnownDiff(..)
+  , IsAppend(..)
+  , diffIsAppend
     -- * Indexing
   , Index
   , indexVal
@@ -186,6 +188,10 @@
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight diff = DiffThere diff
 
+appendDiff :: Size r -> Diff l (l <+> r)
+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)
@@ -199,6 +205,18 @@
 extSize sz DiffHere = sz
 extSize sz (DiffThere diff) = incSize (extSize sz diff)
 
+-- | Proof that @r = l <+> app@ for some @app@
+data IsAppend l r where
+  IsAppend :: Size app -> IsAppend l (l <+> app)
+
+-- | If @l@ is a sub-context of @r@ then extract out their "contextual
+-- difference", i.e., the @app@ such that @r = l <+> app@
+diffIsAppend :: Diff l r -> IsAppend l r
+diffIsAppend DiffHere = IsAppend zeroSize
+diffIsAppend (DiffThere diff) =
+  case diffIsAppend diff of
+    IsAppend sz -> IsAppend (incSize sz)
+
 data DiffView a b where
   NoDiff :: DiffView a a
   ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)
@@ -280,9 +298,10 @@
 extendIndex' DiffHere idx = idx
 extendIndex' (DiffThere diff) idx = IndexThere (extendIndex' diff idx)
 
--- | Given a size @n@, an initial value @v0@, and a function @f@,
--- @forIndex n v0 f@ calls @f@ on each index less than @n@ starting
--- from @0@ and @v0@, with the value @v@ obtained from the last call.
+-- | Given a size @n@, an initial value @v0@, and a function @f@, the
+-- expression @forIndex n v0 f@ calls @f@ on each index less than @n@
+-- starting from @0@ and @v0@, with the value @v@ obtained from the
+-- last call.
 forIndex :: forall ctx r
           . Size ctx
          -> (forall tp . r -> Index ctx tp -> r)
@@ -321,9 +340,10 @@
 forIndexRangeImpl i (SizeSucc sz) d f r =
   forIndexRangeImpl (i-1) sz (LDiffThere d) f r
 
--- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',
--- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and
--- 'f i (forIndexRange (i+1) n v0)' otherwise.
+-- | Given an index @i@, size @n@, a function @f@, value @v@, and a
+-- function @f@, the expression @forIndexRange i n f v@ is equivalent
+-- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@
+-- otherwise.
 forIndexRange :: Int
               -> Size ctx
               -> (forall tp . Index ctx tp -> r -> r)
@@ -409,7 +429,7 @@
 replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx
 replicate n c = generate n (\_ -> c)
 
--- | Create empty indexec vector.
+-- | Create empty indexed vector.
 empty :: Assignment f 'EmptyCtx
 empty = AssignmentEmpty
 
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
@@ -1,6 +1,5 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE GADTs #-}
@@ -32,9 +31,12 @@
   , Diff
   , noDiff
   , extendRight
+  , appendDiff
   , DiffView(..)
   , viewDiff
   , KnownDiff(..)
+  , IsAppend(..)
+  , diffIsAppend
     -- * Indexing
   , Index
   , indexVal
@@ -147,6 +149,8 @@
 newtype Diff (l :: Ctx k) (r :: Ctx k)
       = Diff { _contextExtSize :: Int }
 
+type role Diff nominal nominal
+
 -- | The identity difference.
 noDiff :: Diff l l
 noDiff = Diff 0
@@ -155,6 +159,9 @@
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight (Diff i) = Diff (i+1)
 
+appendDiff :: Size r -> Diff l (l <+> r)
+appendDiff (Size r) = Diff r
+
 instance Cat.Category Diff where
   id = Diff 0
   Diff j . Diff i = Diff (i + j)
@@ -168,6 +175,15 @@
 addSize (Size x) (Size y) = Size (x + y)
 
 
+-- | Proof that @r = l <+> app@ for some @app@
+data IsAppend l r where
+  IsAppend :: Size app -> IsAppend l (l <+> app)
+
+-- | If @l@ is a sub-context of @r@ then extract out their "contextual
+-- difference", i.e., the @app@ such that @r = l <+> app@
+diffIsAppend :: Diff l r -> IsAppend l r
+diffIsAppend (Diff i) = unsafeCoerce $ IsAppend (Size i)
+
 data DiffView a b where
   NoDiff :: DiffView a a
   ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)
@@ -240,8 +256,9 @@
 extendIndex' :: Diff l r -> Index l tp -> Index r tp
 extendIndex' _ = unsafeCoerce
 
--- | Given a size 'n', an initial value 'v0', and a function 'f', 'forIndex n v0 f'
--- is equivalent to 'v0' when 'n' is zero, and 'f (forIndex (n-1) v0) (n-1)' otherwise.
+-- | Given a size @n@, an initial value @v0@, and a function @f@, the
+-- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is
+-- zero, and @f (forIndex (n-1) v0) (n-1)@ otherwise.
 forIndex :: forall ctx r
           . Size ctx
          -> (forall tp . r -> Index ctx tp -> r)
@@ -252,9 +269,10 @@
     ZeroSize -> r
     IncSize p -> f (forIndex p (coerce f) r) (nextIndex p)
 
--- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',
--- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and
--- 'f i (forIndexRange (i+1) n v0)' otherwise.
+-- | Given an index @i@, size @n@, a function @f@, value @v@, and a
+-- function @f@, the expression @forIndex i n f v@ is equivalent to
+-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@
+-- otherwise.
 forIndexRange :: forall ctx r
                . Int
               -> Size ctx
@@ -291,11 +309,11 @@
 indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
 indexOfRange (IndexRange i n) = assert (n == 1) $ Index i
 
--- | `dropTailRange r n` drops the last `n` elements in `r`.
+-- | @dropTailRange r n@ drops the last @n@ elements in @r@.
 dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
 dropTailRange (IndexRange i n) (Size j) = assert (n >= j) $ IndexRange i (n - j)
 
--- | `dropHeadRange r n` drops the first `n` elements in `r`.
+-- | @dropHeadRange r n@ drops the first @n@ elements in @r@.
 dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
 dropHeadRange (IndexRange i n) (Size j) = assert (i' >= i && n >= j) $ IndexRange i' (n - j)
   where i' = i + j
@@ -309,7 +327,7 @@
 type instance Pred ('Succ h) = h
 
 ------------------------------------------------------------------------
--- BalancedTree
+-- * BalancedTree
 
 -- | A balanced tree where all leaves are at the same height.
 --
@@ -459,12 +477,12 @@
   BalPair <$> bal_zipWithM f x1 (unsafeCoerce y1)
           <*> bal_zipWithM f x2 (unsafeCoerce y2)
 #if !MIN_VERSION_base(4,9,0)
-bal_zipWithM _ _ _ = error "ilegal args to bal_zipWithM"
+bal_zipWithM _ _ _ = error "illegal args to bal_zipWithM"
 #endif
 {-# INLINABLE bal_zipWithM #-}
 
 ------------------------------------------------------------------------
--- BinomialTree
+-- * BinomialTree
 
 data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
   Empty :: BinomialTree h f EmptyCtx
@@ -605,7 +623,7 @@
             -> f y
             -> DropResult f (x ::> y)
 
--- | 'bal_drop x y' returns the tree formed 'append x (init y)'
+-- | @bal_drop x y@ returns the tree formed @append x (init y)@
 bal_drop :: forall h f x y
           . BinomialTree h f x
             -- ^ Bina
@@ -686,10 +704,10 @@
 {-# INLINABLE tree_zipWithM #-}
 
 ------------------------------------------------------------------------
--- Assignment
+-- * Assignment
 
--- | An assignment is a sequence that maps each index with type 'tp' to
--- a value of type 'f tp'.
+-- | An assignment is a sequence that maps each index with type @tp@ to
+-- a value of type @f tp@.
 --
 -- This assignment implementation uses a binomial tree implementation
 -- that offers lookups and updates in time and space logarithmic with
@@ -719,7 +737,7 @@
   where r = unsafe_bin_generate (sizeInt n) 0 f
 {-# NOINLINE generate #-}
 
--- | Generate an assignment
+-- | Generate an assignment in an 'Applicative' context
 generateM :: Applicative m
           => Size ctx
           -> (forall tp . Index ctx tp -> m (f tp))
@@ -813,7 +831,7 @@
 unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
 unsafeUpdate i (Assignment a) e = Assignment (runIdentity (unsafe_bin_adjust (\_ -> Identity e) a i 0))
 
--- | View an assignment as either empty or an assignment with one appended.
+-- | Represent an assignment as either empty or an assignment with one appended.
 data AssignView f ctx where
   AssignEmpty :: AssignView f EmptyCtx
   AssignExtend :: Assignment f ctx
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
@@ -1,6 +1,6 @@
 {-|
 Description      : Type-level lists.
-Copyright        : (c) Galois, Inc 2015
+Copyright        : (c) Galois, Inc 2015-2019
 Maintainer       : Joe Hendrix <jhendrix@galois.com>
 
 This module defines type-level lists used for representing the type of
diff --git a/src/Data/Parameterized/Ctx/Proofs.hs b/src/Data/Parameterized/Ctx/Proofs.hs
--- a/src/Data/Parameterized/Ctx/Proofs.hs
+++ b/src/Data/Parameterized/Ctx/Proofs.hs
@@ -1,6 +1,7 @@
 {-|
-Copyright        : (c) Galois, Inc 2015
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : type-level proofs involving contexts
+Copyright   : (c) Galois, Inc 2015-2019
+Maintainer  : Joe Hendrix <jhendrix@galois.com>
 
 This reflects type level proofs involving contexts.
 -}
diff --git a/src/Data/Parameterized/DecidableEq.hs b/src/Data/Parameterized/DecidableEq.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/DecidableEq.hs
@@ -0,0 +1,38 @@
+{-|
+Description : Decideable equality (i.e. evidence of non-equality) on type families
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Langston Barrett <langston@galois.com>
+
+This defines a class @DecidableEq@, which represents decidable equality on a
+type family.
+
+This is different from GHC's @TestEquality@ in that it provides evidence
+of non-equality. In fact, it is a superclass of @TestEquality@.
+-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
+module Data.Parameterized.DecidableEq
+  ( DecidableEq(..)
+  ) where
+
+import Data.Void (Void)
+import Data.Type.Equality ((:~:))
+
+-- | Decidable equality.
+class DecidableEq f where
+  decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)
+
+-- TODO: instances for sums, products of types with decidable equality
+
+-- import Data.Type.Equality ((:~:), TestEquality(..))
+-- instance (DecidableEq f) => TestEquality f where
+--   testEquality a b =
+--     case decEq a b of
+--       Left  prf -> Just prf
+--       Right _   -> Nothing
diff --git a/src/Data/Parameterized/HashTable.hs b/src/Data/Parameterized/HashTable.hs
--- a/src/Data/Parameterized/HashTable.hs
+++ b/src/Data/Parameterized/HashTable.hs
@@ -1,13 +1,14 @@
 ------------------------------------------------------------------------
 -- |
 -- Module           : Data.Parameterized.HashTable
--- Copyright        : (c) Galois, Inc 2014
+-- Description      : a hash table for parameterized keys and values
+-- Copyright        : (c) Galois, Inc 2014-2019
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 --
--- This module provides a ST-based hashtable for parameterized keys and values.
+-- This module provides a 'ST'-based hashtable for parameterized keys and values.
 --
--- NOTE: This API makes use of unsafeCoerce to implement the parameterized
--- hashtable abstraction.  This should be typesafe provided the
+-- NOTE: This API makes use of 'unsafeCoerce' to implement the parameterized
+-- hashtable abstraction.  This should be type-safe provided that the
 -- 'TestEquality' instance on the key type is implemented soundly.
 ------------------------------------------------------------------------
 {-# LANGUAGE KindSignatures #-}
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
@@ -1,10 +1,11 @@
 {-|
-Copyright        : (c) Galois, Inc 2017
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : A type-indexed parameterized list
+Copyright   : (c) Galois, Inc 2017-2019
+Maintainer  : Joe Hendrix <jhendrix@galois.com>
 
 This module defines a list over two parameters.  The first
 is a fixed type-level function @k -> *@ for some kind @k@, and the
-second is a list of types with kind k that provide the indices for
+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
@@ -99,7 +100,7 @@
   knownRepr = knownRepr :< knownRepr
 
 --------------------------------------------------------------------------------
--- Indexed operations
+-- * Indexed operations
 
 
 -- | Represents an index into a type-level list. Used in place of integers to
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
@@ -1,5 +1,6 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2017
+Description : Finite maps with parameterized key and value types
+Copyright   : (c) Galois, Inc 2014-2019
 
 This module defines finite maps where the key and value types are
 parameterized by an arbitrary kind.
@@ -8,17 +9,14 @@
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
@@ -45,13 +43,21 @@
   , fromKeys
   , fromKeysM
    -- * Filter
+  , filter
+  , filterWithKey
   , filterGt
   , filterLt
     -- * Folds
+  , foldlWithKey
+  , foldlWithKey'
   , foldrWithKey
-    -- * Traversal
+  , foldrWithKey'
+  , foldMapWithKey
+    -- * Traversals
   , map
+  , mapWithKey
   , mapMaybe
+  , mapMaybeWithKey
   , traverseWithKey
   , traverseWithKey_
     -- * Complex interface.
@@ -65,18 +71,18 @@
   , Pair(..)
   ) where
 
-import Control.Applicative hiding (empty)
-import Control.Lens (Traversal', Lens')
-import Control.Monad.Identity
-import Data.List (intercalate, foldl')
-import Data.Maybe ()
-import Data.Kind(Type)
+import           Control.Applicative hiding (empty)
+import           Control.Lens (Traversal', Lens')
+import           Control.Monad.Identity
+import           Data.Kind (Type)
+import           Data.List (intercalate, foldl')
+import           Data.Monoid
 
-import Data.Parameterized.Classes
-import Data.Parameterized.Some
-import Data.Parameterized.Pair ( Pair(..) )
-import Data.Parameterized.TraversableF
-import Data.Parameterized.Utils.BinTree
+import           Data.Parameterized.Classes
+import           Data.Parameterized.Some
+import           Data.Parameterized.Pair ( Pair(..) )
+import           Data.Parameterized.TraversableF
+import           Data.Parameterized.Utils.BinTree
   ( MaybeS(..)
   , fromMaybeS
   , Updated(..)
@@ -91,13 +97,13 @@
 import qualified Data.Parameterized.Utils.BinTree as Bin
 
 #if MIN_VERSION_base(4,8,0)
-import Prelude hiding (lookup, map, traverse, null)
+import           Prelude hiding (filter, lookup, map, traverse, null)
 #else
-import Prelude hiding (lookup, map, null)
+import           Prelude hiding (filter, lookup, map, null)
 #endif
 
 ------------------------------------------------------------------------
--- Pair
+-- * Pair
 
 comparePairKeys :: OrdF k => Pair k a -> Pair k a -> Ordering
 comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y)
@@ -106,7 +112,7 @@
 ------------------------------------------------------------------------
 -- MapF
 
--- | A map from parameterized keys to values with the same paramter type.
+-- | A map from parameterized keys to values with the same parameter type.
 data MapF (k :: v -> Type) (a :: v -> Type) where
   Bin :: {-# UNPACK #-}
          !Size -- Number of elements in tree.
@@ -146,7 +152,7 @@
   x == y = size x == size y && toList x == toList y
 
 ------------------------------------------------------------------------
--- Traversals
+-- * Traversals
 
 #ifdef __GLASGOW_HASKELL__
 {-# NOINLINE [1] map #-}
@@ -165,18 +171,30 @@
  #-}
 #endif
 
+
+-- | Apply function to all elements in map.
+mapWithKey
+  :: (forall tp . ktp tp -> f tp -> g tp)
+  -> MapF ktp f
+  -> MapF ktp g
+mapWithKey _ Tip = Tip
+mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r)
+
 -- | Modify elements in a map
 map :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g
-map _ Tip = Tip
-map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r)
+map f = mapWithKey (\_ x -> f x)
 
--- | Run partial map over elements.
+-- | Map keys and elements and collect `Just` results.
+mapMaybeWithKey :: (forall tp . k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k g
+mapMaybeWithKey _ Tip = Tip
+mapMaybeWithKey f (Bin _ k x l r) =
+  case f k x of
+    Just y -> Bin.link (Pair k y) (mapMaybeWithKey f l) (mapMaybeWithKey f r)
+    Nothing -> Bin.merge (mapMaybeWithKey f l) (mapMaybeWithKey f r)
+
+-- | Map elements and collect `Just` results.
 mapMaybe :: (forall tp . f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g
-mapMaybe _ Tip = Tip
-mapMaybe f (Bin _ k x l r) =
-  case f x of
-    Just y -> Bin.link (Pair k y) (mapMaybe f l) (mapMaybe f r)
-    Nothing -> Bin.merge (mapMaybe f l) (mapMaybe f r)
+mapMaybe f = mapMaybeWithKey (\_ x -> f x)
 
 -- | Traverse elements in a map
 traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)
@@ -270,13 +288,43 @@
 elems :: MapF k a -> [Some a]
 elems = foldrF (\e l -> Some e : l) []
 
--- | Perform a fold with the key also provided.
+-- | Perform a left fold with the key also provided.
+foldlWithKey :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b
+foldlWithKey _ z Tip = z
+foldlWithKey f z (Bin _ kx x l r) =
+  let lz = foldlWithKey f z l
+      kz = f lz kx x
+   in foldlWithKey f kz r
+
+-- | Perform a strict left fold with the key also provided.
+foldlWithKey' :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b
+foldlWithKey' _ z Tip = z
+foldlWithKey' f z (Bin _ kx x l r) =
+  let lz = foldlWithKey f z l
+      kz = seq lz $ f lz kx x
+   in seq kz $ foldlWithKey f kz r
+
+-- | Perform a right fold with the key also provided.
 foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b
-foldrWithKey f z = go z
-  where
-    go z' Tip = z'
-    go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l
+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
 
+-- | Perform a strict right fold with the key also provided.
+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 = seq rz $ f kx x rz
+   in seq kz $ foldrWithKey f kz l
+
+-- | Fold the keys and values using the given monoid.
+foldMapWithKey :: Monoid m => (forall s . k s -> a s -> m) -> MapF k a -> m
+foldMapWithKey _ Tip = mempty
+foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r
+
 showMap :: (forall tp . ktp tp -> String)
         -> (forall tp . rtp tp -> String)
         -> MapF ktp rtp
@@ -287,6 +335,17 @@
 ------------------------------------------------------------------------
 -- filter
 
+-- | Return entries with values that satisfy a predicate.
+filter :: (forall tp . f tp -> Bool) -> MapF k f -> MapF k f
+filter f = filterWithKey (\_ v -> f v)
+
+-- | Return key-value pairs that satisfy a predicate.
+filterWithKey :: (forall tp . k tp -> f tp -> Bool) -> MapF k f -> MapF k f
+filterWithKey _ Tip = Tip
+filterWithKey f (Bin _ k x l r)
+  | f k x     = Bin.link (Pair k x) (filterWithKey f l) (filterWithKey f r)
+  | otherwise = Bin.merge (filterWithKey f l) (filterWithKey f r)
+
 compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering
 compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x)
 
@@ -331,9 +390,9 @@
 
 -- | @insertWith f new m@ inserts the binding into @m@.
 --
--- It inserts @f new old@ if @m@ already contains an equivaltn value
--- @old@, and @new@ otherwise.  It returns an Unchanged value if the
--- map stays the same size and an updated value if a new entry was
+-- It inserts @f new old@ if @m@ already contains an equivalent value
+-- @old@, and @new@ otherwise.  It returns an 'Unchanged' value if the
+-- map stays the same size and an 'Updated' value if a new entry was
 -- inserted.
 insertWith :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a
 insertWith = \f k v t -> seq k $ updatedValue (insertWithImpl f k v t)
@@ -356,7 +415,7 @@
 ------------------------------------------------------------------------
 -- updateAtKey
 
--- | Update request tells when to do with value
+-- | 'UpdateRequest' tells what to do with a found value
 data UpdateRequest v
    = -- | Keep the current value.
      Keep
@@ -443,9 +502,9 @@
 fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
           .  (Monad m, Foldable t, OrdF a)
            => (forall tp . a tp -> m (v tp))
-           -- ^ Function for evaluating a register value.
+           -- ^ Function for evaluating an input value to store the result in the map.
            -> t (Some a)
-           -- ^ Set of X86 registers
+           -- ^ Set of input values (traversed via folding)
            -> m (MapF a v)
 fromKeysM f = foldM go empty
   where go :: MapF a v -> Some a -> m (MapF a v)
diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
--- a/src/Data/Parameterized/NatRepr.hs
+++ b/src/Data/Parameterized/NatRepr.hs
@@ -1,21 +1,26 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2015
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : Type level natural number representation at runtime
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Joe Hendrix <jhendrix@galois.com>
 
 This defines a type 'NatRepr' for representing a type-level natural
 at runtime.  This can be used to branch on a type-level value.  For
-each @n@, @NatRepr n@ contains a single value containing the vlaue
+each @n@, @NatRepr n@ contains a single value containing the value
 @n@.  This can be used to help use type-level variables on code
 with data dependendent types.
 
-The 'TestEquality' instance for 'NatRepr' is implemented using
-'unsafeCoerce', as is the `isZeroNat` function. This should be
-typesafe because we maintain the invariant that the integer value
+The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'
+are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This
+should be typesafe because we maintain the invariant that the integer value
 contained in a NatRepr value matches its static type.
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -24,19 +29,25 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 #if MIN_VERSION_base(4,9,0)
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 #endif
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
 module Data.Parameterized.NatRepr
   ( NatRepr
   , natValue
+  , intValue
   , knownNat
   , withKnownNat
   , IsZeroNat(..)
   , isZeroNat
+  , isZeroOrGT1
   , NatComparison(..)
   , compareNat
   , decNat
@@ -49,11 +60,18 @@
   , withDivModNat
   , natMultiply
   , someNat
+  , mkNatRepr
   , maxNat
   , natRec
+  , natRecStrong
+  , natRecBounded
   , natForEach
+  , natFromZero
   , NatCases(..)
   , testNatCases
+    -- * Strict order
+  , lessThanIrreflexive
+  , lessThanAsymmetric
     -- * Bitvector utilities
   , widthVal
   , minUnsigned
@@ -66,6 +84,7 @@
   , signedClamp
     -- * LeqProof
   , LeqProof(..)
+  , decideLeq
   , testLeq
   , testStrictLeq
   , leqRefl
@@ -98,6 +117,7 @@
   , withSubMulDistribRight
   , mulCancelR
   , mul2Plus
+  , lemmaMul
     -- * Re-exports typelists basics
 --  , NatK
   , type (+)
@@ -109,92 +129,35 @@
   , Data.Parameterized.Some.Some
   ) where
 
-import Data.Bits ((.&.))
-import Data.Hashable
-import Data.Proxy as Proxy
+import Data.Bits ((.&.), bit)
+import Data.Data
 import Data.Type.Equality as Equality
-import GHC.TypeLits as TypeLits
+import Data.Void as Void
+import Numeric.Natural
+import GHC.TypeNats as TypeNats
 import Unsafe.Coerce
 
-import Data.Parameterized.Classes
+import Data.Parameterized.NatRepr.Internal
 import Data.Parameterized.Some
 
-maxInt :: Integer
-maxInt = toInteger (maxBound :: Int)
-
-------------------------------------------------------------------------
--- Nat
+maxInt :: Natural
+maxInt = fromIntegral (maxBound :: Int)
 
--- | A runtime presentation of a type-level 'Nat'.
---
--- This can be used for performing dynamic checks on a type-level natural
--- numbers.
-newtype NatRepr (n::Nat) = NatRepr { natValue :: Integer
-                                     -- ^ The underlying integer value of the number.
-                                   }
-  deriving (Hashable)
+intValue :: NatRepr n -> Integer
+intValue n = toInteger (natValue n)
+{-# INLINE intValue #-}
 
 -- | Return the value of the nat representation.
 widthVal :: NatRepr n -> Int
-widthVal (NatRepr i) | i < maxInt = fromInteger i
-                     | otherwise = error "Width is too large."
-
-instance Eq (NatRepr m) where
-  _ == _ = True
-
-instance TestEquality NatRepr where
-  testEquality (NatRepr m) (NatRepr n)
-    | m == n = Just (unsafeCoerce Refl)
-    | otherwise = Nothing
-
--- | Result of comparing two numbers.
-data NatComparison m n where
-  -- First number is less than second.
-  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))
-  NatEQ :: NatComparison x x
-  -- First number is greater than second.
-  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x
-
-compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
-compareNat m n =
-  case compare (natValue m) (natValue n) of
-    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))
-    EQ -> unsafeCoerce  NatEQ
-    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))
-
-instance OrdF NatRepr where
-  compareF x y =
-    case compareNat x y of
-      NatLT _ -> LTF
-      NatEQ -> EQF
-      NatGT _ -> GTF
-
-instance PolyEq (NatRepr m) (NatRepr n) where
-  polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y
-
-instance Show (NatRepr n) where
-  show (NatRepr n) = show n
-
-instance ShowF NatRepr
-
-instance HashableF NatRepr where
-  hashWithSaltF = hashWithSalt
-
--- | This generates a NatRepr from a type-level context.
-knownNat :: forall n . KnownNat n => NatRepr n
-knownNat = NatRepr (natVal (Proxy :: Proxy n))
-
-instance (KnownNat n) => KnownRepr NatRepr n where
-  knownRepr = knownNat
+widthVal (NatRepr i) | i <= maxInt = fromIntegral i
+                     | otherwise   = error ("Width is too large: " ++ show i)
 
-{-# DEPRECATED withKnownNat "This function is potentially unsafe and is schedueled to be removed." #-}
 withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
 withKnownNat (NatRepr nVal) v =
   case someNatVal nVal of
-    Just (SomeNat (Proxy :: Proxy n')) ->
-      case unsafeCoerce (Refl :: 0 :~: 0) :: n :~: n' of
+    SomeNat (Proxy :: Proxy n') ->
+      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of
         Refl -> v
-    Nothing -> error "withKnownNat: inner value in NatRepr is not a natural"
 
 data IsZeroNat n where
   ZeroNat    :: IsZeroNat 0
@@ -204,11 +167,35 @@
 isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat
 isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat
 
+-- | Every nat is either zero or >= 1.
+isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
+isZeroOrGT1 n =
+  case isZeroNat n of
+    ZeroNat    -> Left Refl
+    NonZeroNat -> Right $
+      -- We have n = m + 1 for some m.
+      let
+        -- | x <= x + 1
+        leqSucc:: forall x. LeqProof x (x+1)
+        leqSucc = leqAdd2 (LeqProof :: LeqProof x x) (LeqProof :: LeqProof 0 1)
+        leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y
+        leqPlus fx =
+          case (plusComm fx (knownNat @1) :: x + 1 :~: 1 + x)    of { Refl ->
+          case (plusMinusCancel (knownNat @1) fx :: 1+x-x :~: 1) of { Refl ->
+          case (LeqProof :: LeqProof (x+1) y)                    of { LeqProof ->
+          case (LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ->
+            leqTrans (LeqProof :: LeqProof 1 (y-x))
+                     (leqSub (LeqProof :: LeqProof y y)
+                             (leqTrans (leqSucc :: LeqProof x (x+1))
+                                       (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)
+          }}}}
+      in leqPlus (predNat n)
+
 -- | Decrement a @NatRepr@
 decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1)
 decNat (NatRepr i) = NatRepr (i-1)
 
--- | Get the predicessor of a nat
+-- | Get the predecessor of a nat
 predNat :: NatRepr (n+1) -> NatRepr n
 predNat (NatRepr i) = NatRepr (i-1)
 
@@ -254,15 +241,15 @@
 
 -- | Return maximum unsigned value for bitvector with given width.
 maxUnsigned :: NatRepr w -> Integer
-maxUnsigned w = 2^(natValue w) - 1
+maxUnsigned w = bit (widthVal w) - 1
 
--- | Return minimum value for bitvector in 2s complement with given width.
+-- | Return minimum value for bitvector in two's complement with given width.
 minSigned :: (1 <= w) => NatRepr w -> Integer
-minSigned w = negate (2^(natValue w - 1))
+minSigned w = negate (bit (widthVal w - 1))
 
--- | Return maximum value for bitvector in 2s complement with given width.
+-- | Return maximum value for bitvector in two's complement with given width.
 maxSigned :: (1 <= w) => NatRepr w -> Integer
-maxSigned w = 2^(natValue w - 1) - 1
+maxSigned w = bit (widthVal w - 1) - 1
 
 -- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@.
 toUnsigned :: NatRepr w -> Integer -> Integer
@@ -272,7 +259,7 @@
 -- signed number in two's complement notation and returns that value.
 toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer
 toSigned w i0
-    | i > maxSigned w = i - 2^(natValue w)
+    | i > maxSigned w = i - bit (widthVal w)
     | otherwise       = i
   where i = i0 .&. maxUnsigned w
 
@@ -295,10 +282,16 @@
 ------------------------------------------------------------------------
 -- Some NatRepr
 
-someNat :: Integer -> Maybe (Some NatRepr)
-someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n)))
-          | otherwise = Nothing
+-- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@
+--   if the given value is negative.
+someNat :: Integral a => a -> Maybe (Some NatRepr)
+someNat x | x >= 0 = Just . Some . NatRepr $! fromIntegral x
+someNat _ = Nothing
 
+-- | Turn a @Natural@ into the corresponding @NatRepr@
+mkNatRepr :: Natural -> Some NatRepr
+mkNatRepr n = Some (NatRepr n)
+
 -- | Return the maximum of two nat representations.
 maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
 maxNat x y
@@ -308,11 +301,11 @@
 ------------------------------------------------------------------------
 -- Arithmetic
 
--- | Produce evidence that + is commutative.
+-- | Produce evidence that @+@ is commutative.
 plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m
 plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n)
 
--- | Produce evidence that * is commutative.
+-- | Produce evidence that @*@ is commutative.
 mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
 mulComm _ _ = unsafeCoerce Refl
 
@@ -320,7 +313,7 @@
 mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of
                Refl -> Refl
 
--- | Cancel an add followed b a subtract
+-- | Cancel an add followed by a subtract
 plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m
 plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m)
 
@@ -345,8 +338,6 @@
   case unsafeCoerce (Refl :: 0 :~: 0) of
     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f
 
-
-
 ------------------------------------------------------------------------
 -- LeqProof
 
@@ -355,6 +346,13 @@
 data LeqProof m n where
   LeqProof :: (m <= n) => LeqProof m n
 
+-- | (<=) is a decidable relation on nats.
+decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)
+decideLeq (NatRepr m) (NatRepr n)
+  | m <= n    = Left $ unsafeCoerce (LeqProof :: LeqProof 0 0)
+  | otherwise = Right $
+      \x -> seq x $ error "Impossible [decidable <= on NatRepr]"
+
 testStrictLeq :: forall m n
                . (m <= n)
               => NatRepr m
@@ -384,6 +382,31 @@
     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0))
 {-# NOINLINE testNatCases #-}
 
+-- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.
+lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
+lessThanIrreflexive a prf =
+  let prf1 :: LeqProof (1 + a - a) (a - a)
+      prf1 = leqSub2 prf (LeqProof :: LeqProof a a)
+      prf2 :: 1 + a - a :~: 1
+      prf2 = plusMinusCancel (knownNat @1) a
+      prf3 :: a - a :~: 0
+      prf3 = plusMinusCancel (knownNat @0) a
+      prf4 :: LeqProof 1 0
+      prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }
+  in case prf4 of {}
+
+-- | The strict order on the naturals is irreflexive.
+lessThanAsymmetric :: forall m f n
+                    . LeqProof (n+1) m
+                   -> LeqProof (m+1) n
+                   -> f n
+                   -> Void
+lessThanAsymmetric nLTm mLTn n =
+  case plusComm n (knownNat @1) :: n + 1 :~: 1 + n of { Refl ->
+  case leqAdd (LeqProof :: LeqProof m m) (knownNat @1) :: LeqProof m (m+1) of
+    LeqProof -> lessThanIrreflexive n $ leqTrans (leqTrans nLTm LeqProof) mLTn
+  }
+
 -- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@.
 testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
 testLeq (NatRepr m) (NatRepr n)
@@ -395,7 +418,6 @@
 leqRefl :: forall f n . f n -> LeqProof n n
 leqRefl _ = LeqProof
 
-
 -- | Apply transitivity to LeqProof
 leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
 leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
@@ -509,19 +531,84 @@
            -> [a]
 natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f)
 
+-- | Apply a function to each element in a range starting at zero;
+-- return the list of values obtained.
+natFromZero :: forall h a
+            . NatRepr h
+           -> (forall n. (n <= h) => NatRepr n -> a)
+           -> [a]
+natFromZero = natForEach (knownNat @0)
+
 -- | Recursor for natural numbeers.
-natRec :: forall m f
-       .  NatRepr m
-       -> f 0
+natRec :: forall p f
+       .  NatRepr p
+       -> f 0 {- ^ base case -}
        -> (forall n. NatRepr n -> f n -> f (n + 1))
-       -> f m
-natRec n f0 ih = go n
-  where
-    go :: forall n'. NatRepr n' -> f n'
-    go n' = case isZeroNat n' of
-              ZeroNat    -> f0
-              NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')
+       -> f p
+natRec n base ind =
+  case isZeroNat n of
+    ZeroNat    -> base
+    NonZeroNat -> let n' = predNat n
+                  in ind n' (natRec n' base ind)
 
+-- | Strong induction variant of the recursor.
+natRecStrong :: forall p f
+             .  NatRepr p
+             -> f 0 {- ^ base case -}
+             -> (forall n.
+                  NatRepr n ->
+                  (forall m. (m <= n) => NatRepr m -> f m) ->
+                  f (n + 1)) {- ^ inductive step -}
+             -> f p
+natRecStrong p base ind = natRecStrong' base ind p
+  where -- We can't use use "flip" or some other basic combinator
+        -- because type variables can't be instantiated to contain "forall"s.
+        natRecStrong' :: forall p' f'
+                      .  f' 0 {- ^ base case -}
+                      -> (forall n.
+                            NatRepr n ->
+                            (forall m. (m <= n) => NatRepr m -> f' m) ->
+                            f' (n + 1)) {- ^ inductive step -}
+                      -> NatRepr p'
+                      -> f' p'
+        natRecStrong' base' ind' n =
+          case isZeroNat n of
+            ZeroNat    -> base'
+            NonZeroNat -> ind' (predNat n) (natRecStrong' base' ind')
+
+-- | Bounded recursor for natural numbers.
+--
+-- If you can prove:
+-- - Base case: f 0
+-- - Inductive step: if n <= h and (f n) then (f (n + 1))
+-- You can conclude: for all n <= h, (f (n + 1)).
+natRecBounded :: forall m h f. (m <= h)
+              => NatRepr m
+              -> NatRepr h
+              -> f 0
+              -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))
+              -> f (m + 1)
+natRecBounded m h base indH =
+  case isZeroOrGT1 m of
+    Left Refl      -> indH (knownNat @0) base
+    Right LeqProof ->
+      case decideLeq m h of
+        Left LeqProof {- :: m <= h -} ->
+          let -- Since m is non-zero, it is n + 1 for some n.
+              lemma :: LeqProof (m-1) h
+              lemma = leqSub (LeqProof :: LeqProof m h) (LeqProof :: LeqProof 1 m)
+          in indH m $
+            case lemma of { LeqProof ->
+            case minusPlusCancel m (knownNat @1) of { Refl ->
+              natRecBounded @(m - 1) @h @f (predNat m) h base indH
+            }}
+        Right f {- :: (m <= h) -> Void -} ->
+          absurd $ f (LeqProof :: LeqProof m h)
+
 mulCancelR ::
   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
 mulCancelR _ _ _ = unsafeCoerce Refl
+
+-- | Used in @Vector@
+lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
+lemmaMul = unsafeCoerce Refl
diff --git a/src/Data/Parameterized/NatRepr/Internal.hs b/src/Data/Parameterized/NatRepr/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/NatRepr/Internal.hs
@@ -0,0 +1,99 @@
+{-|
+Copyright        : (c) Galois, Inc 2014-2018
+Maintainer       : Joe Hendrix <jhendrix@galois.com>
+
+This internal module exports the 'NatRepr' type and its constructor. It is intended
+for use only within parameterized-utils, and is excluded from the module export list.
+-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.NatRepr.Internal where
+
+import Data.Data
+import Data.Hashable
+import GHC.TypeNats
+import Numeric.Natural
+import Unsafe.Coerce
+
+import Data.Parameterized.Classes
+import Data.Parameterized.DecidableEq
+
+------------------------------------------------------------------------
+-- Nat
+
+-- | A runtime presentation of a type-level 'Nat'.
+--
+-- This can be used for performing dynamic checks on a type-level natural
+-- numbers.
+newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural
+                                     -- ^ The underlying natural value of the number.
+                                   }
+  deriving (Hashable, Data)
+
+type role NatRepr nominal
+
+instance Eq (NatRepr m) where
+  _ == _ = True
+
+instance TestEquality NatRepr where
+  testEquality (NatRepr m) (NatRepr n)
+    | m == n = Just (unsafeCoerce Refl)
+    | otherwise = Nothing
+
+instance DecidableEq NatRepr where
+  decEq (NatRepr m) (NatRepr n)
+    | m == n    = Left $ unsafeCoerce Refl
+    | otherwise = Right $
+        \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"
+
+compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
+compareNat m n =
+  case compare (natValue m) (natValue n) of
+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))
+    EQ -> unsafeCoerce  NatEQ
+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))
+
+-- | Result of comparing two numbers.
+data NatComparison m n where
+  -- First number is less than second.
+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))
+  NatEQ :: NatComparison x x
+  -- First number is greater than second.
+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x
+
+instance OrdF NatRepr where
+  compareF x y =
+    case compareNat x y of
+      NatLT _ -> LTF
+      NatEQ -> EQF
+      NatGT _ -> GTF
+
+instance PolyEq (NatRepr m) (NatRepr n) where
+  polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y
+
+instance Show (NatRepr n) where
+  show (NatRepr n) = show n
+
+instance ShowF NatRepr
+
+instance HashableF NatRepr where
+  hashWithSaltF = hashWithSalt
+
+-- | This generates a NatRepr from a type-level context.
+knownNat :: forall n . KnownNat n => NatRepr n
+knownNat = NatRepr (natVal (Proxy :: Proxy n))
+
+instance (KnownNat n) => KnownRepr NatRepr n where
+  knownRepr = knownNat
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
@@ -1,12 +1,13 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2016
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : Index generator in the ST monad.
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Joe Hendrix <jhendrix@galois.com>
 
-This module provides a simple generator of new indexes in the ST monad.
+This module provides a simple generator of new indexes in the 'ST' monad.
 It is predictable and not intended for cryptographic purposes.
 
 This module also provides a global nonce generator that will generate
-2^64 nonces before looping.
+2^64 nonces before repeating.
 
 NOTE: The 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply
 compare the generated nonce values and then assert to the compiler
@@ -16,6 +17,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
@@ -29,6 +31,7 @@
   ( -- * NonceGenerator
     NonceGenerator
   , freshNonce
+  , countNoncesGenerated
   , Nonce
   , indexValue
     -- * Accessing a nonce generator
@@ -36,6 +39,7 @@
   , newIONonceGenerator
   , withIONonceGenerator
   , withSTNonceGenerator
+    -- * Global nonce generator
   , withGlobalSTNonceGenerator
   , GlobalNonceGenerator
   , globalNonceGenerator
@@ -53,7 +57,7 @@
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
 
-#if MIN_VERSION_base(4,9,0)
+#if MIN_VERSION_base(4,9,0) && __GLASGOW_HASKELL__ < 805
 import Data.Kind
 #endif
 
@@ -61,55 +65,55 @@
 --
 -- The first type parameter @m@ is the monad used for generating names, and
 -- the second parameter @s@ is used for the counter.
-data NonceGenerator (m :: * -> *) (s :: *) = NonceGenerator {
+data NonceGenerator (m :: * -> *) (s :: *) where
+  STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s
+  IONG :: !(IORef Word64) -> NonceGenerator IO s
+
 #if MIN_VERSION_base(4,9,0)
 -- We have to make the k explicit in GHC 8.0 to avoid a warning.
-    freshNonce :: forall k (tp :: k) . m (Nonce s tp)
+freshNonce :: forall m s k (tp :: k) . NonceGenerator m s -> m (Nonce s tp)
 #else
-    freshNonce :: forall (tp :: k) . m (Nonce s tp)
+freshNonce :: forall m s (tp :: k) . NonceGenerator m s -> m (Nonce s tp)
 #endif
-  }
+freshNonce (IONG r) =
+  atomicModifyIORef' r $ \n -> (n+1, Nonce n)
+freshNonce (STNG r) = do
+  i <- readSTRef r
+  writeSTRef r $! i+1
+  return $ Nonce i
+  -- (Weirdly, there's no atomicModifySTRef'.  Yes, only the IO monad
+  -- does concurrency, but the ST monad is part of the IO monad via
+  -- stToIO, so there's no guarantee that ST code won't be run in
+  -- multiple threads.)
 
--- | Create a new counter.
-withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r
-withGlobalSTNonceGenerator f = runST $ do
-  r <- newSTRef (toEnum 0)
-  f $! NonceGenerator {
-      freshNonce = do
-          i <- readSTRef r
-          writeSTRef r $! succ i
-          return $! Nonce i
-    }
+{-# INLINE freshNonce #-}
+  -- Inlining is particularly necessary since there's no @Monad m@
+  -- constraint on 'freshNonce', so SPECIALIZE doesn't work on it.  In
+  -- this case, though, we get specialization for free from inlining.
+  -- For instance, a @NonceGenerator IO s@ must be an @IONG@, so the
+  -- simplifier eliminates the STNG branch.
 
--- | Create a new nonce generator in the ST monad.
+-- | The number of nonces generated so far by this generator.  Only
+-- really useful for profiling.
+countNoncesGenerated :: NonceGenerator m s -> m Integer
+countNoncesGenerated (IONG r) = toInteger <$> readIORef r
+countNoncesGenerated (STNG r) = toInteger <$> readSTRef r
+
+-- | Create a new nonce generator in the 'ST' monad.
 newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))
-newSTNonceGenerator = g <$> newSTRef (toEnum 0)
-  where g r = Some $!
-          NonceGenerator {
-              freshNonce = do
-                i <- readSTRef r
-                writeSTRef r $! succ i
-                return $! Nonce i
-            }
+newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0)
 
--- | Create a new nonce generator in the ST monad.
+-- | Create a new nonce generator in the 'ST' monad.
 newIONonceGenerator :: IO (Some (NonceGenerator IO))
-newIONonceGenerator = g <$> newIORef (toEnum 0)
-  where g r = Some $!
-          NonceGenerator {
-              freshNonce = do
-                  i <- readIORef r
-                  writeIORef r $! succ i
-                  return $! Nonce i
-            }
+newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0)
 
--- | Run a ST computation with a new nonce generator in the ST monad.
+-- | 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 f = do
   Some r <- newSTNonceGenerator
   f r
 
--- | Create a new nonce generator in the IO monad.
+-- | Create a new nonce generator in the 'IO' monad.
 withIONonceGenerator :: (forall s . NonceGenerator IO s -> IO r) -> IO r
 withIONonceGenerator f = do
   Some r <- newIONonceGenerator
@@ -142,7 +146,7 @@
 instance ShowF (Nonce s)
 
 ------------------------------------------------------------------------
--- GlobalNonceGenerator
+-- * GlobalNonceGenerator
 
 data GlobalNonceGenerator
 
@@ -152,7 +156,10 @@
 
 -- | A nonce generator that uses a globally-defined counter.
 globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator
-globalNonceGenerator =
-  NonceGenerator
-  { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n))
-  }
+globalNonceGenerator = IONG globalNonceIORef
+
+-- | Create a new counter.
+withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r
+withGlobalSTNonceGenerator f = runST $ do
+  r <- newSTRef (toEnum 0)
+  f $! STNG r
diff --git a/src/Data/Parameterized/Nonce/Transformers.hs b/src/Data/Parameterized/Nonce/Transformers.hs
--- a/src/Data/Parameterized/Nonce/Transformers.hs
+++ b/src/Data/Parameterized/Nonce/Transformers.hs
@@ -1,6 +1,7 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2016
-Maintainer       : Eddy Westbrook <westbrook@galois.com>
+Description : A typeclass and monad transformers for generating nonces.
+Copyright   : (c) Galois, Inc 2014-2019
+Maintainer  : Eddy Westbrook <westbrook@galois.com>
 
 This module provides a typeclass and monad transformers for generating
 nonces.
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,6 @@
 {-|
-Copyright        : (c) Galois, Inc 2017
+nDescription : 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
 same existentially quantified parameter.
diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Peano.hs
@@ -0,0 +1,501 @@
+{-|
+Description: Representations of a type-level natural at runtime.
+Copyright        : (c) Galois, Inc 2019
+
+This defines a type 'Peano' and 'PeanoRepr' for representing a
+type-level natural at runtime. These type-level numbers are defined
+inductively instead of using GHC.TypeLits.
+
+As a result, type-level computation defined recursively over these
+numbers works more smoothly. (For example, see the type-level
+function 'Repeat' below.)
+
+Note: as in "NatRepr", in UNSAFE mode, the runtime representation of
+these type-level natural numbers is 'Word64'.
+
+-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MIN_VERSION_base(4,9,0)
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
+module Data.Parameterized.Peano
+   ( -- * Peano
+     Peano
+     , Z , S
+
+     -- * Basic arithmetic 
+     , Plus, Minus, Mul,  Max, Min
+     , plusP, minusP, mulP, maxP, minP
+     , zeroP, succP, predP
+
+     -- * Counting
+     , Repeat, CtxSizeP
+     , repeatP, ctxSizeP
+     
+     -- * Comparisons
+     , Le, Lt, Gt, Ge
+     , leP, ltP, gtP, geP
+
+     -- * Runtime representation
+     , KnownPeano
+     , PeanoRepr
+     , PeanoView(..), peanoView, viewRepr
+
+     -- * 'Some Peano'
+     , mkPeanoRepr, peanoValue     
+     , somePeano
+     , maxPeano
+     , minPeano
+     , peanoLength
+
+     -- * Properties
+     , plusCtxSizeAxiom
+     , minusPlusAxiom
+     , ltMinusPlusAxiom
+
+     -- * Re-exports
+     , TestEquality(..)
+     , (:~:)(..)
+     , Data.Parameterized.Some.Some
+
+     ) where
+
+import           Data.Parameterized.BoolRepr
+import           Data.Parameterized.Classes
+import           Data.Parameterized.DecidableEq
+import           Data.Parameterized.Some
+import           Data.Parameterized.Context
+
+import           Data.Hashable
+import           Data.Word
+
+#ifdef UNSAFE_OPS
+import           Unsafe.Coerce(unsafeCoerce)
+#endif
+
+------------------------------------------------------------------------
+-- * Peano arithmetic
+
+-- | Unary representation for natural numbers
+data Peano = Z | S Peano
+-- | Peano zero
+type Z = 'Z
+-- | Peano successor
+type S = 'S
+
+-- Peano numbers are more about *counting* than arithmetic.
+-- They are most useful as iteration arguments and list indices
+-- However, for completeness, we define a few standard
+-- operations.
+
+
+-- | Addition
+type family Plus (a :: Peano) (b :: Peano) :: Peano where
+  Plus Z     b = b
+  Plus (S a) b = S (Plus a b)
+
+-- | Subtraction
+type family Minus (a :: Peano) (b :: Peano) :: Peano where
+  Minus Z     b     = Z
+  Minus (S a) (S b) = Minus a b
+  Minus a    Z      = a
+
+-- | Multiplication
+type family Mul (a :: Peano) (b :: Peano) :: Peano where
+  Mul Z     b = Z
+  Mul (S a) b = Plus a (Mul a b)
+
+-- | Less-than-or-equal
+type family Le  (a :: Peano) (b :: Peano) :: Bool where
+  Le  Z  b        = 'True
+  Le  a  Z        = 'False
+  Le  (S a) (S b) = Le a b
+
+-- | Less-than
+type family Lt  (a :: Peano) (b :: Peano) :: Bool where
+  Lt a b = Le (S a) b
+
+-- | Greater-than
+type family Gt  (a :: Peano) (b :: Peano) :: Bool where
+  Gt a b = Le b a
+
+-- | Greater-than-or-equal
+type family Ge  (a :: Peano) (b :: Peano) :: Bool where
+  Ge a b = Lt b a
+
+-- | Maximum
+type family Max (a :: Peano) (b :: Peano) :: Peano where
+  Max Z b = b
+  Max a Z = a
+  Max (S a) (S b) = S (Max a b)
+
+-- | Minimum
+type family Min (a :: Peano) (b :: Peano) :: Peano where
+  Min Z b = Z
+  Min a Z = Z
+  Min (S a) (S b) = S (Min a b)
+
+-- | Apply a constructor 'f' n-times to an argument 's'
+type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where
+  Repeat Z f s     = s
+  Repeat (S m) f s = f (Repeat m f s)
+
+-- | Calculate the size of a context
+type family CtxSizeP (ctx :: Ctx k) :: Peano where
+  CtxSizeP 'EmptyCtx   = Z
+  CtxSizeP (xs '::> x) = S (CtxSizeP xs)
+
+------------------------------------------------------------------------
+-- * Run time representation of Peano numbers
+
+#ifdef UNSAFE_OPS
+-- | The run time value, stored as an Word64
+-- As these are unary numbers, we don't worry about overflow.
+newtype PeanoRepr (n :: Peano) =
+  PeanoRepr { peanoValue :: Word64 }
+-- n is Phantom in the definition, but we don't want to allow coerce
+type role PeanoRepr nominal
+#else
+-- | Runtime value
+type PeanoRepr = PeanoView
+-- | Conversion
+peanoValue :: PeanoRepr n -> Word64
+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.
+data PeanoView (n :: Peano) where
+  ZRepr :: PeanoView Z
+  SRepr :: PeanoRepr n -> PeanoView (S n)
+
+-- | Test whether a number is Zero or Successor
+peanoView :: PeanoRepr n -> PeanoView n
+#ifdef UNSAFE_OPS
+peanoView (PeanoRepr i) =
+  if i == 0
+  then unsafeCoerce ZRepr
+  else unsafeCoerce (SRepr (PeanoRepr (i-1)))
+#else
+peanoView = id
+#endif
+
+-- | convert the view back to the runtime representation
+viewRepr :: PeanoView n -> PeanoRepr n
+#ifdef UNSAFE_OPS
+viewRepr ZRepr     = PeanoRepr 0
+viewRepr (SRepr n) = PeanoRepr (peanoValue n + 1)
+#else
+viewRepr = id
+#endif
+
+----------------------------------------------------------
+-- * Class instances
+
+instance Hashable (PeanoRepr n) where
+  hashWithSalt i x = hashWithSalt i (peanoValue x)
+
+instance Eq (PeanoRepr m) where
+  _ == _ = True
+
+instance TestEquality PeanoRepr where
+#ifdef UNSAFE_OPS
+  testEquality (PeanoRepr m) (PeanoRepr n)
+    | m == n = Just (unsafeCoerce Refl)
+    | otherwise = Nothing
+#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
+#ifdef UNSAFE_OPS
+  decEq (PeanoRepr m) (PeanoRepr n)
+    | m == n    = Left $ unsafeCoerce Refl
+    | otherwise = Right $
+        \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]"
+#else
+  decEq ZRepr ZRepr = Left Refl
+  decEq (SRepr m1) (SRepr m2) =
+    case decEq m1 m2 of
+      Left Refl -> Left Refl
+      Right f   -> Right $ \case Refl -> f Refl
+  decEq ZRepr (SRepr _) =
+      Right $ \case {}
+  decEq (SRepr _) ZRepr =
+      Right $ \case {}
+#endif
+
+instance OrdF PeanoRepr where
+#ifdef UNSAFE_OPS
+  compareF (PeanoRepr m) (PeanoRepr n)
+    | m < n     = unsafeCoerce LTF
+    | m == n    = unsafeCoerce EQF
+    | otherwise = unsafeCoerce GTF
+#else
+  compareF ZRepr      ZRepr      = EQF
+  compareF ZRepr      (SRepr _)  = LTF
+  compareF (SRepr _)  ZRepr      = GTF
+  compareF (SRepr m1) (SRepr m2) =
+    case compareF m1 m2 of
+       EQF -> EQF
+       LTF -> LTF
+       GTF -> GTF
+#endif
+
+instance PolyEq (PeanoRepr m) (PeanoRepr n) where
+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y
+
+-- Display as digits, not in unary
+instance Show (PeanoRepr p) where
+  show p = show (peanoValue p)
+
+instance ShowF PeanoRepr
+
+instance HashableF PeanoRepr where
+  hashWithSaltF = hashWithSalt
+
+----------------------------------------------------------
+-- * Implicit runtime Peano numbers
+
+-- | Implicit runtime representation
+type KnownPeano = KnownRepr PeanoRepr
+
+instance KnownRepr PeanoRepr Z where
+  knownRepr = viewRepr ZRepr
+instance (KnownRepr PeanoRepr n) => KnownRepr PeanoRepr (S n) where
+  knownRepr = viewRepr (SRepr knownRepr)
+
+----------------------------------------------------------
+-- * Operations on runtime numbers
+
+
+-- | Zero
+zeroP :: PeanoRepr Z
+#ifdef UNSAFE_OPS
+zeroP = PeanoRepr 0
+#else
+zeroP = ZRepr
+#endif
+
+-- | Successor, Increment
+succP :: PeanoRepr n -> PeanoRepr (S n)
+#ifdef UNSAFE_OPS
+succP (PeanoRepr i) = PeanoRepr (i+1)
+#else
+succP = SRepr
+#endif
+
+-- | Get the predecessor (decrement)
+predP :: PeanoRepr (S n) -> PeanoRepr n
+#ifdef UNSAFE_OPS
+predP (PeanoRepr i) = PeanoRepr (i-1)
+#else
+predP (SRepr i) = i
+#endif
+
+-- | Addition
+plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
+#ifdef UNSAFE_OPS
+plusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a + b)
+#else
+plusP (SRepr a) b = SRepr (plusP a b)
+#endif
+
+-- | Subtraction
+minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
+#ifdef UNSAFE_OPS
+minusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a - b)
+#else
+minusP ZRepr     _b        = ZRepr
+minusP (SRepr a) (SRepr b) = minusP a b
+minusP a ZRepr             = a
+#endif
+
+-- | Multiplication
+mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
+#ifdef UNSAFE_OPS
+mulP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a * b)
+#else
+mulP ZRepr     _b = ZRepr
+mulP (SRepr a) b  = plusP a (mulP a b)
+#endif
+
+-- | Maximum
+maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
+#ifdef UNSAFE_OPS
+maxP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (max a b)
+#else
+maxP ZRepr     b         = b
+maxP a         ZRepr     = a
+maxP (SRepr a) (SRepr b) = SRepr (maxP a b)
+#endif
+
+-- | Minimum
+minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
+#ifdef UNSAFE_OPS
+minP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (min a b)
+#else
+minP ZRepr     _b        = ZRepr
+minP _a        ZRepr     = ZRepr
+minP (SRepr a) (SRepr b) = SRepr (minP a b)
+#endif
+
+-- | Less-than-or-equal-to
+leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
+#ifdef UNSAFE_OPS
+leP  (PeanoRepr a) (PeanoRepr b) =
+  if a <= b then unsafeCoerce (TrueRepr)
+            else unsafeCoerce(FalseRepr)
+#else
+leP ZRepr      ZRepr    = TrueRepr
+leP ZRepr     (SRepr _) = TrueRepr
+leP (SRepr _) ZRepr     = FalseRepr
+leP (SRepr a) (SRepr b) = leP a b
+#endif
+
+-- | Less-than
+ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
+ltP a b = leP (succP a) b
+
+-- | Greater-than-or-equal-to
+geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
+geP a b = ltP b a
+
+-- | Greater-than
+gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
+gtP a b = leP b a
+
+
+-- | Apply a constructor 'f' n-times to an argument 's'
+repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
+repeatP n f s = case peanoView n of
+  ZRepr   -> s
+  SRepr m -> f (repeatP m f s)
+
+-- | Calculate the size of a context
+ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
+ctxSizeP r = case viewAssign r of
+  AssignEmpty -> zeroP
+  AssignExtend a _ -> succP (ctxSizeP a)
+
+------------------------------------------------------------------------
+-- * Some PeanoRepr
+
+-- | Convert a 'Word64' to a 'PeanoRepr'
+mkPeanoRepr :: Word64 -> Some PeanoRepr
+#ifdef UNSAFE_OPS
+mkPeanoRepr n = Some (PeanoRepr n)
+#else
+mkPeanoRepr 0 = Some ZRepr
+mkPeanoRepr n = case mkPeanoRepr (n - 1) of
+                 Some mr -> Some (SRepr mr)
+#endif                 
+
+-- | Turn an @Integral@ value into a 'PeanoRepr'.  Returns @Nothing@
+--   if the given value is negative.
+somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
+somePeano x | x >= 0 = Just . mkPeanoRepr $! fromIntegral x
+somePeano _ = Nothing
+
+-- | Return the maximum of two representations.
+maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
+maxPeano x y = Some (maxP x y)
+
+-- | Return the minimum of two representations.
+minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
+minPeano x y = Some (minP x y)
+
+-- | List length as a Peano number
+peanoLength :: [a] -> Some PeanoRepr
+peanoLength [] = Some zeroP
+peanoLength (_:xs) = case peanoLength xs of
+  Some n -> Some (succP n)
+
+
+------------------------------------------------------------------------
+-- * Properties about Peano numbers
+--
+-- The safe version of these properties includes a runtime proof of
+-- the equality. The unsafe version has no run-time
+-- computation. Therefore, in the unsafe version, the "Repr" arguments
+-- can be used as proxies (i.e. called using 'undefined') but must be
+-- supplied to the safe versions.
+
+
+-- | Context size commutes with context append
+plusCtxSizeAxiom :: forall t1 t2 f.
+  Assignment f t1 -> Assignment f t2 ->
+  CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
+#ifdef UNSAFE_OPS
+plusCtxSizeAxiom _t1 _t2 = unsafeCoerce Refl
+#else
+plusCtxSizeAxiom t1 t2 =
+  case viewAssign t2 of
+    AssignEmpty -> Refl
+    AssignExtend t2' _
+      | Refl <- plusCtxSizeAxiom t1 t2' -> Refl
+#endif
+
+-- | Minus distributes over plus
+--
+minusPlusAxiom :: forall n t 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
+#else
+minusPlusAxiom n t t' = case peanoView t' of
+  ZRepr -> Refl
+  SRepr t1' -> case peanoView n of
+      ZRepr -> Refl
+      SRepr n1 -> case minusPlusAxiom n1 t t1' of
+        Refl -> Refl
+#endif
+
+-- | We can reshuffle minus with less than
+--
+ltMinusPlusAxiom :: forall n t t'.
+  (Lt t (Minus n t') ~ 'True) =>
+  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->
+  Lt (Plus t' t) n :~: 'True
+#ifdef UNSAFE_OPS
+ltMinusPlusAxiom _n _t _t' = unsafeCoerce Refl
+#else
+ltMinusPlusAxiom n t t' = case peanoView n of
+  SRepr m -> case peanoView t' of
+     ZRepr -> Refl
+     SRepr t1' -> case ltMinusPlusAxiom m t t1' of
+        Refl -> Refl
+#endif
+
+------------------------------------------------------------------------
+--  LocalWords:  PeanoRepr runtime Peano unary
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
@@ -1,8 +1,9 @@
 ------------------------------------------------------------------------
 -- |
 -- Module           : Data.Parameterized.Some
--- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2019
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
+-- Description : a GADT that hides a type parameter
 --
 -- This module provides 'Some', a GADT that hides a type parameter.
 ------------------------------------------------------------------------
diff --git a/src/Data/Parameterized/SymbolRepr.hs b/src/Data/Parameterized/SymbolRepr.hs
--- a/src/Data/Parameterized/SymbolRepr.hs
+++ b/src/Data/Parameterized/SymbolRepr.hs
@@ -1,6 +1,7 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2015
+Copyright        : (c) Galois, Inc 2014-2019
 Maintainer       : Joe Hendrix <jhendrix@galois.com>
+Description : a type family for representing a type-level string (AKA symbol) at runtime
 
 This defines a type family 'SymbolRepr' for representing a type-level string
 (AKA symbol) at runtime.  This can be used to branch on a type-level value.
@@ -16,13 +17,11 @@
 {-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE Trustworthy #-}
 module Data.Parameterized.SymbolRepr
   ( -- * SymbolRepr
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
@@ -1,8 +1,9 @@
 ------------------------------------------------------------------------
 -- |
 -- Module           : Data.Parameterized.TH.GADT
--- Copyright        : (c) Galois, Inc 2013-2014
+-- Copyright        : (c) Galois, Inc 2013-2019
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
+-- Description : Template Haskell primitives for working with large GADTs
 --
 -- This module declares template Haskell primitives so that it is easier
 -- to work with GADTs that have many constructors.
@@ -79,7 +80,7 @@
 data TypePat
    = TypeApp TypePat TypePat -- ^ The application of a type.
    | AnyType       -- ^ Match any type.
-   | DataArg Int   -- ^ Match the ith argument of the data type we are traversing.
+   | DataArg Int   -- ^ Match the i'th argument of the data type we are traversing.
    | ConType TypeQ -- ^ Match a ground type.
 
 matchTypePat :: [Type] -> TypePat -> Type -> Q Bool
@@ -198,7 +199,9 @@
   in mkSimpleEqF dVars bnd pats con
 
 -- | @structuralTypeEquality f@ returns a function with the type:
---   forall x y . f x -> f y -> Maybe (x :~: y)
+--   @
+--     forall x y . f x -> f y -> Maybe (x :~: y)
+--   @
 structuralTypeEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ
 structuralTypeEquality tpq pats = do
   d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq
@@ -214,7 +217,9 @@
     else [| \x y -> $(caseE [| x |] (trueEqs [| y |])) |]
 
 -- | @structuralTypeOrd f@ returns a function with the type:
---   forall x y . f x -> f y -> OrderingF x y
+--   @
+--     forall x y . f x -> f y -> OrderingF x y
+--   @
 --
 -- This implementation avoids matching on both the first and second
 -- parameters in a simple case expression in order to avoid stressing
@@ -256,12 +261,12 @@
       | (i,con) <- zip [0..] (datatypeCons d) ]
 
 -- | Generate a list of fresh names using the base name
--- numbered 1 to n to make them useful in conjunction with
--- @-dsuppress-unqiues@.
+-- and numbered 1 to @n@ to make them useful in conjunction with
+-- @-dsuppress-uniques@.
 newNames ::
   String   {- ^ base name                     -} ->
   Int      {- ^ quantity                      -} ->
-  Q [Name] {- ^ list of names: base1, base2.. -}
+  Q [Name] {- ^ list of names: @base1@, @base2@, ... -}
 newNames base n = traverse (\i -> newName (base ++ show i)) [1..n]
 
 
@@ -273,7 +278,7 @@
       EQF -> $(r)
    |]
 
--- | Compare two variables and use following comparison if they are different.
+-- | Compare two variables, returning the third argument if they are equal.
 --
 -- This returns an 'OrdF' instance.
 joinCompareToOrdF :: Name -> Name -> ExpQ -> ExpQ
@@ -284,7 +289,7 @@
       EQ -> $(r)
    |]
 
-  -- Match expression with given type to variables
+-- | Match expression with given type to variables
 matchOrdArguments :: [Type]
                      -- ^ Types bound by data arguments
                   -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments
@@ -343,7 +348,7 @@
        -> Q [MatchQ]
 mkOrdF d pats = mkSimpleOrdF (datatypeVars d) pats
 
--- | Find the first recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@.
+-- | @recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@.
 recurseArg :: (Type -> Q (Maybe ExpQ))
            -> ExpQ -- ^ Function to apply
            -> ExpQ
@@ -361,7 +366,7 @@
 
 -- | @traverseAppMatch f c@ 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
+traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- ^ Pattern match function
                  -> ExpQ -- ^ Function to apply to each argument recursively.
                  -> ConstructorInfo -- ^ Constructor to match.
                  -> MatchQ -- ^ Match expression that
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
@@ -1,14 +1,17 @@
 ------------------------------------------------------------------------
 -- |
 -- Module           : Data.Parameterized.TraversableF
--- Copyright        : (c) Galois, Inc 2014-2015
+-- Copyright        : (c) Galois, Inc 2014-2019
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
+-- Description      : Traversing structures having a single parametric type
 --
 -- This module declares classes for working with structures that accept
 -- a single parametric type parameter.
 ------------------------------------------------------------------------
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Trustworthy #-}
 module Data.Parameterized.TraversableF
   ( FunctorF(..)
@@ -24,9 +27,12 @@
 import Control.Applicative
 import Control.Monad.Identity
 import Data.Coerce
+import Data.Functor.Compose (Compose(..))
 import Data.Monoid
 import GHC.Exts (build)
 
+import Data.Parameterized.TraversableFC
+
 -- | A parameterized type that is a functor on all instances.
 class FunctorF m where
   fmapF :: (forall x . f x -> g x) -> m f -> m g
@@ -42,7 +48,7 @@
 (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
 (#.) _f = coerce
 
--- | This is a generalization of the @Foldable@ class to
+-- | This is a generalization of the 'Foldable' class to
 -- structures over parameterized terms.
 class FoldableF (t :: (k -> *) -> *) where
   {-# MINIMAL foldMapF | foldrF #-}
@@ -76,11 +82,11 @@
   toListF :: (forall tp . f tp -> a) -> t f -> [a]
   toListF f t = build (\c n -> foldrF (\e v -> c (f e) v) n t)
 
--- | Return 'True' if all values satisfy predicate.
+-- | 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)
 
--- | Return 'True' if any values satisfy predicate.
+-- | Return 'True' if any values satisfy the predicate.
 anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool
 anyF p = getAny #. foldMapF (Any #. p)
 
@@ -112,5 +118,30 @@
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f ()) -> t e -> f ()
+traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f ()
 traverseF_ f = foldrF (\e r -> f e *> r) (pure ())
+
+------------------------------------------------------------------------
+-- TraversableF (Compose s t)
+
+instance ( FunctorF (s :: (k -> *) -> *)
+         , FunctorFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         FunctorF (Compose s t) where
+  fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v
+
+instance ( TraversableF (s :: (k -> *) -> *)
+         , TraversableFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         FoldableF (Compose s t) where
+  foldMapF = foldMapFDefault
+
+-- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.
+instance ( TraversableF (s :: (k -> *) -> *)
+         , TraversableFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         TraversableF (Compose s t) where
+  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>
+               (forall (u :: l). f u -> m (g u))
+            -> Compose s t f -> m (Compose s t g)
+  traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v
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
@@ -3,6 +3,7 @@
 -- Module           : Data.Parameterized.TraversableFC
 -- Copyright        : (c) Galois, Inc 2014-2015
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
+-- Description      : Traversing structures having a single parametric type followed by a fixed kind.
 --
 -- This module declares classes for working with structures that accept
 -- a parametric type parameter followed by some fixed kind.
@@ -77,12 +78,12 @@
 ------------------------------------------------------------------------
 -- FoldableF
 
--- | This is a coercision used to avoid overhead associated
+-- | This is a coercion used to avoid overhead associated
 -- with function composition.
 (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
 (#.) _f = coerce
 
--- | This is a generalization of the @Foldable@ class to
+-- | This is a generalization of the 'Foldable' class to
 -- structures over parameterized terms.
 class FoldableFC (t :: (k -> *) -> l -> *) where
   {-# MINIMAL foldMapFC | foldrFC #-}
@@ -150,12 +151,12 @@
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())
+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m a) -> (forall x. t f x -> m ())
 traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ())
 {-# INLINE traverseFC_ #-}
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()
+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
 forMFC_ v f = traverseFC_ f v
 {-# INLINE forMFC_ #-}
diff --git a/src/Data/Parameterized/Utils/BinTree.hs b/src/Data/Parameterized/Utils/BinTree.hs
--- a/src/Data/Parameterized/Utils/BinTree.hs
+++ b/src/Data/Parameterized/Utils/BinTree.hs
@@ -1,6 +1,6 @@
 {-|
 Description      : Utilities for balanced binary trees.
-Copyright        : (c) Galois, Inc 2014
+Copyright        : (c) Galois, Inc 2014-2019
 Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -}
 {-# LANGUAGE ConstraintKinds #-}
@@ -64,7 +64,7 @@
 ------------------------------------------------------------------------
 -- Updated
 
--- | Updated a contains a value that has been flagged on whether it was
+-- | @Updated a@ contains a value that has been flagged on whether it was
 -- modified by an operation.
 data Updated a
    = Updated   !a
@@ -92,7 +92,7 @@
 delta = 3
 ratio = 2
 
--- `balanceL p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.
+-- | @balanceL p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
 --
 -- It assumes that @l@ and @r@ are close to being balanced, and that only
 -- @l@ may contain too many elements.
@@ -108,7 +108,7 @@
     _ -> bin p l r
 {-# INLINE balanceL #-}
 
--- `balanceR p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.
+-- | @balanceR p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
 --
 -- It assumes that @l@ and @r@ are close to being balanced, and that only
 -- @r@ may contain too many elements.
@@ -137,7 +137,7 @@
     TipTree -> bin p tip tip
     BinTree q l r -> balanceL q (insertMin p l) r
 
--- | link is called to insert a key and value between two disjoint subtrees.
+-- | @link@ is called to insert a key and value between two disjoint subtrees.
 link :: IsBinTree c e => e -> c -> c -> c
 link p l r =
   case (asBin l, asBin r) of
@@ -210,7 +210,7 @@
         EQ -> Unchanged (bin x l r)
 {-# INLINABLE insert #-}
 
--- | 'glue l r' concatenates @l@ and @r@.
+-- | @glue l r@ concatenates @l@ and @r@.
 --
 -- It assumes that @l@ and @r@ are already balanced with respect to each other.
 glue :: IsBinTree c e => c -> c -> c
@@ -247,7 +247,7 @@
 -- filter
 
 -- | Returns only entries that are less than predicate with respect to the ordering
--- and Nothing if no elements are discared.
+-- and Nothing if no elements are discarded.
 filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
 filterGt k t =
   case asBin t of
@@ -260,7 +260,7 @@
 {-# INLINABLE filterGt #-}
 
 
--- | @filterLt' k m@ returns submap of @m@ that only contains entries
+-- | @filterLt k m@ returns submap of @m@ that only contains entries
 -- that are smaller than @k@.  If no entries are deleted then return Nothing.
 filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
 filterLt k t =
@@ -276,8 +276,8 @@
 ------------------------------------------------------------------------
 -- Union
 
--- Insert a new key and value in the map if it is not already present.
--- Used by `union`.
+-- | Insert a new key and value in the map if it is not already present.
+-- Used by 'union'.
 insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c
 insertR comp e m = fromMaybeS m (go e m)
   where
diff --git a/src/Data/Parameterized/Utils/Endian.hs b/src/Data/Parameterized/Utils/Endian.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Utils/Endian.hs
@@ -0,0 +1,16 @@
+{-|
+Description: A common location for defining multi-byte value ordering.
+Copyright        : (c) Galois, Inc 2019
+-}
+
+module Data.Parameterized.Utils.Endian where
+
+-- | Determines the composition of smaller numeric values into larger values.
+--
+--  BigEndian = most significant values in the lowest index location / first
+--  LittleEndian = least significant values in the lowest index location / first
+--
+--  Value: 0x01020304
+--  BigEndian    = [ 0x01, 0x02, 0x03, 0x04 ]
+--  LittleEndian = [ 0x04, 0x03, 0x02, 0x01 ]
+data Endian = LittleEndian | BigEndian deriving (Eq,Show,Ord)
diff --git a/src/Data/Parameterized/Vector.hs b/src/Data/Parameterized/Vector.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Vector.hs
@@ -0,0 +1,560 @@
+{-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}
+{-# Language PatternGuards #-}
+{-# Language TypeApplications, ScopedTypeVariables #-}
+{-# Language Rank2Types, RoleAnnotations #-}
+{-# Language CPP #-}
+#if __GLASGOW_HASKELL__ >= 805
+{-# Language NoStarIsType #-}
+#endif
+{-|
+Copyright        : (c) Galois, Inc 2014-2019
+
+A fixed-size vector of typed elements.
+
+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.
+-}
+module Data.Parameterized.Vector
+  ( Vector
+    -- * Lists
+  , fromList
+  , toList
+
+    -- * Length
+  , length
+  , nonEmpty
+  , lengthInt
+
+    -- * Indexing
+  , elemAt
+  , elemAtMaybe
+  , elemAtUnsafe
+
+    -- * Update
+  , insertAt
+  , insertAtMaybe
+
+    -- * Sub sequences
+  , uncons
+  , slice
+  , Data.Parameterized.Vector.take
+
+    -- * Zipping
+  , zipWith
+  , zipWithM
+  , zipWithM_
+  , interleave
+
+    -- * Reorder
+  , shuffle
+  , reverse
+  , rotateL
+  , rotateR
+  , shiftL
+  , shiftR
+
+    -- * Construction
+  , singleton
+  , cons
+  , snoc
+  , generate
+  , generateM
+
+    -- * Splitting and joining
+    -- ** General
+  , joinWithM
+  , joinWith
+  , splitWith
+  , splitWithA
+
+    -- ** Vectors
+  , split
+  , join
+  , append
+
+  ) where
+
+import qualified Data.Vector as Vector
+import Data.Functor.Compose
+import Data.Coerce
+import Data.Vector.Mutable (MVector)
+import qualified Data.Vector.Mutable as MVector
+import Control.Monad.ST
+import Data.Functor.Identity
+import Data.Parameterized.NatRepr
+import Data.Parameterized.NatRepr.Internal
+import Data.Proxy
+import Prelude hiding (length,reverse,zipWith)
+import Numeric.Natural
+
+import Data.Parameterized.Utils.Endian
+
+-- | Fixed-size non-empty vectors.
+data Vector n a where
+  Vector :: (1 <= n) => !(Vector.Vector a) -> Vector n a
+
+type role Vector nominal representational
+
+instance Eq a => Eq (Vector n a) where
+  (Vector x) == (Vector y) = x == y
+
+instance Show a => Show (Vector n a) where
+  show (Vector x) = show x
+
+-- | Get the elements of the vector as a list, lowest index first.
+toList :: Vector n a -> [a]
+toList (Vector v) = Vector.toList v
+{-# Inline toList #-}
+
+-- NOTE: We are using the raw 'NatRepr' constructor here, which is unsafe.
+-- | Length of the vector.
+-- @O(1)@
+length :: Vector n a -> NatRepr n
+length (Vector xs) = NatRepr (fromIntegral (Vector.length xs) :: Natural)
+{-# INLINE length #-}
+
+-- | The length of the vector as an "Int".
+lengthInt :: Vector n a -> Int
+lengthInt (Vector xs) = Vector.length xs
+{-# Inline lengthInt #-}
+
+elemAt :: ((i+1) <= n) => NatRepr i -> Vector n a -> a
+elemAt n (Vector xs) = xs Vector.! widthVal n
+
+-- | Get the element at the given index.
+-- @O(1)@
+elemAtMaybe :: Int -> Vector n a -> Maybe a
+elemAtMaybe n (Vector xs) = xs Vector.!? n
+{-# INLINE elemAt #-}
+
+-- | Get the element at the given index.
+-- Raises an exception if the element is not in the vector's domain.
+-- @O(1)@
+elemAtUnsafe :: Int -> Vector n a -> a
+elemAtUnsafe n (Vector xs) = xs Vector.! n
+{-# INLINE elemAtUnsafe #-}
+
+
+-- | Insert an element at the given index.
+-- @O(n)@.
+insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a
+insertAt n a (Vector xs) = Vector (Vector.unsafeUpd xs [(widthVal n,a)])
+
+-- | Insert an element at the given index.
+-- Return 'Nothing' if the element is outside the vector bounds.
+-- @O(n)@.
+insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)
+insertAtMaybe n a (Vector xs)
+  | 0 <= n && n < Vector.length xs = Just (Vector (Vector.unsafeUpd xs [(n,a)]))
+  | otherwise = Nothing
+
+
+-- | Proof that the length of this vector is not 0.
+nonEmpty :: Vector n a -> LeqProof 1 n
+nonEmpty (Vector _) = LeqProof
+{-# Inline nonEmpty #-}
+
+
+-- | Remove the first element of the vector, and return the rest, if any.
+uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
+uncons v@(Vector xs) = (Vector.head xs, mbTail)
+  where
+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
+  mbTail = case testStrictLeq (knownNat @1) (length v) of
+             Left n2_leq_n ->
+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))
+                  return (Vector (Vector.tail xs))
+             Right Refl    -> Left Refl
+{-# Inline uncons #-}
+
+
+--------------------------------------------------------------------------------
+
+-- | Make a vector of the given length and element type.
+-- Returns "Nothing" if the input list does not have the right number of
+-- elements.
+-- @O(n)@.
+fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)
+fromList n xs
+  | widthVal n == Vector.length v = Just (Vector v)
+  | otherwise                     = Nothing
+  where
+  v = Vector.fromList xs
+{-# INLINE fromList #-}
+
+
+-- | Extract a subvector of the given vector.
+slice :: (i + w <= n, 1 <= w) =>
+            NatRepr i {- ^ Start index -} ->
+            NatRepr w {- ^ Width of sub-vector -} ->
+            Vector n a -> Vector w a
+slice i w (Vector xs) = Vector (Vector.slice (widthVal i) (widthVal w) xs)
+{-# INLINE slice #-}
+
+-- | Take the front (lower-indexes) part of the vector.
+take :: forall n x a. (1 <= n) => NatRepr n -> Vector (n + x) a -> Vector n a
+take | LeqProof <- prf = slice (knownNat @0)
+  where
+  prf = leqAdd (leqRefl (Proxy @n)) (Proxy @x)
+
+--------------------------------------------------------------------------------
+
+instance Functor (Vector n) where
+  fmap f (Vector xs) = Vector (Vector.map f xs)
+  {-# Inline fmap #-}
+
+instance Foldable (Vector n) where
+  foldMap f (Vector xs) = foldMap f xs
+
+instance Traversable (Vector n) where
+  traverse f (Vector xs) = Vector <$> traverse f xs
+  {-# Inline traverse #-}
+
+-- | Zip two vectors, potentially changing types.
+-- @O(n)@
+zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
+zipWith f (Vector xs) (Vector ys) = Vector (Vector.zipWith f xs ys)
+{-# Inline zipWith #-}
+
+zipWithM :: Monad m => (a -> b -> m c) ->
+                       Vector n a -> Vector n b -> m (Vector n c)
+zipWithM f (Vector xs) (Vector ys) = Vector <$> Vector.zipWithM f xs ys
+{-# Inline zipWithM #-}
+
+zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
+zipWithM_ f (Vector xs) (Vector ys) = Vector.zipWithM_ f xs ys
+{-# Inline zipWithM_ #-}
+
+{- | Interleave two vectors.  The elements of the first vector are
+at even indexes in the result, the elements of the second are at odd indexes. -}
+interleave ::
+  forall n a. (1 <= n) => Vector n a -> Vector n a -> Vector (2 * n) a
+interleave (Vector xs) (Vector ys)
+  | LeqProof <- leqMulPos (Proxy @2) (Proxy @n) = Vector zs
+  where
+  len = Vector.length xs + Vector.length ys
+  zs  = Vector.generate len (\i -> let v = if even i then xs else ys
+                                   in v Vector.! (i `div` 2))
+
+
+--------------------------------------------------------------------------------
+
+{- | Move the elements around, as specified by the given function.
+  * Note: the reindexing function says where each of the elements
+          in the new vector come from.
+  * Note: it is OK for the same input element to end up in mulitple places
+          in the result.
+@O(n)@
+-}
+shuffle :: (Int -> Int) -> Vector n a -> Vector n a
+shuffle f (Vector xs) = Vector ys
+  where
+  ys = Vector.generate (Vector.length xs) (\i -> xs Vector.! f i)
+{-# Inline shuffle #-}
+
+-- | Reverse the vector.
+reverse :: forall a n. (1 <= n) => Vector n a -> Vector n a
+reverse x = shuffle (\i -> lengthInt x - i - 1) x
+
+-- | Rotate "left".  The first element of the vector is on the "left", so
+-- rotate left moves all elemnts toward the corresponding smaller index.
+-- Elements that fall off the beginning end up at the end.
+rotateL :: Int -> Vector n a -> Vector n a
+rotateL !n xs = shuffle rotL xs
+  where
+  !len   = lengthInt xs
+  rotL i = (i + n) `mod` len          -- `len` is known to be >= 1
+{-# Inline rotateL #-}
+
+-- | Rotate "right".  The first element of the vector is on the "left", so
+-- rotate right moves all elemnts toward the corresponding larger index.
+-- Elements that fall off the end, end up at the beginning.
+rotateR :: Int -> Vector n a -> Vector n a
+rotateR !n xs = shuffle rotR xs
+  where
+  !len   = lengthInt xs
+  rotR i = (i - n) `mod` len        -- `len` is known to be >= 1
+{-# Inline rotateR #-}
+
+{- | Move all elements towards smaller indexes.
+Elements that fall off the front are ignored.
+Empty slots are filled in with the given element.
+@O(n)@. -}
+shiftL :: Int -> a -> Vector n a -> Vector n a
+shiftL !x a (Vector xs) = Vector ys
+  where
+  !len = Vector.length xs
+  ys   = Vector.generate len (\i -> let j = i + x
+                                    in if j >= len then a else xs Vector.! j)
+{-# Inline shiftL #-}
+
+{- | Move all elements towards the larger indexes.
+Elements that "fall" off the end are ignored.
+Empty slots are filled in with the given element.
+@O(n)@. -}
+shiftR :: Int -> a -> Vector n a -> Vector n a
+shiftR !x a (Vector xs) = Vector ys
+  where
+  !len = Vector.length xs
+  ys   = Vector.generate len (\i -> let j = i - x
+                                    in if j < 0 then a else xs Vector.! j)
+{-# Inline shiftR #-}
+
+-------------------------------------------------------------------------------i
+
+-- | Append two vectors. The first one is at lower indexes in the result.
+append :: Vector m a -> Vector n a -> Vector (m + n) a
+append v1@(Vector xs) v2@(Vector ys) =
+  case leqAddPos (length v1) (length v2) of { LeqProof ->
+    Vector (xs Vector.++ ys)
+  }
+{-# Inline append #-}
+
+--------------------------------------------------------------------------------
+-- Constructing Vectors
+
+-- | Vector with exactly one element
+singleton :: forall a. a -> Vector 1 a
+singleton a = Vector (Vector.singleton a)
+
+leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)
+leqLen v =
+  let leqSucc :: forall f z. f z -> LeqProof z (z + 1)
+      leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)
+  in leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))
+
+-- | Add an element to the head of a vector
+cons :: forall n a. a -> Vector n a -> Vector (n+1) a
+cons a v@(Vector x) = case leqLen v of LeqProof -> (Vector (Vector.cons a x))
+
+-- | Add an element to the tail of a vector
+snoc :: forall n a. Vector n a -> a -> Vector (n+1) a
+snoc v@(Vector x) a = case leqLen v of LeqProof -> (Vector (Vector.snoc x a))
+
+-- | This newtype wraps Vector so that we can curry it in the call to
+-- @natRecBounded@. It adds 1 to the length so that the base case is
+-- a @Vector@ of non-zero length.
+newtype Vector' a n = MkVector' (Vector (n+1) a)
+
+unVector' :: Vector' a n -> Vector (n+1) a
+unVector' (MkVector' v) = v
+
+snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)
+snoc' v = MkVector' . snoc (unVector' v)
+
+generate' :: forall h a
+           . NatRepr h
+          -> (forall n. (n <= h) => NatRepr n -> a)
+          -> Vector' a h
+generate' h gen =
+  case isZeroOrGT1 h of
+    Left Refl -> base
+    Right LeqProof ->
+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->
+      natRecBounded (decNat h) (decNat h) base step
+      }
+  where base :: Vector' a 0
+        base = MkVector' $ singleton (gen (knownNat @0))
+        step :: forall m. (1 <= h, m <= h - 1)
+             => NatRepr m -> Vector' a m -> Vector' a (m + 1)
+        step m v =
+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->
+          case (leqAdd2 (LeqProof :: LeqProof m (h-1))
+                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->
+            snoc' v (gen (incNat m))
+          }}
+
+-- | Apply a function to each element in a range starting at zero;
+-- return the a vector of values obtained.
+-- cf. both @natFromZero@ and @Data.Vector.generate@
+generate :: forall h a
+          . NatRepr h
+         -> (forall n. (n <= h) => NatRepr n -> a)
+         -> Vector (h + 1) a
+generate h gen = unVector' (generate' h gen)
+
+-- | Since @Vector@ is traversable, we can pretty trivially sequence
+-- @natFromZeroVec@ inside a monad.
+generateM :: forall m h a. (Monad m)
+          => NatRepr h
+          -> (forall n. (n <= h) => NatRepr n -> m a)
+          -> m (Vector (h + 1) a)
+generateM h gen = sequence $ generate h gen
+
+--------------------------------------------------------------------------------
+
+coerceVec :: Coercible a b => Vector n a -> Vector n b
+coerceVec = coerce
+
+-- | Monadically join a vector of values, using the given function.
+-- This functionality can sometimes be reproduced by creating a newtype
+-- wrapper and using @joinWith@, this implementation is provided for
+-- convenience.
+joinWithM ::
+  forall m f n w.
+  (1 <= w, Monad m) =>
+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))
+  {- ^ A function for joining contained elements.  The first argument is
+       the size of the accumulated third term, and the second argument
+       is the element to join to the accumulated term.  The function
+       can use any join strategy desired (prepending/"BigEndian",
+       appending/"LittleEndian", etc.). -}
+  -> NatRepr w
+  -> Vector n (f w)
+  -> m (f (n * w))
+
+joinWithM jn w = fmap fst . go
+  where
+  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))
+  go exprs =
+    case uncons exprs of
+      (a, Left Refl) -> return (a, w)
+      (a, Right rest) ->
+        case nonEmpty rest                of { LeqProof ->
+        case leqMulPos (length rest) w    of { LeqProof ->
+        case nonEmpty exprs               of { LeqProof ->
+        case lemmaMul w (length exprs)    of { Refl -> do
+          -- @siddharthist: This could probably be written applicatively?
+          (res, sz) <- go rest
+          joined <- jn sz a res
+          return (joined, addNat w sz)
+        }}}}
+
+-- | Join a vector of vectors, using the given function to combine the
+-- sub-vectors.
+joinWith ::
+  forall f n w.
+  (1 <= w) =>
+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))
+  {- ^ A function for joining contained elements.  The first argument is
+       the size of the accumulated third term, and the second argument
+       is the element to join to the accumulated term.  The function
+       can use any join strategy desired (prepending/"BigEndian",
+       appending/"LittleEndian", etc.). -}
+  -> NatRepr w
+  -> Vector n (f w)
+  -> f (n * w)
+joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v
+{-# Inline joinWith #-}
+
+-- | Split a vector into a vector of vectors.
+--
+-- The "Endian" parameter determines the ordering of the inner
+-- vectors.  If "LittleEndian", then less significant bits go into
+-- smaller indexes.  If "BigEndian", then less significant bits go
+-- into larger indexes.  See the documentation for 'split' for more
+-- details.
+splitWith :: forall f w n.
+  (1 <= w, 1 <= n) =>
+  Endian ->
+  (forall i. (i + w <= n * w) =>
+             NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
+  {- ^ A function for slicing out a chunk of length @w@, starting at @i@ -} ->
+  NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
+splitWith endian select n w val = Vector (Vector.create initializer)
+  where
+  len          = widthVal n
+  start :: Int
+  next :: Int -> Int
+  (start,next) = case endian of
+                   LittleEndian -> (0, succ)
+                   BigEndian    -> (len - 1, pred)
+
+  initializer :: forall s. ST s (MVector s (f w))
+  initializer =
+    do LeqProof <- return (leqMulPos n w)
+       LeqProof <- return (leqMulMono n w)
+
+       v <- MVector.new len
+       let fill :: Int -> NatRepr i -> ST s ()
+           fill loc i =
+             let end = addNat i w in
+             case testLeq end inLen of
+               Just LeqProof ->
+                 do MVector.write v loc (select inLen i val)
+                    fill (next loc) end
+               Nothing -> return ()
+
+
+       fill start (knownNat @0)
+       return v
+
+  inLen :: NatRepr (n * w)
+  inLen = natMultiply n w
+{-# Inline splitWith #-}
+
+-- We can sneakily put our functor in the parameter "f" of @splitWith@ using the
+-- @Compose@ newtype.
+-- | An applicative version of @splitWith@.
+splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) =>
+  Endian ->
+  (forall i. (i + w <= n * w) =>
+             NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))
+  {- ^ f function for slicing out f chunk of length @w@, starting at @i@ -} ->
+  NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
+splitWithA e select n w val = traverse getCompose $
+  splitWith @(Compose f g) e select' n w $ Compose (pure val)
+  where -- Wrap everything in Compose
+        select' :: (forall i. (i + w <= n * w)
+                => NatRepr (n * w) -> NatRepr i -> Compose f g (n * w) -> Compose f g w)
+        -- Whatever we pass in as "val" is what's passed to select anyway,
+        -- so there's no need to examine the argument. Just use "val" directly here.
+        select' nw i _ = Compose $ select nw i val
+
+newtype Vec a n = Vec (Vector n a)
+
+vSlice :: (i + w <= l, 1 <= w) =>
+  NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w
+vSlice w _ i (Vec xs) = Vec (slice i w xs)
+{-# Inline vSlice #-}
+
+-- | Append the two bit vectors.  The first argument is
+-- at the lower indexes of the resulting vector.
+vAppend :: NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)
+vAppend _ (Vec xs) (Vec ys) = Vec (append xs ys)
+{-# Inline vAppend #-}
+
+-- | Split a vector into a vector of vectors.  The default ordering of
+-- the outer result vector is "LittleEndian".
+--
+-- For example:
+-- @
+--   let wordsize = knownNat :: NatRepr 3
+--       vecsize = knownNat :: NatRepr 12
+--       numwords = knownNat :: NatRepr 4  (12 / 3)
+--       Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
+--   in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]"
+-- @
+-- whereas a BigEndian result would have been
+-- @
+--      [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]
+-- @
+split :: (1 <= w, 1 <= n) =>
+         NatRepr n -- ^ Inner vector size
+      -> NatRepr w -- ^ Outer vector size
+      -> Vector (n * w) a -- ^ Input vector
+      -> Vector n (Vector w a)
+split n w xs = coerceVec (splitWith LittleEndian (vSlice w) n w (Vec xs))
+{-# Inline split #-}
+
+-- | Join a vector of vectors into a single vector.  Assumes an
+-- append/"LittleEndian" join strategy: the order of the inner vectors
+-- is preserved in the result vector.
+--
+-- @
+--   let innersize = knownNat :: NatRepr 4
+--       Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
+--       Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
+--       Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
+--       outersize = knownNat :: NatRepr 3
+--       Just outer = fromList outersize [ inner1, inner2, inner3 ]
+--   in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
+-- @
+-- a prepend/"BigEndian" join strategy would have the result:
+-- @
+--   [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]
+-- @
+join :: (1 <= w) => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
+join w xs = ys
+  where Vec ys = joinWith vAppend w (coerceVec xs)
+{-# Inline join #-}
diff --git a/src/Data/Parameterized/WithRepr.hs b/src/Data/Parameterized/WithRepr.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/WithRepr.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-|
+Copyright        : (c) Galois, Inc 2019
+
+This module declares a class with a single method that can be used to
+derive a 'KnownRepr' constraint from an explicit 'Repr' argument.
+Clients of this method need only create an empty instance. The default
+implementation suffices.
+
+For example, suppose we have defined a 'Repr' type for 'Peano' numbers:
+
+@
+data Peano = Z | S Peano
+
+data PeanoRepr p where
+    ZRepr :: PeanoRepr Z
+    SRepr :: PeanoRepr p -> PeanoRepr (S p)
+
+-- KnownRepr instances
+@
+
+Then the instance for this class
+@
+instance IsRepr PeanoRepr
+@
+
+means that functions with 'KnownRepr' constraints can be used after
+pattern matching.
+
+@
+f :: KnownRepr PeanoRepr a => ...
+
+example :: PeanoRepr n -> ...
+example ZRepr = ...
+example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...
+@
+
+
+NOTE: The type 'f' must be a *singleton* type--- i.e.  for a given
+type 'a' there should be only one value that inhabits 'f a'. If that
+is not the case, this operation can be used to subvert coherence.
+
+Credit: the unsafe implementation of 'withRepr' is taken from the
+'withSingI' function in the singletons library
+<http://hackage.haskell.org/package/singletons-2.5.1/>.  Packaging
+this method in a class here makes it more flexible---we do not have to
+define a dedicated 'Sing' type, but can use any convenient singleton
+as a 'Repr'.
+
+NOTE: if this module is compiled without UNSAFE_OPS, the default
+method will not be available.
+
+-}
+module Data.Parameterized.WithRepr(IsRepr(..)) where
+
+import Data.Parameterized.Classes
+
+#ifdef UNSAFE_OPS
+import Data.Constraint(Dict(..))
+import Unsafe.Coerce(unsafeCoerce)
+
+import Data.Parameterized.NatRepr (NatRepr)
+import Data.Parameterized.SymbolRepr (SymbolRepr)
+import Data.Parameterized.Peano (PeanoRepr)
+import Data.Parameterized.Context(Assignment)
+import Data.Parameterized.List(List)
+#else
+import Data.Parameterized.Peano (PeanoRepr,PeanoView(..))
+#endif
+import Data.Parameterized.BoolRepr
+
+-- | Turn an explicit Repr value into an implict KnownRepr constraint
+class IsRepr (f :: k -> *) where
+
+  withRepr :: f a -> (KnownRepr f a => r) -> r
+
+#ifdef UNSAFE_OPS
+  withRepr si r = case reprInstance si of
+                     Dict -> r
+
+reprInstance :: forall f a . IsRepr f => f a -> Dict (KnownRepr f a)
+reprInstance s = with_repr Dict
+   where
+     with_repr :: (KnownRepr f a => Dict (KnownRepr f a)) -> Dict (KnownRepr f a)
+     with_repr si = unsafeCoerce (Don'tInstantiate si) s
+
+newtype DI f a = Don'tInstantiate (KnownRepr f a => Dict (KnownRepr f a))
+#endif
+
+
+------------------------------------
+-- Instances for types defined in parameterized-utils
+
+#ifdef UNSAFE_OPS
+instance IsRepr NatRepr
+instance IsRepr SymbolRepr
+instance IsRepr PeanoRepr
+instance IsRepr BoolRepr
+instance IsRepr f => IsRepr (List f)
+instance IsRepr f => IsRepr (Assignment f)
+#else
+-- awful, slow implementation for PeanoRepr
+instance IsRepr PeanoRepr where
+  withRepr ZRepr f     = f
+  withRepr (SRepr m) f = withRepr m f
+
+instance IsRepr BoolRepr where
+  withRepr TrueRepr f = f
+  withRepr FalseRepr f = f
+#endif
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -16,6 +16,7 @@
 import Data.Parameterized.TraversableFC
 import Data.Parameterized.Some
 
+import qualified Data.Parameterized.Context as C
 import qualified Data.Parameterized.Context.Safe as S
 import qualified Data.Parameterized.Context.Unsafe as U
 
@@ -114,18 +115,13 @@
          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
-             x'' = U.adjust twiddle idx_x x
-             y'' = S.adjust twiddle idx_y y
+         let x' = x & ixF idx_x %~ twiddle
+             y' = y & ixF idx_y %~ twiddle
 
          return (toListFC Some x' == toListFC Some y' &&
                  -- adjust actually modified the entry
                  toListFC Some x /= toListFC Some x' &&
-                 toListFC Some y /= toListFC Some y' &&
-                 -- verify new version is equivalent to older deprecated version
-                 toListFC Some x'' == toListFC Some x' &&
-                 toListFC Some y'' == toListFC Some y')
+                 toListFC Some y /= toListFC Some y')
 
    , testProperty "update test" $ \v vs i -> ioProperty $ do
          let vals = v:vs  -- ensures vals is not an empty array
@@ -138,10 +134,8 @@
 
          let x' = over (ixF idx_x) twiddle x
              y' = (ixF idx_y) %~ twiddle $ y
-             updX = set (ixF idx_x) (x' U.! idx_x) x
-             updY = (ixF idx_y) .~  (y' S.! idx_y) $ y
-             updX' = U.update idx_x (x' U.! idx_x) x
-             updY' = S.update idx_y (y' S.! idx_y) y
+             updX = x & ixF idx_x .~ x' U.! idx_x
+             updY = y & ixF idx_y .~ y' S.! idx_y
 
          return (toListFC Some updX == toListFC Some updY &&
                  -- update actually modified the entry
@@ -149,10 +143,7 @@
                  toListFC Some y /= toListFC Some updY &&
                  -- update modified the expected entry
                  toListFC Some x' == toListFC Some updX &&
-                 toListFC Some y' == toListFC Some updY &&
-                 -- verify new version is equivalent to older deprecated version
-                 toListFC Some updX == toListFC Some updX' &&
-                 toListFC Some updY == toListFC Some updY'
+                 toListFC Some y' == toListFC Some updY
                 )
 
    , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do
@@ -167,4 +158,11 @@
          case testEquality x y of
            Just Refl -> return $ vals1 == vals2
            Nothing   -> return $ vals1 /= vals2
+
+   , 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'
    ]
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Vector.hs
@@ -0,0 +1,70 @@
+{-# Language DataKinds #-}
+{-# Language ExplicitForAll #-}
+{-# Language TypeOperators #-}
+{-# Language TypeFamilies #-}
+{-# Language FlexibleInstances #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language StandaloneDeriving #-}
+{-# Language CPP #-}
+{-# 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 )
+
+import Data.Parameterized.NatRepr
+import Data.Parameterized.Vector
+import GHC.TypeLits
+import Data.Semigroup
+import Prelude hiding (reverse)
+
+
+instance KnownNat n => Arbitrary (NatRepr n) where
+  arbitrary = return knownNat
+
+
+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)
+
+
+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)
+  -- @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))
+  -- @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]))
+  -- @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))
+  ]
diff --git a/test/UnitTest.hs b/test/UnitTest.hs
--- a/test/UnitTest.hs
+++ b/test/UnitTest.hs
@@ -4,6 +4,7 @@
 
 import qualified Test.Context
 import qualified Test.NatRepr
+import qualified Test.Vector
 
 main :: IO ()
 main = tests >>= defaultMainWithIngredients ingrs
@@ -19,4 +20,5 @@
 tests = testGroup "ParameterizedUtils" <$> sequence
   [ Test.Context.contextTests
   , Test.NatRepr.natTests
+  , Test.Vector.vecTests
   ]