Take strict fields into account in coverage checking

Summary:
The current pattern-match coverage checker implements the
formalism presented in the //GADTs Meet Their Match// paper in a
fairly faithful matter. However, it was discovered recently that
there is a class of unreachable patterns that
//GADTs Meet Their Match// does not handle: unreachable code due to
strict argument types, as demonstrated in #15305. This patch
therefore goes off-script a little and implements an extension to
the formalism presented in the paper to handle this case.

Essentially, when determining if each constructor can be matched on,
GHC checks if its associated term and type constraints are
satisfiable. This patch introduces a new form of constraint,
`NonVoid(ty)`, and checks if each constructor's strict argument types
satisfy `NonVoid`. If any of them do not, then that constructor is
deemed uninhabitable, and thus cannot be matched on. For the full
story of how this works, see
`Note [Extensions to GADTs Meet Their Match]`.

Along the way, I did a little bit of much-needed refactoring. In
particular, several functions in `Check` were passing a triple of
`(ValAbs, ComplexEq, Bag EvVar)` around to represent a constructor
and its constraints. Now that we're adding yet another form of
constraint to the mix, I thought it appropriate to turn this into
a proper data type, which I call `InhabitationCandidate`.

Test Plan: make test TEST=T15305

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15305

Differential Revision: https://phabricator.haskell.org/D5087

6 files changed, 338 insertions, 60 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 92edadb524..d57e34a79c 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -156,6 +156,9 @@ data PmPat :: PatTy -> * where
   PmGrd  :: { pm_grd_pv   :: PatVec
             , pm_grd_expr :: PmExpr  } -> PmPat 'PAT
 
+instance Outputable (PmPat a) where
+  ppr = pprPmPatDebug
+
 -- data T a where
 --     MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
 -- or  MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
@@ -426,9 +429,9 @@ checkMatches' vars matches
 --   for details.
 checkEmptyCase' :: Id -> PmM PmResult
 checkEmptyCase' var = do
-  (tm_css, ty_css) <- pmInitialTmTyCs
-  fam_insts        <- liftD dsGetFamInstEnvs
-  mb_candidates    <- inhabitationCandidates fam_insts (idType var)
+  tm_ty_css     <- pmInitialTmTyCs
+  fam_insts     <- liftD dsGetFamInstEnvs
+  mb_candidates <- inhabitationCandidates fam_insts (idType var)
   case mb_candidates of
     -- Inhabitation checking failed / the type is trivially inhabited
     Left ty -> return (uncoveredWithTy ty)
@@ -436,18 +439,15 @@ checkEmptyCase' var = do
     -- A list of inhabitant candidates is available: Check for each
     -- one for the satisfiability of the constraints it gives rise to.
     Right candidates -> do
-      missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
-        mb_sat <- pmIsSatisfiable tm_ct tm_css ty_cs ty_css
-        pure $ case mb_sat of
-                Just (tm_state', all_ty_cs)
-                        -> [(va, all_ty_cs, tm_state')]
-                Nothing -> []
-      let mkValVec (va,all_ty_cs,tm_state')
-            = ValVec [va] (MkDelta all_ty_cs tm_state')
-          uncovered = UncoveredPatterns (map mkValVec missing_m)
+      missing_m <- flip mapMaybeM candidates $
+          \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
+                                , ic_ty_cs = ty_cs
+                                , ic_strict_arg_tys = strict_arg_tys } -> do
+        mb_sat <- pmIsSatisfiable tm_ty_css tm_ct ty_cs strict_arg_tys
+        pure $ fmap (ValVec [va]) mb_sat
       return $ if null missing_m
         then emptyPmResult
-        else PmResult FromBuiltin [] uncovered []
+        else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
 
 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
 -- a closed type constructor.
@@ -545,14 +545,14 @@ pmTopNormaliseType_maybe env typ
 -- use an empty set in its place. (See
 -- @Note [Recovering from unsatisfiable pattern-matching constraints]@
 -- for why this is done.)
-pmInitialTmTyCs :: PmM (TmState, Bag EvVar)
+pmInitialTmTyCs :: PmM Delta
 pmInitialTmTyCs = do
   ty_cs  <- liftD getDictsDs
   tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
   sat_ty <- tyOracle ty_cs
   let initTyCs = if sat_ty then ty_cs else emptyBag
       initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
-  pure (initTmState, initTyCs)
+  pure $ MkDelta{ delta_tm_cs = initTmState, delta_ty_cs = initTyCs }
 
 {-
 Note [Recovering from unsatisfiable pattern-matching constraints]
@@ -574,7 +574,8 @@ afresh with an empty set of constraints. This way, we'll get the warnings
 that we expect.
 -}
 
--- | Given some term and type constraints, check if they are satisfiable.
+-- | Given a conlike's term constraints, type constraints, and strict argument
+-- types, check if they are satisfiable.
 -- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet
 -- Their Match paper.)
 --
@@ -588,24 +589,92 @@ that we expect.
 -- * Since the new term constraint is a separate argument, we only need to
 --   execute one iteration of the term oracle (instead of traversing the
 --   entire set of term constraints).
+--
+-- Taking strict argument types into account is something which was not
+-- discussed in GADTs Meet Their Match. For an explanation of what role they
+-- serve, see @Note [Extensions to GADTs Meet Their Match]@.
 pmIsSatisfiable
-  :: ComplexEq -- ^ The new term constraint.
-  -> TmState   -- ^ The ambient term constraints (known to be satisfiable).
+  :: Delta     -- ^ The ambient term and type constraints
+               --   (known to be satisfiable).
+  -> ComplexEq -- ^ The new term constraint.
+  -> Bag EvVar -- ^ The new type constraints.
+  -> [Type]    -- ^ The strict argument types.
+  -> PmM (Maybe Delta)
+               -- ^ @'Just' delta@ if the constraints (@delta@) are
+               -- satisfiable, and each strict argument type is inhabitable.
+               -- 'Nothing' otherwise.
+pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do
+  mb_sat <- tmTyCsAreSatisfiable amb_cs new_tm_c new_ty_cs
+  case mb_sat of
+    Nothing -> pure Nothing
+    Just delta -> do
+      -- We know that the term and type constraints are inhabitable, so now
+      -- check if each strict argument type is inhabitable.
+      non_voids <- traverse (nonVoid delta) strict_arg_tys
+      pure $ if and non_voids -- Check if each strict argument type
+                              -- is inhabitable
+                then Just delta
+                else Nothing
+
+-- | Like 'pmIsSatisfiable', but only checks if term and type constraints are
+-- satisfiable, and doesn't bother checking anything related to strict argument
+-- types. It's handy to have this factored out into is own function since term
+-- and type constraints are the only forms of constraints that are checked for
+-- each 'InhabitationCandidate' in 'nonVoid'
+-- (as discussed in @Note [Extensions to GADTs Meet Their Match]@).
+tmTyCsAreSatisfiable
+  :: Delta     -- ^ The ambient term and type constraints
+               --   (known to be satisfiable).
+  -> ComplexEq -- ^ The new term constraint.
   -> Bag EvVar -- ^ The new type constraints.
-  -> Bag EvVar -- ^ The ambient type constraints (known to be satisfiable).
-  -> PmM (Maybe (TmState, Bag EvVar))
-               -- ^ @'Just' (term_cs, ty_cs)@ if the constraints are
-               -- satisfiable, where @term_cs@ and @ty_cs@ are the new sets of
-               -- term and type constraints, respectively. 'Nothing' otherwise.
-pmIsSatisfiable new_term_c amb_term_cs new_ty_cs amb_ty_cs = do
+  -> PmM (Maybe Delta)
+       -- ^ @'Just' delta@ if the constraints (@delta@) are
+       -- satisfiable. 'Nothing' otherwise.
+tmTyCsAreSatisfiable
+    (MkDelta{ delta_tm_cs = amb_tm_cs, delta_ty_cs = amb_ty_cs })
+    new_tm_c new_ty_cs = do
   let ty_cs = new_ty_cs `unionBags` amb_ty_cs
   sat_ty <- if isEmptyBag new_ty_cs
                then pure True
                else tyOracle ty_cs
-  pure $ case (sat_ty, solveOneEq amb_term_cs new_term_c) of
-           (True, Just term_cs) -> Just (term_cs, ty_cs)
+  pure $ case (sat_ty, solveOneEq amb_tm_cs new_tm_c) of
+           (True, Just term_cs) -> Just $ MkDelta{ delta_ty_cs = ty_cs
+                                                 , delta_tm_cs = term_cs }
            _unsat               -> Nothing
 
+-- | Checks if a strict argument type of a conlike is inhabitable by a
+-- terminating value (i.e, an 'InhabitationCandidate').
+-- See @Note [Extensions to GADTs Meet Their Match]@.
+nonVoid
+  :: Delta    -- ^ The ambient term/type constraints (known to be satisfiable).
+  -> Type     -- ^ The strict argument type.
+  -> PmM Bool -- ^ 'True' if the strict argument type might be inhabited by a
+              --   terminating value (i.e., an 'InhabitationCandidate').
+              --   'False' if it is definitely uninhabitable by anything
+              --   (except bottom).
+nonVoid amb_cs strict_arg_ty = do
+  fam_insts <- liftD dsGetFamInstEnvs
+  mb_cands <- inhabitationCandidates fam_insts strict_arg_ty
+  case mb_cands of
+    Left _ -> pure True -- The type is trivially inhabited
+    Right cands -> do
+      cand_inhabs <- traverse cand_tm_ty_cs_are_satisfiable cands
+      pure $ or cand_inhabs
+        -- A strict argument type is inhabitable by a terminating value if at
+        -- least one InhabitationCandidate is satisfiable
+  where
+    -- Checks if an InhabitationCandidate for a strict argument type has
+    -- satisfiable term and type constraints. We deliberately don't call
+    -- nonVoid on the InhabitationCandidate's own strict argument types, since
+    -- that can result in infinite loops.
+    -- See Note [Extensions to GADTs Meet Their Match]
+    cand_tm_ty_cs_are_satisfiable :: InhabitationCandidate -> PmM Bool
+    cand_tm_ty_cs_are_satisfiable
+      (InhabitationCandidate{ ic_tm_ct = new_term_c
+                            , ic_ty_cs = new_ty_cs }) = do
+        mb_sat <- tmTyCsAreSatisfiable amb_cs new_term_c new_ty_cs
+        pure $ isJust mb_sat
+
 {- Note [Type normalisation for EmptyCase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 EmptyCase is an exception for pattern matching, since it is strict. This means
@@ -657,14 +726,14 @@ Which means that in source Haskell:
   - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
 -}
 
--- | Generate all inhabitation candidates for a given type. The result is
--- either (Left ty), if the type cannot be reduced to a closed algebraic type
--- (or if it's one trivially inhabited, like Int), or (Right candidates), if it
--- can. In this case, the candidates are the signature of the tycon, each one
--- accompanied by the term- and type- constraints it gives rise to.
+-- | Generate all 'InhabitationCandidate's for a given type. The result is
+-- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type
+-- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@,
+-- if it can. In this case, the candidates are the signature of the tycon, each
+-- one accompanied by the term- and type- constraints it gives rise to.
 -- See also Note [Checking EmptyCase Expressions]
 inhabitationCandidates :: FamInstEnvs -> Type
-                       -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
+                       -> PmM (Either Type [InhabitationCandidate])
 inhabitationCandidates fam_insts ty
   = case pmTopNormaliseType_maybe fam_insts ty of
       Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
@@ -682,19 +751,27 @@ inhabitationCandidates fam_insts ty
 
     -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
     alts_to_check :: Type -> Type -> [DataCon]
-                  -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
+                  -> PmM (Either Type [InhabitationCandidate])
     alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
       Just (tc, _)
-        | tc `elem` trivially_inhabited -> case dcs of
-            []    -> return (Left src_ty)
-            (_:_) -> do var <- liftD $ mkPmId core_ty
-                        let va = build_tm (PmVar var) dcs
-                        return $ Right [(va, mkIdEq var, emptyBag)]
-
-        | pmIsClosedType core_ty -> liftD $ do
-            var  <- mkPmId core_ty -- it would be wrong to unify x
-            alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
-            return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts]
+        |  tc `elem` trivially_inhabited
+        -> case dcs of
+             []    -> return (Left src_ty)
+             (_:_) -> do var <- liftD $ mkPmId core_ty
+                         let va = build_tm (PmVar var) dcs
+                         return $ Right [InhabitationCandidate
+                           { ic_val_abs = va, ic_tm_ct = mkIdEq var
+                           , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }]
+
+        |  pmIsClosedType core_ty && not (isAbstractTyCon tc)
+           -- Don't consider abstract tycons since we don't know what their
+           -- constructors are, which makes the results of coverage checking
+           -- them extremely misleading.
+        -> liftD $ do
+             var  <- mkPmId core_ty -- it would be wrong to unify x
+             alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
+             return $ Right [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
+                            | alt <- alts ]
       -- For other types conservatively assume that they are inhabited.
       _other -> return (Left src_ty)
 
@@ -1284,9 +1361,120 @@ pmPatType (PmGrd  { pm_grd_pv  = pv })
   = ASSERT(patVecArity pv == 1) (pmPatType p)
   where Just p = find ((==1) . patternArity) pv
 
--- | Generate a value abstraction for a given constructor (generate
+-- | Information about a conlike that is relevant to coverage checking.
+-- It is called an \"inhabitation candidate\" since it is a value which may
+-- possibly inhabit some type, but only if its term constraint ('ic_tm_ct')
+-- and type constraints ('ic_ty_cs') are permitting, and if all of its strict
+-- argument types ('ic_strict_arg_tys') are inhabitable.
+-- See @Note [Extensions to GADTs Meet Their Match]@.
+data InhabitationCandidate =
+  InhabitationCandidate
+  { ic_val_abs        :: ValAbs
+  , ic_tm_ct          :: ComplexEq
+  , ic_ty_cs          :: Bag EvVar
+  , ic_strict_arg_tys :: [Type]
+  }
+
+{-
+Note [Extensions to GADTs Meet Their Match]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The GADTs Meet Their Match paper presents the formalism that GHC's coverage
+checker adheres to. Since the paper's publication, there have been some
+additional features added to the coverage checker which are not described in
+the paper. This Note serves as a reference for these new features.
+
+-----
+-- Strict argument type constraints
+-----
+
+In the ConVar case of clause processing, each conlike K traditionally
+generates two different forms of constraints:
+
+* A term constraint (e.g., x ~ K y1 ... yn)
+* Type constraints from the conlike's context (e.g., if K has type
+  forall bs. Q => s1 .. sn -> T tys, then Q would be its type constraints)
+
+As it turns out, these alone are not enough to detect a certain class of
+unreachable code. Consider the following example (adapted from #15305):
+
+  data K = K1 | K2 !Void
+
+  f :: K -> ()
+  f K1 = ()
+
+Even though `f` doesn't match on `K2`, `f` is exhaustive in its patterns. Why?
+Because it's impossible to construct a terminating value of type `K` using the
+`K2` constructor, and thus it's impossible for `f` to ever successfully match
+on `K2`.
+
+The reason is because `K2`'s field of type `Void` is //strict//. Because there
+are no terminating values of type `Void`, any attempt to construct something
+using `K2` will immediately loop infinitely or throw an exception due to the
+strictness annotation. (If the field were not strict, then `f` could match on,
+say, `K2 undefined` or `K2 (let x = x in x)`.)
+
+Since neither the term nor type constraints mentioned above take strict
+argument types into account, we make use of the `nonVoid` function to
+determine whether a strict type is inhabitable by a terminating value or not.
+
+`nonVoid ty` returns True when either:
+1. `ty` has at least one InhabitationCandidate for which both its term and type
+   constraints are satifiable.
+2. We're unsure if it's inhabited by a terminating value.
+
+`nonVoid ty` returns False when `ty` is definitely uninhabited by anything
+(except bottom). Some examples:
+
+* `nonVoid Void` returns False, since Void has no InhabitationCandidates.
+  (This is what lets us discard the `K2` constructor in the earlier example.)
+* `nonVoid (Int :~: Int)` returns True, since it has an InhabitationCandidate
+  (through the Refl constructor), and its term constraint (x ~ Refl) and
+  type constraint (Int ~ Int) are satisfiable.
+* `nonVoid (Int :~: Bool)` returns False. Although it has an
+  InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is
+  not satisfiable.
+
+Observe that the definition of `nonVoid ty` does not say whether `ty`'s
+InhabitationCandidate must itself have `nonVoid` return True for all its own
+strict argument types. This is a deliberate choice, because trying to take
+these into account in a naïve way can lead to infinite loops. Consider the
+following example:
+
+  data Abyss = MkAbyss !Abyss
+
+  stareIntoTheAbyss :: Abyss -> a
+  stareIntoTheAbyss x = case x of {}
+
+In principle, stareIntoTheAbyss is exhaustive, since there is no way to
+construct a terminating value using MkAbyss. However, both the term and type
+constraints for MkAbyss are satisfiable, so the only way one could determine
+that MkAbyss is unreachable is to check if `nonVoid Abyss` returns False.
+There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term
+and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss`
+returns False... and now we've entered an infinite loop!
+
+To avoid this sort of conundrum, `nonVoid ty` doesn't call `nonVoid` on any of
+the strict argument types of `ty`'s InhabitationCandidates. This means
+that `nonVoid` is incomplete. For instance, GHC will warn that
+stareIntoTheAbyss is non-exhaustive, even though it actually is. Properly
+detecting that stareIntoTheAbyss is non-exhaustive would require a much more
+sophisticated implementation for `nonVoid`, however, so for now we simply
+implement the current, more straightforward approach.
+-}
+
+instance Outputable InhabitationCandidate where
+  ppr (InhabitationCandidate { ic_val_abs = va, ic_tm_ct = tm_ct
+                             , ic_ty_cs = ty_cs
+                             , ic_strict_arg_tys = strict_arg_tys }) =
+    text "InhabitationCandidate" <+>
+      vcat [ text "ic_val_abs        =" <+> ppr va
+           , text "ic_tm_ct          =" <+> ppr tm_ct
+           , text "ic_ty_cs          =" <+> ppr ty_cs
+           , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ]
+
+-- | Generate an 'InhabitationCandidate' for a given conlike (generate
 -- fresh variables of the appropriate type for arguments)
-mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
+mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
 --  *  x :: T tys, where T is an algebraic data type
 --     NB: in the case of a data family, T is the *representation* TyCon
 --     e.g.   data instance T (a,b) = T1 a b
@@ -1294,18 +1482,21 @@ mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
 --            data TPair a b = T1 a b  -- The "representation" type
 --       It is TPair, not T, that is given to mkOneConFull
 --
---  * 'con' K is a constructor of data type T
+--  * 'con' K is a conlike of data type T
 --
 -- After instantiating the universal tyvars of K we get
 --          K tys :: forall bs. Q => s1 .. sn -> T tys
 --
--- Results: ValAbs:          K (y1::s1) .. (yn::sn)
---          ComplexEq:       x ~ K y1..yn
---          [EvVar]:         Q
+-- Suppose y1 is a strict field. Then we get
+-- Results: ic_val_abs:        K (y1::s1) .. (yn::sn)
+--          ic_tm_ct:          x ~ K y1..yn
+--          ic_ty_cs:          Q
+--          ic_strict_arg_tys: [s1]
 mkOneConFull x con = do
   let res_ty  = idType x
       (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
         = conLikeFullSig con
+      arg_is_banged = map isBanged $ conLikeImplBangs con
       tc_args = tyConAppArgs res_ty
       subst1  = case con of
                   RealDataCon {} -> zipTvSubst univ_tvs tc_args
@@ -1314,8 +1505,9 @@ mkOneConFull x con = do
 
   (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
 
+  let arg_tys' = substTys subst arg_tys
   -- Fresh term variables (VAs) as arguments to the constructor
-  arguments <-  mapM mkPmVar (substTys subst arg_tys)
+  arguments <-  mapM mkPmVar arg_tys'
   -- All constraints bound by the constructor (alpha-renamed)
   let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
   evvars <- mapM (nameType "pm") theta_cs
@@ -1324,7 +1516,13 @@ mkOneConFull x con = do
                        , pm_con_tvs     = ex_tvs'
                        , pm_con_dicts   = evvars
                        , pm_con_args    = arguments }
-  return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
+      strict_arg_tys = filterByList arg_is_banged arg_tys'
+  return $ InhabitationCandidate
+           { ic_val_abs        = con_abs
+           , ic_tm_ct          = (PmExprVar (idName x), vaToPmExpr con_abs)
+           , ic_ty_cs          = listToBag evvars
+           , ic_strict_arg_tys = strict_arg_tys
+           }
 
 -- ----------------------------------------------------------------------------
 -- * More smart constructors and fresh variable generation
@@ -1607,9 +1805,9 @@ runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
 -- delta with all term and type constraints in scope.
 mkInitialUncovered :: [Id] -> PmM Uncovered
 mkInitialUncovered vars = do
-  (initTmState, initTyCs) <- pmInitialTmTyCs
+  delta <- pmInitialTmTyCs
   let patterns = map PmVar vars
-  return [ValVec patterns (MkDelta initTyCs initTmState)]
+  return [ValVec patterns delta]
 
 -- | Increase the counter for elapsed algorithm iterations, check that the
 -- limit is not exceeded and call `pmcheck`
@@ -1736,13 +1934,12 @@ pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
 
   cons_cs <- mapM (liftD . mkOneConFull x) complete_match
 
-  inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
-    mb_sat <- pmIsSatisfiable tm_ct (delta_tm_cs delta)
-                              ty_cs (delta_ty_cs delta)
-    pure $ case mb_sat of
-             Just (tm_state, ty_state)
-                     -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
-             Nothing -> []
+  inst_vsa <- flip mapMaybeM cons_cs $
+      \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
+                            , ic_ty_cs = ty_cs
+                            , ic_strict_arg_tys = strict_arg_tys } -> do
+    mb_sat <- pmIsSatisfiable delta tm_ct ty_cs strict_arg_tys
+    pure $ fmap (ValVec (va:vva)) mb_sat
 
   set_provenance prov .
     force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
diff --git a/docs/users_guide/8.8.1-notes.rst b/docs/users_guide/8.8.1-notes.rst
index f97e79a3cf..0a095f02f2 100644
--- a/docs/users_guide/8.8.1-notes.rst
+++ b/docs/users_guide/8.8.1-notes.rst
@@ -27,6 +27,19 @@ Language
   they could only stand in for other type variables, but this restriction was deemed
   unnecessary in `GHC proposal #29 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst>`__. Also see :ghc-ticket:`15050`.
 
+- The pattern-match coverage checker now checks for cases that are unreachable
+  due to constructors have strict argument types. For instance, in the
+  following example: ::
+
+    data K = K1 | K2 !Void
+
+    f :: K -> ()
+    f K1 = ()
+
+  ``K2`` cannot be matched on in ``f``, since it is impossible to construct a
+  terminating value of type ``Void``. Accordingly, GHC will not warn about
+  ``K2`` (whereas previous versions of GHC would).
+
 Compiler
 ~~~~~~~~
 
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.hs b/testsuite/tests/pmcheck/should_compile/T15305.hs
new file mode 100644
index 0000000000..82214b7e19
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15305.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T15305 where
+
+import Data.Void
+
+-- Example 1
+
+data (:+:) f g a = Inl !(f a) | Inr !(g a)
+
+data A
+data B
+
+data Foo l where
+  Foo :: Foo A
+
+data Bar l where
+  Bar :: Bar B
+
+type Sig = Foo :+: Bar
+
+fun :: Sig B -> Int
+fun (Inr Bar) = 1
+
+-- Example 2
+
+data GhcPass c
+type family XXHsImplicitBndrs x
+type instance XXHsImplicitBndrs (GhcPass _) = Void
+
+data HsImplicitBndrs pass
+  = UsefulConstructor
+  | XHsImplicitBndrs !(XXHsImplicitBndrs pass)
+
+fun2 :: HsImplicitBndrs (GhcPass pass) -> ()
+fun2 UsefulConstructor = ()
+{-
+NB: the seemingly equivalent function
+
+fun2' :: (p ~ GhcPass pass) => HsImplicitBndrs p -> ()
+fun2' UsefulConstructor = ()
+
+Is mistakenly deemed non-exhaustive at the moment due to #14813.
+-}
+
+-- Example 3
+
+data Abyss = MkAbyss !Abyss
+
+stareIntoTheAbyss :: Abyss -> a
+stareIntoTheAbyss x = case x of {}
+{-
+Alas, this function is marked non-exhaustive, since the way GHC solves
+NonVoid constraints at the moment isn't sophisticated enough to handle
+recursive strict argument types like MkAbyss exhibits. Maybe some day.
+-}
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.stderr b/testsuite/tests/pmcheck/should_compile/T15305.stderr
new file mode 100644
index 0000000000..bb88a9be5b
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15305.stderr
@@ -0,0 +1,4 @@
+
+T15305.hs:53:23: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (MkAbyss _)
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index acb2b7ff74..f2bbfffc00 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -63,6 +63,8 @@ test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15305', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15385', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15450', normal, compile,
diff --git a/testsuite/tests/simplCore/should_compile/T13990.stderr b/testsuite/tests/simplCore/should_compile/T13990.stderr
new file mode 100644
index 0000000000..f30ebece6e
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T13990.stderr
@@ -0,0 +1,4 @@
+
+T13990.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘absurdFoo’: absurdFoo (Foo x) = ...