The "decl coherency check": a type declaration in a namespace is "coherent" if it satisfies both of the following criteria.

1. For each naming of the type decl (say Foo#foohash), there exists exactly one name for each of its constructors arbitrarily deep in the corresponding namespace (Foo in this example).

This allows us to render the decl naturally, as in

structural type Foo = Bar Nat Int | internal.hello.Bonk Nat

which corresponds to the three names

Foo => #foohash Foo.Bar => 0 "Foo.internal.hello.Bonk" => 1

We could not do if there was at least one constructor whose full name does not contain the full name of the type decl itself as a prefix.

A notable consequence of this requirement is that a second naming of a decl (i.e. an alias) cannot be embedded within the first naming, as in:

type Foo = ... type Foo.some.inner.namespace = ... -- an alias of Foo

2. No constructor has a "stray" name that does not have a prefix that equals the type declaration's name. For example, in the namespace

   Foo => #foohash Foo.Bar => 0 Deep.What.SomeAlias => 0

the constructor What.SomeAlias is "stray", as the type decl #foohash has no name that matches any prefix (i.e. Deep.What nor Deep).

On to the implementation. We are going to traverse the namespace depth-first. As we go, we have a stateful mapping between decl reference that we *have* seen a name for in one of our parent namespace, and its corresponding set of constructors that we *haven't* yet seen names for, but expect to, before fully searching the corresponding sub-namespace (e.g. the child namespace named Foo of the namepace that declares a decl Foo).

When processing a namespace, we first process all terms. Each constructor will fall into one of three cases:

+----------------------------------------------------------------------------------------------------------------+
| Case         | Mapping before       | Encountered constructor | Mapping after                                  |
+----------------------------------------------------------------------------------------------------------------+
| Happy path   | { #foo : {0, 1, 2} } | #foo#1                  | { #foo : {0, 2} }                              |
| Already seen | { #foo : {0, 1, 2} } | #foo#5                  | Error: duplicate naming for constructor #foo#5 |
| Never seen   | { #foo : {0, 1, 2} } | #bar#2                  | Error: stray constructor #bar#2                |
+----------------------------------------------------------------------------------------------------------------+

In "happy path", we see a naming of a constructor that we're expecting, and check it off. In "already seen", we see a second naming of a constructor that we're no longer expecting, and fail. In "never seen", we see a naming of a constructor before any naming of its decl, so we fail.

Next, we process all type decls. Each will again fall into one of three cases:

+-----------------------------------------------------------------------------------------------------+
| Case             | Mapping before       | Declaration | Num constructors | New mapping              |
+-----------------------------------------------------------------------------------------------------+
| Uninhabited decl |                      | #foo        | 0                |                          |
| Inhabited decl   |                      | #foo        | 1 or more        | { #foo : {0, ..., n-1} } |
| Already seen     | { foo : {0, 1, 2}  } | #foo        | Irrelevant       | Error: nested decl alias |
+-----------------------------------------------------------------------------------------------------+

In "uninhabited decl", we find a decl with no constructors, so we don't expect anything new. In "already seen", we find a second naming of a decl, whose constructors will necessarily violate coherency condition (1) above.

In "inhabited decl", we find a decl with N constructors, and handle it by: 1. Adding to our state that we expect a name for each. 2. Recursing into the child namespace whose name matches the decl. 3. (If we return from the recursion without short-circuiting) remove the mapping added in step (1) and assert that its value is the empty set (meaning we encountered a name for every constructor).

Note: This check could be moved into SQLite (with sufficient schema support) some day, but for now, we just do this in memory.

Note: once upon a time, decls could be "incoherent". Then, we decided we want decls to be "coherent". Thus, this machinery was invented.