Oh, interesting. After poking around a little, I think that the following happens:

• When loading A.agda for the second time, top-level interaction mode prevents createInterface from actually writing the interface file A.agdai for the modified A.agda.

• Now the source code A.agda (actually: its hash value) doesn't match A.agdai (actually: the source code hash value embedded in it). That's why A.agdai is (rightfully) considered to not be up-to-date when loading B.agda and thus A.agda gets type-checked again.

I think that I get why Agda won't load interface files in top-level interaction mode. As I understand it, interface files only contain a subset of the information gathered during the type-check. In particular, they lack information required by the top-level interaction mode.

But why doesn't Agda save interface files in top-level interaction mode? To speed up the type-check by skipping serialization and compression?

In any case, it seems that the --top-level-interaction-no-private flag doesn't change this behavior. cmd_load' always receives a TypeCheck TopLevelInteraction from the Cmd_load handler. Unless the current top-level file changes, this seems to get passed all the way down to typeCheckMain unchanged. (That's why it takes two loads of A.agda to trigger the issue. The second load doesn't change the current top-level file.) typeCheckMain wraps it in a MainInterface, which ultimately ends up in createInterface, where it prevents writing A.agdai.

After reading the comments on PR #4652 it seems that the .agdai files aren't written in top-level interaction mode, because top-level interaction mode keeps extra information on a module (its private declarations) that's not supposed to go in the .agdai file. So, this behavior is about more than just serialization and compression.

To address this issue, could createInterface in top-level interaction mode still do writeInterface, but ignore the stripped interface returned by writeInterface? So, when in top-level interaction mode, just strip the interface for the sake of serializing it to the .agdai file, but then keep using the original unstripped interface?

The following test with current master seems to indicate that this would do the trick, at least on the small scale of the given test case. What would be the downsides of doing something along these lines?

tlo@carol:~/agda/mine/test/interaction$ git diff
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 9170b8851..324fb0737 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -1056,6 +1056,8 @@ createInterface file mname isMain msi =
         return i
       (_, MainInterface (TypeCheck TopLevelInteraction)) -> do
         reportSLn "import.iface.create" 7 "We are in top-level interaction mode and want to retain private declarations, skipping writing interface file."
+        ifile <- toIFile file
+        _ <- writeInterface ifile i
         return i
       _ -> Bench.billTo [Bench.Serialization] $ do
         reportSLn "import.iface.create" 7 "Actually calling writeInterface."
tlo@carol:~/agda/mine/test/interaction$ stack runghc Issue4959.hs agda
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Issue4959-2 (/home/tlo/agda/mine/test/interaction/Issue4959-2.agda).\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Issue4959-2 (/home/tlo/agda/mine/test/interaction/Issue4959-2.agda).\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Issue4959 (/home/tlo/agda/mine/test/interaction/Issue4959.agda).\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
tlo@carol:~/agda/mine/test/interaction$ 

If work on this issue has stalled, then I suggest that we undo the fix of #4647.

👍 on undoing the fix

I spent some time this week on this issue, let's see if I can carve out more time.

In PR #5402 I am ripping out the fix for #4647, as I do not have the time atm for a proper investigation. Maybe after the release we can revisit #4647 (maybe...).