subst captures variables when substitution is with a bound variable

[liesnikov]

as of 7ce8463 subst checks that variables substituted for are free but doesn't do anything to avoid capture

unbound-generics/src/Unbound/Generics/LocallyNameless/Subst.hs

Lines 103 to 124 in 7ce8463

	subst :: Name b -> b -> a -> a
	default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a
	subst n u x =
	if (isFreeName n)
	then case (isvar x :: Maybe (SubstName a b)) of
	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
	default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
	substs ss x
	| all (isFreeName . fst) ss =
	case (isvar x :: Maybe (SubstName a b)) of
	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)

this means that we take terms from pi-forall (https://github.com/sweirich/pi-forall/blob/729c9f4e348bd94090b0415e3391ad8bb1d89305/full/src/Syntax.hs) and run the following:

import Unbound.Generics.LocallyNameless.Name as Unbound

an :: TName
an = Unbound.string2Name "aname"

bn :: TName
bn= Unbound.string2Name "bname"

match = Match (Unbound.bind (PatCon trueName []) (Var bn))

bound :: TName
bound = Unbound.Bn 0 0 -- a bound variable

abound = Unbound.bind an (Case (Var an) [match])
{-|
>>> show abound 
<aname> Case (Var 0@0) [Match (<(PatCon "True" [])> Var bname)]

>>> show $ Unbound.subst bn (Var bound) $ abound
<aname> Case (Var 0@0) [Match (<(PatCon "True" [])> Var 0@0)]
-}

We see that Var 0@0 is captured by the case, the correct result would be

<aname> Case (Var 0@0) [Match (<(PatCon "True" [])> Var 1@0)]

[lambdageek]

I'm surprised if this is a recent change in behavior. I think this is in fact by design. The locally nameless representation only supports substituting terms that are well formed in the sense that all bound variables occur in a term together with an enclosing binder.

That is Bn 0 0 on its own is not a valid argument for subst.

[liesnikov]

Yeah, the example constructed is somewhat artificial for brevity -- I discovered this behaviour in the implementation of contextual metavariables.
There delayed substitution can appear under a binder and if one substitutes a solution for the meta later it technically becomes subst freeName boundName whateverterm.

concrete example being:

--term before metavar substitution
orb0 = \b10 b20. ?_29 [ b223  →  b20, b116  →  b10, orb0  →  orb0 ]

--metavar solution
--that exists in the context with variables  b223 and b116 available
?_29 = case b116 of
  True -> True
  False -> b223

Regardless, if this is intended behaviour, I can imagine a guard is appropriate that verifies that bound variables don't occur in the term that we substitute with. Something akin to if (isFreeName n).

[lambdageek]

Regardless, if this is intended behaviour, I can imagine a guard is appropriate that verifies that bound variables don't occur in the term that we substitute with. Something akin to if (isFreeName n).

I think that's hard to do because the typeclass Subst b a doesn't actually place any constraints on u :: b - the term that will be substituted for n - in subst n u x. All we know is that n :: Name b is a name that can occur somewhere inside x - we don't know anything about what kind of thing u might be. (Maybe there is something clever we can do, but the straightforward approach doesn't typecheck)