Implementation documentation for Unification

[ClarkeRemy]

I did some minor formatting to make eyeballing the control flow easier. this formatting change can be reverted, it's not the more important part of the changes.

I added some implementation documentation as I found the code hard to follow without context.

I think this adds real value, and will save me time in the future when revisiting this code, and hopefully other contributors.

I've annotated my comments with my name, primarily to avoid confusion about what code is commented out because its debug code that can be helpful, versus implementation documentation.

I've also reordered the blocks in the macro to mirror the use of the macro in the " 'popping " loop.

I've made some small changes where control flow in " 'popping " had branches that were unreachable, and left questions about why they were needed.

The terminating if/else has been replaced with a debug_assert, as the termination condition of popping was already guaranteeing that the stack was empty, but I thought the debug_asset kept the spirit of it as documentation.

[ClarkeRemy]

I added some implementation documentation to apply_e. The code itself is unchanged.

[MesTTo]

read through this properly since it documents the two functions i lean on most, and i checked it
rather than just reading it. builds clean, cargo test -p mork-expr is green (15 + 2), and mork test is byte-identical to 45bdb9a across all 625 lines, so nothing here moves behaviour. it also
merges cleanly with #137 and #138, which both touch the same two files, so no ordering constraint
between us.

the docs match what i have hit independently. in particular "the occurs check here is actually
incomplete" is right, and it lines up with the note already at lib.rs:754 and with something i ran
into on #124: unify checks occurs per equation, and the cycle that escapes it is the one built
across equations, which is why the rejection has to happen again after apply. worth having that
written down where the macro is instead of only at the call site.

the apply_e parameter table is the part i would have wanted most. original_intros versus
new_intros is not guessable from the names, and "you need to apply_e on the patterns first, in
order to compute the original_intros value in the result" is exactly the ordering constraint the
leapfrog dispatch in #124 has to respect when it re-derives bindings, so it is good to see it stated.

one real comment, on the unreachable! at lib.rs:1997.

it is correct today, and i verified that rather than assuming it. match2 calls hole in exactly
two arms, lib.rs:1024 and lib.rs:1030, both guarded on Tag::NewVar | Tag::VarRef(_) on one side or
the other, and var_opt (lib.rs:1786) returns Some for exactly those two tags and None for
SymbolSize/Arity. _ts1.ee.offset(i1) reads the same byte match2 matched on, so at least one
side is always Some and (None, None) cannot happen. the only live push call site is the
match2 callback at lib.rs:2085.

what i am uneasy about is that the invariant lives a thousand lines away in a different function, and
unreachable! panics in release too. adding a hole call to the SymbolSize or Arity arms is a
natural thing to want later, and the day someone does it the unifier panics in production with
nothing in the suite catching it, since the old code just pushed the pair and carried on. either a
debug_assert! falling through to the existing _ => {}, or a line at the two hole sites saying
unify's push relies on this being variable-only, would make it survive that.

two small things: the if PRINT_DEBUG { println!("pushing {} {}", ...) } line went with the rewrite
of that arm, which i assume was not deliberate since the rest of the PRINT_DEBUG tracing is intact
and that one is useful when a unification goes wrong. and "at leat" in the panic string.