{-# LANGUAGE CPP                   #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE TypeOperators         #-}
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module Data.EqP (
    EqP (..),
) where

import Control.Applicative   (Const (..))
import Data.Kind             (Type)
import Data.Proxy            (Proxy (..))
import Data.Type.Equality    ((:~:) (..), (:~~:) (..))
import GHC.Generics          ((:*:) (..), (:+:) (..))
import System.Mem.StableName (StableName, eqStableName)

#if MIN_VERSION_base(4,18,0)
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif

#if !MIN_VERSION_base(4,19,0)
import Data.Orphans ()
#endif

import qualified Type.Reflection as TR

#if __GLASGOW_HASKELL__ >= 810
import Data.Kind (Constraint)
#endif

-- | Heterogenous lifted equality.
--
-- This class is stronger version of 'Eq1' from @base@
--
-- @
-- class (forall a. Eq a => Eq (f a)) => Eq1 f where
--     liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
-- @
--
-- as we don't require a @a -> b -> Bool@ function.
--
-- Morally 'Eq1' should be a superclass of 'EqP', but it cannot be,
-- as GHC wouldn't allow 'EqP' to be polykinded.
-- https://gitlab.haskell.org/ghc/ghc/-/issues/22682
--
-- == Laws
--
-- [reflexivity]    @'eqp' x x ≡ True@
-- [symmetry]       @'eqp' x y ≡ 'eqp' y x@
-- [transitivity]   @'eqp' x y ≡ 'eqp' y z ≡ True ⇒ 'eqp' x z ≡ True@
-- [compatibility]  @'eqp' x y ≡ x '==' y@
-- [extensionality] @'eqp' x y ≡ True ⇒ f x == f y ≡ True@ for polymorphic @f :: forall x. f x -> a@ and @'Eq' a@.
--
-- /Note:/ P stands for phantom.
--
-- @since 1.0.5
#if __GLASGOW_HASKELL__ >= 810
type EqP :: (k -> Type) -> Constraint
#endif
class (forall a. Eq (f a)) => EqP (f :: k -> Type) where
    eqp :: f a -> f b -> Bool

instance EqP ((:~:) a) where
    eqp :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> Bool
eqp a :~: a
_ a :~: b
_ = Bool
True

instance EqP ((:~~:) a) where
    eqp :: forall (a :: k) (b :: k). (a :~~: a) -> (a :~~: b) -> Bool
eqp a :~~: a
_ a :~~: b
_ = Bool
True


#if MIN_VERSION_base(4,18,0)
instance (EqP a, EqP b) => EqP (Sum a b) where
    eqp :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> Bool
eqp (InL a a
x) (InL a b
y) = a a -> a b -> Bool
forall (a :: k) (b :: k). a a -> a b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp a a
x a b
y
    eqp (InR b a
x) (InR b b
y) = b a -> b b -> Bool
forall (a :: k) (b :: k). b a -> b b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp b a
x b b
y
    eqp Sum a b a
_ Sum a b b
_ = Bool
False

instance (EqP a, EqP b) => EqP (Product a b) where
    eqp :: forall (a :: k) (b :: k). Product a b a -> Product a b b -> Bool
eqp (Pair a a
x b a
y) (Pair a b
x' b b
y') = a a -> a b -> Bool
forall (a :: k) (b :: k). a a -> a b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp a a
x a b
x' Bool -> Bool -> Bool
&& b a -> b b -> Bool
forall (a :: k) (b :: k). b a -> b b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp b a
y b b
y'
#endif

instance (EqP f, EqP g) => EqP (f :+: g) where
    eqp :: forall (a :: k) (b :: k). (:+:) f g a -> (:+:) f g b -> Bool
eqp (L1 f a
x) (L1 f b
y) = f a -> f b -> Bool
forall (a :: k) (b :: k). f a -> f b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp f a
x f b
y
    eqp (R1 g a
x) (R1 g b
y) = g a -> g b -> Bool
forall (a :: k) (b :: k). g a -> g b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp g a
x g b
y
    eqp (:+:) f g a
_ (:+:) f g b
_ = Bool
False

instance (EqP a, EqP b) => EqP (a :*: b) where
    eqp :: forall (a :: k) (b :: k). (:*:) a b a -> (:*:) a b b -> Bool
eqp (a a
x :*: b a
y) (a b
x' :*: b b
y') = a a -> a b -> Bool
forall (a :: k) (b :: k). a a -> a b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp a a
x a b
x' Bool -> Bool -> Bool
&& b a -> b b -> Bool
forall (a :: k) (b :: k). b a -> b b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP f =>
f a -> f b -> Bool
eqp b a
y b b
y'

instance EqP TR.TypeRep where
    eqp :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Bool
eqp TypeRep a
x TypeRep b
y = TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
TR.SomeTypeRep TypeRep a
x SomeTypeRep -> SomeTypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep b -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
TR.SomeTypeRep TypeRep b
y

#if MIN_VERSION_base(4,18,0)
instance EqP TL.SChar where
    eqp :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Bool
eqp SChar a
x SChar b
y = SChar a -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar SChar a
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== SChar b -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar SChar b
y

instance EqP TL.SSymbol where
    eqp :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Bool
eqp SSymbol a
x SSymbol b
y = SSymbol a -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol SSymbol a
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SSymbol b -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol SSymbol b
y

instance EqP TN.SNat where
    eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool
eqp SNat a
x SNat b
y = SNat a -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat SNat a
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== SNat b -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat SNat b
y
#endif

instance EqP Proxy where
    eqp :: forall (a :: k) (b :: k). Proxy a -> Proxy b -> Bool
eqp Proxy a
_ Proxy b
_ = Bool
True

instance Eq a => EqP (Const a) where
    eqp :: forall (a :: k) (b :: k). Const a a -> Const a b -> Bool
eqp (Const a
x) (Const a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

instance EqP StableName where
    eqp :: forall a b. StableName a -> StableName b -> Bool
eqp = StableName a -> StableName b -> Bool
forall a b. StableName a -> StableName b -> Bool
eqStableName