Implemented bidirectional type checking
Tested examples from Fairouz's paper