Coverage checker badly interacts with literals

[buzden]

Steps to Reproduce

Consider two variants of the same function:

f : (n : Nat) -> (Void, Void) -> Nat
f 0     (_, _) impossible
f 1     (_, _) impossible
f (S k) x = 5

f : (n : Nat) -> (Void, Void) -> Nat
f Z     (_, _) impossible
f (S Z) (_, _) impossible
f (S k) x = 5

They differ only in literal vs. direct constructors for 0 and 1. For some reason, pair in the second argument is important.

Expected Behavior

Both typecheck.

Observed Behavior

The second one typecheck, but the first one gives

Error: f is not covering.

CoverageFooledByLiterals:1:1--1:37
 1 | f : (n : Nat) -> (Void, Void) -> Nat
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Missing cases:
    f 0 _