idris-lang
Totality Checker fails on definitions involving higher-order non-total functions
Steps to Reproduce
Consider the following code:
total
constant : Nat -> Nat
constant n = n
-- clearly this isn't total
explode : Nat -> Nat
explode n = explode (S n)
total -- ok, this is accepted by the totality checker
things : List (Nat -> Nat)
things = [constant, constant]
total -- error, the totality checker rejects this
things2 : List (Nat -> Nat)
things2 = [constant, explode]
Expected Behavior
Both things and things2 should be checked to be total. Since explode is never actually called, it should not affect the totality of things2.
Observed Behavior
Totality checker rejects things2.
Usability Impact
In my situation I have a list of functions as in things2 above, and I need to prove that the list of functions is NonEmpty. But since the totality checker rejects things2, in type checking things2 is never reduced to a Cons, and thus it seems impossible to prove that things2 is non-empty.
If this code is accepted, I fear that the totality checker might fail at the call site. In order to let it work we might need to distinguish total functions and non-total functions at the type level.
Yeah, I think its a bit of a subtle issue. I don't really need or expect a fix anytime soon, as I can just use believe_me to force my proof of NonEmpty.