[Agda-dev] Qualified full operator name now needs parentheses?

[Wolfram Kahl]

I'm still fighting my way through updating my developments
to a recent development version, and get errors that I consider as quite surprising:

 | Could not parse the application Setoid._≈_ S
 | (the treatment of operators has changed, so code that used to parse
 | may have to be changed)
 | when scope checking Setoid._≈_ S

Changing this to

  (Setoid._≈_) S

makes it parse --- is this requirement for parentheses intentional?
I don't find this mentioned in doc/release-notes/2-4-4.txt.


Related: Is there a way to declare fixity for operators that are
module parameters?
(Or even for function arguments?)


Also quite surprising are error messages resulting from

 | * If an overloaded operator is in scope with several distinct
 |   fixities, then several instances of this operator will be included
 |   in the operator grammar, possibly leading to ambiguity.

because the error message happily shows the two parses
as identical strings.
(I am not even sure that the different infix constructors had different fixity ---
 I'll have to check that when I encounter it again.)


Wolfram