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 PmAltCons (which are
just PmLits at the moment) to each variable denoting above
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.