I'm following the official tutorial on Liquid Haskell, and stumbled upon what seems to be a "bug" in it.
The following code is present in the tutorial, and Liquid Haskell was supposed to check that it is safe.
{-@ type TRUE = {v:Bool | v } @-}
{-@ type FALSE = {v:Bool | not v} @-}
{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
False ==> False = True
False ==> True = True
True ==> True = True
True ==> False = False
{-@ measure f :: Int -> Int @-}
{-@ congruence :: (Int -> Int) -> Int -> Int -> TRUE @-}
congruence :: (Int -> Int) -> Int -> Int -> Bool
congruence f x y = (x == y) ==> (f x == f y)
However, when checking the file I get:
**** RESULT: UNSAFE ************************************************************
/tmp/liquid.hs:14:1-44: Error: Liquid Type Mismatch
14 | congruence f x y = (x == y) ==> (f x == f y)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Inferred type
VV : {v : GHC.Types.Bool | v <=> (x == y => ?d == ?c)}
not a subtype of Required type
VV : {VV : GHC.Types.Bool | VV}
In Context
?c : GHC.Types.Int
x : GHC.Types.Int
?d : GHC.Types.Int
y : GHC.Types.Int
How can I check this property?
I found out the problem. Theorem proving must be enabled in order for this to work.
It can be enabled in the file (or as an argument to liquid
) as follows:
{-@ LIQUID "--reflection" @-}
{-@ type TRUE = {v:Bool | v } @-}
{-@ type FALSE = {v:Bool | not v} @-}
{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
False ==> False = True
False ==> True = True
True ==> True = True
True ==> False = False
{-@ measure f :: Int -> Int @-}
{-@ congruence :: (f :: Int -> Int) -> Int -> Int -> TRUE @-}
congruence :: (Int -> Int) -> Int -> Int -> Bool
congruence f x y = (x == y) ==> (f x == f y)
Then:
LiquidHaskell Version 0.8.6.0, Git revision f4fe82cd03fbe906379c8ebeac5ec3efae0b4cd8 (dirty) [develop@f4fe82cd03fbe906379c8ebeac5ec3efae0b4cd8 (Mon Jun 24 10:55:17 2019 +0200)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.
Targets: liquid.hs
**** [Checking: liquid.hs] *****************************************************
**** DONE: A-Normalization ****************************************************
**** DONE: Extracted Core using GHC *******************************************
**** DONE: Transformed Core ***************************************************
Working 183% [========================================================================================================================]
**** DONE: annotate ***********************************************************
**** RESULT: SAFE **************************************************************