{-# language DataKinds #-}
{-# language GADTs #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeSynonymInstances #-}

module Rel8.Kind.Context
  ( Reifiable( contextSing )
  , SContext(..)
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Prelude ()

-- rel8
import Rel8.Aggregate ( Aggregate )
import Rel8.Expr ( Expr )
import Rel8.Schema.Field ( Field )
import Rel8.Schema.Kind ( Context )
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Result ( Result )


type SContext :: Context -> Type
data SContext context where
  SAggregate :: SContext Aggregate
  SExpr :: SContext Expr
  SField :: SContext (Field table)
  SName :: SContext Name
  SResult :: SContext Result


type Reifiable :: Context -> Constraint
class Reifiable context where
  contextSing :: SContext context


instance Reifiable Aggregate where
  contextSing :: SContext Aggregate
contextSing = SContext Aggregate
SAggregate


instance Reifiable Expr where
  contextSing :: SContext Expr
contextSing = SContext Expr
SExpr


instance Reifiable (Field table) where
  contextSing :: SContext (Field table)
contextSing = SContext (Field table)
forall table. SContext (Field table)
SField


instance Reifiable Result where
  contextSing :: SContext Result
contextSing = SContext Result
SResult


instance Reifiable Name where
  contextSing :: SContext Name
contextSing = SContext Name
SName