liquidhaskell icon indicating copy to clipboard operation
liquidhaskell copied to clipboard

Fix for #1906: adding GADT fields syntax

Open Fizzixnerd opened this issue 3 years ago • 1 comments

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.

Fizzixnerd avatar Jan 10 '22 21:01 Fizzixnerd

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.

Fizzixnerd avatar Jan 10 '22 21:01 Fizzixnerd