auto-split is a newly released GHC plugin that performs automatic case splitting. By tapping into GHC’s knowledge of missing patterns, this plugin is able to update source code to make a targeted pattern match group exhaustive. See the readme for instructions:
32 Likes
This is awesome! I would love a HLS code action version of this. There’s quite a history of people trying, I think the latest info is here: Simpler Tier 1 tactics for case splits · Issue #3525 · haskell/haskell-language-server · GitHub. Your code seems to be brief and neat, so that gives me hope it would not be that difficult to implement.
8 Likes
Wonderful! Sadly, the incomplete pattern match analysis currently in GHC is not working properly, and is likely undecidable thanks to ViewPatterns that can contain arbitrary, even non-terminating functions. See this discussion.
1 Like
The pattern match analysis is adequate in the most common scenarios. It is just a tool to save you from typing out cases by hand. I don’t think it is that bad if it inserts some redundant cases in complicated scenarios. That said, users do indeed need to be warned about this.
1 Like
Indeed it is. I believe that much more convenience could be achieved if view patterns were separated from other patterns. I hope to be able to publish some code in this direction soon.
How is GHC’s exhaustiveness analysis “not working properly”?
That it doesn’t look inside view patterns or pattern synonyms is intended behavior because everything else is a massive abstraction leak.
The correct behavior there is to assume that pattern synonyms are inexhaustive unless there is a COMPLETE pragma and that view patterns can produce any value of the resulting type, which is exactly what GHC does.
2 Likes
That was the opinion already in the Haskell Cafe thread I linked to. From a topological perspective, an ordinary pattern divides a type into two observably distinct parts. Observably here means that the corresponding predicate, e.g. isLeft is total. Since any algebraic type has only finitely many constructor patterns, coverage ought to be decidable. As @jaror said, this will serve in most circumstances.
Opaque synonyms and view patterns, while useful for abstraction, destroy this property and should therefore be considered a different kind of beast, but I seem to be the only one with this opinion. The GHC user guide for ViewPatterns does not mention this at all, and the linked wiki page contains this single short paragraph:
Exhaustiveness/Redundancy. It is hard to check for completeness of pattern matching; and likewise for overlap. But guards already make both of these hard; and GADTs make completeness tricky too. So matters are not much worse than before.
I would say: It needs not be hard, but we would have to sacrifice some expressiveness.
2 Likes
We have something that could improve coverage situation. #19272: E-Graphs for representation of normalised refinement types in the pattern-match checker · Issues · Glasgow Haskell Compiler / GHC · GitLab