Three Dollar Quill

I'm still spitballing ideas for reworking error generation. One thing that I'm kind of stuck on is that I'm fairly sure I'll want to do typing via constraint solving eventually, but do I want do try to get it working right now? And if I don't do constraint solving right now, can I find some way to minimize the disruption of switching to something now, and then from that thing later?

Alternatively, can the ideas I'm messing with currently grow to handle the stuff I think I'll need constraint solving for later? Well, let's consider the "later". I'm going to want to check function bodies "in isolation". In other words, a given function's type ascription checks inward, and it can infer outward from any other ascription, (which points me towards some mild problems with how I'm doing bidirectional typing, and which may be the problem the paper was trying to warn me about), and I'm going to want to verify that the predicates from the refinement types hold. Verifying this may involve the invocation of lemmas, and testing the subtype relation based on predicate implication.

My gut and my heart tell me that this can be made to work in a syntax-directed fashion, but unless I can (figure out how to) prove this, I at least need a backup plan of some kind. Okay, I see "Refinement types combine SMT decidable constraints with a compositional, syntax-directed type system", but do I gotta bring in SMT? Maybe I could conceptualize the current "error" plan as only emitting unsatisfiable constraints? Error reporting would then notionally involve, for each constraint, finding the smallest set of other constraints that are satisfiable without it, but unsatisfiable with it, for some definition of "smallest", and possibly "the".

With all of that in mind, I've got a fairly good idea of how I can proceed with this idea, but I want to take things slow, so I'll wrap this up for tonight and see if I feel ready to take it on tomorrow.

Good night.