agda · nad · Aug 29, 2024 · Aug 26, 2024
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
@@ -641,39 +641,10 @@ getStoredInterface x file msrc = do
 
         reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is up-to-date."]
 
-  -- Check if we have cached the module.
-  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $
-      lift $ getDecodedModule x
-
-  case cachedE of
-    -- If it's cached ignoreInterfaces has no effect;
-    -- to avoid typechecking a file more than once.
-    Right mi -> do
-      (ifile, hashes) <- getIFileHashesET
-
-      let ifp = filePath $ intFilePath ifile
-      let i = miInterface mi
-
-      -- Make sure the hashes match.
-      let cachedIfaceHash = iFullHash i
-      let fileIfaceHash = snd hashes
-      unless (cachedIfaceHash == fileIfaceHash) $ do
-        lift $ dropDecodedModule x
-        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
-        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
-        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
-        throwError $ concat
-          [ "the cached interface hash (", show cachedIfaceHash, ")"
-          , " does not match interface file (", show fileIfaceHash, ")"
-          ]
-
-      Bench.billTo [Bench.Deserialization] $ do
-        checkSourceHashET (iSourceHash i)
-
-        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
-        loadDecodedModule file mi
-
-    Left whyNotCached -> withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do
+  let
+    -- Load or reload the interface file, if possible.
+    loadInterfaceFile whyNotCached =
+      withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do
       whenM ignoreAllInterfaces $
         throwError "we're ignoring all interface files"
 
@@ -711,6 +682,39 @@ getStoredInterface x file msrc = do
           , miMode = ModuleTypeChecked
           }
 
+  -- Check if we have cached the module.
+  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $
+      lift $ getDecodedModule x
+
+  case cachedE of
+    Left whyNotCached -> loadInterfaceFile whyNotCached
+
+    -- If it's cached ignoreInterfaces has no effect;
+    -- to avoid typechecking a file more than once.
+    Right mi -> do
+      (ifile, hashes) <- getIFileHashesET
+
+      let ifp = filePath $ intFilePath ifile
+      let i = miInterface mi
+
+      -- Make sure the hashes match.
+      let cachedIfaceHash = iFullHash i
+      let fileIfaceHash = snd hashes
+      if cachedIfaceHash /= fileIfaceHash then do
+        lift $ dropDecodedModule x
+        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
+        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
+        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
+        loadInterfaceFile $ concat
+          [ "the cached interface hash (", show cachedIfaceHash, ")"
+          , " does not match interface file (", show fileIfaceHash, ")"
+          ]
+       else Bench.billTo [Bench.Deserialization] $ do
+        checkSourceHashET (iSourceHash i)
+
+        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
+        loadDecodedModule file mi
+
 -- | Report those given warnings that come from the given module.
 
 reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> [TCWarning] -> m ()

diff --git a/test/interaction/Issue7199.agda b/test/interaction/Issue7199.agda
@@ -0,0 +1,3 @@
+module Issue7199 where
+
+import Issue7199.M
diff --git a/test/interaction/Issue7199.hs b/test/interaction/Issue7199.hs
@@ -0,0 +1,52 @@
+#!/usr/bin/env runhaskell
+
+{-# LANGUAGE RecordWildCards #-}
+
+import Data.List
+import System.Exit
+
+import RunAgda
+
+moduleM      = "module Issue7199.M where\n"
+moduleMExtra = "postulate A : Set\n"
+
+main :: IO ()
+main = runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
+
+  -- Discard the first prompt.
+  readUntilPrompt
+
+  -- Make sure that Issue7199.M has been defined correctly.
+  writeFile "Issue7199/M.agda" moduleM
+
+  -- Load Issue7199. Discard the output.
+  load "Issue7199.agda"
+  readUntilPrompt
+
+  -- Modify Issue7199.M.
+  writeFile "Issue7199/M.agda" (moduleM ++ moduleMExtra)
+
+  -- Load Issue7199.M in a separate process. Discard the output.
+  (runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
+     readUntilPrompt
+     load "Issue7199/M.agda"
+     readUntilPrompt)
+
+  -- Load Issue7199 again. Store the output.
+  output <- loadAndEcho "Issue7199.agda"
+
+  -- Restore Issue7199.M.
+  writeFile "Issue7199/M.agda" moduleM
+
+  -- Check the output.
+  if not ("(agda2-status-action \"Checked\")" `elem` output)
+  then do
+    putStrLn "The file Issue7199 was not successfully type-checked."
+    exitFailure
+  else if any ("Checking Issue7199.M" `isInfixOf`) output
+  then do
+    putStrLn "The file Issue7199.M was rechecked."
+    exitFailure
+  else do
+    putStrLn "The file Issue7199.M was not rechecked."
+    exitSuccess
diff --git a/test/interaction/Issue7199.out b/test/interaction/Issue7199.out
@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Type-checking*" "Checking Issue7199 (Issue7199.agda). " t)
+(agda2-status-action "Checked")
+(agda2-info-action "*All Done*" "" nil)
+((last . 1) . (agda2-goals-action '()))
+The file Issue7199.M was not rechecked.
diff --git a/test/interaction/Issue7199/M.agda b/test/interaction/Issue7199/M.agda
@@ -0,0 +1 @@
+module Issue7199.M where