[Meta] Naming issues

[franziskuskiefer]

There are a bunch of naming issues right now. This issue is tracking all of them.

Note: this issue is about concrete identifiers, that is global names. Local names are out of scope.

[W95Psp]

Here is a design document for this naming issues:
https://docs.google.com/document/d/1D_Cqa3JU_1ktm4LMZaLY6gowq2-2xdthhoQ3lPJT9_Q/edit?tab=t.as6omwfs8eh2

I think I need 1-2 days to implement it, but this would fix most of those issues.

---

Actions plan

• Frontend: add a DefKind on DefIdContents #1162
• Engine: global names: change the representation from krate * path to path * path * item #1163

[franziskuskiefer]

This was supposed to be cleaned up and closed. What's the state here @W95Psp @maximebuyse ?

[W95Psp]

• Traits cannot be imported by their original module when they are part of a bundle #1285 is a F* bug
• extern crate with the name of the current crate name clashes in f* translation #911 is a wontfix (allowing two crates with the same name means we need to disambiguate everything -- the invasive / frequency of the issue ratio is pretty bad here)
• Include path renaming in name policy #488 is a proverif issue
• Engine: name clash for items within trait methods #1161 is the only that remains and that we should address

[W95Psp]

I'm going to remove the parent to this issue for the first three issues.

[W95Psp]

Putting this issue as High, I will add it to my planning for next week so that we can close this issue.