    ------------------------------------------------------------------------
    -- |
    -- Module           : Data.Parameterized.Context.Safe
    -- Copyright        : (c) Galois, Inc 2014-2015
    -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
    --
    -- This module defines type contexts as a data-kind that consists of
    -- a list of types.  Indexes are defined with respect to these contexts.
    -- In addition, finite dependent products (Assignments) are defined over
    -- type contexts.  The elements of an assignment can be accessed using
    -- appropriately-typed indexes.
    --
    -- This module is intended to export exactly the same API as module
    -- "Data.Parameterized.Context.Unsafe", so that they can be used
    -- interchangeably.
    --
    -- This implementation is entirely typesafe, and provides a proof that
    -- the signature implemented by this module is consistent.  Contexts,
    -- indexes, and assignments are represented naively by linear sequences.
    --
    -- Compared to the implementation in "Data.Parameterized.Context.Unsafe",
    -- this one suffers from the fact that the operation of extending an
    -- the context of an index is /not/ a no-op. We therefore cannot use
    -- 'Data.Coerce.coerce' to understand indexes in a new context without
    -- actually breaking things.
    --------------------------------------------------------------------------
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE InstanceSigs #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE IncoherentInstances #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE StandaloneDeriving #-}
    #if __GLASGOW_HASKELL__ < 806
    {-# LANGUAGE TypeInType #-}
    #endif
    {-# OPTIONS_HADDOCK hide #-}
    module Data.Parameterized.Context.Safe
      ( module Data.Parameterized.Ctx
        -- * Size
      , Size
      , sizeInt
      , zeroSize
      , incSize
      , decSize
      , extSize
      , addSize
      , SizeView(..)
      , viewSize
      , sizeToNatRepr
      , KnownContext(..)
        -- * Diff
      , Diff
      , noDiff
      , addDiff
      , extendRight
      , appendDiff
      , DiffView(..)
      , viewDiff
      , KnownDiff(..)
      , IsAppend(..)
      , diffIsAppend
        -- * Indexing
      , Index
      , indexVal
      , baseIndex
      , skipIndex
      , lastIndex
      , nextIndex
      , leftIndex
      , rightIndex
      , extendIndex
      , extendIndex'
      , extendIndexAppendLeft
      , forIndex
      , forIndexRange
      , intIndex
      , IndexView(..)
      , viewIndex
        -- * Assignments
      , Assignment
      , size
      , Data.Parameterized.Context.Safe.replicate
      , generate
      , generateM
      , empty
      , extend
      , adjust
      , update
      , adjustM
      , AssignView(..)
      , viewAssign
      , (!)
      , (!^)
      , zipWith
      , zipWithM
      , (<++>)
      , traverseWithIndex
      ) where

    import qualified Control.Category as Cat
    import Control.DeepSeq
    import qualified Control.Lens as Lens
    import Control.Monad.Identity (Identity(..))
    import Data.Hashable
    import Data.List (intercalate)
    import Data.Maybe (listToMaybe)
    import Data.Type.Equality
    import Prelude hiding (init, map, null, replicate, succ, zipWith)
    import Data.Kind(Type)

    import Data.Parameterized.Classes
    import Data.Parameterized.Ctx
    import Data.Parameterized.NatRepr
    import Data.Parameterized.Some
    import Data.Parameterized.TraversableFC
    import Data.Parameterized.TraversableFC.WithIndex

    ------------------------------------------------------------------------
    -- Size

    -- | 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)

    -- | Renders as integer literal
    instance Show (Size ctx) where
      show :: Size ctx -> String
    show = Int -> String
    forall a. Show a => a -> String
    show (Int -> String) -> (Size ctx -> Int) -> Size ctx -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt

    instance ShowF Size

    -- | Convert a context size to an 'Int'.
    sizeInt :: Size ctx -> Int
    sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    SizeZero = Int
    0
    sizeInt (SizeSucc Size ctx
    sz) = (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (Int -> Int) -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $! Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    sz

    -- | The size of an empty context.
    zeroSize :: Size 'EmptyCtx
    zeroSize :: forall {k}. Size 'EmptyCtx
    zeroSize = Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    SizeZero

    -- | Increment the size to the next value.
    incSize :: Size ctx -> Size (ctx '::> tp)
    incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size ctx
    sz = Size ctx -> Size (ctx '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    SizeSucc Size ctx
    sz

    decSize :: Size (ctx '::> tp) -> Size ctx
    decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
    decSize (SizeSucc Size ctx
    sz) = Size ctx
    Size ctx
    sz

    -- | The total size of two concatenated contexts.
    addSize :: Size x -> Size y -> Size (x <+> y)
    addSize :: forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size x
    sx Size y
    SizeZero = Size x
    Size (x <+> y)
    sx
    addSize Size x
    sx (SizeSucc Size ctx
    sy) = Size (x <+> ctx) -> Size ((x <+> ctx) '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    SizeSucc (Size x -> Size ctx -> Size (x <+> ctx)
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size x
    sx Size ctx
    sy)

    -- | Allows interpreting a size.
    data SizeView (ctx :: Ctx k) where
      ZeroSize :: SizeView 'EmptyCtx
      IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)

    -- | View a size as either zero or a smaller size plus one.
    viewSize :: Size ctx -> SizeView ctx
    viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
    viewSize Size ctx
    SizeZero = SizeView ctx
    SizeView 'EmptyCtx
    forall {k}. SizeView 'EmptyCtx
    ZeroSize
    viewSize (SizeSucc Size ctx
    s) = Size ctx -> SizeView (ctx '::> tp)
    forall {k} (n :: Ctx k) (tp :: k). Size n -> SizeView (n '::> tp)
    IncSize Size ctx
    s

    -- | Convert a 'Size' into a 'NatRepr'.
    sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
    sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
    sizeToNatRepr Size items
    sz =
      case Size items -> SizeView items
    forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
    viewSize Size items
    sz of
        SizeView items
    ZeroSize -> NatRepr 0
    NatRepr (CtxSize items)
    forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IncSize Size ctx
    sz' ->
          let oldRep :: NatRepr (CtxSize ctx)
    oldRep = Size ctx -> NatRepr (CtxSize ctx)
    forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
    sizeToNatRepr Size ctx
    sz'
          in case NatRepr 1
    -> NatRepr (CtxSize ctx) -> (1 + CtxSize ctx) :~: (CtxSize ctx + 1)
    forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm (NatRepr 1
    forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: NatRepr 1) NatRepr (CtxSize ctx)
    oldRep of
               (1 + CtxSize ctx) :~: (CtxSize ctx + 1)
    Refl -> NatRepr (CtxSize ctx) -> NatRepr (CtxSize ctx + 1)
    forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
    incNat NatRepr (CtxSize ctx)
    oldRep

    ------------------------------------------------------------------------
    -- Size

    -- | A context that can be determined statically at compiler time.
    class KnownContext (ctx :: Ctx k) where
      knownSize :: Size ctx

    instance KnownContext 'EmptyCtx where
      knownSize :: Size 'EmptyCtx
    knownSize = Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    zeroSize

    instance KnownContext ctx => KnownContext (ctx '::> tp) where
      knownSize :: Size (ctx '::> tp)
    knownSize = Size ctx -> Size (ctx '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size ctx
    forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
    knownSize

    ------------------------------------------------------------------------
    -- Diff

    -- | Difference in number of elements between two contexts.
    -- The first context must be a sub-context of the other.
    data Diff (l :: Ctx k) (r :: Ctx k) where
      DiffHere :: Diff ctx ctx
      DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp)

    -- | The identity difference. Identity element of 'Category' instance.
    noDiff :: Diff l l
    noDiff :: forall {k} (l :: Ctx k). Diff l l
    noDiff = Diff l l
    forall {k} (l :: Ctx k). Diff l l
    DiffHere

    -- | The addition of differences. Flipped binary operation
    -- of 'Category' instance.
    addDiff :: Diff a b -> Diff b c -> Diff a c
    addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
    Diff a b -> Diff b c -> Diff a c
    addDiff Diff a b
    x Diff b c
    DiffHere = Diff a b
    Diff a c
    x
    addDiff Diff a b
    x (DiffThere Diff b ctx2
    y) = Diff a ctx2 -> Diff a (ctx2 '::> tp)
    forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff ctx1 n -> Diff ctx1 (n '::> tp)
    DiffThere (Diff a b -> Diff b ctx2 -> Diff a ctx2
    forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
    Diff a b -> Diff b c -> Diff a c
    addDiff Diff a b
    x Diff b ctx2
    y)

    -- | Extend the difference to a sub-context of the right side.
    extendRight :: Diff l r -> Diff l (r '::> tp)
    extendRight :: forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff ctx1 n -> Diff ctx1 (n '::> tp)
    extendRight Diff l r
    diff = Diff l r -> Diff l (r '::> tp)
    forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff ctx1 n -> Diff ctx1 (n '::> tp)
    DiffThere Diff l r
    diff

    appendDiff :: Size r -> Diff l (l <+> r)
    appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff Size r
    SizeZero = Diff l l
    Diff l (l <+> r)
    forall {k} (l :: Ctx k). Diff l l
    DiffHere
    appendDiff (SizeSucc Size ctx
    sz) = Diff l (l <+> ctx) -> Diff l ((l <+> ctx) '::> tp)
    forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff ctx1 n -> Diff ctx1 (n '::> tp)
    DiffThere (Size ctx -> Diff l (l <+> ctx)
    forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff Size ctx
    sz)

    -- | Implemented with 'noDiff' and 'addDiff'
    instance Cat.Category Diff where
      id :: forall (a :: Ctx k). Diff a a
    id = Diff a a
    forall {k} (l :: Ctx k). Diff l l
    DiffHere
      Diff b c
    d1 . :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k).
    Diff b c -> Diff a b -> Diff a c
    . Diff a b
    d2 = Diff a b -> Diff b c -> Diff a c
    forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
    Diff a b -> Diff b c -> Diff a c
    addDiff Diff a b
    d2 Diff b c
    d1

    -- | Extend the size by a given difference.
    extSize :: Size l -> Diff l r -> Size r
    extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
    extSize Size l
    sz Diff l r
    DiffHere = Size l
    Size r
    sz
    extSize Size l
    sz (DiffThere Diff l ctx2
    diff) = Size ctx2 -> Size (ctx2 '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize (Size l -> Diff l ctx2 -> Size ctx2
    forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
    extSize Size l
    sz Diff l ctx2
    diff)

    -- | Proof that @r = l <+> app@ for some @app@
    data IsAppend l r where
      IsAppend :: Size app -> IsAppend l (l <+> app)

    -- | If @l@ is a sub-context of @r@ then extract out their "contextual
    -- difference", i.e., the @app@ such that @r = l <+> app@
    diffIsAppend :: Diff l r -> IsAppend l r
    diffIsAppend :: forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
    diffIsAppend Diff l r
    DiffHere = Size 'EmptyCtx -> IsAppend l (l <+> 'EmptyCtx)
    forall {k} (n :: Ctx k) (l :: Ctx k).
    Size n -> IsAppend l (l <+> n)
    IsAppend Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    zeroSize
    diffIsAppend (DiffThere Diff l ctx2
    diff) =
      case Diff l ctx2 -> IsAppend l ctx2
    forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
    diffIsAppend Diff l ctx2
    diff of
        IsAppend Size app
    sz -> Size (app '::> tp) -> IsAppend l (l <+> (app '::> tp))
    forall {k} (n :: Ctx k) (l :: Ctx k).
    Size n -> IsAppend l (l <+> n)
    IsAppend (Size app -> Size (app '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize Size app
    sz)

    data DiffView a b where
      NoDiff :: DiffView a a
      ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)

    viewDiff :: Diff a b -> DiffView a b
    viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). Diff a b -> DiffView a b
    viewDiff Diff a b
    DiffHere = DiffView a a
    DiffView a b
    forall {k} (a :: Ctx k). DiffView a a
    NoDiff
    viewDiff (DiffThere Diff a ctx2
    diff) = Diff a ctx2 -> DiffView a (ctx2 '::> tp)
    forall {k} (a :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff a n -> DiffView a (n ::> tp)
    ExtendRightDiff Diff a ctx2
    diff

    ------------------------------------------------------------------------
    -- KnownDiff

    -- | A difference that can be automatically inferred at compile time.
    class KnownDiff (l :: Ctx k) (r :: Ctx k) where
      knownDiff :: Diff l r

    instance KnownDiff l l where
      knownDiff :: Diff l l
    knownDiff = Diff l l
    forall {k} (l :: Ctx k). Diff l l
    noDiff

    instance KnownDiff l r => KnownDiff l (r '::> tp) where
      knownDiff :: Diff l (r '::> tp)
    knownDiff = Diff l r -> Diff l (r '::> tp)
    forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
    Diff ctx1 n -> Diff ctx1 (n '::> tp)
    extendRight Diff l r
    forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
    knownDiff

    ------------------------------------------------------------------------
    -- Index

    -- | An index is a reference to a position with a particular type in a
    -- context.
    data Index (ctx :: Ctx k) (tp :: k) where
      IndexHere :: Size ctx -> 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
    indexVal :: forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal (IndexHere Size ctx
    sz) = Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    sz
    indexVal (IndexThere Index ctx tp
    idx) = Index ctx tp -> Int
    forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal Index ctx tp
    idx

    instance Eq (Index ctx tp) where
      Index ctx tp
    idx1 == :: Index ctx tp -> Index ctx tp -> Bool
    == Index ctx tp
    idx2 = Maybe (tp :~: tp) -> Bool
    forall a. Maybe a -> Bool
    isJust (Index ctx tp -> Index ctx tp -> Maybe (tp :~: tp)
    forall (a :: k) (b :: k).
    Index ctx a -> Index ctx b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Index ctx tp
    idx1 Index ctx tp
    idx2)

    instance EqF (Index ctx) where
      eqF :: forall (a :: k). Index ctx a -> Index ctx a -> Bool
    eqF Index ctx a
    idx1 Index ctx a
    idx2 = Maybe (a :~: a) -> Bool
    forall a. Maybe a -> Bool
    isJust (Index ctx a -> Index ctx a -> Maybe (a :~: a)
    forall (a :: k) (b :: k).
    Index ctx a -> Index ctx b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Index ctx a
    idx1 Index ctx a
    idx2)

    instance TestEquality (Index ctx) where
      testEquality :: forall (a :: k) (b :: k).
    Index ctx a -> Index ctx b -> Maybe (a :~: b)
    testEquality (IndexHere Size ctx
    _) (IndexHere Size ctx
    _) = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality (IndexHere Size ctx
    _) (IndexThere Index ctx b
    _) = Maybe (a :~: b)
    forall a. Maybe a
    Nothing
      testEquality (IndexThere Index ctx a
    _) (IndexHere Size ctx
    _) = Maybe (a :~: b)
    forall a. Maybe a
    Nothing
      testEquality (IndexThere Index ctx a
    idx1) (IndexThere Index ctx b
    idx2) =
         case Index ctx a -> Index ctx b -> Maybe (a :~: b)
    forall (a :: k) (b :: k).
    Index ctx a -> Index ctx b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Index ctx a
    idx1 Index ctx b
    Index ctx b
    idx2 of
             Just a :~: b
    Refl -> (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
             Maybe (a :~: b)
    Nothing -> Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance Ord (Index ctx tp) where
      compare :: Index ctx tp -> Index ctx tp -> Ordering
    compare Index ctx tp
    i Index ctx tp
    j = OrderingF tp tp -> Ordering
    forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
    toOrdering (Index ctx tp -> Index ctx tp -> OrderingF tp tp
    forall (x :: k) (y :: k).
    Index ctx x -> Index ctx y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF Index ctx tp
    i Index ctx tp
    j)

    instance OrdF (Index ctx) where
      compareF :: forall (x :: k) (y :: k).
    Index ctx x -> Index ctx y -> OrderingF x y
    compareF (IndexHere Size ctx
    _) (IndexHere Size ctx
    _) = OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
      compareF (IndexThere Index ctx x
    _) (IndexHere Size ctx
    _) = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
      compareF (IndexHere Size ctx
    _) (IndexThere Index ctx y
    _) = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
      compareF (IndexThere Index ctx x
    idx1) (IndexThere Index ctx y
    idx2) = Index ctx x
    -> Index ctx y -> ((x ~ y) => OrderingF x y) -> OrderingF x y
    forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
    OrdF f =>
    f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    lexCompareF Index ctx x
    idx1 Index ctx y
    Index ctx y
    idx2 (((x ~ y) => OrderingF x y) -> OrderingF x y)
    -> ((x ~ y) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $ OrderingF x x
    OrderingF x y
    (x ~ y) => OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF

    -- | Index for first element in context.
    baseIndex :: Index ('EmptyCtx '::> tp) tp
    baseIndex :: forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
    baseIndex = Size 'EmptyCtx -> Index ('EmptyCtx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    SizeZero

    -- | Increase context while staying at same index.
    skipIndex :: Index ctx x -> Index (ctx '::> y) x
    skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex Index ctx x
    idx = Index ctx x -> Index (ctx '::> y) x
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index ctx x
    idx

    -- | Return the index of an element one past the size.
    nextIndex :: Size ctx -> Index (ctx '::> tp) tp
    nextIndex :: forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    nextIndex Size ctx
    sz = Size ctx -> Index (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    sz

    -- | Return the last index of a element.
    lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
    lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
    Size (ctx ::> tp) -> Index (ctx ::> tp) tp
    lastIndex (SizeSucc Size ctx
    s) = Size ctx -> Index (ctx ::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    Size ctx
    s

    -- | Adapts an index in the left hand context of an append operation.
    leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp
    leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k).
    Size r -> Index l tp -> Index (l <+> r) tp
    leftIndex Size r
    sr Index l tp
    il = Diff l (l <+> r) -> Index l tp -> Index (l <+> r) tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' (Size r -> Diff l (l <+> r)
    forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff Size r
    sr) Index l tp
    il

    -- | Adapts an index in the right hand context of an append operation.
    rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    rightIndex Size l
    sl Size r
    sr Index r tp
    ir =
      case Size r -> Index r tp -> IndexView r tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index ctx tp -> IndexView ctx tp
    viewIndex Size r
    sr Index r tp
    ir of
        IndexViewInit Index ctx tp
    i -> Index (l <+> ctx) tp -> Index ((l <+> ctx) '::> u) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex (Size l -> Size ctx -> Index ctx tp -> Index (l <+> ctx) tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    rightIndex Size l
    sl (Size (ctx '::> u) -> Size ctx
    forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
    decSize Size r
    Size (ctx '::> u)
    sr) Index ctx tp
    i)
        IndexViewLast Size ctx
    s -> Size ((l <+> ctx) ::> tp) -> Index ((l <+> ctx) ::> tp) tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size (ctx ::> tp) -> Index (ctx ::> tp) tp
    lastIndex (Size (l <+> ctx) -> Size ((l <+> ctx) ::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    incSize (Size l -> Size ctx -> Size (l <+> ctx)
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size l
    sl Size ctx
    s))

    {-# INLINE extendIndex #-}
    extendIndex :: KnownDiff l r => Index l tp -> Index r tp
    extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    KnownDiff l r =>
    Index l tp -> Index r tp
    extendIndex = Diff l r -> Index l tp -> Index r tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff l r
    forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
    knownDiff

    {-# INLINE extendIndex' #-}
    -- | Compute an 'Index' into a context @r@ from an 'Index' into
    -- a sub-context @l@ of @r@.
    extendIndex' :: Diff l r -> Index l tp -> Index r tp
    extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff l r
    DiffHere Index l tp
    idx = Index l tp
    Index r tp
    idx
    extendIndex' (DiffThere Diff l ctx2
    diff) Index l tp
    idx = Index ctx2 tp -> Index (ctx2 '::> tp) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere (Diff l ctx2 -> Index l tp -> Index ctx2 tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Index l tp -> Index r tp
    extendIndex' Diff l ctx2
    diff Index l tp
    idx)

    {-# INLINE extendIndexAppendLeft #-}
    -- | Compute an 'Index' into an appended context from an 'Index' into
    -- its suffix.
    extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Size l -> Size r -> Index r tp -> Index (l <+> r) tp
    extendIndexAppendLeft Size l
    sz Size r
    sz' Index r tp
    idx = case Size r -> Index r tp -> IndexView r tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index ctx tp -> IndexView ctx tp
    viewIndex Size r
    sz' Index r tp
    idx of
      IndexViewLast Size ctx
    _ -> Size ((l <+> ctx) ::> tp) -> Index ((l <+> ctx) ::> tp) tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size (ctx ::> tp) -> Index (ctx ::> tp) tp
    lastIndex (Size l -> Size r -> Size (l <+> r)
    forall {k} (x :: Ctx k) (y :: Ctx k).
    Size x -> Size y -> Size (x <+> y)
    addSize Size l
    sz Size r
    sz')
      IndexViewInit Index ctx tp
    idx' -> Index (l <+> ctx) tp -> Index ((l <+> ctx) '::> u) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    skipIndex (Size l -> Size ctx -> Index ctx tp -> Index (l <+> 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 l
    sz (Size (ctx '::> u) -> Size ctx
    forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
    decSize Size r
    Size (ctx '::> u)
    sz') Index ctx tp
    idx')

    -- | Given a size @n@, a function @f@, and an initial value @v0@, the
    -- expression @forIndex n f v0@ calls @f@ on each index less than @n@
    -- starting from @0@ and @v0@, with the value @v@ obtained from the
    -- last call.
    forIndex :: forall ctx r
              . Size ctx
             -> (forall tp . r -> Index ctx tp -> r)
             -> r
             -> r
    forIndex :: forall {k} (ctx :: Ctx k) r.
    Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    forIndex Size ctx
    sz_top forall (tp :: k). r -> Index ctx tp -> r
    f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> r -> r
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> r -> r
    go Index ctx tp -> Index ctx tp
    forall (tp :: k). Index ctx tp -> Index ctx tp
    forall a. a -> a
    id Size ctx
    sz_top
     where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> r -> r
           go :: forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> r -> r
    go forall (tp :: k). Index ctx' tp -> Index ctx tp
    _ Size ctx'
    SizeZero = r -> r
    forall a. a -> a
    id
           go forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (SizeSucc Size ctx
    sz) = \r
    r -> (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> r -> r
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> r -> r
    go (\Index ctx tp
    i -> Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Index ctx tp -> Index (ctx '::> tp) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index ctx tp
    i)) Size ctx
    sz  (r -> r) -> r -> r
    forall a b. (a -> b) -> a -> b
    $ r -> Index ctx tp -> r
    forall (tp :: k). r -> Index ctx tp -> r
    f r
    r (Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Size ctx -> Index (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    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 :: forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
    Index a tp -> LDiff a b -> Index b tp
    ldiffIndex Index a tp
    i LDiff a b
    LDiffHere = Index a tp
    Index b tp
    i
    ldiffIndex Index a tp
    i (LDiffThere LDiff (a ::> x) b
    d) = Index (a ::> x) tp -> LDiff (a ::> x) b -> Index b tp
    forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
    Index a tp -> LDiff a b -> Index b tp
    ldiffIndex (Index a tp -> Index (a ::> x) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index a tp
    i) LDiff (a ::> x) b
    d

    forIndexLDiff :: Size a
                  -> LDiff a b
                  -> (forall tp . Index b tp -> r -> r)
                  -> r
                  -> r
    forIndexLDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Size a
    -> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
    forIndexLDiff Size a
    _ LDiff a b
    LDiffHere forall (tp :: k). Index b tp -> r -> r
    _ r
    r = r
    r
    forIndexLDiff Size a
    sz (LDiffThere LDiff (a ::> x) b
    d) forall (tp :: k). Index b tp -> r -> r
    f r
    r =
      Size (a ::> x)
    -> LDiff (a ::> x) b
    -> (forall (tp :: k). Index b tp -> r -> r)
    -> r
    -> r
    forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Size a
    -> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
    forIndexLDiff (Size a -> Size (a ::> x)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    SizeSucc Size a
    sz) LDiff (a ::> x) b
    d Index b tp -> r -> r
    forall (tp :: k). Index b tp -> r -> r
    f (Index b x -> r -> r
    forall (tp :: k). Index b tp -> r -> r
    f (Index (a ::> x) x -> LDiff (a ::> x) b -> Index b x
    forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
    Index a tp -> LDiff a b -> Index b tp
    ldiffIndex (Size a -> Index (a ::> x) x
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size a
    sz) LDiff (a ::> x) b
    d) r
    r)

    forIndexRangeImpl :: Int
                      -> Size a
                      -> LDiff a b
                      -> (forall tp . Index b tp -> r -> r)
                      -> r
                      -> r
    forIndexRangeImpl :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Int
    -> Size a
    -> LDiff a b
    -> (forall (tp :: k). Index b tp -> r -> r)
    -> r
    -> r
    forIndexRangeImpl Int
    0 Size a
    sz LDiff a b
    d forall (tp :: k). Index b tp -> r -> r
    f r
    r = Size a
    -> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
    forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Size a
    -> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
    forIndexLDiff Size a
    sz LDiff a b
    d Index b tp -> r -> r
    forall (tp :: k). Index b tp -> r -> r
    f r
    r
    forIndexRangeImpl Int
    _ Size a
    SizeZero LDiff a b
    _ forall (tp :: k). Index b tp -> r -> r
    _ r
    r = r
    r
    forIndexRangeImpl Int
    i (SizeSucc Size ctx
    sz) LDiff a b
    d forall (tp :: k). Index b tp -> r -> r
    f r
    r =
      Int
    -> Size ctx
    -> LDiff ctx b
    -> (forall (tp :: k). Index b tp -> r -> r)
    -> r
    -> r
    forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Int
    -> Size a
    -> LDiff a b
    -> (forall (tp :: k). Index b tp -> r -> r)
    -> r
    -> r
    forIndexRangeImpl (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Size ctx
    sz (LDiff (ctx '::> tp) b -> LDiff ctx b
    forall {k} (a :: Ctx k) (n :: k) (b :: Ctx k).
    LDiff (a ::> n) b -> LDiff a b
    LDiffThere LDiff a b
    LDiff (ctx '::> tp) b
    d) Index b tp -> r -> r
    forall (tp :: k). Index b tp -> r -> r
    f r
    r

    -- | Given an index @i@, size @n@, a function @f@, and a value @v@,
    -- the expression @forIndexRange i n f v@ is equivalent
    -- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
    -- otherwise.
    forIndexRange :: Int
                  -> Size ctx
                  -> (forall tp . Index ctx tp -> r -> r)
                  -> r
                  -> r
    forIndexRange :: forall {k} (ctx :: Ctx k) r.
    Int
    -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
    forIndexRange Int
    i Size ctx
    sz forall (tp :: k). Index ctx tp -> r -> r
    f r
    r = Int
    -> Size ctx
    -> LDiff ctx ctx
    -> (forall (tp :: k). Index ctx tp -> r -> r)
    -> r
    -> r
    forall {k} (a :: Ctx k) (b :: Ctx k) r.
    Int
    -> Size a
    -> LDiff a b
    -> (forall (tp :: k). Index b tp -> r -> r)
    -> r
    -> r
    forIndexRangeImpl Int
    i Size ctx
    sz LDiff ctx ctx
    forall {k} (a :: Ctx k). LDiff a a
    LDiffHere Index ctx tp -> r -> r
    forall (tp :: k). Index ctx tp -> r -> r
    f r
    r

    indexList :: forall ctx. Size ctx -> [Some (Index ctx)]
    indexList :: forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
    indexList Size ctx
    sz_top = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> [Some (Index ctx)] -> Size ctx -> [Some (Index ctx)]
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
    go Index ctx tp -> Index ctx tp
    forall (tp :: k). Index ctx tp -> Index ctx tp
    forall a. a -> a
    id [] Size ctx
    sz_top
     where go :: (forall tp. Index ctx' tp -> Index ctx tp)
              -> [Some (Index ctx)]
              -> Size ctx'
              -> [Some (Index ctx)]
           go :: forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
    go forall (tp :: k). Index ctx' tp -> Index ctx tp
    _ [Some (Index ctx)]
    ls Size ctx'
    SizeZero       = [Some (Index ctx)]
    ls
           go forall (tp :: k). Index ctx' tp -> Index ctx tp
    g [Some (Index ctx)]
    ls (SizeSucc Size ctx
    sz)  = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> [Some (Index ctx)] -> Size ctx -> [Some (Index ctx)]
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
    go (\Index ctx tp
    i -> Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Index ctx tp -> Index (ctx '::> tp) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index ctx tp
    i)) (Index ctx tp -> Some (Index ctx)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Size ctx -> Index (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    sz)) Some (Index ctx) -> [Some (Index ctx)] -> [Some (Index ctx)]
    forall a. a -> [a] -> [a]
    : [Some (Index ctx)]
    ls) Size ctx
    sz

    -- | Return index at given integer or nothing if integer is out of bounds.
    intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
    intIndex :: forall {k} (ctx :: Ctx k).
    Int -> Size ctx -> Maybe (Some (Index ctx))
    intIndex Int
    n Size ctx
    sz = [Some (Index ctx)] -> Maybe (Some (Index ctx))
    forall a. [a] -> Maybe a
    listToMaybe ([Some (Index ctx)] -> Maybe (Some (Index ctx)))
    -> [Some (Index ctx)] -> Maybe (Some (Index ctx))
    forall a b. (a -> b) -> a -> b
    $ Int -> [Some (Index ctx)] -> [Some (Index ctx)]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([Some (Index ctx)] -> [Some (Index ctx)])
    -> [Some (Index ctx)] -> [Some (Index ctx)]
    forall a b. (a -> b) -> a -> b
    $ Size ctx -> [Some (Index ctx)]
    forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
    indexList Size ctx
    sz

    -- | Renders as integer literal
    instance Show (Index ctx tp) where
       show :: Index ctx tp -> String
    show = Int -> String
    forall a. Show a => a -> String
    show (Int -> String) -> (Index ctx tp -> Int) -> Index ctx tp -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Index ctx tp -> Int
    forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal

    instance ShowF (Index ctx)

    -- | View of indexes as pointing to the last element in the
    -- index range or pointing to an earlier element in a smaller
    -- range.
    data IndexView ctx tp where
      IndexViewLast :: Size  ctx   -> IndexView (ctx '::> t) t
      IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t

    instance ShowF (IndexView ctx)
    deriving instance Show (IndexView ctx tp)

    -- | Project an index
    viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
    viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index ctx tp -> IndexView ctx tp
    viewIndex Size ctx
    _ (IndexHere Size ctx
    sz) = Size ctx -> IndexView (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (t :: k). Size n -> IndexView (n '::> t) t
    IndexViewLast Size ctx
    sz
    viewIndex Size ctx
    _ (IndexThere Index ctx tp
    i) = Index ctx tp -> IndexView (ctx '::> tp') tp
    forall {k} (n :: Ctx k) (t :: k) (tp :: k).
    Index n t -> IndexView (n '::> tp) t
    IndexViewInit Index ctx tp
    i
    -- NB: the unused size parameter is needed in the Unsafe module

    ------------------------------------------------------------------------
    -- Assignment

    -- | An assignment is a sequence that maps each index with type 'tp' to
    -- a value of type 'f tp'.
    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 -> Type) (ctx :: Ctx k) where
      AssignEmpty :: AssignView f EmptyCtx
      AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp)

    viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
    viewAssign :: forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f ctx
    AssignmentEmpty = AssignView f ctx
    AssignView f 'EmptyCtx
    forall {k} (f :: k -> *). AssignView f EmptyCtx
    AssignEmpty
    viewAssign (AssignmentExtend Assignment f ctx
    asgn f tp
    x) = Assignment f ctx -> f tp -> AssignView f (ctx '::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> AssignView f (n ::> tp)
    AssignExtend Assignment f ctx
    asgn f tp
    x

    instance NFData (Assignment f ctx) where
      rnf :: Assignment f ctx -> ()
    rnf Assignment f ctx
    AssignmentEmpty = ()
      rnf (AssignmentExtend Assignment f ctx
    asgn f tp
    x) = Assignment f ctx -> ()
    forall a. NFData a => a -> ()
    rnf Assignment f ctx
    asgn () -> () -> ()
    forall a b. a -> b -> b
    `seq` f tp
    x f tp -> () -> ()
    forall a b. a -> b -> b
    `seq` ()

    -- | Return number of elements in assignment.
    size :: Assignment f ctx -> Size ctx
    size :: forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f ctx
    AssignmentEmpty = Size ctx
    Size 'EmptyCtx
    forall {k}. Size 'EmptyCtx
    SizeZero
    size (AssignmentExtend Assignment f ctx
    asgn f tp
    _) = Size ctx -> Size (ctx '::> tp)
    forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
    SizeSucc (Assignment f ctx -> Size ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f ctx
    asgn)

    -- | Generate an assignment
    generate :: forall ctx f
              . Size ctx
             -> (forall tp . Index ctx tp -> f tp)
             -> Assignment f ctx
    generate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    generate Size ctx
    sz_top forall (tp :: k). Index ctx tp -> f tp
    f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> Assignment f ctx
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> Assignment f ctx'
    go Index ctx tp -> Index ctx tp
    forall (tp :: k). Index ctx tp -> Index ctx tp
    forall a. a -> a
    id Size ctx
    sz_top
     where go :: forall ctx'
               . (forall tp. Index ctx' tp -> Index ctx tp)
              -> Size ctx'
              -> Assignment f ctx'
           go :: forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> Assignment f ctx'
    go forall (tp :: k). Index ctx' tp -> Index ctx tp
    _ Size ctx'
    SizeZero = Assignment f ctx'
    Assignment f 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty
           go forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (SizeSucc Size ctx
    sz) =
                let ctx :: Assignment f ctx
    ctx = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> Assignment f ctx
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> Assignment f ctx'
    go (\Index ctx tp
    i -> Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Index ctx tp -> Index (ctx '::> tp) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index ctx tp
    i)) Size ctx
    sz
                    x :: f tp
    x = Index ctx tp -> f tp
    forall (tp :: k). Index ctx tp -> f tp
    f (Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Size ctx -> Index (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    sz))
                 in Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend Assignment f ctx
    ctx f tp
    x

    -- | Generate an assignment
    generateM :: forall ctx m f
               . Applicative m
              => Size ctx
              -> (forall tp . Index ctx tp -> m (f tp))
              -> m (Assignment f ctx)
    generateM :: forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
    Applicative m =>
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> m (f tp))
    -> m (Assignment f ctx)
    generateM Size ctx
    sz_top forall (tp :: k). Index ctx tp -> m (f tp)
    f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> m (Assignment f ctx)
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> m (Assignment f ctx')
    go Index ctx tp -> Index ctx tp
    forall (tp :: k). Index ctx tp -> Index ctx tp
    forall a. a -> a
    id Size ctx
    sz_top
     where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> m (Assignment f ctx')
           go :: forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> m (Assignment f ctx')
    go forall (tp :: k). Index ctx' tp -> Index ctx tp
    _ Size ctx'
    SizeZero = Assignment f ctx' -> m (Assignment f ctx')
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Assignment f ctx'
    Assignment f 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty
           go forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (SizeSucc Size ctx
    sz) =
                 Assignment f ctx -> f tp -> Assignment f ctx'
    Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend (Assignment f ctx -> f tp -> Assignment f ctx')
    -> m (Assignment f ctx) -> m (f tp -> Assignment f ctx')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((forall (tp :: k). Index ctx tp -> Index ctx tp)
    -> Size ctx -> m (Assignment f ctx)
    forall (ctx' :: Ctx k).
    (forall (tp :: k). Index ctx' tp -> Index ctx tp)
    -> Size ctx' -> m (Assignment f ctx')
    go (\Index ctx tp
    i -> Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Index ctx tp -> Index (ctx '::> tp) tp
    forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
    Index ctx x -> Index (ctx '::> y) x
    IndexThere Index ctx tp
    i)) Size ctx
    sz) m (f tp -> Assignment f ctx') -> m (f tp) -> m (Assignment f ctx')
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Index ctx tp -> m (f tp)
    forall (tp :: k). Index ctx tp -> m (f tp)
    f (Index ctx' tp -> Index ctx tp
    forall (tp :: k). Index ctx' tp -> Index ctx tp
    g (Size ctx -> Index (ctx '::> tp) tp
    forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
    IndexHere Size ctx
    sz))

    -- | @replicate n@ make a context with different copies of the same
    -- polymorphic value.
    replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx
    replicate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
    Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
    replicate Size ctx
    n forall (tp :: k). f tp
    c = 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
    n (\Index ctx tp
    _ -> f tp
    forall (tp :: k). f tp
    c)

    -- | Create empty indexed vector.
    empty :: Assignment f 'EmptyCtx
    empty :: forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty = Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty

    -- n.b. see 'singleton' in Data/Parameterized/Context.hs

    -- | Extend an indexed vector with a new entry.
    extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
    extend :: forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    extend Assignment f ctx
    asgn f tp
    e = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend Assignment f ctx
    asgn f tp
    e

    {-# 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (f tp -> f tp)
    -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
    adjust f tp -> f tp
    f Index ctx tp
    idx Assignment f ctx
    asgn = Identity (Assignment f ctx) -> Assignment f ctx
    forall a. Identity a -> a
    runIdentity ((f tp -> Identity (f tp))
    -> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx)
    forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Functor m =>
    (f tp -> m (f tp))
    -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    adjustM (f tp -> Identity (f tp)
    forall a. a -> Identity a
    Identity (f tp -> Identity (f tp))
    -> (f tp -> f tp) -> f tp -> Identity (f tp)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f tp -> f tp
    f) Index ctx tp
    idx Assignment f ctx
    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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
    update Index ctx tp
    i f tp
    v Assignment f ctx
    a = (f tp -> f tp)
    -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    (f tp -> f tp)
    -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
    adjust (\f tp
    _ -> f tp
    v) Index ctx tp
    i Assignment f ctx
    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 :: forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Functor m =>
    (f tp -> m (f tp))
    -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    adjustM f tp -> m (f tp)
    f = (forall (tp' :: k). f tp' -> f tp')
    -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    forall (g :: k -> *) (ctx' :: Ctx k).
    (forall (tp' :: k). g tp' -> f tp')
    -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
    go (\f tp'
    x -> f tp'
    x)
     where
      go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
      go :: forall (g :: k -> *) (ctx' :: Ctx k).
    (forall (tp' :: k). g tp' -> f tp')
    -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
    go forall (tp' :: k). g tp' -> f tp'
    g (IndexHere Size ctx
    _)     (AssignmentExtend Assignment g ctx
    asgn g tp
    x) = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend ((forall (tp' :: k). g tp' -> f tp')
    -> Assignment g ctx -> Assignment f ctx
    forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> Assignment f c -> Assignment g c
    map g tp -> f tp
    forall (tp' :: k). g tp' -> f tp'
    g Assignment g ctx
    asgn) (f tp -> Assignment f ctx') -> m (f tp) -> m (Assignment f ctx')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f tp -> m (f tp)
    f (g tp -> f tp
    forall (tp' :: k). g tp' -> f tp'
    g g tp
    g tp
    x)
      go forall (tp' :: k). g tp' -> f tp'
    g (IndexThere Index ctx tp
    idx)  (AssignmentExtend Assignment g ctx
    asgn g tp
    x) = (Assignment f ctx -> f tp -> Assignment f ctx')
    -> f tp -> Assignment f ctx -> Assignment f ctx'
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Assignment f ctx -> f tp -> Assignment f ctx'
    Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend (g tp -> f tp
    forall (tp' :: k). g tp' -> f tp'
    g g tp
    x)   (Assignment f ctx -> Assignment f ctx')
    -> m (Assignment f ctx) -> m (Assignment f ctx')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (tp' :: k). g tp' -> f tp')
    -> Index ctx tp -> Assignment g ctx -> m (Assignment f ctx)
    forall (g :: k -> *) (ctx' :: Ctx k).
    (forall (tp' :: k). g tp' -> f tp')
    -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
    go g tp' -> f tp'
    forall (tp' :: k). g tp' -> f tp'
    g Index ctx tp
    idx Assignment g ctx
    Assignment g ctx
    asgn

    type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx
    type instance IxValueF (Assignment (f :: k -> Type) ctx) = f

    instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
      ixF :: Index ctx x -> Lens.Traversal' (Assignment f ctx) (f x)
      ixF :: forall (x :: k). Index ctx x -> Traversal' (Assignment f ctx) (f x)
    ixF Index ctx x
    idx f x -> f (f x)
    f = (f x -> f (f x))
    -> Index ctx x -> Assignment f ctx -> f (Assignment f ctx)
    forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Functor m =>
    (f tp -> m (f tp))
    -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    adjustM f x -> f (f x)
    f Index ctx x
    idx

    instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
      ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
      ixF' :: forall (x :: k). Index ctx x -> Lens' (Assignment f ctx) (f x)
    ixF' Index ctx x
    idx f x -> f (f x)
    f = (f x -> f (f x))
    -> Index ctx x -> Assignment f ctx -> f (Assignment f ctx)
    forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Functor m =>
    (f tp -> m (f tp))
    -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    adjustM f x -> f (f x)
    f Index ctx x
    idx

    idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp
    idxlookup :: forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
    (forall (tp :: k). a tp -> b tp)
    -> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
    idxlookup forall (tp :: k). a tp -> b tp
    f (AssignmentExtend Assignment a ctx
    _   a tp
    x) (IndexHere Size ctx
    _) = a tp -> b tp
    forall (tp :: k). a tp -> b tp
    f a tp
    a tp
    x
    idxlookup forall (tp :: k). a tp -> b tp
    f (AssignmentExtend Assignment a ctx
    ctx a tp
    _) (IndexThere Index ctx tp
    idx) = (forall (tp :: k). a tp -> b tp)
    -> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
    forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
    (forall (tp :: k). a tp -> b tp)
    -> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
    idxlookup a tp -> b tp
    forall (tp :: k). a tp -> b tp
    f Assignment a ctx
    ctx Index ctx tp
    Index ctx tp
    idx
    idxlookup forall (tp :: k). a tp -> b tp
    _ Assignment a ctx
    AssignmentEmpty Index ctx tp
    idx = case Index ctx tp
    idx of {}

    -- | Return value of assignment.
    (!) :: Assignment f ctx -> Index ctx tp -> f tp
    ! :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    (!) Assignment f ctx
    asgn Index ctx tp
    idx = (forall (tp :: k). f tp -> f tp)
    -> Assignment f ctx -> forall (tp :: k). Index ctx tp -> f tp
    forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
    (forall (tp :: k). a tp -> b tp)
    -> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
    idxlookup f tp -> f tp
    forall (tp :: k). f tp -> f tp
    forall a. a -> a
    id Assignment f ctx
    asgn Index ctx tp
    idx

    -- | Return value of assignment, where the index is into an
    --   initial sequence of the assignment.
    (!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
    Assignment f r
    a !^ :: forall {k} (l :: Ctx k) (r :: Ctx k) (f :: k -> *) (tp :: k).
    KnownDiff l r =>
    Assignment f r -> Index l tp -> f tp
    !^ Index l tp
    i = Assignment f r
    a Assignment f r -> Index r tp -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index l tp -> Index r tp
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    KnownDiff l r =>
    Index l tp -> Index r tp
    extendIndex Index l tp
    i

    instance TestEquality f => Eq (Assignment f ctx) where
      Assignment f ctx
    x == :: Assignment f ctx -> Assignment f ctx -> Bool
    == Assignment f ctx
    y = Maybe (ctx :~: ctx) -> Bool
    forall a. Maybe a -> Bool
    isJust (Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
    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 ctx
    x Assignment f ctx
    y)

    instance EqF f => EqF (Assignment f) where
      eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool
    eqF Assignment f a
    AssignmentEmpty Assignment f a
    AssignmentEmpty = Bool
    True
      eqF (AssignmentExtend Assignment f ctx
    ctx1 f tp
    x1) (AssignmentExtend Assignment f ctx
    ctx2 f tp
    x2) =
        Assignment f ctx -> Assignment f ctx -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool
    eqF Assignment f ctx
    ctx1 Assignment f ctx
    Assignment f ctx
    ctx2 Bool -> Bool -> Bool
    && f tp -> f tp -> Bool
    forall (a :: k). f a -> f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF f tp
    x1 f tp
    f tp
    x2

    testEq :: (forall x y. f x -> f y -> Maybe (x :~: y))
           -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
    testEq :: forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
    testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    _ Assignment f cxt1
    AssignmentEmpty Assignment f cxt2
    AssignmentEmpty = (cxt1 :~: cxt2) -> Maybe (cxt1 :~: cxt2)
    forall a. a -> Maybe a
    Just cxt1 :~: cxt1
    cxt1 :~: cxt2
    forall {k} (a :: k). a :~: a
    Refl
    testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test (AssignmentExtend Assignment f ctx
    ctx1 f tp
    x1) (AssignmentExtend Assignment f ctx
    ctx2 f tp
    x2) =
         case (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
    forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
    testEq f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test Assignment f ctx
    ctx1 Assignment f ctx
    ctx2 of
           Maybe (ctx :~: ctx)
    Nothing -> Maybe (cxt1 :~: cxt2)
    forall a. Maybe a
    Nothing
           Just ctx :~: ctx
    Refl ->
              case f tp -> f tp -> Maybe (tp :~: tp)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test f tp
    x1 f tp
    x2 of
                 Maybe (tp :~: tp)
    Nothing -> Maybe (cxt1 :~: cxt2)
    forall a. Maybe a
    Nothing
                 Just tp :~: tp
    Refl -> (cxt1 :~: cxt2) -> Maybe (cxt1 :~: cxt2)
    forall a. a -> Maybe a
    Just cxt1 :~: cxt1
    cxt1 :~: cxt2
    forall {k} (a :: k). a :~: a
    Refl
    testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    _ Assignment f cxt1
    AssignmentEmpty AssignmentExtend{} = Maybe (cxt1 :~: cxt2)
    forall a. Maybe a
    Nothing
    testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    _ AssignmentExtend{} Assignment f cxt2
    AssignmentEmpty = Maybe (cxt1 :~: cxt2)
    forall a. Maybe a
    Nothing

    instance TestEqualityFC Assignment where
       testEqualityFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       Assignment f x -> Assignment f y -> Maybe (x :~: y)
    testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    f = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f x -> Assignment f y -> Maybe (x :~: y)
    forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
    testEq f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    f
    instance TestEquality f => TestEquality (Assignment f) where
       testEquality :: forall (a :: Ctx k) (b :: Ctx k).
    Assignment f a -> Assignment f b -> Maybe (a :~: b)
    testEquality Assignment f a
    x Assignment f b
    y = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f a -> Assignment f b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
    testEq f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Assignment f a
    x Assignment f b
    y
    instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where
      polyEqF :: Assignment f x
    -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y)
    polyEqF Assignment f x
    x Assignment f y
    y = ((x :~: y) -> Assignment f x :~: Assignment f y)
    -> Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\x :~: y
    Refl -> Assignment f x :~: Assignment f x
    Assignment f x :~: Assignment f y
    forall {k} (a :: k). a :~: a
    Refl) (Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y))
    -> Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y)
    forall a b. (a -> b) -> a -> b
    $ Assignment f x -> Assignment f y -> Maybe (x :~: y)
    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 x
    x Assignment f y
    y

    compareAsgn :: (forall x y. f x -> f y -> OrderingF x y)
                -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
    compareAsgn :: forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
    compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ Assignment f ctx1
    AssignmentEmpty Assignment f ctx2
    AssignmentEmpty = OrderingF ctx1 ctx1
    OrderingF ctx1 ctx2
    forall {k} (x :: k). OrderingF x x
    EQF
    compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ Assignment f ctx1
    AssignmentEmpty Assignment f ctx2
    _ = OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
    compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ Assignment f ctx1
    _ Assignment f ctx2
    AssignmentEmpty = OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
    compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test (AssignmentExtend Assignment f ctx
    ctx1 f tp
    x) (AssignmentExtend Assignment f ctx
    ctx2 f tp
    y) =
      case (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f ctx -> Assignment f ctx -> OrderingF ctx ctx
    forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
    compareAsgn f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test Assignment f ctx
    ctx1 Assignment f ctx
    ctx2 of
        OrderingF ctx ctx
    LTF -> OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
        OrderingF ctx ctx
    GTF -> OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
        OrderingF ctx ctx
    EQF -> case f tp -> f tp -> OrderingF tp tp
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test f tp
    x f tp
    y of
                  OrderingF tp tp
    LTF -> OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
                  OrderingF tp tp
    GTF -> OrderingF ctx1 ctx2
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
                  OrderingF tp tp
    EQF -> OrderingF ctx1 ctx1
    OrderingF ctx1 ctx2
    forall {k} (x :: k). OrderingF x x
    EQF

    instance OrdFC Assignment where
      compareFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       Assignment f x -> Assignment f y -> OrderingF x y
    compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    f = (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f x -> Assignment f y -> OrderingF x y
    forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
    compareAsgn f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    f

    instance OrdF f => OrdF (Assignment f) where
      compareF :: forall (x :: Ctx k) (y :: Ctx k).
    Assignment f x -> Assignment f y -> OrderingF x y
    compareF = (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f x -> Assignment f y -> OrderingF x y
    forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
    compareAsgn f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF

    instance OrdF f => Ord (Assignment f ctx) where
      compare :: Assignment f ctx -> Assignment f ctx -> Ordering
    compare Assignment f ctx
    x Assignment f ctx
    y = OrderingF ctx ctx -> Ordering
    forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
    toOrdering (Assignment f ctx -> Assignment f ctx -> OrderingF ctx ctx
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    forall (x :: Ctx k) (y :: Ctx k).
    Assignment f x -> Assignment f y -> OrderingF x y
    compareF Assignment f ctx
    x Assignment f ctx
    y)

    instance Hashable (Index ctx tp) where
      hashWithSalt :: Int -> Index ctx tp -> Int
    hashWithSalt = Int -> Index ctx tp -> Int
    forall (tp :: k). Int -> Index ctx tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    hashWithSaltF
    instance HashableF (Index ctx) where
      hashWithSaltF :: forall (tp :: k). Int -> Index ctx tp -> Int
    hashWithSaltF Int
    s Index ctx tp
    i = Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s (Index ctx tp -> Int
    forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal Index ctx tp
    i)

    instance (HashableF f, TestEquality f) => HashableF (Assignment f) where
      hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int
    hashWithSaltF = Int -> Assignment f tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt

    instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where
      hashWithSalt :: Int -> Assignment f ctx -> Int
    hashWithSalt Int
    s Assignment f ctx
    AssignmentEmpty = Int
    s
      hashWithSalt Int
    s (AssignmentExtend Assignment f ctx
    asgn f tp
    x) = (Int
    s Int -> Assignment f ctx -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` Assignment f ctx
    asgn) Int -> f tp -> Int
    forall (tp :: k). Int -> f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    `hashWithSaltF` f tp
    x

    instance ShowF f => Show (Assignment f ctx) where
      show :: Assignment f ctx -> String
    show Assignment f ctx
    a = String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((forall (tp :: k). f tp -> String) -> Assignment f ctx -> [String]
    forall {k} (f :: k -> *) a (c :: Ctx k).
    (forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
    toList f tp -> String
    forall (tp :: k). f tp -> String
    forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
    showF Assignment f ctx
    a) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"

    instance ShowF f => ShowF (Assignment f)

    instance FunctorFC Assignment where
      fmapFC :: forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x)
    -> forall (x :: Ctx k). Assignment f x -> Assignment g x
    fmapFC = (forall (x :: k). f x -> g x) -> Assignment f x -> Assignment g x
    (forall (x :: k). f x -> g x)
    -> forall (x :: Ctx k). Assignment f x -> Assignment g x
    forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
           (g :: k -> *).
    TraversableFC 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
    fmapFCDefault

    instance FoldableFC Assignment where
      foldMapFC :: forall (f :: k -> *) m.
    Monoid m =>
    (forall (x :: k). f x -> m)
    -> forall (x :: Ctx k). Assignment f x -> m
    foldMapFC = (forall (x :: k). f x -> m) -> Assignment f x -> m
    (forall (x :: k). f x -> m)
    -> forall (x :: Ctx k). Assignment f x -> m
    forall {k} {l} (t :: (k -> *) -> l -> *) m (f :: k -> *).
    (TraversableFC t, Monoid m) =>
    (forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
    foldMapFCDefault

    instance TraversableFC Assignment where
      traverseFC :: forall (f :: k -> *) (g :: k -> *) (m :: * -> *).
    Applicative m =>
    (forall (x :: k). f x -> m (g x))
    -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x)
    traverseFC forall (x :: k). f x -> m (g x)
    f = (forall (x :: k). f x -> m (g x))
    -> Assignment f x -> m (Assignment g x)
    forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> Assignment f c -> m (Assignment g c)
    traverseF f tp -> m (g tp)
    forall (x :: k). f x -> m (g x)
    f

    instance FunctorFCWithIndex Assignment where
      imapFC :: forall (f :: k -> *) (g :: k -> *) (z :: Ctx k).
    (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x)
    -> Assignment f z -> Assignment g z
    imapFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x)
    -> Assignment f z -> Assignment g z
    forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
           (g :: k -> *) (z :: l).
    TraversableFCWithIndex t =>
    (forall (x :: k). IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
    imapFCDefault

    instance FoldableFCWithIndex Assignment where
      ifoldMapFC :: forall (f :: k -> *) m (z :: Ctx k).
    Monoid m =>
    (forall (x :: k). IndexF (Assignment f z) x -> f x -> m)
    -> Assignment f z -> m
    ifoldMapFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> m)
    -> Assignment f z -> m
    forall {k} {l} (t :: (k -> *) -> l -> *) m (z :: l) (f :: k -> *).
    (TraversableFCWithIndex t, Monoid m) =>
    (forall (x :: k). IndexF (t f z) x -> f x -> m) -> t f z -> m
    ifoldMapFCDefault

    instance TraversableFCWithIndex Assignment where
      itraverseFC :: forall (m :: * -> *) (z :: Ctx k) (f :: k -> *) (g :: k -> *).
    Applicative m =>
    (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x))
    -> Assignment f z -> m (Assignment g z)
    itraverseFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x))
    -> Assignment f z -> m (Assignment g z)
    (forall (tp :: k). Index z tp -> f tp -> m (g tp))
    -> Assignment f z -> m (Assignment g z)
    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

    -- | Map assignment
    map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
    map :: forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> Assignment f c -> Assignment g c
    map forall (tp :: k). f tp -> g tp
    f = (forall (tp :: k). f tp -> g tp)
    -> forall (x :: Ctx k). Assignment f x -> Assignment g 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 f x -> g x
    forall (tp :: k). f tp -> g tp
    f

    traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
               . Applicative m
              => (forall tp . f tp -> m (g tp))
              -> Assignment f c
              -> m (Assignment g c)
    traverseF :: forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> Assignment f c -> m (Assignment g c)
    traverseF forall (tp :: k). f tp -> m (g tp)
    _ Assignment f c
    AssignmentEmpty = Assignment g c -> m (Assignment g c)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Assignment g c
    Assignment g 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty
    traverseF forall (tp :: k). f tp -> m (g tp)
    f (AssignmentExtend Assignment f ctx
    asgn f tp
    x) = (Assignment g ctx -> g tp -> Assignment g c)
    -> m (Assignment g ctx -> g tp -> Assignment g c)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Assignment g ctx -> g tp -> Assignment g c
    Assignment g ctx -> g tp -> Assignment g (ctx '::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend m (Assignment g ctx -> g tp -> Assignment g c)
    -> m (Assignment g ctx) -> m (g tp -> Assignment g c)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (forall (tp :: k). f tp -> m (g tp))
    -> Assignment f ctx -> m (Assignment g ctx)
    forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> Assignment f c -> m (Assignment g c)
    traverseF f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f Assignment f ctx
    asgn m (g tp -> Assignment g c) -> m (g tp) -> m (Assignment g c)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f f tp
    x

    -- | Convert assignment to list.
    toList :: (forall tp . f tp -> a)
           -> Assignment f c
           -> [a]
    toList :: forall {k} (f :: k -> *) a (c :: Ctx k).
    (forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
    toList forall (tp :: k). f tp -> a
    f = (forall (tp :: k). f tp -> a)
    -> forall (x :: Ctx k). Assignment f x -> [a]
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: k -> *) a.
    (forall (x :: k). f x -> a)
    -> forall (x :: Ctx k). Assignment f x -> [a]
    toListFC f x -> a
    forall (tp :: k). f tp -> a
    f

    zipWithM :: Applicative m
             => (forall tp . f tp -> g tp -> m (h tp))
             -> Assignment f c
             -> Assignment g c
             -> m (Assignment h c)
    zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> g tp -> m (h tp))
    -> Assignment f c -> Assignment g c -> m (Assignment h c)
    zipWithM forall (tp :: k). f tp -> g tp -> m (h tp)
    f Assignment f c
    x Assignment g c
    y = Assignment f c -> Assignment g c -> m (Assignment h c)
    go Assignment f c
    x Assignment g c
    y
     where go :: Assignment f c -> Assignment g c -> m (Assignment h c)
    go Assignment f c
    AssignmentEmpty Assignment g c
    AssignmentEmpty = Assignment h 'EmptyCtx -> m (Assignment h 'EmptyCtx)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Assignment h 'EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty
           go (AssignmentExtend Assignment f ctx
    asgn1 f tp
    x1) (AssignmentExtend Assignment g ctx
    asgn2 g tp
    x2) =
                 Assignment h ctx -> h tp -> Assignment h (ctx '::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend (Assignment h ctx -> h tp -> Assignment h (ctx '::> tp))
    -> m (Assignment h ctx) -> m (h tp -> Assignment h (ctx '::> tp))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((forall (tp :: k). f tp -> g tp -> m (h tp))
    -> Assignment f ctx -> Assignment g ctx -> m (Assignment h ctx)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> g tp -> m (h tp))
    -> Assignment f c -> Assignment g c -> m (Assignment h c)
    zipWithM f tp -> g tp -> m (h tp)
    forall (tp :: k). f tp -> g tp -> m (h tp)
    f Assignment f ctx
    asgn1 Assignment g ctx
    Assignment g ctx
    asgn2) m (h tp -> Assignment h (ctx '::> tp))
    -> m (h tp) -> m (Assignment h (ctx '::> tp))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (f tp -> g tp -> m (h tp)
    forall (tp :: k). f tp -> g tp -> m (h tp)
    f f tp
    x1 g tp
    g tp
    x2)

    zipWith :: (forall x . f x -> g x -> h x)
            -> Assignment f a
            -> Assignment g a
            -> Assignment h a
    zipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (a :: Ctx k).
    (forall (x :: k). f x -> g x -> h x)
    -> Assignment f a -> Assignment g a -> Assignment h a
    zipWith forall (x :: k). f x -> g x -> h x
    f = \Assignment f a
    x Assignment g a
    y -> Identity (Assignment h a) -> Assignment h a
    forall a. Identity a -> a
    runIdentity (Identity (Assignment h a) -> Assignment h a)
    -> Identity (Assignment h a) -> Assignment h a
    forall a b. (a -> b) -> a -> b
    $ (forall (tp :: k). f tp -> g tp -> Identity (h tp))
    -> Assignment f a -> Assignment g a -> Identity (Assignment h a)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> g tp -> m (h tp))
    -> Assignment f c -> Assignment g c -> m (Assignment h c)
    zipWithM (\f tp
    u g tp
    v -> h tp -> Identity (h tp)
    forall a. a -> Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (f tp -> g tp -> h tp
    forall (x :: k). f x -> g x -> h x
    f f tp
    u g tp
    v)) Assignment f a
    x Assignment g a
    y
    {-# INLINE zipWith #-}

    -- | This is a specialization of 'itraverseFC'.
    traverseWithIndex :: Applicative m
                      => (forall tp . Index ctx tp -> f tp -> m (g tp))
                      -> Assignment f ctx
                      -> m (Assignment g ctx)
    traverseWithIndex :: 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 forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
    f Assignment f ctx
    a = Size ctx
    -> (forall (tp :: k). Index ctx tp -> m (g tp))
    -> m (Assignment g ctx)
    forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
    Applicative m =>
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> m (f tp))
    -> m (Assignment f ctx)
    generateM (Assignment f ctx -> Size ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f ctx
    a) ((forall (tp :: k). Index ctx tp -> m (g tp))
     -> m (Assignment g ctx))
    -> (forall (tp :: k). Index ctx tp -> m (g tp))
    -> m (Assignment g ctx)
    forall a b. (a -> b) -> a -> b
    $ \Index ctx tp
    i -> Index ctx tp -> f tp -> m (g tp)
    forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
    f Index ctx tp
    i (Assignment f ctx
    a Assignment f ctx -> Index ctx tp -> f tp
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index ctx tp
    i)

    (<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
    Assignment f x
    x <++> :: forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    Assignment f x -> Assignment f y -> Assignment f (x <+> y)
    <++> Assignment f y
    AssignmentEmpty = Assignment f x
    Assignment f (x <+> y)
    x
    Assignment f x
    x <++> AssignmentExtend Assignment f ctx
    y f tp
    t = Assignment f (x <+> ctx)
    -> f tp -> Assignment f ((x <+> ctx) ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend (Assignment f x
    x Assignment f x -> Assignment f ctx -> Assignment f (x <+> ctx)
    forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    Assignment f x -> Assignment f y -> Assignment f (x <+> y)
    <++> Assignment f ctx
    y) f tp
    t

    ------------------------------------------------------------------------
    -- KnownRepr instances

    instance (KnownRepr (Assignment f) ctx, KnownRepr f bt)
          => KnownRepr (Assignment f) (ctx ::> bt) where
      knownRepr :: Assignment f (ctx ::> bt)
    knownRepr = Assignment f ctx
    forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr Assignment f ctx -> f bt -> Assignment f (ctx ::> bt)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    `extend` f bt
    forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    instance KnownRepr (Assignment f) EmptyCtx where
      knownRepr :: Assignment f EmptyCtx
    knownRepr = Assignment f EmptyCtx
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty

    --------------------------------------------------------------------------------------
    -- lookups and update for lenses

    data MyNat where
      MyZ :: MyNat
      MyS :: MyNat -> MyNat

    type MyZ = 'MyZ
    type MyS = 'MyS

    data MyNatRepr :: MyNat -> Type where
      MyZR :: MyNatRepr MyZ
      MySR :: MyNatRepr n -> MyNatRepr (MyS n)

    type family StrongCtxUpdate (n::MyNat) (ctx::Ctx k) (z::k) :: Ctx k where
      StrongCtxUpdate n       EmptyCtx     z = EmptyCtx
      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 -> Type) :: Type where
      MyNatLookup n       EmptyCtx  f = ()
      MyNatLookup MyZ     (ctx::>x) f = f x
      MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f

    mynat_lookup :: MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr n
    _   Assignment f ctx
    AssignmentEmpty = ()
    mynat_lookup MyNatRepr n
    MyZR     (AssignmentExtend Assignment f ctx
    _    f tp
    x) = f tp
    MyNatLookup n ctx f
    x
    mynat_lookup (MySR MyNatRepr n
    n) (AssignmentExtend Assignment f ctx
    asgn f tp
    _) = MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr n
    n Assignment f ctx
    asgn

    strong_ctx_update :: MyNatRepr n -> Assignment f ctx -> f tp -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr n
    _        Assignment f ctx
    AssignmentEmpty           f tp
    _ = Assignment f 'EmptyCtx
    Assignment f (StrongCtxUpdate n ctx tp)
    forall {k} (f :: k -> *). Assignment f EmptyCtx
    AssignmentEmpty
    strong_ctx_update MyNatRepr n
    MyZR     (AssignmentExtend Assignment f ctx
    asgn f tp
    _) f tp
    z = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend Assignment f ctx
    asgn f tp
    z
    strong_ctx_update (MySR MyNatRepr n
    n) (AssignmentExtend Assignment f ctx
    asgn f tp
    x) f tp
    z = Assignment f (StrongCtxUpdate n ctx tp)
    -> f tp -> Assignment f (StrongCtxUpdate n ctx tp ::> tp)
    forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
    Assignment f n -> f tp -> Assignment f (n ::> tp)
    AssignmentExtend (MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr n
    n Assignment f ctx
    asgn f tp
    z) f tp
    x

    ------------------------------------------------------------------------
    -- 1 field lens combinators

    type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1)

    instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where

      _1 :: Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
    _1 = (Assignment1 f t -> f t)
    -> (Assignment1 f t -> f u -> Assignment1 f u)
    -> Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment1 f t -> MyNatLookup 'MyZ ('EmptyCtx '::> t) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment1 f t
    -> f u
    -> Assignment f (StrongCtxUpdate 'MyZ ('EmptyCtx '::> t) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 2 field lens combinators

    type Assignment2 f x1 x2
       = Assignment f ('EmptyCtx '::> x1 '::> x2)

    instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where
      _1 :: Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
    _1 = (Assignment2 f t x2 -> f t)
    -> (Assignment2 f t x2 -> f u -> Assignment2 f u x2)
    -> Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment2 f t x2
    -> MyNatLookup (MyS 'MyZ) (('EmptyCtx '::> t) '::> x2) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment2 f t x2
    -> f u
    -> Assignment
         f (StrongCtxUpdate (MyS 'MyZ) (('EmptyCtx '::> t) '::> x2) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where
      _2 :: Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
    _2 = (Assignment2 f x1 t -> f t)
    -> (Assignment2 f x1 t -> f u -> Assignment2 f x1 u)
    -> Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment2 f x1 t
    -> MyNatLookup 'MyZ (('EmptyCtx '::> x1) '::> t) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment2 f x1 t
    -> f u
    -> Assignment
         f (StrongCtxUpdate 'MyZ (('EmptyCtx '::> x1) '::> t) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 3 field lens combinators

    type Assignment3 f x1 x2 x3
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3)

    instance Lens.Field1 (Assignment3 f t x2 x3)
                         (Assignment3 f u x2 x3)
                         (f t)
                         (f u) where
      _1 :: Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
    _1 = (Assignment3 f t x2 x3 -> f t)
    -> (Assignment3 f t x2 x3 -> f u -> Assignment3 f u x2 x3)
    -> Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment3 f t x2 x3
    -> MyNatLookup
         (MyS (MyS 'MyZ)) ((('EmptyCtx '::> t) '::> x2) '::> x3) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment3 f t x2 x3
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ)) ((('EmptyCtx '::> t) '::> x2) '::> x3) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment3 f x1 t x3)
                         (Assignment3 f x1 u x3)
                         (f t)
                         (f u) where
      _2 :: Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
    _2 = (Assignment3 f x1 t x3 -> f t)
    -> (Assignment3 f x1 t x3 -> f u -> Assignment3 f x1 u x3)
    -> Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment3 f x1 t x3
    -> MyNatLookup (MyS 'MyZ) ((('EmptyCtx '::> x1) '::> t) '::> x3) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment3 f x1 t x3
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ) ((('EmptyCtx '::> x1) '::> t) '::> x3) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment3 f x1 x2 t)
                         (Assignment3 f x1 x2 u)
                         (f t)
                         (f u) where
      _3 :: Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
    _3 = (Assignment3 f x1 x2 t -> f t)
    -> (Assignment3 f x1 x2 t -> f u -> Assignment3 f x1 x2 u)
    -> Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment3 f x1 x2 t
    -> MyNatLookup 'MyZ ((('EmptyCtx '::> x1) '::> x2) '::> t) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment3 f x1 x2 t
    -> f u
    -> Assignment
         f (StrongCtxUpdate 'MyZ ((('EmptyCtx '::> x1) '::> x2) '::> t) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 4 field lens combinators

    type Assignment4 f x1 x2 x3 x4
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4)

    instance Lens.Field1 (Assignment4 f t x2 x3 x4)
                         (Assignment4 f u x2 x3 x4)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
    _1 = (Assignment4 f t x2 x3 x4 -> f t)
    -> (Assignment4 f t x2 x3 x4 -> f u -> Assignment4 f u x2 x3 x4)
    -> Lens
         (Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment4 f t x2 x3 x4
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         (((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment4 f t x2 x3 x4
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            (((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment4 f x1 t x3 x4)
                         (Assignment4 f x1 u x3 x4)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
    _2 = (Assignment4 f x1 t x3 x4 -> f t)
    -> (Assignment4 f x1 t x3 x4 -> f u -> Assignment4 f x1 u x3 x4)
    -> Lens
         (Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment4 f x1 t x3 x4
    -> MyNatLookup
         (MyS (MyS 'MyZ)) (((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment4 f x1 t x3 x4
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            (((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment4 f x1 x2 t x4)
                         (Assignment4 f x1 x2 u x4)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
    _3 = (Assignment4 f x1 x2 t x4 -> f t)
    -> (Assignment4 f x1 x2 t x4 -> f u -> Assignment4 f x1 x2 u x4)
    -> Lens
         (Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment4 f x1 x2 t x4
    -> MyNatLookup
         (MyS 'MyZ) (((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment4 f x1 x2 t x4
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ) (((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment4 f x1 x2 x3 t)
                         (Assignment4 f x1 x2 x3 u)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
    _4 = (Assignment4 f x1 x2 x3 t -> f t)
    -> (Assignment4 f x1 x2 x3 t -> f u -> Assignment4 f x1 x2 x3 u)
    -> Lens
         (Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment4 f x1 x2 x3 t
    -> MyNatLookup
         'MyZ (((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment4 f x1 x2 x3 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ (((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 5 field lens combinators

    type Assignment5 f x1 x2 x3 x4 x5
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5)

    instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5)
                         (Assignment5 f u x2 x3 x4 x5)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment5 f t x2 x3 x4 x5)
      (Assignment5 f u x2 x3 x4 x5)
      (f t)
      (f u)
    _1 = (Assignment5 f t x2 x3 x4 x5 -> f t)
    -> (Assignment5 f t x2 x3 x4 x5
        -> f u -> Assignment5 f u x2 x3 x4 x5)
    -> Lens
         (Assignment5 f t x2 x3 x4 x5)
         (Assignment5 f u x2 x3 x4 x5)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment5 f t x2 x3 x4 x5
    -> MyNatLookup
         (MyS (MyS (MyS (MyS 'MyZ))))
         ((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment5 f t x2 x3 x4 x5
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS 'MyZ))))
            ((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5)
                         (Assignment5 f x1 u x3 x4 x5)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment5 f x1 t x3 x4 x5)
      (Assignment5 f x1 u x3 x4 x5)
      (f t)
      (f u)
    _2 = (Assignment5 f x1 t x3 x4 x5 -> f t)
    -> (Assignment5 f x1 t x3 x4 x5
        -> f u -> Assignment5 f x1 u x3 x4 x5)
    -> Lens
         (Assignment5 f x1 t x3 x4 x5)
         (Assignment5 f x1 u x3 x4 x5)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment5 f x1 t x3 x4 x5
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         ((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment5 f x1 t x3 x4 x5
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            ((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5)
                         (Assignment5 f x1 x2 u x4 x5)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment5 f x1 x2 t x4 x5)
      (Assignment5 f x1 x2 u x4 x5)
      (f t)
      (f u)
    _3 = (Assignment5 f x1 x2 t x4 x5 -> f t)
    -> (Assignment5 f x1 x2 t x4 x5
        -> f u -> Assignment5 f x1 x2 u x4 x5)
    -> Lens
         (Assignment5 f x1 x2 t x4 x5)
         (Assignment5 f x1 x2 u x4 x5)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment5 f x1 x2 t x4 x5
    -> MyNatLookup
         (MyS (MyS 'MyZ))
         ((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment5 f x1 x2 t x4 x5
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            ((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5)
                         (Assignment5 f x1 x2 x3 u x5)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment5 f x1 x2 x3 t x5)
      (Assignment5 f x1 x2 x3 u x5)
      (f t)
      (f u)
    _4 = (Assignment5 f x1 x2 x3 t x5 -> f t)
    -> (Assignment5 f x1 x2 x3 t x5
        -> f u -> Assignment5 f x1 x2 x3 u x5)
    -> Lens
         (Assignment5 f x1 x2 x3 t x5)
         (Assignment5 f x1 x2 x3 u x5)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment5 f x1 x2 x3 t x5
    -> MyNatLookup
         (MyS 'MyZ)
         ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment5 f x1 x2 x3 t x5
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ)
            ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t)
                         (Assignment5 f x1 x2 x3 x4 u)
                         (f t)
                         (f u) where
      _5 :: Lens
      (Assignment5 f x1 x2 x3 x4 t)
      (Assignment5 f x1 x2 x3 x4 u)
      (f t)
      (f u)
    _5 = (Assignment5 f x1 x2 x3 x4 t -> f t)
    -> (Assignment5 f x1 x2 x3 x4 t
        -> f u -> Assignment5 f x1 x2 x3 x4 u)
    -> Lens
         (Assignment5 f x1 x2 x3 x4 t)
         (Assignment5 f x1 x2 x3 x4 u)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment5 f x1 x2 x3 x4 t
    -> MyNatLookup
         'MyZ ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t) f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment5 f x1 x2 x3 x4 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t) u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 6 field lens combinators

    type Assignment6 f x1 x2 x3 x4 x5 x6
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6)

    instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6)
                         (Assignment6 f u x2 x3 x4 x5 x6)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment6 f t x2 x3 x4 x5 x6)
      (Assignment6 f u x2 x3 x4 x5 x6)
      (f t)
      (f u)
    _1 = (Assignment6 f t x2 x3 x4 x5 x6 -> f t)
    -> (Assignment6 f t x2 x3 x4 x5 x6
        -> f u -> Assignment6 f u x2 x3 x4 x5 x6)
    -> Lens
         (Assignment6 f t x2 x3 x4 x5 x6)
         (Assignment6 f u x2 x3 x4 x5 x6)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment6 f t x2 x3 x4 x5 x6
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
         (((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
          '::> x6)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment6 f t x2 x3 x4 x5 x6
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
            (((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> x6)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6)
                         (Assignment6 f x1 u x3 x4 x5 x6)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment6 f x1 t x3 x4 x5 x6)
      (Assignment6 f x1 u x3 x4 x5 x6)
      (f t)
      (f u)
    _2 = (Assignment6 f x1 t x3 x4 x5 x6 -> f t)
    -> (Assignment6 f x1 t x3 x4 x5 x6
        -> f u -> Assignment6 f x1 u x3 x4 x5 x6)
    -> Lens
         (Assignment6 f x1 t x3 x4 x5 x6)
         (Assignment6 f x1 u x3 x4 x5 x6)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment6 f x1 t x3 x4 x5 x6
    -> MyNatLookup
         (MyS (MyS (MyS (MyS 'MyZ))))
         (((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
          '::> x6)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment6 f x1 t x3 x4 x5 x6
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS 'MyZ))))
            (((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
             '::> x6)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6)
                         (Assignment6 f x1 x2 u x4 x5 x6)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment6 f x1 x2 t x4 x5 x6)
      (Assignment6 f x1 x2 u x4 x5 x6)
      (f t)
      (f u)
    _3 = (Assignment6 f x1 x2 t x4 x5 x6 -> f t)
    -> (Assignment6 f x1 x2 t x4 x5 x6
        -> f u -> Assignment6 f x1 x2 u x4 x5 x6)
    -> Lens
         (Assignment6 f x1 x2 t x4 x5 x6)
         (Assignment6 f x1 x2 u x4 x5 x6)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment6 f x1 x2 t x4 x5 x6
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         (((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
          '::> x6)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment6 f x1 x2 t x4 x5 x6
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            (((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
             '::> x6)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6)
                         (Assignment6 f x1 x2 x3 u x5 x6)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment6 f x1 x2 x3 t x5 x6)
      (Assignment6 f x1 x2 x3 u x5 x6)
      (f t)
      (f u)
    _4 = (Assignment6 f x1 x2 x3 t x5 x6 -> f t)
    -> (Assignment6 f x1 x2 x3 t x5 x6
        -> f u -> Assignment6 f x1 x2 x3 u x5 x6)
    -> Lens
         (Assignment6 f x1 x2 x3 t x5 x6)
         (Assignment6 f x1 x2 x3 u x5 x6)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment6 f x1 x2 x3 t x5 x6
    -> MyNatLookup
         (MyS (MyS 'MyZ))
         (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
          '::> x6)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment6 f x1 x2 x3 t x5 x6
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
             '::> x6)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6)
                         (Assignment6 f x1 x2 x3 x4 u x6)
                         (f t)
                         (f u) where
      _5 :: Lens
      (Assignment6 f x1 x2 x3 x4 t x6)
      (Assignment6 f x1 x2 x3 x4 u x6)
      (f t)
      (f u)
    _5 = (Assignment6 f x1 x2 x3 x4 t x6 -> f t)
    -> (Assignment6 f x1 x2 x3 x4 t x6
        -> f u -> Assignment6 f x1 x2 x3 x4 u x6)
    -> Lens
         (Assignment6 f x1 x2 x3 x4 t x6)
         (Assignment6 f x1 x2 x3 x4 u x6)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment6 f x1 x2 x3 x4 t x6
    -> MyNatLookup
         (MyS 'MyZ)
         (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
          '::> x6)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment6 f x1 x2 x3 x4 t x6
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ)
            (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
             '::> x6)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t)
                         (Assignment6 f x1 x2 x3 x4 x5 u)
                         (f t)
                         (f u) where
      _6 :: Lens
      (Assignment6 f x1 x2 x3 x4 x5 t)
      (Assignment6 f x1 x2 x3 x4 x5 u)
      (f t)
      (f u)
    _6 = (Assignment6 f x1 x2 x3 x4 x5 t -> f t)
    -> (Assignment6 f x1 x2 x3 x4 x5 t
        -> f u -> Assignment6 f x1 x2 x3 x4 x5 u)
    -> Lens
         (Assignment6 f x1 x2 x3 x4 x5 t)
         (Assignment6 f x1 x2 x3 x4 x5 u)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment6 f x1 x2 x3 x4 x5 t
    -> MyNatLookup
         'MyZ
         (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
          '::> t)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment6 f x1 x2 x3 x4 x5 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ
            (((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> t)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 7 field lens combinators

    type Assignment7 f x1 x2 x3 x4 x5 x6 x7
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7)

    instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7)
                         (Assignment7 f u x2 x3 x4 x5 x6 x7)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment7 f t x2 x3 x4 x5 x6 x7)
      (Assignment7 f u x2 x3 x4 x5 x6 x7)
      (f t)
      (f u)
    _1 = (Assignment7 f t x2 x3 x4 x5 x6 x7 -> f t)
    -> (Assignment7 f t x2 x3 x4 x5 x6 x7
        -> f u -> Assignment7 f u x2 x3 x4 x5 x6 x7)
    -> Lens
         (Assignment7 f t x2 x3 x4 x5 x6 x7)
         (Assignment7 f u x2 x3 x4 x5 x6 x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment7 f t x2 x3 x4 x5 x6 x7
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
         ((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
           '::> x6)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment7 f t x2 x3 x4 x5 x6 x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
            ((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
              '::> x6)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7)
                         (Assignment7 f x1 u x3 x4 x5 x6 x7)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment7 f x1 t x3 x4 x5 x6 x7)
      (Assignment7 f x1 u x3 x4 x5 x6 x7)
      (f t)
      (f u)
    _2 = (Assignment7 f x1 t x3 x4 x5 x6 x7 -> f t)
    -> (Assignment7 f x1 t x3 x4 x5 x6 x7
        -> f u -> Assignment7 f x1 u x3 x4 x5 x6 x7)
    -> Lens
         (Assignment7 f x1 t x3 x4 x5 x6 x7)
         (Assignment7 f x1 u x3 x4 x5 x6 x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment7 f x1 t x3 x4 x5 x6 x7
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
         ((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
           '::> x6)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment7 f x1 t x3 x4 x5 x6 x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
            ((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
              '::> x6)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7)
                         (Assignment7 f x1 x2 u x4 x5 x6 x7)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment7 f x1 x2 t x4 x5 x6 x7)
      (Assignment7 f x1 x2 u x4 x5 x6 x7)
      (f t)
      (f u)
    _3 = (Assignment7 f x1 x2 t x4 x5 x6 x7 -> f t)
    -> (Assignment7 f x1 x2 t x4 x5 x6 x7
        -> f u -> Assignment7 f x1 x2 u x4 x5 x6 x7)
    -> Lens
         (Assignment7 f x1 x2 t x4 x5 x6 x7)
         (Assignment7 f x1 x2 u x4 x5 x6 x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment7 f x1 x2 t x4 x5 x6 x7
    -> MyNatLookup
         (MyS (MyS (MyS (MyS 'MyZ))))
         ((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
           '::> x6)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment7 f x1 x2 t x4 x5 x6 x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS 'MyZ))))
            ((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
              '::> x6)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7)
                         (Assignment7 f x1 x2 x3 u x5 x6 x7)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment7 f x1 x2 x3 t x5 x6 x7)
      (Assignment7 f x1 x2 x3 u x5 x6 x7)
      (f t)
      (f u)
    _4 = (Assignment7 f x1 x2 x3 t x5 x6 x7 -> f t)
    -> (Assignment7 f x1 x2 x3 t x5 x6 x7
        -> f u -> Assignment7 f x1 x2 x3 u x5 x6 x7)
    -> Lens
         (Assignment7 f x1 x2 x3 t x5 x6 x7)
         (Assignment7 f x1 x2 x3 u x5 x6 x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment7 f x1 x2 x3 t x5 x6 x7
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
           '::> x6)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment7 f x1 x2 x3 t x5 x6 x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
              '::> x6)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7)
                         (Assignment7 f x1 x2 x3 x4 u x6 x7)
                         (f t)
                         (f u) where
      _5 :: Lens
      (Assignment7 f x1 x2 x3 x4 t x6 x7)
      (Assignment7 f x1 x2 x3 x4 u x6 x7)
      (f t)
      (f u)
    _5 = (Assignment7 f x1 x2 x3 x4 t x6 x7 -> f t)
    -> (Assignment7 f x1 x2 x3 x4 t x6 x7
        -> f u -> Assignment7 f x1 x2 x3 x4 u x6 x7)
    -> Lens
         (Assignment7 f x1 x2 x3 x4 t x6 x7)
         (Assignment7 f x1 x2 x3 x4 u x6 x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment7 f x1 x2 x3 x4 t x6 x7
    -> MyNatLookup
         (MyS (MyS 'MyZ))
         ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
           '::> x6)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment7 f x1 x2 x3 x4 t x6 x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
              '::> x6)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7)
                         (Assignment7 f x1 x2 x3 x4 x5 u x7)
                         (f t)
                         (f u) where
      _6 :: Lens
      (Assignment7 f x1 x2 x3 x4 x5 t x7)
      (Assignment7 f x1 x2 x3 x4 x5 u x7)
      (f t)
      (f u)
    _6 = (Assignment7 f x1 x2 x3 x4 x5 t x7 -> f t)
    -> (Assignment7 f x1 x2 x3 x4 x5 t x7
        -> f u -> Assignment7 f x1 x2 x3 x4 x5 u x7)
    -> Lens
         (Assignment7 f x1 x2 x3 x4 x5 t x7)
         (Assignment7 f x1 x2 x3 x4 x5 u x7)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment7 f x1 x2 x3 x4 x5 t x7
    -> MyNatLookup
         (MyS 'MyZ)
         ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
           '::> t)
          '::> x7)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment7 f x1 x2 x3 x4 x5 t x7
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ)
            ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
              '::> t)
             '::> x7)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t)
                         (Assignment7 f x1 x2 x3 x4 x5 x6 u)
                         (f t)
                         (f u) where
      _7 :: Lens
      (Assignment7 f x1 x2 x3 x4 x5 x6 t)
      (Assignment7 f x1 x2 x3 x4 x5 x6 u)
      (f t)
      (f u)
    _7 = (Assignment7 f x1 x2 x3 x4 x5 x6 t -> f t)
    -> (Assignment7 f x1 x2 x3 x4 x5 x6 t
        -> f u -> Assignment7 f x1 x2 x3 x4 x5 x6 u)
    -> Lens
         (Assignment7 f x1 x2 x3 x4 x5 x6 t)
         (Assignment7 f x1 x2 x3 x4 x5 x6 u)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment7 f x1 x2 x3 x4 x5 x6 t
    -> MyNatLookup
         'MyZ
         ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
           '::> x6)
          '::> t)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment7 f x1 x2 x3 x4 x5 x6 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ
            ((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
              '::> x6)
             '::> t)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 8 field lens combinators

    type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8)

    instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
                         (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
      (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
      (f t)
      (f u)
    _1 = (Assignment8 f t x2 x3 x4 x5 x6 x7 x8 -> f t)
    -> (Assignment8 f t x2 x3 x4 x5 x6 x7 x8
        -> f u -> Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
    -> Lens
         (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
         (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> Assignment8 f t x2 x3 x4 x5 x6 x7 x8
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
         (((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
            '::> x6)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> Assignment8 f t x2 x3 x4 x5 x6 x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
            (((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
               '::> x6)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
                         (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
      (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
      (f t)
      (f u)
    _2 = (Assignment8 f x1 t x3 x4 x5 x6 x7 x8 -> f t)
    -> (Assignment8 f x1 t x3 x4 x5 x6 x7 x8
        -> f u -> Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
    -> Lens
         (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
         (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment8 f x1 t x3 x4 x5 x6 x7 x8
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
         (((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
            '::> x6)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment8 f x1 t x3 x4 x5 x6 x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
            (((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
               '::> x6)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
                         (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
      (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
      (f t)
      (f u)
    _3 = (Assignment8 f x1 x2 t x4 x5 x6 x7 x8 -> f t)
    -> (Assignment8 f x1 x2 t x4 x5 x6 x7 x8
        -> f u -> Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
    -> Lens
         (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
         (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment8 f x1 x2 t x4 x5 x6 x7 x8
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
         (((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
            '::> x6)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment8 f x1 x2 t x4 x5 x6 x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
            (((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
               '::> x6)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
                         (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
      (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
      (f t)
      (f u)
    _4 = (Assignment8 f x1 x2 x3 t x5 x6 x7 x8 -> f t)
    -> (Assignment8 f x1 x2 x3 t x5 x6 x7 x8
        -> f u -> Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
    -> Lens
         (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
         (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment8 f x1 x2 x3 t x5 x6 x7 x8
    -> MyNatLookup
         (MyS (MyS (MyS (MyS 'MyZ))))
         (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
            '::> x6)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment8 f x1 x2 x3 t x5 x6 x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS 'MyZ))))
            (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
               '::> x6)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
                         (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
                         (f t)
                         (f u) where
      _5 :: Lens
      (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
      (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
      (f t)
      (f u)
    _5 = (Assignment8 f x1 x2 x3 x4 t x6 x7 x8 -> f t)
    -> (Assignment8 f x1 x2 x3 x4 t x6 x7 x8
        -> f u -> Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
    -> Lens
         (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
         (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment8 f x1 x2 x3 x4 t x6 x7 x8
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
            '::> x6)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment8 f x1 x2 x3 x4 t x6 x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
               '::> x6)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
                         (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
                         (f t)
                         (f u) where
      _6 :: Lens
      (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
      (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
      (f t)
      (f u)
    _6 = (Assignment8 f x1 x2 x3 x4 x5 t x7 x8 -> f t)
    -> (Assignment8 f x1 x2 x3 x4 x5 t x7 x8
        -> f u -> Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
    -> Lens
         (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
         (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment8 f x1 x2 x3 x4 x5 t x7 x8
    -> MyNatLookup
         (MyS (MyS 'MyZ))
         (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
            '::> t)
           '::> x7)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment8 f x1 x2 x3 x4 x5 t x7 x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
               '::> t)
              '::> x7)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
                         (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
                         (f t)
                         (f u) where
      _7 :: Lens
      (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
      (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
      (f t)
      (f u)
    _7 = (Assignment8 f x1 x2 x3 x4 x5 x6 t x8 -> f t)
    -> (Assignment8 f x1 x2 x3 x4 x5 x6 t x8
        -> f u -> Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
    -> Lens
         (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
         (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment8 f x1 x2 x3 x4 x5 x6 t x8
    -> MyNatLookup
         (MyS 'MyZ)
         (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
            '::> x6)
           '::> t)
          '::> x8)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment8 f x1 x2 x3 x4 x5 x6 t x8
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ)
            (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
               '::> x6)
              '::> t)
             '::> x8)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
                         (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
                         (f t)
                         (f u) where
      _8 :: Lens
      (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
      (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
      (f t)
      (f u)
    _8 = (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t -> f t)
    -> (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
        -> f u -> Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
    -> Lens
         (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
         (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
    -> MyNatLookup
         'MyZ
         (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
            '::> x6)
           '::> x7)
          '::> t)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ
            (((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
               '::> x6)
              '::> x7)
             '::> t)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR

    ------------------------------------------------------------------------
    -- 9 field lens combinators

    type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9
       = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9)

    instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
                         (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
                         (f t)
                         (f u) where
      _1 :: Lens
      (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
      (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
      (f t)
      (f u)
    _1 = (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9 -> f t)
    -> (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
        -> f u -> Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
    -> Lens
         (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
         (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    -> Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
         ((((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    -> Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
            ((((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
                         (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
                         (f t)
                         (f u) where
      _2 :: Lens
      (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
      (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
      (f t)
      (f u)
    _2 = (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9 -> f t)
    -> (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
        -> f u -> Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
    -> Lens
         (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
         (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
         ((((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
            ((((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
                         (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
                         (f t)
                         (f u) where
      _3 :: Lens
      (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
      (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
      (f t)
      (f u)
    _3 = (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9 -> f t)
    -> (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
        -> f u -> Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
    -> Lens
         (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
         (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
                         (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
                         (f t)
                         (f u) where
      _4 :: Lens
      (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
      (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
      (f t)
      (f u)
    _4 = (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9 -> f t)
    -> (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
        -> f u -> Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
    -> Lens
         (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
         (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    -> Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
     -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
                         (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
                         (f t)
                         (f u) where
      _5 :: Lens
      (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
      (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
      (f t)
      (f u)
    _5 = (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9 -> f t)
    -> (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
        -> f u -> Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
    -> Lens
         (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
         (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS (MyS 'MyZ))))
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    -> Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS (MyS 'MyZ))))
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
     -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
    -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
                         (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
                         (f t)
                         (f u) where
      _6 :: Lens
      (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
      (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
      (f t)
      (f u)
    _6 = (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9 -> f t)
    -> (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
        -> f u -> Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
    -> Lens
         (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
         (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
    -> MyNatLookup
         (MyS (MyS (MyS 'MyZ)))
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> t)
            '::> x7)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
    -> Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS (MyS 'MyZ)))
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
                '::> t)
               '::> x7)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n)
            where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
    n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
    -> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
                         (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
                         (f t)
                         (f u) where
      _7 :: Lens
      (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
      (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
      (f t)
      (f u)
    _7 = (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9 -> f t)
    -> (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
        -> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
    -> Lens
         (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
         (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
    -> MyNatLookup
         (MyS (MyS 'MyZ))
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> x6)
            '::> t)
           '::> x8)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
    n) (MyNatRepr (MyS (MyS 'MyZ))
    -> Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS (MyS 'MyZ))
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
                '::> x6)
               '::> t)
              '::> x8)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
    n)
            where n :: MyNatRepr (MyS (MyS 'MyZ))
    n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
    -> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
                         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
                         (f t)
                         (f u) where
      _8 :: Lens
      (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
      (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
      (f t)
      (f u)
    _8 = (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9 -> f t)
    -> (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
        -> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
    -> Lens
         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr (MyS 'MyZ)
    -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
    -> MyNatLookup
         (MyS 'MyZ)
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> x6)
            '::> x7)
           '::> t)
          '::> x9)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr (MyS 'MyZ)
    n) (MyNatRepr (MyS 'MyZ)
    -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            (MyS 'MyZ)
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
                '::> x6)
               '::> x7)
              '::> t)
             '::> x9)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr (MyS 'MyZ)
    n)
            where n :: MyNatRepr (MyS 'MyZ)
    n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
    MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
    -> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
    forall a b. (a -> b) -> a -> b
    $ MyNatRepr 'MyZ
    MyZR

    instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
                         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
                         (f t)
                         (f u) where
      _9 :: Lens
      (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
      (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
      (f t)
      (f u)
    _9 = (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t -> f t)
    -> (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
        -> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
    -> Lens
         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
         (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
         (f t)
         (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (MyNatRepr 'MyZ
    -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
    -> MyNatLookup
         'MyZ
         ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
             '::> x6)
            '::> x7)
           '::> x8)
          '::> t)
         f
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
    MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
    mynat_lookup MyNatRepr 'MyZ
    n) (MyNatRepr 'MyZ
    -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
    -> f u
    -> Assignment
         f
         (StrongCtxUpdate
            'MyZ
            ((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
                '::> x6)
               '::> x7)
              '::> x8)
             '::> t)
            u)
    forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    MyNatRepr n
    -> Assignment f ctx
    -> f tp
    -> Assignment f (StrongCtxUpdate n ctx tp)
    strong_ctx_update MyNatRepr 'MyZ
    n)
            where n :: MyNatRepr 'MyZ
    n = MyNatRepr 'MyZ
    MyZR