Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users’ burden of proof. However, this reliance on SMT does not come without a price: convincing the Liquid Haskell typechecker that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell’s inner workings.

In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tactic-inspired DSL interface for more concise and user-friendly proofs, and we demonstrate the framework’s capabilities by automating a wide variety of proofs from an existing Liquid Haskell benchmark.