Options and Pragmas¶
LiquidHaskell supports several configuration options, to alter the type checking.
You can pass options in different ways:
-
As a pragma, directly added to the source file: (recommended)
{-@ LIQUID "opt1" @-}
-
As a plugin option:
ghc-options: -fplugin-opt=LiquidHaskell:--opt1 -fplugin-opt=LiquidHaskell:--opt2
-
In the environment variable
LIQUIDHASKELL_OPTS
(e.g. in your.bashrc
orMakefile
):LIQUIDHASKELL_OPTS="--opt1 --opt2"
-
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
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 a
s, 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 filefoo.hs.html
with the annotations. The coloring is done usinghscolour
. -
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 havepandoc
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.