## 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.