Options and Pragmas

LiquidHaskell supports several configuration options, to alter the type checking.

You can pass options in different ways:

1. As a pragma, directly added to the source file: (recommended)

   {-@ LIQUID "opt1" @-}
   

2. As a plugin option:

   ghc-options: -fplugin-opt=LiquidHaskell:--opt1 -fplugin-opt=LiquidHaskell:--opt2
   

3. In the environment variable LIQUIDHASKELL_OPTS (e.g. in your .bashrc or Makefile):

   LIQUIDHASKELL_OPTS="--opt1 --opt2"
   

4. From the command line, if you use the legacy executable:

   liquid --opt1 --opt2 ...
   

The options are descibed below (and by the legacy executable: liquid --help)

Theorem Proving

Options: reflection, ple, ple-local, extensionality, ple-with-undecided-guards

Directives: automatic-instances

To enable theorem proving, e.g. as described here use the option

    {-@ LIQUID "--reflection" @-}

To additionally turn on proof by logical evaluation (PLE) use the option

    {-@ LIQUID "--ple" @-}

You can see many examples of proofs by logical evaluation in tests/benchmarks/popl18/ple/pos

This flag is global and will symbolically evaluate all the terms that appear in the specifications.

As an alternative, the --ple-local flag has local behavior. See

{-@ LIQUID "--ple-local" @-}

will only evaluate terms appearing in the specifications of the function theorem, if the function theorem is annotated for automatic instantiation using the following liquid annotation

{-@ automatic-instances theorem @-}

Normally, PLE will only unfold invocations only if the arguments are known with enough precision to enter some of the equations of the function. For instance, in

{-@ reflect boolToInt @-}
boolToInt :: Bool -> Int
boolToInt False = 0
boolToInt True = 1

{-@ nonNegativeInt :: b:_ -> { boolToInt b >= 0 } @-}
nonNegativeInt :: Bool -> ()
nonNegativeInt _ = ()

the equations boolToInt False = 0 and boolToInt True = 1 would only be used if b is known to be either True or False. Now, if nothing is known about b and we still would like to use the fact that

boolToInt b = if b then 1 else 0

we can instruct Liquid Haskell to do so and accept nonNegativeInt with

{-@ LIQUID "--ple-with-undecided-guards" @-}

--ple-with-undecided-guards causes all invocations that haven't been unfolded due to undecided guards to be unfolded at the end of the algorithm. Alternatively, one could selectively unfold the invocations of some particular function only with Language.Haskell.Liquid.ProofCombinators.pleUnfold.

boolToInt b = pleUnfold (if b then 1 else 0)

Now, PLE will unfold boolToInt as above every time b is undecided. But won't unfold any other invocations with undecided guards unless they also start with an application of pleUnfold.

To allow reasoning about function extensionality use the --extensionality flag. See test T1577.

{-@ LIQUID "--extensionality" @-}

Fast Checking

Options: fast, nopolyinfer

The option --fast or --nopolyinfer greatly recudes verification time, can also reduces precision of type checking. It, per module, deactivates inference of refinements during instantiation of polymorphic type variables. It is suggested to use on theorem proving style when reflected functions are trivially refined.

Incremental Checking

Options: diff

The LiquidHaskell executable supports incremental checking where each run only checks the part of the program that has been modified since the previous run. Each run of liquid saves the file to a .bak file and the subsequent run does a diff to see what has changed w.r.t. the .bak file only generates constraints for the [CoreBind] corresponding to the changed top-level binders and their transitive dependencies.

The time savings are quite significant. For example:

    $ time liquid --notermination -i . Data/ByteString.hs > log 2>&1

    real    7m3.179s
    user    4m18.628s
    sys     0m21.549s

Now if you go and tweak the definition of spanEnd on line 1192 and re-run:

    $ time liquid --diff --notermination -i . Data/ByteString.hs > log 2>&1

    real    0m11.584s
    user    0m6.008s
    sys     0m0.696s

The diff is only performed against code, i.e. if you only change specifications, qualifiers, measures, etc. liquid -d will not perform any checks. In this case, you may specify individual definitions to verify:

    $ liquid -b bar -b baz foo.hs

This will verify bar and baz, as well as any functions they use.

If you always want to run a given file with diff-checking, add the pragma:

{-@ LIQUID "--diff" @-}

Full Checking (DEFAULT)

Options: full

You can force LiquidHaskell to check the whole file (which is the DEFAULT) using the --full option. This will override any other --diff incantation elsewhere (e.g. inside the file). If you always want to run a given file with full-checking, add the pragma:

{-@ LIQUID "--full" @-}

Specifying Different SMT Solvers

Options: smtsolver

By default, LiquidHaskell uses the SMTLIB2 interface for Z3.

To run a different solver (supporting SMTLIB2) do:

$ liquid --smtsolver=NAME foo.hs

Currently, LiquidHaskell supports

• CVC4
• MathSat

To use these solvers, you must install the corresponding binaries from the above web-pages into your PATH.

Short Error Messages

Options: short-errors

By default, subtyping error messages will contain the inferred type, the expected type -- which is not a super-type, hence the error -- and a context containing relevant variables and their type to help you understand the error. If you don't want the above and instead, want only the source position of the error use --short-errors.

Short (Unqualified) Module Names

Options: short-names

By default, the inferred types will have fully qualified module names. To use unqualified names, much easier to read, use --short-names.

Disabling Checks on Functions

Directives: ignore

You can disable checking of a particular function (e.g. because it is unsafe, or somehow not currently outside the scope of LH) by using the ignore directive.

For example,

{-@ ignore foo @-}

will disable the checking of the code for the top-level binder foo.

See tests/pos/Ignores.hs for an example.

Totality Check

Options: no-totality

LiquidHaskell proves the absence of pattern match failures.

For example, the definition

fromJust :: Maybe a -> a
fromJust (Just a) = a

is not total and it will create an error message. If we exclude Nothing from its domain, for example using the following specification

{-@ fromJust :: {v:Maybe a | (isJust v)} -> a @-}

fromJust will be safe.

Use the no-totality flag to disable totality checking.

Termination Check

Options: no-termination

By default a termination check is performed on all recursive functions, but you can disable the check with the --no-termination option.

See the specifications section for how to write termination specifications.

Positivity Check

Options: no-positivity-check By default a positivity check is performed on data definitions.

data Bad = Bad (Bad -> Bad) | Good Bad 
    --           A      B           C
    -- A is in a negative position, B and C are OK

Negative declarations are rejected because they admit non-terminating functions.

If the positivity check is disabled, so that a similar declaration of Bad is allowed, it is possible to construct a term of the empty type, even without recursion. For example see tests/neg/Positivity1.hs and tests/neg/Positivity2.hs

data Evil a = Very (Evil a -> a)

{-@ type Bot = {v: () | false} @-}

{-@ bad :: Evil Bot -> Bot @-}
bad :: Evil () -> ()
bad (Very f) = f (Very f)

{-@ worse :: Bot @-}
worse :: ()
worse = bad (Very bad)

Note that all positive occurrences are permited, unlike Coq that only allows the strictly positive ones (see: https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/)

Total Haskell

Options: total-Haskell

LiquidHaskell provides a total Haskell flag that checks both totallity and termination of the program, overriding a potential no-termination flag.

Lazy Variables

A variable can be specified as LAZYVAR

{-@ LAZYVAR z @-}

With this annotation the definition of z will be checked at the points where it is used. For example, with the above annotation the following code is SAFE:

foo   = if x > 0 then z else x
  where
    z = 42 `safeDiv` x
    x = choose 0

By default, all the variables starting with fail are marked as LAZY, to defer failing checks at the point where these variables are used.

No measure fields

Options: no-measure-fields

When a data type is refined, Liquid Haskell automatically turns the data constructor fields into measures. For example,

{-@ data L a = N | C {hd :: a, tl :: L a} @-}

will automatically create two measures hd and td. To deactivate this automatic measure definition, and speed up verification, you can use the --no-measure-fields flag.

Prune Unsorted Predicates

Options: prune-unsorted

The --prune-unsorted flag is needed when using measures over specialized instances of ADTs.

For example, consider a measure over lists of integers

sum :: [Int] -> Int
sum [] = 0
sum (x:xs) = 1 + sum xs

This measure will translate into strengthening the types of list constructors

[] :: {v:[Int] | sum v = 0 }
(:) :: x:Int -> xs:[Int] -> {v:[Int] | sum v = x + sum xs}

But what if our list is polymorphic [a] and later instantiate to list of ints? The workaround we have right now is to strengthen the polymorphic list with the sum information

[] :: {v:[a] | sum v = 0 }
(:) :: x:a -> xs:[a] -> {v:[a] | sum v = x + sum xs}

But for non numeric as, refinements like x + sum xs are ill-sorted!

We use the flag --prune-unsorted to prune away unsorted expressions (like x + sum xs) inside refinements.

Case Expansion

Options: no-case-expand

By default LiquidHaskell expands all data constructors to the case statements. For example, given the definition

data F = A1 | A2 | .. | A10

LiquidHaskell will expand the code

case f of {A1 -> True; _ -> False}

to

case f of {A1 -> True; A2 -> False; ...; A10 -> False}

This expansion can lead to more precise code analysis but it can get really expensive due to code explosion. The --no-case-expand flag prevents this expansion and keeps the user provided cases for the case expression.

Higher order logic

Options: higherorder

The flag --higherorder allows reasoning about higher order functions.

Restriction to Linear Arithmetic

Options: linear

When using z3 as the solver, LiquidHaskell allows for non-linear arithmetic: division and multiplication on integers are interpreted by z3. To treat division and multiplication as uninterpreted functions use the --linear flag.

Counter examples

Options: counter-examples

Status: experimental

When given the --counter-examples flag, LiquidHaskell will attempt to produce counter-examples for the type errors it discovers. For example, see tests/neg/ListElem.hs

% liquid --counter-examples tests/neg/ListElem.hs

...

tests/neg/ListElem.hs:12:1-8: Error: Liquid Type Mismatch

 12 | listElem _ []      = False
      ^^^^^^^^

   Inferred type
     VV : {VV : Bool | VV == True}
     VV = True

   not a subtype of Required type
     VV : {VV : Bool | Prop VV <=> Set_mem ?b (listElts ?a)}

   In Context
     ?a : {?a : [a] | len ?a >= 0}
     ?a = [1]

     ?b : a
     ?b = 0

The --counter-examples flag requires that each type in the context be an instance of GHC.Generics.Generic or Test.Targetable.Targetable (provided as part of LiquidHaskell). LiquidHaskell cannot generate counter-examples for polymorphic types, but will try (naively) to instantiate type variables with Int (as seen in the example above).

Typeclasses

Options: typeclass

Status: experimental

The --typeclass flag enables LiquidHaskell's support of typeclasses. One limitation is that proofs cannot be written directly within the instance definition unless the --aux-inline flag is turned on as well.

Generating HTML Output

The system produces HTML files with colorized source, and mouseover inferred type annotations, which are quite handy for debugging failed verification attempts.

• Regular Haskell When you run: liquid foo.hs you get a file foo.hs.html with the annotations. The coloring is done using hscolour.

• Markdown + Literate Haskell You can also feed in literate haskell files where the comments are in Pandoc markdown. In this case, the tool will run pandoc to generate the HTML from the comments. Of course, this requires that you have pandoc installed as a binary on your system. If not, hscolour is used to render the HTML.

It is also possible to generate slide shows from the above. See the slides directory for an example.

Loading specifications automatically

By default, Liquid Haskell will load the specifications from module A.B.C_LHAssumptions whenever it finds an import of module A.B.C. For instance,

import Data.Vector
import Data.Vector.Unboxed

would cause Liquid Haskell to try modules Data.Vector_LHAssumptions and Data.Vector.Unboxed_LHAssumptions. If the _LHAssumptions module is missing, vecrification proceeds without any extra specifications.

A.B.C_LHAssumptions is looked in any package that is visible to GHC when verifying a module. But the following flag can be used to stop this automatic loading when the imported module belongs to the given package.

Options: --exclude-automatic-assumptions-for=PACKAGE

Liquid Haskell will not load _LHAssumptions modules upon finding an import of a module coming from package PACKAGE. e.g. --exclude-automatic-assumptions-for=vector would stop loading _LHAssumptions modules for any imports coming from package vector.