That's why you go with bidirectional type checking instead. This scales much better to more interesting language constructs like rank-n polymorphism, and dependent types, gives better localised error messages, and the downside of having to have some top level annotations is worth it, because that's best practice anyway.