{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
{-# LANGUAGE OverloadedStrings #-} -- for builder
{-# LANGUAGE AllowAmbiguousTypes #-} -- for validateVia

module Rerefined.Predicate.Via where

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

{- | Predicate @p@ is implemented via predicate @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.

'Via' assists in doing this. Implement your 'Predicate' instance as normal, then
implement 'Refine' with:

    'validate' = 'validateVia' \@pVia

Now when this predicate fails, it will print the @pVia@ failure with a wrapper
stating the name of the original predicate.

Note that you may not use @DerivingVia@ because it only works on the last
parameter of a multi-parameter type class, and I don't want to switch the order
of the 'Refine' parameters. Even if I did, @DerivingVia@ isn't much different to
or easier than this.
-}
data Via pVia p
instance (Predicate p, Predicate pVia)
  => Predicate (Via pVia p) where
    type PredicateName d (Via pVia p) = ShowParen (d > 9)
        ("Via " ++ PredicateName 10 p ++ " " ++ PredicateName 10 pVia)
instance (Refine pVia a, Predicate p, KnownPredicateName p)
  => Refine (Via pVia p) a where
    validate :: Proxy# (Via pVia p) -> a -> Maybe RefineFailure
validate Proxy# (Via pVia 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 (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) Builder
"via" [RefineFailure
e]

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 = Proxy# (Via pVia p) -> a -> Maybe RefineFailure
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe RefineFailure
validate (forall a. Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @(Via pVia p))