Agda: labels with same letters but different cases (first char) may break the compilation

[Commelina]

Reproduce

Consider the following test.cf:

OpEq. Op ::= "=" ;
opEq. Op ::= "~" ;

define opEq = OpEq ;

Run bnfc --haskell --agda -d -m test.cf && make (after #560 is fixed):

/tmp/Test/AST.agda:29.1-5: error: [ClashingDefinition]
Multiple definitions of opEq. Previous definition at
/tmp/Test/AST.agda:25.5-9
when scope checking the declaration
  opEq : Op

Note

The problem is because the Agda backend transforms all data constructors into non-leading-capital forms (in Agda a constructor cannot overload a data type with the same name). However, it can be not that rare to use constructors with only the first character lowercase, especially when using define.

It is totally fine to mark it as unsupported. But maybe the behavior should be mentioned in the docs.