TmOracle: Replace negative term equalities by refutable PmAltConswip/pmcheck-refuts

The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".

This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.

So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.

This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.

See the Note [Refutable shapes] in TmOracle for a place to start.

Metric Decrease:
    T11195

1 files changed, 1 insertions, 0 deletions

diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index e2d789b172..e8e6bf7317 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -327,6 +327,7 @@ Library
         MkCore
         PprCore
         PmExpr
+        PmPpr
         TmOracle
         Check
         Coverage