Restoring type class support in Liquid Haskell

17 September 2026 Juan Pablo Yamamoto

An internship experience report on reenabling type class support in Liquid Haskell

• liquidhaskell
• haskell
• formal-methods
• high-assurance

Over the last months, I’ve participated in a Google Summer of Code internship at Tweag in collaboration with Haskell.org, with the goal of bringing type class support back to Liquid Haskell. In this post, I will share the major insights and contributions that resulted from this project, walking 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.

What is type class support, anyway?

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 by LH, and that the test suite has been re-enabled.

Most of the machinery for working with type classes isn’t 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.

When a class becomes a proof obligation

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 n

There 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 tells the solver which 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.

What broke in the GHC 8 to 9 migration

In order to do its work, Liquid Haskell hooks into GHC as a plugin: It 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 were 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, errors can be classified in three buckets:

• Name resolution: Refinements that mention type class methods failed because their names weren’t visible to the resolver.
• Elaboration of expressions: Methods (or laws) elaborated through GHC came back incomplete, especially 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 GHC 8 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 will address these issues in the same order in the sections that follow.

Teaching the resolver about class methods

After the migration to GHC 9, Liquid Haskell introduced a significant change: the name resolution module. This new phase in the compilation serves as an entry point 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, LH 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 -> ()

When building this, Liquid Haskell 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 (thus 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 type class checking. Therefore we show an error message inviting the user to enable type class support:

Unknown logic name `check`
This is a class method, but typeclass support is disabled.
Enable it with {-@ LIQUID "--typeclass" @-}.

Where did dictionaries go?

When compiling code that uses a type class method, GHC inserts the dictionary that 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 selector¹ 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 hands the refinement to GHC to obtain 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, the 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.

Counting fields on dictionary constructors

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 generation².

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 were returned by 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 executes when working with type classes, correctly solving the previous errors.

Known limitations

With the original tests passing again, I started adding new ones to cover some scenarios that were missing. That surfaced a few remaining gaps that were already present in GHC 8. 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, where m is a higher-kinded parameter, m will be elaborated as if it had kind Type instead of Type -> Type. This triggers a kind error during the verification process.
• 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.

Conclusion

We now have a working test suite that runs the type class group on GHC 9: all 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 as well, 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 Liquid Haskell’s pipeline had drifted apart, and re-align them, trying to stay as close as possible to the GHC 8 implementation.

I want to thank my mentor, Facundo Domínguez, for his guidance and for steering me in the right direction as each new error came up; to the Haskell.org committee and Google Summer of Code for making the project possible; and to Tweag, for their work on Liquid Haskell and for hosting this post.

1. The exact name is an implementation detail which may vary and is internal to GHC. ↩

2. 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. ↩