PmCheck: No ConLike instantiation in pmcheckwip/pmcheck-ex_tvs

`pmcheck` used to call `refineToAltCon` which would refine the knowledge
we had about a variable by equating it to a `ConLike` application.
Since we weren't particularly smart about this in the Check module, we
simply freshened the constructors existential and term binders utimately
through a call to `mkOneConFull`.

But that instantiation is unnecessary for when we match against a
concrete pattern! The pattern will already have fresh binders and field
types. So we don't call `refineToAltCon` from `Check` anymore.

Subsequently, we can simplify a couple of call sites and functions in
`PmOracle`. Also implementing `computeCovered` becomes viable and we
don't have to live with the hack that was `addVarPatVecCt` anymore.

A side-effect of not indirectly calling `mkOneConFull` anymore is that
we don't generate the proper strict argument field constraints anymore.
Instead we now desugar ConPatOuts as if they had bangs on their strict
fields. This implies that `PmVar` now carries a `HsImplBang` that we
need to respect by a (somewhat ephemeral) non-void check. We fix #17234
in doing so.

5 files changed, 225 insertions, 302 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 52f8c376bc..b86bb785c3 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -6,8 +6,6 @@ Pattern Matching Coverage Checking.
 
 {-# LANGUAGE CPP            #-}
 {-# LANGUAGE GADTs          #-}
-{-# LANGUAGE DataKinds      #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TupleSections  #-}
 {-# LANGUAGE ViewPatterns   #-}
 {-# LANGUAGE MultiWayIf     #-}
@@ -45,25 +43,23 @@ import SrcLoc
 import Util
 import Outputable
 import DataCon
+import PatSyn (patSynArity)
 import BasicTypes (Boxity(..))
 import Var (EvVar)
 import Coercion
 import TcEvidence
 import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr, dsSyntaxExpr)
 import MatchLit (dsLit, dsOverLit)
-import IOEnv
 import DsMonad
 import Bag
 import TyCoRep
 import Type
 import DsUtils       (isTrueLHsExpr)
-import Maybes        (isJust, expectJust)
+import Maybes
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List     (find)
-import Control.Monad (forM, when, forM_)
-import Control.Monad.Trans.Class (lift)
-import Control.Monad.Trans.Maybe
+import Data.List     (find, isSubsequenceOf)
+import Control.Monad (forM, when, forM_, zipWithM)
 import qualified Data.Semigroup as Semi
 
 {-
@@ -88,24 +84,35 @@ The algorithm is based on the paper:
 %************************************************************************
 -}
 
-data PmPat where
-  -- | For the arguments' meaning see 'HsPat.ConPatOut'.
-  PmCon  :: { pm_con_con     :: PmAltCon
-            , pm_con_arg_tys :: [Type]
-            , pm_con_tvs     :: [TyVar]
-            , pm_con_args    :: [PmPat] } -> PmPat
-
-  PmVar  :: { pm_var_id   :: Id } -> PmPat
-
-  PmGrd  :: { pm_grd_pv   :: PatVec -- ^ Always has 'patVecArity' 1.
-            , pm_grd_expr :: CoreExpr } -> PmPat
-     -- (PmGrd pat expr) matches expr against pat, binding the variables in pat
+data PmPat
+  = -- | For the arguments' meaning see 'HsPat.ConPatOut'.
+    PmCon {
+      pm_con_con     :: PmAltCon,
+      pm_con_arg_tys :: [Type],
+      pm_con_tvs     :: [TyVar],
+      pm_con_dicts   :: [EvVar],
+      pm_con_args    :: [PmPat]
+    }
+
+    -- | Possibly strict variable pattern match
+  | PmVar {
+      _pm_var_bang :: HsImplBang,
+      pm_var_id    :: Id
+    }
+
+    -- | @PmGrd pat expr@ matches @expr@ against @pat@,
+    --   binding the variables in @pat@
+  | PmGrd {
+      pm_grd_pv   :: PatVec,
+      -- ^ Always has 'patVecArity' 1.
+      pm_grd_expr :: CoreExpr
+    }
 
 -- | Should not be user-facing.
 instance Outputable PmPat where
-  ppr (PmCon alt _arg_tys _con_tvs con_args)
+  ppr (PmCon alt _arg_tys _con_tvs _con_dicts con_args)
     = cparen (notNull con_args) (hsep [ppr alt, hsep (map ppr con_args)])
-  ppr (PmVar vid) = ppr vid
+  ppr (PmVar bang vid) = (if isBanged bang then char '!' else empty) <> ppr vid
   ppr (PmGrd pv ge) = hsep (map ppr pv) <+> text "<-" <+> ppr ge
 
 -- data T a where
@@ -416,7 +423,7 @@ nullaryConPattern :: ConLike -> PmPat
 -- Nullary data constructor and nullary type constructor
 nullaryConPattern con =
   PmCon { pm_con_con = (PmAltConLike con), pm_con_arg_tys = []
-        , pm_con_tvs = [], pm_con_args = [] }
+        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
 {-# INLINE nullaryConPattern #-}
 
 truePattern :: PmPat
@@ -427,20 +434,22 @@ vanillaConPattern :: ConLike -> [Type] -> PatVec -> PmPat
 -- ADT constructor pattern => no existentials, no local constraints
 vanillaConPattern con arg_tys args =
   PmCon { pm_con_con = PmAltConLike con, pm_con_arg_tys = arg_tys
-        , pm_con_tvs = [], pm_con_args = args }
+        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
 {-# INLINE vanillaConPattern #-}
 
 -- | Create an empty list pattern of a given type
 nilPattern :: Type -> PmPat
 nilPattern ty =
   PmCon { pm_con_con = PmAltConLike (RealDataCon nilDataCon)
-        , pm_con_arg_tys = [ty], pm_con_tvs = [], pm_con_args = [] }
+        , pm_con_arg_tys = [ty], pm_con_tvs = [], pm_con_dicts = []
+        , pm_con_args = [] }
 {-# INLINE nilPattern #-}
 
 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
 mkListPatVec ty xs ys = [PmCon { pm_con_con = PmAltConLike (RealDataCon consDataCon)
                                , pm_con_arg_tys = [ty]
                                , pm_con_tvs = []
+                               , pm_con_dicts = []
                                , pm_con_args = xs++ys }]
 {-# INLINE mkListPatVec #-}
 
@@ -461,6 +470,7 @@ mkPmLitPattern lit@(PmLit _ val)
   = [PmCon { pm_con_con = PmAltLit lit
            , pm_con_arg_tys = []
            , pm_con_tvs = []
+           , pm_con_dicts = []
            , pm_con_args = [] }]
 {-# INLINE mkPmLitPattern #-}
 
@@ -475,17 +485,15 @@ mkPmLitPattern lit@(PmLit _ val)
 translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
 translatePat fam_insts pat = case pat of
   WildPat  ty  -> mkPmVars [ty]
-  VarPat _ id  -> return [PmVar (unLoc id)]
+  VarPat _ id  -> return [PmVar HsLazy (unLoc id)]
   ParPat _ p   -> translatePat fam_insts (unLoc p)
   LazyPat _ _  -> mkPmVars [hsPatType pat] -- like a variable
-
-  -- ignore strictness annotations for now
-  BangPat _ p  -> translatePat fam_insts (unLoc p)
+  BangPat _ p  -> addBangs [HsStrict] <$> translatePat fam_insts (unLoc p)
 
   -- (x@pat)   ===>   x (pat <- x)
   AsPat _ (dL->L _ x) p -> do
     pat <- translatePat fam_insts (unLoc p)
-    pure [PmVar x, PmGrd pat (Var x)]
+    pure [PmVar HsLazy x, PmGrd pat (Var x)]
 
   SigPat _ p _ty -> translatePat fam_insts (unLoc p)
 
@@ -504,8 +512,8 @@ translatePat fam_insts pat = case pat of
     (xp, xe) <- mkPmId2Forms pat_ty
     let ke1 = HsOverLit noExtField (unLoc k1)
         ke2 = HsOverLit noExtField k2
-    g1 <- mkGuardSyntaxExpr [truePattern] ge    [unLoc xe, ke1]
-    g2 <- mkGuardSyntaxExpr [PmVar n]     minus [ke2]
+    g1 <- mkGuardSyntaxExpr [truePattern]    ge    [unLoc xe, ke1]
+    g2 <- mkGuardSyntaxExpr [PmVar HsLazy n] minus [ke2]
     return [xp, g1, g2]
 
   -- (fun -> pat)   ===>   x (pat <- fun x)
@@ -556,11 +564,13 @@ translatePat fam_insts pat = case pat of
   ConPatOut { pat_con     = (dL->L _ con)
             , pat_arg_tys = arg_tys
             , pat_tvs     = ex_tvs
+            , pat_dicts   = dicts
             , pat_args    = ps } -> do
     args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
     return [PmCon { pm_con_con     = PmAltConLike con
                   , pm_con_arg_tys = arg_tys
                   , pm_con_tvs     = ex_tvs
+                  , pm_con_dicts   = dicts
                   , pm_con_args    = args }]
 
   NPat ty (dL->L _ olit) mb_neg _ -> do
@@ -618,36 +628,37 @@ translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
                    -> ConLike -> HsConPatDetails GhcTc
                    -> DsM PatVec
-translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
-  = concat <$> translatePatVec fam_insts (map unLoc ps)
-translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
-  = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
+translateConPatVec fam_insts _univ_tys _ex_tvs c (PrefixCon ps)
+  = addFieldBangs c . concat <$> translatePatVec fam_insts (map unLoc ps)
+translateConPatVec fam_insts _univ_tys _ex_tvs c (InfixCon p1 p2)
+  = addFieldBangs c . concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
 translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
     -- Nothing matched. Make up some fresh term variables
-  | null fs        = mkPmVars arg_tys
+  | null fs        = addFieldBangs c <$> mkPmVars arg_tys
     -- The data constructor was not defined using record syntax. For the
     -- pattern to be in record syntax it should be empty (e.g. Just {}).
     -- So just like the previous case.
-  | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
+  | null orig_lbls = ASSERT(null matched_lbls) addFieldBangs c <$> mkPmVars arg_tys
     -- Some of the fields appear, in the original order (there may be holes).
     -- Generate a simple constructor pattern and make up fresh variables for
     -- the rest of the fields
-  | matched_lbls `subsetOf` orig_lbls
+  | matched_lbls `isSubsequenceOf` orig_lbls
   = ASSERT(orig_lbls `equalLength` arg_tys)
-      let translateOne (lbl, ty) = case lookup lbl matched_pats of
+      let translateOne lbl ty = case lookup lbl matched_pats of
             Just p  -> translatePat fam_insts p
             Nothing -> mkPmVars [ty]
-      in  concatMapM translateOne (zip orig_lbls arg_tys)
+      in  addFieldBangs c . concat <$> zipWithM translateOne orig_lbls arg_tys
     -- The fields that appear are not in the correct order. Make up fresh
     -- variables for all fields and add guards after matching, to force the
     -- evaluation in the correct order.
+    -- See Note [Field match order for RecCon]
   | otherwise = do
-      arg_var_pats    <- mkPmVars arg_tys
+      arg_var_pats    <- addFieldBangs c <$> mkPmVars arg_tys
       translated_pats <- forM matched_pats $ \(x,pat) -> do
         pvec <- translatePat fam_insts pat
         return (x, pvec)
 
-      let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
+      let zipped = zip orig_lbls [ x | PmVar _ x <- arg_var_pats ]
           guards = map (\(name,pvec) -> case lookup name zipped of
                             Just x  -> PmGrd pvec (Var x)
                             Nothing -> panic "translateConPatVec: lookup")
@@ -655,8 +666,8 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
 
       return (arg_var_pats ++ guards)
   where
-    -- The actual argument types (instantiated)
-    arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
+    -- The actual argument types (instantiated), with strictness marks
+    arg_tys     = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
 
     -- Some label information
     orig_lbls    = map flSelector $ conLikeFieldLabels c
@@ -664,13 +675,6 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
                    | (dL->L _ x) <- fs]
     matched_lbls = [ name | (name, _pat) <- matched_pats ]
 
-    subsetOf :: Eq a => [a] -> [a] -> Bool
-    subsetOf []     _  = True
-    subsetOf (_:_)  [] = False
-    subsetOf (x:xs) (y:ys)
-      | x == y    = subsetOf    xs  ys
-      | otherwise = subsetOf (x:xs) ys
-
 -- Translate a single match
 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
                -> DsM (PatVec, [PatVec])
@@ -730,8 +734,59 @@ translateBoolGuard e
     -- PatVec for efficiency
   | otherwise = (:[]) <$> mkGuard [truePattern] (unLoc e)
 
-{- Note [Countering exponential blowup]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- | Adds bangs to 'PmVar's in the 'PatVec' if the corresponding field of the
+-- 'ConLike' definition had one.
+addFieldBangs :: ConLike -> PatVec -> PatVec
+addFieldBangs c ps = addBangs bangs ps
+  where
+    bangs = case c of
+      RealDataCon dc -> dataConImplBangs dc
+      PatSynCon ps   -> take (patSynArity ps) (repeat HsLazy)
+
+-- | Basically zip the bangs with the 'PatVec', with a few caveats:
+--
+--    * Skip 'PmGrd's, because they don't match anything. Each bangs corresponds
+--      to a pattern arity 1 pattern.
+--    * A bang doesn't affect a 'PmCon' because it's already strict, so we just
+--      discharge it.
+--    * Add the bang to the 'PmVar'.
+--
+-- Example: @addBangs [HsStrict, HsStrict] [x, 0 <- e, I# 42, True <- p 2]@
+--          evaluates to @[!x, 0 <- e, I# 42, True <- p 2]@, so only the first
+--          pattern changes from lazy to strict.
+addBangs :: [HsImplBang] -> PatVec -> PatVec
+addBangs (bang:bangs) (PmVar _ x:ps) = PmVar bang x : addBangs bangs ps
+addBangs bangs        (p@PmGrd{}:ps) = p            : addBangs bangs ps
+addBangs (_   :bangs) (p@PmCon{}:ps) = p            : addBangs bangs ps
+addBangs []           []             = []
+addBangs _            _              = panic "addBangs"
+
+
+{- Note [Field match order for RecCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The order for RecCon field patterns actually determines evaluation order of
+the pattern match. For example:
+
+  data T = T { a :: !Bool, b :: Char, c :: Int }
+  f :: T -> ()
+  f T{ c = 42, b = 'b' } = ()
+
+Then
+  * @f (T (error "a") (error "b") (error "c"))@ errors out with "a" because of
+    the strict field.
+  * @f (T True        (error "b") (error "c"))@ errors out with "c" because it
+    is mentioned frist in the pattern match.
+
+This means we can't just desugar the pattern match to the PatVec
+@[T !_ 'b' 42]@. Instead we have to generate variable matches that have
+strictness according to the field declarations and afterwards force them in the
+right order. As a result, we get the PatVec @[T !_ b c, 42 <- c, 'b' <- b]@.
+
+Of course, when the labels occur in the order they are defined, we can just use
+the simpler desugaring.
+
+Note [Countering exponential blowup]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Precise pattern match exhaustiveness checking is necessarily exponential in
 the size of some input programs. We implement a counter-measure in the form of
 the -fmax-pmcheck-models flag, limiting the number of Deltas we check against
@@ -852,11 +907,11 @@ mkGuardSyntaxExpr pv f args = do
   core_args <- traverse dsExpr args
   PmGrd pv <$> dsSyntaxExpr f core_args
 
--- | Generate a variable pattern of a given type
+-- | Generate a lazy variable pattern of a given type
 mkPmVar :: Type -> DsM PmPat
-mkPmVar ty = PmVar <$> mkPmId ty
+mkPmVar ty = PmVar HsLazy <$> mkPmId ty
 
--- | Generate many variable patterns, given a list of types
+-- | Generate many lazy variable patterns, given a list of types
 mkPmVars :: [Type] -> DsM PatVec
 mkPmVars tys = mapM mkPmVar tys
 
@@ -866,7 +921,7 @@ mkPmVars tys = mapM mkPmVar tys
 mkPmId2Forms :: Type -> DsM (PmPat, LHsExpr GhcTc)
 mkPmId2Forms ty = do
   x <- mkPmId ty
-  return (PmVar x, noLoc (HsVar noExtField (noLoc x)))
+  return (PmVar HsLazy x, noLoc (HsVar noExtField (noLoc x)))
 
 {-
 Note [Filtering out non-matching COMPLETE sets]
@@ -1062,14 +1117,19 @@ pmcheck (p@PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) guards vva n delta =
   pmcheckI (pv ++ ps) guards (x : vva) n delta'
 
 -- Var: Add x :-> y to the oracle and recurse
-pmcheck (PmVar x : ps) guards (y : vva) n delta = do
-  delta' <- expectJust "x is fresh" <$> addTmCt delta (TmVarVar x y)
-  pmcheckI ps guards vva n delta'
+pmcheck (PmVar bang x : ps) guards (y : vva) n delta = do
+  delta_lzy <- expectJust "x is fresh" <$> addTmCt delta (TmVarVar x y)
+  if isBanged bang
+    then do
+      pr <- addTmCt delta_lzy (TmVarNonVoid x) >>= \case
+              Nothing        -> pure mempty
+              Just delta_str -> pmcheckI ps guards vva n delta_str
+      pure (forceIfCanDiverge delta x pr)
+    else pmcheckI ps guards vva n delta_lzy
 
 -- ConVar
-pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args
-                , pm_con_arg_tys = arg_tys, pm_con_tvs = ex_tvs } : ps)
-        guards (x : vva) n delta = do
+pmcheck (p : ps) guards (x : vva) n delta
+  | PmCon{ pm_con_con = con, pm_con_args = args, pm_con_dicts = dicts } <- p = do
   -- E.g   f (K p q) = <rhs>
   --       <next equation>
   -- Split the value vector into two value vectors:
@@ -1077,7 +1137,7 @@ pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args
   --    * one for <next equation>, recording that x is /not/ (K _ _)
 
   -- Stuff for <rhs>
-  pr_pos <- refineToAltCon delta x con arg_tys ex_tvs >>= \case
+  pr_pos <- addPmConCts delta x con dicts args >>= \case
     Nothing -> pure mempty
     Just (delta', arg_vas) ->
       pmcheckI (args ++ ps) guards (arg_vas ++ vva) n delta'
@@ -1098,6 +1158,20 @@ pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args
 pmcheck [] _ (_:_) _ _ = panic "pmcheck: nil-cons"
 pmcheck (_:_) _ [] _ _ = panic "pmcheck: cons-nil"
 
+addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> PatVec -> DsM (Maybe (Delta, ValVec))
+addPmConCts delta x con dicts field_pats = do
+  -- mk_id will re-use the variable name if possible. The x ~ x is easily
+  -- discharged by the oracle at no overhead (see 'PmOracle.addVarVarCt').
+  let mk_id (PmVar _ x) = pure (Just x)
+      mk_id p@PmCon{} = Just <$> mkPmId (pmPatType p)
+      mk_id PmGrd{}   = pure Nothing -- PmGrds have arity 0, so just forget about them
+  field_vas <- catMaybes <$> traverse mk_id field_pats
+  runMaybeT $ do
+    delta_ty    <- MaybeT $ addTypeEvidence delta (listToBag dicts)
+    delta_tm_ty <- MaybeT $ addTmCt delta_ty (TmVarCon x con field_vas)
+    -- strictness on fields is unleashed when we match
+    pure (delta_tm_ty, field_vas)
+
 -- ----------------------------------------------------------------------------
 -- * Utilities for main checking
 
@@ -1190,46 +1264,36 @@ addPatTmCs :: [Pat GhcTc]           -- LHS       (should have length 1)
            -> [Id]                  -- MatchVars (should have length 1)
            -> DsM a
            -> DsM a
--- Morally, this computes an approximation of the Covered set for p1
--- (which pmcheck currently discards). TODO: Re-use pmcheck instead of calling
--- out to awkard addVarPatVecCt.
+-- Computes an approximation of the Covered set for p1 (which pmcheck currently
+-- discards).
 addPatTmCs ps xs k = do
   fam_insts <- dsGetFamInstEnvs
   pv <- concat <$> translatePatVec fam_insts ps
-  locallyExtendPmDelta (\delta -> addVarPatVecCt delta xs pv) k
-
--- | Add a constraint equating a variable to a 'PatVec'. Picks out the single
--- 'PmPat' of arity 1 and equates x to it. Returns the original Delta if that
--- fails. Otherwise it returns Nothing when the resulting Delta would be
--- unsatisfiable, or @Just delta'@ when the extended @delta'@ is still possibly
--- satisfiable.
-addVarPatVecCt :: Delta -> [Id] -> PatVec -> DsM (Maybe Delta)
--- This is just a simple version of pmcheck to compute the Covered Delta
--- (which pmcheck doesn't even attempt to keep).
--- Also PmGrd, although having pattern arity 0, really stores important info.
--- For example, as-patterns desugar to a plain variable match and an associated
--- PmGrd for the RHS of the @. We don't currently look into that PmGrd and I'm
--- not willing to duplicate any more of pmcheck.
-addVarPatVecCt delta (x:xs) (pat:pv)
-  | patternArity pat == 1 -- PmVar or PmCon
-  = runMaybeT $ do
-      delta' <- MaybeT (addVarPatCt delta x pat)
-      MaybeT (addVarPatVecCt delta' xs pv)
-  | otherwise -- PmGrd or PmFake
-  = addVarPatVecCt delta (x:xs) pv
-addVarPatVecCt delta []     pv = ASSERT( patVecArity pv == 0 ) pure (Just delta)
-addVarPatVecCt _     (_:_)  [] = panic "More match vars than patterns"
-
--- | Convert a pattern to a 'PmTypes' (will be either 'Nothing' if the pattern is
--- a guard pattern, or 'Just' an expression in all other cases) by dropping the
--- guards
-addVarPatCt :: Delta -> Id -> PmPat -> DsM (Maybe Delta)
-addVarPatCt delta x (PmVar { pm_var_id  = y }) = addTmCt delta (TmVarVar x y)
-addVarPatCt delta x (PmCon { pm_con_con = con, pm_con_args = args }) = runMaybeT $ do
-  arg_ids <- traverse (lift . mkPmId . pmPatType) args
-  delta' <- foldlM (\delta (y, arg) -> MaybeT (addVarPatCt delta y arg)) delta (zip arg_ids args)
-  MaybeT (addTmCt delta' (TmVarCon x con arg_ids))
-addVarPatCt delta _ _pat = ASSERT( patternArity _pat == 0 ) pure (Just delta)
+  locallyExtendPmDelta (\delta -> computeCovered pv xs delta) k
+
+-- | A dead simple version of 'pmcheck' that only computes the Covered set.
+-- So it only cares about collecting positive info.
+-- We use it to collect info from a pattern when we check its RHS.
+-- See 'addPatTmCs'.
+computeCovered :: PatVec -> ValVec -> Delta -> DsM (Maybe Delta)
+-- The duplication with 'pmcheck' is really unfortunate, but it's simpler than
+-- separating out the common cases with 'pmcheck', because that would make the
+-- ConVar case harder to understand.
+computeCovered [] [] delta = pure (Just delta)
+computeCovered (PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) vva delta = do
+  x <- mkPmId (exprType e)
+  delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
+  computeCovered (pv ++ ps) (x : vva) delta'
+computeCovered (PmVar _ x : ps) (y : vva) delta = do
+  delta' <- expectJust "x is fresh" <$> addTmCt delta (TmVarVar x y)
+  computeCovered ps vva delta'
+computeCovered (p : ps) (x : vva) delta
+  | PmCon{ pm_con_con = con, pm_con_args = args, pm_con_dicts = dicts } <- p
+  = addPmConCts delta x con dicts args >>= \case
+      Nothing -> pure Nothing
+      Just (delta', arg_vas) ->
+        computeCovered (args ++ ps) (arg_vas ++ vva) delta'
+computeCovered ps vs _delta = pprPanic "computeCovered" (ppr ps $$ ppr vs)
 
 {-
 %************************************************************************
diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs
index fd5d47c748..e27adc9fcd 100644
--- a/compiler/deSugar/PmOracle.hs
+++ b/compiler/deSugar/PmOracle.hs
@@ -7,9 +7,9 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
 {-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-}
 
 -- | The pattern match oracle. The main export of the module are the functions
--- 'addTmCt', 'refineToAltCon' and 'addRefutableAltCon' for adding
--- facts to the oracle, and 'provideEvidenceForEquation' to turn a 'Delta' into
--- a concrete evidence for an equation.
+-- 'addTmCt', 'addVarCoreCt', 'addRefutableAltCon' and 'addTypeEvidence' for
+-- adding facts to the oracle, and 'provideEvidenceForEquation' to turn a
+-- 'Delta' into a concrete evidence for an equation.
 module PmOracle (
 
         DsM, tracePm, mkPmId,
@@ -21,8 +21,6 @@ module PmOracle (
         addRefutableAltCon, -- Add a negative term equality
         addTmCt,            -- Add a positive term equality x ~ e
         addVarCoreCt,       -- Add a positive term equality x ~ core_expr
-        refineToAltCon,     -- Add a positive refinement x ~ K _ _
-        tmOracle,           -- Add multiple positive term equalities
         provideEvidenceForEquation,
     ) where
 
@@ -149,9 +147,9 @@ getUnmatchedConstructor (PM _tc ms)
 
 -- | Instantiate a 'ConLike' given its universal type arguments. Instantiates
 -- existential and term binders with fresh variables of appropriate type.
--- Also returns instantiated evidence variables from the match and the types of
--- strict constructor fields.
-mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
+-- Returns instantiated term variables from the match, type evidence and the
+-- types of strict constructor fields.
+mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
 --  * 'con' K is a ConLike
 --       - In the case of DataCons and most PatSynCons, these
 --         are associated with a particular TyCon T
@@ -160,9 +158,8 @@ mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
 --  * 'arg_tys' tys are the types K's universally quantified type
 --     variables should be instantiated to.
 --       - For DataCons and most PatSyns these are the arguments of their TyCon
---       - For cases like in #11336, #17112, the univ_ts include those variables
---         from the view pattern, so tys will have to come from the type checker.
---         They can't easily be recovered from the result type.
+--       - For cases like the PatSyns in #11336, #17112, we can't easily guess
+--         these, so don't call this function.
 --
 -- After instantiating the universal tyvars of K to tys we get
 --          K @tys :: forall bs. Q => s1 .. sn -> T tys
@@ -173,15 +170,15 @@ mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
 -- Results: [y1,..,yn]
 --          Q
 --          [s1]
---          [e1,..,en]
 mkOneConFull arg_tys con = do
   let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , field_tys, _con_res_ty)
         = conLikeFullSig con
   -- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ())
   -- Substitute universals for type arguments
   let subst_univ = zipTvSubst univ_tvs arg_tys
-  -- Instantiate fresh existentials as arguments to the contructor
-  (subst, ex_tvs') <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM
+  -- Instantiate fresh existentials as arguments to the contructor. This is
+  -- important for instantiating the Thetas and field types.
+  (subst, _) <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM
   let field_tys' = substTys subst field_tys
   -- Instantiate fresh term variables (VAs) as arguments to the constructor
   vars <- mapM mkPmId field_tys'
@@ -191,17 +188,7 @@ mkOneConFull arg_tys con = do
   -- Figure out the types of strict constructor fields
   let arg_is_banged = map isBanged $ conLikeImplBangs con
       strict_arg_tys = filterByList arg_is_banged field_tys'
-  return (vars, listToBag ty_cs, strict_arg_tys, ex_tvs')
-
-equateTyVars :: [TyVar] -> [TyVar] -> Bag TyCt
-equateTyVars ex_tvs1 ex_tvs2
-  = ASSERT(ex_tvs1 `equalLength` ex_tvs2)
-    listToBag $ catMaybes $ zipWith mb_to_evvar ex_tvs1 ex_tvs2
-  where
-    mb_to_evvar tv1 tv2
-      | tv1 == tv2 = Nothing
-      | otherwise  = Just (to_evvar tv1 tv2)
-    to_evvar tv1 tv2 = TyCt $ mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
+  return (vars, listToBag ty_cs, strict_arg_tys)
 
 -------------------------
 -- * Pattern match oracle
@@ -689,11 +676,7 @@ warning messages (which can be alleviated by someone with enough dedication).
 -- Returns a new 'Delta' if the new constraints are compatible with existing
 -- ones.
 tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
-tmIsSatisfiable new_tm_cs = SC $ \delta -> tmOracle delta new_tm_cs
-
--- | External interface to the term oracle.
-tmOracle :: Foldable f => Delta -> f TmCt -> DsM (Maybe Delta)
-tmOracle delta = runMaybeT . foldlM go delta
+tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM go delta new_tm_cs
   where
     go delta ct = MaybeT (addTmCt delta ct)
 
@@ -773,12 +756,14 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
 -- | A term constraint. Either equates two variables or a variable with a
 -- 'PmAltCon' application.
 data TmCt
-  = TmVarVar !Id !Id
-  | TmVarCon !Id !PmAltCon ![Id]
+  = TmVarVar     !Id !Id
+  | TmVarCon     !Id !PmAltCon ![Id]
+  | TmVarNonVoid !Id
 
 instance Outputable TmCt where
   ppr (TmVarVar x y)        = ppr x <+> char '~' <+> ppr y
   ppr (TmVarCon x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args)
+  ppr (TmVarNonVoid x)      = ppr x <+> text "/~ ⊥"
 
 -- | Add type equalities to 'Delta'.
 addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
@@ -791,6 +776,7 @@ addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
 addTmCt delta ct = runMaybeT $ case ct of
   TmVarVar x y        -> addVarVarCt delta (x, y)
   TmVarCon x con args -> addVarConCt delta x con args
+  TmVarNonVoid x      -> addVarNonVoidCt delta x
 
 -- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
 -- 'Delta' and return @Nothing@ if that leads to a contradiction.
@@ -866,7 +852,7 @@ guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon _) = do
   let (_, tc_args', _) = tcLookupDataFamInst env tc tc_args
   Just tc_args'
 guessConLikeUnivTyArgsFromResTy _   res_ty (PatSynCon ps)  = do
-  -- We were successful if we managed to instantiate *every* univ_tv of con.
+  -- We are successful if we managed to instantiate *every* univ_tv of con.
   -- This is difficult and bound to fail in some cases, see
   -- Note [Pattern synonym result type] in PatSyn.hs. So we just try our best
   -- here and be sure to return an instantiation when we can substitute every
@@ -878,6 +864,17 @@ guessConLikeUnivTyArgsFromResTy _   res_ty (PatSynCon ps)  = do
   subst <- tcMatchTy con_res_ty res_ty
   traverse (lookupTyVar subst) univ_tvs
 
+-- | Kind of tries to add a non-void contraint to 'Delta', but doesn't really
+-- commit to upholding that constraint in the future. This will be rectified
+-- in a follow-up patch. The status quo should work good enough for now.
+addVarNonVoidCt :: Delta -> Id -> MaybeT DsM Delta
+addVarNonVoidCt delta@MkDelta{ delta_tm_st = TmSt env } x = do
+  vi  <- lift $ initLookupVarInfo delta x
+  vi' <- MaybeT $ ensureInhabited delta vi
+  -- vi' has probably constructed and then thinned out some PossibleMatches.
+  -- We want to cache that work
+  pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi')}
+
 ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
    -- Returns (Just vi) guarantees that at least one member
    -- of each ConLike in the COMPLETE set satisfies the oracle
@@ -917,7 +914,7 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
       case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of
         Nothing -> pure True -- be conservative about this
         Just arg_tys -> do
-          (_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull arg_tys con
+          (_vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
           -- No need to run the term oracle compared to pmIsSatisfiable
           fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
             -- Important to pass False to tyIsSatisfiable here, so that we won't
@@ -938,165 +935,6 @@ ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env }
     set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env }
     go vi = MaybeT (ensureInhabited delta vi)
 
--- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at
--- @arg_tys@ with fresh variables (equating existentials to @ex_tyvars@).
--- It adds a new term equality equating @x@ is to the resulting 'PmAltCon' app
--- and new type equalities arising from GADT matches.
--- If successful, returns the new @delta@ and the fresh term variables, or
--- @Nothing@ otherwise.
-refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id]))
-refineToAltCon delta x l@PmAltLit{}           _arg_tys _ex_tvs1 = runMaybeT $ do
-  delta' <- addVarConCt delta x l []
-  pure (delta', [])
-refineToAltCon delta x alt@(PmAltConLike con) arg_tys  ex_tvs1  = do
-  -- The plan for ConLikes:
-  -- Suppose K :: forall a b y z. (y,b) -> z -> T a b
-  --   where the y,z are the existentials
-  -- @refineToAltCon delta x K [ex1, ex2]@ extends delta with the
-  --   positive information x :-> K y' z' p q, for some fresh y', z', p, q.
-  --   This is done by mkOneConFull.
-  --   We return the fresh [p,q] args, and bind the existentials [y',z'] to
-  --   [ex1, ex2].
-  -- Return Nothing if such a match is contradictory with delta.
-
-  (arg_vars, theta_ty_cs, strict_arg_tys, ex_tvs2) <- mkOneConFull arg_tys con
-
-  -- If we have identical constructors but different existential
-  -- tyvars, then generate extra equality constraints to ensure the
-  -- existential tyvars.
-  -- See Note [Coverage checking and existential tyvars].
-  let ex_ty_cs = equateTyVars ex_tvs1 ex_tvs2
-
-  let new_ty_cs = theta_ty_cs `unionBags` ex_ty_cs
-  let new_tm_cs = unitBag (TmVarCon x alt arg_vars)
-
-  -- Now check satifiability
-  mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
-  tracePm "refineToAltCon" (vcat [ ppr x
-                                 , ppr new_tm_cs
-                                 , ppr new_ty_cs
-                                 , ppr strict_arg_tys
-                                 , ppr delta
-                                 , ppr mb_delta ])
-  case mb_delta of
-    Nothing     -> pure Nothing
-    Just delta' -> pure (Just (delta', arg_vars))
-
-{-
-Note [Coverage checking and existential tyvars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-GHC's implementation of the pattern-match coverage algorithm (as described in
-the GADTs Meet Their Match paper) must take some care to emit enough type
-constraints when handling data constructors with exisentially quantified type
-variables. To better explain what the challenge is, consider a constructor K
-of the form:
-
-  K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p
-
-Where:
-
-* e_1, ..., e_m are the existentially bound type variables.
-* ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type
-  (e.g., Eq) or an equality constraint (e.g., e_1 ~ Int).
-* ty_1, ..., ty_n are the types of K's fields.
-* T u_1 ... u_p is the return type, where T is the data type constructor, and
-  u_1, ..., u_p are the universally quantified type variables.
-
-In the ConVar case, the coverage algorithm will have in hand the constructor
-K as well as a list of type arguments [t_1, ..., t_n] to substitute T's
-universally quantified type variables u_1, ..., u_n for. It's crucial to take
-these in as arguments, as it is non-trivial to derive them just from the result
-type of a pattern synonym and the ambient type of the match (#11336, #17112).
-The type checker already did the hard work, so we should just make use of it.
-
-The presence of existentially quantified type variables adds a significant
-wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with,
-but we don't want them to appear in the final PmCon, because then
-calling (mkOneConFull K) for other pattern variables might reuse the same
-existential tyvars, which is certainly wrong.
-
-Previously, GHC's solution to this wrinkle was to always create fresh names
-for the existential tyvars and put them into the PmCon. This works well for
-many cases, but it can break down if you nest GADT pattern matches in just
-the right way. For instance, consider the following program:
-
-    data App f a where
-      App :: f a -> App f (Maybe a)
-
-    data Ty a where
-      TBool :: Ty Bool
-      TInt  :: Ty Int
-
-    data T f a where
-      C :: T Ty (Maybe Bool)
-
-    foo :: T f a -> App f a -> ()
-    foo C (App TBool) = ()
-
-foo is a total program, but with the previous approach to handling existential
-tyvars, GHC would mark foo's patterns as non-exhaustive.
-
-When foo is desugared to Core, it looks roughly like so:
-
-    foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = ()
-
-(Where `a1` is an existential tyvar.)
-
-That, in turn, is processed by the coverage checker to become:
-
-    foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1))
-      | TBool <- pmvar123 |> co1
-      = ()
-
-Note that the type of pmvar123 is `f a1`—this will be important later.
-
-Now, we proceed with coverage-checking as usual. When we come to the
-ConVar case for App, we create a fresh variable `a2` to represent its
-existential tyvar. At this point, we have the equality constraints
-`(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope.
-
-However, when we check the guard, it will use the type of pmvar123, which is
-`f a1`. Thus, when considering if pmvar123 can match the constructor TInt,
-it will generate the constraint `a1 ~ Int`. This means our final set of
-equality constraints would be:
-
-    f  ~ Ty
-    a  ~ Maybe Bool
-    a  ~ Maybe a2
-    a1 ~ Int
-
-Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us,
-because GHC is unable to relate `a2` to `a1`, which really should be the same
-tyvar.
-
-Luckily, we can avoid this pitfall. Recall that the ConVar case was where we
-generated a PmCon with too-fresh existentials. But after ConVar, we have the
-ConCon case, which considers whether each constructor of a particular data type
-can be matched on in a particular spot.
-
-In the case of App, when we get to the ConCon case, we will compare our
-original App PmCon (from the source program) to the App PmCon created from the
-ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the
-existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here
-by emitting an additional `a1 ~ a2` constraint. Now our final set of equality
-constraints will be:
-
-    f  ~ Ty
-    a  ~ Maybe Bool
-    a  ~ Maybe a2
-    a1 ~ Int
-    a1 ~ a2
-
-Which is unsatisfiable, as we desired, since we now have that
-Int ~ a1 ~ a2 ~ Bool.
-
-In general, App might have more than one constructor, in which case we
-couldn't reuse the existential tyvar for App for a different constructor. This
-means that we can only use this trick in ConCon when the constructors are the
-same. But this is fine, since this is the only scenario where this situation
-arises in the first place!
--}
-
 --------------------------------------
 -- * Term oracle unification procedure
 
@@ -1203,7 +1041,7 @@ mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
 mkInhabitationCandidate x dc = do
   let cl = RealDataCon dc
   let tc_args = tyConAppArgs (idType x)
-  (arg_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull tc_args cl
+  (arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl
   pure InhabitationCandidate
         { ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
         , ic_ty_cs = ty_cs
@@ -1600,8 +1438,6 @@ provideEvidenceForEquation = go init_ts
       -> DsM [Delta]
     split_at_con rec_ts delta n x xs cl = do
       -- This will be really similar to the ConVar case
-      let (_,ex_tvs,_,_,_,_,_) = conLikeFullSig cl
-          -- we might need to freshen ex_tvs. Not sure
       -- We may need to reduce type famlies/synonyms in x's type first
       res <- pmTopNormaliseType (delta_ty_st delta) (idType x)
       let res_ty = normalisedSourceType res
@@ -1609,10 +1445,19 @@ provideEvidenceForEquation = go init_ts
       case guessConLikeUnivTyArgsFromResTy env res_ty cl of
         Nothing      -> pure [delta] -- We can't split this one, so assume it's inhabited
         Just arg_tys -> do
-          ev_pos <- refineToAltCon delta x (PmAltConLike cl) arg_tys ex_tvs >>= \case
-            Nothing                -> pure []
-            Just (delta', arg_vas) ->
-              go rec_ts (arg_vas ++ xs) n delta'
+          (arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl
+          let new_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
+          -- Now check satifiability
+          mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
+          tracePm "split_at_con" (vcat [ ppr x
+                                       , ppr new_tm_cs
+                                       , ppr new_ty_cs
+                                       , ppr strict_arg_tys
+                                       , ppr delta
+                                       , ppr mb_delta ])
+          ev_pos <- case mb_delta of
+            Nothing     -> pure []
+            Just delta' -> go rec_ts (arg_vars ++ xs) n delta'
 
           -- Only n' more equations to go...
           let n' = n - length ev_pos
diff --git a/testsuite/tests/pmcheck/should_compile/T17234.hs b/testsuite/tests/pmcheck/should_compile/T17234.hs
new file mode 100644
index 0000000000..27025d430a
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17234.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE BangPatterns #-}
+
+module Lib where
+
+import Data.Void
+
+f :: Void -> ()
+f !_ = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17234.stderr b/testsuite/tests/pmcheck/should_compile/T17234.stderr
new file mode 100644
index 0000000000..0a1912cfab
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17234.stderr
@@ -0,0 +1,4 @@
+
+T17234.hs:8:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f !_ = ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index e41d7f211c..19ae2c71b9 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -82,6 +82,8 @@ test('T17096', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
 test('T17112', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17234', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,