diff --git a/examples/Zip.hs b/examples/Zip.hs
--- a/examples/Zip.hs
+++ b/examples/Zip.hs
@@ -10,6 +10,6 @@
 main = quickSpec [
   -- Explore bigger terms.
   withMaxTermSize 8,
-  con "++" ((++) @ Int),
-  con "zip" (zip @ Int @ Int),
-  predicate "eqLen" (eqLen @ Int @ Int) ]
+  con "++" ((++) @Int),
+  con "zip" (zip @Int @Int),
+  predicate "eqLen" (eqLen @Int @Int) ]
diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,5 +1,5 @@
 Name:                quickspec
-Version:             2.1.5
+Version:             2.2
 Cabal-version:       >= 1.10
 Build-type:          Simple
 
@@ -101,9 +101,9 @@
     QuickSpec.Internal.Utils
 
   Build-depends:
-    QuickCheck >= 2.10,
+    QuickCheck >= 2.14.2,
     quickcheck-instances >= 0.3.16,
-    base >= 4 && < 5,
+    base >= 4.7 && < 5,
     constraints,
     containers,
     data-lens-light >= 0.1.1,
@@ -112,5 +112,5 @@
     spoon,
     template-haskell,
     transformers,
-    twee-lib == 2.2,
+    twee-lib,
     uglymemo
diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs
--- a/src/QuickSpec.hs
+++ b/src/QuickSpec.hs
@@ -31,7 +31,8 @@
 --
 -- You can only declare monomorphic types with `monoType`. If you want to test
 -- your own polymorphic types, you must explicitly declare `Arbitrary` and `Ord`
--- instances using the `inst` function.
+-- instances using the `inst` function. You can also use the `generator` function
+-- to use a custom generator instead of the `Arbitrary` instance for a given type.
 --
 -- You can also use QuickSpec to find conditional equations. To do so, you need
 -- to include some /predicates/ in the signature. These are functions returning
@@ -74,7 +75,7 @@
   A, B, C, D, E,
 
   -- * Declaring types
-  monoType, monoTypeObserve, Observe(..), inst,
+  monoType, monoTypeObserve, Observe(..), inst, generator,
   vars, monoTypeWithVars, monoTypeObserveWithVars,
   variableUse, VariableUse(..),
   
@@ -93,9 +94,10 @@
   type (==>), liftC, instanceOf,
 
   -- * Customising QuickSpec
-  withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,
+  withMaxTermSize, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,
   withPruningDepth, withPruningTermSize, withFixedSeed,
   withInferInstanceTypes, withPrintStyle, PrintStyle(..),
+  withConsistencyCheck,
 
   -- * Integrating with QuickCheck
   (=~=),
diff --git a/src/QuickSpec/Internal.hs b/src/QuickSpec/Internal.hs
--- a/src/QuickSpec/Internal.hs
+++ b/src/QuickSpec/Internal.hs
@@ -1,17 +1,19 @@
 -- | The main QuickSpec module, with internal stuff exported.
 -- For QuickSpec hackers only.
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
 module QuickSpec.Internal where
 
-import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..))
+import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..), HasFriendly, FriendlyPredicateTestCase)
 import qualified QuickSpec.Internal.Haskell as Haskell
 import qualified QuickSpec.Internal.Haskell.Resolve as Haskell
 import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck
@@ -27,7 +29,9 @@
 import QuickSpec.Internal.Type hiding (defaultTo)
 import Data.Proxy
 import System.Environment
+#if !MIN_VERSION_base(4,9,0)
 import Data.Semigroup(Semigroup(..))
+#endif
 
 -- | Run QuickSpec. See the documentation at the top of this file.
 quickSpec :: Signature sig => sig -> IO ()
@@ -116,6 +120,10 @@
 -- It will appear in equations just like any other constant,
 -- but will also be allowed to appear as a condition.
 --
+-- Warning: if the predicate is unlikely to be true for a
+-- randomly-generated value, you will get bad-quality test data.
+-- In that case, use `predicateGen` instead.
+--
 -- For example:
 --
 -- @
@@ -125,6 +133,7 @@
 --   predicate "member" (member :: Int -> [Int] -> Bool) ]
 -- @
 predicate :: ( Predicateable a
+             , Haskell.PredicateResult a ~ Bool
              , Typeable a
              , Typeable (PredicateTestCase a))
              => String -> a -> Sig
@@ -139,11 +148,23 @@
 -- It will appear in equations just like any other constant,
 -- but will also be allowed to appear as a condition.
 -- The third argument is a generator for values satisfying the predicate.
+--
+-- For example, this declares a predicate that checks if a list is
+-- sorted:
+--
+-- > predicateGen "sorted" sorted genSortedList
+--
+-- where
+--
+-- > sorted :: [a] -> Bool
+-- > sorted xs = sort xs == xs
+-- > genSortedList :: Gen [a]
+-- > genSortedList = sort <$> arbitrary
 predicateGen :: ( Predicateable a
                 , Typeable a
-                , Typeable b
-                , Typeable (PredicateTestCase a))
-                => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig
+                , Typeable (PredicateTestCase a)
+                , HasFriendly (PredicateTestCase a))
+                => String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig
 predicateGen name x gen =
   Sig $ \ctx@(Context _ names) ->
     if name `elem` names then id else
@@ -152,6 +173,17 @@
 
 -- | Declare a new monomorphic type.
 -- The type must implement `Ord` and `Arbitrary`.
+--
+-- If the type does not implement `Ord`, you can use `monoTypeObserve`
+-- to declare an observational equivalence function. If the type does
+-- not implement `Arbitrary`, you can use `generator` to declare a
+-- custom QuickCheck generator.
+--
+-- You do not necessarily need `Ord` and `Arbitrary` instances for
+-- every type. If there is no `Ord` (or `Observe` instance) for a
+-- type, you will not get equations between terms of that type. If
+-- there is no `Arbitrary` instance (or generator), you will not get
+-- variables of that type.
 monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
 monoType _ =
   mconcat [
@@ -234,7 +266,6 @@
 variableUse x _ = instFun (Use x :: Use a)
 
 -- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and
--- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and
 -- `Arbitrary` instance for each type you want it to test.
 --
 -- For example, if you are testing @`Data.Map.Map` k v@, you will need to add
@@ -244,9 +275,22 @@
 -- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B))
 -- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B))
 -- @
+--
+-- For a monomorphic type @T@, you can use `monoType` instead, but if you
+-- want to use `inst`, you can do it like this:
+--
+-- @
+-- `inst` (`Sub` `Dict` :: () `:-` Ord T)
+-- `inst` (`Sub` `Dict` :: () `:-` Arbitrary T)
+-- @
 inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig
 inst = instFun
 
+-- | Declare a generator to be used to produce random values of a
+-- given type. This will take precedence over any `Arbitrary` instance.
+generator :: Typeable a => Gen a -> Sig
+generator = instFun
+
 -- | Declare an arbitrary value to be used by instance resolution.
 instFun :: Typeable a => a -> Sig
 instFun x = addInstances (Haskell.inst x)
@@ -316,6 +360,10 @@
 withMaxCommutativeSize :: Int -> Sig
 withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n)
 
+-- | Limit how many different function symbols can occur in a term.
+withMaxFunctions :: Int -> Sig
+withMaxFunctions n = Sig (\_ -> setL Haskell.lens_max_functions n)
+
 -- | Set how many times to test each discovered law (default: 1000).
 withMaxTests :: Int -> Sig
 withMaxTests n =
@@ -364,6 +412,11 @@
 -- available type class instances
 withInferInstanceTypes :: Sig
 withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)
+
+-- | (Experimental) Check that the discovered laws do not imply any
+-- false laws
+withConsistencyCheck :: Sig
+withConsistencyCheck = Sig (\_ -> setL (Haskell.lens_check_consistency) True)
 
 -- | A signature containing boolean functions:
 -- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
diff --git a/src/QuickSpec/Internal/Explore.hs b/src/QuickSpec/Internal/Explore.hs
--- a/src/QuickSpec/Internal/Explore.hs
+++ b/src/QuickSpec/Internal/Explore.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleContexts, PatternGuards #-}
+{-# LANGUAGE FlexibleContexts, PatternGuards, CPP #-}
 module QuickSpec.Internal.Explore where
 
 import QuickSpec.Internal.Explore.Polymorphic
@@ -14,7 +14,9 @@
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.State.Strict
 import Text.Printf
+#if! MIN_VERSION_base(4,9,0)
 import Data.Semigroup(Semigroup(..))
+#endif
 import Data.List
 
 newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }
@@ -62,7 +64,7 @@
   (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, PrettyTerm fun,
   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
   (Prop (Term fun) -> m ()) ->
-  (Term fun -> testcase -> result) ->
+  (Term fun -> testcase -> Maybe result) ->
   Int -> Int -> (Type -> VariableUse) -> Universe -> Enumerator (Term fun) -> m ()
 quickSpec present eval maxSize maxCommutativeSize use univ enum = do
   let
diff --git a/src/QuickSpec/Internal/Explore/Conditionals.hs b/src/QuickSpec/Internal/Explore/Conditionals.hs
--- a/src/QuickSpec/Internal/Explore/Conditionals.hs
+++ b/src/QuickSpec/Internal/Explore/Conditionals.hs
@@ -11,8 +11,8 @@
 {-# LANGUAGE DeriveFunctor #-}
 module QuickSpec.Internal.Explore.Conditionals where
 
-import QuickSpec.Internal.Prop
-import QuickSpec.Internal.Term
+import QuickSpec.Internal.Prop as Prop
+import QuickSpec.Internal.Term as Term
 import QuickSpec.Internal.Type
 import QuickSpec.Internal.Pruning
 import QuickSpec.Internal.Pruning.Background(Background(..))
@@ -37,10 +37,17 @@
     return (norm . fmap Normal)
   add prop = do
     redundant <- conditionallyRedundant prop
-    unless redundant $ do
-      lift (add (mapFun Normal prop))
+    if redundant then return False else do
+      res <- lift (add (Prop.mapFun Normal prop))
       considerConditionalising prop
+      return res
 
+  decodeNormalForm hole t = lift $ do
+    t <- decodeNormalForm (fmap (fmap Normal) . hole) t
+    let f (Normal x) = Just x
+        f _ = Nothing
+    return $ t >>= sequence . Term.mapFun f
+
 conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe
 conditionalsUniverse tys funs =
   universe $
@@ -84,7 +91,7 @@
   termStyle (Normal f) = termStyle f
 
 instance (Predicate fun, Background fun) => Background (WithConstructor fun) where
-  background (Normal f) = map (mapFun Normal) (background f)
+  background (Normal f) = map (Prop.mapFun Normal) (background f)
   background _ = []
 
 instance Typed fun => Typed (WithConstructor fun) where
diff --git a/src/QuickSpec/Internal/Explore/Polymorphic.hs b/src/QuickSpec/Internal/Explore/Polymorphic.hs
--- a/src/QuickSpec/Internal/Explore/Polymorphic.hs
+++ b/src/QuickSpec/Internal/Explore/Polymorphic.hs
@@ -17,7 +17,7 @@
 
 import qualified QuickSpec.Internal.Explore.Schemas as Schemas
 import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..), VariableUse(..))
-import QuickSpec.Internal.Term
+import QuickSpec.Internal.Term hiding (mapFun)
 import QuickSpec.Internal.Type
 import QuickSpec.Internal.Testing
 import QuickSpec.Internal.Pruning
@@ -34,6 +34,7 @@
 import qualified Twee.Base as Twee
 import Control.Monad
 import qualified Data.DList as DList
+import Data.Maybe
 
 data Polymorphic testcase result fun norm =
   Polymorphic {
@@ -60,7 +61,7 @@
   (Type -> VariableUse) ->
   Universe ->
   (Term fun -> Bool) ->
-  (Term fun -> testcase -> result) ->
+  (Term fun -> testcase -> Maybe result) ->
   Polymorphic testcase result fun norm
 initialState use univ inst eval =
   Polymorphic {
@@ -125,11 +126,19 @@
   add prop = PolyM $ do
     univ <- access univ
     let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))
-    mapM_ add insts
+    or <$> mapM add insts
 
+  normTheorems = PolyM normTheorems
+
+  decodeNormalForm hole t =
+    PolyM $ do
+      t <- decodeNormalForm (fmap (fmap fun_specialised) . hole) t
+      return $ fmap (fmap (\f -> PolyFun f f)) t
+
 instance MonadTester testcase (Term fun) m =>
   MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where
   test prop = PolyM $ lift (test (mapFun fun_original prop))
+  retest testcase prop = PolyM $ lift (retest testcase (mapFun fun_original prop))
 
 -- Given a property which only contains one type variable,
 -- add as much polymorphism to the property as possible.
@@ -223,17 +232,32 @@
             ho <- arrows fun,
             sub <- typeInstancesList univBase (components fun) ]
   
-    -- Now close the type universe under "anti-substitution":
-    -- if u = typeSubst sub t, and u is in the universe, then
-    -- oneTypeVar t should be in the universe.
-    -- In practice this means replacing arbitrary subterms of
-    -- each type with a type variable.
-    univ = fixpoint (usort . oneTypeVar . concatMap antisubst) univHo
+    -- Finally, close the universe under the following operations:
+    -- * Unifying two types
+    -- * Unifying a function's argument with another type
+    --   (the closure includes the function type, the argument type
+    --   and the result type)
+    -- but only if some type in the universe is an instance of the
+    -- resulting type. The idea is that, if some term can be built
+    -- whose type is a generalisation of the type in the universe,
+    -- that generalised type should also be in the universe.
+    univ = oneTypeVar (fixpoint (usort . map canonicaliseType . mgus . prune) univHo)
       where
-        antisubst ty =
-          ty:
-          [ Twee.build (Twee.replacePosition n (Twee.var (Twee.V 0)) (Twee.singleton ty))
-          | n <- [0..Twee.len ty-1] ]
+        prune tys = filter (not . subsumed) tys
+          where
+            subsumed ty =
+              or [oneTypeVar pat == oneTypeVar ty && isJust (matchType pat ty) && isNothing (matchType ty pat) | pat <- tys]
+        mgus tys =
+          tys ++
+          [ ty
+          | ty1 <- tys, ty2 <- tys, 
+            ty <- unPoly <$> combine (poly ty1) (poly ty2),
+            or [isJust (matchType ty bound) | bound <- tys] ]
+        combine ty1 ty2 =
+          catMaybes [polyMgu ty1 ty2 | ty1 < ty2] ++
+          maybeToList (tryApply ty1 ty2) ++
+          -- Get the function and argument types used by tryApply
+          concat [[poly x, poly y] | (x, y) <- maybeToList (unPoly <$> polyFunctionMgu ty1 ty2)]
 
     components ty =
       case unpackArrow ty of
diff --git a/src/QuickSpec/Internal/Explore/Schemas.hs b/src/QuickSpec/Internal/Explore/Schemas.hs
--- a/src/QuickSpec/Internal/Explore/Schemas.hs
+++ b/src/QuickSpec/Internal/Explore/Schemas.hs
@@ -22,7 +22,7 @@
 import Data.Set(Set)
 import Data.Maybe
 import Control.Monad
-import Twee.Label
+import Data.Label
 
 -- | Constrains how variables of a particular type may occur in a term.
 data VariableUse =
@@ -51,7 +51,7 @@
 initialState ::
   (Type -> VariableUse) ->
   (Term fun -> Bool) ->
-  (Term fun -> testcase -> result) ->
+  (Term fun -> testcase -> Maybe result) ->
   Schemas testcase result fun norm
 initialState use inst eval =
   Schemas {
@@ -141,8 +141,8 @@
       res <- Terms.explore t
       case res of
         Terms.Discovered prop -> do
-          add prop
-          return (Just prop)
+          res <- add prop
+          if res then return (Just prop) else return Nothing
         _ -> return Nothing)
 
 -- sortBy (comparing generality) should give most general instances first.
diff --git a/src/QuickSpec/Internal/Explore/Terms.hs b/src/QuickSpec/Internal/Explore/Terms.hs
--- a/src/QuickSpec/Internal/Explore/Terms.hs
+++ b/src/QuickSpec/Internal/Explore/Terms.hs
@@ -37,7 +37,7 @@
 treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree)
 
 initialState ::
-  (term -> testcase -> result) ->
+  (term -> testcase -> Maybe result) ->
   Terms testcase result term norm
 initialState eval =
   Terms {
@@ -73,9 +73,11 @@
   exp norm $ \prop -> do
     res <- test prop
     case res of
-      Nothing -> do
+      Untestable ->
+        return Singleton
+      TestPassed -> do
         return (Discovered prop)
-      Just tc -> do
+      TestFailed tc -> do
         treeForType ty %= addTestCase tc
         exp norm $
           error "returned counterexample failed to falsify property"
diff --git a/src/QuickSpec/Internal/Haskell.hs b/src/QuickSpec/Internal/Haskell.hs
--- a/src/QuickSpec/Internal/Haskell.hs
+++ b/src/QuickSpec/Internal/Haskell.hs
@@ -1,4 +1,6 @@
 {-# OPTIONS_HADDOCK hide #-}
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -8,7 +10,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE DefaultSignatures #-}
@@ -31,6 +32,7 @@
 import Test.QuickCheck.Gen.Unsafe
 import Data.Char
 import Data.Ord
+import QuickSpec.Internal.Testing
 import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck
 import qualified QuickSpec.Internal.Pruning.Twee as Twee
 import QuickSpec.Internal.Explore hiding (quickSpec)
@@ -48,7 +50,7 @@
 import Control.Spoon
 import qualified Data.Set as Set
 import qualified Test.QuickCheck.Poly as Poly
-import Numeric.Natural
+import Numeric.Natural(Natural)
 import Test.QuickCheck.Instances()
 import Data.Word
 import Data.List.NonEmpty (NonEmpty)
@@ -60,6 +62,9 @@
 import Data.Unique
 import qualified Data.Monoid as DM
 import qualified Data.Semigroup as DS
+import qualified Data.Map.Strict as Map
+import Test.QuickCheck.Gen
+import Test.QuickCheck.Random
 
 baseInstances :: Instances
 baseInstances =
@@ -256,8 +261,10 @@
   observe t = observe t . DM.getFirst
 instance Observe t p a => Observe t (Maybe p) (DM.Last a) where
   observe t = observe t . DM.getLast
+#if !MIN_VERSION_base(4,16,0)
 instance Observe t p a => Observe t (Maybe p) (DS.Option a) where
   observe t = observe t . DS.getOption
+#endif
 instance Observe t p a => Observe t (Maybe p) (Maybe a) where
   observe t (Just a) = Just $ observe t a
   observe _ Nothing  = Nothing
@@ -367,15 +374,14 @@
 arbitraryFunction gen = promote (\x -> coarbitrary x (gen x))
 
 -- | Evaluate a Haskell term in an environment.
-evalHaskell :: Type -> Instances -> TestCase -> Term Constant -> Either (Value Ordy) (Term Constant)
-evalHaskell def insts (TestCase env obs) t =
-  maybe (Right t) Left $ do
-    let eval env t = evalTerm env (evalConstant insts) t
-    Identity val `In` w <- unwrap <$> eval env (defaultTo def t)
-    res <- obs (wrap w (Identity val))
-    -- Don't allow partial results to enter the decision tree
-    guard (withValue res (\(Ordy x) -> isJust (teaspoon (x == x))))
-    return res
+evalHaskell :: Type -> Instances -> TestCase -> Term Constant -> Maybe (Value Ordy)
+evalHaskell def insts (TestCase env obs) t = do
+  let eval env t = evalTerm env (evalConstant insts) t
+  Identity val `In` w <- unwrap <$> eval env (defaultTo def t)
+  res <- obs (wrap w (Identity val))
+  -- Don't allow partial results to enter the decision tree
+  guard (withValue res (\(Ordy x) -> isJust (teaspoon (x == x))))
+  return res
 
 data Constant =
   Constant {
@@ -385,7 +391,8 @@
     con_type :: Type,
     con_constraints :: [Type],
     con_size :: Int,
-    con_classify :: Classification Constant }
+    con_classify :: Classification Constant,
+    con_is_hole :: Bool }
 
 instance Eq Constant where
   x == y =
@@ -418,7 +425,8 @@
     con_type = ty,
     con_constraints = constraints,
     con_size = 1,
-    con_classify = Function }
+    con_classify = Function,
+    con_is_hole = False }
   where
     (constraints, ty) = splitConstrainedType (typ val)
 
@@ -487,33 +495,51 @@
   --
   -- Some speedup should be possible by using unboxed tuples instead...
   type PredicateTestCase a
-  uncrry :: a -> PredicateTestCase a -> Bool
+  type PredicateResult a
+  uncrry :: a -> PredicateTestCase a -> PredicateResult a
+  true :: proxy a -> Constant
 
 instance Predicateable Bool where
   type PredicateTestCase Bool = ()
+  type PredicateResult Bool = Bool
   uncrry = const
+  true _ = con "True" True
 
 instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where
   type PredicateTestCase (a -> b) = (a, PredicateTestCase b)
+  type PredicateResult (a -> b) = PredicateResult b
   uncrry f (a, b) = uncrry (f a) b
-
-data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }
+  true _ = true (Proxy :: Proxy b)
 
-true :: Constant
-true = con "True" True
+-- A more user-friendly type for PredicateTestCase.
+type FriendlyPredicateTestCase a = Friendly (PredicateTestCase a)
+class HasFriendly a where
+  type Friendly a
+  unfriendly :: Friendly a -> a
+instance HasFriendly () where
+  type Friendly () = ()
+  unfriendly () = ()
+instance HasFriendly (a, ()) where
+  type Friendly (a, ()) = a
+  unfriendly a = (a, ())
+instance HasFriendly (a, (b, ())) where
+  type Friendly (a, (b, ())) = (a, b)
+  unfriendly (a, b) = (a, (b, ()))
+instance HasFriendly (a, (b, (c, ()))) where
+  type Friendly (a, (b, (c, ()))) = (a, b, c)
+  unfriendly (a, b, c) = (a, (b, (c, ())))
+instance HasFriendly (a, (b, (c, (d, ())))) where
+  type Friendly (a, (b, (c, (d, ())))) = (a, b, c, d)
+  unfriendly (a, b, c, d) = (a, (b, (c, (d, ()))))
 
-trueTerm :: Term Constant
-trueTerm = Fun true
+data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }
 
--- | Declare a predicate with a given name and value.
--- The predicate should have type @... -> Bool@.
--- Uses an explicit generator.
-predicateGen :: forall a b. ( Predicateable a
-             , Typeable a
-             , Typeable b
-             , Typeable (PredicateTestCase a))
-             => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
-predicateGen name pred gen =
+unfriendlyPredicateGen :: forall a b. ( Predicateable a
+                       , Typeable a
+                       , Typeable b
+                       , Typeable (PredicateTestCase a))
+                       => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
+unfriendlyPredicateGen name pred gen =
   let
     -- The following doesn't compile on GHC 7.10:
     -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))
@@ -541,7 +567,7 @@
     inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))
     inst2 = Names [name ++ "_var"]
 
-    conPred = (con name pred) { con_classify = Predicate conSels ty (Fun true) }
+    conPred = (con name pred) { con_classify = Predicate conSels ty (Fun (true (Proxy :: Proxy a))) }
     conSels = [ (constant' (name ++ "_" ++ show i) (select (i + length (con_constraints conPred)))) { con_classify = Selector i conPred ty, con_size = 0 } | i <- [0..typeArity (typ conPred)-1] ]
 
     select i =
@@ -559,11 +585,23 @@
 
 -- | Declare a predicate with a given name and value.
 -- The predicate should have type @... -> Bool@.
+-- Uses an explicit generator.
+predicateGen :: forall a. ( Predicateable a
+             , Typeable a
+             , Typeable (PredicateTestCase a)
+             , HasFriendly (PredicateTestCase a))
+             => String -> a -> (Gen (FriendlyPredicateTestCase a)) -> (Instances, Constant)
+predicateGen name pred gen =
+  unfriendlyPredicateGen name pred (\() -> unfriendly <$> gen)
+
+-- | Declare a predicate with a given name and value.
+-- The predicate should have type @... -> Bool@.
 predicate :: forall a. ( Predicateable a
+          , PredicateResult a ~ Bool
           , Typeable a
           , Typeable (PredicateTestCase a))
           => String -> a -> (Instances, Constant)
-predicate name pred = predicateGen name pred inst
+predicate name pred = unfriendlyPredicateGen name pred inst
   where
     inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
     inst Dict = arbitrary `suchThat` uncrry pred
@@ -580,6 +618,7 @@
     cfg_twee :: Twee.Config,
     cfg_max_size :: Int,
     cfg_max_commutative_size :: Int,
+    cfg_max_functions :: Int,
     cfg_instances :: Instances,
     -- This represents the constants for a series of runs of QuickSpec.
     -- Each index in cfg_constants represents one run of QuickSpec.
@@ -589,13 +628,15 @@
     cfg_infer_instance_types :: Bool,
     cfg_background :: [Prop (Term Constant)],
     cfg_print_filter :: Prop (Term Constant) -> Bool,
-    cfg_print_style :: PrintStyle
+    cfg_print_style :: PrintStyle,
+    cfg_check_consistency :: Bool
     }
 
 lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x })
 lens_twee = lens cfg_twee (\x y -> y { cfg_twee = x })
 lens_max_size = lens cfg_max_size (\x y -> y { cfg_max_size = x })
 lens_max_commutative_size = lens cfg_max_commutative_size (\x y -> y { cfg_max_commutative_size = x })
+lens_max_functions = lens cfg_max_functions (\x y -> y { cfg_max_functions = x })
 lens_instances = lens cfg_instances (\x y -> y { cfg_instances = x })
 lens_constants = lens cfg_constants (\x y -> y { cfg_constants = x })
 lens_default_to = lens cfg_default_to (\x y -> y { cfg_default_to = x })
@@ -603,6 +644,7 @@
 lens_background = lens cfg_background (\x y -> y { cfg_background = x })
 lens_print_filter = lens cfg_print_filter (\x y -> y { cfg_print_filter = x })
 lens_print_style = lens cfg_print_style (\x y -> y { cfg_print_style = x })
+lens_check_consistency = lens cfg_check_consistency (\x y -> y { cfg_check_consistency = x })
 
 defaultConfig :: Config
 defaultConfig =
@@ -611,13 +653,15 @@
     cfg_twee = Twee.Config { Twee.cfg_max_term_size = minBound, Twee.cfg_max_cp_depth = maxBound },
     cfg_max_size = 7,
     cfg_max_commutative_size = 5,
+    cfg_max_functions = maxBound,
     cfg_instances = mempty,
     cfg_constants = [],
     cfg_default_to = typeRep (Proxy :: Proxy Int),
     cfg_infer_instance_types = False,
     cfg_background = [],
     cfg_print_filter = \_ -> True,
-    cfg_print_style = ForHumans }
+    cfg_print_style = ForHumans,
+    cfg_check_consistency = False }
 
 -- Extra types for the universe that come from in-scope instances.
 instanceTypes :: Instances -> Config -> [Type]
@@ -689,7 +733,9 @@
 quickSpec cfg@Config{..} = do
   let
     constantsOf f =
-      [true | any (/= Function) (map classify (f cfg_constants))] ++
+      usort (concatMap funs $
+        [clas_true | Predicate{..} <- map classify (f cfg_constants)] ++
+        [clas_true (classify clas_pred) | Selector{..} <- map classify (f cfg_constants)]) ++
       f cfg_constants ++ concatMap selectors (f cfg_constants)
     constants = constantsOf concat
 
@@ -699,17 +745,20 @@
     eval = evalHaskell cfg_default_to instances
     was_observed = isNothing . findOrdInstance instances  -- it was observed if there is no Ord instance directly in scope
 
+    prettierProp funs norm = prettyDefinition funs . prettyAC norm . conditionalise
+    prettiestProp funs norm = prettyProp (names instances) . prettierProp funs norm
+
     present funs prop = do
       norm <- normaliser
-      let prop' = prettyDefinition funs (prettyAC norm (conditionalise prop))
-      when (cfg_print_filter prop) $ do
+      let prop' = prettierProp funs norm prop
+      when (not (hasBackgroundPredicates prop') && not (isBackgroundProp prop') && cfg_print_filter prop) $ do
         (n :: Int, props) <- get
-        put (n+1, prop':props)
+        put (n+1, props)
         putLine $
           case cfg_print_style of
             ForHumans ->
               printf "%3d. %s" n $ show $
-                prettyProp (names instances) prop' <+> disambiguatePropType prop
+                prettiestProp funs norm prop <+> disambiguatePropType prop
             ForQuickCheck ->
               renderStyle (style {lineLength = 78}) $ nest 2 $
                 prettyPropQC
@@ -720,6 +769,22 @@
                   prop'
                   <+> disambiguatePropType prop
 
+    hasBackgroundPredicates (_ :=>: t :=: u)
+      | not (null [p | p <- funs t, isBackgroundPredicate p]),
+        not (null [q | q <- funs u, isBackgroundPredicate q]) =
+        True
+    hasBackgroundPredicates _ = False
+    isBackgroundPredicate p =
+      p `elem` concat (take 1 cfg_constants) &&
+      case classify p of
+        Predicate{} -> True
+        _ -> False
+
+    isBackgroundProp p =
+      not (null fs) && and [f `elem` concat (take 1 cfg_constants) | f <- fs]
+      where
+        fs = funs p
+
     -- XXX do this during testing
     constraintsOk = memo $ \con ->
       or [ and [ isJust (findValue instances (defaultTo cfg_default_to constraint)) | constraint <- con_constraints (typeSubst sub con) ]
@@ -729,6 +794,7 @@
     enumerator cons =
       sortTerms measure $
       filterEnumerator (all constraintsOk . funs) $
+      filterEnumerator (\t -> length (usort (funs t)) <= cfg_max_functions) $
       filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $
       enumerateConstants atomic `mappend` enumerateApplications
       where
@@ -751,7 +817,10 @@
         when (cfg_print_style == ForQuickCheck) $ do
           putLine "quickspec_laws :: [(String, Property)]"
           putLine "quickspec_laws ="
-      let pres = if n == 0 then \_ -> return () else present (constantsOf f)
+      let
+        pres prop = do
+          modify $ \(k, props) -> (k, prop:props)
+          if n == 0 then return () else present (constantsOf f) prop
       QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ
         (enumerator (map Fun (constantsOf g)))
       when (n > 0) $ do
@@ -766,10 +835,54 @@
         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))
         rounds = length cfg_constants
 
+    -- Used in checkConsistency. Generate a term to be used when a
+    -- Twee proof contains a hole ("?"), i.e. a don't-care variable.
+    hole ty = do
+      -- It doesn't matter what the value of the variable is, so
+      -- generate a single random value and use that.
+      vgen <- findInstance instances ty :: Maybe (Value Gen)
+      let runGen g = Identity (unGen g (mkQCGen 1234) 5)
+      return $ Fun $ (constant' "hole" (mapValue runGen vgen)) { con_is_hole = True }
+
+    -- Remove holes by replacing them with a fresh variable.
+    removeHoles prop = mapTerm (flatMapFun f) prop
+      where
+        f con
+          | con_is_hole con = Var (V (typ con) n)
+          | otherwise = Fun con
+        n = freeVar prop
+
+    checkConsistency = do
+      thms <- theorems hole
+      let numThms = length thms
+      norm <- normaliser
+
+      forM_ (zip [1 :: Int ..] thms) $ \(i, thm) -> do
+        putStatus (printf "checking laws for consistency: %d/%d" i numThms)
+        res <- test (prop thm)
+        case res of
+          TestFailed testcase -> do
+            forM_ (axiomsUsed thm) $ \(ax, insts) ->
+              forM_ insts $ \inst -> do
+                res <- retest testcase inst
+                when (testResult res == TestFailed ()) $ do
+                  modify (Map.insertWith Set.union (removeHoles ax) (Set.singleton (removeHoles inst)))
+          _ -> return ()
+
+      falseProps <- get
+      forM_ (Map.toList falseProps) $ \(ax, insts) -> do
+        putLine (printf "*** Law %s is false!" (prettyShow (prettiestProp constants norm ax)))
+        putLine "False instances:"
+        forM_ (Set.toList insts) $ \inst -> do
+          putLine (printf "  %s is false" (prettyShow (prettiestProp constants norm inst)))
+        putLine ""
+
   join $
     fmap withStdioTerminal $
     generate $
     QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $
     Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $
-    runConditionals constants $
-    fmap (reverse . snd) $ flip execStateT (1, []) main
+    runConditionals constants $ do
+      result <- fmap (reverse . snd) $ flip execStateT (1, []) main
+      when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty
+      return result
diff --git a/src/QuickSpec/Internal/Haskell/Resolve.hs b/src/QuickSpec/Internal/Haskell/Resolve.hs
--- a/src/QuickSpec/Internal/Haskell/Resolve.hs
+++ b/src/QuickSpec/Internal/Haskell/Resolve.hs
@@ -13,7 +13,7 @@
 -- their types must be such that the instance search will terminate.
 
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, CPP #-}
 module QuickSpec.Internal.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where
 
 import Twee.Base
@@ -23,7 +23,9 @@
 import Data.Maybe
 import Data.Proxy
 import Control.Monad
+#if !MIN_VERSION_base(4,9,0)
 import Data.Semigroup(Semigroup(..))
+#endif
 
 -- A set of instances.
 data Instances =
@@ -59,9 +61,9 @@
       -- (see comment about is_instances).
       case typ x of
         -- A function of type a -> (b -> c) gets uncurried.
-        App (F Arrow) (Cons _ (Cons (App (F Arrow) _) Empty)) ->
+        App (F _ Arrow) (Cons _ (Cons (App (F _ Arrow) _) Empty)) ->
           polyInst (apply uncur x)
-        App (F Arrow) _ ->
+        App (F _ Arrow) _ ->
           makeInstances [x]
         -- A plain old value x (not a function) turns into \() -> x.
         _ ->
@@ -92,10 +94,10 @@
 --
 -- Invariant: the type of the returned value is an instance of the argument type.
 find_ :: Instances -> Type -> [Value Identity]
-find_ _ (App (F unit) Empty)
+find_ _ (App (F _ unit) Empty)
   | unit == tyCon (Proxy :: Proxy ()) =
     return (toValue (Identity ()))
-find_ insts (App (F pair) (Cons ty1 (Cons ty2 Empty)))
+find_ insts (App (F _ pair) (Cons ty1 (Cons ty2 Empty)))
   | pair == tyCon (Proxy :: Proxy (,)) = do
     x <- is_find insts ty1
     sub <- maybeToList (match ty1 (typ x))
@@ -107,7 +109,7 @@
   -- Find a function whose result type unifies with ty.
   -- Rename it to avoid clashes with ty.
   fun <- fmap (polyRename ty) (is_instances insts)
-  App (F Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)
+  App (F _ Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)
   sub <- maybeToList (unify ty res)
   fun <- return (typeSubst sub fun)
   arg <- return (typeSubst sub arg)
diff --git a/src/QuickSpec/Internal/Parse.hs b/src/QuickSpec/Internal/Parse.hs
--- a/src/QuickSpec/Internal/Parse.hs
+++ b/src/QuickSpec/Internal/Parse.hs
@@ -1,6 +1,6 @@
 -- | Parsing strings into properties.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, GADTs, TypeOperators #-}
 {-# LANGUAGE FlexibleContexts #-}
 module QuickSpec.Internal.Parse where
 
@@ -9,7 +9,7 @@
 import QuickSpec.Internal.Prop
 import QuickSpec.Internal.Term hiding (char)
 import QuickSpec.Internal.Type
-import qualified Twee.Label as Label
+import qualified Data.Label as Label
 import Text.ParserCombinators.ReadP
 
 class Parse fun a where
@@ -20,7 +20,7 @@
     x <- satisfy isUpper
     xs <- munch isAlphaNum
     let name = x:xs
-    -- Use Twee.Label as an easy way to generate a variable number
+    -- Use Data.Label as an easy way to generate a variable number
     return (V typeVar (fromIntegral (Label.labelNum (Label.label name))))
 
 instance (fun1 ~ fun, Apply (Term fun)) => Parse fun1 (Term fun) where
diff --git a/src/QuickSpec/Internal/Prop.hs b/src/QuickSpec/Internal/Prop.hs
--- a/src/QuickSpec/Internal/Prop.hs
+++ b/src/QuickSpec/Internal/Prop.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-}
+{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators, DeriveTraversable #-}
 module QuickSpec.Internal.Prop where
 
 import Data.Bool (bool)
@@ -19,7 +19,7 @@
   (:=>:) {
     lhs :: [Equation a],
     rhs :: Equation a }
-  deriving (Show, Generic, Functor)
+  deriving (Show, Generic, Functor, Traversable, Foldable)
 
 instance Symbolic f a => Symbolic f (Prop a) where
   termsDL (lhs :=>: rhs) =
@@ -43,6 +43,11 @@
 mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
 mapFun f = fmap (fmap f)
 
+mapTerm :: (Term fun1 -> Term fun2) -> Prop (Term fun1) -> Prop (Term fun2)
+mapTerm f (lhs :=>: rhs) = map (both f) lhs :=>: both f rhs
+  where
+    both f (t :=: u) = f t :=: f u
+
 instance Typed a => Typed (Prop a) where
   typ _ = typeOf True
   otherTypesDL p = DList.fromList (literals p) >>= typesDL
@@ -54,7 +59,7 @@
   pPrint p =
     hsep (punctuate (text " &") (map pPrint (lhs p))) <+> text "=>" <+> pPrint (rhs p)
 
-data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor)
+data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor, Traversable, Foldable)
 
 instance Symbolic f a => Symbolic f (Equation a) where
   termsDL (t :=: u) = termsDL t `mplus` termsDL u
diff --git a/src/QuickSpec/Internal/Pruning.hs b/src/QuickSpec/Internal/Pruning.hs
--- a/src/QuickSpec/Internal/Pruning.hs
+++ b/src/QuickSpec/Internal/Pruning.hs
@@ -1,25 +1,65 @@
 -- A type of pruners.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs #-}
+{-# LANGUAGE FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs, TypeOperators, DeriveFunctor, DeriveTraversable #-}
 module QuickSpec.Internal.Pruning where
 
 import QuickSpec.Internal.Prop
 import QuickSpec.Internal.Testing
+import QuickSpec.Internal.Type(Type)
+import Twee.Pretty
 import Control.Monad.Trans.Class
 import Control.Monad.IO.Class
 import Control.Monad.Trans.State.Strict
 import Control.Monad.Trans.Reader
+import Data.Maybe
 
+data Theorem norm =
+  Theorem {
+    prop :: Prop norm,
+    axiomsUsed :: [(Prop norm, [Prop norm])] }
+  deriving (Functor, Foldable, Traversable)
+
+instance Pretty norm => Pretty (Theorem norm) where
+  pPrint thm =
+    (text "prop =" <+> pPrint (prop thm)) $$
+    (text "axioms used =" <+> pPrint (axiomsUsed thm))
+
 class Monad m => MonadPruner term norm m | m -> term norm where
   normaliser :: m (term -> norm)
-  add :: Prop term -> m ()
+  add :: Prop term -> m Bool
+  decodeNormalForm :: (Type -> Maybe term) -> norm -> m (Maybe term)
+  normTheorems :: m [Theorem norm]
 
   default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm)
   normaliser = lift normaliser
 
-  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m ()
+  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool
   add = lift . add
 
+  default normTheorems :: (MonadTrans t, MonadPruner term' norm m', m ~ t m') => m [Theorem norm]
+  normTheorems = lift normTheorems
+
+  default decodeNormalForm :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => (Type -> Maybe term) -> norm -> m (Maybe term)
+  decodeNormalForm hole t = lift (decodeNormalForm hole t)
+
+decodeTheorem :: MonadPruner term norm m => (Type -> Maybe term) -> Theorem norm -> m (Maybe (Theorem term))
+decodeTheorem hole thm = elimMaybeThm <$> mapM (decodeNormalForm hole) thm
+  where
+    elimMaybeThm (Theorem prop axs) =
+      case sequence prop of
+        Nothing -> Nothing
+        Just prop -> Just (Theorem prop (mapMaybe elimMaybeAx axs))
+    elimMaybeAx (ax, insts) =
+      case sequence ax of
+        Nothing -> Nothing
+        Just ax -> Just (ax, mapMaybe elimMaybeInst insts)
+    elimMaybeInst = sequence
+
+theorems :: MonadPruner term norm m => (Type -> Maybe term) -> m [Theorem term]
+theorems hole = do
+  thms <- normTheorems
+  catMaybes <$> mapM (decodeTheorem hole) thms
+
 instance MonadPruner term norm m => MonadPruner term norm (StateT s m)
 instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m)
 
@@ -36,7 +76,7 @@
 
 instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where
   normaliser = ReadOnlyPruner normaliser
-  add _ = return ()
+  add _ = return True
 
 newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)
   deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)
@@ -52,4 +92,4 @@
 watchPruner (WatchPruner mx) = do
   (x, props) <- runStateT mx []
   return (x, reverse props)
-    
+
diff --git a/src/QuickSpec/Internal/Pruning/PartialApplication.hs b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
--- a/src/QuickSpec/Internal/Pruning/PartialApplication.hs
+++ b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
@@ -3,16 +3,15 @@
 {-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}
 module QuickSpec.Internal.Pruning.PartialApplication where
 
-import QuickSpec.Internal.Term
+import QuickSpec.Internal.Term as Term
 import QuickSpec.Internal.Type
 import QuickSpec.Internal.Pruning.Background hiding (Pruner)
 import QuickSpec.Internal.Pruning
-import QuickSpec.Internal.Prop
+import QuickSpec.Internal.Prop as Prop
 import QuickSpec.Internal.Terminal
 import QuickSpec.Internal.Testing
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
-import Twee.Base(Arity(..))
 
 data PartiallyApplied f =
     -- A partially-applied function symbol.
@@ -67,7 +66,7 @@
 
 instance (Typed f, Background f) => Background (PartiallyApplied f) where
   background (Partial f _) =
-    map (mapFun (\f -> Partial f arity)) (background f) ++
+    map (Prop.mapFun (\f -> Partial f arity)) (background f) ++
     [ simpleApply (partial n) (vs !! n) === partial (n+1)
     | n <- [0..arity-1] ]
     where
@@ -94,6 +93,13 @@
   add prop =
     Pruner $ do
       add (encode <$> canonicalise prop)
+
+  decodeNormalForm hole t =
+    Pruner $ do
+      t <- decodeNormalForm (fmap (fmap (flip Partial 0)) . hole) t
+      let f (Partial x _) = NotId x
+          f (Apply _) = Id
+      return $ t >>= eliminateId . Term.mapFun f
 
 encode :: Typed fun => Term fun -> Term (PartiallyApplied fun)
 encode (Var x) = Var x
diff --git a/src/QuickSpec/Internal/Pruning/Twee.hs b/src/QuickSpec/Internal/Pruning/Twee.hs
--- a/src/QuickSpec/Internal/Pruning/Twee.hs
+++ b/src/QuickSpec/Internal/Pruning/Twee.hs
@@ -16,6 +16,7 @@
 import Control.Monad.IO.Class
 import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped
 import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))
+import Data.Typeable
 
 newtype Pruner fun m a =
   Pruner (PartialApplication.Pruner fun (Types.Pruner (PartiallyApplied fun) (Background.Pruner (Tagged (PartiallyApplied fun)) (Untyped.Pruner (Tagged (PartiallyApplied fun)) m))) a)
@@ -25,6 +26,6 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift . lift . lift
 
-run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a
+run :: (Sized fun, Typeable fun, Ord fun, Monad m) => Config -> Pruner fun m a -> m a
 run config (Pruner x) =
   Untyped.run config (Background.run (Types.run (PartialApplication.run x)))
diff --git a/src/QuickSpec/Internal/Pruning/Types.hs b/src/QuickSpec/Internal/Pruning/Types.hs
--- a/src/QuickSpec/Internal/Pruning/Types.hs
+++ b/src/QuickSpec/Internal/Pruning/Types.hs
@@ -1,6 +1,6 @@
 -- Encode monomorphic types during pruning.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RecordWildCards, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
 module QuickSpec.Internal.Pruning.Types where
 
 import QuickSpec.Internal.Pruning
@@ -8,12 +8,10 @@
 import QuickSpec.Internal.Testing
 import QuickSpec.Internal.Term
 import QuickSpec.Internal.Type
-import QuickSpec.Internal.Prop
+import QuickSpec.Internal.Prop hiding (mapFun)
 import QuickSpec.Internal.Terminal
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
-import qualified Twee.Base as Twee
-import Twee.Base(Arity(..))
 
 data Tagged fun =
     Func fun
@@ -28,9 +26,6 @@
   size (Func f) = size f
   size (Tag _) = 0
 
-instance Sized fun => Twee.Sized (Tagged fun) where
-  size f = size f `max` 1
-
 instance Pretty fun => Pretty (Tagged fun) where
   pPrint (Func f) = pPrint f
   pPrint (Tag ty) = text "tag[" <#> pPrint ty <#> text "]"
@@ -39,6 +34,13 @@
   termStyle (Func f) = termStyle f
   termStyle (Tag _) = uncurried
 
+instance Typed fun => Typed (Tagged fun) where
+  typ (Func f) = typ f
+  typ (Tag ty) = arrowType [ty] ty
+
+  typeSubst_ sub (Func f) = Func (typeSubst_ sub f)
+  typeSubst_ sub (Tag ty) = Tag (typeSubst_ sub ty)
+
 instance EqualsBonus (Tagged fun) where
 
 type TypedTerm fun = Term fun
@@ -66,11 +68,18 @@
 
   add prop = lift (add (encode <$> canonicalise prop))
 
-instance (Typed fun, Twee.Arity fun, Background fun) => Background (Tagged fun) where
+  decodeNormalForm hole t =
+    Pruner $ do
+      t <- decodeNormalForm (fmap (fmap Func) . hole) t
+      let f (Func x) = NotId x
+          f (Tag _) = Id
+      return $ t >>= eliminateId . mapFun f
+
+instance (Typed fun, Arity fun, Background fun) => Background (Tagged fun) where
   background = typingAxioms
 
 -- Compute the typing axioms for a function or type tag.
-typingAxioms :: (Typed fun, Twee.Arity fun, Background fun) =>
+typingAxioms :: (Typed fun, Arity fun, Background fun) =>
   Tagged fun -> [Prop (UntypedTerm fun)]
 typingAxioms (Tag ty) =
   [tag ty (tag ty x) === tag ty x]
diff --git a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
--- a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
+++ b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
@@ -16,7 +16,7 @@
 import Twee hiding (Config(..))
 import Twee.Rule hiding (normalForms)
 import Twee.Proof hiding (Config, defaultConfig)
-import Twee.Base(Ordered(..), Extended(..), Arity(..), EqualsBonus)
+import Twee.Base(Ordered(..), Labelled)
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State.Strict hiding (State)
 import Control.Monad.Trans.Class
@@ -24,6 +24,9 @@
 import QuickSpec.Internal.Terminal
 import qualified Data.Set as Set
 import Data.Set(Set)
+import qualified Data.Map.Strict as Map
+import qualified Data.IntMap as IntMap
+import Control.Monad
 
 data Config =
   Config {
@@ -33,9 +36,41 @@
 lens_max_term_size = lens cfg_max_term_size (\x y -> y { cfg_max_term_size = x })
 lens_max_cp_depth = lens cfg_max_cp_depth (\x y -> y { cfg_max_cp_depth = x })
 
-instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Twee.Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
+data Extended fun = Minimal | Skolem Twee.Var | Function fun
+  deriving (Eq, Ord, Typeable)
+
+instance (Ord fun, Typeable fun) => Labelled (Extended fun)
+
+instance Sized fun => Sized (Extended fun) where
+  size (Function f) = size f
+  size _ = 1
+
+instance KBO.Sized (Extended fun) where
+  size _ = 1
+
+instance Arity fun => Arity (Extended fun) where
+  arity (Function f) = arity f
+  arity (Skolem _) = 0
+  arity Minimal = 0
+
+instance (Ord fun, Typeable fun) => Twee.Minimal (Extended fun) where
+  minimal = Twee.fun Minimal
+
+instance EqualsBonus (Extended fun)
+
+instance (Ord fun, Typeable fun, Pretty fun) => Pretty (Extended fun) where
+  pPrintPrec l p (Function f) = pPrintPrec l p f
+  pPrintPrec _ _ Minimal = text "?"
+  pPrintPrec _ _ (Skolem (Twee.V x)) = text ("sk" ++ show x)
+
+instance (Ord fun, Typeable fun, PrettyTerm fun) => PrettyTerm (Extended fun) where
+  termStyle (Function f) = termStyle f
+  termStyle _ = curried
+
+instance (Sized fun, Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
   lessEq = KBO.lessEq
   lessIn = KBO.lessIn
+  lessEqSkolem = KBO.lessEqSkolem
 
 newtype Pruner fun m a =
   Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)
@@ -44,28 +79,26 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift
 
-run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a
+run :: (Typeable fun, Ord fun, Sized fun, Monad m) => Config -> Pruner fun m a -> m a
 run Config{..} (Pruner x) =
-  evalStateT (runReaderT x config) initialState
+  evalStateT (runReaderT x config) (initialState config)
   where
     config =
       defaultConfig {
         Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),
         Twee.cfg_max_cp_depth = cfg_max_cp_depth }
 
-instance Sized fun => Sized (Twee.Term fun) where
+instance (Labelled fun, Sized fun) => Sized (Twee.Term fun) where
   size (Twee.Var _) = 1
   size (Twee.App f ts) =
     size (Twee.fun_value f) + sum (map size (Twee.unpack ts))
 
-instance Sized fun => Sized (Twee.Extended fun) where
-  size Twee.Minimal = 1
-  size (Twee.Skolem _) = 1
-  size (Twee.Function f) = size f
+instance KBO.Weighted (Extended fun) where
+  argWeight _ = 1
 
 type Norm fun = Twee.Term (Extended fun)
 
-instance (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>
+instance (Ord fun, Typed fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>
   MonadPruner (Term fun) (Norm fun) (Pruner fun m) where
   normaliser = Pruner $ do
     state <- lift get
@@ -77,25 +110,65 @@
   add ([] :=>: t :=: u) = Pruner $ do
     state <- lift get
     config <- ask
-    lift (put $! addTwee config t u state)
+    let (t' :=: u') = canonicalise (t :=: u)
+    if not (null (Set.intersection (normalFormsTwee state t') (normalFormsTwee state u'))) then
+      return False
+    else do
+      lift (put $! addTwee config t u state)
+      return True
 
   add _ =
-    return ()
+    return True
     --error "twee pruner doesn't support non-unit equalities"
 
-normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
+  decodeNormalForm hole t = return (decode t (error "ambiguously-typed term"))
+    where
+      decode (Twee.Var (Twee.V n)) ty =
+        Just (Var (V ty n))
+      decode (Twee.App (Twee.F _ Minimal) Twee.Empty) ty =
+        hole ty
+      decode (Twee.App (Twee.F _ (Skolem (Twee.V n))) Twee.Empty) ty =
+        Just (Var (V ty n))
+      decode (Twee.App (Twee.F _ (Function f)) ts) _ =
+        (Fun f :@:) <$> zipWithM decode (Twee.unpack ts) args
+        where
+          args = typeArgs (typ f)
+      decode _ _ = error "ill-typed term"
+
+  normTheorems = Pruner $ do
+    state <- lift get
+    let actives = IntMap.elems (Twee.st_active_set state)
+    let
+      toTheorem active =
+        Theorem
+          (toProp (equation proof))
+          (map toAxiom . Map.toList . groundAxiomsAndSubsts $ deriv)
+        where
+          proof = Twee.active_proof active
+          deriv = derivation proof
+          toProp (t Twee.:=: u) = [] :=>: t :=: u
+          toAxiom (ax, subs) = (toProp eqn, map toProp [Twee.subst sub eqn | sub <- Set.toList subs])
+            where
+              eqn = axiom_eqn ax
+
+    return (map toTheorem actives)
+
+normaliseTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   State (Extended fun) -> Term fun -> Norm fun
 normaliseTwee state t =
-  result (normaliseTerm state (simplifyTerm state (skolemise t)))
+  result u (normaliseTerm state u)
+  where
+    u = simplifyTerm state (skolemise t)
 
-normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
+normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   State (Extended fun) -> Term fun -> Set (Norm fun)
 normalFormsTwee state t =
-  Set.map result (normalForms state (skolemise t))
+  Set.fromList . Map.elems $ Map.mapWithKey result (normalForms state (skolemise t))
 
-addTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
+addTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)
 addTwee config t u state =
+  interreduce config $
   completePure config $
     addAxiom config state axiom
   where
diff --git a/src/QuickSpec/Internal/Term.hs b/src/QuickSpec/Internal/Term.hs
--- a/src/QuickSpec/Internal/Term.hs
+++ b/src/QuickSpec/Internal/Term.hs
@@ -1,7 +1,7 @@
 -- | This module is internal to QuickSpec.
 --
 -- Typed terms and operations on them.
-{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts #-}
+{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts, DeriveTraversable #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 module QuickSpec.Internal.Term(module QuickSpec.Internal.Term, module Twee.Base, module Twee.Pretty) where
 
@@ -18,10 +18,11 @@
 import Data.Map(Map)
 import Data.List
 import Data.Ord
+import Data.Maybe
 
 -- | A typed term.
 data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)
-  deriving (Eq, Ord, Show, Functor)
+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
 
 -- | A variable, which has a type and a number.
 data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }
@@ -148,6 +149,42 @@
 mapVar f (Var x) = Var (f x)
 mapVar _ (Fun x) = Fun x
 mapVar f (t :$: u) = mapVar f t :$: mapVar f u
+
+-- | Map a function over function symbols.
+mapFun :: (f -> g) -> Term f -> Term g
+mapFun _ (Var x) = Var x
+mapFun f (Fun x) = Fun (f x)
+mapFun f (t :$: u) = mapFun f t :$: mapFun f u
+
+-- | Map a function over function symbols.
+flatMapFun :: (f -> Term g) -> Term f -> Term g
+flatMapFun _ (Var x) = Var x
+flatMapFun f (Fun x) = f x
+flatMapFun f (t :$: u) =
+  flatMapFun f t :$: flatMapFun f u
+
+-- | A type representing functions which may be the identity.
+data OrId f = Id | NotId f
+
+-- | Eliminate the identity function from a term.
+eliminateId :: Term (OrId f) -> Maybe (Term f)
+eliminateId t = do
+  t <- elim t
+  case t of
+    Id -> Nothing
+    NotId t -> Just t
+  where
+    elim :: Term (OrId f) -> Maybe (OrId (Term f))
+    elim (Var x) = Just (NotId (Var x))
+    elim (Fun (NotId f)) = Just (NotId (Fun f))
+    elim (Fun Id) = Just Id
+    elim (t :$: u) = do
+      t <- elim t
+      u <- elim u
+      case (t, u) of
+        (Id, _) -> Just u
+        (NotId _, Id) -> Nothing
+        (NotId t, NotId u) -> Just (NotId (t :$: u))
 
 -- | Find all subterms of a term. Includes the term itself.
 subterms :: Term f -> [Term f]
diff --git a/src/QuickSpec/Internal/Terminal.hs b/src/QuickSpec/Internal/Terminal.hs
--- a/src/QuickSpec/Internal/Terminal.hs
+++ b/src/QuickSpec/Internal/Terminal.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs, TypeOperators #-}
 module QuickSpec.Internal.Terminal where
 
 import Control.Monad.Trans.Class
diff --git a/src/QuickSpec/Internal/Testing.hs b/src/QuickSpec/Internal/Testing.hs
--- a/src/QuickSpec/Internal/Testing.hs
+++ b/src/QuickSpec/Internal/Testing.hs
@@ -1,6 +1,6 @@
 -- A type of test case generators.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances, TypeOperators, DeriveFunctor #-}
 module QuickSpec.Internal.Testing where
 
 import QuickSpec.Internal.Prop
@@ -8,11 +8,33 @@
 import Control.Monad.Trans.State.Strict
 import Control.Monad.Trans.Reader
 
+data TestResult testcase =
+    TestPassed
+  | TestFailed testcase
+  | Untestable
+  deriving (Functor, Eq)
+
+testResult :: TestResult testcase -> TestResult ()
+testResult = fmap (const ())
+
+testAnd :: TestResult testcase -> TestResult testcase -> TestResult testcase
+TestPassed `testAnd` x = x
+x `testAnd` _ = x
+
+testImplies :: TestResult testcase -> TestResult testcase -> TestResult testcase
+TestPassed `testImplies` x = x
+TestFailed _ `testImplies` _ = TestPassed
+Untestable `testImplies` _ = Untestable
+
 class Monad m => MonadTester testcase term m | m -> testcase term where
-  test :: Prop term -> m (Maybe testcase)
+  test :: Prop term -> m (TestResult testcase)
+  retest :: testcase -> Prop term -> m (TestResult testcase)
 
-  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (Maybe testcase)
+  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (TestResult testcase)
   test = lift . test
+
+  default retest :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => testcase -> Prop term -> m (TestResult testcase)
+  retest tc = lift . retest tc
 
 instance MonadTester testcase term m => MonadTester testcase term (StateT s m)
 instance MonadTester testcase term m => MonadTester testcase term (ReaderT r m)
diff --git a/src/QuickSpec/Internal/Testing/DecisionTree.hs b/src/QuickSpec/Internal/Testing/DecisionTree.hs
--- a/src/QuickSpec/Internal/Testing/DecisionTree.hs
+++ b/src/QuickSpec/Internal/Testing/DecisionTree.hs
@@ -9,7 +9,7 @@
 data DecisionTree testcase result term =
   DecisionTree {
     -- A function for evaluating terms on test cases.
-    dt_evaluate :: term -> testcase -> result,
+    dt_evaluate :: term -> testcase -> Maybe result,
     -- The set of test cases gathered so far.
     dt_test_cases :: [testcase],
     -- The tree itself.
@@ -24,7 +24,7 @@
   | EqualTo term
 
 -- Make a new decision tree.
-empty :: (term -> testcase -> result) -> DecisionTree testcase result term
+empty :: (term -> testcase -> Maybe result) -> DecisionTree testcase result term
 empty eval =
   DecisionTree {
     dt_evaluate = eval,
@@ -50,17 +50,25 @@
     k tree = dt{dt_tree = Just tree}
     aux _ [] (Singleton y) = EqualTo y
     aux k (t:ts) (Singleton y) =
-      aux k (t:ts) $
-        TestCase (Map.singleton (dt_evaluate y t) (Singleton y)) 
+      case dt_evaluate y t of
+        Nothing ->
+          -- y is untestable, so we can evict it from the tree
+          Distinct (k (Singleton x))
+        Just val ->
+          aux k (t:ts) $
+            TestCase (Map.singleton val (Singleton y)) 
     aux k (t:ts) (TestCase res) =
-      let
-        val = dt_evaluate x t
-        k' tree = k (TestCase (Map.insert val tree res))
-      in case Map.lookup val res of
+      case dt_evaluate x t of
         Nothing ->
-          Distinct (k' (Singleton x))
-        Just tree ->
-          aux k' ts tree
+          Distinct (k (TestCase res))
+        Just val ->
+          let
+            k' tree = k (TestCase (Map.insert val tree res))
+          in case Map.lookup val res of
+            Nothing ->
+              Distinct (k' (Singleton x))
+            Just tree ->
+              aux k' ts tree
     aux _ [] (TestCase _) =
       error "unexpected node in decision tree"
 
diff --git a/src/QuickSpec/Internal/Testing/QuickCheck.hs b/src/QuickSpec/Internal/Testing/QuickCheck.hs
--- a/src/QuickSpec/Internal/Testing/QuickCheck.hs
+++ b/src/QuickSpec/Internal/Testing/QuickCheck.hs
@@ -9,7 +9,6 @@
 import Test.QuickCheck
 import Test.QuickCheck.Gen
 import Test.QuickCheck.Random
-import Control.Monad
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.Reader
@@ -33,7 +32,7 @@
   Environment {
     env_config :: Config,
     env_tests :: [testcase],
-    env_eval :: testcase -> term -> result }
+    env_eval :: testcase -> term -> Maybe result }
 
 newtype Tester testcase term result m a =
   Tester (ReaderT (Environment testcase term result) m a)
@@ -43,21 +42,25 @@
   lift = Tester . lift
 
 run ::
-  Config -> Gen testcase -> (testcase -> term -> result) ->
+  Config -> Gen testcase -> (testcase -> term -> Maybe result) ->
   Tester testcase term result m a -> Gen (m a)
 run config@Config{..} gen eval (Tester x) = do
   seed <- maybe arbitrary return cfg_fixed_seed
   let
     seeds = unfoldr (Just . split) seed
-    n = cfg_num_tests
+    n = fromIntegral (ceiling (fromIntegral cfg_num_tests * (1 - zeroProportion)))
+    zeroes = cfg_num_tests - n
     k = max 1 cfg_max_test_size
     bias = 3
+    -- Run this proportion of tests of size 0.
+    zeroProportion = 0.01
     -- Bias tests towards smaller sizes.
     -- We do this by distributing the cube of the size uniformly.
     sizes =
-      reverse $ map (k -) $
-      map (truncate . (** (1/fromInteger bias)) . fromIntegral) $
-      uniform (toInteger n) (toInteger k^bias)
+      replicate zeroes 0 ++
+      (reverse $ map (k -) $
+       map (truncate . (** (1/fromInteger bias)) . fromIntegral) $
+       uniform (toInteger n) (toInteger k^bias))
     tests = zipWith (unGen gen) seeds sizes
   return $ runReaderT x
     Environment {
@@ -78,20 +81,21 @@
 instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where
   test prop =
     Tester $ do
-      env <- ask
-      return $! quickCheckTest env prop
+      env@Environment{..} <- ask
+      return $! foldr testAnd TestPassed (map (quickCheckTest env prop) env_tests)
+  retest testcase prop =
+    Tester $ do
+      env@Environment{..} <- ask
+      return $! quickCheckTest env prop testcase
 
 quickCheckTest :: Eq result =>
-  Environment testcase term result ->
-  Prop term -> Maybe testcase
-quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) =
-  msum (map test env_tests)
+  Environment testcase term result -> Prop term -> testcase -> TestResult testcase
+quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) testcase =
+  foldr testAnd (testEq rhs) (map testEq lhs)
   where
-    test testcase = do
-        guard $
-          all (testEq testcase) lhs &&
-          not (testEq testcase rhs)
-        return testcase
-
-    testEq testcase (t :=: u) =
-      env_eval testcase t == env_eval testcase u
+    testEq (t :=: u) =
+      case (env_eval testcase t, env_eval testcase u) of
+        (Just t, Just u)
+          | t == u -> TestPassed
+          | otherwise -> TestFailed testcase
+        _ -> Untestable
diff --git a/src/QuickSpec/Internal/Type.hs b/src/QuickSpec/Internal/Type.hs
--- a/src/QuickSpec/Internal/Type.hs
+++ b/src/QuickSpec/Internal/Type.hs
@@ -1,12 +1,13 @@
 -- | This module is internal to QuickSpec.
 --
 -- Polymorphic types and dynamic values.
-{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs #-}
+{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs, TypeOperators #-}
 -- To avoid a warning about TyVarNumber's constructor being unused:
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
 module QuickSpec.Internal.Type(
   -- * Types
   Typeable,
+  Arity(..),
   Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,
   typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,
   arrowType, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,
@@ -18,7 +19,7 @@
   oneTypeVar, defaultTo, skolemiseTypeVars,
   -- * Polymorphic types
   canonicaliseType,
-  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu,
+  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu, polyFunctionMgu,
   -- * Dynamic values
   Value, toValue, fromValue, valueType,
   unwrap, Unwrapped(..), Wrapper(..),
@@ -35,7 +36,7 @@
 import Data.Constraint
 import Twee.Base
 import Data.Proxy
-import Data.List
+import Data.List hiding (singleton)
 import Data.Char
 import Data.Functor.Identity
 
@@ -51,8 +52,10 @@
     -- | A string. Can be used to represent miscellaneous types that do not
     -- really exist in Haskell.
   | String String
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord, Show, Typeable)
 
+instance Labelled TyCon
+
 instance Pretty TyCon where
   pPrint Arrow = text "->"
   pPrint (String x) = text x
@@ -159,20 +162,20 @@
 --
 -- For multiple-argument functions, unpacks one argument.
 unpackArrow :: Type -> Maybe (Type, Type)
-unpackArrow (App (F Arrow) (Cons t (Cons u Empty))) =
+unpackArrow (App (F _ Arrow) (Cons t (Cons u Empty))) =
   Just (t, u)
 unpackArrow _ =
   Nothing
 
 -- | The arguments of a function type.
 typeArgs :: Type -> [Type]
-typeArgs (App (F Arrow) (Cons arg (Cons res Empty))) =
+typeArgs (App (F _ Arrow) (Cons arg (Cons res Empty))) =
   arg:typeArgs res
 typeArgs _ = []
 
 -- | The result of a function type.
 typeRes :: Type -> Type
-typeRes (App (F Arrow) (Cons _ (Cons res Empty))) =
+typeRes (App (F _ Arrow) (Cons _ (Cons res Empty))) =
   typeRes res
 typeRes ty = ty
 
@@ -180,7 +183,7 @@
 -- @n@ arguments. Crashes if the type does not have enough arguments.
 typeDrop :: Int -> Type -> Type
 typeDrop 0 ty = ty
-typeDrop n (App (F Arrow) (Cons _ (Cons ty Empty))) =
+typeDrop n (App (F _ Arrow) (Cons _ (Cons ty Empty))) =
   typeDrop (n-1) ty
 typeDrop _ _ =
   error "typeDrop on non-function type"
@@ -235,7 +238,7 @@
 
 -- | Check if a type is of the form @`Dict` c@, and if so, return @c@.
 getDictionary :: Type -> Maybe Type
-getDictionary (App (F (TyCon dict)) (Cons ty Empty))
+getDictionary (App (F _ (TyCon dict)) (Cons ty Empty))
   | dict == dictTyCon = Just ty
 getDictionary _ = Nothing
 
@@ -259,9 +262,9 @@
   coarbitrary = coarbitrary . singleton
 instance CoArbitrary (TermList TyCon) where
   coarbitrary Empty = variant 0
-  coarbitrary (ConsSym (Var (V x)) ts) =
+  coarbitrary ConsSym{hd = Var (V x), rest = ts} =
     variant 1 . coarbitrary x . coarbitrary ts
-  coarbitrary (ConsSym (App f _) ts) =
+  coarbitrary ConsSym{hd = App f _, rest = ts} =
     variant 2 . coarbitrary (fun_id f) . coarbitrary ts
 
 -- | Pretty-print a type. Differs from the `Pretty` instance by printing type
@@ -355,7 +358,7 @@
   typeSubst_ = subst
 
 instance Apply Type where
-  tryApply (App (F Arrow) (Cons arg (Cons res Empty))) t
+  tryApply (App (F _ Arrow) (Cons arg (Cons res Empty))) t
     | t == arg = Just res
   tryApply _ _ = Nothing
 
@@ -426,6 +429,12 @@
   sub <- unify ty1' ty2'
   return (poly (typeSubst sub ty1'))
 
+polyFunctionMgu :: Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))
+polyFunctionMgu f x = do
+  let (f', (x', resType)) = unPoly (polyPair f (polyPair x (poly (build (var (V 0))))))
+  s <- unify (typ f') (arrowType [typ x'] resType)
+  return (poly (typeSubst s (f', x')))
+
 instance Typed a => Typed (Poly a) where
   typ = typ . unPoly
   otherTypesDL = otherTypesDL . unPoly
@@ -433,10 +442,8 @@
 
 instance Apply a => Apply (Poly a) where
   tryApply f x = do
-    let (f', (x', resType)) = unPoly (polyPair f (polyPair x (poly (build (var (V 0))))))
-    s <- unify (typ f') (arrowType [typ x'] resType)
-    let (f'', x'') = typeSubst s (f', x')
-    fmap poly (tryApply f'' x'')
+    (f', x') <- unPoly <$> polyFunctionMgu f x
+    fmap poly (tryApply f' x')
 
 -- | Convert an ordinary value to a dynamic value.
 toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)
@@ -560,3 +567,7 @@
   case unwrap val of
     x `In` w ->
       fmap (wrap w . Identity) x
+
+class Arity f where
+  -- | Measure the arity.
+  arity :: f -> Int