diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,92 @@
+# NEXT
+
+# 0.4.0
+
+* New binding specification type `Ignore`.
+
+  Any two `Ignore T` terms will always be alpha-equivalent to each other, will
+  be considered to contain no variables, and will not have any substitution
+  apply beneath `Ignore`.  Useful for attaching annotation terms to your AST.
+
+  ```haskell
+    import Text.Parsec.Pos (SourcePos)
+    
+	data Expr =
+	   ...
+	   | Lambda (Ignore SourcePos) (Bind (Name Expr) Expr)
+  ```
+
+  As expected, any two `Lambda` expressions will be considered alpha-equivalent
+  even if they differ in source position.
+
+  Note that the `Ignore` will block operations on `Name a` for all `a`, which can be a little unexpected:
+
+  ```haskell
+    data Ty =
+	  TyVar (Name Ty)
+      | TyArr Ty Ty
+    
+    instance Subst Ty Ty where
+	  ...
+
+	data Expr =
+	  ...
+	  | Var (Name Expr)
+	  | Lambda (Ignore Ty) (Bind (Name Expr) Expr)
+    
+     instance Subst Ty Expr
+  ```
+
+  Applying a substitution of a type for a free type variable to a `Lambda` will
+  not descend into the `Ignore Ty`.
+
+  Thanks Reed Mullanix (TOTWBF) for the new operation.
+
+* Fix an issue in substitution where traversal would not continue in
+  an AST node for which `isvar` or `isCoerceVar` is defined to return
+  non-`Nothing` but which had additional structure.
+
+  For example, in a language with meta variables and explicit substitutions:
+  ```haskell
+     data Expr =
+	   ...
+         -- normal variables that stand for expressions
+       | Var (Name Expr)
+          -- a meta variable occurrence and an explicit substitution
+		  -- of expressions to substitute in for the free variables
+	   | MetaVar (Name Meta) [(Name Expr, Expr)]
+     -- a meta variable stands for an expression with some free term vars
+	 data Meta = MetaVar Expr
+
+     -- substitution for a meta in an expression
+	 instance Subst Expr Meta where
+	   isCoerceVar (MetaVar u sub) = Just (SubstCoerce u (Just . applyExplicitSubst sub))
+	 applyExplicitSubst :: [(Name Expr, Expr)] -> Meta -> Expr
+	 applyExplicitSubst s (MetaVar e) = substs s e
+  ```
+
+  Given an expression `e1` defined as `MetaVar "u" [("x", 10)]`, we may want to
+  substitute a `Meta ("x" + "x")` for `"u"`  to get `10 + 10` (that is,
+  we replace `"u"` by the expression `"x" + "x"` and immediately apply
+  the substitution `10` for `"x"`).
+
+  Now suppose we have an expression `e2` defined as `MetaVar "v" [("y",
+  e1)]` (that is, an occurrence of meta var "v" together with a
+  substitution of `e1` from above for `"y"`).  If we again try to
+  substitute `Meta ("x" + "x")` for `"u"` in `e2`, we would expect to
+  get `MetaVar "v" [("y", 10 + 10)]` (that is, since "v" is not equal to
+  "u", we leave the meta var alone, but substitute for any occurrences
+  of "u" in the explicit substitution, so `e1` becomes `10 + 10` as
+  before).
+
+  The bug in previous versions of `unbound-generics` was that we would
+  incorrectly leave `MetaVar "v" [("y", e1)]` unchanged as soon as we
+  saw that `isCoerceVar (MetaVar "v" [("y", e1)])` returned
+  `Just (SubstCoerce "u" ...)` where `"u" /= "v"`.
+
+  Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue.
+  https://github.com/lambdageek/unbound-generics/issues/26
+
 # 0.3.4
 
 * Bump `containers` upper bound to support `0.6`.
diff --git a/examples/Prof.hs b/examples/Prof.hs
new file mode 100644
--- /dev/null
+++ b/examples/Prof.hs
@@ -0,0 +1,42 @@
+{-# language GADTs, RankNTypes #-}
+module Prof where
+
+import Data.Profunctor
+
+data Shop a b s t where
+  Shop :: (s -> a) -> (s -> b -> t) -> Shop a b s t
+
+type Optic p s t a b  = p a b -> p s t
+type Lens s t a b = forall p . (Strong p) => Optic p s t a b
+
+lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
+lens get set pab = dimap (\s -> (s, get s)) (uncurry set) (second' pab)
+
+instance Profunctor (Shop a b) where
+  dimap f g (Shop get set) = Shop (get . f) (\s -> g . set (f s))
+
+instance Strong (Shop a b) where
+   first' (Shop get set) = Shop (get . fst) (\(s,c) b -> (set s b, c))
+
+withLens :: Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
+withLens l k = case l (Shop id (const id)) of
+                 Shop getter setter -> k getter setter
+
+
+type Prism s t a b = forall p . (Choice p) => Optic p s t a b
+
+prism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
+prism view review pab = dimap view (either id review) (right' pab)
+
+data Market a b s t where
+  Market :: (s -> Either t a) -> (b -> t) -> Market a b s t
+
+instance Profunctor (Market a b) where
+  dimap f g (Market view review) = Market (either (Left . g) Right . (view . f)) (g . review)
+
+instance Choice (Market a b) where
+  left' (Market view review) = Market (either (either (Left . Left) Right . view) (Left . Right)) (Left . review)
+
+withPrism :: Prism s t a b -> ((s -> Either t a) -> (b -> t) -> r) -> r
+withPrism l k = case l (Market Right id) of
+                  Market view review -> k view review
diff --git a/src/Unbound/Generics/LocallyNameless.hs b/src/Unbound/Generics/LocallyNameless.hs
--- a/src/Unbound/Generics/LocallyNameless.hs
+++ b/src/Unbound/Generics/LocallyNameless.hs
@@ -20,6 +20,7 @@
   module Unbound.Generics.LocallyNameless.Name,
   module Unbound.Generics.LocallyNameless.Operations,
   module Unbound.Generics.LocallyNameless.Bind,
+  module Unbound.Generics.LocallyNameless.Ignore,
   module Unbound.Generics.LocallyNameless.Embed,
   module Unbound.Generics.LocallyNameless.Shift,
   module Unbound.Generics.LocallyNameless.Rebind,
@@ -32,6 +33,7 @@
 import Unbound.Generics.LocallyNameless.Alpha
 import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn)
 import Unbound.Generics.LocallyNameless.Bind hiding (B)
+import Unbound.Generics.LocallyNameless.Ignore hiding (I)
 import Unbound.Generics.LocallyNameless.Embed
 import Unbound.Generics.LocallyNameless.Shift
 import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)
diff --git a/src/Unbound/Generics/LocallyNameless/Ignore.hs b/src/Unbound/Generics/LocallyNameless/Ignore.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Ignore.hs
@@ -0,0 +1,47 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Ignore
+-- Copyright  : (c) 2018, Reed Mullanix
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Reed Mullanix
+-- Stability  : experimental
+--
+-- Ignores a term for the purposes of alpha-equality and substitution
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Ignore (
+    Ignore(..)
+    ) where
+
+import Control.DeepSeq (NFData(..))
+import Control.Applicative
+import Data.Monoid 
+
+import GHC.Generics (Generic)
+
+import Unbound.Generics.LocallyNameless.Alpha
+
+-- | Ignores a term 't' for the purpose of alpha-equality and substitution
+data Ignore t = I !t
+        deriving (Generic)
+
+instance (NFData t) => NFData (Ignore t) where
+    rnf (I t) = rnf t `seq` ()
+
+instance (Show t) => Show (Ignore t) where
+    showsPrec prec (I t) = 
+        showParen (prec > 0) (showString "<-" 
+                              . showsPrec prec t
+                              . showString "->")
+
+instance (Show t) => Alpha (Ignore t) where
+    aeq' _ _ _ = True
+    fvAny' _ _ = pure
+    isPat _ = inconsistentDisjointSet
+    isTerm _ = mempty
+    close _ _ = id
+    open _ _ = id
+    namePatFind  _ = NamePatFind $ const $ Left 0
+    nthPatFind _ = NthPatFind Left
+    swaps' _ _ = id
+    lfreshen' _ i cont = cont i mempty
+    freshen' _ i = return (i, mempty)
+    acompare' _ _ _ = EQ
diff --git a/src/Unbound/Generics/LocallyNameless/Operations.hs b/src/Unbound/Generics/LocallyNameless/Operations.hs
--- a/src/Unbound/Generics/LocallyNameless/Operations.hs
+++ b/src/Unbound/Generics/LocallyNameless/Operations.hs
@@ -40,6 +40,10 @@
        , trec
        , untrec
        , luntrec
+         -- * Opaque terms
+       , Ignore
+       , ignore
+       , unignore
        ) where
 
 import Control.Applicative (Applicative)
@@ -55,6 +59,7 @@
 import Unbound.Generics.LocallyNameless.Embed (Embed(..), IsEmbed(..))
 import Unbound.Generics.LocallyNameless.Rebind
 import Unbound.Generics.LocallyNameless.Rec
+import Unbound.Generics.LocallyNameless.Ignore
 import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
 import Unbound.Generics.LocallyNameless.Internal.Lens (view)
 import Unbound.Generics.LocallyNameless.Internal.Iso (from)
@@ -213,3 +218,11 @@
 luntrec :: (Alpha p, LFresh m) => TRec p -> m p
 luntrec (TRec b) =
   lunbind b $ \(p, ()) -> return (unrec p)
+
+-- | Constructor for ignoring a term for the purposes of alpha-equality and substs
+ignore :: t -> Ignore t
+ignore t = I t
+
+-- | Destructor for ignored terms
+unignore :: Ignore t -> t
+unignore (I t) = t
diff --git a/src/Unbound/Generics/LocallyNameless/Subst.hs b/src/Unbound/Generics/LocallyNameless/Subst.hs
--- a/src/Unbound/Generics/LocallyNameless/Subst.hs
+++ b/src/Unbound/Generics/LocallyNameless/Subst.hs
@@ -56,6 +56,7 @@
 import Unbound.Generics.LocallyNameless.Alpha
 import Unbound.Generics.LocallyNameless.Embed
 import Unbound.Generics.LocallyNameless.Shift
+import Unbound.Generics.LocallyNameless.Ignore
 import Unbound.Generics.LocallyNameless.Bind
 import Unbound.Generics.LocallyNameless.Rebind
 import Unbound.Generics.LocallyNameless.Rec
@@ -90,10 +91,10 @@
   subst n u x =
     if (isFreeName n)
     then case (isvar x :: Maybe (SubstName a b)) of
-      Just (SubstName m) -> if m == n then u else 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 -> to $ gsubst n u (from x)
+      Just (SubstName m) | m == n -> u
+      _ -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of
+        Just (SubstCoerce m f) | m == n -> maybe x id (f u)
+        _ -> to $ gsubst n u (from x)
     else error $ "Cannot substitute for bound variable " ++ show n
 
   substs :: [(Name b, b)] -> a -> a
@@ -101,16 +102,10 @@
   substs ss x
     | all (isFreeName . fst) ss =
       case (isvar x :: Maybe (SubstName a b)) of
-        Just (SubstName m) ->
-          case find ((==m) . fst) ss of
-            Just (_, u) -> u
-            Nothing     -> 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 -> to $ gsubsts ss (from x)
+        Just (SubstName m) | Just (_, u) <- find ((==m) . fst) ss -> u
+        _ -> case isCoerceVar x :: Maybe (SubstCoerce a b) of 
+            Just (SubstCoerce m f) | Just (_, u) <- find ((==m) . fst) ss -> maybe x id (f u)
+            _ -> to $ gsubsts ss (from x)
     | otherwise =
       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)
 
@@ -185,3 +180,7 @@
 instance (Subst c p) => Subst c (Rec p)
 
 instance (Alpha p, Subst c p) => Subst c (TRec p)
+
+instance Subst a (Ignore b) where
+  subst _ _ = id
+  substs _ = id
diff --git a/test/TestIgnore.hs b/test/TestIgnore.hs
new file mode 100644
--- /dev/null
+++ b/test/TestIgnore.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}
+module TestIgnore (test_ignore) where
+
+import Data.Typeable(Typeable)
+import GHC.Generics (Generic)
+import Unbound.Generics.LocallyNameless
+
+import AlphaAssertions
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+type Var = Name Term
+
+type SourcePos = (Int, Int)
+data SourceSpan = SourceSpan 
+    { start :: SourcePos
+    , end :: SourcePos
+    }
+    deriving (Show)
+
+data Term
+    = Var Var
+    | Lam (Bind Var Term)
+    | App Term Term
+    | Ann (Ignore SourceSpan) Term
+    | NoSubst (Ignore Term)
+    deriving (Show, Typeable, Generic)
+
+instance Alpha Term
+instance Subst Term Term where
+    isvar (Var x) = Just $ SubstName x
+    isvar _ = Nothing
+
+lam :: Var -> Term -> Term
+lam x t = Lam (bind x t)
+
+x :: Var
+x = s2n "x"
+
+y :: Var
+y = s2n "y"
+
+t1 :: Term
+t1 = Ann (ignore (SourceSpan (0,0) (0,1))) (Var x)
+
+t2 :: Term
+t2 = Ann (ignore (SourceSpan (1,0) (1,10))) (Var x)
+
+test_ignore :: TestTree
+test_ignore =
+    testCase "<-(0,0) (0,1)-> x = <-(1,0) (1,10)-> x" $ assertAeq t1 t2
diff --git a/test/TestRefine.hs b/test/TestRefine.hs
new file mode 100644
--- /dev/null
+++ b/test/TestRefine.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}
+module TestRefine (test_refine) where
+
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+import Unbound.Generics.LocallyNameless
+
+import AlphaAssertions
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- Regular variables range over terms
+type Var = Name Term
+
+-- Metavariables range over extracts
+type MetaVar = Name Extract
+
+data Term 
+    = Var Var
+    | Hole MetaSubst MetaVar -- Every occurance of a metavariable must subst away fvs of extract
+    | Lam (Bind Var Term)
+    | App Term Term
+    deriving (Generic, Typeable, Show)
+
+-- Extracts represent code extracted via refinement
+newtype Extract = Extract { extractTerm :: Term }
+    deriving (Generic, Typeable, Show)
+
+newtype MetaSubst = MetaSubst { unMetaSubst :: [(Var, Term)] }
+    deriving (Generic, Typeable, Show)
+
+instance Alpha Term
+instance Alpha Extract
+instance Alpha MetaSubst
+
+instance Subst Term Term where
+    isvar (Var x) = Just $ SubstName x
+    isvar _ = Nothing
+
+instance Subst Extract Term where
+    isCoerceVar (Hole ms x) = Just $ SubstCoerce x (Just . applyMetaSubst ms)
+    isCoerceVar _ = Nothing
+
+applyMetaSubst :: MetaSubst -> Extract -> Term
+applyMetaSubst (MetaSubst ms) e = substs ms $ extractTerm e
+
+instance Subst Term MetaSubst
+instance Subst Extract MetaSubst
+
+test_refine :: TestTree
+test_refine =
+    testCase "subst ?1 x <a/?1>?0 = <a/x>?0"
+    $ let h0 = s2n "0" :: MetaVar
+          h1 = s2n "1" :: MetaVar
+          a = s2n "a" :: Var
+          x = s2n "x" :: Var
+          e1 = Hole (MetaSubst [(a, Hole (MetaSubst []) h1)]) h0
+          e2 = Hole (MetaSubst [(a, Var x)]) h0
+      in assertAeq (subst h1 (Extract $ Var x) e1) e2
diff --git a/test/test-main.hs b/test/test-main.hs
--- a/test/test-main.hs
+++ b/test/test-main.hs
@@ -7,6 +7,8 @@
 import PropOpenClose
 import TinyLam
 import TestACompare
+import TestRefine
+import TestIgnore
 import TestShiftEmbed
 import TestTH
 
@@ -16,6 +18,8 @@
          test_calc
        , test_parallelReduction
        , test_openClose
+       , test_refine
+       , test_ignore
        , test_tinyLam
        , test_acompare
        , test_shiftEmbed
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
--- a/unbound-generics.cabal
+++ b/unbound-generics.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                unbound-generics
-version:             0.3.4
+version:             0.4.0
 synopsis:            Support for programming with names and binders using GHC Generics
 description:         Specify the binding structure of your data type with an
                      expressive set of type combinators, and unbound-generics
@@ -38,6 +38,7 @@
                        Unbound.Generics.LocallyNameless.LFresh
                        Unbound.Generics.LocallyNameless.Alpha
                        Unbound.Generics.LocallyNameless.Bind
+                       Unbound.Generics.LocallyNameless.Ignore
                        Unbound.Generics.LocallyNameless.Rebind
                        Unbound.Generics.LocallyNameless.Embed
                        Unbound.Generics.LocallyNameless.Shift
@@ -81,6 +82,8 @@
                        TestParallelReduction
                        PropOpenClose
                        TinyLam
+                       TestRefine
+                       TestIgnore
                        TestACompare
                        TestShiftEmbed
                        TestTH