haskell - Liquid Haskell 的简单一致性证明错误 - 液体类型不匹配

Question

我正在关注 official tutorial on Liquid Haskell ，并偶然发现了其中似乎是“错误”的东西。

以下代码为present in the tutorial, 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 **************************************************************