    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE InstanceSigs #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE StandaloneDeriving #-}
    #if __GLASGOW_HASKELL__ < 806
    {-# LANGUAGE TypeInType #-}
    #endif
    {-# OPTIONS_HADDOCK hide #-}
    module Data.Parameterized.Context.Unsafe
      ( module Data.Parameterized.Ctx
      , KnownContext(..)
        -- * Size
      , Size
      , sizeInt
      , zeroSize
      , incSize
      , decSize
      , extSize
      , addSize
      , SizeView(..)
      , viewSize
      , sizeToNatRepr
        -- * 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
        -- ** IndexRange
      , IndexRange
      , allRange
      , indexOfRange
      , dropHeadRange
      , dropTailRange
        -- * Assignments
      , Assignment
      , size
      , Data.Parameterized.Context.Unsafe.replicate
      , generate
      , generateM
      , empty
      , extend
      , adjust
      , update
      , adjustM
      , AssignView(..)
      , viewAssign
      , (!)
      , (!^)
      , Data.Parameterized.Context.Unsafe.zipWith
      , zipWithM
      , (<++>)
      , traverseWithIndex
      ) where

    import qualified Control.Category as Cat
    import           Control.DeepSeq
    import           Control.Exception
    import qualified Control.Lens as Lens
    import           Control.Monad.Identity (Identity(..))
    import           Data.Bits
    import           Data.Coerce
    import           Data.Hashable
    import           Data.List (intercalate)
    import           Data.Proxy
    import           Unsafe.Coerce
    import           Data.Kind(Type)

    import           Data.Parameterized.Axiom
    import           Data.Parameterized.Classes
    import           Data.Parameterized.Ctx
    import           Data.Parameterized.Ctx.Proofs
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr))
    import           Data.Parameterized.Some
    import           Data.Parameterized.TraversableFC
    import           Data.Parameterized.TraversableFC.WithIndex

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

    -- | Represents the size of a context.
    newtype Size (ctx :: Ctx k) = Size Int

    type role Size nominal

    -- | Convert a context size to an 'Int'.
    sizeInt :: Size ctx -> Int
    sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt (Size Int
    n) = Int
    n

    -- | The size of an empty context.
    zeroSize :: Size 'EmptyCtx
    zeroSize :: forall {k}. Size 'EmptyCtx
    zeroSize = Int -> Size 'EmptyCtx
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size Int
    0

    -- | 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 Int
    n) = Int -> Size (ctx '::> tp)
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    decSize :: Size (ctx '::> tp) -> Size ctx
    decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
    decSize (Size Int
    n) = Bool -> Size ctx -> Size ctx
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Int -> Size ctx
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))

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

    -- | Project a size
    viewSize :: Size ctx -> SizeView ctx
    viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
    viewSize (Size Int
    0) = SizeView 'EmptyCtx -> SizeView ctx
    forall a b. a -> b
    unsafeCoerce SizeView 'EmptyCtx
    forall {k}. SizeView 'EmptyCtx
    ZeroSize
    viewSize (Size Int
    n) = Bool -> SizeView ctx -> SizeView ctx
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (SizeView (ZonkAny 51 '::> ZonkAny 52) -> SizeView ctx
    forall a b. a -> b
    unsafeCoerce (Size (ZonkAny 51) -> SizeView (ZonkAny 51 '::> ZonkAny 52)
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> SizeView (ctx '::> tp)
    IncSize (Int -> Size (ZonkAny 51)
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))))

    -- | 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 Int
    n) = Natural -> NatRepr (CtxSize items)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    n)

    instance Show (Size ctx) where
      show :: Size ctx -> String
    show (Size Int
    i) = Int -> String
    forall a. Show a => a -> String
    show Int
    i

    instance ShowF 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.
    newtype Diff (l :: Ctx k) (r :: Ctx k)
          = Diff { forall k (l :: Ctx k) (r :: Ctx k). Diff l r -> Int
    _contextExtSize :: Int }

    type role Diff nominal nominal

    -- | The identity difference. Identity element of 'Category' instance.
    noDiff :: Diff l l
    noDiff :: forall {k} (l :: Ctx k). Diff l l
    noDiff = Int -> Diff l l
    forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
    Diff Int
    0
    {-# INLINE noDiff #-}

    -- | 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 Int
    x) (Diff Int
    y) = Int -> Diff a c
    forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
    Diff (Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    y)
    {-# INLINE addDiff #-}

    -- | Extend the difference to a sub-context of the right side.
    extendRight :: Diff l r -> Diff l (r '::> tp)
    extendRight :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Diff l (r '::> tp)
    extendRight (Diff Int
    i) = Int -> Diff l (r '::> tp)
    forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
    Diff (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    appendDiff :: Size r -> Diff l (l <+> r)
    appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
    appendDiff (Size Int
    r) = Int -> Diff l (l <+> r)
    forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
    Diff Int
    r

    -- | 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
    noDiff
      Diff b c
    j . :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k).
    Diff b c -> Diff a b -> Diff a c
    . Diff a b
    i = 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
    i Diff b c
    j

    -- | 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 Int
    i) (Diff Int
    j) = Int -> Size r
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    j)

    -- | 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 Int
    x) (Size Int
    y) = Int -> Size (x <+> y)
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    y)

    -- | 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 Int
    i) = IsAppend (ZonkAny 47) (ZonkAny 47 <+> ZonkAny 48) -> IsAppend l r
    forall a b. a -> b
    unsafeCoerce (IsAppend (ZonkAny 47) (ZonkAny 47 <+> ZonkAny 48) -> IsAppend l r)
    -> IsAppend (ZonkAny 47) (ZonkAny 47 <+> ZonkAny 48)
    -> IsAppend l r
    forall a b. (a -> b) -> a -> b
    $ Size (ZonkAny 48)
    -> IsAppend (ZonkAny 47) (ZonkAny 47 <+> ZonkAny 48)
    forall {k} (ctx :: Ctx k) (l :: Ctx k).
    Size ctx -> IsAppend l (l <+> ctx)
    IsAppend (Int -> Size (ZonkAny 48)
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size Int
    i)

    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 Int
    i)
      | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = DiffView (ZonkAny 41) (ZonkAny 41) -> DiffView a b
    forall a b. a -> b
    unsafeCoerce DiffView (ZonkAny 41) (ZonkAny 41)
    forall {k} (a :: Ctx k). DiffView a a
    NoDiff
      | Bool
    otherwise  = Bool -> DiffView a b -> DiffView a b
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (DiffView a b -> DiffView a b) -> DiffView a b -> DiffView a b
    forall a b. (a -> b) -> a -> b
    $ DiffView (ZonkAny 43) (ZonkAny 44 ::> ZonkAny 45) -> DiffView a b
    forall a b. a -> b
    unsafeCoerce (DiffView (ZonkAny 43) (ZonkAny 44 ::> ZonkAny 45) -> DiffView a b)
    -> DiffView (ZonkAny 43) (ZonkAny 44 ::> ZonkAny 45)
    -> DiffView a b
    forall a b. (a -> b) -> a -> b
    $ Diff (ZonkAny 43) (ZonkAny 44)
    -> DiffView (ZonkAny 43) (ZonkAny 44 ::> ZonkAny 45)
    forall {k} (a :: Ctx k) (ctx :: Ctx k) (tp :: k).
    Diff a ctx -> DiffView a (ctx ::> tp)
    ExtendRightDiff (Int -> Diff (ZonkAny 43) (ZonkAny 44)
    forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
    Diff (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))

    ------------------------------------------------------------------------
    -- 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 {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where
      knownDiff :: Diff l (r '::> tp)
    knownDiff = Diff l r -> Diff l (r '::> tp)
    forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
    Diff l r -> Diff l (r '::> 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.
    newtype Index (ctx :: Ctx k) (tp :: k) = Index { forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    indexVal :: Int }

    type role Index nominal nominal

    instance Eq (Index ctx tp) where
      Index Int
    i == :: Index ctx tp -> Index ctx tp -> Bool
    == Index Int
    j = Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j

    instance EqF (Index ctx) where
      eqF :: forall (a :: k). Index ctx a -> Index ctx a -> Bool
    eqF (Index Int
    i) (Index Int
    j) = Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j

    instance TestEquality (Index ctx) where
      testEquality :: forall (a :: k) (b :: k).
    Index ctx a -> Index ctx b -> Maybe (a :~: b)
    testEquality (Index Int
    i) (Index Int
    j)
        | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: b
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
        | Bool
    otherwise = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance Ord (Index ctx tp) where
      Index Int
    i compare :: Index ctx tp -> Index ctx tp -> Ordering
    `compare` Index Int
    j = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Int
    i Int
    j

    instance OrdF (Index ctx) where
      compareF :: forall (x :: k) (y :: k).
    Index ctx x -> Index ctx y -> OrderingF x y
    compareF (Index Int
    i) (Index Int
    j)
        | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    j = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
        | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j = OrderingF (ZonkAny 56) (ZonkAny 56) -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce OrderingF (ZonkAny 56) (ZonkAny 56)
    forall {k} (x :: k). OrderingF x x
    EQF
        | Bool
    otherwise = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    -- | Index for first element in context.
    baseIndex :: Index ('EmptyCtx '::> tp) tp
    baseIndex :: forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
    baseIndex = Int -> Index ('EmptyCtx '::> tp) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    0

    -- | 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 Int
    i) = Int -> Index (ctx '::> y) x
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    i

    -- | Return the index of a element one past the size.
    nextIndex :: Size ctx -> Index (ctx ::> tp) tp
    nextIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size ctx
    n = Int -> Index (ctx ::> tp) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index (Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    n)

    -- | 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 Size (ctx ::> tp)
    n = Int -> Index (ctx ::> tp) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index (Size (ctx ::> tp) -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size (ctx ::> tp)
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

    -- | 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
    _ (Index Int
    il) = Int -> Index (l <+> r) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    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 Int
    sl) Size r
    _ (Index Int
    ir) = Int -> Index (l <+> r) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index (Int
    sl Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    ir)

    {-# 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
    _ = Index l tp -> Index r tp
    forall a b. a -> b
    unsafeCoerce

    {-# 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 Int
    l) Size r
    _ (Index Int
    idx) = Int -> Index (l <+> r) tp
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index (Int
    idx Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    l)

    -- | Given a size @n@, a function @f@, and an initial value @v0@, the
    -- expression @forIndex n f v0@ is equivalent to @v0@ when @n@ is
    -- zero, and @f (forIndex (n-1) f v0) n@ otherwise.  Unlike the safe
    -- version, which starts from 'Index' @0@ and increments 'Index'
    -- values, this version starts at 'Index' @(n-1)@ and decrements
    -- 'Index' values to 'Index' @0@.
    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
    n forall (tp :: k). r -> Index ctx tp -> r
    f r
    r =
      case Size ctx -> SizeView ctx
    forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
    viewSize Size ctx
    n of
        SizeView ctx
    ZeroSize -> r
    r
        IncSize Size ctx
    p -> r -> Index ctx tp -> r
    forall (tp :: k). r -> Index ctx tp -> r
    f (Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    forall {k} (ctx :: Ctx k) r.
    Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    forIndex Size ctx
    p ((r -> Index ctx (ZonkAny 53) -> r) -> r -> Index ctx tp -> r
    forall a b. Coercible a b => a -> b
    coerce r -> Index ctx (ZonkAny 53) -> r
    forall (tp :: k). r -> Index ctx tp -> r
    f) r
    r) (Size ctx -> Index (ctx '::> tp) tp
    forall {k} (ctx :: Ctx k) (tp :: k).
    Size ctx -> Index (ctx ::> tp) tp
    nextIndex Size ctx
    p)

    -- | Given an index @i@, size @n@, a function @f@, and a value @v@,
    -- the expression @forIndex i n f v@ is equivalent to
    -- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
    -- otherwise.
    forIndexRange :: forall ctx r
                   . Int
                  -> 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 Int
    n) forall (tp :: k). Index ctx tp -> r -> r
    f r
    r
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n = r
    r
      | Bool
    otherwise = Index ctx (ZonkAny 39) -> r -> r
    forall (tp :: k). Index ctx tp -> r -> r
    f (Int -> Index ctx (ZonkAny 39)
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    i) (Int
    -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
    forall {k} (ctx :: Ctx k) r.
    Int
    -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
    forIndexRange (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (Int -> Size ctx
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size Int
    n) Index ctx tp -> r -> r
    forall (tp :: k). Index ctx tp -> r -> r
    f r
    r)

    -- | 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
    i Size ctx
    n | Int
    0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    i Bool -> Bool -> Bool
    && Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    n = Some (Index ctx) -> Maybe (Some (Index ctx))
    forall a. a -> Maybe a
    Just (Index ctx (ZonkAny 54) -> Some (Index ctx)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (Int -> Index ctx (ZonkAny 54)
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    i))
                 | Bool
    otherwise = Maybe (Some (Index ctx))
    forall a. Maybe a
    Nothing

    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

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

    -- | 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 Int
    sz) (Index Int
    i)
      | Int
    sz' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i  = IndexView (ZonkAny 33 '::> ZonkAny 34) (ZonkAny 34)
    -> IndexView ctx tp
    forall a b. a -> b
    unsafeCoerce (Size (ZonkAny 33)
    -> IndexView (ZonkAny 33 '::> ZonkAny 34) (ZonkAny 34)
    forall {k} (ctx :: Ctx k) (t :: k).
    Size ctx -> IndexView (ctx '::> t) t
    IndexViewLast (Int -> Size (ZonkAny 33)
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size Int
    sz'))
      | Bool
    otherwise = IndexView (ZonkAny 36 '::> ZonkAny 37) (ZonkAny 38)
    -> IndexView ctx tp
    forall a b. a -> b
    unsafeCoerce (Index (ZonkAny 36) (ZonkAny 38)
    -> IndexView (ZonkAny 36 '::> ZonkAny 37) (ZonkAny 38)
    forall {k} (ctx :: Ctx k) (t :: k) (tp :: k).
    Index ctx t -> IndexView (ctx '::> tp) t
    IndexViewInit (Int -> Index (ZonkAny 36) (ZonkAny 38)
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    i))
      where
        sz' :: Int
    sz' = Int
    szInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1

    ------------------------------------------------------------------------
    -- IndexRange

    -- | This represents a contiguous range of indices.
    data IndexRange (ctx :: Ctx k) (sub :: Ctx k)
       = IndexRange {-# UNPACK #-} !Int
                    {-# UNPACK #-} !Int

    -- | Return a range containing all indices in the context.
    allRange :: Size ctx -> IndexRange ctx ctx
    allRange :: forall {k} (ctx :: Ctx k). Size ctx -> IndexRange ctx ctx
    allRange (Size Int
    n) = Int -> Int -> IndexRange ctx ctx
    forall k (ctx :: Ctx k) (sub :: Ctx k).
    Int -> Int -> IndexRange ctx sub
    IndexRange Int
    0 Int
    n

    -- | `indexOfRange` returns the only index in a range.
    indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
    indexOfRange :: forall {k} (ctx :: Ctx k) (e :: k).
    IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
    indexOfRange (IndexRange Int
    i Int
    n) = Bool -> Index ctx e -> Index ctx e
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1) (Index ctx e -> Index ctx e) -> Index ctx e -> Index ctx e
    forall a b. (a -> b) -> a -> b
    $ Int -> Index ctx e
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    i

    -- | @dropTailRange r n@ drops the last @n@ elements in @r@.
    dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
    dropTailRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k).
    IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
    dropTailRange (IndexRange Int
    i Int
    n) (Size Int
    j) = Bool -> IndexRange ctx x -> IndexRange ctx x
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    j) (IndexRange ctx x -> IndexRange ctx x)
    -> IndexRange ctx x -> IndexRange ctx x
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> IndexRange ctx x
    forall k (ctx :: Ctx k) (sub :: Ctx k).
    Int -> Int -> IndexRange ctx sub
    IndexRange Int
    i (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    j)

    -- | @dropHeadRange r n@ drops the first @n@ elements in @r@.
    dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
    dropHeadRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k).
    IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
    dropHeadRange (IndexRange Int
    i Int
    n) (Size Int
    j) = Bool -> IndexRange ctx y -> IndexRange ctx y
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    i' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    i Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    j) (IndexRange ctx y -> IndexRange ctx y)
    -> IndexRange ctx y -> IndexRange ctx y
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> IndexRange ctx y
    forall k (ctx :: Ctx k) (sub :: Ctx k).
    Int -> Int -> IndexRange ctx sub
    IndexRange Int
    i' (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    j)
      where i' :: Int
    i' = Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j

    ------------------------------------------------------------------------
    -- Height

    data Height = Zero | Succ Height

    type family Pred (k :: Height) :: Height
    type instance Pred ('Succ h) = h

    ------------------------------------------------------------------------
    -- * BalancedTree

    -- | A balanced tree where all leaves are at the same height.
    --
    -- The first parameter is the height of the tree.
    -- The second is the parameterized value.
    data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
      BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
      BalPair :: !(BalancedTree h f x)
              -> !(BalancedTree h f y)
              -> BalancedTree ('Succ h) f (x <+> y)

    bal_size :: BalancedTree h f p -> Int
    bal_size :: forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size (BalLeaf f x
    _) = Int
    1
    bal_size (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) = BalancedTree h f x -> Int
    forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size BalancedTree h f x
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + BalancedTree h f y -> Int
    forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size BalancedTree h f y
    y

    instance TestEqualityFC (BalancedTree h) where
      testEqualityFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y)
    testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test (BalLeaf f x
    x) (BalLeaf f x
    y) = do
        Refl <- f x -> f x -> Maybe (x :~: x)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test f x
    x f x
    y
        return Refl
      testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test (BalPair BalancedTree h f x
    x1 BalancedTree h f y
    x2) (BalPair BalancedTree h f x
    y1 BalancedTree h f y
    y2) = do
        Refl <- (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y)
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    TestEqualityFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y)
    testEqualityFC f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test BalancedTree h f x
    x1 BalancedTree h f x
    BalancedTree h f x
    y1
        Refl <- testEqualityFC test x2 y2
        return Refl

    instance OrdFC (BalancedTree h) where
      compareFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test (BalLeaf f x
    x) (BalLeaf f x
    y) =
        OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF (f x -> f x -> OrderingF x x
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test f x
    x f x
    y) (((x ~ x) => OrderingF x y) -> OrderingF x y)
    -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $ OrderingF x x
    OrderingF x y
    (x ~ x) => OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test (BalPair BalancedTree h f x
    x1 BalancedTree h f y
    x2) (BalPair BalancedTree h f x
    y1 BalancedTree h f y
    y2) =
        OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BalancedTree h f x
    x1 BalancedTree h f x
    BalancedTree h f x
    y1) (((x ~ x) => OrderingF x y) -> OrderingF x y)
    -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $
        OrderingF y y -> ((y ~ y) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BalancedTree h f y
    x2 BalancedTree h f y
    BalancedTree h f y
    y2) (((y ~ y) => OrderingF x y) -> OrderingF x y)
    -> ((y ~ y) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $
        OrderingF x x
    OrderingF x y
    (y ~ y) => OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF

    instance HashableF f => HashableF (BalancedTree h f) where
      hashWithSaltF :: forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int
    hashWithSaltF Int
    s BalancedTree h f tp
    t =
        case BalancedTree h f tp
    t of
          BalLeaf f x
    x -> Int
    s Int -> f x -> Int
    forall (tp :: k). Int -> f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    `hashWithSaltF` f x
    x
          BalPair BalancedTree h f x
    x BalancedTree h f y
    y -> Int
    s Int -> BalancedTree h f x -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int
    `hashWithSaltF` BalancedTree h f x
    x Int -> BalancedTree h f y -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int
    `hashWithSaltF` BalancedTree h f y
    y

    fmap_bal :: (forall tp . f tp -> g tp)
             -> BalancedTree h f c
             -> BalancedTree h g c
    fmap_bal :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    fmap_bal = (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    go
      where go :: (forall tp . f tp -> g tp)
                  -> BalancedTree h f c
                  -> BalancedTree h g c
            go :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    go forall (tp :: k). f tp -> g tp
    f (BalLeaf f x
    x) = g x -> BalancedTree 'Zero g (EmptyCtx '::> x)
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (f x -> g x
    forall (tp :: k). f tp -> g tp
    f f x
    x)
            go forall (tp :: k). f tp -> g tp
    f (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) = BalancedTree h g x
    -> BalancedTree h g y -> BalancedTree ('Succ h) g (x <+> y)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair ((forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f x -> BalancedTree h g x
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    go f tp -> g tp
    forall (tp :: k). f tp -> g tp
    f BalancedTree h f x
    x) ((forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f y -> BalancedTree h g y
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    go f tp -> g tp
    forall (tp :: k). f tp -> g tp
    f BalancedTree h f y
    y)
    {-# INLINABLE fmap_bal #-}

    traverse_bal :: Applicative m
                 => (forall tp . f tp -> m (g tp))
                 -> BalancedTree h f c
                 -> m (BalancedTree h g c)
    traverse_bal :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    traverse_bal = (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    go
      where go :: Applicative m
                  => (forall tp . f tp -> m (g tp))
                  -> BalancedTree h f c
                  -> m (BalancedTree h g c)
            go :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    go forall (tp :: k). f tp -> m (g tp)
    f (BalLeaf f x
    x) = g x -> BalancedTree h g c
    g x -> BalancedTree 'Zero g (EmptyCtx '::> x)
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (g x -> BalancedTree h g c) -> m (g x) -> m (BalancedTree h g c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f x -> m (g x)
    forall (tp :: k). f tp -> m (g tp)
    f f x
    x
            go forall (tp :: k). f tp -> m (g tp)
    f (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) = BalancedTree h g x -> BalancedTree h g y -> BalancedTree h g c
    BalancedTree h g x
    -> BalancedTree h g y -> BalancedTree ('Succ h) g (x <+> y)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair (BalancedTree h g x -> BalancedTree h g y -> BalancedTree h g c)
    -> m (BalancedTree h g x)
    -> m (BalancedTree h g y -> BalancedTree h g c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f x -> m (BalancedTree h g x)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    go f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f BalancedTree h f x
    x m (BalancedTree h g y -> BalancedTree h g c)
    -> m (BalancedTree h g y) -> m (BalancedTree h 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))
    -> BalancedTree h f y -> m (BalancedTree h g y)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    go f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f BalancedTree h f y
    y
    {-# INLINABLE traverse_bal #-}

    instance ShowF f => Show (BalancedTree h f tp) where
      show :: BalancedTree h f tp -> String
    show (BalLeaf f x
    x) = f x -> String
    forall (tp :: k). f tp -> String
    forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
    showF f x
    x
      show (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) = String
    "BalPair " String -> ShowS
    forall a. [a] -> [a] -> [a]
    Prelude.++ BalancedTree h f x -> String
    forall a. Show a => a -> String
    show BalancedTree h f x
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    Prelude.++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    Prelude.++ BalancedTree h f y -> String
    forall a. Show a => a -> String
    show BalancedTree h f y
    y

    instance ShowF f => ShowF (BalancedTree h f)

    unsafe_bal_generate :: forall ctx h f t
                         . Int -- ^ Height of tree to generate
                        -> Int -- ^ Starting offset for entries.
                        -> (forall tp . Index ctx tp -> f tp)
                        -> BalancedTree h f t
    unsafe_bal_generate :: forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
    Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree h f t
    unsafe_bal_generate Int
    h Int
    o forall (tp :: k). Index ctx tp -> f tp
    f
      | Int
    h Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <  Int
    0 = String -> BalancedTree h f t
    forall a. (?callStack::CallStack) => String -> a
    error String
    "unsafe_bal_generate given negative height"
      | Int
    h Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = BalancedTree 'Zero f (SingleCtx (ZonkAny 6)) -> BalancedTree h f t
    forall a b. a -> b
    unsafeCoerce (BalancedTree 'Zero f (SingleCtx (ZonkAny 6))
     -> BalancedTree h f t)
    -> BalancedTree 'Zero f (SingleCtx (ZonkAny 6))
    -> BalancedTree h f t
    forall a b. (a -> b) -> a -> b
    $ f (ZonkAny 6) -> BalancedTree 'Zero f (SingleCtx (ZonkAny 6))
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (Index ctx (ZonkAny 6) -> f (ZonkAny 6)
    forall (tp :: k). Index ctx tp -> f tp
    f (Int -> Index ctx (ZonkAny 6)
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    o))
      | Bool
    otherwise =
        let l :: BalancedTree (ZonkAny 7) f (ZonkAny 8)
    l = Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree (ZonkAny 7) f (ZonkAny 8)
    forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
    Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree h f t
    unsafe_bal_generate (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    o Index ctx tp -> f tp
    forall (tp :: k). Index ctx tp -> f tp
    f
            o' :: Int
    o' = Int
    o Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftL` (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)
            u :: BalancedTree (ZonkAny 7) f (ZonkAny 9)
    u = Bool
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    o Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + BalancedTree (ZonkAny 7) f (ZonkAny 8) -> Int
    forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size BalancedTree (ZonkAny 7) f (ZonkAny 8)
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    o') (BalancedTree (ZonkAny 7) f (ZonkAny 9)
     -> BalancedTree (ZonkAny 7) f (ZonkAny 9))
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    forall a b. (a -> b) -> a -> b
    $ Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
    Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree h f t
    unsafe_bal_generate (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    o' Index ctx tp -> f tp
    forall (tp :: k). Index ctx tp -> f tp
    f
         in BalancedTree ('Succ (ZonkAny 7)) f (ZonkAny 8 <+> ZonkAny 9)
    -> BalancedTree h f t
    forall a b. a -> b
    unsafeCoerce (BalancedTree ('Succ (ZonkAny 7)) f (ZonkAny 8 <+> ZonkAny 9)
     -> BalancedTree h f t)
    -> BalancedTree ('Succ (ZonkAny 7)) f (ZonkAny 8 <+> ZonkAny 9)
    -> BalancedTree h f t
    forall a b. (a -> b) -> a -> b
    $ BalancedTree (ZonkAny 7) f (ZonkAny 8)
    -> BalancedTree (ZonkAny 7) f (ZonkAny 9)
    -> BalancedTree ('Succ (ZonkAny 7)) f (ZonkAny 8 <+> ZonkAny 9)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair BalancedTree (ZonkAny 7) f (ZonkAny 8)
    l BalancedTree (ZonkAny 7) f (ZonkAny 9)
    u

    unsafe_bal_generateM :: forall m ctx h f t
                          . Applicative m
                         => Int -- ^ Height of tree to generate
                         -> Int -- ^ Starting offset for entries.
                         -> (forall x . Index ctx x -> m (f x))
                         -> m (BalancedTree h f t)
    unsafe_bal_generateM :: forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree h f t)
    unsafe_bal_generateM Int
    h Int
    o forall (x :: k). Index ctx x -> m (f x)
    f
      | Int
    h Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = BalancedTree 'Zero f (SingleCtx (ZonkAny 10)) -> BalancedTree h f t
    forall a b. a -> b
    unsafeCoerce (BalancedTree 'Zero f (SingleCtx (ZonkAny 10))
     -> BalancedTree h f t)
    -> (f (ZonkAny 10)
        -> BalancedTree 'Zero f (SingleCtx (ZonkAny 10)))
    -> f (ZonkAny 10)
    -> BalancedTree h f t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (ZonkAny 10) -> BalancedTree 'Zero f (SingleCtx (ZonkAny 10))
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (f (ZonkAny 10) -> BalancedTree h f t)
    -> m (f (ZonkAny 10)) -> m (BalancedTree h f t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Index ctx (ZonkAny 10) -> m (f (ZonkAny 10))
    forall (x :: k). Index ctx x -> m (f x)
    f (Int -> Index ctx (ZonkAny 10)
    forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
    Index Int
    o)
      | Bool
    otherwise =
        let o' :: Int
    o' = Int
    o Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftL` (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)
            g :: BalancedTree (ZonkAny 11) f (ZonkAny 12)
    -> BalancedTree (ZonkAny 11) f (ZonkAny 13) -> BalancedTree h f t
    g BalancedTree (ZonkAny 11) f (ZonkAny 12)
    lv BalancedTree (ZonkAny 11) f (ZonkAny 13)
    uv = Bool -> BalancedTree h f t -> BalancedTree h f t
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    o' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    o Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + BalancedTree (ZonkAny 11) f (ZonkAny 12) -> Int
    forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size BalancedTree (ZonkAny 11) f (ZonkAny 12)
    lv) (BalancedTree h f t -> BalancedTree h f t)
    -> BalancedTree h f t -> BalancedTree h f t
    forall a b. (a -> b) -> a -> b
    $
               BalancedTree ('Succ (ZonkAny 11)) f (ZonkAny 12 <+> ZonkAny 13)
    -> BalancedTree h f t
    forall a b. a -> b
    unsafeCoerce (BalancedTree (ZonkAny 11) f (ZonkAny 12)
    -> BalancedTree (ZonkAny 11) f (ZonkAny 13)
    -> BalancedTree ('Succ (ZonkAny 11)) f (ZonkAny 12 <+> ZonkAny 13)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair BalancedTree (ZonkAny 11) f (ZonkAny 12)
    lv BalancedTree (ZonkAny 11) f (ZonkAny 13)
    uv)
          in BalancedTree (ZonkAny 11) f (ZonkAny 12)
    -> BalancedTree (ZonkAny 11) f (ZonkAny 13) -> BalancedTree h f t
    g (BalancedTree (ZonkAny 11) f (ZonkAny 12)
     -> BalancedTree (ZonkAny 11) f (ZonkAny 13) -> BalancedTree h f t)
    -> m (BalancedTree (ZonkAny 11) f (ZonkAny 12))
    -> m (BalancedTree (ZonkAny 11) f (ZonkAny 13)
          -> BalancedTree h f t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree (ZonkAny 11) f (ZonkAny 12))
    forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree h f t)
    unsafe_bal_generateM (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    o  Index ctx x -> m (f x)
    forall (x :: k). Index ctx x -> m (f x)
    f
               m (BalancedTree (ZonkAny 11) f (ZonkAny 13) -> BalancedTree h f t)
    -> m (BalancedTree (ZonkAny 11) f (ZonkAny 13))
    -> m (BalancedTree h f t)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree (ZonkAny 11) f (ZonkAny 13))
    forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree h f t)
    unsafe_bal_generateM (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    o' Index ctx x -> m (f x)
    forall (x :: k). Index ctx x -> m (f x)
    f

    -- | Lookup index in tree.
    unsafe_bal_index :: BalancedTree h f a -- ^ Tree to lookup.
                     -> Int -- ^ Index to lookup.
                     -> Int  -- ^ Height of tree
                     -> f tp
    unsafe_bal_index :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
    BalancedTree h f a -> Int -> Int -> f tp
    unsafe_bal_index BalancedTree h f a
    _ Int
    j Int
    i
      | Int -> Bool -> Bool
    forall a b. a -> b -> b
    seq Int
    j (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> Bool -> Bool
    forall a b. a -> b -> b
    seq Int
    i (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    False = String -> f tp
    forall a. (?callStack::CallStack) => String -> a
    error String
    "bad unsafe_bal_index"
    unsafe_bal_index (BalLeaf f x
    u) Int
    _ Int
    i = Bool -> f tp -> f tp
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0) (f tp -> f tp) -> f tp -> f tp
    forall a b. (a -> b) -> a -> b
    $ f x -> f tp
    forall a b. a -> b
    unsafeCoerce f x
    u
    unsafe_bal_index (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) Int
    j Int
    i
      | Int
    j Int -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) = BalancedTree h f y -> Int -> Int -> f tp
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
    BalancedTree h f a -> Int -> Int -> f tp
    unsafe_bal_index BalancedTree h f y
    y Int
    j (Int -> f tp) -> Int -> f tp
    forall a b. (a -> b) -> a -> b
    $! (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)
      | Bool
    otherwise         = BalancedTree h f x -> Int -> Int -> f tp
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
    BalancedTree h f a -> Int -> Int -> f tp
    unsafe_bal_index BalancedTree h f x
    x Int
    j (Int -> f tp) -> Int -> f tp
    forall a b. (a -> b) -> a -> b
    $! (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

    -- | Update value at index in tree.
    unsafe_bal_adjust :: Functor m
                      => (f x -> m (f y))
                      -> BalancedTree h f a -- ^ Tree to update
                      -> Int -- ^ Index to lookup.
                      -> Int  -- ^ Height of tree
                      -> m (BalancedTree h f b)
    unsafe_bal_adjust :: forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
           (h :: Height) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
    unsafe_bal_adjust f x -> m (f y)
    f (BalLeaf f x
    u) Int
    _ Int
    i = Bool -> m (BalancedTree h f b) -> m (BalancedTree h f b)
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0) (m (BalancedTree h f b) -> m (BalancedTree h f b))
    -> m (BalancedTree h f b) -> m (BalancedTree h f b)
    forall a b. (a -> b) -> a -> b
    $
      (BalancedTree 'Zero f (SingleCtx y) -> BalancedTree h f b
    forall a b. a -> b
    unsafeCoerce (BalancedTree 'Zero f (SingleCtx y) -> BalancedTree h f b)
    -> (f y -> BalancedTree 'Zero f (SingleCtx y))
    -> f y
    -> BalancedTree h f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f y -> BalancedTree 'Zero f (SingleCtx y)
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (f y -> BalancedTree h f b) -> m (f y) -> m (BalancedTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (f x -> m (f y)
    f (f x -> f x
    forall a b. a -> b
    unsafeCoerce f x
    u)))
    unsafe_bal_adjust f x -> m (f y)
    f (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) Int
    j Int
    i
      | Int
    j Int -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) = (BalancedTree ('Succ h) f (x <+> ZonkAny 1) -> BalancedTree h f b
    forall a b. a -> b
    unsafeCoerce (BalancedTree ('Succ h) f (x <+> ZonkAny 1) -> BalancedTree h f b)
    -> (BalancedTree h f (ZonkAny 1)
        -> BalancedTree ('Succ h) f (x <+> ZonkAny 1))
    -> BalancedTree h f (ZonkAny 1)
    -> BalancedTree h f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BalancedTree h f x
    -> BalancedTree h f (ZonkAny 1)
    -> BalancedTree ('Succ h) f (x <+> ZonkAny 1)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair BalancedTree h f x
    x      (BalancedTree h f (ZonkAny 1) -> BalancedTree h f b)
    -> m (BalancedTree h f (ZonkAny 1)) -> m (BalancedTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f x -> m (f y))
    -> BalancedTree h f y
    -> Int
    -> Int
    -> m (BalancedTree h f (ZonkAny 1))
    forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
           (h :: Height) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
    unsafe_bal_adjust f x -> m (f y)
    f BalancedTree h f y
    y Int
    j (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)))
      | Bool
    otherwise         = (BalancedTree ('Succ h) f (ZonkAny 2 <+> y) -> BalancedTree h f b
    forall a b. a -> b
    unsafeCoerce (BalancedTree ('Succ h) f (ZonkAny 2 <+> y) -> BalancedTree h f b)
    -> (BalancedTree h f (ZonkAny 2)
        -> BalancedTree ('Succ h) f (ZonkAny 2 <+> y))
    -> BalancedTree h f (ZonkAny 2)
    -> BalancedTree h f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (BalancedTree h f (ZonkAny 2)
     -> BalancedTree h f y
     -> BalancedTree ('Succ h) f (ZonkAny 2 <+> y))
    -> BalancedTree h f y
    -> BalancedTree h f (ZonkAny 2)
    -> BalancedTree ('Succ h) f (ZonkAny 2 <+> y)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip BalancedTree h f (ZonkAny 2)
    -> BalancedTree h f y -> BalancedTree ('Succ h) f (ZonkAny 2 <+> y)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair BalancedTree h f y
    y (BalancedTree h f (ZonkAny 2) -> BalancedTree h f b)
    -> m (BalancedTree h f (ZonkAny 2)) -> m (BalancedTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f x -> m (f y))
    -> BalancedTree h f x
    -> Int
    -> Int
    -> m (BalancedTree h f (ZonkAny 2))
    forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
           (h :: Height) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
    unsafe_bal_adjust f x -> m (f y)
    f BalancedTree h f x
    x Int
    j (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)))

    {-# SPECIALIZE unsafe_bal_adjust
         :: (f x -> Identity (f y))
         -> BalancedTree h f a
         -> Int
         -> Int
         -> Identity (BalancedTree h f b)
      #-}

    -- | Zip two balanced trees together.
    bal_zipWithM :: Applicative m
                 => (forall x . f x -> g x -> m (h x))
                 -> BalancedTree u f a
                 -> BalancedTree u g a
                 -> m (BalancedTree u h a)
    bal_zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree u f a
    -> BalancedTree u g a
    -> m (BalancedTree u h a)
    bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
    f (BalLeaf f x
    x) (BalLeaf g x
    y) = h x -> BalancedTree u h a
    h x -> BalancedTree 'Zero h (EmptyCtx '::> x)
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf (h x -> BalancedTree u h a) -> m (h x) -> m (BalancedTree u h a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f f x
    x g x
    g x
    y
    bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
    f (BalPair BalancedTree h f x
    x1 BalancedTree h f y
    x2) (BalPair BalancedTree h g x
    y1 BalancedTree h g y
    y2) =
      BalancedTree h h x -> BalancedTree h h y -> BalancedTree u h a
    BalancedTree h h x
    -> BalancedTree h h y -> BalancedTree ('Succ h) h (x <+> y)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair (BalancedTree h h x -> BalancedTree h h y -> BalancedTree u h a)
    -> m (BalancedTree h h x)
    -> m (BalancedTree h h y -> BalancedTree u h a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree h f x
    -> BalancedTree h g x
    -> m (BalancedTree h h x)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree u f a
    -> BalancedTree u g a
    -> m (BalancedTree u h a)
    bal_zipWithM f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BalancedTree h f x
    x1 (BalancedTree h g x -> BalancedTree h g x
    forall a b. a -> b
    unsafeCoerce BalancedTree h g x
    y1)
              m (BalancedTree h h y -> BalancedTree u h a)
    -> m (BalancedTree h h y) -> m (BalancedTree u h a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree h f y
    -> BalancedTree h g y
    -> m (BalancedTree h h y)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree u f a
    -> BalancedTree u g a
    -> m (BalancedTree u h a)
    bal_zipWithM f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BalancedTree h f y
    x2 (BalancedTree h g y -> BalancedTree h g y
    forall a b. a -> b
    unsafeCoerce BalancedTree h g y
    y2)
    {-# INLINABLE bal_zipWithM #-}

    ------------------------------------------------------------------------
    -- * BinomialTree

    data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
      Empty :: BinomialTree h f EmptyCtx

      -- Contains size of the subtree, subtree, then element.
      PlusOne  :: !Int
               -> !(BinomialTree ('Succ h) f x)
               -> !(BalancedTree h f y)
               -> BinomialTree h f (x <+> y)

      -- Contains size of the subtree, subtree, then element.
      PlusZero  :: !Int
                -> !(BinomialTree ('Succ h) f x)
                -> BinomialTree h f x

    tsize :: BinomialTree h f a -> Int
    tsize :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    tsize BinomialTree h f a
    Empty = Int
    0
    tsize (PlusOne Int
    s BinomialTree ('Succ h) f x
    _ BalancedTree h f y
    _) = Int
    2Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1
    tsize (PlusZero  Int
    s BinomialTree ('Succ h) f a
    _) = Int
    2Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    s

    t_cnt_size :: BinomialTree h f a -> Int
    t_cnt_size :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    t_cnt_size BinomialTree h f a
    Empty = Int
    0
    t_cnt_size (PlusOne Int
    _ BinomialTree ('Succ h) f x
    l BalancedTree h f y
    r) = BinomialTree ('Succ h) f x -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    t_cnt_size BinomialTree ('Succ h) f x
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + BalancedTree h f y -> Int
    forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
    BalancedTree h f p -> Int
    bal_size BalancedTree h f y
    r
    t_cnt_size (PlusZero  Int
    _ BinomialTree ('Succ h) f a
    l) = BinomialTree ('Succ h) f a -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    t_cnt_size BinomialTree ('Succ h) f a
    l

    -- | Concatenate a binomial tree and a balanced tree.
    append :: BinomialTree h f x
           -> BalancedTree h f y
           -> BinomialTree h f (x <+> y)
    append :: forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x
    -> BalancedTree h f y -> BinomialTree h f (x <+> y)
    append BinomialTree h f x
    Empty BalancedTree h f y
    y = Int
    -> BinomialTree ('Succ h) f 'EmptyCtx
    -> BalancedTree h f y
    -> BinomialTree h f ('EmptyCtx <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    0 BinomialTree ('Succ h) f 'EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty BalancedTree h f y
    y
    append (PlusOne Int
    _ BinomialTree ('Succ h) f x
    t BalancedTree h f y
    x) BalancedTree h f y
    y =
      case BinomialTree ('Succ h) f x
    -> BalancedTree h f y
    -> BalancedTree h f y
    -> (x <+> (y <+> y)) :~: ((x <+> y) <+> y)
    forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
           (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
    p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
    assoc BinomialTree ('Succ h) f x
    t BalancedTree h f y
    x BalancedTree h f y
    y of
        (x <+> (y <+> y)) :~: ((x <+> y) <+> y)
    Refl ->
          let t' :: BinomialTree ('Succ h) f (x <+> (y <+> y))
    t' = BinomialTree ('Succ h) f x
    -> BalancedTree ('Succ h) f (y <+> y)
    -> BinomialTree ('Succ h) f (x <+> (y <+> y))
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x
    -> BalancedTree h f y -> BinomialTree h f (x <+> y)
    append BinomialTree ('Succ h) f x
    t (BalancedTree h f y
    -> BalancedTree h f y -> BalancedTree ('Succ h) f (y <+> y)
    forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
           (y :: Ctx k).
    BalancedTree ctx f tp
    -> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
    BalPair BalancedTree h f y
    x BalancedTree h f y
    y)
           in Int
    -> BinomialTree ('Succ h) f (x <+> y) -> BinomialTree h f (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero (BinomialTree ('Succ h) f (x <+> y) -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    tsize BinomialTree ('Succ h) f (x <+> y)
    BinomialTree ('Succ h) f (x <+> (y <+> y))
    t') BinomialTree ('Succ h) f (x <+> y)
    BinomialTree ('Succ h) f (x <+> (y <+> y))
    t'
    append (PlusZero Int
    s BinomialTree ('Succ h) f x
    t) BalancedTree h f y
    x = Int
    -> BinomialTree ('Succ h) f x
    -> BalancedTree h f y
    -> BinomialTree h f (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s BinomialTree ('Succ h) f x
    t BalancedTree h f y
    x

    instance TestEqualityFC (BinomialTree h) where
      testEqualityFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree h f x -> BinomialTree h f y -> Maybe (x :~: y)
    testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    _ BinomialTree h f x
    Empty BinomialTree h f y
    Empty = (x :~: y) -> Maybe (x :~: y)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return x :~: x
    x :~: y
    forall {k} (a :: k). a :~: a
    Refl
      testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test (PlusZero Int
    _ BinomialTree ('Succ h) f x
    x1) (PlusZero Int
    _ BinomialTree ('Succ h) f y
    y1) = do
        Refl <- (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> Maybe (x :~: y)
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    TestEqualityFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> Maybe (x :~: y)
    testEqualityFC f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test BinomialTree ('Succ h) f x
    x1 BinomialTree ('Succ h) f y
    y1
        return Refl
      testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test (PlusOne Int
    _ BinomialTree ('Succ h) f x
    x1 BalancedTree h f y
    x2) (PlusOne Int
    _ BinomialTree ('Succ h) f x
    y1 BalancedTree h f y
    y2) = do
        Refl <- (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> Maybe (x :~: y)
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    TestEqualityFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> Maybe (x :~: y)
    testEqualityFC f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test BinomialTree ('Succ h) f x
    x1 BinomialTree ('Succ h) f x
    y1
        Refl <- testEqualityFC test x2 y2
        return Refl
      testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    _ BinomialTree h f x
    _ BinomialTree h f y
    _ = Maybe (x :~: y)
    forall a. Maybe a
    Nothing

    instance OrdFC (BinomialTree h) where
      compareFC :: forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree h f x -> BinomialTree h f y -> OrderingF x y
    compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ BinomialTree h f x
    Empty BinomialTree h f y
    Empty = OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ BinomialTree h f x
    Empty BinomialTree h f y
    _ = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ BinomialTree h f x
    _ BinomialTree h f y
    Empty = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test (PlusZero Int
    _ BinomialTree ('Succ h) f x
    x1) (PlusZero Int
    _ BinomialTree ('Succ h) f y
    y1) =
        OrderingF x y -> ((x ~ y) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BinomialTree ('Succ h) f x
    x1 BinomialTree ('Succ h) f y
    y1) (((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
      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ PlusZero{} BinomialTree h f y
    _ = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    _ BinomialTree h f x
    _ PlusZero{} = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

      compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test (PlusOne Int
    _ BinomialTree ('Succ h) f x
    x1 BalancedTree h f y
    x2) (PlusOne Int
    _ BinomialTree ('Succ h) f x
    y1 BalancedTree h f y
    y2) =
        OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree ('Succ h) f x
       -> BinomialTree ('Succ h) f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BinomialTree ('Succ h) f x
    x1 BinomialTree ('Succ h) f x
    y1) (((x ~ x) => OrderingF x y) -> OrderingF x y)
    -> ((x ~ x) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $
        OrderingF y y -> ((y ~ y) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BalancedTree h f y
    x2 BalancedTree h f y
    y2) (((y ~ y) => OrderingF x y) -> OrderingF x y)
    -> ((y ~ y) => OrderingF x y) -> OrderingF x y
    forall a b. (a -> b) -> a -> b
    $
        OrderingF x x
    OrderingF x y
    (y ~ y) => OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF

    instance HashableF f => HashableF (BinomialTree h f) where
      hashWithSaltF :: forall (tp :: Ctx k). Int -> BinomialTree h f tp -> Int
    hashWithSaltF Int
    s BinomialTree h f tp
    t =
        case BinomialTree h f tp
    t of
          BinomialTree h f tp
    Empty -> Int
    s
          PlusZero Int
    _ BinomialTree ('Succ h) f tp
    x   -> Int
    s Int -> BinomialTree ('Succ h) f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BinomialTree ('Succ h) f tp -> Int
    `hashWithSaltF` BinomialTree ('Succ h) f tp
    x
          PlusOne  Int
    _ BinomialTree ('Succ h) f x
    x BalancedTree h f y
    y -> Int
    s Int -> BinomialTree ('Succ h) f x -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BinomialTree ('Succ h) f tp -> Int
    `hashWithSaltF` BinomialTree ('Succ h) f x
    x Int -> BalancedTree h f y -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int
    `hashWithSaltF` BalancedTree h f y
    y

    -- | Map over a binary tree.
    fmap_bin :: (forall tp . f tp -> g tp)
             -> BinomialTree h f c
             -> BinomialTree h g c
    fmap_bin :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BinomialTree h f c -> BinomialTree h g c
    fmap_bin forall (tp :: k). f tp -> g tp
    _ BinomialTree h f c
    Empty = BinomialTree h g c
    BinomialTree h g 'EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty
    fmap_bin forall (tp :: k). f tp -> g tp
    f (PlusOne Int
    s BinomialTree ('Succ h) f x
    t BalancedTree h f y
    x) = Int
    -> BinomialTree ('Succ h) g x
    -> BalancedTree h g y
    -> BinomialTree h g (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s ((forall (tp :: k). f tp -> g tp)
    -> BinomialTree ('Succ h) f x -> BinomialTree ('Succ h) g x
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BinomialTree h f c -> BinomialTree h g c
    fmap_bin f tp -> g tp
    forall (tp :: k). f tp -> g tp
    f BinomialTree ('Succ h) f x
    t) ((forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f y -> BalancedTree h g y
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BalancedTree h f c -> BalancedTree h g c
    fmap_bal f tp -> g tp
    forall (tp :: k). f tp -> g tp
    f BalancedTree h f y
    x)
    fmap_bin forall (tp :: k). f tp -> g tp
    f (PlusZero Int
    s BinomialTree ('Succ h) f c
    t)  = Int -> BinomialTree ('Succ h) g c -> BinomialTree h g c
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s ((forall (tp :: k). f tp -> g tp)
    -> BinomialTree ('Succ h) f c -> BinomialTree ('Succ h) g c
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BinomialTree h f c -> BinomialTree h g c
    fmap_bin f tp -> g tp
    forall (tp :: k). f tp -> g tp
    f BinomialTree ('Succ h) f c
    t)
    {-# INLINABLE fmap_bin #-}

    traverse_bin :: Applicative m
                 => (forall tp . f tp -> m (g tp))
                 -> BinomialTree h f c
                 -> m (BinomialTree h g c)
    traverse_bin :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree h f c -> m (BinomialTree h g c)
    traverse_bin forall (tp :: k). f tp -> m (g tp)
    _ BinomialTree h f c
    Empty = BinomialTree h g c -> m (BinomialTree h g c)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure BinomialTree h g c
    BinomialTree h g 'EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty
    traverse_bin forall (tp :: k). f tp -> m (g tp)
    f (PlusOne Int
    s BinomialTree ('Succ h) f x
    t BalancedTree h f y
    x) = Int
    -> BinomialTree ('Succ h) g x
    -> BalancedTree h g y
    -> BinomialTree h g (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s  (BinomialTree ('Succ h) g x
     -> BalancedTree h g y -> BinomialTree h g c)
    -> m (BinomialTree ('Succ h) g x)
    -> m (BalancedTree h g y -> BinomialTree h g c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree ('Succ h) f x -> m (BinomialTree ('Succ h) g x)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree h f c -> m (BinomialTree h g c)
    traverse_bin f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f BinomialTree ('Succ h) f x
    t m (BalancedTree h g y -> BinomialTree h g c)
    -> m (BalancedTree h g y) -> m (BinomialTree h 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))
    -> BalancedTree h f y -> m (BalancedTree h g y)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BalancedTree h f c -> m (BalancedTree h g c)
    traverse_bal f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f BalancedTree h f y
    x
    traverse_bin forall (tp :: k). f tp -> m (g tp)
    f (PlusZero Int
    s BinomialTree ('Succ h) f c
    t)  = Int -> BinomialTree ('Succ h) g c -> BinomialTree h g c
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s (BinomialTree ('Succ h) g c -> BinomialTree h g c)
    -> m (BinomialTree ('Succ h) g c) -> m (BinomialTree h g c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree ('Succ h) f c -> m (BinomialTree ('Succ h) g c)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree h f c -> m (BinomialTree h g c)
    traverse_bin f tp -> m (g tp)
    forall (tp :: k). f tp -> m (g tp)
    f BinomialTree ('Succ h) f c
    t
    {-# INLINABLE traverse_bin #-}

    unsafe_bin_generate :: forall h f ctx t
                         . Int -- ^ Size of tree to generate
                        -> Int -- ^ Height of each element.
                        -> (forall x . Index ctx x -> f x)
                        -> BinomialTree h f t
    unsafe_bin_generate :: forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree h f t
    unsafe_bin_generate Int
    sz Int
    h forall (x :: k). Index ctx x -> f x
    f
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = BinomialTree (ZonkAny 27) (ZonkAny 28) EmptyCtx
    -> BinomialTree h f t
    forall a b. a -> b
    unsafeCoerce BinomialTree (ZonkAny 27) (ZonkAny 28) EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty
      | Int
    sz Int -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    0 =
        let s :: Int
    s = Int
    sz Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    1
            t :: BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30)
    t = Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree h f t
    unsafe_bin_generate Int
    s (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Index ctx x -> f x
    forall (x :: k). Index ctx x -> f x
    f
            o :: Int
    o = Int
    s Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    2Int -> Int -> Int
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)
            u :: BalancedTree (ZonkAny 29) f (ZonkAny 31)
    u = Bool
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    o Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30) -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    t_cnt_size BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30)
    t) (BalancedTree (ZonkAny 29) f (ZonkAny 31)
     -> BalancedTree (ZonkAny 29) f (ZonkAny 31))
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    forall a b. (a -> b) -> a -> b
    $ Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
    Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BalancedTree h f t
    unsafe_bal_generate Int
    h Int
    o Index ctx tp -> f tp
    forall (x :: k). Index ctx x -> f x
    f
         in BinomialTree (ZonkAny 29) f (ZonkAny 30 <+> ZonkAny 31)
    -> BinomialTree h f t
    forall a b. a -> b
    unsafeCoerce (Int
    -> BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30)
    -> BalancedTree (ZonkAny 29) f (ZonkAny 31)
    -> BinomialTree (ZonkAny 29) f (ZonkAny 30 <+> ZonkAny 31)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s BinomialTree ('Succ (ZonkAny 29)) f (ZonkAny 30)
    t BalancedTree (ZonkAny 29) f (ZonkAny 31)
    u)
      | Bool
    otherwise =
        let s :: Int
    s = Int
    sz Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    1
            t :: BinomialTree ('Succ h) f t
    t = Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree ('Succ h) f t
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree h f t
    unsafe_bin_generate (Int
    sz Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    1) (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Index ctx x -> f x
    forall (x :: k). Index ctx x -> f x
    f
            r :: BinomialTree h f t
            r :: BinomialTree h f t
    r = Int -> BinomialTree ('Succ h) f t -> BinomialTree h f t
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s BinomialTree ('Succ h) f t
    t
        in BinomialTree h f t
    r

    unsafe_bin_generateM :: forall m h f ctx t
                          . Applicative m
                         => Int -- ^ Size of tree to generate
                         -> Int -- ^ Height of each element.
                         -> (forall x . Index ctx x -> m (f x))
                         -> m (BinomialTree h f t)
    unsafe_bin_generateM :: forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree h f t)
    unsafe_bin_generateM Int
    sz Int
    h forall (x :: k). Index ctx x -> m (f x)
    f
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = BinomialTree h f t -> m (BinomialTree h f t)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BinomialTree (ZonkAny 15) (ZonkAny 16) EmptyCtx
    -> BinomialTree h f t
    forall a b. a -> b
    unsafeCoerce BinomialTree (ZonkAny 15) (ZonkAny 16) EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty)
      | Int
    sz Int -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    0 =
        let s :: Int
    s = Int
    sz Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    1
            t :: m (BinomialTree (ZonkAny 17) f (ZonkAny 18))
    t = Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree (ZonkAny 17) f (ZonkAny 18))
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree h f t)
    unsafe_bin_generateM Int
    s (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Index ctx x -> m (f x)
    forall (x :: k). Index ctx x -> m (f x)
    f
            -- Next offset
            o :: Int
    o = Int
    s Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    2Int -> Int -> Int
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)
            u :: m (BalancedTree (ZonkAny 19) f (ZonkAny 20))
    u = Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree (ZonkAny 19) f (ZonkAny 20))
    forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BalancedTree h f t)
    unsafe_bal_generateM Int
    h Int
    o Index ctx x -> m (f x)
    forall (x :: k). Index ctx x -> m (f x)
    f
            r :: m (BinomialTree h f t)
    r = (BinomialTree ('Succ (ZonkAny 22)) (ZonkAny 23) (ZonkAny 24)
     -> BalancedTree (ZonkAny 22) (ZonkAny 23) (ZonkAny 25)
     -> BinomialTree
          (ZonkAny 22) (ZonkAny 23) (ZonkAny 24 <+> ZonkAny 25))
    -> BinomialTree (ZonkAny 17) f (ZonkAny 18)
    -> BalancedTree (ZonkAny 19) f (ZonkAny 20)
    -> BinomialTree h f t
    forall a b. a -> b
    unsafeCoerce (Int
    -> BinomialTree ('Succ (ZonkAny 22)) (ZonkAny 23) (ZonkAny 24)
    -> BalancedTree (ZonkAny 22) (ZonkAny 23) (ZonkAny 25)
    -> BinomialTree
         (ZonkAny 22) (ZonkAny 23) (ZonkAny 24 <+> ZonkAny 25)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s) (BinomialTree (ZonkAny 17) f (ZonkAny 18)
     -> BalancedTree (ZonkAny 19) f (ZonkAny 20) -> BinomialTree h f t)
    -> m (BinomialTree (ZonkAny 17) f (ZonkAny 18))
    -> m (BalancedTree (ZonkAny 19) f (ZonkAny 20)
          -> BinomialTree h f t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (BinomialTree (ZonkAny 17) f (ZonkAny 18))
    t m (BalancedTree (ZonkAny 19) f (ZonkAny 20) -> BinomialTree h f t)
    -> m (BalancedTree (ZonkAny 19) f (ZonkAny 20))
    -> m (BinomialTree h f t)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (BalancedTree (ZonkAny 19) f (ZonkAny 20))
    u
         in m (BinomialTree h f t)
    r
      | Bool
    otherwise =
        let s :: Int
    s = Int
    sz Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    1
            t :: m (BinomialTree ('Succ h) f t)
    t = Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree ('Succ h) f t)
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree h f t)
    unsafe_bin_generateM Int
    s (Int
    hInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Index ctx x -> m (f x)
    forall (x :: k). Index ctx x -> m (f x)
    f
            r :: m (BinomialTree h f t)
            r :: m (BinomialTree h f t)
    r = Int -> BinomialTree ('Succ h) f t -> BinomialTree h f t
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s (BinomialTree ('Succ h) f t -> BinomialTree h f t)
    -> m (BinomialTree ('Succ h) f t) -> m (BinomialTree h f t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (BinomialTree ('Succ h) f t)
    t
         in m (BinomialTree h f t)
    r

    ------------------------------------------------------------------------
    -- Dropping

    data DropResult f (ctx :: Ctx k) where
      DropEmpty :: DropResult f EmptyCtx
      DropExt   :: BinomialTree 'Zero f x
                -> f y
                -> DropResult f (x ::> y)

    -- | @bal_drop x y@ returns the tree formed @append x (init y)@
    bal_drop :: forall h f x y
              . BinomialTree h f x
                -- ^ Bina
             -> BalancedTree h f y
             -> DropResult f (x <+> y)
    bal_drop :: forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
    bal_drop BinomialTree h f x
    t (BalLeaf f x
    e) = BinomialTree 'Zero f x -> f x -> DropResult f (x ::> x)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    BinomialTree 'Zero f ctx -> f tp -> DropResult f (ctx ::> tp)
    DropExt BinomialTree h f x
    BinomialTree 'Zero f x
    t f x
    e
    bal_drop BinomialTree h f x
    t (BalPair BalancedTree h f x
    x BalancedTree h f y
    y) =
      DropResult f ((ZonkAny 0 <+> x) <+> y) -> DropResult f (x <+> y)
    forall a b. a -> b
    unsafeCoerce (BinomialTree h f (ZonkAny 0 <+> x)
    -> BalancedTree h f y -> DropResult f ((ZonkAny 0 <+> x) <+> y)
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
    bal_drop (Int
    -> BinomialTree ('Succ h) f (ZonkAny 0)
    -> BalancedTree h f x
    -> BinomialTree h f (ZonkAny 0 <+> x)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne (BinomialTree h f x -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    tsize BinomialTree h f x
    t) (BinomialTree h f x -> BinomialTree ('Succ h) f (ZonkAny 0)
    forall a b. a -> b
    unsafeCoerce BinomialTree h f x
    t) BalancedTree h f x
    x) BalancedTree h f y
    y)

    bin_drop :: forall h f ctx
              . BinomialTree h f ctx
             -> DropResult f ctx
    bin_drop :: forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
    BinomialTree h f ctx -> DropResult f ctx
    bin_drop BinomialTree h f ctx
    Empty = DropResult f ctx
    DropResult f 'EmptyCtx
    forall {k} (f :: k -> *). DropResult f EmptyCtx
    DropEmpty
    bin_drop (PlusZero Int
    _ BinomialTree ('Succ h) f ctx
    u) = BinomialTree ('Succ h) f ctx -> DropResult f ctx
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
    BinomialTree h f ctx -> DropResult f ctx
    bin_drop BinomialTree ('Succ h) f ctx
    u
    bin_drop (PlusOne Int
    s BinomialTree ('Succ h) f x
    t BalancedTree h f y
    u) =
      let m :: BinomialTree h f x
    m = case BinomialTree ('Succ h) f x
    t of
                BinomialTree ('Succ h) f x
    Empty -> BinomialTree h f x
    BinomialTree h f 'EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty
                BinomialTree ('Succ h) f x
    _ -> Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s BinomialTree ('Succ h) f x
    t
       in BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
    bal_drop BinomialTree h f x
    m BalancedTree h f y
    u

    ------------------------------------------------------------------------
    -- Indexing

    -- | Lookup value in tree.
    unsafe_bin_index :: BinomialTree h f a -- ^ Tree to lookup in.
                     -> Int
                     -> Int -- ^ Size of tree
                     -> f u
    unsafe_bin_index :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
    BinomialTree h f a -> Int -> Int -> f u
    unsafe_bin_index BinomialTree h f a
    _ Int
    _ Int
    i
      | Int -> Bool -> Bool
    forall a b. a -> b -> b
    seq Int
    i Bool
    False = String -> f u
    forall a. (?callStack::CallStack) => String -> a
    error String
    "bad unsafe_bin_index"
    unsafe_bin_index BinomialTree h f a
    Empty Int
    _ Int
    _ = String -> f u
    forall a. (?callStack::CallStack) => String -> a
    error String
    "unsafe_bin_index reached end of list"
    unsafe_bin_index (PlusOne Int
    sz BinomialTree ('Succ h) f x
    t BalancedTree h f y
    u) Int
    j Int
    i
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i) = BalancedTree h f y -> Int -> Int -> f u
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
    BalancedTree h f a -> Int -> Int -> f tp
    unsafe_bal_index BalancedTree h f y
    u Int
    j Int
    i
      | Bool
    otherwise = BinomialTree ('Succ h) f x -> Int -> Int -> f u
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
    BinomialTree h f a -> Int -> Int -> f u
    unsafe_bin_index BinomialTree ('Succ h) f x
    t Int
    j (Int -> f u) -> Int -> f u
    forall a b. (a -> b) -> a -> b
    $! (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i)
    unsafe_bin_index (PlusZero Int
    sz BinomialTree ('Succ h) f a
    t) Int
    j Int
    i
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i) = String -> f u
    forall a. (?callStack::CallStack) => String -> a
    error String
    "unsafe_bin_index stopped at PlusZero"
      | Bool
    otherwise = BinomialTree ('Succ h) f a -> Int -> Int -> f u
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
    BinomialTree h f a -> Int -> Int -> f u
    unsafe_bin_index BinomialTree ('Succ h) f a
    t Int
    j (Int -> f u) -> Int -> f u
    forall a b. (a -> b) -> a -> b
    $! (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i)

    -- | Lookup value in tree.
    unsafe_bin_adjust :: forall m h f x y a b
                       . Functor m
                      => (f x -> m (f y))
                      -> BinomialTree h f a -- ^ Tree to lookup in.
                      -> Int
                      -> Int -- ^ Size of tree
                      -> m (BinomialTree h f b)
    unsafe_bin_adjust :: forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
           (y :: k) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
    unsafe_bin_adjust f x -> m (f y)
    _ BinomialTree h f a
    Empty Int
    _ Int
    _ = String -> m (BinomialTree h f b)
    forall a. (?callStack::CallStack) => String -> a
    error String
    "unsafe_bin_adjust reached end of list"
    unsafe_bin_adjust f x -> m (f y)
    f (PlusOne Int
    sz BinomialTree ('Succ h) f x
    t BalancedTree h f y
    u) Int
    j Int
    i
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i) =
        BinomialTree h f (x <+> ZonkAny 3) -> BinomialTree h f b
    forall a b. a -> b
    unsafeCoerce (BinomialTree h f (x <+> ZonkAny 3) -> BinomialTree h f b)
    -> (BalancedTree h f (ZonkAny 3)
        -> BinomialTree h f (x <+> ZonkAny 3))
    -> BalancedTree h f (ZonkAny 3)
    -> BinomialTree h f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int
    -> BinomialTree ('Succ h) f x
    -> BalancedTree h f (ZonkAny 3)
    -> BinomialTree h f (x <+> ZonkAny 3)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    sz BinomialTree ('Succ h) f x
    t        (BalancedTree h f (ZonkAny 3) -> BinomialTree h f b)
    -> m (BalancedTree h f (ZonkAny 3)) -> m (BinomialTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f x -> m (f y))
    -> BalancedTree h f y
    -> Int
    -> Int
    -> m (BalancedTree h f (ZonkAny 3))
    forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
           (h :: Height) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
    unsafe_bal_adjust f x -> m (f y)
    f BalancedTree h f y
    u Int
    j Int
    i)
      | Bool
    otherwise =
        BinomialTree h f (ZonkAny 4 <+> y) -> BinomialTree h f b
    forall a b. a -> b
    unsafeCoerce (BinomialTree h f (ZonkAny 4 <+> y) -> BinomialTree h f b)
    -> (BinomialTree ('Succ h) f (ZonkAny 4)
        -> BinomialTree h f (ZonkAny 4 <+> y))
    -> BinomialTree ('Succ h) f (ZonkAny 4)
    -> BinomialTree h f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (BinomialTree ('Succ h) f (ZonkAny 4)
     -> BalancedTree h f y -> BinomialTree h f (ZonkAny 4 <+> y))
    -> BalancedTree h f y
    -> BinomialTree ('Succ h) f (ZonkAny 4)
    -> BinomialTree h f (ZonkAny 4 <+> y)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Int
    -> BinomialTree ('Succ h) f (ZonkAny 4)
    -> BalancedTree h f y
    -> BinomialTree h f (ZonkAny 4 <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    sz) BalancedTree h f y
    u (BinomialTree ('Succ h) f (ZonkAny 4) -> BinomialTree h f b)
    -> m (BinomialTree ('Succ h) f (ZonkAny 4))
    -> m (BinomialTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f x -> m (f y))
    -> BinomialTree ('Succ h) f x
    -> Int
    -> Int
    -> m (BinomialTree ('Succ h) f (ZonkAny 4))
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
           (y :: k) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
    unsafe_bin_adjust f x -> m (f y)
    f BinomialTree ('Succ h) f x
    t Int
    j (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1))
    unsafe_bin_adjust f x -> m (f y)
    f (PlusZero Int
    sz BinomialTree ('Succ h) f a
    t) Int
    j Int
    i
      | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j Int -> Int -> Int
    forall a. Bits a => a -> Int -> a
    `shiftR` (Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i) = String -> m (BinomialTree h f b)
    forall a. (?callStack::CallStack) => String -> a
    error String
    "unsafe_bin_adjust stopped at PlusZero"
      | Bool
    otherwise = Int -> BinomialTree ('Succ h) f b -> BinomialTree h f b
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    sz (BinomialTree ('Succ h) f b -> BinomialTree h f b)
    -> m (BinomialTree ('Succ h) f b) -> m (BinomialTree h f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f x -> m (f y))
    -> BinomialTree ('Succ h) f a
    -> Int
    -> Int
    -> m (BinomialTree ('Succ h) f b)
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
           (y :: k) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
    unsafe_bin_adjust f x -> m (f y)
    f BinomialTree ('Succ h) f a
    t Int
    j (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1))

    {-# SPECIALIZE unsafe_bin_adjust
         :: (f x -> Identity (f y))
         -> BinomialTree h f a
         -> Int
         -> Int
         -> Identity (BinomialTree h f b)
      #-}

    tree_zipWithM :: Applicative m
                 => (forall x . f x -> g x -> m (h x))
                 -> BinomialTree u f a
                 -> BinomialTree u g a
                 -> m (BinomialTree u h a)
    tree_zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree u f a
    -> BinomialTree u g a
    -> m (BinomialTree u h a)
    tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
    _ BinomialTree u f a
    Empty BinomialTree u g a
    Empty = BinomialTree u h a -> m (BinomialTree u h a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure BinomialTree u h a
    BinomialTree u h 'EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty
    tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
    f (PlusOne Int
    s BinomialTree ('Succ u) f x
    x1 BalancedTree u f y
    x2) (PlusOne Int
    _ BinomialTree ('Succ u) g x
    y1 BalancedTree u g y
    y2) =
      Int
    -> BinomialTree ('Succ u) h x
    -> BalancedTree u h y
    -> BinomialTree u h (x <+> y)
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (tp :: Ctx k).
    Int
    -> BinomialTree ('Succ h) f ctx
    -> BalancedTree h f tp
    -> BinomialTree h f (ctx <+> tp)
    PlusOne Int
    s (BinomialTree ('Succ u) h x
     -> BalancedTree u h y -> BinomialTree u h a)
    -> m (BinomialTree ('Succ u) h x)
    -> m (BalancedTree u h y -> BinomialTree u h a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree ('Succ u) f x
    -> BinomialTree ('Succ u) g x
    -> m (BinomialTree ('Succ u) h x)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree u f a
    -> BinomialTree u g a
    -> m (BinomialTree u h a)
    tree_zipWithM f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BinomialTree ('Succ u) f x
    x1 (BinomialTree ('Succ u) g x -> BinomialTree ('Succ u) g x
    forall a b. a -> b
    unsafeCoerce BinomialTree ('Succ u) g x
    y1)
                m (BalancedTree u h y -> BinomialTree u h a)
    -> m (BalancedTree u h y) -> m (BinomialTree u h a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree u f y
    -> BalancedTree u g y
    -> m (BalancedTree u h y)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BalancedTree u f a
    -> BalancedTree u g a
    -> m (BalancedTree u h a)
    bal_zipWithM  f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BalancedTree u f y
    x2 (BalancedTree u g y -> BalancedTree u g y
    forall a b. a -> b
    unsafeCoerce BalancedTree u g y
    y2)
    tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
    f (PlusZero Int
    s BinomialTree ('Succ u) f a
    x1) (PlusZero Int
    _ BinomialTree ('Succ u) g a
    y1) =
      Int -> BinomialTree ('Succ u) h a -> BinomialTree u h a
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
    Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
    PlusZero Int
    s (BinomialTree ('Succ u) h a -> BinomialTree u h a)
    -> m (BinomialTree ('Succ u) h a) -> m (BinomialTree u h a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree ('Succ u) f a
    -> BinomialTree ('Succ u) g a
    -> m (BinomialTree ('Succ u) h a)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree u f a
    -> BinomialTree u g a
    -> m (BinomialTree u h a)
    tree_zipWithM f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BinomialTree ('Succ u) f a
    x1 BinomialTree ('Succ u) g a
    y1
    tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
    _ BinomialTree u f a
    _ BinomialTree u g a
    _ = String -> m (BinomialTree u h a)
    forall a. (?callStack::CallStack) => String -> a
    error String
    "ilegal args to tree_zipWithM"
    {-# INLINABLE tree_zipWithM #-}

    ------------------------------------------------------------------------
    -- * Assignment

    -- | An assignment is a sequence that maps each index with type @tp@ to
    -- a value of type @f tp@.
    --
    -- This assignment implementation uses a binomial tree implementation
    -- that offers lookups and updates in time and space logarithmic with
    -- respect to the number of elements in the context.
    newtype Assignment (f :: k -> Type) (ctx :: Ctx k)
          = Assignment (BinomialTree 'Zero f ctx)

    type role Assignment nominal nominal

    instance NFData (Assignment f ctx) where
      rnf :: Assignment f ctx -> ()
    rnf Assignment f ctx
    a = Assignment f ctx -> () -> ()
    forall a b. a -> b -> b
    seq Assignment f ctx
    a ()

    -- | 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 BinomialTree 'Zero f ctx
    t) = Int -> Size ctx
    forall k (ctx :: Ctx k). Int -> Size ctx
    Size (BinomialTree 'Zero f ctx -> Int
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
    BinomialTree h f a -> Int
    tsize BinomialTree 'Zero f ctx
    t)

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

    -- | Generate an assignment
    generate :: 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
    n forall (tp :: k). Index ctx tp -> f tp
    f  = BinomialTree 'Zero f ctx -> Assignment f ctx
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment BinomialTree 'Zero f ctx
    r
      where r :: BinomialTree 'Zero f ctx
    r = Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> f tp)
    -> BinomialTree 'Zero f ctx
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> f x)
    -> BinomialTree h f t
    unsafe_bin_generate (Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    n) Int
    0 Index ctx x -> f x
    forall (tp :: k). Index ctx tp -> f tp
    f
    {-# NOINLINE generate #-}

    -- | Generate an assignment in an 'Applicative' context
    generateM :: Applicative m
              => Size ctx
              -> (forall tp . Index ctx tp -> m (f tp))
              -> m (Assignment f ctx)
    generateM :: forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
    Applicative m =>
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> m (f tp))
    -> m (Assignment f ctx)
    generateM Size ctx
    n forall (tp :: k). Index ctx tp -> m (f tp)
    f = BinomialTree 'Zero f ctx -> Assignment f ctx
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (BinomialTree 'Zero f ctx -> Assignment f ctx)
    -> m (BinomialTree 'Zero f ctx) -> m (Assignment f ctx)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int
    -> Int
    -> (forall (tp :: k). Index ctx tp -> m (f tp))
    -> m (BinomialTree 'Zero f ctx)
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
           (t :: Ctx k).
    Applicative m =>
    Int
    -> Int
    -> (forall (x :: k). Index ctx x -> m (f x))
    -> m (BinomialTree h f t)
    unsafe_bin_generateM (Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt Size ctx
    n) Int
    0 Index ctx x -> m (f x)
    forall (tp :: k). Index ctx tp -> m (f tp)
    f
    {-# NOINLINE generateM #-}

    -- | Return empty assignment
    empty :: Assignment f EmptyCtx
    empty :: forall {k} (f :: k -> *). Assignment f EmptyCtx
    empty = BinomialTree 'Zero f EmptyCtx -> Assignment f EmptyCtx
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment BinomialTree 'Zero f EmptyCtx
    forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
    Empty

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

    -- | Extend an indexed vector with a new entry.
    extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend :: forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    extend (Assignment BinomialTree 'Zero f ctx
    x) f x
    y = BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x)
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x))
    -> BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x)
    forall a b. (a -> b) -> a -> b
    $ BinomialTree 'Zero f ctx
    -> BalancedTree 'Zero f (SingleCtx x)
    -> BinomialTree 'Zero f (ctx <+> SingleCtx x)
    forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
    BinomialTree h f x
    -> BalancedTree h f y -> BinomialTree h f (x <+> y)
    append BinomialTree 'Zero f ctx
    x (f x -> BalancedTree 'Zero f (SingleCtx x)
    forall {k} (f :: k -> *) (ctx :: k).
    f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
    BalLeaf f x
    y)

    -- | Unexported index that returns an arbitrary type of expression.
    unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u
    unsafeIndex :: forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
    proxy u -> Int -> Assignment f ctx -> f u
    unsafeIndex proxy u
    _ Int
    idx (Assignment BinomialTree 'Zero f ctx
    t) = BinomialTree 'Zero f ctx -> f u -> f u
    forall a b. a -> b -> b
    seq BinomialTree 'Zero f ctx
    t (f u -> f u) -> f u -> f u
    forall a b. (a -> b) -> a -> b
    $ BinomialTree 'Zero f ctx -> Int -> Int -> f u
    forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
    BinomialTree h f a -> Int -> Int -> f u
    unsafe_bin_index BinomialTree 'Zero f ctx
    t Int
    idx Int
    0

    -- | Return value of assignment.
    (!) :: Assignment f ctx -> Index ctx tp -> f tp
    Assignment f ctx
    a ! :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index Int
    i = Bool -> f tp -> f tp
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Int
    0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    i Bool -> Bool -> Bool
    && Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Size ctx -> Int
    forall {k} (ctx :: Ctx k). Size ctx -> Int
    sizeInt (Assignment f ctx -> Size ctx
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    size Assignment f ctx
    a)) (f tp -> f tp) -> f tp -> f tp
    forall a b. (a -> b) -> a -> b
    $
                  Proxy tp -> Int -> Assignment f ctx -> f tp
    forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
    proxy u -> Int -> Assignment f ctx -> f u
    unsafeIndex Proxy tp
    forall {k} (t :: k). Proxy t
    Proxy Int
    i Assignment f ctx
    a

    -- | 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 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)
    test (Assignment BinomialTree 'Zero f x
    x) (Assignment BinomialTree 'Zero f y
    y) = do
         Refl <- (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree 'Zero f x -> BinomialTree 'Zero f y -> Maybe (x :~: y)
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    TestEqualityFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree 'Zero f x -> BinomialTree 'Zero f y -> Maybe (x :~: y)
    testEqualityFC f x -> f y -> Maybe (x :~: y)
    forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
    test BinomialTree 'Zero f x
    x BinomialTree 'Zero f y
    y
         return Refl

    instance EqF f => EqF (Assignment f) where
      eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool
    eqF Assignment f a
    x Assignment f a
    y =
        case (Assignment f a -> AssignView f a
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f a
    x, Assignment f a -> AssignView f a
    forall {k} (f :: k -> *) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f a
    y) of
          (AssignView f a
    AssignEmpty, AssignView f a
    AssignEmpty) ->
            Bool
    True
          (AssignExtend Assignment f ctx
    ctx1 f tp
    x1, AssignExtend Assignment f ctx
    ctx2 f tp
    x2) ->
            Assignment f ctx -> Assignment f ctx -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool
    eqF Assignment f ctx
    ctx1 Assignment f ctx
    Assignment f ctx
    ctx2 Bool -> Bool -> Bool
    && f tp -> f tp -> Bool
    forall (a :: k). f a -> f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF f tp
    x1 f tp
    f tp
    x2

    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 = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (a :: Ctx k) (b :: Ctx k).
       Assignment f a -> Assignment f b -> Maybe (a :~: b)
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    TestEqualityFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
    -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
    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 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

    instance TestEquality f => Eq (Assignment f ctx) where
      Assignment f ctx
    x == :: Assignment f ctx -> Assignment f ctx -> Bool
    == Assignment f ctx
    y = Maybe (ctx :~: ctx) -> Bool
    forall a. Maybe a -> Bool
    isJust (Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Ctx k) (b :: Ctx k).
    Assignment f a -> Assignment f b -> Maybe (a :~: b)
    testEquality Assignment f ctx
    x Assignment f ctx
    y)

    instance 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
    test (Assignment BinomialTree 'Zero f x
    x) (Assignment BinomialTree 'Zero f y
    y) =
         OrderingF x y -> ((x ~ y) => OrderingF x y) -> OrderingF x y
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF ((forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree 'Zero f x -> BinomialTree 'Zero f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    forall (f :: k -> *).
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: Ctx k) (y :: Ctx k).
       BinomialTree 'Zero f x -> BinomialTree 'Zero f y -> OrderingF x y
    compareFC f x -> f y -> OrderingF x y
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    test BinomialTree 'Zero f x
    x BinomialTree 'Zero f y
    y) (((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

    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)
    -> forall (x :: Ctx k) (y :: Ctx k).
       Assignment f x -> Assignment f y -> OrderingF x y
    forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
    OrdFC t =>
    (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
    -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
    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 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 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 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 f, TestEquality f) => Hashable (Assignment f ctx) where
      hashWithSalt :: Int -> Assignment f ctx -> Int
    hashWithSalt Int
    s (Assignment BinomialTree 'Zero f ctx
    a) = Int -> BinomialTree 'Zero f ctx -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    forall (tp :: Ctx k). Int -> BinomialTree 'Zero f tp -> Int
    hashWithSaltF Int
    s BinomialTree 'Zero f ctx
    a

    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 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]
    Prelude.++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((forall (x :: k). f x -> String)
    -> forall (x :: Ctx k). Assignment f x -> [String]
    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 -> String
    forall (x :: k). f x -> String
    forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
    showF Assignment f ctx
    a) String -> ShowS
    forall a. [a] -> [a] -> [a]
    Prelude.++ String
    "]"

    instance ShowF f => ShowF (Assignment f)

    {-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
    adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
    adjust :: forall {k} (f :: k -> *) (tp :: k) (ctx :: Ctx 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 -> *) (tp :: k) (ctx :: Ctx 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 :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
    update :: forall {k} (ctx :: Ctx k) (tp :: k) (f :: 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 -> *) (tp :: k) (ctx :: Ctx 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

    -- | Modify the value of an assignment at a particular index.
    adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
    adjustM :: forall {k} (m :: * -> *) (f :: k -> *) (tp :: k) (ctx :: Ctx 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 (Index Int
    i) (Assignment BinomialTree 'Zero f ctx
    a) = BinomialTree 'Zero f ctx -> Assignment f ctx
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (BinomialTree 'Zero f ctx -> Assignment f ctx)
    -> m (BinomialTree 'Zero f ctx) -> m (Assignment f ctx)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((f tp -> m (f tp))
    -> BinomialTree 'Zero f ctx
    -> Int
    -> Int
    -> m (BinomialTree 'Zero f ctx)
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
           (y :: k) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
    unsafe_bin_adjust f tp -> m (f tp)
    f BinomialTree 'Zero f ctx
    a Int
    i Int
    0)
    {-# SPECIALIZE adjustM :: (f tp -> Identity (f tp)) -> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx) #-}

    type instance IndexF       (Assignment f ctx) = Index ctx
    type instance IxValueF     (Assignment f ctx) = f

    instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) 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 -> *) (tp :: k) (ctx :: Ctx 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 :: forall (x :: k).
    IndexF (Assignment f ctx) x
    -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
    ixF IndexF (Assignment f ctx) x
    idx = IndexF (Assignment f ctx) x
    -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
    forall (x :: k).
    IndexF (Assignment f ctx) x
    -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
    forall k m (x :: k).
    IxedF' k m =>
    IndexF m x -> Lens' m (IxValueF m x)
    ixF' IndexF (Assignment f ctx) x
    idx

    -- This is an unsafe version of update that changes the type of the expression.
    unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
    unsafeUpdate :: forall {k} (f :: k -> *) (ctx :: Ctx k) (u :: k) (ctx' :: Ctx k).
    Int -> Assignment f ctx -> f u -> Assignment f ctx'
    unsafeUpdate Int
    i (Assignment BinomialTree 'Zero f ctx
    a) f u
    e = BinomialTree 'Zero f ctx' -> Assignment f ctx'
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (Identity (BinomialTree 'Zero f ctx') -> BinomialTree 'Zero f ctx'
    forall a. Identity a -> a
    runIdentity ((f (ZonkAny 5) -> Identity (f u))
    -> BinomialTree 'Zero f ctx
    -> Int
    -> Int
    -> Identity (BinomialTree 'Zero f ctx')
    forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
           (y :: k) (a :: Ctx k) (b :: Ctx k).
    Functor m =>
    (f x -> m (f y))
    -> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
    unsafe_bin_adjust (\f (ZonkAny 5)
    _ -> f u -> Identity (f u)
    forall a. a -> Identity a
    Identity f u
    e) BinomialTree 'Zero f ctx
    a Int
    i Int
    0))

    -- | Represent an assignment as either empty or an assignment with one appended.
    data AssignView f ctx where
      AssignEmpty :: AssignView f EmptyCtx
      AssignExtend :: Assignment f ctx
                   -> f tp
                   -> AssignView f (ctx::>tp)

    -- | View an assignment as either empty or an assignment with one appended.
    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 BinomialTree 'Zero f ctx
    x) =
      case BinomialTree 'Zero f ctx -> DropResult f ctx
    forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
    BinomialTree h f ctx -> DropResult f ctx
    bin_drop BinomialTree 'Zero f ctx
    x of
        DropResult f ctx
    DropEmpty -> AssignView f ctx
    AssignView f 'EmptyCtx
    forall {k} (f :: k -> *). AssignView f EmptyCtx
    AssignEmpty
        DropExt BinomialTree 'Zero f x
    t f y
    v -> Assignment f x -> f y -> AssignView f (x '::> y)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
    AssignExtend (BinomialTree 'Zero f x -> Assignment f x
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment BinomialTree 'Zero f x
    t) f y
    v

    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 (x :: k). f x -> g x -> Identity (h x))
    -> Assignment f a -> Assignment g a -> Identity (Assignment h a)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> Assignment f a -> Assignment g a -> m (Assignment h a)
    zipWithM (\f x
    u g x
    v -> h x -> Identity (h x)
    forall a. a -> Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (f x -> g x -> h x
    forall (x :: k). f x -> g x -> h x
    f f x
    u g x
    v)) Assignment f a
    x Assignment g a
    y
    {-# INLINE zipWith #-}

    zipWithM :: Applicative m
             => (forall x . f x -> g x -> m (h x))
             -> Assignment f a
             -> Assignment g a
             -> m (Assignment h a)
    zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> Assignment f a -> Assignment g a -> m (Assignment h a)
    zipWithM forall (x :: k). f x -> g x -> m (h x)
    f (Assignment BinomialTree 'Zero f a
    x) (Assignment BinomialTree 'Zero g a
    y) = BinomialTree 'Zero h a -> Assignment h a
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (BinomialTree 'Zero h a -> Assignment h a)
    -> m (BinomialTree 'Zero h a) -> m (Assignment h a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree 'Zero f a
    -> BinomialTree 'Zero g a
    -> m (BinomialTree 'Zero h a)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (u :: Height) (a :: Ctx k).
    Applicative m =>
    (forall (x :: k). f x -> g x -> m (h x))
    -> BinomialTree u f a
    -> BinomialTree u g a
    -> m (BinomialTree u h a)
    tree_zipWithM f x -> g x -> m (h x)
    forall (x :: k). f x -> g x -> m (h x)
    f BinomialTree 'Zero f a
    x BinomialTree 'Zero g a
    y
    {-# INLINABLE zipWithM #-}

    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
    f (Assignment BinomialTree 'Zero f x
    x) -> BinomialTree 'Zero g x -> Assignment g x
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment ((forall (x :: k). f x -> g x)
    -> BinomialTree 'Zero f x -> BinomialTree 'Zero g x
    forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
    (forall (tp :: k). f tp -> g tp)
    -> BinomialTree h f c -> BinomialTree h g c
    fmap_bin f tp -> g tp
    forall (x :: k). f x -> g x
    f BinomialTree 'Zero f x
    x)
      {-# INLINE fmapFC #-}

    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
      {-# INLINE foldMapFC #-}

    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 (Assignment BinomialTree 'Zero f x
    x) -> BinomialTree 'Zero g x -> Assignment g x
    forall k (f :: k -> *) (ctx :: Ctx k).
    BinomialTree 'Zero f ctx -> Assignment f ctx
    Assignment (BinomialTree 'Zero g x -> Assignment g x)
    -> m (BinomialTree 'Zero g x) -> m (Assignment g x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (x :: k). f x -> m (g x))
    -> BinomialTree 'Zero f x -> m (BinomialTree 'Zero g x)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
           (c :: Ctx k).
    Applicative m =>
    (forall (tp :: k). f tp -> m (g tp))
    -> BinomialTree h f c -> m (BinomialTree h g c)
    traverse_bin f tp -> m (g tp)
    forall (x :: k). f x -> m (g x)
    f BinomialTree 'Zero f x
    x
      {-# INLINE traverseFC #-}

    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

    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} (m :: * -> *) (ctx :: Ctx k) (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)

    ------------------------------------------------------------------------
    -- Appending

    appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
    appendBal :: forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
    appendBal Assignment f x
    x (BalLeaf f x
    a) = Assignment f x
    x Assignment f x -> f x -> Assignment f (x ::> x)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    `extend` f x
    a
    appendBal Assignment f x
    x (BalPair BalancedTree h f x
    y BalancedTree h f y
    z) =
      case Assignment f x
    -> BalancedTree h f x
    -> BalancedTree h f y
    -> (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
    forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
           (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
    p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
    assoc Assignment f x
    x BalancedTree h f x
    y BalancedTree h f y
    z of
        (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
    Refl -> Assignment f x
    x Assignment f x -> BalancedTree h f x -> Assignment f (x <+> x)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
    `appendBal` BalancedTree h f x
    y Assignment f (x <+> x)
    -> BalancedTree h f y -> Assignment f ((x <+> x) <+> y)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
    `appendBal` BalancedTree h f y
    z

    appendBin :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
    appendBin :: forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
    appendBin Assignment f x
    x BinomialTree h f y
    Empty = Assignment f x
    Assignment f (x <+> y)
    x
    appendBin Assignment f x
    x (PlusOne Int
    _ BinomialTree ('Succ h) f x
    y BalancedTree h f y
    z) =
      case Assignment f x
    -> BinomialTree ('Succ h) f x
    -> BalancedTree h f y
    -> (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
    forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
           (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
    p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
    assoc Assignment f x
    x BinomialTree ('Succ h) f x
    y BalancedTree h f y
    z of
        (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
    Refl -> Assignment f x
    x Assignment f x
    -> BinomialTree ('Succ h) f x -> Assignment f (x <+> x)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
    `appendBin` BinomialTree ('Succ h) f x
    y Assignment f (x <+> x)
    -> BalancedTree h f y -> Assignment f ((x <+> x) <+> y)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
    `appendBal` BalancedTree h f y
    z
    appendBin Assignment f x
    x (PlusZero Int
    _ BinomialTree ('Succ h) f y
    y) = Assignment f x
    x Assignment f x
    -> BinomialTree ('Succ h) f y -> Assignment f (x <+> y)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
    `appendBin` BinomialTree ('Succ h) f y
    y

    (<++>) :: 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 BinomialTree 'Zero f y
    y = Assignment f x
    x Assignment f x -> BinomialTree 'Zero f y -> Assignment f (x <+> y)
    forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
    Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
    `appendBin` BinomialTree 'Zero f y
    y

    ------------------------------------------------------------------------
    -- 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 -> *) (ctx :: Ctx k) (x :: k).
    Assignment f ctx -> f x -> Assignment f (ctx ::> x)
    `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

    ------------------------------------------------------------------------
    -- Lens combinators

    unsafeLens :: Int -> Lens.Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    idx =
      (Assignment f ctx -> f tp)
    -> (Assignment f ctx -> f u -> Assignment f ctx')
    -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    Lens.lens (Proxy tp -> Int -> Assignment f ctx -> f tp
    forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
    proxy u -> Int -> Assignment f ctx -> f u
    unsafeIndex Proxy tp
    forall {k} (t :: k). Proxy t
    Proxy Int
    idx) (Int -> Assignment f ctx -> f u -> Assignment f ctx'
    forall {k} (f :: k -> *) (ctx :: Ctx k) (u :: k) (ctx' :: Ctx k).
    Int -> Assignment f ctx -> f u -> Assignment f ctx'
    unsafeUpdate Int
    idx)

    ------------------------------------------------------------------------
    -- 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 = Int -> Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    ------------------------------------------------------------------------
    -- 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 = Int -> Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int -> Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    ------------------------------------------------------------------------
    -- 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 = Int
    -> Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    ------------------------------------------------------------------------
    -- 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 = Int
    -> Lens
         (Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> Lens
         (Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> Lens
         (Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> Lens
         (Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    ------------------------------------------------------------------------
    -- 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 = Int
    -> Lens
         (Assignment5 f t x2 x3 x4 x5)
         (Assignment5 f u x2 x3 x4 x5)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> Lens
         (Assignment5 f x1 t x3 x4 x5)
         (Assignment5 f x1 u x3 x4 x5)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> Lens
         (Assignment5 f x1 x2 t x4 x5)
         (Assignment5 f x1 x2 u x4 x5)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> Lens
         (Assignment5 f x1 x2 x3 t x5)
         (Assignment5 f x1 x2 x3 u x5)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    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 = Int
    -> Lens
         (Assignment5 f x1 x2 x3 x4 t)
         (Assignment5 f x1 x2 x3 x4 u)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    4

    ------------------------------------------------------------------------
    -- 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 = Int
    -> Lens
         (Assignment6 f t x2 x3 x4 x5 x6)
         (Assignment6 f u x2 x3 x4 x5 x6)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> Lens
         (Assignment6 f x1 t x3 x4 x5 x6)
         (Assignment6 f x1 u x3 x4 x5 x6)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> Lens
         (Assignment6 f x1 x2 t x4 x5 x6)
         (Assignment6 f x1 x2 u x4 x5 x6)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> Lens
         (Assignment6 f x1 x2 x3 t x5 x6)
         (Assignment6 f x1 x2 x3 u x5 x6)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    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 = Int
    -> Lens
         (Assignment6 f x1 x2 x3 x4 t x6)
         (Assignment6 f x1 x2 x3 x4 u x6)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    4

    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 = Int
    -> Lens
         (Assignment6 f x1 x2 x3 x4 x5 t)
         (Assignment6 f x1 x2 x3 x4 x5 u)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    5

    ------------------------------------------------------------------------
    -- 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 = Int
    -> Lens
         (Assignment7 f t x2 x3 x4 x5 x6 x7)
         (Assignment7 f u x2 x3 x4 x5 x6 x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> Lens
         (Assignment7 f x1 t x3 x4 x5 x6 x7)
         (Assignment7 f x1 u x3 x4 x5 x6 x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> Lens
         (Assignment7 f x1 x2 t x4 x5 x6 x7)
         (Assignment7 f x1 x2 u x4 x5 x6 x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> Lens
         (Assignment7 f x1 x2 x3 t x5 x6 x7)
         (Assignment7 f x1 x2 x3 u x5 x6 x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    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 = Int
    -> Lens
         (Assignment7 f x1 x2 x3 x4 t x6 x7)
         (Assignment7 f x1 x2 x3 x4 u x6 x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    4

    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 = Int
    -> Lens
         (Assignment7 f x1 x2 x3 x4 x5 t x7)
         (Assignment7 f x1 x2 x3 x4 x5 u x7)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    5

    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 = Int
    -> Lens
         (Assignment7 f x1 x2 x3 x4 x5 x6 t)
         (Assignment7 f x1 x2 x3 x4 x5 x6 u)
         (f t)
         (f u)
    forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    6

    ------------------------------------------------------------------------
    -- 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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    4

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    5

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    6

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    7

    ------------------------------------------------------------------------
    -- 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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    0

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    1

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    2

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    3

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    4

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    5

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    6

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    7

    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 = Int
    -> 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
           (u :: k).
    Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
    unsafeLens Int
    8