Most static type checkers prove (to the limits of the soundness of the type system) that the types of the values at run time will always be compatible with the operations performed on those values. For these checkers, any program that's not provably sound (to the limits of the type system soundness) will be rejected. In other words, most static type checkers answer "is this definitely correct?"

However, it's possible to have a more lenient static type checker that only looks for cases where you're guaranteed to get an illegal operation at runtime. They answer the question "is this definitely wrong?"

For instance, if we have:

  def f(x):
      g(x)
      h(x)

  def g(x):
      x.a()

  def h(x):
      x.b()

If we're doing whole program analysis and there's no type that has both a() and b() methods, then f is guaranteed to call a non-existing method at one place or the other.

This sort of "this is clearly wrong" type checking is much less intrusive than the more common "I'm not positive this is correct" type checking.

If you're not doing whole-program analysis, then you may restrict the type search to the types imported into the transitive closure of the module and its dependencies. This makes type checking slightly more intrusive by sometimes forcing more module imports, but it's still much less intrusive than common type checkers.