    {-|
    Module           : Data.Parameterized.Context
    Copyright        : (c) Galois, Inc 2014-2019
    Maintainer       : Joe Hendrix <jhendrix@galois.com>

    This module reexports either "Data.Parameterized.Context.Safe"
    or "Data.Parameterized.Context.Unsafe" depending on the
    the unsafe-operations compile-time flag.

    It also defines some utility typeclasses for transforming
    between curried and uncurried versions of functions over contexts.

    The 'Assignment' type is isomorphic to the 'Data.Parameterized.List'
    type, except 'Assignment's construct lists from the right-hand side,
    and instead of using type-level @'[]@-style lists, an 'Assignment' is
    indexed by a type-level 'Data.Parameterized.Context.Ctx'. The
    implementation of 'Assignment's is also more efficent than
    'Data.Parameterized.List' for lists of many elements, as it uses a
    balanced binary tree representation rather than a linear-time
    list. For a motivating example, see 'Data.Parameterized.List'.

    -}

    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE FunctionalDependencies #-}
    {-# LANGUAGE InstanceSigs #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE ViewPatterns #-}
    module Data.Parameterized.Context
     (
    #ifdef UNSAFE_OPS
        module Data.Parameterized.Context.Unsafe
    #else
        module Data.Parameterized.Context.Safe
    #endif
      , singleton
      , toVector
      , pattern (:>)
      , pattern Empty
      , decompose
      , Data.Parameterized.Context.null
      , Data.Parameterized.Context.init
      , Data.Parameterized.Context.last
      , Data.Parameterized.Context.view
      , Data.Parameterized.Context.take
      , Data.Parameterized.Context.drop
      , forIndexM
      , generateSome
      , generateSomeM
      , fromList
      , traverseAndCollect
      , traverseWithIndex_
      , dropPrefix
      , unzip
      , flattenAssignment
      , flattenSize

        -- * Context extension and embedding utilities
      , CtxEmbedding(..)
      , ExtendContext(..)
      , ExtendContext'(..)
      , ApplyEmbedding(..)
      , ApplyEmbedding'(..)
      , identityEmbedding
      , extendEmbeddingRightDiff
      , extendEmbeddingRight
      , extendEmbeddingBoth
      , appendEmbedding
      , appendEmbeddingLeft
      , ctxeSize
      , ctxeAssignment

        -- * 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           Prelude hiding (unzip)

    import qualified Control.Applicative as App (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 (-))

    import           Data.Parameterized.Classes
    import           Data.Parameterized.Some
    import           Data.Parameterized.TraversableFC

    #ifdef UNSAFE_OPS
    import           Data.Parameterized.Context.Unsafe
    #else
    import           Data.Parameterized.Context.Safe
    #endif

    -- | Create a single element context.
    singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
    singleton :: forall {k} (f :: k -> *) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    singleton = (Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty Assignment f EmptyCtx -> f tp -> Assignment f (EmptyCtx ::> tp)
    forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :>)

    -- |'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 :: forall {k} (ctx :: Ctx k) (m :: * -> *).
    Applicative m =>
    Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
    forIndexM Size ctx
    sz forall (tp :: k). Index ctx tp -> m ()
    f = Int
    -> Size ctx
    -> (forall (tp :: k). Index ctx tp -> m () -> m ())
    -> m ()
    -> m ()
    forall {k} (ctx :: Ctx k) r.
    Int
    -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
    forIndexRange Int
    0 Size ctx
    sz (\Index ctx tp
    i m ()
    r -> Index ctx tp -> m ()
    forall (tp :: k). Index ctx tp -> m ()
    f Index ctx tp
    i m () -> m () -> m ()
    forall a b. m a -> m b -> m b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> m ()
    r) (() -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ())

    -- | Generate an assignment with some context type that is not known.
    generateSome :: forall f
                  . Int
                 -> (Int -> Some f)
                 -> Some (Assignment f)
    generateSome :: forall {k} (f :: k -> *).
    Int -> (Int -> Some f) -> Some (Assignment f)
    generateSome Int
    n Int -> Some f
    f = Int -> Some (Assignment f)
    go Int
    n
      where go :: Int -> Some (Assignment f)
            go :: Int -> Some (Assignment f)
    go Int
    0 = Assignment f EmptyCtx -> Some (Assignment f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty
            go Int
    i = (\(Some Assignment f x
    a) (Some f x
    e) -> Assignment f (x ::> x) -> Some (Assignment f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (Assignment f x
    a Assignment f x -> f x -> Assignment f (x ::> x)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    `extend` f x
    e)) (Int -> Some (Assignment f)
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)) (Int -> Some f
    f (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    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 :: forall {k} (m :: * -> *) (f :: k -> *).
    Applicative m =>
    Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
    generateSomeM Int
    n Int -> m (Some f)
    f = Int -> m (Some (Assignment f))
    go Int
    n
      where go :: Int -> m (Some (Assignment f))
            go :: Int -> m (Some (Assignment f))
    go Int
    0 = Some (Assignment f) -> m (Some (Assignment f))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Assignment f EmptyCtx -> Some (Assignment f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty)
            go Int
    i = (\(Some Assignment f x
    a) (Some f x
    e) -> Assignment f (x ::> x) -> Some (Assignment f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (Assignment f x
    a Assignment f x -> f x -> Assignment f (x ::> x)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    `extend` f x
    e)) (Some (Assignment f) -> Some f -> Some (Assignment f))
    -> m (Some (Assignment f)) -> m (Some f -> Some (Assignment f))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Some (Assignment f))
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) m (Some f -> Some (Assignment f))
    -> m (Some f) -> m (Some (Assignment f))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> m (Some f)
    f (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

    -- | Convert the assignment to a vector.
    toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e
    toVector :: forall {k} (f :: k -> *) (tps :: Ctx k) e.
    Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
    toVector Assignment f tps
    a forall (tp :: k). f tp -> e
    f = (forall s. ST s (MVector s e)) -> Vector e
    forall a. (forall s. ST s (MVector s a)) -> Vector a
    V.create ((forall s. ST s (MVector s e)) -> Vector e)
    -> (forall s. ST s (MVector s e)) -> Vector e
    forall a b. (a -> b) -> a -> b
    $ do
      vm <- Int -> ST s (MVector (PrimState (ST s)) e)
    forall (m :: * -> *) a.
    PrimMonad m =>
    Int -> m (MVector (PrimState m) a)
    MV.new (Size tps -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt (Assignment f tps -> Size tps
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f tps
    a))
      forIndexM (size a) $ \Index tps tp
    i -> do
        MVector (PrimState (ST s)) e -> Int -> e -> ST s ()
    forall (m :: * -> *) a.
    PrimMonad m =>
    MVector (PrimState m) a -> Int -> a -> m ()
    MV.write MVector s e
    MVector (PrimState (ST s)) e
    vm (Index tps tp -> Int
    forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal Index tps tp
    i) (f tp -> e
    forall (tp :: k). f tp -> e
    f (Assignment f tps
    a Assignment f tps -> Index tps tp -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index tps tp
    i))
      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.
    dropPrefix :: forall f xs prefix a.
      TestEquality f =>
      Assignment f xs     {- ^ Assignment to split -} ->
      Assignment f prefix {- ^ Expected prefix -} ->
      a {- ^ error continuation -} ->
      (forall addl. (xs ~ (prefix <+> addl)) => Assignment f addl -> a)
        {- ^ success continuation -} ->
      a
    dropPrefix :: forall {k} (f :: k -> *) (xs :: Ctx k) (prefix :: Ctx k) a.
    TestEquality f =>
    Assignment f xs
    -> Assignment f prefix
    -> a
    -> (forall (addl :: Ctx k).
        (xs ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    dropPrefix Assignment f xs
    xs0 Assignment f prefix
    prefix a
    err = Assignment f xs
    -> Int
    -> (forall (addl :: Ctx k).
        (xs ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    forall (ys :: Ctx k).
    Assignment f ys
    -> Int
    -> (forall (addl :: Ctx k).
        (ys ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    go Assignment f xs
    xs0 (Size xs -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt (Assignment f xs -> Size xs
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f xs
    xs0))
      where
      sz_prefix :: Int
    sz_prefix = Size prefix -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt (Assignment f prefix -> Size prefix
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f prefix
    prefix)

      go :: forall ys.
       Assignment f ys ->
       Int ->
       (forall addl. (ys ~ (prefix <+> addl)) => Assignment f addl -> a) ->
       a

      go :: forall (ys :: Ctx k).
    Assignment f ys
    -> Int
    -> (forall (addl :: Ctx k).
        (ys ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    go (Assignment f ctx
    xs' :> f tp
    z) Int
    sz_x forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a
    success | Int
    sz_x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    sz_prefix =
        Assignment f ctx
    -> Int
    -> (forall (addl :: Ctx k).
        (ctx ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    forall (ys :: Ctx k).
    Assignment f ys
    -> Int
    -> (forall (addl :: Ctx k).
        (ys ~ (prefix <+> addl)) =>
        Assignment f addl -> a)
    -> a
    go Assignment f ctx
    xs' (Int
    sz_xInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (\Assignment f addl
    zs -> Assignment f (addl ::> tp) -> a
    forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a
    success (Assignment f addl
    zs Assignment f addl -> f tp -> Assignment f (addl ::> tp)
    forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> f tp
    z))

      go Assignment f ys
    xs Int
    _ forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a
    success =
        case Assignment f ys -> Assignment f prefix -> Maybe (ys :~: prefix)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Ctx k) (b :: Ctx k).
    Assignment f a -> Assignment f b -> Maybe (a :~: b)
    testEquality Assignment f ys
    xs Assignment f prefix
    prefix of
          Just ys :~: prefix
    Refl -> Assignment f EmptyCtx -> a
    forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a
    success Assignment f EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Empty
          Maybe (ys :~: prefix)
    Nothing   -> a
    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 :: forall {k} (f :: k -> *) (g :: k -> *) (ctx :: Ctx k).
    Assignment (Product f g) ctx
    -> (Assignment f ctx, Assignment g ctx)
    unzip Assignment (Product f g) ctx
    fgs =
      case Assignment (Product f g) ctx -> AssignView (Product f g) ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment (Product f g) ctx
    fgs of
        AssignView (Product f g) ctx
    AssignEmpty -> (Assignment f ctx
    Assignment f 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty, Assignment g ctx
    Assignment g 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty)
        AssignExtend Assignment (Product f g) ctx1
    rest (Pair f tp
    f g tp
    g) ->
          let (Assignment f ctx1
    fs, Assignment g ctx1
    gs) = Assignment (Product f g) ctx1
    -> (Assignment f ctx1, Assignment g ctx1)
    forall {k} (f :: k -> *) (g :: k -> *) (ctx :: Ctx k).
    Assignment (Product f g) ctx
    -> (Assignment f ctx, Assignment g ctx)
    unzip Assignment (Product f g) ctx1
    rest
          in (Assignment f ctx1 -> f tp -> Assignment f (ctx1 '::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend Assignment f ctx1
    fs f tp
    f, Assignment g ctx1 -> g tp -> Assignment g (ctx1 '::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend Assignment g ctx1
    gs g tp
    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 :: forall {a} (f :: a -> *) (ctxs :: Ctx (Ctx a)).
    Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
    flattenAssignment Assignment (Assignment f) ctxs
    ctxs =
      case Assignment (Assignment f) ctxs -> AssignView (Assignment f) ctxs
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment (Assignment f) ctxs
    ctxs of
        AssignView (Assignment f) ctxs
    AssignEmpty -> Assignment f (CtxFlatten ctxs)
    Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty
        AssignExtend Assignment (Assignment f) ctx1
    ctxs' Assignment f tp
    ctx -> Assignment (Assignment f) ctx1 -> Assignment f (CtxFlatten ctx1)
    forall {a} (f :: a -> *) (ctxs :: Ctx (Ctx a)).
    Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
    flattenAssignment Assignment (Assignment f) ctx1
    ctxs' Assignment f (CtxFlatten ctx1)
    -> Assignment f tp -> Assignment f (CtxFlatten ctx1 <+> tp)
    forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    Assignment f x -> Assignment f y -> Assignment f (x <+> y)
    <++> Assignment f tp
    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 :: forall {k} (ctxs :: Ctx (Ctx k)).
    Assignment Size ctxs -> Size (CtxFlatten ctxs)
    flattenSize Assignment Size ctxs
    a =
      case Assignment Size ctxs -> AssignView Size ctxs
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment Size ctxs
    a of
        AssignView Size ctxs
    AssignEmpty -> Size (CtxFlatten ctxs)
    Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    zeroSize
        AssignExtend Assignment Size ctx1
    b Size tp
    s -> Size (CtxFlatten ctx1) -> Size tp -> Size (CtxFlatten ctx1 <+> tp)
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize (Assignment Size ctx1 -> Size (CtxFlatten ctx1)
    forall {k} (ctxs :: Ctx (Ctx k)).
    Assignment Size ctxs -> Size (CtxFlatten ctxs)
    flattenSize Assignment Size ctx1
    b) Size tp
    s

    --------------------------------------------------------------------------------
    -- Patterns

    -- | Pattern synonym for the empty assignment
    pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
    pattern $mEmpty :: forall {r} {k} {ctx :: Ctx k} {f :: k -> *}.
    Assignment f ctx -> ((ctx ~ EmptyCtx) => r) -> ((# #) -> r) -> r
    $bEmpty :: forall {k} (ctx :: Ctx k) (f :: k -> *).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Empty <- (viewAssign -> AssignEmpty)
      where Empty = Assignment f ctx
    Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty

    infixl :>

    -- | Pattern synonym for extending an assignment on the right
    pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
    pattern $m:> :: forall {r} {k} {ctx' :: Ctx k} {f :: k -> *}.
    Assignment f ctx'
    -> (forall {ctx :: Ctx k} {tp :: k}.
        (ctx' ~ (ctx ::> tp)) =>
        Assignment f ctx -> f tp -> r)
    -> ((# #) -> r)
    -> r
    $b:> :: forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    (:>) a v <- (viewAssign -> AssignExtend a v)
      where Assignment f ctx
    a :> f tp
    v = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend Assignment f ctx
    a f tp
    v

    {-# COMPLETE (:>), Empty :: Assignment  #-}

    --------------------------------------------------------------------------------
    -- Views

    -- | Return true if assignment is empty.
    null :: Assignment f ctx -> Bool
    null :: forall {k} (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Bool
    null Assignment f ctx
    a =
      case Assignment f ctx -> AssignView f ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f ctx
    a of
        AssignView f ctx
    AssignEmpty -> Bool
    True
        AssignExtend{} -> Bool
    False

    decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
    decompose :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
    decompose Assignment f (ctx ::> tp)
    x = (Assignment f (ctx ::> tp) -> Assignment f ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f (ctx '::> tp) -> Assignment f ctx
    Data.Parameterized.Context.init Assignment f (ctx ::> tp)
    x, Assignment f (ctx ::> tp) -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f (ctx '::> tp) -> f tp
    Data.Parameterized.Context.last Assignment f (ctx ::> tp)
    x)

    -- | Return assignment with all but the last block.
    init :: Assignment f (ctx '::> tp) -> Assignment f ctx
    init :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f (ctx '::> tp) -> Assignment f ctx
    init Assignment f (ctx '::> tp)
    x =
      case Assignment f (ctx '::> tp) -> AssignView f (ctx '::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f (ctx '::> tp)
    x of
        AssignExtend Assignment f ctx1
    t f tp
    _ -> Assignment f ctx
    Assignment f ctx1
    t

    -- | Return the last element in the assignment.
    last :: Assignment f (ctx '::> tp) -> f tp
    last :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f (ctx '::> tp) -> f tp
    last Assignment f (ctx '::> tp)
    x =
      case Assignment f (ctx '::> tp) -> AssignView f (ctx '::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f (ctx '::> tp)
    x of
        AssignExtend Assignment f ctx1
    _ f tp
    e -> f tp
    f tp
    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 :: forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    view = Assignment f ctx -> AssignView f ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign

    -- | Return the prefix of an appended 'Assignment'
    take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
    take :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx
    -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
    take Size ctx
    sz Size ctx'
    sz' Assignment f (ctx <+> ctx')
    asgn =
      let diff :: Diff ctx (ctx <+> ctx')
    diff = Size ctx' -> Diff ctx (ctx <+> ctx')
    forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff Size ctx'
    sz' in
      Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx
    sz (\Index ctx tp
    i -> Assignment f (ctx <+> ctx')
    asgn Assignment f (ctx <+> ctx') -> Index (ctx <+> ctx') tp -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Diff ctx (ctx <+> ctx') -> Index ctx tp -> Index (ctx <+> ctx') tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff ctx (ctx <+> ctx')
    diff Index ctx tp
    i)

    -- | Return the suffix of an appended 'Assignment'
    drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
    drop :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx
    -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
    drop Size ctx
    sz Size ctx'
    sz' Assignment f (ctx <+> ctx')
    asgn = Size ctx'
    -> (forall (tp :: k). Index ctx' tp -> f tp) -> Assignment f ctx'
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx'
    sz' (\Index ctx' tp
    i -> Assignment f (ctx <+> ctx')
    asgn Assignment f (ctx <+> ctx') -> Index (ctx <+> ctx') tp -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Size ctx -> Size ctx' -> Index ctx' tp -> Index (ctx <+> ctx') tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    extendIndexAppendLeft Size ctx
    sz Size ctx'
    sz' Index ctx' tp
    i)

    --------------------------------------------------------------------------------
    -- Context embedding.

    -- | This datastructure contains a proof that the first context is
    -- embeddable in the second.  This is useful if we want to add extend
    -- an existing term under a larger context.

    data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)
      = CtxEmbedding { forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    CtxEmbedding ctx ctx' -> Size ctx'
    _ctxeSize       :: Size ctx'
                     , forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    CtxEmbedding ctx ctx' -> Assignment (Index ctx') ctx
    _ctxeAssignment :: Assignment (Index ctx') ctx
                     }

    -- Alternate encoding?
    -- data CtxEmbedding ctx ctx' where
    --   EIdentity  :: CtxEmbedding ctx ctx
    --   ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
    --   ExtendOne  :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)

    ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
    ctxeSize :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (f :: * -> *).
    Functor f =>
    (Size ctx' -> f (Size ctx'))
    -> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
    ctxeSize = (CtxEmbedding ctx ctx' -> Size ctx')
    -> (CtxEmbedding ctx ctx' -> Size ctx' -> CtxEmbedding ctx ctx')
    -> Lens
         (CtxEmbedding ctx ctx')
         (CtxEmbedding ctx ctx')
         (Size ctx')
         (Size ctx')
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CtxEmbedding ctx ctx' -> Size ctx'
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    CtxEmbedding ctx ctx' -> Size ctx'
    _ctxeSize (\CtxEmbedding ctx ctx'
    s Size ctx'
    v -> CtxEmbedding ctx ctx'
    s { _ctxeSize = v })

    ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx')
                           (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)
    ctxeAssignment :: forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k)
           (f :: * -> *).
    Functor f =>
    (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2))
    -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')
    ctxeAssignment = (CtxEmbedding ctx1 ctx' -> Assignment (Index ctx') ctx1)
    -> (CtxEmbedding ctx1 ctx'
        -> Assignment (Index ctx') ctx2 -> CtxEmbedding ctx2 ctx')
    -> Lens
         (CtxEmbedding ctx1 ctx')
         (CtxEmbedding ctx2 ctx')
         (Assignment (Index ctx') ctx1)
         (Assignment (Index ctx') ctx2)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CtxEmbedding ctx1 ctx' -> Assignment (Index ctx') ctx1
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    CtxEmbedding ctx ctx' -> Assignment (Index ctx') ctx
    _ctxeAssignment (\CtxEmbedding ctx1 ctx'
    s Assignment (Index ctx') ctx2
    v -> CtxEmbedding ctx1 ctx'
    s { _ctxeAssignment = v })

    class ApplyEmbedding (f :: Ctx k -> Type) where
      applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx'

    class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where
      applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v

    class ExtendContext (f :: Ctx k -> Type) where
      extendContext :: Diff ctx ctx' -> f ctx -> f ctx'

    class ExtendContext' (f :: Ctx k -> k' -> Type) where
      extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v

    instance ApplyEmbedding' Index where
      applyEmbedding' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k').
    CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v
    applyEmbedding' CtxEmbedding ctx ctx'
    ctxe Index ctx v
    idx = (CtxEmbedding ctx ctx'
    ctxe CtxEmbedding ctx ctx'
    -> Getting
         (Assignment (Index ctx') ctx)
         (CtxEmbedding ctx ctx')
         (Assignment (Index ctx') ctx)
    -> Assignment (Index ctx') ctx
    forall s a. s -> Getting a s a -> a
    ^. Getting
      (Assignment (Index ctx') ctx)
      (CtxEmbedding ctx ctx')
      (Assignment (Index ctx') ctx)
    forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k)
           (f :: * -> *).
    Functor f =>
    (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2))
    -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')
    ctxeAssignment) Assignment (Index ctx') ctx -> Index ctx v -> Index ctx' v
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index ctx v
    idx

    instance ExtendContext' Index where
      extendContext' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k').
    Diff ctx ctx' -> Index ctx v -> Index ctx' v
    extendContext' = Diff ctx ctx' -> Index ctx v -> Index ctx' v
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex'

    -- -- This is the inefficient way of doing things.  A better way is to
    -- -- just have a map between indices.
    -- applyEmbedding :: CtxEmbedding ctx ctx'
    --                -> Index ctx tp -> Index ctx' tp
    -- applyEmbedding ctxe idx = (ctxe ^. ctxeAssignment) ! idx

    identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
    identityEmbedding :: forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx
    identityEmbedding Size ctx
    sz = Size ctx -> Assignment (Index ctx) ctx -> CtxEmbedding ctx ctx
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
    CtxEmbedding Size ctx
    sz (Size ctx
    -> (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Assignment (Index ctx) ctx
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx
    sz Index ctx tp -> Index ctx tp
    forall (tp :: k). Index ctx tp -> Index ctx tp
    forall a. a -> a
    id)

    -- emptyEmbedding :: CtxEmbedding EmptyCtx EmptyCtx
    -- emptyEmbedding = identityEmbedding knownSize

    extendEmbeddingRightDiff :: forall ctx ctx' ctx''.
                                Diff ctx' ctx''
                                -> CtxEmbedding ctx ctx'
                                -> CtxEmbedding ctx ctx''
    extendEmbeddingRightDiff :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
    Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
    extendEmbeddingRightDiff Diff ctx' ctx''
    diff (CtxEmbedding Size ctx'
    sz' Assignment (Index ctx') ctx
    assgn) = Size ctx''
    -> Assignment (Index ctx'') ctx -> CtxEmbedding ctx ctx''
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
    CtxEmbedding (Size ctx' -> Diff ctx' ctx'' -> Size ctx''
    forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
    extSize Size ctx'
    sz' Diff ctx' ctx''
    diff) Assignment (Index ctx'') ctx
    updated
      where
        updated :: Assignment (Index ctx'') ctx
        updated :: Assignment (Index ctx'') ctx
    updated = (forall (x :: k). Index ctx' x -> Index ctx'' x)
    -> forall (x :: Ctx k).
       Assignment (Index ctx') x -> Assignment (Index ctx'') x
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
    FunctorFC t =>
    (forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
    forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x)
    -> forall (x :: Ctx k). Assignment f x -> Assignment g x
    fmapFC (Diff ctx' ctx'' -> Index ctx' x -> Index ctx'' x
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff ctx' ctx''
    diff) Assignment (Index ctx') ctx
    assgn

    extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
    extendEmbeddingRight :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
    CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
    extendEmbeddingRight = Diff ctx' (ctx' ::> tp)
    -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
    forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
    Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
    extendEmbeddingRightDiff Diff ctx' (ctx' ::> tp)
    forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
    knownDiff

    -- | Prove that the prefix of an appended context is embeddable in it
    appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
    appendEmbedding :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
    appendEmbedding Size ctx
    sz Size ctx'
    sz' = Size (ctx <+> ctx')
    -> Assignment (Index (ctx <+> ctx')) ctx
    -> CtxEmbedding ctx (ctx <+> ctx')
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
    CtxEmbedding (Size ctx -> Size ctx' -> Size (ctx <+> ctx')
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size ctx
    sz Size ctx'
    sz') (Size ctx
    -> (forall (tp :: k). Index ctx tp -> Index (ctx <+> ctx') tp)
    -> Assignment (Index (ctx <+> ctx')) ctx
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx
    sz (Diff ctx (ctx <+> ctx') -> Index ctx tp -> Index (ctx <+> ctx') tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff ctx (ctx <+> ctx')
    diff))
      where
      diff :: Diff ctx (ctx <+> ctx')
    diff = Size ctx' -> Diff ctx (ctx <+> ctx')
    forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff Size ctx'
    sz'

    -- | Prove that the suffix of an appended context is embeddable in it
    appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
    appendEmbeddingLeft :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
    appendEmbeddingLeft Size ctx
    sz Size ctx'
    sz' = Size (ctx <+> ctx')
    -> Assignment (Index (ctx <+> ctx')) ctx'
    -> CtxEmbedding ctx' (ctx <+> ctx')
    forall k (ctx :: Ctx k) (ctx' :: Ctx k).
    Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
    CtxEmbedding (Size ctx -> Size ctx' -> Size (ctx <+> ctx')
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size ctx
    sz Size ctx'
    sz') (Size ctx'
    -> (forall (tp :: k). Index ctx' tp -> Index (ctx <+> ctx') tp)
    -> Assignment (Index (ctx <+> ctx')) ctx'
    forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx'
    sz' (Size ctx -> Size ctx' -> Index ctx' tp -> Index (ctx <+> ctx') tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    extendIndexAppendLeft Size ctx
    sz Size ctx'
    sz'))

    extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
    extendEmbeddingBoth :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
    CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
    extendEmbeddingBoth CtxEmbedding ctx ctx'
    ctxe = CtxEmbedding ctx (ctx' ::> tp)
    updated CtxEmbedding ctx (ctx' ::> tp)
    -> (CtxEmbedding ctx (ctx' ::> tp)
        -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp))
    -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
    forall a b. a -> (a -> b) -> b
    & (Assignment (Index (ctx' ::> tp)) ctx
     -> Identity (Assignment (Index (ctx' ::> tp)) (ctx ::> tp)))
    -> CtxEmbedding ctx (ctx' ::> tp)
    -> Identity (CtxEmbedding (ctx ::> tp) (ctx' ::> tp))
    forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k)
           (f :: * -> *).
    Functor f =>
    (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2))
    -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')
    ctxeAssignment ((Assignment (Index (ctx' ::> tp)) ctx
      -> Identity (Assignment (Index (ctx' ::> tp)) (ctx ::> tp)))
     -> CtxEmbedding ctx (ctx' ::> tp)
     -> Identity (CtxEmbedding (ctx ::> tp) (ctx' ::> tp)))
    -> (Assignment (Index (ctx' ::> tp)) ctx
        -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp))
    -> CtxEmbedding ctx (ctx' ::> tp)
    -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
    %~ (Assignment (Index (ctx' ::> tp)) ctx
     -> Index (ctx' ::> tp) tp
     -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp))
    -> Index (ctx' ::> tp) tp
    -> Assignment (Index (ctx' ::> tp)) ctx
    -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Assignment (Index (ctx' ::> tp)) ctx
    -> Index (ctx' ::> tp) tp
    -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend (Size ctx' -> Index (ctx' ::> tp) tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex (CtxEmbedding ctx ctx'
    ctxe CtxEmbedding ctx ctx'
    -> Getting (Size ctx') (CtxEmbedding ctx ctx') (Size ctx')
    -> Size ctx'
    forall s a. s -> Getting a s a -> a
    ^. Getting (Size ctx') (CtxEmbedding ctx ctx') (Size ctx')
    forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (f :: * -> *).
    Functor f =>
    (Size ctx' -> f (Size ctx'))
    -> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
    ctxeSize))
      where
        updated :: CtxEmbedding ctx (ctx' ::> tp)
        updated :: CtxEmbedding ctx (ctx' ::> tp)
    updated = CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
    forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
    CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
    extendEmbeddingRight CtxEmbedding ctx ctx'
    ctxe

    --------------------------------------------------------------------------------
    -- Static indexing based on type-level naturals

    -- | 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 :: forall {k} (n :: Nat) (ctx :: Ctx k) (f :: k -> *) (r :: k).
    Idx n ctx r =>
    Lens' (Assignment f ctx) (f r)
    field = IndexF (Assignment f ctx) r
    -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) r)
    forall (x :: k).
    IndexF (Assignment f ctx) x
    -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
    forall k m (x :: k).
    IxedF' k m =>
    IndexF m x -> Lens' m (IxValueF m x)
    ixF' (forall (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx n ctx r =>
    Index ctx r
    forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx n ctx r =>
    Index ctx r
    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
    -- @ctx@ which has the type @r@.
    type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)

    -- | Compute an 'Index' value for a particular position in a 'Ctx'. The
    -- @TypeApplications@ extension will be needed to disambiguate the choice
    -- of the type @n@.
    natIndex :: forall n ctx r. Idx n ctx r => Index ctx r
    natIndex :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx n ctx r =>
    Index ctx r
    natIndex = forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx' n ctx r =>
    Index ctx r
    natIndex' @_ @(FromLeft ctx n)

    -- | This version of 'natIndex' is suitable for use without the @TypeApplications@
    -- extension.
    natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r
    natIndexProxy :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k) (proxy :: Nat -> *).
    Idx n ctx r =>
    proxy n -> Index ctx r
    natIndexProxy proxy n
    _ = forall (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx n ctx r =>
    Index ctx r
    forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx n ctx r =>
    Index ctx r
    natIndex @n

    ------------------------------------------------------------------------
    -- Implementation
    ------------------------------------------------------------------------

    -- | Class for computing 'Index' values for positions in a 'Ctx'.
    class KnownContext ctx => Idx' (n :: Nat) (ctx :: Ctx k) (r :: k) | n ctx -> r where
      natIndex' :: Index ctx r

    -- | Base-case
    instance KnownContext xs => Idx' 0 (xs '::> x) x where
      natIndex' :: Index (xs '::> x) x
    natIndex' = Size (xs '::> x) -> Index (xs '::> x) x
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size (ctx ::> tp) -> Index (ctx ::> tp) tp
    lastIndex Size (xs '::> x)
    forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
    knownSize

    -- | Inductive-step
    instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) =>
      Idx' n (xs '::> x) r where

      natIndex' :: Index (xs '::> x) r
    natIndex' = Index xs r -> Index (xs '::> x) r
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex (forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
    Idx' n ctx r =>
    Index ctx r
    natIndex' @_ @(n-1))

    --------------------------------------------------------------------------------
    -- * CurryAssignment

    -- | This type family is used to define currying\/uncurrying operations
    -- on assignments.  It is best understood by seeing its evaluation on
    -- several examples:
    --
    -- > CurryAssignment EmptyCtx f x = x
    -- > 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 -> Type) (x :: Type) :: Type where
       CurryAssignment EmptyCtx    f x = x
       CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x)

    -- | This class implements two methods that witness the isomorphism between
    --   curried and uncurried functions.
    class CurryAssignmentClass (ctx :: Ctx k) where

      -- | Transform a function that accepts an assignment into one with a separate
      --   variable for each element of the assignment.
      curryAssignment   :: (Assignment f ctx -> x) -> CurryAssignment ctx f x

      -- | Transform a curried function into one that accepts an assignment value.
      uncurryAssignment :: CurryAssignment ctx f x -> (Assignment f ctx -> x)

    instance CurryAssignmentClass EmptyCtx where
      curryAssignment :: forall (f :: k -> *) x.
    (Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x
    curryAssignment Assignment f EmptyCtx -> x
    k = Assignment f EmptyCtx -> x
    k Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty
      uncurryAssignment :: forall (f :: k -> *) x.
    CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x
    uncurryAssignment CurryAssignment EmptyCtx f x
    k Assignment f EmptyCtx
    _ = x
    CurryAssignment EmptyCtx f x
    k

    instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where
      curryAssignment :: forall (f :: k -> *) x.
    (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x
    curryAssignment Assignment f (ctx ::> a) -> x
    k = (Assignment f ctx -> f a -> x) -> CurryAssignment ctx f (f a -> x)
    forall k (ctx :: Ctx k) (f :: k -> *) x.
    CurryAssignmentClass ctx =>
    (Assignment f ctx -> x) -> CurryAssignment ctx f x
    forall (f :: k -> *) x.
    (Assignment f ctx -> x) -> CurryAssignment ctx f x
    curryAssignment (\Assignment f ctx
    asgn f a
    a -> Assignment f (ctx ::> a) -> x
    k (Assignment f ctx
    asgn Assignment f ctx -> f a -> Assignment f (ctx ::> a)
    forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> f a
    a))
      uncurryAssignment :: forall (f :: k -> *) x.
    CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x
    uncurryAssignment CurryAssignment (ctx ::> a) f x
    k Assignment f (ctx ::> a)
    asgn =
        case Assignment f (ctx ::> a) -> AssignView f (ctx ::> a)
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f (ctx ::> a)
    asgn of
          AssignExtend Assignment f ctx1
    asgn' f tp
    x -> CurryAssignment ctx1 f (f tp -> x)
    -> Assignment f ctx1 -> f tp -> x
    forall k (ctx :: Ctx k) (f :: k -> *) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: k -> *) x.
    CurryAssignment ctx1 f x -> Assignment f ctx1 -> x
    uncurryAssignment CurryAssignment ctx1 f (f tp -> x)
    CurryAssignment (ctx ::> a) f x
    k Assignment f ctx1
    asgn' f tp
    x

    -- | Create an assignment from a list of values.
    fromList :: [Some f] -> Some (Assignment f)
    fromList :: forall {k} (f :: k -> *). [Some f] -> Some (Assignment f)
    fromList = Assignment f EmptyCtx -> [Some f] -> Some (Assignment f)
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> [Some f] -> Some (Assignment f)
    go Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty
      where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
            go :: forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> [Some f] -> Some (Assignment f)
    go Assignment f ctx
    prev [] = Assignment f ctx -> Some (Assignment f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some Assignment f ctx
    prev
            go Assignment f ctx
    prev (Some f x
    g:[Some f]
    next) = (Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f)
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> [Some f] -> Some (Assignment f)
    go (Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f))
    -> Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f)
    forall a b. (a -> b) -> a -> b
    $! Assignment f ctx
    prev Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    `extend` f x
    g) [Some f]
    next

    newtype Collector m w a = Collector { forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    Collector m w a -> m w
    runCollector :: m w }
    instance Functor (Collector m w) where
      fmap :: forall a b. (a -> b) -> Collector m w a -> Collector m w b
    fmap a -> b
    _ (Collector m w
    x) = m w -> Collector m w b
    forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    m w -> Collector m w a
    Collector m w
    x
    instance (Applicative m, Monoid w) => Applicative (Collector m w) where
      pure :: forall a. a -> Collector m w a
    pure a
    _ = m w -> Collector m w a
    forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    m w -> Collector m w a
    Collector (w -> m w
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure w
    forall a. Monoid a => a
    mempty)
      Collector m w
    x <*> :: forall a b.
    Collector m w (a -> b) -> Collector m w a -> Collector m w b
    <*> Collector m w
    y = m w -> Collector m w b
    forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    m w -> Collector m w a
    Collector ((w -> w -> w) -> m w -> m w -> m w
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    App.liftA2 w -> w -> w
    forall a. Semigroup a => a -> a -> a
    (<>) m w
    x m w
    y)

    -- | Visit each of the elements in an @Assignment@ in order
    --   from left to right and collect the results using the provided @Monoid@.
    traverseAndCollect ::
      (Monoid w, Applicative m) =>
      (forall tp. Index ctx tp -> f tp -> m w) ->
      Assignment f ctx ->
      m w
    traverseAndCollect :: forall {k} w (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
    (Monoid w, Applicative m) =>
    (forall (tp :: k). Index ctx tp -> f tp -> m w)
    -> Assignment f ctx -> m w
    traverseAndCollect forall (tp :: k). Index ctx tp -> f tp -> m w
    f =
      Collector m w (Assignment (ZonkAny 0) ctx) -> m w
    forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    Collector m w a -> m w
    runCollector (Collector m w (Assignment (ZonkAny 0) ctx) -> m w)
    -> (Assignment f ctx -> Collector m w (Assignment (ZonkAny 0) ctx))
    -> Assignment f ctx
    -> m w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (tp :: k).
     Index ctx tp -> f tp -> Collector m w (ZonkAny 0 tp))
    -> Assignment f ctx -> Collector m w (Assignment (ZonkAny 0) ctx)
    forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *)
           (g :: k -> *).
    Applicative m =>
    (forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
    -> Assignment f ctx -> m (Assignment g ctx)
    traverseWithIndex (\Index ctx tp
    i f tp
    x -> m w -> Collector m w (ZonkAny 0 tp)
    forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
    m w -> Collector m w a
    Collector (Index ctx tp -> f tp -> m w
    forall (tp :: k). Index ctx tp -> f tp -> m w
    f Index ctx tp
    i f tp
    x))

    -- | Visit each of the elements in an @Assignment@ in order
    --   from left to right, executing an action with each.
    traverseWithIndex_ :: Applicative m
                       => (forall tp . Index ctx tp -> f tp -> m ())
                       -> Assignment f ctx
                       -> m ()
    traverseWithIndex_ :: forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
    Applicative m =>
    (forall (tp :: k). Index ctx tp -> f tp -> m ())
    -> Assignment f ctx -> m ()
    traverseWithIndex_ forall (tp :: k). Index ctx tp -> f tp -> m ()
    f = m () -> m ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (m () -> m ())
    -> (Assignment f ctx -> m ()) -> Assignment f ctx -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (tp :: k). Index ctx tp -> f tp -> m ())
    -> Assignment f ctx -> m ()
    forall {k} w (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
    (Monoid w, Applicative m) =>
    (forall (tp :: k). Index ctx tp -> f tp -> m w)
    -> Assignment f ctx -> m w
    traverseAndCollect Index ctx tp -> f tp -> m ()
    forall (tp :: k). Index ctx tp -> f tp -> m ()
    f

    --------------------------------------------------------------------------------
    -- Size and Index values

    size1 :: Size (EmptyCtx ::> a)
    size1 :: forall {k} (a :: k). Size (EmptyCtx ::> a)
    size1 = Size EmptyCtx -> Size (EmptyCtx '::> a)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size EmptyCtx
    forall {k}. Size 'EmptyCtx
    zeroSize

    size2 :: Size (EmptyCtx ::> a ::> b)
    size2 :: forall {k} (a :: k) (b :: k). Size ((EmptyCtx ::> a) ::> b)
    size2 = Size (EmptyCtx ::> a) -> Size ((EmptyCtx ::> a) '::> b)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size (EmptyCtx ::> a)
    forall {k} (a :: k). Size (EmptyCtx ::> a)
    size1

    size3 :: Size (EmptyCtx ::> a ::> b ::> c)
    size3 :: forall {k} (a :: k) (b :: k) (c :: k).
    Size (((EmptyCtx ::> a) ::> b) ::> c)
    size3 = Size ((EmptyCtx ::> a) ::> b)
    -> Size (((EmptyCtx ::> a) ::> b) '::> c)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size ((EmptyCtx ::> a) ::> b)
    forall {k} (a :: k) (b :: k). Size ((EmptyCtx ::> a) ::> b)
    size2

    size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)
    size4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    size4 = Size (((EmptyCtx ::> a) ::> b) ::> c)
    -> Size ((((EmptyCtx ::> a) ::> b) ::> c) '::> d)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size (((EmptyCtx ::> a) ::> b) ::> c)
    forall {k} (a :: k) (b :: k) (c :: k).
    Size (((EmptyCtx ::> a) ::> b) ::> c)
    size3

    size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
    size5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    size5 = Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    -> Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) '::> e)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    size4

    size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)
    size6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
    size6 = Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    -> Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    size5

    i1of2 :: Index (EmptyCtx ::> a ::> b) a
    i1of2 :: forall {k} (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) a
    i1of2 = Index (EmptyCtx ::> a) a -> Index ((EmptyCtx ::> a) '::> b) a
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (EmptyCtx ::> a) a
    forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
    baseIndex

    i2of2 :: Index (EmptyCtx ::> a ::> b) b
    i2of2 :: forall {k} (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) b
    i2of2 = Size (EmptyCtx ::> a) -> Index ((EmptyCtx ::> a) ::> b) b
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size (EmptyCtx ::> a)
    forall {k} (a :: k). Size (EmptyCtx ::> a)
    size1

    i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a
    i1of3 :: forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) a
    i1of3 = Index ((EmptyCtx ::> a) ::> b) a
    -> Index (((EmptyCtx ::> a) ::> b) '::> c) a
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((EmptyCtx ::> a) ::> b) a
    forall {k} (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) a
    i1of2

    i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b
    i2of3 :: forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) b
    i2of3 = Index ((EmptyCtx ::> a) ::> b) b
    -> Index (((EmptyCtx ::> a) ::> b) '::> c) b
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((EmptyCtx ::> a) ::> b) b
    forall {k} (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) b
    i2of2

    i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c
    i3of3 :: forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) c
    i3of3 = Size ((EmptyCtx ::> a) ::> b)
    -> Index (((EmptyCtx ::> a) ::> b) ::> c) c
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size ((EmptyCtx ::> a) ::> b)
    forall {k} (a :: k) (b :: k). Size ((EmptyCtx ::> a) ::> b)
    size2

    i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a
    i1of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
    i1of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) a
    -> Index ((((EmptyCtx ::> a) ::> b) ::> c) '::> d) a
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) a
    forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) a
    i1of3

    i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b
    i2of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
    i2of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) b
    -> Index ((((EmptyCtx ::> a) ::> b) ::> c) '::> d) b
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) b
    forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) b
    i2of3

    i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c
    i3of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
    i3of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) c
    -> Index ((((EmptyCtx ::> a) ::> b) ::> c) '::> d) c
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) c
    forall {k} (a :: k) (b :: k) (c :: k).
    Index (((EmptyCtx ::> a) ::> b) ::> c) c
    i3of3

    i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d
    i4of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
    i4of4 = Size (((EmptyCtx ::> a) ::> b) ::> c)
    -> Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size (((EmptyCtx ::> a) ::> b) ::> c)
    forall {k} (a :: k) (b :: k) (c :: k).
    Size (((EmptyCtx ::> a) ::> b) ::> c)
    size3

    i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
    i1of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
    i1of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
    -> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) '::> e) a
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
    i1of4

    i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b
    i2of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
    i2of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
    -> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) '::> e) b
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
    i2of4

    i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c
    i3of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
    i3of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
    -> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) '::> e) c
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
    i3of4

    i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d
    i4of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
    i4of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
    -> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) '::> e) d
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
    i4of4

    i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e
    i5of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
    i5of5 = Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    -> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
    Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
    size4

    i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a
    i1of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
    i1of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
    -> Index
         ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f) a
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
    i1of5

    i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b
    i2of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
    i2of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
    -> Index
         ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f) b
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
    i2of5

    i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c
    i3of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
    i3of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
    -> Index
         ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f) c
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
    i3of5

    i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d
    i4of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
    i4of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
    -> Index
         ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f) d
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
    i4of5

    i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e
    i5of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
    i5of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
    -> Index
         ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) '::> f) e
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
    i5of5

    i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f
    i6of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
    Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
    i6of6 = Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    -> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
    Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
    size5