refactor: Split renameVar in to two passes

[georgefst]

Inspired by a comment from @brprice on Keybase dev chat earlier today:

see Primer.Core.Transform.renameVar for conservative “bail out if maybe capture” (though #356 says it is incomplete!): if we would need to go under a binder which binds the new name, we bail out (This could be expressed differently, by doing a first pass to collect binders and checking they do not have the same name, then a separate pass renaming without caring)

As implemented here, we don't "collect binders" in the first pass. I'm not quite sure what that would look like. Instead the first pass just performs the "checking they do not have the same name" part, and the second pass re-traverses the tree, performing the renaming.

The main intention is to reuse transformVar to fix #367 (comment). Which is why that PR's branch is the target of this one.

This needs a little cleaning up (including a better commit message, and possibly some tests), but I wanted to check that we're happy with the approach first.

[georgefst]

We're no longer checking unLocalName v == xn etc. as it's unclear where this should go. But it looks like we'll soon stop requiring this anyway, due to: #375 (comment) (great timing!).

[georgefst]

This seems like it will be useful again in future e.g. if we want to enumerate the shadowing sites for use in a GUI - see #332. But for now it only has one use site. There is already some similar-looking code in Primer.ZipperCxt, but as far as I can tell that's only concerned with walking up the tree, whereas here we only walk down. Maybe there's some way we can reuse that though? I'm not that comfortable with zippers.

[georgefst]

What should we return? I was thinking IDs, but that requires adding a HasID a constraint to renameVar and renameLocalVar. It doesn't bubble up any further than that, since the constraint is satisfied at every call site, but it feels wrong. renameVar doesn't even care what's in the list. I guess we could just return the whole expression?

[brprice]

I think here that we should be able to use Zipper.bindersBelow to see if the new name is bound.

[brprice]

This would not check if the new name occurs free, but we can do that with one of the _freeVars optics (we should probably check both type and term vars). We need to avoid renaming x to y in C x y, as that changes the meaning.

[brprice]

(I'm a bit worried here, as the testsuite passed. Either I've gotten confused, or we should add some extra testing here...)

[brprice]

Can we reuse Core.Utils._freeTmVars here?

[georgefst]

Maybe.

The following doesn't work:

transformVar f x = traverseOf _freeTmVars $ \(m, LocalVarRef -> v) ->
  if v == x then f m v else pure $ Var m v

_freeTmVars doesn't find globals (should it?), so two tests fail (Tests.Action.Prog.rename def referenced and Tests.Action.Prog.rename def recursive).

[brprice]

Hmm. Maybe we should add another traversal focussing on global vars and choose which to use when renaming based on the sort of var?

I expect said traversal should be easy to write using some generics, assuming we don't allow locals and globals to shadow. Alternatively it would be easy to change _freeTmVars to also return globals (and add a wrapper to only look at locals if we require).

[brprice]

This does not seem correct: do you mean v == y?

[georgefst]

Ah, copy-paste error. This branch shouldn't exist. We're just using the variable: there's no shadowing.

PS. there's no y in scope.

[brprice]

By y I mean "the new name" (but you're right, I didn't notice that it was not in scope here), and we need to do some check about it somewhere, see #378 (comment)

[georgefst]

The new name is the one we're checking here - note that renameVar calls this function with its y.

[brprice]

Ah, thanks. This makes sense now.

[brprice]

This is the rough approach I had in mind, but I think we can reuse existing code, rather than writing new traversals.

It may be worth a comment about inefficiency traversing the tree twice, and in the future we could explore a "traversal-with-binding-info", which abstracts out the pattern "focus on bits of the tree and modify them, but keep track of what binders the focus is under". Perhaps something of the form freeVarsWithContext :: Traversal Expr Expr ({goneUnderBinders :: [Name], freeVariableOccurrunce :: Name}) Expr (although I have not thought about whether this is a law-abinding traversal, or of the best way to express the idea. Perhaps something zipper based?).

[georgefst]

This is probably not what we want - it's just the simplest way to get tests to pass.

[georgefst]

This is clearly more subtle then I originally hoped, and it turns out _freeVars (which I learnt about from #378 (comment)) is enough to solve the original issue in #367. So I'm abandoning this PR for now.

FWIW, I think this is genuinely a safe refactor (modulo checking between different scopes - #378 (comment)), but not quite for the reasons I thought. Essentially checkShadowing is a bad name, given that it also bails out over free occurrences. In other words, the original renameVar is more conservative than I realised when it comes to name clashes.

[dhess]

What's the status of this PR? I don't like to leave PRs open for very long and this one has been around going on 4 months. Sounds like it's no longer needed and/or not particularly useful so should we close it?

[georgefst]

As stated in the previous comment, it turned out to be quite complex, and the original issue was solved by other means.

And I expect it may now be some effort to rebase on main.