Update error messages for conflicting or redundant totality modifiers

[andrevidela]

Follow up from #3441 :

Redundant or conflicting totality modifiers do not explain why they are a problem and to not provide the user with a path toward resolution.

No error, redundant but unique modifier

module M

covering
fn : String

This is fine, although the modifier is redundant because files are covering by default it makes clear the intent that this function is meant to be covering, even if the default modifier changes.

No error, different and unique modifier

module M

%default total

covering
fn : String

This is expected, the function fn does not follow the default and needs a bespoke modifier.

Error: incompatible modifier

module M

covering total
fn : a

This is an error since there is no way to know what modifier the user intended for this program. The solutions for it should be to:

• remove covering
• remove total
• remove both

Error: duplicate modifier

module M

covering covering
fn : String

This is an error. There is no reason to put the modifier twice, and changing only one of them will result in an error. In this case, we should as the user to either:

• remove one covering
• remove both covering since the default is covering

Conclusion

The appropriate error messages should also be adapted when the default is not covering

[dunhamsteve]

Another case is forward declarations of data and records, conflicting declarations should be disallowed.

covering
data Foo : Type

total
data Foo : Type where

But leaving it off of the second one should be allowed:

covering
data Foo : Type

data Foo : Type where

This behavior is consistent with the way public export vs export are handled today:

public export
data Foo : Type

export
data Foo : Type where

gives a warning:

1/1: Building Foo (Foo.idr)
Warning: Main.Foo has been forward-declared with public export visibility, cannot change to export. This will be an error in a later release.

[spcfox]

The totality of the data declaration doesn't seem to count for anything right now:

%default total

partial
data D : Type

failing "D is not total, not strictly positive"
  data D where
    Abs : (D -> D) -> D