module Singleraeh.Demote where

import Data.Kind ( Type, Constraint )
import GHC.TypeLits
import GHC.TypeNats qualified as TN

-- | Singleton types which may be demoted.
type Demotable :: (k -> Type) -> Constraint
class Demotable sk where
    -- | Demoted type.
    type Demote sk :: Type

    -- | Demote a term of the singleton @sk@.
    demote :: forall k. sk k -> Demote sk

instance Demotable SNat where
    type Demote SNat = Natural
    demote :: forall (k :: Nat). SNat k -> Demote SNat
demote = SNat k -> Nat
SNat k -> Demote SNat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat

instance Demotable SSymbol where
    type Demote SSymbol = String
    demote :: forall (k :: Symbol). SSymbol k -> Demote SSymbol
demote = SSymbol k -> String
SSymbol k -> Demote SSymbol
forall (s :: Symbol). SSymbol s -> String
fromSSymbol

instance Demotable SChar where
    type Demote SChar = Char
    demote :: forall (k :: Char). SChar k -> Demote SChar
demote = SChar k -> Char
SChar k -> Demote SChar
forall (c :: Char). SChar c -> Char
fromSChar