diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,5 +1,5 @@
 Name:                quickspec
-Version:             0.9.1
+Version:             0.9.2
 Cabal-version:       >=1.6
 Build-type:          Simple
 
@@ -64,6 +64,7 @@
 
 library
   hs-source-dirs: src
+  include-dirs: src/Test/QuickSpec/
   Exposed-modules:
     Test.QuickSpec,
     Test.QuickSpec.Main,
diff --git a/src/Test/QuickSpec.hs b/src/Test/QuickSpec.hs
--- a/src/Test/QuickSpec.hs
+++ b/src/Test/QuickSpec.hs
@@ -68,7 +68,9 @@
    -- * Modifying a signature
    background,
    withDepth,
+   withSize,
    withTests,
+   withQuickCheckSize,
    without,
 
    -- * The standard QuickSpec prelude, to include in your own signatures
diff --git a/src/Test/QuickSpec/Approximate.hs b/src/Test/QuickSpec/Approximate.hs
--- a/src/Test/QuickSpec/Approximate.hs
+++ b/src/Test/QuickSpec/Approximate.hs
@@ -60,12 +60,7 @@
     plug x = frequency [(1, undefined), (3, x)]
 
 pvars :: (Ord a, Partial a) => [String] -> a -> Sig
-pvars xs w =
-  pobserver w
-  `mappend` variableSig [ Variable (Atom (symbol x 0 w) (PGen g g')) | x <- xs ]
-  `mappend` totalSig g
-  `mappend` partialSig g'
-  `mappend` typeSig w
+pvars xs w = pobserver w `mappend` primVars0 0 xs (PGen g g')
   where
     g = arbitrary `asTypeOf` return w
     g' = g >>= genPartial
diff --git a/src/Test/QuickSpec/Equation.hs b/src/Test/QuickSpec/Equation.hs
--- a/src/Test/QuickSpec/Equation.hs
+++ b/src/Test/QuickSpec/Equation.hs
@@ -13,7 +13,7 @@
 
 showEquation :: Sig -> Equation -> String
 showEquation sig (t :=: u) =
-  show (f t) ++ " == " ++ show (f u)
+  show (mapVars f t) ++ " == " ++ show (mapVars f u)
   where f = disambiguate sig (vars t ++ vars u)
 
 instance Show Equation where
diff --git a/src/Test/QuickSpec/Generate.hs b/src/Test/QuickSpec/Generate.hs
--- a/src/Test/QuickSpec/Generate.hs
+++ b/src/Test/QuickSpec/Generate.hs
@@ -6,7 +6,7 @@
 #include "errors.h"
 import Test.QuickSpec.Signature hiding (con)
 import qualified Test.QuickSpec.TestTree as T
-import Test.QuickSpec.TestTree(TestResults, reps, classes, numTests, cutOff, discrete)
+import Test.QuickSpec.TestTree(TestResults, reps, classes, numTests, numResults, cutOff, discrete)
 import Test.QuickSpec.Utils.Typed
 import Test.QuickSpec.Utils.TypeRel(TypeRel)
 import qualified Test.QuickSpec.Utils.TypeRel as TypeRel
@@ -29,6 +29,7 @@
 
 terms' :: Typeable a => Sig -> TypeRel Expr -> a -> [Expr a]
 terms' sig base w =
+  filter (\t -> size 1 (term t) <= maxSize sig) $
   map var (TypeRel.lookup w (variables sig)) ++
   map con (TypeRel.lookup w (constants sig)) ++
   [ app f x
@@ -39,22 +40,20 @@
     arity f > 0,
     not (isUndefined (term f)) ]
 
-test :: Strategy -> [(StdGen, Int)] -> Sig ->
+test :: [(Valuation, StdGen, Int)] -> Sig ->
         TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr)
-test strat seeds sig ts = fmap (mapSome2 (test' strat seeds sig)) ts
+test vals sig ts = fmap (mapSome2 (test' vals sig)) ts
 
 test' :: forall a. Typeable a =>
-         Strategy -> [(StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
-test' strat seeds sig ts
+         [(Valuation, StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
+test' vals sig ts
   | not (testable sig (undefined :: a)) = discrete ts
   | otherwise =
     case observe undefined sig of
       Observer obs ->
-        let testCase (g, n) =
-              let (g1, g2) = split g
-                  val = memoValuation sig (unGen (valuation strat) g1 n) in
-              \x -> spoony . unGen (partialGen obs) g2 n $ eval x val
-        in cutOff base increment (T.test (map testCase seeds) ts)
+        let testCase (val, g, n) x =
+              spoony . unGen (partialGen obs) g n $ eval x val
+        in cutOff base increment (T.test (map testCase vals) ts)
   where
     base = minTests sig `div` 2
     increment = minTests sig - base
@@ -65,6 +64,11 @@
   let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd
   return (zip (rnds rnd) (concat (repeat [0,2..maxSize])))
 
+toValuation :: Strategy -> Sig -> (StdGen, Int) -> (Valuation, StdGen, Int)
+toValuation strat sig (g, n) =
+  let (g1, g2) = split g
+  in (memoValuation sig (unGen (valuation strat) g1 n), g2, n)
+
 generate :: Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr))
 generate strat sig | maxDepth sig < 0 =
   ERROR "generate: maxDepth must be positive"
@@ -79,9 +83,10 @@
       ts = terms sig rs
   printf "%d terms, " (count sum length ts)
   seeds <- genSeeds (maxQuickCheckSize sig)
-  let cs = test strat seeds sig ts
-  printf "%d tests, %d classes, %d raw equations.\n"
+  let cs = test (map (toValuation strat sig) seeds) sig ts
+  printf "%d tests, %d evaluations, %d classes, %d raw equations.\n"
       (count (maximum . (0:)) numTests cs)
+      (count sum numResults cs)
       (count sum (length . classes) cs)
       (count sum (sum . map (subtract 1 . length) . classes) cs)
   return cs
diff --git a/src/Test/QuickSpec/Main.hs b/src/Test/QuickSpec/Main.hs
--- a/src/Test/QuickSpec/Main.hs
+++ b/src/Test/QuickSpec/Main.hs
@@ -111,9 +111,13 @@
     (length reps)
 
   let ctx = initial (maxDepth sig) (symbols sig) reps
-      pruned = filter (not . all silent . eqnFuns)
+      allEqs = map (some eraseEquation) eqs
+      isBackground = all silent . eqnFuns
+      (background, foreground) =
+        partition isBackground allEqs
+      pruned = filter (not . isBackground)
                  (prune ctx (map erase reps) id
-                   (map (some eraseEquation) eqs))
+                   (background ++ foreground))
       eqnFuns (t :=: u) = funs t ++ funs u
       isGround (t :=: u) = null (vars t) && null (vars u)
       byTarget = innerZip [1 :: Int ..] (partitionBy target pruned)
@@ -152,6 +156,6 @@
   printf "== Here are %d terms out of a total of %d ==\n" numTerms (length univ)
   g <- newStdGen
   forM_ (zip [1 :: Int ..] (sampleList g numTerms univ)) $ \(i, t) ->
-    printf "%d: %s\n" i (show (disambiguate sig (vars t) t))
+    printf "%d: %s\n" i (show (mapVars (disambiguate sig (vars t)) t))
 
   putStrLn ""
diff --git a/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs
--- a/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs
+++ b/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE CPP, TupleSections #-}
 module Test.QuickSpec.Reasoning.NaiveEquationalReasoning where
 
-#include "../errors.h"
+#include "errors.h"
 
 import Test.QuickSpec.Term
 import Test.QuickSpec.Equation
diff --git a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs
--- a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs
+++ b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE CPP #-}
 module Test.QuickSpec.Reasoning.PartialEquationalReasoning where
 
-#include "../errors.h"
+#include "errors.h"
 import Test.QuickSpec.Equation
 import Test.QuickSpec.Term hiding (Variable, vars)
 import qualified Test.QuickSpec.Term as Term
@@ -37,8 +37,8 @@
 
 showPEquation :: Sig -> PEquation -> String
 showPEquation sig (pre :\/: t :=: u) =
-  show (f t) ++ " == " ++ show (f u) ++
-  showPre (map (f . Var) pre)
+  show (mapVars f t) ++ " == " ++ show (mapVars f u) ++
+  showPre (map f pre)
   where f = disambiguate sig (Term.vars t ++ Term.vars u ++ pre)
         showPre [] = ""
         showPre xs = " when " ++ conjunction (map show xs) ++ " " ++ plural xs "is" "are" ++ " partial"
diff --git a/src/Test/QuickSpec/Signature.hs b/src/Test/QuickSpec/Signature.hs
--- a/src/Test/QuickSpec/Signature.hs
+++ b/src/Test/QuickSpec/Signature.hs
@@ -1,6 +1,6 @@
 -- | Functions for constructing and analysing signatures.
 
-{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, ScopedTypeVariables #-}
+{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, ScopedTypeVariables, DeriveDataTypeable #-}
 module Test.QuickSpec.Signature where
 
 #include "errors.h"
@@ -8,7 +8,7 @@
 import Test.QuickSpec.Utils.Typeable
 import Data.Monoid
 import Test.QuickCheck
-import Test.QuickSpec.Term hiding (var)
+import Test.QuickSpec.Term hiding (var, vars)
 import Test.QuickSpec.Utils.Typed
 import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
 import Test.QuickSpec.Utils.TypeMap(TypeMap)
@@ -52,26 +52,35 @@
   -- Depth of terms in the universe.
   maxDepth_ :: First Int,
 
+  -- Size of terms in the universe.
+  maxSize_ :: First Int,
+
   -- Minimum number of tests to run.
   minTests_ :: First Int,
 
   -- Maximum size parameter to pass to QuickCheck.
   maxQuickCheckSize_ :: First Int
-  }
+  } deriving Typeable
 
 maxDepth :: Sig -> Int
 maxDepth = fromMaybe 3 . getFirst . maxDepth_
 
+maxSize :: Sig -> Int
+maxSize = fromMaybe 100 . getFirst . maxSize_
+
 updateDepth :: Int -> Sig -> Sig
 updateDepth n sig = sig { maxDepth_ = First (Just n) }
 
+updateSize :: Int -> Sig -> Sig
+updateSize n sig = sig { maxSize_ = First (Just n) }
+
 minTests :: Sig -> Int
 minTests = fromMaybe 500 . getFirst . minTests_
 
 maxQuickCheckSize :: Sig -> Int
 maxQuickCheckSize = fromMaybe 20 . getFirst . maxQuickCheckSize_
 
-instance Show Sig where show = unlines . summarise
+instance Show Sig where show = show . summarise
 
 data Used = Used Witness [Symbol]
 instance Show Used where
@@ -86,55 +95,98 @@
       w' <- constantArgs sig k,
       w == w' ]
 
-summarise :: Sig -> [String]
-summarise sig =
-  section ["-- functions --"]
-    (decls (filter (not . silent) allConstants)) ++
-  section ["-- background functions --"]
-    (decls (filter silent allConstants)) ++
-  section ["-- variables --"]
-    (decls allVariables) ++
-  section ["-- the following types are using non-standard equality --"]
-    (map show (Map.keys (observers sig))) ++
+data Summary = Summary {
+  summaryFunctions :: [Symbol],
+  summaryBackground :: [Symbol],
+  summaryVariables :: [Symbol],
+  summaryObserved :: [TypeRep],
+  summaryUninhabited :: [Used],
+  summaryNoVars :: [TypeRep],
+  summaryUntestable :: [TypeRep],
+  summaryDepth :: Maybe Int,
+  summarySize :: Maybe Int,
+  summaryTests :: Maybe Int,
+  summaryQuickCheckSize :: Maybe Int
+  }
 
-  section ["-- WARNING: the following types are uninhabited --"]
-    (usort
-     [ show (uses sig ty)
-     | ty <- argumentTypes sig,
-       ty `notElem` inhabitedTypes sig,
-       ty `notElem` variableTypes sig ]) ++
+instance Show Summary where
+  show summary = unlines $
+    section ["-- functions --"] (decls (summaryFunctions summary)) ++
+    section ["-- background functions --"] (decls (summaryBackground summary)) ++
+    section ["-- variables --"] (decls (summaryVariables summary)) ++
+    section ["-- the following types are using non-standard equality --"]
+      (map show (summaryObserved summary)) ++
+    section ["-- WARNING: the following types are uninhabited --"]
+      (map show (summaryUninhabited summary)) ++
+    section ["-- WARNING: there are no variables of the following types; consider adding some --"]
+      (map show (summaryNoVars summary)) ++
+    section ["-- WARNING: cannot test the following types; ",
+             "            consider using 'fun' instead of 'blind' or using 'observe' --"]
+      (map show (summaryUntestable summary))
+    where
+      section _ [] = []
+      section msg xs = msg ++ xs ++ [""]
 
-  section ["-- WARNING: there are no variables of the following types; consider adding some --"]
-    (usort
-     [ show ty
-     | ty <- argumentTypes sig,
-       -- There is a non-variable term of this type and it appears as the
-       -- argument to some function
-       ty `elem` inhabitedTypes sig,
-       ty `notElem` variableTypes sig ]) ++
-  section ["-- WARNING: cannot test the following types; ",
-        "            consider using 'fun' instead of 'blind' or using 'observe' --"]
-    (usort
-     [ show ty
-     | ty@(Some (Witness w)) <- saturatedTypes sig,
-       -- The type is untestable and is the result type of a constant
-       not (testable sig w) ])
+      decls xs = map decl (partitionBy symbolType xs)
 
+      decl xs@(x:_) =
+        intercalate ", " (map show xs) ++ " :: " ++ show (symbolType x)
+
+sigToHaskell :: Signature a => a -> String
+sigToHaskell sig = "signature [\n" ++ intercalate ",\n" (map ("  " ++) ls) ++ "]"
   where
+    summary = summarise (signature sig)
+    ls =
+      [ function s | s <- summaryFunctions summary ] ++
+      [ background s | s <- summaryBackground summary ] ++
+      [ variable ss | ss <- partitionBy symbolType (summaryVariables summary) ] ++
+      [ "withDepth " ++ show n | Just n <- [summaryDepth summary] ] ++
+      [ "withSize " ++ show n | Just n <- [summarySize summary] ] ++
+      [ "withTests " ++ show n | Just n <- [summaryTests summary] ] ++
+      [ "withQuickCheckSize " ++ show n | Just n <- [summaryQuickCheckSize summary] ]
+    function s = "\"" ++ show s ++ "\" `fun" ++ show (symbolArity s) ++ "` (" ++
+                 show s ++ " :: " ++ show (symbolType s) ++ ")"
+    background s = "background $ " ++ function s
+    variable ss@(s:_) =
+      show (map name ss) ++ " `vars" ++ show (symbolArity s) ++
+      "` (undefined :: " ++ show (symbolType s) ++ ")"
+
+summarise :: Sig -> Summary
+summarise sig =
+  Summary {
+    summaryFunctions = filter (not . silent) allConstants,
+    summaryBackground = filter silent allConstants,
+    summaryVariables = allVariables,
+    summaryObserved = Map.keys (observers sig),
+    summaryUninhabited =
+      [ uses sig ty
+      | ty <- argumentTypes sig,
+        ty `notElem` inhabitedTypes sig,
+        ty `notElem` variableTypes sig ],
+    summaryNoVars =
+      [ witnessType ty
+      | ty <- argumentTypes sig,
+        -- There is a non-variable term of this type and it appears as the
+        -- argument to some function
+        ty `elem` inhabitedTypes sig,
+        ty `notElem` variableTypes sig ],
+    summaryUntestable =
+      [ witnessType ty
+      | ty@(Some (Witness w)) <- saturatedTypes sig,
+        -- The type is untestable and is the result type of a constant
+        not (testable sig w) ],
+    summaryDepth = getFirst (maxDepth_ sig),
+    summarySize = getFirst (maxSize_ sig),
+    summaryTests = getFirst (minTests_ sig),
+    summaryQuickCheckSize = getFirst (maxQuickCheckSize_ sig) }
+
+  where
     symbols :: (Sig -> TypeRel f) -> (forall a. f a -> Symbol) -> [Symbol]
     symbols f erase = map (some erase) (TypeRel.toList (f sig))
 
     allConstants = symbols constants (sym . unConstant)
     allVariables = symbols variables (sym . unVariable)
 
-    section _ [] = []
-    section msg xs = msg ++ xs ++ [""]
-
-    decls xs = map decl (partitionBy symbolType xs)
-
-    decl xs@(x:_) =
-      intercalate ", " (map show xs) ++ " :: " ++ show (symbolType x)
-
 data Observer a = forall b. Ord b => Observer (PGen (a -> b))
 
 observe x sig =
@@ -143,20 +195,21 @@
   where msg = "no observers found for type " ++ show (typeOf x)
 
 emptySig :: Sig
-emptySig = Sig TypeRel.empty TypeRel.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty mempty mempty mempty
+emptySig = Sig TypeRel.empty TypeRel.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty mempty mempty mempty mempty
 
 instance Monoid Sig where
   mempty = emptySig
   s1 `mappend` s2 =
     Sig {
-      constants = renumber (mapConstant . alter) 0 constants',
-      variables = renumber (mapVariable . alter) (length constants') variables',
+      constants = renumber (mapConstant . alter) (length variables') constants',
+      variables = renumber (mapVariable . alter) 0 variables',
       observers = observers s1 `mappend` observers s2,
       total = total s1 `mappend` total s2,
       partial = partial s1 `mappend` partial s2,
       ords = ords s1 `mappend` ords s2,
       witnesses = witnesses s1 `mappend` witnesses s2,
       maxDepth_ = maxDepth_ s1 `mappend` maxDepth_ s2,
+      maxSize_ = maxSize_ s1 `mappend` maxSize_ s2,
       minTests_ = minTests_ s1 `mappend` minTests_ s2,
       maxQuickCheckSize_ = maxQuickCheckSize_ s1 `mappend` maxQuickCheckSize_ s2 }
     where constants' = TypeRel.toList (constants s1) ++
@@ -209,6 +262,12 @@
 withDepth :: Int -> Sig
 withDepth n = updateDepth n emptySig
 
+-- | If @withSize n@ is in your signature,
+--   QuickSpec will consider terms of up to size @n@
+--   (the default is 100).
+withSize :: Int -> Sig
+withSize n = updateSize n emptySig
+
 -- | If @withTests n@ is in your signature,
 --   QuickSpec will run at least @n@ tests
 --   (the default is 500).
@@ -303,22 +362,50 @@
   where sig' = signature sig
         silence1 x = x { silent = True }
 
+primVars0 :: forall a. Typeable a => Int -> [String] -> PGen a -> Sig
+primVars0 n xs g = variableSig [ Variable (Atom (symbol x n (undefined :: a)) g) | x <- xs ]
+             `mappend` totalSig (totalGen g)
+             `mappend` partialSig (partialGen g)
+             `mappend` typeSig (undefined :: a)
+
+primVars1 :: forall a b. (Typeable a, Typeable b) => Int -> [String] -> PGen (a -> b) -> Sig
+primVars1 n xs g = primVars0 n xs g
+             `mappend` typeSig (undefined :: a)
+             `mappend` typeSig (undefined :: b)
+
+primVars2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => Int -> [String] -> PGen (a -> b -> c) -> Sig
+primVars2 n xs g = primVars1 n xs g
+             `mappend` typeSig (undefined :: b)
+             `mappend` typeSig (undefined :: c)
+
 -- | Similar to `vars`, but takes a generator as a parameter.
 --
 -- @gvars xs (arbitrary :: Gen a)@ is the same as
 -- @vars xs (undefined :: a)@.
-gvars :: forall a. Typeable a => [String] -> Gen a -> Sig
-gvars xs g = variableSig [ Variable (Atom (symbol x 0 (undefined :: a)) (pgen g)) | x <- xs ]
-             `mappend` totalSig g
-             `mappend` typeSig (undefined :: a)
+gvars, gvars0 :: forall a. Typeable a => [String] -> Gen a -> Sig
+gvars xs g = primVars0 0 xs (pgen g)
+gvars0 = gvars
 
+gvars1 :: forall a b. (Typeable a, Typeable b) => [String] -> Gen (a -> b) -> Sig
+gvars1 xs g = primVars1 1 xs (pgen g)
+
+gvars2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => [String] -> Gen (a -> b -> c) -> Sig
+gvars2 xs g = primVars2 2 xs (pgen g)
+
 -- | Declare a set of variables of a particular type.
 --
 -- For example, @vars [\"x\",\"y\",\"z\"] (undefined :: Int)@
 -- defines three variables, @x@, @y@ and @z@, of type `Int`.
-vars :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig
+vars, vars0 :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig
 vars xs _ = gvars xs (arbitrary :: Gen a)
+vars0 = vars
 
+vars1 :: forall a b. (CoArbitrary a, Typeable a, Arbitrary b, Typeable b) => [String] -> (a -> b) -> Sig
+vars1 xs _ = gvars1 xs (arbitrary :: Gen (a -> b))
+
+vars2 :: forall a b c. (CoArbitrary a, Typeable a, CoArbitrary b, Typeable b, Arbitrary c, Typeable c) => [String] -> (a -> b -> c) -> Sig
+vars2 xs _ = gvars2 xs (arbitrary :: Gen (a -> b -> c))
+
 con, fun0 :: (Ord a, Typeable a) => String -> a -> Sig
 -- | A constant. The same as `fun0`.
 con = fun0
@@ -452,12 +539,12 @@
 lookupWitness :: Sig -> TypeRep -> Maybe Witness
 lookupWitness sig ty = Map.lookup ty (witnesses sig)
 
-disambiguate :: Sig -> [Symbol] -> Term -> Term
+disambiguate :: Sig -> [Symbol] -> Symbol -> Symbol
 disambiguate sig ss =
-  mapVars (\x ->
+  \x ->
     fromMaybe (ERROR "variable not found")
       (find (\y -> index x == index y)
-        (aux [] (nub ss))))
+        (aux [] (nub ss)))
   where
     aux used [] = []
     aux used (x:xs) = x { name = next }:aux (next:used) xs
diff --git a/src/Test/QuickSpec/Term.hs b/src/Test/QuickSpec/Term.hs
--- a/src/Test/QuickSpec/Term.hs
+++ b/src/Test/QuickSpec/Term.hs
@@ -6,6 +6,7 @@
 #include "errors.h"
 import Test.QuickSpec.Utils.Typeable
 import Test.QuickCheck
+import Test.QuickCheck.Gen
 import Data.Function
 import Data.Ord
 import Data.Char
@@ -41,7 +42,7 @@
 instance Ord Term where
   compare = comparing stamp
     where
-      stamp t = (depth t, size t, -occur t, body t)
+      stamp t = (depth t, size 0 t, -occur t, body t)
 
       occur t = length (usort (vars t))
 
@@ -87,13 +88,15 @@
         symbols' (Const x) = (x:)
         symbols' (App f x) = symbols' f . symbols' x
 
-depth, size :: Term -> Int
+depth :: Term -> Int
 depth (App f x) = depth f `max` (1 + depth x)
 depth _ = 1
-size (App f x) = size f + size x
-size (Var _) = 0
-size (Const _) = 1
 
+size :: Int -> Term -> Int
+size v (App f x) = size v f + size v x
+size v (Var _) = v
+size v (Const _) = 1
+
 holes :: Term -> [(Symbol, Int)]
 holes t = holes' 0 t []
   where holes' d (Var x) = ((x, d):)
@@ -131,7 +134,7 @@
 data Expr a = Expr {
   term :: Term,
   arity :: {-# UNPACK #-} !Int,
-  eval :: (forall b. Variable b -> b) -> a }
+  eval :: Valuation -> a }
   deriving Typeable
 
 instance Eq (Expr a) where
@@ -170,14 +173,19 @@
 mapConstant f (Constant v) = Constant v { sym = f (sym v) }
 
 -- Generate a random variable valuation
-valuation :: Strategy -> Gen (Variable a -> a)
-valuation strat = promote (\(Variable x) -> index (sym x) `variant'` strat (sym x) (value x))
+newtype Valuation = Valuation { unValuation :: forall a. Variable a -> a }
+
+promoteVal :: (forall a. Gen (Variable a -> a)) -> Gen Valuation
+promoteVal g = MkGen (\r n -> Valuation (unGen g r n))
+
+valuation :: Strategy -> Gen Valuation
+valuation strat = promoteVal (promote (\(Variable x) -> index (sym x) `variant'` strat (sym x) (value x)))
   where -- work around the fact that split doesn't work
         variant' 0 = variant (0 :: Int)
         variant' n = variant (-1 :: Int) . variant' (n-1)
 
 var :: Variable a -> Expr a
-var v@(Variable (Atom x _)) = Expr (Var x) 0 (\env -> env v)
+var v@(Variable (Atom x _)) = Expr (Var x) (symbolArity x) (\env -> unValuation env v)
 
 con :: Constant a -> Expr a
 con (Constant (Atom x v)) = Expr (Const x) (symbolArity x) (const v)
diff --git a/src/Test/QuickSpec/TestTotality.hs b/src/Test/QuickSpec/TestTotality.hs
--- a/src/Test/QuickSpec/TestTotality.hs
+++ b/src/Test/QuickSpec/TestTotality.hs
@@ -65,10 +65,8 @@
       always sig $ do
         let strat s' = if s == s' then partialGen else totalGen
         obs' <- partialGen obs
-        -- Hack around "value restriction" for lambdas
-        MkGen $ \g n ->
-          let v = unGen (valuation strat) g n
-          in spoony (obs' (eval e1 v)) == spoony (obs' (eval e2 v))
+        v <- valuation strat
+        return (spoony (obs' (eval e1 v)) == spoony (obs' (eval e2 v)))
 
 always :: Sig -> Gen Bool -> IO Bool
 always sig x = do
diff --git a/src/Test/QuickSpec/TestTree.hs b/src/Test/QuickSpec/TestTree.hs
--- a/src/Test/QuickSpec/TestTree.hs
+++ b/src/Test/QuickSpec/TestTree.hs
@@ -3,7 +3,8 @@
 
 {-# LANGUAGE CPP #-}
 module Test.QuickSpec.TestTree(TestTree, terms, union, test,
-               TestResults, cutOff, numTests, classes, reps, discrete) where
+               TestResults, cutOff, numTests, numResults,
+               classes, reps, discrete) where
 
 #include "errors.h"
 import Data.List(sort)
@@ -53,6 +54,9 @@
 test' :: Ord r => [a -> r] -> [a] -> TestTree' a
 test' [] _ =
   error "Test.QuickSpec.TestTree.test': ran out of test cases"
+test' (tc:tcs) [] =
+  error "Test.QuickSpec.TestTree.test': found an empty equivalence class"
+test' (tc:tcs) xs@[_] = tree xs tc [test' tcs xs]
 test' (tc:tcs) xs = tree xs tc (map (test' tcs) bs)
   where bs = partitionBy tc xs
 
@@ -72,9 +76,11 @@
 cutOff :: Int -> Int -> TestTree a -> TestResults a
 cutOff _ _ Nil = Results Nil
 cutOff m n (NonNil t) = Results (NonNil (aux m t))
-  where aux 0 t = aux' False n n t
+  where aux _ t@Tree{rest = []} = t { branches = [] }
+        aux 0 t = aux' False n n t
         aux m t = t { branches = map (aux (m-1)) (branches t) }
         -- Exponential backoff if we carry on refining a class
+        aux' _ _ _ t@Tree{rest = []} = t { branches = [] }
         aux' True 0 n t = t { branches = map (aux' False (n*2-1) (n*2)) (branches t) }
         aux' False 0 n t = t { branches = [] }
         aux' x m n t@Tree{branches = [t']} = t { branches = [aux' x (m-1) n t'] }
@@ -85,6 +91,13 @@
 numTests (Results (NonNil t)) = aux t
   where aux Tree{branches = []} = 0
         aux Tree{branches = bs} = 1 + maximum (map aux bs)
+
+numResults :: TestResults a -> Int
+numResults (Results Nil) = 0
+numResults (Results (NonNil t)) = aux t
+  where aux Tree{rest = []} = 0
+        aux Tree{rest = xs, branches = ts} =
+          1 + length xs + sum (map aux ts)
 
 classes :: Ord a => TestResults a -> [[a]]
 classes = sort . map sort . unsortedClasses
diff --git a/src/Test/QuickSpec/Utils/MemoValuation.hs b/src/Test/QuickSpec/Utils/MemoValuation.hs
--- a/src/Test/QuickSpec/Utils/MemoValuation.hs
+++ b/src/Test/QuickSpec/Utils/MemoValuation.hs
@@ -13,8 +13,8 @@
 import Test.QuickSpec.Utils.Typed
 import Test.QuickSpec.Utils.TypeRel
 
-memoValuation :: Sig -> (forall a. Variable a -> a) -> (forall a. Variable a -> a)
-memoValuation sig f = unsafeCoerce . unsafeAt arr . index . sym . unVariable
+memoValuation :: Sig -> Valuation -> Valuation
+memoValuation sig (Valuation f) = Valuation (unsafeCoerce . unsafeAt arr . index . sym . unVariable)
   where arr :: Array Int Any
         arr = array (0, maximum (0:map (some (index . sym . unVariable)) vars))
                 [(index (sym (unVariable v)), unsafeCoerce (f v))
diff --git a/src/Test/QuickSpec/Utils/TypeRel.hs b/src/Test/QuickSpec/Utils/TypeRel.hs
--- a/src/Test/QuickSpec/Utils/TypeRel.hs
+++ b/src/Test/QuickSpec/Utils/TypeRel.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
 module Test.QuickSpec.Utils.TypeRel where
 
-#include "../errors.h"
+#include "errors.h"
 import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
 import Test.QuickSpec.Utils.TypeMap(TypeMap)
 import Test.QuickSpec.Utils.Typed
diff --git a/src/Test/QuickSpec/Utils/Typed.hs b/src/Test/QuickSpec/Utils/Typed.hs
--- a/src/Test/QuickSpec/Utils/Typed.hs
+++ b/src/Test/QuickSpec/Utils/Typed.hs
@@ -1,15 +1,17 @@
 -- | Functions for working with existentially-quantified types
 --   and similar.
 
-{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}
+{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances, PatternGuards #-}
 module Test.QuickSpec.Utils.Typed where
 
-#include "../errors.h"
+#include "errors.h"
 import Control.Monad
 import Test.QuickSpec.Utils.Typeable
 import Data.Ord
 import Data.Function
 import Data.Maybe
+import Data.Typeable (TyCon)
+import Test.QuickSpec.Utils (usort)
 
 data Some f = forall a. Typeable a => Some (f a)
 
@@ -80,3 +82,10 @@
 rightArrow ty = snd (fromMaybe (ERROR msg) (splitArrow ty))
   where
     msg = "type oversaturated"
+
+typeRepTyCons :: TypeRep -> [TyCon]
+typeRepTyCons = usort . go where
+  go ty
+    | Just (t1,t2) <- splitArrow ty = go t1 ++ go t2
+    | (ty_con,ts) <- splitTyConApp ty = ty_con:concatMap go ts
+