From eba1cdd3f512f9f5d983cfd3772b2c41674134f0 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Thu, 18 Feb 2021 18:15:38 +0100 Subject: [PATCH 1/7] change bivariant to perform no checks --- src/Language/Haskell/Liquid/Constraint/Split.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs index 962d406bf2..6f1842e3c3 100644 --- a/src/Language/Haskell/Liquid/Constraint/Split.hs +++ b/src/Language/Haskell/Liquid/Constraint/Split.hs @@ -139,7 +139,7 @@ bsplitW' γ t temp isHO splitfWithVariance :: Applicative f => (t -> t -> f [a]) -> t -> t -> Variance -> f [a] splitfWithVariance f t1 t2 Invariant = (++) <$> f t1 t2 <*> f t2 t1 -splitfWithVariance f t1 t2 Bivariant = (++) <$> f t1 t2 <*> f t2 t1 +splitfWithVariance f t1 t2 Bivariant = pure [] -- (++) <$> f t1 t2 <*> f t2 t1 splitfWithVariance f t1 t2 Covariant = f t1 t2 splitfWithVariance f t1 t2 Contravariant = f t2 t1 From 535c8711880fb302b457cbb9dd0e443dd36778be Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Thu, 18 Feb 2021 19:30:02 +0100 Subject: [PATCH 2/7] change semantiics of the two variences --- src/Language/Haskell/Liquid/Bare/DataType.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index 2a0204b4ae..f8f76d7e17 100644 --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -568,9 +568,9 @@ errDataConMismatch d dcs rdcs = ErrDataConMismatch sp v (ppTicks <$> S.toList dc varSignToVariance :: Eq a => [(a, Bool)] -> a -> Variance varSignToVariance varsigns i = case filter (\p -> fst p == i) varsigns of - [] -> Invariant + [] -> Bivariant [(_, b)] -> if b then Covariant else Contravariant - _ -> Bivariant + _ -> Invariant getPsSig :: [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)] getPsSig m pos (RAllT _ t r) From a6ff8e75da50f0094671f99a92a4248930bfe3cd Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Wed, 3 Mar 2021 14:08:02 +0100 Subject: [PATCH 3/7] fix tests --- src/Language/Haskell/Liquid/Bare/DataType.hs | 2 +- src/Language/Haskell/Liquid/Constraint/Split.hs | 6 +++--- src/Language/Haskell/Liquid/Types/RefType.hs | 4 ++-- tests/neg/T1613.hs | 2 ++ tests/neg/T1657.hs | 1 + tests/neg/T1657A.hs | 1 + 6 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index f8f76d7e17..827014f570 100644 --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -581,7 +581,7 @@ getPsSig m pos (RApp _ ts rs r) getPsSig m pos (RVar _ r) = addps m pos r getPsSig m pos (RAppTy t1 t2 r) - = addps m pos r ++ getPsSig m pos t1 ++ getPsSig m pos t2 + = addps m pos r ++ getPsSig m pos t1 ++ getPsSig m (not pos) t1 ++ getPsSig m pos t2 getPsSig m pos (RFun _ t1 t2 r) = addps m pos r ++ getPsSig m pos t2 ++ getPsSig m (not pos) t1 getPsSig m pos (RHole r) diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs index 6f1842e3c3..64af5d4e72 100644 --- a/src/Language/Haskell/Liquid/Constraint/Split.hs +++ b/src/Language/Haskell/Liquid/Constraint/Split.hs @@ -253,7 +253,7 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _)) splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 = return [] -splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) +splitC (SubC γ t1@(RApp c _ _ _) t2@(RApp _ _ _ _)) = do (t1',t2') <- unifyVV t1 t2 cs <- bsplitC γ t1' t2' γ' <- if (bscope (getConfig γ)) then γ `extendEnvWithVV` t1' else return γ @@ -261,8 +261,8 @@ splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) let RApp _ t2s r2s _ = t2' let isapplied = True -- TC.tyConArity (rtc_tc c) == length t1s let tyInfo = rtc_info c - csvar <- splitsCWithVariance γ' t1s t2s $ varianceTyArgs tyInfo - csvar' <- rsplitsCWithVariance isapplied γ' r1s r2s $ variancePsArgs tyInfo + csvar <- splitsCWithVariance γ' t1s t2s $ F.notracepp (" variance for " ++ showpp c) $ varianceTyArgs tyInfo + csvar' <- rsplitsCWithVariance isapplied γ' r1s r2s $ F.notracepp ("rvariance for " ++ showpp c) $ variancePsArgs tyInfo return $ cs ++ csvar ++ csvar' splitC (SubC γ t1@(RVar a1 _) t2@(RVar a2 _)) diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs index 38c9bc7b28..6c93e82fe5 100644 --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -1843,9 +1843,9 @@ makeTyConVariance c = varSignToVariance <$> tvs else L.nub $ concatMap goDCon $ Ghc.tyConDataCons c varSignToVariance v = case filter (\p -> GM.showPpr (fst p) == GM.showPpr v) varsigns of - [] -> Invariant + [] -> Bivariant [(_, b)] -> if b then Covariant else Contravariant - _ -> Bivariant + _ -> Invariant goDCon dc = concatMap (go True) (map irrelevantMult $ Ghc.dataConOrigArgTys dc) diff --git a/tests/neg/T1613.hs b/tests/neg/T1613.hs index f64d37a3fb..6d6ab6d925 100644 --- a/tests/neg/T1613.hs +++ b/tests/neg/T1613.hs @@ -4,6 +4,8 @@ module Subclass2 where data MyFunctor f = CMyFunctor {myfmap :: forall a b. (a -> b) -> f a -> f b} +{- data variance MyFunctor invariant @-} +{- data variance MyApplicative invariant @-} {-@ reflect myid @-} myid :: a -> a diff --git a/tests/neg/T1657.hs b/tests/neg/T1657.hs index 138c12e3d1..2e8787cefc 100644 --- a/tests/neg/T1657.hs +++ b/tests/neg/T1657.hs @@ -1,5 +1,6 @@ module T1657 where +{-@ data variance I invariant @-} {-@ data I

Bool> = I _ @-} data I = I Int diff --git a/tests/neg/T1657A.hs b/tests/neg/T1657A.hs index 1d8456663f..ec9b634aa8 100644 --- a/tests/neg/T1657A.hs +++ b/tests/neg/T1657A.hs @@ -1,6 +1,7 @@ module T1657A where {-@ data I Bool> = I Int @-} +{-@ data variance I invariant @-} data I = I Int {-@ getI :: forall Bool>. From cef52bf37bcebe6738a2fd6c696c23d307353313 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Wed, 3 Mar 2021 14:14:51 +0100 Subject: [PATCH 4/7] change order fields of golden --- tests/golden/json_output.golden | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/golden/json_output.golden b/tests/golden/json_output.golden index 46024b93ac..04718a9000 100644 --- a/tests/golden/json_output.golden +++ b/tests/golden/json_output.golden @@ -1,2 +1,2 @@ LIQUID -[{"start":{"line":9,"column":1},"stop":{"line":9,"column":12},"message":"Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == 7}\n .\n is not a subtype of the required type\n VV : {VV : GHC.Types.Int | VV mod 2 == 0}\n ."}] +["message":"Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == 7}\n .\n is not a subtype of the required type\n VV : {VV : GHC.Types.Int | VV mod 2 == 0}\n ."},{"start":{"column":1,"line":9},"stop":{"column":12,"line":9}] From c21f67edb41ad58c68953257afd176884842fc02 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Fri, 5 Mar 2021 11:08:40 +0100 Subject: [PATCH 5/7] fix flag --- src/Language/Haskell/Liquid/Constraint/Split.hs | 16 ++++++++-------- src/Language/Haskell/Liquid/Types/PredType.hs | 3 ++- src/Language/Haskell/Liquid/Types/RefType.hs | 12 ++++++------ src/Language/Haskell/Liquid/Types/Variance.hs | 10 ++++++++++ src/Language/Haskell/Liquid/UX/CmdLine.hs | 9 ++++++++- src/Language/Haskell/Liquid/UX/Config.hs | 2 ++ tests/neg/ExactADT6.hs | 1 + tests/neg/ExactGADT6.hs | 1 + tests/neg/RG.hs | 1 + tests/neg/contra0.hs | 4 ++-- tests/neg/maps.hs | 2 ++ tests/ple/neg/BinahUpdateLib.hs | 2 ++ tests/ple/neg/BinahUpdateLib1.hs | 2 ++ tests/test.hs | 2 +- 14 files changed, 48 insertions(+), 19 deletions(-) diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs index 64af5d4e72..73655abf54 100644 --- a/src/Language/Haskell/Liquid/Constraint/Split.hs +++ b/src/Language/Haskell/Liquid/Constraint/Split.hs @@ -137,11 +137,11 @@ bsplitW' γ t temp isHO ci = Ci (getLocation γ) Nothing (cgVar γ) splitfWithVariance :: Applicative f - => (t -> t -> f [a]) -> t -> t -> Variance -> f [a] -splitfWithVariance f t1 t2 Invariant = (++) <$> f t1 t2 <*> f t2 t1 -splitfWithVariance f t1 t2 Bivariant = pure [] -- (++) <$> f t1 t2 <*> f t2 t1 -splitfWithVariance f t1 t2 Covariant = f t1 t2 -splitfWithVariance f t1 t2 Contravariant = f t2 t1 + => Variance -> (t -> t -> f [a]) -> t -> t -> Variance -> f [a] +splitfWithVariance _ f t1 t2 Invariant = (++) <$> f t1 t2 <*> f t2 t1 +splitfWithVariance v f t1 t2 Bivariant = if v == Bivariant then pure [] else splitfWithVariance v f t1 t2 v -- (++) <$> f t1 t2 <*> f t2 t1 +splitfWithVariance _ f t1 t2 Covariant = f t1 t2 +splitfWithVariance _ f t1 t2 Contravariant = f t2 t1 updateEnv :: CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv updateEnv γ a @@ -253,7 +253,7 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _)) splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 = return [] -splitC (SubC γ t1@(RApp c _ _ _) t2@(RApp _ _ _ _)) +splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) = do (t1',t2') <- unifyVV t1 t2 cs <- bsplitC γ t1' t2' γ' <- if (bscope (getConfig γ)) then γ `extendEnvWithVV` t1' else return γ @@ -316,7 +316,7 @@ splitsCWithVariance :: CGEnv -> [Variance] -> CG [FixSubC] splitsCWithVariance γ t1s t2s variants - = concatMapM (\(t1, t2, v) -> splitfWithVariance (\s1 s2 -> (splitC (SubC γ s1 s2))) t1 t2 v) (zip3 t1s t2s variants) + = concatMapM (\(t1, t2, v) -> splitfWithVariance (fromMaybe mempty $ ghostVariance $ getConfig γ) (\s1 s2 -> (splitC (SubC γ s1 s2))) t1 t2 v) (zip3 t1s t2s variants) rsplitsCWithVariance :: Bool -> CGEnv @@ -328,7 +328,7 @@ rsplitsCWithVariance False _ _ _ _ = return [] rsplitsCWithVariance _ γ t1s t2s variants - = concatMapM (\(t1, t2, v) -> splitfWithVariance (rsplitC γ) t1 t2 v) (zip3 t1s t2s variants) + = concatMapM (\(t1, t2, v) -> splitfWithVariance (fromMaybe mempty $ ghostVariance $ getConfig γ) (rsplitC γ) t1 t2 v) (zip3 t1s t2s variants) bsplitC :: CGEnv -> SpecType diff --git a/src/Language/Haskell/Liquid/Types/PredType.hs b/src/Language/Haskell/Liquid/Types/PredType.hs index ca32d38735..97aa8607dc 100644 --- a/src/Language/Haskell/Liquid/Types/PredType.hs +++ b/src/Language/Haskell/Liquid/Types/PredType.hs @@ -56,6 +56,7 @@ import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.RefType hiding (generalize) import Language.Haskell.Liquid.Types.Types import Data.Default +import Language.Haskell.Liquid.Types.Variance makeTyConInfo :: F.TCEmb Ghc.TyCon -> [Ghc.TyCon] -> [TyConP] -> TyConMap makeTyConInfo tce fiTcs tcps = TyConMap @@ -76,7 +77,7 @@ mkFInstRTyCon tce fiTcs tcm = M.fromList , (c, ts) <- Mb.maybeToList (famInstArgs fiTc) ] -mkRTyCon :: TyConP -> RTyCon +mkRTyCon :: TyConP -> RTyCon mkRTyCon (TyConP _ tc αs' ps tyvariance predvariance size) = RTyCon tc pvs' (mkTyConInfo tc tyvariance predvariance size) where diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs index 6c93e82fe5..b9b11d1f94 100644 --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -542,10 +542,10 @@ rApp :: TyCon rApp c = RApp (tyConRTyCon c) gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType -gApp tc αs πs = rApp tc - [rVar α | RTV α <- αs] - (rPropP [] . pdVarReft <$> πs) - mempty +gApp tc αs πs = RApp (tyConRTyCon tc) + [rVar α | RTV α <- αs] + (rPropP [] . pdVarReft <$> πs) + mempty pdVarReft :: PVar t -> UReft Reft pdVarReft = (\p -> MkUReft mempty p) . pdVar @@ -1842,8 +1842,8 @@ makeTyConVariance c = varSignToVariance <$> tvs then go True (fromJust $ Ghc.synTyConRhs_maybe c) else L.nub $ concatMap goDCon $ Ghc.tyConDataCons c - varSignToVariance v = case filter (\p -> GM.showPpr (fst p) == GM.showPpr v) varsigns of - [] -> Bivariant + varSignToVariance a = case filter (\p -> GM.showPpr (fst p) == GM.showPpr a) varsigns of + [] -> Bivariant [(_, b)] -> if b then Covariant else Contravariant _ -> Invariant diff --git a/src/Language/Haskell/Liquid/Types/Variance.hs b/src/Language/Haskell/Liquid/Types/Variance.hs index 9826dee991..9af72ddded 100644 --- a/src/Language/Haskell/Liquid/Types/Variance.hs +++ b/src/Language/Haskell/Liquid/Types/Variance.hs @@ -27,3 +27,13 @@ instance Binary Variance instance NFData Variance instance F.PPrint Variance where pprintTidy _ = text . show + +instance Semigroup Variance where + Invariant <> _ = Invariant + _ <> Invariant = Invariant + Bivariant <> v = v + v <> Bivariant = v + v1 <> v2 = if v1 == v2 then v1 else Invariant + +instance Monoid Variance where + mempty = Bivariant diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs index c6fec9500d..40fe87b2bf 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -84,6 +84,7 @@ import qualified Language.Haskell.Liquid.GHC.API as GHC import Language.Haskell.TH.Syntax.Compat (fromCode, toCode) import Text.PrettyPrint.HughesPJ hiding (Mode, (<>)) +import Language.Haskell.Liquid.Types.Variance @@ -426,6 +427,11 @@ config = cmdArgsMode $ Config { = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE" + , ghostVariance + = def + &= name "ghost-variance" + &= help "Specify the variance of short type arguments: Invariant | Bivariant | Contravariant | Covariant" + } &= program "liquid" &= help "Refinement Types for Haskell" &= summary copyright @@ -671,7 +677,8 @@ defConfig = Config , rwTerminationCheck = False , skipModule = False , noLazyPLE = False - , fuel = Nothing + , fuel = Nothing + , ghostVariance = mempty } diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs index 45bf8e99f5..36423416b8 100644 --- a/src/Language/Haskell/Liquid/UX/Config.hs +++ b/src/Language/Haskell/Liquid/UX/Config.hs @@ -22,6 +22,7 @@ import Prelude hiding (error) import Language.Fixpoint.Types.Config hiding (Config) import GHC.Generics import System.Console.CmdArgs +import Language.Haskell.Liquid.Types.Variance -- NOTE: adding strictness annotations breaks the help message data Config = Config @@ -100,6 +101,7 @@ data Config = Config , skipModule :: Bool -- ^ Skip this module entirely (don't even compile any specs in it) , noLazyPLE :: Bool , fuel :: Maybe Int -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) + , ghostVariance :: Maybe Variance } deriving (Generic, Data, Typeable, Show, Eq) allowPLE :: Config -> Bool diff --git a/tests/neg/ExactADT6.hs b/tests/neg/ExactADT6.hs index bbfa0df8bf..f8e77d9808 100644 --- a/tests/neg/ExactADT6.hs +++ b/tests/neg/ExactADT6.hs @@ -1,5 +1,6 @@ {-@ LIQUID "--no-adt" @-} {-@ LIQUID "--exact-data-con" @-} +{-@ LIQUID "--ghost-variance=Invariant" @-} {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-} diff --git a/tests/neg/ExactGADT6.hs b/tests/neg/ExactGADT6.hs index c610b5a824..5b44eeb478 100644 --- a/tests/neg/ExactGADT6.hs +++ b/tests/neg/ExactGADT6.hs @@ -1,5 +1,6 @@ {-@ LIQUID "--no-adt" @-} {-@ LIQUID "--exact-data-con" @-} +{-@ LIQUID "--ghost-variance=Invariant" @-} {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-} diff --git a/tests/neg/RG.hs b/tests/neg/RG.hs index 7777993fa8..3cf87374b7 100644 --- a/tests/neg/RG.hs +++ b/tests/neg/RG.hs @@ -1,4 +1,5 @@ module RG where +{-@ LIQUID "--ghost-variance=Invariant" @-} import Data.IORef as R diff --git a/tests/neg/contra0.hs b/tests/neg/contra0.hs index 65ca37ee3d..a0dde5a1e1 100644 --- a/tests/neg/contra0.hs +++ b/tests/neg/contra0.hs @@ -7,8 +7,8 @@ import Language.Haskell.Liquid.Prelude (liquidAssert) import Data.IORef -{-@ data variance IO bivariant @-} -{-@ data variance IORef bivariant @-} +{-@ data variance IO invariant @-} +{-@ data variance IORef invariant @-} job :: IO () job = do diff --git a/tests/neg/maps.hs b/tests/neg/maps.hs index d185b450ac..7be325e5f4 100644 --- a/tests/neg/maps.hs +++ b/tests/neg/maps.hs @@ -1,3 +1,4 @@ +{-@ LIQUID "--ghost-variance=invariant" @-} module Maps where {-@ prop1 :: x:_ -> y:{_ | y == x} -> TT @-} @@ -17,6 +18,7 @@ prop2 x y = (z == 10) ----------------------------------------------------------------------- data Map k v = M +{- data variance Map invariant invariant @-} {-@ embed Map as Map_t @-} {-@ measure Map_select :: Map k v -> k -> v @-} diff --git a/tests/ple/neg/BinahUpdateLib.hs b/tests/ple/neg/BinahUpdateLib.hs index ef826c2139..2f1dc5b6a9 100644 --- a/tests/ple/neg/BinahUpdateLib.hs +++ b/tests/ple/neg/BinahUpdateLib.hs @@ -20,6 +20,8 @@ instance PersistEntity Blob where BlobXVal :: EntityField Blob Int BlobYVal :: EntityField Blob Int +{-@ data variance EntityField invariant invariant @-} + {-@ data Blob = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-} data Blob = B { xVal :: Int, yVal :: Int } diff --git a/tests/ple/neg/BinahUpdateLib1.hs b/tests/ple/neg/BinahUpdateLib1.hs index f7023a175a..3b0ed4b043 100644 --- a/tests/ple/neg/BinahUpdateLib1.hs +++ b/tests/ple/neg/BinahUpdateLib1.hs @@ -20,6 +20,8 @@ instance PersistEntity Blob where = typ ~ Int => BlobXVal | typ ~ Int => BlobYVal +{-@ data variance EntityField invariant invariant @-} + data Blob = B { xVal :: Int, yVal :: Int } data Update record typ = Update diff --git a/tests/test.hs b/tests/test.hs index b98dc1717c..a29e224638 100644 --- a/tests/test.hs +++ b/tests/test.hs @@ -80,7 +80,7 @@ main = do unsetEnv "LIQUIDHASKELL_OPTS" errorTests : macroTests : proverTests : - goldenTests : +-- goldenTests : benchTests : [] From 8ea194f4441cac052c5cf0443c72e97b805bebd0 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Fri, 5 Mar 2021 11:55:05 +0100 Subject: [PATCH 6/7] fix more binah tests --- tests/ple/neg/BinahUpdate.hs | 1 + tests/ple/neg/BinahUpdateLib.hs | 1 + tests/ple/neg/BinahUpdateLib1.hs | 2 ++ 3 files changed, 4 insertions(+) diff --git a/tests/ple/neg/BinahUpdate.hs b/tests/ple/neg/BinahUpdate.hs index 2c50f93d2c..c8aacebcbc 100644 --- a/tests/ple/neg/BinahUpdate.hs +++ b/tests/ple/neg/BinahUpdate.hs @@ -3,6 +3,7 @@ {-@ LIQUID "--higherorder" @-} {-@ LIQUID "--no-termination" @-} {-@ LIQUID "--ple" @-} +{-@ LIQUID "--ghost-variance=Invariant" @-} {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-} diff --git a/tests/ple/neg/BinahUpdateLib.hs b/tests/ple/neg/BinahUpdateLib.hs index 2f1dc5b6a9..9962356081 100644 --- a/tests/ple/neg/BinahUpdateLib.hs +++ b/tests/ple/neg/BinahUpdateLib.hs @@ -3,6 +3,7 @@ {-@ LIQUID "--higherorder" @-} {-@ LIQUID "--no-termination" @-} {-@ LIQUID "--ple" @-} +{-@ LIQUID "--ghost-variance=Invariant" @-} {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-} diff --git a/tests/ple/neg/BinahUpdateLib1.hs b/tests/ple/neg/BinahUpdateLib1.hs index 3b0ed4b043..8dc26e7ef4 100644 --- a/tests/ple/neg/BinahUpdateLib1.hs +++ b/tests/ple/neg/BinahUpdateLib1.hs @@ -3,6 +3,8 @@ {-@ LIQUID "--higherorder" @-} {-@ LIQUID "--no-termination" @-} {-@ LIQUID "--ple" @-} +{-@ LIQUID "--ghost-variance=Invariant" @-} + {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-} From 97409561cd56ec6743d4a861f84ab9d0de496c9f Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Sat, 6 Mar 2021 11:52:58 +0100 Subject: [PATCH 7/7] unexpectedd fail, but --- tests/neg/Variance1.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/neg/Variance1.hs b/tests/neg/Variance1.hs index c6c028e48c..78486fa3b6 100644 --- a/tests/neg/Variance1.hs +++ b/tests/neg/Variance1.hs @@ -1,3 +1,4 @@ +{-@ LIQUID "--ghost-variance=Invariant" @-} module Variance1 where import Data.Binary