bugfix: don't prefer the unison file for name suffixes

[mitchellwrosen]

Overview

This PR changes the parse-time name resolution logic. Previously, a locally-bound name ("file name") X.Y.Z would shadow names X.Y.Z, Y.Z, and Z in the namespace ("namespace names").

That feature was implemented in the following PRs:

• Allow suffix-based name resolution to refer to definitions in the current file #1732
• Fixes to suffix-based name resolution when local file names shadow codebase names #4325

The situation prior to the two PRs above was not good: suffixes such as Y.Z or Z (continuing the example above) would not refer to any file name, and would resolve to (if anything) a namespace name.

But the situation after the two PRs above (trunk today) is not good either: it means there is no syntax whatsoever to refer to namespace names Y.Z or Z, if X.Y.Z is a file name. That means we cannot properly render some names, which means update, upgrade, merge, and even edit all have buggy corner cases: #5268

The fix implemented here is to make file names and namespace names exist at the same precedence level (except that file names still shadow namespace names, it's just suffixes of file names that no longer shadow).

Along the way, I discovered a bunch of weird stuff and did my best to either preserve existing behavior or clean up / fix bugs – whichever was easier.

For example, one thing I stumbled upon that I'm particularly happy about: the error message you get when you've typed in an ambiguous pattern actually makes sense now. I'm not sure if there is a ticket about this, but if you had:

type Foo = Bar
type Baz = Bar

in your namespace and tried to write a function

useFoo : Foo -> Nat
useFoo = cases Bar -> 5

you'd get the baffling error message

  I don't know about any data constructor named Bar. Maybe make sure it's
  correctly spelled and that you've imported it:

      3 |   Bar -> 5

Now, you'll get one that looks like the other "ambiguous name" errors:

    ❓

    I couldn't resolve any of these symbols:

        3 |   Bar -> 5


    Symbol   Suggestions

    Bar      Foo.Bar
             Baz.Bar

I also discovered a couple bugs in the recently-implemented namespace directive feature (#5285) that I fixed. The term parser previously did not account for any namespace directive, which it needs to, in order to properly resolve constructor references and type links.

Another bug: Names.shadowing was calling Names.unionLeft, but that's not correct, and neither was Names.unionLeftName, turns out. I removed both of those broken union functions in favor of the one we want and now use: Names.shadowing, which combines two names with a left bias: if a name is related to a set of references r1 from the left argument and r2 from the right argument, then use r1 and drop r2.

Test coverage

I've included a transcript that demonstrates the new behavior. I also deleted a couple old irrelevant transcripts that demonstrated the old behavior.

[aryairani]

Hey this looks good. If we're changing the name resolution rules though, I would want to update them for both terms and types equally in any release of ucm. Are they split up just to avoid merge conflicts, or is there a reason to wait hold off on the terms piece?

[mitchellwrosen]

@aryairani agreed – this part is ready for review but shouldn't be merged before the term half is done and reviewed, too

[aryairani]

Ok sounds good!

[pchiusano]

I'm good with this, but also think that terms should work the same way as types here. So once that's ready, I'm good with merging.

[aryairani]

Converting this to draft until it's ready for further review.

[ChrisPenner]

I'm not sure I understand what the change here is; how does it handle things like this?

data my.cool.Tree a =
  Node
  | Branch (Tree a) (Tree a) 

E.g. does it resolve Tree to the my.cool.Tree in the file, or would it use one that was previously added to the codebase?

I think we really don't want the latter for a bunch of UX reasons

Also, I know Paul and Fabio really want things to pretty print without full qualification whenever possible, e.g. the following is undesirable:

data my.cool.Tree a =
  Node
  | Branch (my.cool.Tree a) (my.cool.Tree a) 

[mitchellwrosen]

@ChrisPenner in this example

data my.cool.Tree a =
  Node
  | Branch (Tree a) (Tree a) 

Tree would resolve to my.cool.Tree if Tree is a unique suffix among all type names in the namespace + file (where file names shadow namespace names, but suffixes of file names don't shadow anything)

[ChrisPenner]

Forgive me, but even with the explanation I'm still a bit confused;

but suffixes of file names don't shadow anything

This is the part that keeps confusing me, you say that my.cool.Tree from the file would shadow the version from the codebase, but then say "suffixes of file names don't shadow anything", isn't Tree in the decl body a "suffix of a file name", and thus would NOT shadow the my.cool.Tree from the codebase, a.k.a. it would USE the codebase my.cool.Tree instead of the file one?

[aryairani]

Is it that the suffix Tree [of a definition in the file] doesn't shadow a definition Tree in the codebase, but that suffixes of definitions in the file do supersede suffixes of definitions in the codebase, but we aren't calling that "shadowing"?

[mitchellwrosen]

This is the part that keeps confusing me, you say that my.cool.Tree from the file would shadow the version from the codebase, but then say "suffixes of file names don't shadow anything", isn't Tree in the decl body a "suffix of a file name", and thus would NOT shadow the my.cool.Tree from the codebase, a.k.a. it would USE the codebase my.cool.Tree instead of the file one?

Tree is a "suffix of a file name" here (namely, the file name my.cool.Tree), but it would not resolve to the my.cool.Tree in the namespace, because that definition is shadowed by the existence of my.cool.Tree bound in the file.

Is it that the suffix Tree [of a definition in the file] doesn't shadow a definition Tree in the codebase,

Correct.

but that suffixes of definitions in the file do supersede suffixes of definitions in the codebase, but we aren't calling that "shadowing"?

No, when resolving a name to a definition, there's no preferential treatment to anything in the file over the namespace.

Does all that make sense @aryairani / @ChrisPenner?

[aryairani]

I'm not clear just from this example about what it means to not have preferential treatment, but I'll read through the transcripts and report back.

[mitchellwrosen]

It means the same thing as "supersede" from your question. A suffix (non-exact match) that could refer to something in the file or the namespace will not resolve to the thing in the file, it will instead be ambiguous. That's the trunk behavior that this PR changes.

[aryairani]

Looks good. Do we need some kind of test to make sure that this change doesn't introduce round-trip errors, or do the existing transcripts cover that?

[aryairani]

This was ambiguous because it could have been [ns.]longer.foo.Foo.Bar or [file.]Foo.Bar, TDNR doesn't help, and so you have to expand it until it's unambiguous or an exact match?

[mitchellwrosen]

Correct. TDNR doesn't apply here – it's not used for patterns.

Spelling out Foo.Bar would even be necessary if there was an explicit type signature on refersToBar.

In principle a type checker could of course help in that case; only a unique suffix among all the constructors of the known type should be required. But we don't make it to the type checker because we eagerly resolve all constructor references in patterns during parsing.

[mitchellwrosen]

@aryairani I'm not sure any existing test covers this change well. A few broke incidentally because they were using suffixes that are now considered ambiguous. The pretty-printer didn't match this feature of the parser: it would sometimes print more segments than necessary because file suffixes shadowed namespace names (which was the bug this fixes). So, now the parser and pretty-printer are in sync wrt. suffixification. I believe the new transcript that demonstrates the new behavior is the main bug-catching test, do you see something that it's missing?

[aryairani]

@aryairani I'm not sure any existing test covers this change well. A few broke incidentally because they were using suffixes that are now considered ambiguous.

👍

I believe the new transcript that demonstrates the new behavior is the main bug-catching test, do you see something that it's missing?

I thought the transcript was excellent; I didn't notice anything missing.

The pretty-printer didn't match this feature of the parser: it would sometimes print more segments than necessary because file suffixes shadowed namespace names (which was the bug this fixes). So, now the parser and pretty-printer are in sync wrt. suffixification.

I guess what might be missing, though it doesn't necessarily belong in this PR, is an equivalent sort of behavior demo for the printer; or even putting the printer and parser together in interesting cases like you've laid out here, as a round-trip test.

I want to keep the known round-trip error list up to date if possible; and any time there's a change to either the parser or the printer there could possibly be an impact to round-trips.

Once we have a passing round-trip test I guess it'll be easier to detect when the property breaks.