WIP support for controlled negative occurrences

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -93,10 +93,9 @@ makeTargetSpec :: Config
                -> TargetDependencies
                -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
 makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
-  let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
   let bareSpecDiagnostics = Bare.checkBareSpec bareSpec
-  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of
+  case depsDiagnostics >> bareSpecDiagnostics of
    Left d | noErrors d -> secondPhase (allWarnings d)
    Left d              -> return $ Left d
    Right ()            -> secondPhase mempty
@@ -109,8 +108,11 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
         Right (warns, ghcSpec) -> do
           let targetSpec = toTargetSpec ghcSpec
               liftedSpec = ghcSpecToLiftedSpec ghcSpec
-          liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
-          return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
+          case Bare.checkTargetSrc cfg targetSrc targetSpec of
+            Right () -> do
+              liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
+              return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
+            Left errors -> return $ Left errors
 
     toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, BareSpec)
     toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), fromBareSpecLHName $ unsafeFromLiftedSpec ls)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs

@@ -59,18 +59,15 @@ import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags), solverFlags)
 ----------------------------------------------------------------------------------------------
 -- | Checking TargetSrc ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------
-checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics ()
-checkTargetSrc cfg spec
-  |  nopositivity cfg
-  || nopositives == emptyDiagnostics
-  = Right ()
-  | otherwise
-  = Left nopositives
-  where nopositives = checkPositives (gsTcs spec)
-
-
-checkPositives :: [TyCon] -> Diagnostics
-checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys)
+checkTargetSrc :: Config -> TargetSrc -> TargetSpec -> Either Diagnostics ()
+checkTargetSrc cfg spec tsp | nopositivity cfg = Right ()
+  | otherwise =
+  let refinedCtors = map Ghc.varName $ filter GM.isDataConId $ map fst $ gsTySigs $ gsSig tsp
+      nopositives = checkPositives (gsTcs spec) (if controlledNegativity cfg then refinedCtors else [])
+  in if nopositives == emptyDiagnostics then Right () else Left nopositives
+
+checkPositives :: [TyCon] -> [Name] -> Diagnostics
+checkPositives tys skippedCtors = mkDiagnostics [] $ mkNonPosError $ getNonPositivesTyCon tys skippedCtors
 
 mkNonPosError :: [(TyCon, [DataCon])]  -> [Error]
 mkNonPosError tcs = [ ErrPosTyCon (getSrcSpan tc) (pprint tc) (pprint dc <+> ":" <+> pprint (dataConRepType dc))

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE MultiParamTypeClasses     #-}
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE ImplicitParams            #-}
+{-# LANGUAGE NamedFieldPuns            #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -28,8 +29,10 @@ import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
 import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
 import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
 import Text.PrettyPrint.HughesPJ ( text )
-import           Control.Monad ( foldM, forM, forM_, when, void )
+import           Control.Monad ( foldM, forM, forM_, when, void, unless)
 import           Control.Monad.State
+import           Control.Monad.Reader
+import           Data.Bifunctor
 import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe)
 import           Data.Either.Extra                             (eitherToMaybe)
 import qualified Data.HashMap.Strict                           as M
@@ -58,6 +61,7 @@ import           Language.Haskell.Liquid.Types.RTypeOp
 import           Language.Haskell.Liquid.Types.RefType
 import           Language.Haskell.Liquid.Types.Specs
 import           Language.Haskell.Liquid.Types.Types hiding (binds)
+import           Language.Haskell.Liquid.Types.Variance
 import           Language.Haskell.Liquid.Constraint.Types
 import           Language.Haskell.Liquid.Constraint.Constraint ( addConstraints )
 import           Language.Haskell.Liquid.Constraint.Template
@@ -70,8 +74,7 @@ import Language.Haskell.Liquid.UX.Config
       Config(typeclass, gradual, checkDerived, extensionality,
              nopolyinfer, noADT, dependantCase, exactDC, rankNTypes),
       patternFlag,
-      higherOrderFlag )
-
+      higherOrderFlag, controlledNegativity, nopositivity)
 --------------------------------------------------------------------------------
 -- | Constraint Generation: Toplevel -------------------------------------------
 --------------------------------------------------------------------------------
@@ -97,6 +100,8 @@ consAct γ cfg info = do
   hws <- gets hsWfs
   fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
   fws <- concat <$> mapM splitW hws
+  -- Alecs: Constraint generation for small negative occurrences
+  when (controlledNegativity cfg && not (nopositivity cfg)) $ checkNegativeConstructors γ sSpc
   modify $ \st -> st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)
                      , cgLits   = litEnv   γ
                      , cgConsts = cgConsts st `mappend` constEnv γ
@@ -115,6 +120,100 @@ consClass γ (x,mt)
 consClass _ _
   = return ()
 
+--- ControlledNegativeity
+
+type FExpr = F.ExprV F.Symbol
+type FRef  = F.ReftV F.Symbol
+type Ctors = S.HashSet F.Symbol
+
+checkNegativeConstructors :: CGEnv -> GhcSpecSig -> CG ()
+checkNegativeConstructors env sSpc = do
+  let ctors = S.fromList $ M.keys $ F.seBinds $ constEnv env
+  let ctorRefinements = filter (GM.isDataConId . fst) $ gsTySigs sSpc
+  forM_ ctorRefinements $ uncurry $ checkCtor ctors
+
+uncurryPi :: SpecType -> ([SpecType], SpecType)
+uncurryPi (RFun _ _ dom cod _) = first (dom :) $ uncurryPi cod
+uncurryPi rest                 = ([], rest)
+
+getIndex :: FRef -> Maybe FExpr
+getIndex (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) to))
+  | n == "Language.Haskell.Liquid.ProofCombinators.prop"
+  , v == v'
+  = Just to
+getIndex _ = Nothing
+
+getTyConName :: SpecType -> Name
+getTyConName a = Ghc.tyConName $ rtc_tc $ rt_tycon a
+
+checkCtor :: Ctors -> Var -> LocSpecType -> CG ()
+checkCtor ctors name typ = do
+  let loc = GM.fSrcSpan $ F.loc typ
+  let (args, ret) = uncurryPi $ val typ
+  -- The constuctor that we want not to appear negatrive
+  let tyName = getTyConName ret
+  -- Its index information
+  let retIdx = getIndex $ ur_reft $ rt_reft ret
+  -- For every argument of the constructor we check that in negative
+  -- position all the self-refernce are refined by a "smaller" `prop`
+  -- annotation
+  forM_ args $ checkNg ctors loc name tyName retIdx
+
+checkNg :: Ctors -> SrcSpan -> Var -> Name -> Maybe FExpr -> SpecType -> CG ()
+checkNg ctors loc ctorName tyName retIdx = flip runReaderT Covariant . go
+  where
+    go :: SpecType -> ReaderT Variance CG ()
+    go RVar {} = pure ()
+    go RAllT { rt_ty } = go rt_ty
+    go RAllP { rt_ty } = go rt_ty
+    go RFun { rt_in, rt_out } = do
+      local (<> Contravariant) $ do
+        go rt_in
+      go rt_out
+    go RApp { rt_tycon = RTyCon { rtc_tc }, rt_args, rt_reft } = do
+      if Ghc.tyConName rtc_tc == tyName then do
+        var <- ask
+        when (var `elem` [ Contravariant, Bivariant ]) $ do
+          -- We are in a possibly engative position
+          let argIdx = getIndex $ ur_reft rt_reft
+          case (retIdx, argIdx) of
+            (Just ret, Just arg) -> do
+              -- We compare index information
+              -- The engativer occurrence is safe iff the index of the
+              -- return type is strictly bigger than the one in negative
+              -- position
+              unless (isStructurallySmaller ctors arg ret) $ do
+                uError $ ErrPosTyCon loc (pprint tyName) (pprint ctorName)
+            -- We don't have index information for both so we bail
+            _ -> uError $ ErrPosTyCon loc (pprint tyName) (pprint ctorName)
+      else do
+        let varInfo = makeTyConVariance rtc_tc
+        forM_ (zip rt_args varInfo) $ \(arg, var) -> do
+          local (<> var) $ go arg
+    go _ = lift $ impossible (Just loc) "checkNg unexpected type"
+
+
+isStructurallySmaller :: Ctors -> FExpr -> FExpr -> Bool
+isStructurallySmaller ctors l r
+  -- Congruence rule
+  | (F.EVar nl, argsl) <- F.splitEAppThroughECst l
+  , (F.EVar nr, argsr) <- F.splitEAppThroughECst r
+  , nl == nr
+  , length argsl == length argsr
+  , nl `elem` ctors
+  = any (uncurry $ isStructurallySmaller ctors) $ zip argsl argsr
+  | otherwise = isSubterm ctors l r && l /= r
+
+isSubterm :: Ctors -> FExpr -> FExpr -> Bool
+isSubterm ctors l r | l == r
+                   = True
+                  -- Congruence rule
+                  | (F.EVar nm, args) <- F.splitEAppThroughECst r
+                  , nm `elem` ctors
+                  = any (isSubterm ctors l) args
+                  | otherwise
+                  = False
+
 --------------------------------------------------------------------------------
 consCBLet :: CGEnv -> CoreBind -> CG CGEnv
 --------------------------------------------------------------------------------

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Play.hs

@@ -11,6 +11,7 @@ import           Control.Arrow       ((***))
 import qualified Data.HashMap.Strict as M
 import qualified Data.List           as L
 import qualified Data.Maybe          as Mb
+import           Data.Bifunctor
 
 import Liquid.GHC.API as Ghc hiding (panic, showPpr)
 import Language.Haskell.Liquid.GHC.Misc ()
@@ -25,15 +26,24 @@ import Language.Haskell.Liquid.Types.Variance
 -- use T in non strictly positive positions, 
 -- then (T,(Di, Dj)) will appear in the result list.  
 
-getNonPositivesTyCon :: [TyCon] -> [(TyCon, [DataCon])]
-getNonPositivesTyCon tcs = Mb.mapMaybe go (M.toList $ makeOccurrences tcs)
+getNonPositivesTyCon :: [TyCon] -> [Name] -> [(TyCon, [DataCon])]
+getNonPositivesTyCon tcs skippedCtors = map skip $ Mb.mapMaybe go (M.toList $ makeOccurrences tcs)
   where
+    skip = second $ filter (not . skipNameUnsafe skippedCtors . Ghc.dataConName)
+
     go (tc,dcocs) = case filter (\(_,occ) -> elem tc (negOcc occ)) dcocs of
                       [] -> Nothing
                       xs -> Just (tc, fst <$> xs)
 
 
 -- OccurrenceMap maps type constructors to their TyConOccurrence. 
+skipNameUnsafe :: [Name] -> Name -> Bool
+skipNameUnsafe skip curr = any (isSameNameUnsafe curr) skip
+  where
+    isSameNameUnsafe :: Name -> Name -> Bool
+    isSameNameUnsafe _a _b = show _a == show _b
+
+
 -- for each of their data constructor. For example, for the below data definition
 -- data T a = P (T a) | N (T a -> Int) | Both (T a -> T a) | None 
 -- the entry below should get generated
@@ -53,7 +63,7 @@ data TyConOccurrence
     = TyConOcc { posOcc :: [TyCon] -- TyCons that occur in positive positions
                , negOcc :: [TyCon] -- TyCons that occur in negative positions
                }
-  deriving Eq
+  deriving (Eq, Show)
 
 instance Monoid TyConOccurrence where
   mempty = TyConOcc mempty mempty

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs

@@ -478,6 +478,10 @@ config = cmdArgsMode $ Config {
     = def &= help "Allow refining constructors with unsafe refinements"
           &= name "allow-unsafe-constructors"
           &= explicit
+  , controlledNegativity
+    = def &= help "Allow negative occurrences in data type declarations as long as they are small"
+          &= name "controlled-negativity"
+          &= explicit
   } &= program "liquid"
     &= help    "Refinement Types for Haskell"
     &= summary copyright
@@ -742,6 +746,7 @@ defConfig = Config
   , dumpOpaqueReflections    = False
   , dumpPreNormalizedCore    = False
   , allowUnsafeConstructors  = False
+  , controlledNegativity     = False
   }
 
 -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs

@@ -125,6 +125,7 @@ data Config = Config
   , dumpOpaqueReflections    :: Bool       -- Dumps all opaque reflections to the stdout
   , dumpPreNormalizedCore    :: Bool       -- Dumps the prenormalized core (before a-normalization)
   , allowUnsafeConstructors  :: Bool       -- ^ Allow refining constructors with unsafe refinements
+  , controlledNegativity     :: Bool
   } deriving (Generic, Data, Show, Eq)
 
 allowPLE :: Config -> Bool