Liquid Haskell (LH) is a formal verification tool for Haskell programs, with the potential to prove correctness with considerably less friction than approaches that aim to make code correct by construction using dependent types—often at the cost of heavy refactoring (as argued in a previous post). It has come a long way towards becoming a usable tool by adding quality-of-life features to foster its adoption. Think optimization of spec verification and improved user experience.

During my GSoC 2025 Haskell.org project with Tweag, I worked on a seemingly small but impactful feature: allowing LH’s type and predicate aliases to be written in qualified form. That is, being able to write Foo.Nat instead of only just Nat, like we can for regular Haskell type aliases.

In this post, I introduce these annotations and their uses, walk through some of the design decisions, and share how I approached the implementation.

Aliasing refinement types

Type and predicate aliases in LH help users abstract over refinement type annotations, making them easier to reuse and more concise. A type alias refines an existing type. For instance, LH comes with built-in aliases like Nat and Odd, which refine Int to represent natural and odd numbers, respectively.

{-@ type Nat = {v: Int | v >= 0 } @-}

{-@ type Odd = {v: Int | (v mod 2) = 1 } @-}

Predicate aliases, by contrast, capture only the predicate part of a refinement type. For example, we might define aliases for positive and negative numerical values.

-- Value parameters in aliases are specified in uppercase,
-- while lowercase is reserved for type parameters.

{-@ predicate Neg N = N < 0 @-}

{-@ predicate Pos N = N > 0 @-}

Enter the subtle art of giving descriptive names so that our specifications read more clearly. Consider declaring aliases for open intervals with freely oriented boundaries.

{-@ predicate InOpenInterval A B X =
      (A != B) &&
      ((X > A && X < B) || (X > B && X < A)) @-}

{-@ type OpenInterval A B = { x:Float | InOpenInterval A B x } @-}

These aliases can then be used to prove, for instance, that an implementation of an affine transformation, fromUnitInterval below, from the open unit interval to an arbitrary interval is a bijection. The proof proceeds by supplying an inverse function (toUnitInterval) and specifying¹ that their composition is the identity. The example shows one half on the proof; the other half is straightforward and left to the reader.

type Bound = Float

{-@ inline fromUnitInterval @-}
{-@ fromUnitInterval :: a : Bound
                     -> { b : Bound | a != b }
                     -> x : OpenInterval 0 1
                     -> v : OpenInterval a b @-}
fromUnitInterval :: Bound -> Bound -> Float -> Float
fromUnitInterval a b x = a + x * (b - a)

{-@ inline toUnitInterval @-}
{-@ toUnitInterval :: a : Bound
                   -> { b : Bound | a != b }
                   -> x : OpenInterval a b
                   -> v : OpenInterval 0 1 @-}
toUnitInterval :: Bound -> Bound -> Float -> Float
toUnitInterval a b x = (x - a) / (b - a)

{-@ intervalId :: a : Bound
                   -> { b : Bound | a != b }
                   -> x : OpenInterval a b
                   -> {v : OpenInterval a b | x = v} @-}
intervalId :: Bound -> Bound -> Float -> Float
intervalId a b x = fromUnitInterval a b . toUnitInterval a b

Another case: refining a Map type to a fixed length allows us to enforce that a function can only grant access privileges to a bounded number of users at any call site.

type Password = String
type Name = String

{-@ type FixedMap a b N = { m : Map a b | len m = N } @-}

{-@ giveAccess :: Name
               -> Password
               -> FixedMap Name Password 3
               -> Bool @-}
giveAccess :: Name -> Password -> Map Name Password -> Bool
giveAccess name psswd users =
  Map.lookup name users == Just psswd

None of these specifications strictly require aliases, but they illustrate the practical convenience they bring.

A crowded name space

When we try to be simple and reasonable about such aliases, it becomes quite likely for other people to converge on the same names to describe similar types. Even a seemingly standard type such as Nat is not safe: someone with a historically informed opinion might want to define it as strictly positive numbers², or may just prefer to refine Word8 instead of Int.

Naturally, this is the familiar problem of name scope, for which established solutions exist, such as modules and local scopes. Yet for LH and its Nat, it was the case that one would have to either invent a non-conflicting name, exclude assumptions for the base package, or avoid importing the Prelude altogether. It might be argued that having to invent alternative names is a minor nuisance, but also that it can quickly lead to unwieldy and convoluted naming conventions once multiple dependencies expose their own specifications.

Simply stated, the problem was that LH imported all aliases from transitive dependencies into a flat namespace. After my contribution, LH still accumulates aliases transitively, but users gain two key capabilities: (i) to disambiguate occurrences by qualifying an identifier, and (ii) to overwrite an imported alias without conflict. In practice, this prevents spurious verification failures and gives the user explicit means to resolve clashes when they matter.

Consider the following scenario. Module A defines alias Foo. Two other modules, B and B', both define an alias Bar and import A.

module A where
{-@ type Foo = { ... } @-}

module B where
import A
{-@ type Bar = { ... } @-}

module B' where
import A
{-@ type Bar = { ... } @-}

A module C that imports B and B' will now see Foo in scope unambiguously, while any occurrence of Bar must be qualified in the usual Haskell manner.

module C where

import B
import B'

{-@ baz :: Foo -> B.Bar @-}
baz _ = undefined

Previously, this would have caused C to fail verification with a conflicting definitions error, even if Bar was never used.

examples/B.hs:3:10: error:
    Multiple definitions of Type Alias `Bar`
    Conflicting definitions at
    .
    * examples/B.hs:3:10-39
    .
    * examples/B'.hs:3:10-39
  |
3 | {-@ type Bar = { ... } @-}
  |          ^^^^^^^^^^^^^^

This error is now only triggered when the alias is defined multiple times within the same module. And instead, when an ambiguous type alias is found, the user is prompted to choose among the matching names in scope and directed to the offending symbol.

examples/C.hs:6:19: error:
    Ambiguous specification symbol `Bar` for type alias
    Could refer to any of the names
    .
    * Bar imported from module B defined at examples/B.hs:3:10-39
    .
    * Bar imported from module B' defined at examples/B'.hs:3:10-39
  |
6 | {-@ baz :: Foo -> Bar @-}
  |                   ^^^

The precise behavior is summarized in a set of explicit rules that I proposed, which specify how aliases are imported and exported under this scheme.

The initial name resolution flow

The project goals were initially put forward on a GitHub issue as a spin-off from a recent refactoring of the codebase that changed the internal representation of names to a structured LHName type that distinguishes between resolved and unresolved names and stores information about where the name originates, so that names are resolved only once for each compiled module.

Name resolution has many moving parts, but in broad terms its implementation is divided into two phases: The first handles names corresponding to entities GHC knows of—data and type constructors, functions, and annotation binders of aliases, measures, and data constructors—and uses its global reader environment to look them up. The resolution of logical entities (i.e. those found in logical expressions) is left for the second phase, where the names resolved during the first phase are used to build custom lookup environments.

Occurrences of type and predicate aliases were resolved by looking them up in an environment indexed by their unqualified name. When two or more dependencies (possibly transitive) defined the same alias, resolution defaulted to whichever definition happened to be encountered first during collection. This accidental choice was effectively irrelevant, however, since a later duplicate-name check would short-circuit with the aforementioned error. Locally defined aliases were recorded in the module’s interface file after verification, and LH assembled the resolution environment by accumulating the aliases from the interface files of all transitive dependencies.

The reason a module import brings all aliases from transitive dependencies into scope is that no mechanism exists to declare which aliases a module exports or imports. Implementing such a mechanism exceeded the project’s allocated time, so a trade-off was called for. On the importing side, Haskell’s qualifying directives could be applied, but an explicit defaulting mechanism was needed to determine what aliases a module exposes. This left us with at least three possibilities:

1. Export no aliases, so that they would be local to each module alone. This no-op solution would allow the user to use any names she wants, but quickly becomes inconvenient as an alias would have to be redefined in each module she intends to use it.
2. Export only those locally defined, so that only aliases from direct dependencies would be in scope for any given module. This could leave out aliases used to specify re-exported functions, so we would end up in a similar situation as before.
3. Export all aliases from transitive dependencies, avoiding the need to ever duplicate an alias definition.

The chosen option (3) reflects the former behavior and, complemented by the ability qualify and overwrite aliases, it was deemed the most effective solution.

Qualifying type aliases

Type aliases are resolved during the first phase, essentially because they are parsed as type constructors, which are resolved uniformly across the input specification. Two changes had to be made to qualify them: include module import information in the resolution environment to discern which module aliases can be used to qualify an imported type alias, and make sure transitively imported aliases are stored in the interface file along with the locally defined type aliases.

Careful examination of the code revealed that we could reuse environments built for other features of LH that could be qualified already! And as a bonus, their lookup function returns close-match alternatives in case of failure. Factoring this out almost did the trick. In addition, I had to add some provisions to give precedence to locally defined aliases during lookups.

Qualifying predicate aliases

Two aspects of the code made predicate aliases somewhat hard to reason about. First, predicate aliases are conflated in environments with Haskell entities lifted by inline and define annotations. The rationale is to use a single mechanism to expand these definitions in logical expressions.

Second, the conflated environments were redundantly gathered twice with different purposes: to resolve Haskell function names in logical expressions, and afterwards again to resolve occurrences of predicate aliases.

Both were not straightforward to deduce from the code. These facts, together with some code comments from the past about predicate aliases being the last names that remained “unhandled”, pointed the way.

The surgical change, then, was to sieve out predicate aliases from the lifted Haskell functions as they were stored together in interface files, and include these predicate aliases in the environment used to resolve qualified names for other features.

Alias expansion

Although the problem I set out to solve was primarily about name resolution, the implementation also required revisiting another process: alias expansion. For a specification to be ready for constraint generation, all aliases must be fully expanded (or unfolded), since liquid-fixpoint³ has no notion of aliases.

Uncovering this detail was crucial to advance with the implementation. It clarified why Haskell functions lifted with inline or define are eventually converted into predicate aliases: doing so allows for every aliasing annotation to be expanded consistently in a single pass wherever they appear in a specification. With qualified aliases, the expansion mechanism needed some adjustments, as the alias names were now more structured (LHName).

An additional complication was that the logic to expand type aliases was shared with predicate aliases, and since I did qualification of type aliases first, I needed to have different behavior for type and predicate aliases. In the end, I opted for duplicating the expansion logic for each case during the transition, and unified it again after implementing qualification of predicate aliases.

Closing remarks

My determination to understand implementation details was rewarded by insights that allowed me to refactor my way to a solution. For perspective, my contribution consisted of a 210 LOC addition for the feature implementation alone, after familiarizing myself with 2,150 LOC out of the 25,000 LOC making up the LH plugin. The bulk of this work is contained in two merged PRs (#2550 and #2566), which include detailed source documentation and tests.

The qualified aliases support and the explicit rules that govern it are a modest addition, but hopefully one of a positive impact on user experience. LH tries to be as close as possible to Haskell, but refinement type aliases still mark the boundary between both worlds. Perhaps the need for an ad hoc mechanism for importing and exporting logic entities will be revised in a horizon where LH gets integrated into GHC (which sounds good to me!).

This project taught me about many language features and introduced me to the GHC API; knowledge I will apply in future projects and to further contribute to the Haskell ecosystem. I am grateful to Facundo Domínguez for his generous and insightful mentoring, which kept on a creative flow throughout the project. Working on Liquid Haskell was lots of fun!