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

-- | Strict variant of NS
--
-- See [@sop-core@'s
-- NS](https://hackage.haskell.org/package/sop-core/docs/Data-SOP-NS.html).
module Data.SOP.Strict.NS (
    -- * NS
    NS (..)
  , index_NS
  , partition_NS
  , sequence_NS'
  , unZ
    -- * Injections
  , Injection
  , injections
  ) where

import           Data.Coerce
import           Data.Kind
import           Data.SOP hiding (Injection, NP (..), NS (..), injections,
                     shiftInjection, unZ)
import           Data.SOP.Classes
import           Data.SOP.Constraint
import           Data.SOP.Strict.NP
import           NoThunks.Class

type NS :: (k -> Type) -> [k] -> Type
data NS f xs where
  Z :: !(f x) -> NS f (x ': xs)
  S :: !(NS f xs) -> NS f (x ': xs)

type instance CollapseTo NS a = a
type instance AllN       NS c = All c
type instance Prod       NS   = NP
type instance SListIN    NS   = SListI
type instance Same       NS   = NS

unZ :: NS f '[x] -> f x
unZ :: forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ (Z f x
x) = f x
f x
x

index_NS :: forall f xs . NS f xs -> Int
index_NS :: forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Int
index_NS = Int -> NS f xs -> Int
forall (ys :: [k]). Int -> NS f ys -> Int
go Int
0
  where
    go :: forall ys . Int -> NS f ys -> Int
    go :: forall (ys :: [k]). Int -> NS f ys -> Int
go !Int
acc (Z f x
_) = Int
acc
    go !Int
acc (S NS f xs
x) = Int -> NS f xs -> Int
forall (ys :: [k]). Int -> NS f ys -> Int
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NS f xs
x

expand_NS :: SListI xs => (forall x. f x) -> NS f xs -> NP f xs
expand_NS :: forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (x :: k). f x) -> NS f xs -> NP f xs
expand_NS = Proxy Top -> (forall (x :: k). Top x => f x) -> NS f xs -> NP f xs
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (xs :: [k]).
All c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

cexpand_NS :: forall c proxy f xs. All c xs
           => proxy c -> (forall x. c x => f x) -> NS f xs -> NP f xs
cexpand_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (xs :: [k]).
All c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS proxy c
p forall (x :: k). c x => f x
d = NS f xs -> NP f xs
forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs'
go
  where
    go :: forall xs'. All c xs' => NS f xs' -> NP f xs'
    go :: forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs'
go (Z f x
x) = f x
x f x -> NP f xs -> NP f (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* proxy c -> (forall (x :: k). c x => f x) -> NP f 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
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure proxy c
p f a
forall (x :: k). c x => f x
d
    go (S NS f xs
i) = f x
forall (x :: k). c x => f x
d f x -> NP f xs -> NP f (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NS f xs -> NP f xs
forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs'
go NS f xs
i

ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS = NP (f -.-> g) xs -> NS f xs -> NS g xs
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
go
  where
    go :: NP (f -.-> g) xs -> NS f xs -> NS g xs
    go :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
go ((-.->) f g x
f :* NP (f -.-> g) xs1
_)  (Z f x
x)  = g x -> NS g (x : xs1)
forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
f xs -> NS f (xs : x)
Z (g x -> NS g (x : xs1)) -> g x -> NS g (x : xs1)
forall a b. (a -> b) -> a -> b
$ (-.->) f g x -> f x -> g x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f g x
f f x
f x
x
    go ((-.->) f g x
_ :* NP (f -.-> g) xs1
fs) (S NS f xs
xs) = NS g xs1 -> NS g (x : xs1)
forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
NS f xs -> NS f (x : xs)
S (NS g xs1 -> NS g (x : xs1)) -> NS g xs1 -> NS g (x : xs1)
forall a b. (a -> b) -> a -> b
$ NP (f -.-> g) xs1 -> NS f xs1 -> NS g xs1
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
go NP (f -.-> g) xs1
fs NS f xs1
NS f xs
xs
    go NP (f -.-> g) xs
Nil       NS f xs
x      = case NS f xs
x of {}

collapse_NS :: NS (K a) xs -> a
collapse_NS :: forall {k} a (xs :: [k]). NS (K a) xs -> a
collapse_NS = NS (K a) xs -> a
forall {k} a (xs :: [k]). NS (K a) xs -> a
go
  where
    go :: NS (K a) xs  -> a
    go :: forall {k} a (xs :: [k]). NS (K a) xs -> a
go (Z (K a
x)) = a
x
    go (S NS (K a) xs
xs)    = NS (K a) xs -> a
forall {k} a (xs :: [k]). NS (K a) xs -> a
go NS (K a) xs
xs

ctraverse'_NS  :: forall c proxy xs f f' g. (All c xs,  Functor g)
               => proxy c
               -> (forall a. c a => f a -> g (f' a))
               -> NS f xs  -> g (NS f' xs)
ctraverse'_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Functor g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
ctraverse'_NS proxy c
_ forall (a :: k). c a => f a -> g (f' a)
f = NS f xs -> g (NS f' xs)
forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
go
  where
    go :: All c ys => NS f ys -> g (NS f' ys)
    go :: forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
go (Z f x
x)  = f' x -> NS f' ys
f' x -> NS f' (x : xs)
forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
f xs -> NS f (xs : x)
Z (f' x -> NS f' ys) -> g (f' x) -> g (NS f' ys)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g (f' x)
forall (a :: k). c a => f a -> g (f' a)
f f x
x
    go (S NS f xs
xs) = NS f' xs -> NS f' ys
NS f' xs -> NS f' (x : xs)
forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
NS f xs -> NS f (x : xs)
S (NS f' xs -> NS f' ys) -> g (NS f' xs) -> g (NS f' ys)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NS f xs -> g (NS f' xs)
forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
go NS f xs
xs

trans_NS :: forall proxy c f g xs ys. AllZip c xs ys
         => proxy c
         -> (forall x y . c x y => f x -> g y)
         -> NS f xs -> NS g ys
trans_NS :: forall {k} {k} (proxy :: (k -> k -> Constraint) -> *)
       (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k])
       (ys :: [k]).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS proxy c
_ forall (x :: k) (y :: k). c x y => f x -> g y
t = NS f xs -> NS g ys
forall (xs' :: [k]) (ys' :: [k]).
AllZip c xs' ys' =>
NS f xs' -> NS g ys'
go
  where
    go :: AllZip c xs' ys' => NS f xs' -> NS g ys'
    go :: forall (xs' :: [k]) (ys' :: [k]).
AllZip c xs' ys' =>
NS f xs' -> NS g ys'
go (Z f x
x) = g (Head ys') -> NS g (Head ys' : Tail ys')
forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
f xs -> NS f (xs : x)
Z (f x -> g (Head ys')
forall (x :: k) (y :: k). c x y => f x -> g y
t f x
x)
    go (S NS f xs
x) = NS g (Tail ys') -> NS g (Head ys' : Tail ys')
forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
NS f xs -> NS f (x : xs)
S (NS f xs -> NS g (Tail ys')
forall (xs' :: [k]) (ys' :: [k]).
AllZip c xs' ys' =>
NS f xs' -> NS g ys'
go NS f xs
x)

-- NOTE: @sop-core@ defines this in terms of @unsafeCoerce@. Currently we
-- don't make much use of this function, so I prefer this more strongly
-- typed version.
coerce_NS :: forall f g xs ys. AllZip (LiftedCoercible f g) xs ys
          => NS f xs -> NS g ys
coerce_NS :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NS f xs -> NS g ys
coerce_NS = Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> NS f xs
-> NS g ys
forall {k} {k} (proxy :: (k -> k -> Constraint) -> *)
       (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k])
       (ys :: [k]).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS (forall {k} (t :: k). Proxy t
forall (t :: k -> k -> Constraint). Proxy t
Proxy @(LiftedCoercible f g)) f x -> g y
forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
forall a b. Coercible a b => a -> b
coerce

-- | 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' :: forall {k} (xs :: [k]) (f :: * -> *) (g :: k -> *).
Functor f =>
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 :: forall (xs' :: [k]). NS (f :.: g) xs' -> f (NS g xs')
go (Z (Comp f (g x)
fx)) = g x -> NS g xs'
g x -> NS g (x : xs)
forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
f xs -> NS f (xs : x)
Z (g x -> NS g xs') -> f (g x) -> f (NS g 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 xs'
NS g xs -> NS g (x : xs)
forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
NS f xs -> NS f (x : xs)
S (NS g xs -> NS g xs') -> f (NS g xs) -> f (NS g 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

partition_NS :: forall xs f. SListI xs => [NS f xs] -> NP ([] :.: f) xs
partition_NS :: forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
[NS f xs] -> NP ([] :.: f) xs
partition_NS =
  (NS f xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs)
-> NP ([] :.: f) xs -> [NS f xs] -> NP ([] :.: f) xs
forall a b. (a -> b -> b) -> b -> [a] -> b
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 (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a
forall (a :: k). (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a
append (NP ([] :.: f) xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs)
-> (NS f xs -> NP ([] :.: f) xs)
-> NS f xs
-> NP ([] :.: f) xs
-> NP ([] :.: f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). (:.:) [] f x)
-> NS ([] :.: f) xs -> Prod NS ([] :.: f) xs
forall (xs :: [k]) (f :: k -> *).
SListIN (Prod NS) xs =>
(forall (x :: k). f x) -> 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 (:.:) [] f x
forall (x :: k). (:.:) [] f x
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 f a -> (:.:) [] f a
forall (a :: k). f a -> (:.:) [] f a
singleton) ((forall (x :: k). (:.:) [] f x) -> NP ([] :.: f) xs
forall (xs :: [k]) (f :: k -> *).
SListIN NP xs =>
(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 (:.:) [] f a
forall (x :: k). (:.:) [] f x
nil)
  where
    nil :: ([] :.: f) a
    nil :: forall (x :: k). (:.:) [] f x
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 :: forall (a :: k). 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 :: forall (a :: k). (:.:) [] 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')

instance HExpand NS where
  hexpand :: forall (xs :: [k]) (f :: k -> *).
SListIN (Prod NS) xs =>
(forall (x :: k). f x) -> NS f xs -> Prod NS f xs
hexpand  = (forall (x :: k). f x) -> NS f xs -> Prod NS f xs
(forall (x :: k). f x) -> NS f xs -> NP f xs
forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (x :: k). f x) -> NS f xs -> NP f xs
expand_NS
  hcexpand :: forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN (Prod NS) c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
hcexpand = proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (xs :: [k]).
All c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS

instance HAp NS where
  hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
hap = Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
NP (f -.-> g) xs -> NS f xs -> NS g xs
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS

instance HCollapse NS where
  hcollapse :: forall (xs :: [k]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
hcollapse = NS (K a) xs -> a
NS (K a) xs -> CollapseTo NS a
forall {k} a (xs :: [k]). NS (K a) xs -> a
collapse_NS

instance HSequence NS where
  hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
(AllN NS c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Functor g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
ctraverse'_NS
  htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
(SListIN NS xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
htraverse'  = Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> h f xs
-> g (h f' xs)
forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
(AllN NS c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
hctraverse' (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)
  hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *).
(SListIN NS xs, Applicative f) =>
NS (f :.: g) xs -> f (NS g xs)
hsequence'  = (forall (a :: k). (:.:) f g a -> f (g a))
-> NS (f :.: g) xs -> f (NS g xs)
forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
(SListIN NS xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, SListIN h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
htraverse' (:.:) f g a -> f (g a)
forall (a :: k). (:.:) f g a -> f (g a)
forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp

instance HTrans NS NS where
  htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2])
       (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
       (g :: k2 -> *).
AllZipN (Prod NS) c xs ys =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NS f xs
-> NS g ys
htrans  = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NS f xs
-> NS g ys
forall {k} {k} (proxy :: (k -> k -> Constraint) -> *)
       (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k])
       (ys :: [k]).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS
  hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [k1]) (ys :: [k2]).
AllZipN (Prod NS) (LiftedCoercible f g) xs ys =>
NS f xs -> NS g ys
hcoerce = NS f xs -> NS g ys
forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NS f xs -> NS g ys
coerce_NS

deriving instance All (Show `Compose` f) xs => Show (NS f xs)
deriving instance All (Eq   `Compose` f) xs => Eq   (NS f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)

instance All (Compose NoThunks f) xs
      => NoThunks (NS (f :: k -> Type) (xs :: [k])) where
  showTypeOf :: Proxy (NS f xs) -> String
showTypeOf Proxy (NS f xs)
_ = String
"NS"
  wNoThunks :: Context -> NS f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt = \case
      Z f x
l -> Context -> f x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"Z" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) f x
l
      S NS f xs
r -> Context -> NS f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"S" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) NS f xs
r

{-------------------------------------------------------------------------------
  Injections
-------------------------------------------------------------------------------}

type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)

injections :: forall xs f. SListI xs => NP (Injection f xs) xs
injections :: forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
NP (Injection f xs) xs
injections = SList xs -> NP (Injection f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: SList xs' -> NP (Injection f xs') xs'
    go :: forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs'
go SList xs'
SNil  = NP (Injection f xs') xs'
NP (Injection f xs') '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = (f x -> K (NS f xs') x) -> (-.->) f (K (NS f xs')) x
forall {k} (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn (NS f xs' -> K (NS f xs') x
forall k a (b :: k). a -> K a b
K (NS f xs' -> K (NS f xs') x)
-> (f x -> NS f xs') -> f x -> K (NS f xs') x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> NS f xs'
f x -> NS f (x : xs)
forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
f xs -> NS f (xs : x)
Z) (-.->) f (K (NS f xs')) x
-> NP (Injection f xs') xs -> NP (Injection f xs') (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* (forall (a :: k). Injection f xs a -> Injection f xs' a)
-> NP (Injection f xs) xs -> NP (Injection f 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 (-.->) f (K (NS f xs)) a -> (-.->) f (K (NS f xs')) a
(-.->) f (K (NS f xs)) a -> Injection f (x : xs) a
forall (a :: k). Injection f xs a -> Injection f xs' a
forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
Injection f xs a -> Injection f (x : xs) a
shiftInjection (SList xs -> NP (Injection f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList)

shiftInjection :: Injection f xs a -> Injection f (x ': xs) a
shiftInjection :: forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
Injection f xs a -> Injection f (x : xs) a
shiftInjection (Fn f a -> K (NS f xs) a
f) = (f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a)
-> (f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a
forall a b. (a -> b) -> a -> b
$ NS f (x : xs) -> K (NS f (x : xs)) a
forall k a (b :: k). a -> K a b
K (NS f (x : xs) -> K (NS f (x : xs)) a)
-> (f a -> NS f (x : xs)) -> f a -> K (NS f (x : xs)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS f xs -> NS f (x : xs)
forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
NS f xs -> NS f (x : xs)
S (NS f xs -> NS f (x : xs))
-> (f a -> NS f xs) -> f a -> NS f (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K (NS f xs) a -> NS f xs
forall {k} a (b :: k). K a b -> a
unK (K (NS f xs) a -> NS f xs)
-> (f a -> K (NS f xs) a) -> f a -> NS f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> K (NS f xs) a
f