Liquid Haskell is a compiler plugin for GHC that can verify properties of Haskell programs. It used to be a standalone analyser tool, but it was converted to a plugin later on. This makes it feasible to support Haskell modules that use the latest language features, and immediately integrates the verification into the build workflows; but it also implies that Liquid Haskell is rather coupled with the internals of GHC. A consequence of this coupling is that a version of Liquid Haskell is likely to require modifications to support newer versions of the compiler. The effort of making these modifications is large enough that Liquid Haskell has lagged three or four versions behind GHC HEAD.

Among other contributions, Tweag committed to upgrading Liquid Haskell from version 9.0 to each major GHC version¹, culminating with the inclusion of Liquid Haskell in head.hackage (more below). This post is a report on the experience of upgrading a compiler plugin of 30,000 lines of code, and on what can be expected of new upgrades going forward. It will likely be of interest to developers using GHC as a library, to maintainers of other GHC plugins, and to potential users of Liquid Haskell who wonder about the effort of keeping it up-to-date.

The feel of a plugin upgrade

By putting a new compiler version on the path and starting a build of Liquid Haskell, we venture into the unknown. Every fresh build attempt with a new compiler version is going to require fiddling with dependency bounds in cabal packages. In addition, we might need to adapt to API changes in boot libraries (e.g. base, bytestring), and almost certainly to changes in the GHC API which Liquid Haskell uses to grab comments and desugar the Haskell programs to analyse.

Most of the time, API changes produce build errors. And most of the time, we can use API documentation to figure out the fixes. The GHC API is an exception though, where the terse documentation might require examining the git history, grepping the source code, and building a working knowledge of GHC internals.

The process can be laborious, but the interactions with the compiler eventually lead to a plugin that builds. Then the time comes to run Liquid Haskell on all of the 1800+ test modules and discover the breakages that did not manifest as build errors.

There are often multiple test failures to diagnose. To progress, one needs to pick the least scary, fix it, and hope that it will make some other test failures go away as well.

Of all the steps, fixing the test failures is by far the most expensive. We need to analyse the execution to discover where it goes amiss, and we get exposed to the internals of Liquid Haskell and GHC in the process. We know what the behavior of the plugin should be, but it is not always obvious how to fix it.

For instance, in GHC 9.2 a function like f x = x + 1 was desugared to:

f x = x + fromInteger 1

In GHC 9.4 the desugaring changes to:

f x = x + fromInteger (GHC.Num.Integer.IS 1#)

And while Liquid Haskell accepts the program with GHC 9.2, with GHC 9.4 it started producing an error in a call site of function f:

    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | (v <=> x < y)
                                 && v == (x < y)}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Bool | VV}
    .

The details of the error message are not important, but it shows that some inspiration and sleuthing is necessary to connect the error message to the change in desugaring, and later on, it requires yet more inspiration to choose a fix. The first fix that came to mind was fiddling with the GHC intermediate AST to retain the old desugaring that GHC 9.4 did. But the weight of many accumulated fixups like that one would suffocate the maintainer. Instead, the adopted fix was to teach Liquid Haskell that GHC.Num.Integer.IS 1# == 1, which is difficult to propose without having some familiarity with both Liquid Haskell and GHC internals.

The hardest test failures

In practice, the upgrade between two consecutive major versions has required between 20 and 60 hours of engineering time, with every upgrade being a unique challenge. But in general, changes in desugaring to Core have been the hardest to adapt to, and at least once it was laborious to find a replacement to a removed feature in the GHC API.

Liquid Haskell is not robust to ingesting every possible Core expression. Instead, it is tailored to the expressions that GHC produces. And invariably, changes in desugaring can only be discovered when running tests. Examples of this are changes to how pattern matching errors are implemented in Core; or changes to the data constructors used for integer literals; or changes to how many type/kind/levity variables the ($) operator employs; or changes to whether breakpoints are inserted by default when desugaring, which does affect whether local bindings are inlined.

An example of a feature that was removed from the GHC API was ApiAnn. This was a collection of annotations about a Haskell program. These annotations included the source code comments holding the specifications that Liquid Haskell needs to verify a Haskell program.

For instance, for a program like:

{-@ f specification in a special comment @-}
f = ... g ... h ...
  where
    -- a regular comment
    h = ...
    {-@ g specification in another comment @-}
    g x = ...

The GHC API would offer all comments together:

[ "{-@ f specification in a special comment @-}"
, "-- a regular comment"
, "{-@ g specification in another comment @-}"
]

It was all too comfortable to reach for this list in the GHC API, and have Liquid Haskell iterate over it to get the relevant comments.

After the removal though, the comments were spread across the abstract syntax tree of Haskell programs, and some investigation was necessary to discover how deep Liquid Haskell needed to dive in the abstract syntax tree, what solution was reasonable for the case, and whether it was already implemented.

What makes changes to the GHC API so hard to tackle is in essence a communication problem. The Liquid Haskell developers need to investigate the changes to the GHC API, analyse their impact, and lay down the context that will enable GHC developers to collaborate. On the other hand we can’t go all the way in the opposite direction and ask the GHC developers to understand what each change breaks in Liquid Haskell by themselves.

I have started developing a suite of unit tests to encode the assumptions that Liquid Haskell makes about desugaring and about the GHC API in general. For example, if Liquid Haskell expects integer literals to be desugared in a specific way, there should be a test here that checks that a concrete integer literal desugars as expected. The test suite still needs to grow for a while before it becomes effective. But nonetheless it is already run against GHC’s HEAD (via head.hackage). Unlike the full test suite of Liquid Haskell, these unit tests only test functions in the GHC API, which makes it feasible for GHC developers to understand test failures. They might not always be sure what to do about it, in which case we can work together to find a solution promptly.

The future on head.hackage

head.hackage is a repository of patched Haskell packages to use with GHC pre-releases. When a package is in head.hackage, GHC developers might contribute fixes to keep the packages building when the compiler changes. This is helpful to test GHC and to allow testing packages whose dependencies don’t support GHC HEAD yet. In this way, GHC developers can also collaborate with users to help them catch up. Liquid Haskell entered head.hackage this year.

Looking at the upgrade issues we encountered, head.hackage is going to help with the first steps in the upgrade process. Dependency bounds will likely be updated in head.hackage, and build errors will be fixed there as well. Features that are removed from the GHC API will be replaced when there is an obvious replacement. This can constitute an important saving of effort, as a replacement can seem obvious to GHC developers more often than it does to users!

That’s not the end of the story though. A case like the removal of ApiAnn admits a simple solution to replace it, but GHC developers might still need insight on what Liquid Haskell needs the old feature for. Otherwise, it may be difficult to pick between the alternatives.

In the short term, changes to desugaring will remain difficult to diagnose until more of the assumptions made about the GHC API are captured in unit tests. These are the only tests that can provide relevant feedback to someone not eager to debug Liquid Haskell. When these tests fail to detect broken assumptions, debugging sessions will ensue.

In sum, having Liquid Haskell in sync with GHC HEAD is going to facilitate the collaboration needed to keep it up-to-date. We can get some of the advice needed from head.hackage and focus on the debugging work that can only be done with insight of the Liquid Haskell internals. Special thanks to the various GHC developers that engaged in exploring the options to set up collaboration, and thanks to Niki Vazou and Ranjit Jhala for helping me analyse Liquid Haskell misbehaviours.