module Language.Haskell.Liquid.Types.Errors (
TError (..)
, CtxError (..)
, errorWithContext
, Oblig (..)
, UserError
, panic
, panicDoc
, todo
, impossible
, uError
, ppError
, ppError'
, realSrcSpan
, unpackRealSrcSpan
) where
import Prelude hiding (error)
import SrcLoc
import FastString
import GHC.Generics
import Control.DeepSeq
import Data.Typeable (Typeable)
import Data.Generics (Data)
import Data.Maybe
import Text.PrettyPrint.HughesPJ
import Data.Aeson hiding (Result)
import qualified Data.HashMap.Strict as M
import Language.Fixpoint.Types (showpp, Tidy (..), PPrint (..), pprint, Symbol, Expr)
import Language.Fixpoint.Misc (dcolon)
import Language.Haskell.Liquid.Misc (intToString)
import Text.Parsec.Error (ParseError)
import qualified Control.Exception as Ex
import System.Directory
import System.FilePath
import Data.List (intersperse )
import Text.Parsec.Error (errorMessages, showErrorMessages)
instance PPrint ParseError where
pprintTidy _ e = vcat $ tail $ map text ls
where
ls = lines $ showErrorMessages "or" "unknown parse error"
"expecting" "unexpected" "end of input"
(errorMessages e)
data CtxError t = CtxError
{ ctErr :: TError t
, ctCtx :: Doc
} deriving (Functor)
instance Eq (CtxError t) where
e1 == e2 = ctErr e1 == ctErr e2
instance Ord (CtxError t) where
e1 <= e2 = ctErr e1 <= ctErr e2
errorWithContext :: TError t -> IO (CtxError t)
errorWithContext e = CtxError e <$> srcSpanContext (pos e)
srcSpanContext :: SrcSpan -> IO Doc
srcSpanContext sp
| Just (f, l, c, c') <- srcSpanInfo sp
= maybe empty (makeContext l c c') <$> getFileLine f l
| otherwise
= return empty
srcSpanInfo :: SrcSpan -> Maybe (FilePath, Int, Int, Int)
srcSpanInfo (RealSrcSpan s)
| l == l' = Just (f, l, c, c')
| otherwise = Nothing
where
f = unpackFS $ srcSpanFile s
l = srcSpanStartLine s
c = srcSpanStartCol s
l' = srcSpanEndLine s
c' = srcSpanEndCol s
srcSpanInfo _ = Nothing
getFileLine :: FilePath -> Int -> IO (Maybe String)
getFileLine f i = do
b <- doesFileExist f
if b
then getNth (i 1) . lines <$> readFile f
else return Nothing
getNth :: Int -> [a] -> Maybe a
getNth i xs
| i < length xs = Just (xs !! i)
| otherwise = Nothing
makeContext :: Int -> Int -> Int -> String -> Doc
makeContext l c c' s = vcat [ text ""
, lnum l <+> (text s $+$ cursor)
, text ""
]
where
lnum n = text (show n) <+> text "|"
cursor = blanks (c 1) <> pointer (c' c)
blanks n = text $ replicate n ' '
pointer n = text $ replicate n '^'
data Oblig
= OTerm
| OInv
| OCons
deriving (Generic, Data, Typeable)
instance Show Oblig where
show OTerm = "termination-condition"
show OInv = "invariant-obligation"
show OCons = "constraint-obligation"
instance NFData Oblig
instance PPrint Oblig where
pprintTidy _ = ppOblig
ppOblig :: Oblig -> Doc
ppOblig OCons = text "Constraint Check"
ppOblig OTerm = text "Termination Check"
ppOblig OInv = text "Invariant Check"
data TError t =
ErrSubType { pos :: !SrcSpan
, msg :: !Doc
, ctx :: !(M.HashMap Symbol t)
, tact :: !t
, texp :: !t
}
| ErrFCrash { pos :: !SrcSpan
, msg :: !Doc
, ctx :: !(M.HashMap Symbol t)
, tact :: !t
, texp :: !t
}
| ErrAssType { pos :: !SrcSpan
, obl :: !Oblig
, msg :: !Doc
, ctx :: !(M.HashMap Symbol t)
, cond :: t
}
| ErrParse { pos :: !SrcSpan
, msg :: !Doc
, pErr :: !ParseError
}
| ErrTySpec { pos :: !SrcSpan
, var :: !Doc
, typ :: !t
, msg :: !Doc
}
| ErrTermSpec { pos :: !SrcSpan
, var :: !Doc
, exp :: !Expr
, msg :: !Doc
}
| ErrDupAlias { pos :: !SrcSpan
, var :: !Doc
, kind :: !Doc
, locs :: ![SrcSpan]
}
| ErrDupSpecs { pos :: !SrcSpan
, var :: !Doc
, locs:: ![SrcSpan]
}
| ErrDupMeas { pos :: !SrcSpan
, var :: !Doc
, tycon :: !Doc
, locs:: ![SrcSpan]
}
| ErrBadData { pos :: !SrcSpan
, var :: !Doc
, msg :: !Doc
}
| ErrDataCon { pos :: !SrcSpan
, var :: !Doc
, msg :: !Doc
}
| ErrInvt { pos :: !SrcSpan
, inv :: !t
, msg :: !Doc
}
| ErrIAl { pos :: !SrcSpan
, inv :: !t
, msg :: !Doc
}
| ErrIAlMis { pos :: !SrcSpan
, tAs :: !t
, tUs :: !t
, msg :: !Doc
}
| ErrMeas { pos :: !SrcSpan
, ms :: !Doc
, msg :: !Doc
}
| ErrHMeas { pos :: !SrcSpan
, ms :: !Doc
, msg :: !Doc
}
| ErrUnbound { pos :: !SrcSpan
, var :: !Doc
}
| ErrGhc { pos :: !SrcSpan
, msg :: !Doc
}
| ErrMismatch { pos :: !SrcSpan
, var :: !Doc
, hs :: !Doc
, lq :: !Doc
, lqPos :: !SrcSpan
}
| ErrPartPred { pos :: !SrcSpan
, ectr :: !Doc
, var :: !Doc
, argN :: !Int
, expN :: !Int
, actN :: !Int
}
| ErrAliasCycle { pos :: !SrcSpan
, acycle :: ![(SrcSpan, Doc)]
}
| ErrIllegalAliasApp { pos :: !SrcSpan
, dname :: !Doc
, dpos :: !SrcSpan
}
| ErrAliasApp { pos :: !SrcSpan
, nargs :: !Int
, dname :: !Doc
, dpos :: !SrcSpan
, dargs :: !Int
}
| ErrSaved { pos :: !SrcSpan
, msg :: !Doc
}
| ErrTermin { pos :: !SrcSpan
, bind :: ![Doc]
, msg :: !Doc
}
| ErrRClass { pos :: !SrcSpan
, cls :: !Doc
, insts :: ![(SrcSpan, Doc)]
}
| ErrBadQual { pos :: !SrcSpan
, qname :: !Doc
, msg :: !Doc
}
| ErrOther { pos :: SrcSpan
, msg :: !Doc
}
deriving (Typeable, Generic, Functor)
instance NFData ParseError where
rnf t = seq t ()
instance Eq (TError a) where
e1 == e2 = errSpan e1 == errSpan e2
instance Ord (TError a) where
e1 <= e2 = errSpan e1 <= errSpan e2
errSpan :: TError a -> SrcSpan
errSpan = pos
type UserError = TError Doc
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 UserError where
pprintTidy k = ppError k empty . fmap pprint
instance Show UserError where
show = showpp
instance Ex.Exception UserError
uError :: UserError -> a
uError = Ex.throw
panicDoc :: SrcSpan -> Doc -> a
panicDoc sp d = Ex.throw (ErrOther sp d :: UserError)
panic :: Maybe SrcSpan -> String -> a
panic sp d = panicDoc (sspan sp) (text d)
where
sspan = fromMaybe noSrcSpan
todo :: Maybe SrcSpan -> String -> a
todo s m = panic s $ unlines
[ "This functionality is currently unimplemented. "
, "If this functionality is critical to you, please contact us at: "
, "https://github.com/ucsd-progsys/liquidhaskell/issues"
, m
]
impossible :: Maybe SrcSpan -> String -> a
impossible s m = panic s $ unlines msg ++ m
where
msg = [ "This should never happen! If you are seeing this message, "
, "please submit a bug report at "
, "https://github.com/ucsd-progsys/liquidhaskell/issues "
, "with this message and the source file that caused this error."
, ""
]
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:"
nests n = foldr (\d acc -> nest n (d $+$ acc)) empty
sepVcat d ds = vcat $ intersperse d ds
blankLine = sizedText 5 " "
ppFull :: Tidy -> Doc -> Doc
ppFull Full d = d
ppFull Lossy _ = empty
ppReqInContext :: (PPrint t, PPrint c) => t -> t -> c -> Doc
ppReqInContext tA tE c
= sepVcat blankLine
[ nests 2 [ text "Inferred type"
, text "VV :" <+> pprint tA]
, nests 2 [ text "not a subtype of Required type"
, text "VV :" <+> pprint tE]
, nests 2 [ text "In Context"
, pprint c ]]
ppPropInContext :: (PPrint p, PPrint c) => p -> c -> Doc
ppPropInContext p c
= sepVcat blankLine
[ nests 2 [ text "Property"
, pprint p]
, nests 2 [ text "Not provable in context"
, pprint c ]]
instance ToJSON RealSrcSpan where
toJSON sp = object [ "filename" .= f
, "startLine" .= l1
, "startCol" .= c1
, "endLine" .= l2
, "endCol" .= c2
]
where
(f, l1, c1, l2, c2) = unpackRealSrcSpan sp
unpackRealSrcSpan rsp = (f, l1, c1, l2, c2)
where
f = unpackFS $ srcSpanFile rsp
l1 = srcSpanStartLine rsp
c1 = srcSpanStartCol rsp
l2 = srcSpanEndLine rsp
c2 = srcSpanEndCol rsp
instance FromJSON RealSrcSpan where
parseJSON (Object v) = realSrcSpan <$> v .: "filename"
<*> v .: "startLine"
<*> v .: "startCol"
<*> v .: "endLine"
<*> v .: "endCol"
parseJSON _ = mempty
realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
realSrcSpan f l1 c1 l2 c2 = mkRealSrcSpan loc1 loc2
where
loc1 = mkRealSrcLoc (fsLit f) l1 c1
loc2 = mkRealSrcLoc (fsLit f) l2 c2
instance ToJSON SrcSpan where
toJSON (RealSrcSpan rsp) = object [ "realSpan" .= True, "spanInfo" .= rsp ]
toJSON (UnhelpfulSpan _) = object [ "realSpan" .= False ]
instance FromJSON SrcSpan where
parseJSON (Object v) = do tag <- v .: "realSpan"
case tag of
False -> return noSrcSpan
True -> RealSrcSpan <$> v .: "spanInfo"
parseJSON _ = mempty
instance (PPrint a, Show a) => ToJSON (TError a) where
toJSON e = object [ "pos" .= (pos e)
, "msg" .= (render $ ppError' Full empty empty e)
]
instance FromJSON (TError a) where
parseJSON (Object v) = errSaved <$> v .: "pos"
<*> v .: "msg"
parseJSON _ = mempty
errSaved :: SrcSpan -> String -> TError a
errSaved x = ErrSaved x . text
ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
ppError' td dSp dCtx (ErrAssType _ o _ c p)
= dSp <+> pprint o
$+$ dCtx
$+$ (ppFull td $ ppPropInContext p c)
ppError' td dSp dCtx (ErrSubType _ _ c tA tE)
= dSp <+> text "Liquid Type Mismatch"
$+$ dCtx
$+$ (ppFull td $ ppReqInContext tA tE c)
ppError' td dSp dCtx (ErrFCrash _ _ c tA tE)
= dSp <+> text "Fixpoint Crash on Constraint"
$+$ dCtx
$+$ (ppFull td $ ppReqInContext tA tE c)
ppError' _ dSp dCtx (ErrParse _ _ e)
= dSp <+> text "Cannot parse specification:"
$+$ dCtx
$+$ (nest 4 $ pprint e)
ppError' _ dSp _ (ErrTySpec _ v t s)
= dSp <+> text "Bad Type Specification"
$+$ (pprint v <+> dcolon <+> pprint t)
$+$ (nest 4 $ pprint s)
ppError' _ dSp _ (ErrBadData _ v s)
= dSp <+> text "Bad Data Specification"
$+$ (pprint v <+> dcolon <+> pprint s)
ppError' _ dSp dCtx (ErrDataCon _ d s)
= dSp <+> "Malformed refined data constructor" <+> pprint d
$+$ dCtx
$+$ s
ppError' _ dSp dCtx (ErrBadQual _ n d)
= dSp <+> text "Bad Qualifier Specification for" <+> n
$+$ dCtx
$+$ (pprint d)
ppError' _ dSp _ (ErrTermSpec _ v e s)
= dSp <+> text "Bad Termination Specification"
$+$ (pprint v <+> dcolon <+> pprint e)
$+$ (nest 4 $ pprint s)
ppError' _ dSp _ (ErrInvt _ t s)
= dSp <+> text "Bad Invariant Specification"
$+$ (nest 4 $ text "invariant " <+> pprint t $+$ pprint s)
ppError' _ dSp _ (ErrIAl _ t s)
= dSp <+> text "Bad Using Specification"
$+$ (nest 4 $ text "as" <+> pprint t $+$ pprint s)
ppError' _ dSp _ (ErrIAlMis _ t1 t2 s)
= dSp <+> text "Incompatible Using Specification"
$+$ (nest 4 $ (text "using" <+> pprint t1 <+> text "as" <+> pprint t2) $+$ pprint s)
ppError' _ dSp _ (ErrMeas _ t s)
= dSp <+> text "Bad Measure Specification"
$+$ (nest 4 $ text "measure " <+> pprint t $+$ pprint s)
ppError' _ dSp _ (ErrHMeas _ t s)
= dSp <+> text "Cannot promote Haskell function" <+> pprint t <+> text "to logic"
$+$ (nest 4 $ pprint s)
ppError' _ dSp _ (ErrDupSpecs _ v ls)
= dSp <+> text "Multiple Specifications for" <+> pprint v <> colon
$+$ (nest 4 $ vcat $ pprint <$> ls)
ppError' _ dSp _ (ErrDupMeas _ v t ls)
= dSp <+> text "Multiple Instance Measures for" <+> pprint v
<+> text "and" <+> pprint t
<> colon
$+$ (nest 4 $ vcat $ pprint <$> ls)
ppError' _ dSp _ (ErrDupAlias _ k v ls)
= dSp <+> text "Multiple Declarations! "
$+$ (nest 2 $ text "Multiple Declarations of" <+> pprint k <+> ppVar v $+$ text "Declared at:")
<+> (nest 4 $ vcat $ pprint <$> ls)
ppError' _ dSp dCtx (ErrUnbound _ x)
= dSp <+> text "Unbound variable" <+> pprint x
$+$ dCtx
ppError' _ dSp dCtx (ErrGhc _ s)
= dSp <+> text "GHC Error"
$+$ dCtx
$+$ (nest 4 $ pprint s)
ppError' _ dSp dCtx (ErrPartPred _ c p i eN aN)
= dSp <+> text "Malformed Predicate Application"
$+$ dCtx
$+$ (nest 4 $ vcat [ "The" <+> text (intToString i) <+> "argument of" <+> c <+> "is predicate" <+> p
, "which expects" <+> pprint eN <+> "arguments" <+> "but is given only" <+> pprint aN
, "Abstract predicates cannot be partially applied, see "
, nest 2 "https://github.com/ucsd-progsys/liquidhaskell/issues/594"
, "for possible fix."
])
ppError' _ dSp dCtx (ErrMismatch _ x τ t hsSp)
= dSp <+> "Specified Type Does Not Refine Haskell Type for" <+> pprint x
$+$ dCtx
$+$ (sepVcat blankLine
[ "The Liquid type"
, nest 4 t
, "is inconsistent with the Haskell type"
, nest 4 τ
, "defined at" <+> pprint hsSp
])
ppError' _ dSp _ (ErrAliasCycle _ acycle)
= dSp <+> text "Cyclic Alias Definitions"
$+$ text "The following alias definitions form a cycle:"
$+$ (nest 4 $ sepVcat blankLine $ map describe acycle)
where
describe (p, n)
= text "Type alias:" <+> pprint n
$+$ text "Defined at:" <+> pprint p
ppError' _ dSp dCtx (ErrIllegalAliasApp _ dn dl)
= dSp <+> text "Refinement Type Alias cannot be used in this context"
$+$ dCtx
$+$ text "Type alias:" <+> pprint dn
$+$ text "Defined at:" <+> pprint dl
ppError' _ dSp dCtx (ErrAliasApp _ n name dl dn)
= dSp <+> text "Malformed Type Alias Application"
$+$ dCtx
$+$ text "Type alias:" <+> pprint name
$+$ text "Defined at:" <+> pprint dl
$+$ text "Expects" <+> pprint dn <+> text "arguments, but is given" <+> pprint n
ppError' _ dSp _ (ErrSaved _ s)
= dSp <+> s
ppError' _ dSp dCtx (ErrOther _ s)
= dSp <+> text "Uh oh."
$+$ dCtx
$+$ nest 4 s
ppError' _ dSp _ (ErrTermin _ xs s)
= dSp <+> text "Termination Error"
<+> (hsep $ intersperse comma xs) $+$ s
ppError' _ dSp _ (ErrRClass p0 c is)
= dSp <+> text "Refined classes cannot have refined instances"
$+$ (nest 4 $ sepVcat blankLine $ describeCls : map describeInst is)
where
describeCls
= text "Refined class definition for:" <+> c
$+$ text "Defined at:" <+> pprint p0
describeInst (p, t)
= text "Refined instance for:" <+> t
$+$ text "Defined at:" <+> pprint p
ppVar v = text "`" <> pprint v <> text "'"