Potential bug in the totality checker

[xuanruiqi]

Problem:

Totality checker seems to have a bug. Specifically, the Idris totality checker thinks this function is not total:

blacken : Tree d c a -> Tree (incrBlack d (inv c)) Black a
blacken Leaf = Leaf
blacken (Node Red _ _ l v r) = Node Black () () l v r
blacken (Node Black _ _ l v r) = Node Black () () l v r

Clearly, this is total as it contains all possible cases (obviously, there are only three cases in a red-black tree). In fact, issuing :missing blacken in the Idris REPL gives me the missing case:

blacken (Node Black _ _ _ _ _)

which has clearly already been covered!

On the other hand, Idris correctly identifies this as total:

blacken : Tree d c a -> Tree (incrBlack d (inv c)) Black a
blacken Leaf = Leaf
blacken (Node c _ _ l v r) with (c)
  | Red = Node Black () () l v r
  | Black = Node Black () () l v r

However it is clear that this is equivalent to the original, which Idris thinks is not total.

This file here contains the full implementation, for your reference. If you replace the second version of blacken with the first, the bug should be replicated.

I am using the latest released version of Idris, v1.3.1.

[zenntenn]

So, I don't know specifically why Idris is not sure that's total. However, in general for things like this it's ususally not a bug, rather what you have here is a feature request (assuming we're not missing a reason this isn't total). Totality checking in the general case is the Halting problem, so Idris instead looks for specific examples of ways that are guaranteed to find totality. If it can't find them, then it marks it as possibly not total, because it doesn't know. New ways of checking for totality can be created, but lacking them is not really a bug.

Also, you're only looking that all cases are covered. Total means that all cases are covered and it is guaranteed to never get stuck in an infinite loop. If you just want to check all cases are covered use the covering keyword, not the total keyword.

[david-christiansen]

While @zenntenn is right that the problem is undecidable and that Idris will only ever do a conservative approximation of totality checking, this case looks to me like the kind of thing that Idris should be supporting well. It's not recursive, so we don't have to worry about loops. The only thing that's not immediately easy to check here is that incrBlack and inv need to have a concrete color in order to reduce, but I would think that the case tree does indeed split there.

Anyway, I don't know what's wrong, but I do think that this is not at all a bonkers bug report!

[xuanruiqi]

@zenntenn blacken is not recursive, corecursive or mutually recursive, so there is no well-foundedness/productivity check necessary, and totality essentially reduces to coverage here.

Also, given that Idris can correctly tell that blacken version 2 is total, IMO there's no reason that it would not be able to tell that blacken version 1 is total! To me, it clearly looks like a bug, not a missing feature.

[xuanruiqi]

Any updates on this?