Note that validate implementations decide what failure information is emitted. They don't even have to emit their own predicate name, even though Predicate is in the context. This is useful in certain cases such as Rerefined.Predicate.Via.

That does mean that the Predicate context may not be used occasionally. But it's very useful, since otherwise combinator predicates have to constantly state (Refine p a, Predicate p), and all predicates should have a pretty name even if it doesn't get printed under normal circumstances.

Minimal complete definition

validate

Instances

Instances details

Refine Fail a Source #
Instance details Defined in Rerefined.Predicate.Fail Methods validate :: Proxy# Fail -> a -> Maybe RefineFailure Source #
Refine Succeed a Source #
Instance details Defined in Rerefined.Predicate.Succeed Methods validate :: Proxy# Succeed -> a -> Maybe RefineFailure Source #
(Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Not Methods validate :: Proxy# (Not p) -> a -> Maybe RefineFailure Source #
(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a Source #	Compare the length of a `MonoFoldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure Source #
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => Refine (CompareValue op sign n :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (And l r)) => Refine (And l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.And Methods validate :: Proxy# (And l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (If l r)) => Refine (If l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.If Methods validate :: Proxy# (If l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (Iff l r)) => Refine (Iff l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Iff Methods validate :: Proxy# (Iff l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (Nand l r)) => Refine (Nand l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Nand Methods validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (Nor l r)) => Refine (Nor l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Nor Methods validate :: Proxy# (Nor l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Or Methods validate :: Proxy# (Or l r) -> a -> Maybe RefineFailure Source #
(Refine l a, Refine r a, KnownPredicateName (Xor l r)) => Refine (Xor l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Xor Methods validate :: Proxy# (Xor l r) -> a -> Maybe RefineFailure Source #

class Predicate p => Refine1 (p :: k) (f :: k1 -> Type) Source #

Refine functor type f with functor predicate p.

By not making the contained type accessible, we ensure refinements apply forall a. f a. That is, refinements here apply only to the functor structure, and not the stored elements.

Minimal complete definition

validate1

Instances

Instances details

(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source #	Compare the length of a `Foldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source #