Exhaustiveness and redundancy checks for case expressions

This PR adds exhaustiveness and redundancy checking for case expressions with pattern holes.

Each pattern form is associated with one or more constraints that determine which expression forms it can match. Case expressions are analyzed statically and classified as either not exhaustive, indeterminately exhaustive, exhaustive, or redundant. Error boundaries are drawn around non-exhaustive case expressions and redundant rules.