{-# 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