LiquidHaskell: DeMorgan law violation

Question

I am having problems proving the following law with LiquidHaskell:

It is known as (one of) the DeMorgan law and simply states that the negation of or with two meanings should be the same as and with the negation of each. This has been proven for a long time and is an example in the LiquidHaskell tutorial . I follow in the tutorial but cannot get the following code:

 -- 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 ab = 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 ab = 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 am by no means an expert at LiquidHaskell, but I'm sure something should be wrong. I convinced myself that the personality existed several years ago, but to make sure that I called the function with every possible input, I ended up running

 λ: :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 should be in the LiquidHaskell specification. It seems that LiquidHaskell cannot conclude that the resulting Bool strictly TRUE :

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

What's my mistake? Any help is appreciated!

PS: I use the z3 solver and run GHC 7.10.3. LiquidHaskell version 2009-15 .

Answer 1

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

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

( Prop syntax is how we raise the Haskell Bool to an SMT boolean.)

For LiquidHaskell to infer this type, it would need to see the predicate Prop v <=> (Prop p <=> Prop q) somewhere in the signature of another type (for some v , p and q ). This snippet does not appear anywhere, so we must explicitly provide a signature.

This is an unfortunate limitation of LiquidHaskell, but is critical to maintaining solvability.

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