Rerefined.Predicate.Via

Documentation

validateVia :: forall {k1} {k2} (pVia :: k1) (p :: k2) a. (Refine pVia a, Predicate p, KnownPredicateName p) => Proxy# p -> a -> Maybe RefineFailure

Implement validate for predicate p via pVia.

This is useful when you need a unique data type for a predicate (e.g. for instances, clarity), but the predicate it tests already exists. In such cases, it would be nice to reuse the existing predicate, while printing both predicates in failures i.e. "predicate X, implemented via predicate Y, failed with Z".

Call using visible type applications:

validate = validateVia @pVia