TmOracle: Replace negative term equalities by refutable PmAltCons

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, 4 insertions, 0 deletions

diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs
index 632ea7742e..0b1cf435bc 100644
--- a/compiler/basicTypes/NameEnv.hs
+++ b/compiler/basicTypes/NameEnv.hs
@@ -25,6 +25,7 @@ module NameEnv (
 
         emptyDNameEnv,
         lookupDNameEnv,
+        delFromDNameEnv,
         mapDNameEnv,
         alterDNameEnv,
         -- ** Dependency analysis
@@ -147,6 +148,9 @@ emptyDNameEnv = emptyUDFM
 lookupDNameEnv :: DNameEnv a -> Name -> Maybe a
 lookupDNameEnv = lookupUDFM
 
+delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a
+delFromDNameEnv = delFromUDFM
+
 mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
 mapDNameEnv = mapUDFM