Pattern match checker stumbles over reasonably tricky pattern-match

In !2192 (comment 247043) Simon finally convinced me that it's reasonable to record type constraints arising from a constructor application in a CoreExpr in the pattern-match checkers type oracle. Namely

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}

module Lib where

data S a where
  S1 :: S Int
  S2 :: S Bool

data T where
  K :: S a -> a -> T

f1 :: S Int -> ()
f1 s = case K @Int s 3 of K S1 _ -> ()

f2 :: S Int -> ()
f2 s = case K @Int s 3 of K s' _ -> case s' of S1 -> ()

data T2 where
  K2 :: (a -> S a) -> a -> T2

g1 :: (Int -> S Int) -> ()
g1 h = case K2 @Int h 3 of K2 h' (h' -> S1) -> ()

g2 :: (Int -> S Int) -> ()
g2 h = case K2 @Int h 3 of K2 h' i' -> case h' i' of S1 -> ()

All pattern matches are exhaustive, yet we currently only flag f1 as such. It's easy to also flag the other cases if we simply record that the a bound by K (and K2, respectively) is subject to the constraint a ~ Int, which is easiest to see by looking at the case's scrutinee.

Taking f2 as the example, the not-so-easy way would be to see that s' ~ s (we already make that connection!), and then from the fact that s :: S Int derive that S2 is not a possible constructor for s, so it can't be for s'. Sadly, apparently we don't make the connection to s's type.