diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -29,7 +29,7 @@
 
   * Clean up some compiler warnings.
 
-Version 0.2.6: 24 August 2011
+Version 0.3: 24 August 2011
 
   * New permutation- and set-binding functions, for creating binders
     which don't care about the order of multiple bound names, and/or
@@ -37,3 +37,7 @@
 
   * Bump RepLib dependency to 0.5, which now has support for GADTs
     without existential type variables.
+
+Version 0.3.1: 25 August 2011
+
+  * Update to build on GHC 7.2.1
diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs
--- a/Unbound/LocallyNameless/Alpha.hs
+++ b/Unbound/LocallyNameless/Alpha.hs
@@ -340,17 +340,16 @@
   freshenD  :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
   lfreshenD :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
   aeqD      :: AlphaCtx -> a -> a -> Bool,
-  -- matchD    :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
+  acompareD :: AlphaCtx -> a -> a -> Ordering,
   closeD    :: Alpha b => AlphaCtx -> b -> a -> a,
   openD     :: Alpha b => AlphaCtx -> b -> a -> a,
   findpatD  :: a -> AnyName -> FindResult,
-  nthpatD   :: a -> NthCont,
-  acompareD :: AlphaCtx -> a -> a -> Ordering
+  nthpatD   :: a -> NthCont
   }
 
 instance Alpha a => Sat (AlphaD a) where
   dict = AlphaD isPat isTerm isEmbed swaps' fv' freshen' lfreshen' aeq' -- match'
-           close open findpatrec nthpatrec acompare'
+          acompare' close open findpatrec nthpatrec 
 
 ----------------------------------------------------------------------
 -- Generic definitions for 'Alpha' methods.  (Note that all functions
@@ -773,7 +772,7 @@
 
 -- note: for Embeds, when the mode is "term" then we are
 -- implementing the "binding" version of the function
--- and we generally should treat the annots as constants
+-- and we generally should treat the embeds as constants
 instance Alpha t => Alpha (Embed t) where
    isPat (Embed t)   = if (isTerm t) then Just [] else Nothing
    isTerm _          = False
diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs
--- a/Unbound/LocallyNameless/Ops.hs
+++ b/Unbound/LocallyNameless/Ops.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE TypeSynonymInstances
+           , FlexibleInstances
+  #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 ----------------------------------------------------------------------
 -- |
diff --git a/Unbound/Util.hs b/Unbound/Util.hs
--- a/Unbound/Util.hs
+++ b/Unbound/Util.hs
@@ -91,3 +91,6 @@
   union     = S.union
   cmap      = S.map
 
+disjoint :: Ord a => S.Set a -> S.Set a -> Bool
+disjoint s1 s2 = S.null( S.intersection s1 s2 )
+
diff --git a/examples/LCTyped.hs b/examples/LCTyped.hs
new file mode 100644
--- /dev/null
+++ b/examples/LCTyped.hs
@@ -0,0 +1,53 @@
+{-# 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
+version:        0.3.1
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
 cabal-version:  >= 1.6
-tested-with:    GHC == 7.0.1, GHC == 7.0.3
+tested-with:    GHC == 7.0.1, GHC == 7.0.3, GHC == 7.0.4, GHC == 7.2.1
 author:         Stephanie Weirich
 maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>
                 Stephanie Weirich <sweirich@cis.upenn.edu>
@@ -30,7 +30,7 @@
 
 Library
   build-depends: base >= 4.3 && < 5,
-                 RepLib >= 0.5,
+                 RepLib >= 0.5.1 && < 0.6,
                  mtl >= 2.0 && < 2.1, transformers >= 0.2.2.0 && < 0.2.3,
                  containers >= 0.3 && < 0.5
   exposed-modules: