Implement bidirectional type-checking