LiquidHaskell

2026-09-27 · 8 min

LiquidHaskell attaches a logical predicate to a type and checks it with an SMTsolver instead of Haskell's own type checker. This builds up from a division that cannot be called with a zero denominator to a red-black tree whose balance invariant is checked at compile time, reading the failures along the way.

§ 01

Setup

Install via cabal, or as a GHC plugin dependency.

$ cabal install liquidhaskell

Run it against a file directly.

$ liquidhaskell src/Safe.hs

Or wire it in as a GHC plugin, so liquid checking runs as part of an ordinary build. This is the way to actually use it in a project.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module Safe where

In the .cabal file, so cabal build and cabal test both check refinements.

build-depends: liquidhaskell
ghc-options: -fplugin=LiquidHaskell

§ 02

The first refinement

A refinement type is a base type plus a predicate in braces, read as the set of values of that type satisfying the predicate. v is the bound variable, standing for the value itself.

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

Refine a function's argument. The {-@ ... @-} pragma is a specially-formatted comment; GHC ignores it and LiquidHaskell reads it.

{-@ divide :: Int -> {v:Int | v /= 0} -> Int @-}
divide :: Int -> Int -> Int
divide x y = x `div` y

A call that violates the refinement is a compile-time error, not a runtime exception. This is the whole value proposition in one example.

bad :: Int
bad = divide 10 0

What LiquidHaskell reports. It is not a vague type mismatch: it names the exact obligation that could not be proved.

Safe.hs:12:14: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {VV : GHC.Types.Int | VV == 0}
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV /= 0}

A call built from an unknown value is rejected too, because nothing in scope proves it nonzero.

risky :: Int -> Int
risky n = divide 10 n   -- rejected: n could be 0

Guard it, and the guard becomes a fact LiquidHaskell can use. This is flow-sensitive: inside the branch, n /= 0 is known.

safe :: Int -> Int
safe n
  | n /= 0    = divide 10 n
  | otherwise = 0

§ 03

Function contracts

A refinement on the result, not just the arguments. abs must return a Nat regardless of what Int comes in.

{-@ absR :: Int -> {v:Int | v >= 0} @-}
absR :: Int -> Int
absR x = if x < 0 then -x else x

Refining in terms of the arguments, not just a fixed set. The result must be at least as large as x.

{-@ addPos :: x:Int -> {v:Int | v > 0} -> {v:Int | v > x} @-}
addPos :: Int -> Int -> Int
addPos x y = x + y

Dependent contracts: division that requires the numerator be a multiple of the denominator, and proves the quotient exactly.

{-@ exactDiv :: n:Int -> {d:Int | d /= 0 && n mod d == 0}
             -> {v:Int | v * d == n} @-}
exactDiv :: Int -> Int -> Int
exactDiv n d = n `div` d

A precondition that the code itself does not need to check. liquidAssert lets a proof obligation appear inline; it disappears from the compiled program once checked.

import Language.Haskell.Liquid.Prelude (liquidAssert)
 
headSafe :: [a] -> a
headSafe (x:_) = x
headSafe []    = liquidAssert False (error "impossible")

§ 04

Refining lists and vectors

A refined type alias for non-empty lists. len is a built-in measure LiquidHaskell already knows about [a].

{-@ type NEList a = {v:[a] | len v > 0} @-}
 
{-@ headR :: NEList a -> a @-}
headR :: [a] -> a
headR (x:_) = x

Calling it with a literal that is provably non-empty typechecks. Calling it with [] is a compile error, because len [] == 0 is a fact LiquidHaskell derives from the definition of len, not from your code.

>>> headR [1, 2, 3]   -- ok, len [1,2,3] == 3
>>> headR []          -- rejected

A length-indexed refinement on zip, ruling out the silent truncation that Haskell's own zip performs on mismatched lists.

{-@ safeZip :: xs:[a] -> {ys:[b] | len ys == len xs} -> [(a, b)] @-}
safeZip :: [a] -> [b] -> [(a, b)]
safeZip [] []         = []
safeZip (x:xs) (y:ys) = (x, y) : safeZip xs ys
safeZip _ _           = []   -- unreachable, given the refinement

Index safety: a bounded Int and a total lookup, checked instead of trusted.

{-@ type Idx Xs = {v:Int | 0 <= v && v < len Xs} @-}
 
{-@ at :: xs:[a] -> Idx xs -> a @-}
at :: [a] -> Int -> a
at (x:_)  0 = x
at (_:xs) n = at xs (n - 1)
at []     _ = error "unreachable"

§ 05

Custom measures

A measure is a Haskell function LiquidHaskell also understands logically, letting refinements talk about a type's structure rather than only its length.

{-@ measure size @-}
size :: Tree a -> Int
size Leaf         = 0
size (Node l _ r) = 1 + size l + size r
 
data Tree a = Leaf | Node (Tree a) a (Tree a)

Refine a smart constructor with it. This says: whatever insert returns has one more element than what went in.

{-@ insert :: x:a -> t:Tree a -> {v:Tree a | size v == size t + 1} @-}
insert :: Ord a => a -> Tree a -> Tree a
insert x Leaf = Node Leaf x Leaf
insert x t@(Node l y r)
  | x < y     = Node (insert x l) y r
  | x > y     = Node l y (insert x r)
  | otherwise = t   -- rejected: size unchanged on the duplicate branch

The duplicate branch really is rejected, and the fix is to write the refinement you actually meant.

{-@ insert :: x:a -> t:Tree a
           -> {v:Tree a | size v == size t || size v == size t + 1} @-}

A measure returning a Bool, used to refine membership. This is how sortedness gets checked structurally instead of by an external property test.

{-@ measure isSorted @-}
isSorted :: [Int] -> Bool
isSorted []       = True
isSorted [_]      = True
isSorted (x:y:xs) = x <= y && isSorted (y:xs)
 
{-@ type Sorted = {v:[Int] | isSorted v} @-}
 
{-@ insertSorted :: Int -> Sorted -> Sorted @-}
insertSorted :: Int -> [Int] -> [Int]
insertSorted x []     = [x]
insertSorted x (y:ys)
  | x <= y    = x : y : ys
  | otherwise = y : insertSorted x ys

§ 06

Refining your own data types

A field-level refinement on a record, checked at every construction site, not just at smart constructors you remember to write.

{-@ data Account = Account
      { balance :: {v:Int | v >= 0}
      , owner   :: String
      } @-}
data Account = Account { balance :: Int, owner :: String }

Every construction is checked against it, including ones far from any function you refined by hand.

ok  = Account { balance = 100, owner = "ada" }
bad = Account { balance = -5,  owner = "ada" }   -- rejected

A refined ADT: the balanced-height invariant of a red-black tree, carried in the type itself rather than checked afterward.

data Color = R | B
 
{-@ data RBTree a = Leaf
                  | Node { c :: Color
                         , l :: RBTreeL a c
                         , v :: a
                         , r :: {t:RBTreeL a c | bheight t == bheight l}
                         } @-}
data RBTree a = Leaf | Node Color (RBTree a) a (RBTree a)
 
{-@ measure bheight @-}
bheight :: RBTree a -> Int
bheight Leaf           = 0
bheight (Node B l _ _) = 1 + bheight l
bheight (Node R l _ _) = bheight l

With that in place, an insert whose rebalancing case forgets to restore the invariant fails to typecheck at the call site that breaks it, rather than corrupting the tree at runtime.

RBTree.hs:41:5: error:
    Liquid Type Mismatch
    The inferred type
      bheight (l') == bheight (l) + 1
    is not a subtype of the required type
      bheight (l') == bheight (r)

§ 07

Termination

LiquidHaskell checks termination by default on recursive functions, by looking for a decreasing argument. A structural recursion like this one is accepted with no annotation.

sumList :: [Int] -> Int
sumList []     = 0
sumList (x:xs) = x + sumList xs   -- xs is structurally smaller

Recursion that is not on a direct subterm needs a decreasing measure named explicitly, so the checker knows what to look at.

{-@ gcdR :: a:Nat -> {b:Nat | b < a} -> Nat / [a] @-}
gcdR :: Int -> Int -> Int
gcdR a 0 = a
gcdR a b = gcdR b (a `mod` b)

Mark a function as not needing the check, for intentionally non-terminating code such as a server loop. This opts out rather than proving anything.

{-@ lazy serverLoop @-}

Ackermann, which needs two arguments in the decreasing measure because neither one alone strictly decreases on every call.

{-@ ackermann :: m:Nat -> n:Nat -> Nat / [m, n] @-}
ackermann :: Int -> Int -> Int
ackermann 0 n = n + 1
ackermann m 0 = ackermann (m - 1) 1
ackermann m n = ackermann (m - 1) (ackermann m (n - 1))

§ 08

Totality

A pattern match LiquidHaskell can prove is exhaustive over the refined domain is accepted, even though GHC's own -Wincomplete-patterns would flag it, because GHC does not see the refinement that rules out the missing case.

{-@ sign :: {v:Int | v /= 0} -> {v:Int | v == 1 || v == -1} @-}
sign :: Int -> Int
sign n
  | n > 0 = 1
  | n < 0 = -1

Remove the refinement and the same function is correctly rejected: without v /= 0, the case n == 0 is unhandled, and now nothing rules it out.

sign :: Int -> Int
sign n
  | n > 0 = 1
  | n < 0 = -1
  -- rejected: n == 0 is reachable and unhandled

§ 09

Proving properties as functions

A proof is a function whose refined type is the theorem and whose body is the derivation. Bool-valued proof terms are the simplest form.

{-@ type Proof = () @-}
 
{-@ addComm :: x:Int -> y:Int -> {x + y == y + x} @-}
addComm :: Int -> Int -> Proof
addComm _ _ = ()   -- discharged entirely by the SMT solver

A property that needs induction: the SMT solver has no notion of a proof by induction on its own, so the recursive structure of the proof function supplies it.

{-@ sumApp :: xs:[Int] -> ys:[Int]
           -> {sum (xs ++ ys) == sum xs + sum ys} @-}
sumApp :: [Int] -> [Int] -> Proof
sumApp []     ys = ()
sumApp (x:xs) ys = sumApp xs ys   -- appeals to the induction hypothesis

Explicit equational reasoning, imported from the proof combinator library, for a chain a reviewer can read step by step rather than trusting a one-line ().

import Language.Haskell.Liquid.ProofCombinators
 
{-@ doubleAdd :: x:Int -> {2 * x == x + x} @-}
doubleAdd :: Int -> Proof
doubleAdd x
  =   2 * x
  === x + x
  *** QED

§ 10

Reading a failure

Run with the flag that keeps the intermediate SMT query, when a message alone is not enough to see why the solver failed.

$ liquidhaskell --keep-quals --save src/Safe.hs

The structure of every error: an inferred type on the left, a required type on the right, and the counterexample is the gap between them.

Safe.hs:23:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {VV : Int | VV == x - 1}
    is not a subtype of the required type
      VV : {VV : Int | VV >= 0}
    .
    In Context
      x : {x : Int | x >= 0}

Read that as: x could be 0, so x - 1 could be -1, which is not >= 0. The fix is either a precondition ruling out x == 0, or handling it as its own case.

{-@ predR :: {x:Int | x > 0} -> Nat @-}
predR :: Int -> Int
predR x = x - 1

A common false failure: LiquidHaskell not knowing a fact that is true but outside what it tracks by default. Nudge it with an explicit assumption.

{-@ assume sqrtNonNeg :: x:Double -> {v:Double | v >= 0} @-}
sqrtNonNeg :: Double -> Double
sqrtNonNeg = sqrt

assume takes the obligation on faith rather than proving it. It is the escape hatch, and every use of it is a place where the guarantee is now only as good as the comment next to it.

-- correct here: sqrt really is non-negative for real inputs,
-- but LiquidHaskell has no model of the Prelude sqrt implementation

The shape of working with it: refine one function at a time, starting from the argument that actually causes the bug you are worried about; when a check fails, read the inferred-versus-required pair as the counterexample it is rather than a generic type error; reach for a measure once a plain len stops being enough to state the property; and treat every assume as a debt, since it is the one place the tool will believe you without checking. Refinement types and deriving sit at opposite ends of the same spectrum: one adds proof obligations by hand, the other generates an instance without any.

← older

A Work-Stealing Scheduler in OCaml

2026-09-26