TmOracle: Replace negative term equalities by refutable PmAltCons

The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".

This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.

So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.

This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.

See the Note [Refutable shapes] in TmOracle for a place to start.

Metric Decrease:
    T11195

15 files changed, 672 insertions, 550 deletions

diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs
index 632ea7742e..0b1cf435bc 100644
--- a/compiler/basicTypes/NameEnv.hs
+++ b/compiler/basicTypes/NameEnv.hs
@@ -25,6 +25,7 @@ module NameEnv (
 
         emptyDNameEnv,
         lookupDNameEnv,
+        delFromDNameEnv,
         mapDNameEnv,
         alterDNameEnv,
         -- ** Dependency analysis
@@ -147,6 +148,9 @@ emptyDNameEnv = emptyUDFM
 lookupDNameEnv :: DNameEnv a -> Name -> Maybe a
 lookupDNameEnv = lookupUDFM
 
+delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a
+delFromDNameEnv = delFromUDFM
+
 mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
 mapDNameEnv = mapUDFM
 
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 4a27d485c0..4147a78ad2 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -25,6 +25,7 @@ module Check (
 import GhcPrelude
 
 import TmOracle
+import PmPpr
 import Unify( tcMatchTy )
 import DynFlags
 import HsSyn
@@ -579,7 +580,7 @@ pmTopNormaliseType_maybe env ty_cs typ
 pmInitialTmTyCs :: PmM Delta
 pmInitialTmTyCs = do
   ty_cs  <- liftD getDictsDs
-  tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
+  tm_cs  <- bagToList <$> liftD getTmCsDs
   sat_ty <- tyOracle ty_cs
   let initTyCs = if sat_ty then ty_cs else emptyBag
       initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -627,7 +628,7 @@ that we expect.
 pmIsSatisfiable
   :: Delta     -- ^ The ambient term and type constraints
                --   (known to be satisfiable).
-  -> ComplexEq -- ^ The new term constraint.
+  -> TmVarCt      -- ^ The new term constraint.
   -> Bag EvVar -- ^ The new type constraints.
   -> [Type]    -- ^ The strict argument types.
   -> PmM (Maybe Delta)
@@ -653,7 +654,7 @@ pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do
 tmTyCsAreSatisfiable
   :: Delta     -- ^ The ambient term and type constraints
                --   (known to be satisfiable).
-  -> ComplexEq -- ^ The new term constraint.
+  -> TmVarCt      -- ^ The new term constraint.
   -> Bag EvVar -- ^ The new type constraints.
   -> PmM (Maybe Delta)
        -- ^ @'Just' delta@ if the constraints (@delta@) are
@@ -1463,7 +1464,7 @@ pmPatType PmFake = pmPatType truePattern
 data InhabitationCandidate =
   InhabitationCandidate
   { ic_val_abs        :: ValAbs
-  , ic_tm_ct          :: ComplexEq
+  , ic_tm_ct          :: TmVarCt
   , ic_ty_cs          :: Bag EvVar
   , ic_strict_arg_tys :: [Type]
   }
@@ -1660,7 +1661,7 @@ mkOneConFull x con = do
       strict_arg_tys = filterByList arg_is_banged arg_tys'
   return $ InhabitationCandidate
            { ic_val_abs        = con_abs
-           , ic_tm_ct          = (PmExprVar (idName x), vaToPmExpr con_abs)
+           , ic_tm_ct          = TVC x (vaToPmExpr con_abs)
            , ic_ty_cs          = listToBag evvars
            , ic_strict_arg_tys = strict_arg_tys
            }
@@ -1678,21 +1679,15 @@ mkGuard pv e = do
      | PmExprOther {} <- expr -> pure PmFake
      | otherwise              -> pure (PmGrd pv expr)
 
--- | Create a term equality of the form: `(False ~ (x ~ lit))`
-mkNegEq :: Id -> PmLit -> ComplexEq
-mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
-{-# INLINE mkNegEq #-}
-
 -- | Create a term equality of the form: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> ComplexEq
-mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
+mkPosEq :: Id -> PmLit -> TmVarCt
+mkPosEq x l = TVC x (PmExprLit l)
 {-# INLINE mkPosEq #-}
 
 -- | Create a term equality of the form: `(x ~ x)`
 -- (always discharged by the term oracle)
-mkIdEq :: Id -> ComplexEq
-mkIdEq x = (PmExprVar name, PmExprVar name)
-  where name = idName x
+mkIdEq :: Id -> TmVarCt
+mkIdEq x = TVC x (PmExprVar (idName x))
 {-# INLINE mkIdEq #-}
 
 -- | Generate a variable pattern of a given type
@@ -2059,8 +2054,7 @@ pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
 
 -- Var
 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
-  | Just tm_state <- solveOneEq (delta_tm_cs delta)
-                                (PmExprVar (idName x), vaToPmExpr va)
+  | Just tm_state <- solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va))
   = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
   | otherwise = return mempty
 
@@ -2122,7 +2116,8 @@ pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
                              ValVec vva (delta {delta_tm_cs = tm_state})
           Nothing       -> return mempty
   where
-    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+    -- See Note [Refutable shapes] in TmOracle
+    us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
        = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
        | otherwise = []
 
@@ -2142,7 +2137,8 @@ pmcheckHd (p@(PmLit l)) ps guards
                 (ValVec vva (delta { delta_tm_cs = tm_state }))
   | otherwise = return non_matched
   where
-    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+    -- See Note [Refutable shapes] in TmOracle
+    us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
        = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
        | otherwise = []
 
@@ -2407,22 +2403,22 @@ these constraints.
 genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
              -> [Pat GhcTc]           -- LHS       (should have length 1)
              -> [Id]                  -- MatchVars (should have length 1)
-             -> DsM (Bag SimpleEq)
+             -> DsM (Bag TmVarCt)
 genCaseTmCs2 Nothing _ _ = return emptyBag
 genCaseTmCs2 (Just scr) [p] [var] = do
   fam_insts <- dsGetFamInstEnvs
   [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
   let scr_e = lhsExprToPmExpr scr
-  return $ listToBag [(var, e), (var, scr_e)]
+  return $ listToBag [(TVC var e), (TVC var scr_e)]
 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
 
 -- | Generate a simple equality when checking a case expression:
 --     case x of { matches }
 -- When checking matches we record that (x ~ y) where y is the initial
 -- uncovered. All matches will have to satisfy this equality.
-genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
+genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmVarCt
 genCaseTmCs1 Nothing     _    = emptyBag
-genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
+genCaseTmCs1 (Just scr) [var] = unitBag (TVC var (lhsExprToPmExpr scr))
 genCaseTmCs1 _ _              = panic "genCaseTmCs1: HsCase"
 
 {- Note [Literals in PmPat]
@@ -2484,21 +2480,15 @@ isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
 
 instance Outputable ValVec where
   ppr (ValVec vva delta)
-    = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
-          vector                = substInValAbs subst vva
-      in  ppr_uncovered (vector, residual_eqs)
+    = let (subst, refuts) = wrapUpTmState (delta_tm_cs delta)
+          vector          = substInValAbs subst vva
+      in  pprUncovered (vector, refuts)
 
 -- | Apply a term substitution to a value vector abstraction. All VAs are
 -- transformed to PmExpr (used only before pretty printing).
-substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
+substInValAbs :: TmVarCtEnv -> [ValAbs] -> [PmExpr]
 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
 
--- | Wrap up the term oracle's state once solving is complete. Drop any
--- information about unhandled constraints (involving HsExprs) and flatten
--- (height 1) the substitution.
-wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
-wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
-
 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
@@ -2538,10 +2528,11 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
     maxPatterns = maxUncoveredPatterns dflags
 
     -- Print a single clause (for redundant/with-inaccessible-rhs)
-    pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
+    pprEqn q txt = pprContext True ctx (text txt) $ \f ->
+      f (pprPats kind (map unLoc q))
 
     -- Print several clauses (for uncovered clauses)
-    pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+    pprEqns qs = pprContext False ctx (text "are non-exhaustive") $ \_ ->
       case qs of -- See #11245
            [ValVec [] _]
                     -> text "Guards do not cover entire pattern space"
@@ -2552,7 +2543,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
 
     -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
     -- which we only know the type and have no inhabitants at hand)
-    warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+    warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ ->
       hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
 
 {- Note [Inaccessible warnings for record updates]
@@ -2624,8 +2615,8 @@ exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete pat
                                        -- incomplete
 
 -- True <==> singular
-pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
+pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
   = vcat [text txt <+> msg,
           sep [ text "In" <+> ppr_match <> char ':'
               , nest 4 (rest_of_msg_fun pref)]]
@@ -2639,87 +2630,10 @@ pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
                   -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
              _    -> (pprMatchContext kind, \ pp -> pp)
 
-ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
-ppr_pats kind pats
+pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
+pprPats kind pats
   = sep [sep (map ppr pats), matchSeparator kind, text "..."]
 
-ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
-ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
-
-ppr_constraint :: (SDoc,[PmLit]) -> SDoc
-ppr_constraint (var, lits) = var <+> text "is not one of"
-                                 <+> braces (pprWithCommas ppr lits)
-
-ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
-ppr_uncovered (expr_vec, complex)
-  | null cs   = fsep vec -- there are no literal constraints
-  | otherwise = hang (fsep vec) 4 $
-                  text "where" <+> vcat (map ppr_constraint cs)
-  where
-    sdoc_vec = mapM pprPmExprWithParens expr_vec
-    (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
-
-{- Note [Representation of Term Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In the paper, term constraints always take the form (x ~ e). Of course, a more
-general constraint of the form (e1 ~ e1) can always be transformed to an
-equivalent set of the former constraints, by introducing a fresh, intermediate
-variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
-to #11160 (incredibly bad performance for literal pattern matching). Two are
-the main sources of this problem (the actual problem is how these two interact
-with each other):
-
-1. Pattern matching on literals generates twice as many constraints as needed.
-   Consider the following (tests/ghci/should_run/ghcirun004):
-
-    foo :: Int -> Int
-    foo 1    = 0
-    ...
-    foo 5000 = 4999
-
-   The covered and uncovered set *should* look like:
-     U0 = { x |> {} }
-
-     C1  = { 1  |> { x ~ 1 } }
-     U1  = { x  |> { False ~ (x ~ 1) } }
-     ...
-     C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
-     U10 = { x  |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
-     ...
-
-     If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
-     we get twice as many constraints. Also note that half of them are just the
-     substitution [x |-> False].
-
-2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
-   (x ~ e) as substitutions [x |-> e]. More specifically, function
-   `extendSubstAndSolve` applies such substitutions in the residual constraints
-   and partitions them in the affected and non-affected ones, which are the new
-   worklist. Essentially, this gives quadradic behaviour on the number of the
-   residual constraints. (This would not be the case if the term oracle used
-   mutable variables but, since we use it to handle disjunctions on value set
-   abstractions (`Union` case), we chose a pure, incremental interface).
-
-Now the problem becomes apparent (e.g. for clause 300):
-  * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
-    constraints that we know that will not reduce (stay in the worklist).
-  * To check for consistency, we apply the substituting constraints ONE BY ONE
-    (since `tmOracle` is called incrementally, it does not have all of them
-    available at once). Hence, we go through the (non-progressing) constraints
-    over and over, achieving over-quadradic behaviour.
-
-If instead we allow constraints of the form (e ~ e),
-  * All uncovered sets Ui contain no substituting constraints and i
-    non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
-    behaves linearly.
-  * All covered sets Ci contain exactly (i-1) non-progressing constraints and
-    a single substituting constraint. So the term oracle goes through the
-    constraints only once.
-
-The performance improvement becomes even more important when more arguments are
-involved.
--}
-
 -- Debugging Infrastructre
 
 tracePm :: String -> SDoc -> PmM ()
@@ -2757,3 +2671,5 @@ pprValAbs ps = hang (text "ValAbs:") 2
 pprValVecDebug :: ValVec -> SDoc
 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
                                   parens (pprValAbs vas)
+                                  -- <not a haddock> $$ ppr (delta_tm_cs _d)
+                                  -- <not a haddock> $$ ppr (delta_ty_cs _d)
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 8e3021fd8a..9534b4e20b 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -396,11 +396,11 @@ addDictsDs ev_vars
   = updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
 
 -- | Get in-scope term constraints (pm check)
-getTmCsDs :: DsM (Bag SimpleEq)
+getTmCsDs :: DsM (Bag TmVarCt)
 getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
 
 -- | Add in-scope term constraints (pm check)
-addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
+addTmCsDs :: Bag TmVarCt -> DsM a -> DsM a
 addTmCsDs tm_cs
   = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
 
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs
index bd0e12e850..3697dd8cc1 100644
--- a/compiler/deSugar/PmExpr.hs
+++ b/compiler/deSugar/PmExpr.hs
@@ -6,12 +6,11 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 module PmExpr (
-        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
-        truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
-        lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
-        pprPmExprWithParens, runPmPprM
+        PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..),
+        eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
     ) where
 
 #include "HsVersions.h"
@@ -23,19 +22,14 @@ import FastString (FastString, unpackFS)
 import HsSyn
 import Id
 import Name
-import NameSet
 import DataCon
 import ConLike
+import TcEvidence (isErasableHsWrapper)
 import TcType (isStringTy)
 import TysWiredIn
 import Outputable
-import Util
 import SrcLoc
 
-import Data.Maybe (mapMaybe)
-import Data.List (groupBy, sortBy, nubBy)
-import Control.Monad.Trans.State.Lazy
-
 {-
 %************************************************************************
 %*                                                                      *
@@ -61,7 +55,6 @@ refer to variables that are otherwise substituted away.
 data PmExpr = PmExprVar   Name
             | PmExprCon   ConLike [PmExpr]
             | PmExprLit   PmLit
-            | PmExprEq    PmExpr PmExpr  -- Syntactic equality
             | PmExprOther (HsExpr GhcTc)  -- Note [PmExprOther in PmExpr]
 
 
@@ -79,6 +72,16 @@ eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
   -- See Note [Undecidable Equality for Overloaded Literals]
 eqPmLit _              _              = False
 
+-- | Represents a match against a literal. We mostly use it to to encode shapes
+-- for a variable that immediately lead to a refutation.
+--
+-- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'.
+newtype PmAltCon = PmAltLit PmLit
+  deriving Outputable
+
+instance Eq PmAltCon where
+  PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+
 {- Note [Undecidable Equality for Overloaded Literals]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Equality on overloaded literals is undecidable in the general case. Consider
@@ -145,24 +148,11 @@ impact of this is the following:
        appearance of the warnings and is, in practice safe.
 -}
 
-nubPmLit :: [PmLit] -> [PmLit]
-nubPmLit = nubBy eqPmLit
+-- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@.
+data TmVarCt = TVC !Id !PmExpr
 
--- | Term equalities
-type SimpleEq  = (Id, PmExpr) -- We always use this orientation
-type ComplexEq = (PmExpr, PmExpr)
-
--- | Lift a `SimpleEq` to a `ComplexEq`
-toComplex :: SimpleEq -> ComplexEq
-toComplex (x,e) = (PmExprVar (idName x), e)
-
--- | Expression `True'
-truePmExpr :: PmExpr
-truePmExpr = mkPmExprData trueDataCon []
-
--- | Expression `False'
-falsePmExpr :: PmExpr
-falsePmExpr = mkPmExprData falseDataCon []
+instance Outputable TmVarCt where
+  ppr (TVC x e) = ppr x <+> char '~' <+> ppr e
 
 -- ----------------------------------------------------------------------------
 -- ** Predicates on PmExpr
@@ -172,66 +162,6 @@ isNotPmExprOther :: PmExpr -> Bool
 isNotPmExprOther (PmExprOther _) = False
 isNotPmExprOther _expr           = True
 
--- | Check whether a literal is negated
-isNegatedPmLit :: PmLit -> Bool
-isNegatedPmLit (PmOLit b _) = b
-isNegatedPmLit _other_lit   = False
-
--- | Check whether a PmExpr is syntactically equal to term `True'.
-isTruePmExpr :: PmExpr -> Bool
-isTruePmExpr (PmExprCon c []) = c == RealDataCon trueDataCon
-isTruePmExpr _other_expr      = False
-
--- | Check whether a PmExpr is syntactically equal to term `False'.
-isFalsePmExpr :: PmExpr -> Bool
-isFalsePmExpr (PmExprCon c []) = c == RealDataCon falseDataCon
-isFalsePmExpr _other_expr      = False
-
--- | Check whether a PmExpr is syntactically e
-isNilPmExpr :: PmExpr -> Bool
-isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
-isNilPmExpr _other_expr     = False
-
--- | Check whether a PmExpr is syntactically equal to (x == y).
--- Since (==) is overloaded and can have an arbitrary implementation, we use
--- the PmExprEq constructor to represent only equalities with non-overloaded
--- literals where it coincides with a syntactic equality check.
-isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
-isPmExprEq (PmExprEq e1 e2) = Just (e1,e2)
-isPmExprEq _other_expr      = Nothing
-
--- | Check if a DataCon is (:).
-isConsDataCon :: DataCon -> Bool
-isConsDataCon con = consDataCon == con
-
--- ----------------------------------------------------------------------------
--- ** Substitution in PmExpr
-
--- | We return a boolean along with the expression. Hence, if substitution was
--- a no-op, we know that the expression still cannot progress.
-substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
-substPmExpr x e1 e =
-  case e of
-    PmExprVar z | x == z    -> (e1, True)
-                | otherwise -> (e, False)
-    PmExprCon c ps -> let (ps', bs) = mapAndUnzip (substPmExpr x e1) ps
-                      in  (PmExprCon c ps', or bs)
-    PmExprEq ex ey -> let (ex', bx) = substPmExpr x e1 ex
-                          (ey', by) = substPmExpr x e1 ey
-                      in  (PmExprEq ex' ey', bx || by)
-    _other_expr    -> (e, False) -- The rest are terminals (We silently ignore
-                                 -- Other). See Note [PmExprOther in PmExpr]
-
--- | Substitute in a complex equality. We return (Left eq) if the substitution
--- affected the equality or (Right eq) if nothing happened.
-substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
-substComplexEq x e (ex, ey)
-  | bx || by  = Left  (ex', ey')
-  | otherwise = Right (ex', ey')
-  where
-    (ex', bx) = substPmExpr x e ex
-    (ey', by) = substPmExpr x e ey
-
 -- -----------------------------------------------------------------------
 -- ** Lift source expressions (HsExpr Id) to PmExpr
 
@@ -240,8 +170,20 @@ lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e
 
 hsExprToPmExpr :: HsExpr GhcTc -> PmExpr
 
+-- Translating HsVar to flexible meta variables in the unification problem is
+-- morally wrong, but it does the right thing for now.
+-- In contrast to the situation in pattern matches, HsVars in expression syntax
+-- are object language variables, most similar to rigid variables with an
+-- unknown solution. The correct way would be to handle them through PmExprOther
+-- and identify syntactically equal occurrences by the same rigid meta variable,
+-- but we can't compare the wrapped HsExpr for equality. Hence we are stuck with
+-- this hack.
 hsExprToPmExpr (HsVar        _ x) = PmExprVar (idName (unLoc x))
-hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c)
+
+-- Translating HsConLikeOut to a flexible meta variable is misleading.
+-- For an example why, consider `consAreRigid` in
+-- `testsuite/tests/pmcheck/should_compile/PmExprVars.hs`.
+-- hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c)
 
 -- Desugar literal strings as a list of characters. For other literal values,
 -- keep it as it is.
@@ -294,7 +236,12 @@ hsExprToPmExpr (HsTickPragma _ _ _ _ e) = lhsExprToPmExpr e
 hsExprToPmExpr (HsSCC          _ _ _ e) = lhsExprToPmExpr e
 hsExprToPmExpr (HsCoreAnn      _ _ _ e) = lhsExprToPmExpr e
 hsExprToPmExpr (ExprWithTySig    _ e _) = lhsExprToPmExpr e
-hsExprToPmExpr (HsWrap           _ _ e) =  hsExprToPmExpr e
+hsExprToPmExpr (HsWrap           _ w e)
+  -- A dictionary application spoils e and we have no choice but to return an
+  -- PmExprOther. Same thing for other stuff that can't erased in the
+  -- compilation process. Otherwise this bites in
+  -- teststuite/tests/pmcheck/should_compile/PmExprVars.hs.
+  | isErasableHsWrapper w = hsExprToPmExpr e
 hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle
 
 stringExprToList :: SourceText -> FastString -> PmExpr
@@ -312,155 +259,22 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
 %************************************************************************
 -}
 
-{- 1. Literals
-~~~~~~~~~~~~~~
-Starting with a function definition like:
-
-    f :: Int -> Bool
-    f 5 = True
-    f 6 = True
-
-The uncovered set looks like:
-    { var |> False == (var == 5), False == (var == 6) }
-
-Yet, we would like to print this nicely as follows:
-   x , where x not one of {5,6}
-
-Function `filterComplex' takes the set of residual constraints and packs
-together the negative constraints that refer to the same variable so we can do
-just this. Since these variables will be shown to the programmer, we also give
-them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.
-
-2. Residual Constraints
-~~~~~~~~~~~~~~~~~~~~~~~
-Unhandled constraints that refer to HsExpr are typically ignored by the solver
-(it does not even substitute in HsExpr so they are even printed as wildcards).
-Additionally, the oracle returns a substitution if it succeeds so we apply this
-substitution to the vectors before printing them out (see function `pprOne' in
-Check.hs) to be more precice.
--}
-
--- -----------------------------------------------------------------------------
--- ** Transform residual constraints in appropriate form for pretty printing
-
-type PmNegLitCt = (Name, (SDoc, [PmLit]))
-
-filterComplex :: [ComplexEq] -> [PmNegLitCt]
-filterComplex = zipWith rename nameList . map mkGroup
-              . groupBy name . sortBy order . mapMaybe isNegLitCs
-  where
-    order x y = compare (fst x) (fst y)
-    name  x y = fst x == fst y
-    mkGroup l = (fst (head l), nubPmLit $ map snd l)
-    rename new (old, lits) = (old, (new, lits))
-
-    isNegLitCs (e1,e2)
-      | isFalsePmExpr e1, Just (x,y) <- isPmExprEq e2 = isNegLitCs' x y
-      | isFalsePmExpr e2, Just (x,y) <- isPmExprEq e1 = isNegLitCs' x y
-      | otherwise = Nothing
-
-    isNegLitCs' (PmExprVar x) (PmExprLit l) = Just (x, l)
-    isNegLitCs' (PmExprLit l) (PmExprVar x) = Just (x, l)
-    isNegLitCs' _ _             = Nothing
-
-    -- Try nice names p,q,r,s,t before using the (ugly) t_i
-    nameList :: [SDoc]
-    nameList = map text ["p","q","r","s","t"] ++
-                 [ text ('t':show u) | u <- [(0 :: Int)..] ]
-
--- ----------------------------------------------------------------------------
-
-runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
-runPmPprM m lit_env = (result, mapMaybe is_used lit_env)
-  where
-    (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
-
-    is_used (x,(name, lits))
-      | elemNameSet x used = Just (name, lits)
-      | otherwise         = Nothing
-
-type PmPprM a = State ([PmNegLitCt], NameSet) a
--- (the first part of the state is read only. make it a reader?)
-
-addUsed :: Name -> PmPprM ()
-addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
-
-checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
-checkNegation x = do
-  negated <- gets fst
-  return $ case lookup x negated of
-    Just (new, _) -> Just new
-    Nothing       -> Nothing
-
--- | Pretty print a pmexpr, but remember to prettify the names of the variables
--- that refer to neg-literals. The ones that cannot be shown are printed as
--- underscores.
-pprPmExpr :: PmExpr -> PmPprM SDoc
-pprPmExpr (PmExprVar x) = do
-  mb_name <- checkNegation x
-  case mb_name of
-    Just name -> addUsed x >> return name
-    Nothing   -> return underscore
-
-pprPmExpr (PmExprCon con args) = pprPmExprCon con args
-pprPmExpr (PmExprLit l)        = return (ppr l)
-pprPmExpr (PmExprEq _ _)       = return underscore -- don't show
-pprPmExpr (PmExprOther _)      = return underscore -- don't show
-
-needsParens :: PmExpr -> Bool
-needsParens (PmExprVar   {}) = False
-needsParens (PmExprLit    l) = isNegatedPmLit l
-needsParens (PmExprEq    {}) = False -- will become a wildcard
-needsParens (PmExprOther {}) = False -- will become a wildcard
-needsParens (PmExprCon (RealDataCon c) es)
-  | isTupleDataCon c
-  || isConsDataCon c || null es = False
-  | otherwise                   = True
-needsParens (PmExprCon (PatSynCon _) es) = not (null es)
-
-pprPmExprWithParens :: PmExpr -> PmPprM SDoc
-pprPmExprWithParens expr
-  | needsParens expr = parens <$> pprPmExpr expr
-  | otherwise        =            pprPmExpr expr
-
-pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
-pprPmExprCon (RealDataCon con) args
-  | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
-  | isConsDataCon con  = pretty_list
-  where
-    mkTuple :: [SDoc] -> SDoc
-    mkTuple = parens     . fsep . punctuate comma
-
-    -- lazily, to be used in the list case only
-    pretty_list :: PmPprM SDoc
-    pretty_list = case isNilPmExpr (last list) of
-      True  -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
-      False -> parens   . hcat . punctuate colon <$> mapM pprPmExpr list
-
-    list = list_elements args
-
-    list_elements [x,y]
-      | PmExprCon c es <- y,  RealDataCon nilDataCon == c
-          = ASSERT(null es) [x,y]
-      | PmExprCon c es <- y, RealDataCon consDataCon == c
-          = x : list_elements es
-      | otherwise = [x,y]
-    list_elements list  = pprPanic "list_elements:" (ppr list)
-pprPmExprCon cl args
-  | conLikeIsInfix cl = case args of
-      [x, y] -> do x' <- pprPmExprWithParens x
-                   y' <- pprPmExprWithParens y
-                   return (x' <+> ppr cl <+> y')
-      -- can it be infix but have more than two arguments?
-      list   -> pprPanic "pprPmExprCon:" (ppr list)
-  | null args = return (ppr cl)
-  | otherwise = do args' <- mapM pprPmExprWithParens args
-                   return (fsep (ppr cl : args'))
-
 instance Outputable PmLit where
   ppr (PmSLit     l) = pmPprHsLit l
   ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
 
--- not really useful for pmexprs per se
 instance Outputable PmExpr where
-  ppr e = fst $ runPmPprM (pprPmExpr e) []
+  ppr = go (0 :: Int)
+    where
+      go _    (PmExprLit l)       = ppr l
+      go _    (PmExprVar v)       = ppr v
+      go _    (PmExprOther e)     = angleBrackets (ppr e)
+      go _    (PmExprCon (RealDataCon dc) args)
+        | isTupleDataCon dc = parens $ comma_sep $ map ppr args
+        | dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args)
+        where
+          comma_sep = fsep . punctuate comma
+          list_cells (hd:tl) = hd : list_cells tl
+          list_cells _       = []
+      go prec (PmExprCon cl args)
+        = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args))
diff --git a/compiler/deSugar/PmPpr.hs b/compiler/deSugar/PmPpr.hs
new file mode 100644
index 0000000000..06b60a6806
--- /dev/null
+++ b/compiler/deSugar/PmPpr.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE CPP #-}
+
+-- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for
+-- user facing pattern match warnings.
+module PmPpr (
+        pprUncovered
+    ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import Name
+import NameEnv
+import NameSet
+import UniqDFM
+import UniqSet
+import ConLike
+import DataCon
+import TysWiredIn
+import Outputable
+import Control.Monad.Trans.State.Strict
+import Maybes
+import Util
+
+import TmOracle
+
+-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
+-- components and refutable shapes associated to any mentioned variables.
+--
+-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]]):
+--
+-- @
+-- (Just p) q
+--     where p is not one of {3, 4}
+--           q is not one of {0, 5}
+-- @
+pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc
+pprUncovered (expr_vec, refuts)
+  | null cs   = fsep vec -- there are no literal constraints
+  | otherwise = hang (fsep vec) 4 $
+                  text "where" <+> vcat (map pprRefutableShapes cs)
+  where
+    sdoc_vec = mapM pprPmExprWithParens expr_vec
+    (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts)
+
+-- | Output refutable shapes of a variable in the form of @var is not one of {2,
+-- Nothing, 3}@.
+pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
+pprRefutableShapes (var, alts)
+  = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
+  where
+    ppr_alt (PmAltLit lit)      = ppr lit
+
+{- 1. Literals
+~~~~~~~~~~~~~~
+Starting with a function definition like:
+
+    f :: Int -> Bool
+    f 5 = True
+    f 6 = True
+
+The uncovered set looks like:
+    { var |> var /= 5, var /= 6 }
+
+Yet, we would like to print this nicely as follows:
+   x , where x not one of {5,6}
+
+Since these variables will be shown to the programmer, we give them better names
+(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'.
+
+2. Residual Constraints
+~~~~~~~~~~~~~~~~~~~~~~~
+Unhandled constraints that refer to HsExpr are typically ignored by the solver
+(it does not even substitute in HsExpr so they are even printed as wildcards).
+Additionally, the oracle returns a substitution if it succeeds so we apply this
+substitution to the vectors before printing them out (see function `pprOne' in
+Check.hs) to be more precise.
+-}
+
+-- | A 'PmRefutEnv' with pretty names for the occuring variables.
+type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon])
+
+-- | Assigns pretty names to constraint variables in the domain of the given
+-- 'PmRefutEnv'.
+prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv
+prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList
+  where
+    rename new (old, lits) = (old, (new, lits))
+    -- Try nice names p,q,r,s,t before using the (ugly) t_i
+    nameList :: [SDoc]
+    nameList = map text ["p","q","r","s","t"] ++
+                 [ text ('t':show u) | u <- [(0 :: Int)..] ]
+
+type PmPprM a = State (PrettyPmRefutEnv, NameSet) a
+-- (the first part of the state is read only. make it a reader?)
+
+runPmPpr :: PmPprM a -> PrettyPmRefutEnv -> (a, [(SDoc,[PmAltCon])])
+runPmPpr m lit_env = (result, mapMaybe is_used (udfmToList lit_env))
+  where
+    (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
+
+    is_used (k,v)
+      | elemUniqSet_Directly k used = Just v
+      | otherwise                   = Nothing
+
+addUsed :: Name -> PmPprM ()
+addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
+
+checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
+checkNegation x = do
+  negated <- gets fst
+  return $ case lookupDNameEnv negated x of
+    Just (new, _) -> Just new
+    Nothing       -> Nothing
+
+-- | Pretty print a pmexpr, but remember to prettify the names of the variables
+-- that refer to neg-literals. The ones that cannot be shown are printed as
+-- underscores.
+pprPmExpr :: PmExpr -> PmPprM SDoc
+pprPmExpr (PmExprVar x) = do
+  mb_name <- checkNegation x
+  case mb_name of
+    Just name -> addUsed x >> return name
+    Nothing   -> return underscore
+pprPmExpr (PmExprCon con args) = pprPmExprCon con args
+pprPmExpr (PmExprLit l)        = return (ppr l)
+pprPmExpr (PmExprOther _)      = return underscore -- don't show
+
+needsParens :: PmExpr -> Bool
+needsParens (PmExprVar   {}) = False
+needsParens (PmExprLit    l) = isNegatedPmLit l
+needsParens (PmExprOther {}) = False -- will become a wildcard
+needsParens (PmExprCon (RealDataCon c) es)
+  | isTupleDataCon c
+  || isConsDataCon c || null es = False
+  | otherwise                   = True
+needsParens (PmExprCon (PatSynCon _) es) = not (null es)
+
+pprPmExprWithParens :: PmExpr -> PmPprM SDoc
+pprPmExprWithParens expr
+  | needsParens expr = parens <$> pprPmExpr expr
+  | otherwise        =            pprPmExpr expr
+
+pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
+pprPmExprCon (RealDataCon con) args
+  | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
+  | isConsDataCon con  = pretty_list
+  where
+    mkTuple :: [SDoc] -> SDoc
+    mkTuple = parens     . fsep . punctuate comma
+
+    -- lazily, to be used in the list case only
+    pretty_list :: PmPprM SDoc
+    pretty_list = case isNilPmExpr (last list) of
+      True  -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
+      False -> parens   . hcat . punctuate colon <$> mapM pprPmExpr list
+
+    list = list_elements args
+
+    list_elements [x,y]
+      | PmExprCon c es <- y,  RealDataCon nilDataCon == c
+          = ASSERT(null es) [x,y]
+      | PmExprCon c es <- y, RealDataCon consDataCon == c
+          = x : list_elements es
+      | otherwise = [x,y]
+    list_elements list  = pprPanic "list_elements:" (ppr list)
+pprPmExprCon cl args
+  | conLikeIsInfix cl = case args of
+      [x, y] -> do x' <- pprPmExprWithParens x
+                   y' <- pprPmExprWithParens y
+                   return (x' <+> ppr cl <+> y')
+      -- can it be infix but have more than two arguments?
+      list   -> pprPanic "pprPmExprCon:" (ppr list)
+  | null args = return (ppr cl)
+  | otherwise = do args' <- mapM pprPmExprWithParens args
+                   return (fsep (ppr cl : args'))
+
+-- | Check whether a literal is negated
+isNegatedPmLit :: PmLit -> Bool
+isNegatedPmLit (PmOLit b _) = b
+isNegatedPmLit _other_lit   = False
+
+-- | Check whether a PmExpr is syntactically e
+isNilPmExpr :: PmExpr -> Bool
+isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
+isNilPmExpr _other_expr     = False
+
+-- | Check if a DataCon is (:).
+isConsDataCon :: DataCon -> Bool
+isConsDataCon con = consDataCon == con
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 87e5f0a268..db3ce6d770 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -1,23 +1,27 @@
 {-
 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
-
-The term equality oracle. The main export of the module is function `tmOracle'.
 -}
 
 {-# LANGUAGE CPP, MultiWayIf #-}
 
+-- | The term equality oracle. The main export of the module are the functions
+-- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'.
+--
+-- If you are looking for an oracle that can solve type-level constraints, look
+-- at 'TcSimplify.tcCheckSatisfiability'.
 module TmOracle (
 
         -- re-exported from PmExpr
-        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
-        eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
-        hsExprToPmExpr, pprPmExprWithParens,
+        PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv,
+        PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
 
         -- the term oracle
-        tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
+        tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
+        extendSubst, canDiverge, isRigid,
+        addSolveRefutableAltCon, lookupRefutableAltCons,
 
         -- misc.
-        toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
+        exprDeepLookup, pmLitType
     ) where
 
 #include "HsVersions.h"
@@ -26,16 +30,19 @@ import GhcPrelude
 
 import PmExpr
 
+import Util
 import Id
 import Name
 import Type
 import HsLit
 import TcHsSyn
 import MonadUtils
-import Util
+import ListSetOps (insertNoDup, unionLists)
+import Maybes
 import Outputable
-
 import NameEnv
+import UniqFM
+import UniqDFM
 
 {-
 %************************************************************************
@@ -45,202 +52,261 @@ import NameEnv
 %************************************************************************
 -}
 
--- | The type of substitutions.
-type PmVarEnv = NameEnv PmExpr
+-- | Pretty much a @['TmVarCt']@ association list where the domain is 'Name'
+-- instead of 'Id'. This is the type of 'tm_pos', where we store solutions for
+-- rigid pattern match variables.
+type TmVarCtEnv = NameEnv PmExpr
+
+-- | An environment assigning shapes to variables that immediately lead to a
+-- refutation. So, if this maps @x :-> [3]@, then trying to solve a 'TmVarCt'
+-- like @x ~ 3@ immediately leads to a contradiction.
+-- Determinism is important since we use this for warning messages in
+-- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain
+-- 'NameEnv'.
+--
+-- See also Note [Refutable shapes] in TmOracle.
+type PmRefutEnv = DNameEnv [PmAltCon]
+
+-- | The state of the term oracle. Tracks all term-level facts of the form "x is
+-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
+--
+-- Subject to Note [The Pos/Neg invariant].
+data TmState = TmS
+  { tm_pos :: !TmVarCtEnv
+  -- ^ A substitution with solutions we extend with every step and return as a
+  -- result. The substitution is in /triangular form/: It might map @x@ to @y@
+  -- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup
+  -- non-idempotent. This means that 'varDeepLookup' potentially has to walk
+  -- along a chain of var-to-var mappings until we find the solution but has the
+  -- advantage that when we update the solution for @y@ above, we automatically
+  -- update the solution for @x@ in a union-find-like fashion.
+  -- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs
+  -- ('PmExprLit', 'PmExprCon'). Ergo, never maps to a 'PmExprOther'.
+  , tm_neg :: !PmRefutEnv
+  -- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
+  -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal
+  -- 3 or 4. Should we later solve @x@ to a variable @y@
+  -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of
+  -- @y@. See also Note [The Pos/Neg invariant].
+  }
+
+{- Note [The Pos/Neg invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint.
+
+For example, it would make no sense to say both
+    tm_pos = [...x :-> 3 ...]
+    tm_neg = [...x :-> [4,42]... ]
+The positive information is strictly more informative than the negative.
+
+Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must
+delete any binding for @x@ from 'tm_neg', to uphold the invariant.
+
+But there is more! Suppose we are adding @x :-> y@ to 'tm_pos', and 'tm_neg'
+contains @x :-> cs, y :-> ds@. Then we want to update 'tm_neg' to
+@y :-> (cs ++ ds)@, to make use of the negative information we have about @x@.
+-}
+
+instance Outputable TmState where
+  ppr state = braces (fsep (punctuate comma (pos ++ neg)))
+    where
+      pos   = map pos_eq (nonDetUFMToList (tm_pos state))
+      neg   = map neg_eq (udfmToList (tm_neg state))
+      pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
+      neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r
+
+-- | Initial state of the oracle.
+initialTmState :: TmState
+initialTmState = TmS emptyNameEnv emptyDNameEnv
+
+-- | Wrap up the term oracle's state once solving is complete. Return the
+-- flattened 'tm_pos' and 'tm_neg'.
+wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv)
+wrapUpTmState solver_state
+  = (flattenTmVarCtEnv (tm_pos solver_state), tm_neg solver_state)
 
--- | The environment of the oracle contains
---     1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
---     2. A substitution we extend with every step and return as a result.
-type TmOracleEnv = (Bool, PmVarEnv)
+-- | Flatten the triangular subsitution.
+flattenTmVarCtEnv :: TmVarCtEnv -> TmVarCtEnv
+flattenTmVarCtEnv env = mapNameEnv (exprDeepLookup env) env
 
 -- | Check whether a constraint (x ~ BOT) can succeed,
 -- given the resulting state of the term oracle.
 canDiverge :: Name -> TmState -> Bool
-canDiverge x (standby, (_unhandled, env))
+canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
   -- If the variable seems not evaluated, there is a possibility for
-  -- constraint x ~ BOT to be satisfiable.
-  | PmExprVar y <- varDeepLookup env x -- seems not forced
-  -- If it is involved (directly or indirectly) in any equality in the
-  -- worklist, we can assume that it is already indirectly evaluated,
-  -- as a side-effect of equality checking. If not, then we can assume
-  -- that the constraint is satisfiable.
-  = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
-  -- Variable x is already in WHNF so the constraint is non-satisfiable
+  -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found
+  -- a solution (i.e. some equivalent literal or constructor) for it yet.
+  | (_, PmExprVar y) <- varDeepLookup pos x -- seems not forced
+  -- Even if we don't have a solution yet, it might be involved in a negative
+  -- constraint, in which case we must already have evaluated it earlier.
+  , Nothing <- lookupDNameEnv neg y
+  = True
+  -- Variable x is already in WHNF or we know some refutable shape, so the
+  -- constraint is non-satisfiable
   | otherwise = False
 
-  where
-    isForcedByEq :: Name -> ComplexEq -> Bool
-    isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
-
--- | Check whether a variable is in the free variables of an expression
-varIn :: Name -> PmExpr -> Bool
-varIn x e = case e of
-  PmExprVar y    -> x == y
-  PmExprCon _ es -> any (x `varIn`) es
-  PmExprLit _    -> False
-  PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
-  PmExprOther _  -> False
-
--- | Flatten the DAG (Could be improved in terms of performance.).
-flattenPmVarEnv :: PmVarEnv -> PmVarEnv
-flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
-
--- | The state of the term oracle (includes complex constraints that cannot
--- progress unless we get more information).
-type TmState = ([ComplexEq], TmOracleEnv)
-
--- | Initial state of the oracle.
-initialTmState :: TmState
-initialTmState = ([], (False, emptyNameEnv))
-
--- | Solve a complex equality (top-level).
-solveOneEq :: TmState -> ComplexEq -> Maybe TmState
-solveOneEq solver_env@(_,(_,env)) complex
-  = solveComplexEq solver_env -- do the actual *merging* with existing state
-  $ simplifyComplexEq               -- simplify as much as you can
-  $ applySubstComplexEq env complex -- replace everything we already know
-
--- | Solve a complex equality.
--- Nothing => definitely unsatisfiable
--- Just tms => I have added the complex equality and added
---             it to the tmstate; the result may or may not be
---             satisfiable
-solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that
+-- @x@ and @e@ are completely substituted before!
+isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
+isRefutable x e env
+  = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+
+-- | Solve an equality (top-level).
+solveOneEq :: TmState -> TmVarCt -> Maybe TmState
+solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e)
+
+exprToAlt :: PmExpr -> Maybe PmAltCon
+exprToAlt (PmExprLit l)    = Just (PmAltLit l)
+exprToAlt _                = Nothing
+
+-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
+-- 'TmState' and return @Nothing@ if that leads to a contradiction.
+addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+addSolveRefutableAltCon original@TmS{ tm_pos = pos, tm_neg = neg } x nalt
+  = case exprToAlt e of
+      -- We have to take care to preserve Note [The Pos/Neg invariant]
+      Nothing         -> Just extended -- Not solved yet
+      Just alt                         -- We have a solution
+        | alt == nalt -> Nothing       -- ... which is contradictory
+        | otherwise   -> Just original -- ... which is compatible, rendering the
+  where                                --     refutation redundant
+    (y, e) = varDeepLookup pos (idName x)
+    extended = original { tm_neg = neg' }
+    neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y
+
+-- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter
+-- intends to provide a suitable interface for 'alterDNameEnv'.
+delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a]
+delNulls f mb_entry
+  | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret
+  | otherwise                              = Nothing
+
+-- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e.
+-- would immediately lead to a refutation by the term oracle.
+lookupRefutableAltCons :: Id -> TmState -> [PmAltCon]
+lookupRefutableAltCons x TmS { tm_neg = neg }
+  = fromMaybe [] (lookupDNameEnv neg (idName x))
+
+-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
+-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
+-- semantically helpful alias for 'lookupNameEnv'.
+isRigid :: TmState -> Name -> Maybe PmExpr
+isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x
+
+-- | @isFlexible tms = isNothing . 'isRigid' tms@
+isFlexible :: TmState -> Name -> Bool
+isFlexible tms = isNothing . isRigid tms
+
+-- | Try to unify two 'PmExpr's and record the gained knowledge in the
+-- 'TmState'.
+--
+-- Returns @Nothing@ when there's a contradiction. Returns @Just tms@
+-- when the constraint was compatible with prior facts, in which case @tms@ has
+-- integrated the knowledge from the equality constraint.
+unify :: TmState -> (PmExpr, PmExpr) -> Maybe TmState
+unify tms eq@(e1, e2) = case eq of
   -- We cannot do a thing about these cases
-  (PmExprOther _,_)            -> Just (standby, (True, env))
-  (_,PmExprOther _)            -> Just (standby, (True, env))
+  (PmExprOther _,_)            -> boring
+  (_,PmExprOther _)            -> boring
 
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
     -- See Note [Undecidable Equality for Overloaded Literals]
-    True  -> Just solver_state
-    False -> Nothing
+    True  -> boring
+    False -> unsat
 
   (PmExprCon c1 ts1, PmExprCon c2 ts2)
-    | c1 == c2  -> foldlM solveComplexEq solver_state (zip ts1 ts2)
-    | otherwise -> Nothing
-  (PmExprCon _ [], PmExprEq t1 t2)
-    | isTruePmExpr e1  -> solveComplexEq solver_state (t1, t2)
-    | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
-  (PmExprEq t1 t2, PmExprCon _ [])
-    | isTruePmExpr e2   -> solveComplexEq solver_state (t1, t2)
-    | isFalsePmExpr e2  -> Just (eq:standby, (unhandled, env))
+    | c1 == c2  -> foldlM unify tms (zip ts1 ts2)
+    | otherwise -> unsat
 
   (PmExprVar x, PmExprVar y)
-    | x == y    -> Just solver_state
-    | otherwise -> extendSubstAndSolve x e2 solver_state
-
-  (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
-  (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
-
-  (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
-
-  _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
-       Just (standby, (True, env)) -- I HATE CATCH-ALLS
-
--- | Extend the substitution and solve the (possibly updated) constraints.
-extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
-extendSubstAndSolve x e (standby, (unhandled, env))
-  = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
+    | x == y    -> boring
+
+  -- It's important to handle both rigid cases first, otherwise we get cyclic
+  -- substitutions. Cf. 'extendSubstAndSolve' and
+  -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@.
+  (PmExprVar x, _)
+    | Just e1' <- isRigid tms x -> unify tms (e1', e2)
+  (_, PmExprVar y)
+    | Just e2' <- isRigid tms y -> unify tms (e1, e2')
+  (PmExprVar x, PmExprVar y)    -> Just (equate x y tms)
+  (PmExprVar x, _)              -> trySolve x e2 tms
+  (_, PmExprVar y)              -> trySolve y e1 tms
+
+  _ -> WARN( True, text "unify: Catch all" <+> ppr eq)
+       boring -- I HATE CATCH-ALLS
+  where
+    boring    = Just tms
+    unsat     = Nothing
+
+-- | Merges the equivalence classes of @x@ and @y@ by extending the substitution
+-- with @x :-> y@.
+-- Preconditions: @x /= y@ and both @x@ and @y@ are flexible (cf.
+-- 'isFlexible'/'isRigid').
+equate :: Name -> Name -> TmState -> TmState
+equate x y tms@TmS{ tm_pos = pos, tm_neg = neg }
+  = ASSERT( x /= y )
+    ASSERT( isFlexible tms x )
+    ASSERT( isFlexible tms y )
+    tms'
   where
-    -- Apply the substitution to the worklist and partition them to the ones
-    -- that had some progress and the rest. Then, recurse over the ones that
-    -- had some progress. Careful about performance:
-    -- See Note [Representation of Term Equalities] in deSugar/Check.hs
-    (changed, unchanged) = partitionWith (substComplexEq x e) standby
-    new_incr_state       = (unchanged, (unhandled, extendNameEnv env x e))
+    pos' = extendNameEnv pos x (PmExprVar y)
+    -- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts
+    -- of x into those of y
+    nalts = fromMaybe [] (lookupDNameEnv neg x)
+    neg'  = alterDNameEnv (delNulls (unionLists nalts)) neg y
+              `delFromDNameEnv` x
+    tms'  = TmS { tm_pos = pos', tm_neg = neg' }
+
+-- | Extend the substitution with a mapping @x: -> e@ if compatible with
+-- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise.
+--
+-- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid').
+-- Precondition: @e@ is a 'PmExprCon' or 'PmExprLit'
+trySolve:: Name -> PmExpr -> TmState -> Maybe TmState
+trySolve x e _tms@TmS{ tm_pos = pos, tm_neg = neg }
+  | ASSERT( isFlexible _tms x )
+    ASSERT( _is_whnf e )
+    isRefutable x e neg
+  = Nothing
+  | otherwise
+  = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x))
+  where
+    _is_whnf PmExprCon{} = True
+    _is_whnf PmExprLit{} = True
+    _is_whnf _           = False
 
 -- | When we know that a variable is fresh, we do not actually have to
 -- check whether anything changes, we know that nothing does. Hence,
--- `extendSubst` simply extends the substitution, unlike what
--- `extendSubstAndSolve` does.
+-- @extendSubst@ simply extends the substitution, unlike what
+-- 'extendSubstAndSolve' does.
 extendSubst :: Id -> PmExpr -> TmState -> TmState
-extendSubst y e (standby, (unhandled, env))
+extendSubst y e solver_state@TmS{ tm_pos = pos }
   | isNotPmExprOther simpl_e
-  = (standby, (unhandled, extendNameEnv env x simpl_e))
-  | otherwise = (standby, (True, env))
+  = solver_state { tm_pos = extendNameEnv pos x simpl_e }
+  | otherwise = solver_state
   where
     x = idName y
-    simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
-
--- | Simplify a complex equality.
-simplifyComplexEq :: ComplexEq -> ComplexEq
-simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
-
--- | Simplify an expression. The boolean indicates if there has been any
--- simplification or if the operation was a no-op.
-simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyPmExpr e = case e of
-  PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
-                      (ts', bs) -> (PmExprCon c ts', or bs)
-  PmExprEq t1 t2 -> simplifyEqExpr t1 t2
-  _other_expr    -> (e, False) -- the others are terminals
-
--- | Simplify an equality expression. The equality is given in parts.
-simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyEqExpr e1 e2 = case (e1, e2) of
-  -- Varables
-  (PmExprVar x, PmExprVar y)
-    | x == y -> (truePmExpr, True)
-
-  -- Literals
-  (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-    -- See Note [Undecidable Equality for Overloaded Literals]
-    True  -> (truePmExpr,  True)
-    False -> (falsePmExpr, True)
-
-  -- Can potentially be simplified
-  (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
-    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
-    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
-    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-  (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
-    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
-    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
-    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-
-  -- Constructors
-  (PmExprCon c1 ts1, PmExprCon c2 ts2)
-    | c1 == c2 ->
-        let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
-            (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
-            (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
-            worst_case  = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
-        in  if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
-               | all isTruePmExpr  tss  -> (truePmExpr, True)
-               | any isFalsePmExpr tss  -> (falsePmExpr, True)
-               | otherwise              -> (worst_case, False)
-    | otherwise -> (falsePmExpr, True)
-
-  -- We cannot do anything about the rest..
-  _other_equality -> (original, False)
-
-  where
-    original = PmExprEq e1 e2 -- reconstruct equality
-
--- | Apply an (un-flattened) substitution to a simple equality.
-applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
-applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
-
--- | Apply an (un-flattened) substitution to a variable.
-varDeepLookup :: PmVarEnv -> Name -> PmExpr
-varDeepLookup env x
-  | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
-  | otherwise                  = PmExprVar x          -- terminal
+    simpl_e = exprDeepLookup pos e
+
+-- | Apply an (un-flattened) substitution to a variable and return its
+-- representative in the triangular substitution @env@ and the completely
+-- substituted expression. The latter may just be the representative wrapped
+-- with 'PmExprVar' if we haven't found a solution for it yet.
+varDeepLookup :: TmVarCtEnv -> Name -> (Name, PmExpr)
+varDeepLookup env x = case lookupNameEnv env x of
+  Just (PmExprVar y) -> varDeepLookup env y
+  Just e             -> (x, exprDeepLookup env e) -- go deeper
+  Nothing            -> (x, PmExprVar x)          -- terminal
 {-# INLINE varDeepLookup #-}
 
 -- | Apply an (un-flattened) substitution to an expression.
-exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
-exprDeepLookup env (PmExprVar x)    = varDeepLookup env x
+exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr
+exprDeepLookup env (PmExprVar x)    = snd (varDeepLookup env x)
 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
-                                               (exprDeepLookup env e2)
 exprDeepLookup _   other_expr       = other_expr -- PmExprLit, PmExprOther
 
 -- | External interface to the term oracle.
-tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
+tmOracle :: TmState -> [TmVarCt] -> Maybe TmState
 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
 
 -- | Type of a PmLit
@@ -248,18 +314,49 @@ pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
 pmLitType (PmSLit   lit) = hsLitType   lit
 pmLitType (PmOLit _ lit) = overLitType lit
 
-{- Note [Deep equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Solving nested equalities is the most difficult part. The general strategy
-is the following:
+{- Note [Refutable shapes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider a pattern match like
+
+    foo x
+      | 0 <- x = 42
+      | 0 <- x = 43
+      | 1 <- x = 44
+      | otherwise = 45
+
+This will result in the following initial matching problem:
+
+    PatVec: x     (0 <- x)
+    ValVec: $tm_y
+
+Where the first line is the pattern vector and the second line is the value
+vector abstraction. When we handle the first pattern guard in Check, it will be
+desugared to a match of the form
+
+    PatVec: x     0
+    ValVec: $tm_y x
+
+In LitVar, this will split the value vector abstraction for `x` into a positive
+`PmLit 0` and a negative `PmLit x [0]` value abstraction. While the former is
+immediately matched against the pattern vector, the latter (vector value
+abstraction `~[0] $tm_y`) is completely uncovered by the clause.
+
+`pmcheck` proceeds by *discarding* the the value vector abstraction involving
+the guard to accomodate for the desugaring. But this also discards the valuable
+information that `x` certainly is not the literal 0! Consequently, we wouldn't
+be able to report the second clause as redundant.
 
-  * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
-    (e1 ~ e2) and then treated recursively.
+That's a typical example of why we need the term oracle, and in this specific
+case, the ability to encode that `x` certainly is not the literal 0. Now the
+term oracle can immediately refute the constraint `x ~ 0` generated by the
+second clause and report the clause as redundant. After the third clause, the
+set of such *refutable* literals is again extended to `[0, 1]`.
 
-  * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
-    we know more about the inner equality (e1 ~ e2). That's exactly what
-    `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
-    truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
-    that it is not e but rather e', since it may perform some
-    simplifications deeper.
+In general, we want to store a set of refutable shapes (`PmAltCon`) for each
+variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will
+add such a refutable mapping to the `PmRefutEnv` in the term oracles state and
+check if causes any immediate contradiction. Whenever we record a solution in
+the substitution via `extendSubstAndSolve`, the refutable environment is checked
+for any matching refutable `PmAltCon`.
 -}
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index e2d789b172..e8e6bf7317 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -327,6 +327,7 @@ Library
         MkCore
         PprCore
         PmExpr
+        PmPpr
         TmOracle
         Check
         Coverage
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 72aed23505..eb65d1e093 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -8,7 +8,8 @@ module TcEvidence (
   HsWrapper(..),
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
   mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
-  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
+  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, isErasableHsWrapper,
+  pprHsWrapper,
 
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
@@ -355,6 +356,21 @@ isIdHsWrapper :: HsWrapper -> Bool
 isIdHsWrapper WpHole = True
 isIdHsWrapper _      = False
 
+-- | Is the wrapper erasable, i.e., will not affect runtime semantics?
+isErasableHsWrapper :: HsWrapper -> Bool
+isErasableHsWrapper = go
+  where
+    go WpHole                  = True
+    go (WpCompose wrap1 wrap2) = go wrap1 && go wrap2
+    -- not so sure about WpFun. But it eta-expands, so...
+    go WpFun{}                 = False
+    go WpCast{}                = True
+    go WpEvLam{}               = False -- case in point
+    go WpEvApp{}               = False
+    go WpTyLam{}               = True
+    go WpTyApp{}               = True
+    go WpLet{}                 = False
+
 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/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index bc307568f8..8957014036 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -391,7 +391,7 @@ data DsLclEnv = DsLclEnv {
         -- These two fields are augmented as we walk inwards,
         -- through each patttern match in turn
         dsl_dicts   :: Bag EvVar,     -- Constraints from GADT pattern-matching
-        dsl_tm_cs   :: Bag SimpleEq,  -- Constraints form term-level pattern matching
+        dsl_tm_cs   :: Bag TmVarCt,      -- Constraints form term-level pattern matching
 
         dsl_pm_iter :: IORef Int  -- Number of iterations for pmcheck so far
                                   -- We fail if this gets too big
@@ -1020,7 +1020,7 @@ splice. In particular it is not set when the splice is renamed or typechecked.
 'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert
 the finalizer (see Note [Delaying modFinalizers in untyped splices]), and
 'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to
-set 'RunSplice' when renaming or typechecking the splice, where 'Splice', 
+set 'RunSplice' when renaming or typechecking the splice, where 'Splice',
 'Brack' or 'Comp' are used instead.
 
 -}
diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs
index 1a134d5dc8..8a6e07d84a 100644
--- a/compiler/utils/ListSetOps.hs
+++ b/compiler/utils/ListSetOps.hs
@@ -14,7 +14,7 @@ module ListSetOps (
         Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
 
         -- Duplicate handling
-        hasNoDups, removeDups, findDupsEq,
+        hasNoDups, removeDups, findDupsEq, insertNoDup,
         equivClasses,
 
         -- Indexing
@@ -169,3 +169,10 @@ findDupsEq _  [] = []
 findDupsEq eq (x:xs) | null eq_xs  = findDupsEq eq xs
                      | otherwise   = (x :| eq_xs) : findDupsEq eq neq_xs
     where (eq_xs, neq_xs) = partition (eq x) xs
+
+-- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
+-- when an equal element couldn't be found in @xs@.
+insertNoDup :: (Eq a) => a -> [a] -> [a]
+insertNoDup x set
+  | elem x set = set
+  | otherwise  = x:set
diff --git a/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
new file mode 100644
index 0000000000..fde022c5cb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
@@ -0,0 +1,15 @@
+-- | The following match demonstrates why we need to detect cyclic solutions
+-- when extending 'TmOracle.tm_pos'.
+--
+-- TLDR; solving @x :-> y@ where @x@ is the representative of @y@'s equivalence
+-- class can easily lead to a cycle in the substitution.
+module CyclicSubst where
+
+-- | The match is translated to @b | a <- b@, the initial unification variable
+-- is @a@ (for some reason). VarVar will assign @b :-> a@ in the match of @a@
+-- against @b@ (vars occuring in a pattern are flexible). The @PmGrd a b@ is
+-- desugared as a match of @$pm_x@ against @a@, where @$pm_x :-> b@, which is
+-- stored as @$pm_x :-> a@ due to the previous solution. Now, VarVar will
+-- assign @a :-> $pm_x@, causing a cycle.
+foo :: Int -> Int
+foo a@b = a + b
diff --git a/testsuite/tests/pmcheck/should_compile/PmExprVars.hs b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
new file mode 100644
index 0000000000..7b17cd5b66
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
@@ -0,0 +1,44 @@
+module PmExprVars where
+
+-- | Demonstrates why we can't lower constructors as flexible meta variables.
+-- If we did, we'd get a warning that cases 1 and 2 were redundant, implying
+-- cases 0 and 3 are not. Arguably this might be better than not warning at
+-- all, but it's very surprising having to supply the third case but not the
+-- first two cases. And it's probably buggy somwhere else. Delete this when we
+-- detect that all but the last case is redundant.
+consAreRigid :: Int
+consAreRigid = case False of
+  False -> case False of
+    False -> 0
+    True -> 1
+  True -> case False of
+    False -> 2
+    True -> 3
+
+data D a = A | B
+
+class C a where
+  d :: D a
+
+instance C Int where
+  d = A
+
+instance C Bool where
+  d = B
+
+-- | Demonstrates why we can't translate arbitrary 'HsVar'
+-- occurrences as 'PmExprVar's (i.e., meta variables). If we did, the following
+-- would warn that the cases 1 and 2 were redundant, which is clearly wrong
+-- (case 1 is the only match). This is an artifact of translating from the
+-- non-desugared 'HsExpr'. If we were to implement 'hsExprToPmExpr' in terms of
+-- 'CoreExpr', we'd see the dictionary application and all would be well. The
+-- solution is to look into the outer 'HsWrap' and determine whether we apply
+-- or abstract over any evidence variables.
+dictVarsAreTypeIndexed:: Int
+dictVarsAreTypeIndexed = case d :: D Int of
+  A -> case d :: D Bool of
+    A -> 0
+    B -> 1
+  B -> case d :: D Bool of
+    A -> 2
+    B -> 3
diff --git a/testsuite/tests/pmcheck/should_compile/T12949.hs b/testsuite/tests/pmcheck/should_compile/T12949.hs
new file mode 100644
index 0000000000..90fe024067
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T12949.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module T12949 where
+
+class Foo a where
+  foo :: Maybe a
+
+data Result a b = Neither | This a | That b | Both a b
+
+q :: forall a b . (Foo a, Foo b) => Result a b
+q = case foo :: Maybe a of
+      Nothing -> case foo :: Maybe b of
+                   Nothing -> Neither
+                   Just c -> That c
+      Just i -> case foo :: Maybe b of
+                   Nothing -> This i
+                   Just c -> Both i c
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index e04f2cf07c..5fe7d9edd1 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -94,8 +94,13 @@ test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T12949', [],  compile, ['-fwarn-overlapping-patterns'])
 test('T12957', [], compile, ['-fwarn-overlapping-patterns'])
 test('T12957a', [], compile, ['-fwarn-overlapping-patterns'])
+test('PmExprVars', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('CyclicSubst', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # EmptyCase
 test('T10746', [], compile,
diff --git a/testsuite/tests/typecheck/should_compile/T5490.stderr b/testsuite/tests/typecheck/should_compile/T5490.stderr
index 3cf5b3e866..93ae57550f 100644
--- a/testsuite/tests/typecheck/should_compile/T5490.stderr
+++ b/testsuite/tests/typecheck/should_compile/T5490.stderr
@@ -1,8 +1,4 @@
 
-T5490.hs:246:5: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In a case alternative: HDropZero -> ...
-
 T5490.hs:295:5: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In a case alternative: _ -> ...