module Singleraeh.List where

import Data.Kind ( Type )
import Singleraeh.Demote

-- | Singleton list.
type SList :: (a -> Type) -> [a] -> Type
data SList sa as where
    SCons :: sa a -> SList sa as -> SList sa (a : as)
    SNil  ::                        SList sa '[]

demoteSList
    :: forall da sa as
    .  (forall a. sa a -> da)
    -> SList sa as
    -> [da]
demoteSList :: forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList forall (a :: a). sa a -> da
demoteSA = \case
  SCons sa a
sa SList sa as
sas -> sa a -> da
forall (a :: a). sa a -> da
demoteSA sa a
sa da -> [da] -> [da]
forall a. a -> [a] -> [a]
: (forall (a :: a). sa a -> da) -> SList sa as -> [da]
forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList sa a -> da
forall (a :: a). sa a -> da
demoteSA SList sa as
sas
  SList sa as
SNil         -> []

instance Demotable sa => Demotable (SList sa) where
    type Demote (SList sa) = [Demote sa]
    demote :: forall (k1 :: [a]). SList sa k1 -> Demote (SList sa)
demote = (forall (a :: a). sa a -> Demote sa) -> SList sa k1 -> [Demote sa]
forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote