subst captures variables when substitution is with a bound variable

[liesnikov]

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

https://github.com/lambdageek/unbound-generics/blob/7ce846322eb03870cf6b76f0fc206cdec337f0db/src/Unbound/Generics/LocallyNameless/Subst.hs#L103-L124

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)