Only activate existential sub-value generalization when there is more than one constructor
This is more of a feature request than a bug itself.
When there is only one possible constructor, existential sub-value generalization does not produce a very useful result.
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)
The property fails, as shown by QuickCheck:
> quickCheck prop_sortCount
*** Failed! Falsifiable (after 51 tests and 9 shrinks):
21
[21,21]
The generalization produced by SmartCheck is not very useful, see:
> smartCheck scStdArgs{format = PrintString} (prop_sortCount :: Int -> [Int] -> Bool)
*** Failed! Falsifiable (after 57 tests and 10 shrinks):
*** Non SmartChecked arguments:
[-10,-10]
*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
-10
*** Extrapolated value:
forall constructors C0:
there exist arguments x̅ s.t.
C0
The existential sub-value generalization is correct: for all possible constructors (GHC.Int) there exists a value (-10) that falsifies the property. But that is obvious from the reported counter-example itself.
Perhaps existential sub-value generalization should only activate when there is more than one constructor that can be placed? (In which case it is really useful -- cf. divSubTerms example from SmartCheck's paper.)
Notes
If we set runExists = False, SmartCheck reports that it cannot extrapolate a
new value -- this is what I would intuitively expect in this case.
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))
The sort example is also used in issue #12.