Merge pull request #2559 from AlecsFerra/develop

Support for controlled negative occurrences

Author: nikivazou

docs/mkDocs/docs/specifications.md

@@ -47,6 +47,9 @@ of each here.
 * `{-@ <binding-signature-with-refinement-type> @-}` introduces a refinement type for the named Haskell definition.
     * For a function, the refinements become pre and post conditions for the functions use.
     * This is probably the most used Liquid Haskell annotation!
+* `{-@ stratified <data-type-declaration> @-}` the datatype is treated as a stratified type by the well-definedness checker.
+  ([Jump to: Stratified Types](http://ucsd-progsys.github.io/liquidhaskell/specifications/#stratified-types))
+
 
 The following sections detail more variety for the uses of the above annotations.
 
@@ -1123,3 +1126,63 @@ safeDiv x y
 ```
 
 In this example, the `lazyvar` annotation on `help` ensures that the check for `help` is deferred until it is used. Without this annotation, LiquidHaskell would incorrectly report an error like `Error: Liquid Type Mismatch`.
+
+## Stratified Types
+
+Liquid Haskell disallows arbitrary user-defined data types, since some
+can be used to derive inconsistencies in the refinement logic.
+
+```haskell
+data Evil a = Very (Evil a -> a)
+
+{-@ type Bot = {v:() | false} @-}
+
+{-@ bad :: Evil Bot -> Bot @-}
+bad :: Evil () -> ()
+bad (Very f) = f (Very f)
+
+{-@ worse :: Bot @-}
+worse :: ()
+worse = bad (Very bad)
+```
+
+This definition is rejected by Liquid Haskell’s [positivity
+checker](https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check),
+which enforces that recursive occurrences of a data type only appear
+in **positive** positions (to the right of function arrows).
+Positivity is a *sufficient* condition for logical consistency but not
+a *necessary* one. Some definitions that fail the positivity check are
+still well-founded and consistent. A class of those are **stratified
+types**.
+
+### Definition
+
+A **stratified type** is a data type refined with `Prop` from
+`Language.Haskell.Liquid.ProofCombinators`, where all recursive
+occurrences of the type:
+- appear under `Prop`, and
+- are indexed by **strictly smaller** values than the index of the
+  constructor itself.
+
+This controlled form of non positive types preserves consistency while
+allowing more expressive data definitions.
+
+### Example
+
+The following defines values of the simply typed lambda calculus as a
+stratified type:
+
+```haskell
+data Ty = TInt | TFun Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+
+  {-@ VFun :: t1:Ty -> t2:Ty
+           -> (Prop (Val t1) -> Prop (Val t2))
+           -> Prop (Val (TFun t1 t2)) @-}
+  VFun :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty
+```

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,101 @@ 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 sn = mapMaybe (getLHGHCName . F.val) $ S.toList $ stratified bs
 
-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 --
+--------------------------------------------------
+
+--- | Like 'Either' but the 'Semigroup' instance combines the failure
+--- | values.
+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
+
+-- | Check that all stratified types have their constructors
+-- defined with refinement type signatures in the BareSpec.
+--
+-- Yields the names of the data constructors of the stratified types.
+checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name]
+checkStratTys bare spec =
+  valToEither
+  $ foldMap (checkStratTy bare)
+  $ mapMaybe (traverse (findTyCon (gsTcs spec)))
+  $ S.toList $ stratified bare
+
+-- | Find the TyCon corresponding to the given LHName in the given list of TyCons
+findTyCon :: [TyCon] -> LHName -> Maybe TyCon
+findTyCon tcs nm = do
+  c <- getLHGHCName nm
+  L.find ((== c) . Ghc.tyConName) tcs
+
+-- | Check that the given TyCon is an ADT and that all its constructors
+-- have refinements in the BareSpec.
+checkStratTy :: BareSpec -> Located TyCon -> Validation Diagnostics [Name]
+checkStratTy spec ltycon =
+  case tyConDataCons_maybe (val ltycon) of
+    Just ctors -> foldMap (checkStratCtor ltycon spec) ctors
+    Nothing    -> Failure $ mkDiagnostics mempty [ err ]
+  where
+    pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon)
+    err = ErrStratNotAdt pos (pprint (Ghc.tyConName $ val ltycon))
+
+-- | Check that the given DataCon has a refinement type signature in the BareSpec.
+--
+-- Yields the names of the data constructors that are stratified.
+checkStratCtor :: Located TyCon -> BareSpec -> DataCon -> Validation Diagnostics [Name]
+checkStratCtor ltycon spec datacon
+  | hasRefinementTypeSignature datacon (map (val . fst) $ sigs spec)
+  = Success [ dataConName datacon ]
+  | otherwise = Failure $ mkDiagnostics mempty [ err ]
+  where
+    pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon)
+    err = ErrStratNotRefCtor pos (pprint $ dataConName datacon) (pprint $ Ghc.tyConName $ val ltycon)
+    hasRefinementTypeSignature :: DataCon -> [LHName] -> Bool
+    hasRefinementTypeSignature dc lns =
+      dataConName dc `elem` mapMaybe getLHGHCName lns
+
+
 ----------------------------------------------------------------------------------------------
 -- | Checking BareSpec ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------
@@ -223,11 +299,7 @@ checkConstructorRefinement = mconcat . map checkOne
     validRef (F.Reft (_, F.PTrue))
                       = True
     -- Prop foo from ProofCombinators
-    validRef (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) _))
-      | n == "Language.Haskell.Liquid.ProofCombinators.prop"
-      , v == v'
-      = True
-    validRef _ = False
+    validRef n = isJust $ getPropIndex n
 
     isCtorName x = case idDetails x of
       DataConWorkId _ -> True