Simple congruence proof error with Liquid Haskell - Liquid Type Mismatch

Question

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?

Henebry

Answer 1

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 **************************************************************

Henebry