Add coverage checking

[jonaprieto]

Description

Coverage checking must be performed after type checking. The algorithm expects all the patterns in clauses to be valid, meaning that every pattern covers at least one value of the corresponding argument type of the function.

Checklist

• [ ] Add a flag to disable the coverage check

• [ ] Add a keyword to disable exhaustiveness, possibly called total

• [ ] Add tests:

  • [ ] Negative tests
  • [ ] Positive tests
  • [ ] Shell tests

• Safeguards:

  • [ ] To carry on the analysis, it comes in handy to compute for each pattern row their set of "compatible" rows. Two rows are incompatible if they have no instance in common.
  • [ ] Delete any row that is "subsumed" by another row.
  • [ ] We announce exhaustiveness as soon as we find a row full of wildcards.

Checks:

• Exhaustiveness: (meaning that the pattern _ does not contribute to match more values):

  • [ ] Error: The pattern-matching is not exhaustive.
    • [ ] Show non-matching values as part of the error message

• [ ] Exact split tree

[lukaszcz]

What is the algorithm that you have in mind here?

[lukaszcz]

Will be closed with a proper implementation of a pattern compilation algorithm from the literature (issue #1798).