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, 8 insertions, 1 deletions

diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs
index 1a134d5dc8..8a6e07d84a 100644
--- a/compiler/utils/ListSetOps.hs
+++ b/compiler/utils/ListSetOps.hs
@@ -14,7 +14,7 @@ module ListSetOps (
         Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
 
         -- Duplicate handling
-        hasNoDups, removeDups, findDupsEq,
+        hasNoDups, removeDups, findDupsEq, insertNoDup,
         equivClasses,
 
         -- Indexing
@@ -169,3 +169,10 @@ findDupsEq _  [] = []
 findDupsEq eq (x:xs) | null eq_xs  = findDupsEq eq xs
                      | otherwise   = (x :| eq_xs) : findDupsEq eq neq_xs
     where (eq_xs, neq_xs) = partition (eq x) xs
+
+-- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
+-- when an equal element couldn't be found in @xs@.
+insertNoDup :: (Eq a) => a -> [a] -> [a]
+insertNoDup x set
+  | elem x set = set
+  | otherwise  = x:set