PmCheck: Handle ⊥ and strict fields correctly (#18341)wip/T18341

In #18341, we discovered an incorrect digression from Lower Your Guards.
This MR changes what's necessary to support properly fixing #18341.

In particular, bottomness constraints are now properly tracked in the
oracle/inhabitation testing, as an additional field
`vi_bot :: Maybe Bool` in `VarInfo`. That in turn allows us to
model newtypes as advertised in the Appendix of LYG and fix #17725.
Proper handling of ⊥ also fixes #17977 (once again) and fixes #18670.

For some reason I couldn't follow, this also fixes #18273.

I also added a couple of regression tests that were missing. Most of
them were already fixed before.

In summary, this patch fixes #18341, #17725, #18273, #17977 and #18670.

Metric Decrease:
    T12227

14 files changed, 220 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T10183.hs b/testsuite/tests/pmcheck/should_compile/T10183.hs
new file mode 100644
index 0000000000..6a02647fa9
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T10183.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, DataKinds, TypeOperators, UnicodeSyntax #-}
+
+module Foo where
+
+import GHC.TypeLits
+
+data List l t where
+     Nil  ∷ List 0 t
+     (:-) ∷ t → List l t → List (l+1) t
+
+head' ∷ (1<=l) ⇒ List l t → t
+head' (x :- _) = x
+
+data T a where
+  TT :: T Bool
+  TF :: T Int
+
+f :: T Bool -> Bool
+f TT = True
+
+g :: (a ~ Bool) => T a -> Bool
+g TT = True
diff --git a/testsuite/tests/pmcheck/should_compile/T17340.stderr b/testsuite/tests/pmcheck/should_compile/T17340.stderr
index c31fb2a6f5..7e87ccb887 100644
--- a/testsuite/tests/pmcheck/should_compile/T17340.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T17340.stderr
@@ -7,6 +7,10 @@ T17340.hs:19:4: warning: [-Wredundant-bang-patterns]
     Pattern match has redundant bang
     In an equation for ‘g’: g x = ...
 
+T17340.hs:23:9: warning: [-Wredundant-bang-patterns]
+    Pattern match has redundant bang
+    In an equation for ‘h’: h x = ...
+
 T17340.hs:27:4: warning: [-Wredundant-bang-patterns]
     Pattern match has redundant bang
     In an equation for ‘k’: k _ = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17378.hs b/testsuite/tests/pmcheck/should_compile/T17378.hs
new file mode 100644
index 0000000000..c9c660fcbe
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17378.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE EmptyCase #-}
+module Lib where
+
+import Data.Type.Equality
+import Data.Functor.Identity
+import Data.Void
+
+f :: a :~: Int -> a :~: Bool -> ()
+f !_ x = case x of {}
+
+g :: Identity (a :~: Int) -> a :~: Bool -> ()
+g (Identity _) Refl = ()
+
+data SMaybe a = SNothing
+              | SJust !a
+
+-- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
+-- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
+-- no longer in scope. Normally, we have no way of matching on that without a
+-- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
+-- evidence saying that @z@ must be 'Void' by matching on 'Refl'.
+h :: forall a. a :~: Void -> Bool -> ()
+h _     True  | let y = undefined :: SMaybe a, SNothing <- y = ()
+h Refl  False                                    = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17725.hs b/testsuite/tests/pmcheck/should_compile/T17725.hs
new file mode 100644
index 0000000000..8ed3856fa3
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17725.hs
@@ -0,0 +1,10 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+module Lib where
+
+newtype IInt = IInt Int
+
+f :: IInt -> Bool -> ()
+f !(IInt _) True = ()
+f (IInt 42) True = ()
+f _         _    = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17725.stderr b/testsuite/tests/pmcheck/should_compile/T17725.stderr
new file mode 100644
index 0000000000..3bf20a6479
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17725.stderr
@@ -0,0 +1,4 @@
+
+T17725.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f (IInt 42) True = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17729.hs b/testsuite/tests/pmcheck/should_compile/T17729.hs
new file mode 100644
index 0000000000..d5ce27a293
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17729.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+
+incomplete :: Maybe a -> Bool
+incomplete ma = case (ma, ()) of
+  (Nothing, _) -> False
+
+{-# COMPLETE Pat #-}
+pattern Pat :: a -> b -> (a, b)
+pattern Pat a b = (a, b)
+
+main :: IO ()
+main = print $ incomplete (Just ())
diff --git a/testsuite/tests/pmcheck/should_compile/T17729.stderr b/testsuite/tests/pmcheck/should_compile/T17729.stderr
new file mode 100644
index 0000000000..ac4f31fcfa
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17729.stderr
@@ -0,0 +1,4 @@
+
+T17729.hs:5:17: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: ((Just _), ())
diff --git a/testsuite/tests/pmcheck/should_compile/T17977.stderr b/testsuite/tests/pmcheck/should_compile/T17977.stderr
new file mode 100644
index 0000000000..43aaa6f735
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17977.stderr
@@ -0,0 +1,10 @@
+
+T17977.hs:31:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’:
+        Patterns not matched:
+            SZ SZ SZ _
+            SZ SZ (SS _) _
+            SZ (SS _) SZ _
+            SZ (SS _) (SS _) _
+            ...
diff --git a/testsuite/tests/pmcheck/should_compile/T18273.hs b/testsuite/tests/pmcheck/should_compile/T18273.hs
new file mode 100644
index 0000000000..d80f517923
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18273.hs
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Bug where
+
+import Data.Kind
+import Data.Void
+
+type SFalse = SBool 'False
+type STrue  = SBool 'True
+
+data SBool :: Bool -> Type where
+  SFalse :: SFalse
+  STrue  :: STrue
+
+type family F (b :: Bool) :: Type where
+  F 'False = Void
+  F 'True  = ()
+
+data T (b :: Bool)
+  = MkT1
+  | MkT2 !(F b)
+
+ex :: SBool b -> T b -> ()
+ex sb t =
+  case t of
+    MkT1 -> ()
+    MkT2 f ->
+      case sb of
+        STrue -> f
+
+ex2 :: SBool b -> T b -> ()
+ex2 sb t =
+  case t of
+    MkT2 f ->
+      case sb of
+        STrue -> f
+    MkT1 -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/T18341.hs b/testsuite/tests/pmcheck/should_compile/T18341.hs
new file mode 100644
index 0000000000..5c867129c2
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18341.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+
+module Lib where
+
+import GHC.Exts
+
+data T = MkT !Int {-# UNPACK #-} !Int Int#
+
+f :: T -> ()
+f (MkT  _ _ _) | False = () -- inaccessible
+f (MkT !_ _ _) | False = () -- redundant, not only inaccessible!
+f _                    = ()
+
+g :: T -> ()
+g (MkT _  _ _) | False = () -- inaccessible
+g (MkT _ !_ _) | False = () -- redundant, not only inaccessible!
+g _                    = ()
+
+h :: T -> ()
+h (MkT _ _  _) | False = () -- inaccessible
+h (MkT _ _ !_) | False = () -- redundant, not only inaccessible!
+h _                    = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T18341.stderr b/testsuite/tests/pmcheck/should_compile/T18341.stderr
new file mode 100644
index 0000000000..ee4838a890
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18341.stderr
@@ -0,0 +1,24 @@
+
+T18341.hs:12:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f (MkT _ _ _) | False = ...
+
+T18341.hs:13:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f (MkT !_ _ _) | False = ...
+
+T18341.hs:17:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘g’: g (MkT _ _ _) | False = ...
+
+T18341.hs:18:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g (MkT _ !_ _) | False = ...
+
+T18341.hs:22:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘h’: h (MkT _ _ _) | False = ...
+
+T18341.hs:23:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘h’: h (MkT _ _ !_) | False = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T18670.hs b/testsuite/tests/pmcheck/should_compile/T18670.hs
new file mode 100644
index 0000000000..4602c0c5d6
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18670.hs
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Lib where
+
+import Data.Type.Equality
+
+data T a where
+  TInt :: T Int
+  TBool :: T Bool
+
+f :: T a -> a :~: Int -> ()
+f TInt Refl = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T18670.stderr b/testsuite/tests/pmcheck/should_compile/T18670.stderr
new file mode 100644
index 0000000000..6b7f6cc207
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18670.stderr
@@ -0,0 +1,4 @@
+
+T18670.hs:16:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’: Patterns not matched: TBool _
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index ee69cf176a..de0998ba29 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -36,6 +36,8 @@ test('T9951b', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T9951', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T10183', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11303', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11276', collect_compiler_stats('bytes allocated',10), compile,
@@ -108,12 +110,18 @@ test('T17357', expect_broken(17357), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17376', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17378', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17465', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17646', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17703', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17725', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17729', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17783', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17977', collect_compiler_stats('bytes allocated',10), compile,
@@ -122,12 +130,18 @@ 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('T18273', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18341', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18478', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18533', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18572', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-incomplete-uni-patterns -fwarn-overlapping-patterns'])
+test('T18670', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,