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** [hunit-dejafu-1.0.0.0][]
+- **Hackage** https://hackage.haskell.org/package/hunit-dejafu-1.0.0.0
+
+### Test.HUnit.DejaFu
+
+- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
+- The `Testable` and `Assertable` instances for `ConcST t ()` are 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.
+
+[hunit-dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/hunit-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/HUnit/DejaFu.hs b/Test/HUnit/DejaFu.hs
--- a/Test/HUnit/DejaFu.hs
+++ b/Test/HUnit/DejaFu.hs
@@ -1,39 +1,27 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# 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.HUnit.DejaFu
--- Copyright   : (c) 2017 Michael Walker
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : stable
--- Portability : CPP, FlexibleContexts, FlexibleInstances, ImpredicativeTypes, LambdaCase, RankNTypes, ScopedTypeVariables, TypeSynonymInstances
+-- Portability : FlexibleContexts, FlexibleInstances, LambdaCase, TypeSynonymInstances
 --
 -- This module allows using Deja Fu predicates with HUnit to test the
 -- behaviour of concurrent systems.
 module Test.HUnit.DejaFu
   ( -- * Unit testing
 
-  -- | This is supported by the 'Assertable' and 'Testable'
-  -- instances for 'ConcST' and 'ConcIO'. These instances try all
-  -- executions, reporting as failures the cases which throw an
-  -- 'HUnitFailure' exception.
+  -- | This is supported by the 'Assertable' and 'Testable' instances
+  -- for 'ConcIO'.  These instances try all executions, reporting as
+  -- failures the cases which throw an 'HUnitFailure' exception.
   --
-  -- @instance Testable   (ConcST t ())@
-  -- @instance Assertable (ConcST t ())@
-  -- @instance Testable   (ConcIO   ())@
-  -- @instance Assertable (ConcIO   ())@
+  -- @instance Testable   (ConcIO ())@
+  -- @instance Assertable (ConcIO ())@
   --
   -- These instances use 'defaultWay' and 'defaultMemType'.
 
@@ -48,18 +36,9 @@
 
   , testDejafuDiscard
 
-  -- ** @IO@
-  , testAutoIO
-  , testDejafuIO
-  , testDejafusIO
-
-  , testAutoWayIO
-  , testDejafuWayIO
-  , testDejafusWayIO
-
-  , testDejafuDiscardIO
-
   -- ** Re-exports
+  , Predicate
+  , ProPredicate(..)
   , Way
   , defaultWay
   , systematically
@@ -89,56 +68,29 @@
   ) where
 
 import           Control.Monad.Catch    (try)
-import           Control.Monad.ST       (runST)
 import qualified Data.Foldable          as F
 import           Data.List              (intercalate, intersperse)
 import           Test.DejaFu            hiding (Testable(..))
 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.HUnit             (Assertable(..), Test(..), Testable(..),
                                          assertFailure, assertString)
 import           Test.HUnit.Lang        (HUnitFailure(..))
 
--- Can't put the necessary forall in the @Assertable Conc.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
-
 --------------------------------------------------------------------------------
 -- HUnit-style unit testing
 
 -- | @since 0.3.0.0
-instance Testable (Conc.ConcST t ()) where
-  test conc = TestCase (assert conc)
-
--- | @since 0.3.0.0
 instance Testable (Conc.ConcIO ()) where
   test conc = TestCase (assert conc)
 
 -- | @since 0.3.0.0
-instance Assertable (Conc.ConcST t ()) where
-  assert conc = do
-    let traces = runSCTst' conc'
-    assertString . showErr $ assertableP traces
-
-    where
-      conc' :: Conc.ConcST t (Either HUnitFailure ())
-      conc' = try conc
-
-      runSCTst' :: Conc.ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Conc.Trace)]
-      runSCTst' = unsafeCoerce $ runSCTst (const Nothing) defaultWay defaultMemType
-
--- | @since 0.3.0.0
 instance Assertable (Conc.ConcIO ()) where
   assert conc = do
-    traces <- runSCTio (const Nothing) defaultWay defaultMemType (try conc)
-    assertString . showErr $ assertableP traces
+    traces <- SCT.runSCTDiscard (pdiscard assertableP) defaultWay defaultMemType (try conc)
+    assertString . showErr $ peval assertableP traces
 
 assertableP :: Predicate (Either HUnitFailure ())
 assertableP = alwaysTrue $ \case
@@ -152,45 +104,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.
   -> Test
 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.
   -> Test
-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 -> Test
-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 -> Test
-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 => [(String, Predicate a)]
@@ -202,116 +135,83 @@
 
 -- | Check that a predicate holds.
 --
--- @since 0.2.0.0
-testDejafu :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> String
+-- @since 1.0.0.0
+testDejafu :: Show b
+  => 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.
   -> Test
 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
   -> 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.
   -> Test
 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.
   -> Test
-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
-  -> [(String, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+-- @since 1.0.0.0
+testDejafus :: Show b
+  => [(String, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
 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
-  -> [(String, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+  -> [(String, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
-testDejafusWay = testst (const Nothing)
-
--- | Variant of 'testDejafu' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafuIO :: Show a => Conc.ConcIO a -> String -> Predicate a -> Test
-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 -> String -> Predicate a -> Test
-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 -> Test
-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 -> [(String, Predicate a)] -> Test
-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 -> [(String, Predicate a)] -> Test
-testDejafusWayIO = testio (const Nothing)
+testDejafusWay = testconc (const Nothing)
 
 
 -------------------------------------------------------------------------------
@@ -351,44 +251,23 @@
 --------------------------------------------------------------------------------
 -- HUnit integration
 
--- | Produce a HUnit 'Test' from a Deja Fu test.
-testst :: Show a
-  => (Either Failure a -> Maybe Discard)
-  -> Way
-  -> MemType
-  -> (forall t. Conc.ConcST t a)
-  -> [(String, Predicate a)]
-  -> Test
-testst discard way memtype conc tests = case map toTest tests of
-  [t] -> t
-  ts  -> TestList ts
-
-  where
-    toTest (name, p) = TestLabel name . TestCase $
-      assertString . showErr $ p traces
-
-    traces = runSCTst discard way memtype conc
-
--- | Produce a HUnit 'Test' from an IO-using Deja Fu test.
-testio :: Show a
+-- | Produce a HUnit 'Test' from a Deja Fu unit test.
+testconc :: Show b
   => (Either Failure a -> Maybe Discard)
   -> Way
   -> MemType
+  -> [(String, ProPredicate a b)]
   -> Conc.ConcIO a
-  -> [(String, Predicate a)]
   -> Test
-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  -> TestList ts
 
   where
     toTest (name, p) = TestLabel name . TestCase $ do
-      -- Sharing of traces probably not possible (without something
-      -- really unsafe) here, as 'test' doesn't allow side-effects
-      -- (eg, constructing an 'MVar' to share the traces after one
-      -- test computed them).
-      traces <- runSCTio discard way memtype concio
-      assertString . showErr $ p traces
+      let discarder = D.strengthenDiscard discard (pdiscard p)
+      traces <- SCT.runSCTDiscard discarder way memtype concio
+      assertString . showErr $ peval p traces
 
 -- | Produce a HUnit 'Test' 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))
@@ -414,7 +293,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/hunit-dejafu.cabal b/hunit-dejafu.cabal
--- a/hunit-dejafu.cabal
+++ b/hunit-dejafu.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                hunit-dejafu
-version:             0.7.1.1
+version:             1.0.0.0
 synopsis:            Deja Fu support for the HUnit 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,7 +30,7 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      hunit-dejafu-0.7.1.1
+  tag:      hunit-dejafu-1.0.0.0
 
 library
   exposed-modules:     Test.HUnit.DejaFu
@@ -38,7 +38,7 @@
   -- other-extensions:    
   build-depends:       base       >=4.8 && <5
                      , exceptions >=0.7 && <0.9
-                     , dejafu     >=0.7.1 && <0.10
+                     , dejafu     >=1.0 && <1.1
                      , HUnit      >=1.2 && <1.7
   -- hs-source-dirs:      
   default-language:    Haskell2010