    {-# 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