| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope
Synopsis
- class WithDeMorganScope (c :: T -> Constraint) t a b where
- withDeMorganScope :: c (t a b) => ((c a, c b) => 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
- 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
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.
Methods
withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret Source #
Instances
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 Source #
Simpler version of withDeMorganScope for ForbidT constraints.
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.