Liquid Haskell的简单一致性证明错误-Liquid Type Mismatch

Question

我遵循的是Liquid Haskell的官方教程，偶然发现了其中的“ bug”。

本教程中包含以下代码，而Liquid Haskell应该检查它是否安全。

{-@ 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)

但是，当检查文件时，我得到：

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

如何检查此属性？

Answer 1

我发现了问题所在。必须启用定理证明才能使其发挥作用。

它可以在文件中启用（或作为 的参数liquid），如下所示：

{-@ 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)

然后：

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