{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Grisette.Core.Data.Class.SimpleMergeableTests
  ( simpleMergeableTests,
  )
where

import Control.Monad.Cont (ContT (ContT, runContT))
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity, runIdentity),
    IdentityT (IdentityT, runIdentityT),
  )
import qualified Control.Monad.RWS.Lazy as RWSTLazy
import qualified Control.Monad.RWS.Strict as RWSTStrict
import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.Monoid as Monoid
import GHC.Generics (Generic)
import Generics.Deriving (Default (Default))
import Grisette
  ( ITEOp (symIte),
    LogicalOp (symNot, (.&&), (.||)),
    Mergeable,
    SimpleMergeable (mrgIte),
    Solvable (con, ssym),
    SymBool,
    Union,
    mrgIf,
    mrgIte1,
    mrgSingle,
  )
import Grisette.Core.Data.Class.TestValues (ssymBool)
import Grisette.Internal.Core.Data.Class.AsKey (AsKey, AsKey1)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))

newtype AndMonoidSymBool = AndMonoidSymBool (AsKey SymBool)
  deriving (Show, Generic, Eq)
  deriving (Mergeable) via (Default AndMonoidSymBool)

instance Semigroup AndMonoidSymBool where
  (AndMonoidSymBool a) <> (AndMonoidSymBool b) = AndMonoidSymBool (a .&& b)

instance Monoid AndMonoidSymBool where
  mempty = AndMonoidSymBool $ con True

simpleMergeableTests :: Test
simpleMergeableTests =
  testGroup
    "SimpleMergeable"
    [ testGroup
        "SimpleMergeable for common types"
        [ testCase "SymBool" $ do
            mrgIte (ssym "a") (ssym "b" :: AsKey SymBool) (ssym "c")
              @?= symIte (ssym "a") (ssym "b") (ssym "c"),
          testCase "()" $ do
            mrgIte (ssym "a") () () @?= (),
          testCase "(SymBool, SymBool)" $ do
            mrgIte
              (ssym "a")
              (ssym "b" :: AsKey SymBool, ssym "d" :: AsKey SymBool)
              (ssym "c", ssym "e")
              @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                    symIte (ssym "a") (ssym "d") (ssym "e")
                  ),
          testCase "(SymBool, SymBool, SymBool)" $ do
            mrgIte
              (ssym "a")
              ( ssym "b" :: AsKey SymBool,
                ssym "d" :: AsKey SymBool,
                ssym "f" :: AsKey SymBool
              )
              (ssym "c", ssym "e", ssym "g")
              @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                    symIte (ssym "a") (ssym "d") (ssym "e"),
                    symIte (ssym "a") (ssym "f") (ssym "g")
                  ),
          testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
            mrgIte
              (ssym "a")
              ( ssym "b" :: AsKey SymBool,
                ssym "d" :: AsKey SymBool,
                ssym "f" :: AsKey SymBool,
                ssym "h" :: AsKey SymBool
              )
              (ssym "c", ssym "e", ssym "g", ssym "i")
              @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                    symIte (ssym "a") (ssym "d") (ssym "e"),
                    symIte (ssym "a") (ssym "f") (ssym "g"),
                    symIte (ssym "a") (ssym "h") (ssym "i")
                  ),
          testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
            mrgIte
              (ssym "a")
              ( ssym "b" :: AsKey SymBool,
                ssym "d" :: AsKey SymBool,
                ssym "f" :: AsKey SymBool,
                ssym "h" :: AsKey SymBool,
                ssym "j" :: AsKey SymBool
              )
              ( ssym "c",
                ssym "e",
                ssym "g",
                ssym "i",
                ssym "k"
              )
              @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                    symIte (ssym "a") (ssym "d") (ssym "e"),
                    symIte (ssym "a") (ssym "f") (ssym "g"),
                    symIte (ssym "a") (ssym "h") (ssym "i"),
                    symIte (ssym "a") (ssym "j") (ssym "k")
                  ),
          testCase "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
            mrgIte
              (ssym "a")
              ( ssym "b" :: AsKey SymBool,
                ssym "d" :: AsKey SymBool,
                ssym "f" :: AsKey SymBool,
                ssym "h" :: AsKey SymBool,
                ssym "j" :: AsKey SymBool,
                ssym "l" :: AsKey SymBool
              )
              ( ssym "c",
                ssym "e",
                ssym "g",
                ssym "i",
                ssym "k",
                ssym "m"
              )
              @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                    symIte (ssym "a") (ssym "d") (ssym "e"),
                    symIte (ssym "a") (ssym "f") (ssym "g"),
                    symIte (ssym "a") (ssym "h") (ssym "i"),
                    symIte (ssym "a") (ssym "j") (ssym "k"),
                    symIte (ssym "a") (ssym "l") (ssym "m")
                  ),
          testCase
            "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
            $ do
              mrgIte
                (ssym "a")
                ( ssym "b" :: AsKey SymBool,
                  ssym "d" :: AsKey SymBool,
                  ssym "f" :: AsKey SymBool,
                  ssym "h" :: AsKey SymBool,
                  ssym "j" :: AsKey SymBool,
                  ssym "l" :: AsKey SymBool,
                  ssym "n" :: AsKey SymBool
                )
                ( ssym "c",
                  ssym "e",
                  ssym "g",
                  ssym "i",
                  ssym "k",
                  ssym "m",
                  ssym "o"
                )
                @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                      symIte (ssym "a") (ssym "d") (ssym "e"),
                      symIte (ssym "a") (ssym "f") (ssym "g"),
                      symIte (ssym "a") (ssym "h") (ssym "i"),
                      symIte (ssym "a") (ssym "j") (ssym "k"),
                      symIte (ssym "a") (ssym "l") (ssym "m"),
                      symIte (ssym "a") (ssym "n") (ssym "o")
                    ),
          testCase
            "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
            $ do
              mrgIte
                (ssymBool "a")
                ( ssym "b" :: AsKey SymBool,
                  ssym "d" :: AsKey SymBool,
                  ssym "f" :: AsKey SymBool,
                  ssym "h" :: AsKey SymBool,
                  ssym "j" :: AsKey SymBool,
                  ssym "l" :: AsKey SymBool,
                  ssym "n" :: AsKey SymBool,
                  ssym "p" :: AsKey SymBool
                )
                ( ssym "c" :: AsKey SymBool,
                  ssym "e" :: AsKey SymBool,
                  ssym "g" :: AsKey SymBool,
                  ssym "i" :: AsKey SymBool,
                  ssym "k" :: AsKey SymBool,
                  ssym "m" :: AsKey SymBool,
                  ssym "o" :: AsKey SymBool,
                  ssym "q" :: AsKey SymBool
                )
                @?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
                      symIte (ssym "a") (ssym "d") (ssym "e"),
                      symIte (ssym "a") (ssym "f") (ssym "g"),
                      symIte (ssym "a") (ssym "h") (ssym "i"),
                      symIte (ssym "a") (ssym "j") (ssym "k"),
                      symIte (ssym "a") (ssym "l") (ssym "m"),
                      symIte (ssym "a") (ssym "n") (ssym "o"),
                      symIte (ssym "a") (ssym "p") (ssym "q")
                    ),
          testCase "SymBool -> SymBool" $ do
            let f = mrgIte (ssym "a") symNot ((ssym "b" :: AsKey SymBool) .&&)
            f (ssym "c")
              @?= symIte
                (ssym "a")
                (symNot $ ssym "c")
                ((ssym "b") .&& (ssym "c")),
          testCase "MaybeT (Union) SymBool" $ do
            let l :: MaybeT (AsKey1 Union) (AsKey SymBool) =
                  MaybeT
                    ( mrgIf
                        (ssym "b")
                        (mrgSingle Nothing)
                        (mrgSingle $ Just $ ssym "c")
                    )
            let r :: MaybeT (AsKey1 Union) (AsKey SymBool) =
                  MaybeT
                    ( mrgIf
                        (ssym "d")
                        (mrgSingle Nothing)
                        (mrgSingle $ Just $ ssym "e")
                    )
            let res :: MaybeT (AsKey1 Union) (AsKey SymBool) =
                  MaybeT
                    ( mrgIf
                        (ssym "a")
                        ( mrgIf
                            (ssym "b")
                            (mrgSingle Nothing)
                            (mrgSingle $ Just $ ssym "c")
                        )
                        ( mrgIf
                            (ssym "d")
                            (mrgSingle Nothing)
                            (mrgSingle $ Just $ ssym "e")
                        )
                    )
            mrgIte (ssym "a") l r @?= res
            mrgIte1 (ssym "a") l r @?= res
            mrgIf (ssym "a") l r @?= res,
          testCase "ExceptT SymBool (Union) SymBool" $ do
            let l :: ExceptT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
                  ExceptT
                    ( mrgIf
                        (ssym "b")
                        (mrgSingle $ Left $ ssym "c")
                        (mrgSingle $ Right $ ssym "d")
                    )
            let r =
                  ExceptT
                    ( mrgIf
                        (ssym "e")
                        (mrgSingle $ Left $ ssym "f")
                        (mrgSingle $ Right $ ssym "g")
                    )
            let res =
                  ExceptT
                    ( mrgIf
                        (ssym "a")
                        ( mrgIf
                            (ssym "b")
                            (mrgSingle $ Left $ ssym "c")
                            (mrgSingle $ Right $ ssym "d")
                        )
                        ( mrgIf
                            (ssym "e")
                            (mrgSingle $ Left $ ssym "f")
                            (mrgSingle $ Right $ ssym "g")
                        )
                    )
            mrgIte (ssym "a") l r @?= res
            mrgIte1 (ssym "a") l r @?= res
            mrgIf (ssym "a") l r @?= res,
          testGroup
            "StateT Integer (Union) SymBool"
            [ testCase "Lazy" $ do
                let st1 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool) =
                      StateLazy.StateT $ \(x :: Integer) ->
                        mrgSingle (ssym "a", x + 2)
                let st2 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool) =
                      StateLazy.StateT $ \(x :: Integer) ->
                        mrgSingle (ssym "b", x * 2)
                let st3 = mrgIte (ssym "c") st1 st2
                let st31 = mrgIte1 (ssym "c") st1 st2
                let st3u1 = mrgIf (ssym "c") st1 st2
                StateLazy.runStateT st3 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateLazy.runStateT st3 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6))
                StateLazy.runStateT st31 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateLazy.runStateT st31 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6))
                StateLazy.runStateT st3u1 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateLazy.runStateT st3u1 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6)),
              testCase "Strict" $ do
                let st1 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool) =
                      StateStrict.StateT $ \(x :: Integer) ->
                        mrgSingle (ssym "a", x + 2)
                let st2 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool) =
                      StateStrict.StateT $ \(x :: Integer) ->
                        mrgSingle (ssym "b", x * 2)
                let st3 = mrgIte (ssym "c") st1 st2
                let st31 = mrgIte1 (ssym "c") st1 st2
                let st3u1 = mrgIf (ssym "c") st1 st2
                StateStrict.runStateT st3 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateStrict.runStateT st3 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6))
                StateStrict.runStateT st31 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateStrict.runStateT st31 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6))
                StateStrict.runStateT st3u1 2
                  @?= mrgSingle
                    (symIte (ssym "c") (ssym "a") (ssym "b"), 4)
                StateStrict.runStateT st3u1 3
                  @?= mrgIf
                    (ssym "c")
                    (mrgSingle (ssym "a", 5))
                    (mrgSingle (ssym "b", 6))
            ],
          testCase "ContT (SymBool, Integer) (Union) (SymBool, Integer)" $ do
            let c1 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer) =
                  ContT $ \f -> f (ssym "a", 2)
            let c2 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer) =
                  ContT $ \f -> f (ssym "b", 3)
            let c3 = mrgIte (ssym "c") c1 c2
            let c3u1 = mrgIf (ssym "c") c1 c2
            let r =
                  mrgIf
                    (ssym "c")
                    ( mrgIf
                        (ssym "p")
                        (mrgSingle (ssym "a", 2))
                        (mrgSingle (symNot $ ssym "a", 3))
                    )
                    ( mrgIf
                        (ssym "p")
                        (mrgSingle (ssym "b", 3))
                        (mrgSingle (symNot $ ssym "b", 4))
                    )
            let f (a, x) =
                  mrgIf
                    (ssym "p")
                    (mrgSingle (a, x))
                    (mrgSingle (symNot a, x + 1)) ::
                    AsKey1 Union (AsKey SymBool, Integer)
            runContT c3 f @?= r
            runContT c3u1 f @?= r,
          testGroup
            "RWST (Integer, SymBool) (Monoid.Sum Integer, AndMonoidSymBool) (Integer, SymBool) (Union) (Integer, SymBool)"
            [ testCase "Lazy" $ do
                let rws1 ::
                      RWSTLazy.RWST
                        (Integer, AsKey SymBool)
                        (Monoid.Sum Integer, AndMonoidSymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTLazy.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .&& bs),
                              (ir - is, br .|| bs),
                              ( Monoid.Sum $ ir * is,
                                AndMonoidSymBool $ bs .&& br
                              )
                            )
                let rws2 ::
                      RWSTLazy.RWST
                        (Integer, AsKey SymBool)
                        (Monoid.Sum Integer, AndMonoidSymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTLazy.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .|| bs),
                              (ir - is, br .&& bs),
                              ( Monoid.Sum $ ir * is,
                                AndMonoidSymBool $ bs .|| br
                              )
                            )
                let rws3 = mrgIte (ssymBool "c") rws1 rws2
                let rws3u1 = mrgIf (ssymBool "c") rws1 rws2

                let res1 ::
                      AsKey1
                        Union
                        ( (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool),
                          (Monoid.Sum Integer, AndMonoidSymBool)
                        ) =
                        mrgIf
                          (ssym "c")
                          ( mrgSingle
                              ( (1, ssym "a" .&& ssym "b"),
                                (-1, ssym "a" .|| ssym "b"),
                                ( 0,
                                  AndMonoidSymBool $
                                    ssym "b" .&& ssym "a"
                                )
                              )
                          )
                          ( mrgSingle
                              ( (1, ssym "a" .|| ssym "b"),
                                (-1, ssym "a" .&& ssym "b"),
                                ( 0,
                                  AndMonoidSymBool $
                                    ssym "b" .|| ssym "a"
                                )
                              )
                          )
                RWSTLazy.runRWST rws3 (0, ssym "a") (1, ssym "b")
                  @?= res1
                RWSTLazy.runRWST rws3u1 (0, ssym "a") (1, ssym "b")
                  @?= res1,
              testCase "Strict" $ do
                let rws1 ::
                      RWSTStrict.RWST
                        (Integer, AsKey SymBool)
                        (Monoid.Sum Integer, AndMonoidSymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTStrict.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .&& bs),
                              (ir - is, br .|| bs),
                              ( Monoid.Sum $ ir * is,
                                AndMonoidSymBool $ bs .&& br
                              )
                            )
                let rws2 ::
                      RWSTStrict.RWST
                        (Integer, AsKey SymBool)
                        (Monoid.Sum Integer, AndMonoidSymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTStrict.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .|| bs),
                              (ir - is, br .&& bs),
                              ( Monoid.Sum $ ir * is,
                                AndMonoidSymBool $ bs .|| br
                              )
                            )
                let rws3 = mrgIte (ssymBool "c") rws1 rws2
                let rws3u1 = mrgIf (ssymBool "c") rws1 rws2

                let res1 ::
                      AsKey1
                        Union
                        ( (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool),
                          (Monoid.Sum Integer, AndMonoidSymBool)
                        ) =
                        mrgIf
                          (ssymBool "c")
                          ( mrgSingle
                              ( (1, ssym "a" .&& ssym "b"),
                                (-1, ssym "a" .|| ssym "b"),
                                ( 0,
                                  AndMonoidSymBool $
                                    ssym "b" .&& ssym "a"
                                )
                              )
                          )
                          ( mrgSingle
                              ( (1, ssym "a" .|| ssym "b"),
                                (-1, ssym "a" .&& ssym "b"),
                                ( 0,
                                  AndMonoidSymBool $
                                    ssym "b" .|| ssym "a"
                                )
                              )
                          )
                RWSTStrict.runRWST rws3 (0, ssym "a") (1, ssym "b")
                  @?= res1
                RWSTStrict.runRWST rws3u1 (0, ssym "a") (1, ssym "b")
                  @?= res1
            ],
          testGroup
            "WriterT (Monoid.Sum Integer) (Union) SymBool"
            [ testCase "Lazy" $ do
                let st1 ::
                      WriterLazy.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterLazy.WriterT $ mrgSingle (ssym "a", 1)
                let st2 ::
                      WriterLazy.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterLazy.WriterT $ mrgSingle (ssym "b", 2)
                let st3 ::
                      WriterLazy.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterLazy.WriterT $ mrgSingle (ssym "c", 1)
                let st4 = mrgIte (ssym "d") st1 st2
                let st41 = mrgIte1 (ssym "d") st1 st2
                let st4u1 = mrgIf (ssym "d") st1 st2
                let st5 = mrgIte (ssym "d") st1 st3
                let st51 = mrgIte1 (ssym "d") st1 st3
                let st5u1 = mrgIf (ssym "d") st1 st3
                WriterLazy.runWriterT st4
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterLazy.runWriterT st41
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterLazy.runWriterT st4u1
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterLazy.runWriterT st5
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
                WriterLazy.runWriterT st51
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
                WriterLazy.runWriterT st5u1
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1),
              testCase "Strict" $ do
                let st1 ::
                      WriterStrict.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterStrict.WriterT $ mrgSingle (ssym "a", 1)
                let st2 ::
                      WriterStrict.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterStrict.WriterT $ mrgSingle (ssym "b", 2)
                let st3 ::
                      WriterStrict.WriterT
                        (Monoid.Sum Integer)
                        (AsKey1 Union)
                        (AsKey SymBool) =
                        WriterStrict.WriterT $ mrgSingle (ssym "c", 1)
                let st4 = mrgIte (ssym "d") st1 st2
                let st41 = mrgIte1 (ssym "d") st1 st2
                let st4u1 = mrgIf (ssym "d") st1 st2
                let st5 = mrgIte (ssym "d") st1 st3
                let st51 = mrgIte1 (ssym "d") st1 st3
                let st5u1 = mrgIf (ssym "d") st1 st3
                WriterStrict.runWriterT st4
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterStrict.runWriterT st41
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterStrict.runWriterT st4u1
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterStrict.runWriterT st5
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
                WriterStrict.runWriterT st51
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
                WriterStrict.runWriterT st5u1
                  @?= mrgSingle
                    (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
            ],
          testCase "ReaderT Integer (Union) Integer" $ do
            let r1 :: ReaderT Integer (AsKey1 Union) Integer =
                  ReaderT $ \(x :: Integer) -> mrgSingle $ x + 2
            let r2 :: ReaderT Integer (AsKey1 Union) Integer =
                  ReaderT $ \(x :: Integer) -> mrgSingle $ x * 2
            let r3 = mrgIte (ssym "c") r1 r2
            let r3u1 = mrgIf (ssym "c") r1 r2
            runReaderT r3 2 @?= mrgSingle 4
            runReaderT r3 3 @?= mrgIf (ssym "c") (mrgSingle 5) (mrgSingle 6)
            runReaderT r3u1 2 @?= mrgSingle 4
            runReaderT r3u1 3
              @?= mrgIf
                (ssym "c")
                (mrgSingle 5)
                (mrgSingle 6)

            let r4 :: ReaderT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
                  ReaderT $ \x -> mrgSingle $ x .&& ssym "x"
            let r5 :: ReaderT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
                  ReaderT $ \x -> mrgSingle $ x .|| ssym "y"
            let r61 = mrgIte1 (ssym "c") r4 r5
            runReaderT r61 (ssym "a")
              @?= mrgSingle
                ( symIte
                    (ssym "c")
                    (ssym "a" .&& ssym "x")
                    (ssym "a" .|| ssym "y")
                ),
          testCase "Identity SymBool" $ do
            let i1 :: Identity (AsKey SymBool) = Identity $ ssym "a"
            let i2 :: Identity (AsKey SymBool) = Identity $ ssym "b"
            let i3 = mrgIte (ssym "c") i1 i2
            let i31 = mrgIte1 (ssym "c") i1 i2
            runIdentity i3 @?= symIte (ssym "c") (ssym "a") (ssym "b")
            runIdentity i31
              @?= symIte (ssym "c") (ssym "a") (ssym "b"),
          testCase "IdentityT (Union) SymBool" $ do
            let i1 :: IdentityT (AsKey1 Union) (AsKey SymBool) =
                  IdentityT $ mrgSingle $ ssym "a"
            let i2 :: IdentityT (AsKey1 Union) (AsKey SymBool) =
                  IdentityT $ mrgSingle $ ssym "b"
            let i3 = mrgIte (ssym "c") i1 i2
            let i31 = mrgIte1 (ssym "c") i1 i2
            let i3u1 = mrgIf (ssym "c") i1 i2
            runIdentityT i3
              @?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
            runIdentityT i31
              @?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
            runIdentityT i3u1
              @?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
        ]
    ]