recheckAt does not always reproduce a test failure

[brprice]

In hedgehog 1.2, a new feature recheckAt was added (#454) to skip directly to a failing test. However this sometimes fails: I have a property that fails, and says "This failure can be reproduced by running recheckAt (Seed _ _) "..." <property>", but running this command reports "gave up after 0 discards, passed 4 tests" (or, sometimes reports the test passed).

I have seen this on a few different tests in a real-life codebase, but certainly not all (i.e. it seems that there is a problem with only some properties). I have never seen anything similar on older releases of hedgehog.

I managed to minimize to the following generator and property (note that recheckAt fails to re-find a failure around 80% of the time):

import Data.Maybe (catMaybes)
import Hedgehog (
  Gen,
  Property,
  discard,
  forAll,
  property,
  (===),
 )
import qualified Hedgehog.Gen as Gen

tasty_replay_broken :: Property
tasty_replay_broken = property $ do
  tgt <- forAll $ genWTType KType
  src <- forAll $ genWTType KType
  case stripArgs tgt src of
    Just instTy -> do
      src === instTy
    _ -> discard

genWTType :: Kind -> Gen Type
genWTType k = do
  Gen.recursive Gen.choice [ehole] $ app : catMaybes [arrow]
  where
    ehole = pure TBase
    app = do TApp <$> genWTType (KFun KType k) <*> genWTType KType
    arrow =
      if k == KType
        then Just $ TFun <$> genWTType KType <*> genWTType KType
        else Nothing

data Type
  = TBase
  | TFun Type Type
  | TApp Type Type
  deriving (Eq, Show)

data Kind = KType | KFun Kind Kind
  deriving (Eq, Show)

stripArgs :: Type -> Type -> Maybe Type
stripArgs tgt ty =
  if tgt == ty
    then Just ty
    else case ty of
      TFun _ t -> stripArgs tgt t
      _ -> Nothing

A representative failure is

ghci> check tasty_replay_broken 
  ✗ <interactive> failed at src/Tests/Refine.hs:22:11
    after 7 tests and 13 discards.
    shrink path: 7:
  
       ┏━━ src/Tests/Refine.hs ━━━
    16 ┃ tasty_replay_broken :: Property
    17 ┃ tasty_replay_broken = property $ do
    18 ┃   tgt <- forAll $ genWTType KType
       ┃   │ TBase
    19 ┃   src <- forAll $ genWTType KType
       ┃   │ TFun TBase TBase
    20 ┃   case stripArgs tgt src of
    21 ┃     Just instTy -> do
    22 ┃       src === instTy
       ┃       ^^^^^^^^^^^^^^
       ┃       │ ━━━ Failed (- lhs) (+ rhs) ━━━
       ┃       │ - TFun TBase TBase
       ┃       │ + TBase
    23 ┃     _ -> discard
  
    This failure can be reproduced by running:
    > recheckAt (Seed 3098031441793650136 15775858570470438977) "7:" <property>
  
False
ghci> recheckAt (Seed 3098031441793650136 15775858570470438977) "7:" tasty_replay_broken 
  ⚐ <interactive> gave up after 0 discards, passed 7 tests.

Note that sometimes (but more rarely) recheckAt will show the test passed.

[brprice]

When minimizing, since the issue only happens randomly, I found it helpful to use the following harness, which repeatedly runs the test and when it finds a failure then reruns with that seed and shrink path; it then reports how often hedgehog failed to replay.

{-# LANGUAGE LambdaCase #-}

module Main (main) where

import Control.Monad (replicateM, unless)
import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)
import Data.Functor (void, (<&>))
import Data.List.Extra (enumerate)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Void (Void, absurd)
import Hedgehog (Property, Seed, withSkip)
import Hedgehog.Internal.Property (
  Property (propertyConfig, propertyTest),
  ShrinkPath,
  Skip (SkipToShrink),
  TestCount,
 )
import Hedgehog.Internal.Report (
  FailureReport (failureShrinkPath),
  Report (reportSeed, reportTests),
  Result (..),
  reportStatus,
 )
import Hedgehog.Internal.Runner (checkReport)
import qualified Hedgehog.Internal.Seed as Seed
import Numeric (showFFloat)
import Numeric.Natural (Natural)
import System.Exit (die)
import Tests.Refine (tasty_replay_broken)
import Prelude

main :: IO ()
main = do
  let n = 1000
  rs <- replicateM (fromIntegral n) runAndRecheck
  let cs = count rs
  void $ M.traverseWithKey (\ri c -> putStrLn $ showPad ri <> " : " <> show c) cs
  let t = (cs M.! RecheckPass) + (cs M.! RecheckDefeat)
  let p = (100 :: Double) * fromIntegral t / fromIntegral n
  if t > n `div` 4
    then putStrLn $ "This tickled non-replay bug " <> showFFloat (Just 2) p "% > 25%"
    else die "This did not tickle non-replay bug much"

-- Bounded & Enum: we explicitly give counts of 0 for those which did not appear
count :: (Bounded a, Enum a, Ord a) => [a] -> Map a Natural
count as = M.unionsWith (+) $ M.fromList [(a, 0) | a <- enumerate] : fmap (`M.singleton` 1) as

-- This runs the test once with a random seed, and
-- - if it fails then rechecks it with the reported skip/shrink, reporting whether it finds an error again
-- - if it passes or gives up, report that
runAndRecheck :: IO RRInfo
runAndRecheck = either id absurd <$> runExceptT go
  where
    go :: ExceptT RRInfo IO Void
    go = do
      seed <- Seed.random
      shrink <-
        ExceptT $
          runProp seed tasty_replay_broken <&> \case
            Passed -> Left RunPass
            Defeat -> Left RunDefeat
            Fail tc sp -> Right $ SkipToShrink tc sp
      -- This is essentially "recheckAt", with the skip/shrink info from above
      ExceptT $
        fmap Left $
          runProp seed (withSkip shrink tasty_replay_broken) <&> \case
            Passed -> RecheckPass
            Defeat -> RecheckDefeat
            Fail _ _ -> RecheckRefind

data RRInfo
  = RunPass
  | RunDefeat
  | RecheckPass
  | RecheckDefeat
  | RecheckRefind -- rechecking finds /an/ error, not asserted /the same/ error
  deriving (Show, Eq, Ord, Enum, Bounded)

showPad :: RRInfo -> String
showPad ri = let s = show ri in s <> replicate (13 - length s) ' '

data RunInfo
  = Passed
  | Defeat
  | Fail TestCount ShrinkPath

runProp :: Seed -> Property -> IO RunInfo
runProp seed prop = do
  report <- checkReport (propertyConfig prop) 0 seed (propertyTest prop) $ const $ pure ()
  let testcount = reportTests report
  let seed' = reportSeed report
  -- check my understanding
  unless (seed == seed') $ die "seed /= seed'"
  pure $ case reportStatus report of
    GaveUp -> Defeat
    OK -> Passed
    Failed x -> Fail testcount $ failureShrinkPath x

which will give output similar to

RunPass       : 0
RunDefeat     : 0
RecheckPass   : 24
RecheckDefeat : 821
RecheckRefind : 155
This tickled non-replay bug 84.50% > 25%

meaning that, we checked the property 1000 times and

• 0 of them passed (i.e. all of them gave up or found a failure)
• 0 of them gave up (i.e. all of them found a failure)

and out of the ones that found a failure (in this case, all of them) we re-ran them with the reported seed and shrink path and found (i.e. recheckAt)

• 24 of them passed (thus exhibiting this bug)
• 821 of them gave up (thus exhibiting this bug)
• 155 of them found the issue again (i.e. worked as expected)

We then report the percentage that tickled this bug (if greater than an arbitrary 25% threshold)

[ChickenProp]

Weird. I implemented this feature, so I'll try to look into this at some point (feel free to @ me if I disappear for a week).

I don't have an immediate guess what's going on. But I am curious what happens if you pass in a seed but not a shrink path. Seems like it will always fail, but will the same seed always give the same counterexample? Will it always give the same shrink path?

(You can test with the env var HEDGEHOG_SEED or with recheckAt (Seed ... ...) SkipNothing.)

It would also be helpful to confirm that earlier versions don't exhibit this bug. If you try this on 1.1.2, it should give you a recheck to run - does that fail reliably?

[ChickenProp]

Oh, actually, here's a guess: discards might throw it off. I think I didn't test with those when implementing. From a quick look at checkReport, I think that when running the test for the first time, each discard will cause an extra split of the generator and an increase in the test size, but since we don't track discards in the Skip those will get lost when we replay.

If I'm right about this:

• When the failure message is "and 0 discards" (or doesn't mention discards, I'm not sure if it will if they're 0), replaying should reproduce the failure.
• If you replay with a fixed seed but no skip, you should always get the same failure; but if there were discards, the replay will either not produce a failure or produce a different failure.
• Less confident, but if you take the recheckAt and add the discard count to the number before the colon (so in your example, make it recheckAt (Seed 3098031441793650136 15775858570470438977) "20:"), it should reproduce the failure.
• If that last one is right, then I think this should be easy enough to fix. SkipToTest and SkipToPath will need to take a DiscardCount as well as a TestCount. The specific ordering of tests versus discards shouldn't matter. (Or we could just add the two counts together, but then it'll say "failed after 9 tests and 4 discards" and you'll replay at test number 13, which might be surprising.)

[TysonMN]

@moodmosaic, you have often said that one difference between the Haskel and F# implantations of Hedgehog is that the F# implementation uses SplitMix. I think that means the F# implementation doesn't have this bug (as is currently suspected).

The F# implementation of efficient recheck doesn't have to skip inputs that passed the test or were discarded. Instead, SplitMix creates a seed used to generate each shrink tree. The initial input to be tested is the root of this tree. Therefore, the seed in the recheck details (both before and after implementing efficient recheck) is the seed that generates the shrink tree of the failing input.

[brprice]

Oh, actually, here's a guess: discards might throw it off. I think I didn't test with those when implementing. From a quick look at checkReport, I think that when running the test for the first time, each discard will cause an extra split of the generator and an increase in the test size, but since we don't track discards in the Skip those will get lost when we replay.

If I'm right about this:

• When the failure message is "and 0 discards" (or doesn't mention discards, I'm not sure if it will if they're 0), replaying should reproduce the failure.

From a quick hacking of my harness above, this looks true

• If you replay with a fixed seed but no skip, you should always get the same failure ...

as does this, although I only checked we get a failure, not necessarily the same one

• ... but if there were discards, the replay will either not produce a failure or produce a different failure.

I'm not sure what you mean by this -- I'm guessing "if there were discards, and you replay with the reported skip, then there is no guarantee what will happen". If so, then I agree, but note that it can "not produce a failure" by giving up (not only passing)

• Less confident, but if you take the recheckAt and add the discard count to the number before the colon (so in your example, make it recheckAt (Seed 3098031441793650136 15775858570470438977) "20:"), it should reproduce the failure.

This seems not true, unfortunately. I have seen rare examples (~ 0.1% of the time) which find a failure with some discards and then passes when replaying with the modified Skip. (Due to the rarity, I have only noticed this via the harness that uses internal hedgehog apis -- this may be a bug in my harness, rather than an actual counterexample). I have seen the following counterexamples:

(Seed 6452199707168887957 15646718791793300813,DiscardCount 96,ShrinkPath [2,0])
(Seed 13370356891669266083 6104360885168595951,DiscardCount 91,ShrinkPath [])
(Seed 1163551958042006297 17919109301615462899,DiscardCount 85,ShrinkPath [2])
(Seed 4718817754769925412 14335419815481689733,DiscardCount 98,ShrinkPath [2])

FTR, my updated harness is

{-# LANGUAGE LambdaCase #-}

module Main (main) where

import Control.Monad (replicateM, unless)
import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)
import Data.Functor (void, (<&>))
import Data.List.Extra (enumerate)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Void (Void, absurd)
import Hedgehog (Property, Seed, withSkip)
import Hedgehog.Internal.Property (
  Property (propertyConfig, propertyTest),
  ShrinkPath,
  Skip (SkipToShrink, SkipNothing),
  TestCount(TestCount), DiscardCount(DiscardCount),
 )
import Hedgehog.Internal.Report (
  FailureReport (failureShrinkPath),
  Report (reportSeed, reportTests, reportDiscards),
  Result (..),
  reportStatus,
 )
import Hedgehog.Internal.Runner (checkReport)
import qualified Hedgehog.Internal.Seed as Seed
import Numeric (showFFloat)
import Numeric.Natural (Natural)
import System.Exit (die)
import Bug (tasty_replay_broken)
import Prelude
import Data.Coerce (coerce)
import Data.Maybe (mapMaybe)

main :: IO ()
main = do
  let n = 1000
  rs <- replicateM (fromIntegral n) runAndRecheck
  let cs = count $ rs <&> \case
        RunPass -> RunPass
        RunDefeat -> RunDefeat
        RunFind (_,_,_,info) -> RunFind info
  putStrLn "Raw data counts:"
  void $ M.traverseWithKey (\ri c -> putStrLn $ show ri <> " : " <> show c) cs
  putStrLn ""
  -- https://github.com/hedgehogqa/haskell-hedgehog/issues/487#issuecomment-1557023408
  putStrLn "Claim 1: if no discards, then replaying reproduces the failure (in each of these claims we only actually check it finds /a/ failure, not necessarily the same one)"
  let found = mapMaybe (\case RunFind (seed, discards, shrink, RRInfo' d a b c) -> Just (seed, discards,shrink,d,a,b,c) ; _ -> Nothing) rs
  print $ all (\(_,_,_,d,a,b,c) -> (d == False) ==> (a == RecheckRefind && b == RecheckRefind && c == RecheckRefind)) found
  putStrLn "Claim 2: if replay with a fixed seed but no skip, you should always get the same failure"
  print $ all (\(_,_,_,_,seedOnly,_,_) -> seedOnly == RecheckRefind) found
  putStrLn "Claim 3: if replay with a skip path modified by discard count, you should always get the same failure"
  let notReplayModified = filter (\(_,_,_,_,_,_,modifiedSkip) -> modifiedSkip /= RecheckRefind) found
  if null notReplayModified
    then print True
    else do print False
            putStrLn "Counterexamples:"
            mapM_ print notReplayModified


(==>) :: Bool -> Bool -> Bool
True ==> b = b
False ==> _ = True

count :: Ord a => [a] -> Map a Natural
count as = M.unionsWith (+) $ fmap (`M.singleton` 1) as

-- This runs the test once with a random seed, and
-- - if it fails then rechecks it with the reported skip/shrink, reporting whether it finds an error again
-- - if it passes or gives up, report that
runAndRecheck :: IO (RRInfo  (Seed, DiscardCount, ShrinkPath, RRInfo'))
runAndRecheck = do
  seed <- Seed.random
  runProp seed tasty_replay_broken >>= \case
    Passed -> pure RunPass
    Defeat -> pure RunDefeat
    Fail discards testCount shrinkPath -> do
      -- essentially @recheckAt (Seed ...) SkipNothing@
      recheckSeed <- recheckInfo <$> runProp seed (withSkip SkipNothing tasty_replay_broken)
      -- essentially @recheckAt (Seed ...) shrink@
      recheckShrink <- recheckInfo <$> runProp seed (withSkip (SkipToShrink testCount shrinkPath) tasty_replay_broken)
      -- essentially @recheckAt (Seed ...) (shrink + discards) @
      recheckAddShrink <- recheckInfo <$> runProp seed (withSkip (SkipToShrink (testCount + coerce discards) shrinkPath) tasty_replay_broken)
      pure $ RunFind (seed, discards, shrinkPath, RRInfo' {anyDiscards = discards > 0, recheckSeed, recheckShrink, recheckAddShrink})


data RRInfo a
  = RunPass
  | RunDefeat
  | RunFind a
  deriving (Show, Eq, Ord)

data RRInfo' = RRInfo' {anyDiscards :: Bool, recheckSeed, recheckShrink, recheckAddShrink :: RecheckInfo}
  deriving (Show, Eq, Ord)

data RecheckInfo
  = RecheckPass
  | RecheckDefeat
  | RecheckRefind -- rechecking finds /an/ error, not asserted /the same/ error
  deriving (Show, Eq, Ord, Enum, Bounded)

recheckInfo :: RunInfo -> RecheckInfo
recheckInfo = \case
  Passed -> RecheckPass
  Defeat -> RecheckDefeat
  Fail{} -> RecheckRefind

data RunInfo
  = Passed
  | Defeat
  | Fail DiscardCount TestCount ShrinkPath
  deriving (Show, Eq, Ord)

runProp :: Seed -> Property -> IO RunInfo
runProp seed prop = do
  report <- checkReport (propertyConfig prop) 0 seed (propertyTest prop) $ const $ pure ()
  let testcount = reportTests report
  let seed' = reportSeed report
  -- check my understanding
  unless (seed == seed') $ die "seed /= seed'"
  pure $ case reportStatus report of
    GaveUp -> Defeat
    OK -> Passed
    Failed x -> Fail (reportDiscards report) testcount $ failureShrinkPath x

[ChickenProp]

The F# implementation of efficient recheck doesn't have to skip inputs that passed the test or were discarded. Instead, SplitMix creates a seed used to generate each shrink tree. The initial input to be tested is the root of this tree. Therefore, the seed in the recheck details (both before and after implementing efficient recheck) is the seed that generates the shrink tree of the failing input.

I don't think this is related to SplitMix specifically. haskell-hedgehog does use a splitting PRNG (which I think might actually be SplitMix but I don't think it matters). But for rechecking, haskell-hedgehog takes in the seed that it started testing with, then does a bunch of splits to get to the seed that generates the shrink tree. It sounds like in F#, rechecking simply takes in the seed that generates the shrink tree.

That's also a fine way to do things, but the haskell-hedgehog approach means you can use the same seed for multiple tests. E.g. if you do HEDGEHOG_SEED="... ..." run-tests and get one or more failures, the failures will tell you to use a recheckAt that has the same seed you passed in. If I understand what you're saying about the F# implementation, if we did it that way then the failures would all tell you to use different seeds.

I'm not sure what you mean by this -- I'm guessing "if there were discards, and you replay with the reported skip, then there is no guarantee what will happen". If so, then I agree, but note that it can "not produce a failure" by giving up (not only passing)

Yeah, you read that right. Giving up is indeed an expected possible outcome there.

This seems not true, unfortunately. I have seen rare examples (~ 0.1% of the time) which find a failure with some discards and then passes when replaying with the modified Skip.

Huh. So it sounds like my hypothesis explains most but not all of the errors? That's weird again... I should run your harness myself and see if I can figure it out, but I'm not sure when I'll get to it. Again, feel free to @ me if it takes a while.

[TysonMN]

@moodmosaic, you have often said that one difference between the Haskel and F# implantations of Hedgehog is that the F# implementation uses SplitMix.

Oh, I misquoted you. QuickCheck doesn't use SplitMix but Hedgehog (both Haskel and F#) do.

I don't think this is related to SplitMix specifically. haskell-hedgehog does use a splitting PRNG (which I think might actually be SplitMix but I don't think it matters).

Yes, thank you for correcting me.

If I understand what you're saying about the F# implementation, if we did it that way then the failures would all tell you to use different seeds.

Yes, everything you said up to here is correct.

What is the average of getting multiple failure messages with the same seed?

[ChickenProp]

What is the average of getting multiple failure messages with the same seed?

(Assuming you mean advantage) It lets you reproduce multiple test failures at once if you're passing in a seed on the command line (which I usually do). Maybe not super helpful, especially if combined with shrink paths. But it also gives me compatibility with hspec, which is the framework I use (via hspec-hedgehog). If I get a failure with --seed, I don't need to change the --seed to reproduce it. And when hspec's failure report tells me to use a --seed, that's the --seed I do in fact need to use. I don't think either of those would be true if I'd gone for F#'s approach.

(Actually, I'm not sure I could reproduce failures at all from the command line, if I'd gone for that. I think hspec-hedgehog ignores the HEDGEHOG_SEED environment variable.)

[moodmosaic]

@ChickenProp

I don't think this is related to SplitMix specifically

True. I think it's more likely in (or around) recheckAt and #454.

@TysonMN

[..] QuickCheck doesn't use SplitMix but Hedgehog (both Haskel and F#) do.

Yes, we used to have our repo for SplitMix, then Jakob created SplitMix.hs and later we ported that in F#. Any bugfixes in SplitMix.hs (should) have been applied also in F#.

[ChickenProp]

Okay! I think the continued failures are because when you try to skip to a test higher than the test limit, we hit the enoughTestsRun branch in checkReport and succeed. I'm not sure this is the ideal behavior, but I'm not sure what else would be ideal either. In any case, adding the DiscardCount to SkipToTest and SkipToShrink should still be a viable fix. I'll work on that.

[ChickenProp]

@bprice, can you confirm that #489 fixes things for you? It passes your harness when I add the discard count to the SkipToShrinks.

[bprice]

@bprice, can you confirm that #489 fixes things for you? It passes your harness when I add the discard count to the SkipToShrinks.

@brprice

[ChickenProp]

Oops, sorry!

[brprice]

can you confirm that #489 fixes things for you? It passes your harness when I add the discard count to the SkipToShrinks.

Yes, it does. Thanks!