# Diff package adopts LiquidHaskell for static checks

**URL:** <https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377>\
**Category:** Announcements\
**Created:** [July 10, 2026, 10:53am UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377 "2026-07-10T10:53:00Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![facundominguez](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/facundominguez/32/3486_2.png) [@facundominguez](https://discourse.haskell.org/u/facundominguez)\
**Post date:** [July 10, 2026, 10:53am UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/1 "2026-07-10T10:53:00Z")

</div>

Hello, dear haskellers!

I want to make a splash about LiquidHaskell being used for static checks in the Diff package, used transitively by more than 17000 packages according to `hackage-revdeps` [[link]](https://hackage.haskell.org/package/hackage-revdeps).

Users of Diff aren’t affected, but Diff contributors can check the package with LiquidHaskell now [[link]](https://github.com/seereason/Diff#checking-diff-with-liquid-haskell). This blog post tells the story of how it came to be [[link]](https://www.tweag.io/blog/2026-06-11-diff-package-static-checks/). And there is the now merged PR adding the initial checks [[link]](https://github.com/seereason/Diff/pull/29).

Thanks much to the maintainers of Diff, David Fox and @Bodigrim. And thanks to Tweag for supporting my colleague @ninioArtillero to do this work.

Onwards and upwards, LiquidHaskell!

---

<div class="post-metadata">

**Author:** ![augustss](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/augustss/32/887_2.png) [@augustss](https://discourse.haskell.org/u/augustss)\
**Post date:** [July 10, 2026, 11:10am UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/2 "2026-07-10T11:10:55Z")

</div>

Out of curiosity, did Liquid Haskell find any bugs?

---

<div class="post-metadata">

**Author:** ![facundominguez](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/facundominguez/32/3486_2.png) [@facundominguez](https://discourse.haskell.org/u/facundominguez)\
**Post date:** [July 10, 2026, 12:13pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/3 "2026-07-10T12:13:31Z")

</div>

The static checks found no violations, but the process of adding the static checks requires a rather deep review of the code and the slim documentation. This review did surface an unlawful Ord instance [[link]](https://github.com/seereason/Diff/pull/24). The unlawful instance didn’t produce misbehavior of Diff though.

IIRC, no other bugs were uncovered, although there was plenty of insight to lower the effort of understanding the code with refactorings and documentation contributions. Together with the static checks, I find Diff a tad easier to change and review now.

---

<div class="post-metadata">

**Author:** ![ranjitjhala](https://avatars.discourse-cdn.com/v4/letter/r/8edcca/32.png) [@ranjitjhala](https://discourse.haskell.org/u/ranjitjhala)\
**Post date:** [July 10, 2026, 7:14pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/4 "2026-07-10T19:14:19Z")

</div>

Great stuff, thanks @facundominguez and @ninioArtillero !!!

---

<div class="post-metadata">

**Author:** ![thielema](https://avatars.discourse-cdn.com/v4/letter/t/ee59a6/32.png) [@thielema](https://discourse.haskell.org/u/thielema)\
**Post date:** [July 16, 2026, 11:15pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/5 "2026-07-16T23:15:52Z")

</div>

Great to see a real world library adopts Liquid Haskell. So far, I had no luck to add Liquid Haskell checks to any of my libraries, even the really simple ones. I always hit a bug or a LH limitation. ☹

---

<div class="post-metadata">

**Author:** ![thielema](https://avatars.discourse-cdn.com/v4/letter/t/ee59a6/32.png) [@thielema](https://discourse.haskell.org/u/thielema)\
**Post date:** [July 17, 2026, 5:04pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/6 "2026-07-17T17:04:23Z")

</div>

LiquidHaskell emits no complaint, however, GHC warns about the use of List.head. Would it be possible to replace the lists in the Diffs by NonEmpty?

---

<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:** [July 17, 2026, 5:13pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/7 "2026-07-17T17:13:02Z")

</div>

If you’re using Liquid Haskell you should just disable that warning. A big advantage of Liquid Haskell is that it can give better errors for functions that would be partial if you don’t refine the type.

---

<div class="post-metadata">

**Author:** ![thielema](https://avatars.discourse-cdn.com/v4/letter/t/ee59a6/32.png) [@thielema](https://discourse.haskell.org/u/thielema)\
**Post date:** [July 17, 2026, 5:28pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/8 "2026-07-17T17:28:53Z")

</div>

In the particular code I see that the function `ses` has an @ignore@ tag, thus no check on `head` is performed. But there is a non-trivial use of `head` in it, namely a `head . dropWhile`.

---

<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:** [July 17, 2026, 5:45pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/9 "2026-07-17T17:45:37Z")

</div>

Ah indeed, I just saw that in the blog post too. It seems to me that any use of `NonEmpty` can easily be replaced by a refinement type, so conversely if we can’t easily give something a suitably refined type then it will probably be even harder to change the code to use `NonEmpty`.

---

<div class="post-metadata">

**Author:** ![facundominguez](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/facundominguez/32/3486_2.png) [@facundominguez](https://discourse.haskell.org/u/facundominguez)\
**Post date:** [July 17, 2026, 5:59pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/10 "2026-07-17T17:59:26Z")

</div>

> [@thielema](#):
>
> But there is a non-trivial use of `head` in it, namely a `head . dropWhile`.

That is well noted. Termination of `ses` would come in a later PR. If you are interested, @ninioArtillero has work in progress about it.

---

<div class="post-metadata">

**Author:** ![ninioArtillero](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ninioartillero/32/4285_2.png) [@ninioArtillero](https://discourse.haskell.org/u/ninioArtillero)\
**Post date:** [July 17, 2026, 8:03pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/11 "2026-07-17T20:03:06Z")

</div>

The `ignore ses` annotation carries heavy weight: proving that `dropWhile` produces a non-empty list, i.e. returns the algorithm’s endpoint, is not straight-forward because Liquid Haskell has important (perhaps fundamental) limitations to reason about infinite values. My current approach is refactoring it to use explicit recursion (not library functions) to translate such requirement to a simple termination proof.

---

<div class="post-metadata">

**Author:** ![ninioArtillero](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ninioartillero/32/4285_2.png) [@ninioArtillero](https://discourse.haskell.org/u/ninioArtillero)\
**Post date:** [July 17, 2026, 8:18pm UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/12 "2026-07-17T20:18:43Z")

</div>

This is surely the case to some degree: both encode a non-emptiness proof in their own way. Intuitively, `NonEmpty` value carries it within, while refinement types enforce it at the boundaries.

---

<div class="post-metadata">

**Author:** ![facundominguez](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/facundominguez/32/3486_2.png) [@facundominguez](https://discourse.haskell.org/u/facundominguez)\
**Post date:** [August 12, 2026, 11:11am UTC](https://discourse.haskell.org/t/diff-package-adopts-liquidhaskell-for-static-checks/14377/13 "2026-08-12T11:11:28Z")

</div>

> [@thielema](#):
>
> In the particular code I see that the function `ses` has an @ignore@ tag

👋 There is a termination proof for `ses` now, which also happens to motivate some optimization of the code.

[Prove termination of (optimized) diff algorithm implementation by ninioArtillero · Pull Request #37 · seereason/Diff · GitHub](https://github.com/seereason/Diff/pull/37)