Three Dollar Quill

All right, let's see where I am:

• Removed explicit type variable construction, replaced it all with callbacks.
• The type annotations are out of control again; I need to figure out how to shorten them.
• Still haven't had the focus to rework variables and labels to work with 1ML.
• Missing several node types required to implement algebraic effects.
• 1ML appears to require boolean types and associated nodes.
• Refinement typing needs integer types, at least to get started with.
• My fingers are still crossed that modular implicits will basically just fall out of combining 1ML and algebraic effects.

My plan is to alternate between refining the current implementation, and planning out what extensions I need to add these other capabilities. I'm intending to implement each one separately, ideally as a higher-level language that produces well-typed trees of the current implementation. I'm going to do them separately because jumping the gun in combining them won't make things any easier, theoretically or practically, and I want as few confounding factors as possible when things inevitably go off the rails.

I'm a little sleepy right now, so I'm going to wrap things up, take care of some chores, and then try to refresh my memory on all of these different theoretical frameworks.

Good night.