Totality annotations are ignored

[ohad]

Steps to Reproduce

run idris2 totality.idr where totality.idr is:

total
foo : a
foo = foo

Expected Behavior

- + Errors (1)
 `-- totality.idr line 3 col 0:
     Main.foo is possibly not total due to recursive path Main.foo --> Main.foo

Observed Behavior

$ idris2 totality.idr 
1/1: Building totality (totality.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :total foo
Main.foo is not terminating due to recursive path Main.foo

[edwinb]

Yes, indeed, they are :). I should probably get around to implementing this sooner rather than later...

[ohad]

Thanks --- definitely not blocking me, just filing it for future reference.

[mx00s]

Is there a target version for this fix?

I was surprised to see unhandled cases, in addition to unproductive self-reference, aren't checked. For example,

total
vadd : Num a => Vect n a -> Vect n a
vadd [] = []
-- vadd (x :: xs) = x :: xs