Implementing a bi-directional type checker for the simply-typed lambda calculus