I have a list of entities. The entities are partitioned by different properties (like color, speed and so on, partitions usualy cover the whole list but not always). Compilers like Haskell and Fsharp can catch exhaustiveness over individual entities or each property individually. Problems arise when they are combined. For example first case covers red and blue entities, second case covers fast entities, thirs case explicitly covers entity 1 and 2. Now the question is whether this is exhaustive. Compiler of Fsharp just tells me it is not and one has to provide the otherwise case and do something there (raise exception, return none or something). But in this case the correctness is proven only during the execution. From the outside persons point of view this is the same behavior. The program has crashed.

I as a developer can go through the cases and reason that those cases are actually exhaustive and move on. Problem is that this is time consuming and one would need to check everything every time the partitionings change (which happens).