Three Dollar Quill

I was mostly focusing on stuff besides Impliciula today, which was... probably good. However, I did just now take a look at the state of type errors with the rewrite, and I have found things that I was ignoring. Basically, I didn't think too hard about how to translate various operations from purely node-based, to base on nodes and bundled metadata. I'd sort of glossed over this with how part of inferring the type of an unpack operation involves synthesizing an existential type from various fields on the unpack node, because all of those fields were from the same node, so whatever. (That previous sentence may have sounded weird. I will not be explaining further.) But now I'm working on checking the type of a pack node, and suddenly I need to perform type substitution with values from two different bundles, and I'm unclear on what the desired semantics even is. Like, do I define some kind of merge operation on paths, or is there some sense in which one of them "wins"?

Thinking about how it'll be used, it's kind of as if the path needs to introduce a variable binding to the bundle that's substituted in? After all, it would be good to know where the value came from, except that currently the substitution is so thorough that it's not obvious, except, except. If the path description is good enough to follow through the nodes (this is a big assumption at present), then it will reach a variable, and if there is a binding to that variable, then there shouldn't be a problem, per se, with using that binding to continue.

So, we need the binding that reaches the variable, obviously, and we need the binding that reaches the value, do we need to track "why did we substitute that variable specifically"? My gut feeling is that it would be very unwise to make a snap decision here, so I am going to try to wind down now, and focus on other stuff for a bit. We'll see how that goes.

Good night.