liquid haskell - Problem with naming record fields for List data type

Question

For the sake of demonstration, I have two nearly-identical files: ListSuccess.hs and 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 }

The only difference between these files is that ListSuccess names the fields of Cons as lh and lt, and ListFailure names the fields of Cons as head and tail.

Compiling with liquid, ListSuccess.hs compiles successfully, however ListFailure fails to compile, yielding this error:

 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

As far as I can tell, using head and tail as the field names should not be an issue, especially because I imported prelude hiding those names. The same error occurs even when I use import qualified Prelude and similar variants.

Is this a bug, or is there something that I'm missing here?

Configuration:

• LiquidHaskell Version 0.8.6.0.

Answer 1

等待大神答复