diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -88,3 +88,32 @@
 Version 0.4.3.1: 8 May 2014
 
   * Allow transformers-0.4 and mtl-2.2
+
+Version 0.4.4: 18 May 2015
+
+  * Update to work with GHC 7.10
+  
+Version 0.4.5: 2 Oct 2015
+
+  * Test suite in cabal file
+  * New optimized function for immediately substitution w/o naming
+    Only works for patterns with a single variable:
+      substBind :: Subst a b => Bind (Name a) b -> a -> b
+
+Version 0.5: August 2016
+
+  * Remove Show superclass for Alpha  (potentially breaking change)
+  * Remove permValid function from Unbound.PermM
+  
+  * New function in Unbound.LocallyNameless.Ops
+      patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t		
+  * More sensible Show instance for bind, shows as code that
+    can be directly parsed to Haskell.
+      old:  <a> (Var 0@0)
+		new:  (bind (string2Name "a") (Var (string2Name "a"))
+  * works with GHC-8.0.1
+  * Error message if don't override aeq' / acompare' for abstract types
+  * More correctness tests
+  
+Planned extensions:
+  * Cache free variables at binders
diff --git a/Unbound/DynR.hs b/Unbound/DynR.hs
new file mode 100644
--- /dev/null
+++ b/Unbound/DynR.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE GADTs, ScopedTypeVariables
+  #-}
+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.RepR
+-- License     :  BSD-like (see LICENSE)
+-- Maintainer  :  sweirich@cis.upenn.edu
+-- Portability :  GHC only (-XKitchenSink)
+--
+-- A Dynamic type based on type representations.
+-- This module should probably be added to RepLib instead of Unbound
+-- However, it is currently used only in an experimental function
+-- (Unbound.Subst.substPats).
+module Unbound.DynR (Dyn, toDyn, fromDyn, fromDynR) where
+
+import Generics.RepLib
+
+-- | Dynamic type based on type representations (replib)
+data Dyn where 
+  Dyn :: Rep a => a -> Dyn
+
+-- | Coerce to a Dynamic type         
+toDyn :: Rep a => a -> Dyn 
+toDyn = Dyn 
+
+-- | Coerce using an explicit type representation
+toDynR :: R a -> a -> Dyn
+toDynR ra = withRep ra toDyn
+
+-- | Dynamic cast from the dynamic type (could fail)
+fromDyn :: forall a. Rep a => Dyn -> Maybe a 
+fromDyn (Dyn x) = cast x
+
+-- | Dyynamic cast using explicit type representation
+fromDynR :: forall a. R a -> Dyn -> Maybe a
+fromDynR r1 (Dyn x) = castR rep r1 x
diff --git a/Unbound/LocallyNameless.hs b/Unbound/LocallyNameless.hs
--- a/Unbound/LocallyNameless.hs
+++ b/Unbound/LocallyNameless.hs
@@ -186,7 +186,7 @@
     -- ** Substitution
 
     -- | Capture-avoiding substitution.
-    Subst(..), SubstName(..),
+    Subst(..), SubstName(..),substBind,
 
     -- ** Permutations
 
diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs
--- a/Unbound/LocallyNameless/Alpha.hs
+++ b/Unbound/LocallyNameless/Alpha.hs
@@ -8,7 +8,7 @@
 -- |
 -- Module      :  Unbound.LocallyNameless.Alpha
 -- License     :  BSD-like (see LICENSE)
--- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
 -- Portability :  GHC only (-XKitchenSink)
 --
 ----------------------------------------------------------------------
@@ -106,8 +106,19 @@
 --
 --   Note how the call to 'aeqR1' handles all the other cases generically.
 --
-class (Show a, Rep1 AlphaD a) => Alpha a where
+--   If you use "Abstract" types (i.e. those with representations derived via
+--   derive_abstract) then you must provide a definition of aeq' and
+--   acompare'.  In these cases, Unbound has no information about the
+--   structure of the type and cannot do anything sensible.
 
+--      swaps'    -- identity function
+--      fv'       -- const mempty
+--      freshen'  -- identity function
+--      lfreshen' -- identity function
+--      open/close -- treat like constants
+
+class (Rep1 AlphaD a) => Alpha a where
+
   -- | See 'swaps'.
   swaps' :: AlphaCtx -> Perm AnyName -> a -> a
   swaps' = swapsR1 rep1
@@ -215,7 +226,7 @@
                 | NamesSeen Integer  -- ^ We haven't found the name
                                      --   (yet), but have seen this many
                                      --   others while looking for it
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord)
 
 -- | @FindResult@ forms a monoid which combines information from
 --   several 'findpatrec' operations.  @mappend@ takes the leftmost
@@ -272,7 +283,7 @@
 nthpat x i = case runNthCont (nthpatrec x) i of
                  CurIndex j -> error
                    ("BUG: pattern index " ++ show i ++
-                    " out of bounds by " ++ show j ++ "in" ++ show x)
+                    " out of bounds by " ++ show j ++ "in")
                  Found nm   -> nm
 
 ------------------------------------------------------------
@@ -289,21 +300,25 @@
 -- the context on.
 data AlphaCtx = AC { mode :: Mode , level :: Integer }
 
+-- | Toplevel alpha-contexts
 initial :: AlphaCtx
 initial = AC Term 0
 
+-- | Call when going under a binder
 incr :: AlphaCtx -> AlphaCtx
 incr c = c { level = level c + 1 }
 
+-- | Call when going in an embedding
 decr :: AlphaCtx -> AlphaCtx
 decr c = -- if level c == 0 then error "Too many outers"
          -- else
          c { level = level c - 1 }
 
-
+-- | Call when entering a pattern
 pat  :: AlphaCtx -> AlphaCtx
 pat c  = c { mode = Pat }
 
+-- | Call when entering a term embedded in a pattern
 term  :: AlphaCtx -> AlphaCtx
 term c  = c { mode = Term }
 
@@ -357,6 +372,7 @@
 -- that take representations end in 'R1'.)
 ----------------------------------------------------------------------
 
+-- | Generic version of close
 closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
 closeR1 (Data1 _ cons) = \i a d ->
    case (findCon cons d) of
@@ -364,7 +380,7 @@
         to c (map_l (\z -> closeD z i a) rec kids)
 closeR1 _               = \_ _ d -> d
 
-
+-- | Generic version of open
 openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
 openR1 (Data1 _ cons) = \i a d ->
    case (findCon cons d) of
@@ -372,24 +388,24 @@
         to c (map_l (\z -> openD z i a) rec kids)
 openR1 _               = \_ _ d -> d
 
-
+-- | Generic version of swaps
 swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
 swapsR1 (Data1 _ cons)  = \ p x d ->
   case (findCon cons d) of
     Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
 swapsR1 _               = \ _ _ d -> d
 
-
+-- | Generic version of fv
 fvR1 :: Collection f => R1 (AlphaD) a -> AlphaCtx -> a -> f AnyName
 fvR1 (Data1 _ cons) = \ p  d ->
   case (findCon cons d) of
-    Val _ rec kids -> fv1 rec p kids
+    Val _ rec kids -> fv1 rec p kids where
+          fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName
+          fv1 MNil _ Nil = emptyC
+          fv1 (r :+: rs) p (p1 :*: t1) =
+               fvD r p p1 `union` fv1 rs p t1
 fvR1 _ = \ _ _ -> emptyC
 
-fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName
-fv1 MNil _ Nil = emptyC
-fv1 (r :+: rs) p (p1 :*: t1) =
-   fvD r p p1 `union` fv1 rs p t1
 
 {-
 matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
@@ -413,6 +429,7 @@
   (l1 `join` l2)
 -}
 
+-- | Generic version of aeq
 aeqR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Bool
 aeqR1 (Data1 _ cons) = loop cons where
    loop (Con emb reps : rest) p x y =
@@ -424,13 +441,16 @@
 aeqR1 Int1     = \ _ x y ->  x == y
 aeqR1 Integer1 = \ _ x y -> x == y
 aeqR1 Char1    = \ _ x y -> x == y
+aeqR1 (Abstract1 _) = \ _ x y -> error "Must override aeq' for abstract types"
 aeqR1 _        = \ _ _ _ -> False
 
+-- | Generic list version of aeq
 aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool
 aeq1 MNil _ Nil Nil = True
 aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
   aeqD r c p1 p2 && aeq1 rs c t1 t2
 
+-- | Generic version of freshen
 freshenR1 :: Fresh m => R1 (AlphaD) a -> AlphaCtx -> a -> m (a,Perm AnyName)
 freshenR1 (Data1 _ cons) = \ p d ->
    case findCon cons d of
@@ -439,6 +459,7 @@
        return (to c l, p')
 freshenR1 _ = \ _ n -> return (n, empty)
 
+-- | Generic list version of freshen
 freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
 freshenL MNil _ Nil = return (Nil, empty)
 freshenL (r :+: rs) p (t :*: ts) = do
@@ -515,8 +536,7 @@
                         (Nothing, Nothing) -> loop rest
                  loop [] = error "acompareR1 found no constructors! Please report this as a bug."
              in loop cons
-acompareR1 (Abstract1 _) _ = \_ _ -> EQ           
-acompareR1 r1 _ = error ("acompareR1 not supported for " ++ show r1)
+acompareR1 r1 _ = error ("acompare' not supported for " ++ show r1)
 
 compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering
 compareTupM MNil _ Nil Nil = EQ
@@ -707,8 +727,8 @@
     acompare' c (B p1 t1) (B p2 t2) =
       mappend (acompare' (pat c) p1 p2) (acompare' (incr c) t1 t2)
 
-    findpatrec _ b = error $ "Binding " ++ show b ++ " used as a pattern"
-    nthpatrec    b = error $ "Binding " ++ show b ++ " used as a pattern"
+    findpatrec _ b = error $ "Binding used as a pattern"
+    nthpatrec    b = error $ "Binding used as a pattern"
 
 instance (Alpha p, Alpha q) => Alpha (Rebind p q) where
   isTerm _ = False
diff --git a/Unbound/LocallyNameless/Fresh.hs b/Unbound/LocallyNameless/Fresh.hs
--- a/Unbound/LocallyNameless/Fresh.hs
+++ b/Unbound/LocallyNameless/Fresh.hs
@@ -82,7 +82,7 @@
 class Monad m => Fresh m where
 
   -- | Generate a new globally unique name based on the given one.
-  fresh :: Name a -> m (Name a)
+  fresh :: Rep a => Name a -> m (Name a)
 
 -- | The @FreshM@ monad transformer.  Keeps track of the lowest index
 --   still globally unused, and increments the index every time it is
diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs
--- a/Unbound/LocallyNameless/Ops.hs
+++ b/Unbound/LocallyNameless/Ops.hs
@@ -8,7 +8,7 @@
 -- |
 -- Module      :  Unbound.LocallyNameless.Ops
 -- License     :  BSD-like (see LICENSE)
--- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
 -- Portability :  GHC only (-XKitchenSink)
 --
 -- Generic operations defined in terms of the RepLib framework and the
@@ -46,11 +46,6 @@
 bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
 bind p t = B p (closeT p t)
 
--- | A destructor for binders that does /not/ guarantee fresh
---   names for the binders.
-unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a,b)
-unsafeUnbind (B a b) = (a, openT a b)
-
 instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where
          readPrec = R.parens $ (R.prec app_prec $ do
                                   R.Ident "<" <- R.lexP
@@ -66,18 +61,8 @@
 -- Set Binding operations
 ----------------------------------------------------------
 
-permCloseAny :: (Alpha t) => [AnyName] -> t -> ([AnyName],t)
-permCloseAny ns t = (ns', closeT ns' t) where
-    -- find where the names occur in the body of the term
-    ns' = map fst . sortBy (comparing snd) 
-        . catMaybes 
-        . map (strength . (\n -> (n, findpat t n))) 
-        $ ns
 
-strength :: Functor f => (a, f b) -> f (a, b)
-strength (a, fb) = fmap ((,) a) fb
-
--- Given a list of names and a term, close the term with those names
+-- | Given a list of names and a term, close the term with those names
 -- where the indices of the bound variables occur in sequential order
 -- and return the equivalent ordering of the names, dropping those
 -- that do not occur in the term at all
@@ -86,7 +71,6 @@
 --    permClose [b,c]    (c,b)   =  ([c,b], (0,1))    -- vars reordered
 --    permClose [a,b,c]  (c,b)   =  ([c,b], (0,1))    -- var dropped
 --    permClose [a,b,c]  (c,b,c) =  ([c,b], (0,1,0))  -- additional occurrence ok
-
 permClose :: (Alpha a, Alpha t) => [Name a] -> t -> ([Name a],t)
 permClose ns t = (ns', closeT ns' t) where
     ns' = map fst . sortBy (comparing snd) 
@@ -94,6 +78,19 @@
         . map (strength . (\n -> (n, findpat t (AnyName n))))
         $ ns
 
+-- | Variant of permClose for dynamically typed names
+permCloseAny :: (Alpha t) => [AnyName] -> t -> ([AnyName],t)
+permCloseAny ns t = (ns', closeT ns' t) where
+    -- find where the names occur in the body of the term
+    ns' = map fst . sortBy (comparing snd) 
+        . catMaybes 
+        . map (strength . (\n -> (n, findpat t n))) 
+        $ ns
+
+strength :: Functor f => (a, f b) -> f (a, b)
+strength (a, fb) = fmap ((,) a) fb
+
+
 -- | Bind the pattern in the term \"up to permutation\" of bound variables.
 --   For example, the following 4 terms are /all/ alpha-equivalent:
 --
@@ -318,29 +315,6 @@
                           swaps (pm' <> pm) p2, openT p1' t2)
          Nothing -> return Nothing
          
-{-         
-unbind2translate :: (Fresh m, MonadPlus m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>
-            GenBind order card p1 t1 -> GenBind order card p2 t2 
-            -> m (p1,t1,p2,t2)
-unbind2translate (B p1 t1) (B p2 t2) = do
-      do fv2' <- translates fv1 fv2 
-         pm   <- mkPerm fv2' fv1 
-         (p1', pm') <- freshen p1
-           return $ Just (p1', openT p1' t1,
-                          swaps (pm' <> pm) p2, openT p1' t2)
-         Nothing -> return Nothing         
-       where fv1 = fvAny p1  
-             fv2 = fvAny p2
-
-translates :: MonadPlus m => [AnyName] -> [AnyName] -> m [AnyName]
-translates ((AnyName (n1 :: Name a)):n1s) ((AnyName n2):n2s) = 
-  liftM (AnyName n2 :) (translates n1s n2s) where
-      n2' :: Name a
-      n2' = translate n2
-translates [] [] = return []      
-translates _ _   = mzero
--}
-
 -- | Unbind three terms with the same fresh names, provided the
 --   binders have the same number of binding variables.  See the
 --   documentation for 'unbind2' for more details.
@@ -401,27 +375,50 @@
 
 --  A few extra simultaneous l/unbinds, specialized to MonadPlus monads.
 
-
+-- | Unbind two binders with the same names, fail if the number of required
+-- names and their sorts does not match. See 'unbind2'
 unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
          => GenBind order card p1 t1
          -> GenBind order card p2 t2
          -> m (p1, t1, p2, t2)
 unbind2Plus bnd bnd' = maybe mzero return =<< unbind2 bnd bnd'
 
+-- | Unbind three binders with the same names, fail if the number of required
+-- names and their sorts does not match. See 'unbind3'
 unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>
             GenBind order card p1 t1 -> GenBind order card p2 t2 
             -> GenBind order card p3 t3 ->  m (p1,t1,p2,t2,p3,t3)
 unbind3Plus b1 b2 b3 = maybe mzero return =<< unbind3 b1 b2 b3            
 
+-- | See 'lunbind2'
 lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
          => GenBind order card p1 t1
          -> GenBind order card p2 t2
          -> ((p1, t1, p2, t2) -> m r) -> m r
 lunbind2Plus bnd bnd' k =          
   lunbind2 bnd bnd' $ maybe mzero k 
-  
+
+-- | See 'lunbind3'
 lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>
             GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 ->
             ((p1,t1,p2,t2,p3,t3) -> m r) ->
             m r
 lunbind3Plus b1 b2 b3 = lunbind3 b1 b2 b3 . maybe mzero
+
+
+------------------------------------------------------------
+-- Opening binders, without freshness
+------------------------------------------------------------
+
+
+-- | A destructor for binders that does /not/ guarantee fresh names 
+--  for the binders. Instead it uses the names in the provided pattern.
+patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t
+patUnbind p (B _ t) = openT p t
+
+
+-- | A destructor for binders that does /not/ guarantee fresh
+--   names for the binders. Instead, it uses the original names from
+--   when the binder was constructed.
+unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a,b)
+unsafeUnbind (B a b) = (a, openT a b)
diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs
--- a/Unbound/LocallyNameless/Subst.hs
+++ b/Unbound/LocallyNameless/Subst.hs
@@ -20,6 +20,10 @@
 import Data.List (find)
 
 import Generics.RepLib
+
+import Data.Proxy
+
+import Unbound.DynR
 import Unbound.LocallyNameless.Types
 import Unbound.LocallyNameless.Alpha
 
@@ -35,6 +39,12 @@
 data SubstCoerce a b where  
   SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
 
+-- | Immediately substitute for a (single) bound variable
+-- in a binder, without first naming that variable.
+substBind :: Subst a b => Bind (Name a) b -> a -> b
+substBind (B _ t) u = substPat initial u t
+
+
 -- | The @Subst@ class governs capture-avoiding substitution.  To
 --   derive this class, you only need to indicate where the variables
 --   are in the data type, by overriding the method 'isvar'.
@@ -85,15 +95,39 @@
     | otherwise =
       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)
 
+
+  -- Pattern substitution (single variable)
+  -- call this using the top level function (substBind)
+  substPat ::AlphaCtx -> b -> a -> a
+  substPat ctx u x = 
+     case (isvar x :: Maybe (SubstName a b)) of
+        Just (SubstName (Bn r j 0)) | level ctx == j -> u
+        _ -> substPatR1 rep1 ctx u x
+
+  -- Pattern substitution (all variables in a single pattern)
+  -- TODO: make this return Maybe when the dynamic chack fails
+  -- i.e. when there aren't the right number/sort of arguments
+  -- for the pattern.  This function isn't yet exposed.
+  substPats :: Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a
+  substPats p ctx us x = 
+     case (isvar x :: Maybe (SubstName a b)) of
+        Just (SubstName (Bn r j i)) | level ctx == j && fromInteger i < length us ->
+          case fromDynR r (us !! fromInteger i) of
+            Just tm -> tm
+            Nothing -> error "internal error: sort mismatch"
+        _ -> substPatsR1 rep1 p ctx us x
+
 -- | Reified class dictionary for 'Subst'.
 data SubstD b a = SubstD {
   isvarD  :: a -> Maybe (SubstName a b),
   substD  ::  Name b -> b -> a -> a ,
-  substsD :: [(Name b, b)] -> a -> a
+  substsD :: [(Name b, b)] -> a -> a ,
+  substPatD :: AlphaCtx -> b -> a -> a ,
+  substPatsD :: Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a
 }
 
 instance Subst b a => Sat (SubstD b a) where
-  dict = SubstD isvar subst substs
+  dict = SubstD isvar subst substs substPat substPats
 
 substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> a
 substDefault = substR1 rep1
@@ -114,6 +148,56 @@
       in (to c z)
 substsR1 _               = \ _ c -> c
 
+substPatsR1 :: R1 (SubstD b) a -> Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a
+substPatsR1 (Data1 _dt cons) = \ p ct s d ->
+  case (findCon cons d) of
+  Val c rec kids ->
+      let z = map_l (\ w -> substPatsD w p ct s) rec kids
+      in (to c z)
+substPatsR1 _               = \ _ _ _ c -> c
+
+substPatR1 :: R1 (SubstD b) a -> AlphaCtx -> b -> a -> a
+substPatR1 (Data1 _dt cons) = \ ct s d ->
+  case (findCon cons d) of
+  Val c rec kids ->
+      let z = map_l (\ w -> substPatD w ct s) rec kids
+      in (to c z)
+substPatR1 _               = \ _ _ c -> c
+
+
+-- instances for types that change the de Bruijn levels of the context
+
+instance (Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) where
+   substPat c us (B p t) = 
+     B (substPat (pat c) us p) (substPat (incr c) us t)
+   substPats pr c us (B p t) = 
+     B (substPats pr (pat c) us p) (substPats pr (incr c) us t)
+  
+instance (Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) where
+   substPat     c us (R p q) = R (substPat     c us p) (substPat     (incr c) us q)
+   substPats pr c us  (R p q) = R (substPats pr c us p) (substPats pr (incr c) us q)
+   
+instance (Alpha p, Subst b p) => Subst b (Rec p) where
+   substPat     c us (Rec p) = Rec (substPat     (incr c) us p)
+   substPats pr c us (Rec p) = Rec (substPats pr (incr c) us p)
+
+instance (Alpha t, Subst b t) => Subst b (Embed t) where
+   substPat c us (Embed x) = case mode c of
+     Pat  -> Embed (substPat (term c) us x)
+     Term -> error "substPat on Embed"
+   substPats pr c us (Embed x) = case mode c of
+     Pat  -> Embed (substPats pr (term c) us x)
+     Term -> error "substPat on Embed"
+
+instance (Alpha a, Subst b a) => Subst b (Shift a) where
+  substPat      c us (Shift x) = Shift (substPat     (decr c) us x)
+  substPats pr  c us (Shift x) = Shift (substPats pr (decr c) us x)
+
+   
+
+
+
+
 instance Subst b Int
 instance Subst b Bool
 instance Subst b ()
@@ -135,11 +219,5 @@
 instance (Subst c a) => Subst c (Maybe a)
 instance (Subst c a, Subst c b) => Subst c (Either a b)
 
-instance (Rep order, Rep card, Subst c b, Subst c a, Alpha a,Alpha b) =>
-    Subst c (GenBind order card a b)
-instance (Subst c b, Subst c a, Alpha a, Alpha b) =>
-    Subst c (Rebind a b)
 
-instance (Subst c a) => Subst c (Shift a)
-instance (Subst c a) => Subst c (Embed a)
-instance (Alpha a, Subst c a) => Subst c (Rec a)
+
diff --git a/Unbound/LocallyNameless/Types.hs b/Unbound/LocallyNameless/Types.hs
--- a/Unbound/LocallyNameless/Types.hs
+++ b/Unbound/LocallyNameless/Types.hs
@@ -45,33 +45,53 @@
 ------------------------------------------------------------
 -- Basic types
 ------------------------------------------------------------
+-- Note: can't use DataKinds here because RepLib does not support
+-- representations of them.
 
+-- | Type level flag for binder that allows permutation
 data RelaxedOrder
+-- | Type level flag for binder that does not allow permutation
 data StrictOrder
 
+-- | Type level flag for binder that allows extra unused variables
 data RelaxedCard
+-- | Type level flag for binder that does not allow weakening
 data StrictCard
 
+--------------------------------------------------  
 -- Bind
 --------------------------------------------------
 
--- XXX update documentation
+-- | Generic binding combinator for a pattern @p@ within a term @t@.
+-- Flexible over the order and cardinality of the variables bound
+-- in the pattern
+data GenBind order card p t = B p t
+
+  
 -- | The most fundamental combinator for expressing binding structure
 --   is 'Bind'.  The /term type/ @Bind p t@ represents a pattern @p@
 --   paired with a term @t@, where names in @p@ are bound within @t@.
 --
 --   Like 'Name', 'Bind' is also abstract. You can create bindings
 --   using 'bind' and take them apart with 'unbind' and friends.
-data GenBind order card p t = B p t
-
 type Bind p t        = GenBind StrictOrder StrictCard p t
+
+
+
+-- | A variant of 'Bind' where alpha-equivalence allows multiple
+-- variables bound in the same pattern to be reordered
 type SetBind p t     = GenBind RelaxedOrder StrictCard p t
+-- | A variant of 'Bind' where alpha-equivalence allows multiple
+-- variables bound in the same pattern to be reordered, and
+-- allows the binding of unused variables
+-- For example,  \{ a b c } . a b `aeq` \ { b a } . a b
 type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t
 
 instance (Show a, Show b) => Show (GenBind order card a b) where
   showsPrec p (B a b) = showParen (p>0)
-      (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)
+      (showString "bind " . showsPrec 11 a . showsPrec 11 b)
 
+--------------------------------------------------
 -- Rebind
 --------------------------------------------------
 
@@ -84,7 +104,7 @@
 
 instance (Show a, Show b) => Show (Rebind a b) where
   showsPrec p (R a b) = showParen (p>0)
-      (showString "<<" . showsPrec p a . showString ">> " . showsPrec 0 b)
+      (showString "rebind " . showsPrec 11 a . showsPrec 11 b)
 
 -- Rec
 --------------------------------------------------
diff --git a/Unbound/PermM.hs b/Unbound/PermM.hs
--- a/Unbound/PermM.hs
+++ b/Unbound/PermM.hs
@@ -11,7 +11,7 @@
 ----------------------------------------------------------------------
 
 module Unbound.PermM (
-    Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm
+    Perm(..), single, compose, apply, support, isid, join, empty, restrict, mkPerm
   ) where
 
 import Data.Monoid
@@ -27,6 +27,7 @@
 --   form the basis for nominal approaches to binding, but can
 --   also be useful in general.
 newtype Perm a = Perm (Map a a)
+
 
 permValid :: Ord a => Perm a -> Bool
 permValid (Perm p) = all (\(_,v) -> M.member v p) (M.assocs p)
diff --git a/Unbound/Util.hs b/Unbound/Util.hs
--- a/Unbound/Util.hs
+++ b/Unbound/Util.hs
@@ -9,7 +9,6 @@
 --
 -- Various utilities for the Unbound library.
 ----------------------------------------------------------------------
-
 module Unbound.Util where
 
 import Data.Maybe (catMaybes)
@@ -99,6 +98,7 @@
   union     = S.union
   cmap      = S.map
 
+-- | Determine whether two sets have an empty intersection
 disjoint :: Ord a => S.Set a -> S.Set a -> Bool
 disjoint s1 s2 = S.null( S.intersection s1 s2 )
 
diff --git a/examples/Abstract.hs b/examples/Abstract.hs
--- a/examples/Abstract.hs
+++ b/examples/Abstract.hs
@@ -21,7 +21,7 @@
 --
 -- Suppose we wish to include Source positions in our Abstract Syntax
 --
-module Abstract where
+module Examples.Abstract where
 
 import Generics.RepLib
 import Unbound.LocallyNameless
diff --git a/examples/Basic.hs b/examples/Basic.hs
--- a/examples/Basic.hs
+++ b/examples/Basic.hs
@@ -13,10 +13,10 @@
 --
 -----------------------------------------------------------------------------
 
-module Basic where
+module Examples.Basic where
 
 import Generics.RepLib
-import Language.Haskell.TH
+--import Language.Haskell.TH
 
 
 -- For each datatype that we define, we need to also create its representation.
@@ -48,9 +48,9 @@
      ''Dept,
      ''CUnit,
      ''Employee,
- 	  ''Manager,
- 	  ''Person,
- 	  ''Salary])
+          ''Manager,
+          ''Person,
+          ''Salary])
 
 
 --
diff --git a/examples/F.hs b/examples/F.hs
--- a/examples/F.hs
+++ b/examples/F.hs
@@ -9,7 +9,6 @@
 module F where
 
 import Unbound.LocallyNameless
-import Unbound.LocallyNameless.NameInstances
 
 import Control.Monad
 import Control.Monad.Trans.Error
diff --git a/examples/LC.hs b/examples/LC.hs
--- a/examples/LC.hs
+++ b/examples/LC.hs
@@ -18,12 +18,14 @@
 
 -- | A very simple example demonstration of the binding library
 -- based on the untyped lambda calculus.
-module LC where
+module Examples.LC where
 
 import Unbound.LocallyNameless
 import Control.Monad.Reader (Reader, runReader)
 import Data.Set as S
 
+import System.Exit (exitFailure)
+
 -- | A Simple datatype for the Lambda Calculus
 data Exp = Var (Name Exp)
          | Lam (Bind (Name Exp) Exp)
@@ -74,8 +76,9 @@
   case e1' of
     -- look for a beta-reduction
     Lam bnd -> do
-        (x, e1'') <- unbind bnd
-        return $ subst x e2' e1''
+    --    (x, e1'') <- unbind bnd
+    --    return $ subst x e2' e1''
+      return $ substBind bnd e2'
     otherwise -> return $ App e1' e2'
 red (Lam bnd) = do
    (x, e) <- unbind bnd
@@ -92,12 +95,12 @@
 
 assert :: String -> Bool -> IO ()
 assert s True  = return ()
-assert s False = print ("Assertion " ++ s ++ " failed")
+assert s False = print ("Assertion " ++ s ++ " failed") >> exitFailure
 
 assertM :: String -> M Bool -> IO ()
 assertM s c =
   if (runFreshM c) then return ()
-  else print ("Assertion " ++ s ++ " failed")
+  else print ("Assertion " ++ s ++ " failed") >> exitFailure
 
 x :: Name Exp
 x = string2Name "x"
diff --git a/examples/Main.hs b/examples/Main.hs
--- a/examples/Main.hs
+++ b/examples/Main.hs
@@ -16,16 +16,17 @@
 
 module Main where
 
-import qualified Basic
-import qualified LC
-import qualified STLC
-import qualified Abstract
+import qualified Examples.Basic as Basic
+import qualified Examples.LC as LC
+import qualified Examples.STLC as STLC
+-- import qualified Examples.Abstract as Abstract
 
 
 main = do
      Basic.main
      LC.main
      STLC.main
-     Abstract.main
+     -- Abstract.main
+     -- F.main
      print "Tests completed"
      
diff --git a/examples/STLC.hs b/examples/STLC.hs
--- a/examples/STLC.hs
+++ b/examples/STLC.hs
@@ -16,7 +16,7 @@
 --
 -----------------------------------------------------------------------------
 
-module STLC where
+module Examples.STLC where
 
 import Unbound.LocallyNameless
 import Data.Set as S
diff --git a/test/Abstract.hs b/test/Abstract.hs
new file mode 100644
--- /dev/null
+++ b/test/Abstract.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
+             TemplateHaskell, UndecidableInstances #-}
+module Lib
+     where
+
+import Unbound.LocallyNameless
+
+data Term = Word Word
+  deriving Show
+
+$(derive_abstract [''Word]) -- No type structure information available
+$(derive [''Term])
+instance Alpha Word
+instance Alpha Term
+
+t1 :: Term
+t1 = Word 5
+
+wrong :: Bool
+wrong = t1 `aeq` t1 -- should throw an error as Word is "abstract"
+
diff --git a/test/F.hs b/test/F.hs
new file mode 100644
--- /dev/null
+++ b/test/F.hs
@@ -0,0 +1,324 @@
+{-# LANGUAGE TemplateHaskell,
+             ScopedTypeVariables,
+             FlexibleInstances,
+             MultiParamTypeClasses,
+             FlexibleContexts,
+             UndecidableInstances,
+             GADTs #-}
+
+module F where
+
+import Unbound.LocallyNameless hiding (prec,empty,Data,Refl)
+
+import Control.Monad
+import Control.Monad.Trans.Except
+import qualified Data.List as List
+import qualified Data.Set as Set
+
+import Test.QuickCheck
+
+import Util
+import Text.PrettyPrint as PP
+
+------------------------------------------------------
+-- System F with type and term variables
+------------------------------------------------------
+
+type TyName = Name Ty
+type TmName = Name Tm
+
+data Ty = TyVar TyName
+        | TyInt
+        | Arr Ty Ty
+        | All (Bind TyName Ty)
+        | TyProd [Ty]
+   deriving Show
+
+data Tm = TmInt Int
+        | TmVar TmName
+        | Fix (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)
+        | App Tm Tm
+        | TmProd [Tm]
+        | TmPrj Tm Int
+        | TmPrim Tm Prim Tm 
+        | TmIf0 Tm Tm Tm
+        | TLam (Bind TyName Tm)
+        | TApp Tm Ty
+        | Ann Tm Ty
+   deriving Show
+
+
+$(derive [''Ty, ''Tm])
+
+------------------------------------------------------
+instance Alpha Ty 
+instance Alpha Tm 
+
+instance Subst Tm Prim  
+instance Subst Tm Ty
+instance Subst Ty Prim
+instance Subst Ty Tm
+instance Subst Tm Tm where
+  isvar (TmVar x) = Just (SubstName x)
+  isvar _  = Nothing
+instance Subst Ty Ty where
+  isvar (TyVar x) = Just (SubstName x)
+  isvar _ = Nothing
+
+
+-----------------------------------------------------------------
+-- Arbitrary 
+-----------------------------------------------------------------
+
+arbTyName :: Gen (Name Ty)
+arbTyName = liftM string2Name (elements (map (:[]) ['a' .. 'z']))
+
+arbAll :: Gen Ty -> Gen Ty
+arbAll gty = do
+  ty <- gty
+  let fvs = fv ty
+  if Set.null fvs 
+    then return ty
+    else do      
+      i <- choose (0, Set.size fvs - 1) 
+      let v = Set.elemAt i fvs
+      return $ All (bind v ty)
+    
+
+genTy :: Int -> Gen Ty 
+genTy 1 = oneof [ return TyInt, liftM TyVar arbTyName ]
+genTy n = frequency [(1, return TyInt),
+                     (3, liftM  TyVar arbTyName),
+                     (4, liftM2 Arr go go),
+                     (20, arbAll go),
+                     (4, liftM  TyProd (listOf go))] where
+  go = genTy (n `div` 2)
+
+instance Arbitrary Ty where
+  arbitrary = sized genTy
+
+-----------------------------------------------------------------
+-- Typechecker
+-----------------------------------------------------------------
+type Delta = [ TyName ]
+type Gamma = [ (TmName, Ty) ]
+
+data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }
+emptyCtx = Ctx { getDelta = [], getGamma = [] }
+
+checkTyVar :: Ctx -> TyName -> M ()
+checkTyVar g v = do
+    if List.elem v (getDelta g) then
+      return ()
+    else
+      throwE "NotFound"
+
+lookupTmVar :: Ctx -> TmName -> M Ty
+lookupTmVar g v = do
+    case lookup v (getGamma g) of
+      Just s -> return s
+      Nothing -> throwE "NotFound"
+
+extendTy :: TyName -> Ctx -> Ctx
+extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }
+
+extendTm :: TmName -> Ty -> Ctx -> Ctx
+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }
+
+-- could be replaced with fv
+tcty :: Ctx -> Ty -> M ()
+tcty g  (TyVar x) =
+   checkTyVar g x
+tcty g  (All b) = do
+   (x, ty') <- unbind b
+   tcty (extendTy x g) ty'
+tcty g  (Arr ty1 ty2) = do
+   tcty g  ty1
+   tcty g  ty2
+tcty g TyInt =  return ()
+tcty g (TyProd tys) = do
+   _ <- mapM (tcty g) tys
+   return ()
+
+typecheck :: Ctx -> Tm -> M Tm
+typecheck g e@(TmVar x) = do 
+  ty <- lookupTmVar g x
+  return $ Ann e ty
+typecheck g (Fix bnd) = do
+  ((f, x, Embed (ty1, ty2)), e1) <- unbind bnd
+  tcty g ty1
+  tcty g ty2
+  ae1@(Ann _ ty2') <- typecheck (extendTm f (Arr ty1 ty2) (extendTm x ty1 g)) e1
+  if not (ty2 `aeq` ty2')
+    then throwE $ "Type Error: Can't match " ++ pp ty2 ++ " and " ++ pp ty2'
+    else return $ Ann 
+           (Fix (bind (f,x, Embed (ty1, ty2)) ae1))
+           (Arr ty1 ty2)
+typecheck g e@(App e1 e2) = do
+  ae1@(Ann _ ty1) <- typecheck g e1
+  ae2@(Ann _ ty2) <- typecheck g e2
+  case ty1 of
+    Arr ty11 ty21 | ty2 `aeq` ty11 ->
+      return (Ann (App ae1 ae2) ty21)
+    _ -> throwE "TypeError"
+typecheck g (TLam bnd) = do
+  (x, e) <- unbind bnd
+  ae@(Ann _ ty) <- typecheck (extendTy x g) e
+  return $ Ann (TLam (bind x ae)) (All (bind x ty))
+typecheck g (TApp e ty) = do
+  ae@(Ann _ tyt) <- typecheck g e
+  case tyt of
+   (All b) -> do
+      tcty g ty
+      (n1, ty1) <- unbind b
+      return $ Ann (TApp ae ty) (subst n1 ty ty1)
+typecheck g (TmProd es) = do 
+  atys <- mapM (typecheck g) es
+  let tys = map (\(Ann _ ty) -> ty) atys
+  return $ Ann (TmProd atys) (TyProd tys)
+typecheck g (TmPrj e i) = do
+  ae@(Ann _ ty) <- typecheck g e
+  case ty of 
+    TyProd tys | i < length tys -> return $ Ann (TmPrj ae i) (tys !! i)
+    _ -> throwE "TypeError"
+typecheck g (TmInt i) = return (Ann (TmInt i) TyInt)
+typecheck g (TmPrim e1 p e2) = do
+  ae1@(Ann _ ty1) <- typecheck g e1
+  ae2@(Ann _ ty2) <- typecheck g e2      
+  case (ty1 , ty2) of 
+    (TyInt, TyInt) -> return (Ann (TmPrim ae1 p ae2) TyInt)
+    _ -> throwE "TypeError"
+typecheck g (TmIf0 e0 e1 e2) = do
+  ae0@(Ann _ ty0) <- typecheck g e0
+  ae1@(Ann _ ty1) <- typecheck g e1
+  ae2@(Ann _ ty2) <- typecheck g e2
+  if ty1 `aeq` ty2 && ty0 `aeq` TyInt then 
+    return (Ann (TmIf0 ae0 ae1 ae2) ty1)
+  else   
+    throwE "TypeError"
+
+-----------------------------------------------------------------
+-- Small-step semantics
+-----------------------------------------------------------------
+
+value :: Tm -> Bool
+value (TmInt _)  = True
+value (Fix _)    = True
+value (TmProd es) = all value es
+value (TLam _)   = True
+value _          = False
+
+steps :: [Tm] -> M [Tm]
+steps [] = throwE "can't step empty list"
+steps (e:es) | value e = do
+  es' <- steps es
+  return (e : es')
+steps (e:es) = do 
+  e'  <- step e
+  return (e' : es)
+  
+step :: Tm -> M Tm
+step e | value e = throwE "can't step value"
+step (TmVar _)   = throwE "unbound variable" 
+step (App e1@(Fix bnd) e2) = 
+  if value e2 
+  then do
+    ((f, x, _), t) <- unbind bnd
+    return $ substs [ (x, e2), (f,e1) ] t
+  else do          
+    e2' <- step e2
+    return (App e1 e2') 
+step (App e1 e2) = do
+  e1' <- step e1
+  return (App e1' e2)
+step (TmPrj e1@(TmProd es) i) | value e1 && i < length es = return $ es !! i
+step (TmPrj e1 i) = do 
+  e1' <- step e1
+  return (TmPrj e1' i) 
+step (TmProd es) = do
+  es' <- steps es
+  return (TmProd es')
+step (TmPrim (TmInt i1) p (TmInt i2)) = 
+  return (TmInt ((evalPrim p) i1 i2))
+step (TmPrim e1 p e2) | value e1 = do
+  e2' <- step e2
+  return (TmPrim e1 p e2')
+  | otherwise = do
+  e1' <- step e1
+  return (TmPrim e1' p e2)
+step (TmIf0 (TmInt i) e1 e2) = if i==0 then return e1 else return e2
+step (TmIf0 e0 e1 e2) = do 
+  e0' <- step e0
+  return (TmIf0 e0' e1 e2)
+step (TApp (TLam bnd) ty) = do
+  (a, e) <- unbind bnd
+  return $ subst a ty e
+step (TApp e ty) = do
+  e' <- step e 
+  return $ TApp e' ty
+step (Ann e ty) = return e
+  
+evaluate :: Tm -> M Tm
+evaluate e = if value e then return e else do
+  e' <- step e
+  evaluate e'
+
+-----------------------------------------------------------------
+-- Pretty-printer
+-----------------------------------------------------------------
+
+instance Display Ty where
+  display (TyVar n)     = display n
+  display (TyInt)       = return $ text "Int"
+  display (Arr ty1 ty2) = do  
+    d1 <- withPrec (precedence "->" + 1) $ display ty1
+    d2 <- withPrec (precedence "->")     $ display ty2
+    binop d1 "->" d2
+  display (All bnd) = lunbind bnd $ \ (a,ty) -> do
+    da <- display a
+    dt <- display ty
+    prefix "forall" (da <> text "." <+> dt)
+  display (TyProd tys) = displayTuple tys
+    
+instance Display Tm where
+  display (TmInt i) = return $ int i
+  display (TmVar n) = display n
+  display (Fix bnd) = lunbind bnd $ \((f,x,Embed (ty1,ty2)), e) -> do
+    df <- display f 
+    dx <- display x      
+    d1 <- display ty1      
+    d2 <- display ty2
+    de <- withPrec (precedence "fix") $ display e
+    let arg = parens (dx <> colon <> d1)
+    --if f `elem` (fv e :: [F.TmName])
+      -- then 
+    prefix "fix" (df <+> arg <> colon <> d2 <> text "." <+> de)
+      -- else prefix "\\"  (arg <> text "." <+> de)
+  display (App e1 e2) = do
+    d1 <- withPrec (precedence " ") $ display e1
+    d2 <- withPrec (precedence " " + 1) $ display e2
+    binop d1 " " d2
+  display (TmProd es) = displayTuple es
+
+  display (TmPrj e i) = do
+    de <- display e 
+    return $ text "Pi" <> int i <+> de
+  display (TmPrim e1 p e2) = do 
+    let str = show p
+    d1 <- withPrec (precedence str)     $ display e1 
+    d2 <- withPrec (precedence str + 1) $ display e2 
+    binop d1 str d2
+  display (TmIf0 e0 e1 e2) = do
+    d0 <- display e0
+    d1 <- display e1
+    d2 <- display e2
+    prefix "if0" $ sep [d0 , text "then" <+> d1 , text "else" <+> d2]
+  display (TLam bnd) = lunbind bnd $ \(a,e) -> do
+    da <- display a
+    de <- withPrec (precedence "/\\") $ display e
+    prefix "/\\" (da <> text "." <+> de)
+  display (TApp e ty) = do
+    d1 <- withPrec (precedence " ") $ display e
+    d2 <- withPrec (precedence " " + 1) $ display ty
+    binop d1 " " d2
+  display (Ann e ty) = display e
diff --git a/test/Perf.hs b/test/Perf.hs
new file mode 100644
--- /dev/null
+++ b/test/Perf.hs
@@ -0,0 +1,17 @@
+
+import Criterion.Main (defaultMain)
+
+import F
+
+
+--- alpha equivalence (System F types)
+
+--- substitution
+
+--- type checking (System F programs)
+
+
+
+main = defaultMain [
+       , bench "fib 35" $ \n -> fib (35+n-n)
+       ]
diff --git a/test/Util.hs b/test/Util.hs
new file mode 100644
--- /dev/null
+++ b/test/Util.hs
@@ -0,0 +1,190 @@
+{-# LANGUAGE TypeSynonymInstances,FlexibleInstances #-}
+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Util where
+
+import Text.PrettyPrint as PP
+import Control.Applicative
+import Control.Monad.Identity
+import Control.Monad.Trans.Except
+import Control.Monad.Reader
+import qualified Data.Set as Set
+import qualified Data.List as List
+
+import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)
+import Unbound.LocallyNameless.Alpha
+import Unbound.LocallyNameless.Types
+
+
+import Test.QuickCheck
+
+------------------
+-- should move to Unbound.LocallyNameless.Ops
+patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t
+patUnbind p (B _ t) = openT p t
+------------------
+
+
+-------------------------------------------------------------------------
+-- Primitives
+-------------------------------------------------------------------------
+
+data Prim = Plus | Minus | Times deriving (Eq, Ord, Enum)
+
+instance Show Prim where
+  show Plus  = "+"
+  show Minus = "-"
+  show Times = "*"
+
+$(derive [''Prim])
+
+instance Alpha Prim
+
+evalPrim :: Prim -> Int -> Int -> Int
+evalPrim Plus  = (+)
+evalPrim Times = (*)
+evalPrim Minus = (-)
+
+instance Arbitrary Prim where
+  arbitrary = elements [Plus ..]
+
+
+
+-------------------------------------------------------------------------
+-- Monad for evaluation, typechecking and translation.
+-------------------------------------------------------------------------
+
+
+type M = ExceptT String FreshM
+
+runM :: M a -> a
+runM m = case (runFreshM (runExceptT m)) of
+   Left s  -> error s
+   Right a -> a
+
+
+-------------------------------------------------------------------------
+-- The Display class and other pretty printing helper functions
+-------------------------------------------------------------------------
+
+-- | pretty-print                  
+pp :: Display t => t -> String
+pp d = render (runIdentity (runReaderT (runDM (display d)) initDI))
+   
+class Display t where
+  -- | Convert a value to a 'Doc'.
+  display  :: t -> DM Doc   
+   
+newtype DM a = DM { runDM :: (ReaderT DispInfo Identity) a } 
+             deriving (Functor,Applicative,Monad)
+
+
+
+maybeParens :: Bool -> Doc -> Doc
+maybeParens b d = if b then parens d else d
+   
+   
+prefix :: String -> Doc -> DM Doc   
+prefix str d = do
+  di <- ask
+  return $ maybeParens (precedence str < prec di) (text str <+> d)
+   
+binop :: Doc -> String -> Doc -> DM Doc
+binop d1 str d2 = do 
+  di <- ask
+  let dop = if str == " " then sep [d1, d2] else sep [d1, text str, d2]
+  return $ maybeParens (precedence str < prec di) dop
+
+   
+   
+precedence :: String -> Int   
+precedence "->" = 10
+precedence " "  = 10
+precedence "forall" = 9
+precedence "if0"    = 9
+precedence "fix"    = 9
+precedence "\\"     = 9
+precedence "*"  = 8
+precedence "+"  = 7
+precedence "-"  = 7
+precedence  _   = 0
+   
+
+
+instance MonadReader DispInfo DM where
+  ask     = DM ask
+  local f (DM m) = DM (local f m) 
+
+-- | The data structure for information about the display
+-- 
+data DispInfo = DI
+  {
+  prec       :: Int,              -- ^ precedence level  
+  showTypes  :: Bool,             -- ^ should we show types?  
+  dispAvoid  :: Set.Set AnyName   -- ^ names that have been used
+  }
+
+instance LFresh DM where
+  lfresh nm = do
+      let s = name2String nm
+      di <- ask;
+      return $ head (filter (\x -> AnyName x `Set.notMember` (dispAvoid di))
+                      (map (makeName s) [0..]))
+  getAvoids = dispAvoid <$> ask
+  avoid names = local upd where
+     upd di = di { dispAvoid = 
+                      (Set.fromList names) `Set.union` (dispAvoid di) }
+
+
+-- | An empty 'DispInfo' context
+initDI :: DispInfo
+initDI = DI 10 False Set.empty
+
+withPrec :: Int -> DM a -> DM a
+withPrec i = 
+  local $ \ di -> di { prec = i }
+                  
+getPrec :: DM Int                  
+getPrec = do
+  di <- ask
+  return (prec di)
+  
+  
+intersperse             :: Doc -> [Doc] -> [Doc]
+intersperse _   []      = []
+intersperse _   [x]     = [x]
+intersperse sep (x:xs)  = x <> sep : intersperse sep xs
+
+displayList :: Display t => [t] -> DM Doc  
+displayList es = do
+  ds <- mapM (withPrec 0 . display) es
+  return $ cat (intersperse comma ds)
+  
+displayTuple :: Display t => [t] -> DM Doc  
+displayTuple es = do  
+  ds <- displayList es
+  return $ text "<" <> ds <> text ">"  
+
+--------------------------------------------
+
+instance Rep a => Display (Name a) where
+  display n = return $ (text . show) n
+  
+--------------------------------------------
+
+instance Display String where
+  display = return . text
+instance Display Int where
+  display = return . text . show
+instance Display Integer where
+  display = return . text . show
+instance Display Double where
+  display = return . text . show
+instance Display Float where
+  display = return . text . show
+instance Display Char where
+  display = return . text . show
+instance Display Bool where
+  display = return . text . show
+
diff --git a/unbound.cabal b/unbound.cabal
--- a/unbound.cabal
+++ b/unbound.cabal
@@ -1,12 +1,12 @@
 name:           unbound
-version:        0.4.4
+version:        0.5.0
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
 cabal-version:  >= 1.10
-tested-with:    GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10
+tested-with:    GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10, GHC == 8.0.1
 author:         Stephanie Weirich, Brent Yorgey
-maintainer:     Stephanie Weirich <sweirich@cis.upenn.edu>, Brent Yorgey <byorgey@cis.upenn.edu> 
+maintainer:     Stephanie Weirich <sweirich@cis.upenn.edu>
 homepage:       https://github.com/sweirich/replib
 category:       Language, Generics, Compilers/Interpreters
 extra-source-files: README,
@@ -31,9 +31,9 @@
   build-depends: base >= 4.3 && < 5,
                  RepLib >= 0.5.3 && < 0.6,
                  mtl >= 2.0 && < 2.3,
-                 transformers >= 0.2.2.0 && < 0.5,
+                 transformers >= 0.2.2.0 && < 0.6,
                  containers >= 0.3 && < 0.6,
-                 binary >= 0.7 && < 0.8
+                 binary >= 0.7 && < 0.9
   exposed-modules:
     Unbound.LocallyNameless,
     Unbound.LocallyNameless.Name,
@@ -43,7 +43,8 @@
     Unbound.LocallyNameless.Subst,
     Unbound.LocallyNameless.Ops,
     Unbound.PermM,
-    Unbound.Util
+    Unbound.Util,
+    Unbound.DynR
   other-extensions: CPP
                     EmptyDataDecls
                     ExistentialQuantification
@@ -60,3 +61,21 @@
                     TypeSynonymInstances
                     UndecidableInstances
   default-language: Haskell2010
+
+Test-Suite lambda-calculus
+    default-language: Haskell2010
+    build-depends: base >= 4.3 && < 5,
+                 RepLib >= 0.5.3 && < 0.6,
+                 mtl >= 2.0 && < 2.3,
+                 transformers >= 0.2.2.0 && < 0.6,
+                 containers >= 0.3 && < 0.6,
+                 binary >= 0.7 && < 0.9,
+                 unbound >= 0.5,
+                 template-haskell >= 2.11,
+                 parsec >= 3.1.9 && < 3.2,
+                 pretty>= 1.1.2 && < 1.2,
+                 QuickCheck>=2.8.2 && < 2.9
+
+
+    type:       exitcode-stdio-1.0
+    main-is:    examples/Main.hs