diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -41,3 +41,11 @@
 Version 0.3.1: 25 August 2011
 
   * Update to build on GHC 7.2.1
+
+Version 0.4: 15 March 2012
+
+  * Update to build on GHC 7.4.1
+  
+  * add MonadWriter instances for FreshMT and LFreshMT
+
+  * Make 'getAvoids' function into a method of the LFresh class
diff --git a/Unbound/LocallyNameless.hs b/Unbound/LocallyNameless.hs
--- a/Unbound/LocallyNameless.hs
+++ b/Unbound/LocallyNameless.hs
@@ -239,7 +239,7 @@
     --   can be freely combined with other standard monads and monad
     --   transformers from the @transformers@ library.
 
-    LFreshM, runLFreshM, getAvoids,
+    LFreshM, runLFreshM,
     LFreshMT, runLFreshMT,
 
     -- * The @Alpha@ class
diff --git a/Unbound/LocallyNameless/Fresh.hs b/Unbound/LocallyNameless/Fresh.hs
--- a/Unbound/LocallyNameless/Fresh.hs
+++ b/Unbound/LocallyNameless/Fresh.hs
@@ -32,7 +32,7 @@
 
     LFresh(..),
 
-    LFreshM, runLFreshM, contLFreshM, getAvoids,
+    LFreshM, runLFreshM, contLFreshM,
     LFreshMT(..), runLFreshMT, contLFreshMT
 
   ) where
@@ -64,6 +64,7 @@
 import qualified Control.Monad.Error.Class as EC
 import qualified Control.Monad.State.Class as StC
 import qualified Control.Monad.Reader.Class as RC
+import qualified Control.Monad.Writer.Class as WC
 
 ------------------------------------------------------------
 -- Fresh
@@ -164,8 +165,11 @@
   ask   = lift RC.ask
   local f = FreshMT . RC.local f . unFreshMT
 
----------------------------------------------------
--- LFresh
+instance WC.MonadWriter w m => WC.MonadWriter w (FreshMT m) where
+  tell   = lift . WC.tell
+  listen = FreshMT . WC.listen . unFreshMT
+  pass   = FreshMT . WC.pass . unFreshMT
+
 ---------------------------------------------------
 
 -- | This is the class of monads that support freshness in an
@@ -177,6 +181,8 @@
   -- | Avoid the given names when freshening in the subcomputation,
   --   that is, add the given names to the in-scope set.
   avoid   :: [AnyName] -> m a -> m a
+  -- | Get the set of names currently being avoided.
+  getAvoids :: m (Set AnyName)
 
 -- | The LFresh monad transformer.  Keeps track of a set of names to
 -- avoid, and when asked for a fresh one will choose the first numeric
@@ -192,10 +198,6 @@
 contLFreshMT :: LFreshMT m a -> Set AnyName -> m a
 contLFreshMT (LFreshMT m) = runReaderT m
 
--- | Get the set of names currently being avoided.
-getAvoids :: Monad m => LFreshMT m (Set AnyName)
-getAvoids = LFreshMT ask
-
 instance Monad m => LFresh (LFreshMT m) where
   lfresh nm = LFreshMT $ do
     let s = name2String nm
@@ -204,6 +206,8 @@
                           (map (makeName s) [0..]))
   avoid names = LFreshMT . local (S.union (S.fromList names)) . unLFreshMT
 
+  getAvoids = LFreshMT ask
+
 -- | A convenient monad which is an instance of 'LFresh'.  It keeps
 --   track of a set of names to avoid, and when asked for a fresh one
 --   will choose the first unused numerical name.
@@ -220,42 +224,52 @@
 instance LFresh m => LFresh (ContT r m) where
   lfresh = lift . lfresh
   avoid  = mapContT . avoid
+  getAvoids = lift getAvoids
 
 instance (Error e, LFresh m) => LFresh (ErrorT e m) where
   lfresh = lift . lfresh
   avoid  = mapErrorT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (IdentityT m) where
   lfresh = lift . lfresh
   avoid  = mapIdentityT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (ListT m) where
   lfresh = lift . lfresh
   avoid  = mapListT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (MaybeT m) where
   lfresh = lift . lfresh
   avoid  = mapMaybeT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (ReaderT r m) where
   lfresh = lift . lfresh
   avoid  = mapReaderT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (Lazy.StateT s m) where
   lfresh = lift . lfresh
   avoid  = Lazy.mapStateT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (Strict.StateT s m) where
   lfresh = lift . lfresh
   avoid  = Strict.mapStateT . avoid
+  getAvoids = lift getAvoids
 
 instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where
   lfresh = lift . lfresh
   avoid  = Lazy.mapWriterT . avoid
+  getAvoids = lift getAvoids
 
 instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where
   lfresh = lift . lfresh
   avoid  = Strict.mapWriterT . avoid
+  getAvoids = lift getAvoids
 
 -- Instances for applying LFreshMT to other monads
 
@@ -276,3 +290,8 @@
 instance RC.MonadReader r m => RC.MonadReader r (LFreshMT m) where
   ask   = lift RC.ask
   local f = LFreshMT . mapReaderT (RC.local f) . unLFreshMT
+
+instance WC.MonadWriter w m => WC.MonadWriter w (LFreshMT m) where
+  tell   = lift . WC.tell
+  listen = LFreshMT . WC.listen . unLFreshMT
+  pass   = LFreshMT . WC.pass . unLFreshMT
diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs
--- a/Unbound/LocallyNameless/Ops.hs
+++ b/Unbound/LocallyNameless/Ops.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeSynonymInstances
            , FlexibleInstances
+           , CPP
   #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 ----------------------------------------------------------------------
@@ -25,6 +26,10 @@
 import Data.Maybe (catMaybes)
 import Data.List  (sortBy)
 import Data.Ord   (comparing)
+
+#if MIN_VERSION_base(4,5,0)
+import Data.Monoid
+#endif
 
 import Control.Monad (liftM)
 import qualified Text.Read as R
diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs
--- a/Unbound/LocallyNameless/Subst.hs
+++ b/Unbound/LocallyNameless/Subst.hs
@@ -30,6 +30,10 @@
 -- | See 'isvar'.
 data SubstName a b where
   SubstName :: (a ~ b) => Name a -> SubstName a b
+  
+-- | See 'isCoerceVar'  
+data SubstCoerce a b where  
+  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
 
 -- | The @Subst@ class governs capture-avoiding substitution.  To
 --   derive this class, you only need to indicate where the variables
@@ -43,6 +47,13 @@
   --   returns 'Nothing'.
   isvar :: a -> Maybe (SubstName a b)
   isvar _ = Nothing
+  
+  -- | This is an alternative version to 'isvar', useable in the case 
+  --   that the substituted argument doesn't have *exactly* the same type
+  --   as the term it should be substituted into.
+  --   The default implementation always returns 'Nothing'.
+  isCoerceVar :: a -> Maybe (SubstCoerce a b)
+  isCoerceVar _ = Nothing
 
   -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@.  It has
   --   a default generic implementation in terms of @isvar@.
@@ -50,7 +61,9 @@
   subst n u x | isFree n =
      case (isvar x :: Maybe (SubstName a b)) of
         Just (SubstName m) -> if  m == n then u else x
-        Nothing -> substR1 rep1 n u x
+        Nothing -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of 
+           Just (SubstCoerce m f) -> if m == n then maybe x id (f u) else x
+           Nothing -> substR1 rep1 n u x
   subst m _ _ = error $ "Cannot substitute for bound variable " ++ show m
 
   -- | Perform several simultaneous substitutions.  This method also
@@ -63,7 +76,12 @@
           case find ((==m) . fst) ss of
             Just (_, u) -> u
             Nothing     -> x
-        Nothing -> substsR1 rep1 ss x
+        Nothing -> case isCoerceVar x :: Maybe (SubstCoerce a b) of 
+            Just (SubstCoerce m f) ->
+              case find ((==m) . fst) ss of 
+                  Just (_, u) -> maybe x id (f u)
+                  Nothing -> x
+            Nothing -> substsR1 rep1 ss x
     | otherwise =
       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)
 
diff --git a/Unbound/Util.hs b/Unbound/Util.hs
--- a/Unbound/Util.hs
+++ b/Unbound/Util.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 ----------------------------------------------------------------------
 -- |
 -- Module      :  Unbound.Util
@@ -21,8 +23,13 @@
 -- Convenient Monoid syntax
 ------------------------------------------------------------
 
+-- As of base-4.5, (<>) is exported by Data.Monoid.
+
+#if MIN_VERSION_base(4,5,0)
+#else
 (<>) :: Monoid m => m -> m -> m
 (<>) = mappend
+#endif
 
 ------------------------------------------------------------
 -- Collections
diff --git a/examples/LCTyped.hs b/examples/LCTyped.hs
deleted file mode 100644
--- a/examples/LCTyped.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# LANGUAGE GADTs
-           , TemplateHaskell
-           , KindSignatures
-           , ScopedTypeVariables
-           , TypeOperators
-  #-}
-
-module LCTyped where
-
-import Unbound.LocallyNameless
-import Data.Type.Equality
-
-import Unsafe.Coerce (unsafeCoerce)
-
-
-
-------------------------------------------------------------
-
-data Res1 c a where
-  Result1   :: Rep b => a :=: (c b) -> Res1 c a
-  NoResult1 :: Res1 c a
-
-destr1 :: R a -> R (c d) -> Res1 c a
-destr1 (Data (DT s1 ((_ :: R b) :+: MNil)) _)
-       (Data (DT s2 _) _)
-  | s1 == s2  = Result1 (unsafeCoerce Refl :: a :=: (c b))
-  | otherwise = NoResult1
-destr1 _ _ = NoResult1
-
-data Res2 c2 a where
-  Result2   :: (Rep d, Rep e) => a :=: (c2 d e) -> Res2 c2 a
-  NoResult2 :: Res2 c2 a
-
-destr2 :: R a -> R (c2 d e) -> Res2 c2 a
-destr2 (Data (DT s1 ((_ :: R d) :+: (_ :: R e) :+: MNil)) _)
-       (Data (DT s2 _) _)
-  | s1 == s2  = Result2 (unsafeCoerce Refl :: a :=: (c2 d e))
-  | otherwise = NoResult2
-destr2 _ _ = NoResult2
-
-------------------------------------------------------------
-
-
-data V :: * -> * -> * where
-  VZ :: V (a,env) a
-  VS :: V env a -> V (b,env) a
-
-data Tm :: * -> * -> * where
-  Var :: V env a -> Tm env a
-  Lam :: Tm (a,env) b -> Tm env (a -> b)
-  App :: Tm env (a -> b) -> Tm env a -> Tm env b
-
-$(derive [''V, ''Tm])
diff --git a/unbound.cabal b/unbound.cabal
--- a/unbound.cabal
+++ b/unbound.cabal
@@ -1,10 +1,10 @@
 name:           unbound
-version:        0.3.1
+version:        0.4
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
 cabal-version:  >= 1.6
-tested-with:    GHC == 7.0.1, GHC == 7.0.3, GHC == 7.0.4, GHC == 7.2.1
+tested-with:    GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1
 author:         Stephanie Weirich
 maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>
                 Stephanie Weirich <sweirich@cis.upenn.edu>