diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,131 @@
+# Builds and tests this Haskell project on "GitHub Actions"
+#
+# 2021  Rudy Matela
+#
+# some docs: https://github.com/haskell/actions/tree/main/setup
+name: build
+on: [push]
+jobs:
+  build-and-test:
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: Cache ~/.cabal/packages
+        uses: actions/cache@v2
+        with:
+          path: ~/.cabal/packages
+          key:          v1-${{ runner.os }}-cabal-packages-${{ hashFiles('hello.cabal') }}
+          restore-keys: v1-${{ runner.os }}-cabal-packages-
+
+      - name: Cache ~/.cabal and ~/.ghc
+        uses: actions/cache@v2
+        with:
+          path: |
+            ~/.cabal
+            !~/.cabal/packages
+            ~/.ghc
+          key:          v1-${{ runner.os }}-cabal-ghc-latest-${{ hashFiles('hello.cabal') }}
+          restore-keys: v1-${{ runner.os }}-cabal-ghc-latest-
+
+      - run: du -hd3 ~/.cabal ~/.ghc || true
+
+      - run: haddock --version || sudo apt-get install ghc-haddock
+      - run: ghc   --version
+      - run: cabal --version
+
+      - name: Check out repository
+        uses: actions/checkout@v2
+
+      - run: cabal update
+      - run: make install-dependencies
+
+      - run: make
+      - run: make test
+      - run: make haddock
+      - run: make test-sdist
+      - run: make test-via-cabal
+
+
+  test-with-ghc:
+    strategy:
+      matrix:
+        ghc:
+          - '9.0'
+          - '8.10'
+          - '8.8'
+          - '8.6'
+          - '8.4'
+          - '8.2'
+          - '8.0'
+          - '7.10'
+          - '7.8'
+    runs-on: ubuntu-latest
+    needs: build-and-test
+    container: haskell:${{ matrix.ghc }}
+    steps:
+      - name: Cache ~/.cabal/packages
+        uses: actions/cache@v2
+        with:
+          path: ~/.cabal/packages
+          key:          v1-${{ runner.os }}-cabal-packages-${{ hashFiles('hello.cabal') }}
+          restore-keys: v1-${{ runner.os }}-cabal-packages-
+
+      - name: Cache ~/.cabal and ~/.ghc
+        uses: actions/cache@v2
+        with:
+          path: |
+            ~/.cabal
+            !~/.cabal/packages
+            ~/.ghc
+          key:          v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-${{ hashFiles('hello.cabal') }}
+          restore-keys: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-
+
+      - run: du -hd3 ~/.cabal ~/.ghc || true
+
+      - run: make --version || rm /etc/apt/sources.list.d/*.list # faster update
+      - run: make --version || apt-get update
+      - run: make --version || apt-get install make
+
+      - run: ghc   --version
+      - run: cabal --version
+
+      - name: Check out repository
+        uses: actions/checkout@v2
+
+      - run: cabal update
+      - run: make install-dependencies
+
+      - run: make
+      - run: make test
+      - run: make haddock
+      - run: make test-sdist
+      - run: make test-via-cabal
+
+  test-with-stack:
+    runs-on: ubuntu-latest
+    needs: build-and-test
+    steps:
+      - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS
+        uses: haskell/actions/setup@v1
+        with: # lts-17.9
+          ghc-version: '8.10.4'
+          cabal-version: '3.2'
+
+      - uses: actions/cache@v2
+        with:
+          path: ~/.stack
+          key:          v1-${{ runner.os }}-stack-${{ hashFiles('stack.yaml') }}
+          restore-keys: v1-${{ runner.os }}-stack-
+
+      - name: Check out repository
+        uses: actions/checkout@v2
+      - run: make test-via-stack
+
+  test-with-hugs:
+    runs-on: ubuntu-latest
+    needs: build-and-test
+    steps:
+      - run: sudo apt-get install hugs
+      - name: Check out repository
+        uses: actions/checkout@v2
+      - run: make hugs-test
diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,6 @@
 # gitignore for Conjure
 #
-# Part of Conjure, Copyright 2020  Rudy Matela,
+# Part of Conjure, Copyright 2021  Rudy Matela,
 # distribued under the 3-clause BSD license.
 
 # temporary files
@@ -31,5 +31,7 @@
 eg/bools
 eg/factorial
 eg/ints
+eg/list
 proto/u-conjure
 test/expr
+test/conjurable
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,94 +0,0 @@
-# .travis.yml file for Conjure
-#
-# Copyright:   (c) 2017-2021 Rudy Matela
-# License:     3-Clause BSD  (see the file LICENSE)
-# Maintainer:  Rudy Matela <rudy@matela.com.br>
-
-language: c  # not really
-
-notifications:
-  email:
-    on_failure: change
-
-sudo: false
-
-cache:
-  directories:
-  - $HOME/.ghc
-  - $HOME/.cabal
-  - $HOME/.stack
-
-before_install:
-- export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
-- ghc --version
-- cabal --version
-- haddock --version
-- du -hd3 ~/.cabal ~/.ghc || true
-- du -hd4 ~/.stack || true
-- rm -f ~/.cabal/config && cabal update
-# Download and unpack the stack executable
-# "Once Travis whitelists the stack.dev files," simply include stack in the
-# addons section. -- https://docs.haskellstack.org/en/stable/travis_ci/
-- mkdir -p ~/.local/bin
-- export PATH=$HOME/.local/bin:$PATH
-- travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
-- stack config set system-ghc --global true
-- stack --version
-- cabal install leancheck express speculate || cabal install leancheck express speculate --lib
-
-script:
-- make && make test
-- make haddock
-- make test-sdist
-- cabal test --ghc-option=-O0
-- stack --resolver $STACKVER --no-terminal --skip-ghc-check test --ghc-options=-O0
-
-matrix:
-  allow_failures:
-  - env:                   GHCVER=head        CABALVER=head    STACKVER=nightly-2021-04-06
-  - env:                   GHCVER=9.0.1       CABALVER=head    STACKVER=nightly-2021-04-06
-  include:
-  - ghc: 'head'
-    env:                   GHCVER=head        CABALVER=head    STACKVER=nightly-2021-04-06
-    addons: {apt: {packages: [ghc-head,  cabal-install-head],  sources: hvr-ghc}}
-  - ghc: '9.0'
-    env:                   GHCVER=9.0.1       CABALVER=head    STACKVER=nightly-2021-04-06
-    addons: {apt: {packages: [ghc-9.0.1, cabal-install-head],  sources: hvr-ghc}}
-  - ghc: '8.10'
-    env:                   GHCVER=8.10.4       CABALVER=3.2    STACKVER=lts-17.9
-    addons: {apt: {packages: [ghc-8.10.4, cabal-install-3.2],  sources: hvr-ghc}}
-  - ghc: '8.8'
-    env:                   GHCVER=8.8.4        CABALVER=3.0    STACKVER=lts-16.31
-    addons: {apt: {packages: [ghc-8.8.4,  cabal-install-3.0],  sources: hvr-ghc}}
-  - ghc: '8.6'
-    env:                   GHCVER=8.6.5        CABALVER=2.4    STACKVER=lts-14.27
-    addons: {apt: {packages: [ghc-8.6.5,  cabal-install-2.4],  sources: hvr-ghc}}
-  - ghc: '8.4'
-    env:                   GHCVER=8.4.4        CABALVER=2.2    STACKVER=lts-12.26
-    addons: {apt: {packages: [ghc-8.4.4,  cabal-install-2.2],  sources: hvr-ghc}}
-  - ghc: '8.2'
-    env:                   GHCVER=8.2.2        CABALVER=2.0    STACKVER=lts-11.22
-    addons: {apt: {packages: [ghc-8.2.2,  cabal-install-2.0],  sources: hvr-ghc}}
-  - ghc: '8.0'
-    env:                   GHCVER=8.0.2        CABALVER=1.24   STACKVER=lts-9.21
-    addons: {apt: {packages: [ghc-8.0.2,  cabal-install-1.24], sources: hvr-ghc}}
-  - ghc: '7.10'
-    env:                   GHCVER=7.10.3       CABALVER=1.22   STACKVER=lts-6.35
-    addons: {apt: {packages: [ghc-7.10.3, cabal-install-1.22], sources: hvr-ghc}}
-  # we only support stack with GHC >= 7.10
-  - ghc: '7.8'
-    env:                   GHCVER=7.8.4        CABALVER=1.18
-    addons: {apt: {packages: [ghc-7.8.4,  cabal-install-1.18], sources: hvr-ghc}}
-    before_install:
-    - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
-    - ghc --version
-    - cabal --version
-    - haddock --version
-    - rm -f ~/.cabal/config && cabal update
-    - cabal install Cabal==1.18.*
-    - cabal install leancheck express speculate
-    script:
-    - make && make test
-    - make haddock HADDOCKFLAGS=
-    - make test-sdist
-    - cabal test
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,9 @@
 GHCIMPORTDIRS = src:test
 GHCFLAGS = -O2 \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic)
-HADDOCKFLAGS = --no-print-missing-docs \
+HADDOCKFLAGS = \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic)
+INSTALL_DEPS = leancheck express speculate
 
 EG = \
   eg/arith \
@@ -12,7 +13,8 @@
   proto/u-conjure
 
 TESTS = \
-  test/expr
+  test/expr \
+  test/conjurable
 
 all: mk/toplibs
 
@@ -38,6 +40,17 @@
 
 test-sdist:
 	./test/sdist
+
+test-via-cabal:
+	cabal configure --enable-tests --enable-benchmarks --ghc-options="$(GHCFLAGS) -O0"
+	cabal build
+	cabal test expr
+
+test-via-stack:
+	stack test code-conjure:test:expr --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal
+
+hugs-test:
+	echo 'Unsupported'
 
 clean: clean-hi-o clean-haddock
 	rm -f $(EG) $(TESTS)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -21,12 +21,11 @@
 To install the [latest Conjure version from Hackage], just run:
 
 	$ cabal update
-	$ cabal install code-conjure
-
-Starting from Cabal v3.0, you need to pass `--lib` as an argument to cabal
-install:
+	$ cabal v1-install code-conjure
 
-	$ cabal install code-conjure --lib
+If you are using Cabal v3.0 or later,
+[avoid using `cabal install`] for the time being
+and use `v1-install` instead.
 
 Prerequisites are [express], [leancheck] and [speculate].
 They should be automatically resolved and installed by [Cabal].
@@ -53,7 +52,6 @@
 	  , val (1::Int)
 	  , value "+" ((+) :: Int -> Int -> Int)
 	  , value "*" ((*) :: Int -> Int -> Int)
-	  , value "==" ((==) :: Int -> Int -> Bool)
 	  ]
 
 running
@@ -96,8 +94,6 @@
 	  , value "isZero" ((==0) :: Int -> Bool)
 	  , val False
 	  , val True
-	  , ifFor (undefined :: Int)
-	  , value "==" ((==) :: Int -> Int -> Bool)
 	  ]
 
 running
@@ -107,7 +103,7 @@
 yields
 
 	factorial :: Int -> Int
-	-- looking through 9266 candidates, 100% match, 6/6 assignments
+	-- looking through 8576 candidates, 100% match, 6/6 assignments
 	factorial x  =  if isZero x then 1 else x * factorial (dec x)
 
 in about 3 seconds.
@@ -143,7 +139,7 @@
 [Conjure's Haddock documentation].
 
 
-Conjure, Copyright 2020  Rudy Matela,
+Conjure, Copyright 2021  Rudy Matela,
 distribued under the 3-clause BSD license.
 
 
@@ -166,8 +162,11 @@
 [MagicHaskeller]: https://hackage.haskell.org/package/MagicHaskeller
 [Barliman]:       https://github.com/webyrd/Barliman
 
-[build-status]:                     https://travis-ci.org/rudymatela/conjure.svg?branch=master
-[build-log]:                        https://travis-ci.org/rudymatela/conjure
+[avoid using `cabal install`]:         https://github.com/haskell/cabal/issues/7373
+[latest Conjure version from Hackage]: https://hackage.haskell.org/package/code-conjure
+
+[build-log]:    https://github.com/rudymatela/conjure/actions/workflows/build.yml
+[build-status]: https://github.com/rudymatela/conjure/actions/workflows/build.yml/badge.svg
 [hackage-version]:                  https://img.shields.io/hackage/v/code-conjure.svg
 [code-conjure-on-hackage]:          https://hackage.haskell.org/package/code-conjure
 [stackage-lts-badge]:               https://stackage.org/package/code-conjure/badge/lts
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,5 +1,5 @@
 -- Setup.hs for code-conjure / Conjure
--- Part of Conjure, Copyright 2020  Rudy Matela,
+-- Part of Conjure, Copyright 2021  Rudy Matela,
 -- distribued under the 3-clause BSD license.
 import Distribution.Simple
 main = defaultMain
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -10,14 +10,6 @@
 * use FitSpec's notation of `"factorial n"` to name the variables
   instead of just `"factorial"`
 
-* Automatically include `if`s and `==`s.
-  Minor problem: typeclass folding is not possible for result values.
-
-* Automatically include background functions based on the argument types.
-  The `Arguable` typeclass is a sketch of how to do that based on
-  the `Generalizable` typeclass from the Extrapolate library.
-  Though the implementation is quite crufty.
-
 * use partially defined implementations?
 
     partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -0,0 +1,1 @@
+3.72
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -0,0 +1,1 @@
+2.78
diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/factorial.runtime
@@ -0,0 +1,1 @@
+2.18
diff --git a/bench/runtime/zero/eg/ints.runtime b/bench/runtime/zero/eg/ints.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/ints.runtime
@@ -0,0 +1,1 @@
+7.00
diff --git a/bench/runtime/zero/proto/u-conjure.runtime b/bench/runtime/zero/proto/u-conjure.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/proto/u-conjure.runtime
@@ -0,0 +1,1 @@
+0.11
diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/versions
@@ -0,0 +1,4 @@
+GHC 8.10.4
+leancheck-0.9.4
+express-0.1.6
+speculate-0.4.6
diff --git a/bench/versions b/bench/versions
new file mode 100644
--- /dev/null
+++ b/bench/versions
@@ -0,0 +1,19 @@
+#!/bin/bash
+#
+# bench/versions: print versions of installed dependencies
+#
+# Copyright (C) 2021  Rudy Matela
+# Distributed under the 3-Clause BSD licence (see the file LICENSE).
+get-ghc-v() {
+    ghc --version | sed -e "s/.* version/GHC/"
+}
+get-pkg-v() {
+    ghc-pkg list $1 2>/dev/null |
+    grep " $1-" |
+    sed -e "s/^ *//" |
+    tail -1
+}
+get-ghc-v
+get-pkg-v leancheck
+get-pkg-v express
+get-pkg-v speculate
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.0.4
+version:             0.1.0
 synopsis:            conjure Haskell functions out of partial definitions
 description:
   Conjure is a tool that produces Haskell functions out of partial definitions.
@@ -25,7 +25,7 @@
                , TODO.md
                , doc/conjure.svg
 extra-source-files: .gitignore
-                  , .travis.yml
+                  , .github/workflows/build.yml
                   , Makefile
                   , proto/*.hs
                   , eg/*.hs
@@ -37,10 +37,10 @@
                   , mk/haskell.mk
                   , mk/install-on
                   , stack.yaml
-                  , eg/runtime/zero/eg/*.runtime
-                  , eg/runtime/zero/proto/*.runtime
-                  , eg/runtime/zero/versions
-                  , eg/versions
+                  , bench/runtime/zero/eg/*.runtime
+                  , bench/runtime/zero/proto/*.runtime
+                  , bench/runtime/zero/versions
+                  , bench/versions
                   , test/model/eg/*.out
                   , test/model/proto/*.out
                   , test/sdist
@@ -53,15 +53,13 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.0.4
+  tag:             v0.1.0
 
 library
   exposed-modules: Conjure
-                 , Conjure.Arguable
                  , Conjure.Conjurable
                  , Conjure.Engine
                  , Conjure.Expr
-                 , Conjure.TypeBinding
                  , Conjure.Utils
   other-extensions: TemplateHaskell, CPP
   build-depends: base >= 4 && < 5
@@ -75,6 +73,14 @@
 test-suite expr
   type:                exitcode-stdio-1.0
   main-is:             expr.hs
+  other-modules:       Test
+  hs-source-dirs:      test
+  build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
+  default-language:    Haskell2010
+
+test-suite conjurable
+  type:                exitcode-stdio-1.0
+  main-is:             conjurable.hs
   other-modules:       Test
   hs-source-dirs:      test
   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure
diff --git a/eg/arith.hs b/eg/arith.hs
--- a/eg/arith.hs
+++ b/eg/arith.hs
@@ -39,5 +39,4 @@
   , val (1::Int)
   , value "+" ((+) :: Int -> Int -> Int)
   , value "*" ((*) :: Int -> Int -> Int)
-  , value "==" ((==) :: Int -> Int -> Bool)
   ]
diff --git a/eg/bools.hs b/eg/bools.hs
--- a/eg/bools.hs
+++ b/eg/bools.hs
@@ -19,8 +19,6 @@
   , value "null" (null :: [Bool] -> Bool)
   , value "head" (head :: [Bool] -> Bool)
   , value "tail" (tail :: [Bool] -> [Bool])
-  , ifFor (undefined :: Bool)
-  , value "==" ((==) :: [Bool] -> [Bool] -> Bool)
   ]
 
 -- target (for and):
diff --git a/eg/factorial.hs b/eg/factorial.hs
--- a/eg/factorial.hs
+++ b/eg/factorial.hs
@@ -27,8 +27,6 @@
   , value "isZero" ((==0) :: Int -> Bool)
   , val False
   , val True
-  , ifFor (undefined :: Int)
-  , value "==" ((==) :: Int -> Int -> Bool)
   ]
 
 
diff --git a/eg/ints.hs b/eg/ints.hs
--- a/eg/ints.hs
+++ b/eg/ints.hs
@@ -31,9 +31,6 @@
   , value "null" (null :: [Int] -> Bool)
   , value "head" (head :: [Int] -> Int)
   , value "tail" (tail :: [Int] -> [Int])
-  , ifFor (undefined :: Int)
-  , value "==" ((==) :: Int -> Int -> Bool)
-  , value "==" ((==) :: [Int] -> [Int] -> Bool)
   ]
 
 -- sum xs      =  if null xs then 0 else head xs + sum (tail xs)
diff --git a/eg/list.hs b/eg/list.hs
new file mode 100644
--- /dev/null
+++ b/eg/list.hs
@@ -0,0 +1,61 @@
+-- list.hs: conjuring functions over lists (of ints)
+--
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+import Data.List (insert)
+
+length' :: [Int] -> Int
+length' []       =  0
+length' [x]      =  1
+length' [x,y]    =  2
+length' [x,y,z]  =  3
+
+reverse' :: [Int] -> [Int]
+reverse' []       =  []
+reverse' [x]      =  [x]
+reverse' [x,y]    =  [y,x]
+reverse' [x,y,z]  =  [z,y,x]
+
+sort' :: [Int] -> [Int]
+sort' []       =  []
+sort' [x]      =  [x]
+sort' [x,y]
+  | x <= y     =  [x,y]
+  | otherwise  =  [y,x]
+sort' [x,y,z]
+  | x <= y && y <= z  =  [x,y,z]
+  | z <= y && y <= x  =  [z,y,x]
+
+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
+  conjureWith args {maxSize = 9} "length" length'
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "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
+  conjureWith args {maxSize = 11} "reverse" reverse'
+    [ val ([] :: [Int])
+    , value "unit" ((:[]) :: Int -> [Int])
+    , value "++" ((++) :: [Int] -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    ]
+
+  -- sort xs  =  if null xs then [] else insert (head xs) (sort (tail xs))
+  --             1  2    3       4       5       6    7    8     9    10
+  conjureWith args {maxSize = 10} "sort" sort'
+    [ val ([] :: [Int])
+    , value "insert" (insert :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    ]
diff --git a/eg/runtime/zero/eg/arith.runtime b/eg/runtime/zero/eg/arith.runtime
deleted file mode 100644
--- a/eg/runtime/zero/eg/arith.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-6.16
diff --git a/eg/runtime/zero/eg/bools.runtime b/eg/runtime/zero/eg/bools.runtime
deleted file mode 100644
--- a/eg/runtime/zero/eg/bools.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-3.33
diff --git a/eg/runtime/zero/eg/factorial.runtime b/eg/runtime/zero/eg/factorial.runtime
deleted file mode 100644
--- a/eg/runtime/zero/eg/factorial.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-2.70
diff --git a/eg/runtime/zero/eg/ints.runtime b/eg/runtime/zero/eg/ints.runtime
deleted file mode 100644
--- a/eg/runtime/zero/eg/ints.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-7.78
diff --git a/eg/runtime/zero/proto/u-conjure.runtime b/eg/runtime/zero/proto/u-conjure.runtime
deleted file mode 100644
--- a/eg/runtime/zero/proto/u-conjure.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-0.12
diff --git a/eg/runtime/zero/versions b/eg/runtime/zero/versions
deleted file mode 100644
--- a/eg/runtime/zero/versions
+++ /dev/null
@@ -1,4 +0,0 @@
-GHC 8.10.4
-leancheck-0.9.4
-express-0.1.6
-speculate-0.4.5
diff --git a/eg/versions b/eg/versions
deleted file mode 100644
--- a/eg/versions
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/bin/bash
-#
-# bench/versions: print versions of installed dependencies
-#
-# Copyright (C) 2021  Rudy Matela
-# Distributed under the 3-Clause BSD licence (see the file LICENSE).
-get-ghc-v() {
-    ghc --version | sed -e "s/.* version/GHC/"
-}
-get-pkg-v() {
-    ghc-pkg list $1 2>/dev/null |
-    grep " $1-" |
-    sed -e "s/^ *//" |
-    tail -1
-}
-get-ghc-v
-get-pkg-v leancheck
-get-pkg-v express
-get-pkg-v speculate
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -38,6 +38,16 @@
   src/Conjure/Engine.hs \
   src/Conjure/Conjurable.hs \
   eg/ints.hs
+eg/list: \
+  eg/list.hs \
+  mk/toplibs
+eg/list.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  eg/list.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
   src/Conjure.hs \
@@ -57,11 +67,6 @@
 proto/u-conjure: \
   proto/u-conjure.hs \
   mk/toplibs
-src/Conjure/Arguable.o: \
-  src/Conjure/Utils.hs \
-  src/Conjure/TypeBinding.hs \
-  src/Conjure/Expr.hs \
-  src/Conjure/Arguable.hs
 src/Conjure/Conjurable.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Expr.hs \
@@ -80,10 +85,20 @@
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Conjurable.hs
-src/Conjure/TypeBinding.o: \
-  src/Conjure/TypeBinding.hs
 src/Conjure/Utils.o: \
   src/Conjure/Utils.hs
+test/conjurable.o: \
+  test/Test.hs \
+  test/conjurable.hs \
+  src/Conjure/Utils.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs
+test/conjurable: \
+  test/Test.hs \
+  test/conjurable.hs \
+  mk/toplibs
 test/expr.o: \
   test/Test.hs \
   test/expr.hs \
diff --git a/mk/haskell.mk b/mk/haskell.mk
--- a/mk/haskell.mk
+++ b/mk/haskell.mk
@@ -21,6 +21,7 @@
 GHC ?= ghc
 GHCCMD = $(GHC) -i$(GHCIMPORTDIRS) $(GHCFLAGS)
 HADDOCK ?= haddock
+CABAL_INSTALL = $(shell cabal --version | grep -q "version [0-2]\." && echo 'cabal install' || echo 'cabal v1-install')
 
 # Hugs Parameters
 HUGSIMPORTDIRS ?= "/usr/lib/hugs/packages/*"
@@ -46,19 +47,13 @@
 
 LIB_DEPS ?= base
 ALL_DEPS ?= $(LIB_DEPS)
+INSTALL_DEPS ?=
 
 PKGNAME = $(shell cat *.cabal | grep "^name:"    | sed -e "s/name: *//")
-HADDOCK_VERSION = $(shell $(HADDOCK) --version | grep version | sed -e 's/.*version //;s/,.*//')
-HADDOCK_MAJOR = $(shell echo $(HADDOCK_VERSION) | sed -e 's/\..*//')
-HADDOCK_MINOR = $(shell echo $(HADDOCK_VERSION) | sed -e 's/[0-9]*\.\([0-9]*\).[0-9]*/\1/')
-HADDOCK_PKG_NAME = $(shell [ $(HADDOCK_MAJOR) -gt 2 ] \
-                        || [ $(HADDOCK_MAJOR) -eq 2 -a $(HADDOCK_MINOR) -ge 20 ] \
-                        && echo "--package-name=$(PKGNAME)")
-HADDOCK_HLNK_SRC = $(shell [ $(HADDOCK_MAJOR) -gt 2 ] \
-                        || [ $(HADDOCK_MAJOR) -eq 2 -a $(HADDOCK_MINOR) -ge 17 ] \
-                        && echo "--hyperlinked-source")
 
+HADDOCK_HAS = haddock --help | grep -q --
 
+
 # Implicit rules
 %.hi %.o: %.hs
 	$(GHCCMD) $< && touch $@
@@ -94,6 +89,9 @@
 depend:
 	find $(ALL_HSS) | ./mk/ghcdeps -i$(GHCIMPORTDIRS) $(GHCFLAGS) > $(DEPMK)
 
+install-dependencies:
+	$(CABAL_INSTALL) $(INSTALL_DEPS)
+
 # haddock rules
 haddock: doc/index.html
 
@@ -110,8 +108,9 @@
 	./mk/haddock-i $(LIB_DEPS) | xargs \
 	$(HADDOCK) --html -odoc $(LIB_HSS) \
 	  --title=$(PKGNAME) \
-	  $(HADDOCK_PKG_NAME) \
-	  $(HADDOCK_HLNK_SRC) \
+	  $(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)
 
 clean-cabal:
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -27,12 +27,8 @@
 -- >   , val (1::Int)
 -- >   , value "+" ((+) :: Int -> Int -> Int)
 -- >   , value "*" ((*) :: Int -> Int -> Int)
--- >   , value "==" ((==) :: Int -> Int -> Bool)
 -- > ]
 --
--- Including equality '==' over the given type is a good rule of thumb to
--- improve performance.
---
 -- Step 3: call conjure and see your generated function:
 --
 -- > > conjure "square" square background
@@ -46,16 +42,23 @@
     conjure
   , val
   , value
-  , ifFor
   , Expr
 
 -- * Advanced use
-  , conjpure
+  , conjureWithMaxSize
+  , conjureWith
   , Args(..)
   , args
-  , conjureWith
+
+-- * When using custom types
+  , Conjurable (conjureEquality, conjureTiers)
+  , reifyEquality, reifyTiers
+
+-- * Pure interfaces
+  , conjpure
   , conjpureWith
   )
 where
 
 import Conjure.Engine
+import Conjure.Conjurable
diff --git a/src/Conjure/Arguable.hs b/src/Conjure/Arguable.hs
deleted file mode 100644
--- a/src/Conjure/Arguable.hs
+++ /dev/null
@@ -1,331 +0,0 @@
--- |
--- Module      : Conjure.Arguable
--- Copyright   : (c) 2021 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- This module is part of 'Arguable'.
---
--- This defines the 'Arguable' typeclass
--- and utilities involving it.
---
--- You are probably better off importing "Conjure".
-{-# LANGUAGE CPP #-}
-module Conjure.Arguable
-  ( Arguable (..)
-  , instances
-
-  , mkEq1
-  , mkEq2
-  , mkEq3
-  , mkEq4
-  , mkOrd1
-  , mkOrd2
-  , mkOrd3
-  , mkOrd4
-
-  , (*==*)
-  , (*/=*)
-  , (*<=*)
-  , (*<*)
-
-  , Listable (..)
-  , module Conjure.Expr
-  )
-where
-
-import Data.Maybe
-import Data.Ratio
-
-import Test.LeanCheck
-import Test.LeanCheck.Utils
-
-import Conjure.Expr hiding (application)
-import Conjure.TypeBinding
-import Test.Speculate.Expr
-
-
--- |
--- Extrapolate can generalize counter-examples of any types that are
--- 'Arguable'.
---
--- 'Arguable' types must first be instances of
---
--- * 'Listable', so Extrapolate knows how to enumerate values;
--- * 'Express', so Extrapolate can represent then manipulate values;
--- * 'Name', so Extrapolate knows how to name variables.
---
--- There are no required functions, so we can define instances with:
---
--- > instance Arguable OurType
---
--- However, it is desirable to define both 'background' and 'subInstances'.
---
--- The following example shows a datatype and its instance:
---
--- > data Stack a = Stack a (Stack a) | Empty
---
--- > instance Arguable a => Arguable (Stack a) where
--- >   subInstances s  =  instances (argTy1of1 s)
---
--- To declare 'instances' it may be useful to use type binding
--- operators such as: 'argTy1of1', 'argTy1of2' and 'argTy2of2'.
---
--- Instances can be automatically derived using
--- 'Conjure.Arguable.Derive.deriveArguable'
--- which will also automatically derivate
--- 'Listable', 'Express' and 'Name' when needed.
-class (Listable a, Express a, Name a, Show a) => Arguable a where
-  -- | List of symbols allowed to appear in side-conditions.
-  --   Defaults to @[]@.  See 'value'.
-  background :: a -> [Expr]
-  background _  =  []
-
-  -- | Computes a list of reified subtype instances.
-  --   Defaults to 'id'.
-  --   See 'instances'.
-  subInstances :: a -> Instances -> Instances
-  subInstances _  =  id
-
-
-instance Arguable ()
-
-instance Arguable Bool where
-  background p  =  reifyEq p
-                ++ [ value "not" not 
-                   , value "&&" (&&)
-                   , value "||" (||)
-                   ]
-
-instance Arguable Int where
-  background x  =  reifyEqOrd x
-                ++ [ value "+" ((+) -:> x)
-                   , value "*" ((*) -:> x)
-                   , value "-" ((-) -:> x)
-                   , value "if" (\b x y -> if b then x else y :: Int)
-                   ]
-
-instance Arguable Integer where
-  background x  =  reifyEqOrd x
-
-instance Arguable Char where
-  background c  =  reifyEqOrd c
-
-instance Arguable a => Arguable (Maybe a) where
-  background mx  =  mkEq1  (maybeEq  ->:> mx)
-                 ++ mkOrd1 (maybeOrd ->:> mx)
-                 ++ [ value "Just" (Just ->: mx) ]
-  subInstances mx  =  instances (fromJust mx)
-
--- TODO: move maybeEq and maybeOrd here, I'll have to change the tests
-
-instance (Arguable a, Arguable b) => Arguable (Either a b) where
-  background exy  =  mkEq2  (eitherEq  ->>:> exy)
-                  ++ mkOrd2 (eitherOrd ->>:> exy)
-                  ++ [ value "Left"  (Left  ->: exy)
-                     , value "Right" (Right ->: exy) ]
-  subInstances exy  =  instances (fromLeft  exy)
-                    .  instances (fromRight exy)
-
--- TODO: move eitherEq and eitherOrd here, I'll have to change the tests
-
-instance (Arguable a, Arguable b) => Arguable (a,b) where
-  background xy  =  mkEq2  (pairEq  ->>:> xy)
-                 ++ mkOrd2 (pairOrd ->>:> xy)
-  subInstances xy  =  instances (fst xy)
-                   .  instances (snd xy)
-
-instance (Arguable a, Arguable b, Arguable c)
-      => Arguable (a,b,c) where
-  background xyz  =  mkEq3  (tripleEq  ->>>:> xyz)
-                  ++ mkOrd3 (tripleOrd ->>>:> xyz)
-  subInstances xyz  =  instances x . instances y . instances z
-                       where (x,y,z) = xyz
-
-instance (Arguable a, Arguable b, Arguable c, Arguable d)
-      => Arguable (a,b,c,d) where
-  background xyzw  =  mkEq4  (quadrupleEq  ->>>>:> xyzw)
-                   ++ mkOrd4 (quadrupleOrd ->>>>:> xyzw)
-  subInstances xyzw  =  instances x
-                     .  instances y
-                     .  instances z
-                     .  instances w
-                     where (x,y,z,w) = xyzw
-
-instance Arguable a => Arguable [a] where
-  background xs  =  mkEq1  (listEq  ->:> xs)
-                 ++ mkOrd1 (listOrd ->:> xs)
-                 ++ [ value "length" (length -:> xs) ]
-                 ++ [ value "elem"      (elemBy (*==*) ->:> xs) | hasEq $ head xs ]
-  subInstances xs  =  instances (head xs)
-
-instance Arguable Ordering where
-  background o  =  reifyEqOrd o
-
-mkEq1 :: (Arguable a, Arguable b)
-      => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
-mkEq1 m = takeWhile (\_ -> hasEq x) . mkEq $ m (*==*)
-  where
-  x = arg1 ==: m
-
-mkEq2 :: (Arguable a, Arguable b, Arguable c)
-      => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
-mkEq2 m = takeWhile (\_ -> hasEq x && hasEq y) . mkEq $ m (*==*) (*==*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-
-mkEq3 :: (Arguable a, Arguable b, Arguable c, Arguable d)
-      => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
-      -> [Expr]
-mkEq3 m = takeWhile (\_ -> hasEq x && hasEq y && hasEq z) . mkEq
-        $ m (*==*) (*==*) (*==*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-  z = arg3 ==: m
-
-mkEq4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e)
-      => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
-      -> [Expr]
-mkEq4 m = takeWhile (\_ -> hasEq x && hasEq y && hasEq z && hasEq w) . mkEq
-        $ m (*==*) (*==*) (*==*) (*==*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-  z = arg3 ==: m
-  w = arg4 ==: m
-
-mkOrd1 :: (Arguable a, Arguable b)
-       => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
-mkOrd1 m = takeWhile (\_ -> hasOrd x) . mkOrdLessEqual
-         $ m (*<=*)
-  where
-  x = arg1 ==: m
-
-mkOrd2 :: (Arguable a, Arguable b, Arguable c)
-       => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
-mkOrd2 m = takeWhile (\_ -> hasOrd x && hasOrd y) . mkOrdLessEqual
-         $ m (*<=*) (*<=*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-
-mkOrd3 :: (Arguable a, Arguable b, Arguable c, Arguable d)
-       => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
-       -> [Expr]
-mkOrd3 m = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z) . mkOrdLessEqual
-         $ m (*<=*) (*<=*) (*<=*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-  z = arg3 ==: m
-
-mkOrd4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e)
-       => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
-       -> [Expr]
-mkOrd4 m = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z && hasOrd w) . mkOrdLessEqual
-         $ m (*<=*) (*<=*) (*<=*) (*<=*)
-  where
-  x = arg1 ==: m
-  y = arg2 ==: m
-  z = arg3 ==: m
-  w = arg4 ==: m
-
--- | Usage: @ins "x" (undefined :: Type)@
-ins :: Arguable a => a -> Instances
-ins x = reifyListable x
-     ++ reifyName x
-     ++ reifyBackground x
-
--- | Used in the definition of 'subInstances'
---   in 'Arguable' typeclass instances.
-instances :: Arguable a => a -> Instances -> Instances
-instances x = this x (subInstances x)
-  where
-  this :: Arguable a
-       => a -> (Instances -> Instances) -> Instances -> Instances
-  this x f is =
-    if isListableT is (typeOf x)
-      then is
-      else f (ins x ++ is)
-  -- TODO: change type to a -> [Instances -> Instances] -> Instances -> Instances
-
-reifyBackground :: Arguable a => a -> Instances
-reifyBackground x = [value "background" (background x)]
-
-fromBackgroundOf :: (Arguable a, Typeable b) => String -> a -> Maybe b
-fromBackgroundOf nm = listToMaybe
-                    . mapMaybe evaluate
-                    . filter (`isConstantNamed` nm)
-                    . background
-
-hasEq :: Arguable a => a -> Bool
-hasEq x = isJust $ "==" `fromBackgroundOf` x -: mayb (x >- x >- bool)
-
-hasOrd :: Arguable a => a -> Bool
-hasOrd x = isJust $ "<=" `fromBackgroundOf` x -: mayb (x >- x >- bool)
-
-(*==*) :: Arguable a => a -> a -> Bool
-x *==* y = x == y
-  where
-  (==) = fromMaybe (error "(*==*): no (==) operator in background")
-       $ "==" `fromBackgroundOf` x
-
-(*/=*) :: Arguable a => a -> a -> Bool
-x */=* y = x /= y
-  where
-  (/=) = fromMaybe (error "(*/=*): no (/=) operator in background")
-       $ "/=" `fromBackgroundOf` x
-
-(*<=*) :: Arguable a => a -> a -> Bool
-x *<=* y = x <= y
-  where
-  (<=) = fromMaybe (error "(*<=*): no (<=) operator in background")
-       $ "<=" `fromBackgroundOf` x
-
-(*<*) :: Arguable a => a -> a -> Bool
-x *<* y = x < y
-  where
-  (<) = fromMaybe (error "(*<*): no (<) operator in background")
-       $ "<" `fromBackgroundOf` x
-
--- -- other Arguable instances -- --
-
-instance (Integral a, Arguable a) => Arguable (Ratio a)
-
-instance ( Arguable a, Arguable b, Arguable c, Arguable d
-         , Arguable e )
-      => Arguable (a,b,c,d,e) where
-  subInstances xyzwv = instances x . instances y . instances z
-                     . instances w . instances v
-                     where (x,y,z,w,v) = xyzwv
-
-instance ( Arguable a, Arguable b, Arguable c, Arguable d
-         , Arguable e, Arguable f )
-      => Arguable (a,b,c,d,e,f) where
-  subInstances xyzwvu = instances x . instances y . instances z
-                      . instances w . instances v . instances u
-               where (x,y,z,w,v,u) = xyzwvu
-
-instance ( Arguable a, Arguable b, Arguable c, Arguable d
-         , Arguable e, Arguable f, Arguable g )
-      => Arguable (a,b,c,d,e,f,g) where
-  subInstances xyzwvut = instances x . instances y . instances z . instances w
-                       . instances v . instances u . instances t
-                where (x,y,z,w,v,u,t) = xyzwvut
-
-#if __GLASGOW_HASKELL__ < 710
--- No 8-tuples for you:
--- On GHC 7.8, 8-tuples are not Typeable instances.  We could add a standalone
--- deriving clause, but that may cause trouble if some other library does the
--- same.  User should declare Generalizable 8-tuples manually when using GHC <=
--- 7.8.
-#else
-instance ( Arguable a, Arguable b, Arguable c, Arguable d
-         , Arguable e, Arguable f, Arguable g, Arguable h )
-      => Arguable (a,b,c,d,e,f,g,h) where
-  subInstances xyzwvuts = instances x . instances y . instances z . instances w
-                        . instances v . instances u . instances t . instances s
-    where (x,y,z,w,v,u,t,s) = xyzwvuts
-#endif
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -11,12 +11,17 @@
 --
 -- You are probably better off importing "Conjure".
 module Conjure.Conjurable
-  ( Conjurable
+  ( Reification1
+  , Reification
+  , Conjurable (..)
+  , conjureType
+  , reifyTiers
+  , reifyEquality
   , canonicalApplication
   , canonicalVarApplication
-  , unifiedArgumentTiers
-  , tiersFor
-  , mkExprTiers
+  , conjureIfs
+  , conjureTiersFor
+  , conjureMkEquation
   )
 where
 
@@ -24,43 +29,269 @@
 import Test.LeanCheck.Utils
 import Conjure.Expr hiding (application)
 import Test.Speculate.Expr
+import Data.Functor ((<$>))
+import Control.Applicative ((<*>))
 
+import Data.Int     -- for instances
+import Data.Word    -- for instances
+import Data.Ratio   -- for instance
+import Data.Complex -- for instance
+
+
+-- | Single reification of some functions over a type as 'Expr's.
+--
+-- A hole, an if function, an equality function and tiers.
+type Reification1  =  (Expr, Expr, Maybe Expr, Maybe [[Expr]])
+
+-- | A reification over a collection of types.
+--
+-- Represented as a transformation of a list to a list.
+type Reification  =  [Reification1] -> [Reification1]
+
+
+-- | Class of 'Conjurable' types.
+-- Functions are 'Conjurable'
+-- if all their arguments are 'Conjurable', 'Listable' and 'Show'able.
+--
+-- For atomic types that are 'Listable',
+-- instances are defined as:
+--
+-- > instance Conjurable Atomic where
+-- >   conjureTiers  =  reifyTiers
+--
+-- For atomic types that are both 'Listable' and 'Eq',
+-- instances are defined as:
+--
+-- > instance Conjurable Atomic where
+-- >   conjureTiers     =  reifyTiers
+-- >   conjureEquality  =  reifyEquality
+--
+-- For types with subtypes,
+-- instances are defined as:
+--
+-- > instance Conjurable Composite where
+-- >   conjureTiers     =  reifyTiers
+-- >   conjureEquality  =  reifyEquality
+-- >   conjureSubTypes x  =  conjureType y
+-- >                      .  conjureType z
+-- >                      .  conjureType w
+-- >     where
+-- >     (Composite ... y ... z ... w ...)  =  x
+--
+-- Above @x@, @y@, @z@ and @w@ are just proxies.
+-- The @Proxy@ type was avoided for backwards compatibility.
+--
+-- Please see the source code of "Conjure.Conjurable" for more examples.
+--
+-- (cf. 'reifyTiers', 'reifyEquality', 'conjureType')
 class Typeable a => Conjurable a where
-  argumentHoles :: a -> [Expr]
-  argumentHoles _  =  []
-  argumentTiers :: a -> [ [[Expr]] ]
-  argumentTiers _  =  []
+  conjureArgumentHoles :: a -> [Expr]
+  conjureArgumentHoles _  =  []
 
-instance Conjurable ()
-instance Conjurable Int
-instance Conjurable Integer
-instance Conjurable Bool
-instance Typeable a => Conjurable [a]
-instance (Typeable a, Typeable b) => Conjurable (a,b)
-instance Typeable a => Conjurable (Maybe a)
-instance (Typeable a, Typeable b) => Conjurable (Either a b)
+  -- | Returns 'Just' the '==' function encoded as an 'Expr' when available
+  --   or 'Nothing' otherwise.
+  conjureEquality :: a -> Maybe Expr
+  conjureEquality _  =  Nothing
 
-instance Conjurable Float
-instance Conjurable Double
-instance Conjurable Ordering
+  -- | Returns 'Just' 'tiers' of values encoded as 'Expr's when possible
+  --   or 'Nothing' otherwise.
+  conjureTiers :: a -> Maybe [[Expr]]
+  conjureTiers _  =  Nothing
 
-instance (Typeable a, Typeable b, Typeable c) => Conjurable (a,b,c)
-instance (Typeable a, Typeable b, Typeable c, Typeable d) => Conjurable (a,b,c,d)
-instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => Conjurable (a,b,c,d,e)
-instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => Conjurable (a,b,c,d,e,f)
+  conjureSubTypes :: a -> Reification
+  conjureSubTypes _  =  id
 
-instance (Listable a, Name a, Show a, Typeable a, Conjurable b) => Conjurable (a -> b) where
-  argumentHoles f  =  hole (arg1 f) : argumentHoles (f undefined)
-  argumentTiers f  =  mkExprTiers (arg1 f) : argumentTiers (f undefined)
 
-arg1 :: (a -> b) -> a
-arg1 _  =  undefined
+conjureType :: Conjurable a => a -> Reification
+conjureType x ms  =
+  if hole x `elem` [h | (h,_,_,_) <- ms]
+  then ms
+  else conjureSubTypes x $ conjureReification1 x : ms
 
+conjureReification1 :: Conjurable a => a -> Reification1
+conjureReification1 x  =  (hole x, ifFor x, conjureEquality x, conjureTiers x)
+
+conjureReification :: Conjurable a => a -> [Reification1]
+conjureReification x  =  conjureType 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.
+--
+-- This is to be used
+-- in the definition of 'conjureEquality'
+-- of 'Conjurable' typeclass instances:
+--
+-- > instance ... => Conjurable <Type> where
+-- >   ...
+-- >   conjureEquality  =  reifyEquality
+-- >   ...
+reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr
+reifyEquality  =  Just . head . reifyEq
+
+-- | Reifies equality to be used in a conjurable type.
+--
+-- This is to be used
+-- in the definition of 'conjureTiers'
+-- of 'Conjurable' typeclass instances:
+--
+-- > instance ... => Conjurable <Type> where
+-- >   ...
+-- >   conjureTiers  =  reifyTiers
+-- >   ...
+reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]]
+reifyTiers  =  Just . mkExprTiers
+
+mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]]
+mkExprTiers a  =  mapT val (tiers -: [[a]])
+
+conjureIfs :: Conjurable f => f -> [Expr]
+conjureIfs f  =  [eef | (_,eef,_,Just _) <- conjureReification f]
+
+conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr
+conjureMkEquation f  =  mkEquation [eq | (_,_,Just eq,_) <- conjureReification f]
+
+conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]]
+conjureTiersFor f e  =  tf allTiers
+  where
+  allTiers :: [ [[Expr]] ]
+  allTiers  =  [etiers | (_,_,_,Just etiers) <- conjureReification f]
+  tf []  =  [[e]] -- no tiers found, keep variable
+  tf (etiers:etc)  =  case etiers of
+                      ((e':_):_) | typ e' == typ e -> etiers
+                      _                            -> tf etc
+
+
+instance Conjurable () where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Bool where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Int where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Integer where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Char where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+-- bind equality to the given argument type
+(==:) :: (a -> a -> Bool) -> a -> (a -> a -> Bool)
+(==:)  =  const
+
+instance (Conjurable a, Listable a, Show a) => Conjurable [a] where
+  conjureSubTypes xs  =  conjureType (head xs)
+  conjureTiers     =  reifyTiers
+  conjureEquality xs  =  from <$> conjureEquality x
+    where
+    x  =  head xs
+    from e  =  value "==" (==)
+      where
+      (.==.)  =  evl e ==: x
+      []     == []     = True
+      (x:xs) == []     = False
+      []     == (y:ys) = False
+      (x:xs) == (y:ys) = x .==. y && xs == ys
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         ) => Conjurable (a,b) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xy  =  conjureType (fst xy)
+                      .  conjureType (snd xy)
+  conjureEquality xy  =  from <$> conjureEquality x <*> conjureEquality y
+    where
+    (x,y)  =  xy
+    from e1 e2  =  value "==" (==)
+      where
+      (==.)  =  evl e1 ==: x
+      (.==)  =  evl e2 ==: y
+      (x1,y1) == (x2,y2)  =  x1 ==. x2 && y1 .== y2
+
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         , Conjurable c, Listable c, Show c
+         ) => Conjurable (a,b,c) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xyz =  conjureType x
+                      .  conjureType y
+                      .  conjureType z
+                      where (x,y,z) = xyz
+  conjureEquality xyz  =  from
+                      <$> conjureEquality x
+                      <*> conjureEquality y
+                      <*> conjureEquality z
+    where
+    (x,y,z)  =  xyz
+    from e1 e2 e3  =  value "==" (==)
+      where
+      (==..)  =  evl e1 ==: x
+      (.==.)  =  evl e2 ==: y
+      (..==)  =  evl e3 ==: z
+      (x1,y1,z1) == (x2,y2,z2)  =  x1 ==.. x2
+                                && y1 .==. y2
+                                && z1 ..== z2
+
+instance (Conjurable a, Listable a, Show a) => Conjurable (Maybe a) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes mx  =  conjureType (fromJust mx)
+  conjureEquality mx  =  from <$> conjureEquality x
+    where
+    x  =  fromJust mx
+    from e  =  value "==" (==)
+      where
+      (.==.)  =  evl e ==: x
+      Nothing  == Nothing   =  True
+      Nothing  == (Just _)  =  False
+      (Just _) == Nothing   =  False
+      (Just x) == (Just y)  =  x .==. y
+
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         ) => Conjurable (Either a b) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes elr  =  conjureType l . conjureType r
+    where
+    Left l   =  elr
+    Right r  =  elr
+  conjureEquality elr  =  from <$> conjureEquality l <*> conjureEquality r
+    where
+    Left l   =  elr
+    Right r  =  elr
+    from el er  =  value "==" (==)
+      where
+      (==.)  =  evl el ==: l
+      (.==)  =  evl er ==: r
+      (Left x)  == (Left y)   =  x ==. y
+      (Left _)  == (Right _)  =  False
+      (Right _) == (Left _)   =  False
+      (Right x) == (Right y)  =  x .== y
+
+instance (Listable a, Show a, Conjurable a, Conjurable b) => Conjurable (a -> b) where
+  conjureArgumentHoles f  =  hole (argTy f) : conjureArgumentHoles (f undefined)
+  conjureSubTypes f  =   conjureType (argTy f) . conjureType (resTy f)
+
+argTy :: (a -> b) -> a
+argTy _  =  undefined
+
+resTy :: (a -> b) -> b
+resTy _  =  undefined
+
 canonicalArgumentVariables :: Conjurable f => f -> [Expr]
 canonicalArgumentVariables  =  unfoldApp
                             .  mostGeneralCanonicalVariation
                             .  foldApp
-                            .  argumentHoles
+                            .  conjureArgumentHoles
 
 canonicalApplication :: Conjurable f => String -> f -> Expr
 canonicalApplication nm f  =  foldApp (value nm f : canonicalArgumentVariables f)
@@ -68,33 +299,215 @@
 canonicalVarApplication :: Conjurable f => String -> f -> Expr
 canonicalVarApplication nm f  =  foldApp (var nm f : canonicalArgumentVariables f)
 
-unifiedArgumentTiers :: Conjurable f => f -> [[Expr]]
-unifiedArgumentTiers  =  foldr (\/) [] . nubArgumentTiers
 
-nubArgumentTiers :: Conjurable f => f -> [[ [Expr] ]]
-nubArgumentTiers  =  nubOn tierepr . argumentTiers
-  where
-  nubOn f  =  nubBy ((==) `on` f)
-  -- NOTE: this is O(n*n),
-  -- not much of a problem the number of arguments will hardly pass 6.
 
-mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]]
-mkExprTiers a  =  mapT val (tiers -: [[a]])
+-- -- -- other Conjurable instances -- -- --
 
-tiersFor :: Conjurable f => f -> Expr -> [[Expr]]
-tiersFor f e  =  tf (mkExprTiers (undefined :: Bool) : argumentTiers f)
-  where
-  tf []  =  [[e]] -- no tiers found, keep variable
-  tf (etiers:etc)  =  case etiers of
-                      ((e':_):_) | typ e' == typ e -> etiers
-                      _                            -> tf etc
+instance Conjurable Ordering where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
 
--- | tries to extract a representative from the first 6 tiers
-tierepr :: [[Expr]] -> Maybe Expr
-tierepr ((e:_):_)                 =  Just e
-tierepr ([]:(e:_):_)              =  Just e
-tierepr ([]:[]:(e:_):_)           =  Just e
-tierepr ([]:[]:[]:(e:_):_)        =  Just e
-tierepr ([]:[]:[]:[]:(e:_):_)     =  Just e
-tierepr ([]:[]:[]:[]:[]:(e:_):_)  =  Just e
-tierepr _                         =  Nothing
+instance Conjurable Float where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Double where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Int8 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Int16 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Int32 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Int64 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Word where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Word8 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Word16 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Word32 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance Conjurable Word64 where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+
+instance (Integral a, Conjurable a, Listable a, Show a, Eq a) => Conjurable (Ratio a) where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+  conjureSubTypes q  =  conjureType (numerator q)
+
+instance (RealFloat a, Conjurable a, Listable a, Show a, Eq a) => Conjurable (Complex a) where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+  conjureSubTypes x  =  conjureType (realPart x)
+
+
+-- Conjurable tuples --
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         , Conjurable c, Listable c, Show c
+         , Conjurable d, Listable d, Show d
+         ) => Conjurable (a,b,c,d) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xyzw =  conjureType x
+                       .  conjureType y
+                       .  conjureType z
+                       .  conjureType w
+                       where (x,y,z,w) = xyzw
+  conjureEquality xyzw  =  from
+                       <$> conjureEquality x
+                       <*> conjureEquality y
+                       <*> conjureEquality z
+                       <*> conjureEquality w
+    where
+    (x,y,z,w)  =  xyzw
+    from e1 e2 e3 e4  =  value "==" (==)
+      where
+      (==...)  =  evl e1 ==: x
+      (.==..)  =  evl e2 ==: y
+      (..==.)  =  evl e3 ==: z
+      (...==)  =  evl e4 ==: w
+      (x1,y1,z1,w1) == (x2,y2,z2,w2)  =  x1 ==... x2
+                                      && y1 .==.. y2
+                                      && z1 ..==. z2
+                                      && w1 ...== w2
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         , Conjurable c, Listable c, Show c
+         , Conjurable d, Listable d, Show d
+         , Conjurable e, Listable e, Show e
+         ) => Conjurable (a,b,c,d,e) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xyzwv =  conjureType x
+                        .  conjureType y
+                        .  conjureType z
+                        .  conjureType w
+                        .  conjureType v
+                        where (x,y,z,w,v) = xyzwv
+  conjureEquality xyzwv  =  from
+                        <$> conjureEquality x
+                        <*> conjureEquality y
+                        <*> conjureEquality z
+                        <*> conjureEquality w
+                        <*> conjureEquality v
+    where
+    (x,y,z,w,v)  =  xyzwv
+    from e1 e2 e3 e4 e5  =  value "==" (==)
+      where
+      (==....)  =  evl e1 ==: x
+      (.==...)  =  evl e2 ==: y
+      (..==..)  =  evl e3 ==: z
+      (...==.)  =  evl e4 ==: w
+      (....==)  =  evl e5 ==: v
+      (x1,y1,z1,w1,v1) == (x2,y2,z2,w2,v2)  =  x1 ==.... x2
+                                            && y1 .==... y2
+                                            && z1 ..==.. z2
+                                            && w1 ...==. w2
+                                            && v1 ....== v2
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         , Conjurable c, Listable c, Show c
+         , Conjurable d, Listable d, Show d
+         , Conjurable e, Listable e, Show e
+         , Conjurable f, Listable f, Show f
+         ) => Conjurable (a,b,c,d,e,f) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xyzwvu =  conjureType x
+                         .  conjureType y
+                         .  conjureType z
+                         .  conjureType w
+                         .  conjureType v
+                         .  conjureType u
+                         where (x,y,z,w,v,u) = xyzwvu
+  conjureEquality xyzwvu  =  from
+                         <$> conjureEquality x
+                         <*> conjureEquality y
+                         <*> conjureEquality z
+                         <*> conjureEquality w
+                         <*> conjureEquality v
+                         <*> conjureEquality u
+    where
+    (x,y,z,w,v,u)  =  xyzwvu
+    from e1 e2 e3 e4 e5 e6  =  value "==" (==)
+      where
+      (==.....)  =  evl e1 ==: x
+      (.==....)  =  evl e2 ==: y
+      (..==...)  =  evl e3 ==: z
+      (...==..)  =  evl e4 ==: w
+      (....==.)  =  evl e5 ==: v
+      (.....==)  =  evl e6 ==: u
+      (x1,y1,z1,w1,v1,u1) == (x2,y2,z2,w2,v2,u2)  =  x1 ==..... x2
+                                                  && y1 .==.... y2
+                                                  && z1 ..==... z2
+                                                  && w1 ...==.. w2
+                                                  && v1 ....==. v2
+                                                  && u1 .....== u2
+
+instance ( Conjurable a, Listable a, Show a
+         , Conjurable b, Listable b, Show b
+         , Conjurable c, Listable c, Show c
+         , Conjurable d, Listable d, Show d
+         , Conjurable e, Listable e, Show e
+         , Conjurable f, Listable f, Show f
+         , Conjurable g, Listable g, Show g
+         ) => Conjurable (a,b,c,d,e,f,g) where
+  conjureTiers     =  reifyTiers
+  conjureSubTypes xyzwvut =  conjureType x
+                          .  conjureType y
+                          .  conjureType z
+                          .  conjureType w
+                          .  conjureType v
+                          .  conjureType u
+                          .  conjureType t
+                         where (x,y,z,w,v,u,t) = xyzwvut
+  conjureEquality xyzwvut  =  from
+                          <$> conjureEquality x
+                          <*> conjureEquality y
+                          <*> conjureEquality z
+                          <*> conjureEquality w
+                          <*> conjureEquality v
+                          <*> conjureEquality u
+                          <*> conjureEquality t
+    where
+    (x,y,z,w,v,u,t)  =  xyzwvut
+    from e1 e2 e3 e4 e5 e6 e7  =  value "==" (==)
+      where
+      (==......)  =  evl e1 ==: x
+      (.==.....)  =  evl e2 ==: y
+      (..==....)  =  evl e3 ==: z
+      (...==...)  =  evl e4 ==: w
+      (....==..)  =  evl e5 ==: v
+      (.....==.)  =  evl e6 ==: u
+      (......==)  =  evl e7 ==: t
+      (x1,y1,z1,w1,v1,u1,t1) == (x2,y2,z2,w2,v2,u2,t2)  =  x1 ==...... x2
+                                                        && y1 .==..... y2
+                                                        && z1 ..==.... z2
+                                                        && w1 ...==... w2
+                                                        && v1 ....==.. v2
+                                                        && u1 .....==. u2
+                                                        && t1 ......== t2
+
+-- TODO: go up to 12-tuples
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -18,10 +18,10 @@
   , args
   , conjure
   , conjureWith
+  , conjureWithMaxSize
   , conjpure
   , conjpureWith
   , candidateExprs
-  , ifFor
   )
 where
 
@@ -41,24 +41,27 @@
 -- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.
 --   See 'args' for the defaults.
 data Args = Args
-  { maxTests         :: Int  -- ^ defaults to 60
-  , maxSize          :: Int  -- ^ defaults to 9, keep greater than maxEquationSize
-  , maxEquationSize  :: Int  -- ^ defaults to 5, keep smaller than maxSize
-  , maxRecursionSize :: Int  -- ^ defaults to 60
+  { maxTests          :: Int  -- ^ defaults to 60
+  , maxSize           :: Int  -- ^ defaults to 9, keep greater than maxEquationSize
+  , maxRecursiveCalls :: Int  -- ^ defaults to 1
+  , maxEquationSize   :: Int  -- ^ defaults to 5, keep smaller than maxSize
+  , maxRecursionSize  :: Int  -- ^ defaults to 60
   }
 
 -- | Default arguments to conjure.
 --
 -- * 60 tests
 -- * functions of up to 9 symbols
+-- * maximum of 1 recursive call
 -- * pruning with equations up to size 5
 -- * recursion up to 60 symbols.
 args :: Args
 args = Args
-  { maxTests          =  60
-  , maxSize           =   9
-  , maxEquationSize   =   5
-  , maxRecursionSize  =  60
+  { maxTests           =  60
+  , maxSize            =   9
+  , maxRecursiveCalls  =   1
+  , maxEquationSize    =   5
+  , maxRecursionSize   =  60
   }
 
 -- | Like 'conjure' but in the pure world.
@@ -88,7 +91,7 @@
   candidates  =  filter (\e -> typ e == typ ffxx)
               .  concat
               .  take maxSize
-              $  candidateExprs nm f maxEquationSize (===) [es]
+              $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) [es ++ conjureIfs f]
   ffxx   =  canonicalApplication nm f
   vffxx  =  canonicalVarApplication nm f
   rrff   =  var nm f
@@ -98,17 +101,14 @@
   e1 ?=? e2  =  isTrueWhenDefined (e1 -==- e2)
 
   e1 .=. e2  =  countTrue         (e1 -==- e2)
-  (-==-)  =  mkEquation  eqs
-    where
-    eqs  =  value "==" ((==) :: Bool -> Bool -> Bool)
-         :  es
+  (-==-)  =  conjureMkEquation f
 
   isTrueWhenDefined  =  all (errorToTrue  . eval False) . gs
   isReallyTrue       =  all (errorToFalse . eval False) . gs
   countTrue        =  count (errorToFalse . eval False) . gs
 
   gs :: Expr -> [Expr]
-  gs  =  take maxTests . grounds (tiersFor f)
+  gs  =  take maxTests . grounds (conjureTiersFor f)
 
 -- | Conjures an implementation of a partially defined function.
 --
@@ -129,7 +129,6 @@
 -- >   , val (1::Int)
 -- >   , value "+" ((+) :: Int -> Int -> Int)
 -- >   , value "*" ((*) :: Int -> Int -> Int)
--- >   , value "==" ((==) :: Int -> Int -> Bool)
 -- > ]
 --
 -- The conjure function does the following:
@@ -139,11 +138,20 @@
 -- > -- looking through 815 candidates, 100% match, 3/3 assignments
 -- > square x  =  x * x
 --
--- The background is defined with 'val', 'value' and 'ifFor'.
+-- The background is defined with 'val' and 'value'.
 conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
 conjure  =  conjureWith args
 
--- | Like 'conjure' but allows setting options through 'Args' and 'args'.
+-- | Like 'conjure' but allows setting the maximum size of considered expressions
+--   instead of the default value of 9.
+--
+-- > conjureWithMaxSize 10 "function" function [...]
+conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()
+conjureWithMaxSize sz  =  conjureWith args{maxSize = sz}
+
+-- | Like 'conjure' but allows setting options through 'Args'/'args'.
+--
+-- > conjureWith args{maxSize = 11} "function" function [...]
 conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
 conjureWith args nm f es  =  do
   print (var nm f)
@@ -163,14 +171,15 @@
 candidateExprs :: Conjurable f
                => String -> f
                -> Int
+               -> Int
                -> (Expr -> Expr -> Bool)
                -> [[Expr]]
                -> [[Expr]]
-candidateExprs nm f sz (===) ess  =  expressionsT $ [ef:exs] \/ ess
+candidateExprs nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess
   where
   (ef:exs)  =  unfoldApp $ canonicalVarApplication nm f
   thy  =  theoryFromAtoms (===) sz $ [nub (b_:map holeAsTypeOf exs)] \/ ess
-  expressionsT ds  =  filterT (\e -> count (== ef) (vars e) <= 1)
+  expressionsT ds  =  filterT (\e -> count (== ef) (vars e) <= mc)
                    $  filterT (isRootNormalE thy)
                    $  ds \/ (delay $ productMaybeWith ($$) es es)
     where
diff --git a/src/Conjure/TypeBinding.hs b/src/Conjure/TypeBinding.hs
deleted file mode 100644
--- a/src/Conjure/TypeBinding.hs
+++ /dev/null
@@ -1,120 +0,0 @@
--- |
--- Module      : Conjure.TypeBinding
--- Copyright   : (c) 2017-2021 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- Some type binding operators that are useful when defining 'Conjurable'
--- instances.
-module Conjure.TypeBinding
-  ( arg1
-  , arg2
-  , arg3
-  , arg4
-  , arg5
-  , arg6
-  , (==:)
-  , argTy1of1
-  , argTy1of2, argTy2of2
-  , argTy1of3, argTy2of3, argTy3of3
-  , argTy1of4, argTy2of4, argTy3of4, argTy4of4
-  , argTy1of5, argTy2of5, argTy3of5, argTy4of5, argTy5of5
-  , argTy1of6, argTy2of6, argTy3of6, argTy4of6, argTy5of6, argTy6of6
-  , module Test.LeanCheck.Utils.TypeBinding
-  )
-where
-
-import Test.LeanCheck.Utils.TypeBinding
-
--- TODO: reexport LeanCheck's typebinding operators
--- TODO: or maybe re-export Express's typebinding operators?
-
-arg1 :: (a -> b) -> a
-arg1 _  =  undefined
-
-arg2 :: (a -> b -> c) -> b
-arg2 _  =  undefined
-
-arg3 :: (a -> b -> c -> d) -> c
-arg3 _  =  undefined
-
-arg4 :: (a -> b -> c -> d -> e) -> d
-arg4 _  =  undefined
-
-arg5 :: (a -> b -> c -> d -> e -> f) -> e
-arg5 _  =  undefined
-
-arg6 :: (a -> b -> c -> d -> e -> f -> g) -> f
-arg6 _  =  undefined
-
-(==:) :: (a -> (b -> c -> d)) -> a -> b
-x ==: y  =  undefined
-
-
-argTy1of1 :: con a -> a
-argTy1of1 _ = undefined
-
-
-argTy1of2 :: con a b -> a
-argTy1of2 _ = undefined
-
-argTy2of2 :: con a b -> b
-argTy2of2 _ = undefined
-
-
-argTy1of3 :: con a b c -> a
-argTy1of3 _ = undefined
-
-argTy2of3 :: con a b c -> b
-argTy2of3 _ = undefined
-
-argTy3of3 :: con a b c -> c
-argTy3of3 _ = undefined
-
-
-argTy1of4 :: con a b c d -> a
-argTy1of4 _ = undefined
-
-argTy2of4 :: con a b c d -> b
-argTy2of4 _ = undefined
-
-argTy3of4 :: con a b c d -> c
-argTy3of4 _ = undefined
-
-argTy4of4 :: con a b c d -> d
-argTy4of4 _ = undefined
-
-
-argTy1of5 :: con a b c d e -> a
-argTy1of5 _ = undefined
-
-argTy2of5 :: con a b c d e -> b
-argTy2of5 _ = undefined
-
-argTy3of5 :: con a b c d e -> c
-argTy3of5 _ = undefined
-
-argTy4of5 :: con a b c d e -> d
-argTy4of5 _ = undefined
-
-argTy5of5 :: con a b c d e -> e
-argTy5of5 _ = undefined
-
-
-argTy1of6 :: con a b c d e f -> a
-argTy1of6 _ = undefined
-
-argTy2of6 :: con a b c d e f -> b
-argTy2of6 _ = undefined
-
-argTy3of6 :: con a b c d e f -> c
-argTy3of6 _ = undefined
-
-argTy4of6 :: con a b c d e f -> d
-argTy4of6 _ = undefined
-
-argTy5of6 :: con a b c d e f -> e
-argTy5of6 _ = undefined
-
-argTy6of6 :: con a b c d e f -> f
-argTy6of6 _ = undefined
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -17,22 +17,6 @@
   , module Data.Typeable
 
   , count
-
-  , fromLeft
-  , fromRight
-  , elemBy
-  , listEq
-  , listOrd
-  , maybeEq
-  , maybeOrd
-  , eitherEq
-  , eitherOrd
-  , pairEq
-  , pairOrd
-  , tripleEq
-  , tripleOrd
-  , quadrupleEq
-  , quadrupleOrd
   )
 where
 
@@ -45,95 +29,3 @@
 
 count :: (a -> Bool) -> [a] -> Int
 count p  =  length . filter p
-
-mapHead :: (a -> a) -> [a] -> [a]
-mapHead f (x:xs)  =  f x : xs
-mapHead _ []  =  error "Conjure.Utils.mapHead: empty list"
-
--- note these versions of fromLeft and fromRight differ from the ones of
--- Data.Either since 4.10.0.0.
-fromLeft :: Either a b -> a
-fromLeft (Left x) = x
-fromLeft _        = error "fromLeft: not a left"
-
-fromRight :: Either a b -> b
-fromRight (Right x) = x
-fromRight _         = error "fromRight: not a right"
-
-elemBy :: (a -> a -> Bool) -> a -> [a] -> Bool
-elemBy (==) x = any (== x)
-
-listEq :: (a -> a -> Bool) -> [a] -> [a] -> Bool
-listEq (==) []     []     = True
-listEq (==) (x:xs) []     = False
-listEq (==) []     (y:ys) = False
-listEq (==) (x:xs) (y:ys) = x == y && listEq (==) xs ys
-
-listOrd :: (a -> a -> Bool) -> [a] -> [a] -> Bool
-listOrd (<=) []     []     = True
-listOrd (<=) (x:xs) []     = False
-listOrd (<=) []     (y:ys) = True
-listOrd (<=) (x:xs) (y:ys) = x <  y
-                          || x == y && listOrd (<=) xs ys
-  where
-  x <  y = x <= y && not (y <= x)
-  x == y = x <= y &&      y <= x
-
-maybeEq :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
-maybeEq (==) Nothing  Nothing  = True
-maybeEq (==) Nothing  (Just y) = False
-maybeEq (==) (Just x) Nothing  = False
-maybeEq (==) (Just x) (Just y) = x == y
-
-maybeOrd :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
-maybeOrd (<=) Nothing  Nothing  = True
-maybeOrd (<=) Nothing  (Just y) = True
-maybeOrd (<=) (Just x) Nothing  = False
-maybeOrd (<=) (Just x) (Just y) = x <= y
-
-eitherEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
-eitherEq (==) _ (Left  x) (Left  y) = x == y
-eitherEq _ (==) (Right x) (Right y) = x == y
-eitherEq _ _ _ _ = False
-
-eitherOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
-eitherOrd (<=) _ (Left  x) (Left  y) = x <= y
-eitherOrd _ (<=) (Right x) (Right y) = x <= y
-eitherOrd _    _ (Left  _) (Right _) = True
-eitherOrd _    _ (Right _) (Left  _) = False
-
-pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool
-pairEq (==.) (.==) (x1,y1) (x2,y2) = x1 ==. x2 && y1 .== y2
-
-pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool
-pairOrd (<=.) (.<=) (x1,y1) (x2,y2) = x1 <. x2
-                                   || x1 ==. x2 && y1 .<= y2
-  where
-  x <.  y = x <=. y && not (y <=. x)
-  x ==. y = x <=. y &&      y <=. x
-
-tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)
-         -> (a,b,c) -> (a,b,c) -> Bool
-tripleEq (==..) (.==.) (..==) (x1,y1,z1) (x2,y2,z2) =
-  x1 ==.. x2 && y1 .==. y2 && z1 ..== z2
-
-tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)
-          -> (a,b,c) -> (a,b,c) -> Bool
-tripleOrd (<=..) (.<=.) (..<=) (x1,y1,z1) (x2,y2,z2) =
-  x1 <.. x2 || x1 ==.. x2 && pairOrd (.<=.) (..<=) (y1,z1) (y2,z2)
-  where
-  x <..  y = x <=.. y && not (y <=.. x)
-  x ==.. y = x <=.. y &&      y <=.. x
-
-quadrupleEq :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)
-            -> (a,b,c,d) -> (a,b,c,d) -> Bool
-quadrupleEq (==...) (.==..) (..==.) (...==) (x1,y1,z1,w1) (x2,y2,z2,w2) =
-  x1 ==... x2 && y1 .==.. y2 && z1 ..==. z2 && w1 ...== w2
-
-quadrupleOrd :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)
-             -> (a,b,c,d) -> (a,b,c,d) -> Bool
-quadrupleOrd (<=...) (.<=..) (..<=.) (...<=) (x1,y1,z1,w1) (x2,y2,z2,w2) =
-  x1 <... x2 || x1 ==... x2 && tripleOrd (.<=..) (..<=.) (...<=) (y1,z1,w1) (y2,z2,w2)
-  where
-  x <...  y = x <=... y && not (y <=... x)
-  x ==... y = x <=... y &&      y <=... x
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -3,7 +3,7 @@
 # Copyright (C) 2021 Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
-resolver: lts-15.6 # or ghc-8.8.3
+resolver: lts-17.9 # or ghc-8.10.4
 
 packages:
 - .
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -9,6 +9,8 @@
 module Test
   ( module Conjure
   , module Conjure.Expr
+  , module Conjure.Conjurable
+  , module Test.LeanCheck
 
   , mainTest
   )
@@ -17,8 +19,11 @@
 import System.Exit (exitFailure)
 import System.Environment (getArgs)
 
+import Test.LeanCheck
+
 import Conjure
 import Conjure.Expr hiding (delete, insert)
+import Conjure.Conjurable
 
 reportTests :: [Bool] -> IO ()
 reportTests tests =
diff --git a/test/conjurable.hs b/test/conjurable.hs
new file mode 100644
--- /dev/null
+++ b/test/conjurable.hs
@@ -0,0 +1,112 @@
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+
+{-# Language DeriveDataTypeable, StandaloneDeriving #-}  -- for GHC < 7.10
+
+import Test
+
+-- An Unit type that is not an Eq instance
+data Unit  =  Unit  deriving Show
+
+deriving instance Typeable Unit  -- for GHC < 7.10
+
+instance Listable Unit where list = [Unit]
+instance Conjurable Unit where
+  conjureTiers = reifyTiers
+
+main :: IO ()
+main  =  mainTest tests 5040
+
+tests :: Int -> [Bool]
+tests n  =
+  [ True
+
+  , holds n $ \x y -> (x <==> y)  ==  (x == (y :: ()))
+  , holds n $ \x y -> (x <==> y)  ==  (x == (y :: Int))
+  , holds n $ \p q -> (p <==> q)  ==  (p == (q :: Bool))
+  , conjureEquality Unit == Nothing
+
+  , holds n $ \xs ys -> (xs <==> ys)  ==  (xs == (ys :: [Int]))
+  , holds n $ \s1 s2 -> (s1 <==> s2)  ==  (s1 == (s2 :: String))
+  , conjureEquality [Unit] == Nothing
+
+  , holds n $ \xy zw -> (xy <==> zw)  ==  (xy == (zw :: (Int,Int)))
+  , holds n $ \xy zw -> (xy <==> zw)  ==  (xy == (zw :: (Bool,Integer)))
+  , holds n $ \xy zw -> (xy <==> zw)  ==  (xy == (zw :: (String,[Int])))
+  , conjureEquality (undefined :: (Int,Unit)) == Nothing
+  , conjureEquality (undefined :: (Unit,Int)) == Nothing
+
+  , holds n $ \xyz wvu -> (xyz <==> wvu)  ==  (xyz == (wvu :: (Int,Int,Int)))
+  , holds n $ \xyz wvu -> (xyz <==> wvu)  ==  (xyz == (wvu :: (Bool,Bool,Bool)))
+  , holds n $ \xyz wvu -> (xyz <==> wvu)  ==  (xyz == (wvu :: (Int,Bool,())))
+  , holds n $ \xyz wvu -> (xyz <==> wvu)  ==  (xyz == (wvu :: (Bool,String,[Integer])))
+  , isNothing $ conjureEquality (undefined :: (Unit,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Unit,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit))
+
+  , holds n $ \mx my -> (mx <==> my)  ==  (mx == (my :: Maybe ()))
+  , holds n $ \mx my -> (mx <==> my)  ==  (mx == (my :: Maybe Bool))
+  , holds n $ \mx my -> (mx <==> my)  ==  (mx == (my :: Maybe Int))
+  , holds n $ \mx my -> (mx <==> my)  ==  (mx == (my :: Maybe [Maybe Int]))
+  , isNothing $ conjureEquality (undefined :: Maybe Unit)
+
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either () ()))
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either Bool Bool))
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either Int Int))
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either Int Bool))
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either Bool Int))
+  , holds n $ \ex ey -> (ex <==> ey)  ==  (ex == (ey :: Either [Int] String))
+  , isNothing $ conjureEquality (undefined :: Either Unit Bool)
+  , isNothing $ conjureEquality (undefined :: Either Bool Unit)
+  , isNothing $ conjureEquality (undefined :: Either Unit Unit)
+
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Int,Int,Int)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,Bool,Bool,Bool)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Bool,(),Char)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,String,[Integer],Bool)))
+  , isNothing $ conjureEquality (undefined :: (Unit,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Unit,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit,Unit))
+
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Int,Int,Int,Int)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,Bool,Bool,Bool,Bool)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Bool,(),Char,String)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,String,[Integer],Bool,String)))
+  , isNothing $ conjureEquality (undefined :: (Unit,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Unit,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Unit,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Unit))
+
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Int,Int,Int,Int,Int)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,Bool,Bool,Bool,Bool,Bool)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Bool,(),Char,String,Bool)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,String,[Integer],Bool,String,Int)))
+  , isNothing $ conjureEquality (undefined :: (Unit,Bool,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Unit,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Unit,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Unit,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Bool,Unit))
+
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Int,Int,Int,Int,Int,Int)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,Bool,Bool,Bool,Bool,Bool,Bool)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Int,Bool,(),Char,String,Bool,Int)))
+  , holds n $ \t1 t2 -> (t1 <==> t2)  ==  (t1 == (t2 :: (Bool,String,[Integer],Bool,String,Int,[Integer])))
+  , isNothing $ conjureEquality (undefined :: (Unit,Bool,Bool,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Unit,Bool,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Unit,Bool,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Unit,Bool,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Unit,Bool,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Bool,Unit,Bool))
+  , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Bool,Bool,Unit))
+  ]
+
+-- Equality but obtained through conjurable
+(<==>) :: Conjurable a => a -> a -> Bool
+x <==> y  =  x == y
+  where
+  (==)  =  eval err . fromMaybe err $ conjureEquality x
+  err  =  error "<==>: could not conjure"
+infix 4 <==>
diff --git a/test/model/eg/bools.out b/test/model/eg/bools.out
--- a/test/model/eg/bools.out
+++ b/test/model/eg/bools.out
@@ -1,8 +1,8 @@
 and :: [Bool] -> Bool
--- looking through 1110 candidates, 100% match, 60/60 assignments
+-- looking through 1207 candidates, 100% match, 60/60 assignments
 and ps  =  null ps || head ps && and (tail ps)
 
 or :: [Bool] -> Bool
--- looking through 1110 candidates, 90% match, 54/60 assignments
+-- looking through 1207 candidates, 90% match, 54/60 assignments
 or ps  =  head ps || or (tail ps)
 
diff --git a/test/model/eg/factorial.out b/test/model/eg/factorial.out
--- a/test/model/eg/factorial.out
+++ b/test/model/eg/factorial.out
@@ -1,4 +1,4 @@
 factorial :: Int -> Int
--- looking through 9266 candidates, 100% match, 6/6 assignments
+-- looking through 8576 candidates, 100% match, 6/6 assignments
 factorial x  =  if isZero x then 1 else x * factorial (dec x)
 
diff --git a/test/model/eg/ints.out b/test/model/eg/ints.out
--- a/test/model/eg/ints.out
+++ b/test/model/eg/ints.out
@@ -1,16 +1,16 @@
 second :: [Int] -> Int
--- looking through 13460 candidates, 100% match, 47/47 assignments
+-- looking through 12955 candidates, 100% match, 47/47 assignments
 second xs  =  head (tail xs)
 
 third :: [Int] -> Int
--- looking through 13460 candidates, 100% match, 34/34 assignments
+-- looking through 12955 candidates, 100% match, 34/34 assignments
 third xs  =  head (tail (tail xs))
 
 sum :: [Int] -> Int
--- looking through 13460 candidates, 8% match, 5/60 assignments
+-- looking through 12955 candidates, 8% match, 5/60 assignments
 sum xs  =  if null (tail xs) then head xs else sum xs
 
 product :: [Int] -> Int
--- looking through 13460 candidates, 81% match, 49/60 assignments
-product xs  =  if 0 == head xs then 0 else product (tail xs)
+-- looking through 12955 candidates, 36% match, 22/60 assignments
+product xs  =  0 * head (tail (tail (tail xs)))