diff --git a/src/Test/QuickCheck.hs b/src/Test/QuickCheck.hs
index 12fb6822..78cbaa1e 100644
--- a/src/Test/QuickCheck.hs
+++ b/src/Test/QuickCheck.hs
@@ -78,6 +78,7 @@ module Test.QuickCheck
   , quickCheckWith
   , quickCheckWithResult
   , quickCheckResult
+  , recheck
   , isSuccess
     -- ** Running tests verbosely
   , verboseCheck
@@ -317,6 +318,12 @@ module Test.QuickCheck
   , (.||.)
   , disjoin
     -- ** What to do on failure
+#ifndef NO_TYPEABLE
+  , Witness(..)
+  , witness
+  , coerceWitness
+  , castWitness
+#endif
   , counterexample
   , printTestCase
   , whenFail
diff --git a/src/Test/QuickCheck/Property.hs b/src/Test/QuickCheck/Property.hs
index f8ab6744..c00f36d5 100644
--- a/src/Test/QuickCheck/Property.hs
+++ b/src/Test/QuickCheck/Property.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE CPP #-}
 #ifndef NO_TYPEABLE
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ExistentialQuantification #-}
 #endif
 #ifndef NO_SAFE_HASKELL
 {-# LANGUAGE Safe #-}
@@ -33,7 +34,7 @@ import Data.Set(Set)
 import Control.DeepSeq
 #endif
 #ifndef NO_TYPEABLE
-import Data.Typeable (Typeable)
+import Data.Typeable (Typeable, cast)
 #endif
 import Data.Maybe
 
@@ -254,6 +255,25 @@ data Callback
 data CallbackKind = Counterexample    -- ^ Affected by the 'verbose' combinator
                   | NotCounterexample -- ^ Not affected by the 'verbose' combinator
 
+#ifndef NO_TYPEABLE
+data Witness = forall a. (Typeable a, Show a) => Wit a
+
+instance Show Witness where
+  show (Wit a) = show a
+
+coerceWitness :: Typeable a => Witness -> a
+coerceWitness (Wit a) = case cast a of
+  Nothing -> error $ "Can't coerceWitness " ++ show a
+  Just a -> a
+
+castWitness :: Typeable a => Witness -> Maybe a
+castWitness (Wit a) = cast a
+
+#define WITNESSES(a) , theWitnesses a
+#else
+#define WITNESSES(a)
+#endif
+
 -- | The result of a single test.
 data Result
   = MkResult
@@ -289,6 +309,7 @@ data Result
     -- ^ the callbacks for this test case
   , testCase            :: [String]
     -- ^ the generated test case
+  WITNESSES(:: [Witness])
   }
 
 exception :: String -> AnException -> Result
@@ -329,6 +350,7 @@ succeeded, failed, rejected :: Result
       , requiredCoverage    = []
       , callbacks           = []
       , testCase            = []
+      WITNESSES(= [])
       }
 
 --------------------------------------------------------------------------
@@ -502,6 +524,23 @@ withMaxShrinks n = n `seq` mapTotalResult (\res -> res{ maybeMaxShrinks = Just n
 withMaxSize :: Testable prop => Int -> prop -> Property
 withMaxSize n = n `seq` mapTotalResult (\res -> res{ maybeMaxTestSize = Just n })
 
+#ifndef NO_TYPEABLE
+-- | Return a value in the 'witnesses' field of the 'Result' returned by 'quickCheckResult'. Witnesses
+-- are returned outer-most first.
+--
+-- In ghci, for example:
+--
+-- >>> [Wit x] <- fmap witnesses . quickCheckResult $ \ x -> witness x $ x == (0 :: Int)
+-- *** Failed! Falsified (after 2 tests):
+-- 1
+-- >>> x
+-- 1
+-- >>> :t x
+-- x :: Int
+witness :: (Typeable a, Show a, Testable prop) => a -> prop -> Property
+witness a = a `seq` mapTotalResult (\res -> res{ theWitnesses = Wit a : theWitnesses res })
+#endif
+
 -- | Check that all coverage requirements defined by 'cover' and 'coverTable'
 -- are met, using a statistically sound test, and fail if they are not met.
 --
@@ -963,7 +1002,9 @@ disjoin ps =
                      callbacks result2,
                    testCase =
                      testCase result1 ++
-                     testCase result2 }
+                     testCase result2
+                   WITNESSES(= theWitnesses result1 ++ theWitnesses result2)
+                   }
                Nothing -> result2
          -- The "obvious" semantics of .||. has:
          --   discard .||. true = true
diff --git a/src/Test/QuickCheck/Test.hs b/src/Test/QuickCheck/Test.hs
index 64000a55..7d7c28f9 100644
--- a/src/Test/QuickCheck/Test.hs
+++ b/src/Test/QuickCheck/Test.hs
@@ -144,6 +144,10 @@ data Result
       -- ^ The test case's labels (see 'label')
     , failingClasses  :: Set String
       -- ^ The test case's classes (see 'classify')
+#ifndef NO_TYPEABLE
+    , witnesses :: [Witness]
+      -- ^ The existentially quantified witnesses provided by 'witness'
+#endif
     }
   -- | A property that should have failed did not
   | NoExpectedFailure
@@ -199,6 +203,11 @@ quickCheckWithResult :: Testable prop => Args -> prop -> IO Result
 quickCheckWithResult a p =
   withState a (\s -> test s (property p))
 
+-- | Re-run a property with the seed and size that failed in a run of 'quickCheckResult'.
+recheck :: Testable prop => Result -> prop -> IO ()
+recheck res@Failure{} = quickCheckWith stdArgs{ replay = Just (usedSeed res, usedSize res)} . once
+recheck _ = error "Can only recheck tests that failed with a counterexample."
+
 withState :: Args -> (State -> IO a) -> IO a
 withState a test = (if chatty a then withStdioTerminal else withNullTerminal) $ \tm -> do
      rnd <- case replay a of
@@ -481,6 +490,9 @@ runATest st prop =
                             , failingTestCase = testCase
                             , failingLabels   = P.labels res
                             , failingClasses  = Set.fromList (map fst $ filter snd $ P.classes res)
+#ifndef NO_TYPEABLE
+                            , witnesses = theWitnesses res
+#endif
                             }
  where
   (rnd1,rnd2) = split (randomSeed st)