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

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

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

-- rel8
import Rel8.Kind.Labels ( Labels, SLabels, KnownLabels, labelsSing )
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 Type


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


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


instance
  ( KnownLabels labels
  , Sql DBType a
  )
  => KnownSpec ('Spec labels a)
 where
  specSing :: SSpec ('Spec labels a)
specSing = SSpec :: forall (labels :: Labels) a.
SLabels labels
-> TypeInformation (Unnullify a)
-> Nullity a
-> SSpec ('Spec labels a)
SSpec
    { labels :: SLabels labels
labels = SLabels labels
forall (labels :: Labels). KnownLabels labels => SLabels labels
labelsSing
    , 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
    }