Add withCounterexample to get a re-useable handle on counterexamples

[MaximilianAlgehed]

The lack of actual values returned by quickCheck when a property fails has been a long standing friction. This PR introduces a simple combinator withCounterexample :: (Typeable a, Show a, Testable prop) => a -> prop -> Property that lets you "export" data to the Failure result of a property.

closes #117
closes #310

[MaximilianAlgehed]

The thing I don't like here is the use of the word "counterexample" as that already has a meaning in QuickCheck. I'm very open to suggestion!!

[nick8325]

I like it!

But also a while back I made a wrapper around QuickCheck which changes the API to have typed counterexamples:

https://hackage.haskell.org/package/quickcheck-with-counterexamples

So I don't know if we should: (1) merge your patch, (2) merge my thingy into main QuickCheck, (3) both. What do you think? Your approach is much simpler and has a far smaller API surface, but needs a bit more work from the user to use it (but maybe not so much).

[MaximilianAlgehed]

Maybe we can do both?

What I would love is if you could use the result of QuickCheck failing to re-run the same property with the counterexample - or with the counterexample slightly modified. That would open up a whole new way of doing testing whereby you would both be able to recheck the property after fixing things, modify the counterexample you have to better understand what's causing the property to fail, etc. etc.

With this light-weight approach we can get most of that given a bit of work from the user without changing the API much, but if we are willing to take the plunge on your approach that would allow us to make things much more seamless.

To reduce the burden on the user of this approach I would try first of all to integrate it with forAll - either by default or ad an optional thing.

Another thing I would like to try is splitting the implementation of Property so that the points of quantification are explicit, that way one could implement replaying a property given [Counterexample] on versions of QuickCheck built with Typeable.

The third thing if we really want to take the plunge is to make the Property type indexed. The thing I worry about with that is that it would completely overhaul the interface of QhickCheck and also risk making things difficult to keep Haskell98 compatible.

One might think that type indexing and wrapping things with existentials or similar could reduce the amount of type casting necessary to deal with replaying a counterexample, but I worry that won't be the case so long as we wish to keep the API at least somewhat similar.

So to sum up my views: I like the fact that this is a conservative extension to the API, I really like your approach making things nice and typed and making all quantification points explicit and repayable with a counterexample, and I think we can figure out a way of getting the best of both worlds. We should just settle on a couple of questions:

1. Do we want to automatically include a withCounterexample when you use forAll?
2. Do we think its possible to change the implementation of Property so that we can replay a property given a counterexample?
3. Is there anything else that we want to add the the API that would be conservative? (I can imagine a quickCheckCounterexample :: Testable p => p -> IO (Maybe [Counterexample]) foe example)

[MaximilianAlgehed]

I discovered a seriously cool feature in ghci that I didn't know about today. It appears it will resolve the type of existentially quantified variables with Typeable for you! I implemented quickCheckCounterexample on this fork but for untyped Property and amazingly ghci appears to know the type of the existentially quantified variable:

$> :t quickCheckCounterexample
quickCheckCounterexample
  :: Testable prop => prop -> IO Counterexamples
$> c :! _ <- quickCheckCounterexample $ \ x -> withCounterexample (x :: Double) (x > 0)
*** Failed! Falsified (after 1 test):  
0.0
$> :t c
c :: Double

Interestingly, it appears to only work for <- bindings, not let:

$> let a :! _ = (0 :: Int) :! NoCounterexamples
<< Big ugly type error >>

It also doesn't work for data types defined in the shell, but it does work for data types defined in the source code.

The cool thing about this is that it might allow us a fairly good middle ground between the strongly typed approach in your thing @nick8325 and a smaller API footprint while not making it a PITA to work with in ghci. I think that's pretty cool!

[nick8325]

Cool! A couple of comments for now!

• When it comes to re-running the same test case or a slightly modified version of it - I don't think that withCounterexample helps there, does it?
• If we want to automatically store typed counterexamples, we would need to change the types of forAll etc to have a Typeable constraint. In the past this would have been a big and annoying breaking change so I didn't seriously consider it, but nowadays GHC automatically generates a Typeable instance for every type so it might be reasonable.

[MaximilianAlgehed]

I think you're right on the re-runnig point - with the current design of Property. But that can possibly change to include the binding-sites.

On the second point I agree and I would put that change under an ifndef NO_AUTO_TYPEABLE pragma to make sure it doesn't become annoying for versions of GHC that don't support automatic typeable.

[MaximilianAlgehed]

Regarding changing the Property type - this might require both existential quantification and might not be entirely feasible. For that reason I don't think it's immediately obvious it can be done without a massive headache. But we can investigate it / put it on the "maybe later" pile.

[MaximilianAlgehed]

I'm uhming and ahing a bit about the idea of putting Typeable on forAll for the sake of this. You'd also have to put it on Testable and in all sorts of other places. That would be a major breaking change and I don't think it's worth delaying this conservative extension for the sake of figuring out how to minimize the damage of a big breaking change. I propose this: we merge this change (perhaps with some cleanup? I'll go over it again) and we make an issue about investigating always producing Counterexamples in the future with a nod to the fact that it would break a lot of stuff.

We could also introduce the interface in quickcheck-with-counterexamples as a module in QuickCheck that builds on this extension to implement what I presume you do with an IORef now in the future. Does that sound like a good idea @nick8325 ?

[MaximilianAlgehed]

To avoid naming confusion I've renamed the new Counterexample Witness instead.

[nick8325]

+1 to naming things Witness instead of Counterexample, and I'm pro this pull request in general, but some comments by way of bikeshedding:

• There is already (the not wonderfully named) counterexample :: Testable prop => String -> prop -> Property. Should the new combinator perhaps be called witness for consistency?
• The Cex constructor should be renamed to e.g. Witness
• What is the purpose of the Witnesses type (as opposed to e.g. just exposing a [Witness])?
• Witnesses is not exported from Test.QuickCheck
• Witnesses is missing a Show instance
• I'm not thrilled about the proliferation of quickCheck* functions (and e.g. we would also need verboseCheckWitness and verboseCheckWithWitness - and, given that there's no function of type Result -> Witnesses, maybe even quickCheckWitnessResult, quickCheckWitnessWithResult, verboseCheckWitnessResult, verboseCheckWitnessWithResult! )

Suggestion: we could get rid of one of Witness and Witnesses. So either:

• Drop Witnesses, and just expose witness :: [Witness] to the user, or
• Drop Witness, so that Result would have a field witness :: Witnesses

Then rather than quickCheckWitness and its many variants, users can just use quickCheckResult together with witnesses, and this could be documented in withWitness.

[MaximilianAlgehed]

Drop Witnesses, and just expose witness :: [Witness] to the user, or

Done. This is probably the least bad option. As per the docs on witness now, you can do:

-- >>> [Wit x] <- fmap witnesses . quickCheckResult $ \ x -> witness x $ x == (0 :: Int)
-- *** Failed! Falsified (after 2 tests):
-- 1
-- >>> x
-- 1
-- >>> :t x
-- x :: Int