Most statically typed functional programming languages allow programmers to write partial functions: functions that are not defined on all the elements of their domain as specified by their type. Applying a partial function to a value on which it is not defined will raise a run-time exception, thus in practice well-typed programs can and do still go wrong. To warn programmers about such errors, contemporary compilers for functional languages employ a local and purely syntactic analysis to detect partial case-expressions—those that do not cover all possible patterns of constructors. As programs often maintain invariants on their data, restricting the potential values of the scrutinee to a subtype of its given or inferred type, many of these incomplete case-expressions are harmless. Such an analysis does not account for these invariants and will thus report many false positives, overwhelming the programmer. We develop a constraint-based type system that detects harmful sources of p...