    {-|
    Copyright  :  (C) 2013-2016, University of Twente,
                      2017     , Myrtle Software Ltd
                      2022-2025, QBayLogic B.V.
                      2024,      Alex Mason
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE QuasiQuotes #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# LANGUAGE Trustworthy #-}

    {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
    {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}

    {-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-redundant-constraints #-}

    {-# OPTIONS_HADDOCK show-extensions #-}

    module Clash.Sized.Vector
      ( -- * 'Vec'tor data type
        Vec(Nil,(:>),(:<),Cons)
        -- * Accessors
        -- ** Length information
      , length, lengthS
        -- ** Indexing
      , (!!), head, last, at
      , indices, indicesI
      , findIndex, elemIndex
        -- ** Extracting sub-vectors (slicing)
      , tail, init
      , take, takeI, drop, dropI
      , select, selectI
        -- *** Splitting
      , splitAt, splitAtI
      , unconcat, unconcatI
        -- * Construction
        -- ** Initialization
      , singleton
      , replicate, repeat
      , iterate, iterateI, generate, generateI
      , unfoldr, unfoldrI
        -- *** Initialization from a list
      , listToVecTH
        -- ** Concatenation
      , (++), (+>>), (<<+), concat, concatMap
      , shiftInAt0, shiftInAtN , shiftOutFrom0, shiftOutFromN
      , merge
        -- * Modifying vectors
      , replace
        -- ** Permutations
      , permute, backpermute, scatter, gather
        -- *** Specialized permutations
      , reverse, transpose, interleave
      , rotateLeft, rotateRight, rotateLeftS, rotateRightS
        -- * Element-wise operations
        -- ** Mapping
      , map, imap, smap
        -- ** Zipping
      , zipWith, zipWith3, zipWith4, zipWith5, zipWith6, zipWith7
      , zip, zip3, zip4, zip5, zip6, zip7
      , izipWith
        -- ** Unzipping
      , unzip, unzip3, unzip4, unzip5, unzip6, unzip7
        -- * Folding
      , foldr, foldl, foldr1, foldl1, fold
      , ifoldr, ifoldl
        -- ** Specialized folds
      , dfold, dtfold, vfold, maximum, minimum
        -- * Prefix sums (scans)
      , scanl, scanl1, scanr, scanr1, postscanl, postscanr
      , mapAccumL, mapAccumR
        -- * Stencil computations
      , stencil1d, stencil2d
      , windows1d, windows2d
        -- * Conversions
      , toList
      , fromList
      , unsafeFromList
      , bv2v
      , v2bv
        -- * Misc
      , lazyV, VCons, asNatProxy, seqV, forceV, seqVX, forceVX
        -- * Primitives
        -- ** 'Traversable' instance
      , traverse#
        -- ** 'BitPack' instance
      , concatBitVector#
      , unconcatBitVector#
      )
    where

    import Control.DeepSeq            (NFData (..))
    import qualified Control.Lens     as Lens hiding (pattern (:>), pattern (:<))
    import Data.Bits                  ((.|.), shiftL)
    import Data.Constraint            ((:-)(..), Dict (..))
    import Data.Constraint.Nat        (leZero)
    import Data.Data
      (Data (..), Constr, DataType, Fixity (..), Typeable, mkConstr, mkDataType)
    import Data.Either                (isLeft)
    #if MIN_VERSION_base(4,18,0)
    import qualified Data.Foldable1   as F1
    #endif
    import Data.Default.Class         (Default (..))
    import qualified Data.Foldable    as F
    import Data.Kind                  (Type)
    import Data.Proxy                 (Proxy (..))
    import Data.Singletons            (TyFun,Apply,type (@@))
    import GHC.TypeLits               (CmpNat, KnownNat, Nat, type (+), type (-), type (*),
                                       type (^), type (<=), natVal)
    import GHC.Base                   (Int(I#),Int#,isTrue#)
    import GHC.Generics               hiding (Fixity (..))
    import qualified GHC.Magic
    import GHC.Prim                   ((==#),(<#),(-#))
    import Language.Haskell.TH        (ExpQ)
    import Language.Haskell.TH.Syntax (Lift(..))
    #if MIN_VERSION_template_haskell(2,16,0)
    import Language.Haskell.TH.Compat
    #endif
    import Prelude                    hiding ((++), (!!), concat, concatMap, drop,
                                              foldl, foldl1, foldr, foldr1, head,
                                              init, iterate, last, length, map,
                                              repeat, replicate, reverse, scanl,
                                              scanl1, scanr, scanr1, splitAt, tail,
                                              take, unzip, unzip3, zip, zip3, zipWith,
                                              zipWith3, maximum, minimum)
    import qualified Data.String.Interpolate as I
    import qualified Prelude          as P
    import Test.QuickCheck
      (Arbitrary(arbitrary, shrink), CoArbitrary(coarbitrary))
    import Unsafe.Coerce              (unsafeCoerce)

    import Clash.Annotations.Primitive
      (Primitive(InlineYamlPrimitive), HDL(..), dontTranslate, hasBlackBox)
    import Clash.Magic (clashCompileError, clashSimulation)
    import Clash.Promoted.Nat
      (SNat (..), SNatLE (..), UNat (..), compareSNat, pow2SNat,
       snatProxy, snatToInteger, subSNat, withSNat, toUNat, natToInteger)
    #if MIN_VERSION_base(4,18,0)
    import Clash.Promoted.Nat (leToPlus)
    #endif
    import Clash.Promoted.Nat.Literals (d1)
    import Clash.Sized.Internal.BitVector (Bit, BitVector (..), split#)
    import Clash.Sized.Index          (Index)

    import Clash.Class.BitPack        (packXWith, BitPack (..))
    import Clash.XException           (ShowX (..), NFDataX (..), seqX, isX)

    {- $setup
    >>> :set -XTypeFamilies
    >>> :set -XTypeOperators
    >>> :set -XTemplateHaskell
    >>> :set -XFlexibleContexts
    >>> :set -fplugin GHC.TypeLits.Normalise
    >>> :set -fplugin GHC.TypeLits.KnownNat.Solver
    >>> :set -fplugin GHC.TypeLits.Extra.Solver
    >>> :m -Prelude
    >>> import Clash.Prelude
    >>> import qualified Clash.Sized.Vector as Vec
    -}

    #define CONS_PREC 5

    infixr CONS_PREC `Cons`
    -- | Fixed size vectors.
    --
    -- * Lists with their length encoded in their type
    -- * 'Vec'tor elements have an __ASCENDING__ subscript starting from 0 and
    --   ending at @'length' - 1@.
    data Vec :: Nat -> Type -> Type where
      Nil  :: Vec 0 a
      Cons :: a -> Vec n a -> Vec (n + 1) a

    {-# COMPLETE Nil, (:>) #-}

    -- | In many cases, this Generic instance only allows generic
    -- functions/instances over vectors of at least size 1, due to the
    -- /n-1/ in the /Rep (Vec n a)/ definition.
    --
    -- We'll have to wait for things like
    -- https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/
    -- before we can work around this limitation
    instance KnownNat n => Generic (Vec n a) where
      type Rep (Vec n a) =
        D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
          (C1 ('MetaCons "Nil" 'PrefixI 'False) U1 :+:
           C1 ('MetaCons "Cons" 'PrefixI 'False)
            (S1 ('MetaSel 'Nothing
                    'NoSourceUnpackedness
                    'NoSourceStrictness
                    'DecidedLazy)
                (Rec0 a) :*:
             S1 ('MetaSel 'Nothing
                    'NoSourceUnpackedness
                    'NoSourceStrictness
                    'DecidedLazy)
                (Rec0 (Vec (n-1) a))))
      from :: forall x. Vec n a -> Rep (Vec n a) x
    from Vec n a
    Nil         = (:+:)
      (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
      (C1
         ('MetaCons "Cons" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a)
          :*: S1
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (Rec0 (Vec (0 - 1) a))))
      x
    -> M1
         D
         ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
         (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1
          :+: C1
                ('MetaCons "Cons" 'PrefixI 'False)
                (S1
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (Rec0 a)
                 :*: S1
                       ('MetaSel
                          'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                       (Rec0 (Vec (0 - 1) a))))
         x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1 x
    -> (:+:)
         (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
         (C1
            ('MetaCons "Cons" 'PrefixI 'False)
            (S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 a)
             :*: S1
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (Rec0 (Vec (0 - 1) a))))
         x
    forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
    f p -> (:+:) f g p
    L1 (U1 x -> M1 C ('MetaCons "Nil" 'PrefixI 'False) U1 x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 U1 x
    forall k (p :: k). U1 p
    U1))
      from (Cons a
    x Vec n a
    xs) = (:+:)
      (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
      (M1
         C
         ('MetaCons "Cons" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a)
          :*: M1
                S
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (K1 R (Vec n a))))
      x
    -> M1
         D
         ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
         (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1
          :+: M1
                C
                ('MetaCons "Cons" 'PrefixI 'False)
                (S1
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (Rec0 a)
                 :*: M1
                       S
                       ('MetaSel
                          'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                       (K1 R (Vec n a))))
         x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 (M1
      C
      ('MetaCons "Cons" 'PrefixI 'False)
      (S1
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (Rec0 a)
       :*: M1
             S
             ('MetaSel
                'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
             (K1 R (Vec n a)))
      x
    -> (:+:)
         (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
         (M1
            C
            ('MetaCons "Cons" 'PrefixI 'False)
            (S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 a)
             :*: M1
                   S
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (K1 R (Vec n a))))
         x
    forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
    g p -> (:+:) f g p
    R1 ((:*:)
      (S1
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (Rec0 a))
      (M1
         S
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (K1 R (Vec n a)))
      x
    -> M1
         C
         ('MetaCons "Cons" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a)
          :*: M1
                S
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (K1 R (Vec n a)))
         x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 (K1 R a x
    -> M1
         S
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (Rec0 a)
         x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 (a -> K1 R a x
    forall k i c (p :: k). c -> K1 i c p
    K1 a
    x) M1
      S
      ('MetaSel
         'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
      (Rec0 a)
      x
    -> M1
         S
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (K1 R (Vec n a))
         x
    -> (:*:)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a))
         (M1
            S
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (K1 R (Vec n a)))
         x
    forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: K1 R (Vec n a) x
    -> M1
         S
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (K1 R (Vec n a))
         x
    forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
    M1 (Vec n a -> K1 R (Vec n a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 Vec n a
    xs))))
      to :: forall x. Rep (Vec n a) x -> Vec n a
    to (M1 (:+:)
      (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
      (C1
         ('MetaCons "Cons" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a)
          :*: S1
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (Rec0 (Vec (n - 1) a))))
      x
    g) = case SNat n -> SNat 0 -> SNatLE n 0
    forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
    compareSNat (forall (n :: Nat). KnownNat n => SNat n
    SNat @n) (forall (n :: Nat). KnownNat n => SNat n
    SNat @0) of
        SNatLE n 0
    SNatLE -> case forall (a :: Nat). (a <= 0) :- (a ~ 0)
    leZero @n of
          Sub Dict (n ~ 0)
    (n <= 0) => Dict (n ~ 0)
    Dict -> Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        SNatLE n 0
    SNatGT -> case (:+:)
      (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
      (C1
         ('MetaCons "Cons" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a)
          :*: S1
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (Rec0 (Vec (n - 1) a))))
      x
    g of
          R1 (M1 (M1 (K1 a
    p) :*: M1 (K1 Vec (n - 1) a
    q))) -> a -> Vec (n - 1) a -> Vec ((n - 1) + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    Cons a
    p Vec (n - 1) a
    q

    instance (KnownNat n, Typeable a, Data a) => Data (Vec n a) where
      gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Vec n a)
    gunfold forall b r. Data b => c (b -> r) -> c r
    k forall r. r -> c r
    z Constr
    _ = case SNat n -> SNat 0 -> SNatLE n 0
    forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
    compareSNat (forall (n :: Nat). KnownNat n => SNat n
    SNat @n) (forall (n :: Nat). KnownNat n => SNat n
    SNat @0) of
        SNatLE n 0
    SNatLE -> case forall (a :: Nat). (a <= 0) :- (a ~ 0)
    leZero @n of
          Sub Dict (n ~ 0)
    (n <= 0) => Dict (n ~ 0)
    Dict -> Vec n a -> c (Vec n a)
    forall r. r -> c r
    z Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        SNatLE n 0
    SNatGT -> c (Vec (n - 1) a -> Vec n a) -> c (Vec n a)
    forall b r. Data b => c (b -> r) -> c r
    k (c (a -> Vec (n - 1) a -> Vec n a) -> c (Vec (n - 1) a -> Vec n a)
    forall b r. Data b => c (b -> r) -> c r
    k (forall r. r -> c r
    z @(a -> Vec (n-1) a -> Vec n a) a -> Vec (n - 1) a -> Vec n a
    a -> Vec (n - 1) a -> Vec ((n - 1) + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    Cons))
      toConstr :: Vec n a -> Constr
    toConstr Vec n a
    Nil        = Constr
    cNil
      toConstr (Cons a
    _ Vec n a
    _) = Constr
    cCons
      dataTypeOf :: Vec n a -> DataType
    dataTypeOf Vec n a
    _        = DataType
    tVec

      gfoldl
        :: (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g)
        -> Vec n a
        -> c (Vec n a)
      gfoldl :: forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Vec n a -> c (Vec n a)
    gfoldl forall d b. Data d => c (d -> b) -> d -> c b
    f forall g. g -> c g
    z Vec n a
    xs = case SNat n -> SNat 0 -> SNatLE n 0
    forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
    compareSNat (forall (n :: Nat). KnownNat n => SNat n
    SNat @n) (forall (n :: Nat). KnownNat n => SNat n
    SNat @0) of
        SNatLE n 0
    SNatLE -> case forall (a :: Nat). (a <= 0) :- (a ~ 0)
    leZero @n of
                      Sub Dict (n ~ 0)
    (n <= 0) => Dict (n ~ 0)
    Dict -> Vec n a -> c (Vec n a)
    forall g. g -> c g
    z Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        SNatLE n 0
    SNatGT -> case Vec n a
    xs of
                      (a
    y :> Vec (n - 1) a
    ys) -> (forall g. g -> c g
    z @(a -> Vec (n-1) a -> Vec n a) a -> Vec (n - 1) a -> Vec n a
    a -> Vec (n - 1) a -> Vec ((n - 1) + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    (:>) c (a -> Vec (n - 1) a -> Vec n a)
    -> a -> c (Vec (n - 1) a -> Vec n a)
    forall d b. Data d => c (d -> b) -> d -> c b
    `f` a
    y c (Vec (n - 1) a -> Vec n a) -> Vec (n - 1) a -> c (Vec n a)
    forall d b. Data d => c (d -> b) -> d -> c b
    `f` Vec (n - 1) a
    ys)

    tVec :: DataType
    tVec :: DataType
    tVec = String -> [Constr] -> DataType
    mkDataType String
    "Vec" [Constr
    cNil, Constr
    cCons]

    cNil :: Constr
    cNil :: Constr
    cNil = DataType -> String -> [String] -> Fixity -> Constr
    mkConstr DataType
    tVec String
    "Nil" [] Fixity
    Prefix

    cCons :: Constr
    cCons :: Constr
    cCons = DataType -> String -> [String] -> Fixity -> Constr
    mkConstr DataType
    tVec String
    "Cons" [] Fixity
    Prefix

    instance NFData a => NFData (Vec n a) where
      rnf :: Vec n a -> ()
    rnf = (() -> a -> ()) -> () -> Vec n a -> ()
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl (\() -> a -> ()
    forall a. NFData a => a -> ()
    rnf) ()

    -- | Add an element to the head of a vector.
    --
    -- >>> 3:>4:>5:>Nil
    -- 3 :> 4 :> 5 :> Nil
    -- >>> let x = 3:>4:>5:>Nil
    -- >>> :t x
    -- x :: Num a => Vec 3 a
    --
    -- Can be used as a pattern:
    --
    -- >>> let f (x :> y :> _) = x + y
    -- >>> :t f
    -- f :: Num a => Vec ((n + 1) + 1) a -> a
    -- >>> f (3:>4:>5:>6:>7:>Nil)
    -- 7
    --
    -- Also in conjunctions with (':<'):
    --
    -- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
    -- >>> :t g
    -- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
    -- >>> g (1:>2:>3:>4:>5:>Nil)
    -- 12
    pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
    pattern $m:> :: forall {r} {a} {n :: Nat}.
    Vec (n + 1) a -> (a -> Vec n a -> r) -> ((# #) -> r) -> r
    $b:> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    (:>) x xs <- ((\Vec (n + 1) a
    ys -> (Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec (n + 1) a
    ys,Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) a
    ys)) -> (x,xs))
      where
        (:>) a
    x Vec n a
    xs = a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    Cons a
    x Vec n a
    xs

    infixr CONS_PREC :>

    instance Show a => Show (Vec n a) where
      showsPrec :: Int -> Vec n a -> ShowS
    showsPrec Int
    n = \case
        Vec n a
    Nil -> String -> ShowS
    showString String
    "Nil"
        Vec n a
    vs -> Bool -> ShowS -> ShowS
    showParen (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > CONS_PREC) (go vs)

       where
        go :: Vec m a -> ShowS
        go :: forall (m :: Nat). Vec m a -> ShowS
    go Vec m a
    Nil = String -> ShowS
    showString String
    "Nil"
        go (a
    x `Cons` Vec n a
    xs) =
            Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec (CONS_PREC + 1) x
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :> "
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n a -> ShowS
    forall (m :: Nat). Vec m a -> ShowS
    go Vec n a
    xs

    instance ShowX a => ShowX (Vec n a) where
      showsPrecX :: Int -> Vec n a -> ShowS
    showsPrecX Int
    n Vec n a
    vs =
        case Vec n a -> Either String (Vec n a)
    forall a. a -> Either String a
    isX Vec n a
    vs of
          Right Vec n a
    Nil -> String -> ShowS
    showString String
    "Nil"
          Left String
    _ -> String -> ShowS
    showString String
    "undefined"
          Either String (Vec n a)
    _ -> Bool -> ShowS -> ShowS
    showParen (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > CONS_PREC) (go vs)
       where
        go :: Vec m a -> ShowS
        go :: forall (m :: Nat). Vec m a -> ShowS
    go (Vec m a -> Either String (Vec m a)
    forall a. a -> Either String a
    isX -> Left String
    _) = String -> ShowS
    showString String
    "undefined"
        go Vec m a
    Nil = String -> ShowS
    showString String
    "Nil"
        go (a
    x `Cons` Vec n a
    xs) =
            Int -> a -> ShowS
    forall a. ShowX a => Int -> a -> ShowS
    showsPrecX (CONS_PREC + 1) x
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :> "
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n a -> ShowS
    forall (m :: Nat). Vec m a -> ShowS
    go Vec n a
    xs

    instance (KnownNat n, Eq a) => Eq (Vec n a) where
      == :: Vec n a -> Vec n a -> Bool
    (==) Vec n a
    Nil Vec n a
    _            = Bool
    True
      (==) v1 :: Vec n a
    v1@(Cons a
    _ Vec n a
    _) Vec n a
    v2 = (Bool -> Bool -> Bool) -> Vec (n + 1) Bool -> Bool
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold Bool -> Bool -> Bool
    (&&) ((a -> a -> Bool) -> Vec n a -> Vec n a -> Vec n Bool
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Vec n a
    v1 Vec n a
    v2)

    instance (KnownNat n, Ord a) => Ord (Vec n a) where
      compare :: Vec n a -> Vec n a -> Ordering
    compare Vec n a
    x Vec n a
    y = (Ordering -> Ordering -> Ordering)
    -> Ordering -> Vec n Ordering -> Ordering
    forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr Ordering -> Ordering -> Ordering
    f Ordering
    EQ (Vec n Ordering -> Ordering) -> Vec n Ordering -> Ordering
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> Ordering) -> Vec n a -> Vec n a -> Vec n Ordering
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Vec n a
    x Vec n a
    y
        where f :: Ordering -> Ordering -> Ordering
    f Ordering
    EQ   Ordering
    keepGoing = Ordering
    keepGoing
              f Ordering
    done Ordering
    _         = Ordering
    done

    instance (KnownNat n, Semigroup a) => Semigroup (Vec n a) where
      <> :: Vec n a -> Vec n a -> Vec n a
    (<>) = (a -> a -> a) -> Vec n a -> Vec n a -> Vec n a
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> a -> a
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance (KnownNat n, Monoid a) => Monoid (Vec n a) where
      mempty :: Vec n a
    mempty = a -> Vec n a
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat a
    forall a. Monoid a => a
    mempty
      mappend :: Vec n a -> Vec n a -> Vec n a
    mappend = Vec n a -> Vec n a -> Vec n a
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance KnownNat n => Applicative (Vec n) where
      pure :: forall a. a -> Vec n a
    pure      = a -> Vec n a
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat
      Vec n (a -> b)
    fs <*> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
    <*> Vec n a
    xs = ((a -> b) -> a -> b) -> Vec n (a -> b) -> Vec n a -> Vec n b
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (a -> b) -> a -> b
    forall a b. (a -> b) -> a -> b
    ($) Vec n (a -> b)
    fs Vec n a
    xs

    {-# RULES
    "zipWith$map" forall f xs ys. zipWith (\g a -> g a) (map f xs) ys = zipWith f xs ys
      #-}

    instance KnownNat n => F.Foldable (Vec n) where
      fold :: forall m. Monoid m => Vec n m -> m
    fold Vec n m
    Nil      = m
    forall a. Monoid a => a
    mempty
      fold z :: Vec n m
    z@Cons{} = (m -> m -> m) -> Vec (n + 1) m -> m
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend Vec n m
    Vec (n + 1) m
    z
      foldMap :: forall m a. Monoid m => (a -> m) -> Vec n a -> m
    foldMap a -> m
    _ Vec n a
    Nil      = m
    forall a. Monoid a => a
    mempty
      foldMap a -> m
    f z :: Vec n a
    z@Cons{} = (m -> m -> m) -> Vec (n + 1) m -> m
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend ((a -> m) -> Vec n a -> Vec n m
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> m
    f Vec n a
    z)
      foldr :: forall a b. (a -> b -> b) -> b -> Vec n a -> b
    foldr     = (a -> b -> b) -> b -> Vec n a -> b
    forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr
      foldl :: forall b a. (b -> a -> b) -> b -> Vec n a -> b
    foldl     = (b -> a -> b) -> b -> Vec n a -> b
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl
      foldr1 :: forall a. (a -> a -> a) -> Vec n a -> a
    foldr1 a -> a -> a
    _ Vec n a
    Nil      = String -> a
    forall a. HasCallStack => String -> a
    clashCompileError String
    "foldr1: empty Vec"
      foldr1 a -> a -> a
    f z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
    foldr1 a -> a -> a
    f Vec n a
    Vec (n + 1) a
    z
      foldl1 :: forall a. (a -> a -> a) -> Vec n a -> a
    foldl1 a -> a -> a
    _ Vec n a
    Nil      = String -> a
    forall a. HasCallStack => String -> a
    clashCompileError String
    "foldl1: empty Vec"
      foldl1 a -> a -> a
    f z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
    foldl1 a -> a -> a
    f Vec n a
    Vec (n + 1) a
    z
      toList :: forall a. Vec n a -> [a]
    toList    = Vec n a -> [a]
    forall (n :: Nat) a. Vec n a -> [a]
    toList
      null :: forall a. Vec n a -> Bool
    null Vec n a
    Nil  = Bool
    True
      null Vec n a
    _    = Bool
    False
      length :: forall a. Vec n a -> Int
    length    = Vec n a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length
      maximum :: forall a. Ord a => Vec n a -> a
    maximum Vec n a
    Nil      = String -> a
    forall a. HasCallStack => String -> a
    clashCompileError String
    "maximum: empty Vec"
      maximum z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold (\a
    x a
    y -> if a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    y then a
    x else a
    y) Vec n a
    Vec (n + 1) a
    z
      minimum :: forall a. Ord a => Vec n a -> a
    minimum Vec n a
    Nil      = String -> a
    forall a. HasCallStack => String -> a
    clashCompileError String
    "minimum: empty Vec"
      minimum z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold (\a
    x a
    y -> if a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    y then a
    x else a
    y) Vec n a
    Vec (n + 1) a
    z
      sum :: forall a. Num a => Vec n a -> a
    sum Vec n a
    Nil      = a
    0
      sum z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold a -> a -> a
    forall a. Num a => a -> a -> a
    (+) Vec n a
    Vec (n + 1) a
    z
      product :: forall a. Num a => Vec n a -> a
    product Vec n a
    Nil      = a
    1
      product z :: Vec n a
    z@Cons{} = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold a -> a -> a
    forall a. Num a => a -> a -> a
    (*) Vec n a
    Vec (n + 1) a
    z

    #if MIN_VERSION_base(4,18,0)
    instance (KnownNat n, 1 <= n) => F1.Foldable1 (Vec n) where
      fold1 :: forall m. Semigroup m => Vec n m -> m
    fold1         = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n m -> m)
     -> Vec n m -> m)
    -> (forall (m :: Nat). (n ~ (1 + m)) => Vec n m -> m)
    -> Vec n m
    -> m
    forall a b. (a -> b) -> a -> b
    $ (m -> m -> m) -> Vec (m + 1) m -> m
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold m -> m -> m
    forall a. Semigroup a => a -> a -> a
    (<>)
      foldMap1 :: forall m a. Semigroup m => (a -> m) -> Vec n a -> m
    foldMap1 a -> m
    f    = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> m)
     -> Vec n a -> m)
    -> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> m)
    -> Vec n a
    -> m
    forall a b. (a -> b) -> a -> b
    $ (m -> m -> m) -> Vec (m + 1) m -> m
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold m -> m -> m
    forall a. Semigroup a => a -> a -> a
    (<>) (Vec n m -> m) -> (Vec n a -> Vec n m) -> Vec n a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m) -> Vec n a -> Vec n m
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> m
    f
      maximum :: forall a. Ord a => Vec n a -> a
    maximum       = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n Vec n a -> a
    Vec (m + 1) a -> a
    forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a
    forall a (n :: Nat). Ord a => Vec (n + 1) a -> a
    maximum
      minimum :: forall a. Ord a => Vec n a -> a
    minimum       = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n Vec n a -> a
    Vec (m + 1) a -> a
    forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a
    forall a (n :: Nat). Ord a => Vec (n + 1) a -> a
    minimum
      head :: forall a. Vec n a -> a
    head          = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n Vec n a -> a
    Vec (m + 1) a -> a
    forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head
      last :: forall a. Vec n a -> a
    last          = forall (k :: Nat) (n :: Nat) r.
    (k <= n) =>
    (forall (m :: Nat). (n ~ (k + m)) => r) -> r
    leToPlus @1 @n Vec n a -> a
    Vec (m + 1) a -> a
    forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last
    #endif

    instance Functor (Vec n) where
      fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
    fmap = (a -> b) -> Vec n a -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map

    instance KnownNat n => Traversable (Vec n) where
      traverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse = (a -> f b) -> Vec n a -> f (Vec n b)
    forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse#

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE traverse# #-}
    {-# ANN traverse# hasBlackBox #-}
    traverse# :: forall a f b n . Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# :: forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# a -> f b
    _ Vec n a
    Nil           = Vec n b -> f (Vec n b)
    forall a. a -> f a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Vec n b
    Vec 0 b
    forall a. Vec 0 a
    Nil
    traverse# a -> f b
    f (a
    x `Cons` Vec n a
    xs) = b -> Vec n b -> Vec n b
    b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    Cons (b -> Vec n b -> Vec n b) -> f b -> f (Vec n b -> Vec n b)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f b
    f a
    x f (Vec n b -> Vec n b) -> f (Vec n b) -> f (Vec n b)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> (a -> f b) -> Vec n a -> f (Vec n b)
    forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# a -> f b
    f Vec n a
    xs

    instance (Default a, KnownNat n) => Default (Vec n a) where
      def :: Vec n a
    def = a -> Vec n a
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat a
    forall a. Default a => a
    def

    instance (NFDataX a, KnownNat n) => NFDataX (Vec n a) where
      deepErrorX :: HasCallStack => String -> Vec n a
    deepErrorX String
    x = a -> Vec n a
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat (String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX String
    x)

      rnfX :: Vec n a -> ()
    rnfX Vec n a
    v =
        -- foldl will fail if the spine of the vector is undefined, so we need to
        -- seqX the result of it. We need to use foldl so Clash won't treat it as
        -- a recursive function.
        () -> () -> ()
    forall a b. a -> b -> b
    seqX ((() -> a -> ()) -> () -> Vec n a -> ()
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl (\() -> a -> ()
    forall a. NFDataX a => a -> ()
    rnfX) () Vec n a
    v) ()

      hasUndefined :: Vec n a -> Bool
    hasUndefined Vec n a
    v =
        if Either String (Vec n a) -> Bool
    forall a b. Either a b -> Bool
    isLeft (Vec n a -> Either String (Vec n a)
    forall a. a -> Either String a
    isX Vec n a
    v) then Bool
    True else Vec n a -> Bool
    forall (m :: Nat) b. (NFDataX b, KnownNat m) => Vec m b -> Bool
    go Vec n a
    v
       where
        go :: forall m b . (NFDataX b, KnownNat m) => Vec m b -> Bool
        go :: forall (m :: Nat) b. (NFDataX b, KnownNat m) => Vec m b -> Bool
    go Vec m b
    Nil = Bool
    False
        go (b
    x `Cons` Vec n b
    xs) = b -> Bool
    forall a. NFDataX a => a -> Bool
    hasUndefined b
    x Bool -> Bool -> Bool
    || Vec n b -> Bool
    forall a. NFDataX a => a -> Bool
    hasUndefined Vec n b
    xs

      ensureSpine :: Vec n a -> Vec n a
    ensureSpine = (a -> a) -> Vec n a -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> a
    forall a. NFDataX a => a -> a
    ensureSpine (Vec n a -> Vec n a) -> (Vec n a -> Vec n a) -> Vec n a -> Vec n a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n a -> Vec n a
    forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
    lazyV

    {-# INLINE singleton #-}
    -- | Create a vector of one element
    --
    -- >>> singleton 5
    -- 5 :> Nil
    singleton :: a -> Vec 1 a
    singleton :: forall a. a -> Vec 1 a
    singleton = (a -> Vec 0 a -> Vec (0 + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec 0 a
    forall a. Vec 0 a
    Nil)

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE head #-}
    {-# ANN head hasBlackBox #-}
    {- | Extract the first element of a vector

    >>> head (1:>2:>3:>Nil)
    1

    #if __GLASGOW_HASKELL__ >= 910
    >>> head Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘head’, namely ‘Nil’
          In the expression: head Nil
          In an equation for ‘it’: it = head Nil
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ >= 900
    >>> head Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘head’, namely ‘Nil’
          In the expression: head Nil
          In an equation for ‘it’: it = head Nil

    #else
    >>> head Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected type: Vec (0 + 1) a
            Actual type: Vec 0 a
        • In the first argument of ‘head’, namely ‘Nil’
          In the expression: head Nil
          In an equation for ‘it’: it = head Nil

    #endif
    -}
    head :: Vec (n + 1) a -> a
    head :: forall (n :: Nat) a. Vec (n + 1) a -> a
    head (a
    x `Cons` Vec n a
    _) = a
    x

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE tail #-}
    {-# ANN tail hasBlackBox #-}
    {- | Extract the elements after the head of a vector

    >>> tail (1:>2:>3:>Nil)
    2 :> 3 :> Nil

    #if __GLASGOW_HASKELL__ >= 910
    >>> tail Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘tail’, namely ‘Nil’
          In the expression: tail Nil
          In an equation for ‘it’: it = tail Nil
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ >= 900
    >>> tail Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘tail’, namely ‘Nil’
          In the expression: tail Nil
          In an equation for ‘it’: it = tail Nil

    #else
    >>> tail Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected type: Vec (0 + 1) a
            Actual type: Vec 0 a
        • In the first argument of ‘tail’, namely ‘Nil’
          In the expression: tail Nil
          In an equation for ‘it’: it = tail Nil

    #endif
    -}
    tail :: Vec (n + 1) a -> Vec n a
    tail :: forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail (a
    _ `Cons` Vec n a
    xs) = Vec n a
    Vec n a
    xs

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE last #-}
    {-# ANN last hasBlackBox #-}
    {- | Extract the last element of a vector

    >>> last (1:>2:>3:>Nil)
    3

    #if __GLASGOW_HASKELL__ >= 910
    >>> last Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘last’, namely ‘Nil’
          In the expression: last Nil
          In an equation for ‘it’: it = last Nil
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ >= 900
    >>> last Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘last’, namely ‘Nil’
          In the expression: last Nil
          In an equation for ‘it’: it = last Nil

    #else
    >>> last Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected type: Vec (0 + 1) a
            Actual type: Vec 0 a
        • In the first argument of ‘last’, namely ‘Nil’
          In the expression: last Nil
          In an equation for ‘it’: it = last Nil

    #endif
    -}
    last :: Vec (n + 1) a -> a
    last :: forall (n :: Nat) a. Vec (n + 1) a -> a
    last (a
    x `Cons` Vec n a
    Nil)         = a
    x
    last (a
    _ `Cons` a
    y `Cons` Vec n a
    ys) = Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last (a
    y a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    ys)

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE init #-}
    {-# ANN init hasBlackBox #-}
    {- | Extract all the elements of a vector except the last element

    >>> init (1:>2:>3:>Nil)
    1 :> 2 :> Nil

    #if __GLASGOW_HASKELL__ >= 910
    >>> init Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘init’, namely ‘Nil’
          In the expression: init Nil
          In an equation for ‘it’: it = init Nil
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ >= 900
    >>> init Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘init’, namely ‘Nil’
          In the expression: init Nil
          In an equation for ‘it’: it = init Nil

    #else
    >>> init Nil
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected type: Vec (0 + 1) a
            Actual type: Vec 0 a
        • In the first argument of ‘init’, namely ‘Nil’
          In the expression: init Nil
          In an equation for ‘it’: it = init Nil

    #endif
    -}
    init :: Vec (n + 1) a -> Vec n a
    init :: forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init (a
    _ `Cons` Vec n a
    Nil)         = Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
    init (a
    x `Cons` a
    y `Cons` Vec n a
    ys) = a
    x a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init (a
    y a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    ys)

    {-# INLINE shiftInAt0 #-}
    -- | Shift in elements to the head of a vector, bumping out elements at the
    -- tail. The result is a tuple containing:
    --
    -- * The new vector
    -- * The shifted out elements
    --
    -- >>> shiftInAt0 (1 :> 2 :> 3 :> 4 :> Nil) ((-1) :> 0 :> Nil)
    -- (-1 :> 0 :> 1 :> 2 :> Nil,3 :> 4 :> Nil)
    -- >>> shiftInAt0 (1 :> Nil) ((-1) :> 0 :> Nil)
    -- (-1 :> Nil,0 :> 1 :> Nil)
    shiftInAt0 :: KnownNat n
               => Vec n a -- ^ The old vector
               -> Vec m a -- ^ The elements to shift in at the head
               -> (Vec n a, Vec m a) -- ^ (The new vector, shifted out elements)
    shiftInAt0 :: forall (n :: Nat) a (m :: Nat).
    KnownNat n =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAt0 Vec n a
    xs Vec m a
    ys = Vec (n + m) a -> (Vec n a, Vec m a)
    forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtI Vec (n + m) a
    Vec (m + n) a
    zs
      where
        zs :: Vec (m + n) a
    zs = Vec m a
    ys Vec m a -> Vec n a -> Vec (m + n) a
    forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ Vec n a
    xs

    {-# INLINE shiftInAtN #-}
    -- | Shift in element to the tail of a vector, bumping out elements at the head.
    -- The result is a tuple containing:
    --
    -- * The new vector
    -- * The shifted out elements
    --
    -- >>> shiftInAtN (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> Nil)
    -- (3 :> 4 :> 5 :> 6 :> Nil,1 :> 2 :> Nil)
    -- >>> shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)
    -- (3 :> Nil,1 :> 2 :> Nil)
    shiftInAtN :: KnownNat m
               => Vec n a -- ^ The old vector
               -> Vec m a -- ^ The elements to shift in at the tail
               -> (Vec n a,Vec m a) -- ^ (The new vector, shifted out elements)
    shiftInAtN :: forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAtN Vec n a
    xs Vec m a
    ys = (Vec n a
    zsR, Vec m a
    zsL)
      where
        zs :: Vec (n + m) a
    zs        = Vec n a
    xs Vec n a -> Vec m a -> Vec (n + m) a
    forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ Vec m a
    ys
        (Vec m a
    zsL,Vec n a
    zsR) = Vec (m + n) a -> (Vec m a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtI Vec (m + n) a
    Vec (n + m) a
    zs

    infixl 5 :<
    -- | Add an element to the tail of a vector.
    --
    -- >>> (3:>4:>5:>Nil) :< 1
    -- 3 :> 4 :> 5 :> 1 :> Nil
    -- >>> let x = (3:>4:>5:>Nil) :< 1
    -- >>> :t x
    -- x :: Num a => Vec 4 a
    --
    -- Can be used as a pattern:
    --
    -- >>> let f (_ :< y :< x) = y + x
    -- >>> :t f
    -- f :: Num a => Vec ((n + 1) + 1) a -> a
    -- >>> f (3:>4:>5:>6:>7:>Nil)
    -- 13
    --
    -- Also in conjunctions with (':>'):
    --
    -- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
    -- >>> :t g
    -- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
    -- >>> g (1:>2:>3:>4:>5:>Nil)
    -- 12
    pattern (:<) :: Vec n a -> a -> Vec (n+1) a
    pattern $m:< :: forall {r} {n :: Nat} {a}.
    Vec (n + 1) a -> (Vec n a -> a -> r) -> ((# #) -> r) -> r
    $b:< :: forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    (:<) xs x <- ((\Vec (n + 1) a
    ys -> (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) a
    ys,Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec (n + 1) a
    ys)) -> (xs,x))
      where
        (:<) Vec n a
    xs a
    x = Vec n a
    xs Vec n a -> Vec 1 a -> Vec (n + 1) a
    forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ a -> Vec 1 a
    forall a. a -> Vec 1 a
    singleton a
    x

    infixr 4 +>>
    -- | Add an element to the head of a vector, and extract all but the last
    -- element.
    --
    -- >>> 1 +>> (3:>4:>5:>Nil)
    -- 1 :> 3 :> 4 :> Nil
    -- >>> 1 +>> Nil
    -- Nil
    (+>>) :: KnownNat n => a -> Vec n a -> Vec n a
    a
    s +>> :: forall (n :: Nat) a. KnownNat n => a -> Vec n a -> Vec n a
    +>> Vec n a
    xs = (Vec n a, Vec 1 a) -> Vec n a
    forall a b. (a, b) -> a
    fst (Vec n a -> Vec 1 a -> (Vec n a, Vec 1 a)
    forall (n :: Nat) a (m :: Nat).
    KnownNat n =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAt0 Vec n a
    xs (a -> Vec 1 a
    forall a. a -> Vec 1 a
    singleton a
    s))
    {-# INLINE (+>>) #-}

    infixl 4 <<+
    -- | Add an element to the tail of a vector, and extract all but the first
    -- element.
    --
    -- >>> (3:>4:>5:>Nil) <<+ 1
    -- 4 :> 5 :> 1 :> Nil
    -- >>> Nil <<+ 1
    -- Nil
    (<<+) :: Vec n a -> a -> Vec n a
    Vec n a
    xs <<+ :: forall (n :: Nat) a. Vec n a -> a -> Vec n a
    <<+ a
    s = (Vec n a, Vec 1 a) -> Vec n a
    forall a b. (a, b) -> a
    fst (Vec n a -> Vec 1 a -> (Vec n a, Vec 1 a)
    forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAtN Vec n a
    xs (a -> Vec 1 a
    forall a. a -> Vec 1 a
    singleton a
    s))
    {-# INLINE (<<+) #-}

    -- | Shift /m/ elements out from the head of a vector, filling up the tail with
    -- 'Default' values. The result is a tuple containing:
    --
    -- * The new vector
    -- * The shifted out values
    --
    -- >>> shiftOutFrom0 d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
    -- (3 :> 4 :> 5 :> 0 :> 0 :> Nil,1 :> 2 :> Nil)
    shiftOutFrom0 :: (Default a, KnownNat m)
                  => SNat m        -- ^ @m@, the number of elements to shift out
                  -> Vec (m + n) a -- ^ The old vector
                  -> (Vec (m + n) a, Vec m a)
                  -- ^ (The new vector, shifted out elements)
    shiftOutFrom0 :: forall a (m :: Nat) (n :: Nat).
    (Default a, KnownNat m) =>
    SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
    shiftOutFrom0 SNat m
    m Vec (m + n) a
    xs = Vec (m + n) a -> Vec m a -> (Vec (m + n) a, Vec m a)
    forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAtN Vec (m + n) a
    xs (SNat m -> a -> Vec m a
    forall (n :: Nat) a. SNat n -> a -> Vec n a
    replicate SNat m
    m a
    forall a. Default a => a
    def)
    {-# INLINE shiftOutFrom0 #-}

    -- | Shift /m/ elements out from the tail of a vector, filling up the head with
    -- 'Default' values. The result is a tuple containing:
    --
    -- * The new vector
    -- * The shifted out values
    --
    -- >>> shiftOutFromN d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
    -- (0 :> 0 :> 1 :> 2 :> 3 :> Nil,4 :> 5 :> Nil)
    shiftOutFromN :: (Default a, KnownNat n)
                  => SNat m        -- ^ @m@, the number of elements to shift out
                  -> Vec (m + n) a -- ^ The old vector
                  -> (Vec (m + n) a, Vec m a)
                  -- ^ (The new vector, shifted out elements)
    shiftOutFromN :: forall a (n :: Nat) (m :: Nat).
    (Default a, KnownNat n) =>
    SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
    shiftOutFromN m :: SNat m
    m@SNat m
    SNat Vec (m + n) a
    xs = Vec (m + n) a -> Vec m a -> (Vec (m + n) a, Vec m a)
    forall (n :: Nat) a (m :: Nat).
    KnownNat n =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAt0 Vec (m + n) a
    xs (SNat m -> a -> Vec m a
    forall (n :: Nat) a. SNat n -> a -> Vec n a
    replicate SNat m
    m a
    forall a. Default a => a
    def)
    {-# INLINE shiftOutFromN #-}

    infixr 5 ++
    -- | Append two vectors.
    --
    -- >>> (1:>2:>3:>Nil) ++ (7:>8:>Nil)
    -- 1 :> 2 :> 3 :> 7 :> 8 :> Nil
    (++) :: Vec n a -> Vec m a -> Vec (n + m) a
    Vec n a
    Nil           ++ :: forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ Vec m a
    ys = Vec m a
    Vec (n + m) a
    ys
    (a
    x `Cons` Vec n a
    xs) ++ Vec m a
    ys = a
    x a -> Vec (n + m) a -> Vec ((n + m) + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    xs Vec n a -> Vec m a -> Vec (n + m) a
    forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ Vec m a
    ys
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE (++) #-}
    {-# ANN (++) hasBlackBox #-}

    -- | Split a vector into two vectors at the given point.
    --
    -- >>> splitAt (SNat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
    -- (1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)
    -- >>> splitAt d3 (1:>2:>3:>7:>8:>Nil)
    -- (1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)
    splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt :: forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt SNat m
    n Vec (m + n) a
    xs = UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtU (SNat m -> UNat m
    forall (n :: Nat). SNat n -> UNat n
    toUNat SNat m
    n) Vec (m + n) a
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE splitAt #-}
    {-# ANN splitAt hasBlackBox #-}

    splitAtU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtU :: forall (m :: Nat) (n :: Nat) a.
    UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtU UNat m
    UZero     Vec (m + n) a
    ys            = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil,Vec n a
    Vec (m + n) a
    ys)
    splitAtU (USucc UNat n
    s) (a
    y `Cons` Vec n a
    ys) = let (Vec n a
    as,Vec n a
    bs) = UNat n -> Vec (n + n) a -> (Vec n a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtU UNat n
    s Vec n a
    Vec (n + n) a
    ys
                                       in  (a
    y a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, Vec n a
    bs)

    -- | Split a vector into two vectors where the length of the two is determined
    -- by the context.
    --
    -- >>> splitAtI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
    -- (1 :> 2 :> Nil,3 :> 7 :> 8 :> Nil)
    splitAtI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtI :: forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtI = (SNat m -> Vec (m + n) a -> (Vec m a, Vec n a))
    -> Vec (m + n) a -> (Vec m a, Vec n a)
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt
    {-# INLINE splitAtI #-}

    -- | Concatenate a vector of vectors.
    --
    -- >>> concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
    -- 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil
    concat :: Vec n (Vec m a) -> Vec (n * m) a
    concat :: forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
    concat Vec n (Vec m a)
    Nil           = Vec 0 a
    Vec (n * m) a
    forall a. Vec 0 a
    Nil
    concat (Vec m a
    x `Cons` Vec n (Vec m a)
    xs) = Vec m a
    x Vec m a -> Vec (n * m) a -> Vec (m + (n * m)) a
    forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
    ++ Vec n (Vec m a) -> Vec (n * m) a
    forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
    concat Vec n (Vec m a)
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE concat #-}
    {-# ANN concat hasBlackBox #-}

    -- | Map a function over all the elements of a vector and concatentate the resulting vectors.
    --
    -- >>> concatMap (replicate d3) (1:>2:>3:>Nil)
    -- 1 :> 1 :> 1 :> 2 :> 2 :> 2 :> 3 :> 3 :> 3 :> Nil
    concatMap :: (a -> Vec m b) -> Vec n a -> Vec (n * m) b
    concatMap :: forall a (m :: Nat) b (n :: Nat).
    (a -> Vec m b) -> Vec n a -> Vec (n * m) b
    concatMap a -> Vec m b
    f Vec n a
    xs = Vec n (Vec m b) -> Vec (n * m) b
    forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
    concat ((a -> Vec m b) -> Vec n a -> Vec n (Vec m b)
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> Vec m b
    f Vec n a
    xs)
    {-# INLINE concatMap #-}

    -- | Split a vector of \(n * m)\ elements into a vector of \"vectors of length
    -- /m/\", where the length /m/ is given.
    --
    -- >>> unconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
    -- (1 :> 2 :> 3 :> 4 :> Nil) :> (5 :> 6 :> 7 :> 8 :> Nil) :> (9 :> 10 :> 11 :> 12 :> Nil) :> Nil
    unconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcat :: forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    SNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcat SNat m
    n Vec (n * m) a
    xs = UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    forall (n :: Nat) (m :: Nat) a.
    UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcatU ((SNat n -> UNat n) -> UNat n
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat n -> UNat n
    forall (n :: Nat). SNat n -> UNat n
    toUNat) (SNat m -> UNat m
    forall (n :: Nat). SNat n -> UNat n
    toUNat SNat m
    n) Vec (n * m) a
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE unconcat #-}
    {-# ANN unconcat hasBlackBox #-}

    unconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcatU :: forall (n :: Nat) (m :: Nat) a.
    UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcatU UNat n
    UZero      UNat m
    _ Vec (n * m) a
    _  = Vec n (Vec m a)
    Vec 0 (Vec m a)
    forall a. Vec 0 a
    Nil
    unconcatU (USucc UNat n
    n') UNat m
    m Vec (n * m) a
    ys = let (Vec m a
    as,Vec (n * m) a
    bs) = UNat m -> Vec (m + (n * m)) a -> (Vec m a, Vec (n * m) a)
    forall (m :: Nat) (n :: Nat) a.
    UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAtU UNat m
    m Vec (m + (n * m)) a
    Vec (n * m) a
    ys
                                in  Vec m a
    as Vec m a -> Vec n (Vec m a) -> Vec (n + 1) (Vec m a)
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    forall (n :: Nat) (m :: Nat) a.
    UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcatU UNat n
    n' UNat m
    m Vec (n * m) a
    bs

    -- | Split a vector of /(n * m)/ elements into a vector of \"vectors of length
    -- /m/\", where the length /m/ is determined by the context.
    --
    -- >>> unconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
    -- (1 :> 2 :> 3 :> 4 :> 5 :> 6 :> Nil) :> (7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil) :> Nil
    unconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
    unconcatI :: forall (n :: Nat) (m :: Nat) a.
    (KnownNat n, KnownNat m) =>
    Vec (n * m) a -> Vec n (Vec m a)
    unconcatI = (SNat m -> Vec (n * m) a -> Vec n (Vec m a))
    -> Vec (n * m) a -> Vec n (Vec m a)
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat m -> Vec (n * m) a -> Vec n (Vec m a)
    forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    SNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcat
    {-# INLINE unconcatI #-}

    -- | Merge two vectors, alternating their elements, i.e.,
    --
    -- >>> merge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
    -- 1 :> 5 :> 2 :> 6 :> 3 :> 7 :> 4 :> 8 :> Nil
    merge :: KnownNat n => Vec n a -> Vec n a -> Vec (2 * n) a
    merge :: forall (n :: Nat) a.
    KnownNat n =>
    Vec n a -> Vec n a -> Vec (2 * n) a
    merge Vec n a
    x Vec n a
    y = Vec n (Vec 2 a) -> Vec (n * 2) a
    forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
    concat (Vec 2 (Vec n a) -> Vec n (Vec 2 a)
    forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    Vec m (Vec n a) -> Vec n (Vec m a)
    transpose (Vec n a
    x Vec n a -> Vec 1 (Vec n a) -> Vec (1 + 1) (Vec n a)
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :> Vec n a -> Vec 1 (Vec n a)
    forall a. a -> Vec 1 a
    singleton Vec n a
    y))
    {-# INLINE merge #-}

    -- | The elements in a vector in reverse order.
    --
    -- >>> reverse (1:>2:>3:>4:>Nil)
    -- 4 :> 3 :> 2 :> 1 :> Nil
    reverse :: Vec n a -> Vec n a
    reverse :: forall (n :: Nat) a. Vec n a -> Vec n a
    reverse Vec n a
    xs = Vec (n - n) a -> Vec n a -> Vec n a
    forall (i :: Nat) (n :: Nat) a.
    (i <= n) =>
    Vec (n - i) a -> Vec i a -> Vec n a
    go Vec 0 a
    Vec (n - n) a
    forall a. Vec 0 a
    Nil Vec n a
    xs
     where
      go :: i <= n => Vec (n - i) a -> Vec i a -> Vec n a
      go :: forall (i :: Nat) (n :: Nat) a.
    (i <= n) =>
    Vec (n - i) a -> Vec i a -> Vec n a
    go Vec (n - i) a
    a (a
    y `Cons` Vec n a
    ys) = Vec (n - n) a -> Vec n a -> Vec n a
    forall (i :: Nat) (n :: Nat) a.
    (i <= n) =>
    Vec (n - i) a -> Vec i a -> Vec n a
    go (a
    y a -> Vec (n - i) a -> Vec ((n - i) + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec (n - i) a
    a) Vec n a
    ys
      go Vec (n - i) a
    a Vec i a
    Nil = Vec n a
    Vec (n - i) a
    a
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE reverse #-}
    {-# ANN reverse hasBlackBox #-}

    -- | \"'map' @f xs@\" is the vector obtained by applying /f/ to each element
    -- of /xs/, i.e.,
    --
    -- > map f (x1 :> x2 :>  ... :> xn :> Nil) == (f x1 :> f x2 :> ... :> f xn :> Nil)
    --
    -- and corresponds to the following circuit layout:
    --
    -- <<doc/map.svg>>
    map :: (a -> b) -> Vec n a -> Vec n b
    map :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> b
    _ Vec n a
    Nil           = Vec n b
    Vec 0 b
    forall a. Vec 0 a
    Nil
    map a -> b
    f (a
    x `Cons` Vec n a
    xs) = a -> b
    f a
    x b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` (a -> b) -> Vec n a -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> b
    f Vec n a
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE map #-}
    {-# ANN map hasBlackBox #-}

    -- | Apply a function of every element of a vector and its index.
    --
    -- >>> :t imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
    -- imap (+) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Index 4)
    -- >>> imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
    -- 2 :> 3 :> *** Exception: X: Clash.Sized.Index: result 4 is out of bounds: [0..3]
    -- ...
    -- >>> imap (\i a -> extend (bitCoerce i) + a) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Unsigned 8)
    -- 2 :> 3 :> 4 :> 5 :> Nil
    --
    -- \"'imap' @f xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/imap.svg>>
    imap :: forall n a b . KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b
    imap :: forall (n :: Nat) a b.
    KnownNat n =>
    (Index n -> a -> b) -> Vec n a -> Vec n b
    imap Index n -> a -> b
    f = Index n -> Vec n a -> Vec n b
    forall (m :: Nat). Index n -> Vec m a -> Vec m b
    go Index n
    0
      where
        -- NOTE This has a black box called imap_go
        go :: Index n -> Vec m a -> Vec m b
        go :: forall (m :: Nat). Index n -> Vec m a -> Vec m b
    go Index n
    _ Vec m a
    Nil           = Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil
        go Index n
    n (a
    x `Cons` Vec n a
    xs) = Index n -> a -> b
    f Index n
    n a
    x b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Index n -> Vec n a -> Vec n b
    forall (m :: Nat). Index n -> Vec m a -> Vec m b
    go (Index n
    nIndex n -> Index n -> Index n
    forall a. Num a => a -> a -> a
    +Index n
    1) Vec n a
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE imap #-}
    {-# ANN imap hasBlackBox #-}

    {- | Zip two vectors with a functions that also takes the elements' indices.

    >>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)
    *** Exception: X: Clash.Sized.Index: result 2 is out of bounds: [0..1]
    ...
    >>> izipWith (\i a b -> extend (bitCoerce i) + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)
    5 :> 6 :> Nil

    \"'imap' @f xs@\" corresponds to the following circuit layout:

    <<doc/izipWith.svg>>

    __NB__: 'izipWith' is /strict/ in its second argument, and /lazy/ in its
    third. This matters when 'izipWith' is used in a recursive setting. See
    'lazyV' for more information.
    -}
    izipWith :: KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b
             -> Vec n c
    izipWith :: forall (n :: Nat) a b c.
    KnownNat n =>
    (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    izipWith Index n -> a -> b -> c
    f Vec n a
    xs Vec n b
    ys = (Index n -> (a, b) -> c) -> Vec n (a, b) -> Vec n c
    forall (n :: Nat) a b.
    KnownNat n =>
    (Index n -> a -> b) -> Vec n a -> Vec n b
    imap (\Index n
    i -> (a -> b -> c) -> (a, b) -> c
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Index n -> a -> b -> c
    f Index n
    i)) (Vec n a -> Vec n b -> Vec n (a, b)
    forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
    zip Vec n a
    xs Vec n b
    ys)
    {-# INLINE izipWith #-}

    -- | Right fold (function applied to each element and its index)
    --
    -- >>> let findLeftmost x xs = ifoldr (\i a b -> if a == x then Just i else b) Nothing xs
    -- >>> findLeftmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Just 1
    -- >>> findLeftmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Nothing
    --
    -- \"'ifoldr' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/ifoldr.svg>>
    ifoldr :: KnownNat n => (Index n -> a -> b -> b) -> b -> Vec n a -> b
    ifoldr :: forall (n :: Nat) a b.
    KnownNat n =>
    (Index n -> a -> b -> b) -> b -> Vec n a -> b
    ifoldr Index n -> a -> b -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b -> b
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec (n + 1) b
    ws
      where
        ws :: Vec (n + 1) b
    ws = (Index n -> a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
    forall (n :: Nat) a b c.
    KnownNat n =>
    (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    izipWith Index n -> a -> b -> b
    f Vec n a
    xs ((Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) b
    ws)) Vec n b -> b -> Vec (n + 1) b
    forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    :< b
    z
    {-# INLINE ifoldr #-}

    -- | Left fold (function applied to each element and its index)
    --
    -- >>> let findRightmost x xs = ifoldl (\a i b -> if b == x then Just i else a) Nothing xs
    -- >>> findRightmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Just 4
    -- >>> findRightmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Nothing
    --
    -- \"'ifoldl' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/ifoldl.svg>>
    ifoldl :: KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a
    ifoldl :: forall (n :: Nat) a b.
    KnownNat n =>
    (a -> Index n -> b -> a) -> a -> Vec n b -> a
    ifoldl a -> Index n -> b -> a
    f a
    z Vec n b
    xs = Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec (n + 1) a
    ws
      where
        ws :: Vec (n + 1) a
    ws = a
    z a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` (Index n -> b -> a -> a) -> Vec n b -> Vec n a -> Vec n a
    forall (n :: Nat) a b c.
    KnownNat n =>
    (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    izipWith (\Index n
    i b
    b a
    a -> a -> Index n -> b -> a
    f a
    a Index n
    i b
    b) Vec n b
    xs (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) a
    ws)
    {-# INLINE ifoldl #-}

    -- | Generate a vector of indices.
    --
    -- >>> indices d4
    -- 0 :> 1 :> 2 :> 3 :> Nil
    indices :: KnownNat n => SNat n -> Vec n (Index n)
    indices :: forall (n :: Nat). KnownNat n => SNat n -> Vec n (Index n)
    indices SNat n
    _ = Vec n (Index n)
    forall (n :: Nat). KnownNat n => Vec n (Index n)
    indicesI
    {-# INLINE indices #-}

    -- | Generate a vector of indices, where the length of the vector is determined
    -- by the context.
    --
    -- >>> indicesI :: Vec 4 (Index 4)
    -- 0 :> 1 :> 2 :> 3 :> Nil
    indicesI :: KnownNat n => Vec n (Index n)
    indicesI :: forall (n :: Nat). KnownNat n => Vec n (Index n)
    indicesI = (Index n -> () -> Index n) -> Vec n () -> Vec n (Index n)
    forall (n :: Nat) a b.
    KnownNat n =>
    (Index n -> a -> b) -> Vec n a -> Vec n b
    imap Index n -> () -> Index n
    forall a b. a -> b -> a
    const (() -> Vec n ()
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat ())
    {-# INLINE indicesI #-}

    -- | \"'findIndex' @p xs@\" returns the index of the /first/ element of /xs/
    -- satisfying the predicate /p/, or 'Nothing' if there is no such element.
    --
    -- >>> findIndex (> 3) (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Just 3
    -- >>> findIndex (> 8) (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Nothing
    findIndex :: KnownNat n => (a -> Bool) -> Vec n a -> Maybe (Index n)
    findIndex :: forall (n :: Nat) a.
    KnownNat n =>
    (a -> Bool) -> Vec n a -> Maybe (Index n)
    findIndex a -> Bool
    f = (Index n -> a -> Maybe (Index n) -> Maybe (Index n))
    -> Maybe (Index n) -> Vec n a -> Maybe (Index n)
    forall (n :: Nat) a b.
    KnownNat n =>
    (Index n -> a -> b -> b) -> b -> Vec n a -> b
    ifoldr (\Index n
    i a
    a Maybe (Index n)
    b -> if a -> Bool
    f a
    a then Index n -> Maybe (Index n)
    forall a. a -> Maybe a
    Just Index n
    i else Maybe (Index n)
    b) Maybe (Index n)
    forall a. Maybe a
    Nothing
    {-# INLINE findIndex #-}

    -- | \"'elemIndex' @a xs@\" returns the index of the /first/ element which is
    -- equal (by '==') to the query element /a/, or 'Nothing' if there is no such
    -- element.
    --
    -- >>> elemIndex 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Just 1
    -- >>> elemIndex 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    -- Nothing
    elemIndex :: (KnownNat n, Eq a) => a -> Vec n a -> Maybe (Index n)
    elemIndex :: forall (n :: Nat) a.
    (KnownNat n, Eq a) =>
    a -> Vec n a -> Maybe (Index n)
    elemIndex a
    x = (a -> Bool) -> Vec n a -> Maybe (Index n)
    forall (n :: Nat) a.
    KnownNat n =>
    (a -> Bool) -> Vec n a -> Maybe (Index n)
    findIndex (a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    ==)
    {-# INLINE elemIndex #-}

    -- | 'zipWith' generalizes 'zip' by zipping with the function given
    -- as the first argument, instead of a tupling function.
    -- For example, \"'zipWith' @(+)@\" applied to two vectors produces the
    -- vector of corresponding sums.
    --
    -- > zipWith f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) == (f x1 y1 :> f x2 y2 :> ... :> f xn yn :> Nil)
    --
    -- \"'zipWith' @f xs ys@\" corresponds to the following circuit layout:
    --
    -- <<doc/zipWith.svg>>
    --
    -- __NB__: 'zipWith' is /strict/ in its second argument, and /lazy/ in its
    -- third. This matters when 'zipWith' is used in a recursive setting. See
    -- 'lazyV' for more information.
    zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith :: forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> b -> c
    _ Vec n a
    Nil           Vec n b
    _  = Vec n c
    Vec 0 c
    forall a. Vec 0 a
    Nil
    zipWith a -> b -> c
    f (a
    x `Cons` Vec n a
    xs) Vec n b
    ys = a -> b -> c
    f a
    x (Vec (n + 1) b -> b
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec n b
    Vec (n + 1) b
    ys) c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> b -> c
    f Vec n a
    xs (Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec n b
    Vec (n + 1) b
    ys)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE zipWith #-}
    {-# ANN zipWith hasBlackBox #-}

    -- | 'zipWith3' generalizes 'zip3' by zipping with the function given
    -- as the first argument, instead of a tupling function.
    --
    -- > zipWith3 f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) (z1 :> z2 :> ... :> zn :> Nil) == (f x1 y1 z1 :> f x2 y2 z2 :> ... :> f xn yn zn :> Nil)
    --
    -- \"'zipWith3' @f xs ys zs@\" corresponds to the following circuit layout:
    --
    -- <<doc/zipWith3.svg>>
    --
    -- __NB__: 'zipWith3' is /strict/ in its second argument, and /lazy/ in its
    -- third and fourth. This matters when 'zipWith3' is used in a recursive setting.
    -- See 'lazyV' for more information.
    zipWith3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
    zipWith3 :: forall a b c d (n :: Nat).
    (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
    zipWith3 a -> b -> c -> d
    f Vec n a
    us Vec n b
    vs Vec n c
    ws = (a -> (b, c) -> d) -> Vec n a -> Vec n (b, c) -> Vec n d
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (\a
    a (b
    b,c
    c) -> a -> b -> c -> d
    f a
    a b
    b c
    c) Vec n a
    us (Vec n b -> Vec n c -> Vec n (b, c)
    forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
    zip Vec n b
    vs Vec n c
    ws)
    {-# INLINE zipWith3 #-}

    -- 'zipWith4' is analogous to 'zipWith3', but with four vectors.
    --
    -- __NB__: 'zipWith4' is /strict/ in its second argument, and /lazy/ its following
    -- arguments. This matters when 'zipWith4' is used in a recursive setting. See
    -- 'lazyV' for more information.
    zipWith4
      :: (a -> b -> c -> d -> e)
      -> Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
    zipWith4 :: forall a b c d e (n :: Nat).
    (a -> b -> c -> d -> e)
    -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
    zipWith4 a -> b -> c -> d -> e
    f Vec n a
    us Vec n b
    vs Vec n c
    ws Vec n d
    xs =
      (a -> (b, c, d) -> e) -> Vec n a -> Vec n (b, c, d) -> Vec n e
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (\a
    a (b
    b,c
    c,d
    d) -> a -> b -> c -> d -> e
    f a
    a b
    b c
    c d
    d) Vec n a
    us (Vec n b -> Vec n c -> Vec n d -> Vec n (b, c, d)
    forall (n :: Nat) a b c.
    Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
    zip3 Vec n b
    vs Vec n c
    ws Vec n d
    xs)
    {-# INLINE zipWith4 #-}

    -- 'zipWith5' is analogous to 'zipWith3', but with five vectors.
    --
    -- __NB__: 'zipWith5' is /strict/ in its second argument, and /lazy/ its following
    -- arguments. This matters when 'zipWith5' is used in a recursive setting. See
    -- 'lazyV' for more information.
    zipWith5
      :: (a -> b -> c -> d -> e -> f)
      -> Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
      -> Vec n f
    zipWith5 :: forall a b c d e f (n :: Nat).
    (a -> b -> c -> d -> e -> f)
    -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f
    zipWith5 a -> b -> c -> d -> e -> f
    f Vec n a
    us Vec n b
    vs Vec n c
    ws Vec n d
    xs Vec n e
    ys =
      (a -> (b, c, d, e) -> f)
    -> Vec n a -> Vec n (b, c, d, e) -> Vec n f
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (\a
    a (b
    b,c
    c,d
    d,e
    e) -> a -> b -> c -> d -> e -> f
    f a
    a b
    b c
    c d
    d e
    e) Vec n a
    us (Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (b, c, d, e)
    forall (n :: Nat) a b c d.
    Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
    zip4 Vec n b
    vs Vec n c
    ws Vec n d
    xs Vec n e
    ys)
    {-# INLINE zipWith5 #-}

    -- 'zipWith6' is analogous to 'zipWith3', but with six vectors.
    --
    -- __NB__: 'zipWith6' is /strict/ in its second argument, and /lazy/ its following
    -- arguments. This matters when 'zipWith6' is used in a recursive setting. See
    -- 'lazyV' for more information.
    zipWith6
      :: (a -> b -> c -> d -> e -> f -> g)
      -> Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
      -> Vec n f
      -> Vec n g
    zipWith6 :: forall a b c d e f g (n :: Nat).
    (a -> b -> c -> d -> e -> f -> g)
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    zipWith6 a -> b -> c -> d -> e -> f -> g
    f Vec n a
    us Vec n b
    vs Vec n c
    ws Vec n d
    xs Vec n e
    ys Vec n f
    zs =
      (a -> (b, c, d, e, f) -> g)
    -> Vec n a -> Vec n (b, c, d, e, f) -> Vec n g
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (\a
    u (b
    v,c
    w,d
    x,e
    y,f
    z) -> a -> b -> c -> d -> e -> f -> g
    f a
    u b
    v c
    w d
    x e
    y f
    z) Vec n a
    us (Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n (b, c, d, e, f)
    forall (n :: Nat) a b c d e.
    Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n (a, b, c, d, e)
    zip5 Vec n b
    vs Vec n c
    ws Vec n d
    xs Vec n e
    ys Vec n f
    zs)
    {-# INLINE zipWith6 #-}

    -- 'zipWith7' is analogous to 'zipWith3', but with seven vectors.
    --
    -- __NB__: 'zipWith7' is /strict/ in its second argument, and /lazy/ its following
    -- arguments. This matters when 'zipWith7' is used in a recursive setting. See
    -- 'lazyV' for more information.
    zipWith7
      :: (a -> b -> c -> d -> e -> f -> g -> h)
      -> Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
      -> Vec n f
      -> Vec n g
      -> Vec n h
    zipWith7 :: forall a b c d e f g h (n :: Nat).
    (a -> b -> c -> d -> e -> f -> g -> h)
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    -> Vec n h
    zipWith7 a -> b -> c -> d -> e -> f -> g -> h
    f Vec n a
    ts Vec n b
    us Vec n c
    vs Vec n d
    ws Vec n e
    xs Vec n f
    ys Vec n g
    zs =
      (a -> (b, c, d, e, f, g) -> h)
    -> Vec n a -> Vec n (b, c, d, e, f, g) -> Vec n h
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (\a
    t (b
    u,c
    v,d
    w,e
    x,f
    y,g
    z) -> a -> b -> c -> d -> e -> f -> g -> h
    f a
    t b
    u c
    v d
    w e
    x f
    y g
    z) Vec n a
    ts (Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    -> Vec n (b, c, d, e, f, g)
    forall (n :: Nat) a b c d e f.
    Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n (a, b, c, d, e, f)
    zip6 Vec n b
    us Vec n c
    vs Vec n d
    ws Vec n e
    xs Vec n f
    ys Vec n g
    zs)
    {-# INLINE zipWith7 #-}

    -- | 'foldr', applied to a binary operator, a starting value (typically
    -- the right-identity of the operator), and a vector, reduces the vector
    -- using the binary operator, from right to left:
    --
    -- > foldr f z (x1 :> ... :> xn1 :> xn :> Nil) == x1 `f` (... (xn1 `f` (xn `f` z))...)
    -- > foldr r z Nil                             == z
    --
    -- >>> foldr (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 1.875
    --
    -- \"'foldr' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/foldr.svg>>
    --
    -- __NB__: @"'foldr' f z xs"@ produces a linear structure, which has a depth, or
    -- delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
    -- associative, as @"'fold' f xs"@ produces a structure with a depth of
    -- O(log_2(@'length' xs@)).
    foldr :: (a -> b -> b) -> b -> Vec n a -> b
    foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr a -> b -> b
    _ b
    z Vec n a
    Nil           = b
    z
    foldr a -> b -> b
    f b
    z (a
    x `Cons` Vec n a
    xs) = a -> b -> b
    f a
    x ((a -> b -> b) -> b -> Vec n a -> b
    forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr a -> b -> b
    f b
    z Vec n a
    xs)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE foldr #-}
    {-# ANN foldr hasBlackBox #-}

    -- | 'foldl', applied to a binary operator, a starting value (typically
    -- the left-identity of the operator), and a vector, reduces the vector
    -- using the binary operator, from left to right:
    --
    -- > foldl f z (x1 :> x2 :> ... :> xn :> Nil) == (...((z `f` x1) `f` x2) `f`...) `f` xn
    -- > foldl f z Nil                            == z
    --
    -- >>> foldl (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 8.333333333333333e-3
    --
    -- \"'foldl' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/foldl.svg>>
    --
    -- __NB__: @"'foldl' f z xs"@ produces a linear structure, which has a depth, or
    -- delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
    -- associative, as @"'fold' f xs"@ produces a structure with a depth of
    -- O(log_2(@'length' xs@)).
    foldl :: (b -> a -> b) -> b -> Vec n a -> b
    foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl b -> a -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b -> b
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last ((b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    forall b a (n :: Nat).
    (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanl b -> a -> b
    f b
    z Vec n a
    xs)
    {-# INLINE foldl #-}

    -- | 'foldr1' is a variant of 'foldr' that has no starting value argument,
    -- and thus must be applied to non-empty vectors.
    --
    -- > foldr1 f (x1 :> ... :> xn2 :> xn1 :> xn :> Nil) == x1 `f` (... (xn2 `f` (xn1 `f` xn))...)
    -- > foldr1 f (x1 :> Nil)                            == x1
    -- > foldr1 f Nil                                    == TYPE ERROR
    --
    -- >>> foldr1 (/) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
    -- 1.875
    --
    -- \"'foldr1' @f xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/foldr1.svg>>
    --
    -- __NB__: @"'foldr1' f z xs"@ produces a linear structure, which has a depth,
    -- or delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
    -- associative, as @"'fold' f xs"@ produces a structure with a depth of
    -- O(log_2(@'length' xs@)).
    foldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
    foldr1 :: forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
    foldr1 a -> a -> a
    f Vec (n + 1) a
    xs = (a -> a -> a) -> a -> Vec n a -> a
    forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr a -> a -> a
    f (Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec (n + 1) a
    xs) (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) a
    xs)
    {-# INLINE foldr1 #-}

    -- | 'foldl1' is a variant of 'foldl' that has no starting value argument,
    -- and thus must be applied to non-empty vectors.
    --
    -- > foldl1 f (x1 :> x2 :> x3 :> ... :> xn :> Nil) == (...((x1 `f` x2) `f` x3) `f`...) `f` xn
    -- > foldl1 f (x1 :> Nil)                          == x1
    -- > foldl1 f Nil                                  == TYPE ERROR
    --
    -- >>> foldl1 (/) (1 :> 5 :> 4 :> 3 :> 2 :> Nil)
    -- 8.333333333333333e-3
    --
    -- \"'foldl1' @f xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/foldl1.svg>>
    --
    -- __NB__: @"'foldl1' f z xs"@ produces a linear structure, which has a depth,
    -- or delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
    -- associative, as @"'fold' f xs"@ produces a structure with a depth of
    -- O(log_2(@'length' xs@)).
    foldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
    foldl1 :: forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
    foldl1 a -> a -> a
    f Vec (n + 1) a
    xs = (a -> a -> a) -> a -> Vec n a -> a
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl a -> a -> a
    f (Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec (n + 1) a
    xs) (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) a
    xs)
    {-# INLINE foldl1 #-}

    -- | 'fold' is a variant of 'foldr1' and 'foldl1', but instead of reducing from
    -- right to left, or left to right, it reduces a vector using a tree-like
    -- structure. The depth, or delay, of the structure produced by
    -- \"@'fold' f xs@\", is hence @O(log_2('length' xs))@, and not
    -- @O('length' xs)@.
    --
    -- __NB__: The binary operator \"@f@\" in \"@'fold' f xs@\" must be associative.
    --
    -- > fold f (x1 :> x2 :> ... :> xn1 :> xn :> Nil) == ((x1 `f` x2) `f` ...) `f` (... `f` (xn1 `f` xn))
    -- > fold f (x1 :> Nil)                           == x1
    -- > fold f Nil                                   == TYPE ERROR
    --
    -- >>> fold (+) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
    -- 15
    --
    -- \"'fold' @f xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/fold.svg>>
    fold :: forall n a . (a -> a -> a) -> Vec (n + 1) a -> a
    fold :: forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold a -> a -> a
    f Vec (n + 1) a
    vs = [a] -> a
    fold' (Vec (n + 1) a -> [a]
    forall (n :: Nat) a. Vec n a -> [a]
    toList Vec (n + 1) a
    vs)
      where
        fold' :: [a] -> a
    fold' [a
    x] = a
    x
        fold' [a]
    xs  = [a] -> a
    fold' [a]
    ys a -> a -> a
    `f` [a] -> a
    fold' [a]
    zs
          where
            ([a]
    ys,[a]
    zs) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    P.splitAt ([a] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    P.length [a]
    xs Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    2) [a]
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE fold #-}
    {-# ANN fold (InlineYamlPrimitive [VHDL,Verilog,SystemVerilog] [I.__i|
      BlackBoxHaskell:
        name: Clash.Sized.Vector.fold
        templateFunction: Clash.Primitives.Sized.Vector.foldBBF
      |]) #-}

    -- | 'scanl' is similar to 'foldl', but returns a vector of successive reduced
    -- values from the left:
    --
    -- > scanl f z (x1 :> x2 :> ... :> Nil) == z :> (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil
    --
    -- >>> scanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 0 :> 5 :> 9 :> 12 :> 14 :> Nil
    --
    -- \"'scanl' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/scanl.svg>>
    --
    -- * __NB__:
    --
    --     > last (scanl f z xs) == foldl f z xs
    --
    -- * For a different trade-off between circuit size and logic depth for
    -- associative operators, see "Clash.Sized.RTree#scans"
    scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanl :: forall b a (n :: Nat).
    (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanl b -> a -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b
    ws
      where
        ws :: Vec (n + 1) b
    ws = b
    z b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` (a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith ((b -> a -> b) -> a -> b -> b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip b -> a -> b
    f) Vec n a
    xs (Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) b
    ws)
    {-# INLINE scanl #-}

    -- | 'scanl' with no seed value
    --
    -- >>> scanl1 (-) (1 :> 2 :> 3 :> 4 :> Nil)
    -- 1 :> -1 :> -4 :> -8 :> Nil
    scanl1 :: KnownNat n => (a -> a -> a) -> Vec (n+1) a -> Vec (n+1) a
    scanl1 :: forall (n :: Nat) a.
    KnownNat n =>
    (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a
    scanl1 a -> a -> a
    op (a
    v:>Vec n a
    vs) = (a -> a -> a) -> a -> Vec n a -> Vec (n + 1) a
    forall b a (n :: Nat).
    (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanl a -> a -> a
    op a
    v Vec n a
    vs
    {-# INLINE scanl1 #-}

    -- | 'scanr' with no seed value
    --
    -- >>> scanr1 (-) (1 :> 2 :> 3 :> 4 :> Nil)
    -- -2 :> 3 :> -1 :> 4 :> Nil
    scanr1 :: KnownNat n => (a -> a -> a) -> Vec (n+1) a -> Vec (n+1) a
    scanr1 :: forall (n :: Nat) a.
    KnownNat n =>
    (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a
    scanr1 a -> a -> a
    op Vec (n + 1) a
    vs = (a -> a -> a) -> a -> Vec n a -> Vec (n + 1) a
    forall a b (n :: Nat).
    (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanr a -> a -> a
    op (Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec (n + 1) a
    vs) (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) a
    vs)
    {-# INLINE scanr1 #-}

    -- | 'postscanl' is a variant of 'scanl' where the first result is dropped:
    --
    -- > postscanl f z (x1 :> x2 :> ... :> Nil) == (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil
    --
    -- >>> postscanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 5 :> 9 :> 12 :> 14 :> Nil
    --
    -- \"'postscanl' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/sscanl.svg>>
    postscanl :: (b -> a -> b) -> b -> Vec n a -> Vec n b
    postscanl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> Vec n b
    postscanl b -> a -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail ((b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    forall b a (n :: Nat).
    (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanl b -> a -> b
    f b
    z Vec n a
    xs)
    {-# INLINE postscanl #-}

    -- | 'scanr' is similar to 'foldr', but returns a vector of successive reduced
    -- values from the right:
    --
    -- > scanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> z :> Nil
    --
    -- >>> scanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 14 :> 9 :> 5 :> 2 :> 0 :> Nil
    --
    -- \"'scanr' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/scanr.svg>>
    --
    -- * __NB__:
    --
    --     > head (scanr f z xs) == foldr f z xs
    --
    -- * For a different trade-off between circuit size and logic depth for
    -- associative operators, see "Clash.Sized.RTree#scans"
    scanr :: (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanr :: forall a b (n :: Nat).
    (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanr a -> b -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b
    ws
      where
        ws :: Vec (n + 1) b
    ws = (a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith a -> b -> b
    f Vec n a
    xs ((Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) b
    ws)) Vec n b -> b -> Vec (n + 1) b
    forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    :< b
    z
    {-# INLINE scanr #-}

    -- | 'postscanr' is a variant of 'scanr' that where the last result is dropped:
    --
    -- > postscanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> Nil
    --
    -- >>> postscanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    -- 14 :> 9 :> 5 :> 2 :> Nil
    --
    -- \"'postscanr' @f z xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/sscanr.svg>>
    postscanr :: (a -> b -> b) -> b -> Vec n a -> Vec n b
    postscanr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> Vec n b
    postscanr a -> b -> b
    f b
    z Vec n a
    xs = Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init ((a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
    forall a b (n :: Nat).
    (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
    scanr a -> b -> b
    f b
    z Vec n a
    xs)
    {-# INLINE postscanr #-}

    -- | The 'mapAccumL' function behaves like a combination of 'map' and 'foldl';
    -- it applies a function to each element of a vector, passing an accumulating
    -- parameter from left to right, and returning a final value of this accumulator
    -- together with the new vector.
    --
    -- >>> mapAccumL (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
    -- (10,1 :> 2 :> 4 :> 7 :> Nil)
    --
    -- \"'mapAccumL' @f acc xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/mapAccumL.svg>>
    mapAccumL :: (acc -> x -> (acc,y)) -> acc -> Vec n x -> (acc,Vec n y)
    mapAccumL :: forall acc x y (n :: Nat).
    (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
    mapAccumL acc -> x -> (acc, y)
    f acc
    acc Vec n x
    xs = (acc
    acc',Vec n y
    ys)
      where
        accs :: Vec (n + 1) acc
    accs        = acc
    acc acc -> Vec n acc -> Vec (n + 1) acc
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n acc
    accs'
        ws :: Vec n (acc, y)
    ws          = (x -> acc -> (acc, y)) -> Vec n x -> Vec n acc -> Vec n (acc, y)
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith ((acc -> x -> (acc, y)) -> x -> acc -> (acc, y)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip acc -> x -> (acc, y)
    f) Vec n x
    xs (Vec (n + 1) acc -> Vec n acc
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec (n + 1) acc
    accs)
        (Vec n acc
    accs', Vec n y
    ys) = Vec n (acc, y) -> (Vec n acc, Vec n y)
    forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzip Vec n (acc, y)
    ws
        acc' :: acc
    acc'        = Vec (n + 1) acc -> acc
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec (n + 1) acc
    accs
    {-# INLINE mapAccumL #-}

    -- | The 'mapAccumR' function behaves like a combination of 'map' and 'foldr';
    -- it applies a function to each element of a vector, passing an accumulating
    -- parameter from right to left, and returning a final value of this accumulator
    -- together with the new vector.
    --
    -- >>> mapAccumR (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
    -- (10,10 :> 8 :> 5 :> 1 :> Nil)
    --
    -- \"'mapAccumR' @f acc xs@\" corresponds to the following circuit layout:
    --
    -- <<doc/mapAccumR.svg>>
    mapAccumR :: (acc -> x -> (acc,y)) -> acc -> Vec n x -> (acc, Vec n y)
    mapAccumR :: forall acc x y (n :: Nat).
    (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
    mapAccumR acc -> x -> (acc, y)
    f acc
    acc Vec n x
    xs = (acc
    acc',Vec n y
    ys)
      where
        accs :: Vec (n + 1) acc
    accs        = Vec n acc
    accs' Vec n acc -> acc -> Vec (n + 1) acc
    forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    :< acc
    acc
        ws :: Vec n (acc, y)
    ws          = (x -> acc -> (acc, y)) -> Vec n x -> Vec n acc -> Vec n (acc, y)
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith ((acc -> x -> (acc, y)) -> x -> acc -> (acc, y)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip acc -> x -> (acc, y)
    f) Vec n x
    xs (Vec (n + 1) acc -> Vec n acc
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) acc
    accs)
        (Vec n acc
    accs', Vec n y
    ys) = Vec n (acc, y) -> (Vec n acc, Vec n y)
    forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzip Vec n (acc, y)
    ws
        acc' :: acc
    acc'        = Vec (n + 1) acc -> acc
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec (n + 1) acc
    accs
    {-# INLINE mapAccumR #-}

    -- | 'zip' takes two vectors and returns a vector of corresponding pairs.
    --
    -- >>> zip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
    -- (1,4) :> (2,3) :> (3,2) :> (4,1) :> Nil
    zip :: Vec n a -> Vec n b -> Vec n (a,b)
    zip :: forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
    zip = (a -> b -> (a, b)) -> Vec n a -> Vec n b -> Vec n (a, b)
    forall a b c (n :: Nat).
    (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
    zipWith (,)
    {-# INLINE zip #-}

    -- | 'zip3' takes three vectors and returns a vector of corresponding triplets.
    --
    -- >>> zip3 (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil) (5:>6:>7:>8:>Nil)
    -- (1,4,5) :> (2,3,6) :> (3,2,7) :> (4,1,8) :> Nil
    zip3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a,b,c)
    zip3 :: forall (n :: Nat) a b c.
    Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
    zip3 = (a -> b -> c -> (a, b, c))
    -> Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
    forall a b c d (n :: Nat).
    (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
    zipWith3 (,,)
    {-# INLINE zip3 #-}

    -- | 'zip4' takes four vectors and returns a list of quadruples, analogous
    -- to 'zip'.
    zip4 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a,b,c,d)
    zip4 :: forall (n :: Nat) a b c d.
    Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
    zip4 = (a -> b -> c -> d -> (a, b, c, d))
    -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
    forall a b c d e (n :: Nat).
    (a -> b -> c -> d -> e)
    -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
    zipWith4 (,,,)
    {-# INLINE zip4 #-}

    -- | 'zip5' takes five vectors and returns a list of five-tuples, analogous
    -- to 'zip'.
    zip5 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (a,b,c,d,e)
    zip5 :: forall (n :: Nat) a b c d e.
    Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n (a, b, c, d, e)
    zip5 = (a -> b -> c -> d -> e -> (a, b, c, d, e))
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n (a, b, c, d, e)
    forall a b c d e f (n :: Nat).
    (a -> b -> c -> d -> e -> f)
    -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f
    zipWith5 (,,,,)
    {-# INLINE zip5 #-}

    -- | 'zip6' takes six vectors and returns a list of six-tuples, analogous
    -- to 'zip'.
    zip6
      :: Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
      -> Vec n f
      -> Vec n (a,b,c,d,e,f)
    zip6 :: forall (n :: Nat) a b c d e f.
    Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n (a, b, c, d, e, f)
    zip6 = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n (a, b, c, d, e, f)
    forall a b c d e f g (n :: Nat).
    (a -> b -> c -> d -> e -> f -> g)
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    zipWith6 (,,,,,)
    {-# INLINE zip6 #-}

    -- | 'zip7' takes seven vectors and returns a list of seven-tuples, analogous
    -- to 'zip'.
    zip7
      :: Vec n a
      -> Vec n b
      -> Vec n c
      -> Vec n d
      -> Vec n e
      -> Vec n f
      -> Vec n g
      -> Vec n (a,b,c,d,e,f,g)
    zip7 :: forall (n :: Nat) a b c d e f g.
    Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    -> Vec n (a, b, c, d, e, f, g)
    zip7 = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    -> Vec n (a, b, c, d, e, f, g)
    forall a b c d e f g h (n :: Nat).
    (a -> b -> c -> d -> e -> f -> g -> h)
    -> Vec n a
    -> Vec n b
    -> Vec n c
    -> Vec n d
    -> Vec n e
    -> Vec n f
    -> Vec n g
    -> Vec n h
    zipWith7 (,,,,,,)
    {-# INLINE zip7 #-}

    -- | 'unzip' transforms a vector of pairs into a vector of first components
    -- and a vector of second components.
    --
    -- >>> unzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
    -- (1 :> 2 :> 3 :> 4 :> Nil,4 :> 3 :> 2 :> 1 :> Nil)
    unzip :: Vec n (a,b) -> (Vec n a, Vec n b)
    unzip :: forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzip Vec n (a, b)
    xs
      | Bool
    clashSimulation = Vec n (a, b) -> (Vec n a, Vec n b)
    forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzipSim Vec n (a, b)
    xs
      | Bool
    otherwise = (((a, b) -> a) -> Vec n (a, b) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (a, b) -> a
    forall a b. (a, b) -> a
    fst Vec n (a, b)
    xs, ((a, b) -> b) -> Vec n (a, b) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (a, b) -> b
    forall a b. (a, b) -> b
    snd Vec n (a, b)
    xs)
     where
      unzipSim :: Vec m (a,b) -> (Vec m a, Vec m b)
      unzipSim :: forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzipSim Vec m (a, b)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil)
      unzipSim (~(a
    a,b
    b) `Cons` Vec n (a, b)
    rest) =
        let (Vec n a
    as, Vec n b
    bs) = Vec n (a, b) -> (Vec n a, Vec n b)
    forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
    unzipSim Vec n (a, b)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs)
    {-# INLINE unzip #-}

    -- | 'unzip3' transforms a vector of triplets into a vector of first components,
    -- a vector of second components, and a vector of third components.
    --
    -- >>> unzip3 ((1,4,5):>(2,3,6):>(3,2,7):>(4,1,8):>Nil)
    -- (1 :> 2 :> 3 :> 4 :> Nil,4 :> 3 :> 2 :> 1 :> Nil,5 :> 6 :> 7 :> 8 :> Nil)
    unzip3 :: Vec n (a,b,c) -> (Vec n a, Vec n b, Vec n c)
    unzip3 :: forall (n :: Nat) a b c.
    Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    unzip3 Vec n (a, b, c)
    xs
      | Bool
    clashSimulation = Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    forall (n :: Nat) a b c.
    Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    unzip3Sim Vec n (a, b, c)
    xs
      | Bool
    otherwise = ( ((a, b, c) -> a) -> Vec n (a, b, c) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    x,b
    _,c
    _) -> a
    x) Vec n (a, b, c)
    xs
                    , ((a, b, c) -> b) -> Vec n (a, b, c) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    y,c
    _) -> b
    y) Vec n (a, b, c)
    xs
                    , ((a, b, c) -> c) -> Vec n (a, b, c) -> Vec n c
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    z) -> c
    z) Vec n (a, b, c)
    xs
                    )
     where
      unzip3Sim :: Vec m (a,b,c) -> (Vec m a, Vec m b, Vec m c)
      unzip3Sim :: forall (n :: Nat) a b c.
    Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    unzip3Sim Vec m (a, b, c)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil, Vec m c
    Vec 0 c
    forall a. Vec 0 a
    Nil)
      unzip3Sim (~(a
    a,b
    b,c
    c) `Cons` Vec n (a, b, c)
    rest) =
        let (Vec n a
    as, Vec n b
    bs, Vec n c
    cs) = Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    forall (n :: Nat) a b c.
    Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
    unzip3Sim Vec n (a, b, c)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs, c
    c c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n c
    cs)
    {-# INLINE unzip3 #-}

    -- | 'unzip4' takes a vector of quadruples and returns four vectors, analogous
    -- to 'unzip'.
    unzip4 :: Vec n (a,b,c,d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    unzip4 :: forall (n :: Nat) a b c d.
    Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    unzip4 Vec n (a, b, c, d)
    xs
      | Bool
    clashSimulation = Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    forall (n :: Nat) a b c d.
    Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    unzip4Sim Vec n (a, b, c, d)
    xs
      | Bool
    otherwise = ( ((a, b, c, d) -> a) -> Vec n (a, b, c, d) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    w,b
    _,c
    _,d
    _) -> a
    w) Vec n (a, b, c, d)
    xs
                    , ((a, b, c, d) -> b) -> Vec n (a, b, c, d) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    x,c
    _,d
    _) -> b
    x) Vec n (a, b, c, d)
    xs
                    , ((a, b, c, d) -> c) -> Vec n (a, b, c, d) -> Vec n c
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    y,d
    _) -> c
    y) Vec n (a, b, c, d)
    xs
                    , ((a, b, c, d) -> d) -> Vec n (a, b, c, d) -> Vec n d
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    z) -> d
    z) Vec n (a, b, c, d)
    xs
                    )
     where
      unzip4Sim :: Vec m (a,b,c,d) -> (Vec m a, Vec m b, Vec m c, Vec m d)
      unzip4Sim :: forall (n :: Nat) a b c d.
    Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    unzip4Sim Vec m (a, b, c, d)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil, Vec m c
    Vec 0 c
    forall a. Vec 0 a
    Nil, Vec m d
    Vec 0 d
    forall a. Vec 0 a
    Nil)
      unzip4Sim (~(a
    a,b
    b,c
    c,d
    d) `Cons` Vec n (a, b, c, d)
    rest) =
        let (Vec n a
    as, Vec n b
    bs, Vec n c
    cs, Vec n d
    ds) = Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    forall (n :: Nat) a b c d.
    Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
    unzip4Sim Vec n (a, b, c, d)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs, c
    c c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n c
    cs, d
    d d -> Vec n d -> Vec (n + 1) d
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n d
    ds)
    {-# INLINE unzip4 #-}

    -- | 'unzip5' takes a vector of five-tuples and returns five vectors, analogous
    -- to 'unzip'.
    unzip5 :: Vec n (a,b,c,d,e) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    unzip5 :: forall (n :: Nat) a b c d e.
    Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    unzip5 Vec n (a, b, c, d, e)
    xs
      | Bool
    clashSimulation = Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    forall (n :: Nat) a b c d e.
    Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    unzip5Sim Vec n (a, b, c, d, e)
    xs
      | Bool
    otherwise = ( ((a, b, c, d, e) -> a) -> Vec n (a, b, c, d, e) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    v,b
    _,c
    _,d
    _,e
    _) -> a
    v) Vec n (a, b, c, d, e)
    xs
                    , ((a, b, c, d, e) -> b) -> Vec n (a, b, c, d, e) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    w,c
    _,d
    _,e
    _) -> b
    w) Vec n (a, b, c, d, e)
    xs
                    , ((a, b, c, d, e) -> c) -> Vec n (a, b, c, d, e) -> Vec n c
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    x,d
    _,e
    _) -> c
    x) Vec n (a, b, c, d, e)
    xs
                    , ((a, b, c, d, e) -> d) -> Vec n (a, b, c, d, e) -> Vec n d
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    y,e
    _) -> d
    y) Vec n (a, b, c, d, e)
    xs
                    , ((a, b, c, d, e) -> e) -> Vec n (a, b, c, d, e) -> Vec n e
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    z) -> e
    z) Vec n (a, b, c, d, e)
    xs
                    )
     where
      unzip5Sim :: Vec m (a,b,c,d,e) -> (Vec m a, Vec m b, Vec m c, Vec m d, Vec m e)
      unzip5Sim :: forall (n :: Nat) a b c d e.
    Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    unzip5Sim Vec m (a, b, c, d, e)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil, Vec m c
    Vec 0 c
    forall a. Vec 0 a
    Nil, Vec m d
    Vec 0 d
    forall a. Vec 0 a
    Nil, Vec m e
    Vec 0 e
    forall a. Vec 0 a
    Nil)
      unzip5Sim (~(a
    a,b
    b,c
    c,d
    d,e
    e) `Cons` Vec n (a, b, c, d, e)
    rest) =
        let (Vec n a
    as, Vec n b
    bs, Vec n c
    cs, Vec n d
    ds, Vec n e
    es) = Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    forall (n :: Nat) a b c d e.
    Vec n (a, b, c, d, e)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
    unzip5Sim Vec n (a, b, c, d, e)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs, c
    c c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n c
    cs, d
    d d -> Vec n d -> Vec (n + 1) d
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n d
    ds, e
    e e -> Vec n e -> Vec (n + 1) e
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n e
    es)
    {-# INLINE unzip5 #-}

    -- | 'unzip6' takes a vector of six-tuples and returns six vectors, analogous
    -- to 'unzip'.
    unzip6
      :: Vec n (a,b,c,d,e,f)
      -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    unzip6 :: forall (n :: Nat) a b c d e f.
    Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    unzip6 Vec n (a, b, c, d, e, f)
    xs
      | Bool
    clashSimulation = Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    forall (n :: Nat) a b c d e f.
    Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    unzip6Sim Vec n (a, b, c, d, e, f)
    xs
      | Bool
    otherwise = ( ((a, b, c, d, e, f) -> a) -> Vec n (a, b, c, d, e, f) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    u,b
    _,c
    _,d
    _,e
    _,f
    _) -> a
    u) Vec n (a, b, c, d, e, f)
    xs
                    , ((a, b, c, d, e, f) -> b) -> Vec n (a, b, c, d, e, f) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    v,c
    _,d
    _,e
    _,f
    _) -> b
    v) Vec n (a, b, c, d, e, f)
    xs
                    , ((a, b, c, d, e, f) -> c) -> Vec n (a, b, c, d, e, f) -> Vec n c
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    w,d
    _,e
    _,f
    _) -> c
    w) Vec n (a, b, c, d, e, f)
    xs
                    , ((a, b, c, d, e, f) -> d) -> Vec n (a, b, c, d, e, f) -> Vec n d
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    x,e
    _,f
    _) -> d
    x) Vec n (a, b, c, d, e, f)
    xs
                    , ((a, b, c, d, e, f) -> e) -> Vec n (a, b, c, d, e, f) -> Vec n e
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    y,f
    _) -> e
    y) Vec n (a, b, c, d, e, f)
    xs
                    , ((a, b, c, d, e, f) -> f) -> Vec n (a, b, c, d, e, f) -> Vec n f
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    _,f
    z) -> f
    z) Vec n (a, b, c, d, e, f)
    xs
                    )
     where
      unzip6Sim :: Vec m (a,b,c,d,e,f) -> (Vec m a, Vec m b, Vec m c, Vec m d, Vec m e, Vec m f)
      unzip6Sim :: forall (n :: Nat) a b c d e f.
    Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    unzip6Sim Vec m (a, b, c, d, e, f)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil, Vec m c
    Vec 0 c
    forall a. Vec 0 a
    Nil, Vec m d
    Vec 0 d
    forall a. Vec 0 a
    Nil, Vec m e
    Vec 0 e
    forall a. Vec 0 a
    Nil, Vec m f
    Vec 0 f
    forall a. Vec 0 a
    Nil)
      unzip6Sim (~(a
    a,b
    b,c
    c,d
    d,e
    e,f
    f) `Cons` Vec n (a, b, c, d, e, f)
    rest) =
        let (Vec n a
    as, Vec n b
    bs, Vec n c
    cs, Vec n d
    ds, Vec n e
    es, Vec n f
    fs) = Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    forall (n :: Nat) a b c d e f.
    Vec n (a, b, c, d, e, f)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
    unzip6Sim Vec n (a, b, c, d, e, f)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs, c
    c c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n c
    cs, d
    d d -> Vec n d -> Vec (n + 1) d
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n d
    ds, e
    e e -> Vec n e -> Vec (n + 1) e
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n e
    es, f
    f f -> Vec n f -> Vec (n + 1) f
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n f
    fs)
    {-# INLINE unzip6 #-}

    -- | 'unzip7' takes a vector of seven-tuples and returns seven vectors, analogous
    -- to 'unzip'.
    unzip7
      :: Vec n (a,b,c,d,e,f,g)
      -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    unzip7 :: forall (n :: Nat) a b c d e f g.
    Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    unzip7 Vec n (a, b, c, d, e, f, g)
    xs
      | Bool
    clashSimulation = Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    forall (n :: Nat) a b c d e f g.
    Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    unzip7Sim Vec n (a, b, c, d, e, f, g)
    xs
      | Bool
    otherwise = ( ((a, b, c, d, e, f, g) -> a)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    t,b
    _,c
    _,d
    _,e
    _,f
    _,g
    _) -> a
    t) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> b)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    u,c
    _,d
    _,e
    _,f
    _,g
    _) -> b
    u) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> c)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n c
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    v,d
    _,e
    _,f
    _,g
    _) -> c
    v) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> d)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n d
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    w,e
    _,f
    _,g
    _) -> d
    w) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> e)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n e
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    x,f
    _,g
    _) -> e
    x) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> f)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n f
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    _,f
    y,g
    _) -> f
    y) Vec n (a, b, c, d, e, f, g)
    xs
                    , ((a, b, c, d, e, f, g) -> g)
    -> Vec n (a, b, c, d, e, f, g) -> Vec n g
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (\(a
    _,b
    _,c
    _,d
    _,e
    _,f
    _,g
    z) -> g
    z) Vec n (a, b, c, d, e, f, g)
    xs
                    )
     where
      unzip7Sim :: Vec m (a,b,c,d,e,f,g) -> (Vec m a, Vec m b, Vec m c, Vec m d, Vec m e, Vec m f, Vec m g)
      unzip7Sim :: forall (n :: Nat) a b c d e f g.
    Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    unzip7Sim Vec m (a, b, c, d, e, f, g)
    Nil = (Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil, Vec m b
    Vec 0 b
    forall a. Vec 0 a
    Nil, Vec m c
    Vec 0 c
    forall a. Vec 0 a
    Nil, Vec m d
    Vec 0 d
    forall a. Vec 0 a
    Nil, Vec m e
    Vec 0 e
    forall a. Vec 0 a
    Nil, Vec m f
    Vec 0 f
    forall a. Vec 0 a
    Nil, Vec m g
    Vec 0 g
    forall a. Vec 0 a
    Nil)
      unzip7Sim (~(a
    a,b
    b,c
    c,d
    d,e
    e,f
    f,g
    g) `Cons` Vec n (a, b, c, d, e, f, g)
    rest) =
        let (Vec n a
    as, Vec n b
    bs, Vec n c
    cs, Vec n d
    ds, Vec n e
    es, Vec n f
    fs, Vec n g
    gs) = Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    forall (n :: Nat) a b c d e f g.
    Vec n (a, b, c, d, e, f, g)
    -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
    unzip7Sim Vec n (a, b, c, d, e, f, g)
    rest
        in (a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n a
    as, b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    bs, c
    c c -> Vec n c -> Vec (n + 1) c
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n c
    cs, d
    d d -> Vec n d -> Vec (n + 1) d
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n d
    ds, e
    e e -> Vec n e -> Vec (n + 1) e
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n e
    es, f
    f f -> Vec n f -> Vec (n + 1) f
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n f
    fs, g
    g g -> Vec n g -> Vec (n + 1) g
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n g
    gs)
    {-# INLINE unzip7 #-}

    index_int :: KnownNat n => Vec n a -> Int -> a
    index_int :: forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a
    index_int Vec n a
    xs i :: Int
    i@(I# Int#
    n0)
      | Int# -> Bool
    isTrue# (Int#
    n0 Int# -> Int# -> Int#
    <# Int#
    0#) = String -> a
    forall a. HasCallStack => String -> a
    error String
    "Clash.Sized.Vector.(!!): negative index"
      | Bool
    otherwise          = Vec n a -> Int# -> a
    forall (m :: Nat) a. Vec m a -> Int# -> a
    sub Vec n a
    xs Int#
    n0
      where
        sub :: Vec m a -> Int# -> a
        sub :: forall (m :: Nat) a. Vec m a -> Int# -> a
    sub Vec m a
    Nil     Int#
    _ = String -> a
    forall a. HasCallStack => String -> a
    error ([String] -> String
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    P.concat [ String
    "Clash.Sized.Vector.(!!): index "
                                        , Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                        , String
    " is larger than maximum index "
                                        , Int -> String
    forall a. Show a => a -> String
    show ((Vec n a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length Vec n a
    xs)Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)
                                        ])
        sub (a
    y `Cons` (!Vec n a
    ys)) Int#
    n = if Int# -> Bool
    isTrue# (Int#
    n Int# -> Int# -> Int#
    ==# Int#
    0#)
                                    then a
    y
                                    else Vec n a -> Int# -> a
    forall (m :: Nat) a. Vec m a -> Int# -> a
    sub Vec n a
    ys (Int#
    n Int# -> Int# -> Int#
    -# Int#
    1#)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE index_int #-}
    {-# ANN index_int hasBlackBox #-}

    -- | \"@xs@ '!!' @n@\" returns the /n/'th element of /xs/.
    --
    -- __NB__: Vector elements have an __ASCENDING__ subscript starting from 0 and
    -- ending at @'length' - 1@.
    --
    -- >>> (1:>2:>3:>4:>5:>Nil) !! 4
    -- 5
    -- >>> (1:>2:>3:>4:>5:>Nil) !! (length (1:>2:>3:>4:>5:>Nil) - 1)
    -- 5
    -- >>> (1:>2:>3:>4:>5:>Nil) !! 1
    -- 2
    -- >>> (1:>2:>3:>4:>5:>Nil) !! 14
    -- *** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 4
    -- ...
    (!!) :: (KnownNat n, Enum i) => Vec n a -> i -> a
    Vec n a
    xs !! :: forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !! i
    i = Vec n a -> Int -> a
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a
    index_int Vec n a
    xs (i -> Int
    forall a. Enum a => a -> Int
    fromEnum i
    i)
    {-# INLINE (!!) #-}

    -- | The length of a 'Vec'tor as an 'Int' value.
    --
    -- >>> length (6 :> 7 :> 8 :> Nil)
    -- 3
    length :: KnownNat n => Vec n a -> Int
    length :: forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int) -> (Vec n a -> Integer) -> Vec n a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n -> Integer) -> (Vec n a -> Proxy n) -> Vec n a -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n a -> Proxy n
    forall (n :: Nat) a. Vec n a -> Proxy n
    asNatProxy
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE length #-}
    {-# ANN length hasBlackBox #-}

    replace_int :: KnownNat n => Vec n a -> Int -> a -> Vec n a
    replace_int :: forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a -> Vec n a
    replace_int Vec n a
    xs i :: Int
    i@(I# Int#
    n0) a
    a
      | Int# -> Bool
    isTrue# (Int#
    n0 Int# -> Int# -> Int#
    <# Int#
    0#) = String -> Vec n a
    forall a. HasCallStack => String -> a
    error String
    "Clash.Sized.Vector.replace: negative index"
      | Bool
    otherwise          = Vec n a -> Int# -> a -> Vec n a
    forall (m :: Nat) b. Vec m b -> Int# -> b -> Vec m b
    sub Vec n a
    xs Int#
    n0 a
    a
      where
        sub :: Vec m b -> Int# -> b -> Vec m b
        sub :: forall (m :: Nat) b. Vec m b -> Int# -> b -> Vec m b
    sub Vec m b
    Nil     Int#
    _ b
    _ = String -> Vec m b
    forall a. HasCallStack => String -> a
    error ([String] -> String
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    P.concat [ String
    "Clash.Sized.Vector.replace: index "
                                          , Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                          , String
    " is larger than maximum index "
                                          , Int -> String
    forall a. Show a => a -> String
    show (Vec n a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length Vec n a
    xs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
                                          ])
        sub (b
    y `Cons` (!Vec n b
    ys)) Int#
    n b
    b = if Int# -> Bool
    isTrue# (Int#
    n Int# -> Int# -> Int#
    ==# Int#
    0#)
                                     then b
    b b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b
    ys
                                     else b
    y b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n b -> Int# -> b -> Vec n b
    forall (m :: Nat) b. Vec m b -> Int# -> b -> Vec m b
    sub Vec n b
    ys (Int#
    n Int# -> Int# -> Int#
    -# Int#
    1#) b
    b
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE replace_int #-}
    {-# ANN replace_int hasBlackBox #-}

    -- | \"'replace' @n a xs@\" returns the vector /xs/ where the /n/'th element is
    -- replaced by /a/.
    --
    -- __NB__: Vector elements have an __ASCENDING__ subscript starting from 0 and
    -- ending at @'length' - 1@.
    --
    -- >>> replace 3 7 (1:>2:>3:>4:>5:>Nil)
    -- 1 :> 2 :> 3 :> 7 :> 5 :> Nil
    -- >>> replace 0 7 (1:>2:>3:>4:>5:>Nil)
    -- 7 :> 2 :> 3 :> 4 :> 5 :> Nil
    -- >>> replace 9 7 (1:>2:>3:>4:>5:>Nil)
    -- 1 :> 2 :> 3 :> 4 :> 5 :> *** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 4
    -- ...
    replace :: (KnownNat n, Enum i) => i -> a -> Vec n a -> Vec n a
    replace :: forall (n :: Nat) i a.
    (KnownNat n, Enum i) =>
    i -> a -> Vec n a -> Vec n a
    replace i
    i a
    y Vec n a
    xs = Vec n a -> Int -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a -> Vec n a
    replace_int Vec n a
    xs (i -> Int
    forall a. Enum a => a -> Int
    fromEnum i
    i) a
    y
    {-# INLINE replace #-}

    {- | \"'take' @n xs@\" returns the /n/-length prefix of /xs/.

    >>> take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> Nil
    >>> take d3               (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> Nil
    >>> take d0               (1:>2:>Nil)
    Nil

    #if __GLASGOW_HASKELL__ >= 910
    >>> take d4               (1:>2:>Nil)
    <interactive>:...
        • Couldn't match type ‘4 + n0’ with ‘2’
          Expected: Vec (4 + n0) a
            Actual: Vec (1 + 1) a
          The type variable ‘n0’ is ambiguous
        • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
          In the expression: take d4 (1 :> 2 :> Nil)
          In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ == 906
    >>> take d4               (1:>2:>Nil)
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘4 + n0’ with ‘2’
          Expected: Vec (4 + n0) a
            Actual: Vec (1 + 1) a
            The type variable ‘n0’ is ambiguous
        • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
          In the expression: take d4 (1 :> 2 :> Nil)
          In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)

    #elif __GLASGOW_HASKELL__ >= 900
    >>> take d4               (1:>2:>Nil)
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘4 + n0’ with ‘2’
          Expected: Vec (4 + n0) a
            Actual: Vec (1 + 1) a
          The type variable ‘n0’ is ambiguous
        • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
          In the expression: take d4 (1 :> 2 :> Nil)
          In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)

    #else
    >>> take d4               (1:>2:>Nil)
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘4 + n0’ with ‘2’
          Expected type: Vec (4 + n0) a
            Actual type: Vec (1 + 1) a
          The type variable ‘n0’ is ambiguous
        • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
          In the expression: take d4 (1 :> 2 :> Nil)
          In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)

    #endif
    -}
    take :: SNat m -> Vec (m + n) a -> Vec m a
    take :: forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec m a
    take SNat m
    n = (Vec m a, Vec n a) -> Vec m a
    forall a b. (a, b) -> a
    fst ((Vec m a, Vec n a) -> Vec m a)
    -> (Vec (m + n) a -> (Vec m a, Vec n a))
    -> Vec (m + n) a
    -> Vec m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt SNat m
    n
    {-# INLINE take #-}

    -- | \"'takeI' @xs@\" returns the prefix of /xs/ as demanded by the context.
    --
    -- >>> takeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
    -- 1 :> 2 :> Nil
    takeI :: KnownNat m => Vec (m + n) a -> Vec m a
    takeI :: forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> Vec m a
    takeI = (SNat m -> Vec (m + n) a -> Vec m a) -> Vec (m + n) a -> Vec m a
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat m -> Vec (m + n) a -> Vec m a
    forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec m a
    take
    {-# INLINE takeI #-}

    {- | \"'drop' @n xs@\" returns the suffix of /xs/ after the first /n/ elements.

    >>> drop (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
    4 :> 5 :> Nil
    >>> drop d3               (1:>2:>3:>4:>5:>Nil)
    4 :> 5 :> Nil
    >>> drop d0               (1:>2:>Nil)
    1 :> 2 :> Nil

    #if __GLASGOW_HASKELL__ >= 910
    >>> drop d4               (1:>2:>Nil)
    <interactive>:...: error:...
        • Couldn't match...type ‘4 + n0...
          The type variable ‘n0’ is ambiguous
        • In the first argument of ‘print’, namely ‘it’
          In a stmt of an interactive GHCi command: print it
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ == 906
    >>> drop d4               (1:>2:>Nil)
    <BLANKLINE>
    <interactive>:...: error:...
        • Couldn't match...type ‘4 + n0...
            The type variable ‘n0’ is ambiguous
        • In the first argument of ‘print’, namely ‘it’
          In a stmt of an interactive GHCi command: print it

    #else
    >>> drop d4               (1:>2:>Nil)
    <BLANKLINE>
    <interactive>:...: error:...
        • Couldn't match...type ‘4 + n0...
          The type variable ‘n0’ is ambiguous
        • In the first argument of ‘print’, namely ‘it’
          In a stmt of an interactive GHCi command: print it

    #endif
    -}
    drop :: SNat m -> Vec (m + n) a -> Vec n a
    drop :: forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
    drop SNat m
    n = (Vec m a, Vec n a) -> Vec n a
    forall a b. (a, b) -> b
    snd ((Vec m a, Vec n a) -> Vec n a)
    -> (Vec (m + n) a -> (Vec m a, Vec n a))
    -> Vec (m + n) a
    -> Vec n a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt SNat m
    n
    {-# INLINE drop #-}

    -- | \"'dropI' @xs@\" returns the suffix of /xs/ as demanded by the context.
    --
    -- >>> dropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
    -- 4 :> 5 :> Nil
    dropI :: KnownNat m => Vec (m + n) a -> Vec n a
    dropI :: forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> Vec n a
    dropI = (SNat m -> Vec (m + n) a -> Vec n a) -> Vec (m + n) a -> Vec n a
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat m -> Vec (m + n) a -> Vec n a
    forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
    drop
    {-# INLINE dropI #-}

    -- | \"'at' @n xs@\" returns /n/'th element of /xs/
    --
    -- __NB__: Vector elements have an __ASCENDING__ subscript starting from 0 and
    -- ending at @'length' - 1@.
    --
    -- >>> at (SNat :: SNat 1) (1:>2:>3:>4:>5:>Nil)
    -- 2
    -- >>> at d1               (1:>2:>3:>4:>5:>Nil)
    -- 2
    at :: SNat m -> Vec (m + (n + 1)) a -> a
    at :: forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + (n + 1)) a -> a
    at SNat m
    n Vec (m + (n + 1)) a
    xs = Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head (Vec (n + 1) a -> a) -> Vec (n + 1) a -> a
    forall a b. (a -> b) -> a -> b
    $ (Vec m a, Vec (n + 1) a) -> Vec (n + 1) a
    forall a b. (a, b) -> b
    snd ((Vec m a, Vec (n + 1) a) -> Vec (n + 1) a)
    -> (Vec m a, Vec (n + 1) a) -> Vec (n + 1) a
    forall a b. (a -> b) -> a -> b
    $ SNat m -> Vec (m + (n + 1)) a -> (Vec m a, Vec (n + 1) a)
    forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt SNat m
    n Vec (m + (n + 1)) a
    xs
    {-# INLINE at #-}

    -- | \"'select' @f s n xs@\" selects /n/ elements with step-size /s/ and
    -- offset @f@ from /xs/.
    --
    -- >>> select (SNat :: SNat 1) (SNat :: SNat 2) (SNat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
    -- 2 :> 4 :> 6 :> Nil
    -- >>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
    -- 2 :> 4 :> 6 :> Nil
    select :: (CmpNat (i + s) (s * n) ~ 'GT)
           => SNat f
           -> SNat s
           -> SNat n
           -> Vec (f + i) a
           -> Vec n a
    select :: forall (i :: Nat) (s :: Nat) (n :: Nat) (f :: Nat) a.
    (CmpNat (i + s) (s * n) ~ 'GT) =>
    SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
    select SNat f
    f SNat s
    s SNat n
    n Vec (f + i) a
    xs = UNat n -> Vec i a -> Vec n a
    forall (n :: Nat) (i :: Nat) a. UNat n -> Vec i a -> Vec n a
    select' (SNat n -> UNat n
    forall (n :: Nat). SNat n -> UNat n
    toUNat SNat n
    n) (Vec i a -> Vec n a) -> Vec i a -> Vec n a
    forall a b. (a -> b) -> a -> b
    $ SNat f -> Vec (f + i) a -> Vec i a
    forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
    drop SNat f
    f Vec (f + i) a
    xs
      where
        select' :: UNat n -> Vec i a -> Vec n a
        select' :: forall (n :: Nat) (i :: Nat) a. UNat n -> Vec i a -> Vec n a
    select' UNat n
    UZero      Vec i a
    _               = Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        select' (USucc UNat n
    n') vs :: Vec i a
    vs@(a
    x `Cons` Vec n a
    _) = a
    x a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons`
                                             UNat n -> Vec (ZonkAny 0) a -> Vec n a
    forall (n :: Nat) (i :: Nat) a. UNat n -> Vec i a -> Vec n a
    select' UNat n
    n' (SNat s -> Vec (s + ZonkAny 0) a -> Vec (ZonkAny 0) a
    forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
    drop SNat s
    s (Vec i a -> Vec (s + ZonkAny 0) a
    forall a b. a -> b
    unsafeCoerce Vec i a
    vs))
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE select #-}
    {-# ANN select hasBlackBox #-}

    -- | \"'selectI' @f s xs@\" selects as many elements as demanded by the context
    -- with step-size /s/ and offset /f/ from /xs/.
    --
    -- >>> selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
    -- 2 :> 4 :> Nil
    selectI :: (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n)
            => SNat f
            -> SNat s
            -> Vec (f + i) a
            -> Vec n a
    selectI :: forall (i :: Nat) (s :: Nat) (n :: Nat) (f :: Nat) a.
    (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n) =>
    SNat f -> SNat s -> Vec (f + i) a -> Vec n a
    selectI SNat f
    f SNat s
    s Vec (f + i) a
    xs = (SNat n -> Vec n a) -> Vec n a
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat (\SNat n
    n -> SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
    forall (i :: Nat) (s :: Nat) (n :: Nat) (f :: Nat) a.
    (CmpNat (i + s) (s * n) ~ 'GT) =>
    SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
    select SNat f
    f SNat s
    s SNat n
    n Vec (f + i) a
    xs)
    {-# INLINE selectI #-}

    -- | \"'replicate' @n a@\" returns a vector that has /n/ copies of /a/.
    --
    -- >>> replicate (SNat :: SNat 3) 6
    -- 6 :> 6 :> 6 :> Nil
    -- >>> replicate d3 6
    -- 6 :> 6 :> 6 :> Nil
    replicate :: SNat n -> a -> Vec n a
    replicate :: forall (n :: Nat) a. SNat n -> a -> Vec n a
    replicate SNat n
    n a
    a = UNat n -> a -> Vec n a
    forall (n :: Nat) a. UNat n -> a -> Vec n a
    replicateU (SNat n -> UNat n
    forall (n :: Nat). SNat n -> UNat n
    toUNat SNat n
    n) a
    a
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE replicate #-}
    {-# ANN replicate hasBlackBox #-}

    replicateU :: UNat n -> a -> Vec n a
    replicateU :: forall (n :: Nat) a. UNat n -> a -> Vec n a
    replicateU UNat n
    UZero     a
    _ = Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
    replicateU (USucc UNat n
    s) a
    x = a
    x a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` UNat n -> a -> Vec n a
    forall (n :: Nat) a. UNat n -> a -> Vec n a
    replicateU UNat n
    s a
    x

    -- | \"'repeat' @a@\" creates a vector with as many copies of /a/ as demanded
    -- by the context.
    --
    -- >>> repeat 6 :: Vec 5 Int
    -- 6 :> 6 :> 6 :> 6 :> 6 :> Nil
    repeat :: KnownNat n => a -> Vec n a
    repeat :: forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat = (SNat n -> a -> Vec n a) -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
    withSNat SNat n -> a -> Vec n a
    forall (n :: Nat) a. SNat n -> a -> Vec n a
    replicate
    {-# INLINE repeat #-}

    -- | \"'iterate' @n f x@\" returns a vector starting with /x/ followed by
    -- /n/ repeated applications of /f/ to /x/.
    --
    -- > iterate (SNat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
    -- > iterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
    --
    -- >>> iterate d4 (+1) 1
    -- 1 :> 2 :> 3 :> 4 :> Nil
    --
    -- \"'iterate' @n f z@\" corresponds to the following circuit layout:
    --
    -- <<doc/iterate.svg>>
    iterate :: SNat n -> (a -> a) -> a -> Vec n a
    iterate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a
    iterate SNat n
    SNat = (a -> a) -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI
    {-# INLINE iterate #-}

    -- | \"'iterateI' @f x@\" returns a vector starting with @x@ followed by @n@
    -- repeated applications of @f@ to @x@, where @n@ is determined by the context.
    --
    -- > iterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)
    --
    -- >>> iterateI (+1) 1 :: Vec 3 Int
    -- 1 :> 2 :> 3 :> Nil
    --
    -- \"'iterateI' @f z@\" corresponds to the following circuit layout:
    --
    -- <<doc/iterate.svg>>
    iterateI :: forall n a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI a -> a
    f = UNat n -> a -> Vec n a
    forall (m :: Nat). UNat m -> a -> Vec m a
    iterateU (SNat n -> UNat n
    forall (n :: Nat). SNat n -> UNat n
    toUNat (forall (n :: Nat). KnownNat n => SNat n
    SNat @n))
     where
      iterateU :: forall m. UNat m -> a -> Vec m a
      iterateU :: forall (m :: Nat). UNat m -> a -> Vec m a
    iterateU UNat m
    UZero a
    _ = Vec m a
    Vec 0 a
    forall a. Vec 0 a
    Nil
      iterateU (USucc UNat n
    s) a
    a = a
    a a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` UNat n -> a -> Vec n a
    forall (m :: Nat). UNat m -> a -> Vec m a
    iterateU UNat n
    s (a -> a
    f a
    a)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE iterateI #-}
    {-# ANN iterateI (InlineYamlPrimitive [VHDL,Verilog,SystemVerilog] [I.__i|
      BlackBoxHaskell:
        name: Clash.Sized.Vector.iterateI
        templateFunction: Clash.Primitives.Sized.Vector.iterateBBF
      |]) #-}

    -- | \"'unfoldr' @n f s@\" builds a vector of length @n@ from a seed value @s@,
    -- where every element @a@ is created by successive calls of @f@ on @s@. Unlike
    -- 'Data.List.unfoldr' from "Data.List" the generating function @f@ cannot
    -- dictate the length of the resulting vector, it must be statically known.
    --
    -- a simple use of 'unfoldr':
    --
    -- >>> unfoldr d10 (\s -> (s,s-1)) 10
    -- 10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil
    unfoldr :: SNat n -> (s -> (a,s)) -> s -> Vec n a
    unfoldr :: forall (n :: Nat) s a. SNat n -> (s -> (a, s)) -> s -> Vec n a
    unfoldr SNat n
    SNat = (s -> (a, s)) -> s -> Vec n a
    forall (n :: Nat) s a. KnownNat n => (s -> (a, s)) -> s -> Vec n a
    unfoldrI
    {-# INLINE unfoldr #-}

    -- | \"'unfoldrI' @f s@\" builds a vector from a seed value @s@, where every
    -- element @a@ is created by successive calls of @f@ on @s@; the length of the
    -- vector is inferred from the context. Unlike 'Data.List.unfoldr' from
    -- "Data.List" the generating function @f@ cannot  dictate the length of the
    -- resulting vector, it must be statically known.
    --
    -- a simple use of 'unfoldrI':
    --
    -- >>> unfoldrI (\s -> (s,s-1)) 10 :: Vec 10 Int
    -- 10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil
    unfoldrI :: KnownNat n => (s -> (a,s)) -> s -> Vec n a
    unfoldrI :: forall (n :: Nat) s a. KnownNat n => (s -> (a, s)) -> s -> Vec n a
    unfoldrI s -> (a, s)
    f s
    s0 = ((a, s) -> a) -> Vec n (a, s) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (a, s) -> a
    forall a b. (a, b) -> a
    fst Vec n (a, s)
    xs
     where
      xs :: Vec n (a, s)
    xs = Vec (n + 1) (a, s) -> Vec n (a, s)
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init (s -> (a, s)
    f s
    s0 (a, s) -> Vec n (a, s) -> Vec (n + 1) (a, s)
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n (a, s)
    ws)
      ws :: Vec n (a, s)
    ws = ((a, s) -> (a, s)) -> Vec n (a, s) -> Vec n (a, s)
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (s -> (a, s)
    f (s -> (a, s)) -> ((a, s) -> s) -> (a, s) -> (a, s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, s) -> s
    forall a b. (a, b) -> b
    snd) (Vec n (a, s) -> Vec n (a, s)
    forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
    lazyV Vec n (a, s)
    xs)
    {-# INLINE unfoldrI #-}

    -- | \"'generate' @n f x@\" returns a vector with @n@ repeated applications of
    -- @f@ to @x@.
    --
    -- > generate (SNat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
    -- > generate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
    --
    -- >>> generate d4 (+1) 1
    -- 2 :> 3 :> 4 :> 5 :> Nil
    --
    -- \"'generate' @n f z@\" corresponds to the following circuit layout:
    --
    -- <<doc/generate.svg>>
    generate :: SNat n -> (a -> a) -> a -> Vec n a
    generate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a
    generate SNat n
    SNat a -> a
    f a
    a = (a -> a) -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI a -> a
    f (a -> a
    f a
    a)
    {-# INLINE generate #-}

    -- | \"'generateI' @f x@\" returns a vector with @n@ repeated applications of
    -- @f@ to @x@, where @n@ is determined by the context.
    --
    -- > generateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)
    --
    -- >>> generateI (+1) 1 :: Vec 3 Int
    -- 2 :> 3 :> 4 :> Nil
    --
    -- \"'generateI' @f z@\" corresponds to the following circuit layout:
    --
    -- <<doc/generate.svg>>
    generateI :: KnownNat n => (a -> a) -> a -> Vec n a
    generateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    generateI a -> a
    f a
    a = (a -> a) -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI a -> a
    f (a -> a
    f a
    a)
    {-# INLINE generateI #-}

    -- | Transpose a matrix: go from row-major to column-major
    --
    -- >>> let xss = (1:>2:>Nil):>(3:>4:>Nil):>(5:>6:>Nil):>Nil
    -- >>> xss
    -- (1 :> 2 :> Nil) :> (3 :> 4 :> Nil) :> (5 :> 6 :> Nil) :> Nil
    -- >>> transpose xss
    -- (1 :> 3 :> 5 :> Nil) :> (2 :> 4 :> 6 :> Nil) :> Nil
    transpose :: KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a)
    transpose :: forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    Vec m (Vec n a) -> Vec n (Vec m a)
    transpose = (Vec n a -> Vec n a) -> Vec m (Vec n a) -> Vec n (Vec m a)
    forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# Vec n a -> Vec n a
    forall a. a -> a
    id
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE transpose #-}
    {-# ANN transpose hasBlackBox #-}

    -- | 1-dimensional stencil computations
    --
    -- \"'stencil1d' @stX f xs@\", where /xs/ has /stX + n/ elements, applies the
    -- stencil computation /f/ on: /n + 1/ overlapping (1D) windows of length /stX/,
    -- drawn from /xs/. The resulting vector has /n + 1/ elements.
    --
    -- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
    -- >>> :t xs
    -- xs :: Num a => Vec 6 a
    -- >>> :t stencil1d d2 sum xs
    -- stencil1d d2 sum xs :: Num b => Vec 5 b
    -- >>> stencil1d d2 sum xs
    -- 3 :> 5 :> 7 :> 9 :> 11 :> Nil
    stencil1d :: KnownNat n
              => SNat (stX + 1) -- ^ Windows length /stX/, at least size 1
              -> (Vec (stX + 1) a -> b) -- ^ The stencil (function)
              -> Vec ((stX + n) + 1) a
              -> Vec (n + 1) b
    stencil1d :: forall (n :: Nat) (stX :: Nat) a b.
    KnownNat n =>
    SNat (stX + 1)
    -> (Vec (stX + 1) a -> b) -> Vec ((stX + n) + 1) a -> Vec (n + 1) b
    stencil1d SNat (stX + 1)
    stX Vec (stX + 1) a -> b
    f Vec ((stX + n) + 1) a
    xs = (Vec (stX + 1) a -> b)
    -> Vec (n + 1) (Vec (stX + 1) a) -> Vec (n + 1) b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map Vec (stX + 1) a -> b
    f (SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    forall (n :: Nat) (stX :: Nat) a.
    KnownNat n =>
    SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    windows1d SNat (stX + 1)
    stX Vec ((stX + n) + 1) a
    xs)
    {-# INLINE stencil1d #-}

    {- | 2-dimensional stencil computations

    \"'stencil2d' @stY stX f xss@\", where /xss/ is a matrix of /stY + m/ rows
    of /stX + n/ elements, applies the stencil computation /f/ on:
    /(m + 1) * (n + 1)/ overlapping (2D) windows of /stY/ rows of /stX/ elements,
    drawn from /xss/. The result matrix has /m + 1/ rows of /n + 1/ elements.

    >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
    >>> :t xss
    xss :: Num a => Vec 4 (Vec 4 a)

    #if __GLASGOW_HASKELL__ >= 902
    >>> :t stencil2d d2 d2 (sum . map sum) xss
    stencil2d d2 d2 (sum . map sum) xss :: Num a => Vec 3 (Vec 3 a)

    #else
    >>> :t stencil2d d2 d2 (sum . map sum) xss
    stencil2d d2 d2 (sum . map sum) xss :: Num b => Vec 3 (Vec 3 b)

    #endif
    >>> stencil2d d2 d2 (sum . map sum) xss
    (14 :> 18 :> 22 :> Nil) :> (30 :> 34 :> 38 :> Nil) :> (46 :> 50 :> 54 :> Nil) :> Nil
    -}
    stencil2d :: (KnownNat n, KnownNat m)
              => SNat (stY + 1) -- ^ Window hight /stY/, at least size 1
              -> SNat (stX + 1) -- ^ Window width /stX/, at least size 1
              -> (Vec (stY + 1) (Vec (stX + 1) a) -> b) -- ^ The stencil (function)
              -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
              -> Vec (m + 1) (Vec (n + 1) b)
    stencil2d :: forall (n :: Nat) (m :: Nat) (stY :: Nat) (stX :: Nat) a b.
    (KnownNat n, KnownNat m) =>
    SNat (stY + 1)
    -> SNat (stX + 1)
    -> (Vec (stY + 1) (Vec (stX + 1) a) -> b)
    -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    -> Vec (m + 1) (Vec (n + 1) b)
    stencil2d SNat (stY + 1)
    stY SNat (stX + 1)
    stX Vec (stY + 1) (Vec (stX + 1) a) -> b
    f Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    xss = ((Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    -> Vec (m + 1) (Vec (n + 1) b)
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map((Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
     -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
     -> Vec (m + 1) (Vec (n + 1) b))
    -> ((Vec (stY + 1) (Vec (stX + 1) a) -> b)
        -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
    -> (Vec (stY + 1) (Vec (stX + 1) a) -> b)
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    -> Vec (m + 1) (Vec (n + 1) b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .(Vec (stY + 1) (Vec (stX + 1) a) -> b)
    -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map) Vec (stY + 1) (Vec (stX + 1) a) -> b
    f (SNat (stY + 1)
    -> SNat (stX + 1)
    -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    forall (n :: Nat) (m :: Nat) (stY :: Nat) (stX :: Nat) a.
    (KnownNat n, KnownNat m) =>
    SNat (stY + 1)
    -> SNat (stX + 1)
    -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    windows2d SNat (stY + 1)
    stY SNat (stX + 1)
    stX Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    xss)
    {-# INLINE stencil2d #-}

    -- | \"'windows1d' @stX xs@\", where the vector /xs/ has /stX + n/ elements,
    -- returns a vector of /n + 1/ overlapping (1D) windows of /xs/ of length /stX/.
    --
    -- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
    -- >>> :t xs
    -- xs :: Num a => Vec 6 a
    -- >>> :t windows1d d2 xs
    -- windows1d d2 xs :: Num a => Vec 5 (Vec 2 a)
    -- >>> windows1d d2 xs
    -- (1 :> 2 :> Nil) :> (2 :> 3 :> Nil) :> (3 :> 4 :> Nil) :> (4 :> 5 :> Nil) :> (5 :> 6 :> Nil) :> Nil
    windows1d :: KnownNat n
              => SNat (stX + 1) -- ^ Length of the window, at least size 1
              -> Vec ((stX + n) + 1) a
              -> Vec (n + 1) (Vec (stX + 1) a)
    windows1d :: forall (n :: Nat) (stX :: Nat) a.
    KnownNat n =>
    SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    windows1d SNat (stX + 1)
    stX Vec ((stX + n) + 1) a
    xs = (Vec ((stX + 1) + n) a -> Vec (stX + 1) a)
    -> Vec (n + 1) (Vec ((stX + 1) + n) a)
    -> Vec (n + 1) (Vec (stX + 1) a)
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (SNat (stX + 1) -> Vec ((stX + 1) + n) a -> Vec (stX + 1) a
    forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec m a
    take SNat (stX + 1)
    stX) (Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec ((stX + n) + 1) a)
    forall {n :: Nat} {n :: Nat} {a}.
    KnownNat n =>
    Vec (n + 1) a -> Vec n (Vec (n + 1) a)
    rotations Vec ((stX + n) + 1) a
    xs)
      where
        rotateL :: Vec (n + 1) a -> Vec (n + 1) a
    rotateL Vec (n + 1) a
    ys   = Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec (n + 1) a
    ys Vec n a -> a -> Vec (n + 1) a
    forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    :< Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec (n + 1) a
    ys
        rotations :: Vec (n + 1) a -> Vec n (Vec (n + 1) a)
    rotations Vec (n + 1) a
    ys = (Vec (n + 1) a -> Vec (n + 1) a)
    -> Vec (n + 1) a -> Vec n (Vec (n + 1) a)
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI Vec (n + 1) a -> Vec (n + 1) a
    forall {n :: Nat} {a}. Vec (n + 1) a -> Vec (n + 1) a
    rotateL Vec (n + 1) a
    ys
    {-# INLINE windows1d #-}

    -- | \"'windows2d' @stY stX xss@\", where matrix /xss/ has /stY + m/ rows of
    -- /stX + n/, returns a matrix of /m+1/ rows of /n+1/ elements. The elements
    -- of this new matrix are the overlapping (2D) windows of /xss/, where every
    -- window has /stY/ rows of /stX/ elements.
    --
    -- >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
    -- >>> :t xss
    -- xss :: Num a => Vec 4 (Vec 4 a)
    -- >>> :t windows2d d2 d2 xss
    -- windows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))
    -- >>> windows2d d2 d2 xss
    -- (((1 :> 2 :> Nil) :> (5 :> 6 :> Nil) :> Nil) :> ((2 :> 3 :> Nil) :> (6 :> 7 :> Nil) :> Nil) :> ((3 :> 4 :> Nil) :> (7 :> 8 :> Nil) :> Nil) :> Nil) :> (((5 :> 6 :> Nil) :> (9 :> 10 :> Nil) :> Nil) :> ((6 :> 7 :> Nil) :> (10 :> 11 :> Nil) :> Nil) :> ((7 :> 8 :> Nil) :> (11 :> 12 :> Nil) :> Nil) :> Nil) :> (((9 :> 10 :> Nil) :> (13 :> 14 :> Nil) :> Nil) :> ((10 :> 11 :> Nil) :> (14 :> 15 :> Nil) :> Nil) :> ((11 :> 12 :> Nil) :> (15 :> 16 :> Nil) :> Nil) :> Nil) :> Nil
    windows2d :: (KnownNat n,KnownNat m)
              => SNat (stY + 1) -- ^ Window hight /stY/, at least size 1
              -> SNat (stX + 1) -- ^ Window width /stX/, at least size 1
              -> Vec ((stY + m) + 1) (Vec (stX + n + 1) a)
              -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    windows2d :: forall (n :: Nat) (m :: Nat) (stY :: Nat) (stX :: Nat) a.
    (KnownNat n, KnownNat m) =>
    SNat (stY + 1)
    -> SNat (stX + 1)
    -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    windows2d SNat (stY + 1)
    stY SNat (stX + 1)
    stX Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    xss = (Vec (stY + 1) (Vec ((stX + n) + 1) a)
     -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    -> Vec (m + 1) (Vec (stY + 1) (Vec ((stX + n) + 1) a))
    -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
    -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))
    forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    Vec m (Vec n a) -> Vec n (Vec m a)
    transpose (Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
     -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
    -> (Vec (stY + 1) (Vec ((stX + n) + 1) a)
        -> Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a)))
    -> Vec (stY + 1) (Vec ((stX + n) + 1) a)
    -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a))
    -> Vec (stY + 1) (Vec ((stX + n) + 1) a)
    -> Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    forall (n :: Nat) (stX :: Nat) a.
    KnownNat n =>
    SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    windows1d SNat (stX + 1)
    stX))) (SNat (stY + 1)
    -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    -> Vec (m + 1) (Vec (stY + 1) (Vec ((stX + n) + 1) a))
    forall (n :: Nat) (stX :: Nat) a.
    KnownNat n =>
    SNat (stX + 1)
    -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
    windows1d SNat (stY + 1)
    stY Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
    xss)
    {-# INLINE windows2d #-}

    -- | Forward permutation specified by an index mapping, /ix/. The result vector
    -- is initialized by the given defaults, /def/, and an further values that are
    -- permuted into the result are added to the current value using the given
    -- combination function, /f/.
    --
    -- The combination function must be /associative/ and /commutative/.
    permute :: (Enum i, KnownNat n, KnownNat m)
            => (a -> a -> a)  -- ^ Combination function, /f/
            -> Vec n a        -- ^ Default values, /def/
            -> Vec m i        -- ^ Index mapping, /is/
            -> Vec (m + k) a  -- ^ Vector to be permuted, /xs/
            -> Vec n a
    permute :: forall i (n :: Nat) (m :: Nat) a (k :: Nat).
    (Enum i, KnownNat n, KnownNat m) =>
    (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
    permute a -> a -> a
    f Vec n a
    defs Vec m i
    is Vec (m + k) a
    xs = Vec n a
    ys
      where
        ixs :: Vec m (i, a)
    ixs = Vec m i -> Vec m a -> Vec m (i, a)
    forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
    zip Vec m i
    is (Vec (m + k) a -> Vec m a
    forall (m :: Nat) (n :: Nat) a.
    KnownNat m =>
    Vec (m + n) a -> Vec m a
    takeI Vec (m + k) a
    xs)
        ys :: Vec n a
    ys  = (Vec n a -> (i, a) -> Vec n a)
    -> Vec n a -> Vec m (i, a) -> Vec n a
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl (\Vec n a
    ks (i
    i,a
    x) -> let ki :: a
    ki = Vec n a
    ksVec n a -> i -> a
    forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !!i
    i in i -> a -> Vec n a -> Vec n a
    forall (n :: Nat) i a.
    (KnownNat n, Enum i) =>
    i -> a -> Vec n a -> Vec n a
    replace i
    i (a -> a -> a
    f a
    x a
    ki) Vec n a
    ks) Vec n a
    defs Vec m (i, a)
    ixs
    {-# INLINE permute #-}

    -- | Backwards permutation specified by an index mapping, /is/, from the
    -- destination vector specifying which element of the source vector /xs/ to
    -- read.
    --
    -- \"'backpermute' @xs is@\" is equivalent to \"'map' @(xs '!!') is@\".
    --
    -- For example:
    --
    -- >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
    -- >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
    -- >>> backpermute input from
    -- 9 :> 4 :> 1 :> 6 :> 2 :> 4 :> Nil
    backpermute :: (Enum i, KnownNat n)
                => Vec n a  -- ^ Source vector, /xs/
                -> Vec m i  -- ^ Index mapping, /is/
                -> Vec m a
    backpermute :: forall i (n :: Nat) a (m :: Nat).
    (Enum i, KnownNat n) =>
    Vec n a -> Vec m i -> Vec m a
    backpermute Vec n a
    xs = (i -> a) -> Vec m i -> Vec m a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (Vec n a
    xsVec n a -> i -> a
    forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !!)
    {-# INLINE backpermute #-}

    -- | Copy elements from the source vector, /xs/, to the destination vector
    -- according to an index mapping /is/. This is a forward permute operation where
    -- a /to/ vector encodes an input to output index mapping. Output elements for
    -- indices that are not mapped assume the value in the default vector /def/.
    --
    -- For example:
    --
    -- >>> let defVec = 0:>0:>0:>0:>0:>0:>0:>0:>0:>Nil
    -- >>> let to = 1:>3:>7:>2:>5:>8:>Nil
    -- >>> let input = 1:>9:>6:>4:>4:>2:>5:>Nil
    -- >>> scatter defVec to input
    -- 0 :> 1 :> 4 :> 9 :> 0 :> 4 :> 0 :> 6 :> 2 :> Nil
    --
    -- __NB__: If the same index appears in the index mapping more than once, the
    -- latest mapping is chosen.
    scatter :: (Enum i, KnownNat n, KnownNat m)
            => Vec n a       -- ^ Default values, /def/
            -> Vec m i       -- ^ Index mapping, /is/
            -> Vec (m + k) a -- ^ Vector to be scattered, /xs/
            -> Vec n a
    scatter :: forall i (n :: Nat) (m :: Nat) a (k :: Nat).
    (Enum i, KnownNat n, KnownNat m) =>
    Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
    scatter = (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
    forall i (n :: Nat) (m :: Nat) a (k :: Nat).
    (Enum i, KnownNat n, KnownNat m) =>
    (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
    permute a -> a -> a
    forall a b. a -> b -> a
    const
    {-# INLINE scatter #-}

    -- | Backwards permutation specified by an index mapping, /is/, from the
    -- destination vector specifying which element of the source vector /xs/ to
    -- read.
    --
    -- \"'gather' @xs is@\" is equivalent to \"'map' @(xs '!!') is@\".
    --
    -- For example:
    --
    -- >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
    -- >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
    -- >>> gather input from
    -- 9 :> 4 :> 1 :> 6 :> 2 :> 4 :> Nil
    gather :: (Enum i, KnownNat n)
           => Vec n a  -- ^ Source vector, /xs/
           -> Vec m i  -- ^ Index mapping, /is/
           -> Vec m a
    gather :: forall i (n :: Nat) a (m :: Nat).
    (Enum i, KnownNat n) =>
    Vec n a -> Vec m i -> Vec m a
    gather Vec n a
    xs = (i -> a) -> Vec m i -> Vec m a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map (Vec n a
    xsVec n a -> i -> a
    forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !!)
    {-# INLINE gather #-}

    -- | \"'interleave' @d xs@\" creates a vector:
    --
    -- > <x_0,x_d,x_(2d),...,x_1,x_(d+1),x_(2d+1),...,x_(d-1),x_(2d-1),x_(3d-1)>
    --
    -- >>> let xs = 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> Nil
    -- >>> interleave d3 xs
    -- 1 :> 4 :> 7 :> 2 :> 5 :> 8 :> 3 :> 6 :> 9 :> Nil
    interleave :: (KnownNat n, KnownNat d)
               => SNat d -- ^ Interleave step, /d/
               -> Vec (n * d) a
               -> Vec (d * n) a
    interleave :: forall (n :: Nat) (d :: Nat) a.
    (KnownNat n, KnownNat d) =>
    SNat d -> Vec (n * d) a -> Vec (d * n) a
    interleave SNat d
    d = Vec d (Vec n a) -> Vec (d * n) a
    forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
    concat (Vec d (Vec n a) -> Vec (d * n) a)
    -> (Vec (n * d) a -> Vec d (Vec n a))
    -> Vec (n * d) a
    -> Vec (d * n) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n (Vec d a) -> Vec d (Vec n a)
    forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    Vec m (Vec n a) -> Vec n (Vec m a)
    transpose (Vec n (Vec d a) -> Vec d (Vec n a))
    -> (Vec (n * d) a -> Vec n (Vec d a))
    -> Vec (n * d) a
    -> Vec d (Vec n a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SNat d -> Vec (n * d) a -> Vec n (Vec d a)
    forall (n :: Nat) (m :: Nat) a.
    KnownNat n =>
    SNat m -> Vec (n * m) a -> Vec n (Vec m a)
    unconcat SNat d
    d
    {-# INLINE interleave #-}

    -- | /Dynamically/ rotate a 'Vec'tor to the left:
    --
    -- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    -- >>> rotateLeft xs 1
    -- 2 :> 3 :> 4 :> 1 :> Nil
    -- >>> rotateLeft xs 2
    -- 3 :> 4 :> 1 :> 2 :> Nil
    -- >>> rotateLeft xs (-1)
    -- 4 :> 1 :> 2 :> 3 :> Nil
    --
    -- __NB__: Use `rotateLeftS` if you want to rotate left by a /static/ amount.
    rotateLeft :: (Enum i, KnownNat n)
               => Vec n a
               -> i
               -> Vec n a
    rotateLeft :: forall i (n :: Nat) a.
    (Enum i, KnownNat n) =>
    Vec n a -> i -> Vec n a
    rotateLeft Vec n a
    xs i
    i = (Int -> a) -> Vec n Int -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map ((Vec n a
    xs Vec n a -> Int -> a
    forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !!) (Int -> a) -> (Int -> Int) -> Int -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    len)) ((Int -> Int) -> Int -> Vec n Int
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Int
    i')
      where
        i' :: Int
    i'  = i -> Int
    forall a. Enum a => a -> Int
    fromEnum i
    i
        len :: Int
    len = Vec n a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length Vec n a
    xs
    {-# INLINE rotateLeft #-}

    -- | /Dynamically/ rotate a 'Vec'tor to the right:
    --
    -- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    -- >>> rotateRight xs 1
    -- 4 :> 1 :> 2 :> 3 :> Nil
    -- >>> rotateRight xs 2
    -- 3 :> 4 :> 1 :> 2 :> Nil
    -- >>> rotateRight xs (-1)
    -- 2 :> 3 :> 4 :> 1 :> Nil
    --
    -- __NB__: Use `rotateRightS` if you want to rotate right by a /static/ amount.
    rotateRight :: (Enum i, KnownNat n)
                => Vec n a
                -> i
                -> Vec n a
    rotateRight :: forall i (n :: Nat) a.
    (Enum i, KnownNat n) =>
    Vec n a -> i -> Vec n a
    rotateRight Vec n a
    xs i
    i = (Int -> a) -> Vec n Int -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map ((Vec n a
    xs Vec n a -> Int -> a
    forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
    !!) (Int -> a) -> (Int -> Int) -> Int -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    len)) ((Int -> Int) -> Int -> Vec n Int
    forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
    iterateI (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Int
    i')
      where
        i' :: Int
    i'  = Int -> Int
    forall a. Num a => a -> a
    negate (i -> Int
    forall a. Enum a => a -> Int
    fromEnum i
    i)
        len :: Int
    len = Vec n a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length Vec n a
    xs
    {-# INLINE rotateRight #-}

    -- | /Statically/ rotate a 'Vec'tor to the left:
    --
    -- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    -- >>> rotateLeftS xs d1
    -- 2 :> 3 :> 4 :> 1 :> Nil
    --
    -- __NB__: Use `rotateLeft` if you want to rotate left by a /dynamic/ amount.
    rotateLeftS :: KnownNat n
                => Vec n a
                -> SNat d
                -> Vec n a
    rotateLeftS :: forall (n :: Nat) a (d :: Nat).
    KnownNat n =>
    Vec n a -> SNat d -> Vec n a
    rotateLeftS Vec n a
    xs SNat d
    d = Integer -> Vec n a -> Vec n a
    forall (k :: Nat) a. Integer -> Vec k a -> Vec k a
    go (SNat d -> Integer
    forall (n :: Nat). SNat n -> Integer
    snatToInteger SNat d
    d Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal (Vec n a -> Proxy n
    forall (n :: Nat) a. Vec n a -> Proxy n
    asNatProxy Vec n a
    xs)) Vec n a
    xs
      where
        go :: Integer -> Vec k a -> Vec k a
        go :: forall (k :: Nat) a. Integer -> Vec k a -> Vec k a
    go Integer
    _ Vec k a
    Nil           = Vec k a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        go Integer
    0 Vec k a
    ys            = Vec k a
    ys
        go Integer
    n (a
    y `Cons` Vec n a
    ys) = Integer -> Vec k a -> Vec k a
    forall (k :: Nat) a. Integer -> Vec k a -> Vec k a
    go (Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) (Vec n a
    ys Vec n a -> a -> Vec (n + 1) a
    forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
    :< a
    y)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE rotateLeftS #-}
    {-# ANN rotateLeftS hasBlackBox #-}

    -- | /Statically/ rotate a 'Vec'tor to the right:
    --
    -- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    -- >>> rotateRightS xs d1
    -- 4 :> 1 :> 2 :> 3 :> Nil
    --
    -- __NB__: Use `rotateRight` if you want to rotate right by a /dynamic/ amount.
    rotateRightS :: KnownNat n
                 => Vec n a
                 -> SNat d
                 -> Vec n a
    rotateRightS :: forall (n :: Nat) a (d :: Nat).
    KnownNat n =>
    Vec n a -> SNat d -> Vec n a
    rotateRightS Vec n a
    xs SNat d
    d = Integer -> Vec n a -> Vec n a
    forall {a} {a :: Nat} {b}. (Eq a, Num a) => a -> Vec a b -> Vec a b
    go (SNat d -> Integer
    forall (n :: Nat). SNat n -> Integer
    snatToInteger SNat d
    d Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal (Vec n a -> Proxy n
    forall (n :: Nat) a. Vec n a -> Proxy n
    asNatProxy Vec n a
    xs)) Vec n a
    xs
      where
        go :: a -> Vec a b -> Vec a b
    go a
    _ Vec a b
    Nil            = Vec a b
    Vec 0 b
    forall a. Vec 0 a
    Nil
        go a
    0 Vec a b
    ys             = Vec a b
    ys
        go a
    n ys :: Vec a b
    ys@(Cons b
    _ Vec n b
    _)  = a -> Vec a b -> Vec a b
    go (a
    na -> a -> a
    forall a. Num a => a -> a -> a
    -a
    1) (Vec (n + 1) b -> b
    forall (n :: Nat) a. Vec (n + 1) a -> a
    last Vec a b
    Vec (n + 1) b
    ys b -> Vec n b -> Vec (n + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :> Vec (n + 1) b -> Vec n b
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    init Vec a b
    Vec (n + 1) b
    ys)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE rotateRightS #-}
    {-# ANN rotateRightS hasBlackBox #-}

    -- | Convert a vector to a list.
    --
    -- >>> toList (1:>2:>3:>Nil)
    -- [1,2,3]
    --
    -- __NB__: This function is not synthesizable
    toList :: Vec n a -> [a]
    toList :: forall (n :: Nat) a. Vec n a -> [a]
    toList = (a -> [a] -> [a]) -> [a] -> Vec n a -> [a]
    forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
    foldr (:) []
    {-# INLINE toList #-}

    -- | Convert a list to a vector. This function returns Nothing if the size of
    -- the list is not equal to the size of the resulting vector.
    --
    -- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 5 Int)
    -- Just (1 :> 2 :> 3 :> 4 :> 5 :> Nil)
    --
    -- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 3 Int)
    -- Nothing
    --
    -- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 10 Int)
    -- Nothing
    --
    -- * __NB__: Use `listToVecTH` if you want to make a /statically known/ vector
    -- * __NB__: This function is not synthesizable
    --
    fromList :: forall n a. (KnownNat n) => [a] -> Maybe (Vec n a)
    fromList :: forall (n :: Nat) a. KnownNat n => [a] -> Maybe (Vec n a)
    fromList [a]
    xs
      | Integer -> [a] -> Bool
    forall {t} {a}. (Eq t, Num t) => t -> [a] -> Bool
    exactLength (forall (n :: Nat). KnownNat n => Integer
    natToInteger @n) [a]
    xs = Vec n a -> Maybe (Vec n a)
    forall a. a -> Maybe a
    Just ([a] -> Vec n a
    forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
    unsafeFromList [a]
    xs)
      | Bool
    otherwise = Maybe (Vec n a)
    forall a. Maybe a
    Nothing
     where
      exactLength :: t -> [a] -> Bool
    exactLength t
    0 [a]
    acc = [a] -> Bool
    forall a. [a] -> Bool
    forall (t :: Type -> Type) a. Foldable t => t a -> Bool
    null [a]
    acc
      exactLength t
    _ []  = Bool
    False
      exactLength t
    i (a
    _:[a]
    ys) = t -> [a] -> Bool
    exactLength (t
    i t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1) [a]
    ys
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE fromList #-}
    {-# ANN fromList dontTranslate #-}

    -- | Convert a list to a vector. This function always returns a vector of the
    -- desired length, by either truncating the list or padding the vector with
    -- undefined elements.
    --
    -- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 5 Int
    -- 1 :> 2 :> 3 :> 4 :> 5 :> Nil
    --
    -- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 3 Int
    -- 1 :> 2 :> 3 :> Nil
    --
    -- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 10 Int
    -- 1 :> 2 :> 3 :> 4 :> 5 :> *** Exception: Clash.Sized.Vector.unsafeFromList: vector larger than list
    -- ...
    --
    -- * __NB__: Use `listToVecTH` if you want to make a /statically known/ vector
    -- * __NB__: This function is not synthesizable
    --
    unsafeFromList :: forall n a. (KnownNat n) => [a] -> Vec n a
    unsafeFromList :: forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
    unsafeFromList = SNat n -> ([a] -> (a, [a])) -> [a] -> Vec n a
    forall (n :: Nat) s a. SNat n -> (s -> (a, s)) -> s -> Vec n a
    unfoldr SNat n
    forall (n :: Nat). KnownNat n => SNat n
    SNat [a] -> (a, [a])
    go
     where
      go :: [a] -> (a, [a])
      go :: [a] -> (a, [a])
    go (a
    x:[a]
    xs) = (a
    x, [a]
    xs)
      go [] =
        let item :: a
    item = String -> a
    forall a. HasCallStack => String -> a
    error String
    "Clash.Sized.Vector.unsafeFromList: vector larger than list"
         in (a
    forall {a}. a
    item, [])
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE unsafeFromList #-}
    {-# ANN unsafeFromList dontTranslate #-}

    -- | Create a vector literal from a list literal.
    --
    -- > $(listToVecTH [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)
    --
    -- >>> [1 :: Signed 8,2,3,4,5]
    -- [1,2,3,4,5]
    -- >>> $(listToVecTH [1::Signed 8,2,3,4,5])
    -- 1 :> 2 :> 3 :> 4 :> 5 :> Nil
    listToVecTH :: Lift a => [a] -> ExpQ
    listToVecTH :: forall a. Lift a => [a] -> ExpQ
    listToVecTH []     = [| Nil |]
    listToVecTH (a
    x:[a]
    xs) = [| x :> $([a] -> ExpQ
    forall a. Lift a => [a] -> ExpQ
    listToVecTH [a]
    xs) |]

    -- | 'Vec'tor as a 'Proxy' for 'Nat'
    asNatProxy :: Vec n a -> Proxy n
    asNatProxy :: forall (n :: Nat) a. Vec n a -> Proxy n
    asNatProxy Vec n a
    _ = Proxy n
    forall {k} (t :: k). Proxy t
    Proxy

    -- | Length of a 'Vec'tor as an 'SNat' value
    lengthS :: KnownNat n => Vec n a -> SNat n
    lengthS :: forall (n :: Nat) a. KnownNat n => Vec n a -> SNat n
    lengthS Vec n a
    _ = SNat n
    forall (n :: Nat). KnownNat n => SNat n
    SNat
    {-# INLINE lengthS #-}

    -- | What you should use when your vector functions are too strict in their
    -- arguments.
    --
    -- === __doctests setup__
    -- >>> let compareSwapL a b = if a < b then (a,b) else (b,a)
    -- >>> :{
    -- let sortVL :: (Ord a, KnownNat (n + 1)) => Vec ((n + 1) + 1) a -> Vec ((n + 1) + 1) a
    --     sortVL xs = map fst sorted :< (snd (last sorted))
    --       where
    --         lefts  = head xs :> map snd (init sorted)
    --         rights = tail xs
    --         sorted = zipWith compareSwapL (lazyV lefts) rights
    -- :}
    --
    -- >>> :{
    -- let sortV_flip xs = map fst sorted :< (snd (last sorted))
    --       where
    --         lefts  = head xs :> map snd (init sorted)
    --         rights = tail xs
    --         sorted = zipWith (flip compareSwapL) rights lefts
    -- :}
    --
    -- === Example usage
    --
    -- For example:
    --
    -- @
    -- -- Bubble sort for 1 iteration
    -- sortV xs = 'map' fst sorted ':<' (snd ('last' sorted))
    --  where
    --    lefts  = 'head' xs :> 'map' snd ('init' sorted)
    --    rights = 'tail' xs
    --    sorted = 'zipWith' compareSwapL lefts rights
    --
    -- -- Compare and swap
    -- compareSwapL a b = if a < b then (a,b)
    --                             else (b,a)
    -- @
    --
    -- Will not terminate because 'zipWith' is too strict in its second argument.
    --
    -- In this case, adding 'lazyV' on 'zipWith's second argument:
    --
    -- @
    -- sortVL xs = 'map' fst sorted ':<' (snd ('last' sorted))
    --  where
    --    lefts  = 'head' xs :> map snd ('init' sorted)
    --    rights = 'tail' xs
    --    sorted = 'zipWith' compareSwapL ('lazyV' lefts) rights
    -- @
    --
    -- Results in a successful computation:
    --
    -- >>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
    -- 1 :> 2 :> 3 :> 4 :> Nil
    --
    -- __NB__: There is also a solution using 'flip', but it slightly obfuscates the
    -- meaning of the code:
    --
    -- @
    -- sortV_flip xs = 'map' fst sorted ':<' (snd ('last' sorted))
    --  where
    --    lefts  = 'head' xs :> 'map' snd ('init' sorted)
    --    rights = 'tail' xs
    --    sorted = 'zipWith' ('flip' compareSwapL) rights lefts
    -- @
    --
    -- >>> sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)
    -- 1 :> 2 :> 3 :> 4 :> Nil
    lazyV :: KnownNat n
          => Vec n a
          -> Vec n a
    lazyV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
    lazyV = Vec n () -> Vec n a -> Vec n a
    forall (n :: Nat) a. Vec n () -> Vec n a -> Vec n a
    lazyV' (() -> Vec n ()
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat ())
      where
        lazyV' :: Vec n () -> Vec n a -> Vec n a
        lazyV' :: forall (n :: Nat) a. Vec n () -> Vec n a -> Vec n a
    lazyV' Vec n ()
    Nil           Vec n a
    _  = Vec n a
    Vec 0 a
    forall a. Vec 0 a
    Nil
        lazyV' (()
    _ `Cons` Vec n ()
    xs) Vec n a
    ys = Vec (n + 1) a -> a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec n a
    Vec (n + 1) a
    ys a -> Vec n a -> Vec (n + 1) a
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    `Cons` Vec n () -> Vec n a -> Vec n a
    forall (n :: Nat) a. Vec n () -> Vec n a -> Vec n a
    lazyV' Vec n ()
    xs (Vec (n + 1) a -> Vec n a
    forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
    tail Vec n a
    Vec (n + 1) a
    ys)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE lazyV #-}
    {-# ANN lazyV hasBlackBox #-}

    -- | A /dependently/ typed fold.
    --
    -- === __doctests setup__
    -- >>> :seti -fplugin GHC.TypeLits.Normalise
    -- >>> import Data.Singletons (Apply, Proxy (..), TyFun)
    -- >>> data Append (m :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
    -- >>> type instance Apply (Append m a) l = Vec (l + m) a
    -- >>> let append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs
    --
    -- === Example usage
    --
    -- Using lists, we can define /append/ (a.k.a. @Data.List.@'Data.List.++') in
    -- terms of @Data.List.@'Data.List.foldr':
    --
    -- >>> import qualified Data.List
    -- >>> let append xs ys = Data.List.foldr (:) ys xs
    -- >>> append [1,2] [3,4]
    -- [1,2,3,4]
    --
    -- However, when we try to do the same for 'Vec', by defining /append'/ in terms
    -- of @Clash.Sized.Vector.@'foldr':
    --
    -- @
    -- append' xs ys = 'foldr' (:>) ys xs
    -- @
    --
    -- we get a type error:
    --
    -- @
    -- __>>> let append' xs ys = foldr (:>) ys xs__
    --
    -- \<interactive\>:...
    --     • Occurs check: cannot construct the infinite type: ... ~ ... + 1
    --       Expected type: a -> Vec ... a -> Vec ... a
    --         Actual type: a -> Vec ... a -> Vec (... + 1) a
    --     • In the first argument of ‘foldr’, namely ‘(:>)’
    --       In the expression: foldr (:>) ys xs
    --       In an equation for ‘append'’: append' xs ys = foldr (:>) ys xs
    --     • Relevant bindings include
    --         ys :: Vec ... a (bound at ...)
    --         append' :: Vec n a -> Vec ... a -> Vec ... a
    --           (bound at ...)
    -- @
    --
    -- The reason is that the type of 'foldr' is:
    --
    -- >>> :t foldr
    -- foldr :: (a -> b -> b) -> b -> Vec n a -> b
    --
    -- While the type of (':>') is:
    --
    -- >>> :t (:>)
    -- (:>) :: a -> Vec n a -> Vec (n + 1) a
    --
    -- We thus need a @fold@ function that can handle the growing vector type:
    -- 'dfold'. Compared to 'foldr', 'dfold' takes an extra parameter, called the
    -- /motive/, that allows the folded function to have an argument and result type
    -- that /depends/ on the current length of the vector. Using 'dfold', we can
    -- now correctly define /append'/:
    --
    -- @
    -- import Data.Singletons
    -- import Data.Proxy
    --
    -- data Append (m :: Nat) (a :: Type) (f :: 'TyFun' Nat Type) :: Type
    -- type instance 'Apply' (Append m a) l = 'Vec' (l + m) a
    --
    -- append' xs ys = 'dfold' (Proxy :: Proxy (Append m a)) (const (':>')) ys xs
    -- @
    --
    -- We now see that /append'/ has the appropriate type:
    --
    -- >>> :t append'
    -- append' :: KnownNat k => Vec k a -> Vec m a -> Vec (k + m) a
    --
    -- And that it works:
    --
    -- >>> append' (1 :> 2 :> Nil) (3 :> 4 :> Nil)
    -- 1 :> 2 :> 3 :> 4 :> Nil
    --
    -- __NB__: \"@'dfold' m f z xs@\" creates a linear structure, which has a depth,
    -- or delay, of O(@'length' xs@). Look at 'dtfold' for a /dependently/ typed
    -- fold that produces a structure with a depth of O(log_2(@'length' xs@)).
    dfold :: forall p k a . KnownNat k
          => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
          -> (forall l . SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))
          -- ^ Function to fold.
          --
          -- __NB__: The @SNat l@ is __not__ the index (see (`!!`)) to the
          -- element /a/. @SNat l@ is the number of elements that occur to the
          -- right of /a/.
          -> (p @@ 0) -- ^ Initial element
          -> Vec k a -- ^ Vector to fold over
          -> (p @@ k)
    dfold :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
    KnownNat k =>
    Proxy p
    -> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
    -> (p @@ 0)
    -> Vec k a
    -> p @@ k
    dfold Proxy p
    _ forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)
    f p @@ 0
    z Vec k a
    xs = SNat k -> Vec k a -> p @@ k
    forall (n :: Nat). SNat n -> Vec n a -> p @@ n
    go (Proxy k -> SNat k
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> SNat n
    snatProxy (Vec k a -> Proxy k
    forall (n :: Nat) a. Vec n a -> Proxy n
    asNatProxy Vec k a
    xs)) Vec k a
    xs
      where
        go :: SNat n -> Vec n a -> (p @@ n)
        go :: forall (n :: Nat). SNat n -> Vec n a -> p @@ n
    go SNat n
    _ Vec n a
    Nil                        = Apply p n
    p @@ 0
    z
        go SNat n
    s (a
    y `Cons` Vec n a
    ys) =
          let s' :: SNat n
    s' = SNat n
    SNat (n + 1)
    s SNat (n + 1) -> SNat 1 -> SNat n
    forall (a :: Nat) (b :: Nat). SNat (a + b) -> SNat b -> SNat a
    `subSNat` SNat 1
    d1
          in  SNat n -> a -> (p @@ n) -> p @@ (n + 1)
    forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)
    f SNat n
    s' a
    y (SNat n -> Vec n a -> p @@ n
    forall (n :: Nat). SNat n -> Vec n a -> p @@ n
    go SNat n
    s' Vec n a
    ys)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE dfold #-}
    {-# ANN dfold hasBlackBox #-}

    {- | A combination of 'dfold' and 'fold': a /dependently/ typed fold that
    reduces a vector in a tree-like structure.

    === __doctests setup__
    >>> :seti -XUndecidableInstances
    >>> import Data.Singletons (Apply, Proxy (..), TyFun)
    >>> data IIndex (f :: TyFun Nat Type) :: Type
    >>> type instance Apply IIndex l = Index ((2^l)+1)
    >>> :{
    let populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) -> Index ((2^k)+1)
        populationCount' bv = dtfold (Proxy @IIndex)
                                     fromIntegral
                                     (\_ x y -> add x y)
                                     (bv2v bv)
    :}

    === Example usage

    As an example of when you might want to use 'dtfold' we will build a
    population counter: a circuit that counts the number of bits set to '1' in
    a 'BitVector'. Given a vector of /n/ bits, we only need we need a data type
    that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@ has a range
    of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.
    As an initial attempt we will use 'sum', because it gives a nice (@log2(n)@)
    tree-structure of adders:

    @
    populationCount :: (KnownNat (n+1), KnownNat (n+2))
                    => 'BitVector' (n+1) -> 'Index' (n+2)
    populationCount = sum . map fromIntegral . 'bv2v'
    @

    The \"problem\" with this description is that all adders have the same
    bit-width, i.e. all adders are of the type:

    @
    (+) :: 'Index' (n+2) -> 'Index' (n+2) -> 'Index' (n+2).
    @

    This is a \"problem\" because we could have a more efficient structure:
    one where each layer of adders is /precisely/ wide enough to count the number
    of bits at that layer. That is, at height /d/ we want the adder to be of
    type:

    @
    'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)
    @

    We have such an adder in the form of the 'Clash.Class.Num.add' function, as
    defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.
    However, we cannot simply use 'fold' to create a tree-structure of
    'Clash.Class.Num.add'es:

    #if __GLASGOW_HASKELL__ >= 910
    >>> :{
    let populationCount' :: (KnownNat (n+1), KnownNat (n+2))
                         => BitVector (n+1) -> Index (n+2)
        populationCount' = fold add . map fromIntegral . bv2v
    :}
    <interactive>:...
        • Couldn't match type: ((n + 2) + (n + 2)) - 1
                         with: n + 2
          Expected: Index (n + 2) -> Index (n + 2) -> Index (n + 2)
            Actual: Index (n + 2)
                    -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))
        • In the first argument of ‘fold’, namely ‘add’
          In the first argument of ‘(.)’, namely ‘fold add’
          In the expression: fold add . map fromIntegral . bv2v
        • Relevant bindings include
            populationCount' :: BitVector (n + 1) -> Index (n + 2)
              (bound at ...)
    <BLANKLINE>

    #elif __GLASGOW_HASKELL__ >= 900
    >>> :{
    let populationCount' :: (KnownNat (n+1), KnownNat (n+2))
                         => BitVector (n+1) -> Index (n+2)
        populationCount' = fold add . map fromIntegral . bv2v
    :}
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type: ((n + 2) + (n + 2)) - 1
                         with: n + 2
          Expected: Index (n + 2) -> Index (n + 2) -> Index (n + 2)
            Actual: Index (n + 2)
                    -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))
        • In the first argument of ‘fold’, namely ‘add’
          In the first argument of ‘(.)’, namely ‘fold add’
          In the expression: fold add . map fromIntegral . bv2v
        • Relevant bindings include
            populationCount' :: BitVector (n + 1) -> Index (n + 2)
              (bound at ...)

    #else
    >>> :{
    let populationCount' :: (KnownNat (n+1), KnownNat (n+2))
                         => BitVector (n+1) -> Index (n+2)
        populationCount' = fold add . map fromIntegral . bv2v
    :}
    <BLANKLINE>
    <interactive>:...
        • Couldn't match type ‘((n + 2) + (n + 2)) - 1’ with ‘n + 2’
          Expected type: Index (n + 2) -> Index (n + 2) -> Index (n + 2)
            Actual type: Index (n + 2)
                         -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))
        • In the first argument of ‘fold’, namely ‘add’
          In the first argument of ‘(.)’, namely ‘fold add’
          In the expression: fold add . map fromIntegral . bv2v
        • Relevant bindings include
            populationCount' :: BitVector (n + 1) -> Index (n + 2)
              (bound at ...)

    #endif

    because 'fold' expects a function of type \"@a -> a -> a@\", i.e. a function
    where the arguments and result all have exactly the same type.

    In order to accommodate the type of our 'Clash.Class.Num.add', where the
    result is larger than the arguments, we must use a dependently typed fold in
    the form of 'dtfold':

    @
    {\-\# LANGUAGE UndecidableInstances \#-\}
    import Data.Singletons
    import Data.Proxy

    data IIndex (f :: 'TyFun' Nat Type) :: Type
    type instance 'Apply' IIndex l = 'Index' ((2^l)+1)

    populationCount' :: (KnownNat k, KnownNat (2^k))
                     => BitVector (2^k) -> Index ((2^k)+1)
    populationCount' bv = 'dtfold' (Proxy @IIndex)
                                 fromIntegral
                                 (\\_ x y -> 'Clash.Class.Num.add' x y)
                                 ('bv2v' bv)
    @

    And we can test that it works:

    >>> :t populationCount' (7 :: BitVector 16)
    populationCount' (7 :: BitVector 16) :: Index 17
    >>> populationCount' (7 :: BitVector 16)
    3

    Some final remarks:

      * By using 'dtfold' instead of 'fold', we had to restrict our 'BitVector'
        argument to have bit-width that is a power of 2.
      * Even though our original /populationCount/ function specified a structure
        where all adders had the same width. Most VHDL/(System)Verilog synthesis
        tools will create a more efficient circuit, i.e. one where the adders
        have an increasing bit-width for every layer, from the
        VHDL/(System)Verilog produced by the Clash compiler.

    __NB__: The depth, or delay, of the structure produced by
    \"@'dtfold' m f g xs@\" is O(log_2(@'length' xs@)).
    -}
    dtfold :: forall p k a . KnownNat k
           => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
           -> (a -> (p @@ 0)) -- ^ Function to apply to every element
           -> (forall l . SNat l -> (p @@ l) -> (p @@ l) -> (p @@ (l + 1)))
           -- ^ Function to combine results.
           --
           -- __NB__: The @SNat l@ indicates the depth/height of the node in the
           -- tree that is created by applying this function. The leafs of the tree
           -- have depth\/height /0/, and the root of the tree has height /k/.
           -> Vec (2^k) a
           -- ^ Vector to fold over.
           --
           -- __NB__: Must have a length that is a power of 2.
           -> (p @@ k)
    dtfold :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
    KnownNat k =>
    Proxy p
    -> (a -> p @@ 0)
    -> (forall (l :: Nat).
        SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1))
    -> Vec (2 ^ k) a
    -> p @@ k
    dtfold Proxy p
    _ a -> p @@ 0
    f forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)
    g = SNat k -> Vec (2 ^ k) a -> p @@ k
    forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
    go (SNat k
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: SNat k)
      where
        go :: forall n . SNat n -> Vec (2^n) a -> (p @@ n)
        go :: forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
    go SNat n
    _  (a
    x `Cons` Vec n a
    Nil) = a -> p @@ 0
    f a
    x
        go SNat n
    sn xs :: Vec (2 ^ n) a
    xs@(Cons a
    _ (Cons a
    _ Vec n a
    _)) =
          let sn' :: SNat (n - 1)
              sn' :: SNat (n - 1)
    sn'       = SNat n
    SNat ((n - 1) + 1)
    sn SNat ((n - 1) + 1) -> SNat 1 -> SNat (n - 1)
    forall (a :: Nat) (b :: Nat). SNat (a + b) -> SNat b -> SNat a
    `subSNat` SNat 1
    d1
              (Vec (2 ^ (n - 1)) a
    xsL,Vec (2 ^ (n - 1)) a
    xsR) = SNat (2 ^ (n - 1))
    -> Vec ((2 ^ (n - 1)) + (2 ^ (n - 1))) a
    -> (Vec (2 ^ (n - 1)) a, Vec (2 ^ (n - 1)) a)
    forall (m :: Nat) (n :: Nat) a.
    SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    splitAt (SNat (n - 1) -> SNat (2 ^ (n - 1))
    forall (a :: Nat). SNat a -> SNat (2 ^ a)
    pow2SNat SNat (n - 1)
    sn') Vec ((2 ^ (n - 1)) + (2 ^ (n - 1))) a
    Vec (2 ^ n) a
    xs
          in  SNat (n - 1)
    -> (p @@ (n - 1)) -> (p @@ (n - 1)) -> p @@ ((n - 1) + 1)
    forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)
    g SNat (n - 1)
    sn' (SNat (n - 1) -> Vec (2 ^ (n - 1)) a -> p @@ (n - 1)
    forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
    go SNat (n - 1)
    sn' Vec (2 ^ (n - 1)) a
    xsL) (SNat (n - 1) -> Vec (2 ^ (n - 1)) a -> p @@ (n - 1)
    forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
    go SNat (n - 1)
    sn' Vec (2 ^ (n - 1)) a
    xsR)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE dtfold #-}
    {-# ANN dtfold hasBlackBox #-}

    -- | To be used as the motive /p/ for 'dfold', when the /f/ in \"'dfold' @p f@\"
    -- is a variation on (':>'), e.g.:
    --
    -- @
    -- map' :: forall n a b . KnownNat n => (a -> b) -> Vec n a -> Vec n b
    -- map' f = 'dfold' (Proxy @('VCons' b)) (\_ x xs -> f x :> xs)
    -- @
    data VCons (a :: Type) (f :: TyFun Nat Type) :: Type
    type instance Apply (VCons a) l = Vec l a

    -- | Specialised version of 'dfold' that builds a triangular computational
    -- structure.
    --
    -- === __doctests setup__
    -- >>> let compareSwap a b = if a > b then (a,b) else (b,a)
    -- >>> let insert y xs = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
    -- >>> let insertionSort = vfold (const insert)
    --
    -- === Example usage
    --
    -- @
    -- compareSwap a b = if a > b then (a,b) else (b,a)
    -- insert y xs     = let (y',xs') = 'mapAccumL' compareSwap y xs in xs' ':<' y'
    -- insertionSort   = 'vfold' (const insert)
    -- @
    --
    -- Builds a triangular structure of compare and swaps to sort a row.
    --
    -- >>> insertionSort (7 :> 3 :> 9 :> 1 :> Nil)
    -- 1 :> 3 :> 7 :> 9 :> Nil
    --
    -- The circuit layout of @insertionSort@, build using 'vfold', is:
    --
    -- <<doc/csSort.svg>>
    vfold :: forall k a b . KnownNat k
          => (forall l . SNat l -> a -> Vec l b -> Vec (l + 1) b)
          -> Vec k a
          -> Vec k b
    vfold :: forall (k :: Nat) a b.
    KnownNat k =>
    (forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b)
    -> Vec k a -> Vec k b
    vfold forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b
    f Vec k a
    xs = Proxy (VCons b)
    -> (forall (l :: Nat).
        SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1))
    -> (VCons b @@ 0)
    -> Vec k a
    -> VCons b @@ k
    forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
    KnownNat k =>
    Proxy p
    -> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
    -> (p @@ 0)
    -> Vec k a
    -> p @@ k
    dfold (forall {k} (t :: k). Proxy t
    forall (t :: TyFun Nat Type -> Type). Proxy t
    Proxy @(VCons b)) SNat l -> a -> Apply (VCons b) l -> Apply (VCons b) (l + 1)
    SNat l -> a -> Vec l b -> Vec (l + 1) b
    forall (l :: Nat).
    SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1)
    forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b
    f VCons b @@ 0
    Vec 0 b
    forall a. Vec 0 a
    Nil Vec k a
    xs
    {-# INLINE vfold #-}

    -- | The largest element of a non-empty vector
    maximum ::
      Ord a =>
      Vec (n + 1) a ->
      a
    maximum :: forall a (n :: Nat). Ord a => Vec (n + 1) a -> a
    maximum = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold (\a
    x a
    y -> if a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    y then a
    x else a
    y)

    -- | The least element of a non-empty vector
    minimum ::
      Ord a =>
      Vec (n + 1) a ->
      a
    minimum :: forall a (n :: Nat). Ord a => Vec (n + 1) a -> a
    minimum = (a -> a -> a) -> Vec (n + 1) a -> a
    forall (n :: Nat) a. (a -> a -> a) -> Vec (n + 1) a -> a
    fold (\a
    x a
    y -> if a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    y then a
    x else a
    y)

    -- | Apply a function to every element of a vector and the element's position
    -- (as an 'SNat' value) in the vector.
    --
    -- >>> let rotateMatrix = smap (flip rotateRightS)
    -- >>> let xss = (1:>2:>3:>Nil):>(1:>2:>3:>Nil):>(1:>2:>3:>Nil):>Nil
    -- >>> xss
    -- (1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> Nil
    -- >>> rotateMatrix xss
    -- (1 :> 2 :> 3 :> Nil) :> (3 :> 1 :> 2 :> Nil) :> (2 :> 3 :> 1 :> Nil) :> Nil
    smap :: forall k a b . KnownNat k => (forall l . SNat l -> a -> b) -> Vec k a -> Vec k b
    smap :: forall (k :: Nat) a b.
    KnownNat k =>
    (forall (l :: Nat). SNat l -> a -> b) -> Vec k a -> Vec k b
    smap forall (l :: Nat). SNat l -> a -> b
    f Vec k a
    xs = Vec k b -> Vec k b
    forall (n :: Nat) a. Vec n a -> Vec n a
    reverse
              (Vec k b -> Vec k b) -> Vec k b -> Vec k b
    forall a b. (a -> b) -> a -> b
    $ Proxy (VCons b)
    -> (forall (l :: Nat).
        SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1))
    -> (VCons b @@ 0)
    -> Vec k a
    -> VCons b @@ k
    forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
    KnownNat k =>
    Proxy p
    -> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
    -> (p @@ 0)
    -> Vec k a
    -> p @@ k
    dfold (forall {k} (t :: k). Proxy t
    forall (t :: TyFun Nat Type -> Type). Proxy t
    Proxy @(VCons b))
                      (\SNat l
    sn a
    x VCons b @@ l
    xs' -> SNat l -> a -> b
    forall (l :: Nat). SNat l -> a -> b
    f SNat l
    sn a
    x b -> Vec l b -> Vec (l + 1) b
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :> VCons b @@ l
    Vec l b
    xs')
                      VCons b @@ 0
    Vec 0 b
    forall a. Vec 0 a
    Nil (Vec k a -> Vec k a
    forall (n :: Nat) a. Vec n a -> Vec n a
    reverse Vec k a
    xs)
    {-# INLINE smap #-}

    instance (KnownNat n, BitPack a) => BitPack (Vec n a) where
      type BitSize (Vec n a) = n * (BitSize a)
      pack :: Vec n a -> BitVector (BitSize (Vec n a))
    pack   = (Vec n a -> BitVector (n * BitSize a))
    -> Vec n a -> BitVector (n * BitSize a)
    forall (n :: Nat) a.
    KnownNat n =>
    (a -> BitVector n) -> a -> BitVector n
    packXWith (Vec n (BitVector (BitSize a)) -> BitVector (n * BitSize a)
    forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) =>
    Vec n (BitVector m) -> BitVector (n * m)
    concatBitVector# (Vec n (BitVector (BitSize a)) -> BitVector (n * BitSize a))
    -> (Vec n a -> Vec n (BitVector (BitSize a)))
    -> Vec n a
    -> BitVector (n * BitSize a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> BitVector (BitSize a))
    -> Vec n a -> Vec n (BitVector (BitSize a))
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map a -> BitVector (BitSize a)
    forall a. BitPack a => a -> BitVector (BitSize a)
    pack)
      unpack :: BitVector (BitSize (Vec n a)) -> Vec n a
    unpack = (BitVector (BitSize a) -> a)
    -> Vec n (BitVector (BitSize a)) -> Vec n a
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
    map BitVector (BitSize a) -> a
    forall a. BitPack a => BitVector (BitSize a) -> a
    unpack (Vec n (BitVector (BitSize a)) -> Vec n a)
    -> (BitVector (n * BitSize a) -> Vec n (BitVector (BitSize a)))
    -> BitVector (n * BitSize a)
    -> Vec n a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BitVector (n * BitSize a) -> Vec n (BitVector (BitSize a))
    forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) =>
    BitVector (n * m) -> Vec n (BitVector m)
    unconcatBitVector#

    concatBitVector#
      :: forall n m
       . (KnownNat n, KnownNat m)
      => Vec n (BitVector m)
      -> BitVector (n * m)
    concatBitVector# :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) =>
    Vec n (BitVector m) -> BitVector (n * m)
    concatBitVector# = BitVector (n * m) -> Vec n (BitVector m) -> BitVector (n * m)
    forall (p :: Nat).
    BitVector (n * m) -> Vec p (BitVector m) -> BitVector (n * m)
    go BitVector (n * m)
    0
     where
      go :: BitVector (n*m) -> Vec p (BitVector m) -> BitVector (n * m)
      go :: forall (p :: Nat).
    BitVector (n * m) -> Vec p (BitVector m) -> BitVector (n * m)
    go BitVector (n * m)
    acc Vec p (BitVector m)
    Nil = BitVector (n * m)
    acc
      go (BV Nat
    accMsk Nat
    accVal) ((BV Nat
    xMsk Nat
    xVal) `Cons` Vec n (BitVector m)
    xs) =
        let sh :: Int
    sh = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy m -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @m)) :: Int in
        BitVector (n * m) -> Vec n (BitVector m) -> BitVector (n * m)
    forall (p :: Nat).
    BitVector (n * m) -> Vec p (BitVector m) -> BitVector (n * m)
    go (Nat -> Nat -> BitVector (n * m)
    forall (n :: Nat). Nat -> Nat -> BitVector n
    BV (Nat -> Int -> Nat
    forall a. Bits a => a -> Int -> a
    shiftL Nat
    accMsk Int
    sh Nat -> Nat -> Nat
    forall a. Bits a => a -> a -> a
    .|. Nat
    xMsk) (Nat -> Int -> Nat
    forall a. Bits a => a -> Int -> a
    shiftL Nat
    accVal Int
    sh Nat -> Nat -> Nat
    forall a. Bits a => a -> a -> a
    .|. Nat
    xVal)) Vec n (BitVector m)
    xs
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE concatBitVector# #-}
    {-# ANN concatBitVector# hasBlackBox #-}

    unconcatBitVector#
      :: forall n m
       . (KnownNat n, KnownNat m)
      => BitVector (n * m)
      -> Vec n (BitVector m)
    unconcatBitVector# :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) =>
    BitVector (n * m) -> Vec n (BitVector m)
    unconcatBitVector# BitVector (n * m)
    orig = (BitVector ((n - n) * m), Vec n (BitVector m))
    -> Vec n (BitVector m)
    forall a b. (a, b) -> b
    snd (UNat n -> (BitVector ((n - n) * m), Vec n (BitVector m))
    forall (p :: Nat).
    (p <= n) =>
    UNat p -> (BitVector ((n - p) * m), Vec p (BitVector m))
    go (SNat n -> UNat n
    forall (n :: Nat). SNat n -> UNat n
    toUNat (forall (n :: Nat). KnownNat n => SNat n
    SNat @n)))
      where
        go :: forall p . (p <= n) => UNat p -> (BitVector ((n-p)*m), Vec p (BitVector m))
        go :: forall (p :: Nat).
    (p <= n) =>
    UNat p -> (BitVector ((n - p) * m), Vec p (BitVector m))
    go UNat p
    UZero = (BitVector (n * m)
    BitVector ((n - p) * m)
    orig,Vec p (BitVector m)
    Vec 0 (BitVector m)
    forall a. Vec 0 a
    Nil)
        go (USucc (UNat (p - 1)
    n :: UNat (p-1))) =
          let (BitVector ((n - n) * m)
    bv,Vec n (BitVector m)
    xs) = UNat n -> (BitVector ((n - n) * m), Vec n (BitVector m))
    forall (p :: Nat).
    (p <= n) =>
    UNat p -> (BitVector ((n - p) * m), Vec p (BitVector m))
    go UNat n
    UNat (p - 1)
    n
              (BitVector ((n - p) * m)
    l,BitVector m
    x) = ((BitVector (((n - p) * m) + m)
     -> (BitVector ((n - p) * m), BitVector m))
    -> BitVector (((n - p) * m) + m)
    -> (BitVector ((n - p) * m), BitVector m)
    forall a. a -> a
    GHC.Magic.noinline BitVector (((n - p) * m) + m)
    -> (BitVector ((n - p) * m), BitVector m)
    forall (n :: Nat) (m :: Nat).
    KnownNat n =>
    BitVector (m + n) -> (BitVector m, BitVector n)
    split#) BitVector (((n - p) * m) + m)
    BitVector ((n - n) * m)
    bv
          in  (BitVector ((n - p) * m)
    l,BitVector m
    x BitVector m -> Vec n (BitVector m) -> Vec (n + 1) (BitVector m)
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :> Vec n (BitVector m)
    xs)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE unconcatBitVector# #-}
    {-# ANN unconcatBitVector# hasBlackBox #-}

    -- | Convert a 'BitVector' to a 'Vec' of 'Bit's.
    --
    -- >>> let x = 6 :: BitVector 8
    -- >>> x
    -- 0b0000_0110
    -- >>> bv2v x
    -- 0 :> 0 :> 0 :> 0 :> 0 :> 1 :> 1 :> 0 :> Nil
    bv2v :: KnownNat n => BitVector n -> Vec n Bit
    bv2v :: forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
    bv2v = BitVector n -> Vec n Bit
    BitVector (BitSize (Vec n Bit)) -> Vec n Bit
    forall a. BitPack a => BitVector (BitSize a) -> a
    unpack

    -- | Convert a 'Vec' of 'Bit's to a 'BitVector'.
    --
    -- >>> let x = (0:>0:>0:>1:>0:>0:>1:>0:>Nil) :: Vec 8 Bit
    -- >>> x
    -- 0 :> 0 :> 0 :> 1 :> 0 :> 0 :> 1 :> 0 :> Nil
    -- >>> v2bv x
    -- 0b0001_0010
    v2bv :: KnownNat n => Vec n Bit -> BitVector n
    v2bv :: forall (n :: Nat). KnownNat n => Vec n Bit -> BitVector n
    v2bv = Vec n Bit -> BitVector n
    Vec n Bit -> BitVector (BitSize (Vec n Bit))
    forall a. BitPack a => a -> BitVector (BitSize a)
    pack

    -- | Evaluate all elements of a vector to WHNF, returning the second argument
    seqV
      :: KnownNat n
      => Vec n a
      -> b
      -> b
    seqV :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
    seqV Vec n a
    v b
    b =
      let s :: () -> a -> ()
    s () a
    e = a -> () -> ()
    forall a b. a -> b -> b
    seq a
    e () in
      (() -> a -> ()) -> () -> Vec n a -> ()
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl () -> a -> ()
    forall {a}. () -> a -> ()
    s () Vec n a
    v () -> b -> b
    forall a b. a -> b -> b
    `seq` b
    b
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE seqV #-}
    {-# ANN seqV hasBlackBox #-}
    infixr 0 `seqV`

    -- | Evaluate all elements of a vector to WHNF
    forceV
      :: KnownNat n
      => Vec n a
      -> Vec n a
    forceV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
    forceV Vec n a
    v =
      Vec n a
    v Vec n a -> Vec n a -> Vec n a
    forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
    `seqV` Vec n a
    v
    {-# INLINE forceV #-}

    -- | Evaluate all elements of a vector to WHNF, returning the second argument.
    -- Does not propagate 'Clash.XException.XException's.
    seqVX
      :: KnownNat n
      => Vec n a
      -> b
      -> b
    seqVX :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
    seqVX Vec n a
    v b
    b =
      let s :: () -> a -> ()
    s () a
    e = a -> () -> ()
    forall a b. a -> b -> b
    seqX a
    e () in
      (() -> a -> ()) -> () -> Vec n a -> ()
    forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
    foldl () -> a -> ()
    forall {a}. () -> a -> ()
    s () Vec n a
    v () -> b -> b
    forall a b. a -> b -> b
    `seqX` b
    b
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE seqVX #-}
    {-# ANN seqVX hasBlackBox #-}
    infixr 0 `seqVX`

    -- | Evaluate all elements of a vector to WHNF. Does not propagate
    -- 'Clash.XException.XException's.
    forceVX
      :: KnownNat n
      => Vec n a
      -> Vec n a
    forceVX :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
    forceVX Vec n a
    v =
      Vec n a
    v Vec n a -> Vec n a -> Vec n a
    forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
    `seqVX` Vec n a
    v
    {-# INLINE forceVX #-}

    instance Lift a => Lift (Vec n a) where
      lift :: forall (m :: Type -> Type). Quote m => Vec n a -> m Exp
    lift Vec n a
    Nil           = [| Nil |]
      lift (a
    x `Cons` Vec n a
    xs) = [| x `Cons` $(Vec n a -> m Exp
    forall t (m :: Type -> Type). (Lift t, Quote m) => t -> m Exp
    forall (m :: Type -> Type). Quote m => Vec n a -> m Exp
    lift Vec n a
    xs) |]
    #if MIN_VERSION_template_haskell(2,16,0)
      liftTyped :: forall (m :: Type -> Type). Quote m => Vec n a -> Code m (Vec n a)
    liftTyped = Vec n a -> Code m (Vec n a)
    forall a (m :: Type -> Type). (Lift a, Quote m) => a -> Code m a
    liftTypedFromUntyped
    #endif

    instance (KnownNat n, Arbitrary a) => Arbitrary (Vec n a) where
      arbitrary :: Gen (Vec n a)
    arbitrary = (Gen a -> Gen a) -> Vec n (Gen a) -> Gen (Vec n a)
    forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# Gen a -> Gen a
    forall a. a -> a
    id (Vec n (Gen a) -> Gen (Vec n a)) -> Vec n (Gen a) -> Gen (Vec n a)
    forall a b. (a -> b) -> a -> b
    $ Gen a -> Vec n (Gen a)
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat Gen a
    forall a. Arbitrary a => Gen a
    arbitrary
      shrink :: Vec n a -> [Vec n a]
    shrink    = ([a] -> [a]) -> Vec n [a] -> [Vec n a]
    forall a (f :: Type -> Type) b (n :: Nat).
    Applicative f =>
    (a -> f b) -> Vec n a -> f (Vec n b)
    traverse# [a] -> [a]
    forall a. a -> a
    id (Vec n [a] -> [Vec n a])
    -> (Vec n a -> Vec n [a]) -> Vec n a -> [Vec n a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> [a]) -> Vec n a -> Vec n [a]
    forall a b. (a -> b) -> Vec n a -> Vec n b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> [a]
    forall a. Arbitrary a => a -> [a]
    shrink

    instance CoArbitrary a => CoArbitrary (Vec n a) where
      coarbitrary :: forall b. Vec n a -> Gen b -> Gen b
    coarbitrary = [a] -> Gen b -> Gen b
    forall b. [a] -> Gen b -> Gen b
    forall a b. CoArbitrary a => a -> Gen b -> Gen b
    coarbitrary ([a] -> Gen b -> Gen b)
    -> (Vec n a -> [a]) -> Vec n a -> Gen b -> Gen b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vec n a -> [a]
    forall (n :: Nat) a. Vec n a -> [a]
    toList

    type instance Lens.Index   (Vec n a) = Index n
    type instance Lens.IxValue (Vec n a) = a
    instance KnownNat n => Lens.Ixed (Vec n a) where
      ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a))
    ix Index (Vec n a)
    i IxValue (Vec n a) -> f (IxValue (Vec n a))
    f Vec n a
    xs = Vec n a -> Int -> a -> Vec n a
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a -> Vec n a
    replace_int Vec n a
    xs (Index n -> Int
    forall a. Enum a => a -> Int
    fromEnum Index (Vec n a)
    Index n
    i) (a -> Vec n a) -> f a -> f (Vec n a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> IxValue (Vec n a) -> f (IxValue (Vec n a))
    f (Vec n a -> Int -> a
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a
    index_int Vec n a
    xs (Index n -> Int
    forall a. Enum a => a -> Int
    fromEnum Index (Vec n a)
    Index n
    i))