[ fix #3437 ] Add a check for multiple totality modifiers

[spcfox]

Description

• Added check for multiple totality modifiers in processFnOpt.
• elabImplementation does not add a totality modifier from the interface if it is overridden in the implementation. This is to prevent multiple modifiers from appearing after desugaring.
• Added a check for totality modifiers when desugaring declarations, as they may not spawn functions (interfaces without implementations or without methods). I'm not sure if this is the right place.
• Added processing of totality modifier on forward-declared data (See Update error messages for conflicting or redundant totality modifiers #3442 (comment)).

Checking when desugaring is enough for Idris, but I left the changes to processFnOpt as they also check TTImp.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[andrevidela]

Would be nice if the message could explain why that's a problem and how to fix it. GenericMsgSol should give you a way to do that.

something like

"Multiple incompatible totality modifier were given for this function." And give multiple ways to solve it. Either by relying on the default totality or by overriding the default.

[spcfox]

"Multiple incompatible totality modifier were given for this function." And give multiple ways to solve it. Either by relying on the default totality or by overriding the default.

I think any use of multiple totality modifiers (including identical ones) on a single declaration should be an error. The default totality no matter.

[andrevidela]

The default totality no matter. (sic)

This is incorrect.

%default total

covering
main : IO ()
main = …

is a common pattern.

In the case of multiple definitions, like total covering the message should say to either remove total and keep covering or remove both and rely on %default total. Similarly if you get covering covering, just change the message explaining why it's bad.

[spcfox]

I mean, the presence of %default does not affect the presence of this error, so it's strange to suggest the user to remove all totality modifiers from the declaration and rely on %default.

[andrevidela]

Alright I'll do it myself

[mattpolzin]

Regardless of the goals of this PR, I’d add that in my opinion it’s ok to have e.g. a %default total plus an explicit total on a function. Sure, the latter is redundant, but it’s harmlessly explicit and it could come into play if the default is modified so there’s a practical impact of it.

That is, in my opinion the only thing that should be an error is if there are multiple totalities defined explicitly on the function.

[andrevidela]

Let's get this in and someone else will implement #3442

[spcfox]

Okay, I understand the errors you suggest. I'll add them

[spcfox]

I have tried to make correct error messages that take into account the presence of all totality modifiers. This commit does not affect the ability to override totality in Data

[spcfox]

I'm sorry if my messages might have come across as rude. I don't always know the best way to express my thoughts in English

[mattpolzin]

I think your messages are coming across just fine (no rude tone detected by me, at least).

[mattpolzin]

Is this throwing away the explicit totality passed to this function quietly? Seems like that could result in surprising behavior.

[spcfox]

treq is a totality from a function declaration in the interface. If the implementation contains its own totality modifier, it is overrided. Previously both flags were left, but this is not useful. See #3437 (comment)