diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,5 +1,5 @@
 Name:          parameterized-utils
-Version:       1.0.0
+Version:       1.0.1
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com
 Build-type:    Simple
@@ -30,7 +30,7 @@
 
 library
   build-depends:
-    base >= 4.7 && < 4.11,
+    base >= 4.7 && < 4.12,
     th-abstraction >=0.1 && <0.3,
     containers,
     deepseq,
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
@@ -39,6 +39,7 @@
   , fromOrdering
     -- * Typeclass generalizations
   , ShowF(..)
+  , showsF
   , HashableF(..)
   , CoercibleF(..)
     -- * Optics generalizations
@@ -211,8 +212,13 @@
   showF :: forall tp . f tp -> String
   showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x)
 
-  showsF :: forall tp . f tp -> String -> String
-  showsF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (shows x)
+  -- | Like 'showsPrec', the precedence argument is /one more/ than the
+  -- precedence of the enclosing context.
+  showsPrecF :: forall tp. Int -> f tp -> String -> String
+  showsPrecF p x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (showsPrec p x)
+
+showsF :: ShowF f => f tp -> String -> String
+showsF x = showsPrecF 0 x
 
 instance Show x => ShowF (Const x)
 
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
@@ -33,60 +33,102 @@
 module Data.Parameterized.Context
  (
 #ifdef UNSAFE_OPS
-   module Data.Parameterized.Context.Unsafe
+    module Data.Parameterized.Context.Unsafe
 #else
-   module Data.Parameterized.Context.Safe
+    module Data.Parameterized.Context.Safe
 #endif
- , singleton
- , toVector
- , pattern (:>)
- , pattern Empty
-   -- * Context extension and embedding utilities
- , CtxEmbedding(..)
- , ExtendContext(..)
- , ExtendContext'(..)
- , ApplyEmbedding(..)
- , ApplyEmbedding'(..)
- , identityEmbedding
- , extendEmbeddingRightDiff
- , extendEmbeddingRight
- , extendEmbeddingBoth
- , ctxeSize
- , ctxeAssignment
-
-   -- * Static indexing and lenses for assignments
- , Idx
- , getCtx
- , setCtx
- , field
- , natIndex
- , natIndexProxy
-
-   -- * Currying and uncurrying for assignments
- , CurryAssignment
- , CurryAssignmentClass(..)
- ) where
-
-import Prelude hiding (null)
+  , singleton
+  , toVector
+  , pattern (:>)
+  , pattern Empty
+  , decompose
+  , Data.Parameterized.Context.null
+  , Data.Parameterized.Context.init
+  , Data.Parameterized.Context.last
+  , Data.Parameterized.Context.view
+  , forIndexM
+  , generateSome
+  , generateSomeM
+  , fromList
+    -- * Context extension and embedding utilities
+  , CtxEmbedding(..)
+  , ExtendContext(..)
+  , ExtendContext'(..)
+  , ApplyEmbedding(..)
+  , ApplyEmbedding'(..)
+  , identityEmbedding
+  , extendEmbeddingRightDiff
+  , extendEmbeddingRight
+  , extendEmbeddingBoth
+  , ctxeSize
+  , ctxeAssignment
 
-import GHC.TypeLits (Nat, type (-))
+    -- * Static indexing and lenses for assignments
+  , Idx
+  , field
+  , natIndex
+  , natIndexProxy
+    -- * Currying and uncurrying for assignments
+  , CurryAssignment
+  , CurryAssignmentClass(..)
+    -- * Size and Index values
+  , size1, size2, size3, size4, size5, size6
+  , i1of2, i2of2
+  , i1of3, i2of3, i3of3
+  , i1of4, i2of4, i3of4, i4of4
+  , i1of5, i2of5, i3of5, i4of5, i5of5
+  , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6
+  ) where
 
-import Control.Lens hiding (Index, view, (:>), Empty)
+import           Control.Lens hiding (Index, (:>), Empty)
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
+import           GHC.TypeLits (Nat, type (-))
 
+import           Data.Parameterized.Classes
+import           Data.Parameterized.Some
+import           Data.Parameterized.TraversableFC
+
 #ifdef UNSAFE_OPS
-import Data.Parameterized.Context.Unsafe
+import           Data.Parameterized.Context.Unsafe
 #else
-import Data.Parameterized.Context.Safe
+import           Data.Parameterized.Context.Safe
 #endif
 
-import Data.Parameterized.TraversableFC
 
 -- | Create a single element context.
 singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
 singleton = (empty :>)
 
+-- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.
+forIndexM :: forall ctx m
+           . Applicative m
+          => Size ctx
+          -> (forall tp . Index ctx tp -> m ())
+          -> m ()
+forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ())
+
+-- | Generate an assignment with some context type that is not known.
+generateSome :: forall f
+              . Int
+             -> (Int -> Some f)
+             -> Some (Assignment f)
+generateSome n f = go n
+  where go :: Int -> Some (Assignment f)
+        go 0 = Some empty
+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1))
+
+-- | Generate an assignment with some context type that is not known.
+generateSomeM :: forall m f
+              .  Applicative m
+              => Int
+              -> (Int -> m (Some f))
+              -> m (Some (Assignment f))
+generateSomeM n f = go n
+  where go :: Int -> m (Some (Assignment f))
+        go 0 = pure (Some empty)
+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1)
+
 -- | Convert the assignment to a vector.
 toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e
 toVector a f = V.create $ do
@@ -97,6 +139,56 @@
 {-# INLINABLE toVector #-}
 
 --------------------------------------------------------------------------------
+-- Patterns
+
+-- | Pattern synonym for the empty assignment
+pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
+pattern Empty <- (viewAssign -> AssignEmpty)
+  where Empty = empty
+
+infixl :>
+
+-- | Pattern synonym for extending an assignment on the right
+pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
+pattern (:>) a v <- (viewAssign -> AssignExtend a v)
+  where a :> v = extend a v
+
+-- The COMPLETE pragma was not defined until ghc 8.2.*
+#if MIN_VERSION_base(4,10,0)
+{-# COMPLETE (:>), Empty :: Assignment  #-}
+#endif
+
+--------------------------------------------------------------------------------
+-- | Views
+
+-- | Return true if assignment is empty.
+null :: Assignment f ctx -> Bool
+null a =
+  case viewAssign a of
+    AssignEmpty -> True
+    AssignExtend{} -> False
+
+decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
+decompose x = (Data.Parameterized.Context.init x, Data.Parameterized.Context.last x)
+
+-- | Return assignment with all but the last block.
+init :: Assignment f (ctx '::> tp) -> Assignment f ctx
+init x =
+  case viewAssign x of
+    AssignExtend t _ -> t
+
+-- | Return the last element in the assignment.
+last :: Assignment f (ctx '::> tp) -> f tp
+last x =
+  case viewAssign x of
+    AssignExtend _ e -> e
+
+{-# DEPRECATED view "Use viewAssign or the Empty and :> patterns instead." #-}
+-- | View an assignment as either empty or an assignment with one appended.
+view :: forall f ctx . Assignment f ctx -> AssignView f ctx
+view = viewAssign
+
+--------------------------------------------------------------------------------
 -- | Context embedding.
 
 -- This datastructure contains a proof that the first context is
@@ -169,38 +261,13 @@
     updated :: CtxEmbedding ctx (ctx' ::> tp)
     updated = extendEmbeddingRight ctxe
 
--- | Pattern synonym for the empty assignment
-pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
-pattern Empty <- (view -> AssignEmpty)
-  where Empty = empty
-
-infixl :>
-
--- | Pattern synonym for extending an assignment on the right
-pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
-pattern (:>) a v <- (view -> AssignExtend a v)
-  where a :> v = extend a v
-
--- The COMPLETE pragma was not defined until ghc 8.2.*
-#if MIN_VERSION_base(4,10,0)
-{-# COMPLETE (:>), Empty :: Assignment  #-}
-#endif
-
 --------------------------------------------------------------------------------
 -- Static indexing based on type-level naturals
 
--- | Get an element from an 'Assignment' by zero-based, left-to-right position.
--- The position must be specified using @TypeApplications@ for the @n@ parameter.
-getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r
-getCtx asgn = asgn ! natIndex @n
-
-setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx
-setCtx = update (natIndex @n)
-
 -- | Get a lens for an position in an 'Assignment' by zero-based, left-to-right position.
 -- The position must be specified using @TypeApplications@ for the @n@ parameter.
 field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)
-field f = adjustM f (natIndex @n)
+field = ixF' (natIndex @n)
 
 -- | Constraint synonym used for getting an 'Index' into a 'Ctx'.
 -- @n@ is the zero-based, left-counted index into the list of types
@@ -234,7 +301,7 @@
 instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) =>
   Idx' n (xs '::> x) r where
 
-  natIndex' = skip (natIndex' @_ @(n-1))
+  natIndex' = skipIndex (natIndex' @_ @(n-1))
 
 
 --------------------------------------------------------------------------------
@@ -270,5 +337,93 @@
 instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where
   curryAssignment k = curryAssignment (\asgn a -> k (asgn :> a))
   uncurryAssignment k asgn =
-    case view asgn of
+    case viewAssign asgn of
       AssignExtend asgn' x -> uncurryAssignment k asgn' x
+
+-- | Create an assignment from a list of values.
+fromList :: [Some f] -> Some (Assignment f)
+fromList = go empty
+  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
+        go prev [] = Some prev
+        go prev (Some g:next) = (go $! prev `extend` g) next
+
+--------------------------------------------------------------------------------
+-- Size and Index values
+
+size1 :: Size (EmptyCtx ::> a)
+size1 = incSize zeroSize
+
+size2 :: Size (EmptyCtx ::> a ::> b)
+size2 = incSize size1
+
+size3 :: Size (EmptyCtx ::> a ::> b ::> c)
+size3 = incSize size2
+
+size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)
+size4 = incSize size3
+
+size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
+size5 = incSize size4
+
+size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)
+size6 = incSize size5
+
+i1of2 :: Index (EmptyCtx ::> a ::> b) a
+i1of2 = skipIndex baseIndex
+
+i2of2 :: Index (EmptyCtx ::> a ::> b) b
+i2of2 = nextIndex size1
+
+i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a
+i1of3 = skipIndex i1of2
+
+i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b
+i2of3 = skipIndex i2of2
+
+i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c
+i3of3 = nextIndex size2
+
+i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a
+i1of4 = skipIndex i1of3
+
+i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b
+i2of4 = skipIndex i2of3
+
+i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c
+i3of4 = skipIndex i3of3
+
+i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d
+i4of4 = nextIndex size3
+
+i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
+i1of5 = skipIndex i1of4
+
+i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b
+i2of5 = skipIndex i2of4
+
+i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c
+i3of5 = skipIndex i3of4
+
+i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d
+i4of5 = skipIndex i4of4
+
+i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e
+i5of5 = nextIndex size4
+
+i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a
+i1of6 = skipIndex i1of5
+
+i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b
+i2of6 = skipIndex i2of5
+
+i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c
+i3of6 = skipIndex i3of5
+
+i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d
+i4of6 = skipIndex i4of5
+
+i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e
+i5of6 = skipIndex i5of5
+
+i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f
+i6of6 = nextIndex size5
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
@@ -24,6 +24,7 @@
 -- 'Data.Coerce.coerce' to understand indexes in a new context without
 -- actually breaking things.
 --------------------------------------------------------------------------
+{-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
@@ -39,9 +40,12 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeInType #-}
 module Data.Parameterized.Context.Safe
   ( module Data.Parameterized.Ctx
+    -- * Size
   , Size
   , sizeInt
   , zeroSize
@@ -56,39 +60,36 @@
   , Diff
   , noDiff
   , extendRight
-  , KnownDiff(..)
   , DiffView(..)
   , viewDiff
+  , KnownDiff(..)
     -- * Indexing
   , Index
   , indexVal
-  , base
-  , skip
+  , baseIndex
+  , skipIndex
   , lastIndex
   , nextIndex
   , extendIndex
   , extendIndex'
   , forIndex
+  , forIndexRange
   , intIndex
     -- * Assignments
   , Assignment
   , size
-  , replicate
+  , Data.Parameterized.Context.Safe.replicate
   , generate
   , generateM
   , empty
-  , null
   , extend
-  , update
   , adjust
+  , update
   , adjustM
-  , init
   , AssignView(..)
-  , view
-  , decompose
+  , viewAssign
   , (!)
   , (!^)
-  , toList
   , zipWith
   , zipWithM
   , (<++>)
@@ -104,6 +105,7 @@
 import Data.Maybe (listToMaybe)
 import Data.Type.Equality
 import Prelude hiding (init, map, null, replicate, succ, zipWith)
+import Data.Kind(Type)
 
 #if !MIN_VERSION_base(4,8,0)
 import Data.Functor
@@ -121,7 +123,7 @@
 -- | An indexed singleton type representing the size of a context.
 data Size (ctx :: Ctx k) where
   SizeZero :: Size 'EmptyCtx
-  SizeSucc :: Size ctx -> Size (ctx '::> tp)
+  SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)
 
 -- | Convert a context size to an 'Int'.
 sizeInt :: Size ctx -> Int
@@ -225,7 +227,7 @@
 -- context.
 data Index (ctx :: Ctx k) (tp :: k) where
   IndexHere :: Size ctx -> Index (ctx '::> tp) tp
-  IndexThere :: Index ctx tp -> Index (ctx '::> tp') tp
+  IndexThere :: !(Index ctx tp) -> Index (ctx '::> tp') tp
 
 -- | Convert an index to an 'Int', where the index of the left-most type in the context is 0.
 indexVal :: Index ctx tp -> Int
@@ -254,12 +256,12 @@
   compareF (IndexThere idx1) (IndexThere idx2) = lexCompareF idx1 idx2 $ EQF
 
 -- | Index for first element in context.
-base :: Index ('EmptyCtx '::> tp) tp
-base = IndexHere SizeZero
+baseIndex :: Index ('EmptyCtx '::> tp) tp
+baseIndex = IndexHere SizeZero
 
 -- | Increase context while staying at same index.
-skip :: Index ctx x -> Index (ctx '::> y) x
-skip idx = IndexThere idx
+skipIndex :: Index ctx x -> Index (ctx '::> y) x
+skipIndex idx = IndexThere idx
 
 -- | Return the index of an element one past the size.
 nextIndex :: Size ctx -> Index (ctx '::> tp) tp
@@ -291,7 +293,44 @@
        go _ SizeZero = id
        go g (SizeSucc sz) = \r -> go (\i -> g (IndexThere i)) sz  $ f r (g (IndexHere sz))
 
+data LDiff (l :: Ctx k) (r :: Ctx k) where
+ LDiffHere :: LDiff a a
+ LDiffThere :: !(LDiff (a::>x) b) -> LDiff a b
 
+ldiffIndex :: Index a tp -> LDiff a b -> Index b tp
+ldiffIndex i LDiffHere = i
+ldiffIndex i (LDiffThere d) = ldiffIndex (IndexThere i) d
+
+forIndexLDiff :: Size a
+              -> LDiff a b
+              -> (forall tp . Index b tp -> r -> r)
+              -> r
+              -> r
+forIndexLDiff _ LDiffHere _ r = r
+forIndexLDiff sz (LDiffThere d) f r =
+  forIndexLDiff (SizeSucc sz) d f (f (ldiffIndex (IndexHere sz) d) r)
+
+forIndexRangeImpl :: Int
+                  -> Size a
+                  -> LDiff a b
+                  -> (forall tp . Index b tp -> r -> r)
+                  -> r
+                  -> r
+forIndexRangeImpl 0 sz d f r = forIndexLDiff sz d f r
+forIndexRangeImpl _ SizeZero _ _ r = r
+forIndexRangeImpl i (SizeSucc sz) d f r =
+  forIndexRangeImpl (i-1) sz (LDiffThere d) f r
+
+-- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',
+-- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and
+-- 'f i (forIndexRange (i+1) n v0)' otherwise.
+forIndexRange :: Int
+              -> Size ctx
+              -> (forall tp . Index ctx tp -> r -> r)
+              -> r
+              -> r
+forIndexRange i sz f r = forIndexRangeImpl i sz LDiffHere f r
+
 indexList :: forall ctx. Size ctx -> [Some (Index ctx)]
 indexList sz_top = go id [] sz_top
  where go :: (forall tp. Index ctx' tp -> Index ctx tp)
@@ -315,21 +354,18 @@
 
 -- | An assignment is a sequence that maps each index with type 'tp' to
 -- a value of type 'f tp'.
-data Assignment (f :: k -> *) (ctx :: Ctx k) where
+data Assignment (f :: k -> Type) (ctx :: Ctx k) where
   AssignmentEmpty :: Assignment f EmptyCtx
   AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
 
 -- | View an assignment as either empty or an assignment with one appended.
-data AssignView (f :: k -> *) (ctx :: Ctx k) where
+data AssignView (f :: k -> Type) (ctx :: Ctx k) where
   AssignEmpty :: AssignView f EmptyCtx
   AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp)
 
-view :: forall f ctx . Assignment f ctx -> AssignView f ctx
-view AssignmentEmpty = AssignEmpty
-view (AssignmentExtend asgn x) = AssignExtend asgn x
-
-decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
-decompose (AssignmentExtend a v) = (a,v)
+viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
+viewAssign AssignmentEmpty = AssignEmpty
+viewAssign (AssignmentExtend asgn x) = AssignExtend asgn x
 
 instance NFData (Assignment f ctx) where
   rnf AssignmentEmpty = ()
@@ -377,20 +413,17 @@
 empty :: Assignment f 'EmptyCtx
 empty = AssignmentEmpty
 
--- | Return true if assignment is empty.
-null :: Assignment f ctx -> Bool
-null AssignmentEmpty = True
-null _ = False
-
 extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
 extend asgn e = AssignmentExtend asgn e
 
-update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
-update idx e asgn = adjust (\_ -> e) idx asgn
-
+{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
 adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
-adjust f idx m = runIdentity (adjustM (Identity . f) idx m)
+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)
 
+{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}
+update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
+update i v a = adjust (\_ -> v) i a
+
 adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
 adjustM f = go (\x -> x)
  where
@@ -404,22 +437,17 @@
   go _ _ _ = error "SafeTypeContext.adjustM: impossible!"
 #endif
 
-type instance IndexF   (Assignment (f :: k -> *) ctx) = Index ctx
-type instance IxValueF (Assignment (f :: k -> *) ctx) = f
+type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx
+type instance IxValueF (Assignment (f :: k -> Type) ctx) = f
 
-instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where
+instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
   ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
   ixF idx f = adjustM f idx
 
-instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where
+instance forall (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
   ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
   ixF' idx f = adjustM f idx
 
-
--- | Return assignment with all but the last block.
-init :: Assignment f (ctx '::> tp) -> Assignment f ctx
-init (AssignmentExtend asgn _) = asgn
-
 idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp
 idxlookup f (AssignmentExtend _   x) (IndexHere _) = f x
 idxlookup f (AssignmentExtend ctx _) (IndexThere idx) = idxlookup f ctx idx
@@ -511,7 +539,7 @@
 map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
 map = fmapFC
 
-traverseF :: forall (f:: k -> *) (g::k -> *) (m:: * -> *) (c::Ctx k)
+traverseF :: forall (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
            . Applicative m
           => (forall tp . f tp -> m (g tp))
           -> Assignment f c
@@ -572,7 +600,7 @@
 type MyZ = 'MyZ
 type MyS = 'MyS
 
-data MyNatRepr :: MyNat -> * where
+data MyNatRepr :: MyNat -> Type where
   MyZR :: MyNatRepr MyZ
   MySR :: MyNatRepr n -> MyNatRepr (MyS n)
 
@@ -581,7 +609,7 @@
   StrongCtxUpdate MyZ     (ctx::>x)    z = ctx ::> z
   StrongCtxUpdate (MyS n) (ctx::>x)    z = (StrongCtxUpdate n ctx z) ::> x
 
-type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> *) :: * where
+type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> Type) :: Type where
   MyNatLookup n       EmptyCtx  f = ()
   MyNatLookup MyZ     (ctx::>x) f = f x
   MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f
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
@@ -12,9 +12,13 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeInType #-}
 module Data.Parameterized.Context.Unsafe
   ( module Data.Parameterized.Ctx
+  , KnownContext(..)
+    -- * Size
   , Size
   , sizeInt
   , zeroSize
@@ -24,26 +28,24 @@
   , addSize
   , SizeView(..)
   , viewSize
-  , KnownContext(..)
     -- * Diff
   , Diff
   , noDiff
   , extendRight
-  , KnownDiff(..)
   , DiffView(..)
   , viewDiff
+  , KnownDiff(..)
     -- * Indexing
   , Index
   , indexVal
-  , base
-  , skip
+  , baseIndex
+  , skipIndex
   , lastIndex
   , nextIndex
   , extendIndex
   , extendIndex'
   , forIndex
   , forIndexRange
-  , forIndexM
   , intIndex
     -- ** IndexRange
   , IndexRange
@@ -54,32 +56,24 @@
     -- * Assignments
   , Assignment
   , size
-  , replicate
+  , Data.Parameterized.Context.Unsafe.replicate
   , generate
   , generateM
-  , generateSome
-  , generateSomeM
   , empty
-  , null
   , extend
-  , update
   , adjust
+  , update
   , adjustM
-  , init
-  , last
   , AssignView(..)
-  , view
-  , decompose
-  , fromList
+  , viewAssign
   , (!)
   , (!^)
-  , zipWith
+  , Data.Parameterized.Context.Unsafe.zipWith
   , zipWithM
   , (<++>)
   , traverseWithIndex
   ) where
 
-import           Control.Applicative hiding (empty)
 import qualified Control.Category as Cat
 import           Control.DeepSeq
 import           Control.Exception
@@ -91,9 +85,7 @@
 import           Data.List (intercalate)
 import           Data.Proxy
 import           Unsafe.Coerce
-
-import           Prelude hiding (init, last, map, null, replicate, succ, zipWith, (++))
-import qualified Prelude
+import           Data.Kind(Type)
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Ctx
@@ -105,8 +97,14 @@
 -- Size
 
 -- | Represents the size of a context.
-newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int }
+newtype Size (ctx :: Ctx k) = Size Int
 
+type role Size nominal
+
+-- | Convert a context size to an 'Int'.
+sizeInt :: Size ctx -> Int
+sizeInt (Size n) = n
+
 -- | The size of an empty context.
 zeroSize :: Size 'EmptyCtx
 zeroSize = Size 0
@@ -199,6 +197,8 @@
 -- context.
 newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int }
 
+type role Index nominal nominal
+
 instance Eq (Index ctx tp) where
   Index i == Index j = i == j
 
@@ -217,12 +217,12 @@
     | otherwise = GTF
 
 -- | Index for first element in context.
-base :: Index ('EmptyCtx '::> tp) tp
-base = Index 0
+baseIndex :: Index ('EmptyCtx '::> tp) tp
+baseIndex = Index 0
 
 -- | Increase context while staying at same index.
-skip :: Index ctx x -> Index (ctx '::> y) x
-skip (Index i) = Index i
+skipIndex :: Index ctx x -> Index (ctx '::> y) x
+skipIndex (Index i) = Index i
 
 -- | Return the index of a element one past the size.
 nextIndex :: Size ctx -> Index (ctx ::> tp) tp
@@ -265,14 +265,6 @@
   | i >= n = r
   | otherwise = f (Index i) (forIndexRange (i+1) (Size n) f r)
 
--- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.
-forIndexM :: forall ctx m
-           . Applicative m
-          => Size ctx
-          -> (forall tp . Index ctx tp -> m ())
-          -> m ()
-forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ())
-
 -- | Return index at given integer or nothing if integer is out of bounds.
 intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
 intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))
@@ -323,7 +315,7 @@
 --
 -- The first parameter is the height of the tree.
 -- The second is the parameterized value.
-data BalancedTree h (f :: k -> *) (p :: Ctx k) where
+data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
   BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
   BalPair :: !(BalancedTree h f x)
           -> !(BalancedTree h f y)
@@ -474,7 +466,7 @@
 ------------------------------------------------------------------------
 -- BinomialTree
 
-data BinomialTree (h::Height) (f :: k -> *) :: Ctx k -> * where
+data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
   Empty :: BinomialTree h f EmptyCtx
 
   -- Contains size of the subtree, subtree, then element.
@@ -607,18 +599,11 @@
 ------------------------------------------------------------------------
 -- Dropping
 
-type family InitCtx (x :: Ctx k) :: Ctx k
-type instance InitCtx (x ::> y) = x
-
-type family LastCtx (x :: Ctx k) :: k
-type instance LastCtx (x ::> y) = y
-
---
 data DropResult f (ctx :: Ctx k) where
   DropEmpty :: DropResult f EmptyCtx
-  DropExt   :: BinomialTree 'Zero f (InitCtx ctx)
-            -> f (LastCtx ctx)
-            -> DropResult f ctx
+  DropExt   :: BinomialTree 'Zero f x
+            -> f y
+            -> DropResult f (x ::> y)
 
 -- | 'bal_drop x y' returns the tree formed 'append x (init y)'
 bal_drop :: forall h f x y
@@ -703,13 +688,17 @@
 ------------------------------------------------------------------------
 -- Assignment
 
-type role Assignment representational nominal
-
 -- | An assignment is a sequence that maps each index with type 'tp' to
 -- a value of type 'f tp'.
-newtype Assignment (f :: k -> *) (ctx :: Ctx k)
+--
+-- This assignment implementation uses a binomial tree implementation
+-- that offers lookups and updates in time and space logarithmic with
+-- respect to the number of elements in the context.
+newtype Assignment (f :: k -> Type) (ctx :: Ctx k)
       = Assignment (BinomialTree 'Zero f ctx)
 
+type role Assignment nominal nominal
+
 instance NFData (Assignment f ctx) where
   rnf a = seq a ()
 
@@ -717,27 +706,6 @@
 size :: Assignment f ctx -> Size ctx
 size (Assignment t) = Size (tsize t)
 
--- | Generate an assignment with some context type that is not known.
-generateSome :: forall f
-              . Int
-             -> (Int -> Some f)
-             -> Some (Assignment f)
-generateSome n f = go n
-  where go :: Int -> Some (Assignment f)
-        go 0 = Some empty
-        go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1))
-
--- | Generate an assignment with some context type that is not known.
-generateSomeM :: forall m f
-              .  Applicative m
-              => Int
-              -> (Int -> m (Some f))
-              -> m (Some (Assignment f))
-generateSomeM n f = go n
-  where go :: Int -> m (Some (Assignment f))
-        go 0 = pure (Some empty)
-        go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1)
-
 -- | @replicate n@ make a context with different copies of the same
 -- polymorphic value.
 replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx
@@ -763,11 +731,6 @@
 empty :: Assignment f EmptyCtx
 empty = Assignment Empty
 
--- | Return true if assignment is empty.
-null :: Assignment f ctx -> Bool
-null (Assignment Empty) = True
-null (Assignment _) = False
-
 extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
 extend (Assignment x) y = Assignment $ append x (BalLeaf y)
 
@@ -823,6 +786,14 @@
 
 instance ShowF f => ShowF (Assignment f)
 
+{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
+adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)
+
+{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}
+update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
+update i v a = adjust (\_ -> v) i a
+
 -- | Modify the value of an assignment at a particular index.
 adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
 adjustM f (Index i) (Assignment a) = Assignment <$> (unsafe_bin_adjust f a i 0)
@@ -831,22 +802,12 @@
 type instance IndexF       (Assignment f ctx) = Index ctx
 type instance IxValueF     (Assignment f ctx) = f
 
-instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where
-  ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
-  ixF idx f = adjustM f idx
-
-instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where
+instance forall (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) ctx) where
   ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
   ixF' idx f = adjustM f idx
 
-
--- | Modify the value of an assignment at a particular index.
-adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
-adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)
-
--- | Update the assignment at a particular index.
-update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
-update i v a = adjust (\_ -> v) i a
+instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
+  ixF = ixF'
 
 -- This is an unsafe version of update that changes the type of the expression.
 unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
@@ -860,26 +821,11 @@
                -> AssignView f (ctx::>tp)
 
 -- | View an assignment as either empty or an assignment with one appended.
-view :: forall f ctx . Assignment f ctx -> AssignView f ctx
-view (Assignment x) =
+viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
+viewAssign (Assignment x) =
   case bin_drop x of
     DropEmpty -> AssignEmpty
-    DropExt t v -> unsafeCoerce $ AssignExtend (Assignment (unsafeCoerce t)) v
-
--- | Return assignment with all but the last block.
-init :: Assignment f (ctx '::> tp) -> Assignment f ctx
-init (Assignment x) =
-  case bin_drop x of
-    DropExt t _ -> Assignment t
-
--- | Return the last element in the assignment.
-last :: Assignment f (ctx '::> tp) -> f tp
-last x =
-  case view x of
-    AssignExtend _ e -> e
-
-decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
-decompose x = case view x of AssignExtend a v -> (a,v)
+    DropExt t v -> AssignExtend (Assignment t) v
 
 zipWith :: (forall x . f x -> g x -> h x)
         -> Assignment f a
@@ -913,13 +859,6 @@
                   -> Assignment f ctx
                   -> m (Assignment g ctx)
 traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i)
-
--- | Create an assignment from a list of values.
-fromList :: [Some f] -> Some (Assignment f)
-fromList = go empty
-  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
-        go prev [] = Some prev
-        go prev (Some g:next) = (go $! prev `extend` g) next
 
 ------------------------------------------------------------------------
 -- Appending
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
@@ -29,6 +29,7 @@
   , indexed
   , imap
   , ifoldr
+  , izipWith
   , itraverse
     -- * Constants
   , index0
@@ -51,8 +52,13 @@
 infixr 5 :<
 
 instance ShowF f => Show (List f sh) where
-  show Nil = "Nil"
-  show (elt :< rest) = showF elt ++ " :< " ++ show rest
+  showsPrec _ Nil = showString "Nil"
+  showsPrec p (elt :< rest) = showParen (p > precCons) $
+    -- Unlike a derived 'Show' instance, we don't print parens implied
+    -- by right associativity.
+    showsPrecF (precCons+1) elt . showString " :< " . showsPrec 0 rest
+    where
+      precCons = 5
 
 instance ShowF f => ShowF (List f)
 
@@ -202,6 +208,24 @@
       case ops of
         Nil -> b
         a :< rest -> f (g IndexHere) a (go (\ix -> g (IndexThere ix)) rest b)
+
+-- | Zip up two lists with a zipper function, which can use the index.
+izipWith :: forall a b c sh . (forall tp. Index sh tp -> a tp -> b tp -> c tp)
+         -> List a sh
+         -> List b sh
+         -> List c sh
+izipWith f = go id
+  where
+    go :: forall sh' .
+          (forall tp . Index sh' tp -> Index sh tp)
+       -> List a sh'
+       -> List b sh'
+       -> List c sh'
+    go g as bs =
+      case (as, bs) of
+        (Nil, Nil) -> Nil
+        (a :< as', b :< bs') ->
+          f (g IndexHere) a b :< go (g . IndexThere) as' bs'
 
 -- | Traverse with an additional index.
 itraverse :: forall a b sh t
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -21,6 +21,7 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
 module Data.Parameterized.Map
   ( MapF
     -- * Construction
@@ -69,6 +70,7 @@
 import Control.Monad.Identity
 import Data.List (intercalate, foldl')
 import Data.Maybe ()
+import Data.Kind(Type)
 
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
@@ -105,7 +107,7 @@
 -- MapF
 
 -- | A map from parameterized keys to values with the same paramter type.
-data MapF (k :: v -> *) (a :: v -> *) where
+data MapF (k :: v -> Type) (a :: v -> Type) where
   Bin :: {-# UNPACK #-}
          !Size -- Number of elements in tree.
       -> !(k x)
@@ -205,12 +207,12 @@
 type instance IxValueF (MapF k v) = v
 
 -- | Turn a map key into a traversal that visits the indicated element in the map, if it exists.
-instance forall (k:: a -> *) v. OrdF k => IxedF a (MapF k v) where
+instance forall (k:: a -> Type) v. OrdF k => IxedF a (MapF k v) where
   ixF :: k x -> Traversal' (MapF k v) (v x)
   ixF i f m = updatedValue <$> updateAtKey i (pure Nothing) (\x -> Set <$> f x) m
 
 -- | Turn a map key into a lens that points into the indicated position in the map.
-instance forall (k:: a -> *) v. OrdF k => AtF a (MapF k v) where
+instance forall (k:: a -> Type) v. OrdF k => AtF a (MapF k v) where
   atF :: k x -> Lens' (MapF k v) (Maybe (v x))
   atF i f m = updatedValue <$> updateAtKey i (f Nothing) (\x -> maybe Delete Set <$> f (Just x)) m
 
@@ -425,7 +427,7 @@
 
 -- | Generate a map from a foldable collection of keys and a
 -- function from keys to values.
-fromKeys :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *)
+fromKeys :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
           .  (Monad m, Foldable t, OrdF a)
             => (forall tp . a tp -> m (v tp))
             -- ^ Function for evaluating a register value.
@@ -438,7 +440,7 @@
 
 -- | Generate a map from a foldable collection of keys and a monadic
 -- function from keys to values.
-fromKeysM :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *)
+fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
           .  (Monad m, Foldable t, OrdF a)
            => (forall tp . a tp -> m (v tp))
            -- ^ Function for evaluating a register value.
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
@@ -26,6 +26,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
 #if MIN_VERSION_base(4,9,0)
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 #endif
@@ -43,6 +44,7 @@
   , incNat
   , addNat
   , subNat
+  , divNat
   , halfNat
   , withDivModNat
   , natMultiply
@@ -78,16 +80,24 @@
   , leqAdd
   , leqSub
   , leqMulPos
+  , leqAddPos
   , addIsLeq
   , withAddLeq
   , addPrefixIsLeq
   , withAddPrefixLeq
   , addIsLeqLeft1
   , dblPosIsPos
+  , leqMulMono
     -- * Arithmetic proof
   , plusComm
+  , mulComm
   , plusMinusCancel
+  , minusPlusCancel
+  , addMulDistribRight
   , withAddMulDistribRight
+  , withSubMulDistribRight
+  , mulCancelR
+  , mul2Plus
     -- * Re-exports typelists basics
 --  , NatK
   , type (+)
@@ -140,17 +150,17 @@
 -- | Result of comparing two numbers.
 data NatComparison m n where
   -- First number is less than second.
-  NatLT :: !(NatRepr y) -> NatComparison x (x+(y+1))
+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))
   NatEQ :: NatComparison x x
   -- First number is greater than second.
-  NatGT :: !(NatRepr y) -> NatComparison (x+(y+1)) x
+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x
 
 compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
 compareNat m n =
   case compare (natValue m) (natValue n) of
-    LT -> unsafeCoerce $ NatLT (NatRepr (natValue n - natValue m - 1))
-    EQ -> unsafeCoerce $ NatEQ
-    GT -> unsafeCoerce $ NatGT (NatRepr (natValue m - natValue n - 1))
+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))
+    EQ -> unsafeCoerce  NatEQ
+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))
 
 instance OrdF NatRepr where
   compareF x y =
@@ -215,6 +225,9 @@
 subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n)
 subNat (NatRepr m) (NatRepr n) = NatRepr (m-n)
 
+divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
+divNat (NatRepr x) (NatRepr y) = NatRepr (div x y)
+
 withDivModNat :: forall n m a.
                  NatRepr n
               -> NatRepr m
@@ -264,7 +277,7 @@
   where i = i0 .&. maxUnsigned w
 
 -- | @unsignedClamp w i@ rounds @i@ to the nearest value between
--- @0@ and @2^w-i@ (inclusive).
+-- @0@ and @2^w-1@ (inclusive).
 unsignedClamp :: NatRepr w -> Integer -> Integer
 unsignedClamp w i
   | i < minUnsigned w = minUnsigned w
@@ -272,7 +285,7 @@
   | otherwise         = i
 
 -- | @signedClamp w i@ rounds @i@ to the nearest value between
--- @-2^(w-1)@ and @2^(w-1)-i@ (inclusive).
+-- @-2^(w-1)@ and @2^(w-1)-1@ (inclusive).
 signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer
 signedClamp w i
   | i < minSigned w = minSigned w
@@ -299,16 +312,41 @@
 plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m
 plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n)
 
+-- | Produce evidence that * is commutative.
+mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
+mulComm _ _ = unsafeCoerce Refl
+
+mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
+mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of
+               Refl -> Refl
+
 -- | Cancel an add followed b a subtract
 plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m
 plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m)
 
+minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m
+minusPlusCancel _ _ = unsafeCoerce (Refl :: m :~: m)
+
+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
+
+
+
 withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p
                     -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
-withAddMulDistribRight _n _m _p f =
+withAddMulDistribRight n m p f =
+  case addMulDistribRight n m p of
+    Refl -> f
+
+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
-    (Refl :: (((n * p) + (m * p)) :~: ((n + m) * p)) ) -> f
+    (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f
 
+
+
 ------------------------------------------------------------------------
 -- LeqProof
 
@@ -379,7 +417,7 @@
 -- LeqProof combinators
 
 -- | Create a leqProof using two proxies
-leqProof :: (m <= n) => f m -> f n -> LeqProof m n
+leqProof :: (m <= n) => f m -> g n -> LeqProof m n
 leqProof _ _ = LeqProof
 
 withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a
@@ -406,11 +444,17 @@
           -> LeqProof 1 (x*y)
 leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y)
 
+leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)
+leqMulMono x y = leqMulCongr (leqProof (Proxy :: Proxy 1) x) (leqRefl y)
+
 -- | Produce proof that adding a value to the larger element in an LeqProof
 -- is larger
 leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)
 leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p)
 
+leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
+leqAddPos m n = leqAdd (leqProof (Proxy :: Proxy 1) m) n
+
 -- | Produce proof that subtracting a value from the smaller element is smaller.
 leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n
 leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p)
@@ -477,3 +521,7 @@
     go n' = case isZeroNat n' of
               ZeroNat    -> f0
               NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')
+
+mulCancelR ::
+  (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
+mulCancelR _ _ _ = unsafeCoerce Refl
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
@@ -14,7 +14,9 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE EmptyCase #-}
 module Data.Parameterized.TH.GADT
-  ( structuralEquality
+  ( -- * Instance generators
+    -- $typePatterns
+  structuralEquality
   , structuralTypeEquality
   , structuralTypeOrd
   , structuralTraversal
@@ -71,6 +73,9 @@
 ------------------------------------------------------------------------
 -- TypePat
 
+-- | A type used to describe (and match) types appearing in generated pattern
+-- matches inside of the TH generators in this module ('structuralEquality',
+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal')
 data TypePat
    = TypeApp TypePat TypePat -- ^ The application of a type.
    | AnyType       -- ^ Match any type.
@@ -117,7 +122,7 @@
 typeVars = Set.fromList . freeVariables
 
 
--- | @declareStructuralEquality@ declares a structural equality predicate.
+-- | @structuralEquality@ declares a structural equality predicate.
 structuralEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ
 structuralEquality tpq pats =
   [| \x y -> isJust ($(structuralTypeEquality tpq pats) x y) |]
@@ -208,7 +213,7 @@
     then [| \x -> case x of {} |]
     else [| \x y -> $(caseE [| x |] (trueEqs [| y |])) |]
 
--- | @structuralTypeEquality f@ returns a function with the type:
+-- | @structuralTypeOrd f@ returns a function with the type:
 --   forall x y . f x -> f y -> OrderingF x y
 --
 -- This implementation avoids matching on both the first and second
@@ -441,3 +446,43 @@
 
 matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ
 matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con))
+
+-- $typePatterns
+--
+-- The Template Haskell instance generators 'structuralEquality',
+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal'
+-- employ heuristics to generate valid instances in the majority of cases.  Most
+-- failures in the heuristics occur on sub-terms that are type indexed.  To
+-- handle cases where these functions fail to produce a valid instance, they
+-- take a list of exceptions in the form of their second parameter, which has
+-- type @[('TypePat', 'ExpQ')]@.  Each 'TypePat' is a /matcher/ that tells the
+-- TH generator to use the 'ExpQ' to process the matched sub-term.  Consider the
+-- following example:
+--
+-- > data T a b where
+-- >   C1 :: NatRepr n -> T () n
+-- >
+-- > instance TestEquality (T a) where
+-- >   testEquality = $(structuralTypeEquality [t|T|]
+-- >                    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
+-- >                    ])
+--
+-- The exception list says that 'structuralTypeEquality' should use
+-- 'testEquality' to compare any sub-terms of type @'NatRepr' n@ in a value of
+-- type @T@.
+--
+-- * 'AnyType' means that the type parameter in that position can be instantiated as any type
+--
+-- * @'DataArg' n@ means that the type parameter in that position is the @n@-th
+--   type parameter of the GADT being traversed (@T@ in the example)
+--
+-- * 'TypeApp' is type application
+--
+-- * 'ConType' specifies a base type
+--
+-- The exception list could have equivalently (and more precisely) have been specified as:
+--
+-- > [(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]
+--
+-- The use of 'DataArg' says that the type parameter of the 'NatRepr' must
+-- be the same as the second type parameter of @T@.
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
@@ -24,11 +24,10 @@
 import Control.Applicative
 import Control.Monad.Identity
 import Data.Coerce
-import Data.Functor.Const
 import Data.Monoid
 import GHC.Exts (build)
 
--- | A parameterized type that is a function on all instances.
+-- | A parameterized type that is a functor on all instances.
 class FunctorF m where
   fmapF :: (forall x . f x -> g x) -> m f -> m g
 
@@ -38,7 +37,7 @@
 ------------------------------------------------------------------------
 -- FoldableF
 
--- | This is a coercision used to avoid overhead associated
+-- | This is a coercion used to avoid overhead associated
 -- with function composition.
 (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
 (#.) _f = coerce
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,9 +38,9 @@
 import Data.Parameterized.Classes
 
 -- | A parameterized type that is a function on all instances.
-class FunctorFC m where
-  fmapFC :: forall f g. (forall x . f x -> g x) ->
-                        (forall x . m f x -> m g x)
+class FunctorFC (t :: (k -> *) -> l -> *) 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.
@@ -89,74 +89,73 @@
 
   -- | Map each element of the structure to a monoid,
   -- and combine the results.
-  foldMapFC :: Monoid m => (forall s . e s -> m) -> t e c -> m
+  foldMapFC :: forall f m. Monoid m => (forall x. f x -> m) -> (forall x. t f x -> m)
   foldMapFC f = foldrFC (mappend . f) mempty
 
   -- | Right-associative fold of a structure.
-  foldrFC :: (forall s . e s -> b -> b) -> b -> t e c -> b
+  foldrFC :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)
   foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z
 
   -- | Left-associative fold of a structure.
-  foldlFC :: (forall s . b -> e s -> b) -> b -> t e c -> b
+  foldlFC :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)
   foldlFC f z t = appEndo (getDual (foldMapFC (\e -> Dual (Endo (\r -> f r e))) t)) z
 
   -- | Right-associative fold of a structure,
   -- but with strict application of the operator.
-  foldrFC' :: (forall s . e s -> b -> b) -> b -> t e c -> b
+  foldrFC' :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)
   foldrFC' f0 z0 xs = foldlFC (f' f0) id xs z0
     where f' f k x z = k $! f x z
 
   -- | Left-associative fold of a parameterized structure
   -- with a strict accumulator.
-  foldlFC' :: (forall s . b -> e s -> b) -> b -> t e c -> b
+  foldlFC' :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)
   foldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0
     where f' f x k z = k $! f z x
 
   -- | Convert structure to list.
-  toListFC :: (forall tp . f tp -> a) -> t f c -> [a]
+  toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])
   toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)
 
 -- | Return 'True' if all values satisfy predicate.
-allFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool
+allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)
 allFC p = getAll #. foldMapFC (All #. p)
 
 -- | Return 'True' if any values satisfy predicate.
-anyFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool
+anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)
 anyFC p = getAny #. foldMapFC (Any #. p)
 
 -- | Return number of elements in list.
-lengthFC :: FoldableFC t => t e c -> Int
+lengthFC :: FoldableFC t => t f x -> Int
 lengthFC = foldrFC (const (+1)) 0
 
 ------------------------------------------------------------------------
 -- TraversableF
 
-class (FunctorFC t, FoldableFC t) => TraversableFC t where
-  traverseFC :: Applicative m
-             => (forall s . e s -> m (f s))
-             -> t e c
-             -> m (t f c)
+class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *) where
+  traverseFC :: forall f g m. Applicative m
+             => (forall x. f x -> m (g x))
+             -> (forall x. t f x -> m (t g x))
 
 -- | This function may be used as a value for `fmapF` in a `FunctorF`
 -- instance.
-fmapFCDefault :: TraversableFC t => (forall s . e s -> f s) -> t e c -> t f c
+fmapFCDefault :: TraversableFC t => forall f g. (forall x. f x -> g x) -> (forall x. t f x -> t g x)
 fmapFCDefault = \f -> runIdentity . traverseFC (Identity . f)
 {-# INLINE fmapFCDefault #-}
 
 -- | This function may be used as a value for `Data.Foldable.foldMap`
 -- in a `Foldable` instance.
-foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall s . e s -> m) -> t e c -> m
+foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)
 foldMapFCDefault = \f -> getConst . traverseFC (Const . f)
 {-# INLINE foldMapFCDefault #-}
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-traverseFC_ :: (FoldableFC t, Applicative f) => (forall s . e s  -> f ()) -> t e c -> f ()
+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())
 traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ())
 {-# INLINE traverseFC_ #-}
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-forMFC_ :: (FoldableFC t, Applicative f) => t e c -> (forall s . e s  -> f ()) -> f ()
+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()
 forMFC_ v f = traverseFC_ f v
 {-# INLINE forMFC_ #-}
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -11,6 +11,7 @@
 import Test.QuickCheck
 import Test.Tasty.QuickCheck
 
+import Control.Lens
 import Data.Parameterized.Classes
 import Data.Parameterized.TraversableFC
 import Data.Parameterized.Some
@@ -90,8 +91,8 @@
          Some a <- return $ mkUAsgn vals
          let vals' = toListFC Some a
          return (vals == vals')
-   , testProperty "adjust_test" $ \v vs i -> ioProperty $ do
-         let vals = v:vs
+   , testProperty "adjust test monadic" $ \v vs i -> ioProperty $ do
+         let vals = v:vs  -- ensures vals is not an empty array
          Some x <- return $ mkUAsgn vals
          Some y <- return $ mkSAsgn vals
          let i' = min (max 0 i) (length vals - 1)
@@ -99,10 +100,61 @@
          Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
          Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
 
-         let x' = U.adjust twiddle idx_x x
-         let y' = S.adjust twiddle idx_y y
+         x' <- U.adjustM (return . twiddle) idx_x x
+         y' <- S.adjustM (return . twiddle) idx_y y
 
          return (toListFC Some x' == toListFC Some y')
+
+   , testProperty "adjust test" $ \v vs i -> ioProperty $ do
+         let vals = v:vs  -- ensures vals is not an empty array
+         Some x <- return $ mkUAsgn vals
+         Some y <- return $ mkSAsgn vals
+         let i' = min (max 0 i) (length vals - 1)
+
+         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+
+         let x' = over (ixF idx_x) twiddle x
+             y' = (ixF idx_y) %~ twiddle $ y
+             x'' = U.adjust twiddle idx_x x
+             y'' = S.adjust twiddle idx_y y
+
+         return (toListFC Some x' == toListFC Some y' &&
+                 -- adjust actually modified the entry
+                 toListFC Some x /= toListFC Some x' &&
+                 toListFC Some y /= toListFC Some y' &&
+                 -- verify new version is equivalent to older deprecated version
+                 toListFC Some x'' == toListFC Some x' &&
+                 toListFC Some y'' == toListFC Some y')
+
+   , testProperty "update test" $ \v vs i -> ioProperty $ do
+         let vals = v:vs  -- ensures vals is not an empty array
+         Some x <- return $ mkUAsgn vals
+         Some y <- return $ mkSAsgn vals
+         let i' = min (max 0 i) (length vals - 1)
+
+         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)
+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)
+
+         let x' = over (ixF idx_x) twiddle x
+             y' = (ixF idx_y) %~ twiddle $ y
+             updX = set (ixF idx_x) (x' U.! idx_x) x
+             updY = (ixF idx_y) .~  (y' S.! idx_y) $ y
+             updX' = U.update idx_x (x' U.! idx_x) x
+             updY' = S.update idx_y (y' S.! idx_y) y
+
+         return (toListFC Some updX == toListFC Some updY &&
+                 -- update actually modified the entry
+                 toListFC Some x /= toListFC Some updX &&
+                 toListFC Some y /= toListFC Some updY &&
+                 -- update modified the expected entry
+                 toListFC Some x' == toListFC Some updX &&
+                 toListFC Some y' == toListFC Some updY &&
+                 -- verify new version is equivalent to older deprecated version
+                 toListFC Some updX == toListFC Some updX' &&
+                 toListFC Some updY == toListFC Some updY'
+                )
+
    , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do
          Some x <- return $ mkSAsgn vals1
          Some y <- return $ mkSAsgn vals2