module Singleraeh.Sing where

import Data.Kind ( Type, Constraint )
import GHC.TypeLits

class Sing (sa :: ak -> Type) where
    type SingC sa :: ak -> Constraint
    sing' :: forall (a :: ak). SingC sa a => sa a

sing
    :: forall {ak} (sa :: ak -> Type) (a :: ak)
    .  (Sing sa, SingC sa a) => sa a
sing :: forall {ak} (sa :: ak -> Type) (a :: ak).
(Sing sa, SingC sa a) =>
sa a
sing = forall ak (sa :: ak -> Type) (a :: ak).
(Sing sa, SingC sa a) =>
sa a
sing' @_ @sa @a

instance Sing SNat where
    type SingC SNat = KnownNat
    sing' :: forall (a :: Nat). SingC SNat a => SNat a
sing' = SNat a
forall (n :: Nat). KnownNat n => SNat n
natSing

instance Sing SSymbol where
    type SingC SSymbol = KnownSymbol
    sing' :: forall (a :: Symbol). SingC SSymbol a => SSymbol a
sing' = SSymbol a
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing

instance Sing SChar where
    type SingC SChar = KnownChar
    sing' :: forall (a :: Char). SingC SChar a => SChar a
sing' = SChar a
forall (n :: Char). KnownChar n => SChar n
charSing