New error LibTooFarDown instead of GenericError

src/full/Agda/TypeChecking/Errors.hs

@@ -37,6 +37,7 @@ import qualified Data.List as List
 import Data.Maybe
 import Data.Set (Set)
 import qualified Data.Set as Set
+import System.FilePath
 import qualified Text.PrettyPrint.Boxes as Boxes
 
 import Agda.Interaction.Options
@@ -69,13 +70,14 @@ import Agda.TypeChecking.SizedTypes.Pretty ()
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Reduce (instantiate)
 
-import Agda.Interaction.Library.Base (formatLibErrors)
+import Agda.Interaction.Library.Base (formatLibErrors, libFile)
 
 import Agda.Utils.FileName
 import Agda.Utils.Float  ( toStringWithoutDotZero )
 import Agda.Utils.Function
 import Agda.Utils.Functor( for )
 import Agda.Utils.IO     ( showIOException )
+import Agda.Utils.Lens
 import Agda.Utils.List   ( initLast, lastMaybe )
 import Agda.Utils.List1 (List1, pattern (:|))
 import qualified Agda.Utils.List1 as List1
@@ -183,6 +185,7 @@ errorString = \case
   InvalidPattern{}                         -> "InvalidPattern"
   InvalidFileName{}                        -> "InvalidFileName"
   LibraryError{}                           -> "LibraryError"
+  LibTooFarDown{}                          -> "LibTooFarDown"
   LiteralTooBig{}                          -> "LiteralTooBig"
   LocalVsImportedModuleClash{}             -> "LocalVsImportedModuleClash"
   MetaCannotDependOn{}                     -> "MetaCannotDependOn"
@@ -905,6 +908,11 @@ instance PrettyTCM TypeError where
 
     LibraryError err -> return $ formatLibErrors err
 
+    LibTooFarDown m lib -> vcat
+      [ text "A .agda-lib file for" <+> pretty m
+      , text "must not be located in the directory" <+> text (takeDirectory (lib ^. libFile))
+      ]
+
     LocalVsImportedModuleClash m -> fsep $
       pwords "The module" ++ [prettyTCM m] ++
       pwords "can refer to either a local module or an imported module"

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -4873,6 +4873,8 @@ data TypeError
     -- Import errors
         | LibraryError LibErrors
             -- ^ Collected errors when processing the @.agda-lib@ file.
+        | LibTooFarDown TopLevelModuleName AgdaLibFile
+            -- ^ The @.agda-lib@ file for the given module is not on the right level.
         | LocalVsImportedModuleClash ModuleName
         | SolvedButOpenHoles
           -- ^ Some interaction points (holes) have not been filled by user.

src/full/Agda/TypeChecking/Monad/Options.hs

@@ -169,10 +169,7 @@ checkLibraryFileNotTooFarDown ::
   AgdaLibFile ->
   TCM ()
 checkLibraryFileNotTooFarDown m lib =
-  when (lib ^. libAbove < size m - 1) $ typeError $ GenericError $
-    "A .agda-lib file for " ++ prettyShow m ++
-    " must not be located in the directory " ++
-    takeDirectory (lib ^. libFile)
+  when (lib ^. libAbove < size m - 1) $ typeError $ LibTooFarDown m lib
 
 -- | Returns the library options for a given file.
 

test/Fail/customised/Issue6465.err

@@ -1,5 +1,5 @@
-customised/Issue6465.agda:1,1-11: error: [GenericError]
-A .agda-lib file for A.B must not be located in the directory
-customised/Issue6465/A
+customised/Issue6465.agda:1,1-11: error: [LibTooFarDown]
+A .agda-lib file for A.B
+must not be located in the directory customised/Issue6465/A
 when scope checking the declaration
   import A.B