diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -7,6 +7,30 @@
 *de facto* standard Haskell versioning scheme.
 
 
+1.0.0.0
+-------
+
+- **Date**    2017-12-23
+- **Git tag** [tasty-dejafu-1.0.0.0][]
+- **Hackage** https://hackage.haskell.org/package/tasty-dejafu-1.0.0.0
+
+### Test.Tasty.DejaFu
+
+- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
+- The `IsTest` instance for `ConcST t (Maybe String)` is gone.
+- All test functions are generalised to take a `ProPredicate`.
+- All test functions now take the action to test as the last parameter.
+
+### Miscellaneous
+
+- The minimum supported version of dejafu is now 1.0.0.0.
+
+[tasty-dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/tasty-dejafu-1.0.0.0
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.7.1.1
 -------
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>
+Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the
diff --git a/Test/Tasty/DejaFu.hs b/Test/Tasty/DejaFu.hs
--- a/Test/Tasty/DejaFu.hs
+++ b/Test/Tasty/DejaFu.hs
@@ -1,40 +1,31 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-#if MIN_TOOL_VERSION_ghc(8,0,0)
--- Impredicative polymorphism checks got stronger in GHC 8, breaking
--- the use of 'unsafeCoerce' below.
-{-# LANGUAGE ImpredicativeTypes #-}
-#endif
-
 -- |
 -- Module      : Test.Tasty.DejaFu
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : stable
--- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, ImpredicativeTypes, LambdaCase, RankNTypes, TypeSynonymInstances
+-- Portability : FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, TypeSynonymInstances
 --
 -- This module allows using Deja Fu predicates with Tasty to test the
 -- behaviour of concurrent systems.
 module Test.Tasty.DejaFu
   ( -- * Unit testing
 
-  -- | This is supported by the 'IsTest' instances for 'ConcST' and
-  -- 'ConcIO'. These instances try all executions, reporting as
-  -- failures the cases which return a 'Just' string.
+  -- | This is supported by an 'IsTest' instance for 'ConcIO'.  This
+  -- instance tries all executions, reporting as failures the cases
+  -- which return a 'Just' string.
   --
-  -- @instance Typeable t => IsTest (ConcST t (Maybe String))@
-  -- @instance               IsTest (ConcIO   (Maybe String))@
+  -- @instance IsTest (ConcIO (Maybe String))@
   -- @instance IsOption Bounds@
   -- @instance IsOption MemType@
 
-  -- * Property testing
+  -- * Unit testing
     testAuto
   , testDejafu
   , testDejafus
@@ -45,18 +36,9 @@
 
   , testDejafuDiscard
 
-  -- ** @IO@
-  , testAutoIO
-  , testDejafuIO
-  , testDejafusIO
-
-  , testAutoWayIO
-  , testDejafuWayIO
-  , testDejafusWayIO
-
-  , testDejafuDiscardIO
-
   -- ** Re-exports
+  , Predicate
+  , ProPredicate(..)
   , Way
   , defaultWay
   , systematically
@@ -85,7 +67,6 @@
   , R.equivalentTo, (R.===)
   ) where
 
-import           Control.Monad.ST       (runST)
 import           Data.Char              (toUpper)
 import qualified Data.Foldable          as F
 import           Data.List              (intercalate, intersperse)
@@ -97,46 +78,25 @@
 import qualified Test.DejaFu.Conc       as Conc
 import qualified Test.DejaFu.Refinement as R
 import qualified Test.DejaFu.SCT        as SCT
+import qualified Test.DejaFu.Types      as D
 import           Test.Tasty             (TestName, TestTree, testGroup)
 import           Test.Tasty.Options     (IsOption(..), OptionDescription(..),
                                          lookupOption)
 import           Test.Tasty.Providers   (IsTest(..), singleTest, testFailed,
                                          testPassed)
 
--- Can't put the necessary forall in the @IsTest ConcST t@
--- instance :(
-import           Unsafe.Coerce          (unsafeCoerce)
-
-runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
-runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
-
-runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
-runSCTio = SCT.runSCTDiscard
-
 --------------------------------------------------------------------------------
 -- Tasty-style unit testing
 
 -- | @since 0.3.0.0
-instance Typeable t => IsTest (Conc.ConcST t (Maybe String)) where
-  testOptions = Tagged concOptions
-
-  run options conc callback = do
-    let memtype = lookupOption options :: MemType
-    let way     = lookupOption options :: Way
-    let runSCTst' :: Conc.ConcST t (Maybe String) -> [(Either Failure (Maybe String), Conc.Trace)]
-        runSCTst' = unsafeCoerce $ runSCTst (const Nothing) way memtype
-    let traces = runSCTst' conc
-    run options (ConcTest traces assertableP) callback
-
--- | @since 0.3.0.0
 instance IsTest (Conc.ConcIO (Maybe String)) where
   testOptions = Tagged concOptions
 
   run options conc callback = do
     let memtype = lookupOption options
     let way     = lookupOption options
-    let traces  = runSCTio (const Nothing) way memtype conc
-    run options (ConcIOTest traces assertableP) callback
+    let traces  = SCT.runSCTDiscard (pdiscard assertableP) way memtype conc
+    run options (ConcTest traces (peval assertableP)) callback
 
 concOptions :: [OptionDescription]
 concOptions =
@@ -177,44 +137,26 @@
 -- | Automatically test a computation. In particular, look for
 -- deadlocks, uncaught exceptions, and multiple return values.
 --
--- This uses the 'Conc' monad for testing, which is an instance of
--- 'MonadConc'. If you need to test something which also uses
--- 'MonadIO', use 'testAutoIO'.
---
--- @since 0.2.0.0
+-- @since 1.0.0.0
 testAuto :: (Eq a, Show a)
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  => Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testAuto = testAutoWay defaultWay defaultMemType
 
 -- | Variant of 'testAuto' which tests a computation under a given
 -- execution way and memory model.
 --
--- @since 0.5.0.0
+-- @since 1.0.0.0
 testAutoWay :: (Eq a, Show a)
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testAutoWay way memtype conc = testDejafusWay way memtype conc autocheckCases
-
--- | Variant of 'testAuto' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> TestTree
-testAutoIO = testAutoWayIO defaultWay defaultMemType
-
--- | Variant of 'testAutoWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testAutoWayIO :: (Eq a, Show a)
-  => Way -> MemType -> Conc.ConcIO a -> TestTree
-testAutoWayIO way memtype concio =
-  testDejafusWayIO way memtype  concio autocheckCases
+testAutoWay way memtype = testDejafusWay way memtype autocheckCases
 
 -- | Predicates for the various autocheck functions.
 autocheckCases :: Eq a => [(TestName, Predicate a)]
@@ -226,116 +168,83 @@
 
 -- | Check that a predicate holds.
 --
--- @since 0.2.0.0
-testDejafu :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> TestName
+-- @since 1.0.0.0
+testDejafu :: Show b
+  => TestName
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafu = testDejafuWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafu' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafuWay :: Show a
+-- @since 1.0.0.0
+testDejafuWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> TestName
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafuWay = testDejafuDiscard (const Nothing)
 
 -- | Variant of 'testDejafuWay' which can selectively discard results.
 --
--- @since 0.7.0.0
-testDejafuDiscard :: Show a
+-- @since 1.0.0.0
+testDejafuDiscard :: Show b
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> String
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testDejafuDiscard discard way memtype conc name test =
-  testst discard way memtype conc [(name, test)]
+testDejafuDiscard discard way memtype name test =
+  testconc discard way memtype [(name, test)]
 
 -- | Variant of 'testDejafu' which takes a collection of predicates to
 -- test. This will share work between the predicates, rather than
 -- running the concurrent computation many times for each predicate.
 --
--- @since 0.2.0.0
-testDejafus :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(TestName, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+-- @since 1.0.0.0
+testDejafus :: Show b
+  => [(TestName, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafus = testDejafusWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafus' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafusWay :: Show a
+-- @since 1.0.0.0
+testDejafusWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(TestName, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+  -> [(TestName, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testDejafusWay = testst (const Nothing)
-
--- | Variant of 'testDejafu' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafuIO :: Show a => Conc.ConcIO a -> TestName -> Predicate a -> TestTree
-testDejafuIO = testDejafuWayIO defaultWay defaultMemType
-
--- | Variant of 'testDejafuWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafuWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> TestName -> Predicate a -> TestTree
-testDejafuWayIO = testDejafuDiscardIO (const Nothing)
-
--- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
---
--- @since 0.7.0.0
-testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> TestTree
-testDejafuDiscardIO discard way memtype concio name test =
-  testio discard way memtype concio [(name, test)]
-
--- | Variant of 'testDejafus' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafusIO :: Show a => Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
-testDejafusIO = testDejafusWayIO defaultWay defaultMemType
-
--- | Variant of 'dejafusWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafusWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
-testDejafusWayIO = testio (const Nothing)
+testDejafusWay = testconc (const Nothing)
 
 
 -------------------------------------------------------------------------------
@@ -376,11 +285,7 @@
 -- Tasty integration
 
 data ConcTest where
-  ConcTest   :: Show a => [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcTest
-  deriving Typeable
-
-data ConcIOTest where
-  ConcIOTest :: Show a => IO [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcIOTest
+  ConcTest :: Show b => IO [(Either Failure a, Conc.Trace)] -> ([(Either Failure a, Conc.Trace)] -> Result b) -> ConcTest
   deriving Typeable
 
 data PropTest where
@@ -390,14 +295,7 @@
 instance IsTest ConcTest where
   testOptions = pure []
 
-  run _ (ConcTest traces p) _ =
-    let err = showErr $ p traces
-     in pure (if null err then testPassed "" else testFailed err)
-
-instance IsTest ConcIOTest where
-  testOptions = pure []
-
-  run _ (ConcIOTest iotraces p) _ = do
+  run _ (ConcTest iotraces p) _ = do
     traces <- iotraces
     let err = showErr $ p traces
     pure (if null err then testPassed "" else testFailed err)
@@ -417,41 +315,23 @@
         ]
       Nothing -> testPassed ""
 
--- | Produce a Tasty 'TestTree' from a Deja Fu test.
-testst :: Show a
-  => (Either Failure a -> Maybe Discard)
-  -> Way
-  -> MemType
-  -> (forall t. Conc.ConcST t a)
-  -> [(TestName, Predicate a)]
-  -> TestTree
-testst discard way memtype conc tests = case map toTest tests of
-  [t] -> t
-  ts  -> testGroup "Deja Fu Tests" ts
-
-  where
-    toTest (name, p) = singleTest name $ ConcTest traces p
-
-    traces = runSCTst discard way memtype conc
-
--- | Produce a Tasty 'Test' from an IO-using Deja Fu test.
-testio :: Show a
+-- | Produce a Tasty 'Test' from a Deja Fu unit test.
+testconc :: Show b
   => (Either Failure a -> Maybe Discard)
   -> Way
   -> MemType
+  -> [(TestName, ProPredicate a b)]
   -> Conc.ConcIO a
-  -> [(TestName, Predicate a)]
   -> TestTree
-testio discard way memtype concio tests = case map toTest tests of
+testconc discard way memtype tests concio = case map toTest tests of
   [t] -> t
   ts  -> testGroup "Deja Fu Tests" ts
 
   where
-    toTest (name, p) = singleTest name $ ConcIOTest traces p
-
-    -- As with HUnit, constructing a test is side-effect free, so
-    -- sharing of traces can't happen here.
-    traces = runSCTio discard way memtype concio
+    toTest (name, p) =
+      let discarder = D.strengthenDiscard discard (pdiscard p)
+          traces    = SCT.runSCTDiscard discarder way memtype concio
+      in singleTest name $ ConcTest traces (peval p)
 
 -- | Produce a Tasty 'TestTree' from a Deja Fu refinement property test.
 testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
@@ -463,7 +343,7 @@
 showErr :: Show a => Result a -> String
 showErr res
   | _pass res = ""
-  | otherwise = "Failed after " ++ show (_casesChecked res) ++ " cases:\n" ++ msg ++ unlines failures ++ rest where
+  | otherwise = "Failed:\n" ++ msg ++ unlines failures ++ rest where
 
   msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
 
diff --git a/tasty-dejafu.cabal b/tasty-dejafu.cabal
--- a/tasty-dejafu.cabal
+++ b/tasty-dejafu.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                tasty-dejafu
-version:             0.7.1.1
+version:             1.0.0.0
 synopsis:            Deja Fu support for the Tasty test framework.
 
 description:
@@ -17,7 +17,7 @@
 license-file:        LICENSE
 author:              Michael Walker
 maintainer:          mike@barrucadu.co.uk
--- copyright:           
+copyright:           (c) 2015--2017 Michael Walker
 category:            Testing
 build-type:          Simple
 extra-source-files:  README.markdown CHANGELOG.markdown
@@ -30,14 +30,14 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      tasty-dejafu-0.7.1.1
+  tag:      tasty-dejafu-1.0.0.0
 
 library
   exposed-modules:     Test.Tasty.DejaFu
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base   >=4.8  && <5
-                     , dejafu >=0.7.1  && <0.10
+                     , dejafu >=1.0  && <1.1
                      , random >=1.0  && <1.2
                      , tagged >=0.8  && <0.9
                      , tasty  >=0.10 && <0.13