diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,7 @@
 tags
 eg/u-extrapolate
 eg/u-speculate
+eg/u-conjure
 bench/compare
 bench/pairs
 bench/sort
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -25,6 +25,7 @@
 BENCHS = \
   eg/u-extrapolate \
   eg/u-speculate \
+  eg/u-conjure \
   bench/compare \
   bench/pairs \
   bench/sort \
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -182,10 +182,10 @@
 
 	tiersFor :: Expr -> [[Expr]]
 	tiersFor e  =  case show (typ e) of
-	  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])
-	  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])
-	  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])
-	  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])
+	  "Int"    ->  mapT val (tiers :: [[Int]])
+	  "Bool"   ->  mapT val (tiers :: [[Bool]])
+	  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])
+	  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]])
 	  _        ->  []
 
 Above, we restrict ourselves to `Int`, `Bool`, `[Int]` and `[Bool]` as test
@@ -337,6 +337,78 @@
 limitations.
 
 
+Example 5: u-Conjure
+--------------------
+
+Using Express, it takes less than 70 lines of code to define a function
+`conjure` that generates a function from a partial function definition
+and a list of primitives.
+
+__Example 5.1.__ Given:
+
+	factorial :: Int -> Int
+	factorial 0  =  1
+	factorial 1  =  1
+	factorial 2  =  2
+	factorial 3  =  6
+	factorial 4  =  24
+
+Running:
+
+	conjure "factorial" factorial
+	  [ val (0 :: Int)
+	  , val (1 :: Int)
+	  , value "+" ((+) :: Int -> Int -> Int)
+	  , value "*" ((*) :: Int -> Int -> Int)
+	  , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
+	  , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])
+	  ]
+
+Prints:
+
+	  factorial :: Int -> Int
+	  factorial x  =  foldr (*) 1 (enumFromTo 1 x)
+
+__Example 5.2.__ Given:
+
+	(+++) :: [Int] -> [Int] -> [Int]
+	[x] +++ [y]  =  [x,y]
+	[x,y] +++ [z,w]  =  [x,y,z,w]
+
+Running:
+
+	conjure "++" (+++)
+      [ val (0 :: Int)
+      , val (1 :: Int)
+      , val ([] :: [Int])
+      , value "head" (head :: [Int] -> Int)
+      , value "tail" (tail :: [Int] -> [Int])
+      , value ":" ((:) :: Int -> [Int] -> [Int])
+      , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
+      ]
+
+Prints:
+
+	(++) :: [Int] -> [Int] -> [Int]
+	xs ++ ys  =  foldr (:) ys xs
+
+Please see the [u-Conjure] example in the [eg](eg) folder for the full code.
+
+[u-Conjure] has some limitations:
+
+* the maximum function size (7) or number of tests (60) are not configurable;
+* the maximum function size has to be kept small (<=7)
+  for a reasonable runtime.
+  Due to this, several simple functions are simply out-of-reach;
+* the number of primitive functions given has to be kept small (<12)
+  for a reasonable runtime;
+* there is no support for explicitly recursive functions
+  thought it is possible to pass `foldr` and similar functions as primitives.
+
+Please see [Conjure] library for an experimental version that addresses
+some the above limitations.
+
+
 Further reading
 ---------------
 
@@ -360,9 +432,11 @@
 [LeanCheck]:   https://hackage.haskell.org/package/leancheck
 [Extrapolate]: https://hackage.haskell.org/package/extrapolate
 [Speculate]:   https://hackage.haskell.org/package/speculate
+[Conjure]:     https://hackage.haskell.org/package/conjure
 
 [u-Speculate]:   eg/u-speculate.hs
 [u-Extrapolate]: eg/u-extrapolate.hs
+[u-Conjure]:     eg/u-conjure.hs
 
 [express-logo]: https://github.com/rudymatela/express/raw/master/doc/express.svg?sanitize=true
 
diff --git a/bench/runtime/zero/bench/compare.runtime b/bench/runtime/zero/bench/compare.runtime
--- a/bench/runtime/zero/bench/compare.runtime
+++ b/bench/runtime/zero/bench/compare.runtime
@@ -1,1 +1,1 @@
-0.01
+0.02
diff --git a/bench/runtime/zero/bench/pairs.runtime b/bench/runtime/zero/bench/pairs.runtime
--- a/bench/runtime/zero/bench/pairs.runtime
+++ b/bench/runtime/zero/bench/pairs.runtime
@@ -1,1 +1,1 @@
-0.00
+0.01
diff --git a/bench/runtime/zero/bench/sort.runtime b/bench/runtime/zero/bench/sort.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/sort.runtime
@@ -0,0 +1,1 @@
+0.19
diff --git a/bench/runtime/zero/bench/tiers.runtime b/bench/runtime/zero/bench/tiers.runtime
--- a/bench/runtime/zero/bench/tiers.runtime
+++ b/bench/runtime/zero/bench/tiers.runtime
@@ -1,1 +1,1 @@
-0.18
+0.20
diff --git a/bench/runtime/zero/eg/u-conjure.runtime b/bench/runtime/zero/eg/u-conjure.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/u-conjure.runtime
@@ -0,0 +1,1 @@
+0.34
diff --git a/bench/runtime/zero/eg/u-extrapolate.runtime b/bench/runtime/zero/eg/u-extrapolate.runtime
--- a/bench/runtime/zero/eg/u-extrapolate.runtime
+++ b/bench/runtime/zero/eg/u-extrapolate.runtime
@@ -1,1 +1,1 @@
-0.00
+0.01
diff --git a/bench/runtime/zero/eg/u-speculate.runtime b/bench/runtime/zero/eg/u-speculate.runtime
--- a/bench/runtime/zero/eg/u-speculate.runtime
+++ b/bench/runtime/zero/eg/u-speculate.runtime
@@ -1,1 +1,1 @@
-0.30
+0.32
diff --git a/changelog.md b/changelog.md
new file mode 100644
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,49 @@
+Changelog for Express
+=====================
+
+
+v0.1.10
+-------
+
+* add the `hasHole` and `isComplete` functions
+* add the `encompasses` function
+* add `appendInt` to `Data.Express.Fixtures`
+* add the `u-conjure` example
+* the `Express` typeclass now requires `Show`
+* improve examples in the `eg/` folder
+* improve tests of `hasInstanceOf` and `isInstanceOf`
+* improve tests
+* add this changelog
+
+
+v0.1.8
+------
+
+* slightly change behaviour of `canonicalVariations` and related functions.
+* add more fixtures and improve fixtures' documentation
+* improve Makefile and test scripts
+* use GitHub actions as CI
+
+
+v0.1.6
+------
+
+* add `compareLexicographically` and `compareQuickly`
+* define behaviour of `canonicalVariations` for some undefined cases
+* improve haddock documentation
+* improve tests
+
+
+v0.1.4
+------
+
+* add the `fill` and `isFun` functions
+* `Data.Express.Fixtures`: more fixtures, define fixity
+* add fixity for some fixtures
+* improve documentation, tests and lint
+
+
+v0.1.3
+------
+
+See the git commit log for v0.1.3 and previous versions.
diff --git a/eg/u-conjure.hs b/eg/u-conjure.hs
new file mode 100644
--- /dev/null
+++ b/eg/u-conjure.hs
@@ -0,0 +1,194 @@
+-- u-conjure.hs -- u-Conjure
+--
+-- This is a prototype for Conjure, a library for conjuring code
+-- out of partially implemented functions.
+--
+--
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+--
+--
+-- To run this you need to have both LeanCheck and Express installed:
+--
+-- $ cabal install leancheck
+-- $ cabal install express
+--
+-- If installation fails, use v1-install:
+--
+-- $ cabal v1-install leancheck
+-- $ cabal v1-install express
+import Data.List
+import Data.Maybe
+import Data.Express
+import Data.Typeable
+import Test.LeanCheck.Error
+
+
+square :: Int -> Int
+square 0  =  0
+square 1  =  1
+square 2  =  4
+square 3  =  9
+square 4  =  16
+
+add :: Int -> Int -> Int
+add 0 0  =  0
+add 0 1  =  1
+add 1 0  =  1
+add 1 1  =  2
+
+factorial :: Int -> Int
+factorial 0  =  1
+factorial 1  =  1
+factorial 2  =  2
+factorial 3  =  6
+factorial 4  =  24
+
+second :: [Int] -> Int
+second [x,y]  =  y
+second [x,y,z]  =  y
+second [x,y,z,w]  =  y
+
+-- reverse
+reverse' :: [Int] -> [Int]
+reverse' [x,y]  =  [y,x]
+reverse' [x,y,z]  =  [z,y,x]
+
+-- ++
+(+++) :: [Int] -> [Int] -> [Int]
+[x] +++ [y]  =  [x,y]
+[x,y] +++ [z,w]  =  [x,y,z,w]
+
+
+main :: IO ()
+main  =  do
+  conjure "square"    square    primitives
+  conjure "add"       add       primitives
+  conjure "factorial" factorial primitives
+
+  conjure "factorial"   factorial
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "*" ((*) :: Int -> Int -> Int)
+    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
+    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])
+    ]
+
+  conjure "second"  second   listPrimitives
+  conjure "++"      (+++)    listPrimitives
+  conjure "reverse" reverse' listPrimitives
+
+  -- even by using fold and some cheating,
+  -- this function is out of reach
+  --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs
+  --  reverse xs  =  foldr (flip (++) . unit) [] xs
+  conjure "reverse" reverse' $ listPrimitives ++
+    [ value "unit" ((:[]) :: Int -> [Int])
+    , value "++" ((++) :: [Int] -> [Int] -> [Int])
+    -- these last two are cheats:
+    , value "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])
+    , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])
+    ]
+
+  where
+
+  primitives :: [Expr]
+  primitives =
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , val (2 :: Int)
+    , val (3 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "*" ((*) :: Int -> Int -> Int)
+    , value "-" ((-) :: Int -> Int -> Int)
+    ]
+
+  listPrimitives :: [Expr]
+  listPrimitives =
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , val ([] :: [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
+    ]
+
+
+conjure :: Typeable f => String -> f -> [Expr] -> IO ()
+conjure nm f primitives  =  do
+  print (value nm f) -- prints the type signature
+  case conjureImplementations nm f primitives of
+    []    -> putStrLn $ "cannot conjure"
+--  es    -> putStrLn $ unlines $ map showEq es  -- uncomment to show all found variations
+    (e:_) -> putStrLn $ showEq e
+  putStrLn ""
+  where
+  showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
+
+
+conjureImplementations :: Typeable f => String -> f -> [Expr] -> [Expr]
+conjureImplementations nm f primitives  =
+  [ appn -==- e
+  | e <- candidateExprsFrom $ exs ++ primitives
+  , isTrue (appn -==- e)
+  ]
+  where
+  appn  =  application nm f primitives
+  (ef:exs)  =  unfoldApp appn
+  isTrue e  =  all (errorToFalse . eval False) . map (e //-) $ definedBinds appn
+
+
+definedBinds :: Expr -> [[(Expr,Expr)]]
+definedBinds ffxx  =  [bs | bs <- bss, errorToFalse . eval False $ e //- bs]
+  where
+  e  =  ffxx -==- ffxx
+  bss  =  take 360 $ groundBinds ffxx
+
+
+application :: Typeable f => String -> f -> [Expr] -> Expr
+application nm f es  =  mostGeneralCanonicalVariation $ appn (value nm f)
+  where
+  appn ff | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of
+                          [] -> error "application: could not find type representative"
+                          (e:_) -> appn (ff :$ holeAsTypeOf e)
+          | otherwise  =  ff
+
+
+candidateExprsFrom :: [Expr] -> [Expr]
+candidateExprsFrom  =  concat . take 7 . expressionsT
+  where
+  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)
+    where
+    es = expressionsT ds
+
+
+(-==-) :: Expr -> Expr -> Expr
+ex -==- ey  =  headOr (val False) . map (:$ ey) $ mapMaybe ($$ ex)
+  [ value "==" ((==) :: Int -> Int -> Bool)
+  , value "==" ((==) :: Bool -> Bool -> Bool)
+  , value "==" ((==) :: [Int] -> [Int] -> Bool)
+  , value "==" ((==) :: [Bool] -> [Bool] -> Bool)
+  ]
+  where
+  headOr x []     =  x
+  headOr _ (x:_)  =  x
+
+
+lhs, rhs :: Expr -> Expr
+lhs (((Value "==" _) :$ e) :$ _)  =  e
+rhs (((Value "==" _) :$ _) :$ e)  =  e
+
+
+groundBinds :: Expr -> [[(Expr,Expr)]]
+groundBinds e  =  concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]
+
+
+tiersFor :: Expr -> [[Expr]]
+tiersFor e  =  case show (typ e) of
+  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])
+  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])
+  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])
+  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])
+  _        ->  []
diff --git a/eg/u-extrapolate.hs b/eg/u-extrapolate.hs
--- a/eg/u-extrapolate.hs
+++ b/eg/u-extrapolate.hs
@@ -29,7 +29,7 @@
 import Data.List
 import Data.Maybe
 import Data.Express
-import Test.LeanCheck hiding (counterExample, check)
+import Test.LeanCheck hiding (counterExamples, check)
 
 main :: IO ()
 main  =  do
@@ -39,6 +39,9 @@
   putStrLn "length . nub = length  (incorrect when there are repeated elements)"
   check $ \xs -> length (nub xs :: [Int]) == length xs
 
+  putStrLn "xs `union` ys == ys `union` xs  (incorrect for repeated elements)"
+  check $ \(xs,ys) -> xs `union` ys == ys `union` (xs :: [Int])
+
   putStrLn "\\(x,y) -> x + y == y + x"
   check $ \(x,y) -> x + y == y + (x :: Int)
 
@@ -53,24 +56,23 @@
 
 
 check :: (Listable a, Express a) => (a -> Bool) -> IO ()
-check prop  =  putStrLn $ case counterExample 500 prop of
-  Nothing -> "+++ Tests passed.\n"
-  Just ce -> "*** Falsified, counterexample:  " ++ show ce
-          ++ case counterExampleGeneralization 500 prop ce of
-             Nothing -> ""
-             Just g -> "\n               generalization:  " ++ show g
-          ++ "\n"
-
-
-counterExample :: (Listable a, Express a) => Int -> (a -> Bool) -> Maybe Expr
-counterExample maxTests prop  =  listToMaybe
-  [expr x | x <- take maxTests list, not (prop x)]
+check prop  =  putStrLn $ case counterExampleAndGeneralizations 500 prop of
+  []      ->  "+++ Tests passed.\n"
+  (ce:gs) -> unlines
+           $ ("*** Falsified, counterexample:  " ++ showExpr ce)
+           : ["               generalization:  " ++ showExpr g | g <- gs ]
 
-counterExampleGeneralization :: Express a => Int -> (a -> Bool) -> Expr -> Maybe Expr
-counterExampleGeneralization maxTests prop e  =  listToMaybe
-  [g | g <- candidateGeneralizations e
-     , all (not . prop . evl) (take maxTests $ grounds g)]
+counterExamples :: (Listable a, Express a) => Int -> (a -> Bool) -> [Expr]
+counterExamples maxTests prop  =  [expr x | x <- take maxTests list, not (prop x)]
 
+counterExampleAndGeneralizations :: (Listable a, Express a)
+                                 => Int -> (a -> Bool) -> [Expr]
+counterExampleAndGeneralizations maxTests prop  =
+  case counterExamples maxTests prop of
+  [] -> []
+  (ce:_) -> ce : discardLater isInstanceOf
+                   [ g | g <- candidateGeneralizations ce
+                       , all (not . prop . evl) (take maxTests $ grounds g) ]
 
 candidateGeneralizations :: Expr -> [Expr]
 candidateGeneralizations  =  map canonicalize
@@ -94,8 +96,15 @@
 
 tiersFor :: Expr -> [[Expr]]
 tiersFor e  =  case show (typ e) of
-  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])
-  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])
-  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])
-  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])
+  "Int"    ->  mapT val (tiers :: [[Int]])
+  "Bool"   ->  mapT val (tiers :: [[Bool]])
+  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])
+  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]])
   _        ->  []
+
+discardLater :: (a -> a -> Bool) -> [a] -> [a]
+discardLater (?)  =  d
+  where
+  d []      =  []
+  d (x:xs)  =  x : d (discard (? x) xs)
+  discard p  =  filter (not . p)
diff --git a/eg/u-speculate.hs b/eg/u-speculate.hs
--- a/eg/u-speculate.hs
+++ b/eg/u-speculate.hs
@@ -13,7 +13,7 @@
 --
 -- Limitations:
 --
--- * even with pruning, this program still prints some redundant rules;
+-- * this program prints redundant equations;
 -- * there is no way to configure maximum number of tests to consider an
 --   equation true;
 -- * runtime is exponential as you add more symbols to speculate about.
@@ -71,25 +71,22 @@
   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
 
 speculateAbout :: [Expr] -> [Expr]
-speculateAbout  =  discardLater hasRewrite
-                .  discardLaterInstances
+speculateAbout  =  discardLater canBeSimplifiedBy
+                .  discardLater isInstanceOf
                 .  concatMap trueCanonicalVariations
-                .  discardLaterInstances
+                .  discardLater (\e1 e2 -> isntIdentity e2 && e2 `isInstanceOf` e1)
                 .  sort
                 .  filter isTrue
                 .  candidateEquationsFrom
   where
-  hasRewrite e1 e2  =  isRule e2 && e1 `hasInstanceOf` lhs e2
+  e1 `canBeSimplifiedBy` e2  =  isRule e2 && e1 `hasInstanceOf` lhs e2
 
 trueCanonicalVariations :: Expr -> [Expr]
-trueCanonicalVariations  =  discardLaterInstances
+trueCanonicalVariations  =  discardLater isInstanceOf
                          .  filter isTrue
                          .  filter isntIdentity
                          .  canonicalVariations
 
-discardLaterInstances :: [Expr] -> [Expr]
-discardLaterInstances =  discardLater (\e1 e2 -> isntIdentity e2 && e1 `isInstanceOf` e2)
-
 candidateEquationsFrom :: [Expr] -> [Expr]
 candidateEquationsFrom es'  =  [e1 -==- e2 | e1 <- es, e2 <- es, e1 >= e2]
   where
@@ -106,15 +103,14 @@
 isTrue  =  all (eval False) . take 60 . grounds
 
 grounds :: Expr -> [Expr]
-grounds e  =  map (e //-)  .  concat
-           $  products [mapT ((,) v) (tiersFor v) | v <- nubVars e]
+grounds e  =  map (e //-) . concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]
 
 tiersFor :: Expr -> [[Expr]]
 tiersFor e  =  case show (typ e) of
-  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])
-  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])
-  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])
-  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])
+  "Int"    ->  mapT val (tiers :: [[Int]])
+  "Bool"   ->  mapT val (tiers :: [[Bool]])
+  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])
+  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]])
   _        ->  []
 
 (-==-) :: Expr -> Expr -> Expr
diff --git a/express.cabal b/express.cabal
--- a/express.cabal
+++ b/express.cabal
@@ -1,6 +1,6 @@
 -- Cabal file for express
 name: express
-version: 0.1.8
+version: 0.1.10
 synopsis: Dynamically-typed expressions involving applications and variables.
 description:
   Express is a library for manipulating dynamically typed Haskell expressions.
@@ -23,6 +23,7 @@
 
 extra-doc-files: README.md
                , TODO.md
+               , changelog.md
                , doc/express.svg
 extra-source-files: .gitignore
                   , .travis.yml
@@ -43,7 +44,9 @@
                   , bench/runtime/zero/versions
                   , bench/runtime/zero/bench/*.runtime
                   , bench/runtime/zero/eg/*.runtime
-tested-with: GHC==8.8
+tested-with: GHC==9.0
+           , GHC==8.10
+           , GHC==8.8
            , GHC==8.6
            , GHC==8.4
            , GHC==8.2
@@ -59,7 +62,7 @@
 source-repository this
   type:           git
   location:       https://github.com/rudymatela/express
-  tag:            v0.1.8
+  tag:            v0.1.10
 
 library
   exposed-modules:     Data.Express
@@ -262,6 +265,13 @@
 benchmark u-speculate
   type:                exitcode-stdio-1.0
   main-is:             u-speculate.hs
+  hs-source-dirs:      eg
+  build-depends:       base >= 4 && < 5, express, leancheck >= 0.9.4
+  default-language:    Haskell2010
+
+benchmark u-conjure
+  type:                exitcode-stdio-1.0
+  main-is:             u-conjure.hs
   hs-source-dirs:      eg
   build-depends:       base >= 4 && < 5, express, leancheck >= 0.9.4
   default-language:    Haskell2010
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -106,6 +106,28 @@
   test/Test/ListableExpr.hs \
   bench/tiers.hs \
   mk/toplibs
+eg/u-conjure: \
+  eg/u-conjure.hs \
+  mk/toplibs
+eg/u-conjure.o: \
+  src/Data/Express/Utils/Typeable.hs \
+  src/Data/Express/Utils/TH.hs \
+  src/Data/Express/Utils/String.hs \
+  src/Data/Express/Utils/List.hs \
+  src/Data/Express.hs \
+  src/Data/Express/Name.hs \
+  src/Data/Express/Name/Derive.hs \
+  src/Data/Express/Match.hs \
+  src/Data/Express/Map.hs \
+  src/Data/Express/Instances.hs \
+  src/Data/Express/Hole.hs \
+  src/Data/Express/Fold.hs \
+  src/Data/Express/Express.hs \
+  src/Data/Express/Express/Derive.hs \
+  src/Data/Express/Core.hs \
+  src/Data/Express/Canon.hs \
+  src/Data/Express/Basic.hs \
+  eg/u-conjure.hs
 eg/u-extrapolate: \
   eg/u-extrapolate.hs \
   mk/toplibs
diff --git a/src/Data/Express.hs b/src/Data/Express.hs
--- a/src/Data/Express.hs
+++ b/src/Data/Express.hs
@@ -142,7 +142,9 @@
   , isWellTyped
   , isFun
   , hasVar
+  , hasHole
   , isGround
+  , isComplete
 
   -- ** Comparing Exprs
   , compareComplexity
@@ -239,6 +241,7 @@
   , isInstanceOf
   , hasInstanceOf
   , isSubexprOf
+  , encompasses
 
   -- -- -- Data.Express.Express exports -- -- --
 
diff --git a/src/Data/Express/Express.hs b/src/Data/Express/Express.hs
--- a/src/Data/Express/Express.hs
+++ b/src/Data/Express/Express.hs
@@ -60,7 +60,7 @@
 -- '-:', '->:', '->>:', '->>>:', '->>>>:', '->>>>>:', ...
 --
 -- For types with atomic values, just declare @ expr = val @
-class Typeable a => Express a where
+class (Show a, Typeable a) => Express a where
   expr :: a -> Expr
 
 instance Express ()        where  expr  =  val
@@ -91,15 +91,14 @@
                   :$ expr x :$ expr y :$ expr z :$ expr w
 
 instance Express a => Express [a] where
-  expr xs@[]
-    | typeOf xs == typeOf ""  =  value "\"\"" ([] -: xs)
-    | otherwise               =  value "[]" ([] -: xs)
-  expr xs@(y:ys)              =  value ":"  ((:) ->>: xs) :$ expr y :$ expr ys
+  expr xs  =  case xs of
+              [] -> val xs
+              (y:ys) -> value ":" ((:) ->>: xs) :$ expr y :$ expr ys
 
 
 -- instances of further types and arities --
 
-instance (Integral a, Show a, Express a) => Express (Ratio a) where
+instance (Integral a, Express a) => Express (Ratio a) where
   expr  =  val
 -- The following would allow zero denominators
 -- expr (n % d) = constant "%" ((%) -:> n) :$ expr n :$ expr d
diff --git a/src/Data/Express/Fixtures.hs b/src/Data/Express/Fixtures.hs
--- a/src/Data/Express/Fixtures.hs
+++ b/src/Data/Express/Fixtures.hs
@@ -168,6 +168,7 @@
   , bs_, pps, qqs
   , and', or'
   , sum', product'
+  , appendInt
 
   -- ** Maybes
   , nothing
@@ -834,6 +835,9 @@
   where
   err  =  error $ "(-:-): unhandled type " ++ show (typ e1)
 infixr 5 -:-
+
+appendInt :: Expr
+appendInt  =  value "++" ((++) :: [Int] -> [Int] -> [Int])
 
 -- | List concatenation lifted over the 'Expr' type.
 --   Works for the element types 'Int', 'Char' and 'Bool'.
diff --git a/src/Data/Express/Hole.hs b/src/Data/Express/Hole.hs
--- a/src/Data/Express/Hole.hs
+++ b/src/Data/Express/Hole.hs
@@ -16,6 +16,8 @@
   -- * Typed holes
   , hole
   , isHole
+  , hasHole
+  , isComplete
   , holes
   , nubHoles
   , holeAsTypeOf
@@ -130,6 +132,42 @@
 -- such as @f (g (h (f (g (h x)))))@.
 nubHoles :: Expr -> [Expr]
 nubHoles  =  nubSort . holes
+
+-- | /O(n)/.
+-- Returns whether an expression contains a hole
+--
+-- > > hasHole $ hole (undefined :: Bool)
+-- > True
+--
+-- > > hasHole $ value "not" not :$ val True
+-- > False
+--
+-- > > hasHole $ value "not" not :$ hole (undefined :: Bool)
+-- > True
+hasHole :: Expr -> Bool
+hasHole  =  any isHole . values
+
+-- | /O(n)/.
+-- Returns whether an expression is complete.
+-- A complete expression is one without holes.
+--
+-- > > isComplete $ hole (undefined :: Bool)
+-- > False
+--
+-- > > isComplete $ value "not" not :$ val True
+-- > True
+--
+-- > > isComplete $ value "not" not :$ hole (undefined :: Bool)
+-- > False
+--
+-- 'isComplete' is the negation of 'hasHole'.
+--
+-- > isComplete  =  not . hasHole
+--
+-- 'isComplete' is to 'hasHole' what
+-- 'isGround' is to 'hasVar'.
+isComplete :: Expr -> Bool
+isComplete  =  not . hasHole
 
 -- |
 -- Generate an infinite list of variables
diff --git a/src/Data/Express/Match.hs b/src/Data/Express/Match.hs
--- a/src/Data/Express/Match.hs
+++ b/src/Data/Express/Match.hs
@@ -11,6 +11,7 @@
   , isInstanceOf
   , hasInstanceOf
   , isSubexprOf
+  , encompasses
   )
 where
 
@@ -76,7 +77,7 @@
 -- checks if the first expression
 -- is an instance of the second
 -- in terms of variables.
--- (cf. 'hasInstanceOf')
+-- (cf. 'encompasses', 'hasInstanceOf')
 --
 -- > > let zero = val (0::Int)
 -- > > let one  = val (1::Int)
@@ -96,6 +97,21 @@
 -- >  (one -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy)  =  False
 isInstanceOf :: Expr -> Expr -> Bool
 e1 `isInstanceOf` e2 = isJust $ e1 `match` e2
+
+
+-- |
+-- Given two 'Expr's,
+-- checks if the first expression
+-- encompasses the second expression
+-- in terms of variables.
+--
+-- This is equivalent to flipping the arguments of 'isInstanceOf'.
+--
+-- > zero `encompasses` xx    =  False
+-- >   xx `encompasses` zero  =  True
+encompasses :: Expr -> Expr -> Bool
+encompasses  =  flip isInstanceOf
+
 
 -- |
 -- Checks if any of the subexpressions of the first argument 'Expr'
diff --git a/test/express.hs b/test/express.hs
--- a/test/express.hs
+++ b/test/express.hs
@@ -72,6 +72,10 @@
   , expr ([0::Int,1])  == zero -:- one -:- nil
   , holds n $ \xs -> expr xs == foldr (-:-) nil (map expr (xs :: [Int]))
   , holds n $ \ps -> expr ps == foldr (-:-) nilBool (map expr (ps :: [Bool]))
+  , expr (""::String) == value "\"\"" ""
+  , expr (""::String) == val ""
+  , expr ("a"::String) == unit (val 'a')
+  , expr ("abc"::String) == val 'a' -:- val 'b' -:- unit (val 'c')
 
   -- Transforming Maybes into Exprs
   , expr (Nothing    :: Maybe Int)   ==  nothing
@@ -81,7 +85,7 @@
   , holds n $ \x -> expr (Just x) == just (expr (x :: Int))
   , holds n $ \p -> expr (Just p) == just (expr (p :: Bool))
 
-  -- Transforming Tuples into Exprs
+  -- Transforming tuples into Exprs
   , expr ((0,False) :: (Int,Bool))  ==  pair zero false
   , expr ((True,1)  :: (Bool,Int))  ==  pair true one
 
@@ -89,6 +93,7 @@
   , holds n $ \x -> show (expr x) == show (x :: ()) ++ " :: ()"
   , holds n $ \x -> show (expr x) == show (x :: Int) ++ " :: Int"
   , holds n $ \p -> show (expr p) == show (p :: Bool) ++ " :: Bool"
+  , holds n $ \s -> show (expr s) == show (s :: String) ++ " :: [Char]"
   , holds n $ \x -> show (expr x) == show (x :: ((),Maybe Int,[Bool]))
                                         ++ " :: ((),(Maybe Int),[Bool])"
   ]
diff --git a/test/hole.hs b/test/hole.hs
--- a/test/hole.hs
+++ b/test/hole.hs
@@ -18,6 +18,10 @@
 
   , holds n $ \e -> isHole e ==> isVar e
   , holds n $ \e1 e2 -> isHole (e1 :$ e2) == False
+  , holds n $ \e -> isHole e ==> hasHole e
+  , holds n $ \e1 e2 -> (hasHole e1 || hasHole e2) == hasHole (e1 :$ e2)
+  , holds n $ \e -> hasHole e == (not . null . holes) e
+  , holds n $ \e -> isComplete e == not (hasHole e)
 
   , holds n $ \e -> holes e `isSubsequenceOf` vars e
   , holds n $ \e -> nubHoles e `isSubsetOf` holes e
diff --git a/test/match.hs b/test/match.hs
--- a/test/match.hs
+++ b/test/match.hs
@@ -15,6 +15,7 @@
   , holds n $ \(IntE e1) (IntE e2) -> (e1 -+- e2) `isInstanceOf` (xx -+- yy)
   , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> not ((e1 -+- e2) `isInstanceOf` (xx -+- xx))
   , holds n $ \e                   -> e /= zero ==> not (e `isInstanceOf` zero)
+  , holds n $ \e1 e2 -> e1 `encompasses` e2 == e2 `isInstanceOf` e1
 
   ,       (zero -+- one)       `isInstanceOf` (xx -+- yy)
   ,       (zero -+- zero)      `isInstanceOf` (xx -+- yy)
@@ -54,4 +55,30 @@
                        == ((ef :$ ex) `isInstanceOf` e || ef `hasInstanceOf` e
                                                        || ex `hasInstanceOf` e)
   , holds n $ \e1 e2 -> e1 `hasInstanceOf` e2 == any (`isInstanceOf` e2) (subexprs e1)
+
+  -- isInstanceOf is reflexive and transitive
+  -- but not antisymmetric nor asymmetric
+  -- so is no order
+  , holds n $ isReflexive     isInstanceOf
+  , holds n $ isTransitive    isInstanceOf
+  , fails n $ isAntisymmetric isInstanceOf -- structural equality
+  , fails n $ isAsymmetric    isInstanceOf
+  , fails n $ isTotalOrder    isInstanceOf
+  , fails n $ isPartialOrder  isInstanceOf
+
+  -- the same goes for hasInstanceOf
+  , holds n $ isReflexive     hasInstanceOf
+  , holds n $ isTransitive    hasInstanceOf
+  , fails n $ isAntisymmetric hasInstanceOf
+  , fails n $ isAsymmetric    hasInstanceOf
+  , fails n $ isTotalOrder    hasInstanceOf
+  , fails n $ isPartialOrder  hasInstanceOf
+
+  -- one can construct the following equivalence
+  , holds n $ isEquivalence (isInstanceOf &&&& flip isInstanceOf)
+
+  -- the following is not an equivalence
+  , fails n $ isEquivalence (isInstanceOf |||| flip isInstanceOf)
+  -- so it cannot be used as an argument to nubBy
+  -- which requires equivalence according to the Haskell 2010 Report.
   ]
diff --git a/test/model/eg/u-conjure.out b/test/model/eg/u-conjure.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/u-conjure.out
@@ -0,0 +1,24 @@
+square :: Int -> Int
+square x  =  x * x
+
+add :: Int -> Int -> Int
+add x y  =  x + y
+
+factorial :: Int -> Int
+cannot conjure
+
+factorial :: Int -> Int
+factorial x  =  foldr (*) 1 (enumFromTo 1 x)
+
+second :: [Int] -> Int
+second xs  =  head (tail xs)
+
+(++) :: [Int] -> [Int] -> [Int]
+xs ++ ys  =  foldr (:) ys xs
+
+reverse :: [Int] -> [Int]
+cannot conjure
+
+reverse :: [Int] -> [Int]
+reverse xs  =  foldr (foldr (:) . unit) [] xs
+
diff --git a/test/model/eg/u-extrapolate.out b/test/model/eg/u-extrapolate.out
--- a/test/model/eg/u-extrapolate.out
+++ b/test/model/eg/u-extrapolate.out
@@ -2,20 +2,25 @@
 +++ Tests passed.
 
 length . nub = length  (incorrect when there are repeated elements)
-*** Falsified, counterexample:  [0,0] :: [Int]
-               generalization:  x:x:xs :: [Int]
+*** Falsified, counterexample:  [0,0]
+               generalization:  x:x:xs
 
+xs `union` ys == ys `union` xs  (incorrect for repeated elements)
+*** Falsified, counterexample:  ([],[0,0])
+               generalization:  (xs,x:x:xs)
+               generalization:  ([],x:x:xs)
+
 \(x,y) -> x + y == y + x
 +++ Tests passed.
 
 \x -> x == x + 1  (always incorrect)
-*** Falsified, counterexample:  0 :: Int
-               generalization:  x :: Int
+*** Falsified, counterexample:  0
+               generalization:  x
 
 \(x,y) -> x + y == x + x  (incorrect)
-*** Falsified, counterexample:  (0,1) :: (Int,Int)
+*** Falsified, counterexample:  (0,1)
 
 \(x,y) -> x /= y  (incorrect whenever x and y are equal)
-*** Falsified, counterexample:  (0,0) :: (Int,Int)
-               generalization:  (x,x) :: (Int,Int)
+*** Falsified, counterexample:  (0,0)
+               generalization:  (x,x)