PmCheck: Rewrite inhabitation test

We used to produce inhabitants of a pattern-match refinement type Nabla
in the checker in at least two different and mostly redundant ways:

  1. There was `provideEvidence` (now called
     `generateInhabitingPatterns`) which is used by
     `GHC.HsToCore.PmCheck` to produce non-exhaustive patterns, which
     produces inhabitants of a Nabla as a sub-refinement type where all
     match variables are instantiated.
  2. There also was `ensure{,All}Inhabited` (now called
     `inhabitationTest`) which worked slightly different, but was
     whenever new type constraints or negative term constraints were
     added. See below why `provideEvidence` and `ensureAllInhabited`
     can't be the same function, the main reason being performance.
  3. And last but not least there was the `nonVoid` test, which tested
     that a given type was inhabited. We did use this for strict fields
     and -XEmptyCase in the past.

The overlap of (3) with (2) was always a major pet peeve of mine. The
latter was quite efficient and proven to work for recursive data types,
etc, but could not handle negative constraints well (e.g. we often want
to know if a *refined* type is empty, such as `{ x:[a] | x /= [] }`).

Lower Your Guards suggested that we could get by with just one, by
replacing both functions with `inhabitationTest` in this patch.
That was only possible by implementing the structure of φ constraints
as in the paper, namely the semantics of φ constructor constraints.

This has a number of benefits:

  a. Proper handling of unlifted types and strict fields, fixing #18249,
     without any code duplication between
     `GHC.HsToCore.PmCheck.Oracle.instCon` (was `mkOneConFull`) and
     `GHC.HsToCore.PmCheck.checkGrd`.
  b. `instCon` can perform the `nonVoid` test (3) simply by emitting
     unliftedness constraints for strict fields.
  c. `nonVoid` (3) is thus simply expressed by a call to
     `inhabitationTest`.
  d. Similarly, `ensureAllInhabited` (2), which we called after adding
     type info, now can similarly be expressed as the fuel-based
     `inhabitationTest`.

See the new `Note [Why inhabitationTest doesn't call generateInhabitingPatterns]`
why we still have tests (1) and (2).

Fixes #18249 and brings nice metric decreases for `T17836` (-76%) and
`T17836b` (-46%), as well as `T18478` (-8%) at the cost of a few very
minor regressions (< +2%), potentially due to the fact that
`generateInhabitingPatterns` does more work to suggest the minimal
COMPLETE set.

Metric Decrease:
    T17836
    T17836b

3 files changed, 58 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T18249.hs b/testsuite/tests/pmcheck/should_compile/T18249.hs
new file mode 100644
index 0000000000..b9bd048cbd
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18249.hs
@@ -0,0 +1,36 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+module T18249 where
+
+import GHC.Exts
+
+f :: Int# -> Int
+-- redundant, not just inaccessible!
+f !_ | False = 1
+f _ = 2
+
+newtype UVoid :: TYPE 'UnliftedRep where
+  UVoid :: UVoid -> UVoid
+
+g :: UVoid -> Int
+-- redundant in a weird way:
+-- there's no way to actually write this function.
+-- Inhabitation testing currently doesn't find that UVoid is empty,
+-- but we should be able to detect the bang as redundant.
+g !_ = 1
+
+h :: (# (), () #) -> Int
+-- redundant, not just inaccessible!
+h (# _, _ #) | False = 1
+h _ = 2
+
+i :: Int -> Int
+i !_      | False = 1
+i (I# !_) | False = 2
+i _               = 3
+
diff --git a/testsuite/tests/pmcheck/should_compile/T18249.stderr b/testsuite/tests/pmcheck/should_compile/T18249.stderr
new file mode 100644
index 0000000000..b13160e183
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18249.stderr
@@ -0,0 +1,20 @@
+
+T18249.hs:14:8: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f !_ | False = ...
+
+T18249.hs:25:4: warning: [-Wredundant-bang-patterns]
+    Pattern match has redundant bang
+    In an equation for ‘g’: g _ = ...
+
+T18249.hs:29:16: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘h’: h (# _, _ #) | False = ...
+
+T18249.hs:33:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘i’: i !_ | False = ...
+
+T18249.hs:34:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘i’: i (I# !_) | False = ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index c2f14ce664..bd5fc60f63 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -134,6 +134,8 @@ test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18049', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18249', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns -Wredundant-bang-patterns'])
 test('T18273', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18341', normal, compile,