Push/pull through position information.
Actually call the bidirectional type checker.
Stuck in push rule for applications.