{-# 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
    sequence_NS'
  , map_NP'
  , partition_NS
  , npWithIndices
  , nsToIndex
  , nsFromIndex
  , Lens(..)
  , lenses_NP
  , npToSListI
  , allComposeShowK
  , fn_5
    -- * Type-level non-empty lists
  , IsNonEmpty(..)
  , ProofNonEmpty(..)
  , checkIsNonEmpty
  ) where

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 :: [Type] -> 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 x (xs :: [*]). 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 x (xs :: [*]). 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