diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,16 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.1.6.0 -- *2022 Dec 18*
+
+  * Added `FinMap`: an integer map with a statically-known maximum size.
+  * Added `someLens` to `Some` to create a parameterized lens.
+  * Allow building with `hashable-1.4.*`. Because `hashable-1.4.0.0` adds an
+    `Eq` superclass to `Hashable`, some instances of `Hashable` in
+    `parameterized-utils` now require additional `TestEquality` constraints, as
+    the corresponding `Eq` instances for these data types also require
+    `TestEquality` constraints.
+  * Bump constraints to allow: vector-0.13, lens-5.2, tasty-hedgehog-1.3.0.0--1.4.0.0, GHC-9.4
+
 ## 2.1.5.0 -- *2022 Mar 08*
 
   * Add support for GHC 9.2.  Drop support for GHC 8.4 (or earlier).
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.1.5.0
+Version:       2.1.6.0
 Author:        Galois Inc.
 Maintainer:    kquick@galois.com
 stability:     stable
@@ -19,7 +19,7 @@
 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.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1
+tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1, GHC==9.4.3
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -51,20 +51,20 @@
   import: bldflags
   build-depends: base >= 4.10 && < 5
                , base-orphans   >=0.8.2 && <0.9
-               , th-abstraction >=0.3  && <0.5
+               , th-abstraction >=0.4.2 && <0.5
                , constraints    >=0.10 && <0.14
                , containers
                , deepseq
                , ghc-prim
-               , hashable       >=1.2  && <1.4
-               , hashtables     ==1.2.*
+               , hashable       >=1.2  && <1.5
+               , hashtables     >=1.2  && <1.4
                , indexed-traversable
-               , lens           >=4.16 && <5.2
+               , lens           >=4.16 && <5.3
                , mtl
                , profunctors    >=5.6 && < 5.7
                , template-haskell
                , text
-               , vector         ==0.12.*
+               , vector         >=0.12 && < 0.14
 
   hs-source-dirs: src
 
@@ -84,6 +84,9 @@
     Data.Parameterized.DataKind
     Data.Parameterized.DecidableEq
     Data.Parameterized.Fin
+    Data.Parameterized.FinMap
+    Data.Parameterized.FinMap.Safe
+    Data.Parameterized.FinMap.Unsafe
     Data.Parameterized.HashTable
     Data.Parameterized.List
     Data.Parameterized.Map
@@ -120,8 +123,10 @@
   other-modules:
     Test.Context
     Test.Fin
+    Test.FinMap
     Test.List
     Test.NatRepr
+    Test.Some
     Test.SymbolRepr
     Test.TH
     Test.Vector
@@ -138,7 +143,7 @@
                , tasty >= 1.2 && < 1.5
                , tasty-ant-xml == 1.1.*
                , tasty-hunit >= 0.9 && < 0.11
-               , tasty-hedgehog
+               , tasty-hedgehog >= 1.2
 
   if impl(ghc >= 8.6)
     build-depends:
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
@@ -351,7 +351,7 @@
 instance ShowF f => Show (TypeAp f tp) where
   showsPrec p (TypeAp x) = showsPrecF p x
 
-instance HashableF f => Hashable (TypeAp f tp) where
+instance (HashableF f, TestEquality f) => Hashable (TypeAp f tp) where
   hashWithSalt s (TypeAp x) = hashWithSaltF s x
 
 ------------------------------------------------------------------------
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
@@ -595,10 +595,10 @@
 instance HashableF (Index ctx) where
   hashWithSaltF s i = hashWithSalt s (indexVal i)
 
-instance HashableF f => HashableF (Assignment f) where
+instance (HashableF f, TestEquality f) => HashableF (Assignment f) where
   hashWithSaltF = hashWithSalt
 
-instance HashableF f => Hashable (Assignment f ctx) where
+instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where
   hashWithSalt s AssignmentEmpty = s
   hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x
 
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
@@ -851,10 +851,10 @@
 instance Hashable (Index ctx tp) where
   hashWithSalt = hashWithSaltF
 
-instance HashableF f => Hashable (Assignment f ctx) where
+instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where
   hashWithSalt s (Assignment a) = hashWithSaltF s a
 
-instance HashableF f => HashableF (Assignment f) where
+instance (HashableF f, TestEquality f) => HashableF (Assignment f) where
   hashWithSaltF = hashWithSalt
 
 instance ShowF f => Show (Assignment f ctx) where
diff --git a/src/Data/Parameterized/Fin.hs b/src/Data/Parameterized/Fin.hs
--- a/src/Data/Parameterized/Fin.hs
+++ b/src/Data/Parameterized/Fin.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {-|
 Copyright        : (c) Galois, Inc 2021
@@ -22,11 +23,14 @@
 module Data.Parameterized.Fin
   ( Fin
   , mkFin
+  , buildFin
+  , countFin
   , viewFin
   , finToNat
   , embed
   , tryEmbed
   , minFin
+  , incFin
   , fin0Void
   , fin1Unit
   , fin2Bool
@@ -62,12 +66,39 @@
 
 mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n
 mkFin = Fin
+{-# INLINE mkFin #-}
 
+newtype Fin' n = Fin' { getFin' :: Fin (n + 1) }
+
+buildFin ::
+  forall m.
+  NatRepr m ->
+  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Fin (n + 1 + 1)) ->
+  Fin (m + 1)
+buildFin m f =
+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> Fin' k -> Fin' (k + 1)
+      f' = (\n (Fin' fin) -> Fin' (f n fin))
+  in getFin' (natRecStrictlyBounded m (Fin' minFin) f')
+
+-- | Count all of the numbers up to @m@ that meet some condition.
+countFin ::
+  NatRepr m ->
+  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Bool) ->
+  Fin (m + 1)
+countFin m f =
+  buildFin m $
+    \n count ->
+      if f n count
+      then incFin count
+      else case leqSucc count of
+              LeqProof -> embed count
+
 viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r
 viewFin f (Fin i) = f i
 
 finToNat :: Fin n -> Natural
 finToNat (Fin i) = natValue i
+{-# INLINABLE finToNat #-}
 
 embed :: forall n m. (n <= m) => Fin n -> Fin m
 embed =
@@ -86,6 +117,12 @@
 -- | The smallest element of @'Fin' n@
 minFin :: (1 <= n) => Fin n
 minFin = Fin (knownNat @0)
+{-# INLINABLE minFin #-}
+
+incFin :: forall n. Fin n -> Fin (n + 1)
+incFin (Fin (i :: NatRepr i)) =
+  case leqAdd2 (LeqProof :: LeqProof (i + 1) n) (LeqProof :: LeqProof 1 1) of
+    LeqProof -> mkFin (incNat i)
 
 fin0Void :: Iso' (Fin 0) Void
 fin0Void =
diff --git a/src/Data/Parameterized/FinMap.hs b/src/Data/Parameterized/FinMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/FinMap.hs
@@ -0,0 +1,79 @@
+{-|
+Copyright        : (c) Galois, Inc 2022
+
+@'FinMap' n a@ conceptually (see NOTE) a map with @'Data.Parameterized.Fin.Fin'
+n@ keys, implying a maximum size of @n@. Here's how 'FinMap' compares to other
+map-like types:
+
+* @'FinMap' n a@ is conceptually isomorphic to a
+  @'Data.Parameterized.Vector' n ('Maybe' a)@, but can be more space-efficient
+  especially if @n@ is large and the vector is populated with a small number of
+  'Just' values.
+* @'FinMap'@ is less general than 'Data.Map.Map', because it has a fixed key
+  type (@'Data.Parameterized.Fin.Fin' n@).
+* @'FinMap' n a@ is similar to @'Data.IntMap.IntMap' a@, but it provides a
+  static guarantee of a maximum size, and its operations (such as 'size') allow
+  the recovery of more type-level information.
+* @'FinMap'@ is dissimilar from "Data.Parameterized.Map.MapF" in that neither
+  the key nor value type of 'FinMap' is parameterized.
+
+The type parameter @n@ doesn't track the /current/ number of key-value pairs in
+a @'FinMap' n@ (i.e., the size of the map), but rather /an upper bound/.
+'insert' and 'delete' don't alter @n@, whereas 'incMax' does - despite the fact
+that it has no effect on the keys and values in the 'FinMap'.
+
+The 'FinMap' interface has two implementations:
+
+* The implementation in "Data.Parameterized.FinMap.Unsafe" is backed by an
+  'Data.IntMap.IntMap', and must have a size of at most @'maxBound' :: 'Int'@.
+  This module uses unsafe operations like 'Unsafe.Coerce.unsafeCoerce'
+  internally for the sake of time and space efficiency.
+* The implementation in "Data.Parameterized.FinMap.Safe" is backed by an
+  @'Data.Map.Map' ('Data.Parameterized.Fin.Fin' n)@. All of its functions are
+  implemented using safe operations.
+
+The implementation in 'Data.Parameterized.FinMap.Unsafe.FinMap' is property
+tested against that in 'Data.Parameterized.FinMap.Safe.FinMap' to ensure
+they have the same behavior.
+
+In this documentation, /W/ is used in big-O notations the same way as in the
+"Data.IntMap" documentation.
+
+NOTE: Where the word "conceptually" is used, it implies that this correspondence
+is not literally true, but is true modulo some details such as differences
+between bounded types like 'Int' and unbounded types like 'Integer'.
+
+Several of the functions in both implementations are marked @INLINE@ or
+@INLINABLE@. There are three reasons for this:
+
+* Some of these just have very small definitions and so inlining is likely more
+  beneficial than harmful.
+* Some participate in @RULES@ relevant to functions used in their
+  implementations.
+* They are thin wrappers (often just newtype wrappers) around functions marked
+  @INLINE@, which should therefore also be inlined.
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.FinMap
+  (
+#ifdef UNSAFE_OPS
+    module Data.Parameterized.FinMap.Unsafe
+#else
+    module Data.Parameterized.FinMap.Safe
+#endif
+  ) where
+
+#ifdef UNSAFE_OPS
+import Data.Parameterized.FinMap.Unsafe
+#else
+import Data.Parameterized.FinMap.Safe
+#endif
diff --git a/src/Data/Parameterized/FinMap/Safe.hs b/src/Data/Parameterized/FinMap/Safe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/FinMap/Safe.hs
@@ -0,0 +1,248 @@
+{-|
+Copyright        : (c) Galois, Inc 2022
+
+See "Data.Parameterized.FinMap".
+-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.FinMap.Safe
+  ( FinMap
+  -- * Query
+  , null
+  , lookup
+  , size
+  -- * Construction
+  , incMax
+  , embed
+  , empty
+  , singleton
+  , insert
+  , buildFinMap
+  , append
+  , fromVector
+  -- * Operations
+  , delete
+  , decMax
+  , mapWithKey
+  , unionWithKey
+  , unionWith
+  , union
+  ) where
+
+import           Prelude hiding (lookup, null)
+
+import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
+import           Data.Functor.WithIndex (FunctorWithIndex(imap))
+import           Data.Maybe (isJust)
+import           Data.Proxy (Proxy(Proxy))
+import           Data.Map (Map)
+import qualified Data.Map as Map
+import           GHC.TypeLits (KnownNat, Nat)
+
+import           Data.Parameterized.Fin (Fin)
+import qualified Data.Parameterized.Fin as Fin
+import           Data.Parameterized.NatRepr (NatRepr, type (+), type (<=))
+import qualified Data.Parameterized.NatRepr as NatRepr
+import           Data.Parameterized.Vector (Vector)
+import qualified Data.Parameterized.Vector as Vec
+
+------------------------------------------------------------------------
+-- Type
+
+-- | @'FinMap' n a@ is a map with @'Fin' n@ keys and @a@ values.
+data FinMap (n :: Nat) a =
+  FinMap
+    { getFinMap :: Map (Fin n) a
+    , maxSize :: NatRepr n
+    }
+
+instance Eq a => Eq (FinMap n a) where
+  fm1 == fm2 = getFinMap fm1 == getFinMap fm2
+  {-# INLINABLE (==) #-}
+
+instance Semigroup (FinMap n a) where
+  (<>) = union
+  {-# INLINE (<>) #-}
+
+instance KnownNat n => Monoid (FinMap n a) where
+  mempty = empty
+  {-# INLINE mempty #-}
+
+instance Functor (FinMap n) where
+  fmap f fm = fm { getFinMap = fmap f (getFinMap fm) }
+  {-# INLINABLE fmap #-}
+
+instance Foldable (FinMap n) where
+  foldMap f = foldMap f . getFinMap
+  {-# INLINABLE foldMap #-}
+
+instance Traversable (FinMap n) where
+  traverse f fm = FinMap <$> traverse f (getFinMap fm) <*> pure (maxSize fm)
+
+instance FunctorWithIndex (Fin n) (FinMap n) where
+  imap f fm = fm { getFinMap = Map.mapWithKey f (getFinMap fm) }
+  -- Inline so that RULES for Map.mapWithKey can fire
+  {-# INLINE imap #-}
+
+instance FoldableWithIndex (Fin n) (FinMap n) where
+  ifoldMap f = Map.foldMapWithKey f . getFinMap
+  {-# INLINABLE ifoldMap #-}
+
+-- | Non-lawful instance, provided for testing
+instance Show a => Show (FinMap n a) where
+  show fm = show (getFinMap fm)
+  {-# INLINABLE show #-}
+
+------------------------------------------------------------------------
+-- Query
+
+-- | /O(1)/. Is the map empty?
+null :: FinMap n a -> Bool
+null = Map.null . getFinMap
+{-# INLINABLE null #-}
+
+-- | /O(log n)/. Fetch the value at the given key in the map.
+lookup :: Fin n -> FinMap n a -> Maybe a
+lookup k = Map.lookup k . getFinMap
+{-# INLINABLE lookup #-}
+
+-- | /O(nlog(n))/. Number of elements in the map.
+--
+-- This operation is much slower than 'Data.Parameterized.FinMap.Unsafe.size'
+-- because its implementation must provide significant evidence to the
+-- type-checker, and the easiest way to do that is fairly inefficient.
+-- If speed is a concern, use "Data.Parameterized.FinMap.Unsafe".
+size :: forall n a. FinMap n a -> Fin (n + 1)
+size fm =
+  Fin.countFin (maxSize fm) (\k _count -> isJust (lookup (Fin.mkFin k) fm))
+
+------------------------------------------------------------------------
+-- Construction
+
+-- | /O(n log n)/. Increase maximum key/size by 1.
+--
+-- This does not alter the key-value pairs in the map, but rather increases the
+-- maximum number of key-value pairs that the map can hold. See
+-- "Data.Parameterized.FinMap" for more information.
+--
+-- Requires @n + 1 < (maxBound :: Int)@.
+incMax :: forall n a. FinMap n a -> FinMap (n + 1) a
+incMax fm =
+  case NatRepr.leqSucc (Proxy :: Proxy n) of
+    NatRepr.LeqProof -> embed (NatRepr.incNat (maxSize fm)) fm
+
+-- | /O(n log n)/. Increase maximum key/size.
+--
+-- Requires @m < (maxBound :: Int)@.
+embed :: (n <= m) => NatRepr m -> FinMap n a -> FinMap m a
+embed m fm =
+  FinMap
+    { getFinMap = Map.mapKeys Fin.embed (getFinMap fm)
+    , maxSize = m
+    }
+
+-- | /O(1)/. The empty map.
+empty :: KnownNat n => FinMap n a
+empty = FinMap Map.empty NatRepr.knownNat
+{-# INLINABLE empty #-}
+
+-- | /O(1)/. A map with one element.
+singleton :: a -> FinMap 1 a
+singleton item =
+  FinMap
+    { getFinMap = Map.singleton (Fin.mkFin (NatRepr.knownNat :: NatRepr 0)) item
+    , maxSize = NatRepr.knownNat :: NatRepr 1
+    }
+
+-- | /O(log n)/.
+insert :: Fin n -> a -> FinMap n a -> FinMap n a
+insert k v fm = fm { getFinMap = Map.insert k v (getFinMap fm) }
+{-# INLINABLE insert #-}
+
+-- buildFinMap, append, and fromVector are duplicated exactly between the safe
+-- and unsafe modules because they are used in comparative testing (and so
+-- implementations must be available for both types).
+
+newtype FinMap' a (n :: Nat) = FinMap' { unFinMap' :: FinMap n a }
+
+buildFinMap ::
+  forall m a.
+  NatRepr m ->
+  (forall n. (n + 1 <= m) => NatRepr n -> FinMap n a -> FinMap (n + 1) a) ->
+  FinMap m a
+buildFinMap m f =
+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> FinMap' a k -> FinMap' a (k + 1)
+      f' = (\n (FinMap' fin) -> FinMap' (f n fin))
+  in unFinMap' (NatRepr.natRecStrictlyBounded m (FinMap' empty) f')
+
+-- | /O(min(n,W))/.
+append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
+append k v fm =
+  case NatRepr.leqSucc k of
+    NatRepr.LeqProof -> insert (Fin.mkFin k) v (incMax fm)
+
+fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
+fromVector v =
+  buildFinMap
+    (Vec.length v)
+    (\k m ->
+      case Vec.elemAt k v of
+        Just e -> append k e m
+        Nothing -> incMax m)
+
+------------------------------------------------------------------------
+-- Operations
+
+-- | /O(log n)/.
+delete :: Fin n -> FinMap n a -> FinMap n a
+delete k fm = fm { getFinMap = Map.delete k (getFinMap fm) }
+{-# INLINABLE delete #-}
+
+-- | Decrement the key/size, removing the item at key @n + 1@ if present.
+decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
+decMax n fm =
+  FinMap
+    { getFinMap = maybeMapKeys (Fin.tryEmbed sz n) (getFinMap fm)
+    , maxSize = n
+    }
+  where
+    sz = maxSize fm
+
+    maybeMapKeys :: Ord k2 => (k1 -> Maybe k2) -> Map k1 a -> Map k2 a
+    maybeMapKeys f m =
+      Map.foldrWithKey
+        (\k v accum ->
+           case f k of
+             Just k' -> Map.insert k' v accum
+             Nothing -> accum)
+        Map.empty
+        m
+
+mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
+mapWithKey f fm = fm { getFinMap = Map.mapWithKey f (getFinMap fm) }
+-- Inline so that RULES for Map.mapWithKey can fire
+{-# INLINE mapWithKey #-}
+
+-- | /O(n+m)/.
+unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
+unionWithKey f fm1 fm2 =
+  FinMap
+    { getFinMap = Map.unionWithKey f (getFinMap fm1) (getFinMap fm2)
+    , maxSize = maxSize fm1
+    }
+
+-- | /O(n+m)/.
+unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
+unionWith f = unionWithKey (\_ v1 v2 -> f v1 v2)
+
+-- | /O(n+m)/. Left-biased union, i.e. (@'union' == 'unionWith' 'const'@).
+union :: FinMap n a -> FinMap n a -> FinMap n a
+union = unionWith const
diff --git a/src/Data/Parameterized/FinMap/Unsafe.hs b/src/Data/Parameterized/FinMap/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/FinMap/Unsafe.hs
@@ -0,0 +1,249 @@
+{-|
+Copyright        : (c) Galois, Inc 2022
+
+See "Data.Parameterized.FinMap".
+-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.FinMap.Unsafe
+  ( FinMap
+  -- * Query
+  , null
+  , lookup
+  , size
+  -- * Construction
+  , incMax
+  , embed
+  , empty
+  , singleton
+  , insert
+  , buildFinMap
+  , append
+  , fromVector
+  -- * Operations
+  , delete
+  , decMax
+  , mapWithKey
+  , unionWithKey
+  , unionWith
+  , union
+  ) where
+
+import           Prelude hiding (lookup, null)
+
+import           Data.Functor.WithIndex (FunctorWithIndex(imap))
+import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
+import           Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import           GHC.TypeLits (KnownNat, Nat)
+import           Numeric.Natural (Natural)
+import           Unsafe.Coerce (unsafeCoerce)
+
+import           Data.Parameterized.Fin (Fin, mkFin)
+import qualified Data.Parameterized.Fin as Fin
+import           Data.Parameterized.NatRepr (LeqProof, NatRepr, type (+), type (<=))
+import qualified Data.Parameterized.NatRepr as NatRepr
+import           Data.Parameterized.Some (Some(Some))
+import           Data.Parameterized.Vector (Vector)
+import qualified Data.Parameterized.Vector as Vec
+
+-- This is pulled out as a function so that it's obvious that its use is safe
+-- (since Natural is unbounded).
+intToNat :: Int -> Natural
+intToNat = fromIntegral
+{-# INLINE intToNat #-}
+
+-- These are pulled out as functions so that it's obvious that their use is
+-- unsafe (since Natural is unbounded).
+
+unsafeFinToInt :: Fin n -> Int
+unsafeFinToInt = fromIntegral . Fin.finToNat
+{-# INLINE unsafeFinToInt #-}
+
+unsafeNatReprToInt :: NatRepr n -> Int
+unsafeNatReprToInt = fromIntegral . NatRepr.natValue
+{-# INLINE unsafeNatReprToInt #-}
+
+------------------------------------------------------------------------
+-- Type
+
+-- This datatype has two important invariants:
+--
+-- * Its keys must be less than the nat in its type.
+-- * Its size must be less than the maximum Int.
+--
+-- If these invariants hold, all of the unsafe operations in this module
+-- (fromJust, unsafeCoerce) will work as intended.
+
+-- | @'FinMap' n a@ is a map with @'Fin' n@ keys and @a@ values.
+newtype FinMap (n :: Nat) a = FinMap { getFinMap :: IntMap a }
+
+instance Eq a => Eq (FinMap n a) where
+  fm1 == fm2 = getFinMap fm1 == getFinMap fm2
+  {-# INLINABLE (==) #-}
+
+instance Semigroup (FinMap n a) where
+  (<>) = union
+  {-# INLINE (<>) #-}
+
+instance KnownNat n => Monoid (FinMap n a) where
+  mempty = empty
+  {-# INLINE mempty #-}
+
+instance Functor (FinMap n) where
+  fmap f = FinMap . fmap f . getFinMap
+  {-# INLINABLE fmap #-}
+
+instance Foldable (FinMap n) where
+  foldMap f = foldMap f . getFinMap
+  {-# INLINABLE foldMap #-}
+
+instance Traversable (FinMap n) where
+  traverse f fm = FinMap <$> traverse f (getFinMap fm)
+
+instance FunctorWithIndex (Fin n) (FinMap n) where
+  imap f = FinMap . IntMap.mapWithKey (f . unsafeFin) . getFinMap
+  -- Inline so that RULES for IntMap.mapWithKey can fire
+  {-# INLINE imap #-}
+
+instance FoldableWithIndex (Fin n) (FinMap n) where
+  ifoldMap f = IntMap.foldMapWithKey (f . unsafeFin) . getFinMap
+
+-- | Non-lawful instance, provided for testing
+instance Show a => Show (FinMap n a) where
+  show fm = show (getFinMap fm)
+  {-# INLINABLE show #-}
+
+------------------------------------------------------------------------
+-- Query
+
+-- | /O(1)/. Is the map empty?
+null :: FinMap n a -> Bool
+null = IntMap.null . getFinMap
+{-# INLINABLE null #-}
+
+-- | /O(min(n,W))/. Fetch the value at the given key in the map.
+lookup :: Fin n -> FinMap n a -> Maybe a
+lookup k = IntMap.lookup (unsafeFinToInt k) . getFinMap
+{-# INLINABLE lookup #-}
+
+-- | Unsafely create a @'Fin' n@ from an 'Int' which is known to be less than
+-- @n@ for reasons not visible to the type system.
+unsafeFin :: forall n. Int -> Fin n
+unsafeFin i =
+  case NatRepr.mkNatRepr (intToNat i) of
+    Some (repr :: NatRepr m) ->
+      case unsafeCoerce (NatRepr.LeqProof :: LeqProof 0 0) :: LeqProof (m + 1) n of
+        NatRepr.LeqProof -> mkFin @m @n repr
+
+-- | /O(1)/. Number of elements in the map.
+size :: forall n a. FinMap n a -> Fin (n + 1)
+size = unsafeFin . IntMap.size . getFinMap
+{-# INLINEABLE size #-}
+
+------------------------------------------------------------------------
+-- Construction
+
+-- | /O(1)/. Increase maximum key/size by 1.
+--
+-- This does not alter the key-value pairs in the map, but rather increases the
+-- maximum number of key-value pairs that the map can hold. See
+-- "Data.Parameterized.FinMap" for more information.
+--
+-- Requires @n + 1 < (maxBound :: Int)@.
+incMax :: FinMap n a -> FinMap (n + 1) a
+incMax = FinMap . getFinMap
+{-# INLINE incMax #-}
+
+-- | /O(1)/. Increase maximum key/size.
+--
+-- Requires @m < (maxBound :: Int)@.
+embed :: (n <= m) => NatRepr m -> FinMap n a -> FinMap m a
+embed _ = FinMap . getFinMap
+{-# INLINE embed #-}
+
+-- | /O(1)/. The empty map.
+empty :: KnownNat n => FinMap n a
+empty = FinMap IntMap.empty
+{-# INLINE empty #-}
+
+-- | /O(1)/. A map with one element.
+singleton :: a -> FinMap 1 a
+singleton = FinMap . IntMap.singleton 0
+{-# INLINABLE singleton #-}
+
+-- | /O(min(n,W))/.
+insert :: Fin n -> a -> FinMap n a -> FinMap n a
+insert k v = FinMap . IntMap.insert (unsafeFinToInt k) v . getFinMap
+{-# INLINABLE insert #-}
+
+-- buildFinMap, append, and fromVector are duplicated exactly between the safe
+-- and unsafe modules because they are used in comparative testing (and so
+-- implementations must be available for both types).
+
+newtype FinMap' a (n :: Nat) = FinMap' { unFinMap' :: FinMap n a }
+
+buildFinMap ::
+  forall m a.
+  NatRepr m ->
+  (forall n. (n + 1 <= m) => NatRepr n -> FinMap n a -> FinMap (n + 1) a) ->
+  FinMap m a
+buildFinMap m f =
+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> FinMap' a k -> FinMap' a (k + 1)
+      f' = (\n (FinMap' fin) -> FinMap' (f n fin))
+  in unFinMap' (NatRepr.natRecStrictlyBounded m (FinMap' empty) f')
+
+-- | /O(min(n,W))/.
+append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
+append k v fm =
+  case NatRepr.leqSucc k of
+    NatRepr.LeqProof -> insert (mkFin k) v (incMax fm)
+
+fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
+fromVector v =
+  buildFinMap
+    (Vec.length v)
+    (\k m ->
+      case Vec.elemAt k v of
+        Just e -> append k e m
+        Nothing -> incMax m)
+
+------------------------------------------------------------------------
+-- Operations
+
+-- | /O(min(n,W))/.
+delete :: Fin n -> FinMap n a -> FinMap n a
+delete k = FinMap . IntMap.delete (unsafeFinToInt k) . getFinMap
+{-# INLINABLE delete #-}
+
+-- | Decrement the key/size, removing the item at key @n + 1@ if present.
+decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
+decMax k = FinMap . IntMap.delete (unsafeNatReprToInt k) . getFinMap
+{-# INLINABLE decMax #-}
+
+mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
+mapWithKey f = FinMap . IntMap.mapWithKey (f . unsafeFin) . getFinMap
+-- Inline so that RULES for IntMap.mapWithKey can fire
+{-# INLINE mapWithKey #-}
+
+-- | /O(n+m)/.
+unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
+unionWithKey f fm1 fm2 =
+  FinMap (IntMap.unionWithKey (f . unsafeFin) (getFinMap fm1) (getFinMap fm2))
+
+-- | /O(n+m)/.
+unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
+unionWith f = unionWithKey (\_ v1 v2 -> f v1 v2)
+
+-- | /O(n+m)/. Left-biased union, i.e. (@'union' == 'unionWith' 'const'@).
+union :: FinMap n a -> FinMap n a -> FinMap n a
+union = unionWith const
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
@@ -63,6 +63,7 @@
   , natRec
   , natRecStrong
   , natRecBounded
+  , natRecStrictlyBounded
   , natForEach
   , natFromZero
   , NatCases(..)
@@ -86,6 +87,7 @@
   , testLeq
   , testStrictLeq
   , leqRefl
+  , leqSucc
   , leqTrans
   , leqZero
   , leqAdd2
@@ -177,8 +179,6 @@
       -- 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 ->
@@ -187,7 +187,7 @@
           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))
+                             (leqTrans (leqSucc (Proxy :: Proxy x))
                                        (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)
           }}}}
       in leqPlus (predNat n)
@@ -423,6 +423,9 @@
 leqRefl :: forall f n . f n -> LeqProof n n
 leqRefl _ = LeqProof
 
+leqSucc :: forall f z. f z -> LeqProof z (z + 1)
+leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)
+
 -- | Apply transitivity to LeqProof
 leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
 leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
@@ -613,6 +616,28 @@
             }}
         Right f {- :: (m <= h) -> Void -} ->
           absurd $ f (LeqProof :: LeqProof m h)
+
+-- | A version of 'natRecBounded' which doesn't require the type index of the
+-- result to be greater than @0@ and provides a strict inequality constraint.
+natRecStrictlyBounded ::
+  forall m f.
+  NatRepr m ->
+  f 0 ->
+  (forall n. (n + 1 <= m) => NatRepr n -> f n -> f (n + 1)) ->
+  f m
+natRecStrictlyBounded m base indH =
+  case isZeroNat m of
+    ZeroNat -> base
+    NonZeroNat ->
+      case predNat m of
+        (p :: NatRepr p) ->
+          natRecBounded
+            p
+            p
+            base
+            (\(k :: NatRepr n) (v :: f n) ->
+              case leqAdd2 (LeqProof :: LeqProof n p) (LeqProof :: LeqProof 1 1) of
+                LeqProof -> indH k v)
 
 mulCancelR ::
   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
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
@@ -17,8 +17,10 @@
   , mapSome
   , traverseSome
   , traverseSome_
+  , someLens
   ) where
 
+import Control.Lens (Lens', lens, (&), (^.), (.~))
 import Data.Hashable
 import Data.Kind
 import Data.Parameterized.Classes
@@ -33,7 +35,7 @@
 instance OrdF f => Ord (Some f) where
   compare (Some x) (Some y) = toOrdering (compareF x y)
 
-instance HashableF f => Hashable (Some f) where
+instance (HashableF f, TestEquality f) => Hashable (Some f) where
   hashWithSalt s (Some x) = hashWithSaltF s x
   hash (Some x) = hashF x
 
@@ -64,3 +66,8 @@
 instance FunctorF     Some where fmapF     = mapSome
 instance FoldableF    Some where foldMapF  = foldMapFDefault
 instance TraversableF Some where traverseF = traverseSome
+
+-- | A lens that is polymorphic in the index may be used on a value with an
+-- existentially-quantified index.
+someLens :: (forall tp. Lens' (f tp) a) -> Lens' (Some f) a
+someLens l = lens (\(Some x) -> x ^. l) (\(Some x) v -> Some (x & l .~ v))
diff --git a/src/Data/Parameterized/Vector.hs b/src/Data/Parameterized/Vector.hs
--- a/src/Data/Parameterized/Vector.hs
+++ b/src/Data/Parameterized/Vector.hs
@@ -441,10 +441,7 @@
 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))
+leqLen v = 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
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -131,250 +132,327 @@
 
 type TestCtx = U.EmptyCtx '::> Int '::> String '::> Int '::> Bool
 
-
 ----------------------------------------------------------------------
+-- Hedgehog properties
 
-contextTests :: IO TestTree
-contextTests = testGroup "Context" <$> return
-   [ testProperty "size (unsafe)" $ property $
-     do vals <- forAll genSomePayloadList
-        Some a <- return $ mkUAsgn vals
-        length vals === U.sizeInt (U.size a)
-   , testProperty "size (safe)" $ property $
-     do vals <- forAll genSomePayloadList
-        Some a <- return $ mkSAsgn vals
-        length vals === S.sizeInt (S.size a)
+prop_sizeUnsafe :: Property
+prop_sizeUnsafe = property $
+  do vals <- forAll genSomePayloadList
+     Some a <- return $ mkUAsgn vals
+     length vals === U.sizeInt (U.size a)
 
-   , testProperty "safe_index_eq" $ property $
+prop_sizeSafe :: Property
+prop_sizeSafe = property $
+  do vals <- forAll genSomePayloadList
+     Some a <- return $ mkSAsgn vals
+     length vals === S.sizeInt (S.size a)
+
+prop_safeIndexEq :: Property
+prop_safeIndexEq = property $
      do vals <- forAll genSomePayloadList
         i' <- forAll $ HG.int (linear 0 $ length vals - 1)
         Some a <- return $ mkSAsgn vals
         Just (Some idx) <- return $ S.intIndex i' (S.size a)
         Some (a S.! idx) === vals !! i'
 
-   , testProperty "unsafe_index_eq" $ property $
-     do vals <- forAll genSomePayloadList
-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
-        Some a <- return $ mkUAsgn vals
-        Just (Some idx) <- return $ U.intIndex i' (U.size a)
-        Some (a U.! idx) === vals !! i'
+prop_unsafeIndexEq :: Property
+prop_unsafeIndexEq = property $
+  do vals <- forAll genSomePayloadList
+     i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+     Some a <- return $ mkUAsgn vals
+     Just (Some idx) <- return $ U.intIndex i' (U.size a)
+     Some (a U.! idx) === vals !! i'
 
-   , testProperty "safe_tolist" $ property $
-     do vals <- forAll genSomePayloadList
-        Some a <- return $ mkSAsgn vals
-        let vals' = toListFC Some a
-        vals === vals'
-   , testProperty "unsafe_tolist" $ property $
-     do vals <- forAll genSomePayloadList
-        Some a <- return $ mkUAsgn vals
-        let vals' = toListFC Some a
-        vals === vals'
+prop_safeToList :: Property
+prop_safeToList = property $
+  do vals <- forAll genSomePayloadList
+     Some a <- return $ mkSAsgn vals
+     let vals' = toListFC Some a
+     vals === vals'
 
-   , testProperty "adjust test monadic" $ property $
-     do vals <- forAll genSomePayloadList
-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+prop_unsafeToList :: Property
+prop_unsafeToList = property $
+  do vals <- forAll genSomePayloadList
+     Some a <- return $ mkUAsgn vals
+     let vals' = toListFC Some a
+     vals === vals'
 
-        Some x <- return $ mkUAsgn vals
-        Some y <- return $ mkSAsgn vals
+prop_adjustTestMonadic :: Property
+prop_adjustTestMonadic = property $
+  do vals <- forAll genSomePayloadList
+     i' <- forAll $ HG.int (linear 0 $ length vals - 1)
 
-        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+     Some x <- return $ mkUAsgn vals
+     Some y <- return $ mkSAsgn vals
 
-        x' <- U.adjustM (return . twiddle) idx_x x
-        y' <- S.adjustM (return . twiddle) idx_y y
+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-        toListFC Some x' === toListFC Some y'
+     x' <- U.adjustM (return . twiddle) idx_x x
+     y' <- S.adjustM (return . twiddle) idx_y y
 
-   , testProperty "adjust test" $ property $
-     do vals <- forAll genSomePayloadList
-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+     toListFC Some x' === toListFC Some y'
 
-        Some x <- return $ mkUAsgn vals
-        Some y <- return $ mkSAsgn vals
+prop_adjustTest :: Property
+prop_adjustTest = property $
+  do vals <- forAll genSomePayloadList
+     i' <- forAll $ HG.int (linear 0 $ length vals - 1)
 
-        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+     Some x <- return $ mkUAsgn vals
+     Some y <- return $ mkSAsgn vals
 
-        let x' = x & ixF idx_x %~ twiddle
-            y' = y & ixF idx_y %~ twiddle
+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-        toListFC Some x' === toListFC Some y'
-        -- adjust actually modified the entry
-        toListFC Some x /== toListFC Some x'
-        toListFC Some y /== toListFC Some y'
+     let x' = x & ixF idx_x %~ twiddle
+         y' = y & ixF idx_y %~ twiddle
 
-   , testProperty "update test" $ property $
-     do vals <- forAll genSomePayloadList
-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)
+     toListFC Some x' === toListFC Some y'
+     -- adjust actually modified the entry
+     toListFC Some x /== toListFC Some x'
+     toListFC Some y /== toListFC Some y'
 
-        Some x <- return $ mkUAsgn vals
-        Some y <- return $ mkSAsgn vals
+prop_updateTest :: Property
+prop_updateTest = property $
+  do vals <- forAll genSomePayloadList
+     i' <- forAll $ HG.int (linear 0 $ length vals - 1)
 
-        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+     Some x <- return $ mkUAsgn vals
+     Some y <- return $ mkSAsgn vals
 
-        let x' = over (ixF idx_x) twiddle x
-            y' = (ixF idx_y) %~ twiddle $ y
-            updX = x & ixF idx_x .~ x' U.! idx_x
-            updY = y & ixF idx_y .~ y' S.! idx_y
+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-        toListFC Some updX === toListFC Some updY
-        -- update actually modified the entry
-        toListFC Some x /== toListFC Some updX
-        toListFC Some y /== toListFC Some updY
-        -- update modified the expected entry
-        toListFC Some x' === toListFC Some updX
-        toListFC Some y' === toListFC Some updY
+     let x' = over (ixF idx_x) twiddle x
+         y' = (ixF idx_y) %~ twiddle $ y
+         updX = x & ixF idx_x .~ x' U.! idx_x
+         updY = y & ixF idx_y .~ y' S.! idx_y
 
-   , testProperty "safe_eq" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        Some x <- return $ mkSAsgn vals1
-        Some y <- return $ mkSAsgn vals2
-        case testEquality x y of
-          Just Refl -> vals1 === vals2
-          Nothing   -> vals1 /== vals2
-   , testProperty "unsafe_eq" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        Some x <- return $ mkUAsgn vals1
-        Some y <- return $ mkUAsgn vals2
-        case testEquality x y of
-          Just Refl -> vals1 === vals2
-          Nothing   -> vals1 /== vals2
+     toListFC Some updX === toListFC Some updY
+     -- update actually modified the entry
+     toListFC Some x /== toListFC Some updX
+     toListFC Some y /== toListFC Some updY
+     -- update modified the expected entry
+     toListFC Some x' === toListFC Some updX
+     toListFC Some y' === toListFC Some updY
 
-   , testProperty "take none" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        vals3 <- forAll genSomePayloadList
-        Some w <- return $ mkUAsgn vals1
-        Some x <- return $ mkUAsgn vals2
-        Some y <- return $ mkUAsgn vals3
-        let z = w U.<++> x U.<++> y
-        case P.leftId z of
-          Refl -> let r = C.take U.zeroSize (U.size z) z in
-                    assert $ isJust $ testEquality U.empty r
-   , testProperty "drop none" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        vals3 <- forAll genSomePayloadList
-        Some w <- return $ mkUAsgn vals1
-        Some x <- return $ mkUAsgn vals2
-        Some y <- return $ mkUAsgn vals3
-        let z = w U.<++> x U.<++> y
-        case P.leftId z of
-          Refl -> let r = C.drop U.zeroSize (U.size z) z in
-                    assert $ isJust $ testEquality z r
+prop_safeEq :: Property
+prop_safeEq = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     Some x <- return $ mkSAsgn vals1
+     Some y <- return $ mkSAsgn vals2
+     case testEquality x y of
+       Just Refl -> vals1 === vals2
+       Nothing   -> vals1 /== vals2
 
-   , testProperty "take all" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        vals3 <- forAll genSomePayloadList
-        Some w <- return $ mkUAsgn vals1
-        Some x <- return $ mkUAsgn vals2
-        Some y <- return $ mkUAsgn vals3
-        let z = w U.<++> x U.<++> y
-        let r = C.take (U.size z) U.zeroSize z
-        assert $ isJust $ testEquality z r
-   , testProperty "drop all" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        vals3 <- forAll genSomePayloadList
-        Some w <- return $ mkUAsgn vals1
-        Some x <- return $ mkUAsgn vals2
-        Some y <- return $ mkUAsgn vals3
-        let z = w U.<++> x U.<++> y
-        let r = C.drop (U.size z) U.zeroSize z
-        assert $ isJust $ testEquality U.empty r
+prop_unsafeEq :: Property
+prop_unsafeEq = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     Some x <- return $ mkUAsgn vals1
+     Some y <- return $ mkUAsgn vals2
+     case testEquality x y of
+       Just Refl -> vals1 === vals2
+       Nothing   -> vals1 /== vals2
 
-   , testProperty "append_take" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        Some x <- return $ mkUAsgn vals1
-        Some y <- return $ mkUAsgn vals2
-        let z = x U.<++> y
-        let x' = C.take (U.size x) (U.size y) z
-        assert $ isJust $ testEquality x x'
+prop_takeNone :: Property
+prop_takeNone = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     vals3 <- forAll genSomePayloadList
+     Some w <- return $ mkUAsgn vals1
+     Some x <- return $ mkUAsgn vals2
+     Some y <- return $ mkUAsgn vals3
+     let z = w U.<++> x U.<++> y
+     case P.leftId z of
+       Refl -> let r = C.take U.zeroSize (U.size z) z in
+                 assert $ isJust $ testEquality U.empty r
 
-   , testProperty "append_take_drop" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        Some x <- return $ mkUAsgn vals1
-        Some y <- return $ mkUAsgn vals2
-        let z = x U.<++> y
-        let x' = C.take (U.size x) (U.size y) z
-        let y' = C.drop (U.size x) (U.size y) z
-        assert $ isJust $ testEquality x x'
-        assert $ isJust $ testEquality y y'
+prop_dropNone :: Property
+prop_dropNone = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     vals3 <- forAll genSomePayloadList
+     Some w <- return $ mkUAsgn vals1
+     Some x <- return $ mkUAsgn vals2
+     Some y <- return $ mkUAsgn vals3
+     let z = w U.<++> x U.<++> y
+     case P.leftId z of
+       Refl -> let r = C.drop U.zeroSize (U.size z) z in
+                 assert $ isJust $ testEquality z r
 
-   , testProperty "append_take_drop_multiple" $ property $
-     do vals1 <- forAll genSomePayloadList
-        vals2 <- forAll genSomePayloadList
-        vals3 <- forAll genSomePayloadList
-        vals4 <- forAll genSomePayloadList
-        vals5 <- forAll genSomePayloadList
-        Some u <- return $ mkUAsgn vals1
-        Some v <- return $ mkUAsgn vals2
-        Some w <- return $ mkUAsgn vals3
-        Some x <- return $ mkUAsgn vals4
-        Some y <- return $ mkUAsgn vals5
-        let uv = u U.<++> v
-        let wxy = w U.<++> x U.<++> y
-        -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y
-        let z = uv U.<++> wxy
-        let uv' = C.take (U.size uv) (U.size wxy) z
-        let wxy' = C.drop (U.size uv) (U.size wxy) z
-        let withWXY = C.dropPrefix z uv (error "failed dropPrefix")
-        assert $ isJust $ testEquality (u U.<++> v) uv'
-        assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'
-        assert $ isJust $ testEquality uv uv'
-        assert $ isJust $ testEquality wxy wxy'
-        withWXY $ \t -> assert $ isJust $ testEquality wxy' t
+prop_takeAll :: Property
+prop_takeAll = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     vals3 <- forAll genSomePayloadList
+     Some w <- return $ mkUAsgn vals1
+     Some x <- return $ mkUAsgn vals2
+     Some y <- return $ mkUAsgn vals3
+     let z = w U.<++> x U.<++> y
+     let r = C.take (U.size z) U.zeroSize z
+     assert $ isJust $ testEquality z r
 
-   , testProperty "zip/unzip" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        let zipped = C.zipWith Pair x x
-        let (x', x'') = C.unzip zipped
-        assert $ isJust $ testEquality x x'
-        assert $ isJust $ testEquality x x''
+prop_dropAll :: Property
+prop_dropAll = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     vals3 <- forAll genSomePayloadList
+     Some w <- return $ mkUAsgn vals1
+     Some x <- return $ mkUAsgn vals2
+     Some y <- return $ mkUAsgn vals3
+     let z = w U.<++> x U.<++> y
+     let r = C.drop (U.size z) U.zeroSize z
+     assert $ isJust $ testEquality U.empty r
 
-   , testProperty "fmapFC_identity" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        assert $ isJust $ testEquality x (fmapFC id x)
+prop_appendTake :: Property
+prop_appendTake = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     Some x <- return $ mkUAsgn vals1
+     Some y <- return $ mkUAsgn vals2
+     let z = x U.<++> y
+     let x' = C.take (U.size x) (U.size y) z
+     assert $ isJust $ testEquality x x'
 
-   , testProperty "fmapFC_assoc" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        Fun f <- forAll $ HG.element funs
-        Fun g <- forAll $ HG.element funs
-        assert $ isJust $ testEquality
-                            (fmapFC g (fmapFC f x))
-                            (fmapFC (g . f) x)
+prop_appendTakeDrop :: Property
+prop_appendTakeDrop = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     Some x <- return $ mkUAsgn vals1
+     Some y <- return $ mkUAsgn vals2
+     let z = x U.<++> y
+     let x' = C.take (U.size x) (U.size y) z
+     let y' = C.drop (U.size x) (U.size y) z
+     assert $ isJust $ testEquality x x'
+     assert $ isJust $ testEquality y y'
 
-   , testProperty "imapFC_index_noop" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        assert $
-          isJust $
-            testEquality x (imapFC (\idx _ -> x U.! idx) x)
+prop_appendTakeDropMultiple :: Property
+prop_appendTakeDropMultiple = property $
+  do vals1 <- forAll genSomePayloadList
+     vals2 <- forAll genSomePayloadList
+     vals3 <- forAll genSomePayloadList
+     vals4 <- forAll genSomePayloadList
+     vals5 <- forAll genSomePayloadList
+     Some u <- return $ mkUAsgn vals1
+     Some v <- return $ mkUAsgn vals2
+     Some w <- return $ mkUAsgn vals3
+     Some x <- return $ mkUAsgn vals4
+     Some y <- return $ mkUAsgn vals5
+     let uv = u U.<++> v
+     let wxy = w U.<++> x U.<++> y
+     -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y
+     let z = uv U.<++> wxy
+     let uv' = C.take (U.size uv) (U.size wxy) z
+     let wxy' = C.drop (U.size uv) (U.size wxy) z
+     let withWXY = C.dropPrefix z uv (error "failed dropPrefix")
+     assert $ isJust $ testEquality (u U.<++> v) uv'
+     assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'
+     assert $ isJust $ testEquality uv uv'
+     assert $ isJust $ testEquality wxy wxy'
+     withWXY $ \t -> assert $ isJust $ testEquality wxy' t
 
-   , testProperty "imapFC/fmapFC" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        Fun f <- forAll $ HG.element funs
-        assert $ isJust $ testEquality
-                            (fmapFC f x)
-                            (imapFC (const f) x)
+prop_zipUnzip :: Property
+prop_zipUnzip = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     let zipped = C.zipWith Pair x x
+     let (x', x'') = C.unzip zipped
+     assert $ isJust $ testEquality x x'
+     assert $ isJust $ testEquality x x''
 
-   , testProperty "ifoldMapFC/foldMapFC" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        assert $ foldMapFC show x == ifoldMapFC (const show) x
+prop_fmapFCIdentity :: Property
+prop_fmapFCIdentity = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     assert $ isJust $ testEquality x (fmapFC id x)
 
-   , testProperty "itraverseFC/traverseFC" $ property $
-     do Some x <- mkUAsgn <$> forAll genSomePayloadList
-        Fun f <- forAll $ HG.element funs
-        let f' :: forall a. Payload a -> Identity (Payload a)
-            f' = Identity . f
-        assert $ isJust $ testEquality
-                            (runIdentity (traverseFC f' x))
-                            (runIdentity (itraverseFC (const f') x))
+prop_fmapFCAssoc :: Property
+prop_fmapFCAssoc = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     Fun f <- forAll $ HG.element funs
+     Fun g <- forAll $ HG.element funs
+     assert $ isJust $ testEquality
+                         (fmapFC g (fmapFC f x))
+                         (fmapFC (g . f) x)
+
+prop_imapFCIndexNoop :: Property
+prop_imapFCIndexNoop = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     assert $
+       isJust $
+         testEquality x (imapFC (\idx _ -> x U.! idx) x)
+
+prop_imapFCFmapFC :: Property
+prop_imapFCFmapFC = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     Fun f <- forAll $ HG.element funs
+     assert $ isJust $ testEquality
+                         (fmapFC f x)
+                         (imapFC (const f) x)
+
+prop_ifoldMapFCFoldMapFC :: Property
+prop_ifoldMapFCFoldMapFC = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     assert $ foldMapFC show x == ifoldMapFC (const show) x
+
+prop_itraverseFCTraverseFC :: Property
+prop_itraverseFCTraverseFC = property $
+  do Some x <- mkUAsgn <$> forAll genSomePayloadList
+     Fun f <- forAll $ HG.element funs
+     let f' :: forall a. Payload a -> Identity (Payload a)
+         f' = Identity . f
+     assert $ isJust $ testEquality
+                         (runIdentity (traverseFC f' x))
+                         (runIdentity (itraverseFC (const f') x))
+
+----------------------------------------------------------------------
+
+contextTests :: IO TestTree
+contextTests = testGroup "Context" <$> return
+   [ testPropertyNamed "size (unsafe)" "prop_sizeUnsafe" prop_sizeUnsafe
+   , testPropertyNamed "size (safe)" "prop_sizeSafe" prop_sizeSafe
+
+   , testPropertyNamed "safe_index_eq" "prop_safeIndexEq" prop_safeIndexEq
+
+   , testPropertyNamed "unsafe_index_eq" "prop_unsafeIndexEq" prop_unsafeIndexEq
+
+   , testPropertyNamed "safe_tolist" "prop_safeToList" prop_safeToList
+   , testPropertyNamed "unsafe_tolist" "prop_unsafeToList" prop_unsafeToList
+
+   , testPropertyNamed "adjust test monadic" "prop_adjustTestMonadic" prop_adjustTestMonadic
+
+   , testPropertyNamed "adjust test" "prop_adjustTest" prop_adjustTest
+
+   , testPropertyNamed "update test" "prop_updateTest" prop_updateTest
+
+   , testPropertyNamed "safe_eq" "prop_safeEq" prop_safeEq
+   , testPropertyNamed "unsafe_eq" "prop_unsafeEq" prop_unsafeEq
+
+   , testPropertyNamed "take none" "prop_takeNone" prop_takeNone
+   , testPropertyNamed "drop none" "prop_dropNone" prop_dropNone
+
+   , testPropertyNamed "take all" "prop_takeAll" prop_takeAll
+   , testPropertyNamed "drop all" "prop_dropAll" prop_dropAll
+
+   , testPropertyNamed "append_take" "prop_appendTake" prop_appendTake
+
+   , testPropertyNamed "append_take_drop" "prop_appendTakeDrop" prop_appendTakeDrop
+
+   , testPropertyNamed "append_take_drop_multiple" "prop_appendTakeDropMultiple" prop_appendTakeDropMultiple
+
+   , testPropertyNamed "zip/unzip" "prop_zipUnzip" prop_zipUnzip
+
+   , testPropertyNamed "fmapFC_identity" "prop_fmapFCIdentity" prop_fmapFCIdentity
+
+   , testPropertyNamed "fmapFC_assoc" "prop_fmapFCAssoc" prop_fmapFCAssoc
+
+   , testPropertyNamed "imapFC_index_noop" "prop_imapFCIndexNoop" prop_imapFCIndexNoop
+
+   , testPropertyNamed "imapFC/fmapFC" "prop_imapFCFmapFC" prop_imapFCFmapFC
+
+   , testPropertyNamed "ifoldMapFC/foldMapFC" "prop_ifoldMapFCFoldMapFC" prop_ifoldMapFCFoldMapFC
+
+   , testPropertyNamed "itraverseFC/traverseFC" "prop_itraverseFCTraverseFC" prop_itraverseFCTraverseFC
 
    , testCaseSteps "explicit indexing (unsafe)" $ \step -> do
        let mkUPayload :: U.Assignment Payload TestCtx
diff --git a/test/Test/Fin.hs b/test/Test/Fin.hs
--- a/test/Test/Fin.hs
+++ b/test/Test/Fin.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# Language CPP #-}
@@ -16,6 +17,7 @@
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range (linear)
 import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.Hedgehog (testPropertyNamed)
 import           Test.Tasty.HUnit (assertBool, testCase)
 
 import           Data.Parameterized.NatRepr
@@ -26,15 +28,29 @@
 import qualified Hedgehog.Classes as HC
 #endif
 
-genFin :: (0 <= n, Monad m) => NatRepr n -> GenT m (Fin n)
+genNatRepr :: (Monad m) => Natural -> GenT m (Some NatRepr)
+genNatRepr bound =
+  do x0 <- HG.integral (linear 0 bound)
+     return (mkNatRepr x0)
+
+genFin :: (1 <= n, Monad m) => NatRepr n -> GenT m (Fin n)
 genFin n =
-  do x0 <- HG.integral (linear 0 ((natValue n) - 1 :: Natural))
-     Some x <- return (mkNatRepr x0)
+  do Some x <- genNatRepr (natValue n - 1 :: Natural)
      return $
        case testLeq (incNat x) n of
          Just LeqProof -> mkFin x
          Nothing -> error "Impossible"
 
+prop_count_true :: Property
+prop_count_true = property $
+  do Some n <- forAll (genNatRepr 100)
+     finToNat (countFin n (\_ _ -> True)) === natValue n
+
+prop_count_false :: Property
+prop_count_false = property $
+  do Some n <- forAll (genNatRepr 100)
+     finToNat (countFin n (\_ _ -> False)) === 0
+
 finTests :: IO TestTree
 finTests =
   testGroup "Fin" <$>
@@ -47,6 +63,9 @@
           assertBool
             "minBound <= maxBound (2)"
             ((minBound :: Fin 2) <= (minBound :: Fin 2))
+
+      , testPropertyNamed "count-true" "prop_count_true" prop_count_true
+      , testPropertyNamed "count-false" "prop_count_false" prop_count_false
 
 #if __GLASGOW_HASKELL__ >= 806
       , testCase "Eq-Fin-laws-1" $
diff --git a/test/Test/FinMap.hs b/test/Test/FinMap.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FinMap.hs
@@ -0,0 +1,393 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+
+module Test.FinMap (finMapTests) where
+
+import           Control.Monad (foldM)
+import           Data.Foldable.WithIndex (itoList)
+import           Data.Functor.WithIndex (FunctorWithIndex(imap))
+import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
+import           Data.Proxy (Proxy(Proxy))
+import           Data.Type.Equality ((:~:)(Refl))
+
+import           Data.Parameterized.Fin (Fin)
+import qualified Data.Parameterized.Fin as Fin
+import           Data.Parameterized.NatRepr (LeqProof, NatRepr, type (<=), type (+))
+import qualified Data.Parameterized.NatRepr as NatRepr
+
+import           Hedgehog
+import qualified Hedgehog.Gen as HG
+import           Hedgehog.Range (linear)
+import           Test.Tasty
+import           Test.Tasty.Hedgehog
+
+#if __GLASGOW_HASKELL__ >= 806
+import           Test.Tasty.HUnit (assertBool, testCase)
+import qualified Hedgehog.Classes as HC
+#endif
+
+import qualified Data.Parameterized.FinMap.Safe as S
+import qualified Data.Parameterized.FinMap.Unsafe as U
+import qualified Data.Parameterized.Vector as Vec
+
+import           Test.Fin (genFin)
+import           Test.Vector (SomeVector(..), genSomeVector, genVectorOfLength, genOrdering, orderingEndomorphisms, orderingToStringFuns)
+
+data SomeSafeFinMap a = forall n. SomeSafeFinMap (NatRepr n) (S.FinMap n a)
+data SomeUnsafeFinMap a = forall n. SomeUnsafeFinMap (NatRepr n) (U.FinMap n a)
+
+instance Show a => Show (SomeSafeFinMap a) where
+  show (SomeSafeFinMap _ v) = show v
+instance Show a => Show (SomeUnsafeFinMap a) where
+  show (SomeUnsafeFinMap _ v) = show v
+
+genSafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (S.FinMap (n + 1) a)
+genSafeFinMap n genElem = S.fromVector <$> genVectorOfLength n (HG.maybe genElem)
+
+genUnsafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (U.FinMap (n + 1) a)
+genUnsafeFinMap n genElem = U.fromVector <$> genVectorOfLength n (HG.maybe genElem)
+
+genSomeSafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeSafeFinMap a)
+genSomeSafeFinMap genElem =
+  do SomeVector v <- genSomeVector (HG.maybe genElem)
+     return (SomeSafeFinMap (Vec.length v) (S.fromVector v))
+
+genSomeUnsafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeUnsafeFinMap a)
+genSomeUnsafeFinMap genElem =
+  do SomeVector v <- genSomeVector (HG.maybe genElem)
+     return (SomeUnsafeFinMap (Vec.length v) (U.fromVector v))
+
+prop_incMax_size_safe :: Property
+prop_incMax_size_safe = property $
+  do SomeSafeFinMap _ fm <- forAll $ genSomeSafeFinMap genOrdering
+     Fin.finToNat (S.size (S.incMax fm)) === Fin.finToNat (S.size fm)
+
+prop_incMax_size_unsafe :: Property
+prop_incMax_size_unsafe = property $
+  do SomeUnsafeFinMap _ fm <- forAll $ genSomeUnsafeFinMap genOrdering
+     Fin.finToNat (U.size (U.incMax fm)) === Fin.finToNat (U.size fm)
+
+prop_imap_const_safe :: Property
+prop_imap_const_safe = property $
+  do f <- forAll (HG.element orderingEndomorphisms)
+     SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)
+     imap (const f) fm === fmap f fm
+
+prop_imap_const_unsafe :: Property
+prop_imap_const_unsafe = property $
+  do f <- forAll (HG.element orderingEndomorphisms)
+     SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)
+     imap (const f) fm === fmap f fm
+
+prop_ifoldMap_const_safe :: Property
+prop_ifoldMap_const_safe = property $
+  do f <- forAll (HG.element orderingToStringFuns)
+     SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)
+     ifoldMap (const f) fm === foldMap f fm
+
+prop_ifoldMap_const_unsafe :: Property
+prop_ifoldMap_const_unsafe = property $
+  do f <- forAll (HG.element orderingToStringFuns)
+     SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)
+     ifoldMap (const f) fm === foldMap f fm
+
+cancelPlusOne ::
+  forall f g i n.
+  f i ->
+  g n ->
+  LeqProof (i + 1) (n + 1) ->
+  LeqProof i n
+cancelPlusOne i n NatRepr.LeqProof =
+  case NatRepr.plusMinusCancel n (NatRepr.knownNat :: NatRepr 1) of
+    Refl ->
+      case NatRepr.plusMinusCancel i (NatRepr.knownNat :: NatRepr 1) of
+        Refl ->
+          case NatRepr.leqSub2
+                  (NatRepr.LeqProof :: LeqProof (i + 1) (n + 1))
+                  (NatRepr.LeqProof :: LeqProof 1 1) of
+            NatRepr.LeqProof -> NatRepr.LeqProof
+
+withIndexSafe ::
+  SomeSafeFinMap a ->
+  (forall n. Fin n -> S.FinMap n a -> PropertyT IO ()) ->
+  PropertyT IO ()
+withIndexSafe (SomeSafeFinMap n fm) k =
+  case NatRepr.isZeroOrGT1 n of
+    Left Refl -> k Fin.minFin (S.incMax fm)
+    Right NatRepr.LeqProof ->
+      do idx <- forAll (genFin n)
+         k idx fm
+
+withIndexUnsafe ::
+  SomeUnsafeFinMap a ->
+  (forall n. Fin n -> U.FinMap n a -> PropertyT IO ()) ->
+  PropertyT IO ()
+withIndexUnsafe (SomeUnsafeFinMap n fm) k =
+  case NatRepr.isZeroOrGT1 n of
+    Left Refl -> k Fin.minFin (U.incMax fm)
+    Right NatRepr.LeqProof ->
+      do idx <- forAll (genFin n)
+         k idx fm
+
+withSizeUnsafe ::
+  U.FinMap n a ->
+  (forall i. (i + 1 <= n + 1, i <= n) => NatRepr i -> r) ->
+  r
+withSizeUnsafe fm k =
+  case U.size fm of
+    (sz :: Fin (n + 1)) ->
+      Fin.viewFin
+        (\(i :: NatRepr i) ->
+          case cancelPlusOne i (Proxy :: Proxy n) NatRepr.LeqProof of
+            NatRepr.LeqProof -> k i)
+        sz
+
+prop_insert_size_safe :: Property
+prop_insert_size_safe = property $
+  do sfm <- forAll $ genSomeSafeFinMap genOrdering
+     withIndexSafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      let size = Fin.finToNat (S.size fm)
+      let newSize = Fin.finToNat (S.size (S.insert (Fin.embed idx) o fm))
+      assert (size == newSize || size + 1 == newSize)
+
+prop_insert_size_unsafe :: Property
+prop_insert_size_unsafe = property $
+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
+     withIndexUnsafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      let size = Fin.finToNat (U.size fm)
+      let newSize = Fin.finToNat (U.size (U.insert (Fin.embed idx) o fm))
+      assert (size == newSize || size + 1 == newSize)
+
+prop_insert_delete_safe :: Property
+prop_insert_delete_safe = property $
+  do sfm <- forAll $ genSomeSafeFinMap genOrdering
+     withIndexSafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      S.delete idx (S.insert idx o fm) === S.delete idx fm
+
+prop_insert_delete_unsafe :: Property
+prop_insert_delete_unsafe = property $
+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
+     withIndexUnsafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      U.delete idx (U.insert idx o fm) === U.delete idx fm
+
+prop_delete_insert_safe :: Property
+prop_delete_insert_safe = property $
+  do sfm <- forAll $ genSomeSafeFinMap genOrdering
+     withIndexSafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      S.insert idx o (S.delete idx fm) === S.insert idx o fm
+
+prop_delete_insert_unsafe :: Property
+prop_delete_insert_unsafe = property $
+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
+     withIndexUnsafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      U.insert idx o (U.delete idx fm) === U.insert idx o fm
+
+prop_empty_insert_safe :: Property
+prop_empty_insert_safe = property $
+  do withIndexSafe (SomeSafeFinMap (NatRepr.knownNat @0) S.empty) $ \idx fm -> do
+      o <- forAll genOrdering
+      fm /== S.insert idx o fm
+
+prop_empty_insert_unsafe :: Property
+prop_empty_insert_unsafe = property $
+  do withIndexUnsafe (SomeUnsafeFinMap (NatRepr.knownNat @0) U.empty) $ \idx fm -> do
+      o <- forAll genOrdering
+      fm /== U.insert idx o fm
+
+prop_insert_insert_safe :: Property
+prop_insert_insert_safe = property $
+  do sfm <- forAll $ genSomeSafeFinMap genOrdering
+     withIndexSafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      S.insert idx o (S.insert idx o fm) === S.insert idx o fm
+
+prop_insert_insert_unsafe :: Property
+prop_insert_insert_unsafe = property $
+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
+     withIndexUnsafe sfm $ \idx fm -> do
+      o <- forAll genOrdering
+      U.insert idx o (U.insert idx o fm) === U.insert idx o fm
+
+prop_delete_delete_safe :: Property
+prop_delete_delete_safe = property $
+  do sfm <- forAll $ genSomeSafeFinMap genOrdering
+     withIndexSafe sfm $ \idx fm -> do
+      S.delete idx (S.delete idx fm) === S.delete idx fm
+
+prop_delete_delete_unsafe :: Property
+prop_delete_delete_unsafe = property $
+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
+     withIndexUnsafe sfm $ \idx fm -> do
+      U.delete idx (U.delete idx fm) === U.delete idx fm
+
+-- | Type used for comparative API tests
+data MatchedMaps a =
+  forall n.
+  MatchedMaps
+    { _unsafe :: U.FinMap n a
+    , _safe :: S.FinMap n a
+    }
+
+operations ::
+  Show a =>
+  Gen a ->
+  -- | For testing 'fmap'.
+  [a -> a] ->
+  [MatchedMaps a -> PropertyT IO (MatchedMaps a)]
+operations genValue valEndomorphisms =
+  [ \(MatchedMaps u s) ->
+      withSizeUnsafe u $ \sz -> do
+        case NatRepr.isZeroOrGT1 sz of
+          Left Refl ->
+            do v <- forAll genValue
+               return $
+                 MatchedMaps
+                   (U.insert Fin.minFin v (U.incMax u))
+                   (S.insert Fin.minFin v (S.incMax s))
+          Right NatRepr.LeqProof ->
+            do idx <- Fin.embed <$> forAll (genFin sz)
+               v <- forAll genValue
+               return (MatchedMaps (U.insert idx v u) (S.insert idx v s))
+  , \(MatchedMaps u s) ->
+      withSizeUnsafe u $ \sz -> do
+        case NatRepr.isZeroOrGT1 sz of
+          Left Refl -> return (MatchedMaps u s)
+          Right NatRepr.LeqProof ->
+            do idx <- Fin.embed <$> forAll (genFin sz)
+               return (MatchedMaps (U.delete idx u) (S.delete idx s))
+  , \(MatchedMaps u s) ->
+        return (MatchedMaps (U.incMax u) (S.incMax s))
+  , \(MatchedMaps u s) ->
+      do f <- forAll (HG.element (id:valEndomorphisms))
+         return (MatchedMaps (fmap f u) (fmap f s))
+  , \(MatchedMaps u s) ->
+      do f <- forAll (HG.element (id:valEndomorphisms))
+         return (MatchedMaps (imap (const f) u) (imap (const f) s))
+  , \(MatchedMaps _ _) ->
+      do v <- forAll genValue
+         return (MatchedMaps (U.singleton v) (S.singleton v))
+  , \(MatchedMaps _ _) ->
+      return (MatchedMaps (U.empty @0) S.empty)
+  , \(MatchedMaps _ _) ->
+      return (MatchedMaps (U.empty @8) S.empty)
+  ]
+
+-- | Possibly the most important and far-reaching test: The unsafe API should
+-- yield the same results as the safe API, after some randomized sequence of
+-- operations.
+prop_safe_unsafe :: Property
+prop_safe_unsafe = property $
+  do numOps <- forAll (HG.integral (linear 0 (99 :: Int)))
+     let empty = MatchedMaps (U.empty @0) S.empty
+     MatchedMaps u s <-
+       doTimes (chooseAndApply orderingOps) numOps empty
+     itoList u === itoList s
+  where
+    orderingOps = operations genOrdering orderingEndomorphisms
+
+    chooseAndApply :: [a -> PropertyT IO b] -> a -> PropertyT IO b
+    chooseAndApply funs arg =
+      do f <- forAll (HG.element funs)
+         f arg
+
+    doTimes f n m = foldM (\accum () -> f accum) m (replicate n ())
+
+
+finMapTests :: IO TestTree
+finMapTests = testGroup "FinMap" <$> return
+  [ testPropertyNamed "incSize-decSize-safe" "prop_incMax_size_safe" prop_incMax_size_safe
+  , testPropertyNamed "incSize-decSize-unsafe" "prop_incMax_size_unsafe" prop_incMax_size_unsafe
+  , testPropertyNamed "insert-size-safe" "prop_insert_size_safe" prop_insert_size_safe
+  , testPropertyNamed "insert-size-unsafe" "prop_insert_size_unsafe" prop_insert_size_unsafe
+  , testPropertyNamed "insert-delete-safe" "prop_insert_delete_safe" prop_insert_delete_safe
+  , testPropertyNamed "insert-delete-unsafe" "prop_insert_delete_unsafe" prop_insert_delete_unsafe
+  , testPropertyNamed "delete-insert-safe" "prop_delete_insert_safe" prop_delete_insert_safe
+  , testPropertyNamed "delete-insert-unsafe" "prop_delete_insert_unsafe" prop_delete_insert_unsafe
+  , testPropertyNamed "empty-insert-safe" "prop_empty_insert_safe" prop_empty_insert_safe
+  , testPropertyNamed "empty-insert-unsafe" "prop_empty_insert_unsafe" prop_empty_insert_unsafe
+  , testPropertyNamed "insert-insert-safe" "prop_insert_insert_safe" prop_insert_insert_safe
+  , testPropertyNamed "insert-insert-unsafe" "prop_insert_insert_unsafe" prop_insert_insert_unsafe
+  , testPropertyNamed "delete-delete-safe" "prop_delete_delete_safe" prop_delete_delete_safe
+  , testPropertyNamed "delete-delete-unsafe" "prop_delete_delete_unsafe" prop_delete_delete_unsafe
+  , testPropertyNamed "imap-const-safe" "prop_imap_const_safe" prop_imap_const_safe
+  , testPropertyNamed "imap-const-unsafe" "prop_imap_const_unsafe" prop_imap_const_unsafe
+  , testPropertyNamed "ifoldMap-const-safe" "prop_ifoldMap_const_safe" prop_ifoldMap_const_safe
+  , testPropertyNamed "ifoldMap-const-unsafe" "prop_ifoldMap_const_unsafe" prop_ifoldMap_const_unsafe
+  , testPropertyNamed "safe-unsafe" "prop_safe_unsafe" prop_safe_unsafe
+
+#if __GLASGOW_HASKELL__ >= 806
+  , testCase "Eq-Safe-FinMap-laws-1" $
+      assertBool "Eq-Safe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Eq-Unsafe-FinMap-laws-1" $
+      assertBool "Eq-Unsafe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Eq-Safe-FinMap-laws-10" $
+      assertBool "Eq-Safe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Eq-Unsafe-FinMap-laws-10" $
+      assertBool "Eq-Unsafe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Semigroup-Safe-FinMap-laws-1" $
+      assertBool "Semigroup-Safe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Semigroup-Unsafe-FinMap-laws-1" $
+      assertBool "Semigroup-Unsafe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Semigroup-Safe-FinMap-laws-10" $
+      assertBool "Semigroup-Safe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Semigroup-Unsafe-FinMap-laws-10" $
+      assertBool "Semigroup-Unsafe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Monoid-Safe-FinMap-laws-1" $
+      assertBool "Monoid-Safe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Monoid-Unsafe-FinMap-laws-1" $
+      assertBool "Monoid-Unsafe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
+  , testCase "Monoid-Safe-FinMap-laws-10" $
+      assertBool "Monoid-Safe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Monoid-Unsafe-FinMap-laws-10" $
+      assertBool "Monoid-Unsafe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
+  , testCase "Foldable-Safe-FinMap-laws-1" $
+      assertBool "Foldable-Safe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @1)))
+  , testCase "Foldable-Unsafe-FinMap-laws-1" $
+      assertBool "Foldable-Unsafe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))
+  , testCase "Foldable-Safe-FinMap-laws-10" $
+      assertBool "Foldable-Safe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @10)))
+  , testCase "Foldable-Unsafe-FinMap-laws-10" $
+      assertBool "Foldable-Unsafe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))
+  , testCase "Traversable-Safe-FinMap-laws-1" $
+      assertBool "Traversable-Safe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @1)))
+  , testCase "Traversable-Unsafe-FinMap-laws-1" $
+      assertBool "Traversable-Unsafe-FinMap-laws-1" =<<
+        HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))
+  , testCase "Traversable-Safe-FinMap-laws-10" $
+      assertBool "Traversable-Safe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @10)))
+  , testCase "Traversable-Unsafe-FinMap-laws-10" $
+      assertBool "Traversable-Unsafe-FinMap-laws-10" =<<
+        HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))
+#endif
+  ]
diff --git a/test/Test/NatRepr.hs b/test/Test/NatRepr.hs
--- a/test/Test/NatRepr.hs
+++ b/test/Test/NatRepr.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE OverloadedStrings #-}
 module Test.NatRepr
   ( natTests
   )
@@ -13,11 +14,14 @@
 import           Data.Parameterized.Some
 import           GHC.TypeLits
 
+prop_withKnownNat :: Property
+prop_withKnownNat = property $
+  do nInt <- forAll $ HG.int (linearBounded :: Range Int)
+     case someNat nInt of
+       Nothing       -> diff nInt (<) 0
+       Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)
+
 natTests :: IO TestTree
 natTests = testGroup "Nat" <$> return
-  [ testProperty "withKnownNat" $ property $ do
-      nInt <- forAll $ HG.int (linearBounded :: Range Int)
-      case someNat nInt of
-        Nothing       -> diff nInt (<) 0
-        Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)
+  [ testPropertyNamed "withKnownNat" "prop_withKnownNat" prop_withKnownNat
   ]
diff --git a/test/Test/Some.hs b/test/Test/Some.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Some.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Test.Some
+  ( someTests
+  )
+where
+
+import           Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))
+import           Control.Lens (Lens', lens, view, set)
+
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.HUnit (assertEqual, testCase)
+
+import           Data.Parameterized.Classes (ShowF)
+import           Data.Parameterized.Some (Some(Some), someLens)
+
+data Item b where
+  BoolItem :: Item Bool
+  IntItem :: Item Int
+
+instance Show (Item b) where
+  show =
+    \case
+      BoolItem -> "BoolItem"
+      IntItem -> "IntItem"
+
+instance TestEquality Item where
+  testEquality x y =
+    case (x, y) of
+      (BoolItem, BoolItem) -> Just Refl
+      (IntItem, IntItem) -> Just Refl
+      _ -> Nothing
+
+data Pair a b =
+  Pair
+    { _fir :: a
+    , _sec :: Item b
+    }
+
+-- This instance isn't compatible with the intended use of TestEquality (which
+-- is supposed to be just for singletons), but it seems fine for tests.
+instance Eq a => TestEquality (Pair a) where
+  testEquality x y =
+    case testEquality (_sec x) (_sec y) of
+      Just Refl -> if _fir x == _fir y then Just Refl else Nothing
+      Nothing -> Nothing
+
+instance (Show a) => Show (Pair a b) where
+  show (Pair a b) = "Pair(" ++ show a ++ ", " ++ show b ++ ")"
+
+instance Show a => ShowF (Pair a)
+
+fir :: Lens' (Pair a b) a
+fir = lens _fir (\s v -> s { _fir = v })
+
+someFir :: Lens' (Some (Pair a)) a
+someFir = someLens fir
+
+someTests :: IO TestTree
+someTests =
+  testGroup "Some" <$>
+    return
+      [ testCase "someLens: view . set" $
+          assertEqual
+            "view l . set l x == const x"
+            (view someFir (set someFir 5 (Some (Pair 1 BoolItem))))
+            (5 :: Int)
+      , testCase "someLens: set . set" $
+          assertEqual
+            "set l y . set l x == set l y"
+            (set someFir 4 (set someFir 5 (Some (Pair 1 IntItem))))
+            (Some (Pair (4 :: Int) IntItem))
+      ]
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
--- a/test/Test/Vector.hs
+++ b/test/Test/Vector.hs
@@ -5,6 +5,7 @@
 {-# Language ExplicitForAll #-}
 {-# Language FlexibleInstances #-}
 {-# Language LambdaCase #-}
+{-# Language OverloadedStrings #-}
 {-# Language ScopedTypeVariables #-}
 {-# Language StandaloneDeriving #-}
 {-# Language TypeFamilies #-}
@@ -15,6 +16,12 @@
 #endif
 module Test.Vector
   ( vecTests
+  , SomeVector(..)
+  , genSomeVector
+  , genVectorOfLength
+  , genOrdering
+  , orderingEndomorphisms
+  , orderingToStringFuns
   )
 where
 
@@ -97,149 +104,208 @@
       EQ -> GT
       GT -> LT
   ]
+  
+-- | Used to test ifoldMap.
+orderingToStringFuns :: [ Ordering -> String ]
+orderingToStringFuns =
+  [ const "s"
+  , show
+  ]
 
+prop_reverse100 :: Property
+prop_reverse100 = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     case testLeq (knownNat @1) (length v) of
+       Nothing -> pure ()
+       Just LeqProof -> v === (reverse $ reverse v)
+
+prop_reverseSingleton :: Property
+prop_reverseSingleton = property $
+  do l <- (:[]) <$> forAll genOrdering
+     Just v <- return $ fromList (knownNat @1) l
+     v === reverse v
+
+prop_splitJoin :: Property
+prop_splitJoin = property $
+  do let n = knownNat @5
+     v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering
+     v === (join n $ split n (knownNat @5) v)
+
+prop_cons :: Property
+prop_cons = property $
+  do let n = knownNat @20
+         w = widthVal n
+     l <- forAll $ HG.list (constant w w) genOrdering
+     x <- forAll genOrdering
+     (cons x <$> fromList n l) === fromList (incNat n) (x:l)
+
+prop_snoc :: Property
+prop_snoc = property $
+  do let n = knownNat @20
+         w = widthVal n
+     l <- forAll $ HG.list (constant w w) genOrdering
+     x <- forAll genOrdering
+     (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])
+
+prop_snocUnsnoc :: Property
+prop_snocUnsnoc = property $
+  do let n = knownNat @20
+         w = widthVal n
+     l <- forAll $ HG.list (constant w w) genOrdering
+     x <- forAll genOrdering
+     (fst  . unsnoc . flip snoc x <$> fromList n l) === Just x
+
+prop_generate :: Property
+prop_generate = property $
+  do let n = knownNat @55
+         w = widthVal n
+         funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values
+         funs =  [ const EQ
+                 , \i -> if i < 10 then LT else if i > 15 then GT else EQ
+                 , \i -> if i == 0 then EQ else GT
+                 ]
+     f <- forAll $ HG.element funs
+     Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])
+
+prop_unfold :: Property
+prop_unfold = property $
+  do let n = knownNat @55
+         w = widthVal n
+         funs :: [ Ordering -> (Ordering, Ordering) ]  -- some miscellaneous functions to generate Vector values
+         funs =  [ const (EQ, EQ)
+                 , \case
+                     LT -> (LT, GT)
+                     GT -> (GT, LT)
+                     EQ -> (EQ, EQ)
+                 ]
+     f <- forAll $ HG.element funs
+     o <- forAll $ HG.element [EQ, LT, GT]
+     Just (unfoldr n f o) === fromList (incNat n) (P.take (w + 1) (List.unfoldr (Just . f) o))
+
+prop_toFromAssignment :: Property
+prop_toFromAssignment = property $
+  do vals <- forAll genSomePayloadList
+     Some a <- return $ mkUAsgn vals
+     let sz = Ctx.size a
+     case Ctx.viewSize sz of
+       Ctx.ZeroSize -> pure ()
+       Ctx.IncSize _ ->
+         let a' =
+               toAssignment
+                 sz
+                 (\_idx val -> Const val)
+                 (fromAssignment Some a)
+         in do assert $
+                 isJust $
+                   testEquality
+                     (Ctx.sizeToNatRepr sz)
+                     (Ctx.sizeToNatRepr (Ctx.size a'))
+               viewSome
+                 (\lastElem ->
+                    assert $
+                      isJust $
+                        testEquality
+                          (a Ctx.! Ctx.lastIndex sz) lastElem)
+                 (getConst (a' Ctx.! Ctx.lastIndex sz))
+
+prop_fmapId :: Property
+prop_fmapId = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     fmap id v === v
+
+prop_fmapCompose :: Property
+prop_fmapCompose = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     f <- forAll $ HG.element orderingEndomorphisms
+     g <- forAll $ HG.element orderingEndomorphisms
+     fmap (g . f) v === fmap g (fmap f v)
+
+prop_iterateNRange :: Property
+prop_iterateNRange = property $
+  do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))
+     toList (iterateN len (+1) 0) === [0..(natValue len)]
+
+prop_indicesOfRange :: Property
+prop_indicesOfRange = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]
+
+prop_imapConst :: Property
+prop_imapConst = property $
+  do f <- forAll $ HG.element orderingEndomorphisms
+     SomeVector v <- forAll $ genSomeVector genOrdering
+     imap (const f) v === fmap f v
+
+prop_ifoldMapConst :: Property
+prop_ifoldMapConst = property $
+  do f <- forAll $ HG.element orderingToStringFuns
+     SomeVector v <- forAll $ genSomeVector genOrdering
+     ifoldMap (const f) v === foldMap f v
+
+prop_imapConstIndicesOf :: Property
+prop_imapConstIndicesOf = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     imap const v === indicesOf v
+
+prop_imapElemAt :: Property
+prop_imapElemAt = property $
+  do SomeVector v <- forAll $ genSomeVector genOrdering
+     imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v
+
+prop_OrdEqVectorIndex :: Property
+prop_OrdEqVectorIndex = property $
+  do i <- forAll $ genFin (knownNat @10)
+     j <- forAll $ genFin (knownNat @10)
+     (i == j) === (compare i j == EQ)
+
 -- We use @Ordering@ just because it's simple
 vecTests :: IO TestTree
 vecTests = testGroup "Vector" <$> return
-  [ testProperty "reverse100" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       case testLeq (knownNat @1) (length v) of
-         Nothing -> pure ()
-         Just LeqProof -> v === (reverse $ reverse v)
-  , testProperty "reverseSingleton" $ property $
-    do l <- (:[]) <$> forAll genOrdering
-       Just v <- return $ fromList (knownNat @1) l
-       v === reverse v
+  [ testPropertyNamed "reverse100" "prop_reverse100" prop_reverse100
+  , testPropertyNamed "reverseSingleton" "prop_reverseSingleton" prop_reverseSingleton
 
-  , testProperty "split-join" $ property $
-    do let n = knownNat @5
-       v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering
-       v === (join n $ split n (knownNat @5) v)
+  , testPropertyNamed "split-join" "prop_splitJoin" prop_splitJoin
 
   -- @cons@ is the same for vectors or lists
-  , testProperty "cons" $ property $
-    do let n = knownNat @20
-           w = widthVal n
-       l <- forAll $ HG.list (constant w w) genOrdering
-       x <- forAll genOrdering
-       (cons x <$> fromList n l) === fromList (incNat n) (x:l)
+  , testPropertyNamed "cons" "prop_cons" prop_cons
 
   -- @snoc@ is like appending to a list
-  , testProperty "snoc" $ property $
-    do let n = knownNat @20
-           w = widthVal n
-       l <- forAll $ HG.list (constant w w) genOrdering
-       x <- forAll genOrdering
-       (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])
+  , testPropertyNamed "snoc" "prop_snoc" prop_snoc
 
   -- @snoc@ and @unsnoc@ are inverses
-  , testProperty "snoc/unsnoc" $ property $
-    do let n = knownNat @20
-           w = widthVal n
-       l <- forAll $ HG.list (constant w w) genOrdering
-       x <- forAll genOrdering
-       (fst  . unsnoc . flip snoc x <$> fromList n l) === Just x
+  , testPropertyNamed "snoc/unsnoc" "prop_snocUnsnoc" prop_snocUnsnoc
 
   -- @generate@ is like mapping a function over indices
-  , testProperty "generate" $ property $
-    do let n = knownNat @55
-           w = widthVal n
-           funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values
-           funs =  [ const EQ
-                   , \i -> if i < 10 then LT else if i > 15 then GT else EQ
-                   , \i -> if i == 0 then EQ else GT
-                   ]
-       f <- forAll $ HG.element funs
-       Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])
+  , testPropertyNamed "generate" "prop_generate" prop_generate
 
   -- @unfold@ works like @unfold@ on lists
-  , testProperty "unfold" $ property $
-    do let n = knownNat @55
-           w = widthVal n
-           funs :: [ Ordering -> (Ordering, Ordering) ]  -- some miscellaneous functions to generate Vector values
-           funs =  [ const (EQ, EQ)
-                   , \case
-                       LT -> (LT, GT)
-                       GT -> (GT, LT)
-                       EQ -> (EQ, EQ)
-                   ]
-       f <- forAll $ HG.element funs
-       o <- forAll $ HG.element [EQ, LT, GT]
-       Just (unfoldr n f o) === fromList (incNat n) (P.take (w + 1) (List.unfoldr (Just . f) o))
+  , testPropertyNamed "unfold" "prop_unfold" prop_unfold
 
   -- Converting to and from assignments preserves size and last element
-  , testProperty "to-from-assignment" $ property $
-    do vals <- forAll genSomePayloadList
-       Some a <- return $ mkUAsgn vals
-       let sz = Ctx.size a
-       case Ctx.viewSize sz of
-         Ctx.ZeroSize -> pure ()
-         Ctx.IncSize _ ->
-           let a' =
-                 toAssignment
-                   sz
-                   (\_idx val -> Const val)
-                   (fromAssignment Some a)
-           in do assert $
-                   isJust $
-                     testEquality
-                       (Ctx.sizeToNatRepr sz)
-                       (Ctx.sizeToNatRepr (Ctx.size a'))
-                 viewSome
-                   (\lastElem ->
-                      assert $
-                        isJust $
-                          testEquality
-                            (a Ctx.! Ctx.lastIndex sz) lastElem)
-                   (getConst (a' Ctx.! Ctx.lastIndex sz))
+  , testPropertyNamed "to-from-assignment" "prop_toFromAssignment" prop_toFromAssignment
 
   -- NOTE: We don't use hedgehog-classes here, because the way the types work
   -- would require this to only tests vectors of some fixed size.
   --
   -- Also, for 'fmap-compose', hedgehog-classes only tests two fixed functions
   -- over integers.
-  , testProperty "fmap-id" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       fmap id v === v
+  , testPropertyNamed "fmap-id" "prop_fmapId" prop_fmapId
 
-  , testProperty "fmap-compose" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       f <- forAll $ HG.element orderingEndomorphisms
-       g <- forAll $ HG.element orderingEndomorphisms
-       fmap (g . f) v === fmap g (fmap f v)
+  , testPropertyNamed "fmap-compose" "prop_fmapCompose" prop_fmapCompose
 
-  , testProperty "iterateN-range" $ property $
-    do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))
-       toList (iterateN len (+1) 0) === [0..(natValue len)]
+  , testPropertyNamed "iterateN-range" "prop_iterateNRange" prop_iterateNRange
 
-  , testProperty "indicesOf-range" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]
+  , testPropertyNamed "indicesOf-range" "prop_indicesOfRange" prop_indicesOfRange
 
-  , testProperty "imap-const" $ property $
-    do f <- forAll $ HG.element orderingEndomorphisms
-       SomeVector v <- forAll $ genSomeVector genOrdering
-       imap (const f) v === fmap f v
+  , testPropertyNamed "imap-const" "prop_imapConst" prop_imapConst
 
-  , testProperty "ifoldMap-const" $ property $
-    do let funs :: [ Ordering -> String ]
-           funs = [const "s", show]
-       f <- forAll $ HG.element funs
-       SomeVector v <- forAll $ genSomeVector genOrdering
-       ifoldMap (const f) v === foldMap f v
+  , testPropertyNamed "ifoldMap-const" "prop_ifoldMapConst" prop_ifoldMapConst
 
-  , testProperty "imap-const-indicesOf" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       imap const v === indicesOf v
+  , testPropertyNamed "imap-const-indicesOf" "prop_imapConstIndicesOf" prop_imapConstIndicesOf
 
-  , testProperty "imap-elemAt" $ property $
-    do SomeVector v <- forAll $ genSomeVector genOrdering
-       imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v
+  , testPropertyNamed "imap-elemAt" "prop_imapElemAt" prop_imapElemAt
 
-  , testProperty "Ord-Eq-VectorIndex" $ property $
-    do i <- forAll $ genFin (knownNat @10)
-       j <- forAll $ genFin (knownNat @10)
-       (i == j) === (compare i j == EQ)
+  , testPropertyNamed "Ord-Eq-VectorIndex" "prop_OrdEqVectorIndex" prop_OrdEqVectorIndex
 
 #if __GLASGOW_HASKELL__ >= 806
   -- Test a few different sizes since the types force each test to use a
diff --git a/test/UnitTest.hs b/test/UnitTest.hs
--- a/test/UnitTest.hs
+++ b/test/UnitTest.hs
@@ -4,8 +4,10 @@
 
 import qualified Test.Context
 import qualified Test.Fin
+import qualified Test.FinMap
 import qualified Test.List
 import qualified Test.NatRepr
+import qualified Test.Some
 import qualified Test.SymbolRepr
 import qualified Test.TH
 import qualified Test.Vector
@@ -25,7 +27,9 @@
   [ Test.Context.contextTests
   , pure Test.List.tests
   , Test.Fin.finTests
+  , Test.FinMap.finMapTests
   , Test.NatRepr.natTests
+  , Test.Some.someTests
   , Test.SymbolRepr.symbolTests
   , Test.TH.thTests
   , Test.Vector.vecTests