inexhaustive pattern examples in error messages

[karananand01]

This pull request aims to produce a more verbose error displayed by the implementation of the exhaustiveness checking feature mentioned in “Live Pattern Matching with Typed Holes (https://victoryyw.github.io/assets/pdfs/pattern.pdf)”.

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 done by using an error_exp called InexhaustiveMatch (created in #1114), which behaves uniquely when supplied to CursorInspector.re. We aim to supplement the produced error hole to display a pattern that can be produced by the case expression’s scrutinee but is not matched by any of the branches of the case expression.

This is planned to be done by utilizing the final constraint generated to produce the inexhaustive error and inverting it ( using the dual of the constraint ). The inverted constraint should include patterns that are not matched and therefore we can map the constraint to a pattern to be displayed on the error interface.

[pigumar1]

Theoretical(?) basis:
A case expression is necessarily exhaustive => (its corresponding final constraint |> truified |> dual) is inconsistent => no values of the given type satisfy it

A case expression is necessarily inexhaustive => some value(s) of the given type satisfy it => there is some non-empty subset of final expressions of the given type that does not satisfy the final constraint, but satisfies its dual.

Next we will show (inductively) that for a consistent dual (sometimes represented as a list of constraints here), there is always some constraint that, obviously, can be emitted from a single pattern that once that constraint is satisfied, the entire dual is satisfied.

Hole constraints are truified, and Falsity constraints shouldn't appear. For simplicity, Truth constraints and repeated constraints are removed.

Base case 1: the dual is a Truth constraint (the case expression has no branches at all). Any pattern of the given type can be used to satisfy the dual.

Base case 2: the dual is a conjunction of Int/NotInt constraints.
For such dual to be consistent, the list should have at most 1 Int constraint, and others (if any) should be NotInt.

• If there is exactly one Int constraint in the list, that constraint must be the one that if satisfied, the whole dual is satisfied. If we pick a different integer, it cannot satisfy that constraint, not to mention the entire dual.
• (credit: @DavidFangWJ) If there is no Int constraint in the list, all the constraints in the list are going to be NotInt. We can pick an integer that is one larger than the largest integer among all associated with the NotInts, which satisfies the dual. We can construct an Int constraint with it to denote this fact.
• The same thing works for Float/NotFloat constraints and String/NotString constraints.

Recursive cases:
And constraint: can always be destructured to a list of constraints.

Or constraint: for such dual to be consistent, there must be a constraint such that once it's satisfied, at least one of the "subconstraints" of the Or is satisfied, and it can be used to satisfy the entire dual.

The dual is a conjunction of InjL constraints: there must be some constraint xi s.t. if it's satisfied, all the "unwrapped constraints" are satisfied:

And InjL(xi) is the constraint that once satisfied, the entire dual will be satisfied.
The same thing works for InjR constraints.

The dual is a conjunction of Pair constraints: there must be at least one constraint xi1 s.t. if it's satisfied, the "0th projection constraint" is satisfied. And there must be another constraint xi2. And Pair(xi1, xi2) is the constraint that once satisfied, the entire dual will be satisfied.

[pigumar1]

A temporary type defined to simulate bool. If some value of b != True, that indicates that some constraint is consistent, and an additional Constraint is kept track of such that once it's satisfied, some dual is satisfied.

It's used to make the changes trackable, but it might be more intutive to change the signature of is_exhaustive = (xi: Constraint.t): bool to satisfy = (xi: Constraint.t): option(Constraint.t) and this auxillary type can be got rid of (drastic change!).

[pigumar1]

The auxilliary constraint is printed to the console.

[pigumar1]

If the basis above works, the next step would be to reverse the auxilliary constraint into a UPat.term based on the type, and the further step would be to display it in the cursor inspector instead of the console.

[cyrus-]

I am unable to actually edit case expressions effectively in this branch, e.g. can't press backspace here and various other similar situations:

[cyrus-]

For when I do get it to work, we need to think about the UI design for large error messages like these where the message gets cut off. Maybe a toggle that makes the bottom bar larger to show the full message when it exceeds the length of the display? Thoughts @disconcision ?

Also, given the above problem is solved, how hard would it be to list all of the cases that aren't matched, rather than just one example?

[disconcision]

@cyrus- to start maybe have a short and long version of messages, with the short version having some affordance at the end e.g. ellipses indicating there's more. clicking on the affordance, or maybe just anywhere in the message part of the bar, could cause the bar to expand to take up more lines. clicking again makes it a single line again.

similarly but alternatively, you could make the bar's expanded state triggered on hover, and while hovered, show an additional pin icon that could be pressed to make the expanded state stick until unpinned.

(for this particular error, it would be nice if we could eventually show it inline... an 'angry ghost' of an unhandled case below the last case)

extremely rough mockup: