On Thu, Jan 17, 2019 at 06:28:32PM +0100, Johannes Waldmann wrote:

Prelude Test.LeanCheck> checkFor 1000 $ \ x y z -> isInfinite x || isInfinite y || isInfinite z || (x::Double) + (y+z) == (x+y)+z *** Failed! Falsifiable (after 306 tests): 1.0 1.0 0.3333333333333333

Turns out the enumeration in Leancheck uses Rationals, while Smallcheck uses encodeFloat, which happens to produce only “nice” numbers (very few bits set) in the beginning.

I improved the LeanCheck floating enumeration starting with v0.8.0 to catch exactly this kind of error. :-)

PS: this post wouldn’t be complete without me complaining that I cannot (easily) put the type annotation where it belongs - in the declaration of the name:

Prelude Test.LeanCheck> check $ \ (x::Double) y z -> x + (y+z) == (x+y)+z

:22:12: error: Illegal type signature: ‘Double’ Type signatures are only allowed in patterns with ScopedTypeVariables

Wat? TypeVariables? There aren’t any!

You can get the above to parse by passing -XScopedTypeVariables to GHC:

$ ghci -XScopedTypeVariables
> import Test.LeanCheck
> check $ \(x::Double) y z -> x + (y+z) == (x+y) + z
*** Failed! Falsifiable (after 87 tests):
0.0 Infinity (-Infinity)