[tzs]

> On the other hand, type checking is not optional, so having to solve a NP-complete problem for that would indeed be problematic.

Not necessarily. There are plenty of NP-complete problems that can be solved optimally fast enough to be useful for the instances that actually come up in real world applications.

For example the Traveling Salesman Problem (TSP) is NP-complete, but there are exact solvers that run in reasonable time for instances of a few hundred vertices. That's fine if you are say a delivery company trying to plan the day's itinerary for one of your delivery trucks.