Substitution should continue traversing even when the variables do not match

[TOTBWF]

Right now, when you try to apply a substitution, and the variables do not match, the traversal of the AST halts, even in cases when the substitution should continue.

For example:

type Var = Name Term
type MetaVar = Name Extract

data Term
data Term
    = Var Var
    | Hole MetaSubst MetaVar
    | Lam (Bind Var Term) 
    | App Term Term
    deriving (Show, Generic, Typeable)

newtype Extract = Extract { unExtract :: Term }
    deriving (Show, Generic, Typeable)

newtype MetaSubst = MetaSubst { metaSubst :: [(Var, Term)] }
    deriving (Show, Generic, Typeable)

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 x)
    isCoerceVar _ = Nothing

applyMetaSubst :: MetaSubst -> Extract -> Term
applyMetaSubst  e = substs ms $ unExtract e

instance Subst Term MetaSubst
instance Subst Extract MetaSubst

When performing the following substitution:

let mv = s2n "_"
     mv1 = s2n "_1"
     h = Hole (MetaSubst [(s2n "a", Hole (MetaSubst []) mv)]) mv1
in subst mv (Extract $ Var $ s2n "x") h

The result is Hole (MetaSubst [(a, Hole (MetaSubst []) _)]) _1 instead of the expected Hole (MetaSubst [(a, Var x)]) _1.

[lambdageek]

Fixed by #27