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

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
Assignment g 'EmptyCtx
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