Safe Haskell	Safe
Language	Haskell98

Propellor.Types.Singletons

Description

Simple implementation of singletons, portable back to ghc 7.6.3

Synopsis

Documentation

data family Sing x Source

The data family of singleton types.

Instances

((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (Property (MetaTypes [k] x)) (Property (MetaTypes [k] y)) Source
((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (Property (MetaTypes [k] x)) (RevertableProperty (MetaTypes [k] y) (MetaTypes k y')) Source
((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (RevertableProperty (MetaTypes [k] x) (MetaTypes k x')) (Property (MetaTypes [k] y)) Source
((~) CheckCombine (CheckCombinable k x y) CanCombine, (~) CheckCombine (CheckCombinable k1 x' y') CanCombine, SingI [k] (Combine k x y), SingI [k1] (Combine k1 x' y')) => Combines (RevertableProperty (MetaTypes [k] x) (MetaTypes [k] x')) (RevertableProperty (MetaTypes [k] y) (MetaTypes [k] y')) Source
data Sing Bool where TrueS :: Sing Bool True FalseS :: Sing Bool False Source
data Sing MetaType where OSDebianS :: Sing MetaType (Targeting OSDebian) OSBuntishS :: Sing MetaType (Targeting OSBuntish) OSFreeBSDS :: Sing MetaType (Targeting OSFreeBSD) WithInfoS :: Sing MetaType WithInfo Source
type (+) * (MetaTypes [k] a) (MetaTypes [k] b) Source
data Sing [k] where Nil :: Sing [k] ([] k) Cons :: Sing k x -> Sing [k] xs -> Sing [k] ((:) k x xs) Source
type CombinedType (Property (MetaTypes [k] x)) (Property (MetaTypes [k] y)) = Property (MetaTypes [k] (Combine k x y)) Source
type CombinedType (Property (MetaTypes [k] x)) (RevertableProperty (MetaTypes [k] y) (MetaTypes k1 y')) = Property (MetaTypes [k] (Combine k x y)) Source
type IncludesInfo (MetaTypes [MetaType] l) Source
type CombinedType (RevertableProperty (MetaTypes [k] x) (MetaTypes k1 x')) (Property (MetaTypes [k] y)) = Property (MetaTypes [k] (Combine k x y)) Source
type CombinedType (RevertableProperty (MetaTypes [k] x) (MetaTypes [k1] x')) (RevertableProperty (MetaTypes [k] y) (MetaTypes [k1] y')) = RevertableProperty (MetaTypes [k] (Combine k x y)) (MetaTypes [k1] (Combine k1 x' y')) Source

class SingI t where Source

A class used to pass singleton values implicitly.

Methods

sing :: Sing t Source

Instances

SingI Bool False Source
SingI Bool True Source
SingI MetaType WithInfo Source
SingI MetaType (Targeting OSDebian) Source
SingI MetaType (Targeting OSBuntish) Source
SingI MetaType (Targeting OSFreeBSD) Source
SingI [k] ([] k) Source
(SingI k x, SingI [k] xs) => SingI [k] ((:) k x xs) Source

class (kparam ~ KProxy) => SingKind kparam where Source

Associated Types

type DemoteRep kparam :: * Source

Methods

fromSing :: Sing (a :: k) -> DemoteRep kparam Source

From singleton to value.

Instances

SingKind Bool (KProxy Bool) Source
SingKind MetaType (KProxy MetaType) Source
SingKind a (KProxy a) => SingKind [a] (KProxy [a]) Source

data KProxy t :: * -> *

A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only

Constructors

KProxy