Totality checking indicates wrong clause

[eraserhd]

Totality checking, in its current design, reports the extent of the first equation. This is a bit more misleading now that the span is computed correctly, since it looks like it's trying to indicate which clause is non-total.

Steps to Reproduce

total
foo : Nat -> Nat
foo Z = 42
foo x = 1 + foo x + 2

Expected Behavior

At least:

/tmp/foo.idr:4:1-21:Main.foo is possibly not total due to recursive path Main.foo --> Main.foo

Better:

/tmp/foo.idr:4:13-17:Main.foo is possibly not total due to recursive path Main.foo --> Main.foo

Observed Behavior

/tmp/foo.idr:3:1-10:Main.foo is possibly not total due to recursive path Main.foo --> Main.foo

[unalos]

As far as the source code goes, this is intended behavior.

The error message is what is given for mutually recursive declarations. For instance

total
foo : Nat -> Nat
foo Z = 42
foo x = 1 + bar x + 2

total
bar : Nat -> Nat
bar x = foo x

In your case, there is only one "mutually" recursive function, which is foo (hence the Main.foo --> Main.foo illegal path).

The error message seems to give the wrong clause because it describes the recursively looping path, not the clause invoking the recursion. It makes more sense in the foo/bar mutually recursive functions than in the example provided, so I'm not so sure we should be fixing this issue.