diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -65,3 +65,4 @@
 test/utils
 test/cases
 test/defn
+test/derive
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,11 @@
 GHCFLAGS = -O2 \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic)
 HADDOCKFLAGS = \
+  -i $(shell find ~/.cabal -name express.haddock | tail -1) \
+  -i $(shell find ~/.cabal -name speculate.haddock | tail -1) \
+  -i $(shell find /usr/share/doc/ghc/html/libraries -name template-haskell.haddock | tail -1) \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic)
+HADDOCK_FILTER = grep -v "^Warning: Couldn't find .haddock for export [A-Z]$$"
 INSTALL_DEPS = leancheck express speculate
 
 EG = \
@@ -113,5 +117,15 @@
 avgs:
 	runhaskell bench/avgs.hs <bench/runtime/$$HOSTNAME/p12.runtimes
 	runhaskell bench/avgs.hs <bench/runtime/$$HOSTNAME/p30.runtimes
+
+gps-each: bench/gps
+	for i in {1..29}; do ./bench/time ./bench/gps $$i; done
+
+terpret-each: bench/terpret
+	for i in {1..8}; do ./bench/time ./bench/terpret $$i; done
+
+gps2-each: bench/gps2
+	for i in {1..25}; do ./bench/time ./bench/gps2 $$i; done
+
 
 include mk/haskell.mk
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -8,11 +8,7 @@
 
 ![Conjure logo][conjure-logo]
 
-Conjure is a tool that produces Haskell functions out of partial definitions.
-
-This is currently an experimental tool in its early stages,
-don't expect much from its current version.
-It is just a piece of curiosity in its current state.
+Conjure is a tool that synthesizes Haskell functions out of partial definitions.
 
 
 Installing
@@ -34,21 +30,27 @@
 -- not to be confused with [Conjure the BitTorrent client].
 
 
-Conjuring functions
--------------------
+Synthesizing functions
+----------------------
 
-You first need to import the library with:
+To use Conjure, import the library with:
 
 	import Conjure
 
-Then, given
+Then, declare a partial definition of a function to be synthesized.
+For example,
+here is a partial implementation of a function that squares a number:
 
 	square :: Int -> Int
 	square 0  =  0
 	square 1  =  1
 	square 2  =  4
 
-and
+Next, declare a list of primitives that seem like interesting pieces
+in the final fully-defined implementation.
+For example,
+here is a list of primitives including
+addition, multiplication and their neutral elements:
 
 	primitives :: [Prim]
 	primitives  =  [ pr (0::Int)
@@ -57,12 +59,10 @@
 	               , prim "*" ((*) :: Int -> Int -> Int)
 	               ]
 
-running
+Finally, call the [`conjure`] function,
+passing the function name, the partial definition and the list of primitives:
 
 	> conjure "square" square primitives
-
-yields
-
 	square :: Int -> Int
 	-- testing 3 combinations of argument values
 	-- pruning with 14/25 rules
@@ -71,23 +71,27 @@
 	-- looking through 9 candidates of size 3
 	square x  =  x * x
 
-in less than a second.
+Conjure is able to synthesize the above implementation in less than a second.
 
-See the `eg/arith.hs` example.
+For more information, see the `eg/arith.hs` example and
+the Haddock documentation for the [`conjure`] and [`conjureWith`] functions.
 
 
-Conjuring recursive functions
------------------------------
+Synthesizing recursive functions
+--------------------------------
 
-Given
+Conjure supports synthetization of recursive functions.
 
+Take for example the following partial implementation of a function
+that computes the factorial of a number:
+
 	factorial :: Int -> Int
 	factorial 1  =  1
 	factorial 2  =  2
 	factorial 3  =  6
 	factorial 4  =  24
 
-and
+Here is a list of primitives:
 
 	primitives :: [Prim]
 	primitives  =  [ pr (0::Int)
@@ -97,12 +101,10 @@
 	               , prim "-" ((-) :: Int -> Int -> Int)
 	               ]
 
-running
+And here is what Conjure produces
+with the above partial definition and list of primitives:
 
 	> conjure "factorial" factorial primitives
-
-yields
-
 	factorial :: Int -> Int
 	-- testing 4 combinations of argument values
 	-- pruning with 27/65 rules
@@ -116,25 +118,185 @@
 	factorial 0  =  1
 	factorial x  =  x * factorial (x - 1)
 
-in less than a second.
+The above synthetization takes less than a second.
 
-It is also possible to generate
+It is also possible to generate a folding implementation
+like the following:
 
 	factorial x  =  foldr (*) 1 [1..x]
 
-by including `enumFromTo` and `foldr` in the background.
+by including [`enumFromTo`] and [`foldr`] in the background.
 
-See the `eg/factorial.hs` example.
+For more information, see the `eg/factorial.hs` example and
+the Haddock documentation for the [`conjure`] and [`conjureWith`] functions.
 
 
+Synthesizing from specifications (for advanced users)
+-----------------------------------------------------
+
+Conjure also supports synthesizing from a functional specification
+with the functions [`conjureFromSpec`] and [`conjureFromSpecWith`]
+as, in some cases,
+a partial definition may not be appropriate
+for one of two reasons:
+
+1. Conjure may fail to "hit" the appropriate data points;
+2. specifying argument-result bindings may not be easy.
+
+Take for example a function `duplicates :: Eq a => [a] -> [a]`
+that should return the duplicate elements in a list without repetitions.
+
+Let's start with the primitives:
+
+	primitives :: [Prim]
+	primitives  =  [ pr ([] :: [Int])
+	               , prim "not" not
+	               , prim "&&" (&&)
+	               , prim ":" ((:) :: Int -> [Int] -> [Int])
+	               , prim "elem" (elem :: Int -> [Int] -> Bool)
+	               , prif (undefined :: [Int])
+	               ]
+
+Now here's a first attempt at a partial definition:
+
+	duplicates' :: [Int] -> [Int]
+	duplicates' []  =  []
+	duplicates' [1,2,3,4,5]  =  []
+	duplicates' [1,2,2,3,4]  =  [2]
+	duplicates' [1,2,3,3,3]  =  [3]
+	duplicates' [1,2,2,3,3]  =  [2,3]
+
+Here is what [`conjureWith`] prints:
+
+	> conjureWith args{maxSize=18} "duplicates" duplicates primitives
+	duplicates :: [Int] -> [Int]
+	-- testing 1 combinations of argument values
+	-- pruning with 21/26 rules
+	-- looking through 2 candidates of size 1
+	duplicates xs  =  xs
+
+The generated function clearly does not follow our specification.
+But if we look at the reported number of tests,
+we see that only _one_ of the argument-result bindings
+of our partial definition was used.
+Conjure failed to hit any of the argument values with five elements.
+(Since Conjure uses enumeration to test functions these values have to be kept "small").
+
+Here is a second attempt:
+
+	duplicates :: [Int] -> [Int]
+	duplicates [0,0]  =  [0]
+	duplicates [0,1]  =  []
+	duplicates [1,0,1]  =  [1]
+
+Here is what [`conjureWith`] now prints:
+
+	> conjureWith args{maxSize=18} "duplicates" duplicates primitives
+	duplicates :: [Int] -> [Int]
+	-- testing 3 combinations of argument values
+	-- pruning with 21/26 rules
+	-- ...
+	-- looking through 16 candidates of size 9
+	duplicates []  =  []
+	duplicates (x:xs)  =  if elem x xs then [x] else []
+
+The `duplicates` function that Conjure generated is still not correct.
+Nevertheless, it does follow our partial definition.  We have to refine it.
+Here is a third attempt with more argument-result bindings:
+
+	duplicates :: [Int] -> [Int]
+	duplicates [0,0]  =  [0]
+	duplicates [0,1]  =  []
+	duplicates [1,0,1]  =  [1]
+	duplicates [0,1,0,1]  =  [0,1]
+
+Here is what Conjure prints:
+
+	duplicates []  =  []
+	duplicates (x:xs)  =  if elem x xs then x:duplicates xs else []
+
+This implementation follows our partial definition, but may return duplicate duplicates,
+see:
+
+	duplicates [1,0,1,0,1]  =  [1,0,1]
+
+Here is a fourth and final refinement:
+
+	duplicates :: [Int] -> [Int]
+	duplicates [0,0]  =  [0]
+	duplicates [0,1]  =  []
+	duplicates [1,0,1]  =  [1]
+	duplicates [0,1,0,1]  =  [0,1]
+	duplicates [1,0,1,0,1]  =  [0,1]
+	duplicates [0,1,2,1]  =  [1]
+
+Now Conjure prints a correct implementation:
+
+	> conjureWith args{maxSize=18} "duplicates" duplicates primitives
+	duplicates :: [Int] -> [Int]
+	-- testing 6 combinations of argument values
+	-- ...
+	-- looking through 2189 candidates of size 17
+	duplicates []  =  []
+	duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
+	(in 1.5s)
+
+In this case,
+specifying the function with specific argument-result bindings
+is perhaps not the best approach.
+It took us four refinements of the partial definition to get a result.
+Specifying test properties perhaps better describes what we want.
+Again, we would like `duplicates` to return all duplicate elements
+without repetitions.
+This can be encoded in a function using [`holds`] from [LeanCheck]:
+
+	import Test.LeanCheck (holds)
+
+	duplicatesSpec :: ([Int] -> [Int]) -> Bool
+	duplicatesSpec duplicates  =  and
+	  [ holds 360 $ \x xs -> (count (x ==) xs > 1) == elem x (duplicates xs)
+	  , holds 360 $ \x xs -> count (x ==) (duplicates xs) <= 1
+	  ]  where  count p  =  length . filter p
+
+This function takes as argument a candidate implementation of `duplicates`
+and returns whether it is valid.
+The first property states that all duplicates must be listed.
+The second property states that duplicates themselves must not repeat.
+
+Now, we can use the function [`conjureFromSpecWith`] to generate the same duplicates function
+passing our `duplicatesSpec` as argument:
+
+	> conjureFromSpecWith args{maxSize=18} "duplicates" duplicatesSpec primitives
+	duplicates :: [Int] -> [Int]
+	duplicates []  =  []
+	duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
+	(in 1.5s)
+
+For more information see the `eg/dupos.hs` example and
+the Haddock documentation for the [`conjureFromSpec`] and [`conjureFromSpecWith`] functions.
+
+The functions [`conjureFromSpec`] and [`conjureFromSpecWith`] also accept specifications
+that bind specific arguments to results.
+Just use `==` and `&&` accordingly:
+
+	duplicatesSpec :: ([Int] -> [Int]) -> Bool
+	duplicatesSpec duplicates  =  duplicates [0,0] == [0]
+	                           && duplicates [0,1]  ==  []
+	                           && duplicates [1,0,1]  ==  [1]
+	                           && duplicates [0,1,0,1]  ==  [0,1]
+	                           && duplicates [1,0,1,0,1]  ==  [0,1]
+	                           && duplicates [0,1,2,1]  ==  [1]
+
+With this, there is no way for Conjure to miss argument-result bindings.
+
+
 Related work
 ------------
 
 [MagicHaskeller] (2007) is another tool
 that is able to generate Haskell code automatically.
 It supports recursion through
-catamorphisms, paramorphisms and the [fix] function.
-It is more mature than Conjure and is several orders of magnitude faster.
+catamorphisms, paramorphisms and the [`fix`] function.
 
 [Barliman] for Lisp is another tool that does program synthesis.
 
@@ -148,14 +310,25 @@
 For a detailed documentation of each function, see
 [Conjure's Haddock documentation].
 
+The `eg` folder in the source distribution
+contains more than 60 examples of use.
 
+
 Conjure, Copyright 2021  Rudy Matela,
 distribued under the 3-clause BSD license.
 
 
 [Conjure's Haddock documentation]: https://hackage.haskell.org/package/code-conjure/docs/Conjure.html
-[fix]: https://hackage.haskell.org/package/base/docs/Data-Function.html#v:fix
+[`conjure`]:             https://hackage.haskell.org/package/code-conjure/docs/Conjure.html#v:conjure
+[`conjureWith`]:         https://hackage.haskell.org/package/code-conjure/docs/Conjure.html#v:conjureWith
+[`conjureFromSpec`]:     https://hackage.haskell.org/package/code-conjure/docs/Conjure.html#v:conjureFromSpec
+[`conjureFromSpecWith`]: https://hackage.haskell.org/package/code-conjure/docs/Conjure.html#v:conjureFromSpecWith
 
+[`foldr`]:               https://hackage.haskell.org/package/base/docs/Prelude.html#v:foldr
+[`enumFromTo`]:          https://hackage.haskell.org/package/base/docs/Prelude.html#v:enumFromTo
+[`fix`]:                 https://hackage.haskell.org/package/base/docs/Data-Function.html#v:fix
+[`holds`]:               https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:holds
+
 [symbol `>`]: https://www.haskell.org/haddock/doc/html/ch03s08.html#idm140354810780208
 [Template Haskell]: https://wiki.haskell.org/Template_Haskell
 
@@ -167,6 +340,7 @@
 [Cabal]:   https://www.haskell.org/cabal
 [Haskell]: https://www.haskell.org/
 [leancheck]:      https://hackage.haskell.org/package/leancheck
+[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
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,6 +3,10 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
+* derive `conjureCases`, `conjureSize` and `conjureSubTypes`;
+
+* implement `deriveConjurable` using TH (cf. `deriveExpress` and `deriveGeneralizable`);
+
 * consider not breaking in some cases (increased crossproduct of patterns)
 
 * reduce the number of `deconstructions` considered:
diff --git a/bench/gps.hs b/bench/gps.hs
--- a/bench/gps.hs
+++ b/bench/gps.hs
@@ -587,9 +587,9 @@
 
 
 -- GPS Benchmark #20 -- Pig Latin --
-gps20p :: String -> String
-gps20p "hello world"  =  "ellohay orldway"
-gps20p "a string"  =  "aay tringsay"
+gps20s :: (String -> String) -> Bool
+gps20s pig  =  pig "hello world" == "ellohay orldway"
+            && pig "a string"    == "aay tringsay"
 
 gps20g :: String -> String
 gps20g  =  pig
@@ -602,11 +602,11 @@
                 then (c:cs) ++ "ay"
                 else cs ++ (c:"ay")
 
-pig1' :: String -> String
-pig1' "hello"   =  "ellohay"
-pig1' "world"   =  "orldway"
-pig1' "string"  =  "tringsay"
-pig1' "east"    =  "eastay"
+pig1Spec :: (String -> String) -> Bool
+pig1Spec pig1  =  pig1 "hello" == "ellohay"
+               && pig1 "world"  == "orldway"
+               && pig1 "string" == "tringsay"
+               && pig1 "east"   == "eastay"
 
 isVowel :: Char -> Bool
 isVowel 'a'  =  True
@@ -644,12 +644,7 @@
     , pr False
     ]
 
-  let force  =  [ [val "hello"]
-                , [val "world"]
-                , [val "string"]
-                , [val "east"]
-                ]
-  conjureWith args{forceTests=force, maxSize=14} "pig1" pig1'
+  conjureFromSpecWith args{maxSize=14} "pig1" pig1Spec
     [ pr "ay"
     , prif (undefined :: String)
     , prim "isVowel" isVowel
@@ -657,10 +652,7 @@
     , prim ":" ((:) :: Char -> String -> String)
     ]
 
-  let force  =  [ [val "hello world"]
-                , [val "a string"]
-                ]
-  conjureWith args{forceTests=force} "gps20c" gps20p
+  conjureFromSpec "gps20c" gps20s
     [ prim "words" (words :: String -> [String])
     , prim "unwords" (unwords :: [String] -> String)
     , prim "map" (map :: (String -> String) -> [String] -> [String])
@@ -692,11 +684,11 @@
 
 
 -- GPS Benchmark #22 -- Scrabble Score --
-gps22p :: String -> Int
-gps22p "a"  =  1
-gps22p "hello"  =  8
-gps22p "world"  =  9
-gps22p "scrabble"  =  14
+gps22s :: (String -> Int) -> Bool
+gps22s scrabble  =  scrabble "a" == 1
+                 && scrabble "hello" == 8
+                 && scrabble "world" == 9
+                 && scrabble "scrabble" == 14
 
 gps22g :: String -> Int
 gps22g  =  scrabble
@@ -725,13 +717,7 @@
 
 gps22c :: IO ()
 gps22c  =  do
-  let force  =  [ [val "a"]
-                , [val "hello"]
-                , [val "world"]
-                , [val "scrabble"]
-                ]
-
-  conjureWith args{forceTests=force} "gps22" gps22p
+  conjureFromSpec "gps22" gps22s
     [ pr (0 :: Int)
     , prim "+" ((+) :: Int -> Int -> Int)
     , prim "map" (map :: (Int -> Int) -> [Int] -> [Int])
@@ -865,13 +851,13 @@
 
 
 -- GPS Benchmark #29 -- Syllables --
-gps29p :: String -> Int
-gps29p "pub"  =  1
-gps29p "hello"  =  2
-gps29p "world"  =  1
-gps29p "string"  =  1
-gps29p "haskell"  =  2
-gps29p "photography"  =  4
+gps29s :: (String -> Int) -> Bool
+gps29s sys  =  sys "pub" == 1
+            && sys "hello" == 2
+            && sys "world" == 1
+            && sys "string" == 1
+            && sys "haskell" == 2
+            && sys "photography" == 4
 
 gps29g :: String -> Int
 gps29g ""  =  0
@@ -880,21 +866,13 @@
                   else gps29g cs
 
 gps29c :: IO ()
-gps29c  =  conjureWith args{forceTests=force} "gps29" gps29p
+gps29c  =  conjureFromSpec "gps29" gps29s
   [ pr (0 :: Int)
   , pr (1 :: Int)
   , prim "+" ((+) :: Int->Int->Int)
   , prif (undefined :: Int)
   , prim "isVowel" isVowel
   ]
-  where
-  force  =  [ [val "pub"]
-            , [val "hello"]
-            , [val "world"]
-            , [val "string"]
-            , [val "haskell"]
-            , [val "photography"]
-            ]
 
 
 main :: IO ()
diff --git a/bench/gps.out b/bench/gps.out
--- a/bench/gps.out
+++ b/bench/gps.out
@@ -339,7 +339,6 @@
 isVowel c  =  False
 
 pig1 :: [Char] -> [Char]
--- testing 4 combinations of argument values
 -- pruning with 5/5 rules
 -- looking through 2 candidates of size 1
 -- looking through 1 candidates of size 2
@@ -359,7 +358,6 @@
 pig1 (c:cs)  =  if isVowel c then (c:cs) ++ "ay" else cs ++ (c:"ay")
 
 gps20c :: [Char] -> [Char]
--- testing 2 combinations of argument values
 -- pruning with 1/1 rules
 -- looking through 1 candidates of size 1
 -- looking through 1 candidates of size 2
@@ -385,7 +383,6 @@
 gps21 (x:xs)  =  (if x < 0 then 0 else x):gps21 xs
 
 gps22 :: [Char] -> Int
--- testing 4 combinations of argument values
 -- pruning with 5/9 rules
 -- looking through 1 candidates of size 1
 -- looking through 0 candidates of size 2
@@ -460,7 +457,6 @@
 gps28 x y z x'  =  x `min` (y `min` (z `min` x'))
 
 gps29 :: [Char] -> Int
--- testing 6 combinations of argument values
 -- pruning with 7/11 rules
 -- looking through 2 candidates of size 1
 -- looking through 2 candidates of size 2
diff --git a/bench/gps2.hs b/bench/gps2.hs
--- a/bench/gps2.hs
+++ b/bench/gps2.hs
@@ -120,12 +120,10 @@
 -- considering we're getting input as kebab-case.
 -- Nevertheless, this one is out of reach performance-wise (and OOM-wise)
 
-gps4p :: String -> String
-gps4p "the-stealth-warrior"  =  "theStealthWarrior"
---gps4p "The_Stealth_Warrior"  =  "TheStealthWarrior"
-gps4p "camel-case"  =  "camelCase"
---gps4p "snake_case"  =  "snakeCase"
-gps4p "Kebab-Case"  =  "KebabCase"
+gps4s :: (String -> String) -> Bool
+gps4s g  =  g "the-stealth-warrior" == "theStealthWarrior"
+         && g "camel-case" == "camelCase"
+         && g "Kebab-Case" == "KebabCase"
 
 gps4g :: String -> String
 gps4g ""  =  ""
@@ -139,15 +137,8 @@
 
 gps4c :: IO ()
 gps4c  =  do
-  let force  =  [ [val "the-stealth-warrior"]
---              , [val "The_Stealth_Warrior"]
-                , [val "camel-case"]
---              , [val "snake_case"]
-                , [val "Kebab-Case"]
-                ]
-  conjureWith args{forceTests = force, maxSize=6} "gps4" gps4p
+  conjureFromSpecWith args{maxSize=6} "gps4" gps4s
     [ pr '-'
---  , pr '_'
     , pr ("" :: String)
     , prim ":" ((:) :: Char -> String -> String)
     , prim "==" ((==) :: Char -> Char -> Bool)
@@ -179,13 +170,13 @@
 gps5p  20  =  [0, 2, 0, 0]
 gps5p   3  =  [0, 0, 0, 3]
 
-gps5p2 :: [Int] -> Int -> [Int]
-gps5p2 [25, 10, 5, 1] 100  =  [4, 0, 0, 0]
-gps5p2 [25, 10, 5, 1]  50  =  [2, 0, 0, 0]
-gps5p2 [25, 10, 5, 1]  25  =  [1, 0, 0, 0]
-gps5p2 [25, 10, 5, 1]  30  =  [1, 0, 1, 0]
-gps5p2 [25, 10, 5, 1]  20  =  [0, 2, 0, 0]
-gps5p2 [25, 10, 5, 1]   3  =  [0, 0, 0, 3]
+gps5s :: ([Int] -> Int -> [Int]) -> Bool
+gps5s t  =  t [25, 10, 5, 1] 100 == [4, 0, 0, 0]
+         && t [25, 10, 5, 1]  50 == [2, 0, 0, 0]
+         && t [25, 10, 5, 1]  25 == [1, 0, 0, 0]
+         && t [25, 10, 5, 1]  30 == [1, 0, 1, 0]
+         && t [25, 10, 5, 1]  20 == [0, 2, 0, 0]
+         && t [25, 10, 5, 1]   3 == [0, 0, 0, 3]
 
 coins :: [Int]
 coins  =  [25, 10, 5, 1]
@@ -204,26 +195,19 @@
     [
     ]
 
-  let force = [ [val coins, val (100::Int)]
-              , [val coins, val ( 50::Int)]
-              , [val coins, val ( 25::Int)]
-              , [val coins, val ( 30::Int)]
-              , [val coins, val ( 20::Int)]
-              , [val coins, val (  3::Int)]
-              ]
-  conjureWith args{forceTests=force} "tell" gps5p2
+  conjureFromSpec "tell" gps5s
     [ pr ([] :: [Int])
     , prim ":" ((:) :: Int -> [Int] -> [Int])
     , prim "`div`" (div :: Int -> Int -> Int)
     , prim "`mod`" (mod :: Int -> Int -> Int)
     ]
 
-  conjureWith args{forceTests=force} "gps5" gps5p
+  conjure "gps5" gps5p
     [ pr coins
     , prim "tell" tell
     ]
 
-  conjureWith args{forceTests=force} "gps5" gps5p
+  conjure "gps5" gps5p
     [ pr (1 :: Int)
     , pr (5 :: Int)
     , pr (10 :: Int)
@@ -568,20 +552,20 @@
   ]
 
 
-gps21p :: String -> String
-gps21p "word"  =  "word"
-gps21p "words"  =  "sdrow"
-gps21p "word words"  =  "word sdrow"
-gps21p "words word"  =  "sdrow word"
+gps21s :: (String -> String) -> Bool
+gps21s s  =  s "word" == "word"
+          && s "words" == "sdrow"
+          && s "word words" == "word sdrow"
+          && s "words word" == "sdrow word"
 
-spin' :: String -> String
-spin' "abc"  =  "abc"
-spin' "abcd"  =  "abcd"
-spin' "word"  =  "word"
-spin' "abcde"  =  "edcba"
-spin' "words"  =  "sdrow"
-spin' "hello"  =  "olleh"
-spin' "world"  =  "dlrow"
+spinSpec :: (String -> String) -> Bool
+spinSpec spin  =  spin "abc" == "abc"
+               && spin "abcd" == "abcd"
+               && spin "word" == "word"
+               && spin "abcde" == "edcba"
+               && spin "words" == "sdrow"
+               && spin "hello" == "olleh"
+               && spin "world" == "dlrow"
 
 spin :: String -> String
 spin w  =  if length w >= 5
@@ -593,15 +577,7 @@
 
 gps21c :: IO ()
 gps21c  =  do
-  let force  =  [ [ val "abc" ]
-                , [ val "abcd" ]
-                , [ val "word" ]
-                , [ val "abcde" ]
-                , [ val "words" ]
-                , [ val "hello" ]
-                , [ val "world" ]
-                ]
-  conjureWith args{maxSize=12, forceTests=force} "spin" spin'
+  conjureFromSpec "spin" spinSpec
     [ prim "length"  (length :: String -> Int)
     , prim "reverse" (reverse :: String -> String)
     , prif (undefined :: String)
@@ -609,12 +585,7 @@
     , pr (5 :: Int)
     ]
 
-  let force  =  [ [ val "word" ]
-                , [ val "words" ]
-                , [ val "word words" ]
-                , [ val "words word" ]
-                ]
-  conjureWith args{maxSize=12, forceTests=force} "gps21_spinwords" gps21p
+  conjureFromSpec "gps21_spinwords" gps21s
     [ prim "words"   words
     , prim "unwords" unwords
     , prim "spin"    (spin :: String -> String)
@@ -657,11 +628,11 @@
     ]
 
 
-gps23p :: String -> String -> String -> String
-gps23p "abcd" "abcd" "abcd"  =  "abcd"
-gps23p "abcd" "dcba" "abcd"  =  "dcba"
-gps23p "abcd" "1234" "abcd"  =  "1234"
-gps23p "abcd" "1234" "bacd"  =  "2134"
+gps23s :: (String -> String -> String -> String) -> Bool
+gps23s s  =  s "abcd" "abcd" "abcd" == "abcd"
+          && s "abcd" "dcba" "abcd" == "dcba"
+          && s "abcd" "1234" "abcd" == "1234"
+          && s "abcd" "1234" "bacd" == "2134"
 
 gps23g :: String -> String -> String -> String
 -- gps23g f t s  =  map (\c -> fromJust $ c `lookup` zipWith (,) f t) s
@@ -669,13 +640,8 @@
 
 gps23c :: IO ()
 gps23c  =  do
-  let force = [ [ val "abcd", val "abcd", val "abcd" ]
-              , [ val "abcd", val "dcba", val "abcd" ]
-              , [ val "abcd", val "1234", val "abcd" ]
-              , [ val "abcd", val "1234", val "bacd" ]
-              ]
   -- cannot conjure, needs lambda
-  conjureWith args{forceTests=force} "gps23" gps23p
+  conjureFromSpec "gps23" gps23s
     [
     ]
 
@@ -708,20 +674,15 @@
                      then TooMany
                      else Tweet (length s)
 
-gps24p_twitter :: String -> Twitter
-gps24p_twitter "" =  Empty
-gps24p_twitter "abcd"  =  Tweet 4
-gps24p_twitter "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij"  =  Tweet 140
-gps24p_twitter "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghijX"  =  TooMany
+gps24s_twitter :: (String -> Twitter) -> Bool
+gps24s_twitter twitter  =  twitter "" == Empty
+                        && twitter "abcd" == Tweet 4
+                        && twitter "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij" == Tweet 140
+                        && twitter "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghijX" == TooMany
 
 gps24c :: IO ()
 gps24c  =  do
-  let force = [ [ val "" ]
-              , [ val "abcd" ]
-              , [ val "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij" ]
-              , [ val "0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghij0123456789abcdefghijX" ]
-              ]
-  conjureWith args{maxTests=360, forceTests=force} "gps24" gps24p_twitter
+  conjureFromSpecWith args{maxTests=360} "gps24" gps24s_twitter
     [ pr Empty
     , pr TooMany
     , prim "Tweet" Tweet
diff --git a/bench/gps2.out b/bench/gps2.out
--- a/bench/gps2.out
+++ b/bench/gps2.out
@@ -47,14 +47,12 @@
 cannot conjure
 
 gps3 :: [Char] -> Int
--- testing 0 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
 cannot conjure
 
 gps4 :: [Char] -> [Char]
--- testing 3 combinations of argument values
 -- pruning with 13/20 rules
 -- looking through 2 candidates of size 1
 -- looking through 3 candidates of size 2
@@ -71,7 +69,6 @@
 cannot conjure
 
 tell :: [Int] -> Int -> [Int]
--- testing 6 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 2 candidates of size 1
 -- looking through 1 candidates of size 2
@@ -183,14 +180,12 @@
 gps13_leaders (x:xs)  =  if all (x >) xs then x:gps13_leaders xs else gps13_leaders xs
 
 gps14_luhn :: [Int] -> Int
--- testing 0 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
 cannot conjure
 
 gps15_mastermind :: () -> ()
--- testing 0 combinations of argument values
 -- pruning with 0/1 rules
 -- looking through 1 candidates of size 1
 gps15_mastermind u  =  u
@@ -246,14 +241,12 @@
 cannot conjure
 
 gps20 :: [Char] -> Bool
--- testing 0 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
 cannot conjure
 
 spin :: [Char] -> [Char]
--- testing 7 combinations of argument values
 -- pruning with 6/6 rules
 -- reasoning produced 1 incorrect properties, please re-run with more tests for faster results
 -- looking through 1 candidates of size 1
@@ -267,7 +260,6 @@
 spin cs  =  if length cs >= 5 then reverse cs else cs
 
 gps21_spinwords :: [Char] -> [Char]
--- testing 4 combinations of argument values
 -- pruning with 16/16 rules
 -- reasoning produced 2 incorrect properties, please re-run with more tests for faster results
 -- looking through 1 candidates of size 1
@@ -295,13 +287,11 @@
 cannot conjure
 
 gps22 :: Int -> [Char]
--- testing 0 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 0 candidates of size 1
 cannot conjure
 
 gps23 :: [Char] -> [Char] -> [Char] -> [Char]
--- testing 4 combinations of argument values
 -- pruning with 0/0 rules
 -- looking through 3 candidates of size 1
 -- looking through 12 candidates of size 2
@@ -318,7 +308,6 @@
 cannot conjure
 
 gps24 :: [Char] -> Twitter
--- testing 4 combinations of argument values
 -- pruning with 4/8 rules
 -- reasoning produced 4 incorrect properties, please re-run with more tests for faster results
 -- looking through 2 candidates of size 1
diff --git a/bench/ill-hit.hs b/bench/ill-hit.hs
--- a/bench/ill-hit.hs
+++ b/bench/ill-hit.hs
@@ -14,34 +14,21 @@
 sum' [3,4,5]  =  12
 sum' [1,2,3,4]  =  10
 
-sumSpec :: [([Int],Int)]
-sumSpec  =  [ [] -= 0
-            , [1] -= 1
-            , [1,2] -= 3
-            , [1,2,3] -= 6
-            , [3,4,5] -= 12
-            , [1,2,3,4] -= 10
-            ]
+sumSpec :: ([Int] -> Int) -> Bool
+sumSpec sum  =  sum [] == 0
+             && sum [1] == 1
+             && sum [1,2] == 3
+             && sum [1,2,3] == 6
+             && sum [3,4,5] == 12
+             && sum [1,2,3,4] == 10
 
 main :: IO ()
 main  =  do
   -- the following does not hit all 6 defined prims, only 4
   conjure "sum" (sum' :: [Int] -> Int) primitives
 
-  -- the following forces 3 argument prims, totaling 6
-  conjureWith as "sum" (sum' :: [Int] -> Int) primitives
-
   -- the following conjures from a spec
-  conjure1 "sum" sumSpec primitives
-
-as :: Args
-as  =  args
-    {  forceTests = map (map val)
-                  [ [[1,2]]
-                  , [[3,4,5::Int]]
-                  , [[1,2,3,4]]
-                  ]
-    }
+  conjureFromSpec "sum" sumSpec primitives
 
 primitives :: [Prim]
 primitives =
diff --git a/bench/ill-hit.out b/bench/ill-hit.out
--- a/bench/ill-hit.out
+++ b/bench/ill-hit.out
@@ -10,18 +10,6 @@
 sum (x:xs)  =  x + sum xs
 
 sum :: [Int] -> Int
--- testing 6 combinations of argument values
--- pruning with 14/25 rules
--- looking through 2 candidates of size 1
--- looking through 5 candidates of size 2
--- looking through 6 candidates of size 3
--- looking through 20 candidates of size 4
--- looking through 34 candidates of size 5
-sum []  =  0
-sum (x:xs)  =  x + sum xs
-
-sum :: [Int] -> Int
--- testing 6 combinations of argument values
 -- pruning with 14/25 rules
 -- looking through 2 candidates of size 1
 -- looking through 5 candidates of size 2
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.1
+9.2
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 @@
-23.8
+22.8
diff --git a/bench/runtime/zero/bench/gps2.runtime b/bench/runtime/zero/bench/gps2.runtime
--- a/bench/runtime/zero/bench/gps2.runtime
+++ b/bench/runtime/zero/bench/gps2.runtime
@@ -1,1 +1,1 @@
-9.5
+9.3
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 @@
-1.3
+0.9
diff --git a/bench/runtime/zero/bench/p12.runtime b/bench/runtime/zero/bench/p12.runtime
--- a/bench/runtime/zero/bench/p12.runtime
+++ b/bench/runtime/zero/bench/p12.runtime
@@ -1,1 +1,1 @@
-3.2
+3.3
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.0
+13.2
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.4
+4.5
diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime
--- a/bench/runtime/zero/eg/fibonacci.runtime
+++ b/bench/runtime/zero/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-8.8
+8.2
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 @@
-0.6
+0.4
diff --git a/bench/runtime/zero/eg/pow.runtime b/bench/runtime/zero/eg/pow.runtime
--- a/bench/runtime/zero/eg/pow.runtime
+++ b/bench/runtime/zero/eg/pow.runtime
@@ -1,1 +1,1 @@
-3.5
+3.4
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 @@
-0.4
+1.1
diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime
--- a/bench/runtime/zero/eg/tree.runtime
+++ b/bench/runtime/zero/eg/tree.runtime
@@ -1,1 +1,1 @@
-1.5
+1.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.4
+GHC 8.10.5
 leancheck-0.9.10
 express-1.0.6
 speculate-0.4.14
diff --git a/bench/terpret.hs b/bench/terpret.hs
--- a/bench/terpret.hs
+++ b/bench/terpret.hs
@@ -66,9 +66,9 @@
 
 t3p :: [Bool] -> [Bool]
 -- t3p [True]  =  [False]
-t3p [True,True]  =  [False,True]             --  11 - 1 =  10
-t3p [False,True]  =  [True,False]            --  10 - 1 =   1
-t3p [False,True,True]  =  [True,False,True]  -- 110 - 1 = 101
+t3p [True,True]  =  [False,True]             -- 3-1=2
+t3p [False,True]  =  [True,False]            -- 2-1=1
+t3p [False,True,True]  =  [True,False,True]  -- 6-1=5
 
 t3g :: [Bool] -> [Bool]
 t3g []  =  []
diff --git a/bench/time b/bench/time
new file mode 100644
--- /dev/null
+++ b/bench/time
@@ -0,0 +1,9 @@
+#!/bin/bash
+#
+# bench/time: runs a program, discards stdout and print name and runtime
+#
+# Copyright (C) 2021 Rudy Matela
+# Distributed under the 3-Clause BSD licence (see the file LICENSE).
+
+printf "%-14s  " "$*"
+/usr/bin/time -f%e "$@" >/dev/null
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,16 @@
 ============================
 
 
+v0.5.0
+------
+
+* allow synthesizing/conjuring from properties with `conjureFromSpec`;
+* complete Haddock documentation;
+* remove several unused functions;
+* add stub `conjurableDerive` functions;
+* Makefile: add targets to run GPS(2) and TerpreT benches.
+
+
 v0.4.4
 ------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,14 +3,10 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.4.4
-synopsis:            conjure Haskell functions out of partial definitions
+version:             0.5.0
+synopsis:            synthesize Haskell functions out of partial definitions
 description:
-  Conjure is a tool that produces Haskell functions out of partial definitions.
-  .
-  This is currently an experimental tool in its early stages,
-  don't expect much from its current version.
-  It is just a piece of curiosity in its current state.
+  Conjure is a tool that synthesizes Haskell functions out of partial definitions.
 
 homepage:            https://github.com/rudymatela/conjure#readme
 license:             BSD3
@@ -48,6 +44,7 @@
                   , bench/runtime/zero/proto/*.runtime
                   , bench/runtime/zero/versions
                   , bench/versions
+                  , bench/time
                   , test/sdist
 tested-with: GHC==9.0
            , GHC==8.10
@@ -66,15 +63,15 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.4.4
+  tag:             v0.5.0
 
 library
   exposed-modules: Conjure
                  , Conjure.Conjurable
+                 , Conjure.Conjurable.Derive
                  , Conjure.Engine
                  , Conjure.Expr
                  , Conjure.Prim
-                 , Conjure.Spec
                  , Conjure.Utils
                  , Conjure.Defn
   other-extensions: TemplateHaskell, CPP
@@ -82,14 +79,14 @@
                , leancheck >= 0.9.10
                , template-haskell
                , speculate >= 0.4.14
-               , express >= 1.0.6
+               , express >= 1.0.8
   hs-source-dirs:      src
   default-language:    Haskell2010
 
 test-suite expr
   type:                exitcode-stdio-1.0
   main-is:             expr.hs
-  other-modules:       Test, Test.ListableExpr, Test.Candidates
+  other-modules:       Test, Test.ListableExpr
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
@@ -97,7 +94,7 @@
 test-suite defn
   type:                exitcode-stdio-1.0
   main-is:             defn.hs
-  other-modules:       Test, Test.ListableExpr, Test.Candidates
+  other-modules:       Test, Test.ListableExpr
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
@@ -105,7 +102,7 @@
 test-suite conjurable
   type:                exitcode-stdio-1.0
   main-is:             conjurable.hs
-  other-modules:       Test, Test.ListableExpr, Test.Candidates
+  other-modules:       Test, Test.ListableExpr
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
@@ -113,7 +110,15 @@
 test-suite utils
   type:                exitcode-stdio-1.0
   main-is:             utils.hs
-  other-modules:       Test, Test.ListableExpr, Test.Candidates
+  other-modules:       Test, Test.ListableExpr
+  hs-source-dirs:      test
+  build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
+  default-language:    Haskell2010
+
+test-suite derive
+  type:                exitcode-stdio-1.0
+  main-is:             derive.hs
+  other-modules:       Test, Test.ListableExpr
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
   default-language:    Haskell2010
diff --git a/eg/dupos.hs b/eg/dupos.hs
--- a/eg/dupos.hs
+++ b/eg/dupos.hs
@@ -3,6 +3,7 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
+import Test.LeanCheck  -- needed for duplicatesSpec only
 
 duplicates :: [Int] -> [Int] -- Eq a => [a] -> [a]
 duplicates []  =  []
@@ -21,6 +22,12 @@
 duplicates' [1,0,1,0,1]  =  [0,1]
 duplicates' [0,1,2,1]  =  [1]
 
+duplicatesSpec :: ([Int] -> [Int]) -> Bool
+duplicatesSpec duplicates  =  and
+  [ holds 360 $ \x xs -> (count (x ==) xs > 1) == elem x (duplicates xs)
+  , holds 360 $ \x xs -> count (x ==) (duplicates xs) <= 1
+  ]  where  count p  =  length . filter p
+
 positionsFrom :: Int -> Int -> [Int] -> [Int]
 positionsFrom n x  =  from n
   where
@@ -54,6 +61,15 @@
   --                       else duplicates xs                              -- 17
   -- within reach performance wise.
   conjureWith args{maxSize=18} "duplicates" duplicates'
+    [ pr ([] :: [Int])
+    , prim "not" not
+    , prim "&&" (&&)
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "elem" (elem :: Int -> [Int] -> Bool)
+    , prif (undefined :: [Int])
+    ]
+
+  conjureFromSpecWith args{maxSize=18} "duplicates" duplicatesSpec
     [ pr ([] :: [Int])
     , prim "not" not
     , prim "&&" (&&)
diff --git a/eg/dupos.out b/eg/dupos.out
--- a/eg/dupos.out
+++ b/eg/dupos.out
@@ -21,6 +21,28 @@
 duplicates []  =  []
 duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
 
+duplicates :: [Int] -> [Int]
+-- pruning with 21/26 rules
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 2 candidates of size 6
+-- looking through 3 candidates of size 7
+-- looking through 8 candidates of size 8
+-- looking through 16 candidates of size 9
+-- looking through 25 candidates of size 10
+-- looking through 36 candidates of size 11
+-- looking through 65 candidates of size 12
+-- looking through 141 candidates of size 13
+-- looking through 322 candidates of size 14
+-- looking through 644 candidates of size 15
+-- looking through 1189 candidates of size 16
+-- looking through 2189 candidates of size 17
+duplicates []  =  []
+duplicates (x:xs)  =  if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
+
 positionsFrom :: Int -> A -> [A] -> [Int]
 -- testing 360 combinations of argument values
 -- pruning with 5/10 rules
diff --git a/eg/list.hs b/eg/list.hs
--- a/eg/list.hs
+++ b/eg/list.hs
@@ -38,36 +38,21 @@
 
 main :: IO ()
 main = do
-  -- length xs  =  if null xs then 0 else 1 + length (tail xs)
-  --               1  2    3       4      5 6 7       8    9
   conjure "length" length'
     [ pr (0 :: Int)
     , pr (1 :: Int)
     , prim "+" ((+) :: Int -> Int -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     ]
 
-  -- reverse xs  =  if null xs then [] else reverse (tail xs) ++ [head xs]
-  --                1  2    3       4       5        6    7   8  9 10 11 12
-  -- needs size 11 with unit
   conjure "reverse" reverse'
     [ pr ([] :: [Int])
     , prim "unit" ((:[]) :: Int -> [Int])
     , prim "++" ((++) :: [Int] -> [Int] -> [Int])
-    , prim "head" (head :: [Int] -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     ]
 
-  -- xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
-  --              1  2    3       4       5    6 7  8   9  10 11
   conjure "++" (+++)
     [ pr ([] :: [Int])
     , prim ":" ((:) :: Int -> [Int] -> [Int])
-    , prim "head" (head :: [Int] -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     ]
 
   -- now through fold
@@ -93,20 +78,13 @@
     , prim "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])
     ]
 
-  -- now through fold
-  -- xs ++ ys  =  foldr (:) ys xs
   conjure "++" (+++)
     [ pr ([] :: [Int])
     , prim ":" ((:) :: Int -> [Int] -> [Int])
     , prim "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
     ]
 
-  -- intercalate
-  -- xs \/ ys  =  if null xs then ys else head xs : (ys \/ tail xs)
   conjure "\\/" (\/)
     [ pr ([] :: [Int])
     , prim ":" ((:) :: Int -> [Int] -> [Int])
-    , prim "head" (head :: [Int] -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     ]
diff --git a/eg/list.out b/eg/list.out
--- a/eg/list.out
+++ b/eg/list.out
@@ -4,32 +4,32 @@
 -- looking through 2 candidates of size 1
 -- looking through 4 candidates of size 2
 -- looking through 3 candidates of size 3
--- looking through 13 candidates of size 4
+-- looking through 11 candidates of size 4
 -- looking through 10 candidates of size 5
 length []  =  0
 length (x:xs)  =  length xs + 1
 
 reverse :: [Int] -> [Int]
 -- testing 360 combinations of argument values
--- pruning with 12/13 rules
+-- pruning with 3/3 rules
 -- looking through 2 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 11 candidates of size 3
--- looking through 24 candidates of size 4
--- looking through 60 candidates of size 5
--- looking through 152 candidates of size 6
+-- looking through 1 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 7 candidates of size 6
 reverse []  =  []
 reverse (x:xs)  =  reverse xs ++ unit x
 
 (++) :: [Int] -> [Int] -> [Int]
 -- testing 360 combinations of argument values
--- pruning with 4/4 rules
+-- pruning with 0/0 rules
 -- looking through 3 candidates of size 1
--- looking through 11 candidates of size 2
--- looking through 38 candidates of size 3
--- looking through 136 candidates of size 4
--- looking through 517 candidates of size 5
--- looking through 1606 candidates of size 6
+-- looking through 8 candidates of size 2
+-- looking through 11 candidates of size 3
+-- looking through 44 candidates of size 4
+-- looking through 116 candidates of size 5
+-- looking through 80 candidates of size 6
 [] ++ xs  =  xs
 (x:xs) ++ ys  =  x:(xs ++ ys)
 
@@ -67,13 +67,13 @@
 
 (\/) :: [Int] -> [Int] -> [Int]
 -- testing 360 combinations of argument values
--- pruning with 4/4 rules
+-- pruning with 0/0 rules
 -- looking through 3 candidates of size 1
--- looking through 11 candidates of size 2
--- looking through 38 candidates of size 3
--- looking through 136 candidates of size 4
--- looking through 517 candidates of size 5
--- looking through 1606 candidates of size 6
+-- looking through 8 candidates of size 2
+-- looking through 11 candidates of size 3
+-- looking through 44 candidates of size 4
+-- looking through 116 candidates of size 5
+-- looking through 80 candidates of size 6
 [] \/ xs  =  xs
 (x:xs) \/ ys  =  x:ys \/ xs
 
diff --git a/eg/spec.hs b/eg/spec.hs
--- a/eg/spec.hs
+++ b/eg/spec.hs
@@ -2,16 +2,36 @@
 --
 -- Adapted from Colin Runciman's example "ListFuns"
 import Conjure
+import Test.LeanCheck (holds, exists)
 import Prelude hiding (sum)
 
 
-sumSpec :: Spec1 [Int] Int
-sumSpec  =
-  [ []      -= 0
-  , [1,2]   -= 3
-  , [3,4,5] -= 12
+squareSpec :: (Int -> Int) -> Bool
+squareSpec square  =  square 0 == 0
+                   && square 1 == 1
+                   && square 2 == 4
+
+squarePrimitives :: [Prim]
+squarePrimitives  =
+  [ pr (0::Int)
+  , pr (1::Int)
+  , prim "+" ((+) :: Int -> Int -> Int)
+  , prim "*" ((*) :: Int -> Int -> Int)
   ]
 
+squarePropertySpec :: (Int -> Int) -> Bool
+squarePropertySpec square  =  and
+  [ holds n $ \x -> square x >= x
+  , holds n $ \x -> square x >= 0
+  , exists n $ \x -> square x > x
+  ]  where  n = 60
+
+
+sumSpec :: ([Int] -> Int) -> Bool
+sumSpec sum  =  sum []      == 0
+             && sum [1,2]   == 3
+             && sum [3,4,5] == 12
+
 -- hoping for something like
 -- sum xs  =  if null xs then 0 else head xs + sum (tail xs)
 
@@ -25,12 +45,10 @@
   ]
 
 
-appSpec :: Spec2 [Int] [Int] [Int]
-appSpec  =
-  [ (,) []      [0,1]   -= [0,1]
-  , (,) [2,3]   []      -= [2,3]
-  , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
-  ]
+appSpec :: ([Int] -> [Int] -> [Int]) -> Bool
+appSpec (++)  =  []      ++ [0,1]   == [0,1]
+              && [2,3]   ++ []      == [2,3]
+              && [4,5,6] ++ [7,8,9] == [4,5,6,7,8,9]
 
 -- hoping for something like
 -- app xs ys = if null xs then ys else head xs : app (tail xs) ys
@@ -46,5 +64,7 @@
 
 main :: IO ()
 main = do
-  conjure1 "sum" sumSpec sumPrimitives
-  conjure2 "++"  appSpec appPrimitives
+  conjureFromSpec "square" squareSpec squarePrimitives
+  conjureFromSpec "square" squarePropertySpec squarePrimitives
+  conjureFromSpec "sum" sumSpec sumPrimitives
+  conjureFromSpec "++"  appSpec appPrimitives
diff --git a/eg/spec.out b/eg/spec.out
--- a/eg/spec.out
+++ b/eg/spec.out
@@ -1,5 +1,18 @@
+square :: Int -> Int
+-- 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
+square x  =  x * x
+
+square :: Int -> Int
+-- 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
+square x  =  x * x
+
 sum :: [Int] -> Int
--- testing 3 combinations of argument values
 -- pruning with 4/8 rules
 -- looking through 1 candidates of size 1
 -- looking through 2 candidates of size 2
@@ -10,7 +23,6 @@
 sum (x:xs)  =  x + sum xs
 
 (++) :: [Int] -> [Int] -> [Int]
--- testing 3 combinations of argument values
 -- pruning with 3/3 rules
 -- looking through 2 candidates of size 1
 -- looking through 4 candidates of size 2
diff --git a/eg/tree.hs b/eg/tree.hs
--- a/eg/tree.hs
+++ b/eg/tree.hs
@@ -14,7 +14,7 @@
 
 -- TODO: remove the following import
 -- and fix build on GHC 7.10 and 7.8
--- the generation fo -: and ->>>: somehow fails.
+-- the generation of -: and ->>>: somehow fails.
 import Test.LeanCheck.Utils
 
 data Tree  =  Leaf
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -8,406 +8,411 @@
   mk/toplibs
 bench/candidates.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/candidates.hs
 bench/gps2: \
   bench/gps2.hs \
   mk/toplibs
 bench/gps2.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/gps2.hs
 bench/gps: \
   bench/gps.hs \
   mk/toplibs
 bench/gps.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/gps.hs
 bench/ill-hit: \
   bench/ill-hit.hs \
   mk/toplibs
 bench/ill-hit.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/ill-hit.hs
 bench/longshot: \
   bench/longshot.hs \
   mk/toplibs
 bench/longshot.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/longshot.hs
 bench/lowtests: \
   bench/lowtests.hs \
   mk/toplibs
 bench/lowtests.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/lowtests.hs
 bench/p12: \
   bench/p12.hs \
   mk/toplibs
 bench/p12.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/p12.hs
 bench/p30: \
   bench/p30.hs \
   mk/toplibs
 bench/p30.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/p30.hs
 bench/self: \
   bench/self.hs \
   mk/toplibs
 bench/self.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/self.hs
 bench/take-drop: \
   bench/take-drop.hs \
   mk/toplibs
 bench/take-drop.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/take-drop.hs
 bench/terpret: \
   bench/terpret.hs \
   mk/toplibs
 bench/terpret.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   bench/terpret.hs
 eg/arith: \
   eg/arith.hs \
   mk/toplibs
 eg/arith.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/arith.hs
 eg/bools: \
   eg/bools.hs \
   mk/toplibs
 eg/bools.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/bools.hs
 eg/count: \
   eg/count.hs \
   mk/toplibs
 eg/count.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/count.hs
 eg/dupos: \
   eg/dupos.hs \
   mk/toplibs
 eg/dupos.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/dupos.hs
 eg/factorial: \
   eg/factorial.hs \
   mk/toplibs
 eg/factorial.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/factorial.hs
 eg/fib01: \
   eg/fib01.hs \
   mk/toplibs
 eg/fib01.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/fib01.hs
 eg/fibonacci: \
   eg/fibonacci.hs \
   mk/toplibs
 eg/fibonacci.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/fibonacci.hs
 eg/gcd: \
   eg/gcd.hs \
   mk/toplibs
 eg/gcd.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/gcd.hs
 eg/ints: \
   eg/ints.hs \
   mk/toplibs
 eg/ints.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/ints.hs
 eg/list: \
   eg/list.hs \
   mk/toplibs
 eg/list.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/list.hs
 eg/pow: \
   eg/pow.hs \
   mk/toplibs
 eg/pow.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/pow.hs
 eg/replicate: \
   eg/replicate.hs \
   mk/toplibs
 eg/replicate.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/replicate.hs
 eg/setelem: \
   eg/setelem.hs \
   mk/toplibs
 eg/setelem.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/setelem.hs
 eg/sort: \
   eg/sort.hs \
   mk/toplibs
 eg/sort.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/sort.hs
 eg/spec: \
   eg/spec.hs \
   mk/toplibs
 eg/spec.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/spec.hs
 eg/subset: \
   eg/subset.hs \
   mk/toplibs
 eg/subset.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/subset.hs
 eg/tapps: \
   eg/tapps.hs \
   mk/toplibs
 eg/tapps.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/tapps.hs
 eg/tree: \
   eg/tree.hs \
   mk/toplibs
 eg/tree.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   eg/tree.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   mk/All.hs
 mk/Toplibs.o: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
-  test/Test/Candidates.hs \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
   mk/Toplibs.hs
 proto/u-conjure.o: \
   proto/u-conjure.hs
 proto/u-conjure: \
   proto/u-conjure.hs \
   mk/toplibs
+src/Conjure/Conjurable/Derive.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
 src/Conjure/Conjurable.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Expr.hs \
@@ -429,125 +434,120 @@
   src/Conjure/Expr.hs
 src/Conjure.o: \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
 src/Conjure/Prim.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Prim.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Defn.hs \
   src/Conjure/Conjurable.hs
-src/Conjure/Spec.o: \
-  src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
-  src/Conjure/Prim.hs \
-  src/Conjure/Expr.hs \
-  src/Conjure/Engine.hs \
-  src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
 src/Conjure/Utils.o: \
   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 \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
 test/conjurable: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
-  test/Test/Candidates.hs \
   test/conjurable.hs \
   mk/toplibs
 test/defn.o: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
-  test/Test/Candidates.hs \
   test/defn.hs \
   src/Conjure/Utils.hs \
-  src/Conjure/Spec.hs \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
 test/defn: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
-  test/Test/Candidates.hs \
   test/defn.hs \
   mk/toplibs
+test/derive.o: \
+  test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/derive.hs \
+  src/Conjure/Utils.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
+test/derive: \
+  test/Test.hs \
+  test/Test/ListableExpr.hs \
+  test/derive.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 \
   src/Conjure/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.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/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.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/Prim.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs
 test/utils: \
   test/utils.hs \
   test/Test.hs \
   test/Test/ListableExpr.hs \
-  test/Test/Candidates.hs \
   mk/toplibs
diff --git a/mk/haskell.mk b/mk/haskell.mk
--- a/mk/haskell.mk
+++ b/mk/haskell.mk
@@ -52,6 +52,7 @@
 PKGNAME = $(shell cat *.cabal | grep "^name:"    | sed -e "s/name: *//")
 
 HADDOCK_HAS = haddock --help | grep -q --
+HADDOCK_FILTER ?= cat
 
 
 # Implicit rules
@@ -111,7 +112,8 @@
 	  $(shell $(HADDOCK_HAS) --package-name          && echo "--package-name=$(PKGNAME)" ) \
 	  $(shell $(HADDOCK_HAS) --hyperlinked-source    && echo "--hyperlinked-source"      ) \
 	  $(shell $(HADDOCK_HAS) --no-print-missing-docs && echo --no-print-missing-docs     ) \
-	  $(HADDOCKFLAGS)
+	  $(HADDOCKFLAGS) | \
+	$(HADDOCK_FILTER)
 
 clean-cabal:
 	rm -rf dist/ dist-newstyle/ cabal.project.local cabal.project.local~
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -27,7 +27,7 @@
 -- >   , pr (1::Int)
 -- >   , prim "+" ((+) :: Int -> Int -> Int)
 -- >   , prim "*" ((*) :: Int -> Int -> Int)
--- > ]
+-- >   ]
 --
 -- Step 3: call conjure and see your generated function:
 --
@@ -59,16 +59,8 @@
   , value
 
 -- * Conjuring from a specification
-  , Spec1
-  , Spec2
-  , Spec3
-  , (-=)
-  , conjure1
-  , conjure2
-  , conjure3
-  , conjure1With
-  , conjure2With
-  , conjure3With
+  , conjureFromSpec
+  , conjureFromSpecWith
 
 -- * When using custom types
   , Conjurable (conjureExpress, conjureEquality, conjureTiers, conjureCases, conjureSubTypes)
@@ -78,6 +70,9 @@
   , conjureType
   , Name (..)
   , Express (..)
+  , deriveConjurable
+  , deriveConjurableIfNeeded
+  , deriveConjurableCascading
 
 -- * Pure interfaces
   , conjpure
@@ -89,6 +84,6 @@
 where
 
 import Conjure.Engine
-import Conjure.Spec
 import Conjure.Conjurable
 import Conjure.Prim
+import Conjure.Conjurable.Derive
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -4,7 +4,7 @@
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
--- This module is part of 'Conjure'.
+-- This module is part of "Conjure".
 --
 -- This defines the 'Conjurable' typeclass
 -- and utilities involving it.
@@ -58,7 +58,14 @@
 
 -- | Single reification of some functions over a type as 'Expr's.
 --
--- A hole, an equality function and tiers.
+-- This is a sixtuple, in order:
+--
+-- 1. a hole encoded as an 'Expr';
+-- 2. the '==' function encoded as an 'Expr' when available;
+-- 3. 'tiers' of enumerated test values encoded as 'Expr's when available;
+-- 4. infinite list of potential variable names;
+-- 5. boolean indicating whether the type is atomic;
+-- 6. the 'conjureSize' function encoded as an 'Expr'.
 type Reification1  =  (Expr, Maybe Expr, Maybe [[Expr]], [String], Bool, Expr)
 
 -- | A reification over a collection of types.
@@ -127,35 +134,55 @@
 
   -- | Returns 'Just' the '==' function encoded as an 'Expr' when available
   --   or 'Nothing' otherwise.
+  --
+  -- Use 'reifyEquality' when defining this.
   conjureEquality :: a -> Maybe Expr
   conjureEquality _  =  Nothing
 
   -- | Returns 'Just' 'tiers' of values encoded as 'Expr's when possible
   --   or 'Nothing' otherwise.
+  --
+  -- Use 'reifyTiers' when defining this.
   conjureTiers :: a -> Maybe [[Expr]]
   conjureTiers _  =  Nothing
 
   conjureSubTypes :: a -> Reification
   conjureSubTypes _  =  id
 
+  -- | Returns an if-function encoded as an 'Expr'.
   conjureIf :: a -> Expr
   conjureIf   =  ifFor
 
+  -- | Returns a top-level case breakdown.
   conjureCases :: a -> [Expr]
   conjureCases _  =  []
 
   conjureArgumentCases :: a -> [[Expr]]
   conjureArgumentCases _  =  []
 
+  -- | Returns the (recursive) size of the given value.
   conjureSize :: a -> Int
   conjureSize _  =  0
 
+  -- | Returns a function that deeply reencodes an expression when possible.
+  --   ('id' when not available.)
+  --
+  -- Use 'reifyExpress' when defining this.
   conjureExpress :: a -> Expr -> Expr
 
   conjureEvaluate :: (Expr->Expr) -> Int -> Defn -> Expr -> Maybe a
   conjureEvaluate  =  devaluate
 
 
+-- | To be used in the implementation of 'conjureSubTypes'.
+--
+-- > instance ... => Conjurable <Type> where
+-- >   ...
+-- >   conjureSubTypes x  =  conjureType (field1 x)
+-- >                      .  conjureType (field2 x)
+-- >                      .  ...
+-- >                      .  conjureType (fieldN x)
+-- >   ...
 conjureType :: Conjurable a => a -> Reification
 conjureType x ms  =
   if hole x `elem` [h | (h,_,_,_,_,_) <- ms]
@@ -168,16 +195,31 @@
 -- The use of nubOn above is O(n^2).
 -- So long as there is not a huge number of subtypes of a, so we're fine.
 
+-- | Conjures a 'Reification1' for a 'Conjurable' type.
+--
+-- This is used in the implementation of 'conjureReification'.
 conjureReification1 :: Conjurable a => a -> Reification1
 conjureReification1 x  =  (hole x, conjureEquality x, conjureTiers x, names x, null $ conjureCases x, value "conjureSize" (conjureSize -:> x))
 
+-- | Conjures a list of 'Reification1'
+--   for a 'Conjurable' type, its subtypes and 'Bool'.
+--
+-- This is used in the implementation of
+-- 'conjureHoles',
+-- 'conjureMkEquation',
+-- 'conjureAreEqual',
+-- 'conjureTiersFor',
+-- 'conjureIsDeconstructor',
+-- 'conjureNamesFor',
+-- 'conjureIsUnbreakable',
+-- etc.
 conjureReification :: Conjurable a => a -> [Reification1]
 conjureReification x  =  nubConjureType x [conjureReification1 bool]
   where
   bool :: Bool
   bool  =  error "conjureReification: evaluated proxy boolean value (definitely a bug)"
 
--- | Reifies equality to be used in a conjurable type.
+-- | Reifies equality '==' in a 'Conjurable' type instance.
 --
 -- This is to be used
 -- in the definition of 'conjureEquality'
@@ -203,6 +245,16 @@
 reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]]
 reifyTiers  =  Just . mkExprTiers
 
+-- | Reifies the 'expr' function in a 'Conjurable' type instance.
+--
+-- This is to be used
+-- in the definition of 'conjureExpress'
+-- of 'Conjurable' typeclass instances.
+--
+-- > instance ... => Conjurable <Type> where
+-- >   ...
+-- >   conjureExpress  =  reifyExpress
+-- >   ...
 reifyExpress :: (Express a, Show a) => a -> Expr -> Expr
 reifyExpress a e  =  case value "expr" (expr -:> a) $$ e of
   Nothing -> e         -- TODO: consider throwing an error
@@ -211,12 +263,20 @@
 mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]]
 mkExprTiers a  =  mapT val (tiers -: [[a]])
 
+-- | Computes a list of holes encoded as 'Expr's
+--   from a 'Conjurable' functional value.
+--
+-- (cf. 'Conjure.Prim.cjHoles')
 conjureHoles :: Conjurable f => f -> [Expr]
 conjureHoles f  =  [eh | (eh,_,Just _,_,_,_) <- conjureReification f]
 
+-- | 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]
 
+-- | Given a 'Conjurable' functional value,
+--   computes a function that checks whether two 'Expr's are equal
+--   up to a given number of tests.
 conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool
 conjureAreEqual f maxTests  =  (===)
   where
@@ -225,6 +285,8 @@
   isTrue  =  all (errorToFalse . eval False) . gs
   gs  =  take maxTests . grounds (conjureTiersFor f)
 
+-- | Compute 'tiers' of values encoded as 'Expr's
+--   of the type of the given 'Expr'.
 conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]]
 conjureTiersFor f e  =  tf allTiers
   where
@@ -235,6 +297,7 @@
                       ((e':_):_) | typ e' == typ e -> etiers
                       _                            -> tf etc
 
+-- | Compute variable names for the given 'Expr' type.
 conjureNamesFor :: Conjurable f => f -> Expr -> [String]
 conjureNamesFor f e  =  head
                      $  [ns | (eh, _, _, ns, _, _) <- conjureReification f, typ e == typ eh]
@@ -244,6 +307,9 @@
 conjureMostGeneralCanonicalVariation f  =  canonicalizeWith (conjureNamesFor f)
                                         .  fastMostGeneralVariation
 
+-- | Checks if an unary function encoded as an 'Expr' is a deconstructor.
+--
+-- (cf. 'conjureIsDeconstruction')
 conjureIsDeconstructor :: Conjurable f => f -> Int -> Expr -> Bool
 conjureIsDeconstructor f maxTests e  =  case as of
   [] -> False
@@ -259,8 +325,14 @@
     esz e  =  eval (0::Int) (sz :$ e)
     is e'  =  errorToFalse $ esz (e :$ e') < esz e'
 
--- the result does not increase the size for at least half the time
--- the result decreases in size for at least a third of the time
+-- | Checks if an expression is a deconstruction.
+--
+-- There should be a single 'hole' in the expression.
+--
+-- 1. The result does not increase the size for at least half the time.
+-- 2. The result decreases in size for at least a third of the time.
+--
+-- (cf. 'conjureIsDeconstructor')
 conjureIsDeconstruction :: Conjurable f => f -> Int -> Expr -> Bool
 conjureIsDeconstruction f maxTests ed  =  length (holes ed) == 1
                                        && typ h == typ ed
@@ -280,6 +352,11 @@
                $  e `match` ed
   err  =  error "conjureIsDeconstructor: the impossible happened"
 
+-- | Compute candidate deconstructions from an 'Expr'.
+--
+-- This is used in the implementation of
+-- 'Conjure.Engine.candidateDefnsC' and 'Conjure.Engine.candidateExprs'
+-- followed by 'conjureIsDeconstruction'.
 candidateDeconstructionsFrom :: Expr -> [Expr]
 candidateDeconstructionsFrom e  =
   [ e'
@@ -289,6 +366,7 @@
   , length (holes e') == 1
   ]
 
+-- | Checks if an 'Expr' is of an unbreakable type.
 conjureIsUnbreakable :: Conjurable f => f -> Expr -> Bool
 conjureIsUnbreakable f e  =  head
   [is | (h,_,_,_,is,_) <- conjureReification f, typ h == typ e]
@@ -326,6 +404,10 @@
 (==:) :: (a -> a -> Bool) -> a -> (a -> a -> Bool)
 (==:)  =  const
 
+-- the reconstruction of equality functions for polymorphic types
+-- such as [a], (a,b), Maybe a, Either a b
+-- is only needed so we don't impose an Eq restriction on the type context.
+
 instance (Conjurable a, Listable a, Express a, Show a) => Conjurable [a] where
   conjureExpress   =  reifyExpress
   conjureSubTypes xs  =  conjureType (head xs)
@@ -466,6 +548,10 @@
 resTy :: (a -> b) -> b
 resTy _  =  undefined
 
+-- | Evaluates a 'Defn' into a regular Haskell value
+--   returning 'Nothing' when there's a type mismatch.
+--
+-- The integer argument indicates the limit of recursive evaluations.
 cevaluate :: Conjurable f => Int -> Defn -> Maybe f
 cevaluate mx defn  =  mr
   where
@@ -473,27 +559,59 @@
   exprExpr  =  conjureExpress $ fromJust mr
   (ef':_)  =  unfoldApp . fst $ head defn
 
+-- | Evaluates a 'Defn' into a regular Haskell value
+--   returning the given default value when there's a type mismatch.
+--
+-- The integer argument indicates the limit of recursive evaluations.
 ceval :: Conjurable f => Int -> f -> Defn -> f
 ceval mx z  =  fromMaybe z . cevaluate mx
 
+-- | Evaluates a 'Defn' into a regular Haskell value
+--   raising an error there's a type mismatch.
+--
+-- The integer argument indicates the limit of recursive evaluations.
 cevl :: Conjurable f => Int -> Defn -> f
 cevl mx  =  ceval mx err
   where
   err  =  error "cevl: type mismatch"
 
+-- | Computes a complete application for the given function.
+--
+-- > > conjureApplication "not" not
+-- > not p :: Bool
+--
+-- > > conjureApplication "+" ((+) :: Int -> Int -> Int)
+-- > x + y :: Int
+--
+-- (cf. 'conjureVarApplication')
 conjureApplication :: Conjurable f => String -> f -> Expr
 conjureApplication  =  conjureWhatApplication value
 
+-- | Computes a complete application for a variable
+--   of the same type of the given function.
+--
+-- > > conjureVarApplication "not" not
+-- > not p :: Bool
+--
+-- > > conjureVarApplication "+" ((+) :: Int -> Int -> Int)
+-- > x + y :: Int
+--
+-- (cf. 'conjureApplication')
 conjureVarApplication :: Conjurable f => String -> f -> Expr
 conjureVarApplication  =  conjureWhatApplication var
 
+-- | Used in the implementation of 'conjureApplication' and 'conjureVarApplication'.
 conjureWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr
 conjureWhatApplication what nm f  =  mostGeneralCanonicalVariation . foldApp
                                   $  what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f)
   where
   (nf:nas)  =  words nm ++ repeat ""
 
-conjurePats :: Conjurable f => [Expr] -> String -> f -> [[[Expr]]]
+-- | Computes tiers of sets of patterns for the given function.
+--
+-- > > conjurePats [zero] "f" (undefined :: Int -> Int)
+-- > [[[f x :: Int]],[[f 0 :: Int,f x :: Int]]]
+conjurePats :: Conjurable f => [Expr] -> String -> f -> [[ [Expr] ]]
 conjurePats es nm f  =  mapT (map mkApp . prods) $ cs
   where
   mkApp  =  foldApp . (ef:)
diff --git a/src/Conjure/Conjurable/Derive.hs b/src/Conjure/Conjurable/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Conjurable/Derive.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE TemplateHaskell, CPP #-}
+-- |
+-- Module      : Conjure.Conjurable.Derive
+-- Copyright   : (c) 2019-2021 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- Allows automatic derivation of 'Conjurable' typeclass instances.
+module Conjure.Conjurable.Derive
+  ( deriveConjurable
+  , deriveConjurableCascading
+  , deriveConjurableIfNeeded
+  )
+where
+
+import Test.LeanCheck
+import Test.LeanCheck.Derive
+import Test.LeanCheck.Utils
+import Conjure.Expr hiding (mkName, Name, isInstanceOf)
+import Conjure.Conjurable hiding (Name)
+import Data.Express.Utils (primeCycle)
+import Data.Express.Utils.TH
+
+import Control.Monad
+import Data.Char
+import Data.List
+import Language.Haskell.TH.Lib
+
+#if __GLASGOW_HASKELL__ < 710
+import Data.Functor ((<$>))
+#endif
+
+-- | Derives an 'Conjurable' instance for the given type 'Name'.
+--
+-- This function needs the @TemplateHaskell@ extension.
+--
+-- If '-:', '->:', '->>:', '->>>:', ... are not in scope,
+-- this will derive them as well.
+--
+-- For now,
+-- this function only derives
+-- 'conjureEquality',
+-- 'conjureTiers' and
+-- 'conjureExpress'
+-- and does not derive
+-- 'conjureSubTypes',
+-- 'conjureArgumentCases' and
+-- 'conjureSize'.
+-- These will be added in future versions.
+-- If you plan to use features that depend on these functionalities,
+-- please define your instances manually.
+deriveConjurable :: Name -> DecsQ
+deriveConjurable  =  deriveWhenNeededOrWarn ''Conjurable reallyDerive
+  where
+  reallyDerive  =  reallyDeriveConjurableWithRequisites
+
+-- | Same as 'deriveConjurable' but does not warn when instance already exists
+--   ('deriveConjurable' is preferable).
+--
+-- For now,
+-- this function only derives
+-- 'conjureEquality',
+-- 'conjureTiers' and
+-- 'conjureExpress'
+-- and does not derive
+-- 'conjureSubTypes',
+-- 'conjureArgumentCases' and
+-- 'conjureSize'.
+-- These will be added in future versions.
+-- If you plan to use features that depend on these functionalities,
+-- please define your instances manually.
+deriveConjurableIfNeeded :: Name -> DecsQ
+deriveConjurableIfNeeded  =  deriveWhenNeeded ''Conjurable reallyDerive
+  where
+  reallyDerive  =  reallyDeriveConjurableWithRequisites
+
+-- | Derives a 'Conjurable' instance for a given type 'Name'
+--   cascading derivation of type arguments as well.
+--
+-- For now,
+-- this function only derives
+-- 'conjureEquality',
+-- 'conjureTiers' and
+-- 'conjureExpress'
+-- and does not derive
+-- 'conjureSubTypes',
+-- 'conjureArgumentCases' and
+-- 'conjureSize'.
+-- These will be added in future versions.
+-- If you plan to use features that depend on these functionalities,
+-- please define your instances manually.
+deriveConjurableCascading :: Name -> DecsQ
+deriveConjurableCascading  =  deriveWhenNeeded ''Conjurable reallyDerive
+  where
+  reallyDerive t  =  concat
+                 <$> sequence [ deriveListableCascading t
+                              , deriveNameCascading t
+                              , deriveExpressCascading t
+                              , reallyDeriveConjurableCascading t ]
+
+reallyDeriveConjurableWithRequisites :: Name -> DecsQ
+reallyDeriveConjurableWithRequisites t  =  concat <$>
+  sequence [ deriveListableIfNeeded t
+           , deriveNameIfNeeded t
+           , deriveExpressIfNeeded t
+           , reallyDeriveConjurable t ]
+
+reallyDeriveConjurable :: Name -> DecsQ
+reallyDeriveConjurable t  =  do
+  isEq <- t `isInstanceOf` ''Eq
+  isOrd <- t `isInstanceOf` ''Ord
+  (nt,vs) <- normalizeType t
+#if __GLASGOW_HASKELL__ >= 710
+  cxt <- sequence [ [t| $(conT c) $(return v) |]
+#else
+  -- template-haskell <= 2.9.0.0:
+  cxt <- sequence [ classP c [return v]
+#endif
+                  | c <- [''Conjurable, ''Listable, ''Express] ++ [''Eq | isEq] ++ [''Ord | isOrd]
+                  , v <- vs]
+  cs <- typeConstructorsArgNames t
+  asName <- newName "x"
+  let withTheReturnTypeOfs = deriveWithTheReturnTypeOfs $ [length ns | (_,ns) <- cs]
+  let inst = [d| instance Conjurable $(return nt) where
+                   conjureExpress   =  reifyExpress
+                   conjureEquality  =  reifyEquality
+                   conjureTiers     =  reifyTiers |]
+  -- withTheReturnTypeOfs |++| (cxt |=>| inst)
+  cxt |=>| inst
+-- TODO: derive conjureCases
+-- TODO: derive conjureSize
+-- TODO: derive conjureSubTypes (cf. Extrapolate.subInstances)
+
+-- Not only really derive Conjurable instances,
+-- but cascade through argument types.
+reallyDeriveConjurableCascading :: Name -> DecsQ
+reallyDeriveConjurableCascading  =  reallyDeriveCascading ''Conjurable reallyDeriveConjurable
+
+deriveWithTheReturnTypeOfs :: [Int] -> DecsQ
+deriveWithTheReturnTypeOfs  =
+  fmap concat . mapM deriveWithTheReturnTypeOf . nubSort
+
+deriveWithTheReturnTypeOf :: Int -> DecsQ
+deriveWithTheReturnTypeOf n  =  do
+  mf <- lookupValueName name
+  case mf of
+    Nothing -> reallyDeriveWithTheReturnTypeOf n
+    Just _  -> return []
+  where
+  name  =  "-" ++ replicate n '>' ++ ":"
+
+reallyDeriveWithTheReturnTypeOf :: Int -> DecsQ
+reallyDeriveWithTheReturnTypeOf n  =  do
+  td <- sigD name theT
+  vd <- [d| $(varP name) = const |]
+  return $ td:vd
+  where
+  theT  =  bind [t| $(theFunT) -> $(last vars) -> $(theFunT) |]
+  theFunT  =  foldr1 funT vars
+  funT t1 t2  =  [t| $(t1) -> $(t2) |]
+  vars  =  map (varT . mkName) . take (n+1) . primeCycle $ map (:"") ['a'..'z']
+  name  =  mkName $ "-" ++ replicate n '>' ++ ":"
+#if __GLASGOW_HASKELL__ >= 800
+  bind  =  id -- unbound variables are automatically bound
+#else
+  bind  =  toBoundedQ
+#endif
diff --git a/src/Conjure/Defn.hs b/src/Conjure/Defn.hs
--- a/src/Conjure/Defn.hs
+++ b/src/Conjure/Defn.hs
@@ -4,7 +4,7 @@
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
--- This module is part of 'Conjure'.
+-- This module is part of "Conjure".
 --
 -- This module exports the 'Defn' type synonym and utilities involving it.
 --
@@ -33,9 +33,30 @@
 import Control.Applicative ((<$>)) -- for older GHCs
 import Test.LeanCheck.Utils ((-:>)) -- for toDynamicWithDefn
 
+-- | A function definition as a list of top-level case bindings ('Bndn').
+--
+-- Here is an example using the notation from "Data.Express.Fixtures":
+--
+-- > sumV :: Expr
+-- > sumV  =  var "sum" (undefined :: [Int] -> Int)
+-- >
+-- > (=-) = (,)
+-- > infixr 0 =-
+-- >
+-- > sumDefn :: Defn
+-- > sumDefn  =  [ sum' nil           =-  zero
+-- >             , sum' (xx -:- xxs)  =-  xx -+- (sumV :$ xxs)
+-- >             ]  where  sum' e  =  sumV :$ e
 type Defn  =  [Bndn]
+
+-- | A single binding in a definition ('Defn').
 type Bndn  =  (Expr,Expr)
 
+-- | Pretty-prints a 'Defn' as a 'String':
+--
+-- > > putStr $ showDefn sumDefn
+-- > sum []  =  0
+-- > sum (x:xs)  =  x + sum xs
 showDefn :: Defn -> String
 showDefn  =  unlines . map show1
   where
@@ -43,8 +64,37 @@
 
 type Memo  =  [(Expr, Maybe Dynamic)]
 
--- | Evaluates an 'Expr' using the given 'Defn' as definition
+-- | Evaluates an 'Expr' to a 'Dynamic' value
+--   using the given 'Defn' as definition
 --   when a recursive call is found.
+--
+-- Arguments:
+--
+-- 1. a function that deeply reencodes an expression (cf. 'expr')
+-- 2. the maximum number of recursive evaluations
+-- 3. a 'Defn' to be used when evaluating the given 'Expr'
+-- 4. an 'Expr' to be evaluated
+--
+-- This function cannot be used to evaluate a functional value for the given 'Defn'
+-- and can only be used when occurrences of the given 'Defn' are fully applied.
+--
+-- The function the deeply reencodes an 'Expr' can be defined using
+-- functionality present in "Conjure.Conjurable".  Here's a quick-and-dirty version
+-- that is able to reencode 'Bool's, 'Int's and their lists:
+--
+-- > exprExpr :: Expr -> Expr
+-- > exprExpr  =  conjureExpress (undefined :: Bool -> [Bool] -> Int -> [Int] -> ())
+--
+-- The maximum number of recursive evaluations counts in two ways:
+--
+-- 1. the maximum number of entries in the recursive-evaluation memo table;
+-- 2. the maximum number of terminal values considered (but in this case the
+--    limit is multiplied by the _size_ of the given 'Defn'.
+--
+-- These could be divided into two separate parameters but
+-- then there would be an extra _dial_ to care about...
+--
+-- (cf. 'devaluate', 'deval', 'devl')
 toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
 toDynamicWithDefn exprExpr mx cx  =  fmap (\(_,_,d) -> d) . re (mx * sum (map (size . snd) cx)) []
   where
@@ -98,18 +148,49 @@
                           Just (n', m', d2) -> (n',m',) <$> dynApply d1 d2
   _ $$ _               =  Nothing
 
+-- | Evaluates an 'Expr' expression into 'Just' a regular Haskell value
+--   using a 'Defn' definition when it is found.
+--   If there's a type-mismatch, this function returns 'Nothing'.
+--
+-- This function requires a 'Expr'-deep-reencoding function
+-- and a limit to the number of recursive evaluations.
+--
+-- (cf. 'toDynamicWithDefn', 'deval', 'devl')
 devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
 devaluate ee n fxpr e  =  toDynamicWithDefn ee n fxpr e >>= fromDynamic
 
+-- | Evaluates an 'Expr' expression into a regular Haskell value
+--   using a 'Defn' definition when it is found in the given expression.
+--   If there's a type-mismatch, this function return a default value.
+--
+-- This function requires a 'Expr'-deep-reencoding function
+-- and a limit to the number of recursive evaluations.
+--
+-- (cf. 'toDynamicWithDefn', 'devaluate', devl')
 deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
 deval ee n fxpr x  =  fromMaybe x . devaluate ee n fxpr
 
+-- | Like 'deval' but only works for when the given 'Defn' definition
+--   has no case breakdowns.
+--
+-- In other words, this only works when the given 'Defn' is a singleton list
+-- whose first value of the only element is a simple application without
+-- constructors.
 devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
 devalFast _ n [defn] x  =  reval defn n x
 
+-- | Evaluates an 'Expr' expression into a regular Haskell value
+--   using a 'Defn' definition when it is found in the given expression.
+--   If there's a type-mismatch, this raises an error.
+--
+-- This function requires a 'Expr'-deep-reencoding function
+-- and a limit to the number of recursive evaluations.
+--
+-- (cf. 'toDynamicWithDefn', 'devaluate', deval')
 devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a
 devl ee n fxpr  =  deval ee n fxpr (error "devl: incorrect type?")
 
+-- | Returns whether the given definition 'apparentlyTerminates'.
 defnApparentlyTerminates :: Defn -> Bool
 defnApparentlyTerminates [(efxs, e)]  =  apparentlyTerminates efxs e
 defnApparentlyTerminates _  =  True
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -4,7 +4,7 @@
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
--- An internal module of 'Conjure',
+-- An internal module of "Conjure",
 -- a library for Conjuring function implementations
 -- from tests or partial definitions.
 -- (a.k.a.: functional inductive programming)
@@ -15,15 +15,22 @@
   , Args(..)
   , args
   , conjureWith
+  , conjureFromSpec
+  , conjureFromSpecWith
+  , conjure0
+  , conjure0With
   , conjpure
   , conjpureWith
+  , conjpureFromSpec
+  , conjpureFromSpecWith
+  , conjpure0
+  , conjpure0With
   , candidateExprs
   , candidateDefns
   , candidateDefns1
   , candidateDefnsC
   , conjureTheory
   , conjureTheoryWith
-  , deconstructions
   , module Data.Express
   , module Data.Express.Fixtures
   , module Test.Speculate.Engine
@@ -69,12 +76,13 @@
 -- >   , pr (1::Int)
 -- >   , prim "+" ((+) :: Int -> Int -> Int)
 -- >   , prim "*" ((*) :: Int -> Int -> Int)
--- > ]
+-- >   ]
 --
 -- The conjure function does the following:
 --
 -- > > conjure "square" square primitives
 -- > square :: Int -> Int
+-- > -- pruning with 14/25 rules
 -- > -- testing 3 combinations of argument values
 -- > -- looking through 3 candidates of size 1
 -- > -- looking through 3 candidates of size 2
@@ -86,6 +94,51 @@
 conjure  =  conjureWith args
 
 
+-- | Conjures an implementation from a function specification.
+--
+-- This function works like 'conjure' but instead of receiving a partial definition
+-- it receives a boolean filter / property about the function.
+--
+-- For example, given:
+--
+-- > squareSpec :: (Int -> Int) -> Bool
+-- > squareSpec square  =  square 0 == 0
+-- >                    && square 1 == 1
+-- >                    && square 2 == 4
+--
+-- Then:
+--
+-- > > conjureFromSpec "square" squareSpec primitives
+-- > square :: Int -> Int
+-- > -- 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
+-- > square x  =  x * x
+--
+-- This allows users to specify QuickCheck-style properties,
+-- here is an example using LeanCheck:
+--
+-- > import Test.LeanCheck (holds, exists)
+-- >
+-- > squarePropertySpec :: (Int -> Int) -> Bool
+-- > squarePropertySpec square  =  and
+-- >   [ holds n $ \x -> square x >= x
+-- >   , holds n $ \x -> square x >= 0
+-- >   , exists n $ \x -> square x > x
+-- >   ]  where  n = 60
+conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO ()
+conjureFromSpec  =  conjureFromSpecWith args
+
+
+-- | Synthesizes an implementation from both a partial definition and a
+--   function specification.
+--
+--   This works like the functions 'conjure' and 'conjureFromSpec' combined.
+conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO ()
+conjure0  =  conjure0With args
+
+
 -- | Like 'conjure' but allows setting the maximum size of considered expressions
 --   instead of the default value of 12.
 --
@@ -109,7 +162,6 @@
   , 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
-  , forceTests            :: [[Expr]]  -- ^ force tests
   }
 
 
@@ -134,7 +186,6 @@
   , requireDescent         =  True
   , usePatterns            =  True
   , showTheory             =  False
-  , forceTests             =  []
   }
 
 
@@ -142,9 +193,20 @@
 --
 -- > conjureWith args{maxSize = 11} "function" function [...]
 conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
-conjureWith args nm f es  =  do
+conjureWith args nm f  =  conjure0With args nm f (const True)
+
+-- | Like 'conjureFromSpec' but allows setting options through 'Args'/'args'.
+--
+-- > conjureFromSpecWith args{maxSize = 11} "function" spec [...]
+conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO ()
+conjureFromSpecWith args nm p  =  conjure0With args nm undefined p
+
+-- | Like 'conjure0' but allows setting options through 'Args'/'args'.
+conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
+conjure0With args nm f p es  =  do
   print (var (head $ words nm) f)
-  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
+  when (length ts > 0) $
+    putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
   putStrLn $ "-- pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"
   when (showTheory args) $ do
     putStrLn $ "{-"
@@ -166,31 +228,52 @@
       []     ->  pr (n+1) rs
       (i:_)  ->  putStrLn $ showDefn i
   rs  =  zip iss css
-  (iss, css, ts, thy)  =  conjpureWith args nm f es
+  (iss, css, ts, thy)  =  conjpure0With args nm f p es
   nRules  =  length (rules thy)
   nREs  =  length (equations thy) + nRules
 
 
 -- | Like 'conjure' but in the pure world.
 --
--- Returns a triple with:
+-- Returns a quadruple with:
 --
 -- 1. tiers of implementations
--- 2. tiers of candidate bodies (right type)
--- 3. tiers of candidate expressions (any type)
--- 4. a list of tests
+-- 2. tiers of candidates
+-- 3. a list of tests
+-- 4. the underlying theory
 conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
 conjpure =  conjpureWith args
 
+-- | Like 'conjureFromSpec' but in the pure world.  (cf. 'conjpure')
+conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpureFromSpec  =  conjpureFromSpecWith args
 
+-- | Like 'conjure0' but in the pure world.  (cf. 'conjpure')
+conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpure0 =  conjpure0With args
+
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
 conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
-conjpureWith args@(Args{..}) nm f es  =  (implementationsT, candidatesT, tests, thy)
+conjpureWith args nm f  =  conjpure0With args nm f (const True)
+
+-- | Like 'conjureFromSpecWith' but in the pure world.  (cf. 'conjpure')
+conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpureFromSpecWith args nm p  =  conjpure0With args nm undefined p
+
+-- | Like 'conjpure0' but allows setting options through 'Args' and 'args'.
+--
+-- This is where the actual implementation resides.  The functions
+-- 'conjpure', 'conjpureWith', 'conjpureFromSpec', 'conjpureFromSpecWith',
+-- 'conjure', 'conjureWith', 'conjureFromSpec', 'conjureFromSpecWith' and
+-- 'conjure0' all refer to this.
+conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpure0With args@(Args{..}) nm f p es  =  (implementationsT, candidatesT, tests, thy)
   where
   tests  =  [ffxx //- bs | bs <- dbss]
   implementationsT  =  filterT implements candidatesT
   implements fx  =  defnApparentlyTerminates fx
                  && requal fx ffxx vffxx
+                 && errorToFalse (p (cevl maxEvalRecursions fx))
   candidatesT  =  take maxSize candidatesTT
   (candidatesTT, thy)  =  candidateDefns args nm f es
   ffxx   =  conjureApplication nm f
@@ -205,18 +288,18 @@
 
   bss, dbss :: [[(Expr,Expr)]]
   bss  =  take maxSearchTests $ groundBinds (conjureTiersFor f) ffxx
-  fbss  =  [zip xxs vs | vs <- forceTests, isWellTyped $ foldApp (rrff:vs)]
-  dbss  =  take maxTests
-        $  ([bs | bs <- bss, errorToFalse . eval False $ e //- bs] \\ fbss)
-        ++ fbss
+  dbss  =  take maxTests [bs | bs <- bss, errorToFalse . eval False $ e //- bs]
     where
     e  =  ffxx -==- ffxx
 
 
+-- | Just prints the underlying theory found by "Test.Speculate"
+--   without actually synthesizing a function.
 conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO ()
 conjureTheory  =  conjureTheoryWith args
 
 
+-- | Like 'conjureTheory' but allows setting options through 'Args'/'args'.
 conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
 conjureTheoryWith args nm f es  =  do
   putStrLn $ "theory with " ++ (show . length $ rules thy) ++ " rules and "
@@ -442,28 +525,6 @@
   isNotConstruction (p,e) | isVar p    =  e == p || e `isDecOf` p
                           | otherwise  =  size e <= size p -- TODO: allow filter and id somehow
 -- TODO: improve this function with better isNotConstruction
-
-
-candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
-candidatesTD keep h primitives  =  filterT (not . hasHole)
-                                $  town [[h]]
-  where
-  most = mostGeneralCanonicalVariation
-
-  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
 
 
 -- hardcoded filtering rules
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
--- a/src/Conjure/Expr.hs
+++ b/src/Conjure/Expr.hs
@@ -17,21 +17,14 @@
   , recursexpr
   , apparentlyTerminates
   , mayNotEvaluateArgument
-  , applicationOld
   , compareSimplicity
   , ifFor
-  , primitiveHoles
-  , primitiveApplications
   , valuesBFS
   , holesBFS
   , fillBFS
-  , showEq
-  , lhs
-  , rhs
   , ($$**)
   , ($$|<)
   , possibleHoles
-  , isDeconstructionE
   , revaluate
   , reval
   , useMatches
@@ -179,15 +172,6 @@
 mayNotEvaluateArgument (Value "||" ce :$ _)       =  True
 mayNotEvaluateArgument _                          =  False
 
-applicationOld :: Expr -> [Expr] -> Maybe Expr
-applicationOld ff es  =  appn ff
-  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
-
 -- | Creates an if 'Expr' of the type of the given proxy.
 --
 -- > > ifFor (undefined :: Int)
@@ -206,23 +190,9 @@
 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
+-- | Lists terminal values in BFS order.
+--
+-- (cf. 'values', 'holesBFS', 'fillBFS')
 valuesBFS :: Expr -> [Expr]
 valuesBFS  =  concat . bfs
   where
@@ -230,10 +200,15 @@
   bfs (ef :$ ex)  =  [] : mzip (bfs ef) (bfs ex)
   bfs e  =  [[e]]
 
--- lists holes in BFS order
+-- | Lists holes in BFS order.
+--
+-- (cf. 'holes', 'valuesBFS', 'fillBFS')
 holesBFS :: Expr -> [Expr]
 holesBFS  =  filter isHole . valuesBFS
 
+-- | Fills holes in BFS order.
+--
+-- (cf. 'fill', 'valuesBFS', 'fillBFS')
 fillBFS :: Expr -> Expr -> Expr
 fillBFS e e'  =  fst (f e)
   where
@@ -251,19 +226,38 @@
       | 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
+-- | Like '$$' but always works regardless of type.
+--
+-- /Warning:/ just like ':$', this may produce ill-typed expressions.
+--
+-- > > zero $$** zero
+-- > Just (0 0 :: ill-typed # Int $ Int #)
+--
+-- Together with '$$|<', this function is unused
+-- but is useful when experiment with the source
+-- to see the effect of type-corrected
+-- on pruning the search space.
+--
+-- (cf. '$$', '$$|<')
 ($$**) :: Expr -> Expr -> Maybe Expr
 e1 $$** e2  =  Just $ e1 :$ e2
 
--- Debug: application that works for the correct kinds
+-- | Like '$$' but relaxed to work on correct kinds.
+--
+-- > > ordE $$|< zero
+-- > Just (ord 0 :: ill-typed # Char -> Int $ Int #)
+--
+-- > > zero $$|< zero
+-- > Nothing
+--
+-- /Warning:/ just like ':$', this may produce ill-typed expressions.
+--
+-- Together with '$$**', this function is unused
+-- but is useful when experiment with the source
+-- to see the effect of type-corrected
+-- on pruning the search space.
+--
+-- (cf. '$$', '$$**')
 ($$|<) :: Expr -> Expr -> Maybe Expr
 e1 $$|< e2  =  if isFunTy t1 && tyArity (argumentTy t1) == tyArity t2
                then Just $ e1 :$ e2
@@ -276,17 +270,36 @@
   ktyp (e1 :$ e2)  =  resultTy (ktyp e1)
   ktyp e  =  typ e
 
+
+-- | Lists all distinct holes that are possible with the given 'Expr's.
+--
+-- > > possibleHoles [zero, one, plus]
+-- > [_ :: Int,_ :: Int -> Int,_ :: Int -> Int -> Int]
+--
+-- > > possibleHoles [ae, ordE]
+-- > [_ :: Char,_ :: Int,_ :: Char -> Int]
 possibleHoles :: [Expr] -> [Expr]
 possibleHoles  =  nubSort . ph . nubSort . map holeAsTypeOf
   where
   ph hs  =  case nubSort $ hs ++ [holeAsTypeOf hfx | hf <- hs, hx <- hs, Just hfx <- [hf $$ hx]] of
             hs' | hs' == hs -> hs
                 | otherwise -> ph hs'
-  nubSort  =  nub . sort -- TODO: this is O(n^2), make this O(n log n)
 
 
 -- -- Expression enumeration -- --
 
+-- | Enumerate applications between values of the given list of primitives
+--   and of the given expressions's type.
+--
+-- __Arguments:__
+--
+-- 1. an 'Expr' whose type we are interested in
+-- 2. a filtering function, returning 'True' for the expressions to keep
+-- 3. a list of primitives to be used in building expression.
+--
+-- __Result:__ a potentially infinite list of list of enumerated expressions
+--
+-- The enumeration here is type-directed for performance reasons.
 enumerateAppsFor :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
 enumerateAppsFor h keep es  =  for h
   where
@@ -303,18 +316,20 @@
           ,  typ h == typ hfx
           ]
 
+-- | Given an expression whose holes are /all of the same type/
+--   and an enumeration of 'Expr's of this same type,
+--   enumerate all possible fillings of the original expression
+--   with the 'Expr's in the enumeration.
 enumerateFillings :: Expr -> [[Expr]] -> [[Expr]]
 enumerateFillings e  =  mapT (fill e)
                      .  products
                      .  replicate (length $ holes e)
 
--- Like 'isDeconstruction' but lifted over the 'Expr' type.
-isDeconstructionE :: [Expr] -> Expr -> Expr -> Bool
---                   [a] -> (a -> Bool) -> (a -> a) -> Bool
-isDeconstructionE [] _ _  =  error "isDeconstructionE: empty list of test values"
-isDeconstructionE es ez ed | all isIllTyped [f :$ e | e <- es, f <- [ez,ed]]  =  error "isDeconstructionE: types do not match"
-isDeconstructionE es ez ed  =  isDeconstruction es (eval False . (ez :$)) (ed :$)
-
+-- | Evaluates an 'Expr' to a 'Dynamic' value
+--   using the given recursive definition and
+--   maximum number of recursive calls.
+--
+-- (cf. 'Conjure.Defn.toDynamicWithDefn')
 recursiveToDynamic :: (Expr,Expr) -> Int -> Expr -> Maybe Dynamic
 recursiveToDynamic (efxs, ebody) n  =  fmap (\(_,_,d) -> d) . re (n * size ebody) n
   where
@@ -353,9 +368,22 @@
                           Just (m', n', d2) -> (m',n',) <$> dynApply d1 d2
   _ $$ _               =  Nothing
 
+-- | Evaluates an 'Expr' to a regular Haskell value
+--   using the given recursive definition and
+--   maximum number of recursive calls.
+--   If there's a type mismatch, this function returns 'Nothing'.
+--
+-- (cf. 'evaluate', 'Conjure.Defn.devaluate')
 revaluate :: Typeable a => (Expr,Expr) -> Int -> Expr -> Maybe a
 revaluate dfn n e  =  recursiveToDynamic dfn n e >>= fromDynamic
 
+-- | Evaluates an 'Expr' to a regular Haskell value
+--   using the given recursive definition and
+--   maximum number of recursive calls.
+--   If there's a type mismatch,
+--   this function returns the given default value.
+--
+-- (cf. 'eval', 'Conjure.Defn.deval')
 reval :: Typeable a => (Expr,Expr) -> Int -> a -> Expr -> a
 reval dfn n x  =  fromMaybe x . revaluate dfn n
 
@@ -386,6 +414,10 @@
   | (e',es') <- choicesThat (\e' _ -> any (`elem` vars e') (vars e)) es'
   ]
 
+-- | Turns all variables of an expression into holes.
+--
+-- > > rehole (xx -+- yy)
+-- > _ + _ :: Int
 rehole :: Expr -> Expr
 rehole (e1 :$ e2)    = rehole e1 :$ rehole e2
 rehole e | isVar e   = "" `varAsTypeOf` e
diff --git a/src/Conjure/Prim.hs b/src/Conjure/Prim.hs
--- a/src/Conjure/Prim.hs
+++ b/src/Conjure/Prim.hs
@@ -4,7 +4,7 @@
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
--- This module is part of 'Conjure'.
+-- This module is part of "Conjure".
 --
 -- The 'Prim' type and utilities involving it.
 --
@@ -57,16 +57,28 @@
 -- Conjure.Conjurable but need a list of Prims instead of a Conjurable
 -- representative.
 
+-- | Computes a list of 'Reification1's from a list of 'Prim's.
+--
+-- This function mirrors functionality of 'conjureReification'.
 cjReification :: [Prim] -> [Reification1]
 cjReification ps  =  nubOn (\(eh,_,_,_,_,_) -> eh)
                   $  foldr (.) id (map snd ps) [conjureReification1 bool]
 
+-- | Computes a list of holes encoded as 'Expr's from a list of 'Prim's.
+--
+-- This function mirrors functionality from 'conjureHoles'.
 cjHoles :: [Prim] -> [Expr]
 cjHoles ps  =  [eh | (eh,_,Just _,_,_,_) <- cjReification ps]
 
+-- | Computes a function that equates two 'Expr's from a list of 'Prim's.
+--
+-- This function mirrors functionality from 'conjureMkEquation'.
 cjMkEquation :: [Prim] -> Expr -> Expr -> Expr
 cjMkEquation ps  =  mkEquation [eq | (_,Just eq,_,_,_,_) <- cjReification ps]
 
+-- | Given a list of 'Prim's,
+--   computes a function that checks whether two 'Expr's are equal
+--   up to a given number of tests.
 cjAreEqual :: [Prim] -> Int -> Expr -> Expr -> Bool
 cjAreEqual ps maxTests  =  (===)
   where
@@ -75,6 +87,11 @@
   isTrue  =  all (errorToFalse . eval False) . gs
   gs  =  take maxTests . grounds (cjTiersFor ps)
 
+-- | Given a list of 'Prim's,
+--   returns a function that given an 'Expr'
+--   will return tiers of test 'Expr' values.
+--
+-- This is used in 'cjAreEqual'.
 cjTiersFor :: [Prim] -> Expr -> [[Expr]]
 cjTiersFor ps e  =  tf allTiers
   where
diff --git a/src/Conjure/Spec.hs b/src/Conjure/Spec.hs
deleted file mode 100644
--- a/src/Conjure/Spec.hs
+++ /dev/null
@@ -1,191 +0,0 @@
--- |
--- Module      : Conjure.Spec
--- Copyright   : (c) 2021 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- An internal module of 'Conjure',
--- a library for Conjuring function implementations
--- from tests or partial definitions.
--- (a.k.a.: functional inductive programming)
-module Conjure.Spec
-  ( Spec1
-  , Spec2
-  , Spec3
-  , (-=)
-  , conjure1
-  , conjure2
-  , conjure3
-  , conjure1With
-  , conjure2With
-  , conjure3With
-  )
-where
-
-import Conjure.Engine
-import Conjure.Conjurable
-import Conjure.Utils
-import Conjure.Prim
-
-
--- | A partial specification of a function with one argument:
---
--- > sumSpec :: Spec1 [Int] Int
--- > sumSpec  =
--- >   [ []      -= 0
--- >   , [1,2]   -= 3
--- >   , [3,4,5] -= 12
--- >   ]
---
--- To be passed as one of the arguments to 'conjure1'.
-type Spec1 a b     = [(a,b)]
-
-
--- | A partial specification of a function with two arguments:
---
--- > appSpec :: Spec2 [Int] [Int] [Int]
--- > appSpec  =
--- >   [ (,) []      [0,1]   -= [0,1]
--- >   , (,) [2,3]   []      -= [2,3]
--- >   , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--- >   ]
---
--- To be passed as one of the arguments to 'conjure2'.
-type Spec2 a b c   = [((a,b),c)]
-
-
--- | A partial specification of a function with three arguments.
---
--- To be passed as one of the arguments to 'conjure3'
-type Spec3 a b c d = [((a,b,c),d)]
-
-
--- | To be used when constructing specifications:
---   'Spec1',
---   'Spec2' and
---   'Spec3'.
-(-=) :: a -> b -> (a,b)
-(-=)  =  (,)
-
-
--- | Conjures a one argument function from a specification.
---
--- Given:
---
--- > sumSpec :: Spec1 [Int] Int
--- > sumSpec  =
--- >   [ []      -= 0
--- >   , [1,2]   -= 3
--- >   , [3,4,5] -= 12
--- >   ]
---
--- > sumPrimitives :: [Prim]
--- > sumPrimitives  =
--- >   [ prim "null" (null :: [Int] -> Bool)
--- >   , pr (0::Int)
--- >   , prim "+"    ((+) :: Int -> Int -> Int)
--- >   , prim "head" (head :: [Int] -> Int)
--- >   , prim "tail" (tail :: [Int] -> [Int])
--- >   ]
---
--- Then:
---
--- > > conjure1 "sum" sumSpec sumPrimitives
--- > sum :: [Int] -> Int
--- > -- testing 3 combinations of argument values
--- > -- ...
--- > -- looking through 189/465 candidates of size 10
--- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
---
--- (cf. 'Spec1', 'conjure1With')
-conjure1 :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b)
-         => String -> Spec1 a b -> [Prim] -> IO ()
-conjure1  =  conjure1With args
-
-
--- | Conjures a two argument function from a specification.
---
--- Given:
---
--- > appSpec :: Spec2 [Int] [Int] [Int]
--- > appSpec  =
--- >   [ (,) []      [0,1]   -= [0,1]
--- >   , (,) [2,3]   []      -= [2,3]
--- >   , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--- >   ]
---
--- > appPrimitives :: [Expr]
--- > appPrimitives =
--- >   [ prim "null" (null :: [Int] -> Bool)
--- >   , prim ":"    ((:) :: Int -> [Int] -> [Int])
--- >   , prim "head" (head :: [Int] -> Int)
--- >   , prim "tail" (tail :: [Int] -> [Int])
--- >   ]
---
--- Then:
---
--- > > conjure2 "++" appSpec appPrimitives
--- > (++) :: [Int] -> [Int] -> [Int]
--- > -- testing 3 combinations of argument values
--- > -- ...
--- > -- looking through 26166/57090 candidates of size 11
--- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
---
--- (cf. 'Spec2', 'conjure2With')
-conjure2 :: ( Conjurable a, Eq a, Show a, Express a
-            , Conjurable b, Eq b, Show b, Express b
-            , Conjurable c, Eq c
-            ) => String -> Spec2 a b c -> [Prim] -> IO ()
-conjure2  =  conjure2With args
-
-
--- | Conjures a three argument function from a specification.
---
--- (cf. 'Spec3', 'conjure3With')
-conjure3 :: ( Conjurable a, Eq a, Show a, Express a
-            , Conjurable b, Eq b, Show b, Express b
-            , Conjurable c, Eq c, Show c, Express c
-            , Conjurable d, Eq d
-            ) => String -> Spec3 a b c d -> [Prim] -> IO ()
-conjure3  =  conjure3With args
-
-
--- | Like 'conjure1' but allows setting options through 'Args'/'args'.
-conjure1With :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b)
-             => Args -> String -> Spec1 a b -> [Prim] -> IO ()
-conjure1With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun1 bs)
-  where
-  ts = [[val x] | (x,_) <- bs]
-
-
--- | Like 'conjure2' but allows setting options through 'Args'/'args'.
-conjure2With :: ( Conjurable a, Eq a, Show a, Express a
-                , Conjurable b, Eq b, Show b, Express b
-                , Conjurable c, Eq c
-                ) => Args -> String -> Spec2 a b c -> [Prim] -> IO ()
-conjure2With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun2 bs)
-  where
-  ts = [[val x, val y] | ((x,y),_) <- bs]
-
-
--- | Like 'conjure3' but allows setting options through 'Args'/'args'.
-conjure3With :: ( Conjurable a, Eq a, Show a, Express a
-                , Conjurable b, Eq b, Show b, Express b
-                , Conjurable c, Eq c, Show c, Express c
-                , Conjurable d, Eq d
-                ) => Args -> String -> Spec3 a b c d -> [Prim] -> IO ()
-conjure3With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun3 bs)
-  where
-  ts = [[val x, val y, val z] | ((x,y,z),_) <- bs]
-
-
-mkFun1 :: Eq a => [(a,b)] -> a -> b
-mkFun1 bs  =  \x -> fromMaybe undefined $ lookup x bs
-
-
-mkFun2 :: (Eq a, Eq b) => [((a,b),c)] -> a -> b -> c
-mkFun2 bs  =  \x y -> fromMaybe undefined $ lookup (x,y) bs
-
-
-mkFun3 :: (Eq a, Eq b, Eq c) => [((a,b,c),d)] -> a -> b -> c -> d
-mkFun3 bs  =  \x y z -> fromMaybe undefined $ lookup (x,y,z) bs
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -4,7 +4,7 @@
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
--- An internal module of 'Conjure'.
+-- An internal module of "Conjure".
 -- This exports 'Data.List', 'Data.Maybe', 'Data.Function'
 -- and a few other simple utitilites.
 {-# LANGUAGE CPP #-}
@@ -19,17 +19,11 @@
   , count
   , nubOn
   , nubSort
-  , iterateUntil
   , mzip
   , groupOn
 #if __GLASGOW_HASKELL__ < 710
   , sortOn
 #endif
-  , takeUntil
-  , takeNextWhile
-  , takeNextUntil
-  , deconstructions
-  , isDeconstruction
   , idIO
   , mapHead
   , sets
@@ -37,7 +31,6 @@
   , allEqual
   , choices
   , choicesThat
-  , filterAnd
   )
 where
 
@@ -50,18 +43,22 @@
 
 import System.IO.Unsafe
 
+-- | Checks if all elements of a list are equal.
 allEqual :: Eq a => [a] -> Bool
 allEqual []  =  False
 allEqual [x]  =  False
 allEqual [x,y]  =  x == y
 allEqual (x:y:xs)  =  x == y && allEqual (y:xs)
 
+-- | Counts the number of occurrences on a list.
 count :: (a -> Bool) -> [a] -> Int
 count p  =  length . filter p
 
+-- | Nubs using a given field.
 nubOn :: Eq b => (a -> b) -> [a] -> [a]
 nubOn f  =  nubBy ((==) `on` f)
 
+-- | Equivalent to @nub . sort@ but running in /O(n log n)/.
 nubSort :: Ord a => [a] -> [a]
 nubSort  =  nnub . sort
   where
@@ -70,55 +67,26 @@
   nnub [x] = [x]
   nnub (x:xs) = x : nnub (dropWhile (==x) xs)
 
-iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
-iterateUntil (?) f  =  iu
-  where
-  iu x | x ? fx     =  x
-       | otherwise  =  iu fx
-    where
-    fx  =  f x
-
+-- | Zips 'Monoid' values leaving trailing values.
+--
+-- > > mzip ["ab","cd"] ["ef"]
+-- > ["abef","cd"]
 mzip :: Monoid a => [a] -> [a] -> [a]
 mzip [] []  =  []
 mzip [] ys  =  ys
 mzip xs []  =  xs
 mzip (x:xs) (y:ys)  =  x <> y : mzip xs ys
 
+-- | Group values using a given field selector.
 groupOn :: Eq b => (a -> b) -> [a] -> [[a]]
 groupOn f = groupBy ((==) `on` f)
 
 #if __GLASGOW_HASKELL__ < 710
+-- | 'sort' on a given field.
 sortOn :: Ord b => (a -> b) -> [a] -> [a]
 sortOn f = sortBy (compare `on` f)
 #endif
 
-takeUntil :: (a -> Bool) -> [a] -> [a]
-takeUntil p  =  takeWhile (not . p)
-
-takeNextWhile :: (a -> a -> Bool) -> [a] -> [a]
-takeNextWhile (?)  =  t
-  where
-  t (x:y:xs) | x ? y  =  x : t (y:xs)
-             | otherwise  =  [x]
-  t xs  =  xs
-
-takeNextUntil :: (a -> a -> Bool) -> [a] -> [a]
-takeNextUntil (?)  =  takeNextWhile (not .: (?))
-  where
-  (.:)  =  (.) . (.)
-
-deconstructions :: (a -> Bool) -> (a -> a) -> a -> [a]
-deconstructions z d x  =  takeUntil z
-                       $  iterate d x
-
--- | The deconstruction is considered valid if it converges
---   for more than half of the given values.
-isDeconstruction :: [a] -> (a -> Bool) -> (a -> a) -> Bool
-isDeconstruction xs z d  =  count is xs >= l `div` 2
-  where
-  is x  =  length (take l $ deconstructions z d x) < l
-  l  =  length xs
-
 -- | __WARNING:__
 --   uses 'unsafePerformIO' and should only be used for debugging!
 --
@@ -130,31 +98,31 @@
   action x
   return x
 
+-- | Applies a function to the head of a list.
 mapHead :: (a -> a) -> [a] -> [a]
 mapHead f (x:xs)  =  f x : xs
 
+-- | Return sets of values based on the list.
+--
+-- The values in the list must me unique.
 sets :: [a] -> [[a]]
 sets []  =  [[]]
 sets (x:xs)  =  map (x:) ss ++ ss
   where
   ss  =  sets xs
 
+-- | Like 'head' but allows providing a default value.
 headOr :: a -> [a] -> a
 headOr x []  =  x
 headOr _ (x:xs)  =  x
 
+-- | Lists choices of values.
 choices :: [a] -> [(a,[a])]
 choices []  =  []
 choices (x:xs)  =  (x,xs) : map (mapSnd (x:)) (choices xs)
   where
   mapSnd f (x,y)  =  (x,f y)
 
+-- | Lists choices of values that follow a property.
 choicesThat :: (a -> [a] -> Bool) -> [a] -> [(a,[a])]
 choicesThat (?)  =  filter (uncurry (?)) . choices
-
-filterAnd :: (a -> Bool) -> [a] -> ([a],Bool)
-filterAnd p xs  =  (xs', and ps)
-  where
-  xps  =  [(x,p x) | x <- xs]
-  xs'  =  [x | (x,True) <- xps]
-  ps   =  [p | (_,p) <- xps]
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -11,4 +11,4 @@
 extra-deps:
 - leancheck-0.9.10
 - speculate-0.4.14
-- express-1.0.6
+- express-1.0.8
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -13,7 +13,6 @@
   , module Test.LeanCheck
   , module Test.LeanCheck.Utils
   , module Test.ListableExpr
-  , module Test.Candidates
 
   , mainTest
   )
@@ -25,7 +24,6 @@
 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
deleted file mode 100644
--- a/test/Test/Candidates.hs
+++ /dev/null
@@ -1,60 +0,0 @@
--- |
--- 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/derive.hs b/test/derive.hs
new file mode 100644
--- /dev/null
+++ b/test/derive.hs
@@ -0,0 +1,91 @@
+-- Copyright (c) 2019-2021 Rudy Matela.
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+import Test hiding ((-:), (->:))
+-- -: and ->: should be generated by deriveConjurable
+
+data Choice  =  Ae | Bee | Cee deriving (Show, Eq, Typeable)
+data Peano  =  Zero | Succ Peano deriving (Show, Eq, Typeable)
+data List a  =  a :- List a | Nil deriving (Show, Eq, Typeable)
+data Bush a  =  Bush a :-: Bush a | Leaf a deriving (Show, Eq, Typeable)
+data Tree a  =  Node (Tree a) a (Tree a) | Null deriving (Show, Eq, Typeable)
+
+deriveConjurable ''Choice
+deriveConjurable ''Peano
+deriveConjurable ''List
+deriveConjurable ''Bush
+deriveConjurable ''Tree
+
+-- Nested datatype cascade
+data Nested  =  Nested N0 (N1 Int) (N2 Int Int) deriving (Eq, Show, Typeable)
+data N0      =  R0 Int deriving (Eq, Show, Typeable)
+data N1 a    =  R1 a   deriving (Eq, Show, Typeable)
+data N2 a b  =  R2 a b deriving (Eq, Show, Typeable)
+
+deriveConjurableCascading ''Nested
+
+-- Recursive nested datatype cascade
+data RN       =  RN RN0 (RN1 Int) (RN2 Int RN) deriving (Eq, Show, Typeable)
+data RN0      =  Nest0 Int | Recurse0 RN deriving (Eq, Show, Typeable)
+data RN1 a    =  Nest1 a   | Recurse1 RN deriving (Eq, Show, Typeable)
+data RN2 a b  =  Nest2 a b | Recurse2 RN deriving (Eq, Show, Typeable)
+-- beware: values of the above type are always infinite!
+--         derivation works but full evaluation does not terminate
+
+deriveConjurableCascading ''RN
+
+-- Those should have no effect (instance already exists):
+{- uncommenting those should generate warnings
+deriveConjurable ''Bool
+deriveConjurable ''Maybe
+deriveConjurable ''Either
+-}
+
+-- Those should not generate warnings
+deriveConjurableIfNeeded ''Bool
+deriveConjurableIfNeeded ''Maybe
+deriveConjurableIfNeeded ''Either
+
+data Mutual    =  Mutual0   | Mutual CoMutual deriving (Eq, Show, Typeable)
+data CoMutual  =  CoMutual0 | CoMutual Mutual deriving (Eq, Show, Typeable)
+
+deriveConjurableCascading ''Mutual
+
+
+main :: IO ()
+main  =  mainTest tests 5040
+
+tests :: Int -> [Bool]
+tests n  =
+  [ True
+
+  , conjurableOK (undefined :: Bool)
+  , conjurableOK (undefined :: Int)
+  , conjurableOK (undefined :: Char)
+  , conjurableOK (undefined :: [Bool])
+  , conjurableOK (undefined :: [Int])
+  , conjurableOK (undefined :: String)
+
+  , conjurableOK (undefined :: Choice)
+  , conjurableOK (undefined :: Peano)
+  , conjurableOK (undefined :: List Int)
+  , conjurableOK (undefined :: Bush Int)
+  , conjurableOK (undefined :: Tree Int)
+--, conjurableOK (undefined :: RN) -- TODO: FIX: infinite loop somewhere...
+  ]
+
+
+-- checks if the functions conjureEquality, conjureExpress and conjureTiers
+-- were correctly generated.
+conjurableOK :: (Eq a, Show a, Express a, Listable a, Conjurable a) => a -> Bool
+conjurableOK x  =  and
+  [ holds 60 $ (-==-) ==== (==)
+  , holds 60 $ expr' === expr
+  , tiers =| 6 |= (tiers -: [[x]])
+  ]
+  where
+  (-==-)  =  evl (fromJust $ conjureEquality x) -:> x
+  tiers'  =  mapT evl (fromJust $ conjureTiers x) -: [[x]]
+  expr'  =  (conjureExpress x . val) -:> x
diff --git a/test/expr.hs b/test/expr.hs
--- a/test/expr.hs
+++ b/test/expr.hs
@@ -67,67 +67,6 @@
        , 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]
@@ -154,12 +93,6 @@
                                     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
-
   , possibleHoles [plus, times, zero, one]
     == [ hole (undefined :: Int)
        , hole (undefined :: Int -> Int)
@@ -226,4 +159,19 @@
          , (yy-:-yys, yy-:-xxs)
          ]
        ]
+
+  -- type-correct applications are allowed on $$, $$|< and $$**
+  , absE $$   zero  ==  Just (abs' zero)
+  , absE $$|< zero  ==  Just (abs' zero)
+  , absE $$** zero  ==  Just (abs' zero)
+
+  -- kind-correct applications are allowed on $$|< and $$**
+  , ordE $$   zero  ==  Nothing
+  , ordE $$|< zero  ==  Just (ordE :$ zero)
+  , ordE $$** zero  ==  Just (ordE :$ zero)
+
+  -- type-incorrect applications are allowed on $$**
+  , zero $$   zero  ==  Nothing
+  , zero $$|< zero  ==  Nothing
+  , zero $$** zero  ==  Just (zero :$ zero)
   ]
diff --git a/test/utils.hs b/test/utils.hs
--- a/test/utils.hs
+++ b/test/utils.hs
@@ -10,48 +10,12 @@
 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]])
 
-  , takeUntil (== 5) [1..] == [1,2,3,4]
-  , takeUntil (> 4)  [1..] == [1,2,3,4]
-
-  , takeNextWhile (<) []  ==  ([]::[Int])
-  , takeNextWhile (<) [0]  ==  [0]
-  , takeNextWhile (<) [0,1]  ==  [0,1]
-  , takeNextWhile (<) [0,1,2]  ==  [0,1,2]
-  , takeNextWhile (<) [0,1,2,1,0]  ==  [0,1,2]
-  , takeNextWhile (/=) [3,2,1,0,0,0] == [3,2,1,0]
-  , takeNextUntil (==) [3,2,1,0,0,0] == [3,2,1,0]
-  , takeNextUntil (>) [0,1,2,1,0] == [0,1,2]
-
-  , deconstructions null tail [1,2,3 :: Int]
-    == [ [1,2,3]
-       , [2,3]
-       , [3]
-       ]
-  , deconstructions null tail ([] :: [Int]) == []
-  , deconstructions (==0) (`div`2) 15
-    == [15, 7, 3, 1]
-
-  ,       isDec m (null :: [A] -> Bool) tail
-  , not $ isDec m (null :: [A] -> Bool) id
-  ,       isDec m (null :: [A] -> Bool) (drop 1)
-  ,       isDec m (null :: [A] -> Bool) (drop 2)
-  ,       isDec m (null :: [A] -> Bool) (drop 3)
-  ,       isDec m (<0) (\x -> x-1 :: Int)
-  ,       isDec m (<0) (\x -> x-2 :: Int)
-  ,       isDec m (==0) (\x -> x-1 :: Int)
-  , not $ isDec m (==0) (\x -> x-2 :: Int)
-  ,       isDec m (==0) (\x -> x `div` 2 :: Int)
-  ,       isDec m (==0) (\x -> x `quot` 2 :: Int)
-
   , sets []  ==  [[] :: [Int]]
   , sets [1]  ==  [[1], [] :: [Int]]
   , sets [1,2]  ==  [[1,2], [1], [2], [] :: [Int]]
@@ -59,13 +23,3 @@
   ]
   where
   m  =  n `div` 60
-
-
--- Checks if the given pair of functions are a valid deconstruction
--- for Listable values.
--- The deconstruction is considered valid if it converges
--- for more than 50% of values.
-isDec :: Listable a
-      => Int
-      -> (a -> Bool) -> (a -> a) -> Bool
-isDec m  =  isDeconstruction (take m list)