Support for controlled negative occurrences

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,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 ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------