Error message changes after interface file has been removed

[nad]

I ran the test suite with --compact-regions turned on, and noted that a test case related to sections failed. This problem can be reproduced without using --compact-regions:

$ agda --ignore-interfaces -itest/Fail/ -itest test/Fail/Sections-1.agda --no-libraries | grep '∸_ (postfix operator section'
  ∸_ (postfix operator section, level 6) [_-_ ([…]/Common/Nat.agda:6,21-24)]                                              
$ rm -f test/Common/Prelude.agdai
$ agda -itest/Fail/ -itest test/Fail/Sections-1.agda --no-libraries | grep '∸_ (postfix operator section'
  ∸_ (postfix operator section, level 6) [_-_ ([…]/lib/prim/Agda/Builtin/Nat.agda:23,1-4)]

Note that the error messages are not identical.

[sattlerc]

Here is a self-contained test case:

• Issue4472X/A.agda

module Issue4472X.A where

postulate
  +_ : Set → Set

• Issue4472X/B.agda

module Issue4472X.B where

open import Issue4472X.A public renaming (+_ to -_)

• Issue4472.agda

open import Issue4472X.B

_ = - -

On master (with or without compact regions patch 556be02), relevant part of the output of agda Issue4472.agda is as follows.

• If the interface file for Issue4472X.B is not used:

Operators used in the grammar:
  - (prefix operator, level 20) [+_ (Issue4472X/B.agda:3,49-51)]

• If the interface file for Issue4472X.B is used:

Operators used in the grammar:
  - (prefix operator, level 20) [+_ (Issue4472X/A.agda:4,3-5)]

Confusingly, the behaviour is different if the qualifier Issue4472X is renamed Issue4472. Then the relevant part of the output is always:

Operators used in the grammar:
  - (prefix operator, level 20) [+_ (Issue4472/B.agda:3,48-50)]

Why is that?

[sattlerc]

Intrigued why the qualifier name part should matter, I ran the test with the following set of files, with RENAME being some some parameter string.

• RENAME.agda

module RENAME where

postulate
  +_ : Set → Set

• B.agda

module B where

open import RENAME public renaming (+_ to -_)

• Test.agda

open import B

_ = - -

With no interface files used, the result is always:

Test.agda:3,5-8
Could not parse the application - -
Operators used in the grammar:
  - (prefix operator, level 20) [+_ (B.agda:3,38-40)]
when scope checking - -

With interface files used, the result depends on RENAME and is apparently pseudo-random, but consistent. For example:

• For

RENAME <- ["f","g","i","j","m","n","r","s","u","v","z"]

the relevant part of the output becomes

  - (prefix operator, level 20) [+_ (RENAME.agda:4,3-5)]

• For

RENAME <- ["a","b","c","d","e","h","k","l","o","p","q","t","w","x","y"]

the result is as with no interface files used.