Check EmptyCase by simply adding a non-void constraint

We can handle non-void constraints since !1733, so we can now express
the strictness of `-XEmptyCase` just by adding a non-void constraint
to the initial Uncovered set.

For `case x of {}` we thus check that the Uncovered set `{ x | x /~ ⊥ }`
is non-empty. This is conceptually simpler than the plan outlined in
 #17376, because it talks to the oracle directly.

In order for this patch to pass the testsuite, I had to fix handling of
newtypes in the pattern-match checker (#17248).

Since we use a different code path (well, the main code path) for
`-XEmptyCase` now, we apparently also handle #13717 correctly.
There's also some dead code that we can get rid off now.

`provideEvidence` has been updated to provide output more in line with
the old logic, which used `inhabitationCandidates` under the hood.

A consequence of the shift away from the `UncoveredPatterns` type is
that we don't report reduced type families for empty case matches,
because the pretty printer is pure and only knows the match variable's
type.

Fixes #13717, #17248, #17386

1 files changed, 3 insertions, 1 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T17248.hs b/testsuite/tests/pmcheck/should_compile/T17248.hs
index e320bd5184..095153fb08 100644
--- a/testsuite/tests/pmcheck/should_compile/T17248.hs
+++ b/testsuite/tests/pmcheck/should_compile/T17248.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns #-}
 module Lib where
 
 data T1 a = T1 a
@@ -10,6 +11,7 @@ f _      _    = ()
 
 g :: T2 a -> Bool -> ()
 g _      True = ()
-g (T2 _) True = ()
+g (T2 _) True = () -- redundant
+g !_     True = () -- inaccessible
 g _      _    = ()