tmpwip/pmcheck-refactor-deltas

6 files changed, 225 insertions, 154 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index c8e42dd248..2e0872a276 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -124,7 +124,7 @@ type GrdVec = [PmGrd]
 -- covered by a pattern match. E.g. @f Nothing = <rhs>@ might be given an
 -- uncovered set @[x :-> Just y]@ or @[x /= Nothing]@, where @x@ is the variable
 -- matching against @f@'s first argument.
-type Uncovered = [Delta]
+type Uncovered = Theta
 
 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
 -- covered and the divergent set (we store the uncovered set though, since we
@@ -210,9 +210,7 @@ combinePartialResults (PartialResult cs1 vsa1 ds1 ap1) (PartialResult cs2 vsa2 d
 
 instance Outputable PartialResult where
   ppr (PartialResult c unc d pc)
-    = hang (text "PartialResult" <+> ppr c <+> ppr d <+> ppr pc) 2 (ppr_unc unc)
-    where
-      ppr_unc = braces . fsep . punctuate comma . map ppr
+    = hang (text "PartialResult" <+> ppr c <+> ppr d <+> ppr pc) 2 (ppr unc)
 
 instance Semi.Semigroup PartialResult where
   (<>) = combinePartialResults
@@ -237,7 +235,7 @@ instance Monoid PartialResult where
 data PmResult =
   PmResult {
       pmresultRedundant    :: [Located [LPat GhcTc]]
-    , pmresultUncovered    :: [Delta]
+    , pmresultUncovered    :: Theta
     , pmresultInaccessible :: [Located [LPat GhcTc]]
     , pmresultApproximate  :: Precision }
 
@@ -269,13 +267,12 @@ checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
 checkSingle' locn var p = do
   fam_insts <- dsGetFamInstEnvs
   grds      <- translatePat fam_insts var p
-  missing   <- getPmDelta
+  missing   <- getPmTheta
   tracePm "checkSingle': missing" (ppr missing)
   PartialResult cs us ds pc <- pmCheck grds [] 1 missing
   dflags <- getDynFlags
-  us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
   let plain = PmResult { pmresultRedundant    = []
-                       , pmresultUncovered    = us'
+                       , pmresultUncovered    = us
                        , pmresultInaccessible = []
                        , pmresultApproximate  = pc }
   return $ case (cs,ds) of
@@ -316,18 +313,17 @@ checkMatches dflags ctxt vars matches = do
 -- | Check a matchgroup (case, functions, etc.).
 checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
 checkMatches' vars matches = do
-  init_delta <- getPmDelta
+  init_theta <- getPmTheta
   missing <- case matches of
     -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
-    [] | [var] <- vars -> maybeToList <$> addTmCt init_delta (TmVarNonVoid var)
-    _                  -> pure [init_delta]
+    [] | [var] <- vars -> addTmCt init_theta (TmVarNonVoid var)
+    _                  -> pure init_theta
   tracePm "checkMatches': missing" (ppr missing)
   (rs,us,ds,pc) <- go matches missing
   dflags <- getDynFlags
-  us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us
   return $ PmResult {
                 pmresultRedundant    = map hsLMatchToLPats rs
-              , pmresultUncovered    = us'
+              , pmresultUncovered    = us
               , pmresultInaccessible = map hsLMatchToLPats ds
               , pmresultApproximate  = pc }
   where
@@ -343,9 +339,9 @@ checkMatches' vars matches = do
       fam_insts          <- dsGetFamInstEnvs
       (clause, guards)   <- translateMatch fam_insts vars m
       let limit                     = maxPmCheckModels dflags
-          n_siblings                = length missing
-          throttled_check delta     =
-            snd <$> throttle limit (pmCheck clause guards) n_siblings delta
+          n_siblings                = sizeTheta missing
+          throttled_check theta     =
+            snd <$> throttle limit (pmCheck clause guards) n_siblings theta
 
       r@(PartialResult cs missing' ds pc1) <- runMany throttled_check missing
 
@@ -363,14 +359,6 @@ checkMatches' vars matches = do
     hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
     hsLMatchToLPats _                                   = panic "checkMatches'"
 
-getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
-getNFirstUncovered _    0 _              = pure []
-getNFirstUncovered _    _ []             = pure []
-getNFirstUncovered vars n (delta:deltas) = do
-  front <- provideEvidence vars n delta
-  back <- getNFirstUncovered vars (n - length front) deltas
-  pure (front ++ back)
-
 {- Note [Checking EmptyCase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -XEmptyCase is useful for matching on empty data types like 'Void'. For example,
@@ -432,7 +420,7 @@ mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
 mkPmLitGrds x (PmLit _ (PmLitString s)) = do
   -- We translate String literals to list literals for better overlap reasoning.
   -- It's a little unfortunate we do this here rather than in
-  -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much
+  -- Oracle.trySolve and Oracle.addRefutableAltCon, but it's so much
   -- simpler here.
   -- See Note [Representation of Strings in TmState] in GHC.HsToCore.PmCheck.Oracle
   vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
@@ -969,9 +957,9 @@ Main functions are:
 -- Otherwise we just return the singleton set of the original @delta@.
 -- This amounts to forgetting about the refined facts we got from running the
 -- action.
-throttle :: Int -> (Int -> Delta -> DsM PartialResult) -> Int -> Delta -> DsM (Int, PartialResult)
-throttle limit f n_siblings delta = do
-  res <- f n_siblings delta
+throttle :: Int -> (Theta -> DsM PartialResult) -> Theta -> DsM (Int, PartialResult)
+throttle limit f theta = do
+  res <- f theta
   let n_own_children = length (presultUncovered res)
   let n_next_gen = n_siblings * n_own_children
   -- Birth control!
@@ -985,29 +973,27 @@ runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
 runMany f unc = mconcat <$> traverse f unc
 
 -- | Print diagnostic info and actually call 'pmCheck''.
-pmCheck :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
-pmCheck ps guards n delta = do
+pmCheck :: GrdVec -> [GrdVec] -> Int -> Theta -> DsM PartialResult
+pmCheck ps guards n theta = do
   tracePm "pmCheck {" $ vcat [ ppr n <> colon
                            , hang (text "patterns:") 2 (ppr ps)
                            , hang (text "guards:") 2 (ppr guards)
-                           , ppr delta ]
-  res <- pmCheck' ps guards n delta
+                           , ppr theta ]
+  res <- pmCheck' ps guards n theta
   tracePm "}:" (ppr res) -- braces are easier to match by tooling
   return res
 
--- | Lifts 'pmCheck' over a 'DsM (Maybe Delta)'.
-pmCheckM :: GrdVec -> [GrdVec] -> Int -> DsM (Maybe Delta) -> DsM PartialResult
-pmCheckM ps guards n m_mb_delta = m_mb_delta >>= \case
-  Nothing    -> pure mempty
-  Just delta -> pmCheck ps guards n delta
+-- | Lifts 'pmCheck' over a 'DsM Theta'.
+pmCheckM :: GrdVec -> [GrdVec] -> Int -> DsM Theta -> DsM PartialResult
+pmCheckM ps guards n m_theta = m_theta >>= pmCheck ps guards n
 
 -- | Check the list of mutually exclusive guards
-pmCheckGuards :: [GrdVec] -> Int -> Delta -> DsM PartialResult
-pmCheckGuards []       _ delta = return (usimple delta)
-pmCheckGuards (gv:gvs) n delta = do
+pmCheckGuards :: [GrdVec] -> Int -> Theta -> DsM PartialResult
+pmCheckGuards []       _ theta = return (usimple theta)
+pmCheckGuards (gv:gvs) n theta = do
   dflags <- getDynFlags
   let limit = maxPmCheckModels dflags `div` 5
-  (n', PartialResult cs unc ds pc) <- throttle limit (pmCheck gv []) n delta
+  (n', PartialResult cs unc ds pc) <- throttle limit (pmCheck gv []) n theta
   (PartialResult css uncs dss pcs) <- runMany (pmCheckGuards gvs n') unc
   return $ PartialResult (cs `mappend` css)
                          uncs
@@ -1022,18 +1008,17 @@ pmCheck'
   -> [GrdVec] -- ^ (Possibly multiple) guards of the clause
   -> Int      -- ^ Estimate on the number of similar 'Delta's to handle.
               --   See 6. in Note [Countering exponential blowup]
-  -> Delta    -- ^ Oracle state giving meaning to the identifiers in the ValVec
+  -> Theta    -- ^ Oracle state giving meaning to the identifiers in the ValVec
   -> DsM PartialResult
-pmCheck' [] guards n delta
+pmCheck' [] guards n theta
   | null guards = return $ mempty { presultCovered = Covered }
-  | otherwise   = pmCheckGuards guards n delta
+  | otherwise   = pmCheckGuards guards n theta
 
 -- let x = e: Add x ~ e to the oracle
-pmCheck' (PmLet { pm_id = x, pm_let_expr = e } : ps) guards n delta = do
+pmCheck' (PmLet { pm_id = x, pm_let_expr = e } : ps) guards n theta = do
   tracePm "PmLet" (vcat [ppr x, ppr e])
-  -- x is fresh because it's bound by the let
-  delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
-  pmCheck ps guards n delta'
+  theta' <- addTmCt theta (TmVarCore x e)
+  pmCheck ps guards n theta'
 
 -- Bang x: Add x /~ _|_ to the oracle
 pmCheck' (PmBang x : ps) guards n delta = do
@@ -1059,7 +1044,7 @@ pmCheck' (p : ps) guards n delta
   let pr_pos' = addConMatchStrictness delta x con pr_pos
 
   -- Stuff for <next equation>
-  pr_neg <- addRefutableAltCon delta x con >>= \case
+  pr_neg <- addTmCt delta (TmVarNotCon x con) >>= \case
     Nothing     -> pure mempty
     Just delta' -> pure (usimple delta')
 
@@ -1069,11 +1054,11 @@ pmCheck' (p : ps) guards n delta
   let pr = mkUnion pr_pos' pr_neg
   pure pr
 
-addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta)
-addPmConCts delta x con dicts fields = runMaybeT $ do
-  delta_ty    <- MaybeT $ addTypeEvidence delta (listToBag dicts)
-  delta_tm_ty <- MaybeT $ addTmCt delta_ty (TmVarCon x con fields)
-  pure delta_tm_ty
+addPmConCts :: Theta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM Theta
+addPmConCts theta x con dicts fields = do
+  theta_ty    <- addTypeEvidence theta (listToBag dicts)
+  theta_tm_ty <- addTmCt theta_ty (TmVarCon x con fields)
+  pure theta_tm_ty
 
 -- ----------------------------------------------------------------------------
 -- * Utilities for main checking
@@ -1141,18 +1126,18 @@ Functions `addScrutTmCs' and `addPatTmCs' are responsible for generating
 these constraints.
 -}
 
-locallyExtendPmDelta :: (Delta -> DsM (Maybe Delta)) -> DsM a -> DsM a
-locallyExtendPmDelta ext k = getPmDelta >>= ext >>= \case
+locallyExtendPmTheta :: (Theta -> DsM Theta) -> DsM a -> DsM a
+locallyExtendPmTheta ext k = getPmTheta >>= ext >>= \case
   -- 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.
-  Nothing     -> k
-  Just delta' -> updPmDelta delta' k
+  EmptyTheta  -> k
+  theta'      -> updPmDelta theta' k
 
 -- | Add in-scope type constraints
 addTyCsDs :: Bag EvVar -> DsM a -> DsM a
 addTyCsDs ev_vars =
-  locallyExtendPmDelta (\delta -> addTypeEvidence delta ev_vars)
+  locallyExtendPmTheta (\theta -> addTypeEvidence theta ev_vars)
 
 -- | Add equalities for the scrutinee to the local 'DsM' environment when
 -- checking a case expression:
@@ -1163,7 +1148,7 @@ addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
 addScrutTmCs Nothing    _   k = k
 addScrutTmCs (Just scr) [x] k = do
   scr_e <- dsLExpr scr
-  locallyExtendPmDelta (\delta -> addVarCoreCt delta x scr_e) k
+  locallyExtendPmTheta (\theta -> addTmCt theta (TmVarCore x scr_e)) k
 addScrutTmCs _   _   _ = panic "addScrutTmCs: HsCase with more than one case binder"
 
 -- | Add equalities to the local 'DsM' environment when checking the RHS of a
@@ -1179,28 +1164,28 @@ addPatTmCs :: [Pat GhcTc]           -- LHS       (should have length 1)
 addPatTmCs ps xs k = do
   fam_insts <- dsGetFamInstEnvs
   grds <- concat <$> zipWithM (translatePat fam_insts) xs ps
-  locallyExtendPmDelta (\delta -> computeCovered grds delta) k
+  locallyExtendPmTheta (\delta -> computeCovered grds 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 :: GrdVec -> Delta -> DsM (Maybe Delta)
+computeCovered :: GrdVec -> Theta -> DsM Theta
 -- 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 (PmLet { pm_id = x, pm_let_expr = e } : ps) delta = do
-  delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
-  computeCovered ps delta'
-computeCovered (PmBang{} : ps) delta = do
-  computeCovered ps delta
-computeCovered (p : ps) delta
+computeCovered [] theta = pure (Just theta)
+computeCovered (PmLet { pm_id = x, pm_let_expr = e } : ps) theta = do
+  theta' <- addTmCt theta (TmVarCore x e)
+  computeCovered ps theta'
+computeCovered (PmBang{} : ps) theta = do
+  computeCovered ps theta
+computeCovered (p : ps) theta
   | PmCon{ pm_id = x, pm_con_con = con, pm_con_args = args
          , pm_con_dicts = dicts } <- p
-  = addPmConCts delta x con dicts args >>= \case
+  = addPmConCts theta x con dicts args >>= \case
       Nothing     -> pure Nothing
-      Just delta' -> computeCovered ps delta'
+      Just theta' -> computeCovered ps theta'
 
 {-
 %************************************************************************
@@ -1247,8 +1232,9 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
       when exists_i $ forM_ inaccessible $ \(dL->L l q) -> do
         putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
                                (pprEqn q "has inaccessible right hand side"))
-      when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
-        pprEqns vars uncovered
+      when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $ do
+        unc_deltas <- provideEvidence vars (maxPatterns + 1) uncovered
+        pprEqns vars unc_deltas
   where
     PmResult
       { pmresultRedundant = redundant
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 1b5c5b24c8..c2b6192e22 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -13,13 +13,11 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
 module GHC.HsToCore.PmCheck.Oracle (
 
         DsM, tracePm, mkPmId,
-        Delta, initDelta, lookupRefuts, lookupSolution,
+        Delta, Theta, initTheta, lookupRefuts, lookupSolution,
 
         TmCt(..),
         addTypeEvidence,    -- Add type equalities
-        addRefutableAltCon, -- Add a negative term equality
-        addTmCt,            -- Add a positive term equality x ~ e
-        addVarCoreCt,       -- Add a positive term equality x ~ core_expr
+        addTmCt,            -- Add a term equality
         canDiverge,         -- Try to add the term equality x ~ ⊥
         provideEvidence,
     ) where
@@ -72,7 +70,7 @@ import DsMonad hiding (foldlM)
 import FamInst
 import FamInstEnv
 
-import Control.Monad (guard, mzero)
+import Control.Monad (guard, mzero, (>=>))
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Trans.State.Strict
 import Data.Bifunctor (second)
@@ -197,27 +195,23 @@ that we expect.
 --   3. 'tysAreNonVoid', checks if the given types have an inhabitant
 -- Functions like 'pmIsSatisfiable', 'nonVoid' and 'testInhabited' plug these
 -- together as they see fit.
-newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta))
+newtype SatisfiabilityCheck = SC (Theta -> DsM Theta)
 
 -- | Check the given 'Delta' for satisfiability by the the given
 -- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Delta' if
 -- successful, and 'Nothing' otherwise.
-runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
-runSatisfiabilityCheck delta (SC chk) = chk delta
+runSatisfiabilityCheck :: Theta -> SatisfiabilityCheck -> DsM Theta
+runSatisfiabilityCheck theta (SC chk) = chk theta
 
--- | Allowing easy composition of 'SatisfiabilityCheck's.
+-- | Allowing easy composition of 'SatisfiabilityCheck's. Like @EndoM Theta@
+-- from the @foldl@ package.
 instance Semigroup SatisfiabilityCheck where
-  -- This is @a >=> b@ from MaybeT DsM
-  SC a <> SC b = SC c
-    where
-      c delta = a delta >>= \case
-        Nothing     -> pure Nothing
-        Just delta' -> b delta'
+  SC a <> SC b = SC (a >=> b)
 
 instance Monoid SatisfiabilityCheck where
   -- We only need this because of mconcat (which we use in place of sconcat,
   -- which requires NonEmpty lists as argument, making all call sites ugly)
-  mempty = SC (pure . Just)
+  mempty = SC pure
 
 -------------------------------
 -- * Oracle transition function
@@ -231,15 +225,14 @@ instance Monoid SatisfiabilityCheck where
 -- discussed in GADTs Meet Their Match. For an explanation of what role they
 -- serve, see @Note [Strict argument type constraints]@.
 pmIsSatisfiable
-  :: Delta       -- ^ The ambient term and type constraints
+  :: Theta       -- ^ The ambient term and type constraints
                  --   (known to be satisfiable).
   -> Bag TmCt    -- ^ The new term constraints.
   -> Bag TyCt    -- ^ The new type constraints.
   -> [Type]      -- ^ The strict argument types.
-  -> DsM (Maybe Delta)
-                 -- ^ @'Just' delta@ if the constraints (@delta@) are
-                 -- satisfiable, and each strict argument type is inhabitable.
-                 -- 'Nothing' otherwise.
+  -> DsM Theta
+                 -- ^ Keeps only 'Delta's which are satisfiable, and each strict
+                 -- argument type is inhabitable.
 pmIsSatisfiable amb_cs new_tm_cs new_ty_cs strict_arg_tys =
   -- The order is important here! Check the new type constraints before we check
   -- whether strict argument types are inhabited given those constraints.
@@ -531,16 +524,17 @@ tyOracle (TySt inert) cts
 -- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
 -- for emptiness if the first argument is 'True'.
 tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck
-tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta ->
+tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \theta ->
   if isEmptyBag new_ty_cs
-    then pure (Just delta)
-    else tyOracle (delta_ty_st delta) new_ty_cs >>= \case
-      Nothing                   -> pure Nothing
-      Just ty_st'               -> do
-        let delta' = delta{ delta_ty_st = ty_st' }
-        if recheck_complete_sets
-          then ensureAllPossibleMatchesInhabited delta'
-          else pure (Just delta')
+    then pure theta
+    else flip liftDeltaM theta $ \delta ->
+      tyOracle (delta_ty_st delta) new_ty_cs >>= \case
+        Nothing                   -> pure Nothing
+        Just ty_st'               -> do
+          let delta' = delta{ delta_ty_st = ty_st' }
+          if recheck_complete_sets
+            then ensureAllPossibleMatchesInhabited delta'
+            else pure (Just delta')
 
 
 {- *********************************************************************
@@ -658,9 +652,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 -> runMaybeT $ foldlM go delta new_tm_cs
-  where
-    go delta ct = MaybeT (addTmCt delta ct)
+tmIsSatisfiable new_tm_cs = SC $ \theta -> foldlM addTmCt theta new_tm_cs
 
 -----------------------
 -- * Looking up VarInfo
@@ -823,36 +815,46 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
 -------------------------------
 -- * Adding facts to the oracle
 
--- | A term constraint. Either equates two variables or a variable with a
--- 'PmAltCon' application.
+-- | A term constraint.
 data TmCt
   = TmVarVar     !Id !Id
+  -- ^ Equates two variables. Prints as @x ~ y@.
   | TmVarCon     !Id !PmAltCon ![Id]
+  -- ^ Equates a variable to a 'PmAltCon' app. Prints as @x ~ Just y@.
   | TmVarNonVoid !Id
+  -- ^ Asserts that a variable is non-void. Prints as @x /~ ⊥@.
+  | TmVarNotCon  !Id !PmAltCon
+  -- ^ Asserts that a variable is /not/ a certain 'PmAltCon' app. Prints as @x /~ Just@.
+  | TmVarCore  !Id !CoreExpr
+  -- ^ Equates a variable with a 'CoreExpr'. Prints as @x ~ f (g 42)@.
 
 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 "/~ ⊥"
+  ppr (TmVarNotCon x con)   = ppr x <+> text "/~" <+> ppr con
+  ppr (TmVarCore x e)       = ppr x <+> char '~' <+> ppr e
 
--- | Add type equalities to 'Delta'.
-addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
-addTypeEvidence delta dicts
-  = runSatisfiabilityCheck delta (tyIsSatisfiable True (TyCt . evVarPred <$> dicts))
+-- | Add type equalities to 'Theta'.
+addTypeEvidence :: Theta -> Bag EvVar -> DsM Theta
+addTypeEvidence theta dicts =
+  runSatisfiabilityCheck theta (tyIsSatisfiable True (TyCt . evVarPred <$> dicts))
 
 -- | Tries to equate two representatives in 'Delta'.
 -- See Note [TmState invariants].
-addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
-addTmCt delta ct = runMaybeT $ case ct of
+addTmCt :: Theta -> TmCt -> DsM Theta
+addTmCt theta ct = flip liftDeltaM theta $ \delta -> 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
+  TmVarNotCon x con   -> addVarNotConCt delta x con
+  TmVarCore x e       -> addVarCoreCt delta x e
 
 -- | 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.
 -- See Note [TmState invariants].
-addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
-addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = runMaybeT $ do
+addVarNotConCt :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
+addVarNotConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
   vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x)
   -- 1. Bail out quickly when nalt contradicts a solution
   let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal
@@ -987,7 +989,7 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
           (_vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
           tracePm "inh_test" (ppr con $$ ppr ty_cs)
           -- No need to run the term oracle compared to pmIsSatisfiable
-          fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
+          fmap isEmptyTheta <$> runSatisfiabilityCheck (unitTheta delta) $ mconcat
             -- Important to pass False to tyIsSatisfiable here, so that we won't
             -- recursively call ensureAllPossibleMatchesInhabited, leading to an
             -- endless recursion.
@@ -1052,7 +1054,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
         let add_fact delta (cl, args) = addVarConCt delta y cl args
         delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x)
         -- Do the same for negative info
-        let add_refut delta nalt = MaybeT (addRefutableAltCon delta y nalt)
+        let add_refut delta nalt = addVarNotConCt delta y nalt
         delta_neg <- foldlM add_refut delta_pos (vi_neg vi_x)
         -- vi_cache will be updated in addRefutableAltCon, so we are good to
         -- go!
@@ -1223,12 +1225,9 @@ we do the following:
 -- check if the @strict_arg_tys@ are actually all inhabited.
 -- Returns the old 'Delta' if all the types are non-void according to 'Delta'.
 tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck
-tysAreNonVoid rec_env strict_arg_tys = SC $ \delta -> do
-  all_non_void <- checkAllNonVoid rec_env delta strict_arg_tys
+tysAreNonVoid rec_env strict_arg_tys = SC $ \theta -> do
   -- Check if each strict argument type is inhabitable
-  pure $ if all_non_void
-            then Just delta
-            else Nothing
+  filterThetaM (\delta -> checkAllNonVoid rec_env delta strict_arg_tys) theta
 
 -- | Implements two performance optimizations, as described in
 -- @Note [Strict argument type constraints]@.
@@ -1281,7 +1280,7 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
       (InhabitationCandidate{ ic_tm_cs          = new_tm_cs
                             , ic_ty_cs          = new_ty_cs
                             , ic_strict_arg_tys = new_strict_arg_tys }) =
-        fmap isJust $ runSatisfiabilityCheck amb_cs $ mconcat
+        fmap (not . isEmptyTheta) $ runSatisfiabilityCheck (unitTheta amb_cs) $ mconcat
           [ tyIsSatisfiable False new_ty_cs
           , tmIsSatisfiable new_tm_cs
           , tysAreNonVoid rec_ts new_strict_arg_tys
@@ -1434,14 +1433,20 @@ on a list of strict argument types, we filter out all of the DI ones.
 --------------------------------------------
 -- * Providing positive evidence for a Delta
 
--- | @provideEvidence vs n delta@ returns a list of
--- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate
--- @vs@ to compatible constructor applications or wildcards.
--- Negative information is only retained if literals are involved or when
--- for recursive GADTs.
-provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
-provideEvidence = go
+-- | @provideEvidence vs n theta@ returns a list of
+-- at most @n@ (but perhaps empty) concrete refinements of @delta@ that
+-- instantiate @vs@ to compatible constructor applications or wildcards.
+-- Negative information is only retained if literals are involved.
+provideEvidence :: [Id] -> Int -> Theta -> DsM [Delta]
+provideEvidence = go_theta
   where
+    go_theta _  0 _                       = pure []
+    go_theta _  _ EmptyTheta              = pure []
+    go_theta xs n (ConsTheta delta theta) = do
+      ev_front <- go xs n delta
+      ev_back  <- go_theta xs (n - length ev_front) theta
+      pure (ev_front ++ ev_back)
+
     go _      0 _     = pure []
     go []     _ delta = pure [delta]
     go (x:xs) n delta = do
@@ -1506,7 +1511,7 @@ provideEvidence = go
           (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
+          theta <- pmIsSatisfiable (unitTheta delta) new_tm_cs new_ty_cs strict_arg_tys
           tracePm "instantiate_cons" (vcat [ ppr x
                                            , ppr (idType x)
                                            , ppr ty
@@ -1516,14 +1521,17 @@ provideEvidence = go
                                            , ppr new_ty_cs
                                            , ppr strict_arg_tys
                                            , ppr delta
-                                           , ppr mb_delta
+                                           , ppr theta
                                            , ppr n ])
-          con_deltas <- case mb_delta of
-            Nothing     -> pure []
+          con_deltas <- case theta of
+            EmptyTheta -> pure []
             -- NB: We don't prepend arg_vars as we don't have any evidence on
             -- them and we only want to split once on a data type. They are
             -- inhabited, otherwise pmIsSatisfiable would have refuted.
-            Just delta' -> go xs n delta'
+            ConsTheta delta' EmptyTheta -> go xs n delta'
+            -- pmIsSatisfiable will only thin out Theta. We supplied it a Theta
+            -- of length one, so this case can't happen.
+            _                           -> pprPanic "instantiate_cons" (ppr theta)
           other_cons_deltas <- instantiate_cons x ty xs (n - length con_deltas) delta cls
           pure (con_deltas ++ other_cons_deltas)
 
@@ -1554,8 +1562,8 @@ representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e = d
 -- type PmM a = StateT Delta (MaybeT DsM) a
 
 -- | Records that a variable @x@ is equal to a 'CoreExpr' @e@.
-addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta)
-addVarCoreCt delta x e = runMaybeT (execStateT (core_expr x e) delta)
+addVarCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
+addVarCoreCt delta x e = execStateT (core_expr x e) delta
   where
     -- | Takes apart a 'CoreExpr' and tries to extract as much information about
     -- literals and constructor applications as possible.
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index 10f172a430..697e1caf38 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -5,6 +5,7 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be>
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TupleSections #-}
 
 -- | Types used through-out pattern match checking. This module is mostly there
@@ -29,7 +30,9 @@ module GHC.HsToCore.PmCheck.Types (
         setIndirectSDIE, setEntrySDIE, traverseSDIE,
 
         -- * The pattern match oracle
-        VarInfo(..), TmState(..), TyState(..), Delta(..), initDelta
+        VarInfo(..), TmState(..), TyState(..), Delta(..),
+        Theta(EmptyTheta), pattern ConsTheta, emptyTheta, unitTheta, unionTheta,
+        isEmptyTheta, sizeTheta, bindTheta, liftDeltaM, filterThetaM, initTheta
     ) where
 
 #include "HsVersions.h"
@@ -64,6 +67,7 @@ import Numeric (fromRat)
 import Data.Foldable (find)
 import qualified Data.List.NonEmpty as NonEmpty
 import Data.Ratio
+import qualified Data.Semigroup as Semigroup
 
 -- | Literals (simple and overloaded ones) for pattern match checking.
 --
@@ -527,8 +531,8 @@ data Delta = MkDelta { delta_ty_st :: TyState    -- Type oracle; things like a~I
                      , delta_tm_st :: TmState }  -- Term oracle; things like x~Nothing
 
 -- | An initial delta that is always satisfiable
-initDelta :: Delta
-initDelta = MkDelta initTyState initTmState
+trueDelta :: Delta
+trueDelta = MkDelta initTyState initTmState
 
 instance Outputable Delta where
   ppr delta = vcat [
@@ -537,3 +541,76 @@ instance Outputable Delta where
       ppr (delta_tm_st delta),
       ppr (delta_ty_st delta)
     ]
+
+data Theta = EmptyTheta
+           | UnitTheta !Delta
+           | UnionTheta !Theta !Theta
+
+emptyTheta :: Theta
+emptyTheta = EmptyTheta
+
+unitTheta :: Delta -> Theta
+unitTheta = UnitTheta
+
+unionTheta :: Theta -> Theta -> Theta
+unionTheta EmptyTheta t          = t
+unionTheta t          EmptyTheta = t
+unionTheta t1         t2         = UnionTheta t1 t2
+
+unconsTheta :: Theta -> Maybe (Delta, Theta)
+unconsTheta EmptyTheta         = Nothing
+unconsTheta (UnitTheta delta)  = Just (delta, EmptyTheta)
+unconsTheta (UnionTheta t1 t2)
+  | Just (delta, t1') <- unconsTheta t1 = Just (delta, unionTheta t1' t2)
+  | otherwise                           = unconsTheta t2
+
+isEmptyTheta :: Theta -> Bool
+isEmptyTheta EmptyTheta = True
+isEmptyTheta _          = False
+
+thetaDeltas :: Theta -> [Delta]
+thetaDeltas = go []
+  where
+    go acc EmptyTheta         = acc
+    go acc (UnitTheta d)      = d:acc
+    go acc (UnionTheta t1 t2) = go (go acc t2) t1
+
+sizeTheta :: Theta -> Int
+sizeTheta = length . thetaDeltas
+
+pattern ConsTheta :: Delta -> Theta -> Theta
+pattern ConsTheta d th <- (unconsTheta -> Just (d, th))
+  where
+    ConsTheta d th = unitTheta d `unionTheta` th
+
+{-# COMPLETE EmptyTheta, ConsTheta #-}
+
+-- | An initial theta that is always satisfiable
+initTheta :: Theta
+initTheta = unitTheta trueDelta
+
+bindTheta :: Monad m => (Delta -> m Theta) -> Theta -> m Theta
+bindTheta f = go
+  where
+    go EmptyTheta         = pure EmptyTheta
+    go (UnitTheta delta)  = f delta
+    go (UnionTheta t1 t2) = unionTheta <$> go t1 <*> go t2
+
+liftDeltaM :: Monad m => (Delta -> m (Maybe Delta)) -> Theta -> m Theta
+liftDeltaM f = bindTheta (fmap (maybe emptyTheta unitTheta) . f)
+
+filterThetaM :: Monad m => (Delta -> m Bool) -> Theta -> m Theta
+filterThetaM f = bindTheta go
+  where
+    go delta = do
+      b <- f delta
+      pure $ if b then emptyTheta else unitTheta delta
+
+instance Semigroup Theta where
+  (<>) = unionTheta
+
+instance Monoid Theta where
+  mempty = emptyTheta
+
+instance Outputable Theta where
+  ppr = braces . fsep . punctuate comma . map ppr . thetaDeltas
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot b/compiler/GHC/HsToCore/PmCheck/Types.hs-boot
index beef421d46..fcf8f9abc4 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs-boot
@@ -2,6 +2,6 @@ module GHC.HsToCore.PmCheck.Types where
 
 import GhcPrelude ()
 
-data Delta
+data Theta
 
-initDelta :: Delta
+initTheta :: Theta
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 5090bc8d81..6ab1475287 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -30,7 +30,7 @@ module DsMonad (
         DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv,
 
         -- Getting and setting pattern match oracle states
-        getPmDelta, updPmDelta,
+        getPmTheta, updPmDelta,
 
         -- Get COMPLETE sets of a TyCon
         dsGetCompleteMatches,
@@ -282,7 +282,7 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var
                            }
         lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv
                            , dsl_loc     = real_span
-                           , dsl_delta   = initDelta
+                           , dsl_theta   = initTheta
                            }
     in (gbl_env, lcl_env)
 
@@ -381,14 +381,14 @@ the @SrcSpan@ being carried around.
 getGhcModeDs :: DsM GhcMode
 getGhcModeDs =  getDynFlags >>= return . ghcMode
 
--- | Get the current pattern match oracle state. See 'dsl_delta'.
-getPmDelta :: DsM Delta
-getPmDelta = do { env <- getLclEnv; return (dsl_delta env) }
+-- | Get the current pattern match oracle state. See 'dsl_theta'.
+getPmTheta :: DsM Theta
+getPmTheta = do { env <- getLclEnv; return (dsl_theta 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 })
+-- See 'dsl_theta'.
+updPmDelta :: Theta -> DsM a -> DsM a
+updPmDelta theta = updLclEnv (\env -> env { dsl_theta = theta })
 
 getSrcSpanDs :: DsM SrcSpan
 getSrcSpanDs = do { env <- getLclEnv
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 8fa12b28b1..3b8ffe696b 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -99,7 +99,7 @@ import TcOrigin
 import Annotations
 import InstEnv
 import FamInstEnv
-import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Delta)
+import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Theta)
 import IOEnv
 import RdrName
 import Name
@@ -319,9 +319,9 @@ data DsLclEnv = DsLclEnv {
         dsl_loc     :: RealSrcSpan,      -- To put in pattern-matching error msgs
 
         -- See Note [Note [Type and Term Equality Propagation] in Check.hs
-        -- The oracle state Delta is augmented as we walk inwards,
+        -- The oracle state Theta is augmented as we walk inwards,
         -- through each pattern match in turn
-        dsl_delta   :: Delta
+        dsl_theta   :: Theta
      }
 
 -- Inside [| |] brackets, the desugarer looks