Agda re-checks a file with an up-to-date interface file

[nad]

Consider the following workflow:

• You load the module B.agda, which imports A.agda, in (say) Emacs.
• You edit A.agda and type-check it by invoking Agda using a shell command.
• You reload B.agda in Emacs.

In this case you might hope that A.agda should not be type-checked again (if the same options are in effect). However, I have observed that, in at least some cases, Agda does type-check the file again instead of loading the interface file.

This is a regression, Agda 2.6.1.2 does not have this bug, but Agda 2.6.2 does. Bisection points towards @rwe's commit 7119290 ("imports/refact: Combine more conditions in getStoredInterface").

Here is a script that can be used to demonstrate the bug:

#!/usr/bin/env runhaskell

{-# LANGUAGE RecordWildCards #-}

import Data.List
import System.Exit

import RunAgda

moduleA      = "module A where\n"
moduleAExtra = "postulate A : Set\n"
moduleB      = "module B where\nimport A\n"

main :: IO ()
main = runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do

  -- Discard the first prompt.
  echoUntilPrompt

  -- Write A and B.
  writeFile "A.agda" moduleA
  writeFile "B.agda" moduleB

  -- Load B.
  loadAndEcho "B.agda"

  -- Modify A.
  writeFile "A.agda" (moduleA ++ moduleAExtra)

  -- Load A in a separate process.
  (runAgda ["--no-libraries"] $ \(AgdaCommands { .. }) -> do
     echoUntilPrompt
     loadAndEcho "A.agda")

  -- Load B again.
  output <- loadAndEcho "B.agda"

  -- Restore A.
  writeFile "A.agda" moduleA

  -- Check the output.
  if not ("(agda2-status-action \"Checked\")" `elem` output) ||
     any ("Checking A" `isInfixOf`) output
  then exitFailure
  else exitSuccess