From 8be96431f4dc3090b47a5535a951cd6cc98269bd Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Mon, 16 Dec 2019 17:07:38 -0500
Subject: [PATCH 1/9] identifying `undefined` not working

---
 .../Haskell/Liquid/Constraint/Generate.hs       |  5 ++++-
 src/Language/Haskell/Liquid/Constraint/Monad.hs | 10 ++++++++++
 src/Language/Haskell/Liquid/GHC/Play.hs         | 17 +++++++++++++++--
 src/Language/Haskell/Liquid/Types/Errors.hs     | 11 +++++++++++
 src/Language/Haskell/Liquid/UX/CmdLine.hs       | 14 ++++++++++++++
 src/Language/Haskell/Liquid/UX/Config.hs        | 10 ++++++++++
 6 files changed, 64 insertions(+), 3 deletions(-)

diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
index 81719966b1..591c713207 100644
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -64,7 +64,7 @@ import           Language.Haskell.Liquid.Constraint.Env
 import           Language.Haskell.Liquid.Constraint.Monad
 import           Language.Haskell.Liquid.Constraint.Split
 import           Language.Haskell.Liquid.Types.Dictionaries
-import           Language.Haskell.Liquid.GHC.Play          (isHoleVar) 
+import           Language.Haskell.Liquid.GHC.Play          (isHoleVar, isUnsafeVar) 
 import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
 import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
 import           Language.Haskell.Liquid.Types                 hiding (binds, Loc, loc, Def)
@@ -674,6 +674,9 @@ cconsE' γ e@(Cast e' c) t
   = do t' <- castTy γ (exprType e) e' c
        addC (SubC γ t' t) ("cconsE Cast: " ++ GM.showPpr e)
 
+cconsE' γ (Var x) t | isUnsafeVar x && detectUnsafe (getConfig γ)
+  = addUnsafeWarning x t γ
+
 cconsE' γ (Var x) t | isHoleVar x && typedHoles (getConfig γ)
   = addHole x t γ 
 
diff --git a/src/Language/Haskell/Liquid/Constraint/Monad.hs b/src/Language/Haskell/Liquid/Constraint/Monad.hs
index e66b3a7e04..e9efafaf38 100644
--- a/src/Language/Haskell/Liquid/Constraint/Monad.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Monad.hs
@@ -108,6 +108,16 @@ addHole x t γ = do
       env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
       x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
 
+-- TODO: Make this a warning instead of an error. FIXME XXX
+addUnsafeWarning :: Var -> SpecType -> CGEnv -> CG () 
+addUnsafeWarning x t γ = do 
+  addWarning $ ErrUnsafe loc (reGlobal env <> reLocal env) x' t
+    where 
+      loc   = srcSpan $ cgLoc γ
+      env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
+      x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
+    
+
 --------------------------------------------------------------------------------
 -- | Update annotations for a location, due to (ghost) predicate applications
 --------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/GHC/Play.hs b/src/Language/Haskell/Liquid/GHC/Play.hs
index 5d8bd89cba..5dad66f5b3 100644
--- a/src/Language/Haskell/Liquid/GHC/Play.hs
+++ b/src/Language/Haskell/Liquid/GHC/Play.hs
@@ -3,15 +3,17 @@
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE PatternSynonyms           #-}
+{-# LANGUAGE TemplateHaskell           #-}
 
 module Language.Haskell.Liquid.GHC.Play where
 
 import Prelude hiding (error)
-import GHC
 import CoreSyn
+import DataCon
+import GHC
+import qualified PrelNames as GHC
 import Var
 import TyCoRep hiding (substTysWith)
-import DataCon
 
 import TyCon
 import Type      (tyConAppArgs_maybe, tyConAppTyCon_maybe, binderVar)
@@ -20,14 +22,25 @@ import PrelNames (isStringClassName)
 import           Control.Arrow       ((***))
 import qualified Data.HashMap.Strict as M
 import qualified Data.List           as L
+-- import qualified Data.Set            as Set
 
 import Language.Haskell.Liquid.GHC.Misc ()
 import Language.Haskell.Liquid.Types.Errors
 
+import Debug.Trace
 
 isHoleVar :: Var -> Bool 
 isHoleVar x = L.isPrefixOf "_" (show x)
 
+isUnsafeVar :: Var -> Bool
+isUnsafeVar x = (varUnique $ trace (show (varUnique x) ++ ": " ++ show x) x) `L.elem` traceShowId unsafeList
+  where
+    unsafeList = [ GHC.undefinedKey]
+-- TODO: How can we get the `Var` for arbitrary variables? FIXME XXX
+-- isUnsafeVar x = x `Set.member` unsafeList
+--   where
+--     unsafeList = Set.fromList ['undefined]
+
 dataConImplicitIds :: DataCon -> [Id]
 dataConImplicitIds dc = [ x | AnId x <- dataConImplicitTyThings dc]
 
diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs
index ea40c142a0..b6a9758709 100644
--- a/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -223,6 +223,13 @@ data TError t =
                , texp :: !t
                } -- ^ liquid type error
 
+  | ErrUnsafe  { pos :: !SrcSpan
+               -- , msg :: !Doc
+               , ctx :: !(M.HashMap Symbol t)
+               , var :: !Doc 
+               , thl :: !t 
+               } -- ^ unsound behavior warning
+
   | ErrHole    { pos :: !SrcSpan
                , msg :: !Doc
                , ctx :: !(M.HashMap Symbol t)
@@ -734,6 +741,10 @@ ppError' td dSp dCtx err@(ErrSubType _ _ _ _ tE)
         $+$ text "Your function is not total: not all patterns are defined." 
         $+$ hint err -- "Hint: Use \"--no-totality\" to deactivate totality checking."
 
+ppError' _td dSp _dCtx (ErrUnsafe _ _ x t)
+  = dSp <+> "Unsafe function used"
+        $+$ pprint x <+> "::" <+> pprint t 
+
 ppError' _td dSp _dCtx (ErrHole _ _ _ x t)
   = dSp <+> "Hole Found"
         $+$ pprint x <+> "::" <+> pprint t 
diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs
index 9489a61e68..e59afa563c 100644
--- a/src/Language/Haskell/Liquid/UX/CmdLine.hs
+++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs
@@ -349,6 +349,18 @@ config = cmdArgsMode $ Config {
     = def 
         &= name "typed-holes"
         &= help "Use (refinement) typed-holes [currently warns on '_x' variables]"
+
+  -- JP: cmdargs is adding two dashes (--) in front of warning arguments... Perhaps use `enum`? FIXME XXX
+  , warnDetectUnsafe
+    = def
+        &= name "Wdetect-unsafe"
+        &= help "Detect unsafe behavior "
+        &= explicit
+  , warnNoDetectUnsafe
+    = def
+        &= name "Wno-detect-unsafe"
+        &= help "Do not detect unsafe behavior. Overridden by -Wdetect-unsafe."
+        &= explicit
   } &= verbosity
     &= program "liquid"
     &= help    "Refinement Types for Haskell"
@@ -578,6 +590,8 @@ defConfig = Config
   , compileSpec       = False
   , noCheckImports    = False
   , typedHoles        = False
+  , warnDetectUnsafe   = False
+  , warnNoDetectUnsafe = False
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs
index 6e95a143ef..e5b78f1ec3 100644
--- a/src/Language/Haskell/Liquid/UX/Config.hs
+++ b/src/Language/Haskell/Liquid/UX/Config.hs
@@ -7,6 +7,7 @@ module Language.Haskell.Liquid.UX.Config (
      Config (..)
    , HasConfig (..)
    , allowPLE, allowLocalPLE, allowGlobalPLE
+   , detectUnsafe
    , patternFlag
    , higherOrderFlag
    , pruneFlag
@@ -89,6 +90,8 @@ data Config = Config
   , compileSpec     :: Bool        -- ^ Only "compile" the spec -- into .bspec file -- don't do any checking. 
   , noCheckImports  :: Bool        -- ^ Do not check the transitive imports  
   , typedHoles      :: Bool        -- ^ Warn about "typed-holes"
+  , warnDetectUnsafe :: Bool       -- ^ Detect unsafe behavior.
+  , warnNoDetectUnsafe :: Bool     -- ^ Do not detect unsafe behavior.
   } deriving (Generic, Data, Typeable, Show, Eq)
 
 instance Serialize SMTSolver
@@ -148,3 +151,10 @@ terminationCheck' cfg = (totalHaskell cfg || not (notermination cfg))
 structuralTerm :: (HasConfig a) => a -> Bool 
 structuralTerm = not . nostructuralterm . getConfig
 
+detectUnsafe :: (HasConfig a) => a -> Bool 
+detectUnsafe a 
+  | warnDetectUnsafe c   = True
+  | warnNoDetectUnsafe c = False
+  | otherwise            = True
+    where
+        c = getConfig a

From d47ef30d035535b92a352461c64f844d51be8e2b Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 18 Dec 2019 11:43:51 -0500
Subject: [PATCH 2/9] Detect lazy and assumed refinements. Temporarily detect
 `undefined` with string hack

---
 .../Haskell/Liquid/Constraint/Generate.hs     |   5 +-
 .../Haskell/Liquid/Constraint/Monad.hs        |   9 --
 src/Language/Haskell/Liquid/GHC/Interface.hs  |  51 ++++++++
 src/Language/Haskell/Liquid/GHC/Play.hs       |  13 +-
 src/Language/Haskell/Liquid/Types/Errors.hs   | 115 +++++++++++++++---
 5 files changed, 160 insertions(+), 33 deletions(-)

diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
index 591c713207..81719966b1 100644
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -64,7 +64,7 @@ import           Language.Haskell.Liquid.Constraint.Env
 import           Language.Haskell.Liquid.Constraint.Monad
 import           Language.Haskell.Liquid.Constraint.Split
 import           Language.Haskell.Liquid.Types.Dictionaries
-import           Language.Haskell.Liquid.GHC.Play          (isHoleVar, isUnsafeVar) 
+import           Language.Haskell.Liquid.GHC.Play          (isHoleVar) 
 import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
 import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
 import           Language.Haskell.Liquid.Types                 hiding (binds, Loc, loc, Def)
@@ -674,9 +674,6 @@ cconsE' γ e@(Cast e' c) t
   = do t' <- castTy γ (exprType e) e' c
        addC (SubC γ t' t) ("cconsE Cast: " ++ GM.showPpr e)
 
-cconsE' γ (Var x) t | isUnsafeVar x && detectUnsafe (getConfig γ)
-  = addUnsafeWarning x t γ
-
 cconsE' γ (Var x) t | isHoleVar x && typedHoles (getConfig γ)
   = addHole x t γ 
 
diff --git a/src/Language/Haskell/Liquid/Constraint/Monad.hs b/src/Language/Haskell/Liquid/Constraint/Monad.hs
index e9efafaf38..3509332e92 100644
--- a/src/Language/Haskell/Liquid/Constraint/Monad.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Monad.hs
@@ -108,15 +108,6 @@ addHole x t γ = do
       env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
       x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
 
--- TODO: Make this a warning instead of an error. FIXME XXX
-addUnsafeWarning :: Var -> SpecType -> CGEnv -> CG () 
-addUnsafeWarning x t γ = do 
-  addWarning $ ErrUnsafe loc (reGlobal env <> reLocal env) x' t
-    where 
-      loc   = srcSpan $ cgLoc γ
-      env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
-      x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
-    
 
 --------------------------------------------------------------------------------
 -- | Update annotations for a location, due to (ghost) predicate applications
diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index 32f6f369cf..cdcbb06956 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -433,8 +433,59 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d
   bareSpecs  <- makeBareSpecs cfg depGraph specEnv     modSum bareSpec
   let ghcSpec = makeGhcSpec   cfg ghcSrc   logicMap           bareSpecs  
   _          <- liftIO $ saveLiftedSpec ghcSrc ghcSpec 
+  runWarnings cfg $ checkWarnings cfg bareSpec ghcSrc -- JP: Not sure if this is the right spot for this.
   return      $ GI ghcSrc ghcSpec
 
+-- runWarnings :: 
+-- TODO: Check for Werror and throw warnings
+-- runWarnings cfg warnings | warningToError cfg = 
+runWarnings _ warnings = liftIO $ mapM_ (putStrLn . showpp) warnings
+
+-- JP: Separate Warning type?
+checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TError Doc]
+checkWarnings cfg bareSpec ghcSrc = unsafeWarnings
+  where
+    unsafeWarnings = if detectUnsafe cfg then
+        checkUnsafeWarning bareSpec ghcSrc
+      else
+        mempty
+
+checkUnsafeWarning :: Ms.BareSpec -> GhcSrc -> [TError Doc]
+checkUnsafeWarning bareSpec ghcSrc = 
+       checkUnsafeAssume bareSpec
+    <> checkUnsafeLazy bareSpec
+    <> checkUnsafeVar ghcSrc
+  where
+    checkUnsafeAssume bareSpec = 
+        let toWarning (ls, lt) =
+              -- let span = srcSpan ls in TODO: How do we get a GHC src span?
+              let span = noSrcSpan in
+              ErrUnsafeAssumed span (pprint ls) (pprint lt)
+        in
+        map toWarning $ asmSigs bareSpec
+    
+    checkUnsafeLazy bareSpec = 
+        let toWarning ls =
+              -- let span = srcSpan ls in TODO: How do we get a GHC src span?
+              let span = noSrcSpan in
+              ErrUnsafeLazy span (pprint ls) -- (pprint lt)
+        in
+        map toWarning $ S.toList $ lazy bareSpec
+
+    checkUnsafeVar ghcSrc = 
+        let cbs = giCbs ghcSrc in
+        concatMap checkUnsafeVarCB cbs
+        
+    checkUnsafeVarCB (NonRec x e) = checkUnsafeVarCB' x e
+    checkUnsafeVarCB (Rec xes)    = concatMap (uncurry checkUnsafeVarCB') xes
+
+    checkUnsafeVarCB' x e = 
+        let vars = readVars e in
+        let unsafeVars = filter isUnsafeVar vars in
+        map (\unsafeVar -> ErrUnsafeVar noSrcSpan (pprint x) (pprint unsafeVar)) unsafeVars
+        -- TODO: How do we get a src span?
+
+
 ---------------------------------------------------------------------------------------
 -- | @makeGhcSrc@ builds all the source-related information needed for consgen 
 ---------------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/GHC/Play.hs b/src/Language/Haskell/Liquid/GHC/Play.hs
index 5dad66f5b3..bf6a784164 100644
--- a/src/Language/Haskell/Liquid/GHC/Play.hs
+++ b/src/Language/Haskell/Liquid/GHC/Play.hs
@@ -11,7 +11,7 @@ import Prelude hiding (error)
 import CoreSyn
 import DataCon
 import GHC
-import qualified PrelNames as GHC
+-- import qualified PrelNames as GHC
 import Var
 import TyCoRep hiding (substTysWith)
 
@@ -22,20 +22,23 @@ import PrelNames (isStringClassName)
 import           Control.Arrow       ((***))
 import qualified Data.HashMap.Strict as M
 import qualified Data.List           as L
--- import qualified Data.Set            as Set
+import qualified Data.Set            as Set
 
 import Language.Haskell.Liquid.GHC.Misc ()
 import Language.Haskell.Liquid.Types.Errors
 
-import Debug.Trace
+-- import Debug.Trace
 
 isHoleVar :: Var -> Bool 
 isHoleVar x = L.isPrefixOf "_" (show x)
 
 isUnsafeVar :: Var -> Bool
-isUnsafeVar x = (varUnique $ trace (show (varUnique x) ++ ": " ++ show x) x) `L.elem` traceShowId unsafeList
+isUnsafeVar x = show x `Set.member` unsafeList
   where
-    unsafeList = [ GHC.undefinedKey]
+    unsafeList = Set.fromList ["GHC.Err.undefined"]
+-- isUnsafeVar x = (varUnique $ trace (show (varUnique x) ++ ": " ++ show x) x) `L.elem` traceShowId unsafeList
+--   where
+--     unsafeList = [ GHC.undefinedKey]
 -- TODO: How can we get the `Var` for arbitrary variables? FIXME XXX
 -- isUnsafeVar x = x `Set.member` unsafeList
 --   where
diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs
index b6a9758709..442000fe58 100644
--- a/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -223,12 +223,27 @@ data TError t =
                , texp :: !t
                } -- ^ liquid type error
 
-  | ErrUnsafe  { pos :: !SrcSpan
-               -- , msg :: !Doc
-               , ctx :: !(M.HashMap Symbol t)
-               , var :: !Doc 
-               , thl :: !t 
-               } -- ^ unsound behavior warning
+  | ErrUnsafeAssumed  { pos :: !SrcSpan
+                      -- , msg :: !Doc
+                      -- , ctx :: !(M.HashMap Symbol t)
+                      , var :: !Doc 
+                      , thl :: !t 
+                      } -- ^ unsound behavior warning
+
+  | ErrUnsafeLazy  { pos :: !SrcSpan
+                   -- , msg :: !Doc
+                   -- , ctx :: !(M.HashMap Symbol t)
+                   , var :: !Doc 
+                   -- , thl :: !t 
+                   } -- ^ unsound behavior warning
+
+  | ErrUnsafeVar  { pos :: !SrcSpan
+                  -- , msg :: !Doc
+                  -- , ctx :: !(M.HashMap Symbol t)
+                  , var :: !Doc 
+                  , unsafeVar :: !Doc 
+                  -- , thl :: !t 
+                  } -- ^ unsound behavior warning
 
   | ErrHole    { pos :: !SrcSpan
                , msg :: !Doc
@@ -449,6 +464,58 @@ data TError t =
   
   deriving (Typeable, Generic , Functor )
 
+-- | Whether an error is a warning.
+-- JP: It might make sense to make a separate Warning type.
+errIsWarning :: TError t -> Bool
+errIsWarning ErrSubType{} = False
+errIsWarning ErrSubTypeModel{} = False
+errIsWarning ErrFCrash{} = False
+errIsWarning ErrUnsafeAssumed{} = True
+errIsWarning ErrUnsafeLazy{} = True
+errIsWarning ErrUnsafeVar{} = True
+errIsWarning ErrHole{} = False
+errIsWarning ErrAssType{} = False
+errIsWarning ErrParse{} = False
+errIsWarning ErrTySpec{} = False
+errIsWarning ErrTermSpec{} = False
+errIsWarning ErrDupAlias{} = False
+errIsWarning ErrDupSpecs{} = False
+errIsWarning ErrDupIMeas{} = False
+errIsWarning ErrDupMeas{} = False
+errIsWarning ErrDupField{} = False
+errIsWarning ErrDupNames{} = False
+errIsWarning ErrBadData{} = False
+errIsWarning ErrBadGADT{} = False
+errIsWarning ErrDataCon{} = False
+errIsWarning ErrInvt{} = False
+errIsWarning ErrIAl{} = False
+errIsWarning ErrIAlMis{} = False
+errIsWarning ErrMeas{} = False
+errIsWarning ErrHMeas{} = False
+errIsWarning ErrUnbound{} = False
+errIsWarning ErrUnbPred{} = False
+errIsWarning ErrGhc{} = False
+errIsWarning ErrResolve{} = False
+errIsWarning ErrMismatch{} = False
+errIsWarning ErrPartPred{} = False
+errIsWarning ErrAliasCycle{} = False
+errIsWarning ErrIllegalAliasApp{} = False
+errIsWarning ErrAliasApp{} = False
+errIsWarning ErrTermin{} = False
+errIsWarning ErrStTerm{} = False
+errIsWarning ErrILaw{} = False
+errIsWarning ErrRClass{} = False
+errIsWarning ErrMClass{} = False
+errIsWarning ErrBadQual{} = False
+errIsWarning ErrSaved{} = False
+errIsWarning ErrFilePragma{} = False
+errIsWarning ErrTyCon{} = False
+errIsWarning ErrLiftExp{} = False
+errIsWarning ErrParseAnn{} = False
+errIsWarning ErrNoSpec{} = False
+errIsWarning ErrOther{} = False
+
+
 errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t
 errDupSpecs d spans@(sp:_) = ErrDupSpecs sp d spans
 errDupSpecs _ _            = impossible Nothing "errDupSpecs with empty spans!"
@@ -573,7 +640,11 @@ ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
 --------------------------------------------------------------------------------
 ppError k dCtx e = ppError' k dSp dCtx e
   where
-    dSp          = pprint (pos e) <-> text ": Error:"
+    dSp          = pprint (pos e) <-> text errText
+    errText      = if errIsWarning e then
+                     ": Warning:"
+                   else
+                     ": Error:"
 
 nests :: Foldable t => Int -> t Doc -> Doc
 nests n      = foldr (\d acc -> nest n (d $+$ acc)) empty
@@ -720,11 +791,16 @@ totalityType td tE = pprintTidy td tE == text "{VV : Addr# | 5 < 4}"
 hint :: TError a -> Doc 
 hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e) 
   where 
-    go (ErrMismatch {}) = Just "Use the hole '_' instead of the mismatched component (in the Liquid specification)"
-    go (ErrBadGADT {})  = Just "Use the hole '_' to specify the type of the constructor" 
-    go (ErrSubType {})  = Just "Use \"--no-totality\" to deactivate totality checking."
-    go (ErrNoSpec {})   = Just "Run 'liquid' on the source file first."
-    go _                = Nothing 
+    go (ErrMismatch {})       = Just "Use the hole '_' instead of the mismatched component (in the Liquid specification)"
+    go (ErrBadGADT {})        = Just "Use the hole '_' to specify the type of the constructor" 
+    go (ErrSubType {})        = Just "Use \"--no-totality\" to deactivate totality checking."
+    go (ErrNoSpec {})         = Just "Run 'liquid' on the source file first."
+    go (ErrUnsafeLazy {})     = Just unsafeHint
+    go (ErrUnsafeAssumed {})  = Just unsafeHint
+    go (ErrUnsafeVar {})      = Just unsafeHint
+    go _                      = Nothing 
+
+    unsafeHint = "Enabled by \"-Wdetect-error\""
 
 --------------------------------------------------------------------------------
 ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
@@ -741,9 +817,18 @@ ppError' td dSp dCtx err@(ErrSubType _ _ _ _ tE)
         $+$ text "Your function is not total: not all patterns are defined." 
         $+$ hint err -- "Hint: Use \"--no-totality\" to deactivate totality checking."
 
-ppError' _td dSp _dCtx (ErrUnsafe _ _ x t)
-  = dSp <+> "Unsafe function used"
-        $+$ pprint x <+> "::" <+> pprint t 
+ppError' _td dSp _dCtx err@(ErrUnsafeAssumed _ x t)
+  = dSp <+> "The refinement type for `" <+> pprint x <+> "` is assumed, which is unsafe."
+        $+$ text "assume" <+> pprint x <+> "::" <+> pprint t 
+        $+$ hint err
+
+ppError' _td dSp _dCtx err@(ErrUnsafeLazy _ x)
+  = dSp <+> "`" <+> pprint x <+> "` is declared as lazy, which is unsafe."
+        $+$ hint err
+
+ppError' _td dSp _dCtx err@(ErrUnsafeVar _ x unsafeX)
+  = dSp <+> "`" <+> pprint unsafeX <+> "` is used in `" <+> pprint x <+> "`, which is unsafe."
+        $+$ hint err
 
 ppError' _td dSp _dCtx (ErrHole _ _ _ x t)
   = dSp <+> "Hole Found"

From 72a2f77af9e869cc0187ded16f9af06966bf0ca1 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 18 Dec 2019 13:23:31 -0500
Subject: [PATCH 3/9] Werror flag

---
 src/Language/Haskell/Liquid/GHC/Interface.hs | 7 +++----
 src/Language/Haskell/Liquid/UX/CmdLine.hs    | 6 ++++++
 src/Language/Haskell/Liquid/UX/Config.hs     | 1 +
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index cdcbb06956..f2d67e4bfd 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -436,10 +436,9 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d
   runWarnings cfg $ checkWarnings cfg bareSpec ghcSrc -- JP: Not sure if this is the right spot for this.
   return      $ GI ghcSrc ghcSpec
 
--- runWarnings :: 
--- TODO: Check for Werror and throw warnings
--- runWarnings cfg warnings | warningToError cfg = 
-runWarnings _ warnings = liftIO $ mapM_ (putStrLn . showpp) warnings
+runWarnings :: Config -> [TError Doc] -> Ghc ()
+runWarnings cfg warnings | wError cfg = mapM_ throw warnings -- JP: Can we show all the warnings?
+runWarnings _   warnings              = liftIO $ mapM_ (putStrLn . showpp) warnings
 
 -- JP: Separate Warning type?
 checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TError Doc]
diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs
index e59afa563c..37f9b9cb8d 100644
--- a/src/Language/Haskell/Liquid/UX/CmdLine.hs
+++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs
@@ -361,6 +361,11 @@ config = cmdArgsMode $ Config {
         &= name "Wno-detect-unsafe"
         &= help "Do not detect unsafe behavior. Overridden by -Wdetect-unsafe."
         &= explicit
+  , wError
+    = def
+        &= name "Werror"
+        &= help "Make warnings fatal."
+        &= explicit
   } &= verbosity
     &= program "liquid"
     &= help    "Refinement Types for Haskell"
@@ -592,6 +597,7 @@ defConfig = Config
   , typedHoles        = False
   , warnDetectUnsafe   = False
   , warnNoDetectUnsafe = False
+  , wError = False
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs
index e5b78f1ec3..0a2a9ca0a4 100644
--- a/src/Language/Haskell/Liquid/UX/Config.hs
+++ b/src/Language/Haskell/Liquid/UX/Config.hs
@@ -92,6 +92,7 @@ data Config = Config
   , typedHoles      :: Bool        -- ^ Warn about "typed-holes"
   , warnDetectUnsafe :: Bool       -- ^ Detect unsafe behavior.
   , warnNoDetectUnsafe :: Bool     -- ^ Do not detect unsafe behavior.
+  , wError          :: Bool        -- ^ Make warnings fatal.
   } deriving (Generic, Data, Typeable, Show, Eq)
 
 instance Serialize SMTSolver

From 0f5952d73592188ae80df042ddc16233ddcf446f Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 18 Dec 2019 15:35:33 -0500
Subject: [PATCH 4/9] tests not working

---
 tests/test.hs              | 2 ++
 tests/unsafe/neg/Assume.hs | 7 +++++++
 tests/unsafe/neg/Lazy.hs   | 7 +++++++
 tests/unsafe/neg/Var.hs    | 6 ++++++
 tests/unsafe/neg/Var1.hs   | 6 ++++++
 5 files changed, 28 insertions(+)
 create mode 100644 tests/unsafe/neg/Assume.hs
 create mode 100644 tests/unsafe/neg/Lazy.hs
 create mode 100644 tests/unsafe/neg/Var.hs
 create mode 100644 tests/unsafe/neg/Var1.hs

diff --git a/tests/test.hs b/tests/test.hs
index e30cb41ea4..eea116aa79 100644
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -249,6 +249,8 @@ microTests = group "Micro"
   , mkMicro "class-laws-neg"   "tests/class-laws/neg"   (ExitFailure 1)
   , mkMicro "implicit-pos"   "tests/implicit/pos"    ExitSuccess
   , mkMicro "implicit-neg"   "tests/implicit/neg"   (ExitFailure 1)
+  -- , mkMicro "unsafe-pos"        "tests/unsafe/pos"         ExitSuccess
+  , mkMicro "unsafe-neg"        "tests/unsafe/neg"         (ExitFailure 1)
   -- RJ: disabling because broken by adt PR #1068
   -- , testGroup "gradual/pos"    <$> dirTests "tests/gradual/pos"                    []                ExitSuccess
   -- , testGroup "gradual/neg"    <$> dirTests "tests/gradual/neg"                    []                (ExitFailure 1)
diff --git a/tests/unsafe/neg/Assume.hs b/tests/unsafe/neg/Assume.hs
new file mode 100644
index 0000000000..10b929eb5e
--- /dev/null
+++ b/tests/unsafe/neg/Assume.hs
@@ -0,0 +1,7 @@
+{-# LIQUID "--Werror" #-}
+
+module Assume where
+
+{-@ assume f :: () @-}
+f :: ()
+f = ()
diff --git a/tests/unsafe/neg/Lazy.hs b/tests/unsafe/neg/Lazy.hs
new file mode 100644
index 0000000000..0ec503fe5b
--- /dev/null
+++ b/tests/unsafe/neg/Lazy.hs
@@ -0,0 +1,7 @@
+{-# LIQUID "--Werror" #-}
+
+module Lazy where
+
+{-@ lazy f @-}
+f :: ()
+f = ()
diff --git a/tests/unsafe/neg/Var.hs b/tests/unsafe/neg/Var.hs
new file mode 100644
index 0000000000..ecf2f4f85f
--- /dev/null
+++ b/tests/unsafe/neg/Var.hs
@@ -0,0 +1,6 @@
+{-# LIQUID "--Werror" #-}
+
+module Var where
+
+g :: ()
+g = undefined
diff --git a/tests/unsafe/neg/Var1.hs b/tests/unsafe/neg/Var1.hs
new file mode 100644
index 0000000000..c8a8beb323
--- /dev/null
+++ b/tests/unsafe/neg/Var1.hs
@@ -0,0 +1,6 @@
+{-# LIQUID "--Werror" #-}
+
+module Var1 where
+
+h :: ()
+h = let x = undefined in x

From db00b91091f6077cd24856eaf8932b3a5c2751ab Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 18 Dec 2019 16:25:59 -0500
Subject: [PATCH 5/9] maybe fixed tests

---
 tests/unsafe/neg/Assume.hs | 2 +-
 tests/unsafe/neg/Lazy.hs   | 2 +-
 tests/unsafe/neg/Var.hs    | 2 +-
 tests/unsafe/neg/Var1.hs   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/unsafe/neg/Assume.hs b/tests/unsafe/neg/Assume.hs
index 10b929eb5e..5d115bc1dc 100644
--- a/tests/unsafe/neg/Assume.hs
+++ b/tests/unsafe/neg/Assume.hs
@@ -1,4 +1,4 @@
-{-# LIQUID "--Werror" #-}
+{-@ LIQUID "--Werror" @-}
 
 module Assume where
 
diff --git a/tests/unsafe/neg/Lazy.hs b/tests/unsafe/neg/Lazy.hs
index 0ec503fe5b..cb0e75a2f0 100644
--- a/tests/unsafe/neg/Lazy.hs
+++ b/tests/unsafe/neg/Lazy.hs
@@ -1,4 +1,4 @@
-{-# LIQUID "--Werror" #-}
+{-@ LIQUID "--Werror" @-}
 
 module Lazy where
 
diff --git a/tests/unsafe/neg/Var.hs b/tests/unsafe/neg/Var.hs
index ecf2f4f85f..bdc1528eb5 100644
--- a/tests/unsafe/neg/Var.hs
+++ b/tests/unsafe/neg/Var.hs
@@ -1,4 +1,4 @@
-{-# LIQUID "--Werror" #-}
+{-@ LIQUID "--Werror" @-}
 
 module Var where
 
diff --git a/tests/unsafe/neg/Var1.hs b/tests/unsafe/neg/Var1.hs
index c8a8beb323..3b7b046ec4 100644
--- a/tests/unsafe/neg/Var1.hs
+++ b/tests/unsafe/neg/Var1.hs
@@ -1,4 +1,4 @@
-{-# LIQUID "--Werror" #-}
+{-@ LIQUID "--Werror" @-}
 
 module Var1 where
 

From d131f5e2a90675b67447933487694c8c9f5fae8b Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 18 Dec 2019 17:35:37 -0500
Subject: [PATCH 6/9] move warnings to separate type. Display hint for -Werror

---
 liquidhaskell.cabal                           |   1 +
 src/Language/Haskell/Liquid/GHC/Interface.hs  |  14 +-
 src/Language/Haskell/Liquid/Types/Errors.hs   | 195 ++++++------------
 src/Language/Haskell/Liquid/Types/Types.hs    |   5 +
 src/Language/Haskell/Liquid/Types/Warnings.hs | 117 +++++++++++
 5 files changed, 193 insertions(+), 139 deletions(-)
 create mode 100644 src/Language/Haskell/Liquid/Types/Warnings.hs

diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
index 6758667c1a..6e8974eaa2 100644
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -142,6 +142,7 @@ library
                       Language.Haskell.Liquid.Types.Types
                       Language.Haskell.Liquid.Types.Variance
                       Language.Haskell.Liquid.Types.Visitors
+                      Language.Haskell.Liquid.Types.Warnings
                       Language.Haskell.Liquid.UX.ACSS
                       Language.Haskell.Liquid.UX.Annotate
                       Language.Haskell.Liquid.UX.CTags
diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index f2d67e4bfd..dbee94fe4d 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -436,12 +436,12 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d
   runWarnings cfg $ checkWarnings cfg bareSpec ghcSrc -- JP: Not sure if this is the right spot for this.
   return      $ GI ghcSrc ghcSpec
 
-runWarnings :: Config -> [TError Doc] -> Ghc ()
-runWarnings cfg warnings | wError cfg = mapM_ throw warnings -- JP: Can we show all the warnings?
+runWarnings :: Config -> [TWarning Doc] -> Ghc ()
+runWarnings cfg warnings | wError cfg = mapM_ (\w -> throw $ ErrWError (wrnPos w) w) warnings -- JP: Can we show all the warnings?
 runWarnings _   warnings              = liftIO $ mapM_ (putStrLn . showpp) warnings
 
 -- JP: Separate Warning type?
-checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TError Doc]
+checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TWarning Doc]
 checkWarnings cfg bareSpec ghcSrc = unsafeWarnings
   where
     unsafeWarnings = if detectUnsafe cfg then
@@ -449,7 +449,7 @@ checkWarnings cfg bareSpec ghcSrc = unsafeWarnings
       else
         mempty
 
-checkUnsafeWarning :: Ms.BareSpec -> GhcSrc -> [TError Doc]
+checkUnsafeWarning :: Ms.BareSpec -> GhcSrc -> [TWarning Doc]
 checkUnsafeWarning bareSpec ghcSrc = 
        checkUnsafeAssume bareSpec
     <> checkUnsafeLazy bareSpec
@@ -459,7 +459,7 @@ checkUnsafeWarning bareSpec ghcSrc =
         let toWarning (ls, lt) =
               -- let span = srcSpan ls in TODO: How do we get a GHC src span?
               let span = noSrcSpan in
-              ErrUnsafeAssumed span (pprint ls) (pprint lt)
+              WrnUnsafeAssumed span (pprint ls) (pprint lt)
         in
         map toWarning $ asmSigs bareSpec
     
@@ -467,7 +467,7 @@ checkUnsafeWarning bareSpec ghcSrc =
         let toWarning ls =
               -- let span = srcSpan ls in TODO: How do we get a GHC src span?
               let span = noSrcSpan in
-              ErrUnsafeLazy span (pprint ls) -- (pprint lt)
+              WrnUnsafeLazy span (pprint ls) -- (pprint lt)
         in
         map toWarning $ S.toList $ lazy bareSpec
 
@@ -481,7 +481,7 @@ checkUnsafeWarning bareSpec ghcSrc =
     checkUnsafeVarCB' x e = 
         let vars = readVars e in
         let unsafeVars = filter isUnsafeVar vars in
-        map (\unsafeVar -> ErrUnsafeVar noSrcSpan (pprint x) (pprint unsafeVar)) unsafeVars
+        map (\unsafeVar -> WrnUnsafeVar noSrcSpan (pprint x) (pprint unsafeVar)) unsafeVars
         -- TODO: How do we get a src span?
 
 
diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs
index 442000fe58..6b412f6490 100644
--- a/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -64,15 +64,15 @@ import           Data.Aeson                   hiding (Result)
 import qualified Data.HashMap.Strict          as M
 import qualified Data.List                    as L 
 import           System.Directory
-import           System.FilePath
 import           Text.PrettyPrint.HughesPJ 
 import           Text.Parsec.Error            (ParseError)
 import           Text.Parsec.Error            (errorMessages, showErrorMessages)
 
 import           Language.Fixpoint.Types      (pprint, showpp, Tidy (..), PPrint (..), Symbol, Expr)
 import qualified Language.Fixpoint.Misc       as Misc
-import qualified Language.Haskell.Liquid.Misc     as Misc 
+import qualified Language.Haskell.Liquid.Misc as Misc 
 import           Language.Haskell.Liquid.Misc ((<->))
+import           Language.Haskell.Liquid.Types.Warnings
 
 instance PPrint ParseError where
   pprintTidy _ e = vcat $ tail $ text <$> ls
@@ -223,28 +223,6 @@ data TError t =
                , texp :: !t
                } -- ^ liquid type error
 
-  | ErrUnsafeAssumed  { pos :: !SrcSpan
-                      -- , msg :: !Doc
-                      -- , ctx :: !(M.HashMap Symbol t)
-                      , var :: !Doc 
-                      , thl :: !t 
-                      } -- ^ unsound behavior warning
-
-  | ErrUnsafeLazy  { pos :: !SrcSpan
-                   -- , msg :: !Doc
-                   -- , ctx :: !(M.HashMap Symbol t)
-                   , var :: !Doc 
-                   -- , thl :: !t 
-                   } -- ^ unsound behavior warning
-
-  | ErrUnsafeVar  { pos :: !SrcSpan
-                  -- , msg :: !Doc
-                  -- , ctx :: !(M.HashMap Symbol t)
-                  , var :: !Doc 
-                  , unsafeVar :: !Doc 
-                  -- , thl :: !t 
-                  } -- ^ unsound behavior warning
-
   | ErrHole    { pos :: !SrcSpan
                , msg :: !Doc
                , ctx :: !(M.HashMap Symbol t)
@@ -462,58 +440,60 @@ data TError t =
                 , msg   :: !Doc
                 } -- ^ Sigh. Other.
   
+  | ErrWError   { pos        :: SrcSpan
+                , errWarning :: TWarning t
+                }
+  
   deriving (Typeable, Generic , Functor )
 
--- | Whether an error is a warning.
--- JP: It might make sense to make a separate Warning type.
-errIsWarning :: TError t -> Bool
-errIsWarning ErrSubType{} = False
-errIsWarning ErrSubTypeModel{} = False
-errIsWarning ErrFCrash{} = False
-errIsWarning ErrUnsafeAssumed{} = True
-errIsWarning ErrUnsafeLazy{} = True
-errIsWarning ErrUnsafeVar{} = True
-errIsWarning ErrHole{} = False
-errIsWarning ErrAssType{} = False
-errIsWarning ErrParse{} = False
-errIsWarning ErrTySpec{} = False
-errIsWarning ErrTermSpec{} = False
-errIsWarning ErrDupAlias{} = False
-errIsWarning ErrDupSpecs{} = False
-errIsWarning ErrDupIMeas{} = False
-errIsWarning ErrDupMeas{} = False
-errIsWarning ErrDupField{} = False
-errIsWarning ErrDupNames{} = False
-errIsWarning ErrBadData{} = False
-errIsWarning ErrBadGADT{} = False
-errIsWarning ErrDataCon{} = False
-errIsWarning ErrInvt{} = False
-errIsWarning ErrIAl{} = False
-errIsWarning ErrIAlMis{} = False
-errIsWarning ErrMeas{} = False
-errIsWarning ErrHMeas{} = False
-errIsWarning ErrUnbound{} = False
-errIsWarning ErrUnbPred{} = False
-errIsWarning ErrGhc{} = False
-errIsWarning ErrResolve{} = False
-errIsWarning ErrMismatch{} = False
-errIsWarning ErrPartPred{} = False
-errIsWarning ErrAliasCycle{} = False
-errIsWarning ErrIllegalAliasApp{} = False
-errIsWarning ErrAliasApp{} = False
-errIsWarning ErrTermin{} = False
-errIsWarning ErrStTerm{} = False
-errIsWarning ErrILaw{} = False
-errIsWarning ErrRClass{} = False
-errIsWarning ErrMClass{} = False
-errIsWarning ErrBadQual{} = False
-errIsWarning ErrSaved{} = False
-errIsWarning ErrFilePragma{} = False
-errIsWarning ErrTyCon{} = False
-errIsWarning ErrLiftExp{} = False
-errIsWarning ErrParseAnn{} = False
-errIsWarning ErrNoSpec{} = False
-errIsWarning ErrOther{} = False
+
+-- -- | Whether an error should display the position.
+displayPos :: TError t -> Bool
+displayPos ErrSubType{} = True
+displayPos ErrSubTypeModel{} = True
+displayPos ErrFCrash{} = True
+displayPos ErrHole{} = True
+displayPos ErrAssType{} = True
+displayPos ErrParse{} = True
+displayPos ErrTySpec{} = True
+displayPos ErrTermSpec{} = True
+displayPos ErrDupAlias{} = True
+displayPos ErrDupSpecs{} = True
+displayPos ErrDupIMeas{} = True
+displayPos ErrDupMeas{} = True
+displayPos ErrDupField{} = True
+displayPos ErrDupNames{} = True
+displayPos ErrBadData{} = True
+displayPos ErrBadGADT{} = True
+displayPos ErrDataCon{} = True
+displayPos ErrInvt{} = True
+displayPos ErrIAl{} = True
+displayPos ErrIAlMis{} = True
+displayPos ErrMeas{} = True
+displayPos ErrHMeas{} = True
+displayPos ErrUnbound{} = True
+displayPos ErrUnbPred{} = True
+displayPos ErrGhc{} = True
+displayPos ErrResolve{} = True
+displayPos ErrMismatch{} = True
+displayPos ErrPartPred{} = True
+displayPos ErrAliasCycle{} = True
+displayPos ErrIllegalAliasApp{} = True
+displayPos ErrAliasApp{} = True
+displayPos ErrTermin{} = True
+displayPos ErrStTerm{} = True
+displayPos ErrILaw{} = True
+displayPos ErrRClass{} = True
+displayPos ErrMClass{} = True
+displayPos ErrBadQual{} = True
+displayPos ErrSaved{} = True
+displayPos ErrFilePragma{} = True
+displayPos ErrTyCon{} = True
+displayPos ErrLiftExp{} = True
+displayPos ErrParseAnn{} = True
+displayPos ErrNoSpec{} = True
+displayPos ErrOther{} = True
+displayPos ErrWError{} = False
 
 
 errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t
@@ -556,41 +536,6 @@ dropModel m = case m of
   NoModel t     -> t
   WithModel _ t -> t
 
-instance PPrint SrcSpan where
-  pprintTidy _ = pprSrcSpan
-
-pprSrcSpan :: SrcSpan -> Doc
-pprSrcSpan (UnhelpfulSpan s) = text $ unpackFS s
-pprSrcSpan (RealSrcSpan s)   = pprRealSrcSpan s
-
-pprRealSrcSpan :: RealSrcSpan -> Doc
-pprRealSrcSpan span
-  | sline == eline && scol == ecol =
-    hcat [ pathDoc <-> colon
-         , int sline <-> colon
-         , int scol
-         ]
-  | sline == eline =
-    hcat $ [ pathDoc <-> colon
-           , int sline <-> colon
-           , int scol
-           ] ++ if ecol - scol <= 1 then [] else [char '-' <-> int (ecol - 1)]
-  | otherwise =
-    hcat [ pathDoc <-> colon
-         , parens (int sline <-> comma <-> int scol)
-         , char '-'
-         , parens (int eline <-> comma <-> int ecol')
-         ]
- where
-   path  = srcSpanFile      span
-   sline = srcSpanStartLine span
-   eline = srcSpanEndLine   span
-   scol  = srcSpanStartCol  span
-   ecol  = srcSpanEndCol    span
-
-   pathDoc = text $ normalise $ unpackFS path
-   ecol'   = if ecol == 0 then ecol else ecol - 1
-
 instance Show UserError where
   show = showpp
 
@@ -640,11 +585,10 @@ ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
 --------------------------------------------------------------------------------
 ppError k dCtx e = ppError' k dSp dCtx e
   where
-    dSp          = pprint (pos e) <-> text errText
-    errText      = if errIsWarning e then
-                     ": Warning:"
-                   else
-                     ": Error:"
+    dSp = if displayPos e then
+        pprint (pos e) <-> text ": Error:"
+      else
+        mempty
 
 nests :: Foldable t => Int -> t Doc -> Doc
 nests n      = foldr (\d acc -> nest n (d $+$ acc)) empty
@@ -795,13 +739,9 @@ hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e)
     go (ErrBadGADT {})        = Just "Use the hole '_' to specify the type of the constructor" 
     go (ErrSubType {})        = Just "Use \"--no-totality\" to deactivate totality checking."
     go (ErrNoSpec {})         = Just "Run 'liquid' on the source file first."
-    go (ErrUnsafeLazy {})     = Just unsafeHint
-    go (ErrUnsafeAssumed {})  = Just unsafeHint
-    go (ErrUnsafeVar {})      = Just unsafeHint
+    go (ErrWError {})         = Just "Warning made fatal by \"-Werror\"."
     go _                      = Nothing 
 
-    unsafeHint = "Enabled by \"-Wdetect-error\""
-
 --------------------------------------------------------------------------------
 ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
 --------------------------------------------------------------------------------
@@ -817,19 +757,6 @@ ppError' td dSp dCtx err@(ErrSubType _ _ _ _ tE)
         $+$ text "Your function is not total: not all patterns are defined." 
         $+$ hint err -- "Hint: Use \"--no-totality\" to deactivate totality checking."
 
-ppError' _td dSp _dCtx err@(ErrUnsafeAssumed _ x t)
-  = dSp <+> "The refinement type for `" <+> pprint x <+> "` is assumed, which is unsafe."
-        $+$ text "assume" <+> pprint x <+> "::" <+> pprint t 
-        $+$ hint err
-
-ppError' _td dSp _dCtx err@(ErrUnsafeLazy _ x)
-  = dSp <+> "`" <+> pprint x <+> "` is declared as lazy, which is unsafe."
-        $+$ hint err
-
-ppError' _td dSp _dCtx err@(ErrUnsafeVar _ x unsafeX)
-  = dSp <+> "`" <+> pprint unsafeX <+> "` is used in `" <+> pprint x <+> "`, which is unsafe."
-        $+$ hint err
-
 ppError' _td dSp _dCtx (ErrHole _ _ _ x t)
   = dSp <+> "Hole Found"
         $+$ pprint x <+> "::" <+> pprint t 
@@ -1084,6 +1011,10 @@ ppError' _ dSp dCtx (ErrParseAnn _ msg)
   = dSp <+> text "Malformed annotation"
         $+$ dCtx
         $+$ nest 4 msg
+ppError' t dSp dCtx e@(ErrWError _ w)
+  = dSp <+> ppWarning t dCtx w
+        $+$ hint e
+            
 
 ppTicks :: PPrint a => a -> Doc
 ppTicks = ticks . pprint 
diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs
index 32f61ec947..a3ea9b91d0 100644
--- a/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/src/Language/Haskell/Liquid/Types/Types.hs
@@ -182,6 +182,9 @@ module Language.Haskell.Liquid.Types.Types (
   , Error
   , ErrorResult
 
+  -- * Warnings
+  , module Language.Haskell.Liquid.Types.Warnings
+
   -- * Source information (associated with constraints)
   , Cinfo (..)
 
@@ -271,6 +274,7 @@ import qualified Language.Fixpoint.Types as F
 
 import           Language.Haskell.Liquid.GHC.Misc
 import           Language.Haskell.Liquid.Types.Variance
+import           Language.Haskell.Liquid.Types.Warnings
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Misc
 import           Language.Haskell.Liquid.UX.Config
@@ -1850,6 +1854,7 @@ type ErrorResult    = F.FixResult UserError
 type Error          = TError SpecType
 
 
+instance NFData a => NFData (TWarning a)
 instance NFData a => NFData (TError a)
 
 --------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Types/Warnings.hs b/src/Language/Haskell/Liquid/Types/Warnings.hs
new file mode 100644
index 0000000000..7e3181b048
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Types/Warnings.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE DeriveFunctor       #-}
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE OverloadedStrings   #-}
+
+module Language.Haskell.Liquid.Types.Warnings (
+  -- * Warning Type
+    TWarning(..)
+
+  -- * Printing Warnings
+  , ppWarning
+  , ppWarning'
+  ) where
+
+import           FastString
+import           SrcLoc                      
+import           Text.PrettyPrint.HughesPJ 
+
+import           Data.Typeable                (Typeable)
+import           GHC.Generics
+import           System.FilePath              (normalise)
+
+import           Language.Fixpoint.Types      (pprint, Tidy (..), PPrint (..))
+import           Language.Haskell.Liquid.Misc ((<->))
+
+ppWarning :: (PPrint a, Show a) => Tidy -> Doc -> TWarning a -> Doc
+ppWarning k dCtx e = 
+            ppWarning' k dSp dCtx e
+        $+$ hint e
+  where
+    dSp          = pprint (wrnPos e) <-> text ": Warning:"
+
+
+data TWarning t =
+    WrnUnsafeAssumed  { wrnPos :: !SrcSpan
+                      -- , msg :: !Doc
+                      -- , ctx :: !(M.HashMap Symbol t)
+                      , wrnVar :: !Doc 
+                      , wrnThl :: !t 
+                      } -- ^ unsound behavior warning
+
+  | WrnUnsafeLazy  { wrnPos :: !SrcSpan
+                   -- , msg :: !Doc
+                   -- , ctx :: !(M.HashMap Symbol t)
+                   , wrnVar :: !Doc 
+                   -- , thl :: !t 
+                   } -- ^ unsound behavior warning
+
+  | WrnUnsafeVar  { wrnPos :: !SrcSpan
+                  -- , msg :: !Doc
+                  -- , ctx :: !(M.HashMap Symbol t)
+                  , wrnVar :: !Doc 
+                  , wrnUnsafeVar :: !Doc 
+                  -- , thl :: !t 
+                  } -- ^ unsound behavior warning
+
+  deriving (Typeable, Generic , Functor )
+
+ppWarning' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TWarning a -> Doc
+ppWarning' _td dSp _dCtx err@(WrnUnsafeAssumed _ x t)
+  = dSp <+> "The refinement type for `" <-> pprint x <-> "` is assumed, which is unsafe."
+        $+$ text "assume" <-> pprint x <-> "::" <+> pprint t 
+
+ppWarning' _td dSp _dCtx err@(WrnUnsafeLazy _ x)
+  = dSp <+> "`" <-> pprint x <-> "` is declared as lazy, which is unsafe."
+
+ppWarning' _td dSp _dCtx err@(WrnUnsafeVar _ x unsafeX)
+  = dSp <+> "`" <-> pprint unsafeX <-> "` is used in `" <+> pprint x <+> "`, which is unsafe."
+
+hint :: TWarning a -> Doc 
+hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e) 
+  where
+    go (WrnUnsafeLazy {})     = Just unsafeHint
+    go (WrnUnsafeAssumed {})  = Just unsafeHint
+    go (WrnUnsafeVar {})      = Just unsafeHint
+    -- go _                      = Nothing 
+
+    unsafeHint = "Enabled by \"-Wdetect-error\"."
+
+
+instance PPrint SrcSpan where
+  pprintTidy _ = pprSrcSpan
+
+pprSrcSpan :: SrcSpan -> Doc
+pprSrcSpan (UnhelpfulSpan s) = text $ unpackFS s
+pprSrcSpan (RealSrcSpan s)   = pprRealSrcSpan s
+
+pprRealSrcSpan :: RealSrcSpan -> Doc
+pprRealSrcSpan span
+  | sline == eline && scol == ecol =
+    hcat [ pathDoc <-> colon
+         , int sline <-> colon
+         , int scol
+         ]
+  | sline == eline =
+    hcat $ [ pathDoc <-> colon
+           , int sline <-> colon
+           , int scol
+           ] ++ if ecol - scol <= 1 then [] else [char '-' <-> int (ecol - 1)]
+  | otherwise =
+    hcat [ pathDoc <-> colon
+         , parens (int sline <-> comma <-> int scol)
+         , char '-'
+         , parens (int eline <-> comma <-> int ecol')
+         ]
+ where
+   path  = srcSpanFile      span
+   sline = srcSpanStartLine span
+   eline = srcSpanEndLine   span
+   scol  = srcSpanStartCol  span
+   ecol  = srcSpanEndCol    span
+
+   pathDoc = text $ normalise $ unpackFS path
+   ecol'   = if ecol == 0 then ecol else ecol - 1
+
+instance PPrint (TWarning Doc) where
+  pprintTidy k = ppWarning k empty . fmap (pprintTidy Lossy)

From 5abc33b5002422e75064a30f59b10cced83f8a12 Mon Sep 17 00:00:00 2001
From: James Parker <dev@jamesparker.me>
Date: Thu, 19 Dec 2019 10:46:29 -0500
Subject: [PATCH 7/9] srcspan for lazy and assume

---
 src/Language/Haskell/Liquid/GHC/Interface.hs  |  7 ++-----
 src/Language/Haskell/Liquid/Types/Errors.hs   |  2 +-
 src/Language/Haskell/Liquid/Types/Warnings.hs | 18 +++++++++---------
 3 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index dbee94fe4d..66e2f4ab25 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -440,7 +440,6 @@ runWarnings :: Config -> [TWarning Doc] -> Ghc ()
 runWarnings cfg warnings | wError cfg = mapM_ (\w -> throw $ ErrWError (wrnPos w) w) warnings -- JP: Can we show all the warnings?
 runWarnings _   warnings              = liftIO $ mapM_ (putStrLn . showpp) warnings
 
--- JP: Separate Warning type?
 checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TWarning Doc]
 checkWarnings cfg bareSpec ghcSrc = unsafeWarnings
   where
@@ -457,16 +456,14 @@ checkUnsafeWarning bareSpec ghcSrc =
   where
     checkUnsafeAssume bareSpec = 
         let toWarning (ls, lt) =
-              -- let span = srcSpan ls in TODO: How do we get a GHC src span?
-              let span = noSrcSpan in
+              let span = fSrcSpan ls in
               WrnUnsafeAssumed span (pprint ls) (pprint lt)
         in
         map toWarning $ asmSigs bareSpec
     
     checkUnsafeLazy bareSpec = 
         let toWarning ls =
-              -- let span = srcSpan ls in TODO: How do we get a GHC src span?
-              let span = noSrcSpan in
+              let span = fSrcSpan ls in
               WrnUnsafeLazy span (pprint ls) -- (pprint lt)
         in
         map toWarning $ S.toList $ lazy bareSpec
diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs
index 6b412f6490..715c68bffd 100644
--- a/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -739,7 +739,7 @@ hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e)
     go (ErrBadGADT {})        = Just "Use the hole '_' to specify the type of the constructor" 
     go (ErrSubType {})        = Just "Use \"--no-totality\" to deactivate totality checking."
     go (ErrNoSpec {})         = Just "Run 'liquid' on the source file first."
-    go (ErrWError {})         = Just "Warning made fatal by \"-Werror\"."
+    go (ErrWError {})         = Just "Warning made fatal by \"--Werror\"."
     go _                      = Nothing 
 
 --------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Types/Warnings.hs b/src/Language/Haskell/Liquid/Types/Warnings.hs
index 7e3181b048..970a8ebf51 100644
--- a/src/Language/Haskell/Liquid/Types/Warnings.hs
+++ b/src/Language/Haskell/Liquid/Types/Warnings.hs
@@ -57,25 +57,25 @@ data TWarning t =
   deriving (Typeable, Generic , Functor )
 
 ppWarning' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TWarning a -> Doc
-ppWarning' _td dSp _dCtx err@(WrnUnsafeAssumed _ x t)
-  = dSp <+> "The refinement type for `" <-> pprint x <-> "` is assumed, which is unsafe."
-        $+$ text "assume" <-> pprint x <-> "::" <+> pprint t 
+ppWarning' _td dSp _dCtx (WrnUnsafeAssumed _ x t)
+  = dSp $+$ "The refinement type for `" <-> pprint x <-> "` is assumed, which is unsafe."
+        $+$ text "assume" <+> pprint x <+> "::" <+> pprint t 
 
-ppWarning' _td dSp _dCtx err@(WrnUnsafeLazy _ x)
-  = dSp <+> "`" <-> pprint x <-> "` is declared as lazy, which is unsafe."
+ppWarning' _td dSp _dCtx (WrnUnsafeLazy _ x)
+  = dSp $+$ "`" <-> pprint x <-> "` is declared as lazy, which is unsafe."
 
-ppWarning' _td dSp _dCtx err@(WrnUnsafeVar _ x unsafeX)
-  = dSp <+> "`" <-> pprint unsafeX <-> "` is used in `" <+> pprint x <+> "`, which is unsafe."
+ppWarning' _td dSp _dCtx (WrnUnsafeVar _ x unsafeX)
+  = dSp $+$ "`" <-> pprint unsafeX <-> "` is used in `" <-> pprint x <-> "`, which is unsafe."
 
 hint :: TWarning a -> Doc 
-hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e) 
+hint e = maybe empty (\d -> "" $+$ ("INFO:" <+> d)) (go e) 
   where
     go (WrnUnsafeLazy {})     = Just unsafeHint
     go (WrnUnsafeAssumed {})  = Just unsafeHint
     go (WrnUnsafeVar {})      = Just unsafeHint
     -- go _                      = Nothing 
 
-    unsafeHint = "Enabled by \"-Wdetect-error\"."
+    unsafeHint = "Enabled by \"--Wdetect-unsafe\"."
 
 
 instance PPrint SrcSpan where

From 40f7126faf9930e936f5f0bbea41094792d85afa Mon Sep 17 00:00:00 2001
From: James Parker <dev@jamesparker.me>
Date: Thu, 19 Dec 2019 15:23:34 -0500
Subject: [PATCH 8/9] span for unsafe Vars

---
 src/Language/Haskell/Liquid/GHC/Interface.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index 66e2f4ab25..02551a220d 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -478,8 +478,10 @@ checkUnsafeWarning bareSpec ghcSrc =
     checkUnsafeVarCB' x e = 
         let vars = readVars e in
         let unsafeVars = filter isUnsafeVar vars in
-        map (\unsafeVar -> WrnUnsafeVar noSrcSpan (pprint x) (pprint unsafeVar)) unsafeVars
-        -- TODO: How do we get a src span?
+        map (\unsafeVar -> 
+            let span = Ghc.getSrcSpan x in
+            WrnUnsafeVar span (pprint x) (pprint unsafeVar)
+          ) unsafeVars
 
 
 ---------------------------------------------------------------------------------------

From 3f3f8b210b47c2df0639fd770e56b2cc7d4507d0 Mon Sep 17 00:00:00 2001
From: James Parker <dev@jamesparker.me>
Date: Thu, 19 Dec 2019 15:31:14 -0500
Subject: [PATCH 9/9] add warnings to readme

---
 README.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/README.md b/README.md
index f0749aa455..3c0e9156fd 100644
--- a/README.md
+++ b/README.md
@@ -1534,4 +1534,11 @@ Here's the magic diff that we did at some point that we keep bumping up to new G
 
 https://github.com/ucsd-progsys/liquidhaskell/commit/d380018850297b8f1878c33d0e4c586a1fddc2b8#diff-3644b76a8e6b3405f5492d8194da3874R224 
 
+Warnings
+========
+
+Liquid Haskell provides the following warnings:
+
+- `--Wdetect-unsafe` warns if your program includes any unsafe functionality, including `undefined`, `lazy`, or `assume`. Liquid Haskell will admit such functionality even if the implementation is not correct. Disable with `--Wno-detect-unsafe`.
+- `--Werror` makes warnings fatal.