PmCheck: Pick up `EvVar`s bound in `HsWrapper`s for long-distance infowip/T18049

`HsWrapper`s introduce evidence bindings through `WpEvLam` which the
pattern-match coverage checker should be made aware of.

Failing to do so caused #18049, where the resulting impreciseness of
imcompleteness warnings seemingly contradicted with
`-Winaccessible-code`.

The solution is simple: Collect all the evidence binders of an
`HsWrapper` and add it to the ambient `Deltas` before desugaring
the wrapped expression.

But that means we pick up many more evidence bindings, even when they
wrap around code without a single pattern match to check! That regressed
`T3064` by over 300%, so now we are adding long-distance info lazily
through judicious use of `unsafeInterleaveIO`.

Fixes #18049.

6 files changed, 95 insertions, 32 deletions

diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 7bc6fe2512..edc1e50ebb 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -33,7 +33,7 @@ import {-# SOURCE #-}   GHC.HsToCore.Match ( matchWrapper )
 import GHC.HsToCore.Monad
 import GHC.HsToCore.GuardedRHSs
 import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck ( needToRunPmCheck, addTyCsDs, checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGuardMatches )
 
 import GHC.Hs             -- lots of things
 import GHC.Core           -- lots of things
@@ -145,12 +145,20 @@ dsHsBind dflags (VarBind { var_id = var
                           else []
         ; return (force_var, [core_bind]) }
 
-dsHsBind dflags b@(FunBind { fun_id = L _ fun
+dsHsBind dflags b@(FunBind { fun_id = L loc fun
                            , fun_matches = matches
                            , fun_ext = co_fn
                            , fun_tick = tick })
- = do   { (args, body) <- matchWrapper
-                           (mkPrefixFunRhs (noLoc $ idName fun))
+ = do   { (args, body) <- addTyCsDs FromSource (hsWrapDictBinders co_fn) $
+                          -- FromSource might not be accurate (we don't have any
+                          -- origin annotations for things in this module), but at
+                          -- worst we do superfluous calls to the pattern match
+                          -- oracle.
+                          -- addTyCsDs: Add type evidence to the refinement type
+                          --            predicate of the coverage checker
+                          -- See Note [Type and Term Equality Propagation] in PmCheck
+                          matchWrapper
+                           (mkPrefixFunRhs (L loc (idName fun)))
                            Nothing matches
         ; core_wrap <- dsHsWrapper co_fn
         ; let body' = mkOptTickBox tick body
@@ -189,15 +197,7 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
                           , abs_exports = exports
                           , abs_ev_binds = ev_binds
                           , abs_binds = binds, abs_sig = has_sig })
-  = do { ds_binds <- applyWhen (needToRunPmCheck dflags FromSource)
-                               -- FromSource might not be accurate, but at worst
-                               -- we do superfluous calls to the pattern match
-                               -- oracle.
-                               -- addTyCsDs: push type constraints deeper
-                               --            for inner pattern match check
-                               -- See Check, Note [Type and Term Equality Propagation]
-                               (addTyCsDs (listToBag dicts))
-                               (dsLHsBinds binds)
+  = do { ds_binds <- addTyCsDs FromSource (listToBag dicts) (dsLHsBinds binds)
 
        ; ds_ev_binds <- dsTcEvBinds_s ev_binds
 
@@ -206,7 +206,6 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
 
 dsHsBind _ (PatSynBind{}) = panic "dsHsBind: PatSynBind"
 
-
 -----------------------
 dsAbsBinds :: DynFlags
            -> [TyVar] -> [EvVar] -> [ABExport GhcTc]
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 2ea1c17e04..0dea21d70b 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -32,7 +32,7 @@ import GHC.HsToCore.ListComp
 import GHC.HsToCore.Utils
 import GHC.HsToCore.Arrows
 import GHC.HsToCore.Monad
-import GHC.HsToCore.PmCheck ( checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGuardMatches )
 import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Core.FamInstEnv( topNormaliseType )
@@ -280,7 +280,8 @@ dsExpr hswrap@(XExpr (HsWrap co_fn e))
                  HsConLikeOut _ (RealDataCon dc) -> return $ varToCoreExpr (dataConWrapId dc)
                  XExpr (HsWrap _ _) -> pprPanic "dsExpr: HsWrap inside HsWrap" (ppr hswrap)
                  HsPar _ _ -> pprPanic "dsExpr: HsPar inside HsWrap" (ppr hswrap)
-                 _ -> dsExpr e
+                 _ -> addTyCsDs FromSource (hsWrapDictBinders co_fn) $
+                      dsExpr e
                -- See Note [Detecting forced eta expansion]
        ; wrap' <- dsHsWrapper co_fn
        ; dflags <- getDynFlags
diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index 8b34f275b0..f9de7c8282 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -14,7 +14,7 @@ Pattern Matching Coverage Checking.
 module GHC.HsToCore.PmCheck (
         -- Checking and printing
         checkSingle, checkMatches, checkGuardMatches,
-        needToRunPmCheck, isMatchContextPmChecked,
+        isMatchContextPmChecked,
 
         -- See Note [Type and Term Equality Propagation]
         addTyCsDs, addScrutTmCs
@@ -45,7 +45,7 @@ import GHC.Core.DataCon
 import GHC.Core.TyCon
 import GHC.Types.Var (EvVar)
 import GHC.Core.Coercion
-import GHC.Tc.Types.Evidence ( HsWrapper(..), isIdHsWrapper )
+import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
 import GHC.Tc.Utils.TcType (evVarPred)
 import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
 import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
@@ -53,6 +53,7 @@ import GHC.HsToCore.Utils (selectMatchVar)
 import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
 import GHC.HsToCore.Monad
 import GHC.Data.Bag
+import GHC.Data.IOEnv (unsafeInterleaveM)
 import GHC.Data.OrdList
 import GHC.Core.TyCo.Rep
 import GHC.Core.Type
@@ -1033,20 +1034,30 @@ Functions `addScrutTmCs' is responsible for generating
 these constraints.
 -}
 
+-- | Locally update 'dsl_deltas' with the given action, but defer evaluation
+-- with 'unsafeInterleaveM' in order not to do unnecessary work.
 locallyExtendPmDelta :: (Deltas -> DsM Deltas) -> DsM a -> DsM a
-locallyExtendPmDelta ext k = getPmDeltas >>= ext >>= \deltas -> do
-  inh <- isInhabited deltas
-  -- If adding a constraint would lead to a contradiction, don't add it.
-  -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@
-  -- for why this is done.
-  if inh
-    then updPmDeltas deltas k
-    else k
-
--- | Add in-scope type constraints
-addTyCsDs :: Bag EvVar -> DsM a -> DsM a
-addTyCsDs ev_vars =
-  locallyExtendPmDelta (\deltas -> addPmCtsDeltas deltas (PmTyCt . evVarPred <$> ev_vars))
+locallyExtendPmDelta ext k = do
+  deltas <- getPmDeltas
+  deltas' <- unsafeInterleaveM $ do
+    deltas' <- ext deltas
+    inh <- isInhabited deltas'
+    -- If adding a constraint would lead to a contradiction, don't add it.
+    -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@
+    -- for why this is done.
+    if inh
+      then pure deltas'
+      else pure deltas
+  updPmDeltas deltas' k
+
+-- | Add in-scope type constraints if the coverage checker might run and then
+-- run the given action.
+addTyCsDs :: Origin -> Bag EvVar -> DsM a -> DsM a
+addTyCsDs origin ev_vars m = do
+  dflags <- getDynFlags
+  applyWhen (needToRunPmCheck dflags origin)
+            (locallyExtendPmDelta (\deltas -> addPmCtsDeltas deltas (PmTyCt . evVarPred <$> ev_vars)))
+            m
 
 -- | Add equalities for the scrutinee to the local 'DsM' environment when
 -- checking a case expression:
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 9c7e237ffe..d496057f47 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -10,7 +10,7 @@ module GHC.Tc.Types.Evidence (
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
   mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
   mkWpFun, idHsWrapper, isIdHsWrapper, isErasableHsWrapper,
-  pprHsWrapper,
+  pprHsWrapper, hsWrapDictBinders,
 
   -- * Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
@@ -370,6 +370,27 @@ isErasableHsWrapper = go
     go WpTyApp{}               = True
     go WpLet{}                 = False
 
+hsWrapDictBinders :: HsWrapper -> Bag DictId
+-- ^ Identifies the /lambda-bound/ dictionaries of an 'HsWrapper'. This is used
+-- (only) to allow the pattern-match overlap checker to know what Given
+-- dictionaries are in scope.
+--
+-- We specifically do not collect dictionaries bound in a 'WpLet'. These are
+-- either superclasses of lambda-bound ones, or (extremely numerous) results of
+-- binding Wanted dictionaries.  We definitely don't want all those cluttering
+-- up the Given dictionaries for pattern-match overlap checking!
+hsWrapDictBinders wrap = go wrap
+ where
+   go (WpEvLam dict_id)   = unitBag dict_id
+   go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
+   go (WpFun _ w _ _)     = go w
+   go WpHole              = emptyBag
+   go (WpCast  {})        = emptyBag
+   go (WpEvApp {})        = emptyBag
+   go (WpTyLam {})        = emptyBag
+   go (WpTyApp {})        = emptyBag
+   go (WpLet   {})        = emptyBag
+
 collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
 -- Collect the outer lambda binders of a HsWrapper,
 -- stopping as soon as you get to a non-lambda binder
diff --git a/testsuite/tests/pmcheck/should_compile/T18049.hs b/testsuite/tests/pmcheck/should_compile/T18049.hs
new file mode 100644
index 0000000000..b63ffdf751
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18049.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+module Bug where
+
+import Data.Kind
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+f :: SBool b
+  -> (b ~ True  => SBool b -> r)
+  -> (b ~ False => SBool b -> r)
+  -> r
+f x t f =
+  case x of
+    SFalse -> f x
+    STrue  -> t x
+
+g :: forall b. SBool b -> ()
+g x = f x
+  (\x' ->
+    case x' of
+      -- SFalse -> ()
+      STrue  -> ())
+  (\_ -> ())
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 0c3bfcf510..2e4e3942ac 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -118,6 +118,8 @@ test('T17977', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 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'])
 
 # Other tests
 test('pmc001', [], compile,