Interaction of totality and coverage checking

[danelahman]

Consider the following code snippets

%default total

covering
f : Int -> Int
f i = f i

total
covering
f : Int -> Int
f i = f i

Steps to Reproduce

Using idris2--0.7.0_3.arm64_sonoma on MacOS Sonoma 14.7.1 installed via Homebrew.

Expected Behavior

In both cases, I would expect to still get an error message about the function f not being total (being nonterminating):

Error: f is not total, possibly not terminating due to recursive path Main.f

Observed Behavior

No error message about f not being total (being nonterminating), neither using CLI nor using the Idris Language VS Code plugin.

[gallais]

In the first example I wouldn't expect such an error given that you purposefully overrode the default.

In the second example, I would expect an error message pointing out the incompatible totality annotations.

[spcfox]

I tried to fix this: spcfox@238f914

But with this fix, the error about multiple totality modifiers occurs in the following code:

interface Inhabited a where
  total
  element : a

covering
Inhabited () where
  element = ()

Similar place in the compiler code:

Idris2/src/Core/Name.idr

Lines 264 to 265 in 826b7eb

	covering
	[Raw] Show Name where