Counter-example too general (includes incorrect counter-examples)

[rudymatela]

Consider the following faulty sort implementation along with a property:

sort :: Ord a => [a] -> [a]
sort [] = []
sort (x:xs) = sort (filter (< x) xs)
           ++ [x]
           ++ sort (filter (> x) xs)

prop_sortCount :: Int -> [Int] -> Bool
prop_sortCount x xs = count x (sort xs) == count x xs
  where
  count x = length . filter (== x)

SmartCheck does work flawlessly if we uncurry the property so it can generalize the second argument as well:

> smartCheck scStdArgs{format = PrintString} $ uncurry prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 8 tests):
*** Smart-shrunk value:
(5,[5,5])

*** Extrapolated value:
forall values x0: (,) 5 (: 5 (: 5 x0))

However, if we flip the property so that SmartCheck can generalize only the second argument, the reported generalization is incorrect:

*Main Test.QuickCheck> smartCheck scStdArgs{format = PrintString} $ flip prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 11 tests):
*** Non SmartChecked arguments:
0
*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
[8,-10,9,0,0,-9,-3,4,-4]

*** Extrapolated value:
forall values x0:
: 8 x0

By incorrect, I mean it includes values that are not counter-examples, like 8:[] or 8:7:6:[]. Of course, it also includes correct counter-examples, like: 8:8:[].

I would expect it to report something like:

*** Extrapolated value:
forall values x0:
: 8 (: 9 (: 0 (: 0 x0)))

I understand this may be hard to fix because of the nature of the generalization algorithm that is being used. The algorithm is unsound in the general case anyway.

I have run this with default values. Maybe just changing the parameters may get rid of the incorrect generalization.

Notes

The sort example is also used in issue #11.