Skip to content

LiquidHaskell Caught Telling Lies!

One crucial goal of a type system is to provide the guarantee, memorably phrased by Milner as well-typed programs don't go wrong. The whole point of LiquidHaskell (and related systems) is to provide the above guarantee for expanded notions of "going wrong". All this time, we've claimed (and believed) that LiquidHaskell provided such a guarantee.

We were wrong.

LiquidHaskell tells lies.

27: {-@ LIQUID "--no-termination" @-}
28: 
29: module TellingLies where
30: 
31: import Language.Haskell.Liquid.Prelude (liquidError)
32: 
33: divide  :: Int -> Int -> Int
34: foo     :: Int -> Int
35: explode :: Int

To catch LiquidHaskell red-handed, we require

  1. a notion of going wrong,
  2. a program that clearly goes wrong, and the smoking gun,
  3. a lie from LiquidHaskell that the program is safe.

The Going Wrong

Lets keep things simple with an old fashioned div-ision operator. A division by zero would be, clearly going wrong.

To alert LiquidHaskell to this possibility, we encode "not going wrong" with the precondition that the denominator be non-zero.

54: {-@ divide :: n:Int -> d:{v:Int | v /= 0} -> Int @-}
55: (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV /= 0)} -> (GHC.Types.Int)divide (GHC.Types.Int)n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}liquidError {VV : [(GHC.Types.Char)] | ((len VV) >= 0) && ((sumLens VV) >= 0)}"no you didn't!"
56: divide n d = {VV : (GHC.Types.Int) | (VV == n)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (((x1 >= 0) && (x2 >= 0)) => (VV >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (VV <= x1)) && (VV == (x1 / x2))}`div` {VV : (GHC.Types.Int) | (VV /= 0)}d

The Program

Now, consider the function foo.

65: {-@ foo :: n:Int -> {v:Nat | v < n} @-}
66: n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo (GHC.Types.Int)n | {VV : (GHC.Types.Int) | (VV == n)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 > x2))}> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0     = {VV : (GHC.Types.Int) | (VV == n)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
67:       | otherwise = n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo {VV : (GHC.Types.Int) | (VV == n)}n

Now, foo should only be called with strictly positive values. In which case, the function returns a Nat that is strictly smaller than the input. The function diverges when called with 0 or negative inputs.

Note that the signature of foo is slightly different, but nevertheless, legitimate, as when the function returns an output, the output is indeed a Nat that is strictly less than the input parameter n. Hence, LiquidHaskell happily checks that foo does indeed satisfy its given type.

So far, nothing has gone wrong either in the program, or with LiquidHaskell, but consider this innocent little function:

86: (GHC.Types.Int)explode = let {VV : (GHC.Types.Int) | (VV == (0  :  int))}z = {VV : (GHC.Types.Int) | (VV == (0  :  int))}0
87:           in  (x:{VV : (GHC.Types.Int) | (VV == 0) && (VV == 1) && (VV == TellingLies.explode) && (VV == z) && (VV > 0) && (VV > TellingLies.explode) && (VV > z) && (VV < 0) && (VV < TellingLies.explode) && (VV < z)}
-> {VV : (GHC.Types.Int) | (VV == 0) && (VV == 1) && (VV == TellingLies.explode) && (VV == x) && (VV == z) && (VV > 0) && (VV > TellingLies.explode) && (VV > x) && (VV > z) && (VV < 0) && (VV < TellingLies.explode) && (VV < x) && (VV < z)}\{VV : (GHC.Types.Int) | (VV == 0) && (VV == 1) && (VV == TellingLies.explode) && (VV == z) && (VV > 0) && (VV > TellingLies.explode) && (VV > z) && (VV < 0) && (VV < TellingLies.explode) && (VV < z)}x -> ({VV : (GHC.Types.Int) | (VV == (2013  :  int))}2013 (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV /= 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV == z) && (VV == (0  :  int))}z)) (n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo {VV : (GHC.Types.Int) | (VV == z) && (VV == (0  :  int))}z)

Thanks to lazy evaluation, the call to foo is ignored, so evaluating explode leads to a crash! Ugh!

The Lie

However, LiquidHaskell produces a polyannish prognosis and cheerfully declares the program safe.

Huh?

Well, LiquidHaskell deduces that

  • z == 0 from the binding,
  • x : Nat from the output type for foo
  • x < z from the output type for foo

Of course, no such x exists! Or, rather, the SMT solver reasons

108:     z == 0 && x >= 0 && x < z  => z /= 0

as the hypotheses are inconsistent. In other words, LiquidHaskell deduces that the call to divide happens in an impossible environment, i.e. is dead code, and hence, the program is safe.

In our defence, the above, sunny prognosis is not totally misguided. Indeed, if Haskell was like ML and had strict evaluation then indeed the program would be safe in that we would not go wrong i.e. would not crash with a divide-by-zero.

But of course, thats a pretty lame excuse, since Haskell doesn't have strict semantics. So looks like LiquidHaskell (and hence, we) have been caught red-handed.

Well then, is there a way to prevent LiquidHaskell from telling lies? That is, can we get Milner's well-typed programs don't go wrong guarantee under lazy evaluation?

Thankfully, there is.

Ranjit Jhala and Niki Vazou
2013-11-23 16:12
termination