Use a separate warning for duplicated interface files

This warning shouldn't be serialized to interface files because it can
be resolved without changing the source code. For example, if the
warning is triggered and serialized into the interface file, The
interface file would still be considered up-to-date, despite that the
warning might have been resolved.

Fixes #7104.

doc/user-manual/tools/command-line-options.rst

@@ -1229,6 +1229,10 @@ The list containing any warning ``NAME`` can be produced by ``agda --help=warnin
 
      ``record`` expression with duplicate field names.
 
+.. option:: DuplicateInterfaceFiles
+
+     There exists both a local interface file and an interface file in ``_build``.
+
 .. option:: DuplicateUsing
 
      Repeated names in ``using`` directive.

src/full/Agda/Interaction/FindFile.hs

@@ -44,7 +44,7 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
   (getIncludeDirs, libToTCM)
 import Agda.TypeChecking.Monad.State (topLevelModuleName)
-import Agda.TypeChecking.Warnings (runPM, genericWarning)
+import Agda.TypeChecking.Warnings (runPM, warning)
 
 import Agda.Version ( version )
 
@@ -96,25 +96,20 @@ toIFile (SourceFile src) = do
       let buildDir = root </> "_build" </> version </> "agda"
           fileName = makeRelative root (filePath localIFile)
           separatedIFile = mkAbsolute $ buildDir </> fileName
-          selectIFile = ifM (optLocalInterfaces <$> commandLineOptions)
-            (pure localIFile)
-            (pure separatedIFile)
+          ifilePreference = ifM (optLocalInterfaces <$> commandLineOptions)
+            (pure (localIFile, separatedIFile))
+            (pure (separatedIFile, localIFile))
       in do
         separatedIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath separatedIFile
         localIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath localIFile
         case (separatedIFileExists, localIFileExists) of
-          (False, False) -> selectIFile
+          (False, False) -> fst <$> ifilePreference
           (False, True) -> pure localIFile
           (True, False) -> pure separatedIFile
           (True, True) -> do
-            ifile <- selectIFile
-            genericWarning $ P.vcat
-                [ P.text "There are two interface files:"
-                , P.nest 4 $ P.text $ filePath separatedIFile
-                , P.nest 4 $ P.text $ filePath localIFile
-                , P.nest 2 $ P.text $ "Using " ++ filePath ifile ++ " for now but please remove at least one of them."
-                ]
-            pure ifile
+            ifiles <- ifilePreference
+            warning $ uncurry DuplicateInterfaceFiles ifiles
+            pure $ fst ifiles
 
 replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
 replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) .  dropAgdaExtension . filePath

src/full/Agda/Interaction/Highlighting/Generate.hs

@@ -539,6 +539,9 @@ warningHighlighting' b w = case tcWarning w of
     UnknownNamesInFixityDecl{}        -> mempty
     UnknownNamesInPolarityPragmas{}   -> mempty
 
+  -- Not source code related
+  DuplicateInterfaceFiles{} -> mempty
+
 recordFieldWarningHighlighting ::
   RecordFieldWarning -> HighlightingInfoBuilder
 recordFieldWarningHighlighting = \case

src/full/Agda/Interaction/Imports.hs

@@ -1266,7 +1266,7 @@ buildInterface src topLevel = do
     -- when expanding a pattern synonym.
     patsyns <- killRange <$> getPatternSyns
     let builtin' = Map.mapWithKey (\ x b -> primName x <$> b) builtin
-    warnings <- getAllWarnings AllWarnings
+    warnings <- filter (isSourceCodeWarning . warningName . tcWarning) <$> getAllWarnings AllWarnings
     let i = Interface
           { iSourceHash      = hashText source
           , iSource          = source

src/full/Agda/Interaction/Options/Warnings.hs

@@ -298,6 +298,8 @@ data WarningName
   -- Cubical
   | FaceConstraintCannotBeHidden_
   | FaceConstraintCannotBeNamed_
+  -- Not source code related
+  | DuplicateInterfaceFiles_
   deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic)
 
 instance NFData WarningName
@@ -479,3 +481,5 @@ warningNameDescription = \case
   -- Cubical
   FaceConstraintCannotBeHidden_    -> "Face constraint patterns that are given as implicit arguments."
   FaceConstraintCannotBeNamed_     -> "Face constraint patterns that are given as named arguments."
+  -- Not source code related
+  DuplicateInterfaceFiles_         -> "Duplicate interface files."

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

@@ -4259,6 +4259,10 @@ data Warning
     -- ^ Face constraint patterns @(i = 0)@ must be visible arguments.
   | FaceConstraintCannotBeNamed NamedName
     -- ^ Face constraint patterns @(i = 0)@ must be unnamed arguments.
+
+  -- Not source code related
+  | DuplicateInterfaceFiles AbsolutePath AbsolutePath
+    -- ^ `DuplicateInterfaceFiles selectedInterfaceFile ignoredInterfaceFile`
   deriving (Show, Generic)
 
 recordFieldWarningToError :: RecordFieldWarning -> TypeError
@@ -4339,6 +4343,15 @@ warningName = \case
   FaceConstraintCannotBeHidden{} -> FaceConstraintCannotBeHidden_
   FaceConstraintCannotBeNamed{}  -> FaceConstraintCannotBeNamed_
 
+  -- Not source code related
+  DuplicateInterfaceFiles{}      -> DuplicateInterfaceFiles_
+
+-- Indicates wether changes in the source code can silence or influence the
+-- warning.
+isSourceCodeWarning :: WarningName -> Bool
+isSourceCodeWarning DuplicateInterfaceFiles_{} = False
+isSourceCodeWarning _ = True
+
 data TCWarning
   = TCWarning
     { tcWarningLocation :: CallStack

src/full/Agda/TypeChecking/Pretty/Warning.hs

@@ -45,6 +45,7 @@ import Agda.Syntax.Translation.InternalToAbstract
 import Agda.Interaction.Options
 import Agda.Interaction.Options.Warnings
 
+import Agda.Utils.FileName (filePath)
 import Agda.Utils.Lens
 import Agda.Utils.List ( editDistance )
 import qualified Agda.Utils.List1 as List1
@@ -239,6 +240,13 @@ prettyWarning = \case
 
     ParseWarning pw -> pretty pw
 
+    DuplicateInterfaceFiles selected ignored -> vcat
+      [ fwords "There are two interface files:"
+      , nest 4 $ text $ filePath selected
+      , nest 4 $ text $ filePath ignored
+      , nest 2 $ fsep $ pwords "Using" ++ [text $ filePath selected] ++ pwords "for now but please remove at least one of them."
+      ]
+
     DeprecationWarning old new version -> fsep $
       [text old] ++ pwords "has been deprecated. Use" ++ [text new] ++ pwords
       "instead. This will be an error in Agda" ++ [text version <> "."]

src/full/Agda/TypeChecking/Serialise.hs

@@ -77,7 +77,7 @@ import Agda.Utils.Impossible
 -- 32-bit machines). Word64 does not have these problems.
 
 currentInterfaceVersion :: Word64
-currentInterfaceVersion = 20240102 * 10 + 0
+currentInterfaceVersion = 20240102 * 10 + 1
 
 -- | The result of 'encode' and 'encodeInterface'.
 

src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs

@@ -89,6 +89,8 @@ instance EmbPrj Warning where
     FaceConstraintCannotBeHidden a        -> icodeN 47 FaceConstraintCannotBeHidden a
     FaceConstraintCannotBeNamed a         -> icodeN 48 FaceConstraintCannotBeNamed a
     PatternShadowsConstructor a b         -> icodeN 49 PatternShadowsConstructor a b
+    -- Not source code related, therefore they should never be serialized
+    DuplicateInterfaceFiles a b           -> __IMPOSSIBLE__
 
   value = vcase $ \ case
     [0, a, b]            -> valuN UnreachableClauses a b
@@ -442,6 +444,7 @@ instance EmbPrj WarningName where
     FaceConstraintCannotBeHidden_                -> 102
     FaceConstraintCannotBeNamed_                 -> 103
     PatternShadowsConstructor_                   -> 104
+    DuplicateInterfaceFiles_                     -> 105
 
   value = \case
     0   -> return OverlappingTokensWarning_
@@ -549,6 +552,7 @@ instance EmbPrj WarningName where
     102 -> return FaceConstraintCannotBeHidden_
     103 -> return FaceConstraintCannotBeNamed_
     104 -> return PatternShadowsConstructor_
+    105 -> return DuplicateInterfaceFiles_
     _   -> malformed