State of Liquid Haskell development

[chrisdone-artificial]

Some questions and observations:

1. I've found that the (default) develop branch of liquidhaskell doesn't build with stack. It's got duplicate entries for containers in the extra-deps. Is nobody using the stack config anymore? Are you developing it against bleeding edge Hackage unpinned?
2. Are we expected always to use the latest Liquid Haskell? I found that a few features documented in the docs just don't match, so I'm attempting to install from GitHub, hence the bullet point above.
3. Is there any work going on to make the parser more user-friendly?
4. Features like abstract refinements don't seem to be documented anywhere. There's a link to two papers ([abstract_refinement_types.pdf](https://ranjitjhala.github.io/static/abstract_refinement_types.pdf)) and [1507.00385v1.pdf](https://arxiv.org/pdf/1507.00385). The <{\x y z -> bool}> syntax appears quite mysterious - there are only a few examples, and I appear to be able to write whatever I want as variable names and they don't do anything (on 0.9.8.2). Perhaps it was a bleeding edge feature, but e.g. \x _ _ _ _ _ _ -> true is accepted, and \x y z -> x == x is accepted, but \x y -> x == y says x is not in scope. In other words it appears completely arbitrary as a user. Maybe I can achieve what I want, maybe I can't. Is there a proper doc somewhere on what's intended vs what's implemented?
5. Meta comment but not important: as LH is niche but also changes fairly often, GenAI is on 95% hallucination mode (it seems to think LH can't deal with unboxed types, but I tested it and it was fine with it).
   • I had some code from 9 years ago where I tried out liquid haskell, and quite a lot of the code no longer parsed or didn't resolve for various reasons.

I suppose I'm having a moan too, as I've been reading through the tutorial again and expected that it would have matured, but it still feels as rough around the edges as a decade ago.

Some basic ergonomics like Foo x:Int vs Foo (x:Int) -- seem to mean different things (not sure whether that's intentional or accidental), and Foo x:(Set Int) is needed for types with params, but you can't write {x:Set Int} as a convenience. Writing Foo x () <{\(x) -> ...}> yields a parse error about () rather than (x), which indicates the parser is still using too many try calls and this shows in the errors.

Stepping back for a more high-level view: For industrial use, it feels like one would have to have a lot of time to go back and forth with the maintainers. That's not a criticism, I'm trying to gauge the reality of where maintenance is at. Is it just a few of you (@ranjitjhala, @facundominguez, etc.) working on it in free time?

I wish I had more time to dabble, because on paper LH is amazing. But the dev experience and learning experience is rough, which I'm sorry about. I'm not sure when I'll get another block of time in which I can dabble with it.

---

Reduced simple example of the above on master:

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

module LH2 where

import Data.Set (Set)
import Data.Functor.Identity

{-@ newtype M i o a <p :: i -> o -> Bool> = M (Identity a) @-}
newtype M i o a = M (Identity a)

{-@ assume foo :: M (Set Int) (Set Int) () <{\x y -> x == y}> @-}
foo :: M (Set Int) (Set Int) ()
foo = M (pure ())

/home/chris/Work/chrisdone/liquidhaskell/LH2.hs:11:19: error:
    Illegal type specification for `LH2.foo`
    LH2.foo :: (LH2.M (Data.Set.Internal.Set GHC.Types.Int) (Data.Set.Internal.Set GHC.Types.Int) {VV : () | x##3 == VV})
    Sort Error in Refinement: {VV : Tuple0 | x##3 == VV}
    Unbound symbol x##3 --- perhaps you meant: VV, papp3, head, tail ?
    Just assume
   |
11 | {-@ assume foo :: M (Set Int) (Set Int) () <{\x y -> x == y}> @-}
   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Failed, 151 modules reloaded.

stack.yaml file which appears to pass tests:

flags:
  liquidhaskell:
    devel: true
  tests:
    stack: true
extra-package-dbs: []
ghc-options:
  hscolour: -w
  liquidhaskell-boot: -j
  liquidhaskell: -j
packages:
- liquid-fixpoint
- liquid-prelude
- liquid-vector
- liquid-parallel
- liquidhaskell-boot
- tests
- .
extra-deps:
  - parallel-3.2.2.0@sha256:3df46ec247e12b5e406a0adb9577294431b24814b30df420551d176fd112a966,2038
resolver: nightly-2026-01-04

nix:
  packages: [cacert, git, hostname, nix, stack, z3]
  path: [nixpkgs=./nixpkgs.nix]

[chrisdone]

Apologies if my tone above comes off as the entitled open source user, having been on the receiving end of that, I know it’s not nice. I am not at all entitled to any of the work you’ve all done and kindly shared.

Suffice to say I had a complicated experience and my report about it is similarly complicated and time poor. On the other hand I have a touch point I can come back to in the future as a reference.

[facundominguez]

Hello @chrisdone 👋. Thanks for your report.

1. I've found that the (default) develop branch of liquidhaskell doesn't build with stack. It's got duplicate entries for containers in the extra-deps. Is nobody using the stack config anymore? Are you developing it against bleeding edge Hackage unpinned?

I know of no maintainer who is using stack at the moment. The stack config is abandoned because often liquidhaskell supports the latest version of GHC before there is a stack snapshot, and the development version of liquidhaskell only builds with one version of GHC.

2. Are we expected always to use the latest Liquid Haskell?

Not really. You could use an older version if you need to use an older compiler. But it is true that such arrangement is not possible if you also want to have the latest fixes.

3. Is there any work going on to make the parser more user-friendly?

Not to my knowledge. But proposals and patches to make it better are welcome.

4. Features like abstract refinements don't seem to be documented anywhere (...) Is there a proper doc somewhere on what's intended vs what's implemented?

I don't think so (cc @nikivazou).

5. Meta comment but not important: as LH is niche but also changes fairly often, GenAI is on 95% hallucination mode (it seems to think LH can't deal with unboxed types, but I tested it and it was fine with it). * I had some code from 9 years ago where I tried out liquid haskell, and quite a lot of the code no longer parsed or didn't resolve for various reasons.

Noted. Backward compatibility is not a priority at the moment, but provisions could be discussed eventually.

Reduced simple example of the above on master:

Thanks, that is worth analyzing to get less confusing behavior. I'm presuming a bug.

[facundominguez]

Is it just a few of you (@ranjitis it just a few of you (@ranjitjhala, @facundominguez, etc.) working on it in free time?

In my case, I've been spending some 10-15 hours weekly with the support of Tweag to investigate flaws, improve the implementation, and help contributors. I also got the assistance of interns and GSoC contributors to work on Liquid Haskell related projects.

There are sporadic academic contributions too, for which Niki and Ranjit do most of the coordination.

My assessment on Liquid Haskell is that any use at scale is still likely to require tuning of the implementation and the documentation for the particular purpose.

[facundominguez]

Reduced simple example of the above on master:

With the version from github, the following works for me. I guess this might work with older versions too.

-{-@ assume foo :: M (Set Int) (Set Int) () <{\x y -> x == y}> @-}
+{-@ assume foo :: (M (Set Int) (Set Int) ()) <{\x y -> x == y}> @-}

then

$ cabal exec ghc -- -fplugin=LiquidHaskell -XHaskell2010 LH.hs
[1 of 1] Compiling LH               ( LH.hs, LH.o )

**** LIQUID: SAFE (0 constraints checked) **************************************

There is still a confusing error message to fix. Isn't it? :)

[ranjitjhala]

Hi @chrisdone-artificial -- first off, many thanks for engaging and your many comments! (And apologies for the frustrating experience!)

For industrial use, it feels like one would have to have a lot of time to go back and forth with the maintainers. That's not a criticism, I'm trying to gauge the reality of where maintenance is at. Is it just a few of you (@ranjitjhala, @facundominguez, etc.) working on it in free time?

As you've noted, the main challenge with a lot of the "paper cuts" is indeed, that is mostly @facundominguez who has been doing the heroic lifting with a lot of the internals in the 10-15 hours from Tweag, whereas @nikivazou and I are contributing in "academic" mode where its been difficult to find the resources/time to address the many many paper cuts (case in point: finally got my head above water from the new classes I'm teaching this quarter to reply to this thread!) I think its a bit of a chicken-and-egg / flywheel problem: if we had some larger industrial use-cases / motivating problems, we could use them to drive fixing the paper cuts, which would perhaps then make it easier to get more people to use it!

Your list is an excellent place to start -- I have been putting off updating the tutorial forever, maybe I should start with that... and indeed, more documentation for abstract refinements... At any rate, any suggestions / advice would be most welcome!

• Ranjit.

[chrisdone]

Reduced simple example of the above on master:

With the version from github, the following works for me. I guess this might work with older versions too.

-{-@ assume foo :: M (Set Int) (Set Int) () <{\x y -> x == y}> @-}
+{-@ assume foo :: (M (Set Int) (Set Int) ()) <{\x y -> x == y}> @-}
then

$ cabal exec ghc -- -fplugin=LiquidHaskell -XHaskell2010 LH.hs
[1 of 1] Compiling LH               ( LH.hs, LH.o )

**** LIQUID: SAFE (0 constraints checked) **************************************

There is still a confusing error message to fix. Isn't it? :)

Oh, brilliant! I didn’t think of that, I was frankly unsure what I was writing was anywhere close to being accurate! Thank you. I’ll be able to have a fiddle around more. 🙏

[chrisdone]

Hi @chrisdone-artificial -- first off, many thanks for engaging and your many comments! (And apologies for the frustrating experience!)

For industrial use, it feels like one would have to have a lot of time to go back and forth with the maintainers. That's not a criticism, I'm trying to gauge the reality of where maintenance is at. Is it just a few of you (@ranjitjhala, @facundominguez, etc.) working on it in free time?

As you've noted, the main challenge with a lot of the "paper cuts" is indeed, that is mostly @facundominguez who has been doing the heroic lifting with a lot of the internals in the 10-15 hours from Tweag, whereas @nikivazou and I are contributing in "academic" mode where its been difficult to find the resources/time to address the many many paper cuts (case in point: finally got my head above water from the new classes I'm teaching this quarter to reply to this thread!) I think its a bit of a chicken-and-egg / flywheel problem: if we had some larger industrial use-cases / motivating problems, we could use them to drive fixing the paper cuts, which would perhaps then make it easier to get more people to use it!

Your list is an excellent place to start -- I have been putting off updating the tutorial forever, maybe I should start with that... and indeed, more documentation for abstract refinements... At any rate, any suggestions / advice would be most welcome!

• Ranjit.

Thanks @ranjitjhala — that adds more clarity. Indeed, I see the chicken and egg problem, and I appreciate that you’re all busy with academic responsibilities. 🙂 I’ll keep this problem in mind.

[facundominguez]

I'm retiring the stack configuration in #2616