bugfix: merge involving constructor deletion

[mitchellwrosen]

Overview

This PR attempts to fix a bug in merge reported at #5092.

The syntactic hashing of constructor referents was wrong, at least in the context of how the rest of the algorithm used the diff computed by syntactic hashes.

Prior to this PR, we computed the syntactic hash of a constructor as equivalent to the term that represents calling that constructor.

For example, if the namespace contains the name

Just = #Maybe#1

then the syntactic hash of that referent was computed as the syntactic hash of the term whose body is just #Maybe#1.

Thus, when updating

type Foo = Bar | Baz

to

type Foo = Bar

the diff would show an update on the type Foo but not the constructor Bar.

There may be a design in which that works out ok, but not in ours: we take the adds, updates, and deletes from the diff and lay them over the LCA. In this example, we'd end up with an updated Foo without a name for its new constructor Bar.

So, the fix I implemented is to change how we compute syntactic hashes of constructors. Now, it's simply equivalent to the syntactic hash of its type declaration (which itself would change if any constructors change in shape or name). Therefore, the constructors of a type that undergoes an update would appear in the diff as updates as well.

Additionally, I noticed while reading the syntactic hashing code that we computed the hash tokens of a constructor reference differently than a normal term reference. That seemed like a mistake, unrelated to this bug, which could cause unnecessary conflicts. So, I fixed that too.

Test coverage

I've added a regression test to the main merge.md transcript. You can see its results flip from incorrect to correct right here: prior to this PR, merge erroneously dropped the name for a constructor, and now it doesn't.

Loose ends

Link to related issues that address things you didn't get to. Stuff you encountered on the way and decided not to include in this PR.