Case expression exhaustiveness & redundancy checking

[pigumar1]

This pull request aims to implement the exhaustiveness checking feature mentioned in Live Pattern Matching with Typed Holes.

If a case expression is necessarily inexhaustive (i.e.: the expression will necessarily fail to match all values of the type of its scrutinee), the expression will be wrapped with an error hole like in Fig. 2b in the paper. This is planned to be done by introducing a new error_exp called InexhaustiveMatch (tentative), which behaves uniquely when supplied to CursorInspector.re. Like discussed in #1059, we probably need a corresponding Self.exp for the new expression error. Self.match() might be modified accordingly.

Exhaustiveness checking on a case expression relies on whether the final constraint for the rules can be entailed from truth (i.e.: all expressions of the type of the case expression’s scrutinee “determinately or indeterminately match any of the branches”). This final constraint for the rules is discovered in the process of typing the rules of the match expression, which is to be implemented by applying the sequence of rules to a type generator called ruls_to_info_map (tentative). It corresponds to the judgment TRules in the paper (ideally). ruls_to_info_map is going to be based on the list scheme List.fold_left instead of List.map since the info of rules will be dependent on each other in the redundancy checking.

The entailment check itself has already been implemented in #1094 as the function Incon.is_exhaustive.

After checking the exhaustiveness, the branches are yet to be checked for type consistency (should they be in sequential order? Or should two errors show up in the cursor inspector at the same time?) So the output of ruls_to_info_map probably contains a list of expression types for branches and the final constraint for the rules.

(Karan Anand got involved in editing the proposal)

[cyrus-]

same here