Warning for incomplete irrefutable patterns is confusing

Edit by @sgraf812: There is a single vestigial TODO in this issue: Introduce a separate flag to control generation of warnings for irrefutable patterns that is not part of -Wall (for some reason). This will require a GHC proposal.

Summary

Pattern exhaustive check is broken for lazy/irrefutable patterns

Steps to reproduce

https://play.haskell.org/saved/o5fg9jiD

try to compile this code with version 9.2+

{-# OPTIONS_GHC -Wall #-}

main :: IO ()
main = foo undefined undefined undefined

foo :: [Either a1 b] -> [a2] -> [a3] -> a4
foo [] _ _ = undefined
foo (Left _ : _) ~(_a:_as) _ = undefined
foo (Right _ : _) _ ~(_a:_as) = undefined
foo _ _ _ = undefined

It produces three warnings. Patterns are non-exhaustive and redundant at the same time:

Main.hs:7:1: warning: [-Wincomplete-uni-patterns]
    Pattern match(es) are non-exhaustive
    In a pattern binding: Patterns of type ‘[a3]’ not matched: []
  |
7 | foo [] _ _ = undefined
  | ^^^^^^^^^^^^^^^^^^^^^^...

Main.hs:7:1: warning: [-Wincomplete-uni-patterns]
    Pattern match(es) are non-exhaustive
    In a pattern binding: Patterns of type ‘[a2]’ not matched: []
  |
7 | foo [] _ _ = undefined
  | ^^^^^^^^^^^^^^^^^^^^^^...

Main.hs:10:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘foo’: foo _ _ _ = ...
   |
10 | foo _ _ _ = undefined
   | ^^^^^^^^^^^^^^^^^^^^^

Expected behavior

Expected only one warning about redundant pattern:

Main.hs:10:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘foo’: foo _ _ _ = ...
   |
10 | foo _ _ _ = undefined
   | ^^^^^^^^^^^^^^^^^^^^^

Environment

• GHC version used: 9.2, 9.4, 9.6, 9.8