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