From 9f2076b127807c2fbc67441b6430be2ba77233e3 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 11:31:17 -0500 Subject: [PATCH 1/7] Fix for #1904 autolifting of data fields --- src/Language/Haskell/Liquid/Bare/DataType.hs | 12 ++++++++---- tests/datacon/pos/AutoliftedFields.hs | 12 ++++++++++++ 2 files changed, 20 insertions(+), 4 deletions(-) create mode 100644 tests/datacon/pos/AutoliftedFields.hs diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index 03f01eec3a..44ea1db40e 100644 --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/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 diff --git a/tests/datacon/pos/AutoliftedFields.hs b/tests/datacon/pos/AutoliftedFields.hs new file mode 100644 index 0000000000..7a7d14cbcc --- /dev/null +++ b/tests/datacon/pos/AutoliftedFields.hs @@ -0,0 +1,12 @@ +{-@ LIQUID "--exact-data-cons" @-} + +module AutoliftedFields 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 From 8aaceac4b505e12cc88da7afd10eb1e9642112c9 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 11:43:35 -0500 Subject: [PATCH 2/7] Add negative test for #1904 --- tests/datacon/neg/AutoliftedFields.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/datacon/neg/AutoliftedFields.hs diff --git a/tests/datacon/neg/AutoliftedFields.hs b/tests/datacon/neg/AutoliftedFields.hs new file mode 100644 index 0000000000..fa4c5048d8 --- /dev/null +++ b/tests/datacon/neg/AutoliftedFields.hs @@ -0,0 +1,12 @@ +{-@ LIQUID "--exact-data-cons" @-} + +module AutoliftedFields 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 From 943cc45318219f2fa1028480069686b8ad8fdf6f Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 14:59:33 -0500 Subject: [PATCH 3/7] More tests for #1904 --- ...AutoliftedFields.hs => AutoliftedFields00.hs} | 4 +++- tests/datacon/neg/AutoliftedFields01.hs | 15 +++++++++++++++ ...AutoliftedFields.hs => AutoliftedFields00.hs} | 4 +++- tests/datacon/pos/AutoliftedFields01.hs | 16 ++++++++++++++++ tests/datacon/pos/AutoliftedFields02.hs | 15 +++++++++++++++ 5 files changed, 52 insertions(+), 2 deletions(-) rename tests/datacon/neg/{AutoliftedFields.hs => AutoliftedFields00.hs} (63%) create mode 100644 tests/datacon/neg/AutoliftedFields01.hs rename tests/datacon/pos/{AutoliftedFields.hs => AutoliftedFields00.hs} (64%) create mode 100644 tests/datacon/pos/AutoliftedFields01.hs create mode 100644 tests/datacon/pos/AutoliftedFields02.hs diff --git a/tests/datacon/neg/AutoliftedFields.hs b/tests/datacon/neg/AutoliftedFields00.hs similarity index 63% rename from tests/datacon/neg/AutoliftedFields.hs rename to tests/datacon/neg/AutoliftedFields00.hs index fa4c5048d8..06974bfc85 100644 --- a/tests/datacon/neg/AutoliftedFields.hs +++ b/tests/datacon/neg/AutoliftedFields00.hs @@ -1,6 +1,8 @@ {-@ LIQUID "--exact-data-cons" @-} -module AutoliftedFields where +-- 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 diff --git a/tests/datacon/neg/AutoliftedFields01.hs b/tests/datacon/neg/AutoliftedFields01.hs new file mode 100644 index 0000000000..73522d5ba8 --- /dev/null +++ b/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 diff --git a/tests/datacon/pos/AutoliftedFields.hs b/tests/datacon/pos/AutoliftedFields00.hs similarity index 64% rename from tests/datacon/pos/AutoliftedFields.hs rename to tests/datacon/pos/AutoliftedFields00.hs index 7a7d14cbcc..7b215a6d76 100644 --- a/tests/datacon/pos/AutoliftedFields.hs +++ b/tests/datacon/pos/AutoliftedFields00.hs @@ -1,6 +1,8 @@ {-@ LIQUID "--exact-data-cons" @-} -module AutoliftedFields where +-- 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 diff --git a/tests/datacon/pos/AutoliftedFields01.hs b/tests/datacon/pos/AutoliftedFields01.hs new file mode 100644 index 0000000000..59fe08bbca --- /dev/null +++ b/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 diff --git a/tests/datacon/pos/AutoliftedFields02.hs b/tests/datacon/pos/AutoliftedFields02.hs new file mode 100644 index 0000000000..e02860d519 --- /dev/null +++ b/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 : T | getT t >= 0 } -> Nat @-} +f :: T -> Nat +f (T x) = x From d737a266a89b3c7d0e2fab518f50c8cff224219b Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 15:34:27 -0500 Subject: [PATCH 4/7] Simplify AutoliftedFields02.hs --- tests/datacon/pos/AutoliftedFields02.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/datacon/pos/AutoliftedFields02.hs b/tests/datacon/pos/AutoliftedFields02.hs index e02860d519..994df82d8f 100644 --- a/tests/datacon/pos/AutoliftedFields02.hs +++ b/tests/datacon/pos/AutoliftedFields02.hs @@ -10,6 +10,6 @@ type Nat = Int {-@ data T = T { getT :: Nat } @-} data T = T { getT :: Int } -{-@ f :: { t : T | getT t >= 0 } -> Nat @-} +{-@ f :: T -> Nat @-} f :: T -> Nat f (T x) = x From 97522e1737375d92f062d262b0a9c79e12d8fe73 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Mon, 10 Jan 2022 14:56:32 -0500 Subject: [PATCH 5/7] Add tests and initial changes --- tests/basic/neg/GADTFields00.hs | 19 +++++++++++++++++++ tests/basic/neg/GADTFields01.hs | 20 ++++++++++++++++++++ tests/basic/pos/GADTFields00.hs | 15 +++++++++++++++ tests/basic/pos/GADTFields01.hs | 15 +++++++++++++++ 4 files changed, 69 insertions(+) create mode 100644 tests/basic/neg/GADTFields00.hs create mode 100644 tests/basic/neg/GADTFields01.hs create mode 100644 tests/basic/pos/GADTFields00.hs create mode 100644 tests/basic/pos/GADTFields01.hs diff --git a/tests/basic/neg/GADTFields00.hs b/tests/basic/neg/GADTFields00.hs new file mode 100644 index 0000000000..69cbf49e4c --- /dev/null +++ b/tests/basic/neg/GADTFields00.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE GADTs #-} + +-- 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)) diff --git a/tests/basic/neg/GADTFields01.hs b/tests/basic/neg/GADTFields01.hs new file mode 100644 index 0000000000..3f8205d3be --- /dev/null +++ b/tests/basic/neg/GADTFields01.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE GADTs #-} + +-- 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)) diff --git a/tests/basic/pos/GADTFields00.hs b/tests/basic/pos/GADTFields00.hs new file mode 100644 index 0000000000..0b0d788800 --- /dev/null +++ b/tests/basic/pos/GADTFields00.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} + +-- Basic syntax checking + +module GADTFields00 where + +{-@ +data T where + T :: { getT :: Int } -> T + @-} +data T where + T :: { getT :: Int } -> T + +main :: IO () +main = print () diff --git a/tests/basic/pos/GADTFields01.hs b/tests/basic/pos/GADTFields01.hs new file mode 100644 index 0000000000..c682ccc0e0 --- /dev/null +++ b/tests/basic/pos/GADTFields01.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} + +-- 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 () From 6d564bf6d4c5fc217ef265eab981118ae00b6977 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Mon, 10 Jan 2022 15:25:36 -0500 Subject: [PATCH 6/7] More tests --- tests/basic/neg/GADTFields00.hs | 2 ++ tests/basic/neg/GADTFields01.hs | 2 ++ tests/basic/neg/GADTFields02.hs | 22 ++++++++++++++++++++++ tests/basic/neg/GADTFields03.hs | 23 +++++++++++++++++++++++ 4 files changed, 49 insertions(+) create mode 100644 tests/basic/neg/GADTFields02.hs create mode 100644 tests/basic/neg/GADTFields03.hs diff --git a/tests/basic/neg/GADTFields00.hs b/tests/basic/neg/GADTFields00.hs index 69cbf49e4c..f0863b4b2d 100644 --- a/tests/basic/neg/GADTFields00.hs +++ b/tests/basic/neg/GADTFields00.hs @@ -1,5 +1,7 @@ {-# LANGUAGE GADTs #-} +{-@ LIQUID "--exact-data-cons" @-} + -- With a refinement type embedded and then used wrongly module GADTFields00 where diff --git a/tests/basic/neg/GADTFields01.hs b/tests/basic/neg/GADTFields01.hs index 3f8205d3be..e2a882a10b 100644 --- a/tests/basic/neg/GADTFields01.hs +++ b/tests/basic/neg/GADTFields01.hs @@ -1,5 +1,7 @@ {-# LANGUAGE GADTs #-} +{-@ LIQUID "--exact-data-cons" @-} + -- With a refinement type embedded in a function using a fieldname, but with a -- bad type diff --git a/tests/basic/neg/GADTFields02.hs b/tests/basic/neg/GADTFields02.hs new file mode 100644 index 0000000000..4ec0a8b63b --- /dev/null +++ b/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)) diff --git a/tests/basic/neg/GADTFields03.hs b/tests/basic/neg/GADTFields03.hs new file mode 100644 index 0000000000..3ff1067c5c --- /dev/null +++ b/tests/basic/neg/GADTFields03.hs @@ -0,0 +1,23 @@ +{-# 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 + @-} +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 = print (getT' (T 5 6)) From 483048e747601cd690161d5c4be97666ca82a61e Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Mon, 10 Jan 2022 16:01:02 -0500 Subject: [PATCH 7/7] Fix tests --- tests/basic/neg/GADTFields03.hs | 21 +++++++++++++++------ tests/basic/neg/GADTFields04.hs | 25 +++++++++++++++++++++++++ tests/basic/pos/GADTFields00.hs | 2 ++ tests/basic/pos/GADTFields01.hs | 2 ++ tests/basic/pos/GADTFields02.hs | 26 ++++++++++++++++++++++++++ 5 files changed, 70 insertions(+), 6 deletions(-) create mode 100644 tests/basic/neg/GADTFields04.hs create mode 100644 tests/basic/pos/GADTFields02.hs diff --git a/tests/basic/neg/GADTFields03.hs b/tests/basic/neg/GADTFields03.hs index 3ff1067c5c..54c9dc252a 100644 --- a/tests/basic/neg/GADTFields03.hs +++ b/tests/basic/neg/GADTFields03.hs @@ -9,15 +9,24 @@ module GADTFields03 where {-@ data T a where - T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int + 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 :: String } -> T Int + S :: { getT :: Int, getS :: Float } -> T Int -{-@ f :: { v:T Int | getT' v < 0 } -> { x:Int | x >= 0 } @-} -f :: T Int -> Int -f = getT' +{-@ +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 (getT' (T 5 6)) +main = print (f (S 5 0.1)) diff --git a/tests/basic/neg/GADTFields04.hs b/tests/basic/neg/GADTFields04.hs new file mode 100644 index 0000000000..37faa8a745 --- /dev/null +++ b/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 "")) diff --git a/tests/basic/pos/GADTFields00.hs b/tests/basic/pos/GADTFields00.hs index 0b0d788800..3972197e4c 100644 --- a/tests/basic/pos/GADTFields00.hs +++ b/tests/basic/pos/GADTFields00.hs @@ -1,5 +1,7 @@ {-# LANGUAGE GADTs #-} +{-@ LIQUID "--exact-data-cons" @-} + -- Basic syntax checking module GADTFields00 where diff --git a/tests/basic/pos/GADTFields01.hs b/tests/basic/pos/GADTFields01.hs index c682ccc0e0..ce984e4cd1 100644 --- a/tests/basic/pos/GADTFields01.hs +++ b/tests/basic/pos/GADTFields01.hs @@ -1,5 +1,7 @@ {-# LANGUAGE GADTs #-} +{-@ LIQUID "--exact-data-cons" @-} + -- With a refinement type embedded module GADTFields01 where diff --git a/tests/basic/pos/GADTFields02.hs b/tests/basic/pos/GADTFields02.hs new file mode 100644 index 0000000000..133faa9681 --- /dev/null +++ b/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 ""))