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.