From 9f2076b127807c2fbc67441b6430be2ba77233e3 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 11:31:17 -0500 Subject: [PATCH 1/6] 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/6] 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/6] 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/6] 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 3500cd9012c1268a4edde4f2a24f649431286035 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Mon, 17 Jan 2022 11:32:02 -0500 Subject: [PATCH 5/6] working on fix for #1904 decls having wrong inferred LH type --- src/Language/Haskell/Liquid/Bare.hs | 6 ++--- src/Language/Haskell/Liquid/Bare/DataType.hs | 2 +- src/Language/Haskell/Liquid/Bare/Expand.hs | 2 +- tests/basic/neg/GADTFields05.hs | 25 ++++++++++++++++++++ tests/datacon/neg/AutoliftedFields00.hs | 2 +- tests/datacon/pos/AutoliftedFields00.hs | 2 +- 6 files changed, 32 insertions(+), 7 deletions(-) create mode 100644 tests/basic/neg/GADTFields05.hs diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs index ff96ea4604..bb4a583be2 100644 --- a/src/Language/Haskell/Liquid/Bare.hs +++ b/src/Language/Haskell/Liquid/Bare.hs @@ -266,7 +266,7 @@ makeGhcSpec0 cfg src lmap mspecsNoCls = do , _gsLSpec = finalLiftedSpec { impSigs = makeImports mspecs , expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ] - , dataDecls = dataDecls mySpec2 + , dataDecls = dataDecls mySpec2 , measures = Ms.measures mySpec -- We want to export measures in a 'LiftedSpec', especially if they are -- required to check termination of some 'liftedSigs' we export. Due to the fact @@ -752,7 +752,7 @@ makeInlSigs env rtEnv makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] makeMsrSigs env rtEnv - = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env))) + = makeLiftedSigs rtEnv (CoreToLogic.measureSpecType (typeclass (getConfig env))) . makeFromSet "hmeas" Ms.hmeas env makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)] @@ -1172,7 +1172,7 @@ makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0 , isLocInFile srcF t ] , Ms.axeqs = gsMyAxioms refl - , Ms.aliases = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE + , Ms.aliases = F.tracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE , Ms.ealiases = M.elems . exprAliases $ myRTE , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual) } diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index 44ea1db40e..92b5ed01ac 100644 --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -340,7 +340,7 @@ fieldName d dp x makeDataFields :: F.TCEmb Ghc.TyCon -> F.FTycon -> [RTyVar] -> [(F.LocSymbol, SpecType)] -> [F.DataField] -makeDataFields tce _c as xts = [ F.DField x (fSort t) | (x, t) <- xts] +makeDataFields tce _c as xts = F.tracepp "dfields" [ F.DField x (fSort t) | (x, t) <- F.tracepp "xts" xts] where su = zip (F.symbol <$> as) [0..] fSort = F.substVars su . F.mapFVar (+ (length as)) . RT.rTypeSort tce diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs index af77169b1b..8b9617610f 100644 --- a/src/Language/Haskell/Liquid/Bare/Expand.hs +++ b/src/Language/Haskell/Liquid/Bare/Expand.hs @@ -327,7 +327,7 @@ instance Expand Body where instance Expand DataCtor where expand rtEnv l c = c { dcTheta = expand rtEnv l (dcTheta c) - , dcFields = [(x, expand rtEnv l t) | (x, t) <- dcFields c ] + , dcFields = F.tracepp "dcFields: postexpand" [(x, expand rtEnv l t) | (x, t) <- F.tracepp "dcFields: preexpand" $ dcFields c ] , dcResult = expand rtEnv l (dcResult c) } diff --git a/tests/basic/neg/GADTFields05.hs b/tests/basic/neg/GADTFields05.hs new file mode 100644 index 0000000000..b29f0ad515 --- /dev/null +++ b/tests/basic/neg/GADTFields05.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE GADTs #-} + +{-@ LIQUID "--exact-data-cons" @-} + +-- With shared field names + +module GADTFields05 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 && 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/datacon/neg/AutoliftedFields00.hs b/tests/datacon/neg/AutoliftedFields00.hs index 06974bfc85..ac90a6bdc8 100644 --- a/tests/datacon/neg/AutoliftedFields00.hs +++ b/tests/datacon/neg/AutoliftedFields00.hs @@ -9,6 +9,6 @@ type Nat = Int data T = T { getT :: Nat } -{-@ f :: { t : T | getT t <= 0 } -> Nat @-} +{-@ f :: T -> { v : Int | v < 0 } @-} f :: T -> Nat f (T x) = x diff --git a/tests/datacon/pos/AutoliftedFields00.hs b/tests/datacon/pos/AutoliftedFields00.hs index 7b215a6d76..83f98ddfac 100644 --- a/tests/datacon/pos/AutoliftedFields00.hs +++ b/tests/datacon/pos/AutoliftedFields00.hs @@ -9,6 +9,6 @@ type Nat = Int data T = T { getT :: Nat } -{-@ f :: { t : T | getT t >= 1 } -> Nat @-} +{-@ f :: T -> Nat @-} f :: T -> Nat f (T x) = x From 8a84fd27d01604f37d624ffb5156681a18ab41b4 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Mon, 17 Jan 2022 11:32:56 -0500 Subject: [PATCH 6/6] Remove bad test from other branch --- tests/basic/neg/GADTFields05.hs | 25 ------------------------- 1 file changed, 25 deletions(-) delete mode 100644 tests/basic/neg/GADTFields05.hs diff --git a/tests/basic/neg/GADTFields05.hs b/tests/basic/neg/GADTFields05.hs deleted file mode 100644 index b29f0ad515..0000000000 --- a/tests/basic/neg/GADTFields05.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-# LANGUAGE GADTs #-} - -{-@ LIQUID "--exact-data-cons" @-} - --- With shared field names - -module GADTFields05 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 && 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 ""))