diff --git a/examples/ListMonad.hs b/examples/ListMonad.hs
--- a/examples/ListMonad.hs
+++ b/examples/ListMonad.hs
@@ -3,6 +3,7 @@
 import QuickSpec
 
 main = quickSpec [
+  withMaxTestSize 20,
   con "return" (return :: A -> [A]),
   con ">>=" ((>>=) :: [A] -> (A -> [B]) -> [B]),
   con "++" ((++) :: [A] -> [A] -> [A]),
diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,5 +1,5 @@
 Name:                quickspec
-Version:             2.1
+Version:             2.1.1
 Cabal-version:       >= 1.6
 Build-type:          Simple
 
@@ -100,7 +100,7 @@
 
   Build-depends:
     QuickCheck >= 2.10,
-    quickcheck-instances >= 0.3.15,
+    quickcheck-instances >= 0.3.16,
     base >= 4 && < 5,
     constraints,
     containers,
diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs
--- a/src/QuickSpec.hs
+++ b/src/QuickSpec.hs
@@ -69,7 +69,7 @@
   quickSpec, Sig, Signature(..),
 
   -- * Declaring functions and predicates
-  con, predicate,
+  con, predicate, predicateGen,
   -- ** Type variables for polymorphic functions
   A, B, C, D, E,
 
@@ -95,10 +95,11 @@
   -- * Re-exported functionality
   Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary,
 
-  -- * Advanced use
-  quickSpecResult) where
+  -- * For QuickSpec hackers
+  unSig, Context(..), SingleUse(..), NoWarnings(..),
+  quickSpecResult, addBackground, addInstances, instFun, customConstant, withPrintFilter, withMaxCommutativeSize) where
 
-import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))
+import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), SingleUse(..), NoWarnings(..))
 import qualified QuickSpec.Haskell as Haskell
 import qualified QuickSpec.Haskell.Resolve as Haskell
 import qualified QuickSpec.Testing.QuickCheck as QuickCheck
@@ -134,6 +135,11 @@
 
   Haskell.quickSpec (runSig sig' (Context 1 []) Haskell.defaultConfig)
 
+-- | Add some properties to the background theory.
+addBackground :: [Prop (Term (PartiallyApplied Haskell.Constant))] -> Sig
+addBackground props =
+  Sig $ \_ cfg -> cfg { Haskell.cfg_background = Haskell.cfg_background cfg ++ props }
+
 -- | A signature.
 newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config }
 
@@ -173,10 +179,11 @@
 con name x =
   Sig $ \ctx@(Context _ names) ->
     if name `elem` names then id else
-      unSig (constant (Haskell.con name x)) ctx
+      unSig (customConstant (Haskell.con name x)) ctx
 
-constant :: Haskell.Constant -> Sig
-constant con =
+-- | Add a custom constant.
+customConstant :: Haskell.Constant -> Sig
+customConstant con =
   Sig $ \(Context n _) ->
     modL Haskell.lens_constants (appendAt n [con])
 
@@ -213,8 +220,24 @@
   Sig $ \ctx@(Context _ names) ->
     if name `elem` names then id else
     let (insts, con) = Haskell.predicate name x in
-      runSig [addInstances insts `mappend` constant con] ctx
+      runSig [addInstances insts `mappend` customConstant con] ctx
 
+-- | Declare a predicate with a given name and value.
+-- The predicate should be a function which returns `Bool`.
+-- 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.
+predicateGen :: ( Predicateable a
+                , Typeable a
+                , Typeable b
+                , Typeable (PredicateTestCase a))
+                => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig
+predicateGen name x gen =
+  Sig $ \ctx@(Context _ names) ->
+    if name `elem` names then id else
+    let (insts, con) = Haskell.predicateGen name x gen in
+      runSig [addInstances insts `mappend` customConstant con] ctx
+
 -- | Declare a new monomorphic type.
 -- The type must implement `Ord` and `Arbitrary`.
 monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
@@ -255,6 +278,7 @@
 inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig
 inst = instFun
 
+-- | Declare an arbitrary value to be used by instance resolution.
 instFun :: Typeable a => a -> Sig
 instFun x = addInstances (Haskell.inst x)
 
@@ -262,6 +286,10 @@
 addInstances insts =
   Sig (\_ -> modL Haskell.lens_instances (`mappend` insts))
 
+withPrintFilter :: (Prop (Term (PartiallyApplied Haskell.Constant)) -> Bool) -> Sig
+withPrintFilter p =
+  Sig (\_ -> setL Haskell.lens_print_filter p)
+
 -- | Declare some functions as being background functions.
 -- These are functions which are not interesting on their own,
 -- but which may appear in interesting laws with non-background functions.
@@ -315,6 +343,9 @@
 -- | Set the maximum size of terms to explore (default: 7).
 withMaxTermSize :: Int -> Sig
 withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n)
+
+withMaxCommutativeSize :: Int -> Sig
+withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n)
 
 -- | Set how many times to test each discovered law (default: 1000).
 withMaxTests :: Int -> Sig
diff --git a/src/QuickSpec/Explore.hs b/src/QuickSpec/Explore.hs
--- a/src/QuickSpec/Explore.hs
+++ b/src/QuickSpec/Explore.hs
@@ -62,10 +62,10 @@
   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
   (Prop (Term fun) -> m ()) ->
   (Term fun -> testcase -> result) ->
-  Int -> Universe -> Enumerator (Term fun) -> m ()
-quickSpec present eval maxSize univ enum = do
+  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()
+quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do
   let
-    state0 = initialState univ (\t -> size t <= 5) eval
+    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval
 
     loop m n _ | m > n = return ()
     loop m n tss = do
diff --git a/src/QuickSpec/Explore/PartialApplication.hs b/src/QuickSpec/Explore/PartialApplication.hs
--- a/src/QuickSpec/Explore/PartialApplication.hs
+++ b/src/QuickSpec/Explore/PartialApplication.hs
@@ -21,7 +21,7 @@
 
 instance Sized f => Sized (PartiallyApplied f) where
   size (Partial f _) = size f
-  size (Apply _) = 0
+  size (Apply _) = 1
 
 instance Arity (PartiallyApplied f) where
   arity (Partial _ n) = n
@@ -75,9 +75,9 @@
 
 instance (Arity f, Typed f, Background f) => Background (PartiallyApplied f) where
   background (Partial f _) =
+    map (mapFun (\f -> Partial f (arity f))) (background f) ++
     [ simpleApply (partial n) (vs !! n) === partial (n+1)
-    | n <- [0..arity f-1] ] ++
-    map (mapFun (\f -> Partial f (arity f))) (background f)
+    | n <- [0..arity f-1] ]
     where
       partial i =
         App (Partial f i) (take i vs)
diff --git a/src/QuickSpec/Explore/Polymorphic.hs b/src/QuickSpec/Explore/Polymorphic.hs
--- a/src/QuickSpec/Explore/Polymorphic.hs
+++ b/src/QuickSpec/Explore/Polymorphic.hs
@@ -1,6 +1,5 @@
 -- Theory exploration which handles polymorphism.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -49,18 +48,18 @@
 -- The set of all types being explored
 data Universe = Universe { univ_types :: Set Type }
 
-makeLensAs ''Polymorphic
-  [("pm_schemas", "schemas"),
-   ("pm_universe", "univ")]
+schemas = lens pm_schemas (\x y -> y { pm_schemas = x })
+univ = lens pm_universe (\x y -> y { pm_universe = x })
 
 initialState ::
+  (Type -> Bool) ->
   Universe ->
   (Term fun -> Bool) ->
   (Term fun -> testcase -> result) ->
   Polymorphic testcase result fun norm
-initialState univ inst eval =
+initialState singleUse univ inst eval =
   Polymorphic {
-    pm_schemas = Schemas.initialState (inst . fmap fun_specialised) (eval . fmap fun_specialised),
+    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),
     pm_universe = univ }
 
 polyFun :: Typed fun => fun -> PolyFun fun
@@ -120,7 +119,7 @@
     return (norm . fmap fun_specialised)
   add prop = PolyM $ do
     univ <- access univ
-    let insts = typeInstances univ (regeneralise (mapFun fun_original prop))
+    let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))
     or <$> mapM add insts
 
 instance MonadTester testcase (Term fun) m =>
@@ -178,18 +177,22 @@
         skel (V ty x) = V (oneTypeVar ty) x
     litCs (t :=: u) = [(typ t, typ u)]
 
-typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a]
-typeInstances Universe{..} prop =
-  [ typeSubst (\x -> Map.findWithDefault (error ("not found: " ++ prettyShow x)) x sub) prop
-  | sub <- cs ]
+typeInstancesList :: [Type] -> [Type] -> [Twee.Var -> Type]
+typeInstancesList types prop =
+  map eval
+    (foldr intersection [Map.empty]
+      (map constrain
+        (usort prop)))
   where
-    cs =
-      foldr intersection [Map.empty]
-        (map (constrain (Set.toList univ_types))
-          (usort (DList.toList (termsDL prop) >>= subterms)))
+    constrain t =
+      usort [ Map.fromList (Twee.substToList sub) | u <- types, Just sub <- [Twee.match t u] ]
+    eval sub x =
+      Map.findWithDefault (error ("not found: " ++ prettyShow x)) x sub
 
-    constrain tys t =
-      usort [ Map.fromList (Twee.substToList sub) | u <- tys, Just sub <- [Twee.match (typ t) u] ]
+typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a]
+typeInstances Universe{..} prop =
+  [ typeSubst sub prop
+  | sub <- typeInstancesList (Set.toList univ_types) (map typ (DList.toList (termsDL prop) >>= subterms)) ]
 
 intersection :: [Map Twee.Var Type] -> [Map Twee.Var Type] -> [Map Twee.Var Type]
 ms1 `intersection` ms2 = usort [ Map.union m1 m2 | m1 <- ms1, m2 <- ms2, ok m1 m2 ]
@@ -197,14 +200,47 @@
     ok m1 m2 = and [ Map.lookup x m1 == Map.lookup x m2 | x <- Map.keys (Map.intersection m1 m2) ]
 
 universe :: Typed a => [a] -> Universe
-universe xs = Universe (Set.fromList base)
+universe xs = Universe (Set.fromList univ)
   where
-    -- The universe contains the type variable "a", the argument and
-    -- result type of every function (with all type variables unified), and all
-    -- subterms of these types
-    base = usort $ typeVar:concatMap (oneTypeVar . typs . typ) xs
-    typs ty = typeRes ty:typeArgs ty
+    -- Types of all functions
+    types = usort $ typeVar:map typ xs
 
+    -- Take the argument and result type of every function.
+    univBase = usort $ concatMap components types
+
+    -- Add partially-applied functions, if they can be used to
+    -- fill in a higher-order argument.
+    univHo = usort $ concatMap addHo univBase
+      where
+        addHo ty =
+          ty:
+          [ typeSubst sub ho
+          | fun <- types,
+            ho <- arrows fun,
+            sub <- typeInstancesList univBase (components fun) ]
+  
+    -- Add antiunifiers of all pairs of types, so that each equation
+    -- has a most general type
+    univ = usort $ oneTypeVar $ fixpoint antiunifiers univHo
+      where
+        antiunifiers tys =
+          usort $ map (unPoly . poly) $
+            tys ++ [antiunify ty1 ty2 | ty1 <- tys, ty2 <- tys]
+
+    components ty =
+      case unpackArrow ty of
+        Nothing -> [ty]
+        Just (ty1, ty2) -> components ty1 ++ components ty2
+
+    arrows ty =
+      concatMap arrows1 (typeArgs ty)
+      where
+        arrows1 ty
+          | isArrowType ty =
+            ty:concatMap arrows1 (typeArgs ty)
+          | otherwise =
+            []
+ 
 inUniverse :: Typed fun => Term fun -> Universe -> Bool
 t `inUniverse` Universe{..} =
   and [oneTypeVar (typ u) `Set.member` univ_types | u <- subterms t]
diff --git a/src/QuickSpec/Explore/Schemas.hs b/src/QuickSpec/Explore/Schemas.hs
--- a/src/QuickSpec/Explore/Schemas.hs
+++ b/src/QuickSpec/Explore/Schemas.hs
@@ -1,6 +1,6 @@
 -- Theory exploration which works on a schema at a time.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, TemplateHaskell, MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, MultiParamTypeClasses, FlexibleInstances #-}
 module QuickSpec.Explore.Schemas where
 
 import qualified Data.Map.Strict as Map
@@ -21,29 +21,33 @@
 import Data.Set(Set)
 import Data.Maybe
 import Control.Monad
+import Twee.Label
 
 data Schemas testcase result fun norm =
   Schemas {
+    sc_single_use :: Type -> Bool,
     sc_instantiate_singleton :: Term fun -> Bool,
     sc_empty :: Terms testcase result (Term fun) norm,
     sc_classes :: Terms testcase result (Term fun) norm,
     sc_instantiated :: Set (Term fun),
     sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) }
 
-makeLensAs ''Schemas
-  [("sc_classes", "classes"),
-   ("sc_instances", "instances"),
-   ("sc_instantiated", "instantiated")]
+classes = lens sc_classes (\x y -> y { sc_classes = x })
+single_use = lens sc_single_use (\x y -> y { sc_single_use = x })
+instances = lens sc_instances (\x y -> y { sc_instances = x })
+instantiated = lens sc_instantiated (\x y -> y { sc_instantiated = x })
 
 instance_ :: Ord fun => Term fun -> Lens (Schemas testcase result fun norm) (Terms testcase result (Term fun) norm)
 instance_ t = reading (\Schemas{..} -> keyDefault t sc_empty # instances)
 
 initialState ::
+  (Type -> Bool) ->
   (Term fun -> Bool) ->
   (Term fun -> testcase -> result) ->
   Schemas testcase result fun norm
-initialState inst eval =
+initialState singleUse inst eval =
   Schemas {
+    sc_single_use = singleUse,
     sc_instantiate_singleton = inst,
     sc_empty = Terms.initialState eval,
     sc_classes = Terms.initialState eval,
@@ -62,6 +66,7 @@
 explore t0 = do
   let t = mostSpecific t0
   res <- zoom classes (Terms.explore t)
+  singleUse <- access single_use
   case res of
     Terms.Singleton -> do
       inst <- gets sc_instantiate_singleton
@@ -69,7 +74,7 @@
         instantiateRep t
        else do
         -- Add the most general instance of the schema
-        zoom (instance_ t) (Terms.explore (mostGeneral t0))
+        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))
         return (Accepted [])
     Terms.Discovered ([] :=>: _ :=: u) ->
       exploreIn u t
@@ -85,7 +90,8 @@
   StateT (Schemas testcase result fun norm) m (Result fun)
 exploreIn rep t = do
   -- First check if schema is redundant
-  res <- zoom (instance_ rep) (Terms.explore (mostGeneral t))
+  singleUse <- access single_use
+  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))
   case res of
     Terms.Discovered prop -> do
       add prop
@@ -118,40 +124,45 @@
   MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>
   Term fun -> Term fun ->
   StateT (Schemas testcase result fun norm) m (Result fun)
-instantiate rep t = zoom (instance_ rep) $ do
-  let instances = sortBy (comparing generality) (allUnifications (mostGeneral t))
-  Accepted <$> catMaybes <$> forM instances (\t -> do
-    res <- Terms.explore t
-    case res of
-      Terms.Discovered prop -> do
-        add prop
-        return (Just prop)
-      _ -> return Nothing)
+instantiate rep t = do
+  singleUse <- access single_use
+  zoom (instance_ rep) $ do
+    let instances = sortBy (comparing generality) (allUnifications singleUse (mostGeneral singleUse t))
+    Accepted <$> catMaybes <$> forM instances (\t -> do
+      res <- Terms.explore t
+      case res of
+        Terms.Discovered prop -> do
+          add prop
+          return (Just prop)
+        _ -> return Nothing)
 
 -- sortBy (comparing generality) should give most general instances first.
 generality :: Term f -> (Int, [Var])
 generality t = (-length (usort (vars t)), vars t)
 
 -- | Instantiate a schema by making all the variables different.
-mostGeneral :: Term f -> Term f
-mostGeneral s = evalState (aux s) Map.empty
+mostGeneral :: (Type -> Bool) -> Term f -> Term f
+mostGeneral singleUse s = evalState (aux s) Map.empty
   where
     aux (Var (V ty _)) = do
       m <- get
-      let n = Map.findWithDefault 0 ty m
-      put $! Map.insert ty (n+1) m
-      return (Var (V ty n))
+      let n :: Int
+          n = Map.findWithDefault 0 ty m
+      unless (singleUse ty) $
+        put $! Map.insert ty (n+1) m
+      let m = fromIntegral (labelNum (label (ty, n)))
+      return (Var (V ty m))
     aux (App f xs) = fmap (App f) (mapM aux xs)
 
 mostSpecific :: Term f -> Term f
 mostSpecific = subst (\(V ty _) -> Var (V ty 0))
 
-allUnifications :: Term fun -> [Term fun]
-allUnifications t = map f ss
+allUnifications :: (Type -> Bool) -> Term fun -> [Term fun]
+allUnifications singleUse t = map f ss
   where
     vs = [ map (x,) (select xs) | xs <- partitionBy typ (usort (vars t)), x <- xs ]
     ss = map Map.fromList (sequence vs)
     go s x = Map.findWithDefault undefined x s
     f s = subst (Var . go s) t
-    select [V ty x] = [V ty x, V ty (succ x)]
+    select [V ty x] | not (singleUse ty) = [V ty x, V ty (succ x)]
     select xs = take 4 xs
diff --git a/src/QuickSpec/Explore/Terms.hs b/src/QuickSpec/Explore/Terms.hs
--- a/src/QuickSpec/Explore/Terms.hs
+++ b/src/QuickSpec/Explore/Terms.hs
@@ -1,6 +1,6 @@
 -- Theory exploration which accepts one term at a time.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TemplateHaskell #-}
+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards #-}
 module QuickSpec.Explore.Terms where
 
 import qualified Data.Map.Strict as Map
@@ -30,7 +30,7 @@
     -- ill-typed equations and bad things happening in the pruner.
     tm_tree   :: Map Type (DecisionTree testcase result term) }
 
-makeLensAs ''Terms [("tm_tree", "tree")]
+tree = lens tm_tree (\x y -> y { tm_tree = x })
 
 treeForType :: Type -> Lens (Terms testcase result term norm) (DecisionTree testcase result term)
 treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree)
diff --git a/src/QuickSpec/Haskell.hs b/src/QuickSpec/Haskell.hs
--- a/src/QuickSpec/Haskell.hs
+++ b/src/QuickSpec/Haskell.hs
@@ -10,7 +10,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FunctionalDependencies #-}
@@ -21,7 +20,7 @@
 import QuickSpec.Type
 import QuickSpec.Prop
 import QuickSpec.Pruning
-import Test.QuickCheck hiding (total)
+import Test.QuickCheck hiding (total, classify, subterms)
 import Data.Constraint hiding ((\\))
 import Data.List
 import Data.Proxy
@@ -45,6 +44,7 @@
 import QuickSpec.Terminal
 import Text.Printf
 import QuickSpec.Utils
+import Data.Lens.Light
 import GHC.TypeLits
 import QuickSpec.Explore.Conditionals
 import Control.Spoon
@@ -138,6 +138,8 @@
 -- A token used in the instance list for types that shouldn't generate warnings
 data NoWarnings a = NoWarnings
 
+data SingleUse a = SingleUse
+
 instance c => Arbitrary (Dict c) where
   arbitrary = return Dict
 
@@ -408,10 +410,6 @@
 
 data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }
 
--- A `suchThat` generator for a predicate
-genSuchThat :: (Predicateable a, Arbitrary (PredicateTestCase a)) => a -> Gen (TestCaseWrapped x (PredicateTestCase a))
-genSuchThat p = TestCaseWrapped <$> arbitrary `suchThat` uncrry p
-
 true :: Constant
 true = con "True" True
 
@@ -420,11 +418,13 @@
 
 -- | Declare a predicate with a given name and value.
 -- The predicate should have type @... -> Bool@.
-predicate :: forall a. ( Predicateable a
+-- Uses an explicit generator.
+predicateGen :: forall a b. ( Predicateable a
              , Typeable a
+             , Typeable b
              , Typeable (PredicateTestCase a))
-             => String -> a -> (Instances, Constant)
-predicate name pred =
+             => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
+predicateGen name pred gen =
   let
     -- The following doesn't compile on GHC 7.10:
     -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))
@@ -446,8 +446,8 @@
       mconcat $ map (valueInst . addName)
         [toValue (Identity inst1), toValue (Identity inst2)]
 
-    inst1 :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
-    inst1 Dict = genSuchThat pred
+    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
+    inst1 x = TestCaseWrapped <$> gen x
 
     inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))
     inst2 = Names [name ++ "_var"]
@@ -468,28 +468,44 @@
   in
     (instances, conPred)
 
+-- | Declare a predicate with a given name and value.
+-- The predicate should have type @... -> Bool@.
+predicate :: forall a. ( Predicateable a
+          , Typeable a
+          , Typeable (PredicateTestCase a))
+          => String -> a -> (Instances, Constant)
+predicate name pred = predicateGen name pred inst
+  where
+    inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
+    inst Dict = arbitrary `suchThat` uncrry pred
+
 data Config =
   Config {
     cfg_quickCheck :: QuickCheck.Config,
     cfg_twee :: Twee.Config,
     cfg_max_size :: Int,
+    cfg_max_commutative_size :: 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.
     -- head cfg_constants contains all the background functions.
     cfg_constants :: [[Constant]],
     cfg_default_to :: Type,
-    cfg_infer_instance_types :: Bool
+    cfg_infer_instance_types :: Bool,
+    cfg_background :: [Prop (Term (PartiallyApplied Constant))],
+    cfg_print_filter :: Prop (Term (PartiallyApplied Constant)) -> Bool
     }
 
-makeLensAs ''Config
-  [("cfg_quickCheck", "lens_quickCheck"),
-   ("cfg_twee", "lens_twee"),
-   ("cfg_max_size", "lens_max_size"),
-   ("cfg_instances", "lens_instances"),
-   ("cfg_constants", "lens_constants"),
-   ("cfg_default_to", "lens_default_to"),
-   ("cfg_infer_instance_types", "lens_infer_instance_types")]
+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_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 })
+lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x })
+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 })
 
 defaultConfig :: Config
 defaultConfig =
@@ -497,10 +513,13 @@
     cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 100, QuickCheck.cfg_fixed_seed = Nothing },
     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_instances = mempty,
     cfg_constants = [],
     cfg_default_to = typeRep (Proxy :: Proxy Int),
-    cfg_infer_instance_types = False }
+    cfg_infer_instance_types = False,
+    cfg_background = [],
+    cfg_print_filter = \_ -> True }
 
 -- Extra types for the universe that come from in-scope instances.
 instanceTypes :: Instances -> Config -> [Type]
@@ -571,7 +590,9 @@
 quickSpec :: Config -> IO [Prop (Term (PartiallyApplied Constant))]
 quickSpec cfg@Config{..} = do
   let
-    constantsOf f = true:f cfg_constants ++ concatMap selectors (f cfg_constants)
+    constantsOf f =
+      [true | any (/= Function) (map classify (f cfg_constants))] ++
+      f cfg_constants ++ concatMap selectors (f cfg_constants)
     constants = constantsOf concat
     
     univ = conditionalsUniverse (instanceTypes instances cfg) constants
@@ -582,11 +603,12 @@
     present funs prop = do
       norm <- normaliser
       let prop' = makeDefinition funs (ac norm (conditionalise prop))
-      (n :: Int, props) <- get
-      put (n+1, prop':props)
-      putLine $
-        printf "%3d. %s" n $ show $
-          prettyProp (names instances) prop' <+> maybeType prop
+      when (cfg_print_filter prop) $ do
+        (n :: Int, props) <- get
+        put (n+1, prop':props)
+        putLine $
+          printf "%3d. %s" n $ show $
+            prettyProp (names instances) prop' <+> maybeType prop
 
     -- Put an equation that defines the function f into the form f lhs = rhs.
     -- An equation defines f if:
@@ -633,10 +655,16 @@
     enumerator cons =
       sortTerms measure $
       filterEnumerator (all constraintsOk . funs) $
+      filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $
       enumerateConstants atomic `mappend` enumerateApplications
       where
         atomic = cons ++ [Var (V typeVar 0)]
 
+    conditions t = usort [p | f <- funs t, Selector _ p _ <- [classify f]]
+
+    singleUse ty =
+      isJust (findInstance instances ty :: Maybe (Value SingleUse))
+
     mainOf n f g = do
       unless (null (f cfg_constants)) $ do
         putLine $ show $ pPrintSignature
@@ -646,12 +674,15 @@
         putText (prettyShow (warnings univ instances cfg))
         putLine "== Laws =="
       let pres = if n == 0 then \_ -> return () else present (constantsOf f)
-      QuickSpec.Explore.quickSpec pres (flip eval) cfg_max_size univ
+      QuickSpec.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size singleUse univ
         (enumerator [partial fun | fun <- constantsOf g])
       when (n > 0) $ do
         putLine ""
 
-    main = mapM_ round [0..rounds-1]
+    main = do
+      forM_ cfg_background $ \prop -> do
+        add prop
+      mapM_ round [0..rounds-1]
       where
         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))
         rounds = length cfg_constants
diff --git a/src/QuickSpec/Pruning/Twee.hs b/src/QuickSpec/Pruning/Twee.hs
--- a/src/QuickSpec/Pruning/Twee.hs
+++ b/src/QuickSpec/Pruning/Twee.hs
@@ -15,12 +15,13 @@
 import QuickSpec.Pruning.UntypedTwee(Config(..))
 
 newtype Pruner fun m a =
-  Pruner (Background.Pruner fun (Types.Pruner fun (Untyped.Pruner (Types.Tagged fun) m)) a)
-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadPruner (Term fun) (Term fun), MonadTerminal)
+  Pruner (Types.Pruner fun (Background.Pruner (Types.Tagged fun) (Untyped.Pruner (Types.Tagged fun) m)) a)
+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term,
+            MonadPruner (Term fun) (Untyped.Norm (Types.Tagged fun)), MonadTerminal)
 
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift . lift
 
 run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a
 run config (Pruner x) =
-  Untyped.run config (Types.run (Background.run x))
+  Untyped.run config (Background.run (Types.run x))
diff --git a/src/QuickSpec/Pruning/Types.hs b/src/QuickSpec/Pruning/Types.hs
--- a/src/QuickSpec/Pruning/Types.hs
+++ b/src/QuickSpec/Pruning/Types.hs
@@ -51,18 +51,18 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner
 
-instance (PrettyTerm fun, Typed fun, MonadPruner (UntypedTerm fun) (UntypedTerm fun) pruner) => MonadPruner (TypedTerm fun) (TypedTerm fun) (Pruner fun pruner) where
+instance (PrettyTerm fun, Typed fun, MonadPruner (UntypedTerm fun) norm pruner) => MonadPruner (TypedTerm fun) norm (Pruner fun pruner) where
   normaliser =
     Pruner $ do
-      norm <- normaliser :: pruner (UntypedTerm fun -> UntypedTerm fun)
-      
+      norm <- normaliser :: pruner (UntypedTerm fun -> norm)
+
       -- Note that we don't call addFunction on the functions in the term.
       -- This is because doing so might be expensive, as adding typing
       -- axioms starts the completion algorithm.
       -- This is OK because in encode, we tag all functions and variables
       -- with their types (i.e. we can fall back to the naive type encoding).
       return $ \t ->
-        decode . norm . encode $ t
+        norm . encode $ t
 
   add prop = lift (add (encode <$> canonicalise prop))
 
@@ -108,20 +108,3 @@
 encode (Var x) = tag (typ x) (Var x)
 encode (App f ts) =
   tag (typeDrop (length ts) (typ f)) (App (Func f) (map encode ts))
-
-decode :: Typed fun => UntypedTerm fun -> TypedTerm fun
-decode = dec Nothing
-  where
-    dec _ (App (Tag ty) [t]) =
-      dec (Just ty) t
-    dec _ (App Tag{} _) =
-      error "Tag function applied with wrong arity"
-    dec (Just ty) (Var (V _ x)) =
-      Var (V ty x)
-    dec Nothing (Var _) =
-      error "Naked variable in type-encoded term"
-    dec _ (App (Func f) ts) =
-      App f $
-        zipWith dec
-          (map Just (typeArgs (typ f)))
-          ts
diff --git a/src/QuickSpec/Pruning/UntypedTwee.hs b/src/QuickSpec/Pruning/UntypedTwee.hs
--- a/src/QuickSpec/Pruning/UntypedTwee.hs
+++ b/src/QuickSpec/Pruning/UntypedTwee.hs
@@ -1,6 +1,6 @@
 -- A pruner that uses twee. Does not respect types.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances, TemplateHaskell #-}
+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}
 module QuickSpec.Pruning.UntypedTwee where
 
 import QuickSpec.Testing
@@ -8,7 +8,7 @@
 import QuickSpec.Prop
 import QuickSpec.Term
 import QuickSpec.Type
-import QuickSpec.Utils
+import Data.Lens.Light
 import qualified Twee
 import qualified Twee.Equation as Twee
 import qualified Twee.KBO as KBO
@@ -16,7 +16,7 @@
 import Twee hiding (Config(..))
 import Twee.Rule hiding (normalForms)
 import Twee.Proof hiding (Config, defaultConfig)
-import Twee.Base(Ordered(..), Extended(..), EqualsBonus, pattern F, pattern Empty, unpack)
+import Twee.Base(Ordered(..), Extended(..), EqualsBonus)
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State.Strict hiding (State)
 import Control.Monad.Trans.Class
@@ -30,9 +30,8 @@
     cfg_max_term_size :: Int,
     cfg_max_cp_depth :: Int }
 
-makeLensAs ''Config
-  [("cfg_max_term_size", "lens_max_term_size"),
-   ("cfg_max_cp_depth", "lens_max_cp_depth")]
+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
   lessEq = KBO.lessEq
@@ -64,8 +63,10 @@
   size (Twee.Skolem _) = 1
   size (Twee.Function f) = size f
 
+type Norm fun = Twee.Term (Extended fun)
+
 instance (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>
-  MonadPruner (Term fun) (Term fun) (Pruner fun m) where
+  MonadPruner (Term fun) (Norm fun) (Pruner fun m) where
   normaliser = Pruner $ do
     state <- lift get
     return $ \t ->
@@ -85,19 +86,18 @@
     return (Set.null (Set.intersection t' u'))
 
   add _ =
-    error "twee pruner doesn't support non-unit equalities"
+    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) =>
-  State (Extended fun) -> Term fun -> Term fun
+  State (Extended fun) -> Term fun -> Norm fun
 normaliseTwee state t =
-  fromTwee $
-    result (normaliseTerm state (simplifyTerm state (skolemise t)))
+  result (normaliseTerm state (simplifyTerm state (skolemise t)))
 
 normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
-  State (Extended fun) -> Term fun -> Set (Term fun)
+  State (Extended fun) -> Term fun -> Set (Norm fun)
 normalFormsTwee state t =
-  Set.map fromTwee $
-    Set.map result (normalForms state (skolemise t))
+  Set.map result (normalForms state (skolemise t))
 
 addTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)
@@ -124,14 +124,3 @@
       Twee.con (Twee.fun (Skolem (Twee.V x)))
     sk (App f ts) =
       Twee.app (Twee.fun (Function f)) (map sk ts)
-
-fromTwee :: Twee.Term (Extended f) -> Term f
-fromTwee = unsk
-  where
-    unsk (Twee.App (F Minimal) Empty) =
-      Var (V typeVar 0)
-    unsk (Twee.App (F (Skolem (Twee.V x))) Empty) =
-      Var (V typeVar x)
-    unsk (Twee.App (F (Function f)) ts) =
-      App f (map unsk (unpack ts))
-    unsk _ = error "variable introduced by rewriting"
diff --git a/src/QuickSpec/Term.hs b/src/QuickSpec/Term.hs
--- a/src/QuickSpec/Term.hs
+++ b/src/QuickSpec/Term.hs
@@ -53,8 +53,8 @@
   size (App f ts) = size f + sum (map size ts)
 
 instance Pretty Var where
-  --pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)
-  pPrint x = text "X" <#> pPrint (var_id x+1)
+  pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)
+  --pPrint x = text "X" <#> pPrint (var_id x+1)
 
 instance PrettyTerm f => Pretty (Term f) where
   pPrintPrec l p (Var x) = pPrintPrec l p x
@@ -148,15 +148,20 @@
 -- | A standard term ordering - size, skeleton, generality.
 -- Satisfies the property:
 -- if measure (schema t) < measure (schema u) then t < u.
-type Measure f = (Int, Int, MeasureFuns f, Int, [Var])
+type Measure f = (Int, Int, Int, MeasureFuns f, Int, [Var])
 -- | Compute the term ordering for a term.
-measure :: Sized f => Term f -> Measure f
+measure :: (Sized f, Typed f) => Term f -> Measure f
 measure t =
-  (size t, -length (vars t), MeasureFuns (skel t),
+  (size t, sizeHO t, -length (vars t), MeasureFuns (skel t),
    -length (usort (vars t)), vars t)
   where
     skel (Var (V ty _)) = Var (V ty 0)
     skel (App f ts) = App f (map skel ts)
+    -- Prefer fully-applied terms to partially-applied ones.
+    -- This function computes the size, but adds 1 for every
+    -- unapplied function.
+    sizeHO (App f ts) = size f + typeArity (typ f) - length ts + sum (map sizeHO ts)
+    sizeHO Var{} = 1
 
 -- | A helper for `Measure`.
 newtype MeasureFuns f = MeasureFuns (Term f)
@@ -201,7 +206,7 @@
 instance (Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) where
   pPrintPrec l p (Inl x) = pPrintPrec l p x
   pPrintPrec l p (Inr x) = pPrintPrec l p x
-  
+
 instance (PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) where
   termStyle (Inl x) = termStyle x
   termStyle (Inr x) = termStyle x
diff --git a/src/QuickSpec/Testing/QuickCheck.hs b/src/QuickSpec/Testing/QuickCheck.hs
--- a/src/QuickSpec/Testing/QuickCheck.hs
+++ b/src/QuickSpec/Testing/QuickCheck.hs
@@ -1,6 +1,6 @@
 -- Testing conjectures using QuickCheck.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving, TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-}
 module QuickSpec.Testing.QuickCheck where
 
 import QuickSpec.Testing
@@ -16,7 +16,7 @@
 import Data.List
 import System.Random
 import QuickSpec.Terminal
-import QuickSpec.Utils
+import Data.Lens.Light
 
 data Config =
   Config {
@@ -25,10 +25,9 @@
     cfg_fixed_seed :: Maybe QCGen}
   deriving Show
 
-makeLensAs ''Config
-  [("cfg_num_tests", "lens_num_tests"),
-   ("cfg_max_test_size", "lens_max_test_size"),
-   ("cfg_fixed_seed", "lens_fixed_seed")]
+lens_num_tests = lens cfg_num_tests (\x y -> y { cfg_num_tests = x })
+lens_max_test_size = lens cfg_max_test_size (\x y -> y { cfg_max_test_size = x })
+lens_fixed_seed = lens cfg_fixed_seed (\x y -> y { cfg_fixed_seed = x })
 
 data Environment testcase term result =
   Environment {
@@ -53,7 +52,6 @@
     n = cfg_num_tests
     k = max 1 cfg_max_test_size
     bias = 3
-    cfg_max_test_size = 100
     -- Bias tests towards smaller sizes.
     -- We do this by distributing the cube of the size uniformly.
     sizes =
@@ -77,7 +75,7 @@
   where
     leftovers = n `mod` k
 
-instance (MonadTerminal m, Eq result) => MonadTester testcase term (Tester testcase term result m) where
+instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where
   test prop =
     Tester $ do
       env <- ask
diff --git a/src/QuickSpec/Type.hs b/src/QuickSpec/Type.hs
--- a/src/QuickSpec/Type.hs
+++ b/src/QuickSpec/Type.hs
@@ -9,7 +9,7 @@
   Typeable,
   Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,
   typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,
-  arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,
+  arrowType, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,
   isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,
   -- * Things that have types
   Typed(..), typeSubst, typesDL, tyVars, cast, matchType,
@@ -150,6 +150,10 @@
 arrowType [] res = res
 arrowType (arg:args) res =
   build (app (fun Arrow) [arg, arrowType args res])
+
+-- | Is a given type a function type?
+isArrowType :: Type -> Bool
+isArrowType = isJust . unpackArrow
 
 -- | Decompose a function type into (argument, result).
 --
diff --git a/src/QuickSpec/Utils.hs b/src/QuickSpec/Utils.hs
--- a/src/QuickSpec/Utils.hs
+++ b/src/QuickSpec/Utils.hs
@@ -17,6 +17,9 @@
 import Data.Map(Map)
 import Language.Haskell.TH.Syntax
 import Data.Lens.Light
+import Twee.Base hiding (lookup)
+import Control.Monad.Trans.State.Strict
+import Control.Monad
 
 (#) :: Category.Category cat => cat b c -> cat a b -> cat a c
 (#) = (Category..)
@@ -104,3 +107,32 @@
 appendAt n xs [] = appendAt n xs [[]]
 appendAt 0 xs (ys:yss) = (ys ++ xs):yss
 appendAt n xs (ys:yss) = ys:appendAt (n-1) xs yss
+
+-- Should be in Twee.Base.
+antiunify :: Ord f => Term f -> Term f -> Term f
+antiunify t u =
+  build $ evalState (loop t u) (succ (snd (bound t) `max` snd (bound u)), Map.empty)
+  where
+    loop (App f ts) (App g us)
+      | f == g =
+        app f <$> zipWithM loop (unpack ts) (unpack us)
+    loop (Var x) (Var y)
+      | x == y =
+        return (var x)
+    loop t u = do
+      (next, m) <- get
+      case Map.lookup (t, u) m of
+        Just v -> return (var v)
+        Nothing -> do
+          put (succ next, Map.insert (t, u) next m)
+          return (var next)
+
+{-# INLINE fixpoint #-}
+fixpoint :: Eq a => (a -> a) -> a -> a
+fixpoint f x = fxp x
+  where
+    fxp x
+      | x == y = x
+      | otherwise = fxp y
+      where
+        y = f x