{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Grisette.Core.Data.Class.SymOrdTests (sordTests) where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bifunctor (Bifunctor (bimap))
import qualified Data.ByteString as B
import Data.Foldable (traverse_)
import Data.Functor.Sum (Sum (InL, InR))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Stack (HasCallStack)
import Grisette
  ( AsKey (AsKey),
    ITEOp (symIte),
    LogicalOp (symNot, (.&&), (.||)),
    Solvable (con),
    SymEq ((.==)),
    SymOrd (symCompare, (.<), (.<=), (.>), (.>=)),
    Union,
    mrgIf,
    mrgMax,
    mrgMin,
    mrgSingle,
    symMax,
    symMin,
  )
import Grisette.Core.Data.Class.TestValues
  ( conBool,
    ssymBool,
  )
import Grisette.Internal.Core.Data.Class.AsKey (AsKey1 (AsKey1))
import Grisette.Lib.Control.Monad (mrgReturn)
import Grisette.SymPrim (SymBool, SymInteger)
import Grisette.TestUtil.SymbolicAssertion ((.@?=))
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, (@?=))
import Test.QuickCheck (ioProperty)

concreteOrdOkProp :: (HasCallStack, SymOrd a, Ord a) => (a, a) -> Assertion
concreteOrdOkProp (i, j) = do
  AsKey (i .<= j) @?= con (i <= j)
  AsKey (i .< j) @?= con (i < j)
  AsKey (i .>= j) @?= con (i >= j)
  AsKey (i .> j) @?= con (i > j)
  AsKey1 (symCompare i j) @?= (mrgReturn $ compare i j :: AsKey1 Union Ordering)

symbolicProdOrdOkProp ::
  (HasCallStack, SymOrd v, SymOrd vl, SymOrd vr) =>
  v ->
  v ->
  vl ->
  vr ->
  vl ->
  vr ->
  Assertion
symbolicProdOrdOkProp l r ll lr rl rr = do
  l .<= r .@?= ((ll .< rl) .|| ((ll .== rl) .&& (lr .<= rr)))
  l .< r .@?= ((ll .< rl) .|| ((ll .== rl) .&& (lr .< rr)))
  l .>= r .@?= ((ll .> rl) .|| ((ll .== rl) .&& (lr .>= rr)))
  l .> r .@?= ((ll .> rl) .|| ((ll .== rl) .&& (lr .> rr)))
  l
    `symCompare` r
    .@?= ( ( do
               lc <- symCompare ll rl
               case lc of
                 EQ -> symCompare lr rr
                 _ -> mrgReturn lc
           ) ::
             Union Ordering
         )

sordTests :: Test
sordTests =
  testGroup
    "SymOrd"
    [ testGroup
        "SymOrd for common types"
        [ testGroup
            "SymBool"
            [ testCase "Concrete SymBool" $ do
                conBool False .<= conBool False .@?= conBool True
                conBool False .< conBool False .@?= conBool False
                conBool False .>= conBool False .@?= conBool True
                conBool False .> conBool False .@?= conBool False
                conBool False .<= conBool True .@?= conBool True
                conBool False .< conBool True .@?= conBool True
                conBool False .>= conBool True .@?= conBool False
                conBool False .> conBool True .@?= conBool False
                conBool True .<= conBool False .@?= conBool False
                conBool True .< conBool False .@?= conBool False
                conBool True .>= conBool False .@?= conBool True
                conBool True .> conBool False .@?= conBool True
                conBool True .<= conBool True .@?= conBool True
                conBool True .< conBool True .@?= conBool False
                conBool True .>= conBool True .@?= conBool True
                conBool True .> conBool True .@?= conBool False,
              testCase "Symbolic SymBool" $ do
                ssymBool "a"
                  .<= ssymBool "b"
                  .@?= (symNot (ssymBool "a"))
                  .|| (ssymBool "b")
                ssymBool "a"
                  .< ssymBool "b"
                  .@?= (symNot (ssymBool "a"))
                  .&& (ssymBool "b")
                ssymBool "a"
                  .>= ssymBool "b"
                  .@?= (ssymBool "a")
                  .|| (symNot (ssymBool "b"))
                ssymBool "a"
                  .> ssymBool "b"
                  .@?= (ssymBool "a")
                  .&& (symNot (ssymBool "b"))
                symCompare (ssymBool "a") (ssymBool "b")
                  .@?= ( mrgIf
                           ((symNot (ssymBool "a")) .&& (ssymBool "b"))
                           (mrgSingle LT)
                           ( mrgIf
                               ((ssymBool "a") .== (ssymBool "b"))
                               (mrgSingle EQ)
                               (mrgSingle GT)
                           ) ::
                           Union Ordering
                       )
            ],
          testProperty "Bool" (ioProperty . concreteOrdOkProp @Bool),
          testProperty "Integer" (ioProperty . concreteOrdOkProp @Integer),
          testProperty "Char" (ioProperty . concreteOrdOkProp @Char),
          testProperty "Int" (ioProperty . concreteOrdOkProp @Int),
          testProperty "Int8" (ioProperty . concreteOrdOkProp @Int8),
          testProperty "Int16" (ioProperty . concreteOrdOkProp @Int16),
          testProperty "Int32" (ioProperty . concreteOrdOkProp @Int32),
          testProperty "Int64" (ioProperty . concreteOrdOkProp @Int64),
          testProperty "Word" (ioProperty . concreteOrdOkProp @Word),
          testProperty "Word8" (ioProperty . concreteOrdOkProp @Word8),
          testProperty "Word16" (ioProperty . concreteOrdOkProp @Word16),
          testProperty "Word32" (ioProperty . concreteOrdOkProp @Word32),
          testProperty "Word64" (ioProperty . concreteOrdOkProp @Word64),
          testGroup
            "List"
            [ testProperty "[Integer]" $
                ioProperty . concreteOrdOkProp @[Integer],
              testProperty "[String]" $
                ioProperty . concreteOrdOkProp @[String],
              testCase "[SymBool]" $ do
                ([] :: [SymBool]) .<= [] .@?= conBool True
                ([] :: [SymBool]) .< [] .@?= conBool False
                ([] :: [SymBool]) .>= [] .@?= conBool True
                ([] :: [SymBool]) .> [] .@?= conBool False
                ([] :: [SymBool])
                  `symCompare` []
                  .@?= (mrgSingle EQ :: Union Ordering)
                [] .<= [ssymBool "a"] .@?= conBool True
                [] .< [ssymBool "a"] .@?= conBool True
                [] .>= [ssymBool "a"] .@?= conBool False
                [] .> [ssymBool "a"] .@?= conBool False
                []
                  `symCompare` [ssymBool "a"]
                  .@?= (mrgSingle LT :: Union Ordering)
                [ssymBool "a"] .<= [] .@?= conBool False
                [ssymBool "a"] .< [] .@?= conBool False
                [ssymBool "a"] .>= [] .@?= conBool True
                [ssymBool "a"] .> [] .@?= conBool True
                [ssymBool "a"]
                  `symCompare` []
                  .@?= (mrgSingle GT :: Union Ordering)

                [ssymBool "a", ssymBool "b"]
                  .<= [ssymBool "c"]
                  .@?= (ssymBool "a" .< ssymBool "c" :: SymBool)
                [ssymBool "a", ssymBool "b"]
                  .< [ssymBool "c"]
                  .@?= (ssymBool "a" .< ssymBool "c" :: SymBool)
                [ssymBool "a", ssymBool "b"]
                  .>= [ssymBool "c"]
                  .@?= ( (ssymBool "a" .> ssymBool "c")
                           .|| (ssymBool "a" .== ssymBool "c") ::
                           SymBool
                       )
                [ssymBool "a", ssymBool "b"]
                  .> [ssymBool "c"]
                  .@?= ( (ssymBool "a" .> ssymBool "c")
                           .|| (ssymBool "a" .== ssymBool "c") ::
                           SymBool
                       )
                [ssymBool "a"]
                  `symCompare` [ssymBool "b"]
                  .@?= (ssymBool "a" `symCompare` ssymBool "b" :: Union Ordering)

                [ssymBool "a"]
                  .<= [ssymBool "b", ssymBool "c"]
                  .@?= ( (ssymBool "a" .< ssymBool "b")
                           .|| (ssymBool "a" .== ssymBool "b") ::
                           SymBool
                       )
                [ssymBool "a"]
                  .< [ssymBool "b", ssymBool "c"]
                  .@?= ( (ssymBool "a" .< ssymBool "b")
                           .|| (ssymBool "a" .== ssymBool "b") ::
                           SymBool
                       )
                [ssymBool "a"]
                  .>= [ssymBool "b", ssymBool "c"]
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                [ssymBool "a"]
                  .> [ssymBool "b", ssymBool "c"]
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                [ssymBool "a"]
                  `symCompare` [ssymBool "b", ssymBool "c"]
                  .@?= ( mrgIf
                           (ssymBool "a" .< ssymBool "b")
                           (mrgSingle LT)
                           ( mrgIf
                               (ssymBool "a" .== ssymBool "b")
                               (mrgSingle LT)
                               (mrgSingle GT)
                           ) ::
                           Union Ordering
                       )

                [ssymBool "a", ssymBool "b"]
                  .<= [ssymBool "c", ssymBool "d"]
                  .@?= ( (ssymBool "a" .< ssymBool "c")
                           .|| ( ssymBool "a"
                                   .== ssymBool "c"
                                   .&& ( (ssymBool "b" .< ssymBool "d")
                                           .|| (ssymBool "b" .== ssymBool "d")
                                       )
                               ) ::
                           SymBool
                       )
                [ssymBool "a", ssymBool "b"]
                  .< [ssymBool "c", ssymBool "d"]
                  .@?= ( (ssymBool "a" .< ssymBool "c")
                           .|| ( ssymBool "a"
                                   .== ssymBool "c"
                                   .&& (ssymBool "b" .< ssymBool "d")
                               ) ::
                           SymBool
                       )
                [ssymBool "a", ssymBool "b"]
                  .>= [ssymBool "c", ssymBool "d"]
                  .@?= ( (ssymBool "a" .> ssymBool "c")
                           .|| ( ssymBool "a"
                                   .== ssymBool "c"
                                   .&& ( (ssymBool "b" .> ssymBool "d")
                                           .|| (ssymBool "b" .== ssymBool "d")
                                       )
                               ) ::
                           SymBool
                       )
                [ssymBool "a", ssymBool "b"]
                  .> [ssymBool "c", ssymBool "d"]
                  .@?= ( (ssymBool "a" .> ssymBool "c")
                           .|| ( ssymBool "a"
                                   .== ssymBool "c"
                                   .&& (ssymBool "b" .> ssymBool "d")
                               ) ::
                           SymBool
                       )
                [ssymBool "a", ssymBool "b"]
                  `symCompare` [ssymBool "c", ssymBool "d"]
                  .@?= ( mrgIf
                           (ssymBool "a" .< ssymBool "c")
                           (mrgSingle LT)
                           ( mrgIf
                               (ssymBool "a" .== ssymBool "c")
                               (ssymBool "b" `symCompare` ssymBool "d")
                               (mrgSingle GT)
                           ) ::
                           Union Ordering
                       )
            ],
          testGroup
            "Maybe"
            [ testProperty "Maybe Integer" $
                ioProperty . concreteOrdOkProp @(Maybe Integer),
              testCase "Maybe SymBool" $ do
                (Nothing :: Maybe SymBool) .<= Nothing .@?= conBool True
                (Nothing :: Maybe SymBool) .< Nothing .@?= conBool False
                (Nothing :: Maybe SymBool) .>= Nothing .@?= conBool True
                (Nothing :: Maybe SymBool) .> Nothing .@?= conBool False
                (Nothing :: Maybe SymBool)
                  `symCompare` Nothing
                  .@?= (mrgSingle EQ :: Union Ordering)
                Nothing .<= Just (ssymBool "a") .@?= conBool True
                Nothing .< Just (ssymBool "a") .@?= conBool True
                Nothing .>= Just (ssymBool "a") .@?= conBool False
                Nothing .> Just (ssymBool "a") .@?= conBool False
                Nothing
                  `symCompare` Just (ssymBool "a")
                  .@?= (mrgSingle LT :: Union Ordering)
                Just (ssymBool "a") .<= Nothing .@?= conBool False
                Just (ssymBool "a") .< Nothing .@?= conBool False
                Just (ssymBool "a") .>= Nothing .@?= conBool True
                Just (ssymBool "a") .> Nothing .@?= conBool True
                Just (ssymBool "a")
                  `symCompare` Nothing
                  .@?= (mrgSingle GT :: Union Ordering)
                Just (ssymBool "a")
                  .<= Just (ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                Just (ssymBool "a")
                  .< Just (ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                Just (ssymBool "a")
                  .>= Just (ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                Just (ssymBool "a")
                  .> Just (ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                Just (ssymBool "a")
                  `symCompare` Just (ssymBool "b")
                  .@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
                           Union Ordering
                       )
            ],
          testGroup
            "MaybeT"
            [ testProperty "MaybeT Maybe Integer" $
                ioProperty
                  . concreteOrdOkProp @(MaybeT Maybe Integer)
                  . bimap MaybeT MaybeT,
              testCase "MaybeT Maybe SymBool" $ do
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .<= MaybeT Nothing
                  .@?= conBool True
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .<= MaybeT (Just (Just (ssymBool "a")))
                  .@?= conBool True
                MaybeT (Just (Just (ssymBool "a")))
                  .<= (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .@?= conBool False
                MaybeT (Just (Just (ssymBool "a")))
                  .<= ( MaybeT (Just (Just (ssymBool "b"))) ::
                          MaybeT Maybe SymBool
                      )
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)

                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .< MaybeT Nothing
                  .@?= conBool False
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .< MaybeT (Just (Just (ssymBool "a")))
                  .@?= conBool True
                MaybeT (Just (Just (ssymBool "a")))
                  .< (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .@?= conBool False
                MaybeT (Just (Just (ssymBool "a")))
                  .< ( MaybeT (Just (Just (ssymBool "b"))) ::
                         MaybeT Maybe SymBool
                     )
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)

                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .>= MaybeT Nothing
                  .@?= conBool True
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .>= MaybeT (Just (Just (ssymBool "a")))
                  .@?= conBool False
                MaybeT (Just (Just (ssymBool "a")))
                  .>= (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .@?= conBool True
                MaybeT (Just (Just (ssymBool "a")))
                  .>= ( MaybeT (Just (Just (ssymBool "b"))) ::
                          MaybeT Maybe SymBool
                      )
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)

                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .> MaybeT Nothing
                  .@?= conBool False
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .> MaybeT (Just (Just (ssymBool "a")))
                  .@?= conBool False
                MaybeT (Just (Just (ssymBool "a")))
                  .> (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .@?= conBool True
                MaybeT (Just (Just (ssymBool "a")))
                  .> ( MaybeT (Just (Just (ssymBool "b"))) ::
                         MaybeT Maybe SymBool
                     )
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)

                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  `symCompare` MaybeT Nothing
                  .@?= (mrgSingle EQ :: Union Ordering)
                (MaybeT Nothing :: MaybeT Maybe SymBool)
                  `symCompare` MaybeT (Just (Just (ssymBool "a")))
                  .@?= (mrgSingle LT :: Union Ordering)
                MaybeT (Just (Just (ssymBool "a")))
                  `symCompare` (MaybeT Nothing :: MaybeT Maybe SymBool)
                  .@?= (mrgSingle GT :: Union Ordering)
                MaybeT (Just (Just (ssymBool "a")))
                  `symCompare` ( MaybeT (Just (Just (ssymBool "b"))) ::
                                   MaybeT Maybe SymBool
                               )
                  .@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
                           Union Ordering
                       )
            ],
          testGroup
            "Either"
            [ testProperty "Either Integer Integer" $
                ioProperty . concreteOrdOkProp @(Either Integer Integer),
              testCase "Either SymBool SymBool" $ do
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .<= Left (ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .< Left (ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .>= Left (ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .> Left (ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  `symCompare` Left (ssymBool "b")
                  .@?= (ssymBool "a" `symCompare` ssymBool "b")
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .<= Right (ssymBool "b")
                  .@?= conBool True
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .< Right (ssymBool "b")
                  .@?= conBool True
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .>= Right (ssymBool "b")
                  .@?= conBool False
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  .> Right (ssymBool "b")
                  .@?= conBool False
                (Left (ssymBool "a") :: Either SymBool SymBool)
                  `symCompare` Right (ssymBool "b")
                  .@?= (mrgSingle LT :: Union Ordering)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .<= Left (ssymBool "b")
                  .@?= conBool False
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .< Left (ssymBool "b")
                  .@?= conBool False
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .>= Left (ssymBool "b")
                  .@?= conBool True
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .> Left (ssymBool "b")
                  .@?= conBool True
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  `symCompare` Left (ssymBool "b")
                  .@?= (mrgSingle GT :: Union Ordering)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .<= Right (ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .< Right (ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .>= Right (ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  .> Right (ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                (Right (ssymBool "a") :: Either SymBool SymBool)
                  `symCompare` Right (ssymBool "b")
                  .@?= (ssymBool "a" `symCompare` ssymBool "b")
            ],
          testGroup
            "ExceptT"
            [ testProperty
                "ExceptT Integer Maybe Integer"
                $ ioProperty
                  . concreteOrdOkProp @(ExceptT Integer Maybe Integer)
                  . bimap ExceptT ExceptT,
              testCase "ExceptT SymBool Maybe SymBool" $ do
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .<= ExceptT Nothing
                  .@?= conBool True
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .<= ExceptT (Just (Left (ssymBool "a")))
                  .@?= conBool True
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .<= ExceptT (Just (Right (ssymBool "a")))
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .<= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool False
                ExceptT (Just (Right (ssymBool "a")))
                  .<= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .<= ( ExceptT (Just (Left (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                ExceptT (Just (Right (ssymBool "a")))
                  .<= ( ExceptT (Just (Left (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .<= ( ExceptT (Just (Right (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= conBool True
                ExceptT (Just (Right (ssymBool "a")))
                  .<= ( ExceptT (Just (Right (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)

                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .< ExceptT Nothing
                  .@?= conBool False
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .< ExceptT (Just (Left (ssymBool "a")))
                  .@?= conBool True
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .< ExceptT (Just (Right (ssymBool "a")))
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .< (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool False
                ExceptT (Just (Right (ssymBool "a")))
                  .< (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .< ( ExceptT (Just (Left (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                ExceptT (Just (Right (ssymBool "a")))
                  .< ( ExceptT (Just (Left (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .< ( ExceptT (Just (Right (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= conBool True
                ExceptT (Just (Right (ssymBool "a")))
                  .< ( ExceptT (Just (Right (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)

                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .>= ExceptT Nothing
                  .@?= conBool True
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .>= ExceptT (Just (Left (ssymBool "a")))
                  .@?= conBool False
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .>= ExceptT (Just (Right (ssymBool "a")))
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .>= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool True
                ExceptT (Just (Right (ssymBool "a")))
                  .>= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .>= ( ExceptT (Just (Left (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                ExceptT (Just (Right (ssymBool "a")))
                  .>= ( ExceptT (Just (Left (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .>= ( ExceptT (Just (Right (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= conBool False
                ExceptT (Just (Right (ssymBool "a")))
                  .>= ( ExceptT (Just (Right (ssymBool "b"))) ::
                          ExceptT SymBool Maybe SymBool
                      )
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)

                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .> ExceptT Nothing
                  .@?= conBool False
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .> ExceptT (Just (Left (ssymBool "a")))
                  .@?= conBool False
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .> ExceptT (Just (Right (ssymBool "a")))
                  .@?= conBool False
                ExceptT (Just (Left (ssymBool "a")))
                  .> (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool True
                ExceptT (Just (Right (ssymBool "a")))
                  .> (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .> ( ExceptT (Just (Left (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                ExceptT (Just (Right (ssymBool "a")))
                  .> ( ExceptT (Just (Left (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= conBool True
                ExceptT (Just (Left (ssymBool "a")))
                  .> ( ExceptT (Just (Right (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= conBool False
                ExceptT (Just (Right (ssymBool "a")))
                  .> ( ExceptT (Just (Right (ssymBool "b"))) ::
                         ExceptT SymBool Maybe SymBool
                     )
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)

                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  `symCompare` ExceptT Nothing
                  .@?= (mrgSingle EQ :: Union Ordering)
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  `symCompare` ExceptT (Just (Left (ssymBool "a")))
                  .@?= (mrgSingle LT :: Union Ordering)
                (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                  `symCompare` ExceptT (Just (Right (ssymBool "a")))
                  .@?= (mrgSingle LT :: Union Ordering)
                ExceptT (Just (Left (ssymBool "a")))
                  `symCompare` ( ExceptT Nothing ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= (mrgSingle GT :: Union Ordering)
                ExceptT (Just (Right (ssymBool "a")))
                  `symCompare` ( ExceptT Nothing ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= (mrgSingle GT :: Union Ordering)
                ExceptT (Just (Left (ssymBool "a")))
                  `symCompare` ( ExceptT (Just (Left (ssymBool "b"))) ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= (ssymBool "a" `symCompare` ssymBool "b" :: Union Ordering)
                ExceptT (Just (Right (ssymBool "a")))
                  `symCompare` ( ExceptT (Just (Left (ssymBool "b"))) ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= (mrgSingle GT :: Union Ordering)
                ExceptT (Just (Left (ssymBool "a")))
                  `symCompare` ( ExceptT (Just (Right (ssymBool "b"))) ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= (mrgSingle LT :: Union Ordering)
                ExceptT (Just (Right (ssymBool "a")))
                  `symCompare` ( ExceptT (Just (Right (ssymBool "b"))) ::
                                   ExceptT SymBool Maybe SymBool
                               )
                  .@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
                           Union Ordering
                       )
            ],
          testProperty "()" (ioProperty . concreteOrdOkProp @()),
          testGroup
            "(,)"
            [ testProperty "(Integer, Integer)" $
                ioProperty . concreteOrdOkProp @(Integer, Integer),
              testCase "(SymBool, SymBool)" $ do
                let l = (ssymBool "a", ssymBool "c")
                let r = (ssymBool "b", ssymBool "d")
                let ll = ssymBool "a"
                let lr = ssymBool "c"
                let rl = ssymBool "b"
                let rr = ssymBool "d"
                symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,)"
            [ testProperty "(Integer, Integer, Integer)" $
                ioProperty . concreteOrdOkProp @(Integer, Integer, Integer),
              testCase "(SymBool, SymBool, SymBool)" $ do
                let l = (ssymBool "a", ssymBool "c", ssymBool "e")
                let r = (ssymBool "b", ssymBool "d", ssymBool "f")
                let ll = ssymBool "a"
                let lr = (ssymBool "c", ssymBool "e")
                let rl = ssymBool "b"
                let rr = (ssymBool "d", ssymBool "f")
                symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,,)"
            [ testProperty
                "(Integer, Integer, Integer, Integer)"
                $ ioProperty
                  . concreteOrdOkProp @(Integer, Integer, Integer, Integer),
              testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
                let l = (ssymBool "a", ssymBool "c", ssymBool "e", ssymBool "g")
                let r = (ssymBool "b", ssymBool "d", ssymBool "f", ssymBool "h")
                let ll = (ssymBool "a", ssymBool "c")
                let lr = (ssymBool "e", ssymBool "g")
                let rl = (ssymBool "b", ssymBool "d")
                let rr = (ssymBool "f", ssymBool "h")
                symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,,,)"
            [ testProperty
                "(Integer, Integer, Integer, Integer, Integer)"
                $ ioProperty
                  . concreteOrdOkProp
                    @(Integer, Integer, Integer, Integer, Integer),
              testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
                let l =
                      ( ssymBool "a",
                        ssymBool "c",
                        ssymBool "e",
                        ssymBool "g",
                        ssymBool "i"
                      )
                let r =
                      ( ssymBool "b",
                        ssymBool "d",
                        ssymBool "f",
                        ssymBool "h",
                        ssymBool "j"
                      )
                let ll = (ssymBool "a", ssymBool "c")
                let lr = (ssymBool "e", ssymBool "g", ssymBool "i")
                let rl = (ssymBool "b", ssymBool "d")
                let rr = (ssymBool "f", ssymBool "h", ssymBool "j")
                symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,,,,)"
            [ testProperty
                "(Integer, Integer, Integer, Integer, Integer, Integer)"
                $ ioProperty
                  . concreteOrdOkProp
                    @( Integer,
                       Integer,
                       Integer,
                       Integer,
                       Integer,
                       Integer
                     ),
              testCase
                "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                $ do
                  let l =
                        ( ssymBool "a",
                          ssymBool "c",
                          ssymBool "e",
                          ssymBool "g",
                          ssymBool "i",
                          ssymBool "k"
                        )
                  let r =
                        ( ssymBool "b",
                          ssymBool "d",
                          ssymBool "f",
                          ssymBool "h",
                          ssymBool "j",
                          ssymBool "l"
                        )
                  let ll = (ssymBool "a", ssymBool "c", ssymBool "e")
                  let lr = (ssymBool "g", ssymBool "i", ssymBool "k")
                  let rl = (ssymBool "b", ssymBool "d", ssymBool "f")
                  let rr = (ssymBool "h", ssymBool "j", ssymBool "l")
                  symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,,,,,)"
            [ testProperty
                "(Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
                $ ioProperty
                  . concreteOrdOkProp @(Integer, Integer, Integer, Integer, Integer, Integer, Integer),
              testCase
                "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                $ do
                  let l =
                        ( ssymBool "a",
                          ssymBool "c",
                          ssymBool "e",
                          ssymBool "g",
                          ssymBool "i",
                          ssymBool "k",
                          ssymBool "m"
                        )
                  let r =
                        ( ssymBool "b",
                          ssymBool "d",
                          ssymBool "f",
                          ssymBool "h",
                          ssymBool "j",
                          ssymBool "l",
                          ssymBool "n"
                        )
                  let ll = (ssymBool "a", ssymBool "c", ssymBool "e")
                  let lr =
                        ( ssymBool "g",
                          ssymBool "i",
                          ssymBool "k",
                          ssymBool "m"
                        )
                  let rl = (ssymBool "b", ssymBool "d", ssymBool "f")
                  let rr =
                        ( ssymBool "h",
                          ssymBool "j",
                          ssymBool "l",
                          ssymBool "n"
                        )
                  symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "(,,,,,,,)"
            [ testProperty
                "(Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
                ( ioProperty
                    . concreteOrdOkProp
                      @( Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer
                       )
                ),
              testCase
                "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                $ do
                  let l =
                        ( ssymBool "a",
                          ssymBool "c",
                          ssymBool "e",
                          ssymBool "g",
                          ssymBool "i",
                          ssymBool "k",
                          ssymBool "m",
                          ssymBool "o"
                        )
                  let r =
                        ( ssymBool "b",
                          ssymBool "d",
                          ssymBool "f",
                          ssymBool "h",
                          ssymBool "j",
                          ssymBool "l",
                          ssymBool "n",
                          ssymBool "p"
                        )
                  let ll =
                        ( ssymBool "a",
                          ssymBool "c",
                          ssymBool "e",
                          ssymBool "g"
                        )
                  let lr =
                        ( ssymBool "i",
                          ssymBool "k",
                          ssymBool "m",
                          ssymBool "o"
                        )
                  let rl =
                        ( ssymBool "b",
                          ssymBool "d",
                          ssymBool "f",
                          ssymBool "h"
                        )
                  let rr =
                        ( ssymBool "j",
                          ssymBool "l",
                          ssymBool "n",
                          ssymBool "p"
                        )
                  symbolicProdOrdOkProp l r ll lr rl rr
            ],
          testGroup
            "Sum"
            [ testProperty
                "Sum Maybe Maybe Integer"
                ( ioProperty . \v ->
                    let eitherToSum ::
                          Either (Maybe Integer) (Maybe Integer) ->
                          Sum Maybe Maybe Integer
                        eitherToSum (Left x) = InL x
                        eitherToSum (Right x) = InR x
                     in concreteOrdOkProp (bimap eitherToSum eitherToSum v)
                ),
              testCase "Sum Maybe Maybe SymBool" $ do
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .<= InL (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .< InL (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .>= InL (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .> InL (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .<= InR (Just $ ssymBool "b")
                  .@?= conBool True
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .< InR (Just $ ssymBool "b")
                  .@?= conBool True
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .>= InR (Just $ ssymBool "b")
                  .@?= conBool False
                (InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .> InR (Just $ ssymBool "b")
                  .@?= conBool False
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .<= InR (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .< InR (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .>= InR (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .> InR (Just $ ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .<= InL (Just $ ssymBool "b")
                  .@?= conBool False
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .< InL (Just $ ssymBool "b")
                  .@?= conBool False
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .>= InL (Just $ ssymBool "b")
                  .@?= conBool True
                (InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
                  .> InL (Just $ ssymBool "b")
                  .@?= conBool True
            ],
          testGroup
            "WriterT"
            [ testGroup
                "Lazy"
                [ testProperty
                    "WriterT Integer (Either Integer) Integer"
                    ( ioProperty
                        . \( v1 :: Either Integer (Integer, Integer),
                             v2 :: Either Integer (Integer, Integer)
                             ) ->
                            concreteOrdOkProp
                              ( WriterLazy.WriterT v1,
                                WriterLazy.WriterT v2
                              )
                    ),
                  testCase "WriterT SymBool (Either SymBool) SymBool" $ do
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
                               Union Ordering
                           )

                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool True
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool True
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool False
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool False
                    ( WriterLazy.WriterT $ Left $ ssymBool "a" ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= (mrgSingle LT :: Union Ordering)

                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= conBool False
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= conBool False
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= conBool True
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= conBool True
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterLazy.WriterT (Left $ ssymBool "b")
                      .@?= (mrgSingle GT :: Union Ordering)

                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .<= (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .< (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .>= (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .> (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
                        WriterLazy.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterLazy.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               `symCompare` (ssymBool "b", ssymBool "d") ::
                               Union Ordering
                           )
                ],
              testGroup
                "Strict"
                [ testProperty
                    "WriterT Integer (Either Integer) Integer"
                    ( ioProperty
                        . \( v1 :: Either Integer (Integer, Integer),
                             v2 :: Either Integer (Integer, Integer)
                             ) ->
                            concreteOrdOkProp
                              ( WriterStrict.WriterT v1,
                                WriterStrict.WriterT v2
                              )
                    ),
                  testCase "WriterT Integer (Either Integer) Integer" $ do
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
                               Union Ordering
                           )

                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool True
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool True
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool False
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= conBool False
                    ( WriterStrict.WriterT $ Left $ ssymBool "a" ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= (mrgSingle LT :: Union Ordering)

                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= conBool False
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= conBool False
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= conBool True
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= conBool True
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterStrict.WriterT (Left $ ssymBool "b")
                      .@?= (mrgSingle GT :: Union Ordering)

                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .<= WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .<= (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .< WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .< (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .>= WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .>= (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      .> WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               .> (ssymBool "b", ssymBool "d") ::
                               SymBool
                           )
                    ( WriterStrict.WriterT $
                        Right (ssymBool "a", ssymBool "c") ::
                        WriterStrict.WriterT SymBool (Either SymBool) SymBool
                      )
                      `symCompare` WriterStrict.WriterT
                        (Right (ssymBool "b", ssymBool "d"))
                      .@?= ( (ssymBool "a", ssymBool "c")
                               `symCompare` (ssymBool "b", ssymBool "d") ::
                               Union Ordering
                           )
                ]
            ],
          testGroup
            "Identity"
            [ testProperty
                "Identity Integer"
                ( ioProperty . \(v1 :: Integer, v2) ->
                    concreteOrdOkProp (Identity v1, Identity v2)
                ),
              testCase "Identity SymBool" $ do
                (Identity $ ssymBool "a" :: Identity SymBool)
                  .<= Identity (ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                (Identity $ ssymBool "a" :: Identity SymBool)
                  .< Identity (ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                (Identity $ ssymBool "a" :: Identity SymBool)
                  .>= Identity (ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                (Identity $ ssymBool "a" :: Identity SymBool)
                  .> Identity (ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
            ],
          testGroup
            "IdentityT"
            [ testProperty
                "IdentityT (Either Integer) Integer"
                ( ioProperty . \(v1 :: Either Integer Integer, v2) ->
                    concreteOrdOkProp (IdentityT v1, IdentityT v2)
                ),
              testCase "IdentityT (Either SymBool) SymBool" $ do
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .<= IdentityT (Left $ ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .< IdentityT (Left $ ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .>= IdentityT (Left $ ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .> IdentityT (Left $ ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  `symCompare` IdentityT (Left $ ssymBool "b")
                  .@?= (ssymBool "a" `symCompare` ssymBool "b")

                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .<= IdentityT (Right $ ssymBool "b")
                  .@?= conBool True
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .< IdentityT (Right $ ssymBool "b")
                  .@?= conBool True
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .>= IdentityT (Right $ ssymBool "b")
                  .@?= conBool False
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .> IdentityT (Right $ ssymBool "b")
                  .@?= conBool False
                ( IdentityT $ Left $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  `symCompare` IdentityT (Right $ ssymBool "b")
                  .@?= (mrgSingle LT :: Union Ordering)

                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .<= IdentityT (Left $ ssymBool "b")
                  .@?= conBool False
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .< IdentityT (Left $ ssymBool "b")
                  .@?= conBool False
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .>= IdentityT (Left $ ssymBool "b")
                  .@?= conBool True
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .> IdentityT (Left $ ssymBool "b")
                  .@?= conBool True
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  `symCompare` IdentityT (Left $ ssymBool "b")
                  .@?= (mrgSingle GT :: Union Ordering)

                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .<= IdentityT (Right $ ssymBool "b")
                  .@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .< IdentityT (Right $ ssymBool "b")
                  .@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .>= IdentityT (Right $ ssymBool "b")
                  .@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  .> IdentityT (Right $ ssymBool "b")
                  .@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
                ( IdentityT $ Right $ ssymBool "a" ::
                    IdentityT (Either SymBool) SymBool
                  )
                  `symCompare` IdentityT (Right $ ssymBool "b")
                  .@?= (ssymBool "a" `symCompare` ssymBool "b")
            ],
          testCase "ByteString" $ do
            let bytestrings :: [B.ByteString] =
                  ["", "a", "b", "ab", "ba", "aa", "bb"]
            traverse_
              concreteOrdOkProp
              [(x, y) | x <- bytestrings, y <- bytestrings]
        ],
      testCase "symMax" $ do
        symMax (1 :: SymInteger) 2 .@?= 2
        let [a, b] = ["a", "b"] :: [SymInteger]
        symMax a b .@?= symIte (a .>= b) a b,
      testCase "symMin" $ do
        symMin (1 :: SymInteger) 2 .@?= 1
        let [a, b] = ["a", "b"] :: [SymInteger]
        symMin a b .@?= symIte (a .>= b) b a,
      testCase "mrgMax" $ do
        mrgMax [1] [0, 3] .@?= (mrgReturn [1] :: Union [SymInteger])
        let [a, b, c] = ["a", "b", "c"] :: [SymInteger]
        (mrgMax [a] [b, c] :: Union [SymInteger])
          .@?= (mrgIf (a .<= b) (return [b, c]) (return [a])),
      testCase "mrgMin" $ do
        mrgMin [1] [0, 3] .@?= (mrgReturn [0, 3] :: Union [SymInteger])
        let [a, b, c] = ["a", "b", "c"] :: [SymInteger]
        (mrgMin [a] [b, c] :: Union [SymInteger])
          .@?= (mrgIf (b .< a) (return [b, c]) (return [a]))
    ]