pretty-printer doesn't consider local terms for unique suffix

[ceedubs]

The raw transcript is here.

pretty-printer doesn't consider local terms for unique suffix

It seems that the pretty-printer doesn't consider function-local terms when determining the minimal suffix to reference a term that is declared outside of the function.

Below we add Foo.bar and the local bar. The watch statement shows that the result is 3, as would be expected.

Foo.bar : Nat
Foo.bar = 1

baz : Nat
baz =
  bar = 2
  Foo.bar + bar

> baz

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:

    ⍟ These new definitions are ok to `add`:

      Foo.bar : Nat
      baz     : Nat

  Now evaluating any watch expressions (lines starting with
  `>`)... Ctrl+C cancels.

    9 | > baz
          ⧩
          3

However, if you use view (or edit), the pretty-printer shows bar + bar, dropping the Foo prefix from the first operand.

.> add

  ⍟ I've added these definitions:

    Foo.bar : Nat
    baz     : Nat

.> view baz

  baz : Nat
  baz =
    use Nat +
    bar = 2
    bar + bar

[atacratic]

Good bug. I think this ought to be caught by the uniqueness filter in calcImports, but it's not being, because local bindings aren't being included in the PrintAnnotation.usages tree of stats about names. I think the fix would be to add a LamsNamedOrDelay' branch to suffixCounterTerm (like the one in prettyBinding0 which actually does the pretty-printing of local bindings). And add tests in the FQN elision zone of the test suite. Note also the long explanatory comment here.

Am unlikely to get to this myself ☹️

[aryairani]

@ChrisPenner Is there an easy fix in the pretty-printer or in PPE construction for this?

[ChrisPenner]

@aryairani There's no simple one-line change AFAICT, we'd need to keep track of all the in-scope locals while pretty-printing in order to do it, then would probably be easiest to just add an argument to the pretty printer of local vars.

Definitely fix-able, but not a super quick win.

Let's look at this in the next triage meeting maybe, if it's high enough priority I could take a look at it 😄

[ceedubs]

I think that this was fixed by #4213