  Benefits of static type systems are well-known: they offer guarantees that no
type error will occur during runtime and, inherently, inferred types serve as
documentation on how functions are called. On the other hand, many type systems
have to limit expressiveness of the language because, in general, it is
undecidable whether a given program is correct regarding types. Another concern
that was not addressed so far is that, for logic programming languages such as
Prolog, it is impossible to distinguish between intended and unintended failure
and, worse, intended and unintended success without additional annotations.
  In this paper, we elaborate on and discuss the aforementioned issues. As an
alternative, we present a static type analysis which is based on plspec.
Instead of ensuring full type-safety, we aim to statically identify type errors
on a best-effort basis without limiting the expressiveness of Prolog programs.
Finally, we evaluate our approach on real-world code featured in the SWI
community packages and a large project implementing a model checker.
