In this problem session, we will discuss a non-trivial way of type information flow in bidirectional type checking.