Invalid pattern-match warnings related to strictness

Here are three function definitions that shouldn't generate a pattern-match warning:

{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyCase #-}
module Lib where

import Data.Type.Equality
import Data.Functor.Identity
import Data.Void

f :: a :~: Int -> a :~: Bool -> ()
f !_ x = case x of {}

g :: Identity (a :~: Int) -> a :~: Bool -> ()
g (Identity _) Refl = ()

data SMaybe a = SNothing
              | SJust !a

-- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
-- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
-- no longer in scope. Normally, we have no way of matching on that without a
-- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
-- evidence saying that @z@ must be 'Void' by matching on 'Void'.
h :: forall a. a :~: Void -> Bool -> ()
h _     True  | let y = undefined :: SMaybe a, SNothing <- y = ()
h Refl  False                                    = ()

Here's the current output:

test.hs:18:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘g’: g (Identity _) Refl = ...
   |
18 | g (Identity _) Refl = ()
   | ^^^^^^^^^^^^^^^^^^^^^^^^

I think we can properly solve this after #17248 (closed) (strictness of newtypes) and #17215 (long distance info) is settled. (Note that even with !1975 (closed), which fixes #17248 (closed), g generates a warning, because we assume that there's a non-void constraint on every variable we have facts about in the oracle.)