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

import Control.Exception
import Control.DeepSeq
import Control.Monad
import Data.Bifunctor
import Data.Int
import Data.List
import Data.Maybe
import Data.Proxy
import Data.Type.Equality
import Data.Typeable
import Data.Void
import Data.Word
import GHC.TypeLits
import System.Exit
import Test.QuickCheck hiding (Small)
import Unsafe.Coerce
import Numeric.Natural

import Debug.Trace

import Data.Finite.Integral
import Data.Finite.Internal.Integral

newtype SmallNonNeg a = SmallNonNeg { getSmallNonNeg :: a }
    deriving (Show)

instance (Integral a, Arbitrary a) => Arbitrary (SmallNonNeg a) where
    arbitrary = SmallNonNeg <$> arbitrarySizedNatural
    shrink (SmallNonNeg x) = SmallNonNeg <$> shrink x

instance Arbitrary Natural where
    arbitrary = fromInteger . getNonNegative <$> arbitrary

instance CoArbitrary Natural where
    coarbitrary n = coarbitrary (toInteger n)

newtype Small a n = Small (Finite a n)
    deriving (Show)

newtype Big a n = Big (Finite a n)
    deriving (Show)

newtype Edgy a n = Edgy (Finite a n)
    deriving (Show)

instance
    (Arbitrary a, SaneIntegral a, KnownIntegral a n)
    => Arbitrary (Small a n) where
    arbitrary
        | intVal @n @a Proxy == 0 = discard
        | otherwise = Small . Finite . (`mod` n)
            . getSmallNonNeg <$> arbitrary
        where n = intVal @n Proxy
    shrink (Small (Finite x)) = Small <$> mapMaybe packFinite (shrink x)

instance
    (Arbitrary a, SaneIntegral a, KnownIntegral a n)
    => Arbitrary (Big a n) where
    arbitrary
        | intVal @n @a Proxy == 0 = discard
        | otherwise = Big . Finite . ((n - 1) -) . (`mod` n)
            . getSmallNonNeg <$> arbitrary
        where n = intVal @n Proxy
    shrink (Big (Finite x)) = Big <$> mapMaybe packFinite (shrink x)

instance CoArbitrary a => CoArbitrary (Big a n) where
    coarbitrary (Big (Finite x)) = coarbitrary x

instance
    (Arbitrary a, SaneIntegral a, KnownIntegral a n)
    => Arbitrary (Edgy a n) where
    arbitrary
        | intVal @n @a Proxy == 0 = discard
        | otherwise = Edgy . Finite <$> oneof
            [ (`mod` n) . getSmallNonNeg <$> arbitrary
            , ((n - 1) -) . (`mod` n) . getSmallNonNeg <$> arbitrary
            ]
        where n = intVal @n Proxy
    shrink (Edgy (Finite x)) = Edgy <$> mapMaybe packFinite (shrink x)

data SLimited a where
    SLimited :: (Limited a n, KnownNat n) => Proxy n -> SLimited a

class MkSLimited (lim :: Maybe Nat) where
    mkSLimited
        :: forall a. (SaneIntegral a, Limit a ~ lim)
        => Integer -> Maybe (SLimited a)

instance KnownNat lim => MkSLimited ('Just lim) where
    mkSLimited
        :: forall a. (SaneIntegral a, Limit a ~ 'Just lim)
        => Integer -> Maybe (SLimited a)
    mkSLimited n = case someNatVal n of
        Just (SomeNat p)
            | n <= natVal @lim Proxy
            -> Just $ unsafeWithLimited (Proxy @a) p $ SLimited p
        _ -> Nothing

instance MkSLimited 'Nothing where
    mkSLimited n = case someNatVal n of
        Just (SomeNat p) -> Just $ SLimited p
        _ -> Nothing

genSmall, genOver7, genOver8, genOver15, genOver16, genOver31, genOver32,
    genOver63, genOver64, genOverI, genOverW, genUnder7, genUnder8, genUnder15,
    genUnder16, genUnder32, genUnder63, genUnder64, genUnderI, genUnderW
    :: Gen Integer
genSmall = getNonNegative <$> arbitrary
genOver7 = (toInteger (maxBound @Int8) +) <$> genSmall
genOver8 = (toInteger (maxBound @Word8) +) <$> genSmall
genOver15 = (toInteger (maxBound @Int16) +) <$> genSmall
genOver16 = (toInteger (maxBound @Word16) +) <$> genSmall
genOver31 = (toInteger (maxBound @Int32) +) <$> genSmall
genOver32 = (toInteger (maxBound @Word32) +) <$> genSmall
genOver63 = (toInteger (maxBound @Int64) +) <$> genSmall
genOver64 = (toInteger (maxBound @Word64) +) <$> genSmall
genOverI = (toInteger (maxBound @Int) +) <$> genSmall
genOverW = (toInteger (maxBound @Word) +) <$> genSmall
genUnder7 = ((toInteger (maxBound @Int8) -) <$> genSmall) `suchThat` (>= 0)
genUnder8 = ((toInteger (maxBound @Word8) -) <$> genSmall) `suchThat` (>= 0)
genUnder15 = ((toInteger (maxBound @Int16) -) <$> genSmall) `suchThat` (>= 0)
genUnder16 = ((toInteger (maxBound @Word16) -) <$> genSmall) `suchThat` (>= 0)
genUnder31 = ((toInteger (maxBound @Int32) -) <$> genSmall) `suchThat` (>= 0)
genUnder32 = ((toInteger (maxBound @Word32) -) <$> genSmall) `suchThat` (>= 0)
genUnder63 = ((toInteger (maxBound @Int64) -) <$> genSmall) `suchThat` (>= 0)
genUnder64 = ((toInteger (maxBound @Word64) -) <$> genSmall) `suchThat` (>= 0)
genUnderI = ((toInteger (maxBound @Int) -) <$> genSmall) `suchThat` (>= 0)
genUnderW = ((toInteger (maxBound @Word) -) <$> genSmall) `suchThat` (>= 0)

shrinkSLimited
    :: (SaneIntegral a, MkSLimited (Limit a), Arbitrary a)
    => SLimited a -> [SLimited a]
shrinkSLimited (SLimited p) = mapMaybe mkSLimited $ shrink $ natVal p

instance Arbitrary (SLimited Integer) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
        , genOverI, genUnderW, genOverW ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Natural) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
        , genOverI, genUnderW, genOverW ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Word) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
        , genOverI, genUnderW ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Int) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Word8) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Int8) where
    arbitrary = oneof
        [ genSmall, genUnder7 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Word16) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Int16) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Word32) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Int32) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31 ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Word64) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genOver63, genUnder64, genOverI, genUnderW
        , genOverW ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

instance Arbitrary (SLimited Int64) where
    arbitrary = oneof
        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
        , genOver32, genUnder63, genUnderI, genOverI, genUnderW, genOverW ]
        `suchThatMap` mkSLimited
    shrink = shrinkSLimited

newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a }

instance (SaneIntegral a, MkSLimited (Limit a), Arbitrary (SLimited a))
    => Arbitrary (SmallLimited a) where
    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkSLimited
    shrink = map SmallLimited . shrink . getSmallLimited

type Good a =
    ( Show a
    , Read a
    , NFData a
    , Typeable a
    , SaneIntegral a
    , Arbitrary a
    , Arbitrary (SLimited a)
    , MkSLimited (Limit a)
    , CoArbitrary a
    )

data SType where
    SType :: Good a => Proxy a -> SType

forType :: forall prop. Testable prop
    => (forall a. Good a => Proxy a -> prop)
    -> Property
forType prop = forAllBlind gen $ \case
    (name, SType p) -> counterexample @prop ("@" ++ name) $ prop p
    where
        gen = elements
            [ ("Integer", SType @Integer Proxy)
            , ("Natural", SType @Natural Proxy)
            , ("Word", SType @Word Proxy)
            , ("Int", SType @Int Proxy)
            , ("Word8", SType @Word8 Proxy)
            , ("Int8", SType @Int8 Proxy)
            , ("Word16", SType @Word16 Proxy)
            , ("Int16", SType @Int16 Proxy)
            , ("Word32", SType @Word32 Proxy)
            , ("Int32", SType @Int32 Proxy)
            , ("Word64", SType @Word64 Proxy)
            , ("Int64", SType @Int64 Proxy)
            ]

forLimit'
    :: forall a. SaneIntegral a
    => Gen (SLimited a)
    -> (SLimited a -> [SLimited a])
    -> (forall n. (KnownIntegral a n, Limited a n)
        => (forall i. Num i => i) -> Proxy n -> Property)
    -> Property
forLimit' gen shr prop = forAllShrinkBlind @Property gen shr $ \case
    SLimited p -> counterexample ("@" ++ show (natVal p)) $
        prop (fromInteger $ natVal p) p

forLimit
    :: forall a. (SaneIntegral a, Arbitrary (SLimited a))
    => (forall n. (KnownIntegral a n, Limited a n)
        => (forall i. Num i => i) -> Proxy n -> Property)
    -> Property
forLimit = forLimit' @a arbitrary shrink


forPositiveLimit
    :: forall a. (SaneIntegral a, Arbitrary (SLimited a))
    => (forall n. (KnownIntegral a n, Limited a n)
        => (forall i. Num i => i) -> Proxy n -> Property)
    -> Property
forPositiveLimit = forLimit' @a
    (arbitrary `suchThat` isPositive)
    (filter isPositive . shrink)
    where
        isPositive :: SLimited a -> Bool
        isPositive (SLimited p) = natVal p > 0

forSmallLimit
    :: forall a. (SaneIntegral a, Arbitrary (SmallLimited a))
    => (forall n. (KnownIntegral a n, Limited a n)
        => (forall i. Num i => i) -> Proxy n -> Property)
    -> Property
forSmallLimit = forLimit' @a
    (getSmallLimited <$> arbitrary)
    (map getSmallLimited . shrink . SmallLimited)

unsafeWithKnownIntegral
    :: forall n a. (SaneIntegral a, MkSLimited (Limit a), Typeable a)
    => Integer -> ((KnownNat n, Limited a n) => Property) -> Property
unsafeWithKnownIntegral n prop
    | Just (SLimited (_ :: Proxy n')) <- mkSLimited @_ @a n
    , Refl <- unsafeCoerce Refl :: n :~: n'
    = prop
    | otherwise = discard

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

prop_isvalid_under = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x ->
    x < 0 ==> not $ isValidFinite @n @a (Finite x)
prop_isvalid_over = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    property $ \x ->
    not (x >= n) .||. not (isValidFinite @n @a (Finite x))

prop_valid_finite = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
    evaluate (isValidFinite $ finite @n @a x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_getFinite_finite = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
    evaluate (getFinite (finite @n @a x) == x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_finite_getFinite = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    finite (getFinite x) === x

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

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

prop_valid_toEnum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
    evaluate (isValidFinite $ toEnum @(Finite a n) x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_fromEnum_toEnum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x -> ioProperty $
    evaluate (fromEnum (toEnum @(Finite a n) x) == x)
        `catch` \(_ :: ErrorCall) -> pure True
prop_toEnum_fromEnum = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    n <= toInteger (maxBound @Int) ==> toEnum (fromEnum x) == x

prop_valid_enumFrom = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) ->
    all isValidFinite [x..]
prop_getFinite_enumFrom = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) ->
    map getFinite [x..]
        === takeWhile (isJust . packFinite @n @a) [getFinite x..]

prop_valid_enumFromTo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) (Big y) ->
    all isValidFinite [x..y]
prop_valid_enumFromTo' = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) ->
    all isValidFinite [x..y]
prop_getFinite_enumFromTo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) (Big y) ->
    map getFinite [x..y] === [getFinite x..getFinite y]
prop_getFinite_enumFromTo' = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) ->
    map getFinite [x..y] === [getFinite x..getFinite y]

prop_valid_enumFromThen = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) (Big y) ->
    x < y ==> all isValidFinite [x,y..]
prop_valid_enumFromThen' = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) ->
    x > y ==> all isValidFinite [x,y..]
prop_getFinite_enumFromThen = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) (Big y) ->
    x < y ==> map getFinite [x,y..]
        === takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..]
prop_getFinite_enumFromThen' = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) ->
    x > y ==> map getFinite [x,y..]
        === takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..]

prop_valid_enumFromThenTo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) (Small z) ->
    x /= y ==> all isValidFinite [x,y..z]
prop_getFinite_enumFromThenTo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Small x :: Small a n) (Small y) (Small z) ->
    x /= y ==> map getFinite [x,y..z] === [getFinite x,getFinite y..getFinite z]

prop_nonint_succ = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Big x :: Big a n) ->
    case packFinite @n @a $ succ $ getFinite x of
        Nothing -> discard
        Just y -> y === succ x

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

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

prop_valid_minus = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) (Edgy y) ->
        isValidFinite $ x - y
prop_getFinite_minus = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) (Edgy y) ->
    (getFinite x + n - getFinite y - getFinite (x - y)) `mod` n === 0

prop_valid_times = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) (Edgy y) ->
        isValidFinite $ x * y
prop_getFinite_times = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) (Edgy y) ->
    (toInteger (getFinite x) * toInteger (getFinite y)
        - toInteger (getFinite $ x * y)) `mod` n === 0

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

prop_valid_abs = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ abs x
prop_getFinite_abs = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    getFinite (abs x) === abs (getFinite x)

prop_valid_signum = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ signum x
prop_getFinite_signum = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    getFinite (signum x) === signum (getFinite x)

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

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

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

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

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

prop_force = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \_ (_ :: Proxy n) ->
    ioProperty $
    evaluate (rnf @(Finite a n) (error "Expected exception") `seq` False)
        `catch` (\(_ :: ErrorCall) -> pure True)

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

prop_valid_finites = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \_ (_ :: Proxy n) ->
    property $
    all isValidFinite $ finites @n @a
prop_finites_minMax = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    n > 0 ==> minBound `elem` finites @n @a .&&. maxBound `elem` finites @n @a
prop_finites_ordered = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \_ (_ :: Proxy n) ->
    finites @n @a === sort finites
prop_finites_all = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \_ (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    x -- could be discard
        `seq` x `elem` finites @n @a

prop_valid_modulo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    property $ \x ->
    isValidFinite $ modulo @n @a x
prop_getFinite_modulo = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \x ->
    (toInteger x - toInteger (getFinite $ modulo @n @a x)) `mod` n === 0

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

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

prop_valid_natToFinite = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $
    property $
    isValidFinite $ natToFinite @n @m @a Proxy
prop_getFinite_natToFinite = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $
    getFinite (natToFinite @n @m @a Proxy) === n

prop_valid_weaken = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ weaken x
prop_finites_weaken = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    map (weaken @n @a) finites === init finites

prop_valid_strengthen = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a (n + 1)) ->
    maybe True isValidFinite $ strengthen x
prop_finites_strengthen = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    map (strengthen @n @a) finites === map Just finites ++ [Nothing]

prop_valid_shift = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ shift x
prop_finites_shift = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    map (shift @n @a) finites === drop 1 finites

prop_valid_unshift = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a (n + 1)) ->
    maybe True isValidFinite $ unshift x
prop_finites_unshift = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    map (unshift @n @a) finites === [Nothing] ++ map Just finites

prop_valid_weakenN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ weakenN @n @m @a x
prop_finites_weakenN = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    map (weakenN @n @m @a) finites === take n finites

prop_valid_strengthenN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    forLimit @a $ \_ (_ :: Proxy m) ->
    property $ \(Edgy x :: Edgy a n) ->
    maybe True isValidFinite $ strengthenN @n @m x
prop_finites_strengthenN = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    map (strengthenN @n @m @a) finites
        === take n (map Just finites) ++ replicate (n - m) Nothing

prop_valid_shiftN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ shiftN @n @m @a x
prop_finites_shiftN = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    map (shiftN @n @m @a) finites === drop (m - n) finites

prop_valid_unshiftN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \_ (_ :: Proxy n) ->
    forLimit @a $ \_ (_ :: Proxy m) ->
    property $ \(Edgy x :: Edgy a n) ->
    maybe True isValidFinite $ unshiftN @n @m x
prop_finites_unshiftN = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    map (unshiftN @n @m @a) finites
        === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)

prop_valid_weakenProxy = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ weakenProxy @n @k Proxy x
prop_finites_weakenProxy = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    map (weakenProxy @n @k @a Proxy) finites === take n finites

prop_valid_strengthenProxy = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a (n + k)) ->
    maybe True isValidFinite $ strengthenProxy @n @k Proxy x
prop_finites_strengthenProxy = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    map (strengthenProxy @n @k @a Proxy) finites
        === take n (map Just finites) ++ replicate k Nothing

prop_valid_shiftProxy = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a n) ->
    isValidFinite $ shiftProxy @n @k Proxy x
prop_finites_shiftProxy = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    map (shiftProxy @n @k @a Proxy) finites === drop k finites

prop_valid_unshiftProxy = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a (n + k)) ->
    maybe True isValidFinite $ unshiftProxy @n @k Proxy x
prop_finites_unshiftProxy = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    map (unshiftProxy @n @k @a Proxy) finites
        === replicate k Nothing ++ map Just finites

prop_strengthen_weaken = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    strengthen (weaken x) === Just x
prop_weaken_strengthen = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a (n + 1)) ->
    maybe True (== x) (weaken <$> strengthen x)

prop_unshift_shift = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    property $ \(Edgy x :: Edgy a n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    unshift (shift x) === Just x
prop_shift_unshift = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
    property $ \(Edgy x :: Edgy a (n + 1)) ->
    maybe True (== x) (shift <$> unshift x)

prop_strengthenN_weakenN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    property $ \(Edgy x :: Edgy a n) ->
    strengthenN (weakenN @n @m x) === Just x
prop_weakenN_strengthenN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    m <= n ==> unsafeWithInequality @m @n $
    property $ \(Edgy x :: Edgy a n) ->
    maybe True (== x) (weakenN <$> strengthenN @n @m x)

prop_unshiftN_shiftN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    n <= m ==> unsafeWithInequality @n @m $
    property $ \(Edgy x :: Edgy a n) ->
    unshiftN (shiftN @n @m x) === Just x
prop_shiftN_unshiftN = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    m <= n ==> unsafeWithInequality @m @n $
    property $ \(Edgy x :: Edgy a n) ->
    maybe True (== x) (shiftN <$> unshiftN @n @m x)

prop_strengthenProxy_weakenProxy = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    property $ \(Edgy x :: Edgy a n) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    strengthenProxy Proxy (weakenProxy @n @k Proxy x) === Just x
prop_weakenProxy_strengthenProxy = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a (n + k)) ->
    maybe True (== x) (weakenProxy Proxy <$> strengthenProxy @n @k Proxy x)

prop_unshiftProxy_shiftProxy = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    property $ \(Edgy x :: Edgy a n) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    unshiftProxy Proxy (shiftProxy @n @k Proxy x) === Just x
prop_shiftProxy_unshiftProxy = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \k (_ :: Proxy k) ->
    unsafeWithKnownIntegral @(n + k) @a (n + k) $
    property $ \(Edgy x :: Edgy a (n + k)) ->
    maybe True (== x) (shiftProxy Proxy <$> unshiftProxy @n @k Proxy x)

prop_valid_add = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
    isValidFinite $ add x y
prop_getFinite_add = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
    getFinite (add x y) === getFinite x + getFinite y

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

prop_valid_multiply = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
    isValidFinite $ multiply x y
prop_getFinite_multiply = forType $ \(_ :: Proxy a) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    forPositiveLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
    getFinite (multiply x y) === getFinite x * getFinite y

prop_valid_combineSum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \e ->
    isValidFinite $ combineSum
        $ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e
prop_finites_combineSum = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    map (combineSum @n @m @a) (map Left finites ++ map Right finites)
        === finites

prop_valid_combineZero = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @0 @a 0 $
    ioProperty $ evaluate (isValidFinite $ combineZero @a $ error "test")
        `catch` \(ErrorCall msg) -> pure (msg == "test")
prop_finites_combineZero = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @0 @a 0 $
    map (combineZero @a) [] === finites

prop_valid_combineProduct = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \p ->
    isValidFinite $ combineProduct
        $ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p
prop_finites_combineProduct = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    map (combineProduct @n @m @a) [(x, y) | y <- finites, x <- finites]
        === finites

prop_valid_combineOne = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @1 @a 1 $
    property $ isValidFinite $ combineOne @a ()
prop_finites_combineOne = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @1 @a 1 $
    property $ [combineOne @a ()] === finites

prop_valid_combineExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    property $ \(Blind (f :: Big a n -> Big a m)) ->
    isValidFinite $ combineExponential (\x -> case f (Big x) of Big y -> y)
prop_finites_combineExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    if m ^ n > 2000000 then property () else
    m ^ n <= 10000 ==>
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    property $
        [ combineExponential ((xs !!) . fromIntegral . getFinite @n @a)
        | xs <- reverse <$> replicateM n (finites @m)
        ] === finites

prop_valid_separateSum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \(Edgy x :: Edgy a (n + m)) ->
    either isValidFinite isValidFinite $ separateSum @n @m x
prop_finites_separateSum = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    map (separateSum @n @m @a) finites === map Left finites ++ map Right finites

prop_seq_separateZero = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @0 @a 0 $
    ioProperty $ evaluate (absurd $ separateZero @a $ error "test")
        `catch` \(ErrorCall msg) -> pure (msg == "test")
prop_finites_separateZero = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @0 @a 0 $
    map (separateZero @a) finites === []

prop_valid_separateProduct = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) ->
    x -- could be discard
        `seq` isValidFinite (fst $ separateProduct @n @m x)
        .&&. isValidFinite (snd $ separateProduct @n @m x)
prop_finites_separateProduct = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    map (separateProduct @n @m @a) finites
        === [(x, y) | y <- finites, x <- finites]

prop_finites_separateOne = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @1 @a 1 $
    map (separateOne @a) finites === [()]

prop_valid_separateExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    property $ \(Big f :: Big a (m ^ n)) (Big x :: Big a n) ->
    f `seq` x -- could be discard
        `seq` isValidFinite (separateExponential @n @m @a f x)
prop_finites_separateExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    if m ^ n > 2000000 then property () else
    m ^ n <= 10000 ==>
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    map (<$> finites) (map (separateExponential @n @m @a) finites)
        === [reverse xs | xs <- replicateM n finites]

prop_combineSum_separateSum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \(Edgy x :: Edgy a (n + m)) ->
    combineSum (separateSum @n @m x) === x
prop_separateSum_combineSum = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n + m) @a (n + m) $
    property $ \e ->
    let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e in
    separateSum (combineSum x) === x

prop_combineProduct_separateProduct = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) ->
    x -- could be discard
        `seq` combineProduct (separateProduct @n @m x) === x
prop_separateProduct_combineProduct = forType $ \(_ :: Proxy a) ->
    forLimit @a $ \n (_ :: Proxy n) ->
    forLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
    property $ \p ->
    let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p in
    force x -- could be discard
        `seq` separateProduct (combineProduct x) === x

prop_combineOne_separateOne = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @1 @a 1 $
    property $ \(Big x :: Big a 1) ->
    combineOne (separateOne @a x) === x
prop_separateOne_combineOne = forType $ \(_ :: Proxy a) ->
    unsafeWithKnownIntegral @1 @a 1 $
    property $ \x ->
    separateOne (combineOne @a x) === x

prop_separateExponential_combineExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    property $ \(Blind (f :: Big a n -> Big a m)) ->
    let f' x = case f (Big x) of Big y -> y in
    force (f' <$> listToMaybe finites) -- could be discard
        `seq` (separateExponential @n @m @a (combineExponential f') <$> finites)
            === (f' <$> finites)
prop_combineExponential_separateExponential = forType $ \(_ :: Proxy a) ->
    forSmallLimit @a $ \n (_ :: Proxy n) ->
    forSmallLimit @a $ \m (_ :: Proxy m) ->
    unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
    property $ \(Big f :: Big a (m ^ n)) ->
    f `seq` -- could be discard
        combineExponential (separateExponential @n @m @a f) === f

prop_valid_castFinite = forType $ \(_ :: Proxy b) ->
    forType $ \(_ :: Proxy a) ->
    forPositiveLimit @b $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @n @a n $
    property $ \(Edgy x :: Edgy a n) ->
        isValidFinite $ castFinite @b x
prop_sym_castFinite = forType $ \(_ :: Proxy a) ->
    forType $ \(_ :: Proxy b) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @n @b n $
    property $ \(Edgy x :: Edgy b n) ->
        castFinite @b (castFinite @a x) === x
prop_trans_castFinite = forType $ \(_ :: Proxy a) ->
    forType $ \(_ :: Proxy b) ->
    forType $ \(_ :: Proxy c) ->
    forPositiveLimit @a $ \n (_ :: Proxy n) ->
    unsafeWithKnownIntegral @n @b n $
    unsafeWithKnownIntegral @n @c n $
    property $ \(Edgy x :: Edgy a n) ->
        castFinite @c (castFinite @b x) === castFinite @c x

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