Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

-------------------------
Metric Decrease:
    ManyAlternatives
    T11195
-------------------------

1 files changed, 22 insertions, 11 deletions

diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs
index 921b829fb9..a0576494a0 100644
--- a/compiler/deSugar/Match.hs
+++ b/compiler/deSugar/Match.hs
@@ -690,7 +690,13 @@ Call @match@ with all of this information!
 
 matchWrapper
   :: HsMatchContext Name               -- ^ For shadowing warning messages
-  -> Maybe (LHsExpr GhcTc)             -- ^ Scrutinee, if we check a case expr
+  -> Maybe (LHsExpr GhcTc)             -- ^ Scrutinee. (Just scrut) for a case expr
+                                       --      case scrut of { p1 -> e1 ... }
+                                       --   (and in this case the MatchGroup will
+                                       --    have all singleton patterns)
+                                       --   Nothing for a function definition
+                                       --      f p1 q1 = ...  -- No "scrutinee"
+                                       --      f p2 q2 = ...  -- in this case
   -> MatchGroup GhcTc (LHsExpr GhcTc)  -- ^ Matches being desugared
   -> DsM ([Id], CoreExpr)              -- ^ Results (usually passed to 'match')
 
@@ -730,25 +736,30 @@ matchWrapper ctxt mb_scr (MG { mg_alts = (dL->L _ matches)
 
         ; eqns_info   <- mapM (mk_eqn_info new_vars) matches
 
-        -- pattern match check warnings
-        ; unless (isGenerated origin) $
-          when (isAnyPmCheckEnabled dflags (DsMatchContext ctxt locn)) $
-          addTmCsDs (genCaseTmCs1 mb_scr new_vars) $
-              -- See Note [Type and Term Equality Propagation]
-          checkMatches dflags (DsMatchContext ctxt locn) new_vars matches
+        -- Pattern match check warnings for /this match-group/
+        ; when (isMatchContextPmChecked dflags origin ctxt) $
+            addScrutTmCs mb_scr new_vars $
+            -- See Note [Type and Term Equality Propagation]
+            checkMatches dflags (DsMatchContext ctxt locn) new_vars matches
 
         ; result_expr <- handleWarnings $
                          matchEquations ctxt new_vars eqns_info rhs_ty
         ; return (new_vars, result_expr) }
   where
+    -- Called once per equation in the match, or alternative in the case
     mk_eqn_info vars (dL->L _ (Match { m_pats = pats, m_grhss = grhss }))
       = do { dflags <- getDynFlags
            ; let upats = map (unLoc . decideBangHood dflags) pats
                  dicts = collectEvVarsPats upats
-           ; tm_cs <- genCaseTmCs2 mb_scr upats vars
-           ; match_result <- addDictsDs dicts $ -- See Note [Type and Term Equality Propagation]
-                             addTmCsDs tm_cs  $ -- See Note [Type and Term Equality Propagation]
-                             dsGRHSs ctxt grhss rhs_ty
+
+           ; match_result <-
+              -- Extend the environment with knowledge about
+              -- the matches before desguaring the RHS
+              -- See Note [Type and Term Equality Propagation]
+              applyWhen (needToRunPmCheck dflags origin)
+                        (addTyCsDs dicts . addScrutTmCs mb_scr vars . addPatTmCs upats vars)
+                        (dsGRHSs ctxt grhss rhs_ty)
+
            ; return (EqnInfo { eqn_pats = upats
                              , eqn_orig = FromSource
                              , eqn_rhs = match_result }) }