diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 7a26cc1bb0..d01b3df96a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/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  = []
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
index c7c9fa4ec0..08955f308a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/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 ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
index 98c2cb78c4..41344b4dd3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/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 --------------
 --------------------------------------------------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 8c07bcb486..963dca7500 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/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  )
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
index c372ac4c4e..2a288b3dff 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -485,10 +485,41 @@ data TError t =
 
   | ErrCtorRefinement { pos :: !SrcSpan
                       , ctorName :: !Doc
-                      } -- ^ The refinement of a data constructor doesn't admit
-                        -- a refinement on the return type that
-                        -- isn't deemd safe
-
+                      }
+    -- ^ The refinement of a data constructor doesn't admit a
+    -- refinement on the return type that isn't deemd safe
+  | ErrStratNotAdt { pos :: !SrcSpan
+                   , tyName :: !Doc
+                   }
+    -- ^ Type was declared stratified but it is not an ADT
+  | ErrStratNotRefCtor { pos :: !SrcSpan
+                       , ctorName :: !Doc
+                       , tyName :: !Doc
+                       }
+    -- ^ Type was declared stratified but one of its constructors is not a
+    -- refinement constructor (i.e. it has no refinement)
+  | ErrStratNotPropRet { pos :: !SrcSpan
+                       , tyName :: !Doc
+                       , ctorName :: !Doc
+                       , retTy  :: !Doc
+                       }
+    -- ^ Type was declared stratified but one of its constructors does not
+    -- return a Prop type
+  | ErrStratOccProp { pos :: !SrcSpan
+                      , tyName :: !Doc
+                      , ctorName :: !Doc
+                      , tyNR :: !Doc
+                      }
+    -- ^ Type was declared stratified but one of its constructors has a recursive
+    -- occurence that is not a Prop type
+  | ErrStratIdxNotSmall { pos :: !SrcSpan
+                        , tyName :: !Doc
+                        , ctorName :: !Doc
+                        , retIdx :: !Doc
+                        , occIdx :: !Doc
+                        }
+  -- ^ Type was declared stratified but one of its constructors has a recursive
+  -- occurence whose index type is not a smaller
   | ErrOther    { pos   :: SrcSpan
                 , msg   :: !Doc
                 } -- ^ Sigh. Other.
@@ -1072,6 +1103,41 @@ ppError' _ dCtx (ErrCtorRefinement _ ctorName)
         $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?")
         $+$ nest 4 (text "You can disable this error by enabling the flag `--allow-unsafe-constructors`")
 
+ppError' _ dCtx (ErrStratNotAdt _ tyName)
+  = text "The type" <+> tyName
+      <+> "was declared stratified but it is not an algebraic data type"
+      $+$ dCtx
+
+ppError' _ dCtx (ErrStratNotRefCtor _ ctorName tyName)
+  = text "The constructor" <+> ctorName
+      <+> "of the type" <+> tyName
+      <+> "was declared stratified but it is not a refinement constructor (i.e. it has no refinement)"
+      $+$ dCtx
+
+ppError' _ dCtx (ErrStratNotPropRet _ tyName ctorName retTy)
+  = text "The constructor" <+> ctorName
+      <+> "of the type" <+> tyName
+      <+> "was declared stratified but it does not return a Prop type, instead it returns"
+      <+> retTy
+      $+$ dCtx
+
+ppError' _ dCtx (ErrStratOccProp _ tyName ctorName tyNR)
+  = text "The constructor" <+> ctorName
+      <+> "of the type" <+> tyName
+      <+> "was declared stratified but it has a recursive occurence of type"
+      <+> tyNR
+      <+> "which is not a Prop type"
+      $+$ dCtx
+
+ppError' _ dCtx (ErrStratIdxNotSmall _ tyName ctorName retIdx occIdx)
+  = text "The constructor" <+> ctorName
+      <+> "of the type" <+> tyName
+      <+> "was declared stratified but it has a recursive occurence whose index type"
+      <+> occIdx
+      <+> "is not smaller than the return index type"
+      <+> retIdx
+      $+$ dCtx
+
 ppError' _ dCtx (ErrParseAnn _ msg)
   = text "Malformed annotation"
         $+$ dCtx
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index bcb6398114..e10ddcd214 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -243,6 +243,7 @@ data GhcSpecQual = SpQual
 
 data GhcSpecSig = SpSig
   { gsTySigs   :: ![(Var, LocSpecType)]           -- ^ Asserted Reftypes
+  , gsStratCtos :: ![Name]                        -- ^ Stratified Ctors
   , gsAsmSigs  :: ![(Var, LocSpecType)]           -- ^ Assumed Reftypes
   , gsAsmReflects  :: ![(Var, Var)]               -- ^ Assumed Reftypes (left is the actual function name and right the pretended one)
   , gsRefSigs  :: ![(Var, LocSpecType)]           -- ^ Reflected Reftypes
@@ -259,6 +260,7 @@ data GhcSpecSig = SpSig
 instance Semigroup GhcSpecSig where
   x <> y = SpSig
     { gsTySigs   = gsTySigs x   <> gsTySigs y
+    , gsStratCtos = gsStratCtos x <> gsStratCtos y
     , gsAsmSigs  = gsAsmSigs x  <> gsAsmSigs y
     , gsAsmReflects = gsAsmReflects x <> gsAsmReflects y
     , gsRefSigs  = gsRefSigs x  <> gsRefSigs y
@@ -278,7 +280,7 @@ instance Semigroup GhcSpecSig where
 
 
 instance Monoid GhcSpecSig where
-  mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty
+  mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty
 
 data GhcSpecData = SpData
   { gsCtors      :: ![(Var, LocSpecType)]         -- ^ Data Constructor Measure Sigs
@@ -398,6 +400,7 @@ data Spec lname ty = Spec
   , rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules
   , fails      :: !(S.HashSet (F.Located LHName))                     -- ^ These Functions should be unsafe
   , reflects   :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to reflect
+  , stratified :: !(S.HashSet (F.Located LHName))                     -- ^ Type declaration to check for stratification
   , privateReflects :: !(S.HashSet F.LocSymbol)                       -- ^ Private binders to reflect
   , opaqueReflects :: !(S.HashSet (F.Located LHName))                 -- ^ Binders to opaque-reflect
   , autois     :: !(S.HashSet (F.Located LHName))                     -- ^ Automatically instantiate axioms in these Functions
@@ -624,6 +627,7 @@ instance Semigroup (Spec lname ty) where
            , rewriteWith = M.union  (rewriteWith s1)  (rewriteWith s2)
            , fails      = S.union   (fails    s1)  (fails    s2)
            , reflects   = S.union   (reflects s1)  (reflects s2)
+           , stratified = S.union (stratified s1) (stratified s2)
            , privateReflects = S.union (privateReflects s1) (privateReflects s2)
            , opaqueReflects   = S.union   (opaqueReflects s1)  (opaqueReflects s2)
            , hmeas      = S.union   (hmeas    s1)  (hmeas    s2)
@@ -660,6 +664,7 @@ instance Monoid (Spec lname ty) where
            , autois     = S.empty
            , hmeas      = S.empty
            , reflects   = S.empty
+           , stratified = S.empty
            , privateReflects = S.empty
            , opaqueReflects = S.empty
            , inlines    = S.empty
@@ -1012,6 +1017,7 @@ unsafeFromLiftedSpec a = Spec
   , rewrites   = mempty
   , rewriteWith = mempty
   , reflects   = mempty
+  , stratified = mempty
   , privateReflects = liftedPrivateReflects a
   , opaqueReflects   = mempty
   , autois     = liftedAutois a
diff --git a/tests/errors/StratNoPropRec.hs b/tests/errors/StratNoPropRec.hs
new file mode 100644
index 0000000000..79936524e9
--- /dev/null
+++ b/tests/errors/StratNoPropRec.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--expect-error-containing=The constructor Test.VArr of the type Test.Val was declared stratified but it has a recursive occurence of type Test.Val which is not a Prop type" @-}
+module StratNoPropRec where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Ty = TInt | TArr Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+  {-@ VArr :: t1:Ty -> t2:Ty -> (Prop (Val t1) -> Val) -> Prop (Val (TArr t1 t2)) @-}
+  VArr :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty
diff --git a/tests/errors/StratNoPropRet.hs b/tests/errors/StratNoPropRet.hs
new file mode 100644
index 0000000000..027d546e8b
--- /dev/null
+++ b/tests/errors/StratNoPropRet.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--expect-error-containing=The constructor Test.VArr of the type Test.Val was declared stratified but it does not return a Prop type, instead it returns Test.Val" @-}
+module StratNoPropRet where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Ty = TInt | TArr Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+  {-@ VArr :: t1:Ty -> t2:Ty -> (Prop (Val t1) -> Prop (Val t2)) -> Val @-}
+  VArr :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty
diff --git a/tests/errors/StratNoRefCtor.hs b/tests/errors/StratNoRefCtor.hs
new file mode 100644
index 0000000000..cc512ec894
--- /dev/null
+++ b/tests/errors/StratNoRefCtor.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--expect-error-containing=The constructor Test.VInt of the type Test.Val was declared stratified but it is not a refinement constructor (i.e. it has no refinement)" @-}
+module StratNoRefCtor where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Ty = TInt | TArr Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+--  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+  {-@ VArr :: t1:Ty -> t2:Ty -> (Prop (Val t1) -> Prop (Val t2)) -> Prop (Val (TArr t1 t2)) @-}
+  VArr :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty
diff --git a/tests/errors/StratNotAdt.hs b/tests/errors/StratNotAdt.hs
new file mode 100644
index 0000000000..9d1706b9ba
--- /dev/null
+++ b/tests/errors/StratNotAdt.hs
@@ -0,0 +1,5 @@
+{-@ LIQUID "--expect-error-containing=The type Test.Val was declared stratified but it is not an algebraic data type" @-}
+module StratNotAdt where
+
+{-@ stratified Val @-}
+type Val = Int
diff --git a/tests/errors/StratRecOccNotSmall.hs b/tests/errors/StratRecOccNotSmall.hs
new file mode 100644
index 0000000000..1228ad93fb
--- /dev/null
+++ b/tests/errors/StratRecOccNotSmall.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--expect-error-containing=The constructor Test.VArr of the type Test.Val was declared stratified but it has a recursive occurence whose index type Test.Val (Test.TArr t1 t2) is not smaller than the return index type Test.Val (Test.TArr t1 t2)" @-}
+module StratRecOccNotSmall where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Ty = TInt | TArr Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+  {-@ VArr :: t1:Ty -> t2:Ty -> (Prop (Val (TArr t1 t2)) -> Prop (Val t2)) -> Prop (Val (TArr t1 t2)) @-}
+  VArr :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty
diff --git a/tests/ple/pos/SKILam.hs b/tests/ple/pos/SKILam.hs
index 2f8c379f01..07496bda24 100644
--- a/tests/ple/pos/SKILam.hs
+++ b/tests/ple/pos/SKILam.hs
@@ -54,8 +54,7 @@ tlen (Lam _ _ _ t)     = 1 + tlen t
 tlen (Var _ _ _)       = 0
 
 
--- VFun function is non positive idk how to fix
-{-@ LIQUID "--no-positivity-check" @-}
+{-@ stratified Value @-}
 data Value where
   {-@ VIota :: Int -> Prop (Value Iota) @-}
   VIota :: Int -> Value
diff --git a/tests/pos/StratVal.hs b/tests/pos/StratVal.hs
new file mode 100644
index 0000000000..2b959c9c5e
--- /dev/null
+++ b/tests/pos/StratVal.hs
@@ -0,0 +1,13 @@
+module StratVal where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Ty = TInt | TArr Ty Ty
+
+{-@ stratified Val @-}
+data Val where
+  {-@ VInt :: Int -> Prop (Val TInt) @-}
+  VInt :: Int -> Val
+  {-@ VArr :: t1:Ty -> t2:Ty -> (Prop (Val t1) -> Prop (Val t2)) -> Prop (Val (TArr t1 t2)) @-}
+  VArr :: Ty -> Ty -> (Val -> Val) -> Val
+data VAL = Val Ty