LiquidHaskell and Cardano SL

LiquidHaskell Info

Version

Package liquidhaskell depends on ghc package. So we have to use liquidhaskell package with the same ghc version as we use in Cardano SL. Otherwise you'll get strange error with "wrong magic number" during liquid launching.

Thus, currently we're using Haskell LTS-9.1 with ghc-8.0.2, so we must install liquidhaskell-0.8.0.5, because it's the latest version of LiquidHaskell with ghc-8.0.2.

Install

First of all, install SMT solver for Liquid Refinement Types, for example z3.

After that:

$ cd
$ stack install liquidhaskell-0.8.0.5

GHC Little "Hack"

There's one strange linker error, with the final sentence recompile with -fPIC.

Open this file ~/.stack/programs/x86_64-linux/ghc-tinfo6-nopie-8.0.2/lib/ghc-8.0.2/settings and replace line:

("C compiler flags", "-fno-PIE -fno-stack-protector")

by line:

("C compiler flags", "-fPIC -fno-stack-protector")

The source is this question on StackOverflow.

Launch

Unfortunately, liquid cannot read our .cabal-files, so we have to pass required GHC-extensions directly:

~/cardano-sl $ stack exec -- liquid tools/src/cli-docs/Main.hs \
    --ghc-option=-XNoImplicitPrelude \
    --ghc-option=-XRecordWildCards \
    --ghc-option=-XGADTs \
    --ghc-option=-XOverloadedStrings \
    --ghc-option=-XApplicativeDo

Custom Prelude Notice

Since Cardano SL uses custom prelude Universum, it can be a reason of some strange errors. For example:

~/.stack/global-project/.stack-work/install/x86_64-linux-tinfo6-nopie/lts-9.13/8.0.2/share/x86_64-linux-ghc-8.0.2/liquidhaskell-0.8.0.5/include/GHC/List.spec:40:12: Error: GHC Error

 40 | splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (Min (len v) (len x) n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}>
                 ^

     Not in scope: variable or data constructor ` Min '

Universum doesn't include Min, so we have to provide custom Liquid-predicate for it. The simplest solution is to add this predicate in the module we want to check (in our example it's tools/src/cli-docs/Main.hs):

{-@ predicate Min V X Y = if X < Y then V = X else V = Y @-}

Of course, in real life we add such a predicate in separate Liquid.Spec-module.

Expected Result

~/cardano-sl $ stack exec -- liquid tools/src/cli-docs/Main.hs --ghc-option=-XNoImplicitPrelude --ghc-option=-XRecordWildCards --ghc-option=-XGADTs --ghc-option=-XOverloadedStrings --ghc-option=-XApplicativeDo
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Defunctionalize ****************************************************

**** DONE:  Elaborate **********************************************************

**** DONE:  Instantiate ********************************************************

**** DONE:  Worklist Initialize ************************************************

Working -9223372036854775808% []

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************

denisshevchenko/LiquidHaskellCardano.md