Totality checker fails to recognize missing cases on irrelevant parameter in irrelevant function

[Adowrath]

total 0
unlift : (0 x : Bool) -> (x == x) = True
unlift True = Refl
-- unlift False = Refl

The totality/coverage checker fails to recognize that this definition isn't total, but only if both unlift and x are marked as irrelevant. It correctly identifies the missing coverage if x is made relevant. This works with other types, like Bits8 and a valid number, as well.

Loading the file in the REPL, and using irrelevantEq to recover a value shows the discrepancy:

> irrelevantEq (unlift True)
Refl
> irrelevantEq (unlift False)
irrelevantEq (unlift False)

Using a similar definition thanks to @gallais, is is possible to prove Void:

total 0
unlift : (0 x : Bool) -> ifThenElse x Unit Void
unlift True = ()

total
boom : Void
boom = void $ unlift False

[gallais]

I suspect it's due to the checker seeing the Bool is 0 and so it assumes the pattern must have been forced by another split. Except that we are in an erased context and so are allowed to split on 0s...