{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, FlexibleContexts #-}

-- | Simple implementation of singletons, portable back to ghc 7.6.3

module Propellor.Types.Singletons (
	module Propellor.Types.Singletons,
	KProxy(..)
) where

#if __GLASGOW_HASKELL__ > 707
import Data.Proxy (KProxy(..))
#else
data KProxy (a :: *) = KProxy
#endif

-- | The data family of singleton types.
data family Sing (x :: k)

-- | A class used to pass singleton values implicitly.
class SingI t where
	sing :: Sing t

-- Lists of singletons
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 = Sing x -> Sing xs -> Sing (x : xs)
forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs)
Cons Sing x
forall k (t :: k). SingI t => Sing t
sing Sing xs
forall k (t :: k). SingI t => Sing t
sing
instance SingI '[] where sing :: 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 :: *
	-- | From singleton to value.
	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 :: Sing a -> DemoteRep 'KProxy
fromSing Sing a
Nil = []
	fromSing (Cons x xs) = Sing x -> DemoteRep 'KProxy
forall k (kparam :: KProxy k) (a :: k).
SingKind kparam =>
Sing a -> DemoteRep kparam
fromSing Sing x
x DemoteRep 'KProxy -> [DemoteRep 'KProxy] -> [DemoteRep 'KProxy]
forall a. a -> [a] -> [a]
: Sing xs -> DemoteRep 'KProxy
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 :: Sing a -> DemoteRep 'KProxy
fromSing Sing a
FalseS = Bool
DemoteRep 'KProxy
False
	fromSing Sing a
TrueS = Bool
DemoteRep 'KProxy
True