{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Main where

import Control.Exception
import Control.DeepSeq
import Data.List
import Data.Maybe
import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits
import System.Exit
import Test.QuickCheck
import Unsafe.Coerce

import Data.Finite
import Data.Finite.Internal

instance KnownNat n => Arbitrary (Finite n) where
    arbitrary
        | natVal @n Proxy == 0 = discard
        | otherwise = oneof
            [ pure (Finite 0)
            , pure (Finite $ natVal @n Proxy - 1)
            , Finite . (`mod` natVal @n Proxy) <$> arbitrary
            ]
    shrink (Finite x) = mapMaybe packFinite $ shrink x

withNat' :: forall prop. Testable prop => Gen Integer -> (Integer -> [Integer]) -> (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
withNat' gen shr prop = forAllShrinkBlind gen shr $ \n -> case someNatVal n of
    Nothing -> counterexample "withNat" False
    Just (SomeNat p) -> counterexample ("@" ++ show n) $ prop (fromInteger (natVal p)) p

withNat :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
withNat = withNat' (getNonNegative <$> arbitrary) (map getNonNegative . shrink . NonNegative)

withNatPos :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
withNatPos = withNat' (getPositive <$> arbitrary) (map getPositive . shrink . Positive)

unsafeWithKnownNat :: forall n prop. Testable prop => Integer -> (KnownNat n => prop) -> Property
unsafeWithKnownNat n prop = case someNatVal n of
    Nothing -> counterexample "unsafeWithKnownNat: someNatVal" False
    Just (SomeNat (_ :: Proxy n')) -> case unsafeCoerce Refl :: n :~: n' of
        Refl -> property prop

newtype IneqCond (n :: Nat) (m :: Nat) = IneqCond ((n <= m) => Property)
unsafeWithInequality :: forall (n :: Nat) (m :: Nat) prop. Testable prop => ((n <= m) => prop) -> Property
unsafeWithInequality prop =
    case unsafeCoerce (IneqCond @n @m $ property prop) :: IneqCond 0 1 of
        IneqCond prop' -> prop'

prop_isvalid_under = withNat $ \_ (_ :: Proxy n) x ->
    x < 0 ==> expectFailure $ isValidFinite @n (Finite x)
prop_isvalid_over = withNat $ \n (_ :: Proxy n) x ->
    x >= n ==> expectFailure $ isValidFinite @n (Finite x)

prop_valid_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (isValidFinite $ finite @n x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_getFinite_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (getFinite (finite @n x) == x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_finite_getFinite = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        finite (getFinite @n x) === x

prop_valid_maxBound = withNat $ \n (_ :: Proxy n) ->
    n > 0 ==> isValidFinite (maxBound @(Finite n))
prop_maxBound_max = withNat $ \n (_ :: Proxy n) ->
    property $ \x ->
        n > 0 ==> maxBound @(Finite n) >= x

prop_valid_minBound = withNat $ \n (_ :: Proxy n) ->
    n > 0 ==> isValidFinite (minBound @(Finite n))
prop_minBound_min = withNat $ \n (_ :: Proxy n) ->
    property $ \x ->
        n > 0 ==> minBound @(Finite n) <= x

prop_valid_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (isValidFinite $ toEnum @(Finite n) x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_fromEnum_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (fromEnum (toEnum @(Finite n) x) == x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_toEnum_fromEnum = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        toEnum @(Finite n) (fromEnum x) == x

prop_valid_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        all isValidFinite $ enumFrom @(Finite n) x
prop_getFinite_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        map getFinite (enumFrom @(Finite n) x)
            === takeWhile (isJust . packFinite @n) (enumFrom (getFinite x))

prop_valid_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        all isValidFinite $ enumFromTo @(Finite n) x y
prop_getFinite_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        map getFinite (enumFromTo @(Finite n) x y)
            === enumFromTo (getFinite x) (getFinite y)

prop_valid_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        x /= y ==> all isValidFinite $ enumFromThen @(Finite n) x y
prop_getFinite_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        x /= y ==> map getFinite (enumFromThen @(Finite n) x y)
            === takeWhile (isJust . packFinite @n) (enumFromThen (getFinite x) (getFinite y))

prop_valid_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y z ->
        x /= y ==> all isValidFinite $ enumFromThenTo @(Finite n) x y z
prop_getFinite_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y z ->
        x /= y ==> map getFinite (enumFromThenTo @(Finite n) x y z)
            === enumFromThenTo (getFinite x) (getFinite y) (getFinite z)

prop_nonint_succ = withNat' genBig shrinkBig $ \_ (_ :: Proxy n) ->
    forAllShrink genBig shrinkBig $ \x ->
        case packFinite @n $ succ x of
            Nothing -> discard
            Just y -> y === succ (finite x)
    where
        big = toInteger (maxBound :: Int)
        genBig = (big +) . getNonNegative <$> arbitrary
        shrinkBig = map ((big +) . getNonNegative) . shrink . NonNegative . subtract big

prop_valid_read = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x -> ioProperty $
            evaluate (isValidFinite $ read @(Finite n) (show @(Finite m) x))
                `catch` \(_ :: ErrorCall) -> pure True
prop_read_show = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        read (show @(Finite n) x) === x

prop_valid_plus = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        isValidFinite @n $ x + y
prop_getFinite_plus = withNatPos $ \n (_ :: Proxy n) ->
    property $ \x y ->
        (getFinite @n (x + y) - (getFinite x + getFinite y)) `mod` n === 0

prop_valid_minus = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        isValidFinite @n $ x - y
prop_getFinite_minus = withNatPos $ \n (_ :: Proxy n) ->
    property $ \x y ->
        (getFinite @n (x - y) - (getFinite x - getFinite y)) `mod` n === 0

prop_valid_times = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        isValidFinite @n $ x * y
prop_getFinite_times = withNatPos $ \n (_ :: Proxy n) ->
    property $ \x y ->
        (getFinite @n (x * y) - (getFinite x * getFinite y)) `mod` n === 0

prop_valid_negate = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        isValidFinite @n $ -x
prop_getFinite_negate = withNatPos $ \n (_ :: Proxy n) ->
    property $ \x ->
        (getFinite @n (-x) - (- getFinite x)) `mod` n === 0

prop_valid_abs = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        isValidFinite @n $ abs x
prop_getFinite_abs = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        getFinite @n (abs x) === abs (getFinite x)

prop_valid_signum = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
        evaluate (isValidFinite @n $ signum x)
            `catch` \(_ :: ErrorCall) -> pure True

prop_getFinite_signum = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
        evaluate (getFinite @n (signum x) == signum (getFinite x))
            `catch` \(_ :: ErrorCall) -> pure True

prop_valid_fromInteger = withNatPos $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (isValidFinite $ fromInteger @(Finite n) x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_toInteger_fromInteger = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    evaluate (toInteger (fromInteger @(Finite n) x) == x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_fromInteger_toInteger = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        fromInteger (toInteger @(Finite n) x) === x

prop_valid_quot = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> isValidFinite @n $ x `quot` y
prop_getFinite_quot = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> getFinite @n (x `quot` y) === getFinite x `quot` getFinite y

prop_valid_rem = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> isValidFinite @n $ x `rem` y
prop_getFinite_rem = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> getFinite @n (x `rem` y) === getFinite x `rem` getFinite y

prop_valid_div = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> isValidFinite @n $ x `div` y
prop_getFinite_div = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> getFinite @n (x `div` y) === getFinite x `div` getFinite y

prop_valid_mod = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> isValidFinite @n $ x `mod` y
prop_getFinite_mod = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x y ->
        y /= 0 ==> getFinite @n (x `mod` y) === getFinite x `mod` getFinite y

prop_force = withNat $ \_ (_ :: Proxy n) ->
    expectFailure $ rnf @(Finite n) (error "Expected exception") `seq` True

prop_valid_packFinite = withNat $ \_ (_ :: Proxy n) x ->
    maybe True isValidFinite $ packFinite @n x
prop_getFinite_packFinite = withNat $ \_ (_ :: Proxy n) x ->
    maybe (property True) ((x ===) . getFinite) $ packFinite @n x
prop_finite_packFinite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
    case packFinite @n x of
        Nothing -> (evaluate (finite @n x) >> pure False)
            `catch` \(_ :: ErrorCall) -> pure True
        Just y -> evaluate (y == finite x)

prop_valid_finites = withNat $ \_ (_ :: Proxy n) ->
    all isValidFinite $ finites @n
prop_finites_minMax = withNatPos $ \_ (_ :: Proxy n) ->
    minBound `elem` finites @n .&&. maxBound `elem` finites @n
prop_finites_ordered = withNat $ \_ (_ :: Proxy n) ->
    finites @n === sort finites
prop_finites_all = withNat $ \_ (_ :: Proxy n) ->
    property $ \x ->
        x {- could be discard -} `seq` x `elem` finites @n

prop_valid_modulo = withNatPos $ \_ (_ :: Proxy n) x ->
    isValidFinite $ modulo @n x
prop_getFinite_modulo = withNatPos $ \n (_ :: Proxy n) x ->
    (getFinite (modulo @n x) - x) `mod` n === 0


prop_getFinite_equals = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            (x `equals` y) === (getFinite @n x == getFinite @m y)

prop_getFinite_cmp = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            (x `cmp` y) === (getFinite @n x `compare` getFinite @m y)

prop_valid_natToFinite = withNat $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Bool $
            isValidFinite $ natToFinite @n @m Proxy
prop_getFinite_natToFinite = withNat $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Property $
            getFinite (natToFinite @n @m Proxy) === natVal @n Proxy

prop_valid_weaken = withNatPos $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            isValidFinite $ weaken @n x
prop_finites_weaken = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        map (weaken @n) finites === init finites

prop_valid_strengthen = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            maybe True isValidFinite $ strengthen @n x
prop_finites_strengthen = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        map (strengthen @n) finites === map Just finites ++ [Nothing]

prop_valid_shift = withNatPos $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            isValidFinite $ shift @n x
prop_finites_shift = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        map (shift @n) finites === tail finites

prop_valid_unshift = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            maybe True isValidFinite $ unshift @n x
prop_finites_unshift = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        map (unshift @n) finites === [Nothing] ++ map Just finites

prop_valid_weakenN = withNatPos $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            property $ \x ->
                isValidFinite $ weakenN @n @m x
prop_finites_weakenN = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            map (weakenN @n @m) finites === take n finites

prop_valid_strengthenN = withNat $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x ->
            maybe True isValidFinite $ strengthenN @n @m x
prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing

prop_valid_shiftN = withNatPos $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            property $ \x ->
                isValidFinite $ shiftN @n @m x
prop_finites_shiftN = withNat $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            map (shiftN @n @m) finites === drop (m - n) finites

prop_valid_unshiftN = withNatPos $ \_ (_ :: Proxy n) ->
    withNat $ \_ (_ :: Proxy m) ->
        property $ \x ->
            maybe True isValidFinite $ unshiftN @n @m x
prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)

prop_valid_weakenProxy = withNatPos $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                isValidFinite $ weakenProxy @Proxy @k @n Proxy x
prop_finites_weakenProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            map (weakenProxy @Proxy @k @n Proxy) finites === take n finites

prop_valid_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                maybe True isValidFinite $ strengthenProxy @n @Proxy @k Proxy x
prop_finites_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            map (strengthenProxy @n @Proxy @k Proxy) finites === take n (map Just finites) ++ replicate k Nothing

prop_valid_shiftProxy = withNatPos $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                isValidFinite $ shiftProxy @k @Proxy @n Proxy x
prop_finites_shiftProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            map (shiftProxy @k @Proxy @n Proxy) finites === drop k finites

prop_valid_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                maybe True isValidFinite $ unshiftProxy @k @Proxy @n Proxy  x
prop_finites_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            map (unshiftProxy @k @Proxy @n Proxy) finites === replicate k Nothing ++ map Just finites

prop_strengthen_weaken = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        strengthen @n (weaken x) === Just x
prop_weaken_strengthen = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            maybe True (== x) (weaken @n <$> strengthen x)

prop_unshift_shift = withNatPos $ \_ (_ :: Proxy n) ->
    property $ \x ->
        unshift @n (shift x) === Just x
prop_shift_unshift = withNat $ \n (_ :: Proxy n) ->
    unsafeWithKnownNat @(n + 1) (n + 1) $
        property $ \x ->
            maybe True (== x) (shift @n <$> unshift x)

prop_strengthenN_weakenN = withNatPos $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        m <= n ==> unsafeWithInequality @m @n @Property $
            property $ \x ->
                strengthenN @m @n (weakenN x) === Just x
prop_weakenN_strengthenN = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            property $ \x ->
                maybe True (== x) (weakenN @n @m <$> strengthenN x)

prop_unshiftN_shiftN = withNatPos $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        m <= n ==> unsafeWithInequality @m @n @Property $
            property $ \x ->
                unshiftN @m @n (shiftN x) === Just x
prop_shiftN_unshiftN = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        n <= m ==> unsafeWithInequality @n @m @Property $
            property $ \x ->
                maybe True (== x) (shiftN @n @m <$> unshiftN x)

prop_strengthenProxy_weakenProxy = withNatPos $ \_ (_ :: Proxy n) ->
    withNat $ \_ (_ :: Proxy k) ->
        property $ \x ->
            strengthenProxy @n @Proxy @k Proxy (weakenProxy Proxy x) === Just x
prop_weakenProxy_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                maybe True (== x) (weakenProxy @Proxy @k @n Proxy <$> strengthenProxy Proxy x)

prop_unshiftProxy_shiftProxy = withNatPos $ \_ (_ :: Proxy n) ->
    withNat $ \_ (_ :: Proxy k) ->
        property $ \x ->
            unshiftProxy @k @Proxy @n Proxy (shiftProxy Proxy x) === Just x
prop_shiftProxy_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
    withNat $ \k (_ :: Proxy k) ->
        unsafeWithKnownNat @(n + k) (n + k) $
            property $ \x ->
                maybe True (== x) (shiftProxy @k @Proxy @n Proxy <$> unshiftProxy Proxy x)

prop_valid_add = withNatPos $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            property $ \x y ->
                isValidFinite $ add @n @m x y
prop_getFinite_add = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            getFinite (add @n @m x y) === getFinite x + getFinite y

prop_valid_sub = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            either isValidFinite isValidFinite $ sub @n @m x y
prop_getFinite_sub = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            either (negate . getFinite) getFinite (sub @n @m x y) === getFinite x - getFinite y
prop_sub_Left_0 = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            sub @n @m x y =/= Left 0

prop_valid_multiply = withNatPos $ \n (_ :: Proxy n) ->
    withNatPos $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            property $ \x y ->
                isValidFinite $ multiply @n @m x y
prop_getFinite_multiply = withNatPos $ \_ (_ :: Proxy n) ->
    withNatPos $ \_ (_ :: Proxy m) ->
        property $ \x y ->
            getFinite (multiply @n @m x y) === getFinite x * getFinite y

prop_valid_combineSum = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            property $ \x ->
                isValidFinite $ combineSum @n @m x
prop_finites_combineSum = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            map (combineSum @n @m) (map Left finites ++ map Right finites) === finites

prop_valid_combineProduct = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            property $ \x ->
                isValidFinite (combineProduct @n @m x)
prop_finites_combineProduct = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            map (combineProduct @n @m) [(x, y) | y <- finites, x <- finites] === finites

prop_valid_separateSum = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            property $ \x ->
                either isValidFinite isValidFinite $ separateSum @n @m x
prop_finites_separateSum = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            map (separateSum @n @m) finites === map Left finites ++ map Right finites

prop_valid_separateProduct = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            property $ \x ->
                x {- could be discard -} `seq` isValidFinite (fst $ separateProduct @n @m x)
                    .&&. isValidFinite (snd $ separateProduct @n @m x)
prop_finites_separateProduct = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            map (separateProduct @n @m) finites === [(x, y) | y <- finites, x <- finites]

prop_combineSum_separateSum = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n + m) (n + m) $
            property $ \x ->
                combineSum @n @m (separateSum x) === x
prop_separateSum_combineSum = withNat $ \_ (_ :: Proxy n) ->
    withNat $ \_ (_ :: Proxy m) ->
        property $ \x ->
            separateSum @n @m (combineSum x) === x

prop_combineProduct_separateProduct = withNat $ \n (_ :: Proxy n) ->
    withNat $ \m (_ :: Proxy m) ->
        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
            property $ \x ->
                x {- could be discard -} `seq` combineProduct @n @m (separateProduct x) === x
prop_separateProduct_combineProduct = withNat $ \_ (_ :: Proxy n) ->
    withNat $ \_ (_ :: Proxy m) ->
        property $ \x ->
            force x {- could be discard -} `seq` separateProduct @n @m (combineProduct x) === x

return []
main = $quickCheckAll >>= \case
    True -> pure ()
    False -> exitFailure