This PR adds support for pretty printing using generalized field
notation (dot notation) for private definitions on public types. It also
modifies dot notation elaboration to resolve names after removing the
private prefix, which enables using dot notation for private definitions
on private imported types.
It won't pretty print with dot notation for definitions on inaccessible
private types from other modules.
Closes#7297
This PR fixes (1) an issue where private names are not unresolved when
they are pretty printed, (2) an issue where in `pp.universes` mode names
were allowed to shadow local names, (3) an issue where in `match`
patterns constants shadowing locals wouldn't use `_root_`, and (4) an
issue where tactics might have an incorrect "try this" when
`pp.fullNames` is set. Adds more delaboration tests for name
unresolution.
It also cleans up the `delabConst` delaborator so that it uses
`unresolveNameGlobalAvoidingLocals`, rather than doing any local context
analysis itself. The `inPattern` logic has been removed; it was a
heuristic added back in #575, but it now leads to incorrect results (and
in `match` patterns, local names shadow constants in name resolution).
@Kha I tried to fix a few issues with private names. The new test
tries to cover them. If you have more, please create an issue.
1- Scoping. A private declaration should shadow one in a previous scope.
2- We should not be able to define the same `private` in the same
module more than once.
```
private def x := 10
private def x := "hello" -- should produce error here
```
3- Dot-notation should work with private declarations in the module
where they were defined.
4- The following should work
```
namespace N
private def x := 10
end N
#check N.x
```
5- The following should **not** work
```
def y := 10
private def y := "hello" -- produce error
private def z := 10
def z := "hello" -- produce error
```
BTW, I am happy to change this behavior. I just mimicked C's
behavior for `static`.
It is not clear whether the following should work or not.
```
namespace N
private def b := 10
end N
open N
#check b
```
