{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Ouroboros.Consensus.Util.SOP (
    -- * Minor variations on standard SOP operators
    Lens (..)
  , allComposeShowK
  , fn_5
  , lenses_NP
  , map_NP'
  , npToSListI
  , npWithIndices
  , nsFromIndex
  , nsToIndex
  , partition_NS
  , sequence_NS'
    -- * Type-level non-empty lists
  , IsNonEmpty (..)
  , ProofNonEmpty (..)
  , checkIsNonEmpty
    -- * Indexing SOP types
  , Index (..)
  , dictIndexAll
  , indices
  , injectNS
  , injectNS'
  , projectNP
    -- * Zipping with indices
  , hcimap
  , hcizipWith
  , hcizipWith3
  , hcizipWith4
  , himap
  , hizipWith
  , hizipWith3
  , hizipWith4
  ) where

import           Data.Coerce
import           Data.Kind (Type)
import           Data.SOP.Dict
import           Data.SOP.Strict
import           Data.Word

{-------------------------------------------------------------------------------
  Minor variations on standard SOP operators
-------------------------------------------------------------------------------}

-- | Version of 'sequence_NS' that requires only 'Functor'
--
-- The version in the library requires 'Applicative', which is unnecessary.
sequence_NS' :: forall xs f g. Functor f
             => NS (f :.: g) xs -> f (NS g xs)
sequence_NS' :: NS (f :.: g) xs -> f (NS g xs)
sequence_NS' = NS (f :.: g) xs -> f (NS g xs)
forall (xs' :: [k]). NS (f :.: g) xs' -> f (NS g xs')
go
  where
    go :: NS (f :.: g) xs' -> f (NS g xs')
    go :: NS (f :.: g) xs' -> f (NS g xs')
go (Z (Comp f (g x)
fx)) = g x -> NS g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (g x -> NS g (x : xs)) -> f (g x) -> f (NS g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g x)
fx
    go (S NS (f :.: g) xs
r)         = NS g xs -> NS g (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS g xs -> NS g (x : xs)) -> f (NS g xs) -> f (NS g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NS (f :.: g) xs -> f (NS g xs)
forall (xs' :: [k]). NS (f :.: g) xs' -> f (NS g xs')
go NS (f :.: g) xs
r

-- | Version of 'map_NP' that does not require a singleton
map_NP' :: forall f g xs. (forall a. f a -> g a) -> NP f xs -> NP g xs
map_NP' :: (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
map_NP' forall (a :: k). f a -> g a
f = NP f xs -> NP g xs
forall (xs' :: [k]). NP f xs' -> NP g xs'
go
  where
    go :: NP f xs' -> NP g xs'
    go :: NP f xs' -> NP g xs'
go NP f xs'
Nil       = NP g xs'
forall k (f :: k -> *). NP f '[]
Nil
    go (f x
x :* NP f xs
xs) = f x -> g x
forall (a :: k). f a -> g a
f f x
x g x -> NP g xs -> NP g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP f xs -> NP g xs
forall (xs' :: [k]). NP f xs' -> NP g xs'
go NP f xs
xs

partition_NS :: forall xs f. SListI xs => [NS f xs] -> NP ([] :.: f) xs
partition_NS :: [NS f xs] -> NP ([] :.: f) xs
partition_NS =
      (NP ([] :.: f) xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs)
-> NP ([] :.: f) xs -> [NP ([] :.: f) xs] -> NP ([] :.: f) xs
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((forall (a :: k). (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a)
-> Prod NP ([] :.: f) xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith forall (a :: k). (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a
append) ((forall (a :: k). (:.:) [] f a) -> NP ([] :.: f) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall (a :: k). (:.:) [] f a
nil)
    ([NP ([] :.: f) xs] -> NP ([] :.: f) xs)
-> ([NS f xs] -> [NP ([] :.: f) xs])
-> [NS f xs]
-> NP ([] :.: f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NS f xs -> NP ([] :.: f) xs) -> [NS f xs] -> [NP ([] :.: f) xs]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (a :: k). (:.:) [] f a)
-> NS ([] :.: f) xs -> Prod NS ([] :.: f) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HExpand h, SListIN (Prod h) xs) =>
(forall (x :: k). f x) -> h f xs -> Prod h f xs
hexpand forall (a :: k). (:.:) [] f a
nil (NS ([] :.: f) xs -> NP ([] :.: f) xs)
-> (NS f xs -> NS ([] :.: f) xs) -> NS f xs -> NP ([] :.: f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). f a -> (:.:) [] f a)
-> NS f xs -> NS ([] :.: f) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall (a :: k). f a -> (:.:) [] f a
singleton)
  where
    nil :: ([] :.: f) a
    nil :: (:.:) [] f a
nil = [f a] -> (:.:) [] f a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp []

    singleton :: f a -> ([] :.: f) a
    singleton :: f a -> (:.:) [] f a
singleton = [f a] -> (:.:) [] f a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp ([f a] -> (:.:) [] f a) -> (f a -> [f a]) -> f a -> (:.:) [] f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> [f a] -> [f a]
forall a. a -> [a] -> [a]
:[])

    append :: ([] :.: f) a -> ([] :.: f) a -> ([] :.: f) a
    append :: (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a
append (Comp [f a]
as) (Comp [f a]
as') = [f a] -> (:.:) [] f a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp ([f a]
as [f a] -> [f a] -> [f a]
forall a. [a] -> [a] -> [a]
++ [f a]
as')

-- | We only allow up to 23 (so counting from 0, 24 elements in @xs@), because
-- CBOR stores a 'Word8' in the range 0-23 as a single byte equal to the value
-- of the 'Word8'. We rely on this in 'reconstructNestedCtxt' and other
-- places.
npWithIndices :: SListI xs => NP (K Word8) xs
npWithIndices :: NP (K Word8) xs
npWithIndices = Word8 -> SList xs -> NP (K Word8) xs
forall k (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs'
go Word8
0 SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: Word8 -> SList xs' -> NP (K Word8) xs'
    go :: Word8 -> SList xs' -> NP (K Word8) xs'
go !Word8
_ SList xs'
SNil  = NP (K Word8) xs'
forall k (f :: k -> *). NP f '[]
Nil
    go Word8
24 SList xs'
SCons = [Char] -> NP (K Word8) xs'
forall a. HasCallStack => [Char] -> a
error [Char]
"npWithIndices out of range"
    go !Word8
i SList xs'
SCons = Word8 -> K Word8 x
forall k a (b :: k). a -> K a b
K Word8
i K Word8 x -> NP (K Word8) xs -> NP (K Word8) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* Word8 -> SList xs -> NP (K Word8) xs
forall k (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs'
go (Word8
i Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList

nsToIndex :: SListI xs => NS f xs -> Word8
nsToIndex :: NS f xs -> Word8
nsToIndex = NS (K Word8) xs -> Word8
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K Word8) xs -> Word8)
-> (NS f xs -> NS (K Word8) xs) -> NS f xs -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). K Word8 a -> f a -> K Word8 a)
-> Prod NS (K Word8) xs -> NS f xs -> NS (K Word8) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith forall (a :: k). K Word8 a -> f a -> K Word8 a
forall a b. a -> b -> a
const Prod NS (K Word8) xs
forall k (xs :: [k]). SListI xs => NP (K Word8) xs
npWithIndices

-- | We only allow up to 23, see 'npWithIndices'.
nsFromIndex :: SListI xs => Word8 -> Maybe (NS (K ()) xs)
nsFromIndex :: Word8 -> Maybe (NS (K ()) xs)
nsFromIndex Word8
n = Word8 -> SList xs -> Maybe (NS (K ()) xs)
forall k (xs' :: [k]). Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go Word8
0 SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: Word8 -> SList xs' -> Maybe (NS (K ()) xs')
    go :: Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go !Word8
i SList xs'
SCons
      | Word8
i Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
24   = [Char] -> Maybe (NS (K ()) xs')
forall a. HasCallStack => [Char] -> a
error [Char]
"nsFromIndex out of range"
      | Word8
i Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
n    = NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs))
forall a. a -> Maybe a
Just (NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs)))
-> NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs))
forall a b. (a -> b) -> a -> b
$ K () x -> NS (K ()) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (K () x -> NS (K ()) (x : xs)) -> K () x -> NS (K ()) (x : xs)
forall a b. (a -> b) -> a -> b
$ () -> K () x
forall k a (b :: k). a -> K a b
K ()
      | Bool
otherwise = NS (K ()) xs -> NS (K ()) (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS (K ()) xs -> NS (K ()) (x : xs))
-> Maybe (NS (K ()) xs) -> Maybe (NS (K ()) (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word8 -> SList xs -> Maybe (NS (K ()) xs)
forall k (xs' :: [k]). Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go (Word8
i Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
    go !Word8
_ SList xs'
SNil    = Maybe (NS (K ()) xs')
forall a. Maybe a
Nothing

-- | Simple lens to access an element of an n-ary product.
data Lens f xs a = Lens {
      Lens f xs a -> NP f xs -> f a
getter :: NP f xs -> f a
    , Lens f xs a -> f a -> NP f xs -> NP f xs
setter :: f a -> NP f xs -> NP f xs
    }

-- | Generate all lenses to access the element of an n-ary product.
lenses_NP :: forall f xs. SListI xs => NP (Lens f xs) xs
lenses_NP :: NP (Lens f xs) xs
lenses_NP = SList xs -> NP (Lens f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Lens f xs') xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: SList xs' -> NP (Lens f xs') xs'
    go :: SList xs' -> NP (Lens f xs') xs'
go SList xs'
SNil  = NP (Lens f xs') xs'
forall k (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = Lens f (x : xs) x
forall (x :: k) (xs' :: [k]). Lens f (x : xs') x
lensFirst Lens f (x : xs) x
-> NP (Lens f (x : xs)) xs -> NP (Lens f (x : xs)) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* (forall (a :: k). Lens f xs a -> Lens f (x : xs) a)
-> NP (Lens f xs) xs -> NP (Lens f (x : xs)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall (a :: k). Lens f xs a -> Lens f (x : xs) a
forall (xs' :: [k]) (a :: k) (x :: k).
Lens f xs' a -> Lens f (x : xs') a
shiftLens (SList xs -> NP (Lens f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Lens f xs') xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList)

    lensFirst :: Lens f (x ': xs') x
    lensFirst :: Lens f (x : xs') x
lensFirst = Lens :: forall k (f :: k -> *) (xs :: [k]) (a :: k).
(NP f xs -> f a) -> (f a -> NP f xs -> NP f xs) -> Lens f xs a
Lens {
          getter :: NP f (x : xs') -> f x
getter = NP f (x : xs') -> f x
forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd
        , setter :: f x -> NP f (x : xs') -> NP f (x : xs')
setter = \f x
a' (f x
_ :* NP f xs
as) -> f x
a' f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP f xs
as
        }

    shiftLens :: Lens f xs' a -> Lens f (x ': xs') a
    shiftLens :: Lens f xs' a -> Lens f (x : xs') a
shiftLens Lens f xs' a
l = Lens :: forall k (f :: k -> *) (xs :: [k]) (a :: k).
(NP f xs -> f a) -> (f a -> NP f xs -> NP f xs) -> Lens f xs a
Lens {
          getter :: NP f (x : xs') -> f a
getter = Lens f xs' a -> NP f xs' -> f a
forall k (f :: k -> *) (xs :: [k]) (a :: k).
Lens f xs a -> NP f xs -> f a
getter Lens f xs' a
l (NP f xs' -> f a)
-> (NP f (x : xs') -> NP f xs') -> NP f (x : xs') -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP f (x : xs') -> NP f xs'
forall k (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl
        , setter :: f a -> NP f (x : xs') -> NP f (x : xs')
setter = \f a
a' (f x
a :* NP f xs
as) -> f x
a f x -> NP f xs' -> NP f (x : xs')
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* Lens f xs' a -> f a -> NP f xs' -> NP f xs'
forall k (f :: k -> *) (xs :: [k]) (a :: k).
Lens f xs a -> f a -> NP f xs -> NP f xs
setter Lens f xs' a
l f a
a' NP f xs'
NP f xs
as
        }

-- | Conjure up an 'SListI' constraint from an 'NP'
npToSListI :: NP a xs -> (SListI xs => r) -> r
npToSListI :: NP a xs -> (SListI xs => r) -> r
npToSListI NP a xs
np = SList xs -> (SListI xs => r) -> r
forall k (xs :: [k]) r. SList xs -> (SListI xs => r) -> r
sListToSListI (SList xs -> (SListI xs => r) -> r)
-> SList xs -> (SListI xs => r) -> r
forall a b. (a -> b) -> a -> b
$ NP a xs -> SList xs
forall k (a :: k -> *) (xs :: [k]). NP a xs -> SList xs
npToSList NP a xs
np
  where
    sListToSListI :: SList xs -> (SListI xs => r) -> r
    sListToSListI :: SList xs -> (SListI xs => r) -> r
sListToSListI SList xs
SNil  SListI xs => r
k = r
SListI xs => r
k
    sListToSListI SList xs
SCons SListI xs => r
k = r
SListI xs => r
k

    npToSList :: NP a xs -> SList xs
    npToSList :: NP a xs -> SList xs
npToSList NP a xs
Nil       = SList xs
forall k. SList '[]
SNil
    npToSList (a x
_ :* NP a xs
xs) = SList xs -> (SListI xs => SList xs) -> SList xs
forall k (xs :: [k]) r. SList xs -> (SListI xs => r) -> r
sListToSListI (NP a xs -> SList xs
forall k (a :: k -> *) (xs :: [k]). NP a xs -> SList xs
npToSList NP a xs
xs) SListI xs => SList xs
forall k (xs :: [k]) (x :: k). SListI xs => SList (x : xs)
SCons

allComposeShowK :: (SListI xs, Show a)
                => Proxy xs -> Proxy a -> Dict (All (Compose Show (K a))) xs
allComposeShowK :: Proxy xs -> Proxy a -> Dict (All (Compose Show (K a))) xs
allComposeShowK Proxy xs
_ Proxy a
_ = NP (Dict (Compose Show (K a))) xs
-> Dict (All (Compose Show (K a))) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (NP (Dict (Compose Show (K a))) xs
 -> Dict (All (Compose Show (K a))) xs)
-> NP (Dict (Compose Show (K a))) xs
-> Dict (All (Compose Show (K a))) xs
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Dict (Compose Show (K a)) a)
-> NP (Dict (Compose Show (K a))) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall (a :: k). Dict (Compose Show (K a)) a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

fn_5 :: (f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
     -> (f0 -.-> f1 -.-> f2 -.-> f3 -.-> f4 -.-> f5) a
fn_5 :: (f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
fn_5 f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f = (f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a)
-> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a)
 -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a)
-> (f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a)
-> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
forall a b. (a -> b) -> a -> b
$ \f0 a
x0 ->
         (f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a)
-> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a)
 -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a)
-> (f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a)
-> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a
forall a b. (a -> b) -> a -> b
$ \f1 a
x1 ->
         (f2 a -> (-.->) f3 (f4 -.-> f5) a)
-> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f2 a -> (-.->) f3 (f4 -.-> f5) a)
 -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a)
-> (f2 a -> (-.->) f3 (f4 -.-> f5) a)
-> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a
forall a b. (a -> b) -> a -> b
$ \f2 a
x2 ->
         (f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a)
-> (f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a
forall a b. (a -> b) -> a -> b
$ \f3 a
x3 ->
         (f4 a -> f5 a) -> (-.->) f4 f5 a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f4 a -> f5 a) -> (-.->) f4 f5 a)
-> (f4 a -> f5 a) -> (-.->) f4 f5 a
forall a b. (a -> b) -> a -> b
$ \f4 a
x4 ->
         f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f f0 a
x0 f1 a
x1 f2 a
x2 f3 a
x3 f4 a
x4

{-------------------------------------------------------------------------------
  Type-level non-empty lists
-------------------------------------------------------------------------------}

data ProofNonEmpty :: [a] -> Type where
  ProofNonEmpty :: Proxy x -> Proxy xs -> ProofNonEmpty (x ': xs)

class IsNonEmpty xs where
  isNonEmpty :: proxy xs -> ProofNonEmpty xs

instance IsNonEmpty (x ': xs) where
  isNonEmpty :: proxy (x : xs) -> ProofNonEmpty (x : xs)
isNonEmpty proxy (x : xs)
_ = Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall a (x :: a) (xs :: [a]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty (Proxy x
forall k (t :: k). Proxy t
Proxy @x) (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs)

checkIsNonEmpty :: forall xs. SListI xs => Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty :: Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty Proxy xs
_ = case SListI xs => SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList @xs of
    SList xs
SNil  -> Maybe (ProofNonEmpty xs)
forall a. Maybe a
Nothing
    SList xs
SCons -> ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs))
forall a. a -> Maybe a
Just (ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs)))
-> ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs))
forall a b. (a -> b) -> a -> b
$ Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall a (x :: a) (xs :: [a]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty Proxy x
forall k (t :: k). Proxy t
Proxy Proxy xs
forall k (t :: k). Proxy t
Proxy

{-------------------------------------------------------------------------------
  Indexing SOP types
-------------------------------------------------------------------------------}

data Index xs x where
  IZ ::               Index (x ': xs) x
  IS :: Index xs x -> Index (y ': xs) x

indices :: forall xs. SListI xs => NP (Index xs) xs
indices :: NP (Index xs) xs
indices = case SListI xs => SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList @xs of
    SList xs
SNil  -> NP (Index xs) xs
forall k (f :: k -> *). NP f '[]
Nil
    SList xs
SCons -> Index (x : xs) x
forall a (x :: a) (xs :: [a]). Index (x : xs) x
IZ Index (x : xs) x
-> NP (Index (x : xs)) xs -> NP (Index (x : xs)) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* (forall (a :: k). Index xs a -> Index (x : xs) a)
-> NP (Index xs) xs -> NP (Index (x : xs)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall (a :: k). Index xs a -> Index (x : xs) a
forall a (xs :: [a]) (x :: a) (y :: a).
Index xs x -> Index (y : xs) x
IS NP (Index xs) xs
forall k (xs :: [k]). SListI xs => NP (Index xs) xs
indices

dictIndexAll :: All c xs => Proxy c -> Index xs x -> Dict c x
dictIndexAll :: Proxy c -> Index xs x -> Dict c x
dictIndexAll Proxy c
p = \case
    Index xs x
IZ      -> Dict c x
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    IS Index xs x
idx' -> Proxy c -> Index xs x -> Dict c x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
Proxy c -> Index xs x -> Dict c x
dictIndexAll Proxy c
p Index xs x
idx'

injectNS :: forall f x xs. Index xs x -> f x -> NS f xs
injectNS :: Index xs x -> f x -> NS f xs
injectNS Index xs x
idx f x
x = case Index xs x
idx of
    Index xs x
IZ      -> f x -> NS f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z f x
x
    IS Index xs x
idx' -> NS f xs -> NS f (y : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (Index xs x -> f x -> NS f xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS Index xs x
idx' f x
x)

injectNS' ::
     forall f a b x xs. (Coercible a (f x), Coercible b (NS f xs))
  => Proxy f -> Index xs x -> a -> b
injectNS' :: Proxy f -> Index xs x -> a -> b
injectNS' Proxy f
_ Index xs x
idx = NS f xs -> b
coerce (NS f xs -> b) -> (a -> NS f xs) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index xs x -> f x -> NS f xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS @f Index xs x
idx (f x -> NS f xs) -> (a -> f x) -> a -> NS f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f x
coerce

projectNP :: Index xs x -> NP f xs -> f x
projectNP :: Index xs x -> NP f xs -> f x
projectNP Index xs x
IZ        (f x
x :* NP f xs
_) = f x
f x
x
projectNP (IS Index xs x
idx) (f x
_ :* NP f xs
xs) = Index xs x -> NP f xs -> f x
forall k (xs :: [k]) (x :: k) (f :: k -> *).
Index xs x -> NP f xs -> f x
projectNP Index xs x
idx NP f xs
NP f xs
xs

{-------------------------------------------------------------------------------
  Zipping with indices
-------------------------------------------------------------------------------}

hcimap ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a)
  -> h f1 xs
  -> h f2 xs
hcimap :: proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
hcimap proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a
f h f1 xs
xs1 =
    proxy c
-> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> f2) a)
-> NP (Index xs -.-> (f1 -.-> f2)) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a) -> (-.->) (Index xs) (f1 -.-> f2) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 Index xs a -> f1 a -> f2 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a
f)
      Prod NP (Index xs -.-> (f1 -.-> f2)) xs
-> NP (Index xs) xs -> NP (f1 -.-> f2) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP (Index xs) xs
forall k (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod h (f1 -.-> f2) xs -> h f1 xs -> h f2 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f1 xs
xs1

himap ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a)
  -> h f1 xs
  -> h f2 xs
himap :: (forall (a :: k). Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs
himap = Proxy Top
-> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
hcimap (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

hcizipWith ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a)
  -> NP f1 xs
  -> h  f2 xs
  -> h  f3 xs
hcizipWith :: proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
hcizipWith proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a
f NP f1 xs
xs1 h f2 xs
xs2 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
       (f''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
fn_3 Index xs a -> f1 a -> f2 a -> f3 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a
f)
      Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs
-> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> f3)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP (Index xs) xs
forall k (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> f3)) xs -> NP f1 xs -> NP (f2 -.-> f3) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f1 xs
xs1
      Prod h (f2 -.-> f3) xs -> h f2 xs -> h f3 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f2 xs
xs2

hizipWith ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a)
  -> NP f1 xs
  -> h  f2 xs
  -> h  f3 xs
hizipWith :: (forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs -> h f2 xs -> h f3 xs
hizipWith = Proxy Top
-> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
hcizipWith (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

hcizipWith3 ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
  -> NP f1 xs
  -> NP f2 xs
  -> h  f3 xs
  -> h  f4 xs
hcizipWith3 :: proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
hcizipWith3 proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
f NP f1 xs
xs1 NP f2 xs
xs2 h f3 xs
xs3 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
       (f''' :: k -> *) (f'''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a -> f'''' a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a
fn_4 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
f)
      Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs
-> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP (Index xs) xs
forall k (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs
-> NP f1 xs -> NP (f2 -.-> (f3 -.-> f4)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f1 xs
xs1
      Prod NP (f2 -.-> (f3 -.-> f4)) xs -> NP f2 xs -> NP (f3 -.-> f4) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f2 xs
xs2
      Prod h (f3 -.-> f4) xs -> h f3 xs -> h f4 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f3 xs
xs3

hizipWith3 ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
  -> NP f1 xs
  -> NP f2 xs
  -> h  f3 xs
  -> h  f4 xs
hizipWith3 :: (forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs
hizipWith3 = Proxy Top
-> (forall (a :: k).
    Top a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
hcizipWith3 (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

hcizipWith4 ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
  -> NP f1 xs
  -> NP f2 xs
  -> NP f3 xs
  -> h  f4 xs
  -> h  f5 xs
hcizipWith4 :: proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
hcizipWith4 proxy c
p forall (a :: k).
c a =>
Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f NP f1 xs
xs1 NP f2 xs
xs2 NP f3 xs
xs3 h f4 xs
xs4 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
forall k (f0 :: k -> *) (a :: k) (f1 :: k -> *) (f2 :: k -> *)
       (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
fn_5 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
forall (a :: k).
c a =>
Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f)
      Prod
  NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs
-> NP (Index xs) xs
-> NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP (Index xs) xs
forall k (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs
-> NP f1 xs -> NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f1 xs
xs1
      Prod NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs
-> NP f2 xs -> NP (f3 -.-> (f4 -.-> f5)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f2 xs
xs2
      Prod NP (f3 -.-> (f4 -.-> f5)) xs -> NP f3 xs -> NP (f4 -.-> f5) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` NP f3 xs
xs3
      Prod h (f4 -.-> f5) xs -> h f4 xs -> h f5 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f4 xs
xs4

hizipWith4 ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
  -> NP f1 xs
  -> NP f2 xs
  -> NP f3 xs
  -> h  f4 xs
  -> h  f5 xs
hizipWith4 :: (forall (a :: k).
 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs
hizipWith4 = Proxy Top
-> (forall (a :: k).
    Top a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
hcizipWith4 (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)