{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, FlexibleContexts #-}
module Propellor.Types.Singletons (
module Propellor.Types.Singletons,
KProxy(..)
) where
import Data.Kind (Type)
import Data.Proxy (KProxy(..))
data family Sing (x :: k)
class SingI t where
sing :: Sing t
data instance Sing (x :: [k]) where
Nil :: Sing '[]
Cons :: Sing x -> Sing xs -> Sing (x ': xs)
instance (SingI x, SingI xs) => SingI (x ': xs) where sing :: Sing (x : xs)
sing = forall {k} (x :: k) (xs :: [k]). Sing x -> Sing xs -> Sing (x : xs)
Cons forall {k} (t :: k). SingI t => Sing t
sing forall {k} (t :: k). SingI t => Sing t
sing
instance SingI '[] where sing :: Sing '[]
sing = forall k. Sing '[]
Nil
data instance Sing (x :: Bool) where
TrueS :: Sing 'True
FalseS :: Sing 'False
instance SingI 'True where sing :: Sing 'True
sing = Sing 'True
TrueS
instance SingI 'False where sing :: Sing 'False
sing = Sing 'False
FalseS
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
type DemoteRep kparam :: Type
fromSing :: Sing (a :: k) -> DemoteRep kparam
instance SingKind ('KProxy :: KProxy a) => SingKind ('KProxy :: KProxy [a]) where
type DemoteRep ('KProxy :: KProxy [a]) = [DemoteRep ('KProxy :: KProxy a)]
fromSing :: forall (a :: [a]). Sing a -> DemoteRep 'KProxy
fromSing Sing a
R:Sing[]x a a
Nil = []
fromSing (Cons Sing x
x Sing xs
xs) = forall k (kparam :: KProxy k) (a :: k).
SingKind kparam =>
Sing a -> DemoteRep kparam
fromSing Sing x
x forall a. a -> [a] -> [a]
: forall k (kparam :: KProxy k) (a :: k).
SingKind kparam =>
Sing a -> DemoteRep kparam
fromSing Sing xs
xs
instance SingKind ('KProxy :: KProxy Bool) where
type DemoteRep ('KProxy :: KProxy Bool) = Bool
fromSing :: forall (a :: Bool). Sing a -> DemoteRep 'KProxy
fromSing Sing a
R:SingBoolx a
FalseS = Bool
False
fromSing Sing a
R:SingBoolx a
TrueS = Bool
True