diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,30 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.1.4.0 -- *2021 Oct 1*
+
+  * Added the `ifoldLM` and `fromSomeList`, `fromListWith`, and
+    `fromListWithM` functions to the `List` module.
+  * Fix the description of the laws of the `OrdF` class.
+  * Fix a bug in which `Data.Parameterized.Vector.{join,joinWith,joinWithM}`
+    and `Data.Parameterized.NatRepr.plusAssoc` could crash at runtime if
+    compiled without optimizations.
+  * Add a `Data.Parameterized.Axiom` module providing `unsafeAxiom` and
+    `unsafeHeteroAxiom`, which can construct proofs of equality between types
+    that GHC isn't able to prove on its own. These functions are unsafe if used
+    improperly, so the responsibility is on the programmer to ensure that these
+    functions are used appropriately.
+  * Various `Proxy` enhancements: adds `KnownRepr`, `EqF`, and `ShowF` instances.
+  * Adds `mkRepr` and `mkKnownReprs` Template Haskell functions.
+  * Added `TraversableFC.WithIndex` module which provides the
+    `FunctorFCWithIndex`, `FoldableFCWithIndex`, and
+    `TraversableFCWithIndex` classes, with instances defined for
+    `Assignment` and `List`.
+  * Added `indicesUpTo`, and `indicesOf` as well as `iterateN` and `iterateNM`
+    for the `Vector` module.
+  * Added `Data.Parameterized.Fin` for finite types which can be used
+    to index into a `Vector n` or other size-indexed datatypes.
+
+
 ## 2.1.3.0 -- *2021 Mar 23*
 
   * Add support for GHC 9.
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,8 +1,8 @@
 Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.1.3.0
+Version:       2.1.4.0
 Author:        Galois Inc.
-Maintainer:    jhendrix@galois.com, kquick@galois.com
+Maintainer:    kquick@galois.com
 stability:     stable
 Build-type:    Simple
 Copyright:     ©2016-2021 Galois, Inc.
@@ -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.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.1
+tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.1
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -58,8 +58,10 @@
                , ghc-prim
                , hashable       >=1.2  && <1.4
                , hashtables     ==1.2.*
+               , indexed-traversable
                , lens           >=4.16 && <5.1
                , mtl
+               , profunctors    >=5.6 && < 5.7
                , template-haskell
                , text
                , vector         ==0.12.*
@@ -69,6 +71,7 @@
   exposed-modules:
     Data.Parameterized
     Data.Parameterized.All
+    Data.Parameterized.Axiom
     Data.Parameterized.BoolRepr
     Data.Parameterized.Classes
     Data.Parameterized.ClassesC
@@ -80,6 +83,7 @@
     Data.Parameterized.Ctx.Proofs
     Data.Parameterized.DataKind
     Data.Parameterized.DecidableEq
+    Data.Parameterized.Fin
     Data.Parameterized.HashTable
     Data.Parameterized.List
     Data.Parameterized.Map
@@ -94,6 +98,7 @@
     Data.Parameterized.TH.GADT
     Data.Parameterized.TraversableF
     Data.Parameterized.TraversableFC
+    Data.Parameterized.TraversableFC.WithIndex
     Data.Parameterized.Utils.BinTree
     Data.Parameterized.Utils.Endian
     Data.Parameterized.Vector
@@ -114,14 +119,18 @@
   main-is: UnitTest.hs
   other-modules:
     Test.Context
+    Test.Fin
+    Test.List
     Test.NatRepr
     Test.SymbolRepr
+    Test.TH
     Test.Vector
 
   build-depends: base
                , hashable
                , hashtables
                , hedgehog
+               , indexed-traversable
                , ghc-prim
                , lens
                , mtl
@@ -130,3 +139,7 @@
                , tasty-ant-xml == 1.1.*
                , tasty-hunit >= 0.9 && < 0.11
                , tasty-hedgehog
+
+  if impl(ghc >= 8.6)
+    build-depends:
+      hedgehog-classes
diff --git a/src/Data/Parameterized/Axiom.hs b/src/Data/Parameterized/Axiom.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Axiom.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Unsafe #-}
+{-|
+Copyright        : (c) Galois, Inc 2014-2021
+
+An unsafe module that provides functionality for constructing equality proofs
+that GHC cannot prove on its own.
+-}
+module Data.Parameterized.Axiom
+  ( unsafeAxiom, unsafeHeteroAxiom
+  ) where
+
+import Data.Type.Equality
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | Assert a proof of equality between two types.
+-- This is unsafe if used improperly, so use this with caution!
+unsafeAxiom :: forall a b. a :~: b
+unsafeAxiom = unsafeCoerce (Refl @a)
+{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]
+
+-- | Assert a proof of heterogeneous equality between two types.
+-- This is unsafe if used improperly, so use this with caution!
+unsafeHeteroAxiom :: forall a b. a :~~: b
+unsafeHeteroAxiom = unsafeCoerce (HRefl @a)
+{-# NOINLINE unsafeHeteroAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]
+
+{-
+Note [Mark unsafe axioms as NOINLINE]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We take care to mark definitions that use unsafeCoerce to construct proofs
+(e.g., unsafeAxiom = unsafeCoerce Refl) as NOINLINE. There are at least two
+good reasons to do so:
+
+1. On old version of GHC (prior to 9.0), GHC was liable to optimize
+   `unsafeCoerce` too aggressively, leading to unsound runtime behavior.
+   See https://gitlab.haskell.org/ghc/ghc/-/issues/16893 for an example.
+
+2. If GHC too heavily optimizes a program which cases on a proof of equality,
+   where the equality is between two types that can be determined not to be
+   equal statically (e.g., case (unsafeAxiom :: Bool :~: Int) of ...), then the
+   optimized program can crash at runtime. See
+   https://gitlab.haskell.org/ghc/ghc/-/issues/16310. Using NOINLINE is
+   sufficient to work around the issue.
+-}
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
@@ -12,6 +12,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -103,6 +104,9 @@
 instance Eq a => EqF (Const a) where
   eqF (Const x) (Const y) = x == y
 
+instance EqF Proxy where
+  eqF _ _ = True
+
 ------------------------------------------------------------------------
 -- PolyEq
 
@@ -174,7 +178,7 @@
 --
 -- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect:
 --
--- * @compareF x y == EQF@ equals @compare x y@ when @Ord (k tp)@ has an instance.
+-- * @toOrdering (compareF x y)@ equals @compare x y@ when @Ord (k tp)@ has an instance.
 -- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance.
 --
 -- Minimal complete definition: either 'compareF' or 'leqF'.
@@ -272,6 +276,8 @@
 
 instance Show x => ShowF (Const x)
 
+instance ShowF Proxy
+
 ------------------------------------------------------------------------
 -- IxedF
 
@@ -357,3 +363,6 @@
 -- kind @k@.
 class KnownRepr (f :: k -> Type) (ctx :: k) where
   knownRepr :: f ctx
+
+instance KnownRepr Proxy ctx where
+  knownRepr = Proxy
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
@@ -124,6 +124,7 @@
 import Data.Parameterized.NatRepr
 import Data.Parameterized.Some
 import Data.Parameterized.TraversableFC
+import Data.Parameterized.TraversableFC.WithIndex
 
 ------------------------------------------------------------------------
 -- Size
@@ -615,6 +616,15 @@
 instance TraversableFC Assignment where
   traverseFC f = traverseF f
 
+instance FunctorFCWithIndex Assignment where
+  imapFC = imapFCDefault
+
+instance FoldableFCWithIndex Assignment where
+  ifoldMapFC = ifoldMapFCDefault
+
+instance TraversableFCWithIndex Assignment where
+  itraverseFC = traverseWithIndex
+
 -- | Map assignment
 map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
 map f = fmapFC f
@@ -650,6 +660,7 @@
 zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y
 {-# INLINE zipWith #-}
 
+-- | This is a specialization of 'itraverseFC'.
 traverseWithIndex :: Applicative m
                   => (forall tp . Index ctx tp -> f tp -> m (g tp))
                   -> Assignment f ctx
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
@@ -98,6 +98,7 @@
 import           Unsafe.Coerce
 import           Data.Kind(Type)
 
+import           Data.Parameterized.Axiom
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Ctx
 import           Data.Parameterized.Ctx.Proofs
@@ -105,6 +106,7 @@
 import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr))
 import           Data.Parameterized.Some
 import           Data.Parameterized.TraversableFC
+import           Data.Parameterized.TraversableFC.WithIndex
 
 ------------------------------------------------------------------------
 -- Size
@@ -245,7 +247,7 @@
 
 instance TestEquality (Index ctx) where
   testEquality (Index i) (Index j)
-    | i == j = Just (unsafeCoerce Refl)
+    | i == j = Just unsafeAxiom
     | otherwise = Nothing
 
 instance Ord (Index ctx tp) where
@@ -926,6 +928,16 @@
 instance TraversableFC Assignment where
   traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x
   {-# INLINE traverseFC #-}
+
+instance FunctorFCWithIndex Assignment where
+  imapFC = imapFCDefault
+
+instance FoldableFCWithIndex Assignment where
+  ifoldMapFC = ifoldMapFCDefault
+
+instance TraversableFCWithIndex Assignment where
+  itraverseFC = traverseWithIndex
+
 
 traverseWithIndex :: Applicative m
                   => (forall tp . Index ctx tp -> f tp -> m (g tp))
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
@@ -13,12 +13,12 @@
   ) where
 
 import Data.Type.Equality
-import Unsafe.Coerce
 
+import Data.Parameterized.Axiom
 import Data.Parameterized.Ctx
 
 leftId :: p x -> (EmptyCtx <+> x) :~: x
-leftId _ = unsafeCoerce Refl
+leftId _ = unsafeAxiom
 
 assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z
-assoc _ _ _ = unsafeCoerce Refl
+assoc _ _ _ = unsafeAxiom
diff --git a/src/Data/Parameterized/Fin.hs b/src/Data/Parameterized/Fin.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Fin.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-|
+Copyright        : (c) Galois, Inc 2021
+
+@'Fin' n@ is a finite type with exactly @n@ elements. Essentially, they bundle a
+'NatRepr' that has an existentially-quantified type parameter with a proof that
+its parameter is less than some fixed natural.
+
+They are useful in combination with types of a fixed size. For example 'Fin' is
+used as the index in the 'Data.Functor.WithIndex.FunctorWithIndex' instance for
+'Data.Parameterized.Vector'. As another example, a @Map ('Fin' n) a@ is a @Map@
+that naturally has a fixed size bound of @n@.
+-}
+module Data.Parameterized.Fin
+  ( Fin
+  , mkFin
+  , viewFin
+  , finToNat
+  , embed
+  , tryEmbed
+  , minFin
+  , fin0Void
+  , fin1Unit
+  , fin2Bool
+  ) where
+
+import Control.Lens.Iso (Iso', iso)
+import GHC.TypeNats (KnownNat)
+import Numeric.Natural (Natural)
+import Data.Void (Void, absurd)
+
+import Data.Parameterized.NatRepr
+
+-- | The type @'Fin' n@ has exactly @n@ inhabitants.
+data Fin n =
+  -- GHC 8.6 and 8.4 require parentheses around 'i + 1 <= n'
+  forall i. (i + 1 <= n) => Fin { _getFin :: NatRepr i }
+
+instance Eq (Fin n) where
+  i == j = finToNat i == finToNat j
+
+instance Ord (Fin n) where
+  compare i j = compare (finToNat i) (finToNat j)
+
+instance (1 <= n, KnownNat n) => Bounded (Fin n) where
+  minBound = Fin (knownNat @0)
+  maxBound =
+    case minusPlusCancel (knownNat @n) (knownNat @1) of
+      Refl -> Fin (decNat (knownNat @n))
+
+-- | Non-lawful instance, intended only for testing.
+instance Show (Fin n) where
+  show i = "Fin " ++ show (finToNat i)
+
+mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n
+mkFin = Fin
+
+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
+
+embed :: forall n m. (n <= m) => Fin n -> Fin m
+embed =
+  viewFin
+    (\(x :: NatRepr o) ->
+      case leqTrans (LeqProof :: LeqProof (o + 1) n) (LeqProof :: LeqProof n m) of
+        LeqProof -> Fin x
+    )
+
+tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
+tryEmbed n m i =
+  case testLeq n m of
+    Just LeqProof -> Just (embed i)
+    Nothing -> Nothing
+
+-- | The smallest element of @'Fin' n@
+minFin :: (1 <= n) => Fin n
+minFin = Fin (knownNat @0)
+
+fin0Void :: Iso' (Fin 0) Void
+fin0Void =
+  iso
+    (viewFin
+      (\(x :: NatRepr o) ->
+        case plusComm x (knownNat @1) of
+          Refl ->
+            case addIsLeqLeft1 @1 @o @0 LeqProof of {}))
+    absurd
+
+fin1Unit :: Iso' (Fin 1) ()
+fin1Unit = iso (const ()) (const minFin)
+
+fin2Bool :: Iso' (Fin 2) Bool
+fin2Bool =
+  iso
+    (viewFin
+      (\n ->
+         case isZeroNat n of
+           ZeroNat -> False
+           NonZeroNat -> True))
+    (\b -> if b then maxBound else minBound)
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
@@ -129,15 +129,20 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 module Data.Parameterized.List
   ( List(..)
+  , fromSomeList
+  , fromListWith
+  , fromListWithM
   , Index(..)
   , indexValue
   , (!!)
   , update
   , indexed
   , imap
+  , ifoldlM
   , ifoldr
   , izipWith
   , itraverse
@@ -149,11 +154,15 @@
   ) where
 
 import qualified Control.Lens as Lens
+import           Data.Foldable
 import           Data.Kind
 import           Prelude hiding ((!!))
+import           Unsafe.Coerce (unsafeCoerce)
 
 import           Data.Parameterized.Classes
+import           Data.Parameterized.Some
 import           Data.Parameterized.TraversableFC
+import           Data.Parameterized.TraversableFC.WithIndex
 
 -- | Parameterized list of elements.
 data List :: (k -> Type) -> [k] -> Type where
@@ -185,6 +194,18 @@
   traverseFC _ Nil = pure Nil
   traverseFC f (h :< r) = (:<) <$> f h <*> traverseFC f r
 
+type instance IndexF   (List (f :: k -> Type) sh) = Index sh
+type instance IxValueF (List (f :: k -> Type) sh) = f
+
+instance FunctorFCWithIndex List where
+  imapFC = imap
+
+instance FoldableFCWithIndex List where
+  ifoldrFC = ifoldr
+
+instance TraversableFCWithIndex List where
+  itraverseFC = itraverse
+
 instance TestEquality f => TestEquality (List f) where
   testEquality Nil Nil = Just Refl
   testEquality (xh :< xl) (yh :< yl) = do
@@ -202,17 +223,38 @@
     lexCompareF xl yl $
     EQF
 
-
 instance KnownRepr (List f) '[] where
   knownRepr = Nil
 
 instance (KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f) (s ': sh) where
   knownRepr = knownRepr :< knownRepr
 
+-- | Apply function to list to yield a parameterized list.
+fromListWith :: forall a f . (a -> Some f) -> [a] -> Some (List f)
+fromListWith f = foldr g (Some Nil)
+  where g :: a -> Some (List f) -> Some (List f)
+        g x (Some r) = viewSome (\h -> Some (h :< r)) (f x)
+
+-- | Apply monadic action to list to yield a parameterized list.
+fromListWithM :: forall a f m
+                  .  Monad m
+                  => (a -> m (Some f))
+                  -> [a]
+                  -> m (Some (List f))
+fromListWithM f = foldrM g (Some Nil)
+  where g :: a -> Some (List f) -> m (Some (List f))
+        g x (Some r) = viewSome (\h -> Some (h :< r)) <$> f x
+
+-- | Map from list of Some to Some list
+fromSomeList :: [Some f] -> Some (List f)
+fromSomeList = fromListWith id
+
+{-# INLINABLE fromListWith #-}
+{-# INLINABLE fromListWithM #-}
+
 --------------------------------------------------------------------------------
 -- * Indexed operations
 
-
 -- | Represents an index into a type-level list. Used in place of integers to
 --   1. ensure that the given index *does* exist in the list
 --   2. guarantee that it has the given kind
@@ -294,6 +336,8 @@
 
 -- | Map over the elements in the list, and provide the index into
 -- each element along with the element itself.
+--
+-- This is a specialization of 'imapFC'.
 imap :: forall f g l
      . (forall x . Index l x -> f x -> g x)
      -> List f l
@@ -309,7 +353,29 @@
         Nil -> Nil
         e :< rest -> f (g IndexHere) e :< go (g . IndexThere) rest
 
+-- | Left fold with an additional index.
+ifoldlM :: forall sh a b m
+        . Monad m
+        => (forall tp . b -> Index sh tp -> a tp -> m b)
+        -> b
+        -> List a sh
+        -> m b
+ifoldlM _ b Nil = pure b
+ifoldlM f b0 (a0 :< r0) = f b0 IndexHere a0 >>= go IndexHere r0
+  where
+    go :: forall tps tp
+        . Index sh tp
+       -> List a tps
+       -> b
+       -> m b
+    go _ Nil b = pure b
+    go idx (a :< rest) b =
+      let idx' = unsafeCoerce (IndexThere idx)
+       in f b idx' a >>= go idx' rest
+
 -- | Right-fold with an additional index.
+--
+-- This is a specialization of 'ifoldrFC'.
 ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b
 ifoldr f seed0 l = go id l seed0
   where
@@ -342,6 +408,8 @@
           f (g IndexHere) a b :< go (g . IndexThere) as' bs'
 
 -- | Traverse with an additional index.
+--
+-- This is a specialization of 'itraverseFC'.
 itraverse :: forall a b sh t
           . Applicative t
           => (forall tp . Index sh tp -> a tp -> t (b tp))
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
@@ -136,6 +136,7 @@
 import GHC.TypeNats as TypeNats
 import Unsafe.Coerce
 
+import Data.Parameterized.Axiom
 import Data.Parameterized.NatRepr.Internal
 import Data.Parameterized.Some
 
@@ -155,7 +156,7 @@
 withKnownNat (NatRepr nVal) v =
   case someNatVal nVal of
     SomeNat (Proxy :: Proxy n') ->
-      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of
+      case unsafeAxiom :: n :~: n' of
         Refl -> v
 
 data IsZeroNat n where
@@ -223,7 +224,7 @@
 withDivModNat n m f =
   case ( Some (NatRepr divPart), Some (NatRepr modPart)) of
      ( Some (divn :: NatRepr div), Some (modn :: NatRepr mod) )
-       -> case unsafeCoerce (Refl :: 0 :~: 0) of
+       -> case unsafeAxiom of
             (Refl :: (n :~: ((div * m) + mod))) -> f divn modn
   where
     (divPart, modPart) = divMod (natValue n) (natValue m)
@@ -302,15 +303,15 @@
 
 -- | 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)
+plusComm _ _ = unsafeAxiom
 
 -- | Produce evidence that @+@ is associative.
 plusAssoc :: forall f m g n h o . f m -> g n -> h o -> m+(n+o) :~: (m+n)+o
-plusAssoc = unsafeCoerce (Refl :: m+(n+o) :~: m+(n+o))
+plusAssoc _ _ _ = unsafeAxiom
 
 -- | Produce evidence that @*@ is commutative.
 mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
-mulComm _ _ = unsafeCoerce Refl
+mulComm _ _ = unsafeAxiom
 
 mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
 mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of
@@ -318,14 +319,14 @@
 
 -- | 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)
+plusMinusCancel _ _ = unsafeAxiom
 
 minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m
-minusPlusCancel _ _ = unsafeCoerce (Refl :: m :~: m)
+minusPlusCancel _ _ = unsafeAxiom
 
 addMulDistribRight :: forall n m p f g h. f n -> g m -> h p
                     -> ((n * p) + (m * p)) :~: ((n + m) * p)
-addMulDistribRight _n _m _p = unsafeCoerce Refl
+addMulDistribRight _n _m _p = unsafeAxiom
 
 
 
@@ -338,7 +339,7 @@
 withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p
                     -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
 withSubMulDistribRight _n _m _p f =
-  case unsafeCoerce (Refl :: 0 :~: 0) of
+  case unsafeAxiom of
     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f
 
 ------------------------------------------------------------------------
@@ -363,7 +364,7 @@
               -> Either (LeqProof (m+1) n) (m :~: n)
 testStrictLeq (NatRepr m) (NatRepr n)
   | m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0))
-  | otherwise = Right (unsafeCoerce (Refl :: m :~: m))
+  | otherwise = Right unsafeAxiom
 {-# NOINLINE testStrictLeq #-}
 
 -- As for NatComparison above, but works with LeqProof
@@ -610,8 +611,8 @@
 
 mulCancelR ::
   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
-mulCancelR _ _ _ = unsafeCoerce Refl
+mulCancelR _ _ _ = unsafeAxiom
 
 -- | Used in @Vector@
 lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
-lemmaMul = unsafeCoerce Refl
+lemmaMul _ _ = unsafeAxiom
diff --git a/src/Data/Parameterized/NatRepr/Internal.hs b/src/Data/Parameterized/NatRepr/Internal.hs
--- a/src/Data/Parameterized/NatRepr/Internal.hs
+++ b/src/Data/Parameterized/NatRepr/Internal.hs
@@ -27,6 +27,7 @@
 import Numeric.Natural
 import Unsafe.Coerce
 
+import Data.Parameterized.Axiom
 import Data.Parameterized.Classes
 import Data.Parameterized.DecidableEq
 
@@ -49,12 +50,12 @@
 
 instance TestEquality NatRepr where
   testEquality (NatRepr m) (NatRepr n)
-    | m == n = Just (unsafeCoerce Refl)
+    | m == n = Just unsafeAxiom
     | otherwise = Nothing
 
 instance DecidableEq NatRepr where
   decEq (NatRepr m) (NatRepr n)
-    | m == n    = Left $ unsafeCoerce Refl
+    | m == n    = Left unsafeAxiom
     | otherwise = Right $
         \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"
 
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
@@ -48,11 +48,11 @@
 import Data.Kind
 import Data.IORef
 import Data.STRef
-import Data.Typeable
 import Data.Word
 import Unsafe.Coerce
 import System.IO.Unsafe (unsafePerformIO)
 
+import Data.Parameterized.Axiom
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
 
@@ -129,7 +129,7 @@
 type role Nonce nominal nominal
 
 instance TestEquality (Nonce s) where
-  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)
+  testEquality x y | indexValue x == indexValue y = Just unsafeAxiom
                    | otherwise = Nothing
 
 instance OrdF (Nonce s) where
diff --git a/src/Data/Parameterized/Nonce/Unsafe.hs b/src/Data/Parameterized/Nonce/Unsafe.hs
--- a/src/Data/Parameterized/Nonce/Unsafe.hs
+++ b/src/Data/Parameterized/Nonce/Unsafe.hs
@@ -43,6 +43,7 @@
 import Data.Word
 import Unsafe.Coerce
 
+import Data.Parameterized.Axiom
 import Data.Parameterized.Classes
 
 -- | A simple type that for getting fresh indices in the 'ST' monad.
@@ -64,7 +65,7 @@
 type role Nonce nominal
 
 instance TestEquality Nonce where
-  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)
+  testEquality x y | indexValue x == indexValue y = Just unsafeAxiom
                    | otherwise = Nothing
 
 instance OrdF Nonce where
diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs
--- a/src/Data/Parameterized/Peano.hs
+++ b/src/Data/Parameterized/Peano.hs
@@ -88,6 +88,7 @@
 import           Data.Word
 
 #ifdef UNSAFE_OPS
+import           Data.Parameterized.Axiom
 import           Unsafe.Coerce(unsafeCoerce)
 #endif
 
@@ -221,7 +222,7 @@
 instance TestEquality PeanoRepr where
 #ifdef UNSAFE_OPS
   testEquality (PeanoRepr m) (PeanoRepr n)
-    | m == n = Just (unsafeCoerce Refl)
+    | m == n = Just unsafeAxiom
     | otherwise = Nothing
 #else
   testEquality ZRepr ZRepr = Just Refl
@@ -235,7 +236,7 @@
 instance DecidableEq PeanoRepr where
 #ifdef UNSAFE_OPS
   decEq (PeanoRepr m) (PeanoRepr n)
-    | m == n    = Left $ unsafeCoerce Refl
+    | m == n    = Left unsafeAxiom
     | otherwise = Right $
         \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]"
 #else
@@ -452,7 +453,7 @@
   Assignment f t1 -> Assignment f t2 ->
   CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
 #ifdef UNSAFE_OPS
-plusCtxSizeAxiom _t1 _t2 = unsafeCoerce Refl
+plusCtxSizeAxiom _t1 _t2 = unsafeAxiom
 #else
 plusCtxSizeAxiom t1 t2 =
   case viewAssign t2 of
@@ -467,7 +468,7 @@
   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
+minusPlusAxiom _n _t _t' = unsafeAxiom
 #else
 minusPlusAxiom n t t' = case peanoView t' of
   ZRepr -> Refl
@@ -484,7 +485,7 @@
   PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->
   Lt (Plus t' t) n :~: 'True
 #ifdef UNSAFE_OPS
-ltMinusPlusAxiom _n _t _t' = unsafeCoerce Refl
+ltMinusPlusAxiom _n _t _t' = unsafeAxiom
 #else
 ltMinusPlusAxiom n t t' = case peanoView n of
   SRepr m -> case peanoView t' of
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
@@ -44,6 +44,7 @@
 import           Data.Proxy
 import qualified Data.Text as Text
 
+import           Data.Parameterized.Axiom
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 
@@ -81,7 +82,7 @@
 
 instance TestEquality SymbolRepr where
    testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)
-      | x == y    = Just (unsafeCoerce (Refl :: x :~: x))
+      | x == y    = Just unsafeAxiom
       | otherwise = Nothing
 instance OrdF SymbolRepr where
    compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)
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
@@ -25,6 +25,10 @@
   , structuralHash
   , structuralHashWithSalt
   , PolyEq(..)
+    -- * Repr generators (\"singletons\")
+    -- $reprs
+  , mkRepr
+  , mkKnownReprs
     -- * Template haskell utilities that may be useful in other contexts.
   , DataD
   , lookupDataType'
@@ -493,6 +497,204 @@
 matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ
 matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con))
 
+-- | Generate a \"repr\" or singleton type from a data kind. For nullary
+-- constructors, this works as follows:
+--
+-- @
+-- data T1 = A | B | C
+-- \$(mkRepr ''T1)
+-- ======>
+-- data T1Repr (tp :: T1)
+--   where
+--     ARepr :: T1Repr 'A
+--     BRepr :: T1Repr 'B
+--     CRepr :: T1Repr 'C
+-- @
+--
+-- For constructors with fields, we assume each field type @T@ already has a
+-- corresponding repr type @TRepr :: T -> *@.
+--
+-- @
+-- data T2 = T2_1 T1 | T2_2 T1
+-- \$(mkRepr ''T2)
+-- ======>
+-- data T2Repr (tp :: T2)
+--   where
+--     T2_1Repr :: T1Repr tp -> T2Repr ('T2_1 tp)
+--     T2_2Repr :: T1Repr tp -> T2Repr ('T2_2 tp)
+-- @
+--
+-- Constructors with multiple fields work fine as well:
+--
+-- @
+-- data T3 = T3 T1 T2
+-- \$(mkRepr ''T3)
+-- ======>
+-- data T3Repr (tp :: T3)
+--   where
+--     T3Repr :: T1Repr tp1 -> T2Repr tp2 -> T3Repr ('T3 tp1 tp2)
+-- @
+--
+-- This is generally compatible with other \"repr\" types provided by
+-- @parameterized-utils@, such as @NatRepr@ and @PeanoRepr@:
+--
+-- @
+-- data T4 = T4_1 Nat | T4_2 Peano
+-- \$(mkRepr ''T4)
+-- ======>
+-- data T4Repr (tp :: T4)
+--   where
+--     T4Repr :: NatRepr tp1 -> PeanoRepr tp2 -> T4Repr ('T4 tp1 tp2)
+-- @
+--
+-- The data kind must be \"simple\", i.e. it must be monomorphic and only
+-- contain user-defined data constructors (no lists, tuples, etc.). For example,
+-- the following will not work:
+--
+-- @
+-- data T5 a = T5 a
+-- \$(mkRepr ''T5)
+-- ======>
+-- Foo.hs:1:1: error:
+--     Exception when trying to run compile-time code:
+--       mkRepr cannot be used on polymorphic data kinds.
+-- @
+--
+-- Similarly, this will not work:
+--
+-- @
+-- data T5 = T5 [Nat]
+-- \$(mkRepr ''T5)
+-- ======>
+-- Foo.hs:1:1: error:
+--     Exception when trying to run compile-time code:
+--       mkRepr cannot be used on this data kind.
+-- @
+--
+-- Note that at a minimum, you will need the following extensions to use this macro:
+--
+-- @
+-- {-\# LANGUAGE DataKinds \#-}
+-- {-\# LANGUAGE GADTs \#-}
+-- {-\# LANGUAGE KindSignatures \#-}
+-- {-\# LANGUAGE TemplateHaskell \#-}
+-- @
+mkRepr :: Name -> DecsQ
+mkRepr typeName = do
+  let reprTypeName = mkReprName typeName
+      varName = mkName "tp"
+  info <- lookupDataType' typeName
+  let gc ci = do
+        let ctorName = constructorName ci
+            reprCtorName = mkReprName ctorName
+            ctorFieldTypeNames = getCtorName <$> constructorFields ci
+            ctorFieldReprNames = mkReprName <$> ctorFieldTypeNames
+        -- Generate a list of type variables to be supplied as type arguments
+        -- for each repr argument.
+        tvars <- replicateM (length (constructorFields ci)) (newName "tp")
+        let appliedType =
+              foldl AppT (PromotedT (constructorName ci)) (VarT <$> tvars)
+            ctorType = AppT (ConT reprTypeName) appliedType
+            ctorArgTypes =
+              zipWith (\n v -> (Bang NoSourceUnpackedness NoSourceStrictness, AppT (ConT n) (VarT v))) ctorFieldReprNames tvars
+        return $ GadtC
+          [reprCtorName]
+          ctorArgTypes
+          ctorType
+  ctors <- mapM gc (datatypeCons info)
+  return $ [ DataD [] reprTypeName
+             [kindedTV varName (ConT typeName)]
+             Nothing
+             ctors
+             []
+           ]
+  where getCtorName :: Type -> Name
+        getCtorName c = case c of
+          ConT nm -> nm
+          VarT _ -> error $ "mkRepr cannot be used on polymorphic data kinds."
+          _ -> error $ "mkRepr cannot be used on this data kind."
+
+-- | Generate @KnownRepr@ instances for each constructor of a data kind. Given a
+-- data kind @T@, we assume a repr type @TRepr (t :: T)@ is in scope with
+-- structure that perfectly matches @T@ (using 'mkRepr' to generate the repr
+-- type will guarantee this).
+--
+-- Given data kinds @T1@, @T2@, and @T3@ from the documentation of 'mkRepr', and
+-- the associated repr types @T1Repr@, @T2Repr@, and @T3Repr@, we can use
+-- 'mkKnownReprs' to generate these instances like so:
+--
+-- @
+-- \$(mkKnownReprs ''T1)
+-- ======>
+-- instance KnownRepr T1Repr 'A where
+--   knownRepr = ARepr
+-- instance KnownRepr T1Repr 'B where
+--   knownRepr = BRepr
+-- instance KnownRepr T1Repr 'C where
+--   knownRepr = CRepr
+-- @
+--
+-- @
+-- \$(mkKnownReprs ''T2)
+-- ======>
+-- instance KnownRepr T1Repr tp =>
+--          KnownRepr T2Repr ('T2_1 tp) where
+--   knownRepr = T2_1Repr knownRepr
+-- @
+--
+-- @
+-- \$(mkKnownReprs ''T3)
+-- ======>
+-- instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) =>
+--          KnownRepr T3Repr ('T3_1 tp1 tp2) where
+--   knownRepr = T3_1Repr knownRepr knownRepr
+-- @
+--
+-- The same restrictions that apply to 'mkRepr' also apply to 'mkKnownReprs'.
+-- The data kind must be \"simple\", i.e. it must be monomorphic and only
+-- contain user-defined data constructors (no lists, tuples, etc.).
+--
+-- Note that at a minimum, you will need the following extensions to use this macro:
+--
+-- @
+-- {-\# LANGUAGE DataKinds \#-}
+-- {-\# LANGUAGE GADTs \#-}
+-- {-\# LANGUAGE KindSignatures \#-}
+-- {-\# LANGUAGE MultiParamTypeClasses \#-}
+-- {-\# LANGUAGE TemplateHaskell \#-}
+-- @
+--
+-- Also, 'mkKnownReprs' must be used in the same module as the definition of
+-- the repr type (not necessarily for the data kind).
+mkKnownReprs :: Name -> DecsQ
+mkKnownReprs typeName = do
+  kr <- [t|KnownRepr|]
+  let krFName = mkName "knownRepr"
+      reprTypeName = mkReprName typeName
+  typeInfo <- lookupDataType' typeName
+  reprInfo <- lookupDataType' reprTypeName
+  forM (zip (datatypeCons typeInfo) (datatypeCons reprInfo)) $ \(tci, rci) -> do
+    vars <- replicateM (length (constructorFields tci)) (newName "tp")
+    krReqs <- forM (zip (constructorFields tci) vars) $ \(tfld, v) -> do
+      let fldReprName = mkReprName (getCtorName tfld)
+      return $ AppT (AppT kr (ConT fldReprName)) (VarT v)
+    let appliedType =
+          foldl AppT (PromotedT (constructorName tci)) (VarT <$> vars)
+        krConstraint = AppT (AppT kr (ConT reprTypeName)) appliedType
+        krExp = foldl AppE (ConE (constructorName rci)) $
+          map (const (VarE krFName)) vars
+        krDec = FunD krFName [Clause [] (NormalB krExp) []]
+
+    return $ InstanceD Nothing krReqs krConstraint [krDec]
+  where getCtorName :: Type -> Name
+        getCtorName c = case c of
+          ConT nm -> nm
+          VarT _ -> error $ "mkKnownReprs cannot be used on polymorphic data kinds."
+          _ -> error $ "mkKnownReprs cannot be used on this data kind."
+
+mkReprName :: Name -> Name
+mkReprName nm = mkName (nameBase nm ++ "Repr")
+
 -- $typePatterns
 --
 -- The Template Haskell instance generators 'structuralEquality',
@@ -532,3 +734,44 @@
 --
 -- The use of 'DataArg' says that the type parameter of the 'NatRepr' must
 -- be the same as the second type parameter of @T@.
+
+-- $reprs
+--
+-- When working with data kinds with run-time representatives, we encourage
+-- users of @parameterized-utils@ to use the following convention. Given a data
+-- kind defined by
+--
+-- @
+-- data T = ...
+-- @
+--
+-- users should also supply a GADT @TRepr@ parameterized by @T@, e.g.
+--
+-- @
+-- data TRepr (t :: T) where ...
+-- @
+--
+-- Each constructor of @TRepr@ should correspond to a constructor of @T@. If @T@
+-- is defined by
+--
+-- @
+-- data T = A | B Nat
+-- @
+--
+-- we have a corresponding
+--
+-- @
+-- data TRepr (t :: T) where
+--   ARepr :: TRepr 'A
+--   BRepr :: NatRepr w -> TRepr ('B w)
+-- @
+--
+-- Assuming the user of @parameterized-utils@ follows this convention, we
+-- provide the Template Haskell construct 'mkRepr' to automate the creation of
+-- the @TRepr@ GADT. We also provide 'mkKnownReprs', which generates 'KnownRepr'
+-- instances for that GADT type. See the documentation for those two functions
+-- for more detailed explanations.
+--
+-- NB: These macros are inspired by the corresponding macros provided by
+-- @singletons-th@, and the \"repr\" programming idiom is very similar to the one
+-- used by @singletons@.
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
@@ -45,7 +45,12 @@
 
 import Data.Parameterized.Classes
 
--- | A parameterized type that is a function on all instances.
+-- | A parameterized type that is a functor on all instances.
+--
+-- Laws:
+--
+-- [Identity]    @'fmapFC' 'id' == 'id'@
+-- [Composition] @'fmapFC' (f . g) == 'fmapFC' f . 'fmapFC' g@
 class FunctorFC (t :: (k -> Type) -> l -> Type) where
   fmapFC :: forall f g. (forall x. f x -> g x) ->
                         (forall x. t f x -> t g x)
diff --git a/src/Data/Parameterized/TraversableFC/WithIndex.hs b/src/Data/Parameterized/TraversableFC/WithIndex.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/TraversableFC/WithIndex.hs
@@ -0,0 +1,175 @@
+------------------------------------------------------------------------
+-- |
+-- Module           : Data.Parameterized.TraversableFC.WithIndex
+-- Copyright        : (c) Galois, Inc 2021
+-- Maintainer       : Langston Barrett
+-- Description      : 'TraversableFC' classes, but with indices.
+--
+-- As in the package indexed-traversable.
+------------------------------------------------------------------------
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.TraversableFC.WithIndex
+  ( FunctorFCWithIndex(..)
+  , FoldableFCWithIndex(..)
+  , ifoldlMFC
+  , ifoldrMFC
+  , iallFC
+  , ianyFC
+  , TraversableFCWithIndex(..)
+  , imapFCDefault
+  , ifoldMapFCDefault
+  ) where
+
+import Data.Functor.Const (Const(Const, getConst))
+import Data.Functor.Identity (Identity(Identity, runIdentity))
+import Data.Kind
+import Data.Monoid (All(..), Any(..), Endo(Endo), appEndo, Dual(Dual, getDual))
+import Data.Profunctor.Unsafe ((#.))
+import GHC.Exts (build)
+
+import Data.Parameterized.Classes
+import Data.Parameterized.TraversableFC
+
+class FunctorFC t => FunctorFCWithIndex (t :: (k -> Type) -> l -> Type) where
+  -- | Like 'fmapFC', but with an index.
+  --
+  -- @
+  -- 'fmapFC' f ≡ 'imapFC' ('const' f)
+  -- @
+  imapFC ::
+    forall f g z.
+    (forall x. IndexF (t f z) x -> f x -> g x)
+    -> t f z
+    -> t g z
+
+------------------------------------------------------------------------
+
+class (FoldableFC t, FunctorFCWithIndex t) => FoldableFCWithIndex (t :: (k -> Type) -> l -> Type) where
+
+  -- | Like 'foldMapFC', but with an index.
+  --
+  -- @
+  -- 'foldMapFC' f ≡ 'ifoldMapFC' ('const' f)
+  -- @
+  ifoldMapFC ::
+    forall f m z.
+    Monoid m =>
+    (forall x. IndexF (t f z) x -> f x -> m) ->
+    t f z ->
+    m
+  ifoldMapFC f = ifoldrFC (\i x -> mappend (f i x)) mempty
+
+  -- | Like 'foldrFC', but with an index.
+  ifoldrFC ::
+    forall z f b.
+    (forall x. IndexF (t f z) x -> f x -> b -> b) ->
+    b ->
+    t f z ->
+    b
+  ifoldrFC f z t = appEndo (ifoldMapFC (\i x -> Endo (f i x)) t) z
+
+  -- | Like 'foldlFC', but with an index.
+  ifoldlFC ::
+    forall f b z.
+    (forall x. IndexF (t f z) x -> b -> f x -> b) ->
+    b ->
+    t f z ->
+    b
+  ifoldlFC f z t =
+    appEndo (getDual (ifoldMapFC (\i e -> Dual (Endo (\r -> f i r e))) t)) z
+
+  -- | Like 'ifoldrFC', but with an index.
+  ifoldrFC' ::
+    forall f b z.
+    (forall x. IndexF (t f z) x -> f x -> b -> b) ->
+    b ->
+    t f z ->
+    b
+  ifoldrFC' f0 z0 xs = ifoldlFC (f' f0) id xs z0
+    where f' f i k x z = k $! f i x z
+
+  -- | Like 'ifoldlFC', but with an index.
+  ifoldlFC' :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)
+  ifoldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0
+    where f' f x k z = k $! f z x
+
+  -- | Convert structure to list.
+  itoListFC ::
+    forall f a z.
+    (forall x. IndexF (t f z) x -> f x -> a) ->
+    t f z ->
+    [a]
+  itoListFC f t = build (\c n -> ifoldrFC (\i e v -> c (f i e) v) n t)
+
+-- | Like 'foldlMFC', but with an index.
+ifoldlMFC ::
+  FoldableFCWithIndex t =>
+  Monad m =>
+  (forall x. IndexF (t f z) x -> b -> f x -> m b) ->
+  b ->
+  t f z ->
+  m b
+ifoldlMFC f z0 xs = ifoldlFC (\i k x z -> f i z x >>= k) return xs z0
+
+-- | Like 'foldrMFC', but with an index.
+ifoldrMFC ::
+  FoldableFCWithIndex t =>
+  Monad m =>
+  (forall x. IndexF (t f z) x -> f x -> b -> m b) ->
+  b ->
+  t f z ->
+  m b
+ifoldrMFC f z0 xs = ifoldlFC (\i k x z -> f i x z >>= k) return xs z0
+
+-- | Like 'allFC', but with an index.
+iallFC ::
+  FoldableFCWithIndex t =>
+  (forall x. IndexF (t f z) x -> f x -> Bool) ->
+  t f z ->
+  Bool
+iallFC p = getAll #. ifoldMapFC (\i x -> All (p i x))
+
+-- | Like 'anyFC', but with an index.
+ianyFC ::
+  FoldableFCWithIndex t =>
+  (forall x. IndexF (t f z) x -> f x -> Bool) ->
+  t f z -> Bool
+ianyFC p = getAny #. ifoldMapFC (\i x -> Any (p i x))
+
+------------------------------------------------------------------------
+
+class (TraversableFC t, FoldableFCWithIndex t) => TraversableFCWithIndex (t :: (k -> Type) -> l -> Type) where
+  -- | Like 'traverseFC', but with an index.
+  --
+  -- @
+  -- 'traverseFC' f ≡ 'itraverseFC' ('const' f)
+  -- @
+  itraverseFC ::
+    forall m z f g.
+    Applicative m =>
+    (forall x. IndexF (t f z) x -> f x -> m (g x)) ->
+    t f z ->
+    m (t g z)
+
+imapFCDefault ::
+  forall t f g z.
+  TraversableFCWithIndex t =>
+  (forall x. IndexF (t f z) x -> f x -> g x)
+  -> t f z
+  -> t g z
+imapFCDefault f = runIdentity #. itraverseFC (\i x -> Identity (f i x))
+{-# INLINEABLE imapFCDefault #-}
+
+ifoldMapFCDefault ::
+  forall t m z f.
+  TraversableFCWithIndex t =>
+  Monoid m =>
+  (forall x. IndexF (t f z) x -> f x -> m) ->
+  t f z ->
+  m
+ifoldMapFCDefault f = getConst #. itraverseFC (\i x -> Const (f i x))
+{-# INLINEABLE ifoldMapFCDefault #-}
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
@@ -1,4 +1,5 @@
 {-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# Language PatternGuards #-}
 {-# Language PolyKinds #-}
 {-# Language TypeApplications, ScopedTypeVariables #-}
@@ -36,6 +37,10 @@
   , elemAtMaybe
   , elemAtUnsafe
 
+    -- * Indexing with Fin
+  , indicesUpTo
+  , indicesOf
+
     -- * Update
   , insertAt
   , insertAtMaybe
@@ -74,6 +79,8 @@
   , unfoldrM
   , unfoldrWithIndex
   , unfoldrWithIndexM
+  , iterateN
+  , iterateNM
 
     -- * Splitting and joining
     -- ** General
@@ -90,15 +97,19 @@
   ) where
 
 import qualified Data.Vector as Vector
-import Data.Functor.Compose
 import Data.Coerce
+import Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
+import Data.Functor.Compose
+import Data.Functor.WithIndex (FunctorWithIndex(imap))
 import Data.Vector.Mutable (MVector)
 import qualified Data.Vector.Mutable as MVector
 import Control.Monad.ST
 import Data.Functor.Identity
+import Data.Parameterized.Fin
 import Data.Parameterized.NatRepr
 import Data.Parameterized.NatRepr.Internal
 import Data.Proxy
+import Data.Traversable.WithIndex (TraversableWithIndex(itraverse))
 import Prelude hiding (length,reverse,zipWith)
 import Numeric.Natural
 
@@ -150,7 +161,36 @@
 elemAtUnsafe n (Vector xs) = xs Vector.! n
 {-# INLINE elemAtUnsafe #-}
 
+--------------------------------------------------------------------------------
 
+indicesUpTo :: NatRepr n -> Vector (n + 1) (Fin (n + 1))
+indicesUpTo n =
+  iterateN
+    n
+    (viewFin
+      (\x ->
+        case testStrictLeq (incNat x) (incNat n) of
+          Left LeqProof -> mkFin (incNat x)
+          Right Refl -> mkFin n))
+    (case addPrefixIsLeq n (knownNat @1) of
+       LeqProof -> mkFin (knownNat @0))
+
+indicesOf :: Vector n a -> Vector n (Fin n)
+indicesOf v@(Vector _) = -- Pattern match to bring 1 <= n into scope
+  case minusPlusCancel (length v) (knownNat @1) of
+    Refl -> indicesUpTo (decNat (length v))
+
+instance FunctorWithIndex (Fin n) (Vector n) where
+  imap f v = zipWith f (indicesOf v) v
+
+instance FoldableWithIndex (Fin n) (Vector n) where
+  ifoldMap f v = foldMap (uncurry f) (imap (,) v)
+
+instance TraversableWithIndex (Fin n) (Vector n) where
+  itraverse f v = traverse (uncurry f) (imap (,) v)
+
+--------------------------------------------------------------------------------
+
 -- | Insert an element at the given index.
 -- @O(n)@.
 insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a
@@ -320,7 +360,6 @@
   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.
@@ -519,6 +558,22 @@
        -> b
        -> Vector (h + 1) a
 unfoldr h gen start = unfoldrWithIndex h (\_ v -> gen v) start
+
+-- | Build a vector by repeatedly applying a monadic function to a seed value.
+--
+-- Compare to 'Vector.iterateNM'.
+iterateNM :: Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
+iterateNM h f start =
+  case isZeroNat h of
+    ZeroNat -> pure (singleton start)
+    NonZeroNat -> cons start <$> unfoldrM (predNat h) (fmap dup . f) start
+  where dup x = (x, x)
+
+-- | Build a vector by repeatedly applying a function to a seed value.
+--
+-- Compare to 'Vector.iterateN'
+iterateN :: NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
+iterateN h f start = runIdentity (iterateNM h (Identity . f) start)
 
 --------------------------------------------------------------------------------
 
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -27,6 +28,7 @@
 import qualified Data.Parameterized.Ctx.Proofs as P
 import           Data.Parameterized.Some
 import           Data.Parameterized.TraversableFC
+import           Data.Parameterized.TraversableFC.WithIndex
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range
@@ -58,13 +60,25 @@
 
 instance ShowF Payload
 
-
 twiddle :: Payload a -> Payload a
 twiddle (IntPayload n) = IntPayload (n+1)
 twiddle (StringPayload str) = StringPayload (str++"asdf")
 twiddle (BoolPayload b) = BoolPayload (not b)
 
+twaddle :: Payload a -> Payload a
+twaddle (IntPayload n) = IntPayload (n-1)
+twaddle (StringPayload str) = StringPayload (reverse str)
+twaddle (BoolPayload b) = BoolPayload (not b)
 
+newtype Fun = Fun (forall a. Payload a -> Payload a)
+
+instance Show Fun where
+  show _ = "unshowable"
+
+-- | Functions for e.g. testing functor laws
+funs :: [Fun]
+funs = [Fun twiddle, Fun twaddle, Fun id]
+
 ----------------------------------------------------------------------
 -- Create another parameterized type for testing.  This one is not a
 -- GADT, which will require some interesting implementation tricks.
@@ -323,6 +337,44 @@
         let (x', x'') = C.unzip zipped
         assert $ isJust $ testEquality x x'
         assert $ isJust $ testEquality x x''
+
+   , testProperty "fmapFC_identity" $ property $
+     do Some x <- mkUAsgn <$> forAll genSomePayloadList
+        assert $ isJust $ testEquality x (fmapFC id 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)
+
+   , testProperty "imapFC_index_noop" $ property $
+     do Some x <- mkUAsgn <$> forAll genSomePayloadList
+        assert $
+          isJust $
+            testEquality x (imapFC (\idx _ -> x U.! idx) x)
+
+   , 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)
+
+   , testProperty "ifoldMapFC/foldMapFC" $ property $
+     do Some x <- mkUAsgn <$> forAll genSomePayloadList
+        assert $ foldMapFC show x == ifoldMapFC (const show) 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))
 
    , testCaseSteps "explicit indexing (unsafe)" $ \step -> do
        let mkUPayload :: U.Assignment Payload TestCtx
diff --git a/test/Test/Fin.hs b/test/Test/Fin.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Fin.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# Language CPP #-}
+
+module Test.Fin
+  ( finTests
+  , genFin
+  )
+where
+
+import           Numeric.Natural (Natural)
+
+import           Hedgehog
+import qualified Hedgehog.Gen as HG
+import           Hedgehog.Range (linear)
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.HUnit (assertBool, testCase)
+
+import           Data.Parameterized.NatRepr
+import           Data.Parameterized.Fin
+import           Data.Parameterized.Some (Some(Some))
+
+#if __GLASGOW_HASKELL__ >= 806
+import qualified Hedgehog.Classes as HC
+#endif
+
+genFin :: (0 <= 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)
+     return $
+       case testLeq (incNat x) n of
+         Just LeqProof -> mkFin x
+         Nothing -> error "Impossible"
+
+finTests :: IO TestTree
+finTests =
+  testGroup "Fin" <$>
+    return
+      [ testCase "minBound <= maxBound (1)" $
+          assertBool
+            "minBound <= maxBound (1)"
+            ((minBound :: Fin 1) <= (minBound :: Fin 1))
+      , testCase "minBound <= maxBound (2)" $
+          assertBool
+            "minBound <= maxBound (2)"
+            ((minBound :: Fin 2) <= (minBound :: Fin 2))
+
+#if __GLASGOW_HASKELL__ >= 806
+      , testCase "Eq-Fin-laws-1" $
+          assertBool "Eq-Fin-laws-1" =<<
+            HC.lawsCheck (HC.eqLaws (genFin (knownNat @1)))
+
+      , testCase "Ord-Fin-laws-1" $
+          assertBool "Ord-Fin-laws-1" =<<
+            HC.lawsCheck (HC.ordLaws (genFin (knownNat @1)))
+
+      , testCase "Eq-Fin-laws-10" $
+          assertBool "Eq-Fin-laws-10" =<<
+            HC.lawsCheck (HC.eqLaws (genFin (knownNat @10)))
+
+      , testCase "Ord-Fin-laws-10" $
+          assertBool "Ord-Fin-laws-10" =<<
+            HC.lawsCheck (HC.ordLaws (genFin (knownNat @10)))
+#endif
+      ]
diff --git a/test/Test/List.hs b/test/Test/List.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/List.hs
@@ -0,0 +1,29 @@
+module Test.List
+  ( tests
+  ) where
+
+import           Control.Monad.Identity
+import           Data.Functor.Const
+import qualified Data.Parameterized.List as PL
+import           Data.Parameterized.Some
+import           Test.Tasty
+import           Test.Tasty.HUnit
+
+-- | Test ifoldlM indexing is correct by summing a list using it.
+testIfoldlMSum :: [Integer] -> TestTree
+testIfoldlMSum l =
+  testCase ("ifoldlMSum " ++ show l) $
+    case PL.fromListWith (Some . Const) l of
+      Some pl ->
+        let expected = sum l
+            actual = PL.ifoldlM (\r i v -> Identity $ r + if pl PL.!! i == v then getConst v else 0) 0 pl
+        in expected @?= runIdentity actual
+
+
+tests :: TestTree
+tests = testGroup "List"
+  [ testIfoldlMSum []
+  , testIfoldlMSum [1]
+  , testIfoldlMSum [1,2]
+  , testIfoldlMSum [1,2,3]
+  ]
diff --git a/test/Test/TH.hs b/test/Test/TH.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/TH.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.TH
+  ( thTests
+  )
+where
+
+import           Test.Tasty
+import           Test.Tasty.HUnit
+
+import           Control.Monad (when)
+import           Data.Parameterized.Classes
+import           Data.Parameterized.NatRepr
+import           Data.Parameterized.TH.GADT
+import           GHC.TypeNats
+
+data T1 = A | B | C
+$(mkRepr ''T1)
+$(mkKnownReprs ''T1)
+$(return [])
+instance TestEquality T1Repr where
+  testEquality = $(structuralTypeEquality [t|T1Repr|] [])
+deriving instance Show (T1Repr t)
+
+data T2 = T2_1 T1 | T2_2 Nat
+$(mkRepr ''T2)
+$(mkKnownReprs ''T2)
+$(return [])
+instance TestEquality T2Repr where
+  testEquality = $(structuralTypeEquality [t|T2Repr|]
+                    [ (AnyType, [|testEquality|]) ])
+deriving instance Show (T2Repr t)
+
+eqTest :: (TestEquality f, Show (f a), Show (f b)) => f a -> f b -> IO ()
+eqTest a b =
+  when (not (isJust (testEquality a b))) $ assertFailure $ show a ++ " /= " ++ show b
+
+neqTest :: (TestEquality f, Show (f a), Show (f b)) => f a -> f b -> IO ()
+neqTest a b =
+  when (isJust (testEquality a b)) $ assertFailure $ show a ++ " == " ++ show b
+
+thTests :: IO TestTree
+thTests = testGroup "TH" <$> return
+  [ testCase "Repr equality test" $ do
+      -- T1
+      ARepr `eqTest` ARepr
+      ARepr `neqTest` BRepr
+      BRepr `eqTest` BRepr
+      BRepr `neqTest` CRepr
+      -- T2
+      T2_1Repr ARepr `eqTest` T2_1Repr ARepr
+      T2_2Repr (knownNat @5) `eqTest` T2_2Repr (knownNat @5)
+      T2_1Repr ARepr `neqTest` T2_1Repr CRepr
+      T2_2Repr (knownNat @5) `neqTest` T2_2Repr (knownNat @9)
+      T2_1Repr BRepr `neqTest` T2_2Repr (knownNat @4)
+
+  , testCase "KnownRepr test" $ do
+      -- T1
+      let aRepr = knownRepr :: T1Repr 'A
+          bRepr = knownRepr :: T1Repr 'B
+          cRepr = knownRepr :: T1Repr 'C
+      aRepr `eqTest` ARepr
+      bRepr `eqTest` BRepr
+      cRepr `eqTest` CRepr
+      --T2
+      let t2ARepr = knownRepr :: T2Repr ('T2_1 'A)
+          t2BRepr = knownRepr :: T2Repr ('T2_1 'B)
+          t25Repr = knownRepr :: T2Repr ('T2_2 5)
+      t2ARepr `eqTest` T2_1Repr ARepr
+      t2BRepr `eqTest` T2_1Repr BRepr
+      t25Repr `eqTest` T2_2Repr (knownNat @5)
+      t2ARepr `neqTest` t2BRepr
+      t2ARepr `neqTest` t25Repr
+      t2BRepr `neqTest` t25Repr
+  ]
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
--- a/test/Test/Vector.hs
+++ b/test/Test/Vector.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeApplications #-}
 {-# Language CPP #-}
 {-# Language DataKinds #-}
@@ -18,9 +19,12 @@
 where
 
 import           Data.Functor.Const (Const(..))
+import           Data.Functor.WithIndex (imap)
+import           Data.Foldable.WithIndex (ifoldMap)
 import           Data.Maybe (isJust)
 import qualified Data.List as List
 import qualified Data.Parameterized.Context as Ctx
+import           Data.Parameterized.Fin
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
 import           Data.Parameterized.Vector
@@ -29,15 +33,42 @@
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range
-import           Prelude hiding (take, reverse)
+import           Numeric.Natural (Natural)
+import           Prelude hiding (take, reverse, length)
 import qualified Prelude as P
+import           Test.Fin (genFin)
 import           Test.Tasty
 import           Test.Tasty.Hedgehog
 import           Test.Context (genSomePayloadList, mkUAsgn)
 
+#if __GLASGOW_HASKELL__ >= 806
+import qualified Hedgehog.Classes as HC
+import           Test.Tasty.HUnit (assertBool, testCase)
+#endif
 
-genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)
-genVector genElem =
+data SomeVector a = forall n. SomeVector (Vector n a)
+
+instance Show a => Show (SomeVector a) where
+  show (SomeVector v) = show v
+
+genVectorOfLength :: (Monad m) => NatRepr n -> GenT m a -> GenT m (Vector (n + 1) a)
+genVectorOfLength n genElem =
+  do let w = widthVal n
+     l <- HG.list (linear (w + 1) (w + 1)) genElem
+     case testLeq (knownNat @1) (incNat n) of
+       Nothing -> error "testLeq in genSomeVector"
+       Just LeqProof ->
+         case fromList (incNat n) l of
+           Just v -> return v
+           Nothing -> error ("fromList failure for size " <> show w)
+
+genSomeVector :: (Monad m) => GenT m a -> GenT m (SomeVector a)
+genSomeVector genElem =
+  do Some len <- mkNatRepr <$> HG.integral (linear 0 (99 :: Natural))
+     SomeVector <$> genVectorOfLength len genElem
+
+genVectorKnownLength :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)
+genVectorKnownLength genElem =
   do let n = knownNat
          w = widthVal n
      l <- HG.list (constant w w) genElem
@@ -48,17 +79,33 @@
 genOrdering :: Monad m => GenT m Ordering
 genOrdering = HG.element [ LT, EQ, GT ]
 
-
 instance Show (a -> b) where
   show _ = "unshowable"
 
+-- Used to test e.g., 'fmap (g . f) = fmap g . fmap f' and 'imap (const f) =
+-- fmap f'.
+orderingEndomorphisms :: [Ordering -> Ordering]
+orderingEndomorphisms =
+  [ const EQ
+  , id
+  , \case
+      EQ -> EQ
+      LT -> GT
+      GT -> LT
+  , \case
+      LT -> EQ
+      EQ -> GT
+      GT -> LT
+  ]
 
 -- We use @Ordering@ just because it's simple
 vecTests :: IO TestTree
 vecTests = testGroup "Vector" <$> return
   [ testProperty "reverse100" $ property $
-    do v <- forAll $ genVector @100 genOrdering
-       v === (reverse $ reverse v)
+    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
@@ -66,7 +113,7 @@
 
   , testProperty "split-join" $ property $
     do let n = knownNat @5
-       v <- forAll $ genVector @(5 * 5) genOrdering
+       v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering
        v === (join n $ split n (knownNat @5) v)
 
   -- @cons@ is the same for vectors or lists
@@ -145,4 +192,81 @@
                           testEquality
                             (a Ctx.! Ctx.lastIndex sz) lastElem)
                    (getConst (a' Ctx.! Ctx.lastIndex sz))
-    ]
+
+  -- 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
+
+  , 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)
+
+  , testProperty "iterateN-range" $ property $
+    do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))
+       toList (iterateN len (+1) 0) === [0..(natValue len)]
+
+  , testProperty "indicesOf-range" $ property $
+    do SomeVector v <- forAll $ genSomeVector genOrdering
+       toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]
+
+  , testProperty "imap-const" $ property $
+    do f <- forAll $ HG.element orderingEndomorphisms
+       SomeVector v <- forAll $ genSomeVector genOrdering
+       imap (const f) v === fmap f v
+
+  , 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
+
+  , testProperty "imap-const-indicesOf" $ property $
+    do SomeVector v <- forAll $ genSomeVector genOrdering
+       imap const v === indicesOf v
+
+  , testProperty "imap-elemAt" $ property $
+    do SomeVector v <- forAll $ genSomeVector genOrdering
+       imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v
+
+  , testProperty "Ord-Eq-VectorIndex" $ property $
+    do i <- forAll $ genFin (knownNat @10)
+       j <- forAll $ genFin (knownNat @10)
+       (i == j) === (compare i j == EQ)
+
+#if __GLASGOW_HASKELL__ >= 806
+  -- Test a few different sizes since the types force each test to use a
+  -- specific size vector.
+  , testCase "Eq-Vector-laws-1" $
+      assertBool "Eq-Vector-laws-1" =<<
+        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @1 genOrdering))
+  , testCase "Eq-Vector-laws-10" $
+      assertBool "Eq-Vector-laws-10" =<<
+        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @10 genOrdering))
+  , testCase "Show-Vector-laws-1" $
+      assertBool "Show-Vector-laws-1" =<<
+        HC.lawsCheck (HC.showLaws (genVectorKnownLength @1 genOrdering))
+  , testCase "Show-Vector-laws-10" $
+      assertBool "Show-Vector-laws-10" =<<
+        HC.lawsCheck (HC.showLaws (genVectorKnownLength @10 genOrdering))
+  , testCase "Foldable-Vector-laws-1" $
+      assertBool "Foldable-Vector-laws-1" =<<
+        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @1))
+  , testCase "Foldable-Vector-laws-10" $
+      assertBool "Foldable-Vector-laws-10" =<<
+        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @10))
+  , testCase "Traversable-Vector-laws-1" $
+      assertBool "Traversable-Vector-laws-1" =<<
+        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @1))
+  , testCase "Traversable-Vector-laws-10" $
+      assertBool "Traversable-Vector-laws-10" =<<
+        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @10))
+#endif
+  ]
diff --git a/test/UnitTest.hs b/test/UnitTest.hs
--- a/test/UnitTest.hs
+++ b/test/UnitTest.hs
@@ -3,8 +3,11 @@
 import Test.Tasty.Runners.AntXML
 
 import qualified Test.Context
+import qualified Test.Fin
+import qualified Test.List
 import qualified Test.NatRepr
 import qualified Test.SymbolRepr
+import qualified Test.TH
 import qualified Test.Vector
 
 main :: IO ()
@@ -20,7 +23,10 @@
 tests :: IO TestTree
 tests = testGroup "ParameterizedUtils" <$> sequence
   [ Test.Context.contextTests
+  , pure Test.List.tests
+  , Test.Fin.finTests
   , Test.NatRepr.natTests
   , Test.SymbolRepr.symbolTests
+  , Test.TH.thTests
   , Test.Vector.vecTests
   ]