Pattern alternative binding empty type does not cause redundant alternative warning

So, lean has coverage checking in pattern-matching, e.g. this code...

def v : Option Bool -> Bool
| .none => false
-- | .some _ => true

...does not get accepted and missing case is reported. Good!

Lets now consider a slightly different definition:

def v' : Option Empty -> Bool
| .none => false

This one is considered correct by lean, no errors about missing cases are reported.
However, if I add another pattern to this definition...

def v' : Option Empty -> Bool
| .none => false
| .some _ => true -- offending pattern

...it still gets accepted without a warning. The redundant pattern is not reported as such!

This means that matches on empty types are redundant, but the helpful warning does not appear.

It would be helpful if it would, if possible.

Start by reproducing the two Option Empty definitions and compare their diagnostics with the Option Bool example. No file or test is named in the issue, so locate the pattern-matching coverage checker and add a regression test showing that the .some _ alternative produces a redundant-pattern warning; done means the warning appears without breaking valid empty-type matches.