Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data MetaType
- type UnixLike = MetaTypes '['Targeting 'OSDebian, 'Targeting 'OSBuntish, 'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD]
- type Linux = MetaTypes '['Targeting 'OSDebian, 'Targeting 'OSBuntish, 'Targeting 'OSArchLinux]
- type DebianLike = MetaTypes '['Targeting 'OSDebian, 'Targeting 'OSBuntish]
- type Debian = MetaTypes '['Targeting 'OSDebian]
- type Buntish = MetaTypes '['Targeting 'OSBuntish]
- type ArchLinux = MetaTypes '['Targeting 'OSArchLinux]
- type FreeBSD = MetaTypes '['Targeting 'OSFreeBSD]
- type HasInfo = MetaTypes '['WithInfo]
- type MetaTypes = Sing
- type family a + b :: * where ...
- sing :: SingI t => Sing t
- class SingI t
- type family IncludesInfo t :: Bool where ...
- type family Targets (l :: [a]) :: [a] where ...
- type family NonTargets (l :: [a]) :: [a] where ...
- type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where ...
- type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where ...
- type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where ...
- type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Constraint where ...
- type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where ...
- type family (a :: Bool) && (b :: Bool) :: Bool where ...
- type family Not (a :: Bool) = (res :: Bool) | res -> a where ...
- type family EqT (a :: MetaType) (b :: MetaType) where ...
- type family Union (list1 :: [a]) (list2 :: [a]) :: [a] where ...
- type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where ...
- type family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where ...
- type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where ...
- type DelayError (err :: ErrorMessage) = Eval (DelayErrorFcf err :: k -> Type)
- data DelayErrorFcf (a :: ErrorMessage) (b :: k)

# Documentation

#### Instances

Eq MetaType Source # | |

Ord MetaType Source # | |

Defined in Propellor.Types.MetaTypes | |

Show MetaType Source # | |

SingI 'WithInfo Source # | |

SingKind ('KProxy :: KProxy MetaType) Source # | |

SingI ('Targeting 'OSDebian) Source # | |

SingI ('Targeting 'OSBuntish) Source # | |

SingI ('Targeting 'OSArchLinux) Source # | |

Defined in Propellor.Types.MetaTypes | |

SingI ('Targeting 'OSFreeBSD) Source # | |

data Sing (x :: MetaType) Source # | |

Defined in Propellor.Types.MetaTypes | |

type DemoteRep ('KProxy :: KProxy MetaType) Source # | |

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

Any unix-like system

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

Any linux system

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

Debian and derivatives.

type HasInfo = MetaTypes '['WithInfo] Source #

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

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

Convenience type operator to combine two `MetaTypes`

lists.

For example:

HasInfo + Debian

Which is shorthand for this type:

MetaTypes '[WithInfo, Targeting OSDebian]

A class used to pass singleton values implicitly.

#### Instances

SingI 'False Source # | |

SingI 'True Source # | |

SingI 'WithInfo Source # | |

SingI ('Targeting 'OSDebian) Source # | |

SingI ('Targeting 'OSBuntish) Source # | |

SingI ('Targeting 'OSArchLinux) Source # | |

Defined in Propellor.Types.MetaTypes | |

SingI ('Targeting 'OSFreeBSD) Source # | |

SingI ('[] :: [k]) Source # | |

Defined in Propellor.Types.Singletons | |

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

Defined in Propellor.Types.Singletons |

type family IncludesInfo t :: Bool where ... Source #

IncludesInfo (MetaTypes l) = Elem 'WithInfo l |

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

NonTargets '[] = '[] | |

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

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

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

PrettyPrintMetaTypes '[] = 'Text "<none>" | |

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

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

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

Every item in the subset must be in the superset.

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

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

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 ... Source #

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

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

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

Allows providing an additional note.

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*

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

Type level intersection. Duplicate list items are eliminated.

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

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

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 ... #

leaves `IfStuck`

expr b c`b`

in the residual constraints whenever
`expr`

is stuck, otherwise it `Eval`

uates `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*

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 = () :}`:{`

`>>>`

... ... Lazy; emitted on use ...`foo`

*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 |