diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index e87eb39d2603094d2ac8c1f720f4a9ef42d75dc8..e44e074e10d81e208883770e323d9d4de1d4995e 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -54,20 +54,19 @@ import TyCoRep
 import Type
 import UniqSupply
 import DsUtils       (isTrueLHsExpr)
-import Maybes        (expectJust)
+import Maybes        (MaybeT (..), expectJust)
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.List     (find)
 import Data.Maybe    (catMaybes, isJust, fromMaybe)
-import Control.Monad (forM, when, forM_, zipWithM, filterM)
+import Control.Monad (forM, foldM, when, guard, forM_, zipWithM, filterM)
+import Control.Monad.Trans.Class (lift)
 import Coercion
 import TcEvidence
 import TcSimplify    (tcNormalise)
 import IOEnv
 import qualified Data.Semigroup as Semi
 
-import ListT (ListT(..), fold, select)
-
 {-
 This module checks pattern matches for:
 \begin{enumerate}
@@ -90,55 +89,7 @@ The algorithm is based on the paper:
 %************************************************************************
 -}
 
--- We use the non-determinism monad to apply the algorithm to several
--- possible sets of constructors. Users can specify complete sets of
--- constructors by using COMPLETE pragmas.
--- The algorithm only picks out constructor
--- sets deep in the bowels which makes a simpler `mapM` more difficult to
--- implement. The non-determinism is only used in one place, see the ConVar
--- case in `pmCheckHd`.
-
-type PmM a = ListT DsM a
-
-liftD :: DsM a -> PmM a
-liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
-
--- Pick the first match complete covered match or otherwise the "best" match.
--- The best match is the one with the least uncovered clauses, ties broken
--- by the number of inaccessible clauses followed by number of redundant
--- clauses.
---
--- This is specified in the
--- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
--- users' guide. If you update the implementation of this function, make sure
--- to update that section of the users' guide as well.
-getResult :: PmM PmResult -> DsM PmResult
-getResult ls
-  = do { res <- fold ls goM (pure Nothing)
-       ; case res of
-            Nothing -> panic "getResult is empty"
-            Just a  -> return a }
-  where
-    goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
-    goM mpm dpm = do { pmr <- dpm
-                     ; return $ Just $ go pmr mpm }
-
-    -- Careful not to force unecessary results
-    go :: Maybe PmResult -> PmResult -> PmResult
-    go Nothing rs = rs
-    go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
-      | null us && null rs && null is = old
-      | otherwise =
-        let PmResult prov' rs' (UncoveredPatterns us') is' = new
-        in case compareLength us us'
-                `mappend` (compareLength is is')
-                `mappend` (compareLength rs rs')
-                `mappend` (compare prov prov') of
-              GT  -> new
-              EQ  -> new
-              LT  -> old
-    go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
-      = panic "getResult: No inhabitation candidates"
+type PmM = DsM
 
 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
 
@@ -156,6 +107,8 @@ data PmPat :: PatTy -> * where
   PmLit  :: { pm_lit_lit  :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
   PmNLit :: { pm_lit_id   :: Id
             , pm_lit_not  :: [PmLit] } -> PmPat 'VA
+  PmNCon :: { pm_con_id   :: Id
+            , pm_con_sets :: [[ConLike]] } -> PmPat 'VA
   PmGrd  :: { pm_grd_pv   :: PatVec
             , pm_grd_expr :: PmExpr } -> PmPat 'PAT
   -- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
@@ -340,8 +293,8 @@ uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
 -- | Check a single pattern binding (let)
 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
-  tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
-  mb_pm_res <- tryM (getResult (checkSingle' locn var p))
+  tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
+  mb_pm_res <- tryM (checkSingle' locn var p)
   case mb_pm_res of
     Left  _   -> warnPmIters dflags ctxt
     Right res -> dsPmWarn dflags ctxt res
@@ -349,14 +302,14 @@ checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
 -- | Check a single pattern binding (let)
 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
 checkSingle' locn var p = do
-  liftD resetPmIterDs -- set the iter-no to zero
-  fam_insts <- liftD dsGetFamInstEnvs
-  clause    <- liftD $ translatePat fam_insts p
+  resetPmIterDs -- set the iter-no to zero
+  fam_insts <- dsGetFamInstEnvs
+  clause    <- translatePat fam_insts p
   missing   <- mkInitialUncovered [var]
   tracePm "checkSingle': missing" (vcat (map pprValVecDebug missing))
                                   -- no guards
   PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
-  let us' = UncoveredPatterns us
+  us' <- UncoveredPatterns <$> normaliseUncovered us
   return $ case (cs,ds) of
     (Covered,  _    )         -> PmResult prov [] us' [] -- useful
     (NotCovered, NotDiverged) -> PmResult prov m  us' [] -- redundant
@@ -367,7 +320,7 @@ checkSingle' locn var p = do
 -- in @MultiIf@ expressions.
 checkGuardMatches :: HsMatchContext Name          -- Match context
                   -> GRHSs GhcTc (LHsExpr GhcTc)  -- Guarded RHSs
-                  -> DsM ()
+                  -> PmM ()
 checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
     dflags <- getDynFlags
     let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
@@ -382,14 +335,14 @@ checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
 
 -- | Check a matchgroup (case, functions, etc.)
 checkMatches :: DynFlags -> DsMatchContext
-             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
+             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM ()
 checkMatches dflags ctxt vars matches = do
-  tracePmD "checkMatches" (hang (vcat [ppr ctxt
+  tracePm "checkMatches" (hang (vcat [ppr ctxt
                                , ppr vars
                                , text "Matches:"])
                                2
                                (vcat (map ppr matches)))
-  mb_pm_res <- tryM $ getResult $ case matches of
+  mb_pm_res <- tryM $ case matches of
     -- Check EmptyCase separately
     -- See Note [Checking EmptyCase Expressions]
     [] | [var] <- vars -> checkEmptyCase' var
@@ -404,14 +357,15 @@ checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
 checkMatches' vars matches
   | null matches = panic "checkMatches': EmptyCase"
   | otherwise = do
-      liftD resetPmIterDs -- set the iter-no to zero
+      resetPmIterDs -- set the iter-no to zero
       missing    <- mkInitialUncovered vars
       tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
       (prov, rs,us,ds) <- go matches missing
+      us' <- normaliseUncovered us
       return $ PmResult {
                    pmresultProvenance   = prov
                  , pmresultRedundant    = map hsLMatchToLPats rs
-                 , pmresultUncovered    = UncoveredPatterns us
+                 , pmresultUncovered    = UncoveredPatterns us'
                  , pmresultInaccessible = map hsLMatchToLPats ds }
   where
     go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
@@ -422,8 +376,8 @@ checkMatches' vars matches
     go []     missing = return (mempty, [], missing, [])
     go (m:ms) missing = do
       tracePm "checkMatches': go" (ppr m $$ ppr missing)
-      fam_insts          <- liftD dsGetFamInstEnvs
-      (clause, guards)   <- liftD $ translateMatch fam_insts m
+      fam_insts          <- dsGetFamInstEnvs
+      (clause, guards)   <- translateMatch fam_insts m
       r@(PartialResult prov cs missing' ds)
         <- runMany (pmcheckI clause guards) missing
       tracePm "checkMatches': go: res" (ppr r)
@@ -514,7 +468,7 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
 -- is a type family with a variable result kind. I (Richard E) can't think
 -- of a way to cause trouble here, though.
 pmTopNormaliseType_maybe env ty_cs typ
-  = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
+  = do (_, mb_typ') <- initTcDsForSolver $ tcNormalise ty_cs typ
          -- Before proceeding, we chuck typ into the constraint solver, in case
          -- solving for given equalities may reduce typ some. See
          -- "Wrinkle: local equalities" in
@@ -577,8 +531,8 @@ pmTopNormaliseType_maybe env ty_cs typ
 -- for why this is done.)
 pmInitialTmTyCs :: PmM Delta
 pmInitialTmTyCs = do
-  ty_cs  <- liftD getDictsDs
-  tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
+  ty_cs  <- getDictsDs
+  tm_cs  <- map toComplex . bagToList <$> getTmCsDs
   sat_ty <- tyOracle ty_cs
   let initTyCs = if sat_ty then ty_cs else emptyBag
       initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -669,12 +623,32 @@ tmTyCsAreSatisfiable
                                                  , delta_tm_cs = term_cs }
            _unsat               -> Nothing
 
+-- | This kicks out patterns with 'PmNCon's where at least one COMPLETE set is
+-- rendered vacuous by equality constraints.
+normaliseUncovered :: Uncovered -> PmM Uncovered
+normaliseUncovered us = do
+  us' <- filterM valvec_inhabited us
+  -- TODO: We could first check for any obviously empty COMPLETE sets before
+  -- asking pmIsSatisfiable
+  tracePm "normaliseUncovered" (vcat (map pprValVecDebug us))
+  pure us'
+  where
+    allM p = foldM (\b a -> if b then p a else pure False) True
+    valvec_inhabited (ValVec vva delta) = allM (valabs_inhabited delta) vva
+    anyM p = foldM (\b a -> if b then pure True else p a) False
+    valabs_inhabited delta v = case v :: ValAbs of
+      PmNCon{} -> allM (anyM (con_inhabited delta (pm_con_id v))) (pm_con_sets v)
+      _ -> pure True
+    con_inhabited delta x con = do
+      ic <- mkOneConFull x con
+      isJust <$> pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+
 -- | Implements two performance optimizations, as described in the
 -- \"Strict argument type constraints\" section of
 -- @Note [Extensions to GADTs Meet Their Match]@.
 checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
 checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
-  fam_insts <- liftD dsGetFamInstEnvs
+  fam_insts <- dsGetFamInstEnvs
   let definitely_inhabited =
         definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
   tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
@@ -831,7 +805,7 @@ equalities (such as i ~ Int) that may be in scope.
 inhabitationCandidates :: Bag EvVar -> Type
                        -> PmM (Either Type (TyCon, [InhabitationCandidate]))
 inhabitationCandidates ty_cs ty = do
-  fam_insts   <- liftD dsGetFamInstEnvs
+  fam_insts   <- dsGetFamInstEnvs
   mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
   case mb_norm_res of
     Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
@@ -855,7 +829,7 @@ inhabitationCandidates ty_cs ty = do
         |  tc `elem` trivially_inhabited
         -> case dcs of
              []    -> return (Left src_ty)
-             (_:_) -> do var <- liftD $ mkPmId core_ty
+             (_:_) -> do var <- mkPmId core_ty
                          let va = build_tm (PmVar var) dcs
                          return $ Right (tc, [InhabitationCandidate
                            { ic_val_abs = va, ic_tm_ct = mkIdEq var
@@ -865,7 +839,7 @@ inhabitationCandidates ty_cs ty = do
            -- Don't consider abstract tycons since we don't know what their
            -- constructors are, which makes the results of coverage checking
            -- them extremely misleading.
-        -> liftD $ do
+        -> do
              var  <- mkPmId core_ty -- it would be wrong to unify x
              alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
              return $ Right
@@ -931,7 +905,7 @@ truePattern = nullaryConPattern (RealDataCon trueDataCon)
 {-# INLINE truePattern #-}
 
 -- | Generate a `canFail` pattern vector of a specific type
-mkCanFailPmPat :: Type -> DsM PatVec
+mkCanFailPmPat :: Type -> PmM PatVec
 mkCanFailPmPat ty = do
   var <- mkPmVar ty
   return [var, PmFake]
@@ -966,7 +940,7 @@ mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
 -- -----------------------------------------------------------------------
 -- * Transform (Pat Id) into of (PmPat Id)
 
-translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
+translatePat :: FamInstEnvs -> Pat GhcTc -> PmM PatVec
 translatePat fam_insts pat = case pat of
   WildPat  ty  -> mkPmVars [ty]
   VarPat _ id  -> return [PmVar (unLoc id)]
@@ -1178,12 +1152,12 @@ from translation in pattern matcher.
 
 -- | Translate a list of patterns (Note: each pattern is translated
 -- to a pattern vector but we do not concatenate the results).
-translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
+translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> PmM [PatVec]
 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
 
 -- | Translate a constructor pattern
 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
-                   -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
+                   -> ConLike -> HsConPatDetails GhcTc -> PmM PatVec
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
   = concat <$> translatePatVec fam_insts (map unLoc ps)
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
@@ -1239,7 +1213,7 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
 
 -- Translate a single match
 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
-               -> DsM (PatVec,[PatVec])
+               -> PmM (PatVec,[PatVec])
 translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) =
   do
   pats'   <- concat <$> translatePatVec fam_insts pats
@@ -1258,11 +1232,11 @@ translateMatch _ _ = panic "translateMatch"
 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
 
 -- | Translate a list of guard statements to a pattern vector
-translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
+translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> PmM PatVec
 translateGuards fam_insts guards = do
   all_guards <- concat <$> mapM (translateGuard fam_insts) guards
   let
-    shouldKeep :: Pattern -> DsM Bool
+    shouldKeep :: Pattern -> PmM Bool
     shouldKeep p
       | PmVar {} <- p = pure True
       | PmCon {} <- p = (&&)
@@ -1287,7 +1261,7 @@ translateGuards fam_insts guards = do
       pure (PmFake : kept)
 
 -- | Check whether a pattern can fail to match
-cantFailPattern :: Pattern -> DsM Bool
+cantFailPattern :: Pattern -> PmM Bool
 cantFailPattern PmVar {}      = pure True
 cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
   = (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
@@ -1295,7 +1269,7 @@ cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
 cantFailPattern _             = pure False
 
 -- | Translate a guard statement to Pattern
-translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
+translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> PmM PatVec
 translateGuard fam_insts guard = case guard of
   BodyStmt _   e _ _ -> translateBoolGuard e
   LetStmt  _   binds -> translateLet (unLoc binds)
@@ -1308,18 +1282,18 @@ translateGuard fam_insts guard = case guard of
   XStmtLR         {} -> panic "translateGuard RecStmt"
 
 -- | Translate let-bindings
-translateLet :: HsLocalBinds GhcTc -> DsM PatVec
+translateLet :: HsLocalBinds GhcTc -> PmM PatVec
 translateLet _binds = return []
 
 -- | Translate a pattern guard
-translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
+translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> PmM PatVec
 translateBind fam_insts (dL->L _ p) e = do
   ps <- translatePat fam_insts p
   g <- mkGuard ps (unLoc e)
   return [g]
 
 -- | Translate a boolean guard
-translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
+translateBoolGuard :: LHsExpr GhcTc -> PmM PatVec
 translateBoolGuard e
   | isJust (isTrueLHsExpr e) = return []
     -- The formal thing to do would be to generate (True <- True)
@@ -1440,6 +1414,7 @@ families is not really efficient.
 pmPatType :: PmPat p -> Type
 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
   = conLikeResTy con tys
+pmPatType (PmNCon { pm_con_id  = x }) = idType x
 pmPatType (PmVar  { pm_var_id  = x }) = idType x
 pmPatType (PmLit  { pm_lit_lit = l }) = pmLitType l
 pmPatType (PmNLit { pm_lit_id  = x }) = idType x
@@ -1609,7 +1584,7 @@ instance Outputable InhabitationCandidate where
 
 -- | Generate an 'InhabitationCandidate' for a given conlike (generate
 -- fresh variables of the appropriate type for arguments)
-mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
+mkOneConFull :: Id -> ConLike -> PmM InhabitationCandidate
 --  *  x :: T tys, where T is an algebraic data type
 --     NB: in the case of a data family, T is the *representation* TyCon
 --     e.g.   data instance T (a,b) = T1 a b
@@ -1663,23 +1638,23 @@ mkOneConFull x con = do
 -- * More smart constructors and fresh variable generation
 
 -- | Create a guard pattern
-mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
+mkGuard :: PatVec -> HsExpr GhcTc -> PmM Pattern
 mkGuard pv e = do
   res <- allM cantFailPattern pv
   let expr = hsExprToPmExpr e
-  tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
+  tracePm "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
   if | res                    -> pure (PmGrd pv expr)
      | 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)
+-- | Create a term equality of the form: `(False ~ (x ~ e))`
+mkNegEq :: Id -> PmExpr -> ComplexEq
+mkNegEq x e = (falsePmExpr, PmExprVar (idName x) `PmExprEq` e)
 {-# INLINE mkNegEq #-}
 
--- | Create a term equality of the form: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> ComplexEq
-mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
+-- | Create a term equality of the form: `(x ~ e)`
+mkPosEq :: Id -> PmExpr -> ComplexEq
+mkPosEq x e = (PmExprVar (idName x), e)
 {-# INLINE mkPosEq #-}
 
 -- | Create a term equality of the form: `(x ~ x)`
@@ -1690,17 +1665,17 @@ mkIdEq x = (PmExprVar name, PmExprVar name)
 {-# INLINE mkIdEq #-}
 
 -- | Generate a variable pattern of a given type
-mkPmVar :: Type -> DsM (PmPat p)
+mkPmVar :: Type -> PmM (PmPat p)
 mkPmVar ty = PmVar <$> mkPmId ty
 {-# INLINE mkPmVar #-}
 
 -- | Generate many variable patterns, given a list of types
-mkPmVars :: [Type] -> DsM PatVec
+mkPmVars :: [Type] -> PmM PatVec
 mkPmVars tys = mapM mkPmVar tys
 {-# INLINE mkPmVars #-}
 
 -- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
+mkPmId :: Type -> PmM Id
 mkPmId ty = getUniqueM >>= \unique ->
   let occname = mkVarOccFS $ fsLit "$pm"
       name    = mkInternalName unique occname noSrcSpan
@@ -1709,7 +1684,7 @@ mkPmId ty = getUniqueM >>= \unique ->
 -- | Generate a fresh term variable of a given and return it in two forms:
 -- * A variable pattern
 -- * A variable expression
-mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
+mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr GhcTc)
 mkPmId2Forms ty = do
   x <- mkPmId ty
   return (PmVar x, noLoc (HsVar noExt (noLoc x)))
@@ -1721,6 +1696,7 @@ mkPmId2Forms ty = do
 vaToPmExpr :: ValAbs -> PmExpr
 vaToPmExpr (PmCon  { pm_con_con = c, pm_con_args = ps })
   = PmExprCon c (map vaToPmExpr ps)
+vaToPmExpr (PmNCon { pm_con_id  = x }) = PmExprVar (idName x)
 vaToPmExpr (PmVar  { pm_var_id  = x }) = PmExprVar (idName x)
 vaToPmExpr (PmLit  { pm_lit_lit = l }) = PmExprLit l
 vaToPmExpr (PmNLit { pm_lit_id  = x }) = PmExprVar (idName x)
@@ -1748,7 +1724,7 @@ coercePmPat PmFake     = [] -- drop the guards
 -- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
 -- it is the only possible match in the given context. See also
 -- 'allCompleteMatches' and Note [Single match constructors].
-singleMatchConstructor :: ConLike -> [Type] -> DsM Bool
+singleMatchConstructor :: ConLike -> [Type] -> PmM Bool
 singleMatchConstructor cl tys =
   any (isSingleton . snd) <$> allCompleteMatches cl tys
 
@@ -1890,8 +1866,7 @@ nameType name ty = do
 -- | Check whether a set of type constraints is satisfiable.
 tyOracle :: Bag EvVar -> PmM Bool
 tyOracle evs
-  = liftD $
-    do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+  = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
        ; case res of
             Just sat -> return sat
             Nothing  -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
@@ -1973,7 +1948,7 @@ mkInitialUncovered vars = do
 -- limit is not exceeded and call `pmcheck`
 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
 pmcheckI ps guards vva = do
-  n <- liftD incrCheckPmIterDs
+  n <- incrCheckPmIterDs
   tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
                         $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
                         $$ pprValVecDebug vva)
@@ -1985,7 +1960,7 @@ pmcheckI ps guards vva = do
 -- | Increase the counter for elapsed algorithm iterations, check that the
 -- limit is not exceeded and call `pmcheckGuards`
 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
-pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
+pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
 {-# INLINE pmcheckGuardsI #-}
 
 -- | Increase the counter for elapsed algorithm iterations, check that the
@@ -1993,7 +1968,7 @@ pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
            -> PmM PartialResult
 pmcheckHdI p ps guards va vva = do
-  n <- liftD incrCheckPmIterDs
+  n <- incrCheckPmIterDs
   tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
                         $$ pprPatVec ps
                         $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
@@ -2023,7 +1998,7 @@ pmcheck (PmFake : ps) guards vva =
 pmcheck (p : ps) guards (ValVec vas delta)
   | PmGrd { pm_grd_pv = pv, pm_grd_expr = e } <- p
   = do
-      y <- liftD $ mkPmId (pmPatType p)
+      y <- mkPmId (pmPatType p)
       let tm_state = extendSubst y e (delta_tm_cs delta)
           delta'   = delta { delta_tm_cs = tm_state }
       utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
@@ -2077,7 +2052,7 @@ pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
           | otherwise  = Just <$> to_evvar tv1 tv2
     evvars <- (listToBag . catMaybes) <$>
               ASSERT(ex_tvs1 `equalLength` ex_tvs2)
-              liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
+              (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
     let delta' = delta { delta_ty_cs = evvars `unionBags` delta_ty_cs delta }
     kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
       <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta')
@@ -2089,34 +2064,50 @@ pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
     False -> return $ ucon va (usimple [vva])
 
 -- ConVar
-pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
-          ps guards
-          (PmVar x) (ValVec vva delta) = do
-  (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
-
-  cons_cs <- mapM (liftD . mkOneConFull x) complete_match
-
-  inst_vsa <- flip mapMaybeM cons_cs $
-      \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
-                            , ic_ty_cs = ty_cs
-                            , ic_strict_arg_tys = strict_arg_tys } -> do
-    mb_sat <- pmIsSatisfiable delta tm_ct ty_cs strict_arg_tys
-    pure $ fmap (ValVec (va:vva)) mb_sat
-
-  set_provenance prov .
-    force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
-      runMany (pmcheckI (p:ps) guards) inst_vsa
+pmcheckHd p@PmCon{} ps guards (PmVar x) vva = do
+  incomplete_sets <- map snd <$> allCompleteMatches (pm_con_con p) (pm_con_arg_tys p)
+  --tracePm "ConVar" (vcat [ppr p, ppr x, ppr incomplete_sets])
+  -- Not all matches are satisfiable, but we will check this as we go, so that
+  -- we don't check satisfiability for every ConLike when we hit a wildcard
+  -- match later on anyway. We finally do so in 'normaliseUncovered'.
+  pmcheckHd p ps guards (PmNCon x incomplete_sets) vva
+
+-- ConNCon
+pmcheckHd p@PmCon{} ps guards (PmNCon x sets) (ValVec vva delta) = do
+  -- Split the value vector into two value vectors: One representing the current
+  -- constructor, the other representing the other constructors of every
+  -- Complete match set.
+  let con = pm_con_con p
+
+  -- For the value vector of the current constructor, we directly recurse into
+  -- checking the the current case, so we get back a PartialResult
+  ic <- mkOneConFull x con
+  pr_con <- fmap (fromMaybe mempty) $ runMaybeT $ do
+    guard (any (elem con) sets)
+    delta' <- MaybeT $ pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+    lift $ pmcheckHdI p ps guards (ic_val_abs ic) (ValVec vva delta')
+
+  let sets' = map (filter (/= con)) sets
+  let us_incomplete
+        | all notNull sets' -- there weren't any obvious complete matches
+        , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x (vaToPmExpr (ic_val_abs ic)))
+        = [ValVec (PmNCon x sets' : vva) (delta { delta_tm_cs = tm_state })]
+        | otherwise = []
+
+  -- Combine both into a single PartialResult
+  let pr_combined = mkUnion pr_con (usimple us_incomplete)
+  pure $ force_if (canDiverge (idName x) (delta_tm_cs delta)) pr_combined
 
 -- LitVar
 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
   = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
       mkUnion non_matched <$>
-        case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
+        case solveOneEq (delta_tm_cs delta) (mkPosEq x (PmExprLit l)) of
           Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
                              ValVec vva (delta {delta_tm_cs = tm_state})
           Nothing       -> return mempty
   where
-    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x (PmExprLit l))
        = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
        | otherwise = []
 
@@ -2126,7 +2117,7 @@ pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
 pmcheckHd (p@(PmLit l)) ps guards
           (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
   | all (not . eqPmLit l) lits
-  , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
+  , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x (PmExprLit l))
     -- Both guards check the same so it would be sufficient to have only
     -- the second one. Nevertheless, it is much cheaper to check whether
     -- the literal is in the list so we check it first, to avoid calling
@@ -2136,7 +2127,7 @@ 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)
+    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x (PmExprLit l))
        = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
        | otherwise = []
 
@@ -2151,7 +2142,7 @@ pmcheckHd (p@(PmLit l)) ps guards
 
 -- LitCon
 pmcheckHd p@PmLit{} ps guards va@PmCon{} (ValVec vva delta)
-  = do y <- liftD $ mkPmId (pmPatType va)
+  = do y <- mkPmId (pmPatType va)
        -- Analogous to the ConVar case, we have to case split the value
        -- abstraction on possible literals. We do so by introducing a fresh
        -- variable that is equated to the constructor. LitVar will then take
@@ -2162,7 +2153,7 @@ pmcheckHd p@PmLit{} ps guards va@PmCon{} (ValVec vva delta)
 
 -- ConLit
 pmcheckHd p@PmCon{} ps guards (PmLit l) (ValVec vva delta)
-  = do y <- liftD $ mkPmId (pmPatType p)
+  = do y <- mkPmId (pmPatType p)
        -- This desugars to the ConVar case by introducing a fresh variable that
        -- is equated to the literal via a constraint. ConVar will then properly
        -- case split on all possible constructors.
@@ -2174,6 +2165,10 @@ pmcheckHd p@PmCon{} ps guards (PmLit l) (ValVec vva delta)
 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
   = pmcheckHdI p ps guards (PmVar x) vva
 
+-- LitNCon
+pmcheckHd (p@(PmLit {})) ps guards (PmNCon { pm_con_id = x }) vva
+  = pmcheckHdI p ps guards (PmVar x) vva
+
 -- Impossible: handled by pmcheck
 pmcheckHd PmFake     _ _ _ _ = panic "pmcheckHd: Fake"
 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
@@ -2357,9 +2352,6 @@ force_if :: Bool -> PartialResult -> PartialResult
 force_if True  pres = forces pres
 force_if False pres = pres
 
-set_provenance :: Provenance -> PartialResult -> PartialResult
-set_provenance prov pr = pr { presultProvenance = prov }
-
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
 
@@ -2367,7 +2359,7 @@ set_provenance prov pr = pr { presultProvenance = prov }
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When checking a match it would be great to have all type and term information
 available so we can get more precise results. For this reason we have functions
-`addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
+`addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
 term constraints (respectively) as we go deeper.
 
 The type constraints we propagate inwards are collected by `collectEvVarsPats'
@@ -2717,11 +2709,7 @@ involved.
 -- Debugging Infrastructre
 
 tracePm :: String -> SDoc -> PmM ()
-tracePm herald doc = liftD $ tracePmD herald doc
-
-
-tracePmD :: String -> SDoc -> DsM ()
-tracePmD herald doc = do
+tracePm herald doc = do
   dflags <- getDynFlags
   printer <- mkPrintUnqualifiedDs
   liftIO $ dumpIfSet_dyn_printer printer dflags
@@ -2731,6 +2719,8 @@ tracePmD herald doc = do
 pprPmPatDebug :: PmPat a -> SDoc
 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
   = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
+pprPmPatDebug (PmNCon x sets)
+  = hsep [text "PmNCon", ppr x, ppr sets]
 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
 pprPmPatDebug (PmLit li)  = text "PmLit" <+> ppr li
 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363a.hs b/testsuite/tests/pmcheck/complete_sigs/T13363a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..9d7b8bcaf5b1dd8388d3912d5304a90f99b4ecab
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363a.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _               = error "impossible"
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr b/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..7982112f67ffcf6383059c448208f789199e2820
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363a.hs:15:1: warning: [-Woverlapping-patterns]
+    Pattern match is redundant
+    In an equation for `catchAll': catchAll _ = ...
+   |
+14 | catchAll _               = error "impossible"
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363b.hs b/testsuite/tests/pmcheck/complete_sigs/T13363b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4f2f07b6a9ec0050729bed81334c6ced60c2b2e3
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363b.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data T = A | B | C
+  deriving Eq
+
+pattern BC :: T
+pattern BC = C
+
+{-# COMPLETE A, BC #-}
+
+f A  = 1
+f B  = 2
+f BC = 3
+f _  = error "impossible"
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr b/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..763bc6e26f66e65da2adc26b94afee8b9cfa8cbc
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363b.hs:16:1: warning: [-Woverlapping-patterns]
+    Pattern match is redundant
+    In an equation for `f': f _ = ...
+   |
+16 | f _  = error "impossible"
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index d58c182f8eda6236a6323bae7a44683007a43cfa..551516bb1b3ea9f79ec2368c4e7d63ed3e4e0a72 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -15,3 +15,5 @@ test('completesig14', normal, compile, [''])
 test('completesig15', normal, compile_fail, [''])
 test('T14059a', normal, compile, [''])
 test('T14253', expect_broken(14253), compile, [''])
+test('T13363a', normal, compile, ['-Wall'])
+test('T13363b', normal, compile, ['-Wall'])