Unnecessary warning for syntax declarations in parameterless submodules

[MatthewDaggitt]

I'm trying to do the following in the standard library in the fix for agda/agda-stdlib#2146:

module Test where

postulate C : Set

module SyntaxA where
  syntax C = A

module SyntaxB where
  syntax C = B

i.e. have different modules export the different pieces of syntax, so that users can pick whichever syntax they like for the same declaration by opening either SyntaxA or SyntaxB modules.

However I'm getting the following warnings:

warning: -W[no]UnknownNamesInFixityDecl
The following names are not declared in the same scope as their
syntax or fixity declaration (i.e., either not in scope at all,
imported from another module, or declared in a super module): C
when scope checking the declaration
  module SyntaxA where

warning: -W[no]UnknownNamesInFixityDecl
The following names are not declared in the same scope as their
syntax or fixity declaration (i.e., either not in scope at all,
imported from another module, or declared in a super module): C
when scope checking the declaration
  module SyntaxB where

So my question is: are these warnings justified? Or can this check be relaxed if the syntax declaration's scopes parameterisations are identical as in the case above?

[andreasabel]

syntax is implemented like infix, it is not scoped in modules but always attaches just to a name.
So I think, with the current theory and implementation of syntax, I think it is not possible what you want to do here.

But it looks like the code in agda/agda-stdlib#2146 (comment) would not be affected by this shortcoming.

@MatthewDaggitt wrote:

module SyntaxB where
  syntax B = A

Did you mean syntax C = B here?

On how to address the OP:
renaming is available for infix, maybe we should enable it for syntax as well?

open Test renaming (C to syntax C = A)
open Test renaming (C to syntax C = B)

[MatthewDaggitt]

Did you mean syntax C = B here?

Yes sorry!

But it looks like the code in agda/agda-stdlib#2146 (comment) would not be affected by this shortcoming.

Sorry, see this later issue for the revised proposal that is even neater if we can rename syntax.

[MatthewDaggitt]

On how to address the OP:
renaming is available for infix, maybe we should enable it for syntax as well?

open Test renaming (C to syntax C = A)
open Test renaming (C to syntax C = B)

Yes, that would work!