Support for controlled negative occurrences

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

@@ -93,17 +93,18 @@ 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 targDiagnostics     = Bare.checkTargetSrc cfg bareSpec targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
   let bareSpecDiagnostics = Bare.checkBareSpec bareSpec
-  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of
-   Left d | noErrors d -> secondPhase (allWarnings d)
+  let stratDiagnostics   = Bare.checkStratTys bareSpec targetSrc
+  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics >> stratDiagnostics of
+   Left d | noErrors d -> secondPhase [] (allWarnings d)
    Left d              -> return $ Left d
-   Right ()            -> secondPhase mempty
+   Right stratNames   -> secondPhase stratNames mempty
   where
-    secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
-    secondPhase phaseOneWarns = do
-      diagOrSpec <- makeGhcSpec cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies
+    secondPhase :: [Ghc.Name] -> [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
+    secondPhase stratNames phaseOneWarns = do
+      diagOrSpec <- makeGhcSpec stratNames cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies
       case diagOrSpec of
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
@@ -144,7 +145,8 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
 -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
 --   validates it using @checkGhcSpec@.
 -------------------------------------------------------------------------------------
-makeGhcSpec :: Config
+makeGhcSpec :: [Ghc.Name]
+            -> Config
             -> LogicNameEnv
             -> Bare.LocalVars
             -> GhcSrc
@@ -153,11 +155,11 @@ makeGhcSpec :: Config
             -> [(ModName, Ms.BareSpec)]
             -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
 -------------------------------------------------------------------------------------
-makeGhcSpec cfg lenv localVars src lmap bareSpec dependencySpecs = do
+makeGhcSpec stratNames cfg lenv localVars src lmap bareSpec dependencySpecs = do
   ghcTyLookupEnv <- Bare.makeGHCTyLookupEnv (_giCbs src)
   tcg <- Ghc.getGblEnv
   instEnvs <- Ghc.tcGetInstEnvs
-  (dg0, sp) <- makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs
+  (dg0, sp) <- makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs
   let diagnostics = Bare.checkTargetSpec (bareSpec : map snd dependencySpecs)
                                          (toTargetSrc src)
                                          (ghcSpecEnv sp)
@@ -195,7 +197,8 @@ ghcSpecEnv sp = F.notracepp "RENV" $ fromListSEnv binds
 --   lets us use aliases inside data-constructor definitions.
 -------------------------------------------------------------------------------------
 makeGhcSpec0
-  :: Config
+  :: [Ghc.Name]
+  -> Config
   -> Bare.GHCTyLookupEnv
   -> Ghc.TcGblEnv
   -> Ghc.InstEnvs
@@ -206,7 +209,7 @@ makeGhcSpec0
   -> Ms.BareSpec
   -> [(ModName, Ms.BareSpec)]
   -> Ghc.TcRn (Diagnostics, GhcSpec)
-makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs = do
+makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs = do
   globalRdrEnv <- Ghc.tcg_rdr_env <$> Ghc.getGblEnv
   -- build up environments
   tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier
@@ -223,7 +226,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec de
   -- NB: we first compute a measure environment w/o the opaque reflections, so that we can bootstrap
   -- the signature `sig`. Then we'll add the opaque reflections before we compute `sData` and al.
   let (dg1, measEnv0) = withDiagnostics $ makeMeasEnv      env tycEnv sigEnv       specs
-  let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src)
+  let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig stratNames cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src)
   elaboratedSig <-
     if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
                               >>= elaborateSig sig
@@ -862,10 +865,10 @@ makeAutoInst env spec = S.fromList <$> kvs
 
 
 ----------------------------------------------------------------------------------------
-makeSpecSig :: Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
+makeSpecSig :: [Ghc.Name] -> Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
             -> Bare.Lookup ([RInstance LocBareType], GhcSpecSig)
 ----------------------------------------------------------------------------------------
-makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do
+makeSpecSig stratNames cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do
   mySigs     <- makeTySigs  env sigEnv name mySpec
   aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs
   let asmSigs =  Bare.tcSelVars tycEnv ++ aSigs
@@ -880,6 +883,7 @@ makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do
   asmRel     <-  makeRelation env name sigEnv (Ms.asmRel mySpec)
   return (instances, SpSig
     { gsTySigs   = tySigs
+    , gsStratCtos = stratNames
     , gsAsmSigs  = asmSigs
     , gsAsmReflects = bimap getVar getVar <$> concatMap (asmReflectSigs . snd) allSpecs
     , gsRefSigs  = []

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

@@ -3,16 +3,18 @@
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE RecordWildCards     #-}
 {-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE DeriveTraversable   #-}
+
 {-# OPTIONS_GHC -Wno-x-partial #-}
 
 module Language.Haskell.Liquid.Bare.Check
   ( checkTargetSpec
   , checkBareSpec
   , checkTargetSrc
+  , checkStratTys
   , tyCompat
   ) where
 
-
 import           Language.Haskell.Liquid.Constraint.ToFixpoint
 
 import           Liquid.GHC.API                   as Ghc hiding ( Located
@@ -55,27 +57,90 @@ import qualified Language.Haskell.Liquid.Bare.Resolve      as Bare
 import           Language.Haskell.Liquid.UX.Config
 import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags), solverFlags)
 
-
 ----------------------------------------------------------------------------------------------
 -- | Checking TargetSrc ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------
-checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics ()
-checkTargetSrc cfg spec
+checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics ()
+checkTargetSrc cfg bare spec
   |  nopositivity cfg
   || nopositives == emptyDiagnostics
   = Right ()
   | otherwise
   = Left nopositives
-  where nopositives = checkPositives (gsTcs spec)
+  where nopositives = checkPositives bare $ gsTcs spec
 
+isStratifiedTyCon :: BareSpec -> TyCon -> Bool
+isStratifiedTyCon bs tc = Ghc.tyConName tc `elem` sn
+  where
+    -- (Alecs): For some reason it can't see that they are the same
+    -- GHC name, probably is due to some worker wrapper shenannigans
+    sn = mapMaybe ctorName $ S.toList $ stratified bs
+    ctorName (F.Loc _ _ (LHNResolved (LHRGHC c) _)) = Just c
+    ctorName _                                      = Nothing
 
-checkPositives :: [TyCon] -> Diagnostics
-checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys)
+checkPositives :: BareSpec -> [TyCon] -> Diagnostics
+checkPositives bare tys = mkDiagnostics []
+                        $ mkNonPosError
+                        $ filter (not . isStratifiedTyCon bare . fst)
+                        $ getNonPositivesTyCon tys
 
 mkNonPosError :: [(TyCon, [DataCon])]  -> [Error]
 mkNonPosError tcs = [ ErrPosTyCon (getSrcSpan tc) (pprint tc) (pprint dc <+> ":" <+> pprint (dataConRepType dc))
                     | (tc, dc:_) <- tcs]
 
+--------------------------------------------------
+-- | Checking that stratified ctors are present --
+--------------------------------------------------
+
+data Validation e a
+  = Failure e
+  | Success a
+  deriving (Show, Eq, Functor, Foldable, Traversable)
+
+instance (Semigroup e, Semigroup a) => Semigroup (Validation e a) where
+  Failure e1 <> Failure e2 = Failure (e1 <> e2)
+  Failure e  <> _          = Failure e
+  _          <> Failure e  = Failure e
+  Success x  <> Success y  = Success (x <> y)
+
+instance (Semigroup e, Monoid a) => Monoid (Validation e a) where
+  mempty = Success mempty
+  mappend = (<>)
+
+valToEither :: Validation e a -> Either e a
+valToEither (Failure e) = Left e
+valToEither (Success x) = Right x
+
+checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name]
+checkStratTys bare spec = valToEither
+                        $ foldMap (uncurry $ checkStratTy bare)
+                        $ mapMaybe (locateStratTcs bare) (gsTcs spec)
+
+locateStratTcs :: BareSpec -> TyCon -> Maybe (SrcSpan, TyCon)
+locateStratTcs bs tc = listToMaybe $ mapMaybe ctorName $ S.toList $ stratified bs
+  where
+    ctorName (F.Loc s e (LHNResolved (LHRGHC c) _))
+      | c == Ghc.tyConName tc = Just (GM.sourcePos2SrcSpan s e, tc)
+    ctorName _               = Nothing
+
+checkStratTy :: BareSpec -> SrcSpan -> TyCon -> Validation Diagnostics [Name]
+checkStratTy spec pos tycon =
+  case tyConDataCons_maybe tycon of
+    Just ctors -> foldMap (checkStratCtor tycon spec pos) ctors
+    Nothing    -> Failure $ mkDiagnostics mempty [ err ]
+  where err = ErrStratNotAdt pos (pprint (Ghc.tyConName tycon))
+
+checkStratCtor :: TyCon -> BareSpec -> SrcSpan -> DataCon -> Validation Diagnostics [Name]
+checkStratCtor tcon spec pos datacon
+  | Just nm <- listToMaybe $ mapMaybe (isThisDataCon . val . fst) $ sigs spec
+  = Success [ nm ]
+  | otherwise = Failure $ mkDiagnostics mempty [ err ]
+  where err = ErrStratNotRefCtor pos (pprint $ dataConName datacon) (pprint $ Ghc.tyConName tcon)
+        isThisDataCon (LHNResolved (LHRGHC c) _)
+          | c == dataConName datacon = Just c
+        isThisDataCon _              = Nothing
+
+
 ----------------------------------------------------------------------------------------------
 -- | Checking BareSpec ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------

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,9 @@ 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           Data.Bifunctor                                (first)
 import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe)
 import           Data.Either.Extra                             (eitherToMaybe)
 import qualified Data.HashMap.Strict                           as M
@@ -97,12 +99,110 @@ consAct γ cfg info = do
   hws <- gets hsWfs
   fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
   fws <- concat <$> mapM splitW hws
+  checkStratCtors γ sSpc
   modify $ \st -> st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)
                      , cgLits   = litEnv   γ
                      , cgConsts = cgConsts st `mappend` constEnv γ
                      , fixCs    = fcs
                      , fixWfs   = fws }
 
+
+---------------------------------
+-- | Checking stratified ctors --
+---------------------------------
+type FExpr = F.ExprV F.Symbol
+type FRef  = F.ReftV F.Symbol
+type Ctors = S.HashSet F.Symbol
+
+checkStratCtors :: CGEnv -> GhcSpecSig -> CG ()
+checkStratCtors env sSpc = do
+  let ctors = S.fromList $ M.keys $ F.seBinds $ constEnv env
+  let ctorRefinements = filter (isStrat . fst) $ gsTySigs sSpc
+  forM_ ctorRefinements $ uncurry $ checkCtor ctors
+  where
+    -- (Alecs): For some reason it can't see that they are the same
+    -- GHC name, probably is due to some worker wrapper shenannigans
+    hack = occNameString . nameOccName
+    isStrat nm = hack (varName nm) `elem` map hack (gsStratCtos sSpc)
+
+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
+  retIdx <- case getIndex $ ur_reft $ rt_reft ret of
+    Just idx -> pure idx
+    Nothing  -> uError $ ErrStratNotPropRet loc (pprint tyName) (pprint name) (F.pprint 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 -> FExpr -> SpecType -> CG ()
+checkNg ctors loc ctorName tyName retIdx = go
+  where
+    go :: SpecType -> 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
+      go rt_in
+      go rt_out
+    go r@RApp { rt_tycon = RTyCon { rtc_tc }, rt_args, rt_reft } = do
+      if Ghc.tyConName rtc_tc == tyName then do
+          case getIndex $ ur_reft rt_reft of
+            (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 retIdx) $ do
+                uError $ ErrStratIdxNotSmall loc
+                  (pprint tyName) (pprint ctorName) (F.pprint retIdx) (F.pprint arg)
+            -- We don't have index information for both so we bail
+            _ -> uError $ ErrStratOccProp loc (pprint tyName) (pprint ctorName) (F.pprint r)
+      else do
+        forM_ rt_args go
+    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
+
 --------------------------------------------------------------------------------
 -- | Ensure that the instance type is a subtype of the class type --------------
 --------------------------------------------------------------------------------

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

@@ -899,6 +899,7 @@ data BPspec
   | Insts   (Located LHName)                              -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
   | HMeas   (Located LHName)                              -- ^ 'measure' annotation; lift Haskell binder as measure
   | Reflect (Located LHName)                              -- ^ 'reflect' annotation; reflect Haskell binder as function in logic
+  | Stratified (Located LHName)                           -- ^ 'stratified' annotation; stratification check for type declarations
   | PrivateReflect LocSymbol                              -- ^ 'private-reflect' annotation
   | OpaqueReflect (Located LHName)                        -- ^ 'opaque-reflect' annotation
   | Inline  (Located LHName)                              -- ^ 'inline' annotation;  inline (non-recursive) binder as an alias
@@ -984,6 +985,8 @@ ppPspec k (HMeas   lx)
   = "measure" <+> pprintTidy k (val lx)
 ppPspec k (Reflect lx)
   = "reflect" <+> pprintTidy k (val lx)
+ppPspec k (Stratified lx)
+  = "stratified" <+> pprintTidy k (val lx)
 ppPspec k (PrivateReflect lx)
   = "private-reflect" <+> pprintTidy k (val lx)
 ppPspec k (OpaqueReflect lx)
@@ -1106,6 +1109,7 @@ mkSpec xs = Measure.Spec
   , Measure.rewriteWith = M.fromList [s | Rewritewith s <- xs]
   , Measure.bounds     = M.fromList [(bname i, i) | PBound i <- xs]
   , Measure.reflects   = S.fromList [s | Reflect s <- xs]
+  , Measure.stratified = S.fromList [s | Stratified s <- xs]
   , Measure.privateReflects = S.fromList [s | PrivateReflect s <- xs]
   , Measure.opaqueReflects = S.fromList [s | OpaqueReflect s <- xs]
   , Measure.hmeas      = S.fromList [s | HMeas  s <- xs]
@@ -1129,6 +1133,7 @@ specP
     -- TODO: These next two are synonyms, kill one
     <|> fallbackSpecP "axiomatize"  (fmap Reflect locBinderLHNameP)
     <|> fallbackSpecP "reflect"     (fmap Reflect locBinderLHNameP)
+    <|> fallbackSpecP "stratified"  (fmap Stratified tyConBindLHNameP)
     <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )
     <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  )