This post is under revision by the Tweag editors, and will undergo a few adjustements before being posted on the Tweag blog.
In this post I share the main insights and contributions done during my project for the Google Summer of Code with Haskell.org and Tweag. I will walk through the main breaking points that I identified and their solutions, before briefly discussing the current state of the project and the limitations that emerged while expanding the test suite.
Ask a Haskell programmer what makes a Monoid instance well-behaved, and the
answer will certainly involve laws: <> should be associative and mempty
should act as an identity. In Haskell, it is common practice to describe
structures, many of them implemented as type classes, in terms of the properties
that should hold for them.
However, the responsibility of checking that the instances are well-behaved usually falls on the developer. This is where Liquid Haskell (LH) can be really convenient, as it will delegate to an SMT solver the task of proving that the properties hold for instances of a class.
That feature used to exist back when LH targeted GHC 8, but as the library moved on to GHC 9, it broke and its test suite was disabled. During my GSoC 2026 project, I worked on bringing it back; the work is documented in this PR. I am thrilled to say that type classes are once again supported in LH and the test suite has been re-enabled.
Most of the machinery for working with type classes is not new. It was built during the GHC 8 era, and credit goes to its original authors: Yiyun Liu, James Parker and Niki Vazou. What the restoration required was a proper integration with the new GHC 9 API, and making targeted adjustments that account for recent developments that have taken place in LH since then.
Before we dive into the work that was done, let's take a look at an example
(taken from
All.hs
in the test suite):
class Semigroup a where
{-@ mappend :: a -> a -> a @-}
mappend :: a -> a -> a
class Semigroup a => VSemigroup a where
{-@ lawAssociative :: v:a -> v':a -> v'':a -> {mappend (mappend v v') v'' == mappend v (mappend v' v'')} @-}
lawAssociative :: a -> a -> a -> ()
data PNat = Z | S PNat
instance Semigroup PNat where
mappend Z n = n
mappend (S m) n = S (mappend m n)
instance VSemigroup PNat where
lawAssociative Z _ _ = ()
lawAssociative (S p) m n = lawAssociative p m nThere are a few things worth noticing here. The laws that describe the behaviour
of a class are no longer an agreement invisible to the user, but through
VSemigroup, we actually have a way of allowing the user to provide a proof to
the specification declared as a method.
For PNat, the body of lawAssociative serves as the proof that the law holds
for that instance. The recursive call on the first argument carries out the
induction: LH verifies the base case directly and the recursive call on the first
argument instructs the solver the induction hypothesis to use for the successor
case.
In order to accomplish this, LH mirrors what GHC already does: while GHC compiles classes into record types, LH will generate a specification of the respective dictionary; GHC turns methods into record selectors, and LH lifts them into the refinement logic; and instances are elaborated into evidence by GHC, whereas LH will check the class's laws for a concrete type.
In order to do its work, LiquidHaskell hooks into GHC as a plugin: LH consumes GHC's intermediate representation, calls its API, and even asks GHC to elaborate expressions on its behalf. This closeness between the two makes their integration seamless, but also puts pressure on the LH maintainers to keep up with the changes made to the compiler.
In particular, the release of the compiler's version 9 brought many changes to LH, but the feature to check type classes was left behind, and thus the corresponding tests where guarded for earlier GHC versions:
executable typeclass-pos
...
-- Fails on GHC 9.0.1
if impl(ghc < 9)
other-modules: ...
So, the first thing to do was to run the broken tests and identify the errors. The exploration was not as straightforward, since often an error would only show up after solving a different error at an earlier stage in the pipeline.
But looking back, the errors can be classified in three buckets:
- Name resolution: Refinements that mentioned type class methods failed because their names were not visible to the resolver.
- Elaboration of expressions: Methods (or laws) elaborated through GHC came back incomplete, specially in subclasses; e.g. unbound symbols and wrong number of binders.
- Measure generation: The generated measures had dictionary constructors of the wrong shape, producing arity errors and mismatched types in the constraints.
The way I approached these problems was to use the behavior of the GHC 8 version as an oracle: I traced each error to find the pieces of code where the behaviour diverged from the working implementation, and re-aligned the two.
I address these issues in the same order in the sections that follow.
After the migration to GHC 9, LiquidHaskell introduced a significant change: the name resolution module. This new phase in the compilation stands as an entrypoint through which all names used by LH have to go. However, this new pipeline did not account for type class methods.
If you tried to run a test involving type classes after the introduction of name
resolution, even doing something as simple as mentioning an imported class
method in a specification, would throw an error. For example, this module
imports check and uses it in the specification of a class law:
{-@ LIQUID "--typeclass" @-}
module Example where
import Check (MyCheck, check)
class MyCheck a => MyVCheck a where
{-@ lawValid :: v:a -> {check v} @-}
lawValid :: a -> ()LiquidHaskell could not resolve check in the specification:
Unknown logic name `check`
Cannot resolve name
|
7 | {-@ lawValid :: v:a -> {check v} @-}
| ^^^^^
The way to solve this consists of making LH aware of the existence of such class methods during the name resolution phase. If the lookup in LH's environment fails, we can leverage GHC's environment and check if there is a match for the name we are interested in. If that is the case, the name can be registered in the logic as long as the entry's parent is a class (making sure it is a class method).
For the time being, we assume that if the user wants to use class methods in specifications, they will also want to activate typeclass checking. Therefore we show an error message inviting the user to enable typeclass support.
Unknown logic name `check`
This is a class method, but typeclass support is disabled.
Enable it with {-@ LIQUID "--typeclass" @-}.
When compiling code that uses a type class method, GHC will insert the dictionary
which corresponds to the instance on which it is being called. Similarly, in
order to reach a superclass method, it is necessary to first extract the parent
dictionary. GHC stores that parent dictionary as a field of the subclass
dictionary and generates a selector to retrieve it. For example, $p1VSemigroup
is a compiler-generated selector1 for the Semigroup dictionary stored
inside a VSemigroup dictionary, so GHC produces
mappend ($p1VSemigroup vsemigroupDict) x y instead of
mappend vsemigroupDict x y. This applies only to subclasses, since only they
have superclass dictionaries.
For LH to check a specification referencing these methods, it will hand the refinement to GHC and get back a Core expression. Therefore, GHC decides what dictionaries to insert at each location. These dictionaries are the evidence LH needs: they carry the implementations of methods and, for subclasses, the dictionaries of their superclasses. However, there were some slight changes in how those dictionaries are given: in GHC 8, the dictionaries used to be inlined in the application, whereas GHC 9 uses let-bindings to pass those arguments.
This was a breaking change, because the previous code was expecting abstract syntax trees with a different shape. In particular, non-inlined dictionary bindings were ignored, discarding important evidence in the elaborated expressions. The expressions therefore referred to free variables, resulting in errors such as "Unbound symbol".
The fix, then, was to not discard that evidence when elaborating the expressions. As with the rest of the restoration, I used GHC 8 as the source of truth and mimicked the behaviour it previously had: to inline the evidence instead.
Once the elaborated Core expression is returned by GHC, a function will traverse the tree to find evidence bindings (which can be easily identified via the GHC API) and substitute their occurrences by their definitions. This produces a valid expression with no unbound symbols.
I previously mentioned how classes are transformed into record types: every class declaration gives rise to the specification of a record that describes what the shape of the dictionary is, its fields and their respective types. That description is consumed in several places, most noticeably during measure generation2.
To use these record types, LH must determine the number of fields each record has and reconstruct the shape of the corresponding GHC dictionary. This must account for fields storing superclass dictionaries.
GHC 9 had some changes on what fields where returned by calls in the GHC API, and the expected arities started disagreeing in a few places because superclass fields were missing from the information LH received. This caused a series of errors and panics: "GHC gave back more/less binders than I expected", "Liquid Type Mismatch", "GHC and Liquid specifications have different numbers of fields", and so on.
Previously, different phases had different counting rules. The solution required
finding the correct rule to decide the arity of constructors, and applying the
adjustment throughout the code base. In particular it was necessary to always
count superclass dictionaries as fields for class dictionaries, by including the
data constructor's
theta information
: the type class constraints that accompany the constructor. This ensures that
all constraints, especially subclass constraints, are correctly included.
This was a targeted fix that only takes place when working with type classes, correctly solving the previous errors.
With the original tests passing again, I started adding new ones to cover some scenarios that were missing. That surfaced a few remaining gaps, present in GHC 8 too. Tickets were opened for each one, with small code examples to reproduce the errors:
- Issue #2727: For
a class such as
class M m where ret :: a -> m a, wheremis a higher-kinded parameter,mwill be elaborated as if it had kindTypeinstead ofType -> Type. This triggers a kind error during the verification process. - Issue #2728: GHC treats instances of single-method classes differently than it does others. The difference in the encoding will produce a result which, despite being verifiable by LH, triggers an error during the post-verification phase. Adding a second method (even a dummy one) will avoid the crash.
- Issue #2743: Some
special classes, such as
Eq,Ord, and the numeric classes, are embedded directly in the SMT solver. Their methods are translated into SMT primitives instead of using the definitions supplied by their instances. As a result, LH assumes that these instances have the standard behaviour of their classes and cannot verify laws against their actual implementations. - Issue #2744: A class is lifted into the LH logic only when at least one of its methods carries an LH specification. Without one, its methods cannot be used in refinements, and its instances are not checked against class specifications. It could be worth eliminating this requirement to make type class support easier to use, or documenting better how it is needed.
- Issue #2745: When a specification uses a class method whose constraints cannot be satisfied, LH reports an unbound dictionary symbol instead of a clear error resembling GHC's error messages.
These are the immediately identified issues. As type class support remains experimental, we should expect some other issues to be uncovered still by more tests to come.
Now we have a working test suite that runs the typeclass group on GHC 9: all the previously working tests pass again, unchanged, showing that the restoration was done properly. A few more tests were added, to check some specific critical points in the pipeline. Negative tests were included, to verify that LH fails when that is expected behaviour.
The user documentation was updated to match the implementation. Comments were added too, to explain some design choices and non-obvious steps in the code.
The whole restoration fits in about 150 lines of code, a small number because none of it is new machinery. Every change followed the same approach: find the place where GHC 9 and LiquidHaskell's pipeline had drifted apart, and re-align them, trying to stay as close as possible to the GHC 8 implementation.
Thanks to my mentor, Facundo Domínguez, for the guidance and for steering me in the right direction as every new error came up; to the Haskell Foundation and Google Summer of Code for making the project possible; and to Tweag, for their work on LiquidHaskell and for hosting this post.
Footnotes
-
The exact name is an implementation detail which may vary and is internal to GHC. ↩
-
Measures are functions that refine the types of data constructors and lift them to the logic. Generating a measure for a data constructor (or a record type) requires identifying the shape of that constructor. This is important for type classes because of the transformation they undergo during compilation into record types. ↩