使用SmallCheck测试整数集无穷性失败，如何调整测试方案？

要验证整数集的无穷性——对任意整数n，存在整数m满足m > n，使用SmallCheck编写的测试代码如下：

...
, testProperty "infinity of integers set" $
  forAll $ \(n::Integer) -> exists $ \m -> m > n
...

但测试失败，报错信息：

...
  infinity of Ints:              FAIL
    there exists 5 such that
      argument does not exist
    Use -p '/infinity of Ints/' to rerun this test only.
...

交换forall与exists的量词顺序后仍然失败，推测是两者使用了相同的量化深度：当n取到当前深度的最大值时，无法在同一范围内找到更大的m。尝试调整exists部分的深度，但localOption需要TestTree作为参数，而exists $ ...返回的是Property类型，不知道如何修改。

方案1：绕开exists量词，直接构造满足条件的m #

既然明确知道对任意n，n+1必然大于n，可以完全不用exists，直接构造这个m来验证：

, testProperty "infinity of integers set" $
  forAll $ \(n::Integer) -> property (n + 1 > n)

这种方式避开了SmallCheck的量化深度限制，不需要生成候选m，直接用逻辑上必然成立的实例完成验证，简洁又可靠。

方案2：给exists单独设置更高的量化深度 #

如果一定要保留exists量词，可以使用SmallCheck的withDepth函数为exists部分设置比forall更高的深度，确保能生成比n更大的m：

import Test.SmallCheck (withDepth)

...
, testProperty "infinity of integers set" $
  forAll $ \(n::Integer) -> exists $ withDepth (\d -> d + 1) $ \m -> m > n
...

也可以通过localOption在测试树级别整体调整深度，但方案1是最优选择，因为它直接利用整数的数学性质，不依赖测试框架的量化逻辑。

内容的提问来源于stack exchange，提问作者RandomB