# Auto-split: Automatic case splitting GHC plugin

**URL:** <https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404>\
**Category:** Announcements\
**Created:** [February 14, 2025, 5:31am UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404 "2025-02-14T05:31:32Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![aaron-allen](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aaron-allen/32/3168_2.png) [@aaron-allen](https://discourse.haskell.org/u/aaron-allen)\
**Post date:** [February 14, 2025, 5:31am UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/1 "2025-02-14T05:31:32Z")

</div>

`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:

[Github](https://github.com/aaronallen8455/auto-split)  
[Hackage](https://hackage.haskell.org/package/auto-split-0.1.0.2)

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [February 14, 2025, 2:07pm UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/2 "2025-02-14T14:07:46Z")

</div>

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](https://github.com/haskell/haskell-language-server/issues/3525#issuecomment-1469322994). Your code seems to be brief and neat, so that gives me hope it would not be that difficult to implement.

---

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [February 15, 2025, 10:15am UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/3 "2025-02-15T10:15:47Z")

</div>

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.](https://mail.haskell.org/pipermail/haskell-cafe/2024-January/136545.html)

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [February 15, 2025, 2:23pm UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/4 "2025-02-15T14:23:51Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [February 15, 2025, 8:56pm UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/5 "2025-02-15T20:56:35Z")

</div>

> [@jaror](#):
>
> The pattern match analysis is adequate in the most common scenarios.

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.

---

<div class="post-metadata">

**Author:** ![prophet](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/prophet/32/5031_2.png) [@prophet](https://discourse.haskell.org/u/prophet)\
**Post date:** [February 16, 2025, 1:27am UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/6 "2025-02-16T01:27:37Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [February 16, 2025, 9:30pm UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/7 "2025-02-16T21:30:41Z")

</div>

> [@prophet](#):
>
> That it doesn’t look inside view patterns or pattern synonyms is intended behavior because everything else is a massive abstraction leak.

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](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/view_patterns.html) does not mention this at all, and the linked [wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/view-patterns#view-patterns-lightweight-views-for-haskell) 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.

---

<div class="post-metadata">

**Author:** ![soulomoon](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/soulomoon/32/2272_2.png) [@soulomoon](https://discourse.haskell.org/u/soulomoon)\
**Post date:** [February 18, 2025, 5:21pm UTC](https://discourse.haskell.org/t/auto-split-automatic-case-splitting-ghc-plugin/11404/8 "2025-02-18T17:21:03Z")

</div>

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](https://gitlab.haskell.org/ghc/ghc/-/issues/19272#note_450805)