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

[Nils Anders Danielsson]

On 2015-03-20 01:45, Wolfram Kahl wrote:
> 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.

This could be a bug. Please report this on the issue tracker.

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

I don't think so.

> 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.)

The error messages were recently improved (?). Now you get information
about all the operators that were used to construct the parser.

The treatment of overloaded operators with conflicting fixities is still
up for discussion:

   Overloaded operators with distinct precedence levels are not handled
     correctly
   https://code.google.com/p/agda/issues/detail?id=1436

-- 
/NAD