Propellor.Types.MetaTypes

Documentation

data MetaType

Constructors

Targeting TargetOS

A target OS of a Property

WithInfo

Indicates that a Property has associated Info

Instances

Eq MetaType

Defined in Propellor.Types.MetaTypes

Methods

(==) :: MetaType -> MetaType -> Bool

(/=) :: MetaType -> MetaType -> Bool

Ord MetaType

Defined in Propellor.Types.MetaTypes

Methods

compare :: MetaType -> MetaType -> Ordering

(<) :: MetaType -> MetaType -> Bool

(<=) :: MetaType -> MetaType -> Bool

(>) :: MetaType -> MetaType -> Bool

(>=) :: MetaType -> MetaType -> Bool

max :: MetaType -> MetaType -> MetaType

min :: MetaType -> MetaType -> MetaType

Show MetaType

Defined in Propellor.Types.MetaTypes

Methods

showsPrec :: Int -> MetaType -> ShowS

show :: MetaType -> String

showList :: [MetaType] -> ShowS

SingI WithInfo

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing WithInfo

SingKind (KProxy :: KProxy MetaType)

Defined in Propellor.Types.MetaTypes

Associated Types

type DemoteRep KProxy :: Type

Methods

fromSing :: Sing a -> DemoteRep KProxy0

SingI (Targeting OSDebian)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSDebian)

SingI (Targeting OSBuntish)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSBuntish)

SingI (Targeting OSArchLinux)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSArchLinux)

SingI (Targeting OSFreeBSD)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSFreeBSD)

data Sing (x :: MetaType)

Defined in Propellor.Types.MetaTypes

data Sing (x :: MetaType) where

• OSDebianS :: forall (x :: MetaType). Sing (Targeting OSDebian)
• OSBuntishS :: forall (x :: MetaType). Sing (Targeting OSBuntish)
• OSFreeBSDS :: forall (x :: MetaType). Sing (Targeting OSFreeBSD)
• OSArchLinuxS :: forall (x :: MetaType). Sing (Targeting OSArchLinux)
• WithInfoS :: forall (x :: MetaType). Sing WithInfo

type DemoteRep (KProxy :: KProxy MetaType)

Defined in Propellor.Types.MetaTypes

type DemoteRep (KProxy :: KProxy MetaType) = MetaType

type UnixLike = MetaTypes '[Targeting OSDebian, Targeting OSBuntish, Targeting OSArchLinux, Targeting OSFreeBSD]

Any unix-like system

type Linux = MetaTypes '[Targeting OSDebian, Targeting OSBuntish, Targeting OSArchLinux]

Any linux system

type DebianLike = MetaTypes '[Targeting OSDebian, Targeting OSBuntish]

Debian and derivatives.

type Debian = MetaTypes '[Targeting OSDebian]

type Buntish = MetaTypes '[Targeting OSBuntish]

type ArchLinux = MetaTypes '[Targeting OSArchLinux]

type FreeBSD = MetaTypes '[Targeting OSFreeBSD]

type HasInfo = MetaTypes '[WithInfo]

Used to indicate that a Property adds Info to the Host where it's used.

type MetaTypes = Sing

type family a + b :: * where ...

Convenience type operator to combine two MetaTypes lists.

For example:

HasInfo + Debian

Which is shorthand for this type:

MetaTypes '[WithInfo, Targeting OSDebian]

Equations

(MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)

sing :: SingI t => Sing t

class SingI t

A class used to pass singleton values implicitly.

Minimal complete definition

sing

Instances

SingI False

Defined in Propellor.Types.Singletons

Methods

sing :: Sing False

SingI True

Defined in Propellor.Types.Singletons

Methods

sing :: Sing True

SingI WithInfo

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing WithInfo

SingI (Targeting OSDebian)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSDebian)

SingI (Targeting OSBuntish)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSBuntish)

SingI (Targeting OSArchLinux)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSArchLinux)

SingI (Targeting OSFreeBSD)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing (Targeting OSFreeBSD)

SingI ([] :: [k])

Defined in Propellor.Types.Singletons

Methods

sing :: Sing []

(SingI x, SingI xs) => SingI (x ': xs :: [a])

Defined in Propellor.Types.Singletons

Methods

sing :: Sing (x ': xs)

type family IncludesInfo t :: Bool where ...

Equations

IncludesInfo (MetaTypes l) = Elem WithInfo l

type family Targets (l :: [a]) :: [a] where ...

Equations

Targets '[] = '[]

Targets (x ': xs) = If (IsTarget x) (x ': Targets xs) (Targets xs)

type family NonTargets (l :: [a]) :: [a] where ...

Equations

NonTargets '[] = '[]

NonTargets (x ': xs) = If (IsTarget x) (NonTargets xs) (x ': NonTargets xs)

type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where ...

Pretty-prints a list of MetaTypes for display in a type error message.

Equations

PrettyPrintMetaTypes '[] = Text "<none>"

PrettyPrintMetaTypes (t ': '[]) = PrettyPrintMetaType t

PrettyPrintMetaTypes (t ': ts) = (PrettyPrintMetaType t :<>: Text " + ") :<>: PrettyPrintMetaTypes ts

type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where ...

Every item in the subset must be in the superset.

Equations

IsSubset '[] superset = True

IsSubset (s ': rest) superset = If (Elem s superset) (IsSubset rest superset) False

type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where ...

Combine two MetaTypes lists, yielding a list that has targets present in both, and nontargets present in either.

Equations

Combine (list1 :: [a]) (list2 :: [a]) = Concat (NonTargets list1 `Union` NonTargets list2) (Targets list1 `Intersect` Targets list2)

type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Constraint where ...

This (or CheckCombinableNote) should be used anywhere Combine is used, as an additional constraint. For example:

foo :: CheckCombinable x y => x -> y -> Combine x y

Equations

CheckCombinable list1 list2 = If (IsCombinable list1 list2) (True ~ True) (CannotCombine list1 list2 Nothing)

type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where ...

Allows providing an additional note.

Equations

CheckCombinableNote list1 list2 note = If (IsCombinable list1 list2) (True ~ True) (CannotCombine list1 list2 (Just ((Text "(" :<>: note) :<>: Text ")")))

type family (a :: Bool) && (b :: Bool) :: Bool where ... infixr 3

Type-level "and"

Equations

False && a = False

True && a = a

a && False = False

a && True = a

a && a = a

type family Not (a :: Bool) = (res :: Bool) | res -> a where ...

Type-level "not". An injective type family since 4.10.0.0.

Since: base-4.7.0.0

Equations

Not False = True

Not True = False

type family EqT (a :: MetaType) (b :: MetaType) where ...

Type level equality of metatypes.

Equations

EqT a a = True

EqT a b = False

type family Union (list1 :: [a]) (list2 :: [a]) :: [a] where ...

Type level union.

Equations

Union '[] list2 = list2

Union (a ': rest) list2 = If (Elem a list2 || Elem a rest) (Union rest list2) (a ': Union rest list2)

type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where ...

Type level intersection. Duplicate list items are eliminated.

Equations

Intersect '[] list2 = '[]

Intersect (a ': rest) list2 = If (Elem a list2 && Not (Elem a rest)) (a ': Intersect rest list2) (Intersect rest list2)

type family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where ...

Type level difference. Items that are in the first list, but not in the second.

Equations

Difference '[] list2 = '[]

Difference (a ': rest) list2 = If (Elem a list2) (Difference rest list2) (a ': Difference rest list2)

type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where ...

IfStuck expr b c leaves b in the residual constraints whenever expr is stuck, otherwise it Evaluates c.

Often you want to leave a DelayError in b in order to report an error when expr is stuck.

The c parameter is a first-class family, which allows you to perform arbitrarily-complicated type-level computations whenever expr isn't stuck. For example, you might want to produce a typeclass Constraint here. Alternatively, you can nest calls to IfStuck in order to do subsequent processing.

This is a generalization of kcsongor's Break machinery described in detecting the undetectable.

Since: type-errors-0.1.0.0

Equations

IfStuck (_ AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind :: k) (b :: k1) (c :: Exp k1) = b

IfStuck (a2 :: k) (b :: a1) (c :: Exp a1) = Eval c

type DelayError (err :: ErrorMessage) = Eval (DelayErrorFcf err :: k -> Type)

Error messages produced via TypeError are often too strict, and will be emitted sooner than you'd like. The solution is to use DelayError, which will switch the error messages to being consumed lazily.

>>> :{
foo :: TypeError ('Text "Too eager; prevents compilation") => ()
foo = ()
:}
...
... Too eager; prevents compilation
...

>>> :{
foo :: DelayError ('Text "Lazy; emitted on use") => ()
foo = ()
:}

>>> foo
...
... Lazy; emitted on use
...

Since: type-errors-0.1.0.0

data DelayErrorFcf (a :: ErrorMessage) (b :: k) :: forall k. ErrorMessage -> k -> Type

Like DelayError, but implemented as a first-class family. DelayErrorFcf is useful when used as the last argument to IfStuck and UnlessStuck.

Since: type-errors-0.1.0.0

Instances

type Eval (DelayErrorFcf a2 :: a1 -> Type)

Defined in Type.Errors

type Eval (DelayErrorFcf a2 :: a1 -> Type) = (TypeError a2 :: a1)