Odd behavior when using `scoped syntax` and `withNamespace`

Stream: metaprogramming / tactics

[Tate Rowney]

Good morning! I've been having trouble understanding some behavior of scoped syntax declarations. For example, something like this is totally fine:

namespace outer

scoped syntax "myterm" : term

end outer

#eval `(term|myterm) -- parses as an identifier

...but calling the withNamespace function at any point beforehand changes things:

#eval do
  withNamespace `outer do
    logInfo "shouldn't affect anything"

namespace outer

scoped syntax "myterm" : term

end outer

#eval `(term|myterm) -- now parses as a keyword (`outer.termMyterm) despite being out of scope

...and running it at any point within the namespace with any argument also changes things:

namespace outer

#eval do
  withNamespace `anything do
    logInfo "shouldn't affect anything"

scoped syntax "myterm" : term

end outer

#eval `(term|myterm) -- parses as a keyword again

Even more strangely, everything is fine if these namespaces are opened/closed manually using namespace ... /end ..., or if addNamespace is open privated and used; and #where reveals no namespace leakage or other weirdness. I've tested this all on v4.28.0.

I can't make heads or tails of this... is this intended behavior? Is there a better way to programatically declare scoped syntax (as I was hoping to do using withNamespace)? Thank you very much!

[Albert Smith]

I think this is a bug in the definition of withNamespace. If you look at the definition of end you'll see that it ends with a popScopes, which is missing in withNamespace even though it calls an analogous pushScope (indirectly), which I guess desyncs scoped persistent env extensions including the one used for parser extensions. The fix should just be to add popScopes ns.getNumParts to withNamespace just before the return

[Tate Rowney]

Thank you, this indeed appears to be the problem. Adding the proper calls to popScope fixes it. I've opened an issue on GitHub.