module Singleraeh.List where

import Data.Kind ( Type )

-- | 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         -> []