agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Include error location when reporting imports that clash

Open omelkonian opened this issue 1 year ago • 0 comments

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 "

omelkonian avatar Mar 09 '23 13:03 omelkonian