{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language GADTs #-}
{-# language StandaloneKindSignatures #-}
{-# language UndecidableInstances #-}

module Rel8.Schema.Spec
  ( Spec( Spec )
  , SSpec( SSpec, labels, necessity, info, nullity )
  , KnownSpec( specSing )
  )
where

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

-- rel8
import Rel8.Kind.Labels ( Labels, SLabels, KnownLabels, labelsSing )
import Rel8.Kind.Necessity
  ( Necessity
  , SNecessity
  , KnownNecessity, necessitySing
  )
import Rel8.Schema.Null ( Nullity, Sql, Unnullify, nullable )
import Rel8.Type ( DBType, typeInformation )
import Rel8.Type.Information ( TypeInformation )


type Spec :: Type
data Spec = Spec Labels Necessity Type


type SSpec :: Spec -> Type
data SSpec spec where
  SSpec ::
    { SSpec ('Spec labels necessity a) -> SLabels labels
labels :: SLabels labels
    , SSpec ('Spec labels necessity a) -> SNecessity necessity
necessity :: SNecessity necessity
    , SSpec ('Spec labels necessity a) -> TypeInformation (Unnullify a)
info :: TypeInformation (Unnullify a)
    , SSpec ('Spec labels necessity a) -> Nullity a
nullity :: Nullity a
    }
    -> SSpec ('Spec labels necessity a)


type KnownSpec :: Spec -> Constraint
class KnownSpec spec where
  specSing :: SSpec spec


instance
  ( KnownLabels labels
  , KnownNecessity necessity
  , Sql DBType a
  )
  => KnownSpec ('Spec labels necessity a)
 where
  specSing :: SSpec ('Spec labels necessity a)
specSing = SSpec :: forall (labels :: Labels) (necessity :: Necessity) a.
SLabels labels
-> SNecessity necessity
-> TypeInformation (Unnullify a)
-> Nullity a
-> SSpec ('Spec labels necessity a)
SSpec
    { labels :: SLabels labels
labels = SLabels labels
forall (labels :: Labels). KnownLabels labels => SLabels labels
labelsSing
    , necessity :: SNecessity necessity
necessity = SNecessity necessity
forall (necessity :: Necessity).
KnownNecessity necessity =>
SNecessity necessity
necessitySing
    , info :: TypeInformation (Unnullify a)
info = TypeInformation (Unnullify a)
forall a. DBType a => TypeInformation a
typeInformation
    , nullity :: Nullity a
nullity = Nullity a
forall a. Nullable a => Nullity a
nullable
    }