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].
Users of Diff aren’t affected, but Diff contributors can check the package with LiquidHaskell now [link]. This blog post tells the story of how it came to be [link]. And there is the now merged PR adding the initial checks [link].
Thanks much to the maintainers of Diff, David Fox and @Bodigrim. And thanks to Tweag for supporting my colleague @ninioArtillero to do this work.
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]. 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.
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.
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.
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.
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.
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.
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.
