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

0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/zanzi/statuses/115493412927449622 on your instance and quote it. (Note that quoting is not supported in Mastodon.)