Your comment expanded out is what I had hoped that blogpost would have been. Thank you for posting this. It's hard to overstate how much easier bidirectional ty

Your comment expanded out is what I had hoped that blogpost would have been. Thank you for posting this. It's hard to overstate how much easier bidirectional typechecking is compared to other approaches. My favorite starting point is actually Dunfield's lecture notes on bidirectional type checking, https://people.mpi-sws.org/~joshua/bitype.pdf https://people.mpi-sws.org/~joshua/bitype.pdf The paper you mentioned is great at showing the approach scales well to giving you all the fancy features you might want that are in modern languages.