{-# OPTIONS_GHC -Wno-orphans #-}

{- | Merging multiple Ema sites into one.

    This is implemented in using `sop-core`'s NS and NP types. Use as
    `MultiRoute '[MySite1, MySite2, ...]`.
-}
module Ema.Route.Lib.Multi (
  MultiRoute,
  MultiModel,
) where

import Data.SOP (I (..), NP (..), NS (..))
import Ema.Route.Class (IsRoute (..))
import Ema.Route.Prism
import Ema.Site (EmaSite (..), EmaStaticSite)
import Optics.Core (equality, iso, prism', (%))

{- | The merged site's route is represented as a n-ary sum (`NS`) of the
 sub-routes.
-}
type MultiRoute (rs :: [Type]) = NS I rs

type family MultiModel (rs :: [Type]) :: [Type] where
  MultiModel '[] = '[]
  MultiModel (r ': rs) = RouteModel r : MultiModel rs

type family MultiSiteArg (rs :: [Type]) :: [Type] where
  MultiSiteArg '[] = '[]
  MultiSiteArg (r ': rs) = SiteArg r : MultiSiteArg rs

instance IsRoute (MultiRoute '[]) where
  type RouteModel (MultiRoute '[]) = NP I '[]
  routePrism :: RouteModel (MultiRoute ('[] @Type))
-> Prism_ FilePath (MultiRoute ('[] @Type))
routePrism = NP @Type I ('[] @Type) -> Prism_ FilePath (MultiRoute ('[] @Type))
RouteModel (MultiRoute ('[] @Type))
-> Prism_ FilePath (MultiRoute ('[] @Type))
impossiblePrism
    where
      impossiblePrism :: (NP I '[] -> Prism_ FilePath (MultiRoute '[]))
      impossiblePrism :: NP @Type I ('[] @Type) -> Prism_ FilePath (MultiRoute ('[] @Type))
impossiblePrism NP @Type I ('[] @Type)
Nil =
        Prism' FilePath (MultiRoute ('[] @Type))
-> Prism_ FilePath (MultiRoute ('[] @Type))
forall s a. Prism' s a -> Prism_ s a
toPrism_ (Prism' FilePath (MultiRoute ('[] @Type))
 -> Prism_ FilePath (MultiRoute ('[] @Type)))
-> Prism' FilePath (MultiRoute ('[] @Type))
-> Prism_ FilePath (MultiRoute ('[] @Type))
forall a b. (a -> b) -> a -> b
$ (MultiRoute ('[] @Type) -> FilePath)
-> (FilePath -> Maybe (MultiRoute ('[] @Type)))
-> Prism' FilePath (MultiRoute ('[] @Type))
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' (\case {}) (Maybe (MultiRoute ('[] @Type))
-> FilePath -> Maybe (MultiRoute ('[] @Type))
forall a b. a -> b -> a
const Maybe (MultiRoute ('[] @Type))
forall a. Maybe a
Nothing)
  routeUniverse :: RouteModel (MultiRoute ('[] @Type)) -> [MultiRoute ('[] @Type)]
routeUniverse RouteModel (MultiRoute ('[] @Type))
Nil = [MultiRoute ('[] @Type)]
forall a. Monoid a => a
mempty

instance
  ( IsRoute r
  , IsRoute (MultiRoute rs)
  , RouteModel (MultiRoute rs) ~ NP I (MultiModel rs)
  ) =>
  IsRoute (MultiRoute (r ': rs))
  where
  type RouteModel (MultiRoute (r ': rs)) = NP I (RouteModel r ': MultiModel rs)
  routePrism :: RouteModel (MultiRoute ((':) @Type r rs))
-> Prism_ FilePath (MultiRoute ((':) @Type r rs))
routePrism =
    IsRoute r => RouteModel r -> Prism_ FilePath r
forall r. IsRoute r => RouteModel r -> Prism_ FilePath r
routePrism @r
      (RouteModel r -> Prism_ FilePath r)
-> (NP @Type I (MultiModel rs) -> Prism_ FilePath (MultiRoute rs))
-> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs))
-> Prism_ FilePath (MultiRoute ((':) @Type r rs))
forall a r (as :: [Type]) (rs :: [Type]).
(a -> Prism_ FilePath r)
-> (NP @Type I as -> Prism_ FilePath (NS @Type I rs))
-> NP @Type I ((':) @Type a as)
-> Prism_ FilePath (NS @Type I ((':) @Type r rs))
`nsRoutePrism` IsRoute (MultiRoute rs) =>
RouteModel (MultiRoute rs) -> Prism_ FilePath (MultiRoute rs)
forall r. IsRoute r => RouteModel r -> Prism_ FilePath r
routePrism @(MultiRoute rs)
  routeUniverse :: RouteModel (MultiRoute ((':) @Type r rs))
-> [MultiRoute ((':) @Type r rs)]
routeUniverse (I m :* ms) =
    (r -> MultiRoute ((':) @Type r rs))
-> [r] -> [MultiRoute ((':) @Type r rs)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either r (MultiRoute rs) -> MultiRoute ((':) @Type r rs)
forall a (as :: [Type]).
Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS (Either r (MultiRoute rs) -> MultiRoute ((':) @Type r rs))
-> (r -> Either r (MultiRoute rs))
-> r
-> MultiRoute ((':) @Type r rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Either r (MultiRoute rs)
forall a b. a -> Either a b
Left) (RouteModel r -> [r]
forall r. IsRoute r => RouteModel r -> [r]
routeUniverse @r x
RouteModel r
m)
      [MultiRoute ((':) @Type r rs)]
-> [MultiRoute ((':) @Type r rs)] -> [MultiRoute ((':) @Type r rs)]
forall a. Semigroup a => a -> a -> a
<> (MultiRoute rs -> MultiRoute ((':) @Type r rs))
-> [MultiRoute rs] -> [MultiRoute ((':) @Type r rs)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either r (MultiRoute rs) -> MultiRoute ((':) @Type r rs)
forall a (as :: [Type]).
Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS (Either r (MultiRoute rs) -> MultiRoute ((':) @Type r rs))
-> (MultiRoute rs -> Either r (MultiRoute rs))
-> MultiRoute rs
-> MultiRoute ((':) @Type r rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultiRoute rs -> Either r (MultiRoute rs)
forall a b. b -> Either a b
Right) (RouteModel (MultiRoute rs) -> [MultiRoute rs]
forall r. IsRoute r => RouteModel r -> [r]
routeUniverse @(MultiRoute rs) NP @Type I xs
RouteModel (MultiRoute rs)
ms)

instance EmaSite (MultiRoute '[]) where
  type SiteArg (MultiRoute '[]) = NP I '[]
  siteInput :: Some @Type Action
-> SiteArg (MultiRoute ('[] @Type))
-> m (Dynamic m (RouteModel (MultiRoute ('[] @Type))))
siteInput Some @Type Action
_ SiteArg (MultiRoute ('[] @Type))
Nil = Dynamic m (NP @Type I ('[] @Type))
-> m (Dynamic m (NP @Type I ('[] @Type)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Dynamic m (NP @Type I ('[] @Type))
 -> m (Dynamic m (NP @Type I ('[] @Type))))
-> Dynamic m (NP @Type I ('[] @Type))
-> m (Dynamic m (NP @Type I ('[] @Type)))
forall a b. (a -> b) -> a -> b
$ NP @Type I ('[] @Type) -> Dynamic m (NP @Type I ('[] @Type))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil
  siteOutput :: Prism' FilePath (MultiRoute ('[] @Type))
-> RouteModel (MultiRoute ('[] @Type))
-> MultiRoute ('[] @Type)
-> m (SiteOutput (MultiRoute ('[] @Type)))
siteOutput Prism' FilePath (MultiRoute ('[] @Type))
_ RouteModel (MultiRoute ('[] @Type))
Nil = \case {}

instance
  ( EmaStaticSite r
  , EmaStaticSite (MultiRoute rs)
  , SiteArg (MultiRoute rs) ~ NP I (MultiSiteArg rs)
  , RouteModel (MultiRoute rs) ~ NP I (MultiModel rs)
  ) =>
  EmaSite (MultiRoute (r ': rs))
  where
  type SiteArg (MultiRoute (r ': rs)) = NP I (MultiSiteArg (r ': rs))
  siteInput :: Some @Type Action
-> SiteArg (MultiRoute ((':) @Type r rs))
-> m (Dynamic m (RouteModel (MultiRoute ((':) @Type r rs))))
siteInput Some @Type Action
cliAct (I i :* is) = do
    Dynamic m (RouteModel r)
m <- Some @Type Action -> SiteArg r -> m (Dynamic m (RouteModel r))
forall r (m :: Type -> Type).
(EmaSite r, MonadIO m, MonadUnliftIO m, MonadLoggerIO m) =>
Some @Type Action -> SiteArg r -> m (Dynamic m (RouteModel r))
siteInput @r Some @Type Action
cliAct x
SiteArg r
i
    Dynamic m (NP @Type I (MultiModel rs))
ms <- Some @Type Action
-> SiteArg (MultiRoute rs)
-> m (Dynamic m (RouteModel (MultiRoute rs)))
forall r (m :: Type -> Type).
(EmaSite r, MonadIO m, MonadUnliftIO m, MonadLoggerIO m) =>
Some @Type Action -> SiteArg r -> m (Dynamic m (RouteModel r))
siteInput @(MultiRoute rs) Some @Type Action
cliAct NP @Type I xs
SiteArg (MultiRoute rs)
is
    Dynamic m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
-> m (Dynamic
        m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs))))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Dynamic m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
 -> m (Dynamic
         m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))))
-> Dynamic
     m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
-> m (Dynamic
        m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs))))
forall a b. (a -> b) -> a -> b
$ ((RouteModel r, NP @Type I (MultiModel rs))
 -> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
-> RouteModel r
-> NP @Type I (MultiModel rs)
-> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (RouteModel r, NP @Type I (MultiModel rs))
-> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs))
forall a (as :: [Type]).
(a, NP @Type I as) -> NP @Type I ((':) @Type a as)
toNP (RouteModel r
 -> NP @Type I (MultiModel rs)
 -> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
-> Dynamic m (RouteModel r)
-> Dynamic
     m
     (NP @Type I (MultiModel rs)
      -> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic m (RouteModel r)
m Dynamic
  m
  (NP @Type I (MultiModel rs)
   -> NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
-> Dynamic m (NP @Type I (MultiModel rs))
-> Dynamic
     m (NP @Type I ((':) @Type (RouteModel r) (MultiModel rs)))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Dynamic m (NP @Type I (MultiModel rs))
ms
  siteOutput :: Prism' FilePath (MultiRoute ((':) @Type r rs))
-> RouteModel (MultiRoute ((':) @Type r rs))
-> MultiRoute ((':) @Type r rs)
-> m (SiteOutput (MultiRoute ((':) @Type r rs)))
siteOutput Prism' FilePath (MultiRoute ((':) @Type r rs))
rp (I m :* ms) =
    MultiRoute ((':) @Type r rs) -> Either r (MultiRoute rs)
forall a (as :: [Type]).
NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
fromNS
      (MultiRoute ((':) @Type r rs) -> Either r (MultiRoute rs))
-> (Either r (MultiRoute rs) -> m (Asset LByteString))
-> MultiRoute ((':) @Type r rs)
-> m (Asset LByteString)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category @k cat =>
cat a b -> cat b c -> cat a c
>>> (r -> m (Asset LByteString))
-> (MultiRoute rs -> m (Asset LByteString))
-> Either r (MultiRoute rs)
-> m (Asset LByteString)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
        (Prism' FilePath r -> RouteModel r -> r -> m (SiteOutput r)
forall r (m :: Type -> Type).
(EmaSite r, MonadIO m, MonadLoggerIO m) =>
Prism' FilePath r -> RouteModel r -> r -> m (SiteOutput r)
siteOutput @r (Prism' FilePath (MultiRoute ((':) @Type r rs))
rp Prism' FilePath (MultiRoute ((':) @Type r rs))
-> Optic
     A_Prism
     ('[] @Type)
     (MultiRoute ((':) @Type r rs))
     (MultiRoute ((':) @Type r rs))
     r
     r
-> Prism' FilePath r
forall k l m (is :: [Type]) (js :: [Type]) (ks :: [Type]) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Prism
  ('[] @Type)
  (MultiRoute ((':) @Type r rs))
  (MultiRoute ((':) @Type r rs))
  r
  r
forall {a} {as :: [Type]}.
Prism
  (NS @Type I ((':) @Type a as)) (NS @Type I ((':) @Type a as)) a a
headRoute) x
RouteModel r
m)
        (Prism' FilePath (MultiRoute rs)
-> RouteModel (MultiRoute rs)
-> MultiRoute rs
-> m (SiteOutput (MultiRoute rs))
forall r (m :: Type -> Type).
(EmaSite r, MonadIO m, MonadLoggerIO m) =>
Prism' FilePath r -> RouteModel r -> r -> m (SiteOutput r)
siteOutput @(MultiRoute rs) (Prism' FilePath (MultiRoute ((':) @Type r rs))
rp Prism' FilePath (MultiRoute ((':) @Type r rs))
-> Optic
     A_Prism
     ('[] @Type)
     (MultiRoute ((':) @Type r rs))
     (MultiRoute ((':) @Type r rs))
     (MultiRoute rs)
     (MultiRoute rs)
-> Prism' FilePath (MultiRoute rs)
forall k l m (is :: [Type]) (js :: [Type]) (ks :: [Type]) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Prism
  ('[] @Type)
  (MultiRoute ((':) @Type r rs))
  (MultiRoute ((':) @Type r rs))
  (MultiRoute rs)
  (MultiRoute rs)
forall {a} {as :: [Type]}.
Prism
  (NS @Type I ((':) @Type a as))
  (NS @Type I ((':) @Type a as))
  (NS @Type I as)
  (NS @Type I as)
tailRoute) NP @Type I xs
RouteModel (MultiRoute rs)
ms)
    where
      tailRoute :: Prism
  (NS @Type I ((':) @Type a as))
  (NS @Type I ((':) @Type a as))
  (NS @Type I as)
  (NS @Type I as)
tailRoute =
        ((NS @Type I as -> NS @Type I ((':) @Type a as))
-> (NS @Type I ((':) @Type a as) -> Maybe (NS @Type I as))
-> Prism
     (NS @Type I ((':) @Type a as))
     (NS @Type I ((':) @Type a as))
     (NS @Type I as)
     (NS @Type I as)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' (Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
forall a (as :: [Type]).
Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS (Either a (NS @Type I as) -> NS @Type I ((':) @Type a as))
-> (NS @Type I as -> Either a (NS @Type I as))
-> NS @Type I as
-> NS @Type I ((':) @Type a as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS @Type I as -> Either a (NS @Type I as)
forall a b. b -> Either a b
Right) (NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
forall a (as :: [Type]).
NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
fromNS (NS @Type I ((':) @Type a as) -> Either a (NS @Type I as))
-> (Either a (NS @Type I as) -> Maybe (NS @Type I as))
-> NS @Type I ((':) @Type a as)
-> Maybe (NS @Type I as)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category @k cat =>
cat a b -> cat b c -> cat a c
>>> Either a (NS @Type I as) -> Maybe (NS @Type I as)
forall l r. Either l r -> Maybe r
rightToMaybe))
      headRoute :: Prism
  (NS @Type I ((':) @Type a as)) (NS @Type I ((':) @Type a as)) a a
headRoute =
        ((a -> NS @Type I ((':) @Type a as))
-> (NS @Type I ((':) @Type a as) -> Maybe a)
-> Prism
     (NS @Type I ((':) @Type a as)) (NS @Type I ((':) @Type a as)) a a
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' (Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
forall a (as :: [Type]).
Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS (Either a (NS @Type I as) -> NS @Type I ((':) @Type a as))
-> (a -> Either a (NS @Type I as))
-> a
-> NS @Type I ((':) @Type a as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a (NS @Type I as)
forall a b. a -> Either a b
Left) (NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
forall a (as :: [Type]).
NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
fromNS (NS @Type I ((':) @Type a as) -> Either a (NS @Type I as))
-> (Either a (NS @Type I as) -> Maybe a)
-> NS @Type I ((':) @Type a as)
-> Maybe a
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category @k cat =>
cat a b -> cat b c -> cat a c
>>> Either a (NS @Type I as) -> Maybe a
forall l r. Either l r -> Maybe l
leftToMaybe))

-- | Like `eitherRoutePrism` but uses sop-core types instead of Either/Product.
nsRoutePrism ::
  (a -> Prism_ FilePath r) ->
  (NP I as -> Prism_ FilePath (NS I rs)) ->
  (NP I (a ': as) -> Prism_ FilePath (NS I (r ': rs)))
nsRoutePrism :: (a -> Prism_ FilePath r)
-> (NP @Type I as -> Prism_ FilePath (NS @Type I rs))
-> NP @Type I ((':) @Type a as)
-> Prism_ FilePath (NS @Type I ((':) @Type r rs))
nsRoutePrism a -> Prism_ FilePath r
a NP @Type I as -> Prism_ FilePath (NS @Type I rs)
b =
  (a -> Prism_ FilePath r)
-> (NP @Type I as -> Prism_ FilePath (NS @Type I rs))
-> (a, NP @Type I as)
-> Prism_ FilePath (Either r (NS @Type I rs))
forall a r1 b r2.
(a -> Prism_ FilePath r1)
-> (b -> Prism_ FilePath r2)
-> (a, b)
-> Prism_ FilePath (Either r1 r2)
eitherRoutePrism a -> Prism_ FilePath r
a NP @Type I as -> Prism_ FilePath (NS @Type I rs)
b
    ((a, NP @Type I as) -> Prism_ FilePath (Either r (NS @Type I rs)))
-> (((a, NP @Type I as)
     -> Prism_ FilePath (Either r (NS @Type I rs)))
    -> NP @Type I ((':) @Type a as)
    -> Prism_ FilePath (NS @Type I ((':) @Type r rs)))
-> NP @Type I ((':) @Type a as)
-> Prism_ FilePath (NS @Type I ((':) @Type r rs))
forall a b. a -> (a -> b) -> b
& Optic' An_Iso ('[] @Type) FilePath FilePath
-> Optic'
     An_Iso
     ('[] @Type)
     (Either r (NS @Type I rs))
     (NS @Type I ((':) @Type r rs))
-> (NP @Type I ((':) @Type a as) -> (a, NP @Type I as))
-> ((a, NP @Type I as)
    -> Prism_ FilePath (Either r (NS @Type I rs)))
-> NP @Type I ((':) @Type a as)
-> Prism_ FilePath (NS @Type I ((':) @Type r rs))
forall pr pf r1 r2 b a.
(Is pr A_Prism, Is pf A_Prism) =>
Optic' pf ('[] @Type) FilePath FilePath
-> Optic' pr ('[] @Type) r1 r2
-> (b -> a)
-> (a -> Prism_ FilePath r1)
-> b
-> Prism_ FilePath r2
mapRoutePrism Optic' An_Iso ('[] @Type) FilePath FilePath
forall s a t b.
((s :: Type) ~ (a :: Type), (t :: Type) ~ (b :: Type)) =>
Iso s t a b
equality ((Either r (NS @Type I rs) -> NS @Type I ((':) @Type r rs))
-> (NS @Type I ((':) @Type r rs) -> Either r (NS @Type I rs))
-> Optic'
     An_Iso
     ('[] @Type)
     (Either r (NS @Type I rs))
     (NS @Type I ((':) @Type r rs))
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Either r (NS @Type I rs) -> NS @Type I ((':) @Type r rs)
forall a (as :: [Type]).
Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS NS @Type I ((':) @Type r rs) -> Either r (NS @Type I rs)
forall a (as :: [Type]).
NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
fromNS) NP @Type I ((':) @Type a as) -> (a, NP @Type I as)
forall a (as :: [Type]).
NP @Type I ((':) @Type a as) -> (a, NP @Type I as)
fromNP

fromNP :: NP I (a ': as) -> (a, NP I as)
fromNP :: NP @Type I ((':) @Type a as) -> (a, NP @Type I as)
fromNP (I x
x :* NP @Type I xs
y) = (a
x
x, NP @Type I as
NP @Type I xs
y)

toNP :: (a, NP I as) -> NP I (a ': as)
toNP :: (a, NP @Type I as) -> NP @Type I ((':) @Type a as)
toNP (a
x, NP @Type I as
y) = a -> I a
forall a. a -> I a
I a
x I a -> NP @Type I as -> NP @Type I ((':) @Type a as)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I as
y

fromNS :: NS I (a ': as) -> Either a (NS I as)
fromNS :: NS @Type I ((':) @Type a as) -> Either a (NS @Type I as)
fromNS = \case
  Z (I x
x) -> x -> Either x (NS @Type I as)
forall a b. a -> Either a b
Left x
x
  S NS @Type I xs
xs -> NS @Type I xs -> Either a (NS @Type I xs)
forall a b. b -> Either a b
Right NS @Type I xs
xs

toNS :: Either a (NS I as) -> NS I (a ': as)
toNS :: Either a (NS @Type I as) -> NS @Type I ((':) @Type a as)
toNS = (a -> NS @Type I ((':) @Type a as))
-> (NS @Type I as -> NS @Type I ((':) @Type a as))
-> Either a (NS @Type I as)
-> NS @Type I ((':) @Type a as)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (I a -> NS @Type I ((':) @Type a as)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (I a -> NS @Type I ((':) @Type a as))
-> (a -> I a) -> a -> NS @Type I ((':) @Type a as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> I a
forall a. a -> I a
I) NS @Type I as -> NS @Type I ((':) @Type a as)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S