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

<blockquote><p>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</p>

<p>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.</p></blockquote>

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

<blockquote><p>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:</p>

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

<p><interactive>:22:12: error:
    Illegal type signature: ‘Double’
      Type signatures are only allowed in patterns with ScopedTypeVariables</p>

<p>Wat? TypeVariables? There aren’t any!</p></blockquote>

<p>You can get the above to parse by passing <code>-XScopedTypeVariables</code> to GHC:</p>

<pre><code>$ 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)
</code></pre>