Liquid Haskell is a system that extends GHC with refinement types. Constraints arising from the refinement types are sent to an external automatic theorem prover such as z3. By employing such additional checks, one can express more interesting properties about Haskell programs statically.

Up until now, Liquid Haskell has been a separate executable that uses the GHC API, but would run on Haskell files individually and just say “SAFE” or “UNSAFE”. If “SAFE”, one could then proceed to compile a program normally.

In the recent months, we have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are: First, there is just a single invocation necessary per Haskell source file, so the workflow becomes easier. Second, we can integrate with GHC and Cabal to support libraries and packages properly. When checking source files, Liquid Haskell requires information about the constraints already established for dependent libraries. Previously, these had to be hand-distributed for selected modules with Liquid Haskell itself. Now, they become part of normal GHC interface files and can be distributed for arbitrary user packages via Hackage.

In this talk, we present the Liquid Haskell plugin workflow and why we think it is superior to the old approach. We also discuss the implementation of the plugin: it is interesting because it does not neatly fit into the plugin categories currently provided. Morally, Liquid Haskell typechecks the code, but in order to generate constraints to feed to the prover, it must access (unoptimised!) core code. We explain the final design, and some of the iterations we needed to get there.