最近在看https://www.microsoft.com/en-us/research/wp-content/uploads/1999/01/recpro.pdf 和 https://people.cs.uchicago.edu/~blume/papers/icfp06.pdf ，感觉已经会用了，但是对实现还是有点把握不准，特别是当我要把这个东西放进 bidirectional type-checking 的时候