Propellor.Types.MetaTypes

Documentation

data MetaType

Constructors

Targeting TargetOS

A target OS of a Property

WithInfo

Indicates that a Property has associated Info

Instances

Show MetaType

Defined in Propellor.Types.MetaTypes

Methods

showsPrec :: Int -> MetaType -> ShowS

show :: MetaType -> String

showList :: [MetaType] -> ShowS

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

SingI 'WithInfo

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing 'WithInfo

SingI ('Targeting 'OSArchLinux)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSArchLinux)

SingI ('Targeting 'OSBuntish)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSBuntish)

SingI ('Targeting 'OSDebian)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSDebian)

SingI ('Targeting 'OSFreeBSD)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSFreeBSD)

SingKind ('KProxy :: KProxy MetaType)

Defined in Propellor.Types.MetaTypes

Associated Types

type DemoteRep 'KProxy

Methods

fromSing :: forall (a :: k). Sing a -> DemoteRep 'KProxy0

data Sing (x :: MetaType)

Defined in Propellor.Types.MetaTypes

data Sing (x :: MetaType) where

• OSDebianS :: Sing ('Targeting 'OSDebian)
• OSBuntishS :: Sing ('Targeting 'OSBuntish)
• OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
• OSArchLinuxS :: Sing ('Targeting 'OSArchLinux)
• WithInfoS :: 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 :: Type 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 'WithInfo

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing 'WithInfo

SingI 'False

Defined in Propellor.Types.Singletons

Methods

sing :: Sing 'False

SingI 'True

Defined in Propellor.Types.Singletons

Methods

sing :: Sing 'True

SingI ('Targeting 'OSArchLinux)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSArchLinux)

SingI ('Targeting 'OSBuntish)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSBuntish)

SingI ('Targeting 'OSDebian)

Defined in Propellor.Types.MetaTypes

Methods

sing :: Sing ('Targeting 'OSDebian)

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 ('WithInfo ': list1) ('WithInfo ': list2) = 'WithInfo ': (list1 `Intersect` list2)

Combine ('WithInfo ': list1) list2 = 'WithInfo ': (list1 `Intersect` list2)

Combine list1 ('WithInfo ': list2) = 'WithInfo ': (list1 `Intersect` list2)

Combine list1 list2 = list1 `Intersect` 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 (_1 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)

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