PmCheck: Record type constraints arising from existentials in `PmCoreCt`s

In #17703 (a follow-up of !2192), we established that contrary to my
belief, type constraints arising from existentials in code like

```hs
data Ex where Ex :: a -> Ex
f _ | let x = Ex @Int 15 = case x of Ex -> ...
```

are in fact useful.

This commit makes a number of refactorings and improvements to comments,
but fundamentally changes `addCoreCt.core_expr` to record the type
constraint `a ~ Int` in addition to `x ~ Ex @a y` and `y ~ 15`.

Fixes #17703.

2 files changed, 29 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T17703.hs b/testsuite/tests/pmcheck/should_compile/T17703.hs
new file mode 100644
index 0000000000..b4ac6dfd72
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17703.hs
@@ -0,0 +1,27 @@
+{-# 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 -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 47aa073c66..9d37f36fe5 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -110,6 +110,8 @@ test('T17465', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17646', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17703', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,