    -- |
    -- Module      : Basement.Sized.List
    -- License     : BSD-style
    -- Maintainer  : Vincent Hanquez <vincent@snarc.org>
    -- Stability   : experimental
    -- Portability : portable
    --
    -- A Nat-sized list abstraction
    --
    -- Using this module is limited to GHC 7.10 and above.
    --
    {-# LANGUAGE KindSignatures            #-}
    {-# LANGUAGE DataKinds                 #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE TypeOperators             #-}
    {-# LANGUAGE TypeFamilies              #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE ScopedTypeVariables       #-}
    {-# LANGUAGE UndecidableInstances      #-}
    {-# LANGUAGE AllowAmbiguousTypes       #-}
    {-# LANGUAGE DeriveDataTypeable        #-}
    {-# LANGUAGE DeriveGeneric             #-}
    {-# LANGUAGE FlexibleContexts          #-}
    module Basement.Sized.List
        ( ListN
        , toListN
        , toListN_
        , unListN
        , length
        , create
        , createFrom
        , empty
        , singleton
        , uncons
        , cons
        , unsnoc
        , snoc
        , index
        , indexStatic
        , updateAt
        , map
        , mapi
        , elem
        , foldl
        , foldl'
        , foldl1'
        , scanl'
        , scanl1'
        , foldr
        , foldr1
        , reverse
        , append
        , minimum
        , maximum
        , head
        , tail
        , init
        , take
        , drop
        , splitAt
        , zip, zip3, zip4, zip5
        , unzip
        , zipWith, zipWith3, zipWith4, zipWith5
        , replicate
        -- * Applicative And Monadic
        , replicateM
        , sequence
        , sequence_
        , mapM
        , mapM_
        ) where

    import           Data.Proxy
    import qualified Data.List
    import           Basement.Compat.Base
    import           Basement.Compat.CallStack
    import           Basement.Compat.Natural
    import           Basement.Nat
    import           Basement.NormalForm
    import           Basement.Numerical.Additive
    import           Basement.Numerical.Subtractive
    import           Basement.Types.OffsetSize
    import           Basement.Compat.ExtList ((!!))
    import qualified Prelude
    import qualified Control.Monad as M (replicateM, mapM, mapM_, sequence, sequence_)

    impossible :: HasCallStack => a
    impossible :: forall a. HasCallStack => a
    impossible = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "ListN: internal error: the impossible happened"

    -- | A Typed-level sized List equivalent to [a]
    newtype ListN (n :: Nat) a = ListN { forall (n :: Nat) a. ListN n a -> [a]
    unListN :: [a] }
        deriving (ListN n a -> ListN n a -> Bool
    (ListN n a -> ListN n a -> Bool)
    -> (ListN n a -> ListN n a -> Bool) -> Eq (ListN n a)
    forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
    == :: ListN n a -> ListN n a -> Bool
    $c/= :: forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
    /= :: ListN n a -> ListN n a -> Bool
    Eq,Eq (ListN n a)
    Eq (ListN n a) =>
    (ListN n a -> ListN n a -> Ordering)
    -> (ListN n a -> ListN n a -> Bool)
    -> (ListN n a -> ListN n a -> Bool)
    -> (ListN n a -> ListN n a -> Bool)
    -> (ListN n a -> ListN n a -> Bool)
    -> (ListN n a -> ListN n a -> ListN n a)
    -> (ListN n a -> ListN n a -> ListN n a)
    -> Ord (ListN n a)
    ListN n a -> ListN n a -> Bool
    ListN n a -> ListN n a -> Ordering
    ListN n a -> ListN n a -> ListN n a
    forall (n :: Nat) a. Ord a => Eq (ListN n a)
    forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
    forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Ordering
    forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Ordering
    compare :: ListN n a -> ListN n a -> Ordering
    $c< :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
    < :: ListN n a -> ListN n a -> Bool
    $c<= :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
    <= :: ListN n a -> ListN n a -> Bool
    $c> :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
    > :: ListN n a -> ListN n a -> Bool
    $c>= :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
    >= :: ListN n a -> ListN n a -> Bool
    $cmax :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
    max :: ListN n a -> ListN n a -> ListN n a
    $cmin :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
    min :: ListN n a -> ListN n a -> ListN n a
    Ord,Typeable,(forall x. ListN n a -> Rep (ListN n a) x)
    -> (forall x. Rep (ListN n a) x -> ListN n a)
    -> Generic (ListN n a)
    forall (n :: Nat) a x. Rep (ListN n a) x -> ListN n a
    forall (n :: Nat) a x. ListN n a -> Rep (ListN n a) x
    forall x. Rep (ListN n a) x -> ListN n a
    forall x. ListN n a -> Rep (ListN n a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall (n :: Nat) a x. ListN n a -> Rep (ListN n a) x
    from :: forall x. ListN n a -> Rep (ListN n a) x
    $cto :: forall (n :: Nat) a x. Rep (ListN n a) x -> ListN n a
    to :: forall x. Rep (ListN n a) x -> ListN n a
    Generic)

    instance Show a => Show (ListN n a) where
        show :: ListN n a -> [Char]
    show (ListN [a]
    l) = [a] -> [Char]
    forall a. Show a => a -> [Char]
    show [a]
    l

    instance NormalForm a => NormalForm (ListN n a) where
        toNormalForm :: ListN n a -> ()
    toNormalForm (ListN [a]
    l) = [a] -> ()
    forall a. NormalForm a => a -> ()
    toNormalForm [a]
    l

    -- | Try to create a ListN from a List, succeeding if the length is correct
    toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
    toListN :: forall (n :: Nat) a.
    (KnownNat n, NatWithinBound Int n) =>
    [a] -> Maybe (ListN n a)
    toListN [a]
    l
        | Int
    expected Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral ([a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    Prelude.length [a]
    l) = ListN n a -> Maybe (ListN n a)
    forall a. a -> Maybe a
    Just ([a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    l)
        | Bool
    otherwise                                           = Maybe (ListN n a)
    forall a. Maybe a
    Nothing
      where
        expected :: Int
    expected = Proxy n -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)

    -- | Create a ListN from a List, expecting a given length
    --
    -- If this list contains more or less than the expected length of the resulting type,
    -- then an asynchronous error is raised. use 'toListN' for a more friendly functions
    toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
    toListN_ :: forall (n :: Nat) a.
    (HasCallStack, NatWithinBound Int n, KnownNat n) =>
    [a] -> ListN n a
    toListN_ [a]
    l
        | Int
    expected Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    got = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    l
        | Bool
    otherwise       = [Char] -> ListN n a
    forall a. HasCallStack => [Char] -> a
    error ([Char]
    "toListN_: expecting list of " [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    expected [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> [Char]
    " elements, got " [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    got [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> [Char]
    " elements")
      where
        expected :: Int
    expected = Proxy n -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)
        got :: Int
    got      = [a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    Prelude.length [a]
    l

    -- | performs a monadic action n times, gathering the results in a List of size n.
    replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
    replicateM :: forall (n :: Nat) (m :: * -> *) a.
    (NatWithinBound Int n, Monad m, KnownNat n) =>
    m a -> m (ListN n a)
    replicateM m a
    action = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> m [a] -> m (ListN n a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m a -> m [a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    M.replicateM (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)) m a
    action

    -- | Evaluate each monadic action in the list sequentially, and collect the results.
    sequence :: Monad m => ListN n (m a) -> m (ListN n a)
    sequence :: forall (m :: * -> *) (n :: Nat) a.
    Monad m =>
    ListN n (m a) -> m (ListN n a)
    sequence (ListN [m a]
    l) = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> m [a] -> m (ListN n a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [m a] -> m [a]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    M.sequence [m a]
    l

    -- | Evaluate each monadic action in the list sequentially, and ignore the results.
    sequence_ :: Monad m => ListN n (m a) -> m ()
    sequence_ :: forall (m :: * -> *) (n :: Nat) a. Monad m => ListN n (m a) -> m ()
    sequence_ (ListN [m a]
    l) = [m a] -> m ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    M.sequence_ [m a]
    l

    -- | Map each element of a List to a monadic action, evaluate these
    -- actions sequentially and collect the results
    mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
    mapM :: forall (m :: * -> *) a b (n :: Nat).
    Monad m =>
    (a -> m b) -> ListN n a -> m (ListN n b)
    mapM a -> m b
    f (ListN [a]
    l) = [b] -> ListN n b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([b] -> ListN n b) -> m [b] -> m (ListN n b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a -> m b) -> [a] -> m [b]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    M.mapM a -> m b
    f [a]
    l

    -- | Map each element of a List to a monadic action, evaluate these
    -- actions sequentially and ignore the results
    mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
    mapM_ :: forall (m :: * -> *) a b (n :: Nat).
    Monad m =>
    (a -> m b) -> ListN n a -> m ()
    mapM_ a -> m b
    f (ListN [a]
    l) = (a -> m b) -> [a] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    M.mapM_ a -> m b
    f [a]
    l

    -- | Create a list of n elements where each element is the element in argument
    replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
    replicate :: forall (n :: Nat) a.
    (NatWithinBound Int n, KnownNat n) =>
    a -> ListN n a
    replicate a
    a = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> [a] -> ListN n a
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> [a]
    forall a. Int -> a -> [a]
    Prelude.replicate (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)) a
    a

    -- | Decompose a list into its head and tail.
    uncons :: (1 <= n) => ListN n a -> (a, ListN (n-1) a)
    uncons :: forall (n :: Nat) a. (1 <= n) => ListN n a -> (a, ListN (n - 1) a)
    uncons (ListN (a
    x:[a]
    xs)) = (a
    x, [a] -> ListN (n - 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    xs)
    uncons ListN n a
    _ = (a, ListN (n - 1) a)
    forall a. HasCallStack => a
    impossible

    -- | prepend an element to the list
    cons :: a -> ListN n a -> ListN (n+1) a
    cons :: forall a (n :: Nat). a -> ListN n a -> ListN (n + 1) a
    cons a
    a (ListN [a]
    l) = [a] -> ListN (n + 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (a
    a a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    l)

    -- | Decompose a list into its first elements and the last.
    unsnoc :: (1 <= n) => ListN n a -> (ListN (n-1) a, a)
    unsnoc :: forall (n :: Nat) a. (1 <= n) => ListN n a -> (ListN (n - 1) a, a)
    unsnoc (ListN [a]
    l) = ([a] -> ListN (n - 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN (n - 1) a) -> [a] -> ListN (n - 1) a
    forall a b. (a -> b) -> a -> b
    $ [a] -> [a]
    forall a. HasCallStack => [a] -> [a]
    Data.List.init [a]
    l, [a] -> a
    forall a. HasCallStack => [a] -> a
    Data.List.last [a]
    l)

    -- | append an element to the list
    snoc :: ListN n a -> a -> ListN (n+1) a
    snoc :: forall (n :: Nat) a. ListN n a -> a -> ListN (n + 1) a
    snoc (ListN [a]
    l) a
    a = [a] -> ListN (n + 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a]
    l [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    Prelude.++ [a
    a])

    -- | Create an empty list of a
    empty :: ListN 0 a
    empty :: forall a. ListN 0 a
    empty = [a] -> ListN 0 a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []

    -- | Get the length of a list
    length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
    length :: forall a (n :: Nat).
    (KnownNat n, NatWithinBound Int n) =>
    ListN n a -> CountOf a
    length ListN n a
    _ = Int -> CountOf a
    forall ty. Int -> CountOf ty
    CountOf (Int -> CountOf a) -> Int -> CountOf a
    forall a b. (a -> b) -> a -> b
    $ Proxy n -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)

    -- | Create a new list of size n, repeately calling f from 0 to n-1
    create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
    create :: forall a (n :: Nat). KnownNat n => (Nat -> a) -> ListN n a
    create Nat -> a
    f = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> [a] -> ListN n a
    forall a b. (a -> b) -> a -> b
    $ (Integer -> a) -> [Integer] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    Prelude.map (Nat -> a
    f (Nat -> a) -> (Integer -> Nat) -> Integer -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Integer -> Nat
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral) [Integer
    0..(Integer
    lenInteger -> Integer -> Difference Integer
    forall a. Subtractive a => a -> a -> Difference a
    -Integer
    1)]
      where
        len :: Integer
    len = Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)

    -- | Same as create but apply an offset
    createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
               => Proxy start -> (Natural -> a) -> ListN n a
    createFrom :: forall a (n :: Nat) (start :: Nat).
    (KnownNat n, KnownNat start) =>
    Proxy start -> (Nat -> a) -> ListN n a
    createFrom Proxy start
    p Nat -> a
    f = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> [a] -> ListN n a
    forall a b. (a -> b) -> a -> b
    $ (Integer -> a) -> [Integer] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    Prelude.map (Nat -> a
    f (Nat -> a) -> (Integer -> Nat) -> Integer -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Integer -> Nat
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral) [Integer
    idx..(Integer
    idxInteger -> Integer -> Integer
    forall a. Additive a => a -> a -> a
    +Integer
    lenInteger -> Integer -> Difference Integer
    forall a. Subtractive a => a -> a -> Difference a
    -Integer
    1)]
      where
        len :: Integer
    len = Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)
        idx :: Integer
    idx = Proxy start -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal Proxy start
    p

    -- | create a list of 1 element
    singleton :: a -> ListN 1 a
    singleton :: forall a. a -> ListN 1 a
    singleton a
    a = [a] -> ListN 1 a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a
    a]

    -- | Check if a list contains the element a
    elem :: Eq a => a -> ListN n a -> Bool
    elem :: forall a (n :: Nat). Eq a => a -> ListN n a -> Bool
    elem a
    a (ListN [a]
    l) = a -> [a] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    Prelude.elem a
    a [a]
    l

    -- | Append 2 list together returning the new list
    append :: ListN n a -> ListN m a -> ListN (n+m) a
    append :: forall (n :: Nat) a (m :: Nat).
    ListN n a -> ListN m a -> ListN (n + m) a
    append (ListN [a]
    l1) (ListN [a]
    l2) = [a] -> ListN (n + m) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a]
    l1 [a] -> [a] -> [a]
    forall a. Semigroup a => a -> a -> a
    <> [a]
    l2)

    -- | Get the maximum element of a list
    maximum :: (Ord a, 1 <= n) => ListN n a -> a
    maximum :: forall a (n :: Nat). (Ord a, 1 <= n) => ListN n a -> a
    maximum (ListN [a]
    l) = [a] -> a
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    Prelude.maximum [a]
    l

    -- | Get the minimum element of a list
    minimum :: (Ord a, 1 <= n) => ListN n a -> a
    minimum :: forall a (n :: Nat). (Ord a, 1 <= n) => ListN n a -> a
    minimum (ListN [a]
    l) = [a] -> a
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    Prelude.minimum [a]
    l

    -- | Get the head element of a list
    head :: (1 <= n) => ListN n a -> a
    head :: forall (n :: Nat) a. (1 <= n) => ListN n a -> a
    head (ListN (a
    x:[a]
    _)) = a
    x
    head ListN n a
    _ = a
    forall a. HasCallStack => a
    impossible

    -- | Get the tail of a list
    tail :: (1 <= n) => ListN n a -> ListN (n-1) a
    tail :: forall (n :: Nat) a. (1 <= n) => ListN n a -> ListN (n - 1) a
    tail (ListN (a
    _:[a]
    xs)) = [a] -> ListN (n - 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    xs
    tail ListN n a
    _ = ListN (n - 1) a
    forall a. HasCallStack => a
    impossible

    -- | Get the list with the last element missing
    init :: (1 <= n) => ListN n a -> ListN (n-1) a
    init :: forall (n :: Nat) a. (1 <= n) => ListN n a -> ListN (n - 1) a
    init (ListN [a]
    l) = [a] -> ListN (n - 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN (n - 1) a) -> [a] -> ListN (n - 1) a
    forall a b. (a -> b) -> a -> b
    $ [a] -> [a]
    forall a. HasCallStack => [a] -> [a]
    Data.List.init [a]
    l

    -- | Take m elements from the beggining of the list.
    --
    -- The number of elements need to be less or equal to the list in argument
    take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
    take :: forall a (m :: Nat) (n :: Nat).
    (KnownNat m, NatWithinBound Int m, m <= n) =>
    ListN n a -> ListN m a
    take (ListN [a]
    l) = [a] -> ListN m a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    Prelude.take Int
    n [a]
    l)
      where n :: Int
    n = Proxy m -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)

    -- | Drop elements from a list keeping the m remaining elements
    drop :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
    drop :: forall a (d :: Nat) (m :: Nat) (n :: Nat).
    (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) =>
    ListN n a -> ListN m a
    drop (ListN [a]
    l) = [a] -> ListN m a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    Prelude.drop Int
    n [a]
    l)
      where n :: Int
    n = Proxy d -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy d
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy d)

    -- | Split a list into two, returning 2 lists
    splitAt :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (n-m) a)
    splitAt :: forall a (d :: Nat) (m :: Nat) (n :: Nat).
    (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) =>
    ListN n a -> (ListN m a, ListN (n - m) a)
    splitAt (ListN [a]
    l) = let ([a]
    l1, [a]
    l2) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    Prelude.splitAt Int
    n [a]
    l in ([a] -> ListN m a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    l1, [a] -> ListN d a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    l2)
      where n :: Int
    n = Proxy d -> Int
    forall (n :: Nat) (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt (Proxy d
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy d)

    -- | Get the i'th elements
    --
    -- This only works with TypeApplication:
    --
    -- > indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
    indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
    indexStatic :: forall (i :: Nat) (n :: Nat) a.
    (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) =>
    ListN n a -> a
    indexStatic (ListN [a]
    l) = [a]
    l [a] -> Offset a -> a
    forall a. [a] -> Offset a -> a
    !! (Proxy i -> Offset a
    forall (n :: Nat) ty (proxy :: Nat -> *).
    (KnownNat n, NatWithinBound (Offset ty) n) =>
    proxy n -> Offset ty
    natValOffset (Proxy i
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy i))

    -- | Get the i'the element
    index :: ListN n ty -> Offset ty -> ty
    index :: forall (n :: Nat) ty. ListN n ty -> Offset ty -> ty
    index (ListN [ty]
    l) Offset ty
    ofs = [ty]
    l [ty] -> Offset ty -> ty
    forall a. [a] -> Offset a -> a
    !! Offset ty
    ofs

    -- | Update the value in a list at a specific location
    updateAt :: forall n a
             .  Offset a
             -> (a -> a)
             -> ListN n a
             -> ListN n a
    updateAt :: forall (n :: Nat) a. Offset a -> (a -> a) -> ListN n a -> ListN n a
    updateAt Offset a
    o a -> a
    f (ListN [a]
    l) = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (Offset a -> [a] -> [a]
    doUpdate Offset a
    0 [a]
    l)
      where doUpdate :: Offset a -> [a] -> [a]
    doUpdate Offset a
    _ []     = []
            doUpdate Offset a
    i (a
    x:[a]
    xs)
                | Offset a
    i Offset a -> Offset a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Offset a
    o      = a -> a
    f a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    xs
                | Bool
    otherwise   = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : Offset a -> [a] -> [a]
    doUpdate (Offset a
    iOffset a -> Offset a -> Offset a
    forall a. Additive a => a -> a -> a
    +Offset a
    1) [a]
    xs

    -- | Map all elements in a list
    map :: (a -> b) -> ListN n a -> ListN n b
    map :: forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
    map a -> b
    f (ListN [a]
    l) = [b] -> ListN n b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ((a -> b) -> [a] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    Prelude.map a -> b
    f [a]
    l)

    -- | Map all elements in a list with an additional index
    mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
    mapi :: forall a b (n :: Nat). (Nat -> a -> b) -> ListN n a -> ListN n b
    mapi Nat -> a -> b
    f (ListN [a]
    l) = [b] -> ListN n b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([b] -> ListN n b) -> ([a] -> [b]) -> [a] -> ListN n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Nat -> [a] -> [b]
    loop Nat
    0 ([a] -> ListN n b) -> [a] -> ListN n b
    forall a b. (a -> b) -> a -> b
    $ [a]
    l
      where loop :: Nat -> [a] -> [b]
    loop Nat
    _ []     = []
            loop Nat
    i (a
    x:[a]
    xs) = Nat -> a -> b
    f Nat
    i a
    x b -> [b] -> [b]
    forall a. a -> [a] -> [a]
    : Nat -> [a] -> [b]
    loop (Nat
    iNat -> Nat -> Nat
    forall a. Additive a => a -> a -> a
    +Nat
    1) [a]
    xs

    -- | Fold all elements from left
    foldl :: (b -> a -> b) -> b -> ListN n a -> b
    foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
    foldl b -> a -> b
    f b
    acc (ListN [a]
    l) = (b -> a -> b) -> b -> [a] -> b
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    Prelude.foldl b -> a -> b
    f b
    acc [a]
    l

    -- | Fold all elements from left strictly
    foldl' :: (b -> a -> b) -> b -> ListN n a -> b
    foldl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
    foldl' b -> a -> b
    f b
    acc (ListN [a]
    l) = (b -> a -> b) -> b -> [a] -> b
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    Data.List.foldl' b -> a -> b
    f b
    acc [a]
    l

    -- | Fold all elements from left strictly with a first element
    -- as the accumulator
    foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
    foldl1' :: forall (n :: Nat) a. (1 <= n) => (a -> a -> a) -> ListN n a -> a
    foldl1' a -> a -> a
    f (ListN [a]
    l) = (a -> a -> a) -> [a] -> a
    forall a. HasCallStack => (a -> a -> a) -> [a] -> a
    Data.List.foldl1' a -> a -> a
    f [a]
    l

    -- | Fold all elements from right
    foldr :: (a -> b -> b) -> b -> ListN n a -> b
    foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> ListN n a -> b
    foldr a -> b -> b
    f b
    acc (ListN [a]
    l) = (a -> b -> b) -> b -> [a] -> b
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Prelude.foldr a -> b -> b
    f b
    acc [a]
    l

    -- | Fold all elements from right assuming at least one element is in the list.
    foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
    foldr1 :: forall (n :: Nat) a. (1 <= n) => (a -> a -> a) -> ListN n a -> a
    foldr1 a -> a -> a
    f (ListN [a]
    l) = (a -> a -> a) -> [a] -> a
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    Prelude.foldr1 a -> a -> a
    f [a]
    l

    -- | 'scanl' is similar to 'foldl', but returns a list of successive
    -- reduced values from the left
    --
    -- > scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
    scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
    scanl' :: forall b a (n :: Nat).
    (b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b
    scanl' b -> a -> b
    f b
    initialAcc (ListN [a]
    start) = [b] -> ListN (n + 1) b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (b -> [a] -> [b]
    go b
    initialAcc [a]
    start)
      where
        go :: b -> [a] -> [b]
    go !b
    acc [a]
    l = b
    acc b -> [b] -> [b]
    forall a. a -> [a] -> [a]
    : case [a]
    l of
                            []     -> []
                            (a
    x:[a]
    xs) -> b -> [a] -> [b]
    go (b -> a -> b
    f b
    acc a
    x) [a]
    xs

    -- | 'scanl1' is a variant of 'scanl' that has no starting value argument:
    --
    -- > scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
    scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
    scanl1' :: forall a (n :: Nat). (a -> a -> a) -> ListN n a -> ListN n a
    scanl1' a -> a -> a
    f (ListN [a]
    l) = case [a]
    l of
                            []     -> [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []
                            (a
    x:[a]
    xs) -> [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> ListN n a) -> [a] -> ListN n a
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> a) -> a -> [a] -> [a]
    forall b a. (b -> a -> b) -> b -> [a] -> [b]
    Data.List.scanl' a -> a -> a
    f a
    x [a]
    xs

    -- | Reverse a list
    reverse :: ListN n a -> ListN n a
    reverse :: forall (n :: Nat) a. ListN n a -> ListN n a
    reverse (ListN [a]
    l) = [a] -> ListN n a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> [a]
    forall a. [a] -> [a]
    Prelude.reverse [a]
    l)

    -- | Zip 2 lists of the same size, returning a new list of
    -- the tuple of each elements
    zip :: ListN n a -> ListN n b -> ListN n (a,b)
    zip :: forall (n :: Nat) a b. ListN n a -> ListN n b -> ListN n (a, b)
    zip (ListN [a]
    l1) (ListN [b]
    l2) = [(a, b)] -> ListN n (a, b)
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    Prelude.zip [a]
    l1 [b]
    l2)

    -- | Unzip a list of tuple, to 2 List of the deconstructed tuples
    unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
    unzip :: forall (n :: Nat) a b. ListN n (a, b) -> (ListN n a, ListN n b)
    unzip ListN n (a, b)
    l = (((a, b) -> a) -> ListN n (a, b) -> ListN n a
    forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
    map (a, b) -> a
    forall a b. (a, b) -> a
    fst ListN n (a, b)
    l, ((a, b) -> b) -> ListN n (a, b) -> ListN n b
    forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
    map (a, b) -> b
    forall a b. (a, b) -> b
    snd ListN n (a, b)
    l)

    -- | Zip 3 lists of the same size
    zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
    zip3 :: forall (n :: Nat) a b c.
    ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c)
    zip3 (ListN [a]
    x1) (ListN [b]
    x2) (ListN [c]
    x3) = [(a, b, c)] -> ListN n (a, b, c)
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> [b] -> [c] -> [(a, b, c)]
    forall {a} {b} {c}. [a] -> [b] -> [c] -> [(a, b, c)]
    loop [a]
    x1 [b]
    x2 [c]
    x3)
      where loop :: [a] -> [b] -> [c] -> [(a, b, c)]
    loop (a
    l1:[a]
    l1s) (b
    l2:[b]
    l2s) (c
    l3:[c]
    l3s) = (a
    l1,b
    l2,c
    l3) (a, b, c) -> [(a, b, c)] -> [(a, b, c)]
    forall a. a -> [a] -> [a]
    : [a] -> [b] -> [c] -> [(a, b, c)]
    loop [a]
    l1s [b]
    l2s [c]
    l3s
            loop []       [b]
    _        [c]
    _        = []
            loop [a]
    _        [b]
    _        [c]
    _        = [(a, b, c)]
    forall a. HasCallStack => a
    impossible

    -- | Zip 4 lists of the same size
    zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
    zip4 :: forall (n :: Nat) a b c d.
    ListN n a
    -> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d)
    zip4 (ListN [a]
    x1) (ListN [b]
    x2) (ListN [c]
    x3) (ListN [d]
    x4) = [(a, b, c, d)] -> ListN n (a, b, c, d)
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
    forall {a} {b} {c} {d}. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
    loop [a]
    x1 [b]
    x2 [c]
    x3 [d]
    x4)
      where loop :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
    loop (a
    l1:[a]
    l1s) (b
    l2:[b]
    l2s) (c
    l3:[c]
    l3s) (d
    l4:[d]
    l4s) = (a
    l1,b
    l2,c
    l3,d
    l4) (a, b, c, d) -> [(a, b, c, d)] -> [(a, b, c, d)]
    forall a. a -> [a] -> [a]
    : [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
    loop [a]
    l1s [b]
    l2s [c]
    l3s [d]
    l4s
            loop []       [b]
    _        [c]
    _        [d]
    _        = []
            loop [a]
    _        [b]
    _        [c]
    _        [d]
    _        = [(a, b, c, d)]
    forall a. HasCallStack => a
    impossible

    -- | Zip 5 lists of the same size
    zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
    zip5 :: forall (n :: Nat) a b c d e.
    ListN n a
    -> ListN n b
    -> ListN n c
    -> ListN n d
    -> ListN n e
    -> ListN n (a, b, c, d, e)
    zip5 (ListN [a]
    x1) (ListN [b]
    x2) (ListN [c]
    x3) (ListN [d]
    x4) (ListN [e]
    x5) = [(a, b, c, d, e)] -> ListN n (a, b, c, d, e)
    forall (n :: Nat) a. [a] -> ListN n a
    ListN ([a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
    forall {a} {b} {c} {d} {e}.
    [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
    loop [a]
    x1 [b]
    x2 [c]
    x3 [d]
    x4 [e]
    x5)
      where loop :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
    loop (a
    l1:[a]
    l1s) (b
    l2:[b]
    l2s) (c
    l3:[c]
    l3s) (d
    l4:[d]
    l4s) (e
    l5:[e]
    l5s) = (a
    l1,b
    l2,c
    l3,d
    l4,e
    l5) (a, b, c, d, e) -> [(a, b, c, d, e)] -> [(a, b, c, d, e)]
    forall a. a -> [a] -> [a]
    : [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
    loop [a]
    l1s [b]
    l2s [c]
    l3s [d]
    l4s [e]
    l5s
            loop []       [b]
    _        [c]
    _        [d]
    _        [e]
    _        = []
            loop [a]
    _        [b]
    _        [c]
    _        [d]
    _        [e]
    _        = [(a, b, c, d, e)]
    forall a. HasCallStack => a
    impossible

    -- | Zip 2 lists using a function
    zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
    zipWith :: forall a b x (n :: Nat).
    (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
    zipWith a -> b -> x
    f (ListN (a
    v1:[a]
    vs)) (ListN (b
    w1:[b]
    ws)) = [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (a -> b -> x
    f a
    v1 b
    w1 x -> [x] -> [x]
    forall a. a -> [a] -> [a]
    : ListN (ZonkAny 0) x -> [x]
    forall (n :: Nat) a. ListN n a -> [a]
    unListN ((a -> b -> x)
    -> ListN (ZonkAny 0) a
    -> ListN (ZonkAny 0) b
    -> ListN (ZonkAny 0) x
    forall a b x (n :: Nat).
    (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
    zipWith a -> b -> x
    f ([a] -> ListN (ZonkAny 0) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    vs) ([b] -> ListN (ZonkAny 0) b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [b]
    ws)))
    zipWith a -> b -> x
    _ (ListN [])       ListN n b
    _ = [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []
    zipWith a -> b -> x
    _ ListN n a
    _                ListN n b
    _ = ListN n x
    forall a. HasCallStack => a
    impossible

    -- | Zip 3 lists using a function
    zipWith3 :: (a -> b -> c -> x)
             -> ListN n a
             -> ListN n b
             -> ListN n c
             -> ListN n x
    zipWith3 :: forall a b c x (n :: Nat).
    (a -> b -> c -> x)
    -> ListN n a -> ListN n b -> ListN n c -> ListN n x
    zipWith3 a -> b -> c -> x
    f (ListN (a
    v1:[a]
    vs)) (ListN (b
    w1:[b]
    ws)) (ListN (c
    x1:[c]
    xs)) =
        [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (a -> b -> c -> x
    f a
    v1 b
    w1 c
    x1 x -> [x] -> [x]
    forall a. a -> [a] -> [a]
    : ListN (ZonkAny 1) x -> [x]
    forall (n :: Nat) a. ListN n a -> [a]
    unListN ((a -> b -> c -> x)
    -> ListN (ZonkAny 1) a
    -> ListN (ZonkAny 1) b
    -> ListN (ZonkAny 1) c
    -> ListN (ZonkAny 1) x
    forall a b c x (n :: Nat).
    (a -> b -> c -> x)
    -> ListN n a -> ListN n b -> ListN n c -> ListN n x
    zipWith3 a -> b -> c -> x
    f ([a] -> ListN (ZonkAny 1) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    vs) ([b] -> ListN (ZonkAny 1) b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [b]
    ws) ([c] -> ListN (ZonkAny 1) c
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [c]
    xs)))
    zipWith3 a -> b -> c -> x
    _ (ListN []) ListN n b
    _       ListN n c
    _ = [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []
    zipWith3 a -> b -> c -> x
    _ ListN n a
    _          ListN n b
    _       ListN n c
    _ = ListN n x
    forall a. HasCallStack => a
    impossible

    -- | Zip 4 lists using a function
    zipWith4 :: (a -> b -> c -> d -> x)
             -> ListN n a
             -> ListN n b
             -> ListN n c
             -> ListN n d
             -> ListN n x
    zipWith4 :: forall a b c d x (n :: Nat).
    (a -> b -> c -> d -> x)
    -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
    zipWith4 a -> b -> c -> d -> x
    f (ListN (a
    v1:[a]
    vs)) (ListN (b
    w1:[b]
    ws)) (ListN (c
    x1:[c]
    xs)) (ListN (d
    y1:[d]
    ys)) =
        [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (a -> b -> c -> d -> x
    f a
    v1 b
    w1 c
    x1 d
    y1 x -> [x] -> [x]
    forall a. a -> [a] -> [a]
    : ListN (ZonkAny 2) x -> [x]
    forall (n :: Nat) a. ListN n a -> [a]
    unListN ((a -> b -> c -> d -> x)
    -> ListN (ZonkAny 2) a
    -> ListN (ZonkAny 2) b
    -> ListN (ZonkAny 2) c
    -> ListN (ZonkAny 2) d
    -> ListN (ZonkAny 2) x
    forall a b c d x (n :: Nat).
    (a -> b -> c -> d -> x)
    -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
    zipWith4 a -> b -> c -> d -> x
    f ([a] -> ListN (ZonkAny 2) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    vs) ([b] -> ListN (ZonkAny 2) b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [b]
    ws) ([c] -> ListN (ZonkAny 2) c
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [c]
    xs) ([d] -> ListN (ZonkAny 2) d
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [d]
    ys)))
    zipWith4 a -> b -> c -> d -> x
    _ (ListN []) ListN n b
    _       ListN n c
    _       ListN n d
    _ = [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []
    zipWith4 a -> b -> c -> d -> x
    _ ListN n a
    _          ListN n b
    _       ListN n c
    _       ListN n d
    _ = ListN n x
    forall a. HasCallStack => a
    impossible

    -- | Zip 5 lists using a function
    zipWith5 :: (a -> b -> c -> d -> e -> x)
             -> ListN n a
             -> ListN n b
             -> ListN n c
             -> ListN n d
             -> ListN n e
             -> ListN n x
    zipWith5 :: forall a b c d e x (n :: Nat).
    (a -> b -> c -> d -> e -> x)
    -> ListN n a
    -> ListN n b
    -> ListN n c
    -> ListN n d
    -> ListN n e
    -> ListN n x
    zipWith5 a -> b -> c -> d -> e -> x
    f (ListN (a
    v1:[a]
    vs)) (ListN (b
    w1:[b]
    ws)) (ListN (c
    x1:[c]
    xs)) (ListN (d
    y1:[d]
    ys)) (ListN (e
    z1:[e]
    zs)) =
        [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN (a -> b -> c -> d -> e -> x
    f a
    v1 b
    w1 c
    x1 d
    y1 e
    z1 x -> [x] -> [x]
    forall a. a -> [a] -> [a]
    : ListN (ZonkAny 3) x -> [x]
    forall (n :: Nat) a. ListN n a -> [a]
    unListN ((a -> b -> c -> d -> e -> x)
    -> ListN (ZonkAny 3) a
    -> ListN (ZonkAny 3) b
    -> ListN (ZonkAny 3) c
    -> ListN (ZonkAny 3) d
    -> ListN (ZonkAny 3) e
    -> ListN (ZonkAny 3) x
    forall a b c d e x (n :: Nat).
    (a -> b -> c -> d -> e -> x)
    -> ListN n a
    -> ListN n b
    -> ListN n c
    -> ListN n d
    -> ListN n e
    -> ListN n x
    zipWith5 a -> b -> c -> d -> e -> x
    f ([a] -> ListN (ZonkAny 3) a
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [a]
    vs) ([b] -> ListN (ZonkAny 3) b
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [b]
    ws) ([c] -> ListN (ZonkAny 3) c
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [c]
    xs) ([d] -> ListN (ZonkAny 3) d
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [d]
    ys) ([e] -> ListN (ZonkAny 3) e
    forall (n :: Nat) a. [a] -> ListN n a
    ListN [e]
    zs)))
    zipWith5 a -> b -> c -> d -> e -> x
    _ (ListN []) ListN n b
    _       ListN n c
    _       ListN n d
    _       ListN n e
    _ = [x] -> ListN n x
    forall (n :: Nat) a. [a] -> ListN n a
    ListN []
    zipWith5 a -> b -> c -> d -> e -> x
    _ ListN n a
    _          ListN n b
    _       ListN n c
    _       ListN n d
    _       ListN n e
    _ = ListN n x
    forall a. HasCallStack => a
    impossible