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

4 files changed, 80 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
new file mode 100644
index 0000000000..fde022c5cb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
@@ -0,0 +1,15 @@
+-- | The following match demonstrates why we need to detect cyclic solutions
+-- when extending 'TmOracle.tm_pos'.
+--
+-- TLDR; solving @x :-> y@ where @x@ is the representative of @y@'s equivalence
+-- class can easily lead to a cycle in the substitution.
+module CyclicSubst where
+
+-- | The match is translated to @b | a <- b@, the initial unification variable
+-- is @a@ (for some reason). VarVar will assign @b :-> a@ in the match of @a@
+-- against @b@ (vars occuring in a pattern are flexible). The @PmGrd a b@ is
+-- desugared as a match of @$pm_x@ against @a@, where @$pm_x :-> b@, which is
+-- stored as @$pm_x :-> a@ due to the previous solution. Now, VarVar will
+-- assign @a :-> $pm_x@, causing a cycle.
+foo :: Int -> Int
+foo a@b = a + b
diff --git a/testsuite/tests/pmcheck/should_compile/PmExprVars.hs b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
new file mode 100644
index 0000000000..7b17cd5b66
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
@@ -0,0 +1,44 @@
+module PmExprVars where
+
+-- | Demonstrates why we can't lower constructors as flexible meta variables.
+-- If we did, we'd get a warning that cases 1 and 2 were redundant, implying
+-- cases 0 and 3 are not. Arguably this might be better than not warning at
+-- all, but it's very surprising having to supply the third case but not the
+-- first two cases. And it's probably buggy somwhere else. Delete this when we
+-- detect that all but the last case is redundant.
+consAreRigid :: Int
+consAreRigid = case False of
+  False -> case False of
+    False -> 0
+    True -> 1
+  True -> case False of
+    False -> 2
+    True -> 3
+
+data D a = A | B
+
+class C a where
+  d :: D a
+
+instance C Int where
+  d = A
+
+instance C Bool where
+  d = B
+
+-- | Demonstrates why we can't translate arbitrary 'HsVar'
+-- occurrences as 'PmExprVar's (i.e., meta variables). If we did, the following
+-- would warn that the cases 1 and 2 were redundant, which is clearly wrong
+-- (case 1 is the only match). This is an artifact of translating from the
+-- non-desugared 'HsExpr'. If we were to implement 'hsExprToPmExpr' in terms of
+-- 'CoreExpr', we'd see the dictionary application and all would be well. The
+-- solution is to look into the outer 'HsWrap' and determine whether we apply
+-- or abstract over any evidence variables.
+dictVarsAreTypeIndexed:: Int
+dictVarsAreTypeIndexed = case d :: D Int of
+  A -> case d :: D Bool of
+    A -> 0
+    B -> 1
+  B -> case d :: D Bool of
+    A -> 2
+    B -> 3
diff --git a/testsuite/tests/pmcheck/should_compile/T12949.hs b/testsuite/tests/pmcheck/should_compile/T12949.hs
new file mode 100644
index 0000000000..90fe024067
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T12949.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module T12949 where
+
+class Foo a where
+  foo :: Maybe a
+
+data Result a b = Neither | This a | That b | Both a b
+
+q :: forall a b . (Foo a, Foo b) => Result a b
+q = case foo :: Maybe a of
+      Nothing -> case foo :: Maybe b of
+                   Nothing -> Neither
+                   Just c -> That c
+      Just i -> case foo :: Maybe b of
+                   Nothing -> This i
+                   Just c -> Both i c
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index e04f2cf07c..5fe7d9edd1 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -94,8 +94,13 @@ test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T12949', [],  compile, ['-fwarn-overlapping-patterns'])
 test('T12957', [], compile, ['-fwarn-overlapping-patterns'])
 test('T12957a', [], compile, ['-fwarn-overlapping-patterns'])
+test('PmExprVars', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('CyclicSubst', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # EmptyCase
 test('T10746', [], compile,