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

module Rel8.Kind.Algebra
  ( Algebra( Product, Sum )
  , SAlgebra( SProduct, SSum )
  , KnownAlgebra( algebraSing )
  )
where

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


type Algebra :: Type
data Algebra = Product | Sum


type SAlgebra :: Algebra -> Type
data SAlgebra algebra where
  SProduct :: SAlgebra 'Product
  SSum :: SAlgebra 'Sum


type KnownAlgebra :: Algebra -> Constraint
class KnownAlgebra algebra where
  algebraSing :: SAlgebra algebra


instance KnownAlgebra 'Product where
  algebraSing :: SAlgebra 'Product
algebraSing = SAlgebra 'Product
SProduct


instance KnownAlgebra 'Sum where
  algebraSing :: SAlgebra 'Sum
algebraSing = SAlgebra 'Sum
SSum