diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -111,8 +111,8 @@
     steps:
       - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS
         uses: haskell/actions/setup@v1
-        with: # lts-17.9
-          ghc-version: '8.10.4'
+        with: # lts-18.14
+          ghc-version: '8.10.7'
           cabal-version: '3.2'
 
       - uses: actions/cache@v2
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 GHCIMPORTDIRS = src:test
-GHCFLAGS = -O2 \
+GHCFLAGS = -O2 -v0 \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic)
 HADDOCKFLAGS = \
   -i $(shell find ~/.cabal -name express.haddock | tail -1) \
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -17,11 +17,7 @@
 To install the [latest Conjure version from Hackage], just run:
 
 	$ cabal update
-	$ cabal v1-install code-conjure
-
-If you are using Cabal v3.0 or later,
-[avoid using `cabal install`] for the time being
-and use `v1-install` instead.
+	$ cabal install code-conjure
 
 Prerequisites are [express], [leancheck] and [speculate].
 They should be automatically resolved and installed by [Cabal].
@@ -29,7 +25,21 @@
 NOTE: the name of the Hackage package is __[`code-conjure`]__
 -- not to be confused with [Conjure the BitTorrent client].
 
+Starting from Cabal v3.0, you need to pass `--lib` as an argument to
+`cabal install` to install packages globally on the `default` user environment:
 
+	$ cabal install code-conjure --lib
+
+If you already have Conjure installed
+[Cabal may refuse to update](https://github.com/haskell/cabal/issues/7373)
+to the latest version.
+To update, you need to reset your user's cabal installation with:
+
+	rm -rf ~/.cabal/{bin,lib,logs,share,store} ~/.ghc/*/
+
+WARNING: the above command will erase all user-local packages.
+
+
 Synthesizing functions
 ----------------------
 
@@ -293,17 +303,61 @@
 Related work
 ------------
 
+__Conjure's dependencies__.
+Internally, Conjure uses [LeanCheck], [Speculate] and [Express].
+[LeanCheck] does testing similarly to [QuickCheck], [SmallCheck] or [Feat].
+[Speculate] discovers equations similarly to [QuickSpec].
+[Express] encodes expressions involving [Dynamic] types.
+
+[Speculate]:  https://github.com/rudymatela/speculate
+[Express]:    https://github.com/rudymatela/express
+[QuickCheck]: https://hackage.haskell.org/package/QuickCheck
+[smallcheck]: https://hackage.haskell.org/package/smallcheck
+[Feat]:       https://hackage.haskell.org/package/testing-feat
+[QuickSpec]:  https://hackage.haskell.org/package/quickspec
+[Dynamic]:    https://hackage.haskell.org/package/base/docs/Data-Dynamic.html
+
+
+__Program synthesis within Haskell.__
+
+[MagicHaskeller]: https://hackage.haskell.org/package/MagicHaskeller
+[Igor II]: https://cogsys.uni-bamberg.de/projects/effalip
+
 [MagicHaskeller] (2007) is another tool
 that is able to generate Haskell code automatically.
 It supports recursion through
 catamorphisms, paramorphisms and the [`fix`] function.
+[Igor II] (2010) is able to synthesize Haskell
+programs as well.
 
-[Barliman] for Lisp is another tool that does program synthesis.
+[Hoogle]: https://hoogle.haskell.org/
+[Hoogle+]: https://hoogleplus.goto.ucsd.edu/
 
-There are hundreds of others,
-I'll add the most closely related here when I have the time.
+[Hoogle] (2004) is a search engine for Haskell functions.
+It is not able to synthesize expressions
+but it can find functions that match a type.
+[Hoogle+] (2020) is similar to Hoogle
+but is able to search for small expressions.
+In addition to the type, Hoogle+ allows
+users to provide tests that the function should pass.
 
 
+__Program synthesis beyond Haskell.__
+
+[PushGP]: https://github.com/lspector/Clojush
+[G3P]: https://github.com/t-h-e/HeuristicLab.CFGGP
+
+[PushGP] (2002) and [G3P] (2017) are genetic programming systems 
+that are able to synthesize programs in Push and Python respectively.
+Differently from Conjure or MagicHaskeller,
+they require around a hundred tests for traning
+instead of just about half a dozen.
+
+[Barliman]:       https://github.com/webyrd/Barliman
+
+[Barliman] (2016) for Lisp is another tool that does program synthesis.
+
+
 Further reading
 ---------------
 
@@ -343,8 +397,6 @@
 [LeanCheck]:      https://hackage.haskell.org/package/leancheck
 [express]:        https://hackage.haskell.org/package/express
 [speculate]:      https://hackage.haskell.org/package/speculate
-[MagicHaskeller]: https://hackage.haskell.org/package/MagicHaskeller
-[Barliman]:       https://github.com/webyrd/Barliman
 
 [avoid using `cabal install`]:         https://github.com/haskell/cabal/issues/7373
 [latest Conjure version from Hackage]: https://hackage.haskell.org/package/code-conjure
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,9 +3,7 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
-* derive `conjureCases`, `conjureSize` and `conjureSubTypes`;
-
-* implement `deriveConjurable` using TH (cf. `deriveExpress` and `deriveGeneralizable`);
+* test `conjureCases` from `deriveConjurable`;
 
 * consider not breaking in some cases (increased crossproduct of patterns)
 
diff --git a/bench/gps.hs b/bench/gps.hs
--- a/bench/gps.hs
+++ b/bench/gps.hs
@@ -321,6 +321,15 @@
     , prif (undefined :: Rational)
     ]
 
+  -- simplified background
+  conjure "wallisNext" wallisNextP
+    [ pr (0 :: Integer)
+    , pr (1 :: Integer)
+    , prim "+" ((+) :: Integer -> Integer -> Integer)
+    , prim "*" ((*) :: Integer -> Integer -> Integer)
+    , prim "%" ((%) :: Integer -> Integer -> Rational)
+    ]
+
   conjure "gps10" gps10p
     [ pr (2 :: Integer)
     , pr (3 :: Integer)
@@ -829,11 +838,17 @@
 -- Conjure found a smaller implementation!
 
 gps27c :: IO ()
-gps27c  =  conjure "gps27" gps27p
-  [ prim "<" ((<) :: Int -> Int -> Bool)
-  , prim "&&" (&&)
-  , prif (undefined :: Int)
-  ]
+gps27c  =  do
+  conjure "gps27" gps27p
+    [ prim "<" ((<) :: Int -> Int -> Bool)
+    , prim "&&" (&&)
+    , prif (undefined :: Int)
+    ]
+
+  conjure "gps27b" gps27p
+    [ prim "min" (min :: Int -> Int -> Int)
+    , prim "max" (max :: Int -> Int -> Int)
+    ]
 
 
 -- GPS Benchmark #28 -- Smallest --
diff --git a/bench/gps.out b/bench/gps.out
--- a/bench/gps.out
+++ b/bench/gps.out
@@ -5,6 +5,7 @@
 -- looking through 1 candidates of size 2
 -- looking through 1 candidates of size 3
 -- looking through 2 candidates of size 4
+-- tested 4 candidates
 gps1 x y  =  fromIntegral x + y
 
 gps2 :: Int -> Maybe [Char]
@@ -23,6 +24,7 @@
 -- looking through 176 candidates of size 11
 -- looking through 704 candidates of size 12
 -- looking through 1856 candidates of size 13
+-- tested 1744 candidates
 gps2 x  =  if 2000 <= x then Just "large" else (if x < 1000 then Just "small" else Nothing)
 
 gps3 :: Int -> Int -> Int -> [Int]
@@ -36,6 +38,7 @@
 -- looking through 1536 candidates of size 6
 -- looking through 0 candidates of size 7
 -- looking through 26991 candidates of size 8
+-- tested 19480 candidates
 gps3 x y z  =  enumFromThenTo x (x + z) (y - 1)
 
 gps3 :: Int -> Int -> Int -> [Int]
@@ -49,6 +52,7 @@
 -- looking through 0 candidates of size 6
 -- looking through 108 candidates of size 7
 -- looking through 36 candidates of size 8
+-- tested 166 candidates
 cannot conjure
 
 gps4 :: [Char] -> [Char] -> [Char] -> Bool
@@ -65,6 +69,7 @@
 -- looking through 162 candidates of size 9
 -- looking through 30 candidates of size 10
 -- looking through 30 candidates of size 11
+-- tested 201 candidates
 gps4 cs ds es  =  length cs < length ds && length ds < length es
 
 gps5 :: [Char] -> [Char]
@@ -76,6 +81,7 @@
 -- looking through 6 candidates of size 4
 -- looking through 5 candidates of size 5
 -- looking through 13 candidates of size 6
+-- tested 30 candidates
 cannot conjure
 
 gps6 :: Int -> Int
@@ -87,6 +93,7 @@
 -- looking through 146 candidates of size 4
 -- looking through 624 candidates of size 5
 -- looking through 2576 candidates of size 6
+-- tested 3392 candidates
 cannot conjure
 
 gps7 :: [Char] -> ([Char],Int)
@@ -103,6 +110,7 @@
 -- looking through 88 candidates of size 9
 -- looking through 201 candidates of size 10
 -- looking through 442 candidates of size 11
+-- tested 546 candidates
 gps7 cs  =  (init (unlines (words cs)),length (filter (not . isSpace) cs))
 
 gps8 :: [Char] -> [Char] -> [(Int,Char,Char)]
@@ -111,6 +119,7 @@
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
 -- looking through 0 candidates of size 3
+-- tested 0 candidates
 cannot conjure
 
 gps9 :: Int -> [Int]
@@ -126,6 +135,7 @@
 -- looking through 83 candidates of size 8
 -- looking through 143 candidates of size 9
 -- looking through 259 candidates of size 10
+-- tested 328 candidates
 gps9 x  =  filter even (filter (x >) (map sq [1..x]))
 
 wallisNext :: Ratio Integer -> Ratio Integer
@@ -139,8 +149,23 @@
 -- looking through 118 candidates of size 6
 -- looking through 5 candidates of size 7
 -- looking through 1001 candidates of size 8
+-- tested 1015 candidates
 wallisNext (x % y)  =  (y + 1) % (x + 1)
 
+wallisNext :: Ratio Integer -> Ratio Integer
+-- testing 6 combinations of argument values
+-- pruning with 15/26 rules
+-- looking through 1 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 16 candidates of size 4
+-- looking through 3 candidates of size 5
+-- looking through 103 candidates of size 6
+-- looking through 5 candidates of size 7
+-- looking through 801 candidates of size 8
+-- tested 832 candidates
+wallisNext (x % y)  =  (y + 1) % (x + 1)
+
 gps10 :: Int -> Ratio Integer
 -- testing 6 combinations of argument values
 -- pruning with 3/4 rules
@@ -152,6 +177,7 @@
 -- looking through 5 candidates of size 6
 -- looking through 8 candidates of size 7
 -- looking through 13 candidates of size 8
+-- tested 33 candidates
 gps10 x  =  product (take x (iterate wallisNext (2 % 3)))
 
 gps11 :: [[Char]] -> [Int]
@@ -161,6 +187,7 @@
 -- looking through 0 candidates of size 2
 -- looking through 1 candidates of size 3
 -- looking through 1 candidates of size 4
+-- tested 2 candidates
 gps11 css  =  reverse (map length css)
 
 gps11 :: [[Char]] -> [Int]
@@ -174,6 +201,7 @@
 -- looking through 2 candidates of size 6
 -- looking through 0 candidates of size 7
 -- looking through 2 candidates of size 8
+-- tested 6 candidates
 gps11 []  =  []
 gps11 (cs:css)  =  gps11 css ++ [length cs]
 
@@ -191,6 +219,7 @@
 -- looking through 1166 candidates of size 9
 -- looking through 3187 candidates of size 10
 -- looking through 9282 candidates of size 11
+-- tested 10413 candidates
 gps12 xs  =  (length xs - fromJust (findIndex (0 ==) (reverse xs))) - 1
 
 gps13 :: [Ratio Integer] -> Ratio Integer
@@ -204,6 +233,7 @@
 -- looking through 56 candidates of size 6
 -- looking through 125 candidates of size 7
 -- looking through 449 candidates of size 8
+-- tested 317 candidates
 gps13 qs  =  foldr (+) 0 qs / fromIntegral (length qs)
 
 odd :: Int -> Bool
@@ -214,6 +244,7 @@
 -- looking through 7 candidates of size 3
 -- looking through 0 candidates of size 4
 -- looking through 71 candidates of size 5
+-- tested 17 candidates
 odd x  =  x `mod` 2 /= 0
 
 gps14 :: [Int] -> Int
@@ -223,6 +254,7 @@
 -- looking through 1 candidates of size 2
 -- looking through 0 candidates of size 3
 -- looking through 1 candidates of size 4
+-- tested 2 candidates
 gps14 xs  =  length (filter odd xs)
 
 gps14 :: [Int] -> Int
@@ -235,6 +267,7 @@
 -- looking through 66 candidates of size 5
 -- looking through 600 candidates of size 6
 -- looking through 1034 candidates of size 7
+-- tested 749 candidates
 gps14 []  =  0
 gps14 (x:xs)  =  x `mod` 2 + gps14 xs
 
@@ -245,6 +278,7 @@
 -- looking through 0 candidates of size 2
 -- looking through 2 candidates of size 3
 -- looking through 8 candidates of size 4
+-- tested 4 candidates
 gps15 xs ys  =  reverse xs == ys
 
 gps16 :: [Char] -> [Char] -> Bool
@@ -255,6 +289,7 @@
 -- looking through 2 candidates of size 3
 -- looking through 6 candidates of size 4
 -- looking through 2 candidates of size 5
+-- tested 9 candidates
 gps16 cs ds  =  sort cs `isSubsequenceOf` sort ds
 
 gps17 :: Int -> Int
@@ -269,6 +304,7 @@
 -- looking through 577 candidates of size 7
 -- looking through 1311 candidates of size 8
 -- looking through 5282 candidates of size 9
+-- tested 2201 candidates
 gps17 0  =  0
 gps17 x  =  x * x + gps17 (x - 1)
 
@@ -284,6 +320,7 @@
 -- looking through 791 candidates of size 7
 -- looking through 220 candidates of size 8
 -- looking through 4632 candidates of size 9
+-- tested 3931 candidates
 gps18 [] []  =  []
 gps18 [] (x:xs)  =  xs
 gps18 (x:xs) []  =  xs
@@ -296,6 +333,7 @@
 -- looking through 2 candidates of size 2
 -- looking through 0 candidates of size 3
 -- looking through 12 candidates of size 4
+-- tested 14 candidates
 gps18 xs ys  =  zipWith (+) xs ys
 
 gps19 :: Int -> [Char] -> [Char]
@@ -303,6 +341,7 @@
 -- pruning with 0/0 rules
 -- looking through 1 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 1 candidates
 cannot conjure
 
 isVowel :: Char -> Bool
@@ -330,6 +369,7 @@
 -- looking through 62 candidates of size 20
 -- looking through 62 candidates of size 21
 -- looking through 126 candidates of size 22
+-- tested 1207 candidates
 isVowel 'a'  =  True
 isVowel 'e'  =  True
 isVowel 'i'  =  True
@@ -354,6 +394,7 @@
 -- looking through 3495 candidates of size 12
 -- looking through 6382 candidates of size 13
 -- looking through 20409 candidates of size 14
+-- tested 27901 candidates
 pig1 ""  =  "ay"
 pig1 (c:cs)  =  if isVowel c then (c:cs) ++ "ay" else cs ++ (c:"ay")
 
@@ -364,6 +405,7 @@
 -- looking through 2 candidates of size 3
 -- looking through 3 candidates of size 4
 -- looking through 5 candidates of size 5
+-- tested 12 candidates
 gps20c cs  =  unwords (map pig1 (words cs))
 
 gps21 :: [Int] -> [Int]
@@ -379,6 +421,7 @@
 -- looking through 30 candidates of size 8
 -- looking through 25 candidates of size 9
 -- looking through 65 candidates of size 10
+-- tested 96 candidates
 gps21 []  =  []
 gps21 (x:xs)  =  (if x < 0 then 0 else x):gps21 xs
 
@@ -390,6 +433,7 @@
 -- looking through 0 candidates of size 4
 -- looking through 0 candidates of size 5
 -- looking through 4 candidates of size 6
+-- tested 5 candidates
 gps22 ""  =  0
 gps22 (c:cs)  =  scrabble1 c + gps22 cs
 
@@ -398,6 +442,7 @@
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 gps24 :: [Char] -> Char
@@ -413,12 +458,14 @@
 -- looking through 97 candidates of size 8
 -- looking through 286 candidates of size 9
 -- looking through 739 candidates of size 10
+-- tested 673 candidates
 gps24 cs  =  chr (ord ' ' + sum (map ord cs) `mod` 64)
 
 gps25 :: Int -> [Int]
 -- testing 4 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 gps26 :: Int -> Int -> Int -> Int -> Int -> Char
@@ -426,6 +473,7 @@
 -- pruning with 4/4 rules
 -- looking through 5 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 5 candidates
 cannot conjure
 
 gps27 :: Int -> Int -> Int -> Int
@@ -442,8 +490,20 @@
 -- looking through 0 candidates of size 9
 -- looking through 180 candidates of size 10
 -- looking through 2592 candidates of size 11
+-- tested 1579 candidates
 gps27 x y z  =  if x < y then (if y < z then y else z) else x
 
+gps27b :: Int -> Int -> Int -> Int
+-- testing 3 combinations of argument values
+-- pruning with 20/30 rules
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 12 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 36 candidates of size 5
+-- tested 16 candidates
+gps27b x y z  =  min (max x y) z
+
 gps28 :: Int -> Int -> Int -> Int -> Int
 -- testing 5 combinations of argument values
 -- pruning with 6/10 rules
@@ -454,6 +514,7 @@
 -- looking through 24 candidates of size 5
 -- looking through 0 candidates of size 6
 -- looking through 72 candidates of size 7
+-- tested 44 candidates
 gps28 x y z x'  =  x `min` (y `min` (z `min` x'))
 
 gps29 :: [Char] -> Int
@@ -467,6 +528,7 @@
 -- looking through 18 candidates of size 7
 -- looking through 33 candidates of size 8
 -- looking through 65 candidates of size 9
+-- tested 86 candidates
 gps29 ""  =  0
 gps29 (c:cs)  =  (if isVowel c then 1 else 0) + gps29 cs
 
diff --git a/bench/gps2.hs b/bench/gps2.hs
--- a/bench/gps2.hs
+++ b/bench/gps2.hs
@@ -482,7 +482,8 @@
 
 
 -- can generate at size 15 in 18 seconds
--- setting limit of 5 for faster output
+-- setting limit of 5 for faster automated tests
+-- BENCHMARK: increase maxSize from 5 to 18
 gps17c :: IO ()
 gps17c  =  conjureWith args{maxSize=5} "gps17_pds" gps17p
   [ pr (0 :: Int)
diff --git a/bench/gps2.out b/bench/gps2.out
--- a/bench/gps2.out
+++ b/bench/gps2.out
@@ -11,6 +11,7 @@
 -- looking through 0 candidates of size 8
 -- looking through 1 candidates of size 9
 -- looking through 2 candidates of size 10
+-- tested 5 candidates
 gps1 xs  =  findIndex (0 >) (map (foldr (+) 0) (tail (inits xs)))
 
 gps1 :: [Int] -> Maybe Int
@@ -24,6 +25,7 @@
 -- looking through 0 candidates of size 6
 -- looking through 1 candidates of size 7
 -- looking through 4 candidates of size 8
+-- tested 6 candidates
 gps1 xs  =  findIndex (0 >) (map sum (tail (inits xs)))
 
 gps1 :: Int -> [Int] -> Int
@@ -33,6 +35,7 @@
 -- looking through 25 candidates of size 2
 -- looking through 255 candidates of size 3
 -- looking through 451 candidates of size 4
+-- tested 735 candidates
 cannot conjure
 
 gps2 :: Double -> Double -> Int -> Double
@@ -44,12 +47,14 @@
 -- looking through 70 candidates of size 4
 -- looking through 314 candidates of size 5
 -- looking through 1432 candidates of size 6
+-- tested 1838 candidates
 cannot conjure
 
 gps3 :: [Char] -> Int
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 gps4 :: [Char] -> [Char]
@@ -60,12 +65,14 @@
 -- looking through 22 candidates of size 4
 -- looking through 54 candidates of size 5
 -- looking through 124 candidates of size 6
+-- tested 214 candidates
 cannot conjure
 
 gps5 :: Int -> [Int]
 -- testing 6 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 tell :: [Int] -> Int -> [Int]
@@ -80,6 +87,7 @@
 -- looking through 538 candidates of size 8
 -- looking through 134 candidates of size 9
 -- looking through 5299 candidates of size 10
+-- tested 2699 candidates
 tell [] x  =  []
 tell (x:xs) y  =  y `div` x:tell xs (y `mod` x)
 
@@ -89,6 +97,7 @@
 -- looking through 1 candidates of size 1
 -- looking through 0 candidates of size 2
 -- looking through 1 candidates of size 3
+-- tested 2 candidates
 gps5 x  =  tell [25,10,5,1] x
 
 gps5 :: Int -> [Int]
@@ -105,6 +114,7 @@
 -- looking through 4450 candidates of size 9
 -- looking through 9710 candidates of size 10
 -- looking through 44767 candidates of size 11
+-- tested 32953 candidates
 gps5 x  =  tell [25,10,5,1] x
 
 gps6 :: [Int] -> Int
@@ -112,12 +122,14 @@
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 gps7 :: Integer -> Integer -> Ratio Integer
 -- testing 6 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 gps :: Int -> [Int] -> (Int,Int)
@@ -125,18 +137,21 @@
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 gps :: Int -> [Char]
 -- testing 7 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 gps :: Int -> [Char]
 -- testing 7 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 gcd :: Int -> Int -> Int
@@ -148,6 +163,7 @@
 -- looking through 60 candidates of size 4
 -- looking through 150 candidates of size 5
 -- looking through 472 candidates of size 6
+-- tested 246 candidates
 gcd x 0  =  x
 gcd x y  =  gcd y (x `mod` y)
 
@@ -159,6 +175,7 @@
 -- looking through 0 candidates of size 3
 -- looking through 0 candidates of size 4
 -- looking through 4 candidates of size 5
+-- tested 3 candidates
 gps12 cs ds  =  findIndices (ds `isPrefixOf`) (tails cs)
 
 gps13_leaders :: [Int] -> [Int]
@@ -176,6 +193,7 @@
 -- looking through 21 candidates of size 10
 -- looking through 34 candidates of size 11
 -- looking through 67 candidates of size 12
+-- tested 83 candidates
 gps13_leaders []  =  []
 gps13_leaders (x:xs)  =  if all (x >) xs then x:gps13_leaders xs else gps13_leaders xs
 
@@ -183,11 +201,13 @@
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 gps15_mastermind :: () -> ()
 -- pruning with 0/1 rules
 -- looking through 1 candidates of size 1
+-- tested 1 candidates
 gps15_mastermind u  =  u
 
 gps16_middle :: [Char] -> [Char]
@@ -205,6 +225,7 @@
 -- looking through 824 candidates of size 10
 -- looking through 2282 candidates of size 11
 -- looking through 6293 candidates of size 12
+-- tested 3977 candidates
 gps16_middle ""  =  ""
 gps16_middle (c:cs)  =  if length cs <= 1 then c:cs else gps16_middle (init cs)
 
@@ -216,6 +237,7 @@
 -- looking through 2 candidates of size 3
 -- looking through 1 candidates of size 4
 -- looking through 5 candidates of size 5
+-- tested 11 candidates
 cannot conjure
 
 gps18_price :: [Double] -> [Double] -> Double
@@ -227,6 +249,7 @@
 -- looking through 72 candidates of size 4
 -- looking through 1192 candidates of size 5
 -- looking through 696 candidates of size 6
+-- tested 2042 candidates
 cannot conjure
 
 gps19_snowday :: Int -> Double -> Double -> Double -> Double
@@ -238,12 +261,14 @@
 -- looking through 169 candidates of size 4
 -- looking through 543 candidates of size 5
 -- looking through 3608 candidates of size 6
+-- tested 4361 candidates
 cannot conjure
 
 gps20 :: [Char] -> Bool
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
+-- tested 0 candidates
 cannot conjure
 
 spin :: [Char] -> [Char]
@@ -257,6 +282,7 @@
 -- looking through 0 candidates of size 6
 -- looking through 0 candidates of size 7
 -- looking through 4 candidates of size 8
+-- tested 3 candidates
 spin cs  =  if length cs >= 5 then reverse cs else cs
 
 gps21_spinwords :: [Char] -> [Char]
@@ -267,6 +293,7 @@
 -- looking through 2 candidates of size 3
 -- looking through 3 candidates of size 4
 -- looking through 5 candidates of size 5
+-- tested 12 candidates
 gps21_spinwords cs  =  unwords (map spin (words cs))
 
 digits :: Int -> [Int]
@@ -284,11 +311,13 @@
 -- looking through 935 candidates of size 10
 -- looking through 9018 candidates of size 11
 -- looking through 9686 candidates of size 12
+-- tested 20746 candidates
 cannot conjure
 
 gps22 :: Int -> [Char]
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
+-- tested 0 candidates
 cannot conjure
 
 gps23 :: [Char] -> [Char] -> [Char] -> [Char]
@@ -305,6 +334,7 @@
 -- looking through 0 candidates of size 10
 -- looking through 0 candidates of size 11
 -- looking through 5184 candidates of size 12
+-- tested 9174 candidates
 cannot conjure
 
 gps24 :: [Char] -> Twitter
@@ -322,6 +352,7 @@
 -- looking through 232 candidates of size 10
 -- looking through 322 candidates of size 11
 -- looking through 483 candidates of size 12
+-- tested 936 candidates
 gps24 ""  =  Empty
 gps24 (c:cs)  =  if 140 > length cs then Tweet (length (c:cs)) else TooMany
 
@@ -334,5 +365,6 @@
 -- looking through 312 candidates of size 4
 -- looking through 2262 candidates of size 5
 -- looking through 9400 candidates of size 6
+-- tested 12074 candidates
 cannot conjure
 
diff --git a/bench/ill-hit.out b/bench/ill-hit.out
--- a/bench/ill-hit.out
+++ b/bench/ill-hit.out
@@ -6,6 +6,7 @@
 -- looking through 6 candidates of size 3
 -- looking through 20 candidates of size 4
 -- looking through 34 candidates of size 5
+-- tested 34 candidates
 sum []  =  0
 sum (x:xs)  =  x + sum xs
 
@@ -16,6 +17,7 @@
 -- looking through 6 candidates of size 3
 -- looking through 20 candidates of size 4
 -- looking through 34 candidates of size 5
+-- tested 34 candidates
 sum []  =  0
 sum (x:xs)  =  x + sum xs
 
diff --git a/bench/lowtests.out b/bench/lowtests.out
--- a/bench/lowtests.out
+++ b/bench/lowtests.out
@@ -21,6 +21,7 @@
 -- looking through 0 candidates of size 10
 -- looking through 0 candidates of size 11
 -- looking through 0 candidates of size 12
+-- tested 48 candidates
 cannot conjure
 
 subset :: [Int] -> [Int] -> Bool
@@ -38,6 +39,7 @@
 -- looking through 2 candidates of size 3
 -- looking through 6 candidates of size 4
 -- looking through 2 candidates of size 5
+-- tested 9 candidates
 subset xs ys  =  sort xs `isSubsequenceOf` sort ys
 
 replicates :: [Char] -> Int -> [Char]
@@ -61,6 +63,7 @@
 -- looking through 1 candidates of size 10
 -- looking through 0 candidates of size 11
 -- looking through 0 candidates of size 12
+-- tested 4 candidates
 cannot conjure
 
 replicates :: [Char] -> Int -> [Char]
@@ -77,5 +80,6 @@
 -- looking through 0 candidates of size 3
 -- looking through 1 candidates of size 4
 -- looking through 1 candidates of size 5
+-- tested 3 candidates
 replicates cs x  =  concat (transpose (replicate x cs))
 
diff --git a/bench/p12.out b/bench/p12.out
--- a/bench/p12.out
+++ b/bench/p12.out
@@ -8,6 +8,7 @@
 -- looking through 82 candidates of size 4
 -- looking through 263 candidates of size 5
 -- looking through 960 candidates of size 6
+-- tested 406 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (dec x)
 
diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime
--- a/bench/runtime/zero/bench/candidates.runtime
+++ b/bench/runtime/zero/bench/candidates.runtime
@@ -1,1 +1,1 @@
-9.2
+9.3
diff --git a/bench/runtime/zero/bench/gps.runtime b/bench/runtime/zero/bench/gps.runtime
--- a/bench/runtime/zero/bench/gps.runtime
+++ b/bench/runtime/zero/bench/gps.runtime
@@ -1,1 +1,1 @@
-22.8
+23.8
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 @@
-0.9
+0.8
diff --git a/bench/runtime/zero/bench/terpret.runtime b/bench/runtime/zero/bench/terpret.runtime
--- a/bench/runtime/zero/bench/terpret.runtime
+++ b/bench/runtime/zero/bench/terpret.runtime
@@ -1,1 +1,1 @@
-13.2
+13.3
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
--- a/bench/runtime/zero/eg/arith.runtime
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -1,1 +1,1 @@
-1.2
+1.8
diff --git a/bench/runtime/zero/eg/count.runtime b/bench/runtime/zero/eg/count.runtime
--- a/bench/runtime/zero/eg/count.runtime
+++ b/bench/runtime/zero/eg/count.runtime
@@ -1,1 +1,1 @@
-0.5
+0.6
diff --git a/bench/runtime/zero/eg/dupos.runtime b/bench/runtime/zero/eg/dupos.runtime
--- a/bench/runtime/zero/eg/dupos.runtime
+++ b/bench/runtime/zero/eg/dupos.runtime
@@ -1,1 +1,1 @@
-3.1
+4.5
diff --git a/bench/runtime/zero/eg/fib01.runtime b/bench/runtime/zero/eg/fib01.runtime
--- a/bench/runtime/zero/eg/fib01.runtime
+++ b/bench/runtime/zero/eg/fib01.runtime
@@ -1,1 +1,1 @@
-4.5
+4.4
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.5
 leancheck-0.9.10
-express-1.0.6
+express-1.0.8
 speculate-0.4.14
diff --git a/bench/self.out b/bench/self.out
--- a/bench/self.out
+++ b/bench/self.out
@@ -4,6 +4,7 @@
 -- looking through 4 candidates of size 1
 -- looking through 18 candidates of size 2
 -- looking through 120 candidates of size 3
+-- tested 24 candidates
 x ? y  =  x + y
 
 (?) :: Int -> Int -> Int
@@ -12,6 +13,7 @@
 -- looking through 4 candidates of size 1
 -- looking through 18 candidates of size 2
 -- looking through 120 candidates of size 3
+-- tested 40 candidates
 x ? y  =  x * y
 
 i :: Int -> Int
@@ -20,6 +22,7 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 22 candidates of size 3
+-- tested 10 candidates
 i x  =  x + 1
 
 d :: Int -> Int
@@ -28,5 +31,6 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 22 candidates of size 3
+-- tested 29 candidates
 cannot conjure
 
diff --git a/bench/take-drop.out b/bench/take-drop.out
--- a/bench/take-drop.out
+++ b/bench/take-drop.out
@@ -10,6 +10,7 @@
 -- looking through 132 candidates of size 7
 -- looking through 127 candidates of size 8
 -- looking through 458 candidates of size 9
+-- tested 495 candidates
 drop 0 []  =  []
 drop 0 (x:xs)  =  x:xs
 drop x []  =  []
@@ -27,6 +28,7 @@
 -- looking through 132 candidates of size 7
 -- looking through 127 candidates of size 8
 -- looking through 458 candidates of size 9
+-- tested 484 candidates
 take 0 []  =  []
 take 0 (x:xs)  =  []
 take x []  =  []
diff --git a/bench/terpret.hs b/bench/terpret.hs
--- a/bench/terpret.hs
+++ b/bench/terpret.hs
@@ -137,6 +137,7 @@
 
   -- using primitives123 below works, but increases the runtime to 18 seconds
   -- let's leave it commented out so runtime is faster when running automated tests
+  -- BENCHMARK: uncomment primitives123
   conjure "fadder" t5p $ -- primitives123 ++
     [ prim "not" not
     , prim "," ((,) :: Bool -> Bool -> (Bool,Bool))
diff --git a/bench/terpret.out b/bench/terpret.out
--- a/bench/terpret.out
+++ b/bench/terpret.out
@@ -9,6 +9,7 @@
 -- looking through 10 candidates of size 4
 -- looking through 17 candidates of size 5
 -- looking through 41 candidates of size 6
+-- tested 36 candidates
 invert []  =  []
 invert (p:ps)  =  not p:invert ps
 
@@ -20,6 +21,7 @@
 -- looking through 2 candidates of size 1
 -- looking through 1 candidates of size 2
 -- looking through 5 candidates of size 3
+-- tested 5 candidates
 prependZero ps  =  False:ps
 
 TerpreT benchmark #3: binary decrement
@@ -36,6 +38,7 @@
 -- looking through 86 candidates of size 7
 -- looking through 202 candidates of size 8
 -- looking through 487 candidates of size 9
+-- tested 418 candidates
 decrement []  =  []
 decrement (p:ps)  =  not p:(if p then ps else decrement ps)
 
@@ -56,6 +59,7 @@
 -- looking through 8154 candidates of size 9
 -- looking through 27432 candidates of size 10
 -- looking through 174839 candidates of size 11
+-- tested 137576 candidates
 cshift (p,q,r)  =  if p then (p,r,q) else (p,q,r)
 
 cshift :: Bool -> Bool -> Bool -> (Bool,Bool,Bool)
@@ -70,6 +74,7 @@
 -- looking through 1035 candidates of size 6
 -- looking through 2457 candidates of size 7
 -- looking through 20250 candidates of size 8
+-- tested 22191 candidates
 cshift False p q  =  (False,p,q)
 cshift True p q  =  (True,q,p)
 
@@ -89,6 +94,7 @@
 -- looking through 2148 candidates of size 9
 -- looking through 5520 candidates of size 10
 -- looking through 13656 candidates of size 11
+-- tested 16290 candidates
 fadder p q r  =  if p == q then (p,r) else (r,not r)
 
 TerpreT benchmark #6: 2-bit adder
@@ -103,6 +109,7 @@
 -- looking through 8 candidates of size 4
 -- looking through 128 candidates of size 5
 -- looking through 408 candidates of size 6
+-- tested 544 candidates
 cannot conjure
 
 TerpreT benchmark #7: access
@@ -113,6 +120,7 @@
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
 -- looking through 1 candidates of size 3
+-- tested 1 candidates
 xs `access` x  =  xs !! x
 
 access :: [A] -> Int -> A
@@ -125,6 +133,7 @@
 -- looking through 19 candidates of size 5
 -- looking through 23 candidates of size 6
 -- looking through 68 candidates of size 7
+-- tested 67 candidates
 [] `access` 0  =  undefined
 [] `access` x  =  undefined
 (x:xs) `access` 0  =  x
@@ -142,6 +151,7 @@
 -- looking through 9 candidates of size 5
 -- looking through 29 candidates of size 6
 -- looking through 41 candidates of size 7
+-- tested 53 candidates
 decrelements []  =  []
 decrelements (x:xs)  =  x - 1:decrelements xs
 
@@ -152,5 +162,6 @@
 -- looking through 1 candidates of size 2
 -- looking through 3 candidates of size 3
 -- looking through 8 candidates of size 4
+-- tested 8 candidates
 decrelements xs  =  map (subtract 1) xs
 
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,16 @@
 ============================
 
 
+0.5.2
+-----
+
+* show number of tested candidates
+* complete `Conjurable` derivation functions
+* reference related work on README
+* add switch to unique-modulo-testing candidates (slow)
+  to allow computing the near upper/lower limit on pruning
+
+
 v0.5.0
 ------
 
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.5.0
+version:             0.5.2
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -63,7 +63,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.5.0
+  tag:             v0.5.2
 
 library
   exposed-modules: Conjure
diff --git a/eg/arith.hs b/eg/arith.hs
--- a/eg/arith.hs
+++ b/eg/arith.hs
@@ -10,6 +10,12 @@
 double 2  =  4
 double 3  =  6
 
+triple :: Int -> Int
+triple 0  =  0
+triple 1  =  3
+triple 2  =  6
+triple 3  =  9
+
 add :: Int -> Int -> Int
 add 0 0  =  0
 add 0 1  =  1
@@ -21,6 +27,11 @@
 square 1  =  1
 square 2  =  4
 
+cube :: Int -> Int
+cube 0  =  0
+cube 1  =  1
+cube 2  =  8
+
 tnpo :: Int -> Int
 tnpo 0  =  1
 tnpo 1  =  4
@@ -29,8 +40,10 @@
 main :: IO ()
 main = do
   conjure "double" double primitives
+  conjure "triple" triple primitives
   conjure "add"    add    primitives
   conjure "square" square primitives
+  conjure "cube"   cube   primitives
   conjure "tnpo"   tnpo   primitives
 
 primitives :: [Prim]
diff --git a/eg/arith.out b/eg/arith.out
--- a/eg/arith.out
+++ b/eg/arith.out
@@ -4,14 +4,27 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 9 candidates of size 3
+-- tested 8 candidates
 double x  =  x + x
 
+triple :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 14/25 rules
+-- looking through 3 candidates of size 1
+-- looking through 4 candidates of size 2
+-- looking through 9 candidates of size 3
+-- looking through 23 candidates of size 4
+-- looking through 29 candidates of size 5
+-- tested 43 candidates
+triple x  =  x + (x + x)
+
 add :: Int -> Int -> Int
 -- testing 4 combinations of argument values
 -- pruning with 14/25 rules
 -- looking through 4 candidates of size 1
 -- looking through 18 candidates of size 2
 -- looking through 101 candidates of size 3
+-- tested 24 candidates
 add x y  =  x + y
 
 square :: Int -> Int
@@ -20,8 +33,20 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 9 candidates of size 3
+-- tested 12 candidates
 square x  =  x * x
 
+cube :: Int -> Int
+-- testing 3 combinations of argument values
+-- pruning with 14/25 rules
+-- looking through 3 candidates of size 1
+-- looking through 4 candidates of size 2
+-- looking through 9 candidates of size 3
+-- looking through 23 candidates of size 4
+-- looking through 29 candidates of size 5
+-- tested 55 candidates
+cube x  =  x * (x * x)
+
 tnpo :: Int -> Int
 -- testing 3 combinations of argument values
 -- pruning with 14/25 rules
@@ -32,5 +57,6 @@
 -- looking through 29 candidates of size 5
 -- looking through 71 candidates of size 6
 -- looking through 113 candidates of size 7
+-- tested 163 candidates
 tnpo x  =  x + (x + (x + 1))
 
diff --git a/eg/bools.out b/eg/bools.out
--- a/eg/bools.out
+++ b/eg/bools.out
@@ -6,6 +6,7 @@
 -- looking through 12 candidates of size 3
 -- looking through 16 candidates of size 4
 -- looking through 42 candidates of size 5
+-- tested 45 candidates
 and []  =  True
 and (p:ps)  =  p && and ps
 
@@ -17,6 +18,7 @@
 -- looking through 12 candidates of size 3
 -- looking through 16 candidates of size 4
 -- looking through 42 candidates of size 5
+-- tested 39 candidates
 or []  =  False
 or (p:ps)  =  p || or ps
 
@@ -27,6 +29,7 @@
 -- looking through 6 candidates of size 2
 -- looking through 12 candidates of size 3
 -- looking through 18 candidates of size 4
+-- tested 28 candidates
 and ps  =  foldr (&&) True ps
 
 or :: [Bool] -> Bool
@@ -36,5 +39,6 @@
 -- looking through 6 candidates of size 2
 -- looking through 12 candidates of size 3
 -- looking through 18 candidates of size 4
+-- tested 27 candidates
 or ps  =  foldr (||) False ps
 
diff --git a/eg/count.out b/eg/count.out
--- a/eg/count.out
+++ b/eg/count.out
@@ -6,6 +6,7 @@
 -- looking through 0 candidates of size 3
 -- looking through 0 candidates of size 4
 -- looking through 1 candidates of size 5
+-- tested 2 candidates
 count x xs  =  length (filter (x ==) xs)
 
 count :: A -> [A] -> Int
@@ -22,6 +23,7 @@
 -- looking through 272 candidates of size 9
 -- looking through 648 candidates of size 10
 -- looking through 1549 candidates of size 11
+-- tested 1751 candidates
 count x []  =  0
 count x (y:xs)  =  (if x == y then 1 else 0) + count x xs
 
diff --git a/eg/dupos.out b/eg/dupos.out
--- a/eg/dupos.out
+++ b/eg/dupos.out
@@ -18,6 +18,7 @@
 -- looking through 644 candidates of size 15
 -- looking through 1189 candidates of size 16
 -- looking through 2189 candidates of size 17
+-- tested 2599 candidates
 duplicates []  =  []
 duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
 
@@ -40,6 +41,7 @@
 -- looking through 644 candidates of size 15
 -- looking through 1189 candidates of size 16
 -- looking through 2189 candidates of size 17
+-- tested 2599 candidates
 duplicates []  =  []
 duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
 
@@ -60,6 +62,7 @@
 -- looking through 4520 candidates of size 12
 -- looking through 10066 candidates of size 13
 -- looking through 21492 candidates of size 14
+-- tested 19274 candidates
 positionsFrom x y []  =  []
 positionsFrom x y (z:xs)  =  (if y == z then (x :) else id) (positionsFrom (x + 1) y xs)
 
diff --git a/eg/factorial.out b/eg/factorial.out
--- a/eg/factorial.out
+++ b/eg/factorial.out
@@ -8,6 +8,7 @@
 -- looking through 75 candidates of size 5
 -- looking through 183 candidates of size 6
 -- looking through 577 candidates of size 7
+-- tested 343 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -20,5 +21,6 @@
 -- looking through 34 candidates of size 4
 -- looking through 75 candidates of size 5
 -- looking through 247 candidates of size 6
+-- tested 172 candidates
 factorial x  =  foldr (*) 1 [1..x]
 
diff --git a/eg/fib01.out b/eg/fib01.out
--- a/eg/fib01.out
+++ b/eg/fib01.out
@@ -6,6 +6,7 @@
 -- looking through 295 candidates of size 3
 -- looking through 1968 candidates of size 4
 -- looking through 10684 candidates of size 5
+-- tested 12982 candidates
 cannot conjure
 
 fib01 :: Int -> Int -> Int -> Int
@@ -21,5 +22,6 @@
 -- looking through 391 candidates of size 8
 -- looking through 840 candidates of size 9
 -- looking through 6414 candidates of size 10
+-- tested 8002 candidates
 cannot conjure
 
diff --git a/eg/fibonacci.out b/eg/fibonacci.out
--- a/eg/fibonacci.out
+++ b/eg/fibonacci.out
@@ -13,6 +13,7 @@
 -- looking through 13000 candidates of size 10
 -- looking through 33460 candidates of size 11
 -- looking through 85901 candidates of size 12
+-- tested 56285 candidates
 fibonacci 0  =  1
 fibonacci 1  =  1
 fibonacci x  =  fibonacci (x - 1) + fibonacci (x - 2)
diff --git a/eg/gcd.out b/eg/gcd.out
--- a/eg/gcd.out
+++ b/eg/gcd.out
@@ -7,6 +7,7 @@
 -- looking through 60 candidates of size 4
 -- looking through 150 candidates of size 5
 -- looking through 472 candidates of size 6
+-- tested 246 candidates
 gcd x 0  =  x
 gcd x y  =  gcd y (x `mod` y)
 
diff --git a/eg/ints.out b/eg/ints.out
--- a/eg/ints.out
+++ b/eg/ints.out
@@ -4,6 +4,7 @@
 -- looking through 0 candidates of size 1
 -- looking through 1 candidates of size 2
 -- looking through 1 candidates of size 3
+-- tested 2 candidates
 second xs  =  head (tail xs)
 
 third :: [Int] -> Int
@@ -13,6 +14,7 @@
 -- looking through 1 candidates of size 2
 -- looking through 1 candidates of size 3
 -- looking through 1 candidates of size 4
+-- tested 3 candidates
 third xs  =  head (tail (tail xs))
 
 sum :: [Int] -> Int
@@ -23,6 +25,7 @@
 -- looking through 3 candidates of size 3
 -- looking through 13 candidates of size 4
 -- looking through 14 candidates of size 5
+-- tested 23 candidates
 sum []  =  0
 sum (x:xs)  =  x + sum xs
 
@@ -34,6 +37,7 @@
 -- looking through 3 candidates of size 3
 -- looking through 13 candidates of size 4
 -- looking through 14 candidates of size 5
+-- tested 33 candidates
 product []  =  1
 product (x:xs)  =  x * product xs
 
@@ -44,6 +48,7 @@
 -- looking through 4 candidates of size 2
 -- looking through 3 candidates of size 3
 -- looking through 16 candidates of size 4
+-- tested 10 candidates
 sum xs  =  foldr (+) 0 xs
 
 product :: [Int] -> Int
@@ -53,5 +58,6 @@
 -- looking through 4 candidates of size 2
 -- looking through 3 candidates of size 3
 -- looking through 16 candidates of size 4
+-- tested 12 candidates
 product xs  =  foldr (*) 1 xs
 
diff --git a/eg/list.out b/eg/list.out
--- a/eg/list.out
+++ b/eg/list.out
@@ -6,6 +6,7 @@
 -- looking through 3 candidates of size 3
 -- looking through 11 candidates of size 4
 -- looking through 10 candidates of size 5
+-- tested 23 candidates
 length []  =  0
 length (x:xs)  =  length xs + 1
 
@@ -18,6 +19,7 @@
 -- looking through 2 candidates of size 4
 -- looking through 5 candidates of size 5
 -- looking through 7 candidates of size 6
+-- tested 18 candidates
 reverse []  =  []
 reverse (x:xs)  =  reverse xs ++ unit x
 
@@ -30,6 +32,7 @@
 -- looking through 44 candidates of size 4
 -- looking through 116 candidates of size 5
 -- looking through 80 candidates of size 6
+-- tested 236 candidates
 [] ++ xs  =  xs
 (x:xs) ++ ys  =  x:(xs ++ ys)
 
@@ -41,6 +44,7 @@
 -- looking through 3 candidates of size 3
 -- looking through 13 candidates of size 4
 -- looking through 16 candidates of size 5
+-- tested 25 candidates
 length []  =  0
 length (x:xs)  =  length xs + 1
 
@@ -53,6 +57,7 @@
 -- looking through 2 candidates of size 4
 -- looking through 5 candidates of size 5
 -- looking through 15 candidates of size 6
+-- tested 18 candidates
 reverse []  =  []
 reverse (x:xs)  =  reverse xs ++ unit x
 
@@ -63,6 +68,7 @@
 -- looking through 8 candidates of size 2
 -- looking through 11 candidates of size 3
 -- looking through 48 candidates of size 4
+-- tested 57 candidates
 xs ++ ys  =  foldr (:) ys xs
 
 (\/) :: [Int] -> [Int] -> [Int]
@@ -74,6 +80,7 @@
 -- looking through 44 candidates of size 4
 -- looking through 116 candidates of size 5
 -- looking through 80 candidates of size 6
+-- tested 238 candidates
 [] \/ xs  =  xs
 (x:xs) \/ ys  =  x:ys \/ xs
 
diff --git a/eg/pow.out b/eg/pow.out
--- a/eg/pow.out
+++ b/eg/pow.out
@@ -9,6 +9,7 @@
 -- looking through 3438 candidates of size 6
 -- looking through 21096 candidates of size 7
 -- looking through 34780 candidates of size 8
+-- tested 27290 candidates
 pow x 0  =  1
 pow x y  =  x * pow x (y - 1)
 
@@ -21,5 +22,6 @@
 -- looking through 378 candidates of size 4
 -- looking through 1690 candidates of size 5
 -- looking through 4572 candidates of size 6
+-- tested 6778 candidates
 cannot conjure
 
diff --git a/eg/replicate.out b/eg/replicate.out
--- a/eg/replicate.out
+++ b/eg/replicate.out
@@ -9,6 +9,7 @@
 -- looking through 7 candidates of size 6
 -- looking through 5 candidates of size 7
 -- looking through 16 candidates of size 8
+-- tested 20 candidates
 replicate 0 c  =  ""
 replicate x c  =  c:replicate (x - 1) c
 
@@ -20,6 +21,7 @@
 -- looking through 0 candidates of size 3
 -- looking through 1 candidates of size 4
 -- looking through 1 candidates of size 5
+-- tested 3 candidates
 replicates cs x  =  concat (transpose (replicate x cs))
 
 replicates :: [Char] -> Int -> [Char]
@@ -30,6 +32,7 @@
 -- looking through 0 candidates of size 3
 -- looking through 0 candidates of size 4
 -- looking through 1 candidates of size 5
+-- tested 2 candidates
 replicates cs x  =  concat (map (replicate x) cs)
 
 replicates :: [Char] -> Int -> [Char]
@@ -43,6 +46,7 @@
 -- looking through 161 candidates of size 6
 -- looking through 469 candidates of size 7
 -- looking through 1303 candidates of size 8
+-- tested 791 candidates
 replicates "" x  =  ""
 replicates (c:cs) x  =  replicate x c ++ replicates cs x
 
diff --git a/eg/setelem.out b/eg/setelem.out
--- a/eg/setelem.out
+++ b/eg/setelem.out
@@ -9,6 +9,7 @@
 -- looking through 124 candidates of size 6
 -- looking through 305 candidates of size 7
 -- looking through 999 candidates of size 8
+-- tested 826 candidates
 elem x []  =  False
 elem x (y:xs)  =  x == y || elem x xs
 
@@ -23,6 +24,7 @@
 -- looking through 83 candidates of size 6
 -- looking through 245 candidates of size 7
 -- looking through 617 candidates of size 8
+-- tested 466 candidates
 set []  =  True
 set (x:xs)  =  not (elem x xs) && set xs
 
diff --git a/eg/sort.out b/eg/sort.out
--- a/eg/sort.out
+++ b/eg/sort.out
@@ -6,6 +6,7 @@
 -- looking through 7 candidates of size 3
 -- looking through 16 candidates of size 4
 -- looking through 36 candidates of size 5
+-- tested 31 candidates
 sort []  =  []
 sort (x:xs)  =  insert x (sort xs)
 
@@ -16,6 +17,7 @@
 -- looking through 1 candidates of size 2
 -- looking through 1 candidates of size 3
 -- looking through 4 candidates of size 4
+-- tested 6 candidates
 sort xs  =  foldr insert [] xs
 
 qsort :: [Int] -> [Int]
@@ -35,6 +37,7 @@
 -- looking through 767 candidates of size 12
 -- looking through 1600 candidates of size 13
 -- looking through 3499 candidates of size 14
+-- tested 3668 candidates
 qsort []  =  []
 qsort (x:xs)  =  filter (x >) (qsort xs) ++ (x:filter (x <=) (qsort xs))
 
@@ -53,5 +56,6 @@
 -- looking through 1448 candidates of size 10
 -- looking through 12905 candidates of size 11
 -- looking through 15208 candidates of size 12
+-- tested 34066 candidates
 cannot conjure
 
diff --git a/eg/spec.out b/eg/spec.out
--- a/eg/spec.out
+++ b/eg/spec.out
@@ -3,6 +3,7 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 9 candidates of size 3
+-- tested 12 candidates
 square x  =  x * x
 
 square :: Int -> Int
@@ -10,6 +11,7 @@
 -- looking through 3 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 9 candidates of size 3
+-- tested 12 candidates
 square x  =  x * x
 
 sum :: [Int] -> Int
@@ -19,6 +21,7 @@
 -- looking through 3 candidates of size 3
 -- looking through 4 candidates of size 4
 -- looking through 7 candidates of size 5
+-- tested 11 candidates
 sum []  =  0
 sum (x:xs)  =  x + sum xs
 
@@ -30,6 +33,7 @@
 -- looking through 28 candidates of size 4
 -- looking through 78 candidates of size 5
 -- looking through 172 candidates of size 6
+-- tested 196 candidates
 [] ++ xs  =  xs
 (x:xs) ++ ys  =  x:(xs ++ ys)
 
diff --git a/eg/subset.out b/eg/subset.out
--- a/eg/subset.out
+++ b/eg/subset.out
@@ -9,6 +9,7 @@
 -- looking through 0 candidates of size 6
 -- looking through 448 candidates of size 7
 -- looking through 784 candidates of size 8
+-- tested 1318 candidates
 subset [] xs  =  True
 subset (x:xs) ys  =  elem x ys && subset xs ys
 
@@ -20,5 +21,6 @@
 -- looking through 2 candidates of size 3
 -- looking through 6 candidates of size 4
 -- looking through 2 candidates of size 5
+-- tested 9 candidates
 subset xs ys  =  sort xs `isSubsequenceOf` sort ys
 
diff --git a/eg/tapps.out b/eg/tapps.out
--- a/eg/tapps.out
+++ b/eg/tapps.out
@@ -5,6 +5,7 @@
 -- looking through 5 candidates of size 2
 -- looking through 6 candidates of size 3
 -- looking through 20 candidates of size 4
+-- tested 18 candidates
 third xs  =  head (tail (tail xs))
 
 product :: [Int] -> Int
@@ -15,6 +16,7 @@
 -- looking through 6 candidates of size 3
 -- looking through 20 candidates of size 4
 -- looking through 34 candidates of size 5
+-- tested 44 candidates
 product []  =  1
 product (x:xs)  =  x * product xs
 
@@ -25,5 +27,6 @@
 -- looking through 5 candidates of size 2
 -- looking through 6 candidates of size 3
 -- looking through 23 candidates of size 4
+-- tested 20 candidates
 product xs  =  foldr (*) 1 xs
 
diff --git a/eg/tree.out b/eg/tree.out
--- a/eg/tree.out
+++ b/eg/tree.out
@@ -8,6 +8,7 @@
 -- looking through 0 candidates of size 5
 -- looking through 4 candidates of size 6
 -- looking through 16 candidates of size 7
+-- tested 9 candidates
 leftmost Leaf  =  undefined
 leftmost (Node t1 x t2)  =  if nil t1 then x else leftmost t1
 
@@ -21,6 +22,7 @@
 -- looking through 0 candidates of size 5
 -- looking through 4 candidates of size 6
 -- looking through 16 candidates of size 7
+-- tested 18 candidates
 rightmost Leaf  =  undefined
 rightmost (Node t1 x t2)  =  if nil t2 then x else rightmost t2
 
@@ -35,6 +37,7 @@
 -- looking through 66 candidates of size 6
 -- looking through 163 candidates of size 7
 -- looking through 311 candidates of size 8
+-- tested 428 candidates
 size Leaf  =  0
 size (Node t1 x t2)  =  size t1 + (size t2 + 1)
 
@@ -49,6 +52,7 @@
 -- looking through 472 candidates of size 6
 -- looking through 1440 candidates of size 7
 -- looking through 5781 candidates of size 8
+-- tested 4171 candidates
 height Leaf  =  -1
 height (Node t1 x t2)  =  max (height t1) (height t2) + 1
 
@@ -67,6 +71,7 @@
 -- looking through 0 candidates of size 10
 -- looking through 0 candidates of size 11
 -- looking through 184 candidates of size 12
+-- tested 107 candidates
 mem x Leaf  =  False
 mem x (Node t1 y t2)  =  mem x t1 || (x == y || mem x t2)
 
@@ -85,5 +90,6 @@
 -- looking through 2204 candidates of size 10
 -- looking through 3651 candidates of size 11
 -- looking through 8280 candidates of size 12
+-- tested 14743 candidates
 cannot conjure
 
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -32,6 +32,7 @@
   , conjureIsUnbreakable
   , conjureReification
   , conjureReification1
+  , conjureDynamicEq
   , cevaluate
   , ceval
   , cevl
@@ -48,6 +49,7 @@
 import Test.Speculate.Expr
 import Data.Functor ((<$>))
 import Control.Applicative ((<*>))
+import Data.Dynamic
 import Data.Express
 
 import Data.Int     -- for instances
@@ -273,6 +275,13 @@
 -- | Computes a function that makes an equation between two expressions.
 conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr
 conjureMkEquation f  =  mkEquation [eq | (_,Just eq,_,_,_,_) <- conjureReification f]
+
+conjureDynamicEq :: Conjurable f => f -> Dynamic
+conjureDynamicEq f  =  case conjureMkEquation f efxs efxs of
+                       (Value "==" deq :$ _ :$ _) -> deq
+                       _ -> error "conjureDynamicEq: expected an == but found something else.  Bug!"
+  where
+  efxs  =  conjureApplication "f" f
 
 -- | Given a 'Conjurable' functional value,
 --   computes a function that checks whether two 'Expr's are equal
diff --git a/src/Conjure/Conjurable/Derive.hs b/src/Conjure/Conjurable/Derive.hs
--- a/src/Conjure/Conjurable/Derive.hs
+++ b/src/Conjure/Conjurable/Derive.hs
@@ -126,11 +126,65 @@
                    conjureEquality  =  reifyEquality
                    conjureTiers     =  reifyTiers |]
   -- withTheReturnTypeOfs |++| (cxt |=>| inst)
-  cxt |=>| inst
--- TODO: derive conjureCases
--- TODO: derive conjureSize
--- TODO: derive conjureSubTypes (cf. Extrapolate.subInstances)
+  cxt |=>| inst `addFun` deriveSize t `mergeI` deriveSubTypes t `mergeI` deriveCases t
+-- TODO: derive conjureCases, e.g.:
+-- conjureCases mx  =  [ value "Nothing" (Nothing -: mx)
+--                     , value "Just" (Just ->: mx) :$ hole x
+--                     ]
 
+deriveCases :: Name -> DecsQ
+deriveCases t  =  do
+  n <- newName "x"
+  (nt,vs) <- normalizeType t
+  cs <- typeConstructorsArgNames t
+  let lets = [letin n c ns | (c,ns) <- cs]
+  let rhs = foldr (\e1 e2 -> [| $e1 : $e2 |]) [|[]|] lets
+  [d| instance Conjurable $(return nt) where
+        conjureCases $(varP n) = $rhs |]
+  where
+  letin :: Name -> Name -> [Name] -> ExpQ
+  letin x c ns = do
+    und <- VarE <$> lookupValN "undefined"
+    let lhs = conP c (map varP ns)
+    let rhs = return $ foldl AppE (ConE c) [und | _ <- ns]
+    let retTypeOf = varE $ mkName $ "-" ++ replicate (length ns) '>' ++ ":"
+    let ins = foldl (\e1 e2 -> [| $e1 :$ $e2 |])
+                [| value $(stringE $ nameBase c) ($retTypeOf $(conE c) $(varE x)) |]
+                [ [| hole $(varE n) |] | n <- ns ]
+    [| let $lhs = $rhs `asTypeOf` $(varE x) in $ins |]
+
+deriveSubTypes :: Name -> DecsQ
+deriveSubTypes t  =  do
+  n <- newName "x"
+  (nt,vs) <- normalizeType t
+  cs <- typeConstructorsArgNames t
+  let lets = [letin n c ns | (c,ns) <- cs, not (null ns)]
+  let rhs = foldr0 (\e1 e2 -> [| $e1 . $e2 |]) [|id|] lets
+  [d| instance Conjurable $(return nt) where
+        conjureSubTypes $(varP n) = $rhs |]
+  where
+  letin :: Name -> Name -> [Name] -> ExpQ
+  letin x c ns = do
+    und <- VarE <$> lookupValN "undefined"
+    let lhs = conP c (map varP ns)
+    let rhs = return $ foldl AppE (ConE c) [und | _ <- ns]
+    let bot = foldl1 (\e1 e2 -> [| $e1 . $e2 |])
+                     [ [| conjureType $(varE n) |] | n <- ns ]
+    [| let $lhs = $rhs `asTypeOf` $(varE x) in $bot |]
+
+deriveSize :: Name -> DecsQ
+deriveSize t  =  ((:[]) . FunD (mkName "conjureSize")) <$> deriveSizeClauses t
+
+deriveSizeClauses :: Name -> Q [Clause]
+deriveSizeClauses t  =  mapM (uncurry mkClause) =<< typeConstructors t
+  where
+  mkClause :: Name -> [Type] -> Q Clause
+  mkClause n as  =  clause pat body []
+    where
+    ns  =  take (length as) $ map mkName (variableNamesFromTemplate "x")
+    pat  =  [conP n [varP n | n <- ns]]
+    body  =  normalB $ foldl (\e n -> [| $e + conjureSize $(varE n) |]) [| 1 |] ns
+
 -- Not only really derive Conjurable instances,
 -- but cascade through argument types.
 reallyDeriveConjurableCascading :: Name -> DecsQ
@@ -164,4 +218,15 @@
   bind  =  id -- unbound variables are automatically bound
 #else
   bind  =  toBoundedQ
+#endif
+
+addFun :: DecsQ -> DecsQ -> DecsQ
+qds1 `addFun` qds2 = do ds1 <- qds1
+                        ds2 <- qds2
+                        return $ ds1 `m` ds2
+  where
+#if __GLASGOW_HASKELL__ < 800
+  [InstanceD   c ts ds1] `m` ds2 = [InstanceD   c ts (ds1 ++ ds2)]
+#else
+  [InstanceD o c ts ds1] `m` ds2 = [InstanceD o c ts (ds1 ++ ds2)]
 #endif
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -44,12 +44,14 @@
 import Data.Express.Fixtures hiding ((-==-))
 import qualified Data.Express.Triexpr as T
 
+import Data.Dynamic (fromDyn, dynApp)
+
 import Test.LeanCheck
 import Test.LeanCheck.Tiers
 import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
 
 import Test.Speculate.Reason (Thy, rules, equations, invalid, canReduceTo, printThy, closureLimit, doubleCheck)
-import Test.Speculate.Engine (theoryFromAtoms, groundBinds, boolTy)
+import Test.Speculate.Engine (theoryFromAtoms, grounds, groundBinds, boolTy)
 
 import Conjure.Expr
 import Conjure.Conjurable
@@ -162,6 +164,7 @@
   , requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments
   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates
   , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
+  , uniqueCandidates      :: Bool -- ^ unique-modulo-testing candidates
   }
 
 
@@ -175,6 +178,7 @@
 -- * search for defined applications for up to 100000 combinations
 -- * require recursive calls to deconstruct arguments
 -- * don't show the theory used in pruning
+-- * do not make candidates unique module testing
 args :: Args
 args = Args
   { maxTests               =  360
@@ -186,6 +190,7 @@
   , requireDescent         =  True
   , usePatterns            =  True
   , showTheory             =  False
+  , uniqueCandidates       =  False
   }
 
 
@@ -216,17 +221,19 @@
     putStrLn $ "-- reasoning produced "
             ++ show (length (invalid thy)) ++ " incorrect properties,"
             ++ " please re-run with more tests for faster results"
-  pr 1 rs
+  pr 1 0 rs
   where
-  pr n []  =  putStrLn $ "cannot conjure\n"
-  pr n ((is,cs):rs)  =  do
-    putStrLn $ "-- looking through "
-            ++ show (length cs)
-            ++ " candidates of size " ++ show n
+  pr n t []  =  do putStrLn $ "-- tested " ++ show t ++ " candidates"
+                   putStrLn $ "cannot conjure\n"
+  pr n t ((is,cs):rs)  =  do
+    let nc  =  length cs
+    putStrLn $ "-- looking through " ++ show nc ++ " candidates of size " ++ show n
     -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs
     case is of
-      []     ->  pr (n+1) rs
-      (i:_)  ->  putStrLn $ showDefn i
+      []     ->  pr (n+1) (t+nc) rs
+      (i:_)  ->  do let nc' = fromMaybe nc (findIndex (i==) cs)
+                    putStrLn $ "-- tested " ++ show (t+nc'+1) ++ " candidates"
+                    putStrLn $ showDefn i
   rs  =  zip iss css
   (iss, css, ts, thy)  =  conjpure0With args nm f p es
   nRules  =  length (rules thy)
@@ -274,7 +281,8 @@
   implements fx  =  defnApparentlyTerminates fx
                  && requal fx ffxx vffxx
                  && errorToFalse (p (cevl maxEvalRecursions fx))
-  candidatesT  =  take maxSize candidatesTT
+  candidatesT  =  (if uniqueCandidates then nubCandidates args nm f else id)
+               $  take maxSize candidatesTT
   (candidatesTT, thy)  =  candidateDefns args nm f es
   ffxx   =  conjureApplication nm f
   vffxx  =  conjureVarApplication nm f
@@ -311,11 +319,25 @@
 
 -- | Return apparently unique candidate definitions.
 candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
-candidateDefns args  =  cds args
+candidateDefns args  =  candidateDefns' args
   where
-  cds  =  if usePatterns args
-          then candidateDefnsC
-          else candidateDefns1
+  candidateDefns'  =  if usePatterns args
+                      then candidateDefnsC
+                      else candidateDefns1
+
+
+nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]
+nubCandidates Args{..} nm f  =  discardLaterT (===)
+  where
+  err  =  error "nubCandidates: unexpected evaluation error."
+  eq  =  conjureDynamicEq f
+  d1 === d2  =  all are $ take maxTests $ grounds (conjureTiersFor f) (conjureVarApplication nm f)
+    where
+    are :: Expr -> Bool
+    are e  =  errorToFalse -- silences errors, ok since this is for optional measuring of optimal pruning
+           $  (`fromDyn` err)
+           $  eq `dynApp` fromMaybe err (toDynamicWithDefn (conjureExpress f) maxEvalRecursions d1 e)
+                 `dynApp` fromMaybe err (toDynamicWithDefn (conjureExpress f) maxEvalRecursions d2 e)
 
 
 -- | Return apparently unique candidate definitions
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -31,6 +31,7 @@
   , allEqual
   , choices
   , choicesThat
+  , foldr0
   )
 where
 
@@ -126,3 +127,8 @@
 -- | Lists choices of values that follow a property.
 choicesThat :: (a -> [a] -> Bool) -> [a] -> [(a,[a])]
 choicesThat (?)  =  filter (uncurry (?)) . choices
+
+-- | A variation of foldr that only uses "zero" when the list is empty
+foldr0 :: (a -> a -> a) -> a -> [a] -> a
+foldr0 f z xs | null xs   = z
+              | otherwise = foldr1 f xs
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -3,7 +3,7 @@
 # Copyright (C) 2021 Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
-resolver: lts-17.9 # or ghc-8.10.4
+resolver: lts-18.14 # or ghc-8.10.7
 
 packages:
 - .
diff --git a/test/conjurable.hs b/test/conjurable.hs
--- a/test/conjurable.hs
+++ b/test/conjurable.hs
@@ -4,6 +4,7 @@
 {-# Language DeriveDataTypeable, StandaloneDeriving #-}  -- for GHC < 7.10
 
 import Test
+import Data.Dynamic
 
 -- An Unit type that is not an Eq instance
 data Unit  =  Unit  deriving Show
@@ -193,6 +194,76 @@
          ]
        ]
 
+  , concat (conjurePats [zero, one] "foo" (undefined :: [Int] -> Int -> Int))
+    == [ [ ffoo xxs xx
+         ]
+       , [ ffoo xxs zero
+         , ffoo xxs xx
+         ]
+       , [ ffoo nil xx
+         , ffoo (xx -:- xxs) yy
+         ]
+       , [ ffoo xxs one
+         , ffoo xxs xx
+         ]
+       , [ ffoo nil zero
+         , ffoo nil xx
+         , ffoo (xx -:- xxs) zero
+         , ffoo (xx -:- xxs) yy
+         ]
+       , [ ffoo xxs zero
+         , ffoo xxs one
+         , ffoo xxs xx
+         ]
+       , [ ffoo nil one
+         , ffoo nil xx
+         , ffoo (xx -:- xxs) one
+         , ffoo (xx -:- xxs) yy
+         ]
+       , [ ffoo nil zero
+         , ffoo nil one
+         , ffoo nil xx
+         , ffoo (xx -:- xxs) zero
+         , ffoo (xx -:- xxs) one
+         , ffoo (xx -:- xxs) yy
+         ]
+       ]
+
+  , concat (conjurePats [zero, one] "foo" (undefined :: Int -> [Int] -> Int))
+    == [ [ ffoo xx xxs
+         ]
+       , [ ffoo xx nil
+         , ffoo xx (yy -:- xxs)
+         ]
+       , [ ffoo zero xxs
+         , ffoo xx xxs
+         ]
+       , [ ffoo zero nil
+         , ffoo zero (xx -:- xxs)
+         , ffoo xx nil
+         , ffoo xx (yy -:- xxs)
+         ]
+       , [ ffoo one xxs
+         , ffoo xx xxs
+         ]
+       , [ ffoo one nil
+         , ffoo one (xx -:- xxs)
+         , ffoo xx nil
+         , ffoo xx (yy -:- xxs)
+         ]
+       , [ ffoo zero xxs
+         , ffoo one xxs
+         , ffoo xx xxs
+         ]
+       , [ ffoo zero nil
+         , ffoo zero (xx -:- xxs)
+         , ffoo one nil
+         , ffoo one (xx -:- xxs)
+         , ffoo xx nil
+         , ffoo xx (yy -:- xxs)
+         ]
+       ]
+
   , conjurePats [] "foo" (undefined :: [Int] -> [Char] -> Int)
     == [ [ [ ffoo xxs ccs
            ]
@@ -248,6 +319,11 @@
                                                  ]
   , candidateDeconstructionsFrom (div' xx xx) == []
   , candidateDeconstructionsFrom ((xx -+- xx) -+- yy) == [(xx -+- xx) -+- i_]
+
+  , fromDynamic (conjureDynamicEq ((+) :: Int -> Int -> Int) `dynApp` toDyn (1::Int) `dynApp` toDyn (2::Int))
+    == Just False
+  , fromDynamic (conjureDynamicEq ((+) :: Int -> Int -> Int) `dynApp` toDyn (1::Int) `dynApp` toDyn (1::Int))
+    == Just True
   ]
 
 isDecon :: Expr -> Bool
@@ -259,9 +335,15 @@
   ffE  =  var "f" (undefined :: [Int] -> Int)
 
 ffoo :: Expr -> Expr -> Expr
-ffoo e1 e2  =  fooE :$ e1 :$ e2
+ffoo ex ey  =  headOr err . mapMaybe ($$ ey) . mapMaybe ($$ ex)
+            $  [ var "foo" (undefined :: [Int] -> [Char] -> Int)
+               , var "foo" (undefined :: Int -> [Int] -> Int)
+               , var "foo" (undefined :: [Int] -> Int -> Int)
+               ]
   where
-  fooE  =  var "foo" (undefined :: [Int] -> [Char] -> Int)
+  err  =  error $ "ffoo: cannot apply `foo :: * -> * -> *` to `"
+               ++ show ex ++ "' and `" ++ show ey ++ "'.  Unhandled types?"
+
 
 -- Equality but obtained through conjurable
 (<==>) :: Conjurable a => a -> a -> Bool
diff --git a/test/derive.hs b/test/derive.hs
--- a/test/derive.hs
+++ b/test/derive.hs
@@ -3,6 +3,9 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 
+-- uncomment to debug derivation:
+-- {-# OPTIONS_GHC -ddump-splices #-}
+
 import Test hiding ((-:), (->:))
 -- -: and ->: should be generated by deriveConjurable
 
@@ -74,6 +77,78 @@
   , conjurableOK (undefined :: Bush Int)
   , conjurableOK (undefined :: Tree Int)
 --, conjurableOK (undefined :: RN) -- TODO: FIX: infinite loop somewhere...
+
+  , conjureSize Ae == 1
+  , conjureSize Bee == 1
+  , conjureSize Cee == 1
+  , conjureSize Zero == 1
+  , conjureSize (Succ Zero) == 2
+  , conjureSize (Succ (Succ Zero)) == 3
+  , conjureSize (Nil :: List Int) == 1
+  , conjureSize (10 :- (20 :- Nil) :: List Int) == 33
+
+  , conjureCases choice
+    == [ val Ae
+       , val Bee
+       , val Cee
+       ]
+
+  , conjureCases peano
+    == [ val Zero
+       , value "Succ" Succ :$ hole (undefined :: Peano)
+       ]
+
+  , conjureCases (lst int)
+    == [ value ":-" ((:-) ->>: lst int) :$ hole int :$ hole (lst int)
+       , val (Nil :: List Int)
+       ]
+
+  , conjureCases (bush int)
+    == [ value ":-:" ((:-:) ->>: bush int) :$ hole (bush int) :$ hole (bush int)
+       , value "Leaf" (Leaf ->: bush int) :$ hole int
+       ]
+
+  , conjureCases (tree int)
+    == [ value "Node" (Node ->>>: tree int) :$ hole (tree int) :$ hole int :$ hole (tree int)
+       , val (Null :: Tree Int)
+       ]
+
+  , conjureCases nested
+    == [ value "Nested" Nested :$ hole n0 :$ hole (n1 int) :$ hole (n2 int int)
+       ]
+
+  , conjureHoles (undefined :: Choice) == [ hole (undefined :: Choice)
+                                          , hole (undefined :: Bool)
+                                          ]
+  , conjureHoles (undefined :: Peano) == [ hole (undefined :: Peano)
+                                         , hole (undefined :: Bool)
+                                         ]
+  , conjureHoles (undefined :: List Int) == [ hole (undefined :: Int)
+                                            , hole (undefined :: List Int)
+                                            , hole (undefined :: Bool)
+                                            ]
+  , conjureHoles (undefined :: Nested) == [ hole (undefined :: N0)
+                                          , hole (undefined :: N1 Int)
+                                          , hole (undefined :: Int)
+                                          , hole (undefined :: N2 Int Int)
+                                          , hole (undefined :: Nested)
+                                          , hole (undefined :: Bool)
+                                          ]
+  , conjureHoles (undefined :: RN) == [ hole (undefined :: RN0)
+                                      , hole (undefined :: RN1 Int)
+                                      , hole (undefined :: Int)
+                                      , hole (undefined :: RN2 Int RN)
+                                      , hole (undefined :: RN)
+                                      , hole (undefined :: Bool)
+                                      ]
+  , conjureHoles (undefined :: Mutual) == [ hole (undefined :: CoMutual)
+                                          , hole (undefined :: Mutual)
+                                          , hole (undefined :: Bool)
+                                          ]
+  , conjureHoles (undefined :: CoMutual) == [ hole (undefined :: Mutual)
+                                            , hole (undefined :: CoMutual)
+                                            , hole (undefined :: Bool)
+                                            ]
   ]
 
 
@@ -89,3 +164,32 @@
   (-==-)  =  evl (fromJust $ conjureEquality x) -:> x
   tiers'  =  mapT evl (fromJust $ conjureTiers x) -: [[x]]
   expr'  =  (conjureExpress x . val) -:> x
+
+
+-- proxies --
+choice :: Choice
+choice  =  undefined
+
+peano :: Peano
+peano  =  undefined
+
+lst :: a -> List a
+lst _  =  undefined
+
+bush :: a -> Bush a
+bush _  =  undefined
+
+tree :: a -> Tree a
+tree _  =  undefined
+
+nested :: Nested
+nested  =  undefined
+
+n0 :: N0
+n0  =  undefined
+
+n1 :: a -> N1 a
+n1 _  =  undefined
+
+n2 :: a -> b -> N2 a b
+n2 _ _  =  undefined