Does anyone have a reference for combining unification-based type inference with bidirectional type-checking?
ie you should be able to take a bidirectional type system and formulate a constraint-based version it, and I've done that a few times in an ad-hoc way, but I'd like to see if there's a proper principled approach to it