fix: make name unresolution consistent and avoid auxiliary names

[jrr6]

This PR ensures that names suggested by simp? are not shadowed by auxiliary declarations in the local context.

This PR moves unresolveNameGlobalAvoidingLocals into the Term namespace and restricts it to TermElabM, since it is impossible to correctly resolve some auxiliary declarations (e.g., in a mutual block) without access to the auxDeclToFullName map in the TermElabM context. It also adds auxDeclToFullName to the SavedContext for postponed expressions, which ensures that (un)resolution of auxiliary-declaration names is consistent between terms and tactic blocks (previously, it was not possible to refer to certain auxiliary declarations by suffixes in a tactic block).

Closes #6706.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6938 build failed against this PR. (2025-02-04 03:51:53) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f1133fe69caddf47b5d3766888da929513917af --onto befee896b38349a51dad1627360adbab317f3192. (2025-02-11 19:25:20)

[jrr6]

This would be a breaking change if integrated as-is (it changes both the type and namespace of unresolveNameGlobalAvoidingLocals; it also modifies the signature of unresolveNameGlobal, though using a default parameter such that most existing uses of the function should continue to compile).

As far as I can tell, the change in the type of the local-avoiding variant is unavoidable if we want to truly guarantee that it avoids all locals: as I note in the PR description, there are situations where it is impossible to determine the full set of locally shadowed names outside TermElabM. Because the situations in which these cases arise are somewhat uncommon, we could additionally continue to expose a variant that behaves like the current one, i.e., that can only guarantee that the name it produces doesn't conflict with non-auxiliary locals. Even so, the larger issue is that the change to the type of unresolveNameGlobalAvoidingLocals propagates to its callers like mkSimpOnly—which would ideally use the fully correct TermElabM variant—that are currently in MetaM. This, for instance, would break Aesop, which relies on mkSimpOnly acting in MetaM.

It's not immediately clear to me what the best path forward is. Given that the unresolution errors caused by the current implementation of unresolveNameGlobalAvoidingLocals require semi-pathological name conflicts (see #6706), I could see the case for abandoning this PR entirely and living with the behavior as-is. Alternatively, we could keep unresolveNameGlobalAvoidingLocals in MetaM but add a naïve namespace-relative name-component comparison on auxiliary declarations to catch errors like #6706, though this would introduce both false negatives and false positives for where or let rec bindings.

[nomeata]

Fixing this while staying in MetaM means it works properly, unless we have where or let rec names conflicting, right? The problem is all with auxDeclToFullName, correct?

So I wonder about these alternatives way to address this:

1. move auxDeclToFullName to the MetaM context. Would that suffices?

2. (more bold, probably there are good reasons why this does not work)

   Do we even need aux decls in the first place? Can we not add the recursive definitions to the elaborator’s environment temporarily as axioms, so that they are referred to as constants they should be, and late replace them by their real implementation (of course, the kernel environment should only see the post-derecursified definitions).

   Maybe this makes it harder to implement the behavior where a recursive call does not have to repeat the variable-declared parameters. So maybe this direction is far too big of a hammer.

[jrr6]

Fixing this while staying in MetaM means it works properly, unless we have where or let rec names conflicting, right? The problem is all with auxDeclToFullName, correct?

Yes, if we simply assume that an auxiliary decl named d has the fully-qualified name N.d where N is the current namespace, we'll be correct for recursive references, but a where or let rec named e, which has fully-qualified name N.d.e, will instead be erroneously treated as N.e. (So we'd still be able to detect name conflicts with e, but none that span between the preceding components and e.)

I've tried your suggestion (1), and it does resolve the issue of avoiding conflicts with auxiliary declarations. I worried a little bit that auxDeclToFullName might be more at home in the TermElab context, although perhaps this example is decent evidence that it actually doesn't (more concretely, I suppose the argument here is that "name (un)resolution is a Meta task, so structures used to resolve names should live in MetaM"). I agree that option (2), while aesthetically tempting, might be "too big of a hammer," especially since option (1) seemingly works.

Unfortunately, option (1), on its own, does not address the other issue of correctly resolving fully-qualified names of auxiliary declarations when resuming postponed elaboration; we may (and presumably do) call synthesizeSyntheticMVars at some point at which the relevant declarations are no longer in the auxDeclToFullName map. I'm not entirely sure how much overhead this map adds to the saved context, but if we want one-to-one parity in name resolution between postponed and non-postponed elaboration, I think this change is still required.

If option (1) is a preferable route, I can either open a separate PR with those changes or revert this PR's changes and push them here (if it's easier to keep things in one place).

[nomeata]

I am somewhat out of my depth here, with postponed elaboratation etc. Maybe @Kha can advise?

Would it help if the aux declarations would be added to the context with the fully qualified name, so the map isn't even needed, and with name resolution adjusted to heed the currently opened namespaces also when looking up local variables? Or would that break other things?

(Separate PRs of competing options might be useful to compare and for later reference.)

[Kha]

Do we even need aux decls in the first place? Can we not add the recursive definitions to the elaborator’s environment temporarily as axioms, so that they are referred to as constants they should be, and late replace them by their real implementation (of course, the kernel environment should only see the post-derecursified definitions).

I agree, and with addConstAsync we may now be in a position where reverting the axiom addition is actually feasible as async constants are specifically not sent to the kernel immediately. But also agreed that would be a rather large change with interesting questions such as whether we can put free variables in temporary constants to address your variable caveat... probably not the time for this.

[Kha]

we may (and presumably do) call synthesizeSyntheticMVars at some point at which the relevant declarations are no longer in the auxDeclToFullName map.

This would be addressed if every withAuxDecl call included Term.synthesizeSyntheticMVarsNoPostponing, which seems to be the case for top-level functions but not the other caller, let recs. But also... how often do we mix let recs and proofs? Did you encounter this issue in practice?

[jrr6]

But also... how often do we mix let recs and proofs? Did you encounter this issue in practice?

This particular issue did not arise in practice—I noticed it while trying to resolve the originally reported issue (where we were resolving local names properly but not detecting them during unresolution). I suppose the issue here could arise if a proof were split into lemmas using where declarations or if an intermediate have turned out to require induction (necessitating a let rec) and the user then shadowed the unqualified name, though these admittedly are something of a corner case. (The fact that we hide auxiliary declarations in the Infoview probably discourages these approaches in the first place.) My concern was more generally that we have inconsistent name resolution behavior in different contexts, which might be a source of confusion (since it doesn't appear a priori that this behavior should differ between tactic and term modes).

[nomeata]

Let’s not worry too much about name resolution or even unresolution in corner cases for which we have no evidence that they occur in practice. So if the code stays significantly simpler by not worrying, that’s probably the better trade off for now. Leaving a comment in the code and/or a low-priority issue to keep track might pay off.