1

为了演示，我有两个几乎相同的文件：ListSuccess.hs和ListFailure.hs：

-- File: ListSuccess.hs
module ListSuccess where


import           Prelude                 hiding ( head
                                                , tail
                                                )


{-@
data List a = Nil | Cons { lh :: a , lt :: List a }
@-}
data List a = Nil |Cons { lh :: a , lt :: List a }

-- File: ListFailure.hs
module ListFailure where


import           Prelude                 hiding ( head
                                                , tail
                                                )


{-@
data List a = Nil | Cons { head :: a , tail :: List a }
@-}
data List a = Nil | Cons { head :: a , tail :: List a }

这些文件之间的唯一区别在于ListSuccess将字段命名为Consaslh和lt，并将ListFailure字段命名为Consashead和tail。

用 编译liquid，ListSuccess.hs编译成功，但是ListFailure编译失败，产生这个错误：

 10 | data List a = Nil | Cons { head :: a , tail :: List a }
           ^^^^^

     ListFailure.head :: forall a .
                         lq$recSel:(ListFailure.List a) -> {VV : a | VV == head lq$recSel}
     Sort Error in Refinement: {VV : a##xo | VV == head lq$recSel}
     Cannot unify fix$36$$91$$93$ with ListFailure.List in expression: head lq$recSel


 /Users/henry/Documents/Prototypes/liquidhaskell/list-fields-bug/ListFailure.hs:12:21-55: Error: Illegal type specification for `ListFailure.Cons`

 12 | data List a = Nil | Cons { head :: a , tail :: List a }
                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

     ListFailure.Cons :: forall a .
                         head:a -> tail:(ListFailure.List a) -> {VV : (ListFailure.List a) | tail VV == tail
                                                                                             && head VV == head}
     Sort Error in Refinement: {VV : (ListFailure.List a##agi) | (tail VV == tail##ListFailure.Cons
                                                                  && head VV == head##ListFailure.Cons)}
     Cannot unify fix$36$$91$$93$ with ListFailure.List in expression: tail VV

据我所知，使用head和tail作为字段名称应该不是问题，特别是因为我导入了隐藏这些名称的前奏。即使我使用import qualified Prelude和类似的变体，也会发生同样的错误。

这是一个错误，还是我在这里遗漏了什么？

配置：

  • LiquidHaskell 版本 0.8.6.0。
4

0 回答 0