haskellz3boolean-logicliquid-haskell

LiquidHaskell: failing DeMorgan's law

I am having troubles proving the following law with LiquidHaskell:

DeMorgan's law

It is known as (one of) DeMorgan's law, and simply states that the negation of oring two values must be the same as anding the negation of each. It's been proven for a long time, and is an example in LiquidHaskell's tutorial. I am following along in the tutorial, but fail to get the following code to pass:

-- Test.hs
module Main where

main :: IO ()
main = return ()

(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

(<=>)  :: Bool -> Bool -> Bool
False <=> False = True
False <=> True  = False
True  <=> True  = True
True  <=> False = False

{-@ type TRUE  = {v:Bool | Prop v}       @-}
{-@ type FALSE = {v:Bool | not (Prop v)} @-}

{-@ deMorgan :: Bool -> Bool -> TRUE @-}
deMorgan :: Bool -> Bool -> Bool
deMorgan a b = not (a || b) <=> (not a && not b)

When running liquid Test.hs, I get the following output:

LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE:  Parsed All Specifications ******************************************


**** DONE:  Loaded Targets *****************************************************


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

Working   0%     [.................................................................]
Done solving.

**** DONE:  solve **************************************************************


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


**** RESULT: UNSAFE ************************************************************


 Test.hs:23:16-48: Error: Liquid Type Mismatch

 23 | deMorgan a b = not (a || b) <=> (not a && not b)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : Bool

   not a subtype of Required type
     VV : {VV : Bool | Prop VV}

   In Context

Now I'm by no means a LiquidHaskell expert, but I'm pretty sure something must be wrong. I have convinced myself that the identity holds a few years ago, but to make sure I called the function with every possible input, and eventually ran

λ: :l Test.hs 
λ: import Test.QuickCheck
λ: quickCheck deMorgan 
>>> +++ OK, passed 100 tests.

So I don't seem to have a typo in the Haskell code, the error must lie in the LiquidHaskell specification. It seems that LiquidHaskell cannot infer that the resulting Bool is strictly TRUE:

Inferred type
  VV : Bool

not a subtype of Required type
  VV : {VV : Bool | Prop VV}

What is my mistake here? Any help is appreciated!

PS: I'm using the z3 solver, and running GHC 7.10.3. LiquidHaskell version is 2009-15.

Solution

  • LiquidHaskell cannot prove your program safe because it does not have a strong enough type for (<=>). We do infer types for functions, but the inference is based on the other type signatures in the program. Specifically, we need to figure out that

    {-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | Prop v <=> (Prop p <=> Prop q)} @-}

    (The Prop syntax is how we lift a Haskell Bool to an SMT boolean.)

    In order for for LiquidHaskell to infer this type, it would need to see a predicate Prop v <=> (Prop p <=> Prop q) somewhere in another type signature (for some v, p, and q). This fragment doesn't appear anywhere, so we need to provide the signature explicitly.

    It's an unfortunate limitation of LiquidHaskell, but is crucial for retaining decidability.

    PS: Here's a link to a working version of your example. http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1461434240_7574.hs