diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -144,6 +144,9 @@
 
 For more examples, see the [eg](eg) and [bench](bench) folders.
 
+Speculate has been subject to a paper, see the
+[(Draft) Paper about Speculate (to appear) on Haskell Symposium 2017](https://matela.com.br/paper/speculate.pdf).
+
 [leancheck]: https://hackage.haskell.org/package/leancheck
 [LeanCheck]: https://hackage.haskell.org/package/leancheck
 [QuickSpec]: https://github.com/nick8325/quickspec
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -24,7 +24,18 @@
   ":".
 
 
+isolate most of the Expr module
+-------------------------------
 
+Maybe most of the `Expr` module could be isolated from the rest of Speculate
+and released as a separate package.
+
+I'll have to see how it goes in other modules, specially the `grounds`
+function.  Which could be interesting to include in the "expr" package but
+would still depend on Listable and LeanCheck (maybe make it depend on it
+anyway...)
+
+
 later
 -----
 
@@ -149,7 +160,7 @@
 
 * (for interface) I actually do not need to provide 0-argument constants in the
   background algebra.  Since I am using an enumerative strategy, I can actually
-  enumerate those from the TypeInfo.  This way, background will look nicer,
+  enumerate those from `Instances`.  This way, background will look nicer,
   with less functions and values.  Computing the size of values and expressions
   may be a problem.
 
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.2.4
+version:             0.2.5
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -18,7 +18,7 @@
 maintainer:          Rudy Matela <rudy@matela.com.br>
 category:            Testing
 build-type:          Simple
-cabal-version:       >=1.10
+cabal-version:       >=1.18
 
 extra-doc-files: README.md
                , TODO.md
@@ -31,7 +31,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.2.4
+  tag:             v0.2.5
 
 
 library
@@ -44,8 +44,8 @@
                  , Test.Speculate.Expr.Core
                  , Test.Speculate.Expr.Equate
                  , Test.Speculate.Expr.Ground
+                 , Test.Speculate.Expr.Instance
                  , Test.Speculate.Expr.Match
-                 , Test.Speculate.Expr.TypeInfo
                  , Test.Speculate.Pretty
                  , Test.Speculate.Reason
                  , Test.Speculate.Reason.Order
@@ -67,7 +67,7 @@
                  , Test.Speculate.Utils.Timeout
                  , Test.Speculate.Utils.Tuple
                  , Test.Speculate.Utils.Typeable
-  build-depends: base >= 4 && < 5, leancheck >= 0.6.1, cmdargs, containers
+  build-depends: base >= 4 && < 5, leancheck >= 0.6.3, cmdargs, containers
   hs-source-dirs:    src
   default-language:  Haskell2010
 
diff --git a/src/Test/Speculate/Expr.hs b/src/Test/Speculate/Expr.hs
--- a/src/Test/Speculate/Expr.hs
+++ b/src/Test/Speculate/Expr.hs
@@ -11,7 +11,7 @@
   ( module Test.Speculate.Expr.Core
   , module Test.Speculate.Expr.Ground
   , module Test.Speculate.Expr.Match
-  , module Test.Speculate.Expr.TypeInfo
+  , module Test.Speculate.Expr.Instance
   , module Test.Speculate.Expr.Equate
   , module Test.Speculate.Expr.Canon
   )
@@ -20,6 +20,6 @@
 import Test.Speculate.Expr.Core
 import Test.Speculate.Expr.Ground
 import Test.Speculate.Expr.Match
-import Test.Speculate.Expr.TypeInfo
+import Test.Speculate.Expr.Instance
 import Test.Speculate.Expr.Equate
 import Test.Speculate.Expr.Canon
diff --git a/src/Test/Speculate/Expr/Canon.hs b/src/Test/Speculate/Expr/Canon.hs
--- a/src/Test/Speculate/Expr/Canon.hs
+++ b/src/Test/Speculate/Expr/Canon.hs
@@ -16,7 +16,7 @@
 
 import Test.Speculate.Expr.Core
 import Test.Speculate.Expr.Match
-import Test.Speculate.Expr.TypeInfo
+import Test.Speculate.Expr.Instance
 import Data.List ((\\))
 
 -- | Canonicalize variable names in an expression.
diff --git a/src/Test/Speculate/Expr/Core.hs b/src/Test/Speculate/Expr/Core.hs
--- a/src/Test/Speculate/Expr/Core.hs
+++ b/src/Test/Speculate/Expr/Core.hs
@@ -7,6 +7,7 @@
 -- This module is part of Speculate.
 --
 -- Defines the 'Expr' type and basic operations on it.
+{-# LANGUAGE DeriveDataTypeable #-} -- for GHC < 7.10
 module Test.Speculate.Expr.Core
   ( Expr (..)
   -- * Smart constructors
@@ -76,6 +77,7 @@
 data Expr = Constant String Dynamic
           | Var String TypeRep
           | Expr :$ Expr
+  deriving Typeable -- for GHC < 7.10
 
 -- | Encode a constant Haskell expression for use by Speculate.
 --   It takes a string representation of a value and a value, returning an
@@ -145,12 +147,33 @@
   where sp = if atomic s then isInfix s else maybe True (d >) $ outernmostPrec s
 showsPrecExpr d (Var "" _)     = showString "_" -- a hole
 showsPrecExpr d (Var s _)      = showParen (isInfix s) $ showString s
+showsPrecExpr d ((Constant ":" _ :$ e1@(Constant _ _)) :$ e2)
+  | typ e1 == typeOf (undefined :: Char) =
+  case showsTailExpr e2 "" of
+    '\"':cs  -> showString ("\"" ++ (init . tail) (showsPrecExpr 0 e1 "") ++ cs)
+    cs -> showParen (d > prec ":")
+        $ showsOpExpr ":" e1 . showString ":" . showString cs
 showsPrecExpr d ((Constant ":" _ :$ e1) :$ e2) =
-  case showsPrecExpr 0 e2 "" of
+  case showsTailExpr e2 "" of
     "[]" -> showString "[" . showsPrecExpr 0 e1 . showString "]"
     '[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs
     cs -> showParen (d > prec ":")
-        $ showsOpExpr ":" e1 . showString ":" . showsOpExpr ":" e2
+        $ showsOpExpr ":" e1 . showString ":" . showString cs
+showsPrecExpr d ((Constant "," _ :$ e1) :$ e2) =
+    showString "(" . showsPrecExpr 0 e1
+  . showString "," . showsPrecExpr 0 e2
+  . showString ")"
+showsPrecExpr d (((Constant ",," _ :$ e1) :$ e2) :$ e3) =
+    showString "(" . showsPrecExpr 0 e1
+  . showString "," . showsPrecExpr 0 e2
+  . showString "," . showsPrecExpr 0 e3
+  . showString ")"
+showsPrecExpr d ((((Constant ",,," _ :$ e1) :$ e2) :$ e3) :$ e4) =
+    showString "(" . showsPrecExpr 0 e1
+  . showString "," . showsPrecExpr 0 e2
+  . showString "," . showsPrecExpr 0 e3
+  . showString "," . showsPrecExpr 0 e4
+  . showString ")"
 showsPrecExpr d ((Constant f _ :$ e1) :$ e2)
   | isInfix f = showParen (d > prec f)
               $ showsOpExpr f e1
@@ -167,6 +190,20 @@
                            $ showsPrecExpr (prec " ") e1
                            . showString " "
                            . showsPrecExpr (prec " " + 1) e2
+
+-- bad smell here, repeated code!
+showsTailExpr :: Expr -> String -> String
+showsTailExpr ((Constant ":" _ :$ e1@(Constant _ _)) :$ e2)
+  | typ e1 == typeOf (undefined :: Char) =
+  case showsPrecExpr 0 e2 "" of
+    '\"':cs  -> showString ("\"" ++ (init . tail) (showsPrecExpr 0 e1 "") ++ cs)
+    cs -> showsOpExpr ":" e1 . showString ":" . showsTailExpr e2
+showsTailExpr ((Constant ":" _ :$ e1) :$ e2) =
+  case showsPrecExpr 0 e2 "" of
+    "[]" -> showString "[" . showsPrecExpr 0 e1 . showString "]"
+    '[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs
+    cs -> showsOpExpr ":" e1 . showString ":" . showsTailExpr e2
+showsTailExpr e = showsOpExpr ":" e
 
 showsOpExpr :: String -> Expr -> String -> String
 showsOpExpr op = showsPrecExpr (prec op + 1)
diff --git a/src/Test/Speculate/Expr/Equate.hs b/src/Test/Speculate/Expr/Equate.hs
--- a/src/Test/Speculate/Expr/Equate.hs
+++ b/src/Test/Speculate/Expr/Equate.hs
@@ -30,7 +30,7 @@
 import Data.List ((\\))
 import Test.Speculate.Utils
 import Test.Speculate.Expr.Core
-import Test.Speculate.Expr.TypeInfo
+import Test.Speculate.Expr.Instance
 
 equation :: Instances -> Expr -> Expr -> Maybe Expr
 equation ti e1 e2 = do
diff --git a/src/Test/Speculate/Expr/Ground.hs b/src/Test/Speculate/Expr/Ground.hs
--- a/src/Test/Speculate/Expr/Ground.hs
+++ b/src/Test/Speculate/Expr/Ground.hs
@@ -26,7 +26,7 @@
 
 import Test.Speculate.Expr.Core
 import Test.Speculate.Expr.Match
-import Test.Speculate.Expr.TypeInfo
+import Test.Speculate.Expr.Instance
 import Test.Speculate.Expr.Equate
 import Test.LeanCheck
 import Data.Ratio
diff --git a/src/Test/Speculate/Expr/Instance.hs b/src/Test/Speculate/Expr/Instance.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Speculate/Expr/Instance.hs
@@ -0,0 +1,261 @@
+{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC <= 7.8
+-- |
+-- Module      : Test.Speculate.Expr.Instance
+-- Copyright   : (c) 2016-2017 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- This module is part of Speculate.
+--
+-- Typeclass instance information.
+module Test.Speculate.Expr.Instance
+  ( Instances
+  , Instance (..)
+  , TypeRep
+
+  -- * Smart constructors
+  , ins
+  , eq,       eqWith
+  , ord,      ordWith
+  , eqOrd
+  , listable, listableWith
+  , name
+
+  -- * Queries on Instances
+  , instanceType
+  , findInfo
+  , names
+  , eqE,      isEq,       isEqE
+  , leE, ltE, isOrd,      isOrdE
+  ,           isEqOrd,    isEqOrdE
+  , tiersE,   isListable
+
+  -- * Type info for standard Haskell types
+  , preludeInstances
+
+  -- * Does not belong here?
+  , defNames
+
+  , boolTy
+  , mkEqnTy
+  )
+where
+
+import Test.Speculate.Expr.Core
+import Test.Speculate.Expr.Match
+import Test.Speculate.Utils hiding (ord)
+import Test.LeanCheck
+import Test.LeanCheck.Utils hiding (comparison)
+import Test.LeanCheck.Error (errorToFalse)
+import Data.Dynamic
+
+import Data.Maybe (isJust,fromMaybe,listToMaybe,catMaybes,mapMaybe)
+import Data.List (find,(\\))
+import Data.Monoid ((<>))
+
+
+-- | Type information needed to Speculate expressions (single type / single class).
+data Instance = Instance String TypeRep [Expr]
+  deriving Show
+
+instance Eq Instance where
+  Instance s1 t1 _ == Instance s2 t2 _  =  s1 == s2 && t1 == t2
+
+instance Ord Instance where
+  Instance s1 t1 _ `compare` Instance s2 t2 _  =  s1 `compare` s2 <> t1 `compare` t2
+
+
+-- | Type information needed to Speculate expressions.
+type Instances = [Instance]
+
+instanceType :: Instance -> TypeRep
+instanceType (Instance _ t _)  =  t
+
+-- | Usage: @ins1 "x" (undefined :: Type)@
+ins1 :: (Typeable a, Listable a, Show a, Eq a, Ord a)
+          => String -> a -> Instances
+ins1 n x = eq x ++ ord x ++ listable x ++ name n x
+
+ins :: (Typeable a, Listable a, Show a, Eq a, Ord a)
+    => String -> a -> Instances
+ins n x = concat
+  [    x      / n
+
+  ,   [x]     / n ++ "s"
+  ,  [[x]]    / n ++ "ss"
+--, [[[x]]]   / n ++ "ss"
+
+  , (x,x)     / n ++ m
+  , (x,x,x)   / n ++ m ++ o
+--, (x,x,x,x) / n ++ m ++ o ++ p
+
+  , [(x,x)]   / n ++ m ++ "s"
+--, [(x,x,x)] / n ++ m ++ o ++ "ss"
+
+--, (x,[x])   / n ++ m ++ "s"
+--, ([x],x)   / n ++ "s" ++ m
+--, ([x],[x]) / n ++ "s" ++ m ++ "s"
+--, (x,(x,x)) / n ++ m ++ o
+--, ((x,x),x) / n ++ m ++ o
+
+  , mayb x    / "m" ++ n ++ "1"
+--, eith x x  / "e" ++ n ++ o ++ "1"
+  ]
+  where
+  (/) :: (Typeable a, Listable a, Show a, Eq a, Ord a)
+      => a -> String -> Instances -- monomorphism restriction strikes again
+  (/) = flip ins1
+  infixr 0 /
+  m = namesFromTemplate n !! 1
+  o = namesFromTemplate m !! 1
+  p = namesFromTemplate o !! 1
+-- NOTE: the function typeInfoN is not perfect: it won't help produce types
+-- combining different sub-types, like for example: (Bool,Int).  But it is
+-- way better than the original version in which I had to explictly define
+-- everything.  A definitive solution is still to be thought of.
+-- NOTE: see related TODO on the definition of basicInstances
+
+eq :: (Typeable a, Eq a) => a -> Instances
+eq x = eqWith $ (==) -:> x
+
+ord :: (Typeable a, Ord a) => a -> Instances
+ord x = ordWith $ (<=) -:> x
+
+eqOrd :: (Typeable a, Eq a, Ord a) => a -> Instances
+eqOrd x = eq x ++ ord x
+
+listable :: (Typeable a, Show a, Listable a) => a -> Instances
+listable x = listableWith $ tiers `asTypeOf` [[x]]
+
+name :: Typeable a => String -> a -> Instances
+name n x = [ Instance "Names" (typeOf x)
+               [constant "names" $ namesFromTemplate n] ]
+
+eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances
+eqWith (==) = [ Instance "Eq" (typeOf $ arg (==))
+                  [constant "==" $ errorToFalse .: (==)] ]
+  where
+  arg :: (a -> b) -> a
+  arg _ = undefined
+
+ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances
+ordWith (<=) = [ Instance "Ord" (typeOf $ arg (<=))
+                   [ constant "<=" $ errorToFalse .: (<=)
+                   , constant "<"  $ (errorToFalse . not) .: flip (<=) ] ]
+  where
+  arg :: (a -> b) -> a
+  arg _ = undefined
+
+listableWith :: (Typeable a, Show a) => [[a]] -> Instances
+listableWith xss = [ Instance "Listable" (typeOf $ head $ head xss)
+                       [constant "tiers" $ mapT showConstant xss] ]
+
+isEq :: Instances -> TypeRep -> Bool
+isEq ti = isJust . eqE ti
+
+isOrd :: Instances -> TypeRep -> Bool
+isOrd ti = isJust . ltE ti
+
+isEqOrd :: Instances -> TypeRep -> Bool
+isEqOrd ti t = isOrd ti t && isEq ti t
+
+isEqE :: Instances -> Expr -> Bool
+isEqE ti = isEq ti . typ
+
+isOrdE :: Instances -> Expr -> Bool
+isOrdE ti = isOrd ti . typ
+
+isEqOrdE :: Instances -> Expr -> Bool
+isEqOrdE ti = isEqOrd ti . typ
+
+isListable :: Instances -> TypeRep -> Bool
+isListable ti t = isJust $ findInfo m ti
+  where
+  m (Instance "Listable" t' ts) | t' == t = Just ts
+  m _                                     = Nothing
+
+-- TODO: implement above using something similar to the following
+-- isComparable ti = isJust . (`findInfo` ti) . typ
+
+findInfo :: (Instance -> Maybe a) -> Instances -> Maybe a
+findInfo may = listToMaybe . mapMaybe may
+
+findInfoOr :: a -> (Instance -> Maybe a) -> Instances -> a
+findInfoOr def may = fromMaybe def . findInfo may
+
+names :: Instances -> TypeRep -> [String]
+names ti t = findInfoOr defNames m ti
+  where
+  m (Instance "Names" t' [ns]) | t == t' = Just $ eval defNames ns
+  m _                                    = Nothing
+
+tiersE :: Instances -> TypeRep -> [[Expr]]
+tiersE ti t = findInfoOr (error $ "could not find Listable " ++ show t) m ti
+  where
+  m (Instance "Listable" t' [ts]) | t == t' = Just $ eval (error $ "invalid Listable " ++ show t) ts
+  m _                                       = Nothing
+
+eqE :: Instances -> TypeRep -> Maybe Expr
+eqE ti t = findInfo m ti
+  where
+  m (Instance "Eq" t' [eq]) | t == t' = Just eq
+  m _                                 = Nothing
+
+ltE :: Instances -> TypeRep -> Maybe Expr
+ltE ti t = findInfo m ti
+  where
+  m (Instance "Ord" t' [_,lt]) | t == t' = Just lt
+  m _                                    = Nothing
+
+leE :: Instances -> TypeRep -> Maybe Expr
+leE ti t = findInfo m ti
+  where
+  m (Instance "Ord" t' [le,_]) | t == t' = Just le
+  m _                                    = Nothing
+
+deriving instance Typeable Word2 -- for GHC <= 7.8
+
+-- TODO: include *ALL* prelude types on basicInstances
+preludeInstances :: Instances
+preludeInstances = concat
+  [ ins1 "x"  (undefined :: ())
+  , ins1 "xs" (undefined :: [()])
+
+  , ins "p" (undefined :: Bool)
+
+  , ins "x" (undefined :: Int)
+--, ins "x" (undefined :: Word)
+  , ins "x" (undefined :: Integer)
+
+  , ins "o" (undefined :: Ordering)
+  , ins "c" (undefined :: Char)
+
+  , ins "q" (undefined :: Rational)
+  , ins "f" (undefined :: Float)
+  , ins "f" (undefined :: Double)
+
+-- TODO: uncomment the following and investigate why compilation takes so long
+--, ins "x" (undefined :: Int1)
+--, ins "x" (undefined :: Int2)
+--, ins "x" (undefined :: Int3)
+--, ins "x" (undefined :: Int4)
+--, ins "x" (undefined :: Word1)
+  , ins "x" (undefined :: Word2)
+--, ins "x" (undefined :: Word3)
+--, ins "x" (undefined :: Word4)
+--, ins "x" (undefined :: Nat1)
+--, ins "x" (undefined :: Nat2)
+--, ins "x" (undefined :: Nat3)
+--, ins "x" (undefined :: Nat4)
+--, ins "x" (undefined :: Nat5)
+--, ins "x" (undefined :: Nat6)
+--, ins "x" (undefined :: Nat7)
+  ]
+-- WHOA!  Have I discovered a "bug" in GHC?  adding to many type compositions
+-- on ins and types on preludeInstances makes compilation of this module
+-- *really* slow: it takes a whopping 2 minutes!
+-- (the above report is using -O2, I have not tested without optimizations).
+
+
+defNames :: [String]
+defNames = namesFromTemplate "x"
diff --git a/src/Test/Speculate/Expr/Match.hs b/src/Test/Speculate/Expr/Match.hs
--- a/src/Test/Speculate/Expr/Match.hs
+++ b/src/Test/Speculate/Expr/Match.hs
@@ -150,24 +150,45 @@
           | otherwise = const Nothing
 
 unify :: Expr -> Expr -> Maybe Expr
-unify e1 e2 = (e1' `assigning`) <$> unification e1' e2'
-  where
-  e1' = renameBy (++ "1") e1
-  e2' = renameBy (++ "2") e2
+unify e1 e2 = (e1 `assigning`) <$> unification e1 e2
 
--- NOTE: Take care of passing disjoing variable namespaces on both expressions!
--- see unify for an example of that.
 unification :: Expr -> Expr -> Maybe Binds
-unification e1' e2' = u e1' e2' []
+unification = naiveUnification
+
+findBind :: Expr -> Expr -> Either Bool (String,Expr)
+findBind e1         e2          |  typ e1 /= typ e2  =  Left False
+                                |  e1 == e2          =  Left True
+findBind (Var s t)  e2          =  Right (s,e2)
+findBind e1         (Var s t)   =  Right (s,e1)
+findBind (f1 :$ x1) (f2 :$ x2)  =  case findBind f1 f2 of
+                                   Left True -> findBind x1 x2
+                                   r         -> r
+findBind e1         e2          =  Left (e1 == e2)
+
+-- NOTE: there are faster methods for unification.
+naiveUnification :: Expr -> Expr -> Maybe Binds
+naiveUnification e1' e2' = uu e1' e2' []
   where
-  u :: Expr -> Expr -> Binds -> Maybe Binds
-  u e1 e2 | typ e1 /= typ e2 = const Nothing
-  u e1@(Var s1 t1) e2@(Var s2 t2) = updateAssignments s1 e2 >=> updateAssignments s2 e1
-  u e1 (Var s t) = updateAssignments s e1
-  u (Var s t) e2 = updateAssignments s e2
-  u (f1 :$ x1) (f2 :$ x2) = u f1 f2 >=> u x1 x2
-  u e1 e2 | e1 == e2  = Just
-          | otherwise = const Nothing
+  uu :: Expr -> Expr -> Binds -> Maybe Binds
+  uu e1' e2' bs' =
+    case u e1' e2' bs' of
+      Nothing -> Nothing
+      Just (e1,e2,bs) ->
+        if e1' == e1 && e2' == e2
+        then Just bs
+        else uu e1 e2 bs
+  u :: Expr -> Expr -> Binds -> Maybe (Expr,Expr,Binds)
+  u e1 e2 bs =
+    case findBind e1 e2 of
+    Left False -> Nothing
+    Left True  -> Just (e1,e2,bs)
+    Right (s,e) ->
+      if (Var s (typ e)) `isSub` e
+      then Nothing
+      else Just ( e1 `assigning` [(s,e)]
+                , e2 `assigning` [(s,e)]
+                , (s,e):[(s',e' `assigning` [(s,e)]) | (s',e') <- bs]
+                )
 
 -- 0 `isInstanceOf` x = True
 -- y `isInstanceOf` x = True
diff --git a/src/Test/Speculate/Expr/TypeInfo.hs b/src/Test/Speculate/Expr/TypeInfo.hs
deleted file mode 100644
--- a/src/Test/Speculate/Expr/TypeInfo.hs
+++ /dev/null
@@ -1,255 +0,0 @@
-{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC <= 7.8
--- |
--- Module      : Test.Speculate.Expr.TypeInfo
--- Copyright   : (c) 2016-2017 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- This module is part of Speculate.
---
--- Typeclass instance information.
-module Test.Speculate.Expr.TypeInfo
-  ( Instances
-  , Instance (..)
-  , TypeRep
-
-  -- * Smart constructors
-  , ins
-  , eq,       eqWith
-  , ord,      ordWith
-  , eqOrd
-  , listable, listableWith
-
-  -- * Queries on Instances
-  , instanceType
-  , findInfo
-  , names
-  , eqE,      isEq,       isEqE
-  , leE, ltE, isOrd,      isOrdE
-  ,           isEqOrd,    isEqOrdE
-  , tiersE,   isListable
-
-  -- * Type info for standard Haskell types
-  , preludeInstances
-
-  -- * Does not belong here?
-  , defNames
-
-  , boolTy
-  , mkEqnTy
-  )
-where
-
-import Test.Speculate.Expr.Core
-import Test.Speculate.Expr.Match
-import Test.Speculate.Utils hiding (ord)
-import Test.LeanCheck
-import Test.LeanCheck.Utils hiding (comparison)
-import Test.LeanCheck.Error (errorToFalse)
-import Data.Dynamic
-
-import Data.Maybe (isJust,fromMaybe,listToMaybe,catMaybes,mapMaybe)
-import Data.List (find,(\\))
-
-
--- | Type information needed to Speculate expressions (single type / single class).
-data Instance = Eq TypeRep Expr
-              | Ord TypeRep Expr Expr
-              | Listable TypeRep [[Expr]]
-              | Names TypeRep [String]
-
--- | Type information needed to Speculate expressions.
-type Instances = [Instance]
-
-instanceType :: Instance -> TypeRep
-instanceType (Eq       t _)   = t
-instanceType (Ord      t _ _) = t
-instanceType (Listable t _)   = t
-instanceType (Names    t _)   = t
-
--- | Usage: @ins1 "x" (undefined :: Type)@
-ins1 :: (Typeable a, Listable a, Show a, Eq a, Ord a)
-          => String -> a -> Instances
-ins1 n x = eq x ++ ord x ++ listable x ++ name n x
-
-ins :: (Typeable a, Listable a, Show a, Eq a, Ord a)
-    => String -> a -> Instances
-ins n x = concat
-  [    x      / n
-
-  ,   [x]     / n ++ "s"
-  ,  [[x]]    / n ++ "ss"
---, [[[x]]]   / n ++ "ss"
-
-  , (x,x)     / n ++ m
-  , (x,x,x)   / n ++ m ++ o
---, (x,x,x,x) / n ++ m ++ o ++ p
-
-  , [(x,x)]   / n ++ m ++ "s"
---, [(x,x,x)] / n ++ m ++ o ++ "ss"
-
---, (x,[x])   / n ++ m ++ "s"
---, ([x],x)   / n ++ "s" ++ m
---, ([x],[x]) / n ++ "s" ++ m ++ "s"
---, (x,(x,x)) / n ++ m ++ o
---, ((x,x),x) / n ++ m ++ o
-
-  , mayb x    / "m" ++ n ++ "1"
---, eith x x  / "e" ++ n ++ o ++ "1"
-  ]
-  where
-  (/) :: (Typeable a, Listable a, Show a, Eq a, Ord a)
-      => a -> String -> Instances -- monomorphism restriction strikes again
-  (/) = flip ins1
-  infixr 0 /
-  m = namesFromTemplate n !! 1
-  o = namesFromTemplate m !! 1
-  p = namesFromTemplate o !! 1
--- NOTE: the function typeInfoN is not perfect: it won't help produce types
--- combining different sub-types, like for example: (Bool,Int).  But it is
--- way better than the original version in which I had to explictly define
--- everything.  A definitive solution is still to be thought of.
--- NOTE: see related TODO on the definition of basicInstances
-
-eq :: (Typeable a, Eq a) => a -> Instances
-eq x = eqWith $ (==) -:> x
-
-ord :: (Typeable a, Ord a) => a -> Instances
-ord x = ordWith $ (<=) -:> x
-
-eqOrd :: (Typeable a, Eq a, Ord a) => a -> Instances
-eqOrd x = eq x ++ ord x
-
-listable :: (Typeable a, Show a, Listable a) => a -> Instances
-listable x = listableWith $ tiers `asTypeOf` [[x]]
-
-name :: Typeable a => String -> a -> Instances
-name n x = [Names (typeOf x) (namesFromTemplate n)]
-
-eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances
-eqWith (==) = [Eq (typeOf $ arg (==)) $ constant "==" $ errorToFalse .: (==)]
-  where
-  arg :: (a -> b) -> a
-  arg _ = undefined
-
-ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances
-ordWith (<=) = [Ord (typeOf $ arg (<=))
-                    (constant "<=" (errorToFalse .: (<=)))
-                    (constant "<"  ((errorToFalse . not) .: flip (<=)))]
-  where
-  arg :: (a -> b) -> a
-  arg _ = undefined
-
-listableWith :: (Typeable a, Show a) => [[a]] -> Instances
-listableWith xss =
-  [Listable (typeOf $ head $ head xss) (mapT showConstant xss)]
-
-isEq :: Instances -> TypeRep -> Bool
-isEq ti = isJust . eqE ti
-
-isOrd :: Instances -> TypeRep -> Bool
-isOrd ti = isJust . ltE ti
-
-isEqOrd :: Instances -> TypeRep -> Bool
-isEqOrd ti t = isOrd ti t && isEq ti t
-
-isEqE :: Instances -> Expr -> Bool
-isEqE ti = isEq ti . typ
-
-isOrdE :: Instances -> Expr -> Bool
-isOrdE ti = isOrd ti . typ
-
-isEqOrdE :: Instances -> Expr -> Bool
-isEqOrdE ti = isEqOrd ti . typ
-
-isListable :: Instances -> TypeRep -> Bool
-isListable ti t = isJust $ findInfo m ti
-  where
-  m (Listable t' ts) | t' == t = Just ts
-  m _                          = Nothing
-
--- TODO: implement above using something similar to the following
--- isComparable ti = isJust . (`findInfo` ti) . typ
-
-findInfo :: (Instance -> Maybe a) -> Instances -> Maybe a
-findInfo may = listToMaybe . mapMaybe may
-
-findInfoOr :: a -> (Instance -> Maybe a) -> Instances -> a
-findInfoOr def may = fromMaybe def . findInfo may
-
-names :: Instances -> TypeRep -> [String]
-names ti t = findInfoOr defNames m ti
-  where
-  m (Names t' ns) | t == t' = Just ns
-  m _                       = Nothing
-
-tiersE :: Instances -> TypeRep -> [[Expr]]
-tiersE ti t = findInfoOr (error $ "could not find Listable " ++ show t) m ti
-  where
-  m (Listable t' ts) | t == t' = Just ts
-  m _                          = Nothing
-
-eqE :: Instances -> TypeRep -> Maybe Expr
-eqE ti t = findInfo m ti
-  where
-  m (Eq t' eq) | t == t' = Just eq
-  m _                    = Nothing
-
-ltE :: Instances -> TypeRep -> Maybe Expr
-ltE ti t = findInfo m ti
-  where
-  m (Ord t' _ lt) | t == t' = Just lt
-  m _                       = Nothing
-
-leE :: Instances -> TypeRep -> Maybe Expr
-leE ti t = findInfo m ti
-  where
-  m (Ord t' le _) | t == t' = Just le
-  m _                       = Nothing
-
-deriving instance Typeable Word2 -- for GHC <= 7.8
-
--- TODO: include *ALL* prelude types on basicInstances
-preludeInstances :: Instances
-preludeInstances = concat
-  [ ins1 "x"  (undefined :: ())
-  , ins1 "xs" (undefined :: [()])
-
-  , ins "p" (undefined :: Bool)
-
-  , ins "x" (undefined :: Int)
---, ins "x" (undefined :: Word)
-  , ins "x" (undefined :: Integer)
-
-  , ins "o" (undefined :: Ordering)
-  , ins "c" (undefined :: Char)
-
-  , ins "q" (undefined :: Rational)
-  , ins "f" (undefined :: Float)
-  , ins "f" (undefined :: Double)
-
--- TODO: uncomment the following and investigate why compilation takes so long
---, ins "x" (undefined :: Int1)
---, ins "x" (undefined :: Int2)
---, ins "x" (undefined :: Int3)
---, ins "x" (undefined :: Int4)
---, ins "x" (undefined :: Word1)
-  , ins "x" (undefined :: Word2)
---, ins "x" (undefined :: Word3)
---, ins "x" (undefined :: Word4)
---, ins "x" (undefined :: Nat1)
---, ins "x" (undefined :: Nat2)
---, ins "x" (undefined :: Nat3)
---, ins "x" (undefined :: Nat4)
---, ins "x" (undefined :: Nat5)
---, ins "x" (undefined :: Nat6)
---, ins "x" (undefined :: Nat7)
-  ]
--- WHOA!  Have I discovered a "bug" in GHC?  adding to many type compositions
--- on ins and types on preludeInstances makes compilation of this module
--- *really* slow: it takes a whopping 2 minutes!
--- (the above report is using -O2, I have not tested without optimizations).
-
-
-defNames :: [String]
-defNames = namesFromTemplate "x"
diff --git a/src/Test/Speculate/Utils/Typeable.hs b/src/Test/Speculate/Utils/Typeable.hs
--- a/src/Test/Speculate/Utils/Typeable.hs
+++ b/src/Test/Speculate/Utils/Typeable.hs
@@ -67,7 +67,7 @@
 unFunTy :: TypeRep -> (TypeRep,TypeRep)
 unFunTy t
   | isFunTy t = let (f,[a,b]) = splitTyConApp t in (a,b)
-  | otherwise = error "unFunTy: not a function type"
+  | otherwise = error $ "error (unFunTy): `" ++ show t ++ "` is not a function type"
 
 argumentTy :: TypeRep -> TypeRep
 argumentTy = fst . unFunTy
diff --git a/tests/Test.hs b/tests/Test.hs
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -49,6 +49,7 @@
   , ii, jj, kk, ii'
   , negate'
   , ff, gg
+  , ff2, hh2, hh3, hh4, hh5, hh6, hh7
   , succ'
 
   , idE
@@ -67,10 +68,13 @@
   , odd', even'
 
   -- ** Characters
-  , aa
+  , aa, bb
+  , space, lineBreak
   , cc, dd
   , ord'
   , ordE
+  , emptyString
+  , ccs
 
   -- ** Lists (of Inteters)
   , ll
@@ -350,7 +354,39 @@
 gg :: Expr -> Expr
 gg = (ggE :$) where ggE = constant "g" (undefined :: Int -> Int)
 
+ff2 :: Expr -> Expr -> Expr
+ff2 e1 e2 = ffE :$ e1 :$ e2
+  where ffE = constant "f" (undefined :: Int -> Int -> Int)
 
+hh2 :: Expr -> Expr -> Expr
+hh2 e1 e2 = hhE :$ e1 :$ e2
+  where hhE = constant "h" (undefined :: Int -> Int -> Int)
+
+hh3 :: Expr -> Expr -> Expr -> Expr
+hh3 e1 e2 e3 = hhE :$ e1 :$ e2 :$ e3
+  where hhE = constant "h" (undefined :: Int -> Int -> Int -> Int)
+
+hh4 :: Expr -> Expr -> Expr -> Expr -> Expr
+hh4 e1 e2 e3 e4 = hhE :$ e1 :$ e2 :$ e3 :$ e4
+  where hhE = constant "h" (undefined :: Int -> Int -> Int -> Int -> Int)
+
+hh5 :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr
+hh5 e1 e2 e3 e4 e5 = hhE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5
+  where hhE = constant "h" (undefined :: Int -> Int -> Int -> Int -> Int -> Int)
+
+hh6 :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr
+hh6 e1 e2 e3 e4 e5 e6 = hhE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5 :$ e6
+  where hhE = constant "h" (undefined :: Int -> Int -> Int -> Int -> Int -> Int -> Int)
+
+hh7 :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr
+hh7 e1 e2 e3 e4 e5 e6 e7 = hhE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5 :$ e6 :$ e7
+  where hhE = constant "h" (undefined :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int)
+
+-- unification (hh5 yy zz (ff2 ii ii) (ff2 jj jj) kk) (hh5 (ff2 xx xx) (ff2 yy yy) jj kk zz)
+
+-- unification (hh7 yy zz xx' (ff2 ii ii) (ff2 jj jj) (ff2 kk kk) ii')
+--             (hh7 (ff2 xx xx) (ff2 yy yy) (ff2 zz zz) jj kk ii' xx')
+
 true :: Expr
 true = showConstant (True :: Bool)
 
@@ -406,9 +442,18 @@
 even' = (evenE :$) where evenE = constant "even" (even :: Int -> Bool)
 
 
-aa :: Expr -- a, the character, not variable
+aa :: Expr -- a, the character, not a variable
 aa = showConstant 'a'
 
+bb :: Expr -- bee, the character, not a variable
+bb = showConstant 'b'
+
+space :: Expr -- space, the character
+space = showConstant ' '
+
+lineBreak :: Expr -- lineBreak, the character
+lineBreak = showConstant '\n'
+
 cc :: Expr -- cee, a variable character
 cc = var "c" char
 
@@ -421,7 +466,13 @@
 ordE :: Expr
 ordE = constant "ord" Data.Char.ord
 
+emptyString :: Expr
+emptyString = showConstant ""
 
+ccs :: Expr -- cees
+ccs = var "cs" [char]
+
+
 ll :: Expr
 ll = showConstant ([] :: [Int])
 
@@ -432,7 +483,11 @@
 yys = var "ys" [int]
 
 (-:-) :: Expr -> Expr -> Expr
-e1 -:- e2 = consE :$ e1 :$ e2
+e1 -:- e2
+  | typ e1 == typeOf (undefined :: Int)  = consE :$ e1 :$ e2
+  | typ e1 == typeOf (undefined :: Char) = stringConsE :$ e1 :$ e2
+  where
+  stringConsE = constant ":" ((:) :: Char -> String -> String)
 infixr 5 -:-
 
 consE :: Expr
@@ -460,8 +515,9 @@
 sort' :: Expr -> Expr
 sort' exs = sortE :$ exs where sortE = constant "sort" (sort :: [Int] -> [Int])
 
--- boolTy already exported by Speculate.TypeInfo
 
+-- boolTy already exported by Speculate.Instance
+
 intTy :: TypeRep
 intTy = typeOf int
 
@@ -647,3 +703,5 @@
 -- TODO: maybe use expressionsT as the main function to generate Exprs.
 -- By using it, I speculate a 20% increase in runtime.  But the code will
 -- certainly be smaller and easier to maintain.
+
+instance Listable Instance where list = preludeInstances
diff --git a/tests/test-expr.hs b/tests/test-expr.hs
--- a/tests/test-expr.hs
+++ b/tests/test-expr.hs
@@ -16,7 +16,6 @@
 -- for Travis:
 deriving instance Typeable Thyght
 deriving instance Typeable Equation
-deriving instance Typeable Expr
 
 main :: IO ()
 main = mainTest tests 10000
@@ -41,6 +40,7 @@
 
 
   , holds n $ okEqOrd -:> expr
+  , holds n $ okEqOrd -:> (undefined :: Instance)
   , holds n $ compare ==== compareComplexity
   , holds n $ LC.comparison lexicompare
   , holds n $ LC.comparison compareComplexity
@@ -100,22 +100,6 @@
   , renameBy (\(c:cs) -> succ c:cs) ((xx -+- yy) -+- ord' cc)
                                  == ((yy -+- zz) -+- ord' dd)
 
-  , unification xx yy == Just [("y",xx),("x",yy)]
-  , (canonicalize <$> unify xx yy) == Just xx
-  , unification zero zero == Just []
-  , unification zero one  == Nothing
-  , unification xx one == Just [("x",one)]
-  , unification (zero -+- xx) (zero -+- one) == Just [("x",one)]
-  , unification (zero -+- xx) (yy -+- one) == Just [("x",one),("y",zero)]
-  , unify (zero -+- xx) (yy -+- one) == Just (zero -+- one)
-  , unification (ff xx) (ff (gg yy)) == Just [("x",gg yy)]
-  , unification (ff xx -+- xx) (yy -+- zero) == Just [("x",zero),("y",ff xx)]
-  , unify (ff xx -+- xx) (yy -+- zero) == Just (ff zero -+- zero)
-  , unification (ff xx) (gg yy) == Nothing
-  , unification (ff xx) (ff yy) == unification xx yy
-  , (canonicalize <$> unify (negate' (negate' xx) -+- yy) (xx -+- zero))
-    == Just (negate' (negate' xx) -+- zero)
-
   , canonicalize (xx -+- yy)
               == (xx -+- yy)
   , canonicalize (jj -+- (ii -+- ii))
@@ -209,4 +193,15 @@
 #endif
 
   , holds n $ \e1 e2 -> e1 `isSub` e2 == (e1 `elem` subexprsV e2)
+
+  , show (emptyString) == "\"\" :: [Char]"
+  , show (space -:- emptyString) == "\" \" :: [Char]"
+  , show (space -:- ccs)         == "' ':cs :: [Char]"
+  , show (aa -:- bb -:- emptyString) == "\"ab\" :: [Char]"
+  , show (aa -:- bb -:- ccs)         == "'a':'b':cs :: [Char]"
+  , show (aa -:- space -:- bb -:- lineBreak -:- emptyString) == "\"a b\\n\" :: [Char]"
+  , show (cc -:- space -:- dd -:- lineBreak -:- emptyString) == "c:' ':d:\"\\n\" :: [Char]"
+  , show (cc -:- space -:- dd -:- lineBreak -:- ccs)         == "c:' ':d:'\\n':cs :: [Char]"
+  , show (cc -:- aa -:- bb -:- emptyString) == "c:\"ab\" :: [Char]"
+  , show (cc -:- aa -:- bb -:- space -:- aa -:- bb -:- emptyString) == "c:\"ab ab\" :: [Char]"
   ]