Agda: No error location for error in imported module when .agdai file exists

[msuperdock]

The general issue

Suppose we have files Test1.agda and Test2.agda, such that Test2 imports Test1, either directly or indirectly, with no open interaction points in Test1, Test2, or any of their dependencies. Then:

• Run agda Test2.agda, generating Test1.agdai and Test2.agdai.
• Modify Test1.agda so that it contains at least one or more interaction points (none of them implicit).
• Run agda Test2.agda again. (No error location is given.)
• Delete Test2.agdai and run agda Test2.agda again. (An error location is now given.)

The issue is that no error location is given in the third step. This can make it difficult to figure out where the open interaction point actually is, especially if you don't know the workaround of deleting the interface file.

How to reproduce

Here's a more explicit description of how to reproduce this issue. Create files as follows:

Test1.agda:

module Test1 where

data ⊤
  : Set
  where

  tt
    : ⊤

x
  : ⊤
x
  = tt

Test2.agda:

module Test2 where

import Test1

• Run agda Test2.agda, generating interface files for both modules.
• Replace the tt in the last line of Test1.agda with ?.
• Run agda Test2.agda again.

The result:

 Checking Test1 (/data/code/agda-test/Test1.agda).
Module cannot be imported since it has open interaction points
(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this
module)

• Delete Test2.agdai.
• Run agda Test2.agda again.

The result:

Checking Test2 (/data/code/agda-test/Test2.agda).
 Checking Test1 (/data/code/agda-test/Test1.agda).
/data/code/agda-test/Test2.agda:3,1-13
Module cannot be imported since it has open interaction points
(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this
module)
when scope checking the declaration
  import Test1

Notice the helpful location information which is missing when the Test2.agdai file already exists.

Notes

When running agda from the terminal, this issue is not too painful, since the user should be able to tell which module has open interaction points by looking at the "Checking" message just before the error. But in editor plugins, including the emacs mode, this is more of a problem, since the user sees the "Checking" messages only in passing.

This issue is broader than just the "Module cannot be imported" error. For example, if instead of replacing tt with ?, we add a new line to the end of Test1.agda with content y = ?, then we've added implicit interaction points to Test1 as well as an explicit one. In this case the error message begins with "Unsolved metas." In this case also, the output is different depending on whether a Test2.agdai file exists; if it does, we get just the naked error message, and if it doesn't, we get the error message with additional location information before and after as in the example above.

[MatthewDaggitt]

:+1: from me. This behaviour can be incredibly irritating. Thank you for discovering and publishing the work around!

[UlfNorell]

Thanks for the great analysis. I think I can fix this.

[UlfNorell]

The problem was that in the case of the existing interface we fail too early, already when checking the hash of the interface of Test1. At that point we don't have the source location of the import. The fix is to simply discard the interface if we can't get the hash without errors. That triggers rechecking and we'll get the error at a point where we actually have the import source location.