Implement exhaustivity checks

[DarkDimius]

Better done as a separate phase before pattern matcher.

[DarkDimius]

See http://research.microsoft.com/en-us/um/people/simonpj/papers/pattern-matching/gadtpm-acm.pdf

[smarter]

Note that the Scala equivalent of their vzip example does not compile in Dotty currently because our gadt support is overly restrictive, I hope to be able to fix this at some point.

[liufengyun]

As an update, currently I'm playing with an algorithm outlined as follows:

https://gist.github.com/liufengyun/66bf0c1bc44cdad12e45dd6db689e9b3

The algorithm is basically in the same spirit as what's done in OCaml (Warnings for pattern matching, L. Maranget, 2007), but is more intuitive, easy to adapt for Scala and generate friendly warning messages.

I haven't proved correctness of the algorithm, it's possible to do a mechanised proof. But for now, if it makes some sense to you, I want to focus on implementation and rely on testing to ensure its correctness.

[smarter]

@liufengyun : This looks interesting. @adriaanm : the exhaustiveness checker in scalac uses a SAT solver, do you think this is actually fundamentally needed?

[adriaanm]

The solver is not fundamental, but I feel it has made for a nice separation-of-concerns in the pattern matcher analyses. I'm not familiar with Maranget's algorithm, but integrating ML-style pattern matching into Scala's was how the old pattern matcher actually became quite hard to maintain. That doesn't mean all similar approaches are doomed -- just a datapoint.

[liufengyun]

Thanks @adriaanm . To be clear, the algorithm I'm playing with doesn't touch anything related to patmat compilation. If the previous complexity was related to ML-style patmat compilation, that might be a relief.

[adriaanm]

Part of the complexity was because compilation and analysis were intertwined in the old algorithm. The new approach rewrites for optimization, so that you can actually turn off all analyses and do the naive desugaring.

[smarter]

What kind of optimizations does the analysis enable?

[adriaanm]

The same logic enables common prefix elimination (e.g., if all outer patterns check the same thing for all cases) but we could do more.

[DarkDimius]

Was implemented in #1364