Fix for #1906: adding GADT fields syntax

src/Language/Haskell/Liquid/Bare/DataType.hs

@@ -73,11 +73,15 @@ makeDataConChecker = F.testSymbol . F.symbol
 -- equivalent to `head` and `tail`.
 --------------------------------------------------------------------------------
 makeDataConSelector :: Maybe Bare.DataConMap -> Ghc.DataCon -> Int -> F.Symbol
-makeDataConSelector dmMb d i = M.lookupDefault def (F.symbol d, i) dm
- where 
- dm = Mb.fromMaybe M.empty dmMb 
+makeDataConSelector dmMb d i
+ | Just ithField <- ithFieldMb = F.symbol (Ghc.flSelector ithField)
+ | otherwise = M.lookupDefault def (F.symbol d, i) dm
+ where
+ fields = Ghc.dataConFieldLabels d
+ ithFieldMb = Misc.getNth (i - 1) fields
+ dm = Mb.fromMaybe M.empty dmMb
  def = makeDataConSelector' d i
- 
+
 
 makeDataConSelector' :: Ghc.DataCon -> Int -> F.Symbol
 makeDataConSelector' d i

tests/basic/neg/GADTFields00.hs

@@ -0,0 +1,21 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded and then used wrongly
+
+module GADTFields00 where
+
+{-@
+data T where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T
+ @-}
+data T where
+ T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: T -> { v:Int | v < 0} @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))

tests/basic/neg/GADTFields01.hs

@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields01 where
+
+{-@
+data T where
+ T :: { getT :: Int, getT' :: Int } -> T 
+ @-}
+data T where
+ T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: { v:T | getT' v < 0 } -> { x:Int | x >= 0 } @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))

tests/basic/neg/GADTFields02.hs

@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields02 where
+
+{-@
+data T where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T 
+ @-}
+data T where
+ T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: { v:T | getT' v < 0 } -> { x:Int | x >= 0 } @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))

tests/basic/neg/GADTFields03.hs

@@ -0,0 +1,32 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields03 where
+
+{-@
+data T a where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+ S :: { getT :: Int, getS :: Float } -> T Int
+ @-}
+data T a where
+ T :: { getT :: Int, getT' :: Int } -> T Int
+ S :: { getT :: Int, getS :: Float } -> T Int
+
+{-@
+measure isT
+isT :: T Int -> Bool
+@-}
+isT :: T Int -> Bool
+isT (T _ _) = True
+isT _ = False
+
+{-@ f :: { v: T Int | isT v && getS v >= 0 } -> Float @-}
+f :: T Int -> Float
+f = getS
+
+main :: IO ()
+main = print (f (S 5 0.1))

tests/basic/neg/GADTFields04.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With shared field names
+
+module GADTFields04 where
+
+{-@
+data T a where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+ S :: { getT :: Int, getS :: String } -> T Int
+ @-}
+data T a where
+ T :: { getT :: Int, getT' :: Int } -> T Int
+ S :: { getT :: Int, getS :: String } -> T Int
+
+{-@ f :: { v:T Int | getT v >= 0 } -> { x: Int | x >= 0 } @-}
+f :: T Int -> Int
+f = getT
+
+main :: IO ()
+main = do
+ print (f (T 5 6))
+ print (f (S 3 ""))

tests/basic/pos/GADTFields00.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- Basic syntax checking
+
+module GADTFields00 where
+
+{-@
+data T where
+ T :: { getT :: Int } -> T
+ @-}
+data T where
+ T :: { getT :: Int } -> T
+
+main :: IO ()
+main = print ()

tests/basic/pos/GADTFields01.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded
+
+module GADTFields01 where
+
+{-@
+data T where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T
+ @-}
+data T where
+ T :: { getT :: Int, getT' :: Int } -> T
+
+main :: IO ()
+main = print ()

tests/basic/pos/GADTFields02.hs

@@ -0,0 +1,26 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--reflection" @-}
+
+-- With shared field names
+
+module GADTFields02 where
+
+{-@
+data T a where
+ T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+ S :: { getT :: Int, getS :: String } -> T Int
+ @-}
+data T a where
+ T :: { getT :: Int, getT' :: Int } -> T Int
+ S :: { getT :: Int, getS :: String } -> T Int
+
+{-@ f :: { v:T Int | getT v >= 0 } -> { x: Int | x >= 0 } @-}
+f :: T Int -> Int
+f = getT
+
+main :: IO ()
+main = do
+ print (f (T 5 6))
+ print (f (S 3 ""))

tests/datacon/neg/AutoliftedFields00.hs

@@ -0,0 +1,14 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH is missing and uses a LH-refined type alias incorrectly
+
+module AutoliftedFields00 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t <= 0 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/neg/AutoliftedFields01.hs

@@ -0,0 +1,15 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell do not match and the LH one is not a subtype
+
+module AutoliftedFields01 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getT :: Float } @-}
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t >= 1 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/pos/AutoliftedFields00.hs

@@ -0,0 +1,14 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH is missing but uses a LH-refined type alias correctly
+
+module AutoliftedFields00 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t >= 1 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/pos/AutoliftedFields01.hs

@@ -0,0 +1,16 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell give different names to the fields, but use them
+-- in valid ways.
+
+module AutoliftedFields01 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getMyT :: Nat } @-}
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t == getMyT t } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/pos/AutoliftedFields02.hs

@@ -0,0 +1,15 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell do not match but the LH is a subtype
+
+module AutoliftedFields02 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getT :: Nat } @-}
+data T = T { getT :: Int }
+
+{-@ f :: T -> Nat @-}
+f :: T -> Nat
+f (T x) = x