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. 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/Constraint/Monad.hs b/src/Language/Haskell/Liquid/Constraint/Monad.hs index e66b3a7e04..3509332e92 100644 --- a/src/Language/Haskell/Liquid/Constraint/Monad.hs +++ b/src/Language/Haskell/Liquid/Constraint/Monad.hs @@ -108,6 +108,7 @@ addHole x t γ = do 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..02551a220d 100644 --- a/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -433,8 +433,57 @@ 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 :: 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 + +checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TWarning Doc] +checkWarnings cfg bareSpec ghcSrc = unsafeWarnings + where + unsafeWarnings = if detectUnsafe cfg then + checkUnsafeWarning bareSpec ghcSrc + else + mempty + +checkUnsafeWarning :: Ms.BareSpec -> GhcSrc -> [TWarning Doc] +checkUnsafeWarning bareSpec ghcSrc = + checkUnsafeAssume bareSpec + <> checkUnsafeLazy bareSpec + <> checkUnsafeVar ghcSrc + where + checkUnsafeAssume bareSpec = + let toWarning (ls, lt) = + let span = fSrcSpan ls in + WrnUnsafeAssumed span (pprint ls) (pprint lt) + in + map toWarning $ asmSigs bareSpec + + checkUnsafeLazy bareSpec = + let toWarning ls = + let span = fSrcSpan ls in + WrnUnsafeLazy 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 -> + let span = Ghc.getSrcSpan x in + WrnUnsafeVar span (pprint x) (pprint unsafeVar) + ) unsafeVars + + --------------------------------------------------------------------------------------- -- | @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 5d8bd89cba..bf6a784164 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,28 @@ 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 = show x `Set.member` unsafeList + where + 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 +-- 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..715c68bffd 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 @@ -440,8 +440,62 @@ data TError t = , msg :: !Doc } -- ^ Sigh. Other. + | ErrWError { pos :: SrcSpan + , errWarning :: TWarning t + } + deriving (Typeable, Generic , Functor ) + +-- -- | 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 errDupSpecs d spans@(sp:_) = ErrDupSpecs sp d spans errDupSpecs _ _ = impossible Nothing "errDupSpecs with empty spans!" @@ -482,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 @@ -566,7 +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 ": 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 @@ -713,11 +735,12 @@ 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 (ErrWError {}) = Just "Warning made fatal by \"--Werror\"." + go _ = Nothing -------------------------------------------------------------------------------- ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc @@ -988,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..970a8ebf51 --- /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 (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 (WrnUnsafeLazy _ x) + = dSp $+$ "`" <-> pprint x <-> "` is declared as lazy, 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 -> "" $+$ ("INFO:" <+> d)) (go e) + where + go (WrnUnsafeLazy {}) = Just unsafeHint + go (WrnUnsafeAssumed {}) = Just unsafeHint + go (WrnUnsafeVar {}) = Just unsafeHint + -- go _ = Nothing + + unsafeHint = "Enabled by \"--Wdetect-unsafe\"." + + +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) diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs index 9489a61e68..37f9b9cb8d 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -349,6 +349,23 @@ 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 + , wError + = def + &= name "Werror" + &= help "Make warnings fatal." + &= explicit } &= verbosity &= program "liquid" &= help "Refinement Types for Haskell" @@ -578,6 +595,9 @@ defConfig = Config , compileSpec = False , noCheckImports = False , 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 6e95a143ef..0a2a9ca0a4 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,9 @@ 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. + , wError :: Bool -- ^ Make warnings fatal. } deriving (Generic, Data, Typeable, Show, Eq) instance Serialize SMTSolver @@ -148,3 +152,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 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..5d115bc1dc --- /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..cb0e75a2f0 --- /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..bdc1528eb5 --- /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..3b7b046ec4 --- /dev/null +++ b/tests/unsafe/neg/Var1.hs @@ -0,0 +1,6 @@ +{-@ LIQUID "--Werror" @-} + +module Var1 where + +h :: () +h = let x = undefined in x