diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,26 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.1.3.0 -- *2021 Mar 23*
+
+  * Add support for GHC 9.
+  * In the `Context` module:
+    * Added `sizeToNatRepr` function for converting a `Context` `Size`.
+    * Added `unzip` to unzip an `Assignment` of `Product(Pair)` into a
+      separate `Assignment` for each element of the `Pair` (the
+      inverse of the `zipWith Pair` operation).
+    * Added `flattenAssignment` to convert an `Assignment` of
+      `Assignment` into an `Assignment` of `CtxFlatten`.  Also adds
+      `flattenSize` to combine the sizes of each context into the size
+      of the corresponding `CtxFlatten`.
+  * In the `Vector` module:
+    * Added `fromAssignment` and `toAssignment` to allow conversions
+      between `Assignment` and `Vector`.
+    * Added `unsnoc`, `unfoldr`, `unfoldrM`, `unfoldrWithIndex`, and
+      `unfoldrWithIndexM` functions.
+  * Various haddock documentation updates and corrections.
+  * Updated the Cabal specification to Cabal-version 2.2.
+
+
 ## 2.1.2 -- *2021 Jan 25*
 
   * Added `SomeSym` and `viewSomeSym` for existentially hidden Symbol
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,12 +1,12 @@
+Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.1.2.0
+Version:       2.1.3.0
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com, kquick@galois.com
 stability:     stable
 Build-type:    Simple
-Cabal-version: >= 1.10
 Copyright:     ©2016-2021 Galois, Inc.
-License:       BSD3
+License:       BSD-3-Clause
 License-file:  LICENSE
 category:      Data Structures, Dependent Types
 Synopsis: Classes and data structures for working with data-kind indexed types
@@ -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.3, GHC==8.10.1
+tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.1
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -34,17 +34,31 @@
   type: git
   location: https://github.com/GaloisInc/parameterized-utils
 
+
+common bldflags
+  ghc-options: -Wall
+               -Wcompat
+               -Wpartial-fields
+               -Wincomplete-uni-patterns
+               -Werror=incomplete-patterns
+               -Werror=missing-methods
+               -Werror=overlapping-patterns
+               -fhide-source-paths
+  default-language: Haskell2010
+
+
 library
+  import: bldflags
   build-depends: base >= 4.10 && < 5
                , base-orphans   >=0.8.2 && <0.9
                , th-abstraction >=0.3  && <0.5
-               , constraints    >=0.10 && <0.13
+               , constraints    >=0.10 && <0.14
                , containers
                , deepseq
                , ghc-prim
                , hashable       >=1.2  && <1.4
                , hashtables     ==1.2.*
-               , lens           >=4.16 && <4.20
+               , lens           >=4.16 && <5.1
                , mtl
                , template-haskell
                , text
@@ -88,20 +102,15 @@
   other-modules:
     Data.Parameterized.NatRepr.Internal
 
-  ghc-options: -Wall
-  default-language: Haskell2010
-
   if flag(unsafe-operations)
     cpp-options: -DUNSAFE_OPS
 
 
 test-suite parameterizedTests
+  import: bldflags
   type: exitcode-stdio-1.0
   hs-source-dirs: test
 
-  ghc-options: -Wall
-  default-language: Haskell2010
-
   main-is: UnitTest.hs
   other-modules:
     Test.Context
@@ -117,7 +126,7 @@
                , lens
                , mtl
                , parameterized-utils
-               , tasty >= 1.2 && < 1.4
+               , tasty >= 1.2 && < 1.5
                , tasty-ant-xml == 1.1.*
                , tasty-hunit >= 0.9 && < 0.11
                , tasty-hedgehog
diff --git a/src/Data/Parameterized/All.hs b/src/Data/Parameterized/All.hs
--- a/src/Data/Parameterized/All.hs
+++ b/src/Data/Parameterized/All.hs
@@ -46,11 +46,12 @@
   ) where
 
 import Data.Functor.Const (Const(..))
+import Data.Kind
 
 import Data.Parameterized.Classes
 import Data.Parameterized.TraversableF
 
-newtype All (f :: k -> *) = All { getAll :: forall x. f x }
+newtype All (f :: k -> Type) = All { getAll :: forall x. f x }
 
 instance FunctorF All where
   fmapF f (All a) = All (f a)
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
@@ -80,7 +80,7 @@
 --   all the types of a family.  We generally use this to witness
 --   the fact that the type parameter to @rtp@ is a phantom type
 --   by giving an implementation in terms of Data.Coerce.coerce.
-class CoercibleF (rtp :: k -> *) where
+class CoercibleF (rtp :: k -> Type) where
   coerceF :: rtp a -> rtp b
 
 instance CoercibleF (Const x) where
@@ -97,7 +97,7 @@
 -- type when they are equal. Thus this can be implemented over
 -- parameterized types that are unable to provide evidence that their
 -- type arguments are equal.
-class EqF (f :: k -> *) where
+class EqF (f :: k -> Type) where
   eqF :: f a -> f a -> Bool
 
 instance Eq a => EqF (Const a) where
@@ -179,7 +179,7 @@
 --
 -- Minimal complete definition: either 'compareF' or 'leqF'.
 -- Using 'compareF' can be more efficient for complex types.
-class TestEquality ktp => OrdF (ktp :: k -> *) where
+class TestEquality ktp => OrdF (ktp :: k -> Type) where
   {-# MINIMAL compareF | leqF #-}
 
   compareF :: ktp x -> ktp y -> OrderingF x y
@@ -219,7 +219,7 @@
 
 -- | Compare two values, and if they are equal compare the next values,
 -- otherwise return LTF or GTF
-lexCompareF :: forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k)
+lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k)
              .  OrdF f
             => f a
             -> f b
@@ -230,7 +230,7 @@
 -- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
 -- for the \"inner\" functor. The type-level evidence of equality is deduced
 -- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
-ordFCompose :: forall k l (f :: k -> *) (g :: l -> k) x y.
+ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                 (forall w z. f w -> f z -> OrderingF w z)
             -> Compose f g x
             -> Compose f g y
@@ -252,7 +252,7 @@
 -- To implement @'ShowF' g@, one should implement an instance @'Show'
 -- (g tp)@ for all argument types @tp@, then write an empty instance
 -- @instance 'ShowF' g@.
-class ShowF (f :: k -> *) where
+class ShowF (f :: k -> Type) where
   -- | Provides a show instance for each type.
   withShow :: p f -> q tp -> (Show (f tp) => a) -> a
 
@@ -275,8 +275,8 @@
 ------------------------------------------------------------------------
 -- IxedF
 
-type family IndexF       (m :: *) :: k -> *
-type family IxValueF     (m :: *) :: k -> *
+type family IndexF       (m :: Type) :: k -> Type
+type family IxValueF     (m :: Type) :: k -> Type
 
 -- | Parameterized generalization of the lens @Ixed@ class.
 class IxedF k m where
@@ -315,7 +315,7 @@
 {-# INLINE defaultSalt #-}
 
 -- | A parameterized type that is hashable on all instances.
-class HashableF (f :: k -> *) where
+class HashableF (f :: k -> Type) where
   hashWithSaltF :: Int -> f tp -> Int
 
   -- | Hash with default salt.
@@ -355,5 +355,5 @@
 -- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of
 -- singleton types indexed by @k@), and an index parameter @ctx@ of
 -- kind @k@.
-class KnownRepr (f :: k -> *) (ctx :: k) where
+class KnownRepr (f :: k -> Type) (ctx :: k) where
   knownRepr :: f ctx
diff --git a/src/Data/Parameterized/ClassesC.hs b/src/Data/Parameterized/ClassesC.hs
--- a/src/Data/Parameterized/ClassesC.hs
+++ b/src/Data/Parameterized/ClassesC.hs
@@ -26,17 +26,18 @@
   ) where
 
 import Data.Type.Equality ((:~:)(..))
+import Data.Kind
 import Data.Maybe (isJust)
 import Data.Parameterized.Classes (OrderingF, toOrdering)
 import Data.Parameterized.Some (Some(..))
 
-class TestEqualityC (t :: (k -> *) -> *) where
+class TestEqualityC (t :: (k -> Type) -> Type) where
   testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))
                 -> t f
                 -> t f
                 -> Bool
 
-class TestEqualityC t => OrdC (t :: (k -> *) -> *) where
+class TestEqualityC t => OrdC (t :: (k -> Type) -> Type) where
   compareC :: (forall x y. f x -> g y -> OrderingF x y)
            -> t f
            -> t g
diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs
--- a/src/Data/Parameterized/Compose.hs
+++ b/src/Data/Parameterized/Compose.hs
@@ -21,13 +21,14 @@
   ) where
 
 import Data.Functor.Compose
+import Data.Kind
 import Data.Orphans () -- For the TestEquality (Compose f g) instance
 import Data.Type.Equality
 
 -- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
 --
 -- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
-testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
+testEqualityComposeBare :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                            (forall w z. f w -> f z -> Maybe (w :~: z))
                         -> Compose f g x
                         -> Compose f g y
diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs
--- a/src/Data/Parameterized/Context.hs
+++ b/src/Data/Parameterized/Context.hs
@@ -64,6 +64,9 @@
   , traverseAndCollect
   , traverseWithIndex_
   , dropPrefix
+  , unzip
+  , flattenAssignment
+  , flattenSize
 
     -- * Context extension and embedding utilities
   , CtxEmbedding(..)
@@ -97,9 +100,13 @@
   , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6
   ) where
 
+import           Prelude hiding (unzip)
+
 import           Control.Applicative (liftA2)
 import           Control.Lens hiding (Index, (:>), Empty)
 import           Data.Functor (void)
+import           Data.Functor.Product (Product(Pair))
+import           Data.Kind
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
 import           GHC.TypeLits (Nat, type (-))
@@ -157,7 +164,6 @@
   return vm
 {-# INLINABLE toVector #-}
 
-
 -- | Utility function for testing if @xs@ is an assignment with
 --   `prefix` as a prefix, and computing the tail of xs
 --   not in the prefix, if so.
@@ -187,9 +193,39 @@
       Just Refl -> success Empty
       Nothing   -> err
 
+-- | Unzip an assignment of pairs into a pair of assignments.
+--
+-- This is the inverse of @'zipWith' 'Pair'@.
+unzip :: Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)
+unzip fgs =
+  case viewAssign fgs of
+    AssignEmpty -> (empty, empty)
+    AssignExtend rest (Pair f g) ->
+      let (fs, gs) = unzip rest
+      in (extend fs f, extend gs g)
 
+-- | Flattens a nested assignment over a context of contexts @ctxs :: Ctx (Ctx
+-- a)@ into a flat assignment over the flattened context @CtxFlatten ctxs@.
+flattenAssignment ::
+  Assignment (Assignment f) ctxs ->
+  Assignment f (CtxFlatten ctxs)
+flattenAssignment ctxs =
+  case viewAssign ctxs of
+    AssignEmpty -> empty
+    AssignExtend ctxs' ctx -> flattenAssignment ctxs' <++> ctx
 
+-- | Given the size of each context in @ctxs@, returns the size of @CtxFlatten
+-- ctxs@.  You can obtain the former from any nested assignment @Assignment
+-- (Assignment f) ctxs@, by calling @fmapFC size@.
+flattenSize ::
+  Assignment Size ctxs ->
+  Size (CtxFlatten ctxs)
+flattenSize a =
+  case viewAssign a of
+    AssignEmpty -> zeroSize
+    AssignExtend b s -> addSize (flattenSize b) s
 
+
 --------------------------------------------------------------------------------
 -- Patterns
 
@@ -272,16 +308,16 @@
                        (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)
 ctxeAssignment = lens _ctxeAssignment (\s v -> s { _ctxeAssignment = v })
 
-class ApplyEmbedding (f :: Ctx k -> *) where
+class ApplyEmbedding (f :: Ctx k -> Type) where
   applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx'
 
-class ApplyEmbedding' (f :: Ctx k -> k' -> *) where
+class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where
   applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
 
-class ExtendContext (f :: Ctx k -> *) where
+class ExtendContext (f :: Ctx k -> Type) where
   extendContext :: Diff ctx ctx' -> f ctx -> f ctx'
 
-class ExtendContext' (f :: Ctx k -> k' -> *) where
+class ExtendContext' (f :: Ctx k -> k' -> Type) where
   extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v
 
 instance ApplyEmbedding' Index where
@@ -384,7 +420,7 @@
 -- > CurryAssignment (EmptyCtx ::> a) f x = f a -> x
 -- > CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
 -- > CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x
-type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where
+type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) (x :: Type) :: Type where
    CurryAssignment EmptyCtx    f x = x
    CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> 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
@@ -57,6 +57,7 @@
   , addSize
   , SizeView(..)
   , viewSize
+  , sizeToNatRepr
   , KnownContext(..)
     -- * Diff
   , Diff
@@ -120,6 +121,7 @@
 
 import Data.Parameterized.Classes
 import Data.Parameterized.Ctx
+import Data.Parameterized.NatRepr
 import Data.Parameterized.Some
 import Data.Parameterized.TraversableFC
 
@@ -168,6 +170,16 @@
 viewSize SizeZero = ZeroSize
 viewSize (SizeSucc s) = IncSize s
 
+-- | Convert a 'Size' into a 'NatRepr'.
+sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
+sizeToNatRepr sz =
+  case viewSize sz of
+    ZeroSize -> knownRepr
+    IncSize sz' ->
+      let oldRep = sizeToNatRepr sz'
+      in case plusComm (knownRepr :: NatRepr 1) oldRep of
+           Refl -> incNat oldRep
+
 ------------------------------------------------------------------------
 -- Size
 
@@ -332,8 +344,8 @@
   IndexViewLast _ -> lastIndex (addSize sz sz')
   IndexViewInit idx' -> skipIndex (extendIndexAppendLeft sz (decSize sz') idx')
 
--- | Given a size @n@, an initial value @v0@, and a function @f@, the
--- expression @forIndex n v0 f@ calls @f@ on each index less than @n@
+-- | Given a size @n@, a function @f@, and an initial value @v0@, the
+-- expression @forIndex n f v0@ calls @f@ on each index less than @n@
 -- starting from @0@ and @v0@, with the value @v@ obtained from the
 -- last call.
 forIndex :: forall ctx r
@@ -374,9 +386,9 @@
 forIndexRangeImpl i (SizeSucc sz) d f r =
   forIndexRangeImpl (i-1) sz (LDiffThere d) f r
 
--- | Given an index @i@, size @n@, a function @f@, value @v@, and a
--- function @f@, the expression @forIndexRange i n f v@ is equivalent
--- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@
+-- | Given an index @i@, size @n@, a function @f@, and a value @v@,
+-- the expression @forIndexRange i n f v@ is equivalent
+-- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
 -- otherwise.
 forIndexRange :: Int
               -> Size ctx
@@ -484,6 +496,9 @@
 empty :: Assignment f 'EmptyCtx
 empty = AssignmentEmpty
 
+-- n.b. see 'singleton' in Data/Parameterized/Context.hs
+
+-- | Extend an indexed vector with a new entry.
 extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
 extend asgn e = AssignmentExtend asgn e
 
@@ -506,7 +521,7 @@
 type instance IxValueF (Assignment (f :: k -> Type) ctx) = f
 
 instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
-  ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
+  ixF :: Index ctx x -> Lens.Traversal' (Assignment f ctx) (f x)
   ixF idx f = adjustM f idx
 
 instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
@@ -544,7 +559,7 @@
 testEq _ AssignmentExtend{} AssignmentEmpty = Nothing
 
 instance TestEqualityFC Assignment where
-   testEqualityFC = testEq
+   testEqualityFC f = testEq f
 instance TestEquality f => TestEquality (Assignment f) where
    testEquality x y = testEq testEquality x y
 instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where
@@ -565,7 +580,7 @@
               EQF -> EQF
 
 instance OrdFC Assignment where
-  compareFC = compareAsgn
+  compareFC f = compareAsgn f
 
 instance OrdF f => OrdF (Assignment f) where
   compareF = compareAsgn compareF
@@ -598,11 +613,11 @@
   foldMapFC = foldMapFCDefault
 
 instance TraversableFC Assignment where
-  traverseFC = traverseF
+  traverseFC f = traverseF f
 
 -- | Map assignment
 map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
-map = fmapFC
+map f = fmapFC f
 
 traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
            . Applicative m
@@ -616,7 +631,7 @@
 toList :: (forall tp . f tp -> a)
        -> Assignment f c
        -> [a]
-toList = toListFC
+toList f = toListFC f
 
 zipWithM :: Applicative m
          => (forall tp . f tp -> g tp -> m (h tp))
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
@@ -29,6 +29,7 @@
   , addSize
   , SizeView(..)
   , viewSize
+  , sizeToNatRepr
     -- * Diff
   , Diff
   , noDiff
@@ -100,6 +101,8 @@
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Ctx
 import           Data.Parameterized.Ctx.Proofs
+import           Data.Parameterized.NatRepr
+import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr))
 import           Data.Parameterized.Some
 import           Data.Parameterized.TraversableFC
 
@@ -136,6 +139,10 @@
 viewSize (Size 0) = unsafeCoerce ZeroSize
 viewSize (Size n) = assert (n > 0) (unsafeCoerce (IncSize (Size (n-1))))
 
+-- | Convert a 'Size' into a 'NatRepr'.
+sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
+sizeToNatRepr (Size n) = NatRepr (fromIntegral n)
+
 instance Show (Size ctx) where
   show (Size i) = show i
 
@@ -290,9 +297,9 @@
 extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
 extendIndexAppendLeft (Size l) _ (Index idx) = Index (idx + l)
 
--- | Given a size @n@, an initial value @v0@, and a function @f@, the
--- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is
--- zero, and @f (forIndex (n-1) v0) n@ otherwise.  Unlike the safe
+-- | Given a size @n@, a function @f@, and an initial value @v0@, the
+-- expression @forIndex n f v0@ is equivalent to @v0@ when @n@ is
+-- zero, and @f (forIndex (n-1) f v0) n@ otherwise.  Unlike the safe
 -- version, which starts from 'Index' @0@ and increments 'Index'
 -- values, this version starts at 'Index' @(n-1)@ and decrements
 -- 'Index' values to 'Index' @0@.
@@ -306,9 +313,9 @@
     ZeroSize -> r
     IncSize p -> f (forIndex p (coerce f) r) (nextIndex p)
 
--- | Given an index @i@, size @n@, a function @f@, value @v@, and a
--- function @f@, the expression @forIndex i n f v@ is equivalent to
--- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@
+-- | Given an index @i@, size @n@, a function @f@, and a value @v@,
+-- the expression @forIndex i n f v@ is equivalent to
+-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
 -- otherwise.
 forIndexRange :: forall ctx r
                . Int
@@ -794,6 +801,9 @@
 empty :: Assignment f EmptyCtx
 empty = Assignment Empty
 
+-- n.b. see 'singleton' in Data/Parameterized/Context.hs
+
+-- | Extend an indexed vector with a new entry.
 extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
 extend (Assignment x) y = Assignment $ append x (BalLeaf y)
 
@@ -870,7 +880,7 @@
   ixF' idx f = adjustM f idx
 
 instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
-  ixF = ixF'
+  ixF idx = ixF' idx
 
 -- This is an unsafe version of update that changes the type of the expression.
 unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
diff --git a/src/Data/Parameterized/Ctx.hs b/src/Data/Parameterized/Ctx.hs
--- a/src/Data/Parameterized/Ctx.hs
+++ b/src/Data/Parameterized/Ctx.hs
@@ -31,6 +31,7 @@
   , CtxUpdate
   , CtxLookupRight
   , CtxUpdateRight
+  , CtxFlatten
   , CheckIx
   , ValidIx
   , FromLeft
@@ -101,3 +102,8 @@
 --   is out of range, the context is unchanged.
 type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k)
   = CtxUpdateRight (FromLeft ctx n) x ctx
+
+-- | Flatten a nested context
+type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where
+  CtxFlatten EmptyCtx = EmptyCtx
+  CtxFlatten (ctxs ::> ctx) = CtxFlatten ctxs <+> ctx
diff --git a/src/Data/Parameterized/DataKind.hs b/src/Data/Parameterized/DataKind.hs
--- a/src/Data/Parameterized/DataKind.hs
+++ b/src/Data/Parameterized/DataKind.hs
@@ -13,9 +13,10 @@
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.TH.GADT as TH
 
+import           Data.Kind
 import           Prelude hiding ( fst, snd )
 
-data PairRepr (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)) where
+data PairRepr (f :: k1 -> Type) (g :: k2 -> Type) (p :: (k1, k2)) where
   PairRepr :: f a -> g b -> PairRepr f g '(a, b)
 
 type family Fst (pair :: (k1, k2)) where
diff --git a/src/Data/Parameterized/HashTable.hs b/src/Data/Parameterized/HashTable.hs
--- a/src/Data/Parameterized/HashTable.hs
+++ b/src/Data/Parameterized/HashTable.hs
@@ -31,6 +31,7 @@
 import Control.Applicative
 import Control.Monad.ST
 import qualified Data.HashTable.ST.Basic as H
+import Data.Kind
 import GHC.Exts (Any)
 import Unsafe.Coerce
 
@@ -40,7 +41,7 @@
 import Data.Parameterized.Some
 
 -- | A hash table mapping nonces to values.
-newtype HashTable s (key :: k -> *) (val :: k -> *)
+newtype HashTable s (key :: k -> Type) (val :: k -> Type)
       = HashTable (H.HashTable s (Some key) Any)
 
 -- | Create a new empty table.
@@ -73,7 +74,7 @@
 
 -- | Insert new key and value mapping into table.
 insert :: (HashableF key, TestEquality key)
-       => HashTable s (key :: k -> *) (val :: k -> *)
+       => HashTable s (key :: k -> Type) (val :: k -> Type)
        -> key tp
        -> val tp
        -> ST s ()
@@ -81,18 +82,18 @@
 
 -- | Return true if the key is in the hash table.
 member :: (HashableF key, TestEquality key)
-       => HashTable s (key :: k -> *) (val :: k -> *)
+       => HashTable s (key :: k -> Type) (val :: k -> Type)
        -> key (tp :: k)
        -> ST s Bool
 member (HashTable h) k = isJust <$> H.lookup h (Some k)
 
 -- | Delete an element from the hash table.
 delete :: (HashableF key, TestEquality key)
-       => HashTable s (key :: k -> *) (val :: k -> *)
+       => HashTable s (key :: k -> Type) (val :: k -> Type)
        -> key (tp :: k)
        -> ST s ()
 delete (HashTable h) k = H.delete h (Some k)
 
 clear :: (HashableF key, TestEquality key)
-      => HashTable s (key :: k -> *) (val :: k -> *) -> ST s ()
+      => HashTable s (key :: k -> Type) (val :: k -> Type) -> ST s ()
 clear (HashTable h) = H.mapM_ (\(k,_) -> H.delete h k) h
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
@@ -149,13 +149,14 @@
   ) where
 
 import qualified Control.Lens as Lens
+import           Data.Kind
 import           Prelude hiding ((!!))
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.TraversableFC
 
 -- | Parameterized list of elements.
-data List :: (k -> *) -> [k] -> * where
+data List :: (k -> Type) -> [k] -> Type where
   Nil  :: List f '[]
   (:<) :: f tp -> List f tps -> List f (tp : tps)
 
@@ -215,7 +216,7 @@
 -- | 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
-data Index :: [k] -> k -> *  where
+data Index :: [k] -> k -> Type  where
   IndexHere :: Index (x:r) x
   IndexThere :: !(Index r y) -> Index (x:r) y
 
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
@@ -540,7 +540,7 @@
             . NatRepr h
            -> (forall n. (n <= h) => NatRepr n -> a)
            -> [a]
-natFromZero = natForEach (knownNat @0)
+natFromZero h f = natForEach (knownNat @0) h f
 
 -- | Recursor for natural numbeers.
 natRec :: forall p f
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
@@ -14,7 +14,6 @@
 (via 'unsafeCoerce') that the types ascribed to the nonces are equal
 if their values are equal.
 -}
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE GADTs #-}
@@ -46,6 +45,7 @@
 
 import Control.Monad.ST
 import Data.Hashable
+import Data.Kind
 import Data.IORef
 import Data.STRef
 import Data.Typeable
@@ -56,15 +56,11 @@
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
 
-#if __GLASGOW_HASKELL__ < 805
-import Data.Kind
-#endif
-
 -- | Provides a monadic action for getting fresh typed names.
 --
 -- The first type parameter @m@ is the monad used for generating names, and
 -- the second parameter @s@ is used for the counter.
-data NonceGenerator (m :: * -> *) (s :: *) where
+data NonceGenerator (m :: Type -> Type) (s :: Type) where
   STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s
   IONG :: !(IORef Word64) -> NonceGenerator IO s
 
@@ -123,7 +119,7 @@
   f r
 
 -- | An index generated by the counter.
-newtype Nonce (s :: *) (tp :: k) = Nonce { indexValue :: Word64 }
+newtype Nonce (s :: Type) (tp :: k) = Nonce { indexValue :: Word64 }
   deriving (Eq, Ord, Hashable, Show)
 
 --  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce
diff --git a/src/Data/Parameterized/Nonce/Transformers.hs b/src/Data/Parameterized/Nonce/Transformers.hs
--- a/src/Data/Parameterized/Nonce/Transformers.hs
+++ b/src/Data/Parameterized/Nonce/Transformers.hs
@@ -25,6 +25,7 @@
 import Control.Monad.Reader
 import Control.Monad.ST
 import Control.Monad.State
+import Data.Kind
 
 import Data.Parameterized.Nonce
 
@@ -33,7 +34,7 @@
 -- (where we view the phantom type parameter of 'Nonce' as a designator of the
 -- set that the 'Nonce' came from).
 class Monad m => MonadNonce m where
-  type NonceSet m :: *
+  type NonceSet m :: Type
   freshNonceM :: forall k (tp :: k) . m (Nonce (NonceSet m) tp)
 
 -- | This transformer adds a nonce generator to a given monad.
diff --git a/src/Data/Parameterized/Pair.hs b/src/Data/Parameterized/Pair.hs
--- a/src/Data/Parameterized/Pair.hs
+++ b/src/Data/Parameterized/Pair.hs
@@ -17,13 +17,14 @@
   , viewPair
   ) where
 
+import Data.Kind
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
 import Data.Parameterized.TraversableF
 
 -- | Like a 2-tuple, but with an existentially quantified parameter that both of
 -- the elements share.
-data Pair (a :: k -> *) (b :: k -> *) where
+data Pair (a :: k -> Type) (b :: k -> Type) where
   Pair :: !(a tp) -> !(b tp) -> Pair a b
 
 instance (TestEquality a, EqF b) => Eq (Pair a b) where
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
@@ -20,11 +20,12 @@
   ) where
 
 import Data.Hashable
+import Data.Kind
 import Data.Parameterized.Classes
 import Data.Parameterized.TraversableF
 
 
-data Some (f:: k -> *) = forall x . Some (f x)
+data Some (f:: k -> Type) = forall x . Some (f x)
 
 instance TestEquality f => Eq (Some f) where
   Some x == Some y = isJust (testEquality x y)
diff --git a/src/Data/Parameterized/TraversableF.hs b/src/Data/Parameterized/TraversableF.hs
--- a/src/Data/Parameterized/TraversableF.hs
+++ b/src/Data/Parameterized/TraversableF.hs
@@ -35,6 +35,7 @@
 import Control.Monad.Identity
 import Data.Coerce
 import Data.Functor.Compose (Compose(..))
+import Data.Kind
 import Data.Monoid
 import GHC.Exts (build)
 
@@ -57,7 +58,7 @@
 
 -- | This is a generalization of the 'Foldable' class to
 -- structures over parameterized terms.
-class FoldableF (t :: (k -> *) -> *) where
+class FoldableF (t :: (k -> Type) -> Type) where
   {-# MINIMAL foldMapF | foldrF #-}
 
   -- | Map each element of the structure to a monoid,
@@ -167,24 +168,24 @@
 ------------------------------------------------------------------------
 -- TraversableF (Compose s t)
 
-instance ( FunctorF (s :: (k -> *) -> *)
-         , FunctorFC (t :: (l -> *) -> (k -> *))
+instance ( FunctorF (s :: (k -> Type) -> Type)
+         , FunctorFC (t :: (l -> Type) -> (k -> Type))
          ) =>
          FunctorF (Compose s t) where
   fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v
 
-instance ( TraversableF (s :: (k -> *) -> *)
-         , TraversableFC (t :: (l -> *) -> (k -> *))
+instance ( TraversableF (s :: (k -> Type) -> Type)
+         , TraversableFC (t :: (l -> Type) -> (k -> Type))
          ) =>
          FoldableF (Compose s t) where
   foldMapF = foldMapFDefault
 
 -- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.
-instance ( TraversableF (s :: (k -> *) -> *)
-         , TraversableFC (t :: (l -> *) -> (k -> *))
+instance ( TraversableF (s :: (k -> Type) -> Type)
+         , TraversableFC (t :: (l -> Type) -> (k -> Type))
          ) =>
          TraversableF (Compose s t) where
-  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>
+  traverseF :: forall (f :: l -> Type) (g :: l -> Type) m. (Applicative m) =>
                (forall (u :: l). f u -> m (g u))
             -> Compose s t f -> m (Compose s t g)
   traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v
diff --git a/src/Data/Parameterized/TraversableFC.hs b/src/Data/Parameterized/TraversableFC.hs
--- a/src/Data/Parameterized/TraversableFC.hs
+++ b/src/Data/Parameterized/TraversableFC.hs
@@ -38,6 +38,7 @@
 import Control.Applicative (Const(..) )
 import Control.Monad.Identity ( Identity (..) )
 import Data.Coerce
+import Data.Kind
 import Data.Monoid
 import GHC.Exts (build)
 import Data.Type.Equality
@@ -45,13 +46,13 @@
 import Data.Parameterized.Classes
 
 -- | A parameterized type that is a function on all instances.
-class FunctorFC (t :: (k -> *) -> l -> *) where
+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)
 
 -- | A parameterized class for types which can be shown, when given
 --   functions to show parameterized subterms.
-class ShowFC (t :: (k -> *) -> l -> *) where
+class ShowFC (t :: (k -> Type) -> l -> Type) where
   {-# MINIMAL showFC | showsPrecFC #-}
 
   showFC :: forall f. (forall x. f x -> String)
@@ -65,19 +66,19 @@
 
 -- | A parameterized class for types which can be hashed, when given
 --   functions to hash parameterized subterms.
-class HashableFC (t :: (k -> *) -> l -> *) where
+class HashableFC (t :: (k -> Type) -> l -> Type) where
   hashWithSaltFC :: forall f. (forall x. Int -> f x -> Int) ->
                               (forall x. Int -> t f x -> Int)
 
 -- | A parameterized class for types which can be tested for parameterized equality,
 --   when given an equality test for subterms.
-class TestEqualityFC (t :: (k -> *) -> l -> *) where
+class TestEqualityFC (t :: (k -> Type) -> l -> Type) where
   testEqualityFC :: forall f. (forall x y. f x -> f y -> (Maybe (x :~: y))) ->
                               (forall x y. t f x -> t f y -> (Maybe (x :~: y)))
 
 -- | A parameterized class for types which can be tested for parameterized ordering,
 --   when given an comparison test for subterms.
-class TestEqualityFC t => OrdFC (t :: (k -> *) -> l -> *) where
+class TestEqualityFC t => OrdFC (t :: (k -> Type) -> l -> Type) where
   compareFC :: forall f. (forall x y. f x -> f y -> OrderingF x y) ->
                          (forall x y. t f x -> t f y -> OrderingF x y)
 
@@ -91,7 +92,7 @@
 
 -- | This is a generalization of the 'Foldable' class to
 -- structures over parameterized terms.
-class FoldableFC (t :: (k -> *) -> l -> *) where
+class FoldableFC (t :: (k -> Type) -> l -> Type) where
   {-# MINIMAL foldMapFC | foldrFC #-}
 
   -- | Map each element of the structure to a monoid,
@@ -158,7 +159,7 @@
 ------------------------------------------------------------------------
 -- TraversableF
 
-class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *) where
+class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> Type) -> l -> Type) where
   traverseFC :: forall f g m. Applicative m
              => (forall x. f x -> m (g x))
              -> (forall x. t f x -> m (t g x))
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,6 +1,8 @@
 {-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}
 {-# Language PatternGuards #-}
+{-# Language PolyKinds #-}
 {-# Language TypeApplications, ScopedTypeVariables #-}
+{-# Language TupleSections #-}
 {-# Language Rank2Types, RoleAnnotations #-}
 {-# Language CPP #-}
 #if __GLASGOW_HASKELL__ >= 805
@@ -20,6 +22,10 @@
   , fromList
   , toList
 
+    -- * Assignments
+  , fromAssignment
+  , toAssignment
+
     -- * Length
   , length
   , nonEmpty
@@ -36,6 +42,7 @@
 
     -- * Sub sequences
   , uncons
+  , unsnoc
   , slice
   , Data.Parameterized.Vector.take
   , replace
@@ -62,6 +69,11 @@
   , snoc
   , generate
   , generateM
+  -- ** Unfolding
+  , unfoldr
+  , unfoldrM
+  , unfoldrWithIndex
+  , unfoldrWithIndexM
 
     -- * Splitting and joining
     -- ** General
@@ -90,6 +102,7 @@
 import Prelude hiding (length,reverse,zipWith)
 import Numeric.Natural
 
+import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.Utils.Endian
 
 -- | Fixed-size non-empty vectors.
@@ -170,7 +183,19 @@
              Right Refl    -> Left Refl
 {-# Inline uncons #-}
 
+-- | Remove the last element of the vector, and return the rest, if any.
+unsnoc :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
+unsnoc v@(Vector xs) = (Vector.last xs, mbTail)
+  where
+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
+  mbTail = case testStrictLeq (knownNat @1) (length v) of
+             Left n2_leq_n ->
+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))
+                  return (Vector (Vector.slice 0 (Vector.length xs - 1) xs))
+             Right Refl    -> Left Refl
+{-# Inline unsnoc #-}
 
+
 --------------------------------------------------------------------------------
 
 -- | Make a vector of the given length and element type.
@@ -185,7 +210,34 @@
   v = Vector.fromList xs
 {-# INLINE fromList #-}
 
+-- | Convert a non-empty 'Ctx.Assignment' to a fixed-size 'Vector'.
+--
+-- This function uses the same ordering convention as 'Ctx.toVector'.
+fromAssignment ::
+  forall f ctx tp e.
+  (forall tp'. f tp' -> e) ->
+  Ctx.Assignment f (ctx Ctx.::> tp) ->
+  Vector (Ctx.CtxSize (ctx Ctx.::> tp)) e
+fromAssignment f assign =
+  case Ctx.viewAssign assign of
+    Ctx.AssignExtend assign' _ ->
+      case leqAdd (leqRefl (knownNat @1)) (Ctx.sizeToNatRepr (Ctx.size assign')) of
+        LeqProof -> Vector (Ctx.toVector assign f)
 
+-- | Convert a 'Vector' into a 'Ctx.Assignment'.
+--
+-- This function uses the same ordering convention as 'Ctx.toVector'.
+toAssignment ::
+  Ctx.Size ctx ->
+  (forall tp. Ctx.Index ctx tp -> e -> f tp) ->
+  Vector (Ctx.CtxSize ctx) e ->
+  Ctx.Assignment f ctx
+toAssignment sz g vec =
+  -- The unsafe indexing here relies on the safety of the rest of the Vector
+  -- API, specifically the inability to construct vectors that have an
+  -- underlying size that differs from the size in their type.
+  Ctx.generate sz (\idx -> g idx (elemAtUnsafe (Ctx.indexVal idx) vec))
+
 -- | Extract a subvector of the given vector.
 slice :: (i + w <= n, 1 <= w) =>
             NatRepr i {- ^ Start index -} ->
@@ -219,7 +271,7 @@
             NatRepr i {- ^ Start index -} ->
             NatRepr w {- ^ Section width -} ->
             (Vector w a -> Vector w a) {-^ map for the sub-vector -} ->
-            Vector n a -> Vector n a 
+            Vector n a -> Vector n a
 mapAt i w f vn = runIdentity $ mapAtM i w (pure . f) vn
 
 -- | Replace a sub-section of a vector with the given sub-vector.
@@ -371,30 +423,12 @@
 unVector' :: Vector' a n -> Vector (n+1) a
 unVector' (MkVector' v) = v
 
-snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)
-snoc' v = MkVector' . snoc (unVector' v)
-
 generate' :: forall h a
            . NatRepr h
           -> (forall n. (n <= h) => NatRepr n -> a)
           -> Vector' a h
 generate' h gen =
-  case isZeroOrGT1 h of
-    Left Refl -> base
-    Right LeqProof ->
-      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->
-      natRecBounded (decNat h) (decNat h) base step
-      }
-  where base :: Vector' a 0
-        base = MkVector' $ singleton (gen (knownNat @0))
-        step :: forall m. (1 <= h, m <= h - 1)
-             => NatRepr m -> Vector' a m -> Vector' a (m + 1)
-        step m v =
-          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->
-          case (leqAdd2 (LeqProof :: LeqProof m (h-1))
-                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->
-            snoc' v (gen (incNat m))
-          }}
+  runIdentity $ unfoldrWithIndexM' h (\n _last -> Identity (gen n, ())) ()
 
 -- | Apply a function to each element in a range starting at zero;
 -- return the a vector of values obtained.
@@ -412,6 +446,79 @@
           -> (forall n. (n <= h) => NatRepr n -> m a)
           -> m (Vector (h + 1) a)
 generateM h gen = sequence $ generate h gen
+
+newtype Compose3 m f g a = Compose3 { getCompose3 :: m (f (g a)) }
+
+unfoldrWithIndexM' :: forall m h a b. (Monad m)
+                  => NatRepr h
+                  -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))
+                  -> b
+                  -> m (Vector' a h)
+unfoldrWithIndexM' h gen start =
+  case isZeroOrGT1 h of
+    Left Refl -> snd <$> getCompose3 base
+    Right LeqProof ->
+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->
+        snd <$> getCompose3 (natRecBounded (decNat h) (decNat h) base step)
+      }
+  where base :: Compose3 m ((,) b) (Vector' a) 0
+        base = Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start
+        step :: forall p. (1 <= h, p <= h - 1)
+             => NatRepr p
+             -> Compose3 m ((,) b) (Vector' a) p
+             -> Compose3 m ((,) b) (Vector' a) (p + 1)
+        step p (Compose3 mv) =
+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->
+          case (leqAdd2 (LeqProof :: LeqProof p (h-1))
+                        (LeqProof :: LeqProof 1 1) :: LeqProof (p+1) h) of { LeqProof ->
+            Compose3 $
+              do (seed, MkVector' v) <- mv
+                 (next, nextSeed) <- gen (incNat p) seed
+                 pure $ (nextSeed, MkVector' $ snoc v next)
+          }}
+
+-- | Monadically unfold a vector, with access to the current index.
+--
+-- c.f. @Data.Vector.unfoldrExactNM@
+unfoldrWithIndexM :: forall m h a b. (Monad m)
+                 => NatRepr h
+                 -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))
+                 -> b
+                 -> m (Vector (h + 1) a)
+unfoldrWithIndexM h gen start = unVector' <$> unfoldrWithIndexM' h gen start
+
+-- | Unfold a vector, with access to the current index.
+--
+-- c.f. @Data.Vector.unfoldrExactN@
+unfoldrWithIndex :: forall h a b
+                . NatRepr h
+                -> (forall n. (n <= h) => NatRepr n -> b -> (a, b))
+                -> b
+                -> Vector (h + 1) a
+unfoldrWithIndex h gen start =
+  unVector' $ runIdentity $ unfoldrWithIndexM' h (\n v -> Identity (gen n v)) start
+
+-- | Monadically construct a vector with exactly @h + 1@ elements by repeatedly
+-- applying a generator function to a seed value.
+--
+-- c.f. @Data.Vector.unfoldrExactNM@
+unfoldrM :: forall m h a b. (Monad m)
+        => NatRepr h
+        -> (b -> m (a, b))
+        -> b
+        -> m (Vector (h + 1) a)
+unfoldrM h gen start = unfoldrWithIndexM h (\_ v -> gen v) start
+
+-- | Construct a vector with exactly @h + 1@ elements by repeatedly applying a
+-- generator function to a seed value.
+--
+-- c.f. @Data.Vector.unfoldrExactN@
+unfoldr :: forall h a b
+        . NatRepr h
+       -> (b -> (a, b))
+       -> b
+       -> Vector (h + 1) a
+unfoldr h gen start = unfoldrWithIndex h (\_ v -> gen v) start
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Data/Parameterized/WithRepr.hs b/src/Data/Parameterized/WithRepr.hs
--- a/src/Data/Parameterized/WithRepr.hs
+++ b/src/Data/Parameterized/WithRepr.hs
@@ -58,6 +58,7 @@
 -}
 module Data.Parameterized.WithRepr(IsRepr(..)) where
 
+import Data.Kind
 import Data.Parameterized.Classes
 
 #ifdef UNSAFE_OPS
@@ -75,7 +76,7 @@
 import Data.Parameterized.BoolRepr
 
 -- | Turn an explicit Repr value into an implict KnownRepr constraint
-class IsRepr (f :: k -> *) where
+class IsRepr (f :: k -> Type) where
 
   withRepr :: f a -> (KnownRepr f a => r) -> r
 
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 PatternGuards #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
@@ -9,10 +10,15 @@
 
 module Test.Context
   ( contextTests
+  , genSomePayloadList
+  , mkUAsgn
+  , mkSAsgn
   )
 where
 
 import           Control.Lens
+import           Data.Functor.Product (Product(Pair))
+import           Data.Kind
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as C
 import qualified Data.Parameterized.Context.Safe as S
@@ -32,7 +38,7 @@
 -- Create a Payload GADT which is the parameterized type used for many
 -- of the Context/Assignment tests in this module.
 
-data Payload (ty :: *) where
+data Payload (ty :: Type) where
   IntPayload    :: Int -> Payload Int
   StringPayload :: String -> Payload String
   BoolPayload   :: Bool -> Payload Bool
@@ -310,6 +316,13 @@
         assert $ isJust $ testEquality uv uv'
         assert $ isJust $ testEquality wxy wxy'
         withWXY $ \t -> assert $ isJust $ testEquality wxy' t
+
+   , 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''
 
    , testCaseSteps "explicit indexing (unsafe)" $ \step -> do
        let mkUPayload :: U.Assignment Payload TestCtx
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
--- a/test/Test/Vector.hs
+++ b/test/Test/Vector.hs
@@ -3,6 +3,7 @@
 {-# Language DataKinds #-}
 {-# Language ExplicitForAll #-}
 {-# Language FlexibleInstances #-}
+{-# Language LambdaCase #-}
 {-# Language ScopedTypeVariables #-}
 {-# Language StandaloneDeriving #-}
 {-# Language TypeFamilies #-}
@@ -16,16 +17,23 @@
   )
 where
 
+import           Data.Functor.Const (Const(..))
+import           Data.Maybe (isJust)
+import qualified Data.List as List
+import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.NatRepr
+import           Data.Parameterized.Some
 import           Data.Parameterized.Vector
 import           Data.Semigroup
 import           GHC.TypeLits
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range
-import           Prelude hiding (reverse)
+import           Prelude hiding (take, reverse)
+import qualified Prelude as P
 import           Test.Tasty
 import           Test.Tasty.Hedgehog
+import           Test.Context (genSomePayloadList, mkUAsgn)
 
 
 genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)
@@ -41,7 +49,7 @@
 genOrdering = HG.element [ LT, EQ, GT ]
 
 
-instance Show (Int -> Ordering) where
+instance Show (a -> b) where
   show _ = "unshowable"
 
 
@@ -77,6 +85,14 @@
        x <- forAll genOrdering
        (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])
 
+  -- @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
+
   -- @generate@ is like mapping a function over indices
   , testProperty "generate" $ property $
     do let n = knownNat @55
@@ -88,4 +104,45 @@
                    ]
        f <- forAll $ HG.element funs
        Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])
-  ]
+
+  -- @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))
+
+  -- 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))
+    ]