agda2hs
agda2hs copied to clipboard
Include error location when reporting imports that clash
The error produced when we detect clashing imports does not currently contain an error location, c.f. the clashingImports function.
One solution might be to add a field importRange :: Range
to the type of Import
records here and then tweak clashingImports
like so:
checkClashingImports :: Imports -> TCM ()
checkClashingImports [] = return ()
- checkClashingImports (Import mod as p q : is) =
+ checkClashingImports (Import mod as p q loc : is) =
case filter isClashing is of
- (i : _) -> genericDocError =<< text (mkErrorMsg i)
+ (i : _) -> setCurrentRange loc $ genericDocError =<< text (mkErrorMsg i)
[] -> checkClashingImports is
where
- isClashing (Import _ as' p' q') = (as' == as) && (p' /= p) && (q' == q)
+ isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q)
mkErrorMsg (Import _ _ p' q') =
"Clashing import: " ++ pp q ++ " (both from "
++ prettyShow (pp <$> p) ++ " and "