Recursive exhaustivity checker for pattern

Motivation

GHC pattern exhaustivity checker is not able to compute exhaustivity when the cases are handled using a combination of multiples case or pattern in function operations.

For example, the following:

foo :: Bool -> String
foo True = "True"
foo i = case i of
  False -> "False"

bar :: Bool -> String
bar True = "True"
bar i = bir i
  where
    bir False = "False"

baz :: Bool -> String
baz i = case i of
  True -> "True"
  _ -> case i of
    False -> "False"

-- Amazingly this does not trigger a warning
baz' :: Bool -> String
baz' i = case i of
  True -> "True"
  False -> case i of
    False -> "False"


bur :: Bool -> String
bur True = "True"
bur i = case i of
  True -> "True"
  _ -> boz i
    where
      boz False = "False"


-- This should not fail
-- That's a proof that all function are total
test :: [String]
test = [foo, bar, baz, baz', bur] <*> [minBound..maxBound]

Implements five total functions (I tried multiples combination of case/equation pattern).

However warnings are generated for four of them:

BetterCase.hs:3:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: True
  |
3 | foo i = case i of
  |         ^^^^^^^^^...

BetterCase.hs:10:5: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘bir’: Patterns not matched: True
   |
10 |     bir False = "False"
   |     ^^^^^^^^^^^^^^^^^^^

BetterCase.hs:15:8: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: True
   |
15 |   _ -> case i of
   |        ^^^^^^^^^...

BetterCase.hs:32:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘boz’: Patterns not matched: True
   |
32 |       boz False = "False"
   |       ^^^^^^^^^^^^^^^^^^^
Ok, one module loaded.

It is interesting to observe that baz', which seems highly similar to baz does not trigger a warning.

Proposal

I'd like the exhaustivity checker to recognizes variations of theses cases and not generate a warning.