diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -39,3 +39,4 @@
 proto/u-conjure
 test/expr
 test/conjurable
+test/utils
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,8 @@
 
 TESTS = \
   test/expr \
-  test/conjurable
+  test/conjurable \
+  test/utils
 
 all: mk/toplibs
 
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -4,18 +4,36 @@
 A non-exhaustive list of things TO DO for Conjure.
 
 
+* top-down generation of candidate expressions
+
+* generate functions with top-level case patterns:
+
+        len []  =  0
+        len (x:xs)  =  1 + len xs
+
+* only allow recursion on deconstructed arguments:
+
+        foo (x:xs)  =  ... len xs ...
+
+  this will require generation of functions with top-level case patterns.
+
+
 ### for later
 
-* allow conjuring from tests instead of partial definitions?
+* exclude magic numbers?  e.g.: `1+1`?
 
 * allow conjuring from partially defined implementations?
 
-    partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)
-    partial impl  =  f
-      where
-      f n  =  if n == 0
-              then 1
-              else impl f n
+        partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)
+        partial impl  =  f
+          where
+          f n  =  if n == 0
+                  then 1
+                  else impl f n
+
+* consider leveraging lazyness somehow?
+
+* consider leveraging polymorphism somehow?
 
 
 This file is part of Conjure,
diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime
--- a/bench/runtime/zero/bench/ill-hit.runtime
+++ b/bench/runtime/zero/bench/ill-hit.runtime
@@ -1,1 +1,1 @@
-2.26
+1.89
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
--- a/bench/runtime/zero/eg/bools.runtime
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -1,1 +1,1 @@
-7.78
+7.20
diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime
--- a/bench/runtime/zero/eg/factorial.runtime
+++ b/bench/runtime/zero/eg/factorial.runtime
@@ -1,1 +1,1 @@
-6.99
+7.18
diff --git a/bench/runtime/zero/eg/ints.runtime b/bench/runtime/zero/eg/ints.runtime
--- a/bench/runtime/zero/eg/ints.runtime
+++ b/bench/runtime/zero/eg/ints.runtime
@@ -1,1 +1,1 @@
-1.83
+1.84
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-10.71
+10.23
diff --git a/bench/runtime/zero/eg/spec.runtime b/bench/runtime/zero/eg/spec.runtime
--- a/bench/runtime/zero/eg/spec.runtime
+++ b/bench/runtime/zero/eg/spec.runtime
@@ -1,1 +1,1 @@
-1.63
+1.47
diff --git a/bench/runtime/zero/eg/tapps.runtime b/bench/runtime/zero/eg/tapps.runtime
--- a/bench/runtime/zero/eg/tapps.runtime
+++ b/bench/runtime/zero/eg/tapps.runtime
@@ -1,1 +1,1 @@
-0.96
+0.87
diff --git a/bench/runtime/zero/proto/u-conjure.runtime b/bench/runtime/zero/proto/u-conjure.runtime
--- a/bench/runtime/zero/proto/u-conjure.runtime
+++ b/bench/runtime/zero/proto/u-conjure.runtime
@@ -1,1 +1,1 @@
-0.10
+0.32
diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions
--- a/bench/runtime/zero/versions
+++ b/bench/runtime/zero/versions
@@ -1,4 +1,4 @@
 GHC 8.10.4
 leancheck-0.9.4
-express-0.1.8
+express-0.1.10
 speculate-0.4.6
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,14 @@
 ============================
 
 
+v0.2.6
+------
+
+* require Express v0.1.10 due to `hasHole` being now exported there
+* require Eq result on `conjure1`, `conjure2` and `conjure3`
+* code cleanup and more tests
+
+
 v0.2.4
 ------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.2.4
+version:             0.2.6
 synopsis:            conjure Haskell functions out of partial definitions
 description:
   Conjure is a tool that produces Haskell functions out of partial definitions.
@@ -65,7 +65,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.2.4
+  tag:             v0.2.6
 
 library
   exposed-modules: Conjure
@@ -79,14 +79,14 @@
                , leancheck >= 0.9.4
                , template-haskell
                , speculate >= 0.4.6
-               , express >= 0.1.8
+               , express >= 0.1.10
   hs-source-dirs:      src
   default-language:    Haskell2010
 
 test-suite expr
   type:                exitcode-stdio-1.0
   main-is:             expr.hs
-  other-modules:       Test
+  other-modules:       Test, Test.ListableExpr, Test.Candidates
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
@@ -94,7 +94,15 @@
 test-suite conjurable
   type:                exitcode-stdio-1.0
   main-is:             conjurable.hs
-  other-modules:       Test
+  other-modules:       Test, Test.ListableExpr, Test.Candidates
+  hs-source-dirs:      test
+  build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
+  default-language:    Haskell2010
+
+test-suite utils
+  type:                exitcode-stdio-1.0
+  main-is:             utils.hs
+  other-modules:       Test, Test.ListableExpr, Test.Candidates
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -147,6 +147,8 @@
   src/Conjure/Utils.hs
 test/conjurable.o: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   test/conjurable.hs \
   src/Conjure/Utils.hs \
   src/Conjure/Spec.hs \
@@ -156,10 +158,14 @@
   src/Conjure/Conjurable.hs
 test/conjurable: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   test/conjurable.hs \
   mk/toplibs
 test/expr.o: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   test/expr.hs \
   src/Conjure/Utils.hs \
   src/Conjure/Spec.hs \
@@ -169,10 +175,20 @@
   src/Conjure/Conjurable.hs
 test/expr: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   test/expr.hs \
   mk/toplibs
+test/Test/Candidates.o: \
+  test/Test/Candidates.hs \
+  src/Conjure/Utils.hs \
+  src/Conjure/Expr.hs
+test/Test/ListableExpr.o: \
+  test/Test/ListableExpr.hs
 test/Test.o: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   src/Conjure/Utils.hs \
   src/Conjure/Spec.hs \
   src/Conjure.hs \
@@ -181,4 +197,23 @@
   src/Conjure/Conjurable.hs
 test/Test: \
   test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
+  mk/toplibs
+test/utils.o: \
+  test/utils.hs \
+  test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs
+test/utils: \
+  test/utils.hs \
+  test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/Test/Candidates.hs \
   mk/toplibs
diff --git a/proto/u-conjure.hs b/proto/u-conjure.hs
--- a/proto/u-conjure.hs
+++ b/proto/u-conjure.hs
@@ -20,8 +20,10 @@
 import Data.List
 import Data.Maybe
 import Data.Express
+import Data.Typeable
 import Test.LeanCheck.Error
 
+
 square :: Int -> Int
 square 0  =  0
 square 1  =  1
@@ -35,37 +37,64 @@
 add 1 0  =  1
 add 1 1  =  2
 
-fact :: Int -> Int
-fact 0  =  1
-fact 1  =  1
-fact 2  =  2
-fact 3  =  6
-fact 4  =  24
+factorial :: Int -> Int
+factorial 0  =  1
+factorial 1  =  1
+factorial 2  =  2
+factorial 3  =  6
+factorial 4  =  24
 
 second :: [Int] -> Int
 second [x,y]  =  y
 second [x,y,z]  =  y
 second [x,y,z,w]  =  y
 
+-- reverse
+reverse' :: [Int] -> [Int]
+reverse' [x,y]  =  [y,x]
+reverse' [x,y,z]  =  [z,y,x]
+
+-- ++
+(+++) :: [Int] -> [Int] -> [Int]
+[x] +++ [y]  =  [x,y]
+[x,y] +++ [z,w]  =  [x,y,z,w]
+
+
 main :: IO ()
 main  =  do
-  value "square" (square :: Int -> Int) `conjureFrom` intBackground
-  value "add" (add :: Int -> Int -> Int) `conjureFrom` intBackground
-  value "fact" (fact :: Int -> Int) `conjureFrom` intBackground
+  conjure "square"    square    primitives
+  conjure "add"       add       primitives
+  conjure "factorial" factorial primitives
 
-  value "==>" (==>) `conjureFrom`
-    [ val False
-    , val True
-    , value "not" not
-    , value "&&" (&&)
-    , value "||" (||)
+  conjure "factorial"   factorial
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "*" ((*) :: Int -> Int -> Int)
+    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
+    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])
     ]
 
-  value "second" (second :: [Int] -> Int) `conjureFrom` listBackground
-  value "reverse" (reverse :: [Int] -> [Int]) `conjureFrom` listBackground
+  conjure "second"  second   listPrimitives
+  conjure "++"      (+++)    listPrimitives
+  conjure "reverse" reverse' listPrimitives
+
+  -- even by using fold and some cheating,
+  -- this function is out of reach
+  --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs
+  --  reverse xs  =  foldr (flip (++) . unit) [] xs
+  conjure "reverse" reverse' $ listPrimitives ++
+    [ value "unit" ((:[]) :: Int -> [Int])
+    , value "++" ((++) :: [Int] -> [Int] -> [Int])
+    -- these last two are cheats:
+    , value "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])
+    , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])
+    ]
+
   where
-  intBackground :: [Expr]
-  intBackground  =
+
+  primitives :: [Expr]
+  primitives =
     [ val (0 :: Int)
     , val (1 :: Int)
     , val (2 :: Int)
@@ -74,67 +103,65 @@
     , value "*" ((*) :: Int -> Int -> Int)
     , value "-" ((-) :: Int -> Int -> Int)
     ]
-  listBackground :: [Expr]
-  listBackground  =
+
+  listPrimitives :: [Expr]
+  listPrimitives =
     [ val (0 :: Int)
     , val (1 :: Int)
     , val ([] :: [Int])
     , value "head" (head :: [Int] -> Int)
     , value "tail" (tail :: [Int] -> [Int])
     , value ":" ((:) :: Int -> [Int] -> [Int])
-    , value "++" ((++) :: [Int] -> [Int] -> [Int])
+    , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
     ]
 
 
-conjureFrom :: Expr -> [Expr] -> IO ()
-ff `conjureFrom` es  =  do
-  print ff  -- prints the type signature
-  case rs of
+conjure :: Typeable f => String -> f -> [Expr] -> IO ()
+conjure nm f primitives  =  do
+  print (value nm f) -- prints the type signature
+  case conjureImplementations nm f primitives of
     []    -> putStrLn $ "cannot conjure"
 --  es    -> putStrLn $ unlines $ map showEq es  -- uncomment to show all found variations
     (e:_) -> putStrLn $ showEq e
   putStrLn ""
   where
-  nm (Value s _)  =  s
-  rrff  =  ('_':nm ff) `varAsTypeOf` ff
-  rs  =  [ ffxx -==- e
-         | e <- candidateExprsFrom $ [rrff] ++ xxs ++ filter isGround es
-         , isWellTyped (ffxx -==- e)
-         , isTrue (ffxx -==- e)
-         , isDefined e
-         ]
-  ffxx  =  mostGeneralCanonicalVariation
-        .  fromJust
-        $  application ff es
-  (_:xxs)  =  unfoldApp ffxx
   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
 
 
-application :: Expr -> [Expr] -> Maybe Expr
-application ff es  =  appn ff
+conjureImplementations :: Typeable f => String -> f -> [Expr] -> [Expr]
+conjureImplementations nm f primitives  =
+  [ appn -==- e
+  | e <- candidateExprsFrom $ exs ++ primitives
+  , isTrue (appn -==- e)
+  ]
   where
-  appn ff
-    | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of
-                    [] -> Nothing  -- could not find type representative in es
-                    (e:_) -> appn (ff :$ holeAsTypeOf e)
-    | otherwise  =  Just ff
+  appn  =  application nm f primitives
+  (ef:exs)  =  unfoldApp appn
+  isTrue e  =  all (errorToFalse . eval False) . map (e //-) $ definedBinds appn
 
 
-candidateExprsFrom :: [Expr] -> [Expr]
-candidateExprsFrom  =  concat . take 6 . expressionsT
+definedBinds :: Expr -> [[(Expr,Expr)]]
+definedBinds ffxx  =  [bs | bs <- bss, errorToFalse . eval False $ e //- bs]
   where
-  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)
-    where
-    es = expressionsT ds
+  e  =  ffxx -==- ffxx
+  bss  =  take 360 $ groundBinds ffxx
 
 
-isTrue :: Expr -> Bool
-isTrue  =  all (errorToTrue . eval False) . take 60 . grounds
+application :: Typeable f => String -> f -> [Expr] -> Expr
+application nm f es  =  mostGeneralCanonicalVariation $ appn (value nm f)
+  where
+  appn ff | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of
+                          [] -> error "application: could not find type representative"
+                          (e:_) -> appn (ff :$ holeAsTypeOf e)
+          | otherwise  =  ff
 
 
--- checks if a function is defined for at least one combination of argument values
-isDefined :: Expr -> Bool
-isDefined e  =  any (isJust . errorToNothing . eval False) . take 60 . grounds $ (e -==- e)
+candidateExprsFrom :: [Expr] -> [Expr]
+candidateExprsFrom  =  concat . take 7 . expressionsT
+  where
+  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)
+    where
+    es = expressionsT ds
 
 
 (-==-) :: Expr -> Expr -> Expr
@@ -148,14 +175,14 @@
   headOr x []     =  x
   headOr _ (x:_)  =  x
 
+
 lhs, rhs :: Expr -> Expr
 lhs (((Value "==" _) :$ e) :$ _)  =  e
 rhs (((Value "==" _) :$ _) :$ e)  =  e
 
 
-grounds :: Expr -> [Expr]
-grounds e  =  map (e //-)  .  concat
-           $  products [mapT ((,) v) (tiersFor v) | v <- nubVars e]
+groundBinds :: Expr -> [[(Expr,Expr)]]
+groundBinds e  =  concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]
 
 
 tiersFor :: Expr -> [[Expr]]
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -10,35 +10,82 @@
 -- (a.k.a.: functional inductive programming)
 {-# LANGUAGE CPP, RecordWildCards, TupleSections #-}
 module Conjure.Engine
-  ( module Data.Express
-  , module Data.Express.Fixtures
-  , module Test.Speculate.Engine
-  , module Test.Speculate.Reason
+  ( conjure
+  , conjureWithMaxSize
   , Args(..)
   , args
-  , conjure
   , conjureWith
-  , conjureWithMaxSize
   , conjpure
   , conjpureWith
   , candidateExprs
+  , module Data.Express
+  , module Data.Express.Fixtures
+  , module Test.Speculate.Engine
+  , module Test.Speculate.Reason
   )
 where
 
 import Data.Express
 import Data.Express.Fixtures hiding ((-==-))
-import qualified Data.Ratio
-import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
+
+import Test.LeanCheck
 import Test.LeanCheck.Tiers
-import Test.Speculate hiding ((===), Args(..), args)
-import Test.Speculate.Reason
-import Test.Speculate.Engine
-import Test.Speculate.Expr
-import System.IO
+import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
 
+import Test.Speculate.Reason (isRootNormalE)
+import Test.Speculate.Engine (theoryFromAtoms, groundBinds)
+
 import Conjure.Expr
 import Conjure.Conjurable
 
+
+-- | Conjures an implementation of a partially defined function.
+--
+-- Takes a 'String' with the name of a function,
+-- a partially-defined function from a conjurable type,
+-- and a list of building blocks encoded as 'Expr's.
+--
+-- For example, given:
+--
+-- > square :: Int -> Int
+-- > square 0  =  0
+-- > square 1  =  1
+-- > square 2  =  4
+-- >
+-- > primitives :: [Expr]
+-- > primitives =
+-- >   [ val (0::Int)
+-- >   , val (1::Int)
+-- >   , value "+" ((+) :: Int -> Int -> Int)
+-- >   , value "*" ((*) :: Int -> Int -> Int)
+-- > ]
+--
+-- The conjure function does the following:
+--
+-- > > conjure "square" square primitives
+-- > square :: Int -> Int
+-- > -- testing 3 combinations of argument values
+-- > -- looking through 3 candidates of size 1
+-- > -- looking through 3 candidates of size 2
+-- > -- looking through 5 candidates of size 3
+-- > square x  =  x * x
+--
+-- The primitives list is defined with 'val' and 'value'.
+conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
+conjure  =  conjureWith args
+
+
+-- | Like 'conjure' but allows setting the maximum size of considered expressions
+--   instead of the default value of 12.
+--
+-- > conjureWithMaxSize 10 "function" function [...]
+conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()
+conjureWithMaxSize sz  =  conjureWith args
+                       {  maxSize = sz
+                       ,  maxEquationSize = min sz (maxEquationSize args)
+                       }
+
+
 -- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.
 --   See 'args' for the defaults.
 data Args = Args
@@ -51,6 +98,7 @@
   , forceTests :: [[Expr]]  -- ^ force tests
   }
 
+
 -- | Default arguments to conjure.
 --
 -- * 60 tests
@@ -70,6 +118,29 @@
   , forceTests         =  []
   }
 
+
+-- | Like 'conjure' but allows setting options through 'Args'/'args'.
+--
+-- > conjureWith args{maxSize = 11} "function" function [...]
+conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
+conjureWith args nm f es  =  do
+  print (var (head $ words nm) f)
+  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
+  pr 1 rs
+  where
+  pr n []  =  putStrLn $ "cannot conjure"
+  pr n ((is,cs,es):rs)  =  do
+    putStrLn $ "-- looking through "
+            ++ show (length cs) ++ "/" ++ show (length es)
+            ++ " candidates of size " ++ show n
+    case is of
+      []     ->  pr (n+1) rs
+      (i:_)  ->  do putStrLn $ showEq i
+                    putStrLn ""
+  rs  =  zip3 iss css ess
+  (iss, css, ess, ts)  =  conjpureWith args nm f es
+
+
 -- | Like 'conjure' but in the pure world.
 --
 -- Returns a triple with:
@@ -81,6 +152,7 @@
 conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
 conjpure =  conjpureWith args
 
+
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
 conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
 conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, allCandidatesT, tests)
@@ -111,75 +183,7 @@
     where
     e  =  ffxx -==- ffxx
 
--- | Conjures an implementation of a partially defined function.
---
--- Takes a 'String' with the name of a function,
--- a partially-defined function from a conjurable type,
--- and a list of building blocks encoded as 'Expr's.
---
--- For example, given:
---
--- > square :: Int -> Int
--- > square 0  =  0
--- > square 1  =  1
--- > square 2  =  4
--- >
--- > primitives :: [Expr]
--- > primitives =
--- >   [ val (0::Int)
--- >   , val (1::Int)
--- >   , value "+" ((+) :: Int -> Int -> Int)
--- >   , value "*" ((*) :: Int -> Int -> Int)
--- > ]
---
--- The conjure function does the following:
---
--- > > conjure "square" square primitives
--- > square :: Int -> Int
--- > -- testing 3 combinations of argument values
--- > -- looking through 3 candidates of size 1
--- > -- looking through 3 candidates of size 2
--- > -- looking through 5 candidates of size 3
--- > square x  =  x * x
---
--- The primitives list is defined with 'val' and 'value'.
-conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
-conjure  =  conjureWith args
 
--- | Like 'conjure' but allows setting the maximum size of considered expressions
---   instead of the default value of 9.
---
--- > conjureWithMaxSize 10 "function" function [...]
-conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()
-conjureWithMaxSize sz  =  conjureWith args
-                       {  maxSize = sz
-                       ,  maxEquationSize = min sz (maxEquationSize args)
-                       }
-
-
-
--- | Like 'conjure' but allows setting options through 'Args'/'args'.
---
--- > conjureWith args{maxSize = 11} "function" function [...]
-conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
-conjureWith args nm f es  =  do
-  print (var (head $ words nm) f)
-  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
-  pr 1 rs
-  where
-  pr n []  =  putStrLn $ "cannot conjure"
-  pr n ((is,cs,es):rs)  =  do
-    putStrLn $ "-- looking through "
-            ++ show (length cs) ++ "/" ++ show (length es)
-            ++ " candidates of size " ++ show n
-    case is of
-      []     ->  pr (n+1) rs
-      (i:_)  ->  do putStrLn $ showEq i
-                    putStrLn ""
-  rs  =  zip3 iss css ess
-  (iss, css, ess, ts)  =  conjpureWith args nm f es
-  showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
-
 candidateExprs :: Conjurable f
                => String -> f
                -> Int
@@ -190,6 +194,7 @@
 candidateExprs nm f sz mc (===) es  =
   candidateExprsT nm f sz mc (===) [nub $ es ++ conjureIfs f]
 
+
 candidateExprsT :: Conjurable f
                 => String -> f
                 -> Int
@@ -197,44 +202,42 @@
                 -> (Expr -> Expr -> Bool)
                 -> [[Expr]]
                 -> [[Expr]]
-candidateExprsT nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess
+candidateExprsT nm f sz mc (===) ess  =
+  candidateExprsTT keep $ [ef:exs] \/ ess
   where
   (ef:exs)  =  unfoldApp $ conjureVarApplication nm f
+  keep e  =  isRootNormalE thy e && count (== ef) (vars e) <= mc
+  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f ++ falseAndTrue]
+                                  \/ filterT (`notElem` falseAndTrue) ess
   falseAndTrue  =  [val False, val True]
-  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f ++ falseAndTrue] \/ filterT (`notElem` falseAndTrue) ess
-  nubET  =  id -- no nub, good enough results
-  -- nubET  =  discardLaterT (===) -- huge computational cost
-  expressionsT ds  =  nubET
-                   $  filterT (\e -> count (== ef) (vars e) <= mc)
-                   $  filterT (isRootNormalE thy)
-                   $  ds \/ (delay $ productMaybeWith ($$) es es)
-    where
-    es = expressionsT ds
 
-lhs, rhs :: Expr -> Expr
-lhs (((Value "==" _) :$ e) :$ _)  =  e
-rhs (((Value "==" _) :$ _) :$ e)  =  e
 
-compareResult :: (Int,Expr) -> (Int,Expr) -> Ordering
-compareResult (n1,e1) (n2,e2)  =  n2 `compare` n1
-                               <> e1 `compareSimplicity` e2
+candidateExprsTT :: (Expr -> Bool) -> [[Expr]] -> [[Expr]]
+candidateExprsTT keep  =  exprT
+  where
+  exprT ess  =  filterT keep
+             $  ess \/ (delay $ productMaybeWith ($$) rss rss)
+    where
+    rss = exprT ess
 
-(%) :: Int -> Int -> Int
-x % y  =  x * 100 `div` y
 
--- Debug: application that always works
-(*$$*) :: Expr -> Expr -> Maybe Expr
-e1 *$$* e2  =  Just $ e1 :$ e2
-
--- Debug: application that works for the correct kinds
-(>$$<) :: Expr -> Expr -> Maybe Expr
-e1 >$$< e2  =  if isFunTy t1 && tyArity (argumentTy t1) == tyArity t2
-               then Just $ e1 :$ e2
-               else Nothing
+candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
+candidatesTD keep h primitives  =  filterT (not . hasHole)
+                                $  town [[h]]
   where
-  t1  =  ktyp e1
-  t2  =  ktyp e2
+  most = mostGeneralCanonicalVariation
 
-ktyp :: Expr -> TypeRep
-ktyp (e1 :$ e2)  =  resultTy (ktyp e1)
-ktyp e  =  typ e
+  town :: [[Expr]] -> [[Expr]]
+  town ((e:es):ess) | keep (most e)  =  [[e]] \/ town (expand e \/ (es:ess))
+                    | otherwise      =  town (es:ess)
+  town ([]:ess)  =  []:town ess
+  town []  =  []
+
+  expand :: Expr -> [[Expr]]
+  expand e  =  case holesBFS e of
+    [] -> []
+    (h:_) -> mapT (fillBFS e) (replacementsFor h)
+
+  replacementsFor :: Expr -> [[Expr]]
+  replacementsFor h  =  filterT (\e -> typ e == typ h)
+                     $  primitiveApplications primitives
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
--- a/src/Conjure/Expr.hs
+++ b/src/Conjure/Expr.hs
@@ -11,6 +11,7 @@
   ( module Data.Express
   , module Data.Express.Fixtures
 
+  , (>$$<)
   , funToVar
   , recursexpr
   , apparentlyTerminates
@@ -18,6 +19,16 @@
   , applicationOld
   , compareSimplicity
   , ifFor
+  , primitiveHoles
+  , primitiveApplications
+  , valuesBFS
+  , holesBFS
+  , fillBFS
+  , showEq
+  , lhs
+  , rhs
+  , ($$**)
+  , ($$|<)
 
   , module Conjure.Utils
   )
@@ -26,6 +37,7 @@
 import Conjure.Utils
 
 import Data.Express
+import Data.Express.Utils.Typeable
 import Data.Express.Fixtures hiding ((-==-))
 
 -- | /O(n)/.
@@ -172,3 +184,78 @@
 -- if you want recursive functions to be considered and produced.
 ifFor :: Typeable a => a -> Expr
 ifFor a  =  value "if" (\p x y -> if p then x else y `asTypeOf` a)
+
+-- | Application cross-product between lists of Exprs
+(>$$<) :: [Expr] -> [Expr] -> [Expr]
+exs >$$< eys  =  catMaybes [ex $$ ey | ex <- exs, ey <- eys]
+-- TODO: move >$$< into Data.Express?
+
+primitiveHoles :: [Expr] -> [Expr]
+primitiveHoles prims  =  sort $ ph hs
+  where
+  hs  =  nub $ map holeAsTypeOf prims
+  ph  =  iterateUntil (==) ps
+  ps es  =  nub $ es ++ sq es
+  sq es  =  nub $ map holeAsTypeOf $ es >$$< es
+-- FIXME: the function above is quite inefficient.
+--        Should run fast for a small number of types,
+--        but if this number increases runtime may start
+--        to become significant.
+
+primitiveApplications :: [Expr] -> [[Expr]]
+primitiveApplications prims  =  takeWhile (not . null)
+                             $  iterate (>$$< primitiveHoles prims) prims
+
+-- lists terminal values in BFS order
+valuesBFS :: Expr -> [Expr]
+valuesBFS  =  concat . bfs
+  where
+  bfs :: Expr -> [[Expr]]
+  bfs (ef :$ ex)  =  [] : mzip (bfs ef) (bfs ex)
+  bfs e  =  [[e]]
+
+-- lists holes in BFS order
+holesBFS :: Expr -> [Expr]
+holesBFS  =  filter isHole . valuesBFS
+
+fillBFS :: Expr -> Expr -> Expr
+fillBFS e e'  =  fst (f e)
+  where
+  f :: Expr -> (Expr,Maybe Int)
+  f (ef :$ ex)  =  case (mf, mx) of
+    (Nothing, Nothing)             -> (ef :$ ex, Nothing)
+    (Just lf, Nothing)             -> (ef' :$ ex, Just $ lf+1)
+    (Nothing, Just lx)             -> (ef :$ ex', Just $ lx+1)
+    (Just lf, Just lx) | lf <= lx  -> (ef' :$ ex, Just $ lf+1)
+                       | otherwise -> (ef :$ ex', Just $ lx+1)
+    where
+    (ef', mf)  =  f ef
+    (ex', mx)  =  f ex
+  f e | isHole e && typ e == typ e'  =  (e', Just 0)
+      | otherwise                    =  (e, Nothing)
+-- TODO: move BFS functions into Express?
+
+showEq :: Expr -> String
+showEq (((Value "==" _) :$ lhs) :$ rhs)  =  showExpr lhs ++ "  =  " ++ showExpr rhs
+showEq e  =  "not an Eq: " ++ show e
+
+lhs, rhs :: Expr -> Expr
+lhs (((Value "==" _) :$ e) :$ _)  =  e
+rhs (((Value "==" _) :$ _) :$ e)  =  e
+
+-- Debug: application that always works
+($$**) :: Expr -> Expr -> Maybe Expr
+e1 $$** e2  =  Just $ e1 :$ e2
+
+-- Debug: application that works for the correct kinds
+($$|<) :: Expr -> Expr -> Maybe Expr
+e1 $$|< e2  =  if isFunTy t1 && tyArity (argumentTy t1) == tyArity t2
+               then Just $ e1 :$ e2
+               else Nothing
+  where
+  t1  =  ktyp e1
+  t2  =  ktyp e2
+
+  ktyp :: Expr -> TypeRep
+  ktyp (e1 :$ e2)  =  resultTy (ktyp e1)
+  ktyp e  =  typ e
diff --git a/src/Conjure/Spec.hs b/src/Conjure/Spec.hs
--- a/src/Conjure/Spec.hs
+++ b/src/Conjure/Spec.hs
@@ -97,7 +97,7 @@
 -- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
 --
 -- (cf. 'Spec1', 'conjure1With')
-conjure1 :: (Eq a, Show a, Conjurable a, Conjurable b)
+conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b)
          => String -> Spec1 a b -> [Expr] -> IO ()
 conjure1  =  conjure1With args
 
@@ -133,7 +133,7 @@
 -- (cf. 'Spec2', 'conjure2With')
 conjure2 :: ( Conjurable a, Eq a, Show a
             , Conjurable b, Eq b, Show b
-            , Conjurable c
+            , Conjurable c, Eq c
             ) => String -> Spec2 a b c -> [Expr] -> IO ()
 conjure2  =  conjure2With args
 
@@ -144,13 +144,13 @@
 conjure3 :: ( Conjurable a, Eq a, Show a
             , Conjurable b, Eq b, Show b
             , Conjurable c, Eq c, Show c
-            , Conjurable d
+            , Conjurable d, Eq d
             ) => String -> Spec3 a b c d -> [Expr] -> IO ()
 conjure3  =  conjure3With args
 
 
 -- | Like 'conjure1' but allows setting options through 'Args'/'args'.
-conjure1With :: (Eq a, Show a, Conjurable a, Conjurable b)
+conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b)
              => Args -> String -> Spec1 a b -> [Expr] -> IO ()
 conjure1With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun1 bs)
   where
@@ -160,7 +160,7 @@
 -- | Like 'conjure2' but allows setting options through 'Args'/'args'.
 conjure2With :: ( Conjurable a, Eq a, Show a
                 , Conjurable b, Eq b, Show b
-                , Conjurable c
+                , Conjurable c, Eq c
                 ) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()
 conjure2With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun2 bs)
   where
@@ -171,7 +171,7 @@
 conjure3With :: ( Conjurable a, Eq a, Show a
                 , Conjurable b, Eq b, Show b
                 , Conjurable c, Eq c, Show c
-                , Conjurable d
+                , Conjurable d, Eq d
                 ) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()
 conjure3With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun3 bs)
   where
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -18,6 +18,8 @@
 
   , count
   , nubOn
+  , iterateUntil
+  , mzip
   )
 where
 
@@ -33,3 +35,17 @@
 
 nubOn :: Eq b => (a -> b) -> [a] -> [a]
 nubOn f  =  nubBy ((==) `on` f)
+
+iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
+iterateUntil (?) f  =  iu
+  where
+  iu x | x ? fx     =  x
+       | otherwise  =  iu fx
+    where
+    fx  =  f x
+
+mzip :: Monoid a => [a] -> [a] -> [a]
+mzip [] []  =  []
+mzip [] ys  =  ys
+mzip xs []  =  xs
+mzip (x:xs) (y:ys)  =  x <> y : mzip xs ys
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -11,6 +11,9 @@
   , module Conjure.Expr
   , module Conjure.Conjurable
   , module Test.LeanCheck
+  , module Test.LeanCheck.Utils
+  , module Test.ListableExpr
+  , module Test.Candidates
 
   , mainTest
   )
@@ -20,6 +23,9 @@
 import System.Environment (getArgs)
 
 import Test.LeanCheck
+import Test.LeanCheck.Utils
+import Test.ListableExpr
+import Test.Candidates
 
 import Conjure
 import Conjure.Expr hiding (delete, insert)
diff --git a/test/Test/Candidates.hs b/test/Test/Candidates.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Candidates.hs
@@ -0,0 +1,60 @@
+-- |
+-- Module      : TEst.Candidates
+-- Copyright   : (c) 2021 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- Reference implementations of candidate generation.
+--
+-- Bottom-up and top-down
+module Test.Candidates
+  ( boupCandidates
+  , townCandidates
+  , dropTrail
+  )
+where
+
+import Conjure.Expr
+import Test.LeanCheck
+
+boupCandidates :: Expr -> [Expr] -> [[Expr]]
+boupCandidates appn primitives  =  dropTrail $ filterT (\e -> typ e == typ appn) boup
+  where
+  boup :: [[Expr]]
+  boup = expressionsT [primitives]
+
+  expressionsT ds  =  ds \/ (delay $ productMaybeWith ($$) es es)
+    where
+    es = expressionsT ds
+
+townCandidates :: Expr -> [Expr] -> [[Expr]]
+townCandidates appn primitives  =  normalizeT
+                                $  filterT (not . hasHole)
+                                $  town [[holeAsTypeOf appn]]
+  where
+  town :: [[Expr]] -> [[Expr]]
+  town ((e:es):ess)  =  [[e]] \/ town (expand e \/ (es:ess))
+  town ([]:ess)  =  []:town ess
+  town []  =  []
+
+  expand :: Expr -> [[Expr]]
+  expand e  =  case holesBFS e of
+    [] -> []
+    (h:_) -> mapT (fillBFS e) (replacementsFor h)
+
+  replacementsFor :: Expr -> [[Expr]]
+  replacementsFor h  =  filterT (\e -> typ e == typ h)
+                     $  primitiveApplications primitives
+
+-- like normalizeT, but considers 6 empty tiers as an infinite trail of tiers
+-- this should only be used on testing
+dropTrail :: [[a]] -> [[a]]
+dropTrail []  =  []
+dropTrail [[]]  =  []
+dropTrail [[],[]]  =  []
+dropTrail [[],[],[]]  =  []
+dropTrail [[],[],[],[]]  =  []
+dropTrail [[],[],[],[],[]]  =  []
+dropTrail [[],[],[],[],[],[]]  =  []
+dropTrail ([]:[]:[]:[]:[]:[]:_)  =   []
+dropTrail (xs:xss)  =  xs:dropTrail xss
diff --git a/test/Test/ListableExpr.hs b/test/Test/ListableExpr.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/ListableExpr.hs
@@ -0,0 +1,285 @@
+-- |
+-- Module      : Test.ListableExpr
+-- Copyright   : (c) 2019-2021 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- This module exports a 'Listable' 'Expr' instance.
+-- This instance does not, by any means, list all possible expressions.
+-- It lists expressions based on a subset of the symbols exported by
+-- "Data.Express.Fixtures".
+--
+-- This is only intended to be used for testing,
+-- so this will not be exported on @ express.cabal @.
+module Test.ListableExpr
+  (
+  -- * The Expr type
+    Expr
+
+  -- * Expressions of a type
+  , IntE (..)
+  , BoolE (..)
+  , IntsE (..)
+  , CharE (..)
+
+  , IntE0 (..)
+  , IntEV (..)
+  , BoolE0 (..)
+  , BoolEV (..)
+  , IntsE0 (..)
+  , IntsEV (..)
+  , CharE0 (..)
+  , CharEV (..)
+
+  -- ** Functional values
+  , IntToIntE (..)
+  , IntToIntToIntE (..)
+  , BoolToBoolE (..)
+  , BoolToBoolToBoolE (..)
+
+  , SameTypeE (..)
+  , unSameTypeE
+  , SameTypedPairsE (..)
+
+  -- * Terminal expressions
+  , E0 (..)
+  , EV (..)
+
+  -- * Ill typed expressions
+  , Ill (..)
+  )
+where
+
+-- TODO: StringE
+
+import Test.LeanCheck
+import Test.LeanCheck.Function.ShowFunction
+import Data.Express.Fixtures
+import Data.Function (on)
+
+-- | Terminal constants.
+newtype E0  =  E0 { unE0 :: Expr }
+
+-- | Variables.
+newtype EV  =  EV { unEV :: Expr }
+
+-- | Expression of 'Int' type.
+newtype IntE  =  IntE { unIntE :: Expr }
+
+-- | Constant terminal value of 'Int' type.
+newtype IntE0  =  IntE0 { unIntE0 :: Expr }
+
+-- | Variable of 'Int' type.
+newtype IntEV  =  IntEV { unIntEV :: Expr }
+
+-- | Functions from Int to Int
+newtype IntToIntE  =  IntToIntE { unIntToIntE :: Expr }
+newtype IntToIntToIntE  =  IntToIntToIntE { unIntToIntToIntE :: Expr }
+
+-- | Expression of 'Bool' type.
+newtype BoolE  =  BoolE { unBoolE :: Expr }
+
+-- | Constant terminal value of 'Bool' type.
+newtype BoolE0  =  BoolE0 { unBoolE0 :: Expr }
+
+-- | Varialbe of 'Bool' type.
+newtype BoolEV  =  BoolEV { unBoolEV :: Expr }
+
+-- | Functions from Bool to Bool
+newtype BoolToBoolE  =  BoolToBoolE { unBoolToBoolE :: Expr }
+newtype BoolToBoolToBoolE  =  BoolToBoolToBoolE { unBoolToBoolToBoolE :: Expr }
+
+newtype CharE  =  CharE { unCharE :: Expr }
+
+newtype CharE0  =  CharE0 { unCharE0 :: Expr }
+
+newtype CharEV  =  CharEV { unCharEV :: Expr }
+
+data SameTypeE  =  SameTypeE Expr Expr
+
+unSameTypeE :: SameTypeE -> (Expr,Expr)
+unSameTypeE (SameTypeE e1 e2)  =  (e1,e2)
+
+data SameTypedPairsE  =  SameTypedPairsE { unSameTypedPairsE :: [(Expr,Expr)] }
+
+-- | Ill typed expressions.
+newtype Ill  =  Ill { unIll :: Expr }
+
+
+instance Show E0  where  show (E0 e) = show e
+instance Show EV  where  show (EV e) = show e
+
+instance Show IntE  where  show (IntE e) = show e
+
+instance Show IntE0  where  show (IntE0 e) = show e
+instance Show IntEV  where  show (IntEV e) = show e
+
+instance Show IntToIntE  where  show (IntToIntE e) = show e
+instance Show IntToIntToIntE  where  show (IntToIntToIntE e) = show e
+
+instance Show BoolE  where  show (BoolE e) = show e
+
+instance Show BoolE0  where  show (BoolE0 e) = show e
+instance Show BoolEV  where  show (BoolEV e) = show e
+
+instance Show BoolToBoolE  where  show (BoolToBoolE e) = show e
+instance Show BoolToBoolToBoolE  where  show (BoolToBoolToBoolE e) = show e
+
+instance Show IntsE  where  show (IntsE e) = show e
+
+instance Show IntsE0  where  show (IntsE0 e) = show e
+instance Show IntsEV  where  show (IntsEV e) = show e
+
+instance Show CharE  where  show (CharE e) = show e
+
+instance Show CharE0  where  show (CharE0 e) = show e
+instance Show CharEV  where  show (CharEV e) = show e
+
+instance Show SameTypeE  where  show (SameTypeE e1 e2) = show (e1,e2)
+
+instance Show SameTypedPairsE  where  show (SameTypedPairsE ees)  =  show ees
+
+-- | Expression of 'Ints' type.
+newtype IntsE  =  IntsE { unIntsE :: Expr }
+
+-- | Constant terminal value of 'Ints' type.
+newtype IntsE0  =  IntsE0 { unIntsE0 :: Expr }
+
+-- | Varialbe of 'Ints' type.
+newtype IntsEV  =  IntsEV { unIntsEV :: Expr }
+
+instance Show Ill where  show (Ill e) = show e
+
+instance Listable IntE  where
+  tiers  =  mapT IntE
+         $  cons0 i_
+         \/ cons1 unIntEV
+         \/ cons1 unIntE0
+         \/ cons2 (\(IntToIntE f) (IntE xx) -> f :$ xx)
+         \/ cons1 (head' . unIntsE) `ofWeight` 2
+         \/ cons1 (ord' . unCharE) `ofWeight` 2
+
+instance Listable IntE0 where
+  tiers  =  (IntE0 . val) `mapT` (tiers :: [[Int]])
+
+instance Listable IntEV where
+  list  =  map IntEV $ listVars "x" (undefined :: Int)
+
+instance Listable IntToIntE where
+  tiers  =  mapT IntToIntE
+         $  cons0 idE
+         \/ cons0 negateE `addWeight` 1
+         \/ cons0 absE    `addWeight` 1
+         \/ cons2 (\(IntToIntToIntE ef) (IntE ex) -> ef :$ ex)
+         \/ toTiers (listVars "f" (undefined :: Int -> Int)) `addWeight` 2
+
+instance Listable IntToIntToIntE where
+  list  =  map IntToIntToIntE [plus, times]
+
+instance Listable IntsE  where
+  tiers  =  mapT IntsE
+         $  cons0 is_
+         \/ cons1 unIntsEV
+         \/ cons1 unIntsE0
+         \/ cons2 (\(IntE ex) (IntsE exs) -> ex -:- exs)
+         \/ cons1 (tail' . unIntsE) `ofWeight` 2
+         \/ cons2 (\(IntsE exs) (IntsE eys) -> exs -++- eys) `ofWeight` 2
+         \/ cons1 (\(IntsE exs) -> sort' exs) `ofWeight` 3
+         \/ cons2 (\(IntE ex) (IntsE exs) -> insert' ex exs) `ofWeight` 3
+
+instance Listable IntsE0 where
+  tiers  =  (IntsE0 . val) `mapT` (tiers :: [[ [Int] ]])
+
+instance Listable IntsEV where
+  list  =  map IntsEV $ listVars "xs" (undefined :: [Int])
+
+instance Listable BoolE  where
+  tiers  =  mapT BoolE
+         $  cons0 b_
+         \/ cons1 unBoolEV
+         \/ cons1 unBoolE0
+         \/ cons2 (\(BoolToBoolE ef) (BoolE ep) -> ef :$ ep)
+         \/ cons2 ((-==-) `on` unIntE)  `addWeight` 2
+         \/ cons2 ((-==-) `on` unBoolE) `addWeight` 2
+         \/ cons2 ((-<=-) `on` unIntE)  `addWeight` 3
+         \/ cons2 ((-<=-) `on` unBoolE) `addWeight` 3
+         \/ cons2 ((-<-)  `on` unIntE)  `addWeight` 4
+         \/ cons2 ((-<-)  `on` unBoolE) `addWeight` 4
+         \/ cons2 ((-/=-) `on` unIntE)  `addWeight` 5
+         \/ cons2 ((-/=-) `on` unBoolE) `addWeight` 5
+         \/ cons1 (odd'  . unIntE) `addWeight` 2
+         \/ cons1 (even' . unIntE) `addWeight` 2
+         \/ cons2 (\(IntE ex) (IntsE exs) -> elem' ex exs) `addWeight` 2
+
+instance Listable BoolE0 where
+  tiers  =  (BoolE0 . val) `mapT` (tiers :: [[Bool]])
+
+instance Listable BoolEV where
+  list  =  map BoolEV $ listVars "p" (undefined :: Bool)
+
+instance Listable BoolToBoolE where
+  tiers  =  mapT BoolToBoolE
+         $  cons0 notE
+         \/ cons2 (\(BoolToBoolToBoolE ef) (BoolE ex) -> ef :$ ex)
+
+instance Listable BoolToBoolToBoolE where
+  list  =  map BoolToBoolToBoolE [orE, andE, implies]
+
+instance Listable CharE where
+  tiers  =  mapT CharE $ cons0 c_
+                      \/ cons1 unCharEV
+                      \/ cons1 unCharE0
+
+instance Listable CharEV where
+  list  =  map CharEV $ listVars "c" (undefined :: Char)
+
+instance Listable CharE0 where
+  tiers  =  (CharE0 . val) `mapT` (tiers :: [[Char]])
+
+instance Listable SameTypeE where
+  tiers = cons1 (\(IntE  e1, IntE  e2) -> SameTypeE e1 e2) `ofWeight` 0
+       \/ cons1 (\(BoolE e1, BoolE e2) -> SameTypeE e1 e2) `ofWeight` 1
+       \/ cons1 (\(IntsE e1, IntsE e2) -> SameTypeE e1 e2) `ofWeight` 1
+       \/ cons1 (\(CharE e1, CharE e2) -> SameTypeE e1 e2) `ofWeight` 2
+       \/ cons1 (\(IntToIntE e1, IntToIntE e2)     -> SameTypeE e1 e2) `ofWeight` 2
+       \/ cons1 (\(BoolToBoolE e1, BoolToBoolE e2) -> SameTypeE e1 e2) `ofWeight` 2
+       \/ cons1 (\(BoolToBoolToBoolE e1, BoolToBoolToBoolE e2) -> SameTypeE e1 e2) `ofWeight` 2
+       \/ cons1 (\(IntToIntToIntE e1, IntToIntToIntE e2)       -> SameTypeE e1 e2) `ofWeight` 2
+
+instance Listable SameTypedPairsE where
+  tiers = cons1 (SameTypedPairsE . map unSameTypeE) `ofWeight` 0
+
+instance Listable E0 where
+  tiers  =  mapT E0
+         $  cons1 unIntE0  `ofWeight` 0
+         \/ cons1 unBoolE0 `ofWeight` 1
+         \/ cons1 unIntsE0 `ofWeight` 1
+
+instance Listable EV where
+  tiers  =  mapT EV
+         $  cons1 unIntEV  `ofWeight` 0
+         \/ cons1 unBoolEV `ofWeight` 1
+         \/ cons1 unIntsEV `ofWeight` 1
+
+
+instance Listable Expr where
+  tiers  =  reset (cons1 unIntE)
+         \/ cons1 unBoolE
+         \/ cons1 unCharE
+         \/ cons1 unIntsE
+         \/ cons1 unIntToIntE         `addWeight` 1
+         \/ cons1 unIntToIntToIntE    `addWeight` 1
+         \/ cons1 unBoolToBoolE       `addWeight` 2
+         \/ cons1 unBoolToBoolToBoolE `addWeight` 2
+
+
+-- | This listable instance only produces Ill typed expressions
+instance Listable Ill where
+  tiers  =  mapT Ill
+         $  cons2 (\(IntE ef) (IntE ex) -> ef :$ ex) `ofWeight` 0
+         \/ cons2 (\(IntToIntE ef) (IntToIntE ex) -> ef :$ ex)
+         \/ cons2 (\(Ill ef) ex -> ef :$ ex)
+         \/ cons2 (\ef (Ill ex)-> ef :$ ex)
+
+
+instance ShowFunction Expr where bindtiers  =  bindtiersShow
diff --git a/test/expr.hs b/test/expr.hs
--- a/test/expr.hs
+++ b/test/expr.hs
@@ -34,4 +34,129 @@
   , apparentlyTerminates ffE (if' pp zero (ff xx)) == True
   , apparentlyTerminates ffE (if' pp (ff xx) zero) == False
   , apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero) == False
+
+  , [false, true, zero, one] >$$< [notE, andE, orE, plus, times] == []
+  , [notE, andE, orE, plus, times] >$$< [false, true, zero, one]
+    == [ not' false
+       , not' true
+       , andE :$ false
+       , andE :$ true
+       , orE :$ false
+       , orE :$ true
+       , plus :$ zero
+       , plus :$ one
+       , times :$ zero
+       , times :$ one
+       ]
+  , [notE, andE, orE, plus, times] >$$< [false, true, zero, one] >$$< [false, true, zero, one]
+    == [ false -&&- false
+       , false -&&- true
+       , true -&&- false
+       , true -&&- true
+       , false -||- false
+       , false -||- true
+       , true -||- false
+       , true -||- true
+       , zero -+- zero
+       , zero -+- one
+       , one -+- zero
+       , one -+- one
+       , zero -*- zero
+       , zero -*- one
+       , one -*- zero
+       , one -*- one
+       ]
+
+  , primitiveHoles [false, true]  ==  [b_]
+  , primitiveHoles [zero, one]  ==  [i_]
+  , primitiveHoles [false, zero]  ==  [b_, i_]
+
+  , primitiveHoles [false, true, notE]  ==
+      [ hole (undefined :: Bool)
+      , hole (undefined :: Bool -> Bool)
+      ]
+
+  , primitiveHoles [false, true, notE, andE, orE]  ==
+      [ hole (undefined :: Bool)
+      , hole (undefined :: Bool -> Bool)
+      , hole (undefined :: Bool -> Bool -> Bool)
+      ]
+
+  , primitiveHoles [false, true, andE, orE]  ==
+      [ hole (undefined :: Bool)
+      , hole (undefined :: Bool -> Bool)
+      , hole (undefined :: Bool -> Bool -> Bool)
+      ]
+
+  , primitiveHoles [zero, one, plus, times]  ==
+      [ hole (undefined :: Int)
+      , hole (undefined :: Int -> Int)
+      , hole (undefined :: Int -> Int -> Int)
+      ]
+
+  , primitiveHoles [false, true, andE, orE, zero, one, plus, times]
+    == [ hole (undefined :: Bool)
+       , hole (undefined :: Int)
+       , hole (undefined :: Bool -> Bool)
+       , hole (undefined :: Int -> Int)
+       , hole (undefined :: Bool -> Bool -> Bool)
+       , hole (undefined :: Int -> Int -> Int)
+       ]
+
+  , holds n $ \es -> all (`elem` primitiveHoles es) (map holeAsTypeOf es)
+  , fails n $ \es -> primitiveHoles es == map holeAsTypeOf es
+
+  , map (map show) (primitiveApplications [false, true, andE, orE, zero, one, plus, times])
+    == [ [ "False :: Bool"
+         , "True :: Bool"
+         , "(&&) :: Bool -> Bool -> Bool"
+         , "(||) :: Bool -> Bool -> Bool"
+         , "0 :: Int"
+         , "1 :: Int"
+         , "(+) :: Int -> Int -> Int"
+         , "(*) :: Int -> Int -> Int"
+         ]
+       , [ "(_ &&) :: Bool -> Bool"
+         , "(_ ||) :: Bool -> Bool"
+         , "(_ +) :: Int -> Int"
+         , "(_ *) :: Int -> Int"
+         ]
+       , [ "_ && _ :: Bool"
+         , "_ || _ :: Bool"
+         , "_ + _ :: Int"
+         , "_ * _ :: Int"
+         ]
+       ]
+
+  , holds n $ \e -> sort (valuesBFS e) == sort (values e)
+  , holds n $ \e -> holesBFS e == filter isHole (valuesBFS e)
+  , valuesBFS false == [false]
+  , valuesBFS true  == [true]
+  , valuesBFS zero  == [zero]
+  , valuesBFS one   == [one]
+  , valuesBFS (not' false) == [notE, false]
+  , valuesBFS (not' true)  == [notE, true]
+  , valuesBFS (not' $ not' true) == [notE, notE, true]
+  , valuesBFS (false -&&- true) == [true, andE, false]
+  , valuesBFS (true -||- false) == [false, orE, true]
+  , valuesBFS (one -*- two -+- three -*- xx)
+    == [plus, xx, two, times, three, times, one]
+    -- (((+) (((*) 1) 2)) (((*) 3) x))
+
+  , fillBFS (b_ -&&- b_) false == (b_ -&&- false)
+  , fillBFS (b_ -&&- b_) (b_ -&&- b_) == (b_ -&&- (b_ -&&- b_))
+  , fillBFS (b_ -&&- (b_ -&&- b_)) false == (false -&&- (b_ -&&- b_))
+  , fillBFS (b_ -&&- (b_ -&&- b_)) (b_ -&&- b_) == ((b_ -&&- b_) -&&- (b_ -&&- b_))
+  , fillBFS ((b_ -&&- b_) -&&- (b_ -&&- b_)) false == ((b_ -&&- b_) -&&- (b_ -&&- false))
+  , fillBFS true false == true
+
+  , holds n $ \(SameTypeE e1 e2) -> let e3 = fillBFS e1 e2
+                                    in e3 == e1
+                                    || length (holes e3) == length (holes e1) - 1 + length (holes e2)
+
+  , boupCandidates i_ [zero, one, plus] =$ map sort . take 12 $=
+    townCandidates i_ [zero, one, plus]
+
+  , holds n $ \e es -> not (any hasHole es)
+                   ==> boupCandidates e es =$ map sort . take 12 $= townCandidates e es
   ]
diff --git a/test/model/proto/u-conjure.out b/test/model/proto/u-conjure.out
--- a/test/model/proto/u-conjure.out
+++ b/test/model/proto/u-conjure.out
@@ -4,15 +4,21 @@
 add :: Int -> Int -> Int
 add x y  =  x + y
 
-fact :: Int -> Int
+factorial :: Int -> Int
 cannot conjure
 
-(==>) :: Bool -> Bool -> Bool
-p ==> q  =  q || not p
+factorial :: Int -> Int
+factorial x  =  foldr (*) 1 (enumFromTo 1 x)
 
 second :: [Int] -> Int
 second xs  =  head (tail xs)
 
+(++) :: [Int] -> [Int] -> [Int]
+xs ++ ys  =  foldr (:) ys xs
+
 reverse :: [Int] -> [Int]
 cannot conjure
+
+reverse :: [Int] -> [Int]
+reverse xs  =  foldr (foldr (:) . unit) [] xs
 
diff --git a/test/utils.hs b/test/utils.hs
new file mode 100644
--- /dev/null
+++ b/test/utils.hs
@@ -0,0 +1,21 @@
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+
+import Test
+
+main :: IO ()
+main  =  mainTest tests 5040
+
+tests :: Int -> [Bool]
+tests n  =
+  [ True
+
+  , holds n $ \x -> iterateUntil (==) (`quot` (2 :: Int)) x == 0
+  , holds n $ \xs -> iterateUntil (==) (drop 1) xs == ([]::[Bool])
+
+  , holds n $ \xs ys -> length xs == length ys
+                    ==> zipWith (<>) xs ys == mzip xs (ys :: [[Int]])
+
+  , holds n $ \xs ys -> length xs >= length ys
+                    ==> zipWith (<>) xs (ys <> repeat mempty) == mzip xs (ys :: [[Int]])
+  ]