I am very lucky to have been accepted to the Google Summer of Code 2026, to be working under the Haskell Foundation in LiquidHaskell.
I still remember trying out LiquidHaskell for the first time a couple of years ago in my Formal Methods course, and being surprised that we can extend the language with liquid types via this library/plugin.
Lately I’ve been trying to figure out what works best for me when it comes to making my brain work and how to come up with actual original creative ideas. I have this feeling that I didn’t explore that as much as I should have during my undergrad years.
For this project I want to do something different: I will be documenting my learning progress and my creative process in here. I don’t know how to structure this yet, maybe I’ll dump everything I do in a week on a post, or maybe I will keep them thematic. I will figure it out eventually.
In the meantime I just want to say, it’s good to be back on the blog. I’ve never been consistent with this and hopefully this new approach will force me to develop a new habit.
On the issue to solve
To not repeat myself, here is an extract taken from the abstract posted on the GSoC page for the project “Restoring Typeclass Refinement Support in LiquidHaskell”:
LiquidHaskell is a verification tool that allows Haskell developers to prove the correctness of their code through refinement types. This proposal aims to restore the support for type class elaboration: a feature that enables the verification of typeclasses laws and instances.
The work that had been done previously to support typeclass elaboration is currently broken: typeclass methods produce “Unknown logic name” errors, hence the test suite for the feature has been disabled.
The aim of this project is to restore this functionality, by fixing the elaboration mechanism responsible for making typeclass methods available during verification. I will trace the elaboration pipeline, implement the necessary fixes and extend test coverage.
The entry point for the challenge at hand is the following issue on the LiquidHaskell repository: #2450 Revive type class elaboration.
There are a few important links that we can gather. I won’t explain each one in detail, as they’re probably going to be irrelevant to anyone but me. But, I’ll leave them here for future reference.
- PR. #2434 Remove untested typeclass elaboration: The PR (never closed, but force-pushed to the main branch) disabling the tests that check typeclass elaboration, as long as the GHC version is 9 or more.
- A few issues that appear to be caused by the lack of proper typeclass support:
- Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell by Liu, et al.: The paper explaining the original implementation of typeclasses in LiquidHaskell.