{-# LANGUAGE OverloadedStrings   #-} -- for builder
{-# LANGUAGE AllowAmbiguousTypes #-} -- 'validateVia' is designed for this

module Rerefined.Predicate.Via where

import Rerefined.Predicate.Common
import GHC.Exts ( Proxy# )

{- | 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
@
-}
validateVia
    :: forall pVia p a
    .  (Refine pVia a, Predicate p, KnownPredicateName p)
    => Proxy# p -> a -> Maybe RefineFailure
validateVia :: forall {k} {k} (pVia :: k) (p :: k) a.
(Refine pVia a, Predicate p, KnownPredicateName p) =>
Proxy# p -> a -> Maybe RefineFailure
validateVia Proxy# p
p a
a =
    case Proxy# pVia -> a -> Maybe RefineFailure
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe RefineFailure
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @pVia) a
a of
      Maybe RefineFailure
Nothing -> Maybe RefineFailure
forall a. Maybe a
Nothing
      Just RefineFailure
e  -> Proxy# p -> Builder -> [RefineFailure] -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Builder -> [RefineFailure] -> Maybe RefineFailure
validateFail Proxy# p
p Builder
"via" [RefineFailure
e]