Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class WithDeMorganScope (c :: T -> Constraint) t a b where
- withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
- simpleWithDeMorgan :: forall a b ret op. ((ContainsT op a || ContainsT op b) ~ 'False, SingI a) => Sing op -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret
- simpleWithDeMorgan' :: forall b ret op a. (ContainsT op a || ContainsT op b) ~ 'False => Sing op -> Sing a -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret
- deMorganForbidT :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False => Sing p -> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
Documentation
class WithDeMorganScope (c :: T -> Constraint) t a b where Source #
Allows using a scope that can be proven true with a De Morgan law.
Many scopes are defined as not a
(or rather a ~ 'False
) where a
is a
negative property we want to avoid as a Constraint
.
The negative constraints are implemented with a type family that for some
combination types resolves to itself applied to the type arguments in an or
,
e.g. A pair l r
has x
if l
or r
contain x
.
Because of the De Morgan laws not (a or b)
implies (not a) and (not b)
or in our case: pair
does not contain x
-> a
and b
don't contain x
.
withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret Source #
Instances
simpleWithDeMorgan :: forall a b ret op. ((ContainsT op a || ContainsT op b) ~ 'False, SingI a) => Sing op -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret Source #
When a class looks like
class (SomeTypeFamily t ~ 'False, ...) => TheClass t instance (SomeTypeFamily t ~ 'False, ...) => TheClass t
and the additional constraints are satisfied by the instance constraints of
the WithDeMorganScope
instance for TheClass
, we can use
simpleWithDeMorgan
to define withDeMorganScope
for the instance.