module Language.Haskell.Liquid.Types.Errors (
TError (..)
, CtxError (..)
, errorWithContext
, Oblig (..)
, WithModel (..), dropModel
, UserError
, panic
, panicDoc
, todo
, impossible
, uError
, sourceErrors
, errDupSpecs
, ppError
, ppError'
, ppVar
, realSrcSpan
, unpackRealSrcSpan
) where
import Prelude hiding (error)
import SrcLoc
import FastString
import HscTypes (srcErrorMessages, SourceError)
import ErrUtils
import Bag
import GHC.Generics
import Control.DeepSeq
import Data.Typeable (Typeable)
import Data.Generics (Data)
import qualified Data.Binary as B
import Data.Maybe
import Text.PrettyPrint.HughesPJ
import Data.Aeson hiding (Result)
import qualified Data.HashMap.Strict as M
import Language.Fixpoint.Types (pprint, showpp, Tidy (..), PPrint (..), Symbol, Expr)
import qualified Language.Fixpoint.Misc as Misc
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 $ 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 Doc -> IO (CtxError Doc)
errorWithContext e = CtxError e <$> srcSpanContext (pos e)
srcSpanContext :: SrcSpan -> IO Doc
srcSpanContext sp
| Just (f, l, c, l', c') <- srcSpanInfo sp
= makeContext l c c' <$> getFileLines f l l'
| otherwise
= return empty
srcSpanInfo :: SrcSpan -> Maybe (FilePath, Int, Int, Int, Int)
srcSpanInfo (RealSrcSpan s) = Just (f, l, c, l', c')
where
f = unpackFS $ srcSpanFile s
l = srcSpanStartLine s
c = srcSpanStartCol s
l' = srcSpanEndLine s
c' = srcSpanEndCol s
srcSpanInfo _ = Nothing
getFileLines :: FilePath -> Int -> Int -> IO [String]
getFileLines f i j = do
b <- doesFileExist f
if b
then slice (i 1) (j 1) . lines <$> readFile f
else return []
slice :: Int -> Int -> [a] -> [a]
slice i j xs = take (j i + 1) (drop i xs)
makeContext :: Int -> Int -> Int -> [String] -> Doc
makeContext _ _ _ [] = empty
makeContext l c c' [s] = makeContext1 l c c' s
makeContext l _ _ ss = vcat $ text " "
: (zipWith makeContextLine [l..] ss)
++ [ text " "
, text " " ]
makeContextLine :: Int -> String -> Doc
makeContextLine l s = lnum l <+> text s
where
lnum n = text (show n) <+> text "|"
makeContext1 :: Int -> Int -> Int -> String -> Doc
makeContext1 l c c' s = vcat [ text " "
, lnum l <+> (text s $+$ cursor)
, text " "
, text " "
]
where
lnum n = text (show n) <+> text "|"
cursor = blanks (c 1) <> pointer (max 1 (c' c))
blanks n = text $ replicate n ' '
pointer n = text $ replicate n '^'
data Oblig
= OTerm
| OInv
| OCons
deriving (Generic, Data, Typeable)
instance B.Binary Oblig
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
}
| ErrSubTypeModel
{ pos :: !SrcSpan
, msg :: !Doc
, ctxM :: !(M.HashMap Symbol (WithModel t))
, tactM :: !(WithModel 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
, msg :: !Doc
, exp :: !Expr
, msg' :: !Doc
}
| ErrDupAlias { pos :: !SrcSpan
, var :: !Doc
, kind :: !Doc
, locs :: ![SrcSpan]
}
| ErrDupSpecs { pos :: !SrcSpan
, var :: !Doc
, locs:: ![SrcSpan]
}
| ErrDupIMeas { pos :: !SrcSpan
, var :: !Doc
, tycon :: !Doc
, locs :: ![SrcSpan]
}
| ErrDupMeas { pos :: !SrcSpan
, var :: !Doc
, locs :: ![SrcSpan]
}
| ErrDupField { pos :: !SrcSpan
, dcon :: !Doc
, field :: !Doc
}
| ErrDupNames { pos :: !SrcSpan
, var :: !Doc
, names :: ![Doc]
}
| 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
}
| ErrUnbPred { pos :: !SrcSpan
, var :: !Doc
}
| ErrGhc { pos :: !SrcSpan
, msg :: !Doc
}
| ErrMismatch { pos :: !SrcSpan
, var :: !Doc
, msg :: !Doc
, hs :: !Doc
, lqTy :: !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
, dname :: !Doc
, dpos :: !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
}
| ErrSaved { pos :: !SrcSpan
, nam :: !Doc
, msg :: !Doc
}
| ErrFilePragma { pos :: !SrcSpan
}
| ErrTyCon { pos :: !SrcSpan
, msg :: !Doc
, tcname :: !Doc
}
| ErrLiftExp { pos :: !SrcSpan
, msg :: !Doc
}
| ErrParseAnn { pos :: !SrcSpan
, msg :: !Doc
}
| ErrOther { pos :: SrcSpan
, msg :: !Doc
}
deriving (Typeable, Generic , Functor )
errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t
errDupSpecs d spans@(sp:_) = ErrDupSpecs sp d spans
errDupSpecs _ _ = impossible Nothing "errDupSpecs with empty spans!"
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 UserError where
pprintTidy k = ppError k empty . fmap (pprintTidy Lossy)
data WithModel t
= NoModel t
| WithModel !Doc t
deriving (Functor, Show, Eq, Generic)
instance NFData t => NFData (WithModel t)
dropModel :: WithModel t -> t
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
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 :: Foldable t => Int -> t Doc -> Doc
nests n = foldr (\d acc -> nest n (d $+$ acc)) empty
sepVcat :: Doc -> [Doc] -> Doc
sepVcat d ds = vcat $ intersperse d ds
blankLine :: Doc
blankLine = sizedText 5 " "
ppFull :: Tidy -> Doc -> Doc
ppFull Full d = d
ppFull Lossy _ = empty
ppReqInContext :: PPrint t => Tidy -> t -> t -> M.HashMap Symbol t -> Doc
ppReqInContext td tA tE c
= sepVcat blankLine
[ nests 2 [ text "Inferred type"
, text "VV :" <+> pprintTidy td tA]
, nests 2 [ text "not a subtype of Required type"
, text "VV :" <+> pprintTidy td tE]
, nests 2 [ text "In Context"
, vsep (map (uncurry (pprintBind td)) (M.toList c))
]
]
pprintBind :: PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind td v t = pprintTidy td v <+> char ':' <+> pprintTidy td t
ppReqModelInContext
:: (PPrint t) => Tidy -> WithModel t -> t -> (M.HashMap Symbol (WithModel t)) -> Doc
ppReqModelInContext td tA tE c
= sepVcat blankLine
[ nests 2 [ text "Inferred type"
, pprintModel td "VV" tA]
, nests 2 [ text "not a subtype of Required type"
, pprintModel td "VV" (NoModel tE)]
, nests 2 [ text "In Context"
, vsep (map (uncurry (pprintModel td)) (M.toList c))
]
]
vsep :: [Doc] -> Doc
vsep = vcat . intersperse (char ' ')
pprintModel :: PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel td v wm = case wm of
NoModel t
-> pprintTidy td v <+> char ':' <+> pprintTidy td t
WithModel m t
-> pprintTidy td v <+> char ':' <+> pprintTidy td t $+$
pprintTidy td v <+> char '=' <+> pprintTidy td m
ppPropInContext :: (PPrint p, PPrint c) => Tidy -> p -> c -> Doc
ppPropInContext td p c
= sepVcat blankLine
[ nests 2 [ text "Property"
, pprintTidy td p]
, nests 2 [ text "Not provable in context"
, pprintTidy td 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 :: RealSrcSpan -> (String, Int, Int, Int, Int)
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 ToJSONKey SrcSpan
instance FromJSONKey SrcSpan
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 sp body = ErrSaved sp (text n) (text $ unlines m)
where
n : m = lines body
totalityType :: PPrint a => Tidy -> a -> Bool
totalityType td tE = pprintTidy td tE == text "{VV : Addr# | 5 < 4}"
ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
ppError' td dSp dCtx (ErrAssType _ o _ c p)
= dSp <+> pprintTidy td o
$+$ dCtx
$+$ (ppFull td $ ppPropInContext td p c)
ppError' td dSp dCtx (ErrSubType _ _ _ _ tE)
| totalityType td tE
= dSp <+> text "Totality Error"
$+$ dCtx
$+$ text "Your function is not total: not all patterns are defined."
$+$ "Hint: Use \"--no-totality\" to deactivate totality checking."
ppError' td dSp dCtx (ErrSubType _ _ c tA tE)
= dSp <+> text "Liquid Type Mismatch"
$+$ dCtx
$+$ (ppFull td $ ppReqInContext td tA tE c)
ppError' td dSp dCtx (ErrSubTypeModel _ _ c tA tE)
= dSp <+> text "Liquid Type Mismatch"
$+$ dCtx
$+$ (ppFull td $ ppReqModelInContext td tA tE c)
ppError' td dSp dCtx (ErrFCrash _ _ c tA tE)
= dSp <+> text "Fixpoint Crash on Constraint"
$+$ dCtx
$+$ (ppFull td $ ppReqInContext td tA tE c)
ppError' _ dSp dCtx (ErrParse _ _ e)
= dSp <+> text "Cannot parse specification:"
$+$ dCtx
$+$ (nest 4 $ pprint e)
ppError' _ dSp dCtx (ErrTySpec _ v t s)
= dSp <+> text "Illegal type specification for" <+> ppVar v
$+$ dCtx
$+$ nest 4 (vcat [ pprint v <+> Misc.dcolon <+> pprint t
, pprint s
])
ppError' _ dSp dCtx (ErrLiftExp _ v)
= dSp <+> text "Cannot lift" <+> ppVar v <+> "into refinement logic"
$+$ dCtx
$+$ (nest 4 $ text "Please export the binder from the module to enable lifting.")
ppError' _ dSp dCtx (ErrBadData _ v s)
= dSp <+> text "Bad Data Specification"
$+$ dCtx
$+$ (pprint s <+> "for" <+> ppVar v)
ppError' _ dSp dCtx (ErrDataCon _ d s)
= dSp <+> "Malformed refined data constructor" <+> ppVar d
$+$ dCtx
$+$ s
ppError' _ dSp dCtx (ErrBadQual _ n d)
= dSp <+> text "Illegal qualifier specification for" <+> ppVar n
$+$ dCtx
$+$ pprint d
ppError' _ dSp dCtx (ErrTermSpec _ v msg e s)
= dSp <+> text "Illegal termination specification for" <+> ppVar v
$+$ dCtx
$+$ (nest 4 $ ((text "Termination metric" <+> pprint e <+> text "is" <+> msg)
$+$ 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 dCtx (ErrHMeas _ t s)
= dSp <+> text "Cannot lift Haskell function" <+> ppVar t <+> text "to logic"
$+$ dCtx
$+$ (nest 4 $ pprint s)
ppError' _ dSp dCtx (ErrDupSpecs _ v ls)
= dSp <+> text "Multiple specifications for" <+> ppVar v <+> colon
$+$ dCtx
$+$ ppSrcSpans ls
ppError' _ dSp dCtx (ErrDupIMeas _ v t ls)
= dSp <+> text "Multiple instance measures" <+> ppVar v <+> text "for type" <+> ppVar t
$+$ dCtx
$+$ ppSrcSpans ls
ppError' _ dSp dCtx (ErrDupMeas _ v ls)
= dSp <+> text "Multiple measures named" <+> ppVar v
$+$ dCtx
$+$ ppSrcSpans ls
ppError' _ dSp dCtx (ErrDupField _ dc x)
= dSp <+> text "Malformed refined data constructor" <+> dc
$+$ dCtx
$+$ (nest 4 $ text "Duplicated definitions for field" <+> ppVar x)
ppError' _ dSp dCtx (ErrDupNames _ x ns)
= dSp <+> text "Ambiguous specification symbol" <+> ppVar x
$+$ dCtx
$+$ ppNames ns
ppError' _ dSp dCtx (ErrDupAlias _ k v ls)
= dSp <+> text "Multiple definitions of" <+> pprint k <+> ppVar v
$+$ dCtx
$+$ ppSrcSpans ls
ppError' _ dSp dCtx (ErrUnbound _ x)
= dSp <+> text "Unbound variable" <+> pprint x
$+$ dCtx
ppError' _ dSp dCtx (ErrUnbPred _ p)
= dSp <+> text "Cannot apply unbound abstract refinement" <+> ppVar p
$+$ 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" <+> ppVar p
, "which expects" <+> pprint eN <+> "arguments" <+> "but is given only" <+> pprint aN
, " "
, "Abstract predicates cannot be partially applied; for a possible fix see:"
, " "
, nest 4 "https://github.com/ucsd-progsys/liquidhaskell/issues/594"
])
ppError' _ dSp dCtx (ErrMismatch _ x msg τ t hsSp)
= dSp <+> "Specified type does not refine Haskell type for" <+> ppVar x <+> parens msg
$+$ dCtx
$+$ (sepVcat blankLine
[ "The Liquid type"
, nest 4 t
, "is inconsistent with the Haskell type"
, nest 4 τ
, "defined at" <+> pprint hsSp
])
ppError' _ dSp dCtx (ErrAliasCycle _ acycle)
= dSp <+> text "Cyclic type alias definition for" <+> ppVar n0
$+$ dCtx
$+$ (nest 4 $ sepVcat blankLine (hdr : map describe acycle))
where
hdr = text "The following alias definitions form a cycle:"
describe (p, n) = text "*" <+> ppVar n <+> parens (text "defined at:" <+> pprint p)
n0 = snd . head $ acycle
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 _ name dl s)
= dSp <+> text "Malformed application of type alias" <+> ppVar name
$+$ dCtx
$+$ (nest 4 $ vcat [ text "The alias" <+> ppVar name <+> "defined at:" <+> pprint dl
, s ] )
ppError' _ dSp dCtx (ErrSaved _ name s)
= dSp <+> name
$+$ dCtx
$+$ s
ppError' _ dSp dCtx (ErrFilePragma _)
= dSp <+> text "Illegal pragma"
$+$ dCtx
$+$ text "--idirs, --c-files, and --ghc-option cannot be used in file-level pragmas"
ppError' _ dSp dCtx (ErrOther _ s)
= dSp <+> text "Uh oh."
$+$ dCtx
$+$ nest 4 s
ppError' _ dSp dCtx (ErrTermin _ xs s)
= dSp <+> text "Termination Error"
$+$ dCtx
<+> (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
ppError' _ dSp dCtx (ErrTyCon _ msg ty)
= dSp <+> text "Illegal data refinement for" <+> ppVar ty
$+$ dCtx
$+$ nest 4 msg
ppError' _ dSp dCtx (ErrParseAnn _ msg)
= dSp <+> text "Malformed annotation"
$+$ dCtx
$+$ nest 4 msg
ppVar :: PPrint a => a -> Doc
ppVar v = text "`" <> pprint v <> text "`"
ppSrcSpans :: [SrcSpan] -> Doc
ppSrcSpans = ppList (text "Conflicting definitions at")
ppNames :: [Doc] -> Doc
ppNames ds = ppList "Could refer to any of the names" ds
ppList :: (PPrint a) => Doc -> [a] -> Doc
ppList d ls
= nest 4 (sepVcat blankLine (d : [ text "*" <+> pprint l | l <- ls ]))
sourceErrors :: String -> SourceError -> [TError t]
sourceErrors s = concatMap (errMsgErrors s) . bagToList . srcErrorMessages
errMsgErrors :: String -> ErrMsg -> [TError t]
errMsgErrors s e = [ ErrGhc (errMsgSpan e) msg ]
where
msg = text s
$+$ nest 4 (text (show e))