diff --git a/examples/Curry.hs b/examples/Curry.hs
new file mode 100644
--- /dev/null
+++ b/examples/Curry.hs
@@ -0,0 +1,9 @@
+import QuickSpec
+
+main = quickSpec [
+  con "curry" (curry :: ((A, B) -> C) -> A -> B -> C),
+  con "fst" (fst :: (A, B) -> A),
+  con "snd" (snd :: (A, B) -> B),
+  con "id" (id :: A -> A),
+  con "." ((.) :: (B -> C) -> (A -> B) -> A -> C),
+  con "|" ((\f g x -> (f x, g x)) :: (A -> B) -> (A -> C) -> A -> (B, C))]
diff --git a/examples/Lists.hs b/examples/Lists.hs
--- a/examples/Lists.hs
+++ b/examples/Lists.hs
@@ -1,7 +1,6 @@
 -- Some usual list functions.
 {-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-}
 import QuickSpec
-import Data.List
 
 main = quickSpec [
   con "reverse" (reverse :: [A] -> [A]),
@@ -12,6 +11,4 @@
   con "concat" (concat :: [[A]] -> [A]),
 
   -- Add some numeric functions to get more laws about length.
-  background [
-    con "0" (0 :: Int),
-    con "+" ((+) :: Int -> Int -> Int) ] ]
+  arith (Proxy :: Proxy Int) ]
diff --git a/examples/PrettyPrinting.hs b/examples/PrettyPrinting.hs
--- a/examples/PrettyPrinting.hs
+++ b/examples/PrettyPrinting.hs
@@ -2,6 +2,7 @@
 -- Illustrates observational equality and using custom generators.
 -- See the QuickSpec paper for more details.
 {-# LANGUAGE DeriveDataTypeable, TypeOperators, StandaloneDeriving, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
+import Prelude hiding ((<>))
 import Control.Monad
 import Test.QuickCheck
 import QuickSpec
@@ -65,6 +66,5 @@
   con "<>" (<>),
   con "$$" ($$),
 
-  inst (Sub Dict :: () :- Observe Context Str Doc),
-  inst (Sub Dict :: () :- Arbitrary Doc),
+  monoTypeObserve (Proxy :: Proxy Doc),
   defaultTo (Proxy :: Proxy Bool)]
diff --git a/examples/PrettyPrintingModel.hs b/examples/PrettyPrintingModel.hs
--- a/examples/PrettyPrintingModel.hs
+++ b/examples/PrettyPrintingModel.hs
@@ -2,6 +2,7 @@
 -- Illustrates running QuickSpec on a progressively larger set of signatures.
 -- See the QuickSpec paper for more details.
 {-# LANGUAGE DeriveDataTypeable, TypeOperators #-}
+import Prelude hiding ((<>))
 import Control.Monad
 import Test.QuickCheck
 import QuickSpec
@@ -43,7 +44,11 @@
     con "0" (0 :: Int),
     con "+" ((+) :: Int -> Int -> Int),
     con "length" (length :: String -> Int) ],
-  con "text" text,
-  con "nest" nest,
-  con "$$" ($$),
-  con "<>" (<>) ]
+  series [sig1, sig2]]
+  where
+    sig1 = [
+      con "text" text,
+      con "nest" nest,
+      con "$$" ($$),
+      con "<>" (<>) ]
+    sig2 = [con "nesting" nesting]
diff --git a/examples/Sorted.hs b/examples/Sorted.hs
--- a/examples/Sorted.hs
+++ b/examples/Sorted.hs
@@ -9,10 +9,7 @@
 sorted (x:y:xs) = x <= y && sorted (y:xs)
 
 main = quickSpec [
-  background [
-    con ":" ((:) :: A -> [A] -> [A]),
-    con "[]" ([] :: [A]) ],
-
+  lists `without` ["++"],
   con "sort" (sort :: [Int] -> [Int]),
   con "insert" (insert :: Int -> [Int] -> [Int]),
   predicate "sorted" (sorted :: [Int] -> Bool) ]
diff --git a/examples/Zip.hs b/examples/Zip.hs
--- a/examples/Zip.hs
+++ b/examples/Zip.hs
@@ -10,7 +10,6 @@
 main = quickSpec [
   -- Explore bigger terms.
   withMaxTermSize 8,
-  withPruningDepth 10,
   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
+Version:             2.1
 Cabal-version:       >= 1.6
 Build-type:          Simple
 
@@ -51,6 +51,7 @@
   examples/Arith.hs
   examples/Bools.hs
   examples/Composition.hs
+  examples/Curry.hs
   examples/Geometry.hs
   examples/HugeLists.hs
   examples/IntSet.hs
@@ -82,6 +83,7 @@
     QuickSpec.Explore.Terms
     QuickSpec.Haskell
     QuickSpec.Haskell.Resolve
+    QuickSpec.Parse
     QuickSpec.Prop
     QuickSpec.Pruning
     QuickSpec.Pruning.Background
@@ -98,14 +100,15 @@
 
   Build-depends:
     QuickCheck >= 2.10,
+    quickcheck-instances >= 0.3.15,
     base >= 4 && < 5,
     constraints,
     containers,
     data-lens-light >= 0.1.1,
     dlist,
     random,
-    reflection,
+    spoon,
     template-haskell,
     transformers,
-    twee-lib >= 2.1.2,
+    twee-lib == 2.1.5,
     uglymemo
diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs
--- a/src/QuickSpec.hs
+++ b/src/QuickSpec.hs
@@ -22,10 +22,12 @@
 -- You must also declare those instances to QuickSpec, by including them in the
 -- signature. For monomorphic types you can do this using `monoType`:
 --
--- > data T = ...
--- > main = quickSpec [
--- >   ...,
--- >   `monoType` (Proxy :: Proxy T)]
+-- @
+-- data T = ...
+-- main = quickSpec [
+--   ...,
+--   `monoType` (Proxy :: Proxy T)]
+-- @
 --
 -- You can only declare monomorphic types with `monoType`. If you want to test
 -- your own polymorphic types, you must explicitly declare `Arbitrary` and `Ord`
@@ -52,10 +54,16 @@
 -- * @<https://github.com/nick8325/quickspec/tree/master/examples/Parsing.hs Parsing.hs>@: parser combinators. Demonstrates testing polymorphic datatypes and using observational equality.
 --
 -- You can also find some larger case studies in our paper,
--- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick
--- specifications for the busy programmer>.
+-- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick specifications for the busy programmer>.
 
-{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, TypeOperators, MultiParamTypeClasses, FunctionalDependencies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
 module QuickSpec(
   -- * Running QuickSpec
   quickSpec, Sig, Signature(..),
@@ -66,23 +74,38 @@
   A, B, C, D, E,
 
   -- * Declaring types
-  monoType, vars, monoTypeWithVars, inst, Observe(..),
+  monoType, monoTypeObserve, vars, monoTypeWithVars, inst, Observe(..),
 
+  -- * Standard signatures
+  -- | The \"prelude\": a standard signature containing useful functions
+  --   like '++', which can be used as background theory.
+  lists, arith, funs, bools, prelude, without,
+
   -- * Exploring functions in series
   background, series,
 
+  -- * Including type class constraints (experimental, subject to change)
+  type (==>), liftC, instanceOf,
+
   -- * Customising QuickSpec
   withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,
   withPruningDepth, withPruningTermSize, withFixedSeed,
+  withInferInstanceTypes,
 
   -- * Re-exported functionality
-  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where
+  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary,
 
-import QuickSpec.Haskell(Predicateable, TestCase, Names(..), Observe(..))
+  -- * Advanced use
+  quickSpecResult) where
+
+import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))
 import qualified QuickSpec.Haskell as Haskell
 import qualified QuickSpec.Haskell.Resolve as Haskell
 import qualified QuickSpec.Testing.QuickCheck as QuickCheck
 import qualified QuickSpec.Pruning.UntypedTwee as Twee
+import QuickSpec.Explore.PartialApplication
+import QuickSpec.Prop
+import QuickSpec.Term(Term)
 import Test.QuickCheck
 import Test.QuickCheck.Random
 import Data.Constraint
@@ -90,32 +113,55 @@
 import QuickSpec.Utils
 import QuickSpec.Type hiding (defaultTo)
 import Data.Proxy
+import System.Environment
+import Data.Semigroup(Semigroup(..))
 
 -- | Run QuickSpec. See the documentation at the top of this file.
 quickSpec :: Signature sig => sig -> IO ()
-quickSpec signature =
-  Haskell.quickSpec (sig 0 Haskell.defaultConfig)
-  where
-    Sig sig = toSig signature
+quickSpec sig = do
+  quickSpecResult sig
+  return ()
 
+-- | Run QuickSpec, returning the list of discovered properties.
+quickSpecResult :: Signature sig => sig -> IO [Prop (Term (PartiallyApplied Haskell.Constant))]
+quickSpecResult sig = do
+  -- Undocumented feature for testing :)
+  seed <- lookupEnv "QUICKCHECK_SEED"
+  let
+    sig' = case seed of
+      Nothing -> signature sig
+      Just xs -> signature [signature sig, withFixedSeed (read xs)]
+
+  Haskell.quickSpec (runSig sig' (Context 1 []) Haskell.defaultConfig)
+
 -- | A signature.
-newtype Sig = Sig (Int -> Haskell.Config -> Haskell.Config)
+newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config }
 
+-- Settings for building the signature.
+-- Int: number of nested calls to 'background'.
+-- [String]: list of names to exclude.
+data Context = Context Int [String]
+
+instance Semigroup Sig where
+  Sig sig1 <> Sig sig2 = Sig (\ctx -> sig2 ctx . sig1 ctx)
 instance Monoid Sig where
   mempty = Sig (\_ -> id)
-  Sig sig1 `mappend` Sig sig2 = Sig (\n -> sig2 n . sig1 n)
+  mappend = (<>)
 
 -- | A class of things that can be used as a QuickSpec signature.
 class Signature sig where
   -- | Convert the thing to a signature.
-  toSig :: sig -> Sig
+  signature :: sig -> Sig
 
 instance Signature Sig where
-  toSig = id
+  signature = id
 
 instance Signature sig => Signature [sig] where
-  toSig = mconcat . map toSig
+  signature = mconcat . map signature
 
+runSig :: Signature sig => sig -> Context -> Haskell.Config -> Haskell.Config
+runSig = unSig . signature
+
 -- | Declare a constant with a given name and value.
 -- If the constant you want to use is polymorphic, you can use the types
 -- `A`, `B`, `C`, `D`, `E` to monomorphise it, for example:
@@ -125,8 +171,27 @@
 -- QuickSpec will then understand that the constant is really polymorphic.
 con :: Typeable a => String -> a -> Sig
 con name x =
-  Sig (\n -> modL Haskell.lens_constants (appendAt n (Haskell.con name x)))
+  Sig $ \ctx@(Context _ names) ->
+    if name `elem` names then id else
+      unSig (constant (Haskell.con name x)) ctx
 
+constant :: Haskell.Constant -> Sig
+constant con =
+  Sig $ \(Context n _) ->
+    modL Haskell.lens_constants (appendAt n [con])
+
+-- | Type class constraints as first class citizens
+type c ==> t = Dict c -> t
+
+-- | Lift a constrained type to a `==>` type which QuickSpec
+-- can work with
+liftC :: (c => a) -> c ==> a
+liftC a Dict = a
+
+-- | Add an instance of a type class to the signature
+instanceOf :: forall c. (Typeable c, c) => Sig
+instanceOf = inst (Sub Dict :: () :- c)
+
 -- | 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,
@@ -142,15 +207,13 @@
 -- @
 predicate :: ( Predicateable a
              , Typeable a
-             , Typeable (TestCase a))
+             , Typeable (PredicateTestCase a))
              => String -> a -> Sig
 predicate name x =
-  Sig (\n -> modL Haskell.lens_predicates (appendAt n (Haskell.predicate name x)))
-
-appendAt :: Int -> a -> [[a]] -> [[a]]
-appendAt n x [] = appendAt n x [[]]
-appendAt 0 x (xs:xss) = (xs ++ [x]):xss
-appendAt n x (xs:xss) = xs:appendAt (n-1) x xss
+  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
 
 -- | Declare a new monomorphic type.
 -- The type must implement `Ord` and `Arbitrary`.
@@ -160,6 +223,16 @@
     inst (Sub Dict :: () :- Ord a),
     inst (Sub Dict :: () :- Arbitrary a)]
 
+-- | Declare a new monomorphic type using observational equivalence.
+-- The type must implement `Observe` and `Arbitrary`.
+monoTypeObserve :: forall proxy test outcome a.
+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
+  proxy a -> Sig
+monoTypeObserve _ =
+  mconcat [
+    inst (Sub Dict :: () :- Observe test outcome a),
+    inst (Sub Dict :: () :- Arbitrary a)]
+
 -- | Declare a new monomorphic type, saying how you want variables of that type to be named.
 monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
 monoTypeWithVars xs proxy =
@@ -183,9 +256,12 @@
 inst = instFun
 
 instFun :: Typeable a => a -> Sig
-instFun x =
-  Sig (\_ -> modL Haskell.lens_instances (`mappend` Haskell.inst x))
+instFun x = addInstances (Haskell.inst x)
 
+addInstances :: Haskell.Instances -> Sig
+addInstances insts =
+  Sig (\_ -> modL Haskell.lens_instances (`mappend` insts))
+
 -- | 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.
@@ -202,11 +278,15 @@
 -- >     con "0" (0 :: Int),
 -- >     con "+" ((+) :: Int -> Int -> Int) ] ]
 background :: Signature sig => sig -> Sig
-background signature =
-  Sig (\n -> sig (n+1))
-  where
-    Sig sig = toSig signature
+background sig =
+  Sig (\(Context _ xs) -> runSig sig (Context 0 xs))
 
+-- | Remove a function or predicate from the signature.
+-- Useful in combination with 'prelude' and friends.
+without :: Signature sig => sig -> [String] -> Sig
+without sig xs =
+  Sig (\(Context n ys) -> runSig sig (Context n (ys ++ xs)))
+
 -- | Run QuickCheck on a series of signatures. Tests the functions in the first
 -- signature, then adds the functions in the second signature, then adds the
 -- functions in the third signature, and so on.
@@ -226,9 +306,11 @@
 -- >       con "++" ((++) :: [A] -> [A] -> [A]),
 -- >       con "length" (length :: [A] -> Int) ]
 series :: Signature sig => [sig] -> Sig
-series = foldl op mempty . map toSig
+series = foldr op mempty . map signature
   where
-    op sigs sig = toSig [background sigs, sig]
+    op sig sigs = sig `mappend` later (signature sigs)
+    later sig =
+      Sig (\(Context n xs) cfg -> unSig sig (Context (n+1) xs) cfg)
 
 -- | Set the maximum size of terms to explore (default: 7).
 withMaxTermSize :: Int -> Sig
@@ -270,3 +352,51 @@
 -- Useful if you want repeatable results.
 withFixedSeed :: Int -> Sig
 withFixedSeed s = Sig (\_ -> setL (QuickCheck.lens_fixed_seed # Haskell.lens_quickCheck) (Just . mkQCGen $ s))
+
+-- | Automatically infer types to add to the universe from
+-- available type class instances
+withInferInstanceTypes :: Sig
+withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)
+
+-- | A signature containing boolean functions:
+-- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
+bools :: Sig
+bools = background [
+  "||"    `con` (||),
+  "&&"    `con` (&&),
+  "not"   `con` not,
+  "True"  `con` True,
+  "False" `con` False]
+
+-- | A signature containing arithmetic operations:
+-- @0@, @1@, @(`+`)@.
+-- Instantiate it with e.g. @arith (`Proxy` :: `Proxy` `Int`)@.
+arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig
+arith proxy = background [
+  monoType proxy,
+  "0" `con` (0   :: a),
+  "1" `con` (1   :: a),
+  "+" `con` ((+) :: a -> a -> a)]
+
+-- | A signature containing list operations:
+-- @[]@, @(:)@, @(`++`)@.
+lists :: Sig
+lists = background [
+  "[]"      `con` ([]      :: [A]),
+  ":"       `con` ((:)     :: A -> [A] -> [A]),
+  "++"      `con` ((++)    :: [A] -> [A] -> [A])]
+
+-- | A signature containing higher-order functions:
+-- @(`.`)@ and `id`.
+-- Useful for testing `map` and similar.
+funs :: Sig
+funs = background [
+  "."  `con` ((.) :: (A -> A) -> (A -> A) -> (A -> A)),
+  "id" `con` (id  :: A -> A) ]
+
+-- | The QuickSpec prelude.
+-- Contains boolean, arithmetic and list functions, and function composition.
+-- For more precise control over what gets included,
+-- see 'bools', 'arith', 'lists', 'funs' and 'without'.
+prelude :: Sig
+prelude = signature [bools, arith (Proxy :: Proxy Int), lists]
diff --git a/src/QuickSpec/Explore.hs b/src/QuickSpec/Explore.hs
--- a/src/QuickSpec/Explore.hs
+++ b/src/QuickSpec/Explore.hs
@@ -14,32 +14,56 @@
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.State.Strict
 import Text.Printf
+import Data.Semigroup(Semigroup(..))
 
-moreTerms :: (Ord a, Apply (Term f), Sized f, Typed f) => Universe -> [f] -> (Term f -> a) -> [[Term f]] -> [Term f]
-moreTerms univ funs measure tss =
-  sortBy' measure $
-    atomic ++
+newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }
+
+-- N.B. order matters!
+-- Later enumerators get to see terms which were generated by earlier ones.
+instance Semigroup (Enumerator a) where
+  e1 <> e2 = Enumerator $ \n tss ->
+    let us = enumerate e1 n tss
+        vs = enumerate e2 n (appendAt n us tss)
+    in us ++ vs
+instance Monoid (Enumerator a) where
+  mempty = Enumerator (\_ _ -> [])
+  mappend = (<>)
+
+mapEnumerator :: ([a] -> [a]) -> Enumerator a -> Enumerator a
+mapEnumerator f e =
+  Enumerator $ \n tss ->
+    f (enumerate e n tss)
+
+filterEnumerator :: (a -> Bool) -> Enumerator a -> Enumerator a
+filterEnumerator p e =
+  mapEnumerator (filter p) e
+
+enumerateConstants :: Sized a => [a] -> Enumerator a
+enumerateConstants ts = Enumerator (\n _ -> [t | t <- ts, size t == n])
+
+enumerateApplications :: Apply a => Enumerator a
+enumerateApplications = Enumerator $ \n tss ->
     [ unPoly v
     | i <- [0..n],
-      t <- uss !! i,
-      u <- uss !! (n-i),
-      Just v <- [tryApply (poly t) (poly u)],
-      unPoly v `usefulForUniverse` univ ]
-  where
-    n = length tss
-    atomic =
-      [App f [] | f <- funs, size f == n] ++
-      [Var (V typeVar 0) | n == 1]
-    uss = tss ++ [atomic]
+      t <- tss !! i,
+      u <- tss !! (n-i),
+      Just v <- [tryApply (poly t) (poly u)] ]
 
+filterUniverse :: Typed f => Universe -> Enumerator (Term f) -> Enumerator (Term f)
+filterUniverse univ e =
+  filterEnumerator (`usefulForUniverse` univ) e
+
+sortTerms :: Ord b => (a -> b) -> Enumerator a -> Enumerator a
+sortTerms measure e =
+  mapEnumerator (sortBy' measure) e
+
 quickSpec ::
-  (Ord measure, Ord fun, Ord norm, Sized fun, Typed fun, Ord result, Apply (Term fun), PrettyTerm fun,
-   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
+  (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, Apply (Term fun), PrettyTerm fun,
+  MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
   (Prop (Term fun) -> m ()) ->
-  (Term fun -> measure) ->
   (Term fun -> testcase -> result) ->
-  Int -> Universe -> [fun] -> m ()
-quickSpec present measure eval maxSize univ funs = do
+  Int -> Universe -> Enumerator (Term fun) -> m ()
+quickSpec present eval maxSize univ enum = do
   let
     state0 = initialState univ (\t -> size t <= 5) eval
 
@@ -47,7 +71,7 @@
     loop m n tss = do
       putStatus (printf "enumerating terms of size %d" m)
       let
-        ts = moreTerms univ funs measure tss
+        ts = enumerate (filterUniverse univ enum) m tss
         total = length ts
         consider (i, t) = do
           putStatus (printf "testing terms of size %d: %d/%d" m i total)
@@ -59,6 +83,17 @@
             Rejected _ -> return False
       us <- map snd <$> filterM consider (zip [1 :: Int ..] ts)
       clearStatus
-      loop (m+1) n (tss ++ [us])
+      loop (m+1) n (appendAt m us tss)
 
-  evalStateT (loop 0 maxSize []) state0
+  evalStateT (loop 0 maxSize (repeat [])) state0
+
+pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc
+pPrintSignature funs =
+  text "== Functions ==" $$
+  vcat (map pPrintDecl decls)
+  where
+    decls = [ (prettyShow f, pPrintType (typ f)) | f <- funs ]
+    maxWidth = maximum (0:map (length . fst) decls)
+    pad xs = nest (maxWidth - length xs) (text xs)
+    pPrintDecl (name, ty) =
+      pad name <+> text "::" <+> ty
diff --git a/src/QuickSpec/Explore/Conditionals.hs b/src/QuickSpec/Explore/Conditionals.hs
--- a/src/QuickSpec/Explore/Conditionals.hs
+++ b/src/QuickSpec/Explore/Conditionals.hs
@@ -43,11 +43,13 @@
       when res (considerConditionalising prop)
       return res
 
-conditionalsUniverse :: (Typed fun, Predicate fun) => [fun] -> Universe
-conditionalsUniverse funs =
+conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe
+conditionalsUniverse tys funs =
   universe $
-    map Normal funs ++
-    [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ]
+    tys ++
+    (map typ $
+      map Normal funs ++
+      [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])
 
 runConditionals ::
   (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
@@ -86,7 +88,7 @@
   arity (Normal f) = arity f
 
 instance Pretty fun => Pretty (WithConstructor fun) where
-  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <> text "_con"
+  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"
   pPrintPrec l p (Normal f) = pPrintPrec l p f
 
 instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where
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
@@ -1,6 +1,6 @@
 -- Pruning support for partial application and the like.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}
 module QuickSpec.Explore.PartialApplication where
 
 import QuickSpec.Term
@@ -17,7 +17,7 @@
     -- The ($) operator, for oversaturated applications.
     -- The type argument is the type of the first argument to ($).
   | Apply Type
-  deriving (Eq, Ord)
+  deriving (Eq, Ord, Functor)
 
 instance Sized f => Sized (PartiallyApplied f) where
   size (Partial f _) = size f
@@ -40,7 +40,7 @@
   prettyArity (Apply _) = 1
 
 instance Typed f => Typed (PartiallyApplied f) where
-  typ (Apply ty) = Twee.build (Twee.app (Twee.fun Arrow) [ty, ty])
+  typ (Apply ty) = arrowType [ty] ty
   typ (Partial f _) = typ f
   otherTypesDL (Apply _) = mempty
   otherTypesDL (Partial f _) = otherTypesDL f
@@ -61,6 +61,9 @@
 getTotal (Partial f n) | arity f == n = Just f
 getTotal _ = Nothing
 
+partial :: f -> Term (PartiallyApplied f)
+partial f = App (Partial f 0) []
+
 total :: Arity f => f -> PartiallyApplied f
 total f = Partial f (arity f)
 
@@ -81,9 +84,12 @@
       vs = map Var (zipWith V (typeArgs (typ f)) [0..])
   background _ = []
 
-instance (Applicative f, Eval fun (Value f)) => Eval (PartiallyApplied fun) (Value f) where
-  eval var (Partial f _) = eval var f
-  eval _ (Apply ty) =
-    fromJust $
-      cast (Twee.build (Twee.app (Twee.fun Arrow) [ty, ty]))
-        (toValue (pure (($) :: (A -> B) -> (A -> B))))
+evalPartiallyApplied ::
+  (Applicative f, Monad m) =>
+  (fun -> m (Value f)) ->
+  (PartiallyApplied fun -> m (Value f))
+evalPartiallyApplied eval (Partial f _) = eval f
+evalPartiallyApplied _ (Apply ty) =
+  return $ fromJust $
+    cast (Twee.build (Twee.app (Twee.fun Arrow) [ty, ty]))
+      (toValue (pure (($) :: (A -> B) -> (A -> B))))
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,7 +1,16 @@
 -- Theory exploration which handles polymorphism.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE TemplateHaskell, FlexibleContexts, GeneralizedNewtypeDeriving, FlexibleInstances, MultiParamTypeClasses, BangPatterns, UndecidableInstances, RankNTypes, GADTs, RecordWildCards #-}
-module QuickSpec.Explore.Polymorphic(module QuickSpec.Explore.Polymorphic, Result(..)) where
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RecordWildCards #-}
+module QuickSpec.Explore.Polymorphic(module QuickSpec.Explore.Polymorphic, Result(..), Universe(..)) where
 
 import qualified QuickSpec.Explore.Schemas as Schemas
 import QuickSpec.Explore.Schemas(Schemas, Result(..))
@@ -20,14 +29,11 @@
 import Control.Monad.Trans.Class
 import qualified Twee.Base as Twee
 import Control.Monad
-import Data.Maybe
 import qualified Data.DList as DList
 
 data Polymorphic testcase result fun norm =
   Polymorphic {
     pm_schemas :: Schemas testcase result (PolyFun fun) norm,
-    pm_unifiable :: Map (Poly Type) ([Poly Type], [(Poly Type, Poly Type)]),
-    pm_accepted :: Map (Poly Type) (Set (Term fun)),
     pm_universe :: Universe }
 
 data PolyFun fun =
@@ -40,15 +46,11 @@
 instance PrettyTerm fun => PrettyTerm (PolyFun fun) where
   termStyle = termStyle . fun_specialised
 
--- univ_inner: the type universe, with all type variables unified
--- univ_root: the set of types allowed for partially applied functions, only at
--- the root of a term
-data Universe = Universe { univ_inner :: Set Type, univ_root :: Set Type }
+-- The set of all types being explored
+data Universe = Universe { univ_types :: Set Type }
 
 makeLensAs ''Polymorphic
   [("pm_schemas", "schemas"),
-   ("pm_unifiable", "unifiable"),
-   ("pm_accepted", "accepted"),
    ("pm_universe", "univ")]
 
 initialState ::
@@ -59,8 +61,6 @@
 initialState univ inst eval =
   Polymorphic {
     pm_schemas = Schemas.initialState (inst . fmap fun_specialised) (eval . fmap fun_specialised),
-    pm_unifiable = Map.empty,
-    pm_accepted = Map.empty,
     pm_universe = univ }
 
 polyFun :: Typed fun => fun -> PolyFun fun
@@ -89,25 +89,13 @@
   if not (t `inUniverse` univ) then
     return (Accepted [])
    else do
-    let ty = polyTyp (poly t)
-    addPolyType ty
-
-    unif <- access unifiable
-    let (here, there) = Map.findWithDefault undefined ty unif
-    acc <- access accepted
-    ress1 <-
-      concat <$>
-      forM there (\(ty', mgu) ->
-        forM (Set.toList (Map.findWithDefault undefined ty' acc)) (\u ->
-          exploreNoMGU (u `at` mgu)))
     res <- exploreNoMGU t
-    ress2 <-
-      forM here (\mgu ->
-        exploreNoMGU (t `at` mgu))
-    return res { result_props = concatMap result_props (ress1 ++ [res] ++ ress2) }
-    where
-      t `at` ty =
-        fromMaybe undefined (cast (unPoly ty) t)
+    case res of
+      Rejected{} -> return res
+      Accepted{} -> do
+        ress <- forM (typeInstances univ t) $ \u ->
+          exploreNoMGU u
+        return res { result_props = concatMap result_props (res:ress) }
 
 exploreNoMGU ::
   (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),
@@ -116,11 +104,7 @@
   StateT (Polymorphic testcase result fun norm) m (Result fun)
 exploreNoMGU t = do
   univ <- access univ
-  let ty = polyTyp (poly t)
-  acc <- access accepted
-  if (t `Set.member` Map.findWithDefault Set.empty ty acc ||
-      not (t `inUniverse` univ)) then return (Rejected []) else do
-    accepted %= Map.insertWith Set.union ty (Set.singleton t)
+  if not (t `inUniverse` univ) then return (Rejected []) else do
     schemas1 <- access schemas
     (res, schemas2) <- unPolyM (runStateT (Schemas.explore (polyTerm t)) schemas1)
     schemas ~= schemas2
@@ -129,20 +113,6 @@
     mapProps f (Accepted props) = Accepted (map f props)
     mapProps f (Rejected props) = Rejected (map f props)
 
-addPolyType :: Monad m => Poly Type -> StateT (Polymorphic testcase result fun norm) m ()
-addPolyType ty = do
-  unif <- access unifiable
-  univ <- access univ
-  unless (ty `Map.member` unif) $ do
-    let
-      tys = [(ty', mgu) | ty' <- Map.keys unif, Just mgu <- [polyMgu ty ty']]
-      ok ty mgu = oneTypeVar ty /= mgu && oneTypeVar (unPoly mgu) `Set.member` univ_root univ
-      here = [mgu | (_, mgu) <- tys, ok mgu ty]
-      there = [(ty', mgu) | (ty', mgu) <- tys, ok mgu ty']
-    key ty # unifiable ~= Just (here, there)
-    forM_ there $ \(ty', _) ->
-      sndLens # keyDefault ty' undefined # unifiable %= (there ++)
-
 instance (PrettyTerm fun, Ord fun, Typed fun, Apply (Term fun), MonadPruner (Term fun) norm m) =>
   MonadPruner (Term (PolyFun fun)) norm (PolyM testcase result fun norm m) where
   normaliser = PolyM $ do
@@ -215,10 +185,8 @@
   where
     cs =
       foldr intersection [Map.empty]
-        (map (constrain (Set.toList univ_inner))
-          (usort (DList.toList (termsDL prop) >>= properSubterms)) ++
-         map (constrain (Set.toList univ_root))
-          (usort (DList.toList (termsDL prop))))
+        (map (constrain (Set.toList univ_types))
+          (usort (DList.toList (termsDL prop) >>= subterms)))
 
     constrain tys t =
       usort [ Map.fromList (Twee.substToList sub) | u <- tys, Just sub <- [Twee.match (typ t) u] ]
@@ -229,35 +197,19 @@
     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) (Set.fromList (withFunctions base))
+universe xs = Universe (Set.fromList base)
   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) >>= Twee.subterms
-
-    -- We then add partial applications, according to the rule:
-    -- if f : A1 -> ... -> An -> B is a function in the signature,
-    -- and s(A1)...s(An), s(B) are in the universe where s is a substitution,
-    -- then s(A1 -> ... -> An -> B) is in the universe, together with all subterms
-    withFunctions tys =
-      tys ++
-      concat [func Twee.emptySubst (typ f) tys >>= Twee.subterms | f <- xs]
-
-    func sub ty tys =
-      filter (`elem` tys) [oneTypeVar (typeSubst sub ty)] ++
-      [ arrowType [t'] u'
-      | Just (t, u) <- [unpackArrow ty],
-        t' <- tys,
-        Just sub <- [Twee.matchIn sub t t'],
-        u' <- func sub u tys ]
+    typs ty = typeRes ty:typeArgs ty
 
 inUniverse :: Typed fun => Term fun -> Universe -> Bool
 t `inUniverse` Universe{..} =
-  and [oneTypeVar (typ u) `Set.member` univ_inner | u <- subterms t]
+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- subterms t]
 
 usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool
 t `usefulForUniverse` Universe{..} =
-  oneTypeVar (typ t) `Set.member` univ_root &&
-  and [oneTypeVar (typ u) `Set.member` univ_inner | u <- properSubterms t]
+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- properSubterms t] &&
+  oneTypeVar (typeRes (typ t)) `Set.member` univ_types
diff --git a/src/QuickSpec/Haskell.hs b/src/QuickSpec/Haskell.hs
--- a/src/QuickSpec/Haskell.hs
+++ b/src/QuickSpec/Haskell.hs
@@ -2,38 +2,56 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, RecordWildCards, TemplateHaskell, UndecidableInstances, DefaultSignatures, FunctionalDependencies #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ConstraintKinds #-}
 module QuickSpec.Haskell where
 
 import QuickSpec.Haskell.Resolve
 import QuickSpec.Type
 import QuickSpec.Prop
+import QuickSpec.Pruning
 import Test.QuickCheck hiding (total)
-import Data.Constraint
+import Data.Constraint hiding ((\\))
+import Data.List
 import Data.Proxy
-import qualified Twee.Base as B
+import qualified Twee.Base as Twee
 import QuickSpec.Term
 import Data.Functor.Identity
 import Data.Maybe
 import Data.MemoUgly
-import Test.QuickCheck.Gen
-import Test.QuickCheck.Random
-import System.Random
+import Test.QuickCheck.Gen.Unsafe
 import Data.Char
 import Data.Ord
 import qualified QuickSpec.Testing.QuickCheck as QuickCheck
 import qualified QuickSpec.Pruning.Twee as Twee
+import QuickSpec.Explore hiding (quickSpec)
 import qualified QuickSpec.Explore
 import QuickSpec.Explore.PartialApplication
+import QuickSpec.Explore.Polymorphic(Universe(..))
 import QuickSpec.Pruning.Background(Background)
 import Control.Monad
 import Control.Monad.Trans.State.Strict
 import QuickSpec.Terminal
 import Text.Printf
-import Data.Reflection hiding (D)
 import QuickSpec.Utils
 import GHC.TypeLits
 import QuickSpec.Explore.Conditionals
+import Control.Spoon
+import qualified Data.Set as Set
+import qualified Test.QuickCheck.Poly as Poly
+import Numeric.Natural
+import Test.QuickCheck.Instances()
 
 baseInstances :: Instances
 baseInstances =
@@ -48,6 +66,7 @@
     inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) -> Dict :: Dict (ClassA, ClassB, ClassC),
     inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD),
     inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE),
+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) (Dict :: Dict ClassF) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE, ClassF),
     -- Derive typeclass instances using (:-)
     -- N.B. flip is there to resolve (:-) first to reduce backtracking
     inst $ flip $ \(Dict :: Dict ClassA) (Sub Dict :: ClassA :- ClassB) -> Dict :: Dict ClassB,
@@ -56,18 +75,27 @@
       Names (map (++ "s") names) :: Names [A],
     inst (Names ["p", "q", "r"] :: Names (A -> Bool)),
     inst (Names ["f", "g", "h"] :: Names (A -> B)),
+    inst (Names ["dict"] :: Names (Dict ClassA)),
     inst (Names ["x", "y", "z", "w"] :: Names A),
     -- Standard instances
     baseType (Proxy :: Proxy ()),
     baseType (Proxy :: Proxy Int),
     baseType (Proxy :: Proxy Integer),
+    baseType (Proxy :: Proxy Natural),
     baseType (Proxy :: Proxy Bool),
     baseType (Proxy :: Proxy Char),
+    baseType (Proxy :: Proxy Poly.OrdA),
+    baseType (Proxy :: Proxy Poly.OrdB),
+    baseType (Proxy :: Proxy Poly.OrdC),
     inst (Sub Dict :: () :- CoArbitrary ()),
     inst (Sub Dict :: () :- CoArbitrary Int),
     inst (Sub Dict :: () :- CoArbitrary Integer),
+    inst (Sub Dict :: () :- CoArbitrary Natural),
     inst (Sub Dict :: () :- CoArbitrary Bool),
     inst (Sub Dict :: () :- CoArbitrary Char),
+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdA),
+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdB),
+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdC),
     inst (Sub Dict :: Eq A :- Eq [A]),
     inst (Sub Dict :: Ord A :- Ord [A]),
     inst (Sub Dict :: Arbitrary A :- Arbitrary [A]),
@@ -97,15 +125,22 @@
     inst (Sub Dict :: Ord A :- Eq A),
     -- From Arbitrary to Gen
     inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,
-    inst $ \(dict :: Dict ClassA) -> return dict :: Gen (Dict ClassA),
-    -- Observe
-    inst (\(Dict :: Dict (Observe A B C)) -> Observe2 (do { env <- arbitrary; return (\x -> observe env (x :: C)) })),
-    inst (Sub Dict :: (Arbitrary A, Observe B C D) :- Observe (A, B) C (A -> D)),
-    inst (\(Dict :: Dict (Ord A)) -> Observe2 (return id) :: Observe2 A A),
-    inst (\(Observe2 obsm :: Observe2 B C) (xm :: Gen A) ->
-      Observe2 (do {x <- xm; obs <- obsm; return (\f -> obs (f x))}) :: Observe2 (A -> B) C),
-    inst (\(obs :: Observe2 A B) -> Observe1 (toValue obs))]
+    -- Observation functions
+    inst (\(Dict :: Dict (Observe A B C)) -> observeObs :: ObserveData C B),
+    inst (\(Dict :: Dict (Ord A)) -> observeOrd :: ObserveData A A),
+    inst (\(Dict :: Dict (Arbitrary A)) (obs :: ObserveData B C) -> observeFunction obs :: ObserveData (A -> B) C),
+    inst (\(obs :: ObserveData A B) -> WrappedObserveData (toValue obs)),
+    -- No warnings for TestCaseWrapped
+    inst (NoWarnings :: NoWarnings (TestCaseWrapped SymA A)),
+    -- Needed for typeclass-polymorphic predicates to work currently
+    inst (\(Dict :: Dict ClassA) -> Dict :: Dict (Arbitrary (Dict ClassA)))]
 
+-- A token used in the instance list for types that shouldn't generate warnings
+data NoWarnings a = NoWarnings
+
+instance c => Arbitrary (Dict c) where
+  arbitrary = return Dict
+
 -- | A typeclass for types which support observational equality, typically used
 -- for types that have no `Ord` instance.
 --
@@ -114,11 +149,11 @@
 -- @observe :: test -> outcome -> a@. Then, two values @x@ and @y@ are considered
 -- equal, if for many random values of type @test@, @observe test x == observe test y@.
 --
--- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.
+-- The function `QuickSpec.monoTypeObserve` declares a monomorphic
+-- type with an observation function. For polymorphic types, use
+-- `QuickSpec.inst` to declare the `Observe` instance.
 --
--- You must use `QuickSpec.inst` to add the @Observe@ instance to your signature.
--- Note that `QuickSpec.monoType` requires an `Ord` instance, so this even applies for
--- monomorphic types. Don't forget to add the `Arbitrary` instance too in that case.
+-- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.
 class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where
   -- | Make an observation on a value. Should satisfy the following law: if
   -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@.
@@ -130,106 +165,118 @@
 instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where
   observe (x, obs) f = observe obs (f x)
 
-data Observe2 a b where
-  Observe2 :: Ord b => Gen (a -> b) -> Observe2 a b
-  deriving Typeable
-data Observe1 a = Observe1 (Value (Observe2 a)) deriving Typeable
+-- An observation function along with instances.
+-- The parameters are in this order so that we can use findInstance to get at appropriate Wrappers.
+data ObserveData a outcome where
+  ObserveData :: (Arbitrary test, Ord outcome) => (test -> a -> outcome) -> ObserveData a outcome
+newtype WrappedObserveData a = WrappedObserveData (Value (ObserveData a))
 
--- | Declare that values of a particular type should be compared by observational equality.
---
--- See @examples/PrettyPrinting.hs@ for an example.
---
--- XXX mention what instances must be in scope
--- XXX remove constraints etc
--- observe :: Ord res => Gen env -> (env -> val -> res) -> Observe val res
--- observe gen f =
---   Observe (do { env <- gen; return (\x -> f env x) })
-  
+observeOrd :: Ord a => ObserveData a a
+observeOrd = ObserveData (\() x -> x)
 
--- data SomeObserve a = forall args res. (Ord res, Arbitrary args) => SomeObserve (a -> args -> res) deriving Typeable
+observeFunction :: Arbitrary a => ObserveData b outcome -> ObserveData (a -> b) outcome
+observeFunction (ObserveData obs) =
+  ObserveData (\(x, test) f -> obs test (f x))
 
+observeObs :: Observe test outcome a => ObserveData a outcome
+observeObs = ObserveData observe
+
 baseType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Instances
 baseType _ =
   mconcat [
     inst (Dict :: Dict (Ord a)),
     inst (Dict :: Dict (Arbitrary a))]
 
--- | Declare what variable names you would like to use for values of a particular type. See also `baseTypeNames`.
+-- Declares what variable names should be used for values of a particular type.
 newtype Names a = Names { getNames :: [String] }
 
 names :: Instances -> Type -> [String]
 names insts ty =
   case findInstance insts (skolemiseTypeVars ty) of
-    (x:_) -> ofValue getNames x
-    [] -> error "don't know how to name variables"
-
-arbitraryVal :: Type -> Instances -> Gen (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy))
-arbitraryVal def insts =
-  MkGen $ \g n ->
-    let (g1, g2) = split g in
-    (memo $ \(V ty x) ->
-       case genType ty of
-         Nothing ->
-           fromJust $ cast (defaultTo def ty) (toValue (Nothing :: Maybe A))
-         Just gen ->
-           forValue gen $ \gen ->
-             Just (unGen (coarbitrary x gen) g1 n),
-     ordyVal g2 n)
-  where
-    genType :: Type -> Maybe (Value Gen)
-    genType = memo $ \ty ->
-      case findInstance insts (defaultTo def ty) of
-        [] -> Nothing
-        (gen:_) ->
-          Just (mapValue (coarbitrary ty) gen)
-
-    ordyVal :: QCGen -> Int -> Value Identity -> Maybe (Value Ordy)
-    ordyVal g n x =
-      let ty = defaultTo def (typ x) in
-      case ordyTy ty of
-        Nothing -> Nothing
-        Just f -> Just (unGen f g n x)
-
-    ordyTy :: Type -> Maybe (Gen (Value Identity -> Value Ordy))
-    ordyTy = memo $ \ty ->
-      case findInstance insts ty :: [Value Observe1] of
-        [] -> Nothing
-        (val:_) ->
-          case unwrap val of
-            Observe1 val `In` w1 ->
-              case unwrap val of
-                Observe2 obs `In` w2 ->
-                  Just $
-                    MkGen $ \g n ->
-                      let observe = unGen obs g n in
-                      \x -> wrap w2 (Ordy (observe (runIdentity (reunwrap w1 x))))
+    Just x  -> ofValue getNames x
+    Nothing -> error "don't know how to name variables"
 
+-- An Ordy a represents a value of type a together with its Ord instance.
+-- A Value Ordy is a value of unknown type which implements Ord.
 data Ordy a where Ordy :: Ord a => a -> Ordy a
 instance Eq (Value Ordy) where x == y = compare x y == EQ
 
 instance Ord (Value Ordy) where
   compare x y =
-    compare (typ x) (typ y) `mappend`
     case unwrap x of
       Ordy xv `In` w ->
         let Ordy yv = reunwrap w y in
         compare xv yv
 
-evalHaskell :: (Given Type, Typed f, PrettyTerm f, Eval f (Value Maybe)) => (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy)) -> Term f -> Either (Value Ordy) (Term f)
-evalHaskell (env, obs) t =
-  case unwrap (eval env t) of
-    Nothing `In` _ -> Right t
-    Just val `In` w ->
-      case obs (wrap w (Identity val)) of
-        Nothing -> Right t
-        Just ordy -> Left ordy
+-- | A test case is everything you need to evaluate a Haskell term.
+data TestCase =
+  TestCase {
+    -- | Evaluate a variable. Returns @Nothing@ if no `Arbitrary` instance was found.
+    tc_eval_var :: Var -> Maybe (Value Identity),
+    -- | Apply an observation function to get a value implementing `Ord`.
+    -- Returns @Nothing@ if no observer was found.
+    tc_test_result :: Value Identity -> Maybe (Value Ordy) }
 
+-- | Generate a random test case.
+arbitraryTestCase :: Type -> Instances -> Gen TestCase
+arbitraryTestCase def insts =
+  TestCase <$> arbitraryValuation def insts <*> arbitraryObserver def insts
+
+-- | Generate a random variable valuation.
+arbitraryValuation :: Type -> Instances -> Gen (Var -> Maybe (Value Identity))
+arbitraryValuation def insts = do
+  memo <$> arbitraryFunction (sequence . findGenerator def insts . var_ty)
+
+-- | Generate a random observation.
+arbitraryObserver :: Type -> Instances -> Gen (Value Identity -> Maybe (Value Ordy))
+arbitraryObserver def insts = do
+  find <- arbitraryFunction $ sequence . findObserver insts
+  return $ \x -> do
+    obs <- find (defaultTo def (typ x))
+    return (obs x)
+
+findGenerator :: Type -> Instances -> Type -> Maybe (Gen (Value Identity))
+findGenerator def insts ty =
+  bringFunctor <$> (findInstance insts (defaultTo def ty) :: Maybe (Value Gen))
+
+findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy))
+findObserver insts ty = do
+  inst <- findInstance insts ty :: Maybe (Value WrappedObserveData)
+  return $
+    case unwrap inst of
+      WrappedObserveData val `In` valueWrapper ->
+        case unwrap val of
+          -- This brings Arbitrary and Ord instances into scope
+          ObserveData obs `In` outcomeWrapper -> do
+            test <- arbitrary
+            return $ \x ->
+              let value = runIdentity (reunwrap valueWrapper x)
+                  outcome = obs test value
+              in wrap outcomeWrapper (Ordy outcome)
+
+-- | Generate a random function. Should be in QuickCheck.
+arbitraryFunction :: CoArbitrary a => (a -> Gen b) -> Gen (a -> b)
+arbitraryFunction gen = promote (\x -> coarbitrary x (gen x))
+
+-- | Evaluate a Haskell term in an environment.
+evalHaskell :: Type -> Instances -> TestCase -> Term (PartiallyApplied Constant) -> Either (Value Ordy) (Term (PartiallyApplied Constant))
+evalHaskell def insts (TestCase env obs) t =
+  maybe (Right t) Left $ do
+    let eval env t = evalTerm env (evalPartiallyApplied (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 {
     con_name  :: String,
     con_style :: TermStyle,
     con_pretty_arity :: Int,
     con_value :: Value Identity,
+    con_type :: Type,
+    con_constraints :: [Type],
     con_size :: Int,
     con_classify :: Classification Constant }
 
@@ -271,8 +318,12 @@
           | isOp name -> 1
           | otherwise -> typeArity (typ val),
     con_value = val,
+    con_type = ty,
+    con_constraints = constraints,
     con_size = 1,
     con_classify = Function }
+  where
+    (constraints, ty) = splitConstrainedType (typ val)
 
 isOp :: String -> Bool
 isOp "[]" = False
@@ -282,9 +333,24 @@
   where
     isIdent x = isAlphaNum x || x == '\'' || x == '_' || x == '.'
 
+-- Get selectors of a predicate
+selectors :: Constant -> [Constant]
+selectors con =
+  case con_classify con of
+    Predicate{..} -> clas_selectors
+    _ -> []
+
+-- Move the constraints of a constant back into the main type
+unhideConstraint :: Constant -> Constant
+unhideConstraint con =
+  con {
+    con_type = typ (con_value con),
+    con_constraints = [] }
+
 instance Typed Constant where
-  typ = typ . con_value
+  typ = con_type
   otherTypesDL con =
+    return (typ (con_value con)) `mplus`
     case con_classify con of
       Predicate{..} ->
         -- Don't call typesDL on clas_selectors because it in turn
@@ -295,6 +361,8 @@
       Function -> mzero
   typeSubst_ sub con =
     con { con_value = typeSubst_ sub (con_value con),
+          con_type = typeSubst_ sub (con_type con),
+          con_constraints = map (typeSubst_ sub) (con_constraints con),
           con_classify = fmap (typeSubst_ sub) (con_classify con) }
 
 instance Pretty Constant where
@@ -315,39 +383,35 @@
 instance Predicate Constant where
   classify = con_classify
 
-instance (Given Type, Applicative f) => Eval Constant (Value f) where
-  eval _ = mapValue (pure . runIdentity) . con_value
+evalConstant :: Instances -> Constant -> Maybe (Value Identity)
+evalConstant insts Constant{..} = foldM app con_value con_constraints
+  where
+    app val constraint = do
+      dict <- findValue insts constraint
+      return (apply val dict)
 
 class Predicateable a where
-  uncrry :: a -> TestCase a -> Bool
+  -- A test case for predicates of type a
+  -- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))`
+  --
+  -- Some speedup should be possible by using unboxed tuples instead...
+  type PredicateTestCase a
+  uncrry :: a -> PredicateTestCase a -> Bool
 
 instance Predicateable Bool where
+  type PredicateTestCase Bool = ()
   uncrry = const
 
-instance forall a b. (Predicateable b, Typeable a, TestCase (a -> b) ~ (a, TestCase b)) => Predicateable (a -> b) where
+instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where
+  type PredicateTestCase (a -> b) = (a, PredicateTestCase b)
   uncrry f (a, b) = uncrry (f a) b
 
--- Foldr over functions
-type family (Foldr f b fun) :: * where
-  Foldr f def (a -> b) = f a (Foldr f def b)
-  Foldr f def b        = def
-
--- A test case for predicates of type a
--- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))`
---
--- Some speedup should be possible by using unboxed tuples instead...
-type TestCase a = Foldr (,) () a
-
 data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }
 
 -- A `suchThat` generator for a predicate
-genSuchThat :: (Predicateable a, Arbitrary (TestCase a)) => a -> Gen (TestCaseWrapped x (TestCase a))
+genSuchThat :: (Predicateable a, Arbitrary (PredicateTestCase a)) => a -> Gen (TestCaseWrapped x (PredicateTestCase a))
 genSuchThat p = TestCaseWrapped <$> arbitrary `suchThat` uncrry p
 
-data PredRep = PredRep { predInstances :: Instances
-                       , predCon :: Constant
-                       , predCons :: [Constant] }
-
 true :: Constant
 true = con "True" True
 
@@ -358,44 +422,65 @@
 -- The predicate should have type @... -> Bool@.
 predicate :: forall a. ( Predicateable a
              , Typeable a
-             , Typeable (TestCase a))
-             => String -> a -> PredRep
+             , Typeable (PredicateTestCase a))
+             => String -> a -> (Instances, Constant)
 predicate name pred =
-  case someSymbolVal name of
-    SomeSymbol (_ :: Proxy sym) ->
-      let
-        instances =
-          inst (\(dict :: Dict (Arbitrary (TestCase a))) -> (withDict dict genSuchThat) pred :: Gen (TestCaseWrapped sym (TestCase a)))
-          `mappend`
-          inst (Names [name ++ "_var"] :: Names (TestCaseWrapped sym (TestCase a)))
+  let
+    -- The following doesn't compile on GHC 7.10:
+    -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))
+    -- (where sym was created using someSymbolVal)
+    -- So do it by hand instead:
+    ty = addName (typeRep (Proxy :: Proxy (TestCaseWrapped SymA (PredicateTestCase a))))
 
-        conPred = (con name pred) { con_classify = Predicate conSels ty (App true []) }
-        conSels = [ (constant' (name ++ "_" ++ show i) (select i)) { con_classify = Selector i conPred ty, con_size = 0 } | i <- [0..typeArity (typeOf pred)-1] ]
+    -- Replaces SymA with 'String name'
+    -- (XXX: not correct if the type 'a' also contains SymA)
+    addName :: forall a. Typed a => a -> a
+    addName = typeSubst sub
+      where
+        sub x
+          | Twee.build (Twee.var x) == typeRep (Proxy :: Proxy SymA) =
+            Twee.builder (typeFromTyCon (String name))
+          | otherwise = Twee.var x
 
-        select i =
-          fromJust (cast (arrowType [ty] (typeArgs (typeOf pred) !! i)) (unPoly (compose (sel i) unwrapV)))
-          where
-            compose f g = apply (apply cmpV f) g
-            sel 0 = fstV
-            sel n = compose (sel (n-1)) sndV
-            fstV = toPolyValue (fst :: (A, B) -> A)
-            sndV = toPolyValue (snd :: (A, B) -> B)
-            cmpV = toPolyValue ((.) :: (B -> C) -> (A -> B) -> A -> C)
-            unwrapV = toPolyValue (unTestCaseWrapped :: TestCaseWrapped SymA A -> A)
+    instances =
+      mconcat $ map (valueInst . addName)
+        [toValue (Identity inst1), toValue (Identity inst2)]
 
-        ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (TestCase a)))
-      in
-        PredRep instances conPred (conPred:conSels)
+    inst1 :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
+    inst1 Dict = genSuchThat pred
 
+    inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))
+    inst2 = Names [name ++ "_var"]
+
+    conPred = (con name pred) { con_classify = Predicate conSels ty (App true []) }
+    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 =
+      fromJust (cast (arrowType [ty] (typeArgs (typeOf pred) !! i)) (unPoly (compose (sel i) unwrapV)))
+      where
+        compose f g = apply (apply cmpV f) g
+        sel 0 = fstV
+        sel n = compose (sel (n-1)) sndV
+        fstV = toPolyValue (fst :: (A, B) -> A)
+        sndV = toPolyValue (snd :: (A, B) -> B)
+        cmpV = toPolyValue ((.) :: (B -> C) -> (A -> B) -> A -> C)
+        unwrapV = toPolyValue (unTestCaseWrapped :: TestCaseWrapped SymA A -> A)
+  in
+    (instances, conPred)
+
 data Config =
   Config {
     cfg_quickCheck :: QuickCheck.Config,
     cfg_twee :: Twee.Config,
     cfg_max_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_predicates :: [[PredRep]],
-    cfg_default_to :: Type }
+    cfg_default_to :: Type,
+    cfg_infer_instance_types :: Bool
+    }
 
 makeLensAs ''Config
   [("cfg_quickCheck", "lens_quickCheck"),
@@ -403,68 +488,178 @@
    ("cfg_max_size", "lens_max_size"),
    ("cfg_instances", "lens_instances"),
    ("cfg_constants", "lens_constants"),
-   ("cfg_predicates", "lens_predicates"),
-   ("cfg_default_to", "lens_default_to")]
+   ("cfg_default_to", "lens_default_to"),
+   ("cfg_infer_instance_types", "lens_infer_instance_types")]
 
 defaultConfig :: Config
 defaultConfig =
   Config {
-    cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 20, QuickCheck.cfg_fixed_seed = Nothing },
+    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_instances = mempty,
     cfg_constants = [],
-    cfg_predicates = [],
-    cfg_default_to = typeRep (Proxy :: Proxy Int) }
+    cfg_default_to = typeRep (Proxy :: Proxy Int),
+    cfg_infer_instance_types = False }
 
-quickSpec :: Config -> IO ()
-quickSpec Config{..} = give cfg_default_to $ do
+-- Extra types for the universe that come from in-scope instances.
+instanceTypes :: Instances -> Config -> [Type]
+instanceTypes insts Config{..}
+  | not cfg_infer_instance_types = []
+  | otherwise =
+    [ tv
+    | cls <- dicts,
+      inst <- groundInstances,
+      sub <- maybeToList (matchType cls inst),
+      (_, tv) <- Twee.substToList sub ]
+  where
+    dicts =
+      concatMap con_constraints (concat cfg_constants) >>=
+      maybeToList . getDictionary
+
+    groundInstances :: [Type]
+    groundInstances =
+      [ dict
+      | -- () :- dict
+        Twee.App tc (Twee.Cons (Twee.App unit Twee.Empty) (Twee.Cons dict Twee.Empty)) <-
+        map (typeRes . typ) (is_instances insts),
+        Twee.fun_value tc == tyCon (Proxy :: Proxy (:-)),
+        Twee.fun_value unit == tyCon (Proxy :: Proxy (() :: Constraint)),
+        Twee.isGround dict ]
+
+data Warnings =
+  Warnings {
+    warn_no_generator :: [Type],
+    warn_no_observer :: [Type] }
+
+warnings :: Universe -> Instances -> Config -> Warnings
+warnings univ insts Config{..} =
+  Warnings {
+    warn_no_generator =
+      [ ty | ty <- types, isNothing (findGenerator cfg_default_to insts ty) ],
+    warn_no_observer =
+      [ ty | ty <- types, isNothing (findObserver insts ty) ] }
+  where
+    -- Check after defaulting types to Int (or whatever it is)
+    types =
+      [ ty
+      | ty <- defaultTo cfg_default_to . Set.toList . univ_types $ univ,
+        isNothing (findInstance insts ty :: Maybe (Value NoWarnings)) ]
+
+instance Pretty Warnings where
+  pPrint Warnings{..} =
+    vcat $
+      [section genDoc warn_no_generator] ++
+      [section obsDoc warn_no_observer] ++
+      [text "" | warnings ]
+    where
+      warnings = not (null warn_no_generator) || not (null warn_no_observer)
+      section _ [] = pPrintEmpty
+      section doc xs =
+        doc $$
+        nest 2 (vcat (map pPrintType xs)) $$
+        text ""
+
+      genDoc =
+        text "WARNING: The following types have no 'Arbitrary' instance declared." $$
+        text "You will not get any variables of the following types:"
+
+      obsDoc =
+        text "WARNING: The following types have no 'Ord' or 'Observe' instance declared." $$
+        text "You will not get any equations about the following types:"
+
+quickSpec :: Config -> IO [Prop (Term (PartiallyApplied Constant))]
+quickSpec cfg@Config{..} = do
   let
-    constantsOf f = true:f cfg_constants ++ f (map (concatMap predCons) cfg_predicates)
+    constantsOf f = true:f cfg_constants ++ concatMap selectors (f cfg_constants)
     constants = constantsOf concat
-    univ = conditionalsUniverse constants
-    instances = mconcat (cfg_instances:map predInstances (concat cfg_predicates) ++ [baseInstances])
+    
+    univ = conditionalsUniverse (instanceTypes instances cfg) constants
+    instances = cfg_instances `mappend` baseInstances
 
-    present prop = do
-      n :: Int <- get
-      put (n+1)
-      putLine (printf "%3d. %s" n (show (prettyProp (names instances) (conditionalise prop) <+> maybeType prop)))
+    eval = evalHaskell cfg_default_to instances
 
+    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
+
+    -- Put an equation that defines the function f into the form f lhs = rhs.
+    -- An equation defines f if:
+    --   * it is of the form f lhs = rhs (or vice versa).
+    --   * f is not a background function.
+    --   * lhs only contains background functions.
+    --   * rhs does not contain f.
+    --   * all vars in rhs appear in lhs
+    makeDefinition cons (lhs :=>: t :=: u)
+      | Just (f, ts) <- defines u,
+        f `notElem` mapMaybe getTotal (funs t),
+        null (usort (vars t) \\ vars ts) =
+        lhs :=>: u :=: t
+        -- In the case where t defines f, the equation is already oriented correctly
+      | otherwise = lhs :=>: t :=: u
+      where
+        defines (App (Partial f _) ts)
+          | f `elem` cons,
+            all (`notElem` cons) (mapMaybe getTotal (funs ts)) = Just (f, ts)
+        defines _ = Nothing
+
+    -- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative
+    ac norm (lhs :=>: App f [Var x, App f1 [Var y, Var z]] :=: App f2 [Var y1, App f3 [Var x1, Var z1]])
+      | f == f1, f1 == f2, f2 == f3,
+        x == x1, y == y1, z == z1,
+        x /= y, y /= z, x /= z,
+        norm (App f [Var x, Var y]) == norm (App f [Var y, Var x]) =
+          lhs :=>: App f [App f [Var x, Var y], Var z] :=: App f [Var x, App f [Var y, Var z]]
+    ac _ prop = prop
+
     -- Add a type signature when printing the equation x = y.
     maybeType (_ :=>: x@(Var _) :=: Var _) =
       text "::" <+> pPrintType (typ x)
     maybeType _ = pPrintEmpty
 
-    mainOf f g = do
-      printConstants (f cfg_constants ++ f (map (map predCon) cfg_predicates))
-      putLine ""
-      putLine "== Laws =="
-      QuickSpec.Explore.quickSpec present measure (flip evalHaskell) cfg_max_size univ
-        [ Partial fun 0 | fun <- constantsOf g ]
-      putLine ""
+    -- XXX do this during testing
+    constraintsOk (Partial f _) = constraintsOk1 f
+    constraintsOk (Apply _) = True
+    constraintsOk1 = memo $ \con ->
+      or [ and [ isJust (findValue instances (defaultTo cfg_default_to constraint)) | constraint <- con_constraints (typeSubst sub con) ]
+         | ty <- Set.toList (univ_types univ),
+           sub <- maybeToList (matchType (typeRes (typ con)) ty) ]
 
-    main = mapM_ round [1..rounds]
+    enumerator cons =
+      sortTerms measure $
+      filterEnumerator (all constraintsOk . funs) $
+      enumerateConstants atomic `mappend` enumerateApplications
       where
-        round n = mainOf (concat . take 1 . drop (rounds-n)) (concat . drop (rounds-n))
-        rounds = max (length cfg_constants) (length cfg_predicates)
+        atomic = cons ++ [Var (V typeVar 0)]
 
+    mainOf n f g = do
+      unless (null (f cfg_constants)) $ do
+        putLine $ show $ pPrintSignature
+          (map (partial . unhideConstraint) (f cfg_constants))
+        putLine ""
+      when (n > 0) $ do
+        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
+        (enumerator [partial fun | fun <- constantsOf g])
+      when (n > 0) $ do
+        putLine ""
+
+    main = mapM_ round [0..rounds-1]
+      where
+        round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))
+        rounds = length cfg_constants
+
   join $
     fmap withStdioTerminal $
     generate $
-    QuickCheck.run cfg_quickCheck (arbitraryVal cfg_default_to instances) evalHaskell $
+    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 (map total constants) $
-    flip evalStateT 1 $
-      main
-
-printConstants :: MonadTerminal m => [Constant] -> m ()
-printConstants cs = do
-  putLine "== Functions =="
-  let
-    decls = [ (show (pPrint (App (Partial c 0) [])), pPrintType (typ c)) | c <- cs ]
-    maxWidth = maximum (0:map (length . fst) decls)
-    pad xs = replicate (maxWidth - length xs) ' ' ++ xs
-    pPrintDecl (name, ty) =
-      hang (text (pad name) <+> text "::") 2 ty
-
-  mapM_ (putLine . show . pPrintDecl) decls
+    fmap (reverse . snd) $ flip execStateT (1, []) main
diff --git a/src/QuickSpec/Haskell/Resolve.hs b/src/QuickSpec/Haskell/Resolve.hs
--- a/src/QuickSpec/Haskell/Resolve.hs
+++ b/src/QuickSpec/Haskell/Resolve.hs
@@ -14,7 +14,7 @@
 
 {-# OPTIONS_HADDOCK hide #-}
 {-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
-module QuickSpec.Haskell.Resolve(Instances, inst, findInstance, findValue) where
+module QuickSpec.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where
 
 import Twee.Base
 import QuickSpec.Type
@@ -23,6 +23,7 @@
 import Data.Maybe
 import Data.Proxy
 import Control.Monad
+import Data.Semigroup(Semigroup(..))
 
 -- A set of instances.
 data Instances =
@@ -39,22 +40,27 @@
   where
     inst = Instances is (memo (find_ inst . canonicaliseType))
 
+instance Semigroup Instances where
+  x <> y = makeInstances (is_instances x ++ is_instances y)
 instance Monoid Instances where
   mempty = makeInstances []
-  x `mappend` y = makeInstances (is_instances x ++ is_instances y)
+  mappend = (<>)
 
 -- Create a single instance.
 inst :: Typeable a => a -> Instances
-inst x = instValue (toPolyValue x)
+inst x = valueInst (toValue (Identity x))
+
+valueInst :: Value Identity -> Instances
+valueInst x = polyInst (poly x)
   where
-    instValue :: Poly (Value Identity) -> Instances
-    instValue x =
+    polyInst :: Poly (Value Identity) -> Instances
+    polyInst x =
       -- Transform x into a single-argument function
       -- (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)) ->
-          instValue (apply uncur x)
+          polyInst (apply uncur x)
         App (F Arrow) _ ->
           makeInstances [x]
         -- A plain old value x (not a function) turns into \() -> x.
@@ -66,14 +72,14 @@
 
 -- Construct a value of a particular type.
 -- If the type is polymorphic, may return an instance of it.
-findValue :: Instances -> Type -> [Value Identity]
-findValue = is_find
+findValue :: Instances -> Type -> Maybe (Value Identity)
+findValue insts = listToMaybe . is_find insts . skolemiseTypeVars
 
 -- Given a type a, construct a value of type f a.
 -- If the type is polymorphic, may return an instance of it.
-findInstance :: forall f. Typeable f => Instances -> Type -> [Value f]
+findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f)
 findInstance insts ty =
-  map (unwrapFunctor runIdentity) (findValue insts ty')
+  unwrapFunctor runIdentity <$> findValue insts ty'
   where
     ty' = typeRep (Proxy :: Proxy f) `applyType` ty
 
@@ -89,12 +95,12 @@
 find_ _ (App (F unit) Empty)
   | unit == tyCon (Proxy :: Proxy ()) =
     return (toValue (Identity ()))
-find_ res (App (F pair) (Cons ty1 (Cons ty2 Empty)))
+find_ insts (App (F pair) (Cons ty1 (Cons ty2 Empty)))
   | pair == tyCon (Proxy :: Proxy (,)) = do
-    x <- findValue res ty1
+    x <- is_find insts ty1
     sub <- maybeToList (match ty1 (typ x))
     -- N.B.: subst sub ty2 because searching for x may have constrained y's type
-    y <- findValue res (subst sub ty2)
+    y <- is_find insts (subst sub ty2)
     sub <- maybeToList (match ty2 (typ y))
     return (pairValues (liftM2 (,)) (typeSubst sub x) y)
 find_ insts ty = do
@@ -106,6 +112,6 @@
   fun <- return (typeSubst sub fun)
   arg <- return (typeSubst sub arg)
   -- Find an argument for that function and apply the function.
-  val <- findValue insts arg
+  val <- is_find insts arg
   sub <- maybeToList (match arg (typ val))
   return (apply (typeSubst sub fun) val)
diff --git a/src/QuickSpec/Parse.hs b/src/QuickSpec/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/QuickSpec/Parse.hs
@@ -0,0 +1,60 @@
+-- | Parsing strings into properties.
+{-# OPTIONS_HADDOCK hide #-}
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+module QuickSpec.Parse where
+
+import Control.Monad
+import Data.Char
+import QuickSpec.Prop
+import QuickSpec.Term hiding (char)
+import QuickSpec.Type
+import qualified Twee.Label as Label
+import Text.ParserCombinators.ReadP
+
+class Parse fun a where
+  parse :: ReadP fun -> ReadP a
+
+instance Parse fun Var where
+  parse _ = do
+    x <- satisfy isUpper
+    xs <- munch isAlphaNum
+    let name = x:xs
+    -- Use Twee.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
+  parse pfun =
+    parseApp <++ parseVar
+    where
+      parseVar = Var <$> parse pfun
+      parseApp = do
+        f <- pfun
+        args <- parseArgs <++ return []
+        return (unPoly (foldl apply (poly (App f [])) (map poly args)))
+      parseArgs = between (char '(') (char ')') (sepBy (parse pfun) (char ','))
+
+instance (Parse fun a, Typed a) => Parse fun (Equation a) where
+  parse pfun = do
+    t <- parse pfun
+    string "="
+    u <- parse pfun
+    -- Compute type unifier of t and u
+    -- "maybe mzero return" injects Maybe into MonadPlus
+    pt <- maybe mzero return (polyMgu (poly (typ t)) (poly (typ u)))
+    t <- maybe mzero return (cast (unPoly pt) t)
+    u <- maybe mzero return (cast (unPoly pt) u)
+    return (t :=: u)
+
+instance (Parse fun a, Typed a) => Parse fun (Prop a) where
+  parse pfun = do
+    lhs <- sepBy (parse pfun) (string "&")
+    unless (null lhs) (void (string "=>"))
+    rhs <- parse pfun
+    return (lhs :=>: rhs)
+
+parseProp :: (Parse fun a, Pretty a) => ReadP fun -> String -> a
+parseProp pfun xs =
+  case readP_to_S (parse pfun <* eof) (filter (not . isSpace) xs) of
+    [(x, [])] -> x
+    ps -> error ("parse': got result " ++ prettyShow ps ++ " while parsing " ++ xs)
diff --git a/src/QuickSpec/Prop.hs b/src/QuickSpec/Prop.hs
--- a/src/QuickSpec/Prop.hs
+++ b/src/QuickSpec/Prop.hs
@@ -72,7 +72,8 @@
     | isTrue y = pPrint x
     | otherwise = pPrint x <+> text "=" <+> pPrint y
     where
-      isTrue x = show (pPrint x) `elem` ["true", "True"]
+      -- XXX this is a hack
+      isTrue x = show (pPrint x) == "True"
 
 infix 4 ===
 (===) :: a -> a -> Prop a
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
@@ -21,6 +21,6 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift . lift
 
-run :: Monad m => Config -> Pruner fun m a -> m a
+run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a
 run config (Pruner x) =
   Untyped.run config (Types.run (Background.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
@@ -13,6 +13,7 @@
 import QuickSpec.Terminal
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
+import qualified Twee.Base as Twee
 
 data Tagged fun =
     Func fun
@@ -27,9 +28,12 @@
   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 "]"
+  pPrint (Tag ty) = text "tag[" <#> pPrint ty <#> text "]"
 
 instance PrettyTerm fun => PrettyTerm (Tagged fun) where
   termStyle (Func f) = termStyle f
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
@@ -34,27 +34,37 @@
   [("cfg_max_term_size", "lens_max_term_size"),
    ("cfg_max_cp_depth", "lens_max_cp_depth")]
 
-instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
+instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Twee.Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
   lessEq = KBO.lessEq
   lessIn = KBO.lessIn
 
 newtype Pruner fun m a =
-  Pruner (ReaderT Twee.Config (StateT (State (Extended fun)) m) a)
+  Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)
   deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)
 
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift
 
-run :: Monad m => Config -> Pruner fun m a -> m a
+run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a
 run Config{..} (Pruner x) =
   evalStateT (runReaderT x config) initialState
   where
     config =
       defaultConfig {
-        Twee.cfg_max_term_size = cfg_max_term_size,
+        Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),
         Twee.cfg_max_cp_depth = cfg_max_cp_depth }
 
-instance (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>
+instance 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 (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>
   MonadPruner (Term fun) (Term fun) (Pruner fun m) where
   normaliser = Pruner $ do
     state <- lift get
@@ -77,20 +87,20 @@
   add _ =
     error "twee pruner doesn't support non-unit equalities"
 
-normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>
+normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
   State (Extended fun) -> Term fun -> Term fun
 normaliseTwee state t =
   fromTwee $
     result (normaliseTerm state (simplifyTerm state (skolemise t)))
 
-normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>
+normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
   State (Extended fun) -> Term fun -> Set (Term fun)
 normalFormsTwee state t =
   Set.map fromTwee $
     Set.map result (normalForms state (skolemise t))
 
-addTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>
-  Twee.Config -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)
+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)
 addTwee config t u state =
   completePure config $
     addAxiom config state axiom
diff --git a/src/QuickSpec/Term.hs b/src/QuickSpec/Term.hs
--- a/src/QuickSpec/Term.hs
+++ b/src/QuickSpec/Term.hs
@@ -1,5 +1,6 @@
--- Typed terms.
-{-# OPTIONS_HADDOCK hide #-}
+-- | 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 #-}
 module QuickSpec.Term(module QuickSpec.Term, module Twee.Base, module Twee.Pretty) where
 
@@ -10,15 +11,16 @@
 import Test.QuickCheck(CoArbitrary)
 import Data.DList(DList)
 import qualified Data.DList as DList
-import Twee.Base(Sized(..), Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
+import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
 import Twee.Pretty
 import qualified Data.Map.Strict as Map
 import Data.List
-import Data.Reflection
 
+-- | A typed term.
 data Term f = Var {-# UNPACK #-} !Var | App !f ![Term f]
   deriving (Eq, Ord, Show, Functor)
 
+-- | A variable, which has a type and a number.
 data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }
   deriving (Eq, Ord, Show, Generic, CoArbitrary)
 
@@ -27,8 +29,11 @@
   otherTypesDL _ = mzero
   typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x
 
+-- | A class for things that contain terms.
 class Symbolic f a | a -> f where
+  -- | A different list of all terms contained in the thing.
   termsDL :: a -> DList (Term f)
+  -- | Apply a substitution to all terms in the thing.
   subst :: (Var -> Term f) -> a -> a
 
 instance Symbolic f (Term f) where
@@ -40,55 +45,73 @@
   termsDL = msum . map termsDL
   subst sub = map (subst sub)
 
+class Sized a where
+  size :: a -> Int
+
 instance Sized f => Sized (Term f) where
   size (Var _) = 1
   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
   pPrintPrec l p (App f xs) =
     pPrintTerm (termStyle f) l p (pPrint f) xs
 
+-- | Is a term an application (i.e. not a variable)?
 isApp :: Term f -> Bool
 isApp App{} = True
 isApp Var{} = False
 
+-- | Is a term a variable?
 isVar :: Term f -> Bool
 isVar = not . isApp
 
+-- | All terms contained in a `Symbolic`.
 terms :: Symbolic f a => a -> [Term f]
 terms = DList.toList . termsDL
 
+-- | All function symbols appearing in a `Symbolic`, in order of appearance,
+-- with duplicates included.
 funs :: Symbolic f a => a -> [f]
 funs x = [ f | t <- terms x, App f _ <- subterms t ]
 
+-- | All variables appearing in a `Symbolic`, in order of appearance,
+-- with duplicates included.
 vars :: Symbolic f a => a -> [Var]
 vars x = [ v | t <- terms x, Var v <- subterms t ]
 
+-- | Compute the number of a variable which does /not/ appear in the `Symbolic`.
 freeVar :: Symbolic f a => a -> Int
 freeVar x = maximum (0:map (succ . var_id) (vars x))
 
+-- | Count how many times a given function symbol occurs.
 occ :: (Eq f, Symbolic f a) => f -> a -> Int
 occ x t = length (filter (== x) (funs t))
 
+-- | Count how many times a given variable occurs.
 occVar :: Symbolic f a => Var -> a -> Int
 occVar x t = length (filter (== x) (vars t))
 
+-- | Map a function over variables.
 mapVar :: (Var -> Var) -> Term f -> Term f
 mapVar f (Var x) = Var (f x)
 mapVar f (App g xs) = App g (map (mapVar f) xs)
 
-subterms, properSubterms :: Term f -> [Term f]
+-- | Find all subterms of a term. Includes the term itself.
+subterms :: Term f -> [Term f]
 subterms t = t:properSubterms t
+
+-- | Find all subterms of a term. Does not include the term itself.
+properSubterms :: Term f -> [Term f]
 properSubterms (App _ ts) = concatMap subterms ts
 properSubterms _ = []
 
--- Introduces variables in a canonical order.
--- Also makes sure that variables of different types have different numbers
+-- | Renames variables so that they appear in a canonical order.
+-- Also makes sure that variables of different types have different numbers.
 canonicalise :: Symbolic fun a => a -> a
 canonicalise t = subst (\x -> Map.findWithDefault undefined x sub) t
   where
@@ -97,18 +120,15 @@
         [(x, Var (V ty n))
         | (x@(V ty _), n) <- zip (nub (vars t)) [0..]]
 
-class Eval term val where
-  eval :: (Var -> val) -> term -> val
-
-instance (Typed fun, Given Type, Apply a, Eval fun a) => Eval (Term fun) a where
-  eval env = evaluateTerm (eval env) env
-
-evaluateTerm :: (Typed fun, Given Type, Apply a) => (fun -> a) -> (Var -> a) -> Term fun -> a
-evaluateTerm fun var = eval
+-- | Evaluate a term, given a valuation for variables and function symbols.
+evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a
+evalTerm var fun = eval
   where
     eval (Var x) = var x
-    eval (App f ts) =
-      foldl apply (fun (defaultTo given f)) (map eval ts)
+    eval (App f ts) = do
+      f <- fun f
+      ts <- mapM eval ts
+      return (foldl apply f ts)
 
 instance Typed f => Typed (Term f) where
   typ (Var x) = typ x
@@ -125,10 +145,11 @@
       tsub (App f ts) =
         App (typeSubst_ sub f) (map tsub ts)
 
--- A standard term ordering - size, skeleton, generality.
+-- | 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])
+-- | Compute the term ordering for a term.
 measure :: Sized f => Term f -> Measure f
 measure t =
   (size t, -length (vars t), MeasureFuns (skel t),
@@ -137,12 +158,14 @@
     skel (Var (V ty _)) = Var (V ty 0)
     skel (App f ts) = App f (map skel ts)
 
+-- | A helper for `Measure`.
 newtype MeasureFuns f = MeasureFuns (Term f)
 instance Ord f => Eq (MeasureFuns f) where
   t == u = compare t u == EQ
 instance Ord f => Ord (MeasureFuns f) where
   compare (MeasureFuns t) (MeasureFuns u) = compareFuns t u
 
+-- | A helper for `Measure`.
 compareFuns :: Ord f => Term f -> Term f -> Ordering
 compareFuns (Var x) (Var y) = compare x y
 compareFuns Var{} App{} = LT
@@ -152,14 +175,12 @@
   compare (map MeasureFuns ts) (map MeasureFuns us)
 
 ----------------------------------------------------------------------
--- Data types a la carte-ish.
+-- * Data types a la carte-ish.
 ----------------------------------------------------------------------
 
+-- | A sum type. Intended to be used to build the type of function
+-- symbols. Comes with instances that are useful for QuickSpec.
 data a :+: b = Inl a | Inr b deriving (Eq, Ord)
-
-instance (Eval fun1 a, Eval fun2 a) => Eval (fun1 :+: fun2) a where
-  eval env (Inl x) = eval env x
-  eval env (Inr x) = eval env x
 
 instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where
   size (Inl x) = size x
diff --git a/src/QuickSpec/Terminal.hs b/src/QuickSpec/Terminal.hs
--- a/src/QuickSpec/Terminal.hs
+++ b/src/QuickSpec/Terminal.hs
@@ -9,9 +9,13 @@
 import qualified Test.QuickCheck.Text as Text
 
 class Monad m => MonadTerminal m where
+  putText :: String -> m ()
   putLine :: String -> m ()
   putTemp :: String -> m ()
 
+  default putText :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()
+  putText = lift . putText
+
   default putLine :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()
   putLine = lift . putLine
 
@@ -34,6 +38,10 @@
   deriving (Functor, Applicative, Monad, MonadIO)
 
 instance MonadTerminal Terminal where
+  putText str = Terminal $ do
+    term <- ask
+    liftIO $ Text.putPart term str
+
   putLine str = Terminal $ do
     term <- ask
     liftIO $ Text.putLine term str
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
@@ -4,6 +4,7 @@
 module QuickSpec.Testing.QuickCheck where
 
 import QuickSpec.Testing
+import QuickSpec.Pruning
 import QuickSpec.Prop
 import Test.QuickCheck
 import Test.QuickCheck.Gen
@@ -37,7 +38,7 @@
 
 newtype Tester testcase term result m a =
   Tester (ReaderT (Environment testcase term result) m a)
-  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal)
+  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal, MonadPruner term' res')
 
 instance MonadTrans (Tester testcase term result) where
   lift = Tester . lift
@@ -50,21 +51,31 @@
   let
     seeds = unfoldr (Just . split) seed
     n = cfg_num_tests
-    k = cfg_max_test_size
-    -- Divide tests equally between all sizes.
-    -- There are n total tests of k+1 different sizes.
-    -- If it doesn't divide equally, the biggest size gets the
-    -- left-overs.
+    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 =
-      concat [replicate (n `div` (k+1)) i | i <- [0..k-1]] ++
-      replicate (n `divRoundUp` (k+1)) k
-    m `divRoundUp` n = (m-1) `div` n + 1
+      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 {
       env_config = config,
       env_tests = tests,
       env_eval = eval }
+
+-- uniform n k: generate a list of n integers which are distributed evenly between 0 and k-1.
+uniform :: Integer -> Integer -> [Integer]
+uniform n k =
+  -- n `div` k: divide evenly as far as possible.
+  concat [replicate (fromIntegral (n `div` k)) i | i <- [0..k-1]] ++
+  -- The leftovers get distributed at equal intervals.
+  [i * k `div` leftovers | i <- [0..leftovers-1]]
+  where
+    leftovers = n `mod` k
 
 instance (MonadTerminal m, Eq result) => MonadTester testcase term (Tester testcase term result m) where
   test prop =
diff --git a/src/QuickSpec/Type.hs b/src/QuickSpec/Type.hs
--- a/src/QuickSpec/Type.hs
+++ b/src/QuickSpec/Type.hs
@@ -1,26 +1,28 @@
+-- | This module is internal to QuickSpec.
+--
 -- Polymorphic types and dynamic values.
-{-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs #-}
 -- To avoid a warning about TyVarNumber's constructor being unused:
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
 module QuickSpec.Type(
-  -- Types.
+  -- * Types
   Typeable,
-  Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, SymA, typeVar, isTypeVar,
-  typeOf, typeRep, applyType, fromTypeRep,
-  arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity, oneTypeVar, defaultTo, skolemiseTypeVars,
-  isDictionary, getDictionary, pPrintType,
-  -- Things that have types.
-  Typed(..), typeSubst, typesDL, tyVars, cast,
+  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,
+  isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,
+  -- * Things that have types
+  Typed(..), typeSubst, typesDL, tyVars, cast, matchType,
   TypeView(..),
   Apply(..), apply, canApply,
-  -- Polymorphic types.
+  oneTypeVar, defaultTo, skolemiseTypeVars,
+  -- * Polymorphic types
   canonicaliseType,
-  Poly, toPolyValue, poly, unPoly, polyTyp, polyMap, polyRename, polyApply, polyPair, polyList, polyMgu,
-  -- Dynamic values.
-  Value, toValue, fromValue,
-  Unwrapped(..), unwrap, Wrapper(..),
-  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor) where
+  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu,
+  -- * Dynamic values
+  Value, toValue, fromValue, valueType,
+  unwrap, Unwrapped(..), Wrapper(..),
+  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor, bringFunctor) where
 
 import Control.Monad
 import Data.DList(DList)
@@ -35,11 +37,21 @@
 import Data.Proxy
 import Data.List
 import Data.Char
+import Data.Functor.Identity
 
--- A (possibly polymorphic) type.
+-- | A (possibly polymorphic) type.
 type Type = Term TyCon
 
-data TyCon = Arrow | String String | TyCon Ty.TyCon deriving (Eq, Ord, Show)
+-- | A type constructor.
+data TyCon =
+    -- | The function type constructor @(->)@.
+    Arrow
+    -- | An ordinary Haskell type constructor.
+  | TyCon Ty.TyCon
+    -- | A string. Can be used to represent miscellaneous types that do not
+    -- really exist in Haskell.
+  | String String
+  deriving (Eq, Ord, Show)
 
 instance Pretty TyCon where
   pPrint Arrow = text "->"
@@ -84,9 +96,13 @@
 deriving instance Typeable ClassD
 class ClassE
 deriving instance Typeable ClassE
+class ClassF
+deriving instance Typeable ClassF
 
+-- | A polymorphic type of kind Symbol.
 type SymA = "__polymorphic_symbol__"
 
+-- | All type variables that are defined in this module.
 typeVars :: [Ty.TypeRep]
 typeVars =
   [Ty.typeRep (Proxy :: Proxy A),
@@ -99,45 +115,65 @@
    Ty.typeRep (Proxy :: Proxy ClassC),
    Ty.typeRep (Proxy :: Proxy ClassD),
    Ty.typeRep (Proxy :: Proxy ClassE),
+   Ty.typeRep (Proxy :: Proxy ClassF),
    Ty.typeRep (Proxy :: Proxy SymA)]
 
+-- | A type variable.
 typeVar :: Type
 typeVar = typeRep (Proxy :: Proxy A)
 
+-- | Check if a type is a type variable.
 isTypeVar :: Type -> Bool
 isTypeVar = isVar
 
+-- | Construct a type from a `Typeable`.
 typeOf :: Typeable a => a -> Type
 typeOf x = fromTypeRep (Ty.typeOf x)
 
+-- | Construct a type from a `Typeable`.
 typeRep :: Typeable (a :: k) => proxy a -> Type
 typeRep x = fromTypeRep (Ty.typeRep x)
 
+-- | Turn a `TyCon` into a type.
+typeFromTyCon :: TyCon -> Type
+typeFromTyCon tc = build (con (fun tc))
+
+-- | Function application for type constructors.
+--
+-- For example, @applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])@.
 applyType :: Type -> Type -> Type
 applyType (App f tys) ty = build (app f (unpack tys ++ [ty]))
 applyType _ _ = error "tried to apply type variable"
 
+-- | Construct a function type.
 arrowType :: [Type] -> Type -> Type
 arrowType [] res = res
 arrowType (arg:args) res =
   build (app (fun Arrow) [arg, arrowType args res])
 
+-- | Decompose a function type into (argument, result).
+--
+-- For multiple-argument functions, unpacks one argument.
 unpackArrow :: Type -> Maybe (Type, Type)
 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))) =
   arg:typeArgs res
 typeArgs _ = []
 
+-- | The result of a function type.
 typeRes :: Type -> Type
 typeRes (App (F Arrow) (Cons _ (Cons res Empty))) =
   typeRes res
 typeRes ty = ty
 
+-- | Given the type of a function, returns the type of applying that function to
+-- @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))) =
@@ -145,20 +181,26 @@
 typeDrop _ _ =
   error "typeDrop on non-function type"
 
+-- | How many arguments does a function take?
 typeArity :: Type -> Int
 typeArity = length . typeArgs
 
+-- | Unify all type variables in a type.
 oneTypeVar :: Typed a => a -> a
 oneTypeVar = typeSubst (const (var (V 0)))
 
+-- | Replace all type variables with a particular type.
 defaultTo :: Typed a => Type -> a -> a
 defaultTo def = typeSubst (const def)
 
+-- | Make a type ground by replacing all type variables
+-- with Skolem constants.
 skolemiseTypeVars :: Typed a => a -> a
 skolemiseTypeVars = typeSubst (const aTy)
   where
     aTy = build (con (fun (tyCon (Proxy :: Proxy A))))
 
+-- | Construct a type from a `Ty.TypeRep`.
 fromTypeRep :: Ty.TypeRep -> Type
 fromTypeRep ty
   | Just n <- elemIndex ty typeVars =
@@ -167,11 +209,13 @@
     let (tyCon, tys) = Ty.splitTyConApp ty in
     build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys))
 
+-- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`.
 fromTyCon :: Ty.TyCon -> TyCon
 fromTyCon ty
   | ty == arrowTyCon = Arrow
   | otherwise = TyCon ty
 
+-- | Some built-in type consructors.
 arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon
 arrowTyCon = mkCon (Proxy :: Proxy (->))
 commaTyCon = mkCon (Proxy :: Proxy (,))
@@ -181,17 +225,31 @@
 mkCon :: Typeable a => proxy a -> Ty.TyCon
 mkCon = fst . Ty.splitTyConApp . Ty.typeRep
 
+-- | Get the outermost `TyCon` of a `Typeable`.
 tyCon :: Typeable a => proxy a -> TyCon
 tyCon = fromTyCon . mkCon
 
+-- | 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))
   | dict == dictTyCon = Just ty
 getDictionary _ = Nothing
 
+-- | Check if a type is of the form @`Dict` c@.
 isDictionary :: Type -> Bool
 isDictionary = isJust . getDictionary
 
+-- | Count how many dictionary arguments a type has.
+dictArity :: Type -> Int
+dictArity = length . takeWhile isDictionary . typeArgs
+
+-- | Split a type into constraints and normal type.
+splitConstrainedType :: Type -> ([Type], Type)
+splitConstrainedType ty =
+  (dicts, arrowType rest (typeRes ty))
+  where
+    (dicts, rest) = splitAt (dictArity ty) (typeArgs ty)
+
 -- CoArbitrary instances.
 instance CoArbitrary Type where
   coarbitrary = coarbitrary . singleton
@@ -202,27 +260,36 @@
   coarbitrary (ConsSym (App f _) ts) =
     variant 2 . coarbitrary (fun_id f) . coarbitrary ts
 
+-- | Pretty-print a type. Differs from the `Pretty` instance by printing type
+-- variables in lowercase.
 pPrintType :: Type -> Doc
-pPrintType = pPrint . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise
+pPrintType = ppr . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise
   where
     as = supply [[x] | x <- ['a'..'z']]
+    -- Print dictionary arguments specially
+    ppr ty
+      | Just (dict, res) <- unpackArrow ty,
+        Just constraint <- getDictionary dict =
+      pPrint constraint <+> text "=>" <+> ppr res
+    ppr ty = pPrint ty
 
--- Things with types.
+-- | A class for things that have a type.
 class Typed a where
-  -- The type.
+  -- | The type.
   typ :: a -> Type
-  -- Any other types that may appear in subterms etc
-  -- (enough at least to collect all type variables and type constructors).
+  -- | Types that appear elsewhere in the `Typed`, for example, types of subterms.
+  -- Should return everything which is affected by `typeSubst`.
   otherTypesDL :: a -> DList Type
   otherTypesDL _ = mzero
-  -- Substitute for all type variables.
+  -- | Substitute for all type variables.
   typeSubst_ :: (Var -> Builder TyCon) -> a -> a
 
+-- | Substitute for all type variables in a `Typed`.
 {-# INLINE typeSubst #-}
 typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a
 typeSubst s x = typeSubst_ (evalSubst s) x
 
--- Using the normal term machinery on types.
+-- | A wrapper for using the `Twee.Base.Symbolic` machinery on types.
 newtype TypeView a = TypeView { unTypeView :: a }
 instance Typed a => Symbolic (TypeView a) where
   type ConstantOf (TypeView a) = TyCon
@@ -231,22 +298,39 @@
 instance Typed a => Has (TypeView a) Type where
   the = typ . unTypeView
 
+-- | All types that occur in a `Typed`.
 typesDL :: Typed a => a -> DList Type
 typesDL ty = return (typ ty) `mplus` otherTypesDL ty
 
+-- | All type variables that occur in a `Typed`.
 tyVars :: Typed a => a -> [Var]
 tyVars = vars . TypeView
 
+-- | Cast a `Typed` to a target type.
+-- Succeeds if the target type is an instance of the current type.
 cast :: Typed a => Type -> a -> Maybe a
 cast ty x = do
   s <- match (typ x) ty
   return (typeSubst s x)
 
--- Typed things that support function application.
+-- | Check if the second argument is an instance of the first argument.
+matchType :: Type -> Type -> Maybe (Subst TyCon)
+matchType = match
+
+-- | Typed things that support function application.
 class Typed a => Apply a where
-  -- Apply a function to its argument.
+  -- | Apply a function to its argument.
+  --
+  -- For most instances of `Typed`, the type of the argument must be exactly
+  -- equal to the function's argument type. If you want unification to happen,
+  -- use the `Typed` instance of `Poly`.
   tryApply :: a -> a -> Maybe a
 
+-- | Apply a function to its argument, crashing on failure.
+--
+-- For most instances of `Typed`, the type of the argument must be exactly
+-- equal to the function's argument type. If you want unification to happen,
+-- use the `Typed` instance of `Poly`.
 infixl `apply`
 apply :: Apply a => a -> a -> a
 apply f x =
@@ -257,6 +341,7 @@
         prettyShow (typ f) ++ " to " ++ prettyShow (typ x)
     Just y -> y
 
+-- | Check if a function can be applied to its argument.
 canApply :: Apply a => a -> a -> Bool
 canApply f x = isJust (tryApply f x)
 
@@ -290,38 +375,47 @@
   otherTypesDL (x:xs) = otherTypesDL x `mplus` msum (map typesDL xs)
   typeSubst_ f xs = map (typeSubst_ f) xs
 
--- Represents a forall-quantifier over all the type variables in a type.
--- Wrapping a term in Poly normalises the type by alpha-renaming
+-- | Represents a forall-quantifier over all the type variables in a type.
+-- Wrapping a term in @Poly@ normalises the type by alpha-renaming
 -- type variables canonically.
+--
+-- The `Apply` instance for `Poly` does unification to handle applying a
+-- polymorphic function.
 newtype Poly a = Poly { unPoly :: a }
   deriving (Eq, Ord, Show, Pretty, Typeable)
 
+-- | Build a `Poly`.
 poly :: Typed a => a -> Poly a
 poly x = Poly (canonicaliseType x)
 
+-- | Alpha-rename type variables in a canonical way.
 canonicaliseType :: Typed a => a -> a
 canonicaliseType = unTypeView . canonicalise . TypeView
 
+-- | Get the polymorphic type of a polymorphic value.
 polyTyp :: Typed a => Poly a -> Poly Type
 polyTyp (Poly x) = Poly (typ x)
 
-polyMap :: (Typed a, Typed b) => (a -> b) -> Poly a -> Poly b
-polyMap f (Poly x) = poly (f x)
-
+-- | Rename the type variables of the second argument so that they don't overlap
+-- with those of the first argument.
 polyRename :: (Typed a, Typed b) => a -> Poly b -> b
 polyRename x (Poly y) =
   unTypeView (renameAvoiding (TypeView x) (TypeView y))
 
+-- | Rename the type variables of both arguments so that they don't overlap.
 polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c
 polyApply f (Poly x) y = poly (f x (polyRename x y))
 
+-- | Rename the type variables of both arguments so that they don't overlap.
 polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
 polyPair = polyApply (,)
 
+-- | Rename the type variables of all arguments so that they don't overlap.
 polyList :: Typed a => [Poly a] -> Poly [a]
 polyList [] = poly []
 polyList (x:xs) = polyApply (:) x (polyList xs)
 
+-- | Find the most general unifier of two types.
 polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)
 polyMgu ty1 ty2 = do
   let (ty1', ty2') = unPoly (polyPair ty1 ty2)
@@ -340,10 +434,13 @@
     let (f'', x'') = typeSubst s (f', x')
     fmap poly (tryApply f'' x'')
 
+-- | Convert an ordinary value to a dynamic value.
 toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)
 toPolyValue = poly . toValue . pure
 
--- Dynamic values inside an applicative functor.
+-- | Dynamic values inside an applicative functor.
+--
+-- For example, a value of type @Value Maybe@ represents a @Maybe something@.
 data Value f =
   Value {
     valueType :: Type,
@@ -358,9 +455,11 @@
 toAny :: f a -> f Any
 toAny = unsafeCoerce
 
+-- | Construct a `Value`.
 toValue :: forall f (a :: *). Typeable a => f a -> Value f
 toValue x = Value (typeRep (Proxy :: Proxy a)) (toAny x)
 
+-- | Deconstruct a `Value`.
 fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)
 fromValue x = do
   guard (typ x == typeRep (Proxy :: Proxy a))
@@ -374,14 +473,7 @@
     ty <- tryApply (typ f) (typ x)
     return (Value ty (fromAny (value f) <*> value x))
 
--- Unwrap a value to get at the thing inside, while still being able
--- to wrap it up again.
-data Unwrapped f = forall a. f a `In` Wrapper a
-data Wrapper a =
-  Wrapper {
-    wrap :: forall g. g a -> Value g,
-    reunwrap :: forall g. Value g -> g a }
-
+-- | Unwrap a value to get at the thing inside, with an existential type.
 unwrap :: Value f -> Unwrapped f
 unwrap x =
   value x `In`
@@ -392,22 +484,40 @@
         then fromAny (value y)
         else error "non-matching types")
 
+-- | The unwrapped value. Consists of the value itself (with an existential
+-- type) and functions to wrap it up again.
+data Unwrapped f where
+  In :: f a -> Wrapper a -> Unwrapped f
+
+-- | Functions for re-wrapping an `Unwrapped` value.
+data Wrapper a =
+  Wrapper {
+    -- | Wrap up a value which has the same existential type as this one.
+    wrap :: forall g. g a -> Value g,
+    -- | Unwrap a value which has the same existential type as this one.
+    reunwrap :: forall g. Value g -> g a }
+
+-- | Apply a polymorphic function to a `Value`.
 mapValue :: (forall a. f a -> g a) -> Value f -> Value g
 mapValue f v =
   case unwrap v of
     x `In` w -> wrap w (f x)
 
+-- | Apply a polymorphic function to a `Value`.
 forValue :: Value f -> (forall a. f a -> g a) -> Value g
 forValue x f = mapValue f x
 
+-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.
 ofValue :: (forall a. f a -> b) -> Value f -> b
 ofValue f v =
   case unwrap v of
     x `In` _ -> f x
 
+-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.
 withValue :: Value f -> (forall a. f a -> b) -> b
 withValue x f = ofValue f x
 
+-- | Apply a polymorphic function to a pair of `Value`s.
 pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f
 pairValues f x y =
   ty `seq`
@@ -440,3 +550,9 @@
     _ -> error "value of type f a had wrong type"
   where
     ty = typeRep (Proxy :: Proxy g)
+
+bringFunctor :: Functor f => Value f -> f (Value Identity)
+bringFunctor val =
+  case unwrap val of
+    x `In` w ->
+      fmap (wrap w . Identity) x
diff --git a/src/QuickSpec/Utils.hs b/src/QuickSpec/Utils.hs
--- a/src/QuickSpec/Utils.hs
+++ b/src/QuickSpec/Utils.hs
@@ -5,6 +5,7 @@
 
 import Control.Arrow((&&&))
 import Control.Exception
+import Control.Spoon
 import Data.List(groupBy, sortBy)
 #if !MIN_VERSION_base(4,8,0)
 import Data.Monoid
@@ -84,30 +85,8 @@
     (hSetBuffering stdout buf)
     x
 
-newtype Max a = Max { getMax :: Maybe a }
-
-getMaxWith :: Ord a => a -> Max a -> a
-getMaxWith x (Max (Just y)) = x `max` y
-getMaxWith x (Max Nothing)  = x
-
-instance Ord a => Monoid (Max a) where
-  mempty = Max Nothing
-  Max (Just x) `mappend` y = Max (Just (getMaxWith x y))
-  Max Nothing  `mappend` y = y
-
-newtype Min a = Min { getMin :: Maybe a }
-
-getMinWith :: Ord a => a -> Min a -> a
-getMinWith x (Min (Just y)) = x `min` y
-getMinWith x (Min Nothing)  = x
-
-minimumBy :: (a -> a -> Bool) -> [a] -> a
-minimumBy f = foldr1 (\x y -> if f x y then x else y)
-
-instance Ord a => Monoid (Min a) where
-  mempty = Min Nothing
-  Min (Just x) `mappend` y = Min (Just (getMinWith x y))
-  Min Nothing  `mappend` y = y
+spoony :: Eq a => a -> Maybe a
+spoony x = teaspoon ((x == x) `seq` x)
 
 labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]
 labelM f = mapM (\x -> do { y <- f x; return (x, y) })
@@ -120,3 +99,8 @@
   | x == y = xs `isSubsequenceOf` ys
   | otherwise = (x:xs) `isSubsequenceOf` ys
 #endif
+
+appendAt :: Int -> [a] -> [[a]] -> [[a]]
+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