content: -- | Specification for valid Response component types used at the Kind and Type level
  -- for creating an API structure.
  --
  module Hreq.Core.API.Response where
  
  import Data.Kind (Type)
  import Data.Singletons (Sing, SingI (..))
  import GHC.TypeLits (Nat, Symbol)
  
  -- * Response type
  data ResContent a =
      ResBody a a
    | ResHeaders [(Symbol, a)]
    | ResStream a a
    | ResStatus a Nat
    | Raw a
  
  -- * Response type synonyms
  type ResBody = 'ResBody
  type ResHeaders = 'ResHeaders
  type ResStream = 'ResStream
  type Raw = 'Raw ()
  type ResStatus = 'ResStatus ()
  
  -- * Response as a Singleton GADT
  data SResContent (a :: ResContent Type) where
    SResBody :: forall ctyp a. Sing ctyp -> Sing a -> SResContent ('ResBody ctyp a)
    SResStream :: forall ctyp a. Sing ctyp -> Sing a -> SResContent ('ResStream ctyp a)
    SResHeaders :: forall (ts :: [(Symbol, Type)]). Sing ts -> SResContent ('ResHeaders ts)
    SResStatus :: forall (a :: Type) (n :: Nat) . Sing a -> Sing n ->  SResContent ('ResStatus a n)
    SRaw :: forall (a :: Type) . Sing a -> SResContent ('Raw a)
  type instance Sing = SResContent
  
  instance (SingI a, SingI ctyp) => SingI ('ResStream ctyp a :: ResContent Type) where
    sing = SResStream sing sing
  
  instance (SingI ctyp, SingI a) => SingI ('ResBody ctyp a :: ResContent Type) where
    sing = SResBody sing sing
  
  instance SingI ts => SingI ('ResHeaders ts :: ResContent Type) where
    sing = SResHeaders sing
  
  instance (SingI a, SingI n) => SingI ('ResStatus a n :: ResContent Type) where
    sing = SResStatus sing sing
  
  instance SingI a => SingI ('Raw a :: ResContent Type) where
    sing = SRaw sing
  