subst captures variables when substitution is with a bound variable about unbound-generics

[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)