liquidhaskell
liquidhaskell copied to clipboard
Fix for #1906: adding GADT fields syntax
This is for issue #1906. I have made the majority of the changes, but need to write more tests as things can get quite tricky.
Notably, GADTs can have shared field names only when the result type is the same, so the following is illegal, but if both were -> T Int
it would be fine:
data T a where
T :: { getT :: Int } -> T Int
S :: { getT :: Int } -> T Float
I want to make sure the names are resolved properly, so any ideas for additional tests are appreciated.
Depends on PR 1921.
tests/basic/pos/GADTFields02.hs currently fails with:
liquidhaskell > > **** LIQUID: UNSAFE ************************************************************
liquidhaskell > >
liquidhaskell > > tests/basic/pos/GADTFields02.hs:21:1: error:
liquidhaskell > > Liquid Type Mismatch
liquidhaskell > > .
liquidhaskell > > The inferred type
liquidhaskell > > VV : GHC.Types.Int
liquidhaskell > > .
liquidhaskell > > is not a subtype of the required type
liquidhaskell > > VV : {VV : GHC.Types.Int | VV >= 0}
liquidhaskell > > .
liquidhaskell > > Constraint id 22
liquidhaskell > > |
liquidhaskell > > 21 | f = getT
liquidhaskell > > | ^^^^^^^^
liquidhaskell > >
liquidhaskell >
I also just realized I put the tests under basic
so they would be run earlier, but I should probably move them to datacons
.