This happens primarily when printing the Call, i.e. "when [...]" part of the error message. If the user wrote it, we should be able to point to it in her file. We do not have an exact printer, and abstract syntax is already desugared ("nicified") compared to what the user wrote. Consequently, the errors are both inaccurate and overly verbose. Compare the declaration:
xwheredataD(A:Set):Setwherec:DAwith the error message:
/home/amelia/default/Projects/agda/test/Fail/AbsToConDecl.agda:3.1-5.14:error:[AbsentRHSRequiresAbsurdPattern]Theright-handsidecanonlybeomittedifthereisanabsurdpattern,()or{},intheleft-handside.whencheckingthattheclausexwheremutualdataD(A:Set):Setwherec:DAhastype_1This happens primarily when printing the `Call`, i.e. "when [...]" part of the error message. If the user wrote it, we should be able to point to it in her file. We do not have an exact printer, and abstract syntax is *already* desugared ("nicified") compared to what the user wrote. Consequently, the errors are both inaccurate *and* overly verbose. Compare the declaration:
```agda
x where
data D (A : Set) : Set where
c : D A
```
with the error message:
```agda
/home/amelia/default/Projects/agda/test/Fail/AbsToConDecl.agda:3.1-5.14: error: [AbsentRHSRequiresAbsurdPattern]
The right-hand side can only be omitted if there is an absurd
pattern, () or {}, in the left-hand side.
when checking that the clause
x where
mutual
data D (A : Set) : Set where
c : D A
has type _1
```