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, 11 insertions, 22 deletions

diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 9534b4e20b..d937b3b134 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -29,8 +29,8 @@ module DsMonad (
 
         DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv,
 
-        -- Getting and setting EvVars and term constraints in local environment
-        getDictsDs, addDictsDs, getTmCsDs, addTmCsDs,
+        -- Getting and setting pattern match oracle states
+        getPmDelta, updPmDelta,
 
         -- Iterations for pm checking
         incrCheckPmIterDs, resetPmIterDs, dsGetCompleteMatches,
@@ -70,7 +70,7 @@ import BasicTypes ( Origin )
 import DataCon
 import ConLike
 import TyCon
-import PmExpr
+import {-# SOURCE #-} PmOracle
 import Id
 import Module
 import Outputable
@@ -82,7 +82,6 @@ import NameEnv
 import DynFlags
 import ErrUtils
 import FastString
-import Var (EvVar)
 import UniqFM ( lookupWithDefaultUFM )
 import Literal ( mkLitString )
 import CostCentreState
@@ -285,8 +284,7 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar cc_st_var
                            }
         lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv
                            , dsl_loc     = real_span
-                           , dsl_dicts   = emptyBag
-                           , dsl_tm_cs   = emptyBag
+                           , dsl_delta   = initDelta
                            , dsl_pm_iter = pmvar
                            }
     in (gbl_env, lcl_env)
@@ -386,23 +384,14 @@ the @SrcSpan@ being carried around.
 getGhcModeDs :: DsM GhcMode
 getGhcModeDs =  getDynFlags >>= return . ghcMode
 
--- | Get in-scope type constraints (pm check)
-getDictsDs :: DsM (Bag EvVar)
-getDictsDs = do { env <- getLclEnv; return (dsl_dicts env) }
+-- | Get the current pattern match oracle state. See 'dsl_delta'.
+getPmDelta :: DsM Delta
+getPmDelta = do { env <- getLclEnv; return (dsl_delta env) }
 
--- | Add in-scope type constraints (pm check)
-addDictsDs :: Bag EvVar -> DsM a -> DsM a
-addDictsDs ev_vars
-  = updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
-
--- | Get in-scope term constraints (pm check)
-getTmCsDs :: DsM (Bag TmVarCt)
-getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
-
--- | Add in-scope term constraints (pm check)
-addTmCsDs :: Bag TmVarCt -> DsM a -> DsM a
-addTmCsDs tm_cs
-  = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
+-- | Set the pattern match oracle state within the scope of the given action.
+-- See 'dsl_delta'.
+updPmDelta :: Delta -> DsM a -> DsM a
+updPmDelta delta = updLclEnv (\env -> env { dsl_delta = delta })
 
 -- | Increase the counter for elapsed pattern match check iterations.
 -- If the current counter is already over the limit, fail