{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq
  ( (.==),
    (./=),
    symDistinct,
    liftSymEq,
    symEq1,
    liftSymEq2,
    symEq2,
  )
where

import Control.Monad.Except (ExceptT)
import Control.Monad.Identity (Identity, IdentityT)
import Control.Monad.Trans.Maybe (MaybeT)
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Classes (Eq1 (liftEq), Eq2 (liftEq2), eq1, eq2)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Ratio (Ratio)
import qualified Data.Text as T
import Data.Type.Bool (If)
import Data.Word (Word16, Word32, Word64, Word8)
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq
  ( SymEq,
    SymEq1,
    SymEq2,
  )
import qualified Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq as SymEq
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymEq
  ( UnifiedSymEq (withBaseSymEq),
    UnifiedSymEq1 (withBaseSymEq1),
    UnifiedSymEq2 (withBaseSymEq2),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode)
import Grisette.Internal.TH.Derivation.Common
  ( DeriveConfig (bitSizePositions, fpBitSizePositions),
  )
import Grisette.Internal.TH.Derivation.Derive (derive, deriveWith)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (S), IsConMode)
import Grisette.Internal.Unified.UnifiedBool (UnifiedBool (GetBool))
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- | Unified `(Grisette.Internal.Core.Data.Class.SymEq..==)`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > a .== b :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Internal.Unified.Class.UnifiedBranching.mrgIf`.
(.==) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
.== :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymEq mode a) =>
a -> a -> GetBool mode
(.==) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
SymEq..== a
b)

-- | Unified `(Grisette.Internal.Core.Data.Class.SymEq../=)`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > a ./= b :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Internal.Unified.Class.UnifiedBranching.mrgIf`.
(./=) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
./= :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymEq mode a) =>
a -> a -> GetBool mode
(./=) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
SymEq../= a
b)

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symDistinct`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > symDistinct l :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Internal.Unified.Class.UnifiedBranching.mrgIf`.
symDistinct ::
  forall mode a. (DecideEvalMode mode, UnifiedSymEq mode a) => [a] -> GetBool mode
symDistinct :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymEq mode a) =>
[a] -> GetBool mode
symDistinct [a]
l =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        [a] -> Bool
forall a. Eq a => [a] -> Bool
SymEq.distinct [a]
l
    )
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        [a] -> SymBool
forall a. SymEq a => [a] -> SymBool
SymEq.symDistinct [a]
l
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.liftSymEq`.
liftSymEq ::
  forall mode f a b.
  (DecideEvalMode mode, UnifiedSymEq1 mode f) =>
  (a -> b -> GetBool mode) ->
  f a ->
  f b ->
  GetBool mode
liftSymEq :: forall (mode :: EvalModeTag) (f :: * -> *) a b.
(DecideEvalMode mode, UnifiedSymEq1 mode f) =>
(a -> b -> GetBool mode) -> f a -> f b -> GetBool mode
liftSymEq a -> b -> GetBool mode
f f a
a f b
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> f a -> f b -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
a -> b -> GetBool mode
f f a
a f b
b)
    ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        (a -> b -> SymBool) -> f a -> f b -> SymBool
forall a b. (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
SymEq.liftSymEq a -> b -> SymBool
a -> b -> GetBool mode
f f a
a f b
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symEq1`.
symEq1 ::
  forall mode f a.
  (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) =>
  f a ->
  f a ->
  GetBool mode
symEq1 :: forall (mode :: EvalModeTag) (f :: * -> *) a.
(DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) =>
f a -> f a -> GetBool mode
symEq1 f a
a f a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a f a -> f a -> Bool
f a -> f a -> GetBool mode
If (IsConMode mode) (Eq a) (SymEq a) => f a -> f a -> GetBool mode
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 f a
a f a
b)
    ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          f a -> f a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
SymEq.symEq1 f a
a f a
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.liftSymEq2`.
liftSymEq2 ::
  forall mode f a b c d.
  (DecideEvalMode mode, UnifiedSymEq2 mode f) =>
  (a -> b -> GetBool mode) ->
  (c -> d -> GetBool mode) ->
  f a c ->
  f b d ->
  GetBool mode
liftSymEq2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b c d.
(DecideEvalMode mode, UnifiedSymEq2 mode f) =>
(a -> b -> GetBool mode)
-> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode
liftSymEq2 a -> b -> GetBool mode
f c -> d -> GetBool mode
a f a c
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => f b d -> GetBool mode)
 -> f b d -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) =>
    f b d -> GetBool mode)
-> f b d
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
forall a b c d.
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 a -> b -> Bool
a -> b -> GetBool mode
f c -> d -> Bool
c -> d -> GetBool mode
a f a c
b)
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => f b d -> GetBool mode)
 -> f b d -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) =>
    f b d -> GetBool mode)
-> f b d
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        (a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
forall (f :: * -> * -> *) a b c d.
SymEq2 f =>
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
SymEq.liftSymEq2 a -> b -> SymBool
a -> b -> GetBool mode
f c -> d -> SymBool
c -> d -> GetBool mode
a f a c
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symEq2`.
symEq2 ::
  forall mode f a b.
  ( DecideEvalMode mode,
    UnifiedSymEq mode a,
    UnifiedSymEq mode b,
    UnifiedSymEq2 mode f
  ) =>
  f a b ->
  f a b ->
  GetBool mode
symEq2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b.
(DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq mode b,
 UnifiedSymEq2 mode f) =>
f a b -> f a b -> GetBool mode
symEq2 f a b
a f a b
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b f a b -> f a b -> Bool
f a b -> f a b -> GetBool mode
If (IsConMode mode) (Eq b) (SymEq b) =>
f a b -> f a b -> GetBool mode
forall (f :: * -> * -> *) a b.
(Eq2 f, Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 f a b
a f a b
b
    )
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b ((If (IsConMode mode) (Eq b) (SymEq b) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq b) (SymEq b) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
            f a b -> f a b -> SymBool
forall a b (f :: * -> * -> *).
(SymEq a, SymEq b, SymEq2 f) =>
f a b -> f a b -> SymBool
SymEq.symEq2 f a b
a f a b
b
    )

instance
  {-# INCOHERENT #-}
  (DecideEvalMode mode, If (IsConMode mode) (Eq a) (SymEq a)) =>
  UnifiedSymEq mode a
  where
  withBaseSymEq :: forall r. (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq If (IsConMode mode) (Eq a) (SymEq a) => r
r = r
If (IsConMode mode) (Eq a) (SymEq a) => r
r
  {-# INLINE withBaseSymEq #-}

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    If (IsConMode mode) (Eq1 f) (SymEq1 f),
    forall a. (UnifiedSymEq mode a) => UnifiedSymEq mode (f a)
  ) =>
  UnifiedSymEq1 mode f
  where
  withBaseSymEq1 :: forall r. (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 If (IsConMode mode) (Eq1 f) (SymEq1 f) => r
r = r
If (IsConMode mode) (Eq1 f) (SymEq1 f) => r
r
  {-# INLINE withBaseSymEq1 #-}

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    If (IsConMode mode) (Eq2 f) (SymEq2 f),
    forall a. (UnifiedSymEq mode a) => UnifiedSymEq1 mode (f a)
  ) =>
  UnifiedSymEq2 mode f
  where
  withBaseSymEq2 :: forall r. (If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 If (IsConMode mode) (Eq2 f) (SymEq2 f) => r
r = r
If (IsConMode mode) (Eq2 f) (SymEq2 f) => r
r
  {-# INLINE withBaseSymEq2 #-}

instance (UnifiedSymEq 'S v) => UnifiedSymEq 'S (Union v) where
  withBaseSymEq :: forall r.
(If (IsConMode 'S) (Eq (Union v)) (SymEq (Union v)) => r) -> r
withBaseSymEq If (IsConMode 'S) (Eq (Union v)) (SymEq (Union v)) => r
r = forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @'S @v r
If (IsConMode 'S) (Eq v) (SymEq v) => r
If (IsConMode 'S) (Eq (Union v)) (SymEq (Union v)) => r
r
  {-# INLINE withBaseSymEq #-}

derive
  [ ''Either,
    ''(,)
  ]
  [''UnifiedSymEq, ''UnifiedSymEq1, ''UnifiedSymEq2]

derive
  [ ''[],
    ''Maybe,
    ''Identity,
    ''ExceptT,
    ''MaybeT,
    ''WriterLazy.WriterT,
    ''WriterStrict.WriterT
  ]
  [''UnifiedSymEq, ''UnifiedSymEq1]

derive
  [ ''Bool,
    ''Integer,
    ''Char,
    ''Int,
    ''Int8,
    ''Int16,
    ''Int32,
    ''Int64,
    ''Word,
    ''Word8,
    ''Word16,
    ''Word32,
    ''Word64,
    ''Float,
    ''Double,
    ''B.ByteString,
    ''T.Text,
    ''FPRoundingMode,
    ''(),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''Ratio
  ]
  [''UnifiedSymEq]

#if MIN_VERSION_base(4,16,0)
derive
  [ ''(,,),
    ''(,,,)
  ]
  [''UnifiedSymEq, ''UnifiedSymEq1, ''UnifiedSymEq2]
#else
derive
  [ ''(,,),
    ''(,,,)
  ]
  [''UnifiedSymEq]
#endif

deriveWith
  (mempty {bitSizePositions = [0]})
  [''WordN, ''IntN]
  [''UnifiedSymEq]

deriveWith
  (mempty {fpBitSizePositions = [(0, 1)]})
  [''FP]
  [''UnifiedSymEq]

-- Sum
instance
  ( DecideEvalMode mode,
    UnifiedSymEq1 mode f,
    UnifiedSymEq1 mode g,
    UnifiedSymEq mode a
  ) =>
  UnifiedSymEq mode (Sum f g a)
  where
  withBaseSymEq :: forall r.
(If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r)
-> r
withBaseSymEq If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g ((If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r)
-> (If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r
      )
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g ((If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r)
-> (If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r
      )
  {-# INLINE withBaseSymEq #-}

instance
  (DecideEvalMode mode, UnifiedSymEq1 mode f, UnifiedSymEq1 mode g) =>
  UnifiedSymEq1 mode (Sum f g)
  where
  withBaseSymEq1 :: forall r.
(If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r) -> r
withBaseSymEq1 If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g r
If (IsConMode mode) (Eq1 g) (SymEq1 g) => r
If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g r
If (IsConMode mode) (Eq1 g) (SymEq1 g) => r
If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r)
  {-# INLINE withBaseSymEq1 #-}

-- IdentityT
instance
  (DecideEvalMode mode, UnifiedSymEq1 mode m, UnifiedSymEq mode a) =>
  UnifiedSymEq mode (IdentityT m a)
  where
  withBaseSymEq :: forall r.
(If
   (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
 r)
-> r
withBaseSymEq If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m ((If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r)
-> (If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m ((If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r)
-> (If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r)
  {-# INLINE withBaseSymEq #-}

instance
  (DecideEvalMode mode, UnifiedSymEq1 mode m) =>
  UnifiedSymEq1 mode (IdentityT m)
  where
  withBaseSymEq1 :: forall r.
(If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) =>
 r)
-> r
withBaseSymEq1 If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m r
If (IsConMode mode) (Eq1 m) (SymEq1 m) => r
If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r) (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m r
If (IsConMode mode) (Eq1 m) (SymEq1 m) => r
If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r)
  {-# INLINE withBaseSymEq1 #-}