Three Dollar Quill

I didn't get quite as far as I might have liked today. I copied over the binding elaborations unchanged, because I just don't think there's a good way to bidirectionalize them. Then I started on the expression elaborations, did a few, and then decided to skip ahead to rules for wrapped values so I don't forget them. In working on this, I found some potential issues that I think I addressed, but I'm frankly not really sure.

Basically, doing bidirectionalization means replacing a lot of X nodes in expressions with E nodes, because variables are synthesizing, and the syntactic sugar for using expressions instead of variables is also synthesizing, so if I want a term to check, it has to use expressions "natively". This sometimes results in different typing behavior from the syntactic sugar version, I think always involving existential types. For if nodes, I think there isn't a major difference, but I had to think a bit for function, application, and sealing nodes. Basically, bidirectionalized application needs more information in the function type, compared to the sugared version; this is because the argument type can carry more information. A similar story holds for sealing.

Now, unwrapping got weird for a similar but more involved reason. As before, the X is replaced with E, but then the type must be unwrapped, and used to generate a coercion function. Now, if we're working with an expression, then the type must handle being abstracted, which means that there could be a bunch of existential types outside the wrap type, and therefore the value could have a bunch of pack nodes, and by describing this, I've decided that my original implementation was probably wrong, but I've come up with something that I think has a colorable argument for being closer to right.

The current solution is, get all of the existential type variables, bind them, determine the coercion function between the wrapped type and the checked type, then generate an expression that unpacks every existential type variable from the wrapped expression, and only then applies the coercion function.

If this actually works, and I can keep on applying it, I should be able to get somewhere. Now, next thing to consider: hey, how should I implement union types and case expressions?

For now, I'm going to get to bed, since it's super late.

Good night.