Currently it's impossible to refer to syntax declarations in a using, hiding declaration etc. because they have no name. I propose that Agda should automatically generate a name for the syntax.

As a motivating example, we've just run into a problem in v2.0 of the standard library where we converted a definition:

https://github.com/agda/agda-stdlib/blob/0817da6877aa045932221134913d8511caa78d97/src/Relation/Binary/PropositionalEquality/Core.agda#L113

into syntax:

https://github.com/agda/agda-stdlib/blob/711ac53c07e4cb3328216288c1c6206814785e81/src/Relation/Binary/Reasoning/Syntax.agda#L401

which is nearly backwards compatible unless, as PLFA does, you import the definition named.

If for every syntax declaration, Agda automatically created a name for it with misfix holes _ substituted for the variable locations then we would be able to avoid this problem and have the ability to selectively hide and use syntax as would like.

Of course syntax that uses freshly bound variables might be problematic, but I would propose fresh variables simply get zapped in the name, e.g.

syntax step-↭-⟩ x yRz x↭y = x ↭⟨ x↭y ⟩ yRz        generates    _↭⟨_⟩_
syntax step-≡-∣ x xRy     = x ≡⟨⟩ xRy             generates    _≡⟨⟩_
syntax ∄-syntax (λ x → B) = ∄[ x ] B              generates    ∄[]_

Possibly related issues: #3790, #3481