diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index 2a0204b4ae..827014f570 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) @@ -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 962d406bf2..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 = (++) <$> 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 @@ -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 _)) @@ -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 38c9bc7b28..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,10 +1842,10 @@ 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 - [] -> Invariant + varSignToVariance a = case filter (\p -> GM.showPpr (fst p) == GM.showPpr a) varsigns of + [] -> Bivariant [(_, b)] -> if b then Covariant else Contravariant - _ -> Bivariant + _ -> Invariant goDCon dc = concatMap (go True) (map irrelevantMult $ Ghc.dataConOrigArgTys dc) 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/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}] 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/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>. 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 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/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 ef826c2139..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 #-} @@ -20,6 +21,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..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 #-} @@ -20,6 +22,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 : []