Safe Haskell | None |
---|---|
Language | Haskell98 |
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) :: forall k. ErrorMessage -> k -> Type
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 data Sing (x :: MetaType) where
| |
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 cb
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
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 |