change bivariant to perform no checks

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)

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

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

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)

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

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 
   }
 
 

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

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}]

tests/neg/ExactADT6.hs

@@ -1,5 +1,6 @@
 {-@ LIQUID "--no-adt"         @-}
 {-@ LIQUID "--exact-data-con" @-}
+{-@ LIQUID "--ghost-variance=Invariant" @-}
 
 {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}
 

tests/neg/ExactGADT6.hs

@@ -1,5 +1,6 @@
 {-@ LIQUID "--no-adt"         @-}
 {-@ LIQUID "--exact-data-con" @-}
+{-@ LIQUID "--ghost-variance=Invariant" @-}
 
 {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}
 

tests/neg/RG.hs

@@ -1,4 +1,5 @@
 module RG where
+{-@ LIQUID "--ghost-variance=Invariant" @-}
 
 import Data.IORef as R
 

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

tests/neg/T1657.hs

@@ -1,5 +1,6 @@
 module T1657 where
 
+{-@ data variance I invariant @-}
 {-@ data I <p :: Int -> Bool> = I _ @-}
 data I = I Int
 

tests/neg/T1657A.hs

@@ -1,6 +1,7 @@
 module T1657A where
 
 {-@ data I <pigbert :: Int -> Bool> = I Int @-}
+{-@ data variance I invariant @-}
 
 data I = I Int
 {-@ getI :: forall <pp :: Int -> Bool>. 

tests/neg/Variance1.hs

@@ -1,3 +1,4 @@
+{-@ LIQUID "--ghost-variance=Invariant" @-}
 module Variance1 where
 
 import Data.Binary

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

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 @-}

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 #-}
 

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 }
 

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

tests/test.hs

@@ -80,7 +80,7 @@ main = do unsetEnv "LIQUIDHASKELL_OPTS"
                             errorTests  : 
                             macroTests  :
                             proverTests :
-                            goldenTests :
+--                             goldenTests :
                             benchTests  : 
                             []