Get counterexample from Failure

[japesinator]

I'm working on an application using hedgehog and attempting to do some further analysis on why a given test failed. To do this, I'd like to get a specific counterexample for a given property (not necessarily a Property, willing to manipulate the types if necessary).

I attempted to do this by looking into Failures, but as far as I can tell the information on how something failed is represented as a String.

Ideally, I'd like something :: PropertyT m a -> m a or similar. Is this possible? Happy to contribute code if necessary.

[arianvp]

I had the exact same question today, and someone else seems to have done this with quickcheck using
type families:

https://github.com/nick8325/quickcheck-with-counterexamples

Should be possible to add it to Hedgehog too.

I have many datatypes for which I don't have Show instances (on purpose, for example data Password), which I still want to use in property-based testing, but currently I can't which is very frustrating.

[thumphries]

I think this can be done at the PropertyT level, as you suggest.

If you add a type parameter to Result, you should be able to write a variant of check / recheck that produces an a on failure. We could probably do so without breaking any public APIs.

[thumphries]

If you'd like to work on this, get in touch and we can add you to the Hedgehog Slack.

[arianvp]

I'm definitely open to give it a shot! E-mail is on my Github page / inside my commit logs

[arianvp]

I have made some sketches for the API to see if this stuff is possible, and it seems it is!
Just needs some actualy coding!

We can keep all the existing machinery GenT, TestT

and then created an indexed version of PropertyT

The nice thing is, that we can probably make a backwards compatible wrapper
around IxPropertyT that ignores all the extra state, and exposes the exact same old
interface. Old users will not have breaking changes, and new users can actually get counter examples back!

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

import qualified Prelude
import Prelude hiding ((>>=), return)
import Control.Monad
import Control.Applicative

-- | This is somewhere in Hedgehog already
checkIt :: TestT (GenT IO) () -> IO Bool
checkIt = undefined

class IxFunctor m where
  imap :: (a -> b) -> m j k a -> m j k b

class IxFunctor m =>
      IxPointed m
  where
  ireturn :: a -> m i i a

class IxPointed m =>
      IxApplicative m
  where
  iap :: m i j (a -> b) -> m j k a -> m i k b

class IxApplicative m =>
      IxMonad m
  where
  ibind :: m i j a -> (a -> m j k b) ->  m i k b

class IxMonadTrans t where
  ilift :: Monad m => m a -> t m i i a

-- | Simply use Hedgehog's GenT 
data GenT m a

instance Functor (GenT m) where
instance Applicative (GenT m) where
instance Monad (GenT m) where
instance Functor (TestT (GenT m)) where
instance Applicative (TestT (GenT m)) where
instance Monad (TestT (GenT m)) where

-- | Simply use Hedgehog's TestT
data TestT m a = TestT (m a)

infixr 5 :*

-- | Collects the inputs that our 'GenT's generated for our 'TestT's
data Inputs :: [*] -> * where
  N0 :: Inputs '[]
  (:*) :: x -> Inputs s -> Inputs (x : xs)

--- TODO: Implement. Can be done with  All Show xs => Show (Inputs xs)
showInputs :: Inputs xs -> String
showInputs = undefined


newtype IxStateT m i j a = IxStateT { runIxStateT :: i -> m (a, j) }

instance IxFunctor (IxStateT m)
instance IxPointed (IxStateT m)
instance IxApplicative (IxStateT m)
instance IxMonad (IxStateT m)



-- | Indexed version of PropertyT, that keeps track of what inputs 
-- we took from our GenT
type IxPropertyT m i j a = IxStateT (TestT (GenT m)) (Inputs i) (Inputs j) a

iget :: IxPropertyT m i i (Inputs i)
iget = IxStateT $ \s -> return (s, s)

iput :: Inputs j -> IxPropertyT m i j ()
iput s = IxStateT $ \_ -> return ((), s)

type PropertyT m a = IxPropertyT '[] '[] m a


data IxProperty j = IxProperty
  { propertyTest :: IxPropertyT IO '[] j ()
  }

iproperty :: IxPropertyT IO  '[] j () -> IxProperty  j
iproperty = IxProperty


number :: GenT m Prelude.Int
number = undefined
list :: GenT m a -> GenT m [a]
list = undefined

-- | Add an input
iforAllT :: Prelude.Monad m => GenT m a -> IxPropertyT m xs (a ': xs) a
iforAllT gen =
  IxStateT $ \x -> TestT (gen >>= \a -> return (a, a :* x))
  

runTestT :: TestT m a -> m a
runTestT = undefined

-- moc
runGenT :: GenT m a -> IO (Maybe a)
runGenT = undefined

-- | Takes a property, and either succeeds, or returns
-- the inputs that made it fail
check :: IxProperty j ->  IO (Maybe (Inputs j))
check (IxProperty (IxStateT f)) = do
  fmap (fmap snd) $ runGenT $ runTestT $ f N0
  

checkProp :: IO ()
checkProp = do
  x <- check prop_lol
  case x of
    Just counterexample -> putStrLn (showInputs counterexample)
    Nothing -> putStrLn "OK!"

prop_lol :: IxProperty '[[Int], Int, Int]
prop_lol = iproperty $ do
  x <- iforAllT number
  y <- iforAllT number
  stuff <- iforAllT $ list number
  return ()
  where
    (>>=) = ibind
    return = ireturn

[thumphries]

That's awesome and very promising!

I think there's room for both the simple approach (just use PropertyT's return parameter) and clever approach (indexed properties). The former is a lot easier for us to add to the API, will (I think) solve @japesinator 's problem, and is a thing I've wanted myself from time to time.

The latter is obviously a much more comprehensive approach and will probably make for a very compelling downstream library, hedgehog-indexed or something.

[arianvp]

Yes I agree. I'll see if I can fix the "simple" approach too while I'm at it.

However, I'm not sure yet if downstreaming is the best solution. Reason is that we can define Property in terms of IxProperty but not the other way around. So I would have to duplicate all the functions (like forall) in the downstream library, (and keep the interface compatible, every time something changes in Hedgehog) , whilst if we'd implement Property in terms of IxProperty, then forAll is just iforAll that ignores the type parameters of IxMonad

But let me first actually write the code, and then see if it's actually such a big problem.

[japesinator]

Whoa this looks awesome! Apologies for the late response, but I can confirm a version of [re]check that returns a result would wholly solve my problem

[japesinator]

Also, could I get added to the Hedgehog slack? I'm not sure how soon I'll have time to start contributing, but would absolutely love to at some point