diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.5.3
+Version:		0.6
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -98,6 +98,9 @@
   testsuite/tests/Data_Test.hs,
   testsuite/tests/Data/Comp_Test.hs,
   testsuite/tests/Data/Comp/Equality_Test.hs,
+  testsuite/tests/Data/Comp/Variables_Test.hs,
+  testsuite/tests/Data/Comp/Multi_Test.hs,
+  testsuite/tests/Data/Comp/Multi/Variables_Test.hs,
   testsuite/tests/Data/Comp/Examples_Test.hs,
   testsuite/tests/Data/Comp/Examples/Comp.hs,
   testsuite/tests/Data/Comp/Examples/Multi.hs,
@@ -171,6 +174,7 @@
                         Data.Comp.Automata.Product,
                         Data.Comp.Number,
                         Data.Comp.Thunk,
+                        Data.Comp.Ops,
 
                         Data.Comp.Multi,
                         Data.Comp.Multi.Term,
@@ -185,7 +189,7 @@
                         Data.Comp.Multi.Ordering,
                         Data.Comp.Multi.Variables,
                         Data.Comp.Multi.Ops,
-                        Data.Comp.Ops,
+                        Data.Comp.Multi.Number,
                         Data.Comp.Multi.Derive
                         Data.Comp.Multi.Generic,
                         Data.Comp.Multi.Desugar,
@@ -281,7 +285,7 @@
   Type:                 exitcode-stdio-1.0
   Main-is:		Data_Test.hs
   hs-source-dirs:	src testsuite/tests examples
-  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers
+  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers
 
 Executable benchmark
   Main-is:		Benchmark.hs
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -26,6 +26,7 @@
       QHom
     , below
     , above
+    , pureHom
     -- ** Bottom-Up State Propagation
     , upTrans
     , runUpHom
@@ -141,17 +142,13 @@
                            
 type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
 
--- -- | This type represents (pure, i.e. stateless) homomorphism by
--- -- universally quantifying over the state type.
--- type PHom f g = forall q . QHom f q g
 
--- -- | This combinator runs a stateless homomorphism. (use
--- -- 'Data.Comp.Algebra.appHom' instead).
--- runPHom :: forall f g . (Functor f, Functor g) => PHom f g -> CxtFun f g
--- runPHom hom = run where
---     run :: CxtFun f g
---     run (Hole x) = Hole x
---     run (Term t) = appCxt (explicit () (const ()) hom (fmap run t))
+-- | This function turns a stateful homomorphism with a fully
+-- polymorphic state type into a (stateless) homomorphism.
+pureHom :: (forall q . QHom f q g) -> Hom f g
+pureHom phom t = let ?above = undefined 
+                     ?below = const undefined
+                 in phom t
 
 -- | This type represents transition functions of deterministic
 -- bottom-up tree transducers (DUTTs).
diff --git a/src/Data/Comp/Matching.hs b/src/Data/Comp/Matching.hs
--- a/src/Data/Comp/Matching.hs
+++ b/src/Data/Comp/Matching.hs
@@ -24,9 +24,10 @@
 import Data.Comp.Variables
 import qualified Data.Map as Map
 import Data.Map (Map)
+import Data.Traversable
 import Data.Foldable
 
-import Prelude hiding (mapM_, all)
+import Prelude hiding (mapM_, mapM, all)
 
 {-| This is an auxiliary function for implementing 'matchCxt'. It behaves
 similarly as 'match' but is oblivious to non-linearity. Therefore, the
@@ -70,7 +71,7 @@
 {-| This function is similar to 'matchCxt' but instead of a context it
 matches a term with variables against a context.  -}
 
-matchTerm :: (Ord v, EqF f, Eq (Cxt h f a) , Functor f, Foldable f, HasVars f v)
+matchTerm :: (Ord v, EqF f, Eq (Cxt h f a) , Traversable f, HasVars f v)
           => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v)
 matchTerm t = matchCxt (varsToHoles t)
 
diff --git a/src/Data/Comp/Multi/Equality.hs b/src/Data/Comp/Multi/Equality.hs
--- a/src/Data/Comp/Multi/Equality.hs
+++ b/src/Data/Comp/Multi/Equality.hs
@@ -37,8 +37,8 @@
 instance Eq a => KEq (K a) where
     keq (K x) (K y) = x == y
 
-instance KEq a => Eq (A a) where
-     A x == A y = x `keq`  y
+instance KEq a => Eq (E a) where
+     E x == E y = x `keq`  y
 
 {-|
   'EqF' is propagated through sums.
@@ -69,7 +69,7 @@
 consisting of corresponding components of the two functorial
 values. -}
 
-heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]
+heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(E a, E b)]
 heqMod s t
     | unit s `eqHF` unit' t = Just args
     | otherwise = Nothing
diff --git a/src/Data/Comp/Multi/Generic.hs b/src/Data/Comp/Multi/Generic.hs
--- a/src/Data/Comp/Multi/Generic.hs
+++ b/src/Data/Comp/Multi/Generic.hs
@@ -30,19 +30,19 @@
 
 -- | This function returns a list of all subterms of the given
 -- term. This function is similar to Uniplate's @universe@ function.
-subterms :: forall f  . HFoldable f => Term f  :=> [A (Term f)]
+subterms :: forall f  . HFoldable f => Term f  :=> [E (Term f)]
 subterms t = build (f t)
-    where f :: Term f :=> (A (Term f) -> b -> b) -> b -> b
-          f t cons nil = A t `cons` hfoldl (\u s -> f s cons u) nil (unTerm t)
+    where f :: Term f :=> (E (Term f) -> b -> b) -> b -> b
+          f t cons nil = E t `cons` hfoldl (\u s -> f s cons u) nil (unTerm t)
 
 -- | This function returns a list of all subterms of the given term
 -- that are constructed from a particular functor.
-subterms' :: forall f g . (HFoldable f, g :<: f) => Term f :=> [A (g (Term f))]
+subterms' :: forall f g . (HFoldable f, g :<: f) => Term f :=> [E (g (Term f))]
 subterms' (Term t) = build (f t)
-    where f :: f (Term f) :=> (A (g (Term f)) -> b -> b) -> b -> b
+    where f :: f (Term f) :=> (E (g (Term f)) -> b -> b) -> b -> b
           f t cons nil = let rest = hfoldl (\u (Term s) -> f s cons u) nil t
                          in case proj t of
-                              Just t' -> A t' `cons` rest
+                              Just t' -> E t' `cons` rest
                               Nothing -> rest
 
 -- | This function transforms every subterm according to the given
@@ -66,12 +66,12 @@
 --     where run i@(Term t) = foldl (\s x -> s `c` run x) (q i) t
 query q c i@(Term t) = hfoldl (\s x -> s `c` query q c x) (q i) t
 
-subs :: HFoldable f => Term f  :=> [A (Term f)]
-subs = query (\x-> [A x]) (++)
+subs :: HFoldable f => Term f  :=> [E (Term f)]
+subs = query (\x-> [E x]) (++)
 
-subs' :: (HFoldable f, g :<: f) => Term f :=> [A (g (Term f))]
+subs' :: (HFoldable f, g :<: f) => Term f :=> [E (g (Term f))]
 subs' = mapMaybe pr . subs
-        where pr (A v) = fmap A (project v)
+        where pr (E v) = fmap E (project v)
 
 -- | This function computes the generic size of the given term,
 -- i.e. the its number of subterm occurrences.
diff --git a/src/Data/Comp/Multi/HFoldable.hs b/src/Data/Comp/Multi/HFoldable.hs
--- a/src/Data/Comp/Multi/HFoldable.hs
+++ b/src/Data/Comp/Multi/HFoldable.hs
@@ -56,8 +56,8 @@
                 mf Nothing (K y) = Just y
                 mf (Just x) (K y) = Just (f x y)
 
-htoList :: (HFoldable f) => f a :=> [A a]
-htoList = hfoldr (\ n l ->  A n : l) []
+htoList :: (HFoldable f) => f a :=> [E a]
+htoList = hfoldr (\ n l ->  E n : l) []
     
 kfoldr :: (HFoldable f) => (a -> b -> b) -> b -> f (K a) :=> b
 kfoldr f = hfoldr (\ (K x) y -> f x y)
diff --git a/src/Data/Comp/Multi/HFunctor.hs b/src/Data/Comp/Multi/HFunctor.hs
--- a/src/Data/Comp/Multi/HFunctor.hs
+++ b/src/Data/Comp/Multi/HFunctor.hs
@@ -23,6 +23,7 @@
      I (..),
      K (..),
      A (..),
+     E (..),
      (:.:)(..)
      ) where
 
@@ -35,7 +36,9 @@
 instance Functor (K a) where
     fmap _ (K x) = K x
 
-data A f = forall i. A {unA :: f i}
+data E f = forall i. E {unE :: f i}
+
+data A f = A {unA :: forall i. f i}
 
 instance Eq a => Eq (K a i) where
     K x == K y = x == y
diff --git a/src/Data/Comp/Multi/Number.hs b/src/Data/Comp/Multi/Number.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Multi/Number.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE TypeOperators #-}
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Multi.Number
+-- Copyright   :  (c) 2012 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+-- 
+-- This module provides functionality to number the components of a
+-- functorial value with consecutive integers.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Multi.Number 
+    ( Numbered (..)
+    , unNumbered
+    , number
+    , HTraversable ()) where
+
+import Data.Comp.Multi.HTraversable
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Ordering
+import Data.Comp.Multi.Equality
+
+
+import Control.Monad.State
+
+
+-- | This type is used for numbering components of a functorial value.
+newtype Numbered a i = Numbered (Int, a i)
+
+unNumbered :: Numbered a :-> a
+unNumbered (Numbered (_, x)) = x
+
+instance KEq (Numbered a) where
+  keq (Numbered (i,_))  (Numbered (j,_)) = i == j
+
+instance KOrd (Numbered a) where
+    kcompare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j
+
+-- | This function numbers the components of the given functorial
+-- value with consecutive integers starting at 0.
+number :: HTraversable f => f a :-> f (Numbered a)
+number x = fst $ runState (hmapM run x) 0 where
+  run b = do n <- get
+             put (n+1)
+             return $ Numbered (n,b)
diff --git a/src/Data/Comp/Multi/Ordering.hs b/src/Data/Comp/Multi/Ordering.hs
--- a/src/Data/Comp/Multi/Ordering.hs
+++ b/src/Data/Comp/Multi/Ordering.hs
@@ -33,8 +33,8 @@
 class EqHF f => OrdHF f where
     compareHF :: KOrd a => f a i -> f a j -> Ordering
 
---instance KOrd f => Ord (f i) where
---    compare = kcompare
+instance KOrd f => Ord (E f) where
+    compare (E x) (E y) = kcompare x y
 
 instance Ord a => KOrd (K a) where
     kcompare (K x) (K y) = compare x y
diff --git a/src/Data/Comp/Multi/Show.hs b/src/Data/Comp/Multi/Show.hs
--- a/src/Data/Comp/Multi/Show.hs
+++ b/src/Data/Comp/Multi/Show.hs
@@ -39,7 +39,7 @@
 instance (ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a) where
     kshow = free showHF kshow
 
-instance (KShow f) => Show (f i) where
+instance (KShow (Cxt h f a)) => Show (Cxt h f a i) where
     show = unK . kshow
 
 instance (ShowHF f, Show p) => ShowHF (f :&: p) where
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -31,30 +31,64 @@
     ) where
 
 import Data.Comp.Multi.Term
+import Data.Comp.Multi.Ordering
+import Data.Comp.Multi.Number
+import Data.Comp.Multi.Ops
 import Data.Comp.Multi.Algebra
 import Data.Comp.Multi.Derive
 import Data.Comp.Multi.HFunctor
 import Data.Comp.Multi.HFoldable
+import Data.Map (Map)
+import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Maybe
 
 
-type GSubst v a = NatM Maybe (K v) a
+type GSubst v a = Map v (A a)
 
 type CxtSubst h a f v =  GSubst v (Cxt h f a)
 
 type Subst f v = CxtSubst NoHole (K ()) f v
 
+type SubstFun v a = NatM Maybe (K v) a
+
+
+
+substFun :: Ord v => GSubst v a -> SubstFun v a
+substFun s (K v) = fmap unA $ Map.lookup v s
+
 {-| This multiparameter class defines functors with variables. An instance
   @HasVar f v@ denotes that values over @f@ might contain and bind variables of
   type @v@. -}
 class HasVars (f  :: (* -> *) -> * -> *) v where
+    -- | Indicates whether the @f@ constructor is a variable. The
+    -- default implementation returns @Nothing@.
     isVar :: f a :=> Maybe v
     isVar _ = Nothing
-    bindsVars :: f a :=> [v]
-    bindsVars _ = []
     
+    -- | Indicates the set of variables bound by the @f@ constructor
+    -- for each argument of the constructor. For example for a
+    -- non-recursive let binding:
+    -- @
+    -- data Let i e = Let Var (e i) (e i)
+    -- instance HasVars Let Var where
+    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]
+    -- @
+    -- If, instead, the let binding is recursive, the methods has to
+    -- be implemented like this:
+    -- @
+    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),
+    --                                         (y, (Set.singleton v))]
+    -- @
+    -- This indicates that the scope of the bound variable also
+    -- extends to the right-hand side of the variable binding.
+    --
+    -- The default implementation returns the empty map.
+    bindsVars :: KOrd a => f a :=> Map (E a) (Set v)
+    bindsVars _ = Map.empty
+
+$(derive [liftSum] [''HasVars])
+    
 -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
 -- @v@ is contained in the given set of variables.
     
@@ -64,66 +98,87 @@
                    then Nothing
                    else return v
 
-$(derive [liftSum] [''HasVars])
+-- | This combinator pairs every argument of a given constructor with
+-- the set of (newly) bound variables according to the corresponding
+-- 'HasVars' type class instance.
+getBoundVars :: forall f a v i . (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i
+getBoundVars t = let n :: f (Numbered a) i
+                     n = number t
+                     m :: Map (E (Numbered a)) (Set v)
+                     m = bindsVars n
+                     trans :: Numbered a :-> (a :*: K (Set v))
+                     trans x = unNumbered x :*: (K (Map.findWithDefault Set.empty (E x) m))
+                 in hfmap trans n
+                    
+-- | This combinator combines 'getBoundVars' with the 'mfmap' function.
+hfmapBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) 
+                  => (Set v -> a :-> b) -> f a i -> f b i
+hfmapBoundVars f t = let n :: f (Numbered a) i
+                         n = number t
+                         m :: Map (E (Numbered a)) (Set v)
+                         m = bindsVars n
+                         trans :: Numbered a :-> b
+                         trans x = f (Map.findWithDefault Set.empty (E x) m) (unNumbered x)
+                     in hfmap trans n
+                        
+-- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.   
+hfoldlBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) 
+                  => (b -> Set v ->  a :=> b) -> b -> f a i -> b
+hfoldlBoundVars f e t = let n :: f (Numbered a) i
+                            n = number t
+                            m :: Map (E (Numbered a)) (Set v)
+                            m = bindsVars n
+                            trans :: b -> Numbered a :=> b
+                            trans x y = f x (Map.findWithDefault Set.empty (E y) m) (unNumbered y)
+                       in hfoldl trans e n
 
-instance HasVars f v => HasVars (Cxt h f) v where
-    isVar (Term t) = isVar t
-    isVar _ = Nothing
-    bindsVars (Term t) = bindsVars t
-    bindsVars _ = []
 
+
 -- Auxiliary data type, used only to define varsToHoles
-data C a b i = C{ unC :: a -> b i }
+newtype C a b i = C{ unC :: a -> b i }
 
-varsToHoles :: forall f v. (HFunctor f, HasVars f v, Eq v) =>
+varsToHoles :: forall f v. (HTraversable f, HasVars f v, Ord v) =>
                 Term f :-> Context f (K v)
-varsToHoles t = unC (cata alg t) []
-    where alg :: (HFunctor f, HasVars f v, Eq v) =>
-                 Alg f (C [v] (Context f (K v)))
-          alg t = C $ \vars ->
-              let vars' = vars ++ bindsVars t in
-              case isVar t of
-                Just v ->
-                    -- Check for scope
-                    if v `elem` vars' then
-                        Term $ hfmap (`unC` vars') t
-                    else
-                        Hole $ K v
-                Nothing ->
-                    Term $ hfmap (`unC` vars') t
-
-containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> Alg f (K Bool)
-containsVarAlg v t = K $ v `notElem` bindsVars t &&
-                         (local || kfoldl (||) False t)
+varsToHoles t = unC (cata alg t) Set.empty
+    where alg :: (HTraversable f, HasVars f v, Ord v) => Alg f (C (Set v) (Context f (K v)))
+          alg t = C $ \vars -> case isVar t of
+            Just v | v `Set.member` vars -> Hole $ K v
+            _  -> Term $ hfmapBoundVars run t
+              where 
+                run :: Set v -> C (Set v) (Context f (K v))  :-> Context f (K v)
+                run newVars f = f `unC` (newVars `Set.union` vars)
+                
+-- | Convert variables to holes, except those that are bound.
+containsVarAlg :: forall v f . (Ord v, HasVars f v, HTraversable f) => v -> Alg f (K Bool)
+containsVarAlg v t = K $ hfoldlBoundVars run local t
     where local = case isVar t of
                     Just v' -> v == v'
                     Nothing -> False
+          run :: Bool -> Set v -> (K Bool i) -> Bool
+          run acc vars (K b) = acc || (not (v `Set.member` vars) && b)
 
 {-| This function checks whether a variable is contained in a context. -}
-containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f)
+containsVar :: (Ord v, HasVars f v, HTraversable f, HFunctor f)
             => v -> Cxt h f a :=> Bool
 containsVar v = unK . free (containsVarAlg v) (const $ K False)
 
-variableListAlg :: (HasVars f v, HFoldable f, Eq v) => Alg f (K [v])
-variableListAlg t = K $ filter (`notElem` bindsVars t) $ kfoldl (++) local t
-    where local = case isVar t of
-                    Just v -> [v]
-                    Nothing -> [] 
 
 {-| This function computes the list of variables occurring in a context. -}
-variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v)
+variableList :: (HasVars f v, HTraversable f, HFunctor f, Ord v)
              => Cxt h f a :=> [v]
-variableList = unK . free variableListAlg (const $ K [])
+variableList = Set.toList . variables
 
-variablesAlg :: (Ord v, HasVars f v, HFoldable f) => Alg f (K (Set v))
-variablesAlg t = K $ Set.filter (`notElem` bindsVars t) $
-                     kfoldl Set.union local t
+-- |Algebra for checking whether a variable is contained in a term, except those
+-- that are bound.
+variablesAlg :: (Ord v, HasVars f v, HTraversable f) => Alg f (K (Set v))
+variablesAlg t = K $ hfoldlBoundVars run local t
     where local = case isVar t of
                     Just v -> Set.singleton v
                     Nothing -> Set.empty
+          run acc bvars (K vars) = acc `Set.union` (vars `Set.difference` bvars)
 
 {-| This function computes the set of variables occurring in a context. -}
-variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f)
+variables :: (Ord v, HasVars f v, HTraversable f, HFunctor f)
             => Cxt h f a :=> Set v
 variables = unK . free variablesAlg (const $ K Set.empty)
 
@@ -137,29 +192,30 @@
 {-| This function substitutes variables in a context according to a
 partial mapping from variables to contexts.-}
 class SubstVars v t a where
-    substVars :: (Set v) -> GSubst v t -> a :-> a
+    substVars :: SubstFun v t -> a :-> a
 
-appSubst :: SubstVars v t a => GSubst v t -> a :-> a
-appSubst = substVars Set.empty
+appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a
+appSubst subst = substVars (substFun subst)
 
-instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (Cxt h f a) (Cxt h f a) where
+instance (Ord v, HasVars f v, HTraversable f) => SubstVars v (Cxt h f a) (Cxt h f a) where
     -- have to use explicit GADT pattern matching!!
-    substVars _ _ (Hole a) = Hole a
-    substVars b f (Term v) = substAlg f (hfmap (substVars newBound f) v)
-        where  substAlg :: (HasVars f v) => CxtSubst h a f v
-                        -> Alg f (Cxt h f a)
-               substAlg f t = fromMaybe (Term t) (isVar' b t >>= f . K)
-               newBound = b `Set.union` Set.fromList (bindsVars v)
+    substVars subst = doSubst Set.empty
+      where doSubst :: Set v -> Cxt h f a :-> Cxt h f a
+            doSubst _ (Hole a) = Hole a
+            doSubst b (Term t) = case isVar' b t >>= subst . K of 
+              Just new -> new
+              Nothing  -> Term $ hfmapBoundVars run t
+                where run :: Set v -> Cxt h f a :-> Cxt h f a
+                      run vars s = doSubst (b `Set.union` vars) s
 
 instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
-    substVars b f = hfmap (substVars b f) 
+    substVars subst = hfmap (substVars subst) 
 
 {-| This function composes two substitutions @s1@ and @s2@. That is,
 applying the resulting substitution is equivalent to first applying
 @s2@ and then @s1@. -}
 
-compSubst :: (Ord v, HasVars f v, HFunctor f)
+compSubst :: (Ord v, HasVars f v, HTraversable f)
           => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
-compSubst s1 s2 v = case s2 v of
-                      Nothing -> s1 v
-                      Just t -> Just $ appSubst s1 t
+compSubst s1 s2 = Map.map f s2
+    where f (A t) = A (appSubst s1 t)
diff --git a/src/Data/Comp/MultiParam/HDifunctor.hs b/src/Data/Comp/MultiParam/HDifunctor.hs
--- a/src/Data/Comp/MultiParam/HDifunctor.hs
+++ b/src/Data/Comp/MultiParam/HDifunctor.hs
@@ -22,6 +22,7 @@
      HFunctor (..),
      I (..),
      K (..),
+     E (..),
      A (..),
      (:->),
      NatM
diff --git a/src/Data/Comp/Param/Term.hs b/src/Data/Comp/Param/Term.hs
--- a/src/Data/Comp/Param/Term.hs
+++ b/src/Data/Comp/Param/Term.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,
-  MultiParamTypeClasses #-}
+  MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Param.Term
@@ -24,6 +24,7 @@
      Context,
      simpCxt,
      toCxt,
+     cxtMap,
      ParamFunctor(..)
     ) where
 
@@ -68,6 +69,13 @@
 toCxt :: Difunctor f => Trm f a -> Cxt h f a b
 {-# INLINE toCxt #-}
 toCxt = unsafeCoerce
+
+-- | This combinator maps a function over a context by applying the
+-- function to each hole.
+cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c
+cxtMap f (Hole x) = Hole (f x)
+cxtMap _ (Var x)  = Var x
+cxtMap f (In t)   = In (dimap id (cxtMap f) t)
 
 -- Param Functor
 
diff --git a/src/Data/Comp/Unification.hs b/src/Data/Comp/Unification.hs
--- a/src/Data/Comp/Unification.hs
+++ b/src/Data/Comp/Unification.hs
@@ -22,6 +22,8 @@
 import Control.Monad.Error
 import Control.Monad.State
 
+import Data.Traversable
+
 import qualified Data.Map as Map
 
 {-| This type represents equations between terms over a specific
@@ -56,7 +58,7 @@
 
 -- | This function applies a substitution to each term in a list of
 -- equations.
-appSubstEq :: (Ord v,  HasVars f v, Functor f) =>
+appSubstEq :: (Ord v,  HasVars f v, Traversable f) =>
      Subst f v -> Equation f -> Equation f
 appSubstEq s (t1,t2) = (appSubst s t1,appSubst s t2)
 
@@ -64,7 +66,7 @@
 {-| This function returns the most general unifier of the given
 equations using the algorithm of Martelli and Montanari. -}
 
-unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))
+unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)
       => Equations f -> m (Subst f v)
 unify = runUnifyM runUnify
 
@@ -95,18 +97,18 @@
 putEqs eqs = modify addEqs
     where addEqs s = s {usEqs = eqs ++ usEqs s}
 
-putBinding :: (Monad m, Ord v, HasVars f v, Functor f) => (v, Term f) -> UnifyM f v m ()
+putBinding :: (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m ()
 putBinding bind = modify appSubst
     where binds = Map.fromList [bind]
           appSubst s = s { usEqs = map (appSubstEq binds) (usEqs s),
                              usSubst = compSubst binds (usSubst s)}
 
 
-runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))
+runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)
          => UnifyM f v m ()
 runUnify = withNextEq (\ e -> unifyStep e >> runUnify)
 
-unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) 
+unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) 
           => Equation f -> UnifyM f v m ()
 unifyStep (s,t) = case decompose s of
                     Var v1 -> case decompose t of
diff --git a/src/Data/Comp/Variables.hs b/src/Data/Comp/Variables.hs
--- a/src/Data/Comp/Variables.hs
+++ b/src/Data/Comp/Variables.hs
@@ -30,6 +30,7 @@
     ) where
 
 import Data.Comp.Term
+import Data.Comp.Number
 import Data.Comp.Algebra
 import Data.Comp.Derive
 import Data.Foldable hiding (elem, notElem)
@@ -52,72 +53,107 @@
   @HasVar f v@ denotes that values over @f@ might contain and bind variables of
   type @v@. -}
 class HasVars f v where
-    -- |Indicates whether the @f@ constructor is a variable.
+    -- | Indicates whether the @f@ constructor is a variable. The
+    -- default implementation returns @Nothing@.
     isVar :: f a -> Maybe v
     isVar _ = Nothing
-    -- |Indicates the set of variables bound by the @f@ constructor.
-    bindsVars :: f a -> [v]
-    bindsVars _ = []
+    
+    -- | Indicates the set of variables bound by the @f@ constructor
+    -- for each argument of the constructor. For example for a
+    -- non-recursive let binding:
+    -- @
+    -- data Let e = Let Var e e
+    -- instance HasVars Let Var where
+    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]
+    -- @
+    -- If, instead, the let binding is recursive, the methods has to
+    -- be implemented like this:
+    -- @
+    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),
+    --                                         (y, (Set.singleton v))]
+    -- @
+    -- This indicates that the scope of the bound variable also
+    -- extends to the right-hand side of the variable binding.
+    --
+    -- The default implementation returns the empty map.
+    bindsVars :: Ord a => f a -> Map a (Set v)
+    bindsVars _ = Map.empty
 
+
 $(derive [liftSum] [''HasVars])
 
-instance HasVars f v => HasVars (Cxt h f) v where
-    isVar (Term t) = isVar t
-    isVar _ = Nothing
-    bindsVars (Term t) = bindsVars t
-    bindsVars _ = []
+-- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
+-- @v@ is contained in the given set of variables.
+    
+isVar' :: (HasVars f v, Ord v) => Set v -> f a -> Maybe v
+isVar' b t = do v <- isVar t
+                if v `Set.member` b
+                   then Nothing
+                   else return v
+   
+-- | This combinator pairs every argument of a given constructor with
+-- the set of (newly) bound variables according to the corresponding
+-- 'HasVars' type class instance.
+getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)
+getBoundVars t = let n = number t
+                     m = bindsVars n
+                     trans x = (Map.findWithDefault Set.empty x m, unNumbered x)
+                 in fmap trans n
+                    
+-- | This combinator combines 'getBoundVars' with the generic 'fmap' function.
+fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b
+fmapBoundVars f t = let n = number t
+                        m = bindsVars n
+                        trans x = f (Map.findWithDefault Set.empty x m) (unNumbered x)
+                    in fmap trans n                    
+                    
+-- | This combinator combines 'getBoundVars' with the generic 'foldl' function.   
+foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b
+foldlBoundVars f e t = let n = number t
+                           m = bindsVars n
+                           trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y) 
+                       in foldl trans e n
 
 -- | Convert variables to holes, except those that are bound.
-varsToHoles :: (Functor f, HasVars f v, Eq v) => Term f -> Context f v
-varsToHoles t = cata alg t []
-    where alg :: (Functor f, HasVars f v, Eq v) => Alg f ([v] -> Context f v)
-          alg t vars =
-              let vars' = vars ++ bindsVars t in
-              case isVar t of
-                Just v ->
-                    -- Check for scope
-                    if v `elem` vars' then
-                        Term $ fmap (\x -> x vars') t
-                    else
-                        Hole v
-                Nothing ->
-                    Term $ fmap (\x -> x vars') t
+varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v
+varsToHoles t = cata alg t Set.empty
+    where alg :: (Traversable f, HasVars f v, Ord v) => Alg f (Set v -> Context f v)
+          alg t vars = case isVar t of
+            Just v | v `Set.member` vars -> Hole v
+            _  -> Term $ fmapBoundVars run t
+              where 
+                run newVars f = f $ newVars `Set.union` vars
 
 -- |Algebra for checking whether a variable is contained in a term, except those
 -- that are bound.
-containsVarAlg :: (Eq v, HasVars f v, Foldable f) => v -> Alg f Bool
-containsVarAlg v t = v `notElem` bindsVars t && (local || or t)
+containsVarAlg :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Alg f Bool
+containsVarAlg v t = foldlBoundVars run local t
     where local = case isVar t of
                     Just v' -> v == v'
                     Nothing -> False
+          run acc vars b = acc || (not (v `Set.member` vars) && b)
 
 {-| This function checks whether a variable is contained in a context. -}
-containsVar :: (Eq v, HasVars f v, Foldable f, Functor f)
+containsVar :: (Eq v, HasVars f v, Traversable f, Ord v)
             => v -> Cxt h f a -> Bool
 containsVar v = free (containsVarAlg v) (const False)
 
 -- |Algebra for generating a set of variables contained in a term, except those
 -- that are bound.
-variablesAlg :: (Ord v, HasVars f v, Foldable f) => Alg f (Set v)
-variablesAlg t = Set.filter (`notElem` bindsVars t) $ foldl Set.union local t
+variablesAlg :: (Ord v, HasVars f v, Traversable f) => Alg f (Set v)
+variablesAlg t = foldlBoundVars run local t
     where local = case isVar t of
                     Just v -> Set.singleton v
                     Nothing -> Set.empty
+          run acc bvars vars = acc `Set.union` (vars `Set.difference` bvars)
 
--- |Algebra for generating a list of variables contained in a term, except those
--- that are bound.
-variableListAlg :: (Ord v, HasVars f v, Foldable f) => Alg f [v]
-variableListAlg t = filter (`notElem` bindsVars t) $ foldl (++) local t
-    where local = case isVar t of
-                    Just v -> [v]
-                    Nothing -> [] 
 
 {-| This function computes the list of variables occurring in a context. -}
-variableList :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> [v]
-variableList = free variableListAlg (const [])
+variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v]
+variableList = Set.toList . variables
 
 {-| This function computes the set of variables occurring in a context. -}
-variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set v
+variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v
 variables = free variablesAlg (const Set.empty)
 
 {-| This function computes the set of variables occurring in a constant. -}
@@ -136,18 +172,16 @@
 appSubst subst = substVars f
     where f v = Map.lookup v subst
 
-instance (Ord v, HasVars f v, Functor f)
+instance (Ord v, HasVars f v, Traversable f)
     => SubstVars v (Cxt h f a) (Cxt h f a) where
         -- have to use explicit GADT pattern matching!!
         -- subst f = free (substAlg f) Hole
-    substVars _ (Hole a) = Hole a
-    substVars f (Term v) = let f' = res (bindsVars v) f in
-                           substAlg f' $ fmap (substVars f') v
-            where substAlg :: (HasVars f v) => (v -> Maybe (Cxt h f a))
-                           -> Alg f (Cxt h f a)
-                  substAlg f t = fromMaybe (Term t) (isVar t >>= f)
-                  res :: Eq v => [v] -> (v -> Maybe t) -> v -> Maybe t
-                  res vars f x = if x `elem` vars then Nothing else f x
+  substVars subst = doSubst Set.empty
+    where doSubst _ (Hole a) = Hole a
+          doSubst b (Term t) = case isVar' b t >>= subst of 
+            Just new -> new
+            Nothing  -> Term $ fmapBoundVars run t
+              where run vars s = doSubst (b `Set.union` vars) s
 
 instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where
     substVars f = fmap (substVars f) 
@@ -155,6 +189,6 @@
 {-| This function composes two substitutions @s1@ and @s2@. That is,
 applying the resulting substitution is equivalent to first applying
 @s2@ and then @s1@. -}
-compSubst :: (Ord v, HasVars f v, Functor f)
+compSubst :: (Ord v, HasVars f v, Traversable f)
           => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
 compSubst s1 s2 = fmap (appSubst s1) s2 `Map.union` s1
diff --git a/testsuite/tests/Data/Comp/Examples/Comp.hs b/testsuite/tests/Data/Comp/Examples/Comp.hs
--- a/testsuite/tests/Data/Comp/Examples/Comp.hs
+++ b/testsuite/tests/Data/Comp/Examples/Comp.hs
@@ -9,8 +9,8 @@
 import Data.Comp
 
 import Test.Framework
-import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
+import Test.Framework.Providers.HUnit
+import Test.HUnit
 import Test.Utils hiding (iPair)
 
 
@@ -22,10 +22,10 @@
 --------------------------------------------------------------------------------
 
 tests = testGroup "Compositional Data Types" [
-         testProperty "eval" evalTest,
-         testProperty "evalM" evalMTest,
-         testProperty "desugarEval" desugarEvalTest,
-         testProperty "desugarPos" desugarPosTest
+         testCase "eval" evalTest,
+         testCase "evalM" evalMTest,
+         testCase "desugarEval" desugarEvalTest,
+         testCase "desugarPos" desugarPosTest
         ]
 
 
@@ -36,10 +36,10 @@
 instance (EqF f, Eq p) => EqF (f :&: p) where
     eqF (v1 :&: p1) (v2 :&: p2) = p1 == p2 && v1 `eqF` v2
 
-evalTest = Eval.evalEx == iConst 5
-evalMTest = evalMEx == Just (iConst 5)
-desugarEvalTest = Desugar.evalEx == iPair (iConst 2) (iConst 1)
-desugarPosTest = desugPEx == iAPair (Pos 1 0)
+evalTest = Eval.evalEx @=? iConst 5
+evalMTest = evalMEx @=? Just (iConst 5)
+desugarEvalTest = Desugar.evalEx @=? iPair (iConst 2) (iConst 1)
+desugarPosTest = desugPEx @=? iAPair (Pos 1 0)
                                     (iASnd (Pos 1 0)
                                            (iAPair (Pos 1 1)
                                                    (iAConst (Pos 1 2) 1)
diff --git a/testsuite/tests/Data/Comp/Examples/Multi.hs b/testsuite/tests/Data/Comp/Examples/Multi.hs
--- a/testsuite/tests/Data/Comp/Examples/Multi.hs
+++ b/testsuite/tests/Data/Comp/Examples/Multi.hs
@@ -10,8 +10,8 @@
 import Data.Comp.Multi
 
 import Test.Framework
-import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
+import Test.Framework.Providers.HUnit
+import Test.HUnit
 import Test.Utils hiding (iPair)
 
 --------------------------------------------------------------------------------
@@ -19,11 +19,11 @@
 --------------------------------------------------------------------------------
 
 tests = testGroup "Generalised Compositional Data Types" [
-         testProperty "eval" evalTest,
-         testProperty "evalI" evalITest,
-         testProperty "evalM" evalMTest,
-         testProperty "desugarEval" desugarEvalTest,
-         testProperty "desugarPos" desugarPosTest
+         testCase "eval" evalTest,
+         testCase "evalI" evalITest,
+         testCase "evalM" evalMTest,
+         testCase "desugarEval" desugarEvalTest,
+         testCase "desugarPos" desugarPosTest
         ]
 
 
@@ -34,11 +34,11 @@
 instance (EqHF f, Eq p) => EqHF (f :&: p) where
     eqHF (v1 :&: p1) (v2 :&: p2) = p1 == p2 && v1 `eqHF` v2
 
-evalTest = Eval.evalEx == iConst 2
-evalITest = evalIEx == 2
-evalMTest = evalMEx == Just (iConst 5)
-desugarEvalTest = Desugar.evalEx == iPair (iConst 2) (iConst 1)
-desugarPosTest = desugPEx == iAPair (Pos 1 0)
+evalTest = Eval.evalEx @=? iConst 2
+evalITest = evalIEx @=? 2
+evalMTest = evalMEx @=? Just (iConst 5)
+desugarEvalTest = Desugar.evalEx @=? iPair (iConst 2) (iConst 1)
+desugarPosTest = desugPEx @=? iAPair (Pos 1 0)
                                     (iASnd (Pos 1 0)
                                     (iAPair (Pos 1 1)
                                             (iAConst (Pos 1 2) 1)
diff --git a/testsuite/tests/Data/Comp/Examples/MultiParam.hs b/testsuite/tests/Data/Comp/Examples/MultiParam.hs
--- a/testsuite/tests/Data/Comp/Examples/MultiParam.hs
+++ b/testsuite/tests/Data/Comp/Examples/MultiParam.hs
@@ -7,8 +7,8 @@
 import Data.Comp.MultiParam.FreshM (Name)
 
 import Test.Framework
-import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
+import Test.Framework.Providers.HUnit
+import Test.HUnit
 import Test.Utils
 
 
@@ -20,7 +20,7 @@
 --------------------------------------------------------------------------------
 
 tests = testGroup "Parametric Compositional Data Types" [
-         testProperty "FOL" folTest
+         testCase "FOL" folTest
         ]
 
 
@@ -28,7 +28,7 @@
 -- Properties
 --------------------------------------------------------------------------------
 
-folTest = show (foodFact7 :: INF Name TFormula) == "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" ++
+folTest = show (foodFact7 :: INF Name TFormula) @=? "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" ++
           "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Eats(Skol6(x2), x2))\n" ++
                                                                                         "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Person(Skol6(x2)))\n" ++
                                                                                         "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Eats(Skol6(x2), x2))"
diff --git a/testsuite/tests/Data/Comp/Examples/Param.hs b/testsuite/tests/Data/Comp/Examples/Param.hs
--- a/testsuite/tests/Data/Comp/Examples/Param.hs
+++ b/testsuite/tests/Data/Comp/Examples/Param.hs
@@ -7,8 +7,8 @@
 import Data.Comp.Param
 
 import Test.Framework
-import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
+import Test.Framework.Providers.HUnit
+import Test.HUnit
 import Test.Utils
 
 
@@ -20,8 +20,8 @@
 --------------------------------------------------------------------------------
 
 tests = testGroup "Parametric Compositional Data Types" [
-         testProperty "names" namesTest,
-         testProperty "graph" graphTest
+         testCase "names" namesTest,
+         testCase "graph" graphTest
         ]
 
 
@@ -34,5 +34,5 @@
                                      b2 <- eqD v1 v2
                                      return $ b1 && b2
 
-namesTest = en == en' && ep == ep'
-graphTest = g == g && n == 5 && f == [0,2,1,2]
+namesTest = sequence_ [en @=? en', ep @=? ep']
+graphTest = sequence_ [n @=? 5, f @=? [0,2,1,2]]
diff --git a/testsuite/tests/Data/Comp/Multi/Variables_Test.hs b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances,
+MultiParamTypeClasses, TypeOperators, FlexibleContexts , RankNTypes,
+GADTs, ScopedTypeVariables, EmptyDataDecls#-}
+
+module Data.Comp.Multi.Variables_Test where
+
+
+import Data.Comp.Multi.Variables
+import Data.Comp.Multi.Derive
+import Data.Comp.Multi.Sum
+import Data.Comp.Multi.Term
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.Show ()
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit
+
+
+
+--------------------------------------------------------------------------------
+-- Definitions
+--------------------------------------------------------------------------------
+
+data Var = X | Y | Z deriving (Eq,Ord,Show)
+
+
+data Ex
+
+type Value f = forall i . Term f i
+type Expression f = Term f Ex
+
+data Val e i where 
+    Abs :: Var -> e Ex -> Val e i
+    Var :: Var -> Val e i
+    Int :: Int -> Val e i
+
+
+data Op e i where
+    App :: e Ex -> e Ex -> Op e Ex
+    Plus :: e Ex -> e Ex -> Op e Ex
+
+
+data Let e i  where 
+             Let :: Var -> e Ex -> e Ex -> Let e Ex
+
+data LetRec e i  where 
+             LetRec :: Var -> e Ex -> e Ex -> LetRec e Ex
+
+type Sig = Op :+: Val
+
+type SigLet = Let :+: Sig
+
+type SigRec = LetRec :+: Sig
+
+$(derive [makeHFunctor, makeHTraversable, makeHFoldable,
+          makeEqHF, makeShowHF, smartConstructors]
+         [''Op, ''Val, ''Let, ''LetRec])
+
+instance HasVars Val Var where
+    isVar (Var v) = Just v
+    isVar _       = Nothing
+    
+    bindsVars (Abs v a) = Map.singleton (E a) (Set.singleton v)
+    bindsVars _         = Map.empty
+
+instance HasVars Op a where
+
+instance HasVars Let Var where
+    bindsVars (Let v _ a) = Map.singleton (E a) (Set.singleton v)
+
+instance HasVars LetRec Var where
+    bindsVars (LetRec v a b) = Map.fromList [(E a,vs),(E b,vs)]
+        where vs = Set.singleton v
+
+-- let x = x + 1 in (\y. y + x) z
+letExp, letExp' :: Expression SigLet
+letExp = iLet X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
+letExp' = iLet X (iInt 1 `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)
+
+-- letrec x = x + 1 in (\y. y + x) z
+recExp, recExp :: Expression SigRec
+recExp = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
+recExp' = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)
+
+subst :: (Val :<: f) => Subst f Var
+subst = Map.fromList [(X, A $ iInt 1), (Y, A $ iInt 2), (Z, A $ iInt 3)]
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------
+
+case_letFree = variables letExp @=? Set.fromList [Z,X]
+
+case_recFree = variables recExp @=? Set.fromList [Z]
+
+case_letSubst = appSubst s letExp @=? letExp'
+    where s = subst :: Subst SigLet Var
+
+case_recSubst = appSubst s recExp @=? recExp'
+    where s = subst :: Subst SigRec Var
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+main = defaultMain [tests]
+
+tests = testGroup "Variables" [
+         testCase "case_letFree" case_letFree
+        ,testCase "case_recFree" case_recFree
+        ,testCase "case_letSubst" case_letSubst
+        ,testCase "case_recSubst" case_recSubst
+        ]
diff --git a/testsuite/tests/Data/Comp/Multi_Test.hs b/testsuite/tests/Data/Comp/Multi_Test.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Multi_Test.hs
@@ -0,0 +1,18 @@
+module Data.Comp.Multi_Test where
+
+import Test.Framework
+import qualified Data.Comp.Multi.Variables_Test
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+main = defaultMain [tests]
+
+tests = testGroup "Multi" [
+         Data.Comp.Multi.Variables_Test.tests
+       ]
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------
diff --git a/testsuite/tests/Data/Comp/Variables_Test.hs b/testsuite/tests/Data/Comp/Variables_Test.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Variables_Test.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances,
+FlexibleInstances, MultiParamTypeClasses, TypeOperators, FlexibleContexts#-}
+
+module Data.Comp.Variables_Test where
+
+
+import Data.Comp.Variables
+import Data.Comp.Derive
+import Data.Comp.Sum
+import Data.Comp.Term
+import Data.Comp.Show ()
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit
+
+
+
+--------------------------------------------------------------------------------
+-- Definitions
+--------------------------------------------------------------------------------
+
+data Var = X | Y | Z deriving (Eq,Ord,Show)
+
+
+data Val e = Abs Var e
+           | Var Var
+           | Int Int
+
+data Op e = App e e
+          | Plus e e
+
+data Let e = Let Var e e
+
+data LetRec e = LetRec Var e e
+
+type Sig = Op :+: Val
+
+type SigLet = Let :+: Sig
+
+type SigRec = LetRec :+: Sig
+
+$(derive [makeFunctor, makeTraversable, makeFoldable,
+          makeEqF, makeShowF, smartConstructors]
+         [''Op, ''Val, ''Let, ''LetRec])
+
+instance HasVars Val Var where
+    isVar (Var v) = Just v
+    isVar _       = Nothing
+    
+    bindsVars (Abs v a) = Map.singleton a (Set.singleton v)
+    bindsVars _         = Map.empty
+
+instance HasVars Op a where
+
+instance HasVars Let Var where
+    bindsVars (Let v _ a) = Map.singleton a (Set.singleton v)
+
+instance HasVars LetRec Var where
+    bindsVars (LetRec v a b) = Map.fromList [(a,vs),(b,vs)]
+        where vs = Set.singleton v
+
+-- let x = x + 1 in (\y. y + x) z
+letExp, letExp' :: Term SigLet
+letExp = iLet X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
+letExp' = iLet X (iInt 1 `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)
+
+-- letrec x = x + 1 in (\y. y + x) z
+recExp, recExp :: Term SigRec
+recExp = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
+recExp' = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)
+
+subst :: (Val :<: f) => Subst f Var
+subst = Map.fromList [(X, iInt 1), (Y, iInt 2), (Z, iInt 3)]
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------
+
+case_letFree = Set.fromList [Z,X] @=? variables letExp
+
+case_recFree = Set.fromList [Z] @=? variables recExp
+
+case_letSubst = letExp' @=? appSubst s letExp
+    where s = subst :: Subst SigLet Var
+
+case_recSubst = recExp' @=? appSubst s recExp
+    where s = subst :: Subst SigRec Var
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+main = defaultMain [tests]
+
+tests = testGroup "Variables" [
+         testCase "case_letFree" case_letFree
+        ,testCase "case_recFree" case_recFree
+        ,testCase "case_letSubst" case_letSubst
+        ,testCase "case_recSubst" case_recSubst
+        ]
diff --git a/testsuite/tests/Data/Comp_Test.hs b/testsuite/tests/Data/Comp_Test.hs
--- a/testsuite/tests/Data/Comp_Test.hs
+++ b/testsuite/tests/Data/Comp_Test.hs
@@ -1,18 +1,11 @@
 module Data.Comp_Test where
 
-
-import Data.Comp
-import Data.Comp.Equality
-import Data.Comp.Arbitrary ()
-import Data.Comp.Show ()
-
-import Test.Framework
-import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
-import Test.Utils
+import Test.Framework 
 
 import qualified Data.Comp.Equality_Test
 import qualified Data.Comp.Examples_Test
+import qualified Data.Comp.Variables_Test
+import qualified Data.Comp.Multi_Test
 
 --------------------------------------------------------------------------------
 -- Test Suits
@@ -22,7 +15,9 @@
 
 tests = testGroup "Comp" [
          Data.Comp.Equality_Test.tests,
-         Data.Comp.Examples_Test.tests
+         Data.Comp.Examples_Test.tests,
+         Data.Comp.Variables_Test.tests,
+         Data.Comp.Multi_Test.tests
         ]
 
 --------------------------------------------------------------------------------