PmCheck: Disattach COMPLETE pragma lookup from TyCons

By not attaching COMPLETE pragmas with a particular TyCon and instead
assume that every COMPLETE pragma is applicable everywhere, we can
drastically simplify the logic that tries to initialise available
COMPLETE sets of a variable during the pattern-match checking process,
as well as fixing a few bugs.

Of course, we have to make sure not to report any of the
ill-typed/unrelated COMPLETE sets, which came up in a few regression
tests.

In doing so, we fix #17207, #18277 and #14422.

There was a metric decrease in #18478 by ~20%.

Metric Decrease:
    T18478

22 files changed, 367 insertions, 467 deletions

diff --git a/compiler/GHC/Driver/Types.hs b/compiler/GHC/Driver/Types.hs
index 9e922850e2..672dd1b451 100644
--- a/compiler/GHC/Driver/Types.hs
+++ b/compiler/GHC/Driver/Types.hs
@@ -61,7 +61,7 @@ module GHC.Driver.Types (
         lookupIfaceByModule, emptyPartialModIface, emptyFullModIface, lookupHptByModule,
 
         PackageInstEnv, PackageFamInstEnv, PackageRuleBase,
-        PackageCompleteMatchMap,
+        PackageCompleteMatches,
 
         mkSOName, mkHsSOName, soExt,
 
@@ -146,8 +146,7 @@ module GHC.Driver.Types (
         handleFlagWarnings, printOrThrowWarnings,
 
         -- * COMPLETE signature
-        CompleteMatch(..), CompleteMatchMap,
-        mkCompleteMatchMap, extendCompleteMatchMap,
+        ConLikeSet, CompleteMatch, CompleteMatches,
 
         -- * Exstensible Iface fields
         ExtensibleFields(..), FieldName,
@@ -735,7 +734,7 @@ lookupIfaceByModule hpt pit mod
 -- of its own, but it doesn't seem worth the bother.
 
 hptCompleteSigs :: HscEnv -> [CompleteMatch]
-hptCompleteSigs = hptAllThings  (md_complete_sigs . hm_details)
+hptCompleteSigs = hptAllThings  (md_complete_matches . hm_details)
 
 -- | Find all the instance declarations (of classes and families) from
 -- the Home Package Table filtered by the provided predicate function.
@@ -1093,7 +1092,7 @@ data ModIface_ (phase :: ModIfacePhase)
                 -- itself) but imports some trustworthy modules from its own
                 -- package (which does require its own package be trusted).
                 -- See Note [Trust Own Package] in GHC.Rename.Names
-        mi_complete_sigs :: [IfaceCompleteMatch],
+        mi_complete_matches :: [IfaceCompleteMatch],
 
         mi_doc_hdr :: Maybe HsDocString,
                 -- ^ Module header.
@@ -1184,7 +1183,7 @@ instance Binary ModIface where
                  mi_hpc       = hpc_info,
                  mi_trust     = trust,
                  mi_trust_pkg = trust_pkg,
-                 mi_complete_sigs = complete_sigs,
+                 mi_complete_matches = complete_matches,
                  mi_doc_hdr   = doc_hdr,
                  mi_decl_docs = decl_docs,
                  mi_arg_docs  = arg_docs,
@@ -1230,7 +1229,7 @@ instance Binary ModIface where
         put_ bh hpc_info
         put_ bh trust
         put_ bh trust_pkg
-        put_ bh complete_sigs
+        put_ bh complete_matches
         lazyPut bh doc_hdr
         lazyPut bh decl_docs
         lazyPut bh arg_docs
@@ -1263,7 +1262,7 @@ instance Binary ModIface where
         hpc_info    <- get bh
         trust       <- get bh
         trust_pkg   <- get bh
-        complete_sigs <- get bh
+        complete_matches <- get bh
         doc_hdr     <- lazyGet bh
         decl_docs   <- lazyGet bh
         arg_docs    <- lazyGet bh
@@ -1287,7 +1286,7 @@ instance Binary ModIface where
                  mi_trust       = trust,
                  mi_trust_pkg   = trust_pkg,
                         -- And build the cached values
-                 mi_complete_sigs = complete_sigs,
+                 mi_complete_matches = complete_matches,
                  mi_doc_hdr     = doc_hdr,
                  mi_decl_docs   = decl_docs,
                  mi_arg_docs    = arg_docs,
@@ -1332,7 +1331,7 @@ emptyPartialModIface mod
                mi_hpc         = False,
                mi_trust       = noIfaceTrustInfo,
                mi_trust_pkg   = False,
-               mi_complete_sigs = [],
+               mi_complete_matches = [],
                mi_doc_hdr     = Nothing,
                mi_decl_docs   = emptyDeclDocMap,
                mi_arg_docs    = emptyArgDocMap,
@@ -1388,7 +1387,7 @@ data ModDetails
         md_rules     :: ![CoreRule],    -- ^ Domain may include 'Id's from other modules
         md_anns      :: ![Annotation],  -- ^ Annotations present in this module: currently
                                         -- they only annotate things also declared in this module
-        md_complete_sigs :: [CompleteMatch]
+        md_complete_matches :: [CompleteMatch]
           -- ^ Complete match pragmas for this module
      }
 
@@ -1401,7 +1400,7 @@ emptyModDetails
                  md_rules     = [],
                  md_fam_insts = [],
                  md_anns      = [],
-                 md_complete_sigs = [] }
+                 md_complete_matches = [] }
 
 -- | Records the modules directly imported by a module for extracting e.g.
 -- usage information, and also to give better error message
@@ -1464,7 +1463,7 @@ data ModGuts
         -- ^ Files to be compiled with the C compiler
         mg_warns     :: !Warnings,       -- ^ Warnings declared in the module
         mg_anns      :: [Annotation],    -- ^ Annotations declared in this module
-        mg_complete_sigs :: [CompleteMatch], -- ^ Complete Matches
+        mg_complete_matches :: [CompleteMatch], -- ^ Complete Matches
         mg_hpc_info  :: !HpcInfo,        -- ^ Coverage tick boxes in the module
         mg_modBreaks :: !(Maybe ModBreaks), -- ^ Breakpoints for the module
 
@@ -2685,7 +2684,7 @@ type PackageRuleBase         = RuleBase
 type PackageInstEnv          = InstEnv
 type PackageFamInstEnv       = FamInstEnv
 type PackageAnnEnv           = AnnEnv
-type PackageCompleteMatchMap = CompleteMatchMap
+type PackageCompleteMatches = CompleteMatches
 
 -- | Information about other packages that we have slurped in by reading
 -- their interface files
@@ -2747,8 +2746,8 @@ data ExternalPackageState
                                                -- from all the external-package modules
         eps_ann_env      :: !PackageAnnEnv,    -- ^ The total 'AnnEnv' accumulated
                                                -- from all the external-package modules
-        eps_complete_matches :: !PackageCompleteMatchMap,
-                                  -- ^ The total 'CompleteMatchMap' accumulated
+        eps_complete_matches :: !PackageCompleteMatches,
+                                  -- ^ The total 'CompleteMatches' accumulated
                                   -- from all the external-package modules
 
         eps_mod_fam_inst_env :: !(ModuleEnv FamInstEnv), -- ^ The family instances accumulated from external
@@ -3204,83 +3203,14 @@ byteCodeOfObject other       = pprPanic "byteCodeOfObject" (ppr other)
 
 -------------------------------------------
 
+type ConLikeSet = UniqDSet ConLike
+
 -- | A list of conlikes which represents a complete pattern match.
 -- These arise from @COMPLETE@ signatures.
+-- See also Note [Implementation of COMPLETE pragmas].
+type CompleteMatch = ConLikeSet
 
--- See Note [Implementation of COMPLETE signatures]
-data CompleteMatch = CompleteMatch {
-                            completeMatchConLikes :: [Name]
-                            -- ^ The ConLikes that form a covering family
-                            -- (e.g. Nothing, Just)
-                          , completeMatchTyCon :: Name
-                            -- ^ The TyCon that they cover (e.g. Maybe)
-                          }
-
-instance Outputable CompleteMatch where
-  ppr (CompleteMatch cl ty) = text "CompleteMatch:" <+> ppr cl
-                                                    <+> dcolon <+> ppr ty
-
--- | A map keyed by the 'completeMatchTyCon' which has type Name.
-
--- See Note [Implementation of COMPLETE signatures]
-type CompleteMatchMap = UniqFM Name [CompleteMatch]
-
-mkCompleteMatchMap :: [CompleteMatch] -> CompleteMatchMap
-mkCompleteMatchMap = extendCompleteMatchMap emptyUFM
-
-extendCompleteMatchMap :: CompleteMatchMap -> [CompleteMatch]
-                       -> CompleteMatchMap
-extendCompleteMatchMap = foldl' insertMatch
-  where
-    insertMatch :: CompleteMatchMap -> CompleteMatch -> CompleteMatchMap
-    insertMatch ufm c@(CompleteMatch _ t) = addToUFM_C (++) ufm t [c]
-
-{-
-Note [Implementation of COMPLETE signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A COMPLETE signature represents a set of conlikes (i.e., constructors or
-pattern synonyms) such that if they are all pattern-matched against in a
-function, it gives rise to a total function. An example is:
-
-  newtype Boolean = Boolean Int
-  pattern F, T :: Boolean
-  pattern F = Boolean 0
-  pattern T = Boolean 1
-  {-# COMPLETE F, T #-}
-
-  -- This is a total function
-  booleanToInt :: Boolean -> Int
-  booleanToInt F = 0
-  booleanToInt T = 1
-
-COMPLETE sets are represented internally in GHC with the CompleteMatch data
-type. For example, {-# COMPLETE F, T #-} would be represented as:
-
-  CompleteMatch { complateMatchConLikes = [F, T]
-                , completeMatchTyCon    = Boolean }
-
-Note that GHC was able to infer the completeMatchTyCon (Boolean), but for the
-cases in which it's ambiguous, you can also explicitly specify it in the source
-language by writing this:
-
-  {-# COMPLETE F, T :: Boolean #-}
-
-For efficiency purposes, GHC collects all of the CompleteMatches that it knows
-about into a CompleteMatchMap, which is a map that is keyed by the
-completeMatchTyCon. In other words, you could have a multiple COMPLETE sets
-for the same TyCon:
-
-  {-# COMPLETE F, T1 :: Boolean #-}
-  {-# COMPLETE F, T2 :: Boolean #-}
-
-And looking up the values in the CompleteMatchMap associated with Boolean
-would give you [CompleteMatch [F, T1] Boolean, CompleteMatch [F, T2] Boolean].
-dsGetCompleteMatches in GHC.HsToCore.Quote accomplishes this lookup.
-
-Also see Note [Typechecking Complete Matches] in GHC.Tc.Gen.Bind for a more detailed
-explanation for how GHC ensures that all the conlikes in a COMPLETE set are
-consistent.
--}
+type CompleteMatches = [CompleteMatch]
 
 -- | Foreign language of the phase if the phase deals with a foreign code
 phaseForeignLanguage :: Phase -> Maybe ForeignSrcLang
diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs
index 5c1f62104e..3b013850b2 100644
--- a/compiler/GHC/HsToCore.hs
+++ b/compiler/GHC/HsToCore.hs
@@ -228,7 +228,7 @@ deSugar hsc_env
                 mg_modBreaks    = modBreaks,
                 mg_safe_haskell = safe_mode,
                 mg_trust_pkg    = imp_trust_own_pkg imports,
-                mg_complete_sigs = complete_matches,
+                mg_complete_matches = complete_matches,
                 mg_doc_hdr      = doc_hdr,
                 mg_decl_docs    = decl_docs,
                 mg_arg_docs     = arg_docs
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index 08b62ee14f..e7a820a86e 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/compiler/GHC/HsToCore/Monad.hs
@@ -88,7 +88,6 @@ import GHC.Driver.Ppr
 import GHC.Utils.Error
 import GHC.Utils.Panic
 import GHC.Data.FastString
-import GHC.Types.Unique.FM ( lookupWithDefaultUFM_Directly )
 import GHC.Types.Literal ( mkLitString )
 import GHC.Types.CostCentre.State
 
@@ -210,13 +209,15 @@ mkDsEnvsFromTcGbl :: MonadIO m
                   -> m (DsGblEnv, DsLclEnv)
 mkDsEnvsFromTcGbl hsc_env msg_var tcg_env
   = do { cc_st_var   <- liftIO $ newIORef newCostCentreState
+       ; eps <- liftIO $ hscEPS hsc_env
        ; let dflags   = hsc_dflags hsc_env
              this_mod = tcg_mod tcg_env
              type_env = tcg_type_env tcg_env
              rdr_env  = tcg_rdr_env tcg_env
              fam_inst_env = tcg_fam_inst_env tcg_env
-             complete_matches = hptCompleteSigs hsc_env
-                                ++ tcg_complete_matches tcg_env
+             complete_matches = hptCompleteSigs hsc_env         -- from the home package
+                                ++ tcg_complete_matches tcg_env -- from the current module
+                                ++ eps_complete_matches eps     -- from imports
        ; return $ mkDsEnvs dflags this_mod rdr_env type_env fam_inst_env
                            msg_var cc_st_var complete_matches
        }
@@ -239,13 +240,15 @@ initDsWithModGuts :: HscEnv -> ModGuts -> DsM a -> IO (Messages, Maybe a)
 initDsWithModGuts hsc_env guts thing_inside
   = do { cc_st_var   <- newIORef newCostCentreState
        ; msg_var <- newIORef emptyMessages
+       ; eps <- liftIO $ hscEPS hsc_env
        ; let dflags   = hsc_dflags hsc_env
              type_env = typeEnvFromEntities ids (mg_tcs guts) (mg_fam_insts guts)
              rdr_env  = mg_rdr_env guts
              fam_inst_env = mg_fam_inst_env guts
              this_mod = mg_module guts
-             complete_matches = hptCompleteSigs hsc_env
-                                ++ mg_complete_sigs guts
+             complete_matches = hptCompleteSigs hsc_env     -- from the home package
+                                ++ mg_complete_matches guts -- from the current module
+                                ++ eps_complete_matches eps -- from imports
 
              bindsToIds (NonRec v _)   = [v]
              bindsToIds (Rec    binds) = map fst binds
@@ -281,7 +284,7 @@ initTcDsForSolver thing_inside
          thing_inside }
 
 mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
-         -> IORef Messages -> IORef CostCentreState -> [CompleteMatch]
+         -> IORef Messages -> IORef CostCentreState -> CompleteMatches
          -> (DsGblEnv, DsLclEnv)
 mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var
          complete_matches
@@ -290,7 +293,6 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var
         if_lenv = mkIfLclEnv mod (text "GHC error in desugarer lookup in" <+> ppr mod)
                              NotBoot
         real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1)
-        completeMatchMap = mkCompleteMatchMap complete_matches
         gbl_env = DsGblEnv { ds_mod     = mod
                            , ds_fam_inst_env = fam_inst_env
                            , ds_if_env  = (if_genv, if_lenv)
@@ -299,7 +301,7 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var
                                              (mkHomeUnitFromFlags dflags)
                                              rdr_env
                            , ds_msgs    = msg_var
-                           , ds_complete_matches = completeMatchMap
+                           , ds_complete_matches = complete_matches
                            , ds_cc_st   = cc_st_var
                            }
         lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv
@@ -533,18 +535,9 @@ dsGetFamInstEnvs
 dsGetMetaEnv :: DsM (NameEnv DsMetaVal)
 dsGetMetaEnv = do { env <- getLclEnv; return (dsl_meta env) }
 
--- | The @COMPLETE@ pragmas provided by the user for a given `TyCon`.
-dsGetCompleteMatches :: TyCon -> DsM [CompleteMatch]
-dsGetCompleteMatches tc = do
-  eps <- getEps
-  env <- getGblEnv
-      -- We index into a UniqFM from Name -> elt, for tyCon it holds that
-      -- getUnique (tyConName tc) == getUnique tc. So we lookup using the
-      -- unique directly instead.
-  let lookup_completes ufm = lookupWithDefaultUFM_Directly ufm [] (getUnique tc)
-      eps_matches_list = lookup_completes $ eps_complete_matches eps
-      env_matches_list = lookup_completes $ ds_complete_matches env
-  return $ eps_matches_list ++ env_matches_list
+-- | The @COMPLETE@ pragmas that are in scope.
+dsGetCompleteMatches :: DsM CompleteMatches
+dsGetCompleteMatches = ds_complete_matches <$> getGblEnv
 
 dsLookupMetaEnv :: Name -> DsM (Maybe DsMetaVal)
 dsLookupMetaEnv name = do { env <- getLclEnv; return (lookupNameEnv (dsl_meta env) name) }
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 78238965fc..0109d596c5 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -67,13 +67,13 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.Type
 import GHC.Tc.Solver   (tcNormalise, tcCheckSatisfiability)
 import GHC.Core.Unify    (tcMatchTy)
-import GHC.Tc.Types      (completeMatchConLikes)
 import GHC.Core.Coercion
 import GHC.Utils.Monad hiding (foldlM)
 import GHC.HsToCore.Monad hiding (foldlM)
 import GHC.Tc.Instance.Family
 import GHC.Core.FamInstEnv
 
+import Control.Applicative ((<|>))
 import Control.Monad (guard, mzero, when)
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Trans.State.Strict
@@ -81,7 +81,6 @@ import Data.Bifunctor (second)
 import Data.Either   (partitionEithers)
 import Data.Foldable (foldlM, minimumBy, toList)
 import Data.List     (find)
-import qualified Data.List.NonEmpty as NonEmpty
 import Data.Ord      (comparing)
 import qualified Data.Semigroup as Semigroup
 import Data.Tuple    (swap)
@@ -106,11 +105,114 @@ mkPmId ty = getUniqueM >>= \unique ->
 -----------------------------------------------
 -- * Caching possible matches of a COMPLETE set
 
-markMatched :: ConLike -> PossibleMatches -> PossibleMatches
-markMatched _   NoPM    = NoPM
-markMatched con (PM ms) = PM (del_one_con con <$> ms)
+-- See Note [Implementation of COMPLETE pragmas]
+
+-- | Traverse the COMPLETE sets of 'ResidualCompleteMatches'.
+trvRcm :: Applicative f => (ConLikeSet -> f ConLikeSet) -> ResidualCompleteMatches -> f ResidualCompleteMatches
+trvRcm f (RCM vanilla pragmas) = RCM <$> traverse f vanilla
+                                     <*> traverse (traverse f) pragmas
+-- | Update the COMPLETE sets of 'ResidualCompleteMatches'.
+updRcm :: (ConLikeSet -> ConLikeSet) -> ResidualCompleteMatches -> ResidualCompleteMatches
+updRcm f (RCM vanilla pragmas) = RCM (f <$> vanilla) (fmap f <$> pragmas)
+
+-- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data
+-- 'TyCon'.
+-- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
+vanillaCompleteMatchTC :: TyCon -> Maybe ConLikeSet
+vanillaCompleteMatchTC tc =
+  let -- | TYPE acts like an empty data type on the term-level (#14086), but
+      -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
+      -- special case.
+      mb_dcs | tc == tYPETyCon = Just []
+             | otherwise       = tyConDataCons_maybe tc
+  in mkUniqDSet . map RealDataCon <$> mb_dcs
+
+-- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
+-- if the given 'ResidualCompleteMatches' were empty.
+addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
+addCompleteMatches (RCM v Nothing) = RCM v . Just <$> dsGetCompleteMatches
+addCompleteMatches rcm             = pure rcm
+
+-- | Adds the declared 'CompleteMatches' from COMPLETE pragmas, as well as the
+-- vanilla data defn if it is a 'DataCon'.
+addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
+addConLikeMatches (RealDataCon dc) rcm = addTyConMatches (dataConTyCon dc) rcm
+addConLikeMatches (PatSynCon _)    rcm = addCompleteMatches rcm
+
+-- | Adds
+--    * the 'CompleteMatches' from COMPLETE pragmas
+--    * and the /vanilla/ 'CompleteMatch' from the data 'TyCon'
+-- to the 'ResidualCompleteMatches', if not already present.
+addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
+addTyConMatches tc rcm = add_tc_match <$> addCompleteMatches rcm
   where
-    del_one_con = flip delOneFromUniqDSet
+    -- | Add the vanilla COMPLETE set from the data defn, if any. But only if
+    -- it's not already present.
+    add_tc_match rcm
+      = rcm{rcm_vanilla = rcm_vanilla rcm <|> vanillaCompleteMatchTC tc}
+
+markMatched :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
+markMatched cl rcm = do
+  rcm' <- addConLikeMatches cl rcm
+  pure $ updRcm (flip delOneFromUniqDSet cl) rcm'
+
+{-
+Note [Implementation of COMPLETE pragmas]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A COMPLETE set represents a set of conlikes (i.e., constructors or
+pattern synonyms) such that if they are all pattern-matched against in a
+function, it gives rise to a total function. An example is:
+
+  newtype Boolean = Boolean Int
+  pattern F, T :: Boolean
+  pattern F = Boolean 0
+  pattern T = Boolean 1
+  {-# COMPLETE F, T #-}
+
+  -- This is a total function
+  booleanToInt :: Boolean -> Int
+  booleanToInt F = 0
+  booleanToInt T = 1
+
+COMPLETE sets are represented internally in GHC a set of 'ConLike's. For
+example, the pragma {-# COMPLETE F, T #-} would be represented as:
+
+  {F, T}
+
+GHC collects all COMPLETE pragmas from the current module and from imports
+into a field in the DsM environment, which can be accessed with
+dsGetCompleteMatches from "GHC.HsToCore.Monad".
+Currently, COMPLETE pragmas can't be orphans (e.g. at least one ConLike must
+also be defined in the module of the pragma) and do not impact recompilation
+checking (#18675).
+
+The pattern-match checker will then initialise each variable's 'VarInfo' with
+*all* imported COMPLETE sets (in 'GHC.HsToCore.PmCheck.Oracle.addCompleteMatches'),
+well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
+COMPLETE set that is ill-typed for that match variable could never be written by
+the user! And we make sure not to report any ill-typed COMPLETE sets when
+formatting 'Nabla's for warnings in 'provideEvidence'.
+
+A 'ResidualCompleteMatches' is a list of all COMPLETE sets, minus the ConLikes
+we know a particular variable can't be (through negative constructor constraints
+@x /~ K@ or a failed attempt at instantiating that ConLike during inhabitation
+testing). If *any* of the COMPLETE sets become empty, we know that the match
+was exhaustive.
+
+We assume that a COMPLETE set is non-empty if for one of its ConLikes
+we fail to 'guessConLikeUnivTyArgsFromResTy'. That accounts for ill-typed
+COMPLETE sets. So why don't we simply prune those ill-typed COMPLETE sets from
+'ResidualCompleteMatches'? The answer is that additional type constraints might
+make more COMPLETE sets applicable! Example:
+
+  f :: a -> a :~: Boolean -> ()
+  f x Refl | T <- x = ()
+           | F <- x = ()
+
+If we eagerly prune {F,T} from the residual matches of @x@, then we don't see
+that the match in the guards of @f@ is exhaustive, where the COMPLETE set
+applies due to refined type information.
+-}
 
 ---------------------------------------------------
 -- * Instantiating constructors, types and evidence
@@ -493,7 +595,7 @@ tyOracle (TySt inert) cts
 -- | A 'SatisfiabilityCheck' based on new type-level constraints.
 -- Returns a new 'Nabla' if the new constraints are compatible with existing
 -- ones. Doesn't bother calling out to the type oracle if the bag of new type
--- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
+-- constraints was empty. Will only recheck 'ResidualCompleteMatches' in the term oracle
 -- for emptiness if the first argument is 'True'.
 tyIsSatisfiable :: Bool -> Bag PredType -> SatisfiabilityCheck
 tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \nabla ->
@@ -545,10 +647,10 @@ of a PatSynCon (Just42,[]), this solution is incomparable to both Nothing and
 Just. Hence we retain the info in vi_neg, which eventually allows us to detect
 the complete pattern match.
 
-The Pos/Neg invariant extends to vi_cache, which stores essentially positive
-information. We make sure that vi_neg and vi_cache never overlap. This isn't
-strictly necessary since vi_cache is just a cache, so doesn't need to be
-accurate: Every suggestion of a possible ConLike from vi_cache might be
+The Pos/Neg invariant extends to vi_rcm, which stores essentially positive
+information. We make sure that vi_neg and vi_rcm never overlap. This isn't
+strictly necessary since vi_rcm is just a cache, so doesn't need to be
+accurate: Every suggestion of a possible ConLike from vi_rcm might be
 refutable by the type oracle anyway. But it helps to maintain sanity while
 debugging traces.
 
@@ -569,7 +671,7 @@ The term oracle state is never obviously (i.e., without consulting the type
 oracle) contradictory. This implies a few invariants:
 * Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute.
   This is implied by the Note [Pos/Neg invariant].
-* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_cache to
+* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm to
   detect this, but we could just compare whole COMPLETE sets to vi_neg every
   time, if it weren't for performance.
 
@@ -625,13 +727,16 @@ tmIsSatisfiable new_tm_cs = SC $ \nabla -> runMaybeT $ foldlM addTmCt nabla new_
 -----------------------
 -- * Looking up VarInfo
 
+emptyRCM :: ResidualCompleteMatches
+emptyRCM = RCM Nothing Nothing
+
 emptyVarInfo :: Id -> VarInfo
 -- We could initialise @bot@ to @Just False@ in case of an unlifted type here,
 -- but it's cleaner to let the user of the constraint solver take care of this.
 -- After all, there are also strict fields, the unliftedness of which isn't
 -- evident in the type. So treating unlifted types here would never be
 -- sufficient anyway.
-emptyVarInfo x = VI (idType x) [] emptyPmAltConSet MaybeBot NoPM
+emptyVarInfo x = VI (idType x) [] emptyPmAltConSet MaybeBot emptyRCM
 
 lookupVarInfo :: TmState -> Id -> VarInfo
 -- (lookupVarInfo tms x) tells what we know about 'x'
@@ -657,85 +762,6 @@ lookupVarInfoNT ts x = case lookupVarInfo ts x of
       | isNewDataCon dc = Just y
     go _                = Nothing
 
-initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
-initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do
-  -- New evidence might lead to refined info on ty, in turn leading to discovery
-  -- of a COMPLETE set.
-  res <- pmTopNormaliseType ty_st ty
-  let ty' = normalisedSourceType res
-  case splitTyConApp_maybe ty' of
-    Nothing -> pure vi{ vi_ty = ty' }
-    Just (tc, [_])
-      | tc == tYPETyCon
-      -- TYPE acts like an empty data type on the term-level (#14086), but
-      -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
-      -- special case.
-      -> pure vi{ vi_ty = ty', vi_cache = PM (pure emptyUniqDSet) }
-    Just (tc, tc_args) -> do
-      -- See Note [COMPLETE sets on data families]
-      (tc_rep, tc_fam) <- case tyConFamInst_maybe tc of
-        Just (tc_fam, _) -> pure (tc, tc_fam)
-        Nothing -> do
-          env <- dsGetFamInstEnvs
-          let (tc_rep, _tc_rep_args, _co) = tcLookupDataFamInst env tc tc_args
-          pure (tc_rep, tc)
-      -- Note that the common case here is tc_rep == tc_fam
-      let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc_rep
-      let rdcs = maybeToList mb_rdcs
-      -- NB: tc_fam, because COMPLETE sets are associated with the parent data
-      -- family TyCon
-      pragmas <- dsGetCompleteMatches tc_fam
-      let fams = mapM dsLookupConLike . completeMatchConLikes
-      pscs <- mapM fams pragmas
-      -- pprTrace "initPossibleMatches" (ppr ty $$ ppr ty' $$ ppr tc_rep <+> ppr tc_fam <+> ppr tc_args $$ ppr (rdcs ++ pscs)) (return ())
-      case NonEmpty.nonEmpty (rdcs ++ pscs) of
-        Nothing -> pure vi{ vi_ty = ty' } -- Didn't find any COMPLETE sets
-        Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) }
-initPossibleMatches _     vi                                   = pure vi
-
-{- Note [COMPLETE sets on data families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-User-defined COMPLETE sets involving data families are attached to the family
-TyCon, whereas the built-in COMPLETE set is attached to a data family instance's
-representation TyCon. This matters for COMPLETE sets involving both DataCons
-and PatSyns (from #17207):
-
-  data family T a
-  data family instance T () = A | B
-  pattern C = B
-  {-# COMPLETE A, C #-}
-  f :: T () -> ()
-  f A = ()
-  f C = ()
-
-The match on A is actually wrapped in a CoPat, matching impedance between T ()
-and its representation TyCon, which we translate as
-@x | let y = x |> co, A <- y@ in PmCheck.
-
-Which TyCon should we use for looking up the COMPLETE set? The representation
-TyCon from the match on A would only reveal the built-in COMPLETE set, while the
-data family TyCon would only give the user-defined one. But when initialising
-the PossibleMatches for a given Type, we want to do so only once, because
-merging different COMPLETE sets after the fact is very complicated and possibly
-inefficient.
-
-So in fact, we just *drop* the coercion arising from the CoPat when handling
-handling the constraint @y ~ x |> co@ in addCoreCt, just equating @y ~ x@.
-We then handle the fallout in initPossibleMatches, which has to get a hand at
-both the representation TyCon tc_rep and the parent data family TyCon tc_fam.
-It considers three cases after having established that the Type is a TyConApp:
-
-1. The TyCon is a vanilla data type constructor
-2. The TyCon is tc_rep
-3. The TyCon is tc_fam
-
-1. is simple and subsumed by the handling of the other two.
-We check for case 2. by 'tyConFamInst_maybe' and get the tc_fam out.
-Otherwise (3.), we try to lookup the data family instance at that particular
-type to get out the tc_rep. In case 1., this will just return the original
-TyCon, so tc_rep = tc_fam afterwards.
--}
-
 ------------------------------------------------
 -- * Exported utility functions querying 'Nabla'
 
@@ -898,11 +924,7 @@ addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
 addNotConCt _ _ (PmAltConLike (RealDataCon dc))
   | isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches]
 addNotConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
-  -- For good performance, it's important to initPossibleMatches here.
-  -- Otherwise we can't mark nalt as matched later on, incurring unnecessary
-  -- inhabitation tests for nalt.
-  vi@(VI _ pos neg _ pm) <- lift $ initPossibleMatches (nabla_ty_st nabla)
-                                                       (lookupVarInfo ts x)
+  let vi@(VI _ pos neg _ rcm) = lookupVarInfo ts x
   -- 1. Bail out quickly when nalt contradicts a solution
   let contradicts nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Equal
   guard (not (any (contradicts nalt) pos))
@@ -918,9 +940,11 @@ addNotConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
   let vi1 = vi{ vi_neg = neg', vi_bot = IsNotBot }
   -- 3. Make sure there's at least one other possible constructor
   vi2 <- case nalt of
-    PmAltConLike cl
-      -> ensureInhabited nabla vi1{ vi_cache = markMatched cl pm }
-    _ -> pure vi1
+    PmAltConLike cl -> do
+      rcm' <- lift (markMatched cl rcm)
+      ensureInhabited nabla vi1{ vi_rcm = rcm' }
+    _ ->
+      pure vi1
   pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env x vi2) reps }
 
 hasRequiredTheta :: PmAltCon -> Bool
@@ -964,13 +988,15 @@ storing required arguments along with the PmAltConLike in 'vi_neg'.
 -- its result type. Rather easy for DataCons, but not so much for PatSynCons.
 -- See Note [Pattern synonym result type] in "GHC.Core.PatSyn".
 guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type]
-guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon _) = do
+guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon dc) = do
   (tc, tc_args) <- splitTyConApp_maybe res_ty
   -- Consider data families: In case of a DataCon, we need to translate to
   -- the representation TyCon. For PatSyns, they are relative to the data
   -- family TyCon, so we don't need to translate them.
-  let (_, tc_args', _) = tcLookupDataFamInst env tc tc_args
-  Just tc_args'
+  let (rep_tc, tc_args', _) = tcLookupDataFamInst env tc tc_args
+  if rep_tc == dataConTyCon dc
+    then Just tc_args'
+    else Nothing
 guessConLikeUnivTyArgsFromResTy _   res_ty (PatSynCon ps)  = do
   -- We are successful if we managed to instantiate *every* univ_tv of con.
   -- This is difficult and bound to fail in some cases, see
@@ -999,7 +1025,7 @@ addNotBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do
 -- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
 -- set satisfies the oracle
 --
--- Internally uses and updates the ConLikeSets in vi_cache.
+-- Internally uses and updates the ConLikeSets in vi_rcm.
 --
 -- NB: Does /not/ filter each ConLikeSet with the oracle; members may
 --     remain that do not statisfy it.  This lazy approach just
@@ -1008,17 +1034,32 @@ ensureInhabited :: Nabla -> VarInfo -> MaybeT DsM VarInfo
 ensureInhabited nabla vi = case vi_bot vi of
   MaybeBot -> pure vi -- The |-Bot rule from the paper
   IsBot    -> pure vi
-  IsNotBot -> lift (initPossibleMatches (nabla_ty_st nabla) vi) >>= inst_complete_sets
+  IsNotBot -> lift (add_matches vi) >>= inst_complete_sets
   where
+    add_matches :: VarInfo -> DsM VarInfo
+    add_matches vi = do
+      res <- pmTopNormaliseType (nabla_ty_st nabla) (vi_ty vi)
+      rcm <- case reprTyCon_maybe (normalisedSourceType res) of
+        Just tc -> addTyConMatches tc (vi_rcm vi)
+        Nothing -> addCompleteMatches (vi_rcm vi)
+      pure vi{ vi_rcm = rcm }
+
+    reprTyCon_maybe :: Type -> Maybe TyCon
+    reprTyCon_maybe ty = case splitTyConApp_maybe ty of
+      Nothing          -> Nothing
+      Just (tc, _args) -> case tyConFamInst_maybe tc of
+        Nothing          -> Just tc
+        Just (tc_fam, _) -> Just tc_fam
+
     -- | This is the |-Inst rule from the paper (section 4.5). Tries to
     -- find an inhabitant in every complete set by instantiating with one their
     -- constructors. If there is any complete set where we can't find an
     -- inhabitant, the whole thing is uninhabited.
+    -- See also Note [Implementation of COMPLETE pragmas].
     inst_complete_sets :: VarInfo -> MaybeT DsM VarInfo
-    inst_complete_sets vi@VI{ vi_cache = NoPM }  = pure vi
-    inst_complete_sets vi@VI{ vi_cache = PM ms } = do
-      ms <- traverse (\cs -> inst_complete_set vi cs (uniqDSetToList cs)) ms
-      pure vi{ vi_cache = PM ms }
+    inst_complete_sets vi@VI{ vi_rcm = rcm } = do
+      rcm' <- trvRcm (\cls -> inst_complete_set vi cls (uniqDSetToList cls)) rcm
+      pure vi{ vi_rcm = rcm' }
 
     inst_complete_set :: VarInfo -> ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
     -- (inst_complete_set cs cls) iterates over cls, deleting from cs
@@ -1053,7 +1094,7 @@ ensureInhabited nabla vi = case vi_bot vi of
             ]
 
 -- | Checks if every 'VarInfo' in the term oracle has still an inhabited
--- 'vi_cache', considering the current type information in 'Nabla'.
+-- 'vi_rcm', considering the current type information in 'Nabla'.
 -- This check is necessary after having matched on a GADT con to weed out
 -- impossible matches.
 ensureAllInhabited :: Nabla -> DsM (Maybe Nabla)
@@ -1112,7 +1153,7 @@ equate nabla@MkNabla{ nabla_tm_st = TmSt env reps } x y
         -- Do the same for negative info
         let add_refut nabla nalt = addNotConCt nabla y nalt
         nabla_neg <- foldlM add_refut nabla_pos (pmAltConSetElems (vi_neg vi_x))
-        -- vi_cache will be updated in addNotConCt, so we are good to
+        -- vi_rcm will be updated in addNotConCt, so we are good to
         -- go!
         pure nabla_neg
 
@@ -1124,7 +1165,7 @@ equate nabla@MkNabla{ nabla_tm_st = TmSt env reps } x y
 -- See Note [TmState invariants].
 addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
 addConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x alt tvs args = do
-  let VI ty pos neg bot cache = lookupVarInfo ts x
+  let VI ty pos neg bot rcm = lookupVarInfo ts x
   -- First try to refute with a negative fact
   guard (not (elemPmAltConSet alt neg))
   -- Then see if any of the other solutions (remember: each of them is an
@@ -1143,7 +1184,8 @@ addConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x alt tvs args = do
       MaybeT $ addPmCts nabla (listToBag ty_cts `unionBags` listToBag tm_cts)
     Nothing -> do
       let pos' = (alt, tvs, args):pos
-      let nabla_with bot = nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot cache)) reps}
+      let nabla_with bot =
+            nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot rcm)) reps}
       -- Do (2) in Note [Coverage checking Newtype matches]
       case (alt, args) of
         (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
@@ -1575,7 +1617,7 @@ provideEvidence = go
     try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
     -- Convention: x binds the outer constructor in the chain, y the inner one.
     try_instantiate x xs n nabla = do
-      (_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x)
+      (_src_ty, dcs, rep_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x)
       let build_newtype (x, nabla) (_ty, dc, arg_ty) = do
             y <- lift $ mkPmId arg_ty
             -- Newtypes don't have existentials (yet?!), so passing an empty
@@ -1587,11 +1629,13 @@ provideEvidence = go
         Just (y, newty_nabla) -> do
           -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥.
           let vi = lookupVarInfo (nabla_tm_st newty_nabla) y
-          vi <- initPossibleMatches (nabla_ty_st newty_nabla) vi
-          mb_cls <- pickMinimalCompleteSet newty_nabla (vi_cache vi)
+          rcm <- case splitTyConApp_maybe rep_ty of
+                Nothing      -> pure (vi_rcm vi)
+                Just (tc, _) -> addTyConMatches tc (vi_rcm vi)
+          mb_cls <- pickMinimalCompleteSet rep_ty rcm
           case uniqDSetToList <$> mb_cls of
             Just cls -> do
-              nablas <- instantiate_cons y core_ty xs n newty_nabla cls
+              nablas <- instantiate_cons y rep_ty xs n newty_nabla cls
               if null nablas && vi_bot vi /= IsNotBot
                 then go xs n newty_nabla -- bot is still possible. Display a wildcard!
                 else pure nablas
@@ -1633,13 +1677,15 @@ provideEvidence = go
           other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls
           pure (con_nablas ++ other_cons_nablas)
 
-pickMinimalCompleteSet :: Nabla -> PossibleMatches -> DsM (Maybe ConLikeSet)
-pickMinimalCompleteSet _ NoPM      = pure Nothing
--- TODO: First prune sets with type info in nabla. But this is good enough for
--- now and less costly. See #17386.
-pickMinimalCompleteSet _ (PM clss) = do
-  tracePm "pickMinimalCompleteSet" (ppr $ NonEmpty.toList clss)
-  pure (Just (minimumBy (comparing sizeUniqDSet) clss))
+pickMinimalCompleteSet :: Type -> ResidualCompleteMatches -> DsM (Maybe ConLikeSet)
+pickMinimalCompleteSet ty rcm = do
+  env <- dsGetFamInstEnvs
+  pure $ case filter (all (is_valid env) . uniqDSetToList) (getRcm rcm) of
+    []    -> Nothing
+    clss' -> Just (minimumBy (comparing sizeUniqDSet) clss')
+  where
+    is_valid :: FamInstEnvs -> ConLike -> Bool
+    is_valid env cl = isJust (guessConLikeUnivTyArgsFromResTy env ty cl)
 
 -- | Finds a representant of the semantic equality class of the given @e@.
 -- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index aa778cd34b..eea6130791 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -24,8 +24,8 @@ module GHC.HsToCore.PmCheck.Types (
         literalToPmLit, negatePmLit, overloadPmLit,
         pmLitAsStringLit, coreExprAsPmLit,
 
-        -- * Caching partially matched COMPLETE sets
-        ConLikeSet, PossibleMatches(..),
+        -- * Caching residual COMPLETE sets
+        ConLikeSet, ResidualCompleteMatches(..), getRcm,
 
         -- * PmAltConSet
         PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
@@ -69,10 +69,10 @@ import GHC.Builtin.Names
 import GHC.Builtin.Types
 import GHC.Builtin.Types.Prim
 import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Driver.Types (ConLikeSet)
 
 import Numeric (fromRat)
 import Data.Foldable (find)
-import qualified Data.List.NonEmpty as NonEmpty
 import Data.Ratio
 import qualified Data.Semigroup as Semi
 
@@ -415,21 +415,32 @@ instance Outputable PmAltCon where
 instance Outputable PmEquality where
   ppr = text . show
 
-type ConLikeSet = UniqDSet ConLike
+-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
+-- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
+-- which we already know @x /~ K@ from these sets.
+--
+-- For motivation, see Section 5.3 in Lower Your Guards.
+-- See also Note [Implementation of COMPLETE pragmas]
+data ResidualCompleteMatches
+  = RCM
+  { rcm_vanilla :: !(Maybe ConLikeSet)
+  -- ^ The residual set for the vanilla COMPLETE set from the data defn.
+  -- Tracked separately from 'rcm_pragmas', because it might only be
+  -- known much later (when we have enough type information to see the 'TyCon'
+  -- of the match), or not at all even. Until that happens, it is 'Nothing'.
+  , rcm_pragmas :: !(Maybe [ConLikeSet])
+  -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
+  -- visible when compiling this module. Querying that set with
+  -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
+  -- until first needed in a 'DsM' context.
+  }
 
--- | A data type caching the results of 'completeMatchConLikes' with support for
--- deletion of constructors that were already matched on.
-data PossibleMatches
-  = PM (NonEmpty.NonEmpty ConLikeSet)
-  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE set
-  -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
-  -- set at all, for which we have 'NoPM'.
-  | NoPM
-  -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
+getRcm :: ResidualCompleteMatches -> [ConLikeSet]
+getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
 
-instance Outputable PossibleMatches where
-  ppr (PM cs) = ppr (NonEmpty.toList cs)
-  ppr NoPM = text "<NoPM>"
+instance Outputable ResidualCompleteMatches where
+  -- formats as "[{Nothing,Just},{P,Q}]"
+  ppr rcm = ppr (getRcm rcm)
 
 -- | Either @Indirect x@, meaning the value is represented by that of @x@, or
 -- an @Entry@ containing containing the actual value it represents.
@@ -516,8 +527,8 @@ data TmState
 
 -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
 -- and negative ('vi_neg') facts, like "x is not (:)".
--- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set
--- ('vi_cache').
+-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
+-- ('vi_rcm').
 --
 -- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle".
 data VarInfo
@@ -559,7 +570,7 @@ data VarInfo
   --    * 'IsBot': @x ~ ⊥@
   --    * 'IsNotBot': @x ≁ ⊥@
 
-  , vi_cache :: !PossibleMatches
+  , vi_rcm :: !ResidualCompleteMatches
   -- ^ A cache of the associated COMPLETE sets. At any time a superset of
   -- possible constructors of each COMPLETE set. So, if it's not in here, we
   -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
diff --git a/compiler/GHC/Iface/Load.hs b/compiler/GHC/Iface/Load.hs
index f687bf11a6..85b8b524f6 100644
--- a/compiler/GHC/Iface/Load.hs
+++ b/compiler/GHC/Iface/Load.hs
@@ -38,7 +38,7 @@ import GHC.Prelude
 
 import {-# SOURCE #-} GHC.IfaceToCore
    ( tcIfaceDecl, tcIfaceRules, tcIfaceInst, tcIfaceFamInst
-   , tcIfaceAnnotations, tcIfaceCompleteSigs )
+   , tcIfaceAnnotations, tcIfaceCompleteMatches )
 
 import GHC.Driver.Session
 import GHC.Driver.Backend
@@ -479,7 +479,7 @@ loadInterface doc_str mod from
         ; new_eps_fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
         ; new_eps_rules     <- tcIfaceRules ignore_prags (mi_rules iface)
         ; new_eps_anns      <- tcIfaceAnnotations (mi_anns iface)
-        ; new_eps_complete_sigs <- tcIfaceCompleteSigs (mi_complete_sigs iface)
+        ; new_eps_complete_matches <- tcIfaceCompleteMatches (mi_complete_matches iface)
 
         ; let { final_iface = iface {
                                 mi_decls     = panic "No mi_decls in PIT",
@@ -509,9 +509,7 @@ loadInterface doc_str mod from
                   eps_rule_base    = extendRuleBaseList (eps_rule_base eps)
                                                         new_eps_rules,
                   eps_complete_matches
-                                   = extendCompleteMatchMap
-                                         (eps_complete_matches eps)
-                                         new_eps_complete_sigs,
+                                   = eps_complete_matches eps ++ new_eps_complete_matches,
                   eps_inst_env     = extendInstEnvList (eps_inst_env eps)
                                                        new_eps_insts,
                   eps_fam_inst_env = extendFamInstEnvList (eps_fam_inst_env eps)
@@ -1037,9 +1035,8 @@ initExternalPackageState home_unit
       eps_fam_inst_env     = emptyFamInstEnv,
       eps_rule_base        = mkRuleBase builtinRules',
         -- Initialise the EPS rule pool with the built-in rules
-      eps_mod_fam_inst_env
-                           = emptyModuleEnv,
-      eps_complete_matches = emptyUFM,
+      eps_mod_fam_inst_env = emptyModuleEnv,
+      eps_complete_matches = [],
       eps_ann_env          = emptyAnnEnv,
       eps_stats = EpsStats { n_ifaces_in = 0, n_decls_in = 0, n_decls_out = 0
                            , n_insts_in = 0, n_insts_out = 0
@@ -1181,7 +1178,7 @@ pprModIface iface@ModIface{ mi_final_exts = exts }
         , ppr (mi_warns iface)
         , pprTrustInfo (mi_trust iface)
         , pprTrustPkg (mi_trust_pkg iface)
-        , vcat (map ppr (mi_complete_sigs iface))
+        , vcat (map ppr (mi_complete_matches iface))
         , text "module header:" $$ nest 2 (ppr (mi_doc_hdr iface))
         , text "declaration docs:" $$ nest 2 (ppr (mi_decl_docs iface))
         , text "arg docs:" $$ nest 2 (ppr (mi_arg_docs iface))
diff --git a/compiler/GHC/Iface/Make.hs b/compiler/GHC/Iface/Make.hs
index 3fd0eaac29..941aa4083c 100644
--- a/compiler/GHC/Iface/Make.hs
+++ b/compiler/GHC/Iface/Make.hs
@@ -57,6 +57,7 @@ import GHC.Types.Avail
 import GHC.Types.Name.Reader
 import GHC.Types.Name.Env
 import GHC.Types.Name.Set
+import GHC.Types.Unique.DSet
 import GHC.Unit
 import GHC.Utils.Error
 import GHC.Utils.Outputable
@@ -220,7 +221,7 @@ mkIface_ hsc_env
                       md_anns      = anns,
                       md_types     = type_env,
                       md_exports   = exports,
-                      md_complete_sigs = complete_sigs }
+                      md_complete_matches = complete_matches }
 -- NB:  notice that mkIface does not look at the bindings
 --      only at the TypeEnv.  The previous Tidy phase has
 --      put exactly the info into the TypeEnv that we want
@@ -256,7 +257,7 @@ mkIface_ hsc_env
         iface_fam_insts = map famInstToIfaceFamInst fam_insts
         trust_info  = setSafeMode safe_mode
         annotations = map mkIfaceAnnotation anns
-        icomplete_sigs = map mkIfaceCompleteSig complete_sigs
+        icomplete_matches = map mkIfaceCompleteMatch complete_matches
 
     ModIface {
           mi_module      = this_mod,
@@ -285,7 +286,7 @@ mkIface_ hsc_env
           mi_hpc         = isHpcUsed hpc_info,
           mi_trust       = trust_info,
           mi_trust_pkg   = pkg_trust_req,
-          mi_complete_sigs = icomplete_sigs,
+          mi_complete_matches = icomplete_matches,
           mi_doc_hdr     = doc_hdr,
           mi_decl_docs   = decl_docs,
           mi_arg_docs    = arg_docs,
@@ -322,8 +323,9 @@ mkIface_ hsc_env
 ************************************************************************
 -}
 
-mkIfaceCompleteSig :: CompleteMatch -> IfaceCompleteMatch
-mkIfaceCompleteSig (CompleteMatch cls tc) = IfaceCompleteMatch cls tc
+mkIfaceCompleteMatch :: CompleteMatch -> IfaceCompleteMatch
+mkIfaceCompleteMatch cls =
+  IfaceCompleteMatch (map conLikeName (uniqDSetToList cls))
 
 
 {-
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index b7d8f62401..3def579fb7 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -324,11 +324,11 @@ data IfaceAnnotation
 
 type IfaceAnnTarget = AnnTarget OccName
 
-data IfaceCompleteMatch = IfaceCompleteMatch [IfExtName] IfExtName
+newtype IfaceCompleteMatch = IfaceCompleteMatch [IfExtName]
 
 instance Outputable IfaceCompleteMatch where
-  ppr (IfaceCompleteMatch cls ty) = text "COMPLETE" <> colon <+> ppr cls
-                                                    <+> dcolon <+> ppr ty
+  ppr (IfaceCompleteMatch cls) = text "COMPLETE" <> colon <+> ppr cls
+
 
 
 
@@ -2481,8 +2481,8 @@ instance Binary IfaceTyConParent where
                 return $ IfDataInstance ax pr ty
 
 instance Binary IfaceCompleteMatch where
-  put_ bh (IfaceCompleteMatch cs ts) = put_ bh cs >> put_ bh ts
-  get bh = IfaceCompleteMatch <$> get bh <*> get bh
+  put_ bh (IfaceCompleteMatch cs) = put_ bh cs
+  get bh = IfaceCompleteMatch <$> get bh
 
 
 {-
@@ -2638,7 +2638,7 @@ instance NFData IfaceConAlt where
     IfaceLitAlt lit -> lit `seq` ()
 
 instance NFData IfaceCompleteMatch where
-  rnf (IfaceCompleteMatch f1 f2) = rnf f1 `seq` rnf f2
+  rnf (IfaceCompleteMatch f1) = rnf f1
 
 instance NFData IfaceRule where
   rnf (IfaceRule f1 f2 f3 f4 f5 f6 f7 f8) =
diff --git a/compiler/GHC/Iface/Tidy.hs b/compiler/GHC/Iface/Tidy.hs
index 4afd7517e8..f90abbf921 100644
--- a/compiler/GHC/Iface/Tidy.hs
+++ b/compiler/GHC/Iface/Tidy.hs
@@ -143,7 +143,7 @@ mkBootModDetailsTc hsc_env
                   tcg_patsyns          = pat_syns,
                   tcg_insts            = insts,
                   tcg_fam_insts        = fam_insts,
-                  tcg_complete_matches = complete_sigs,
+                  tcg_complete_matches = complete_matches,
                   tcg_mod              = this_mod
                 }
   = -- This timing isn't terribly useful since the result isn't forced, but
@@ -151,13 +151,13 @@ mkBootModDetailsTc hsc_env
     Err.withTiming dflags
                    (text "CoreTidy"<+>brackets (ppr this_mod))
                    (const ()) $
-    return (ModDetails { md_types         = type_env'
-                       , md_insts         = insts'
-                       , md_fam_insts     = fam_insts
-                       , md_rules         = []
-                       , md_anns          = []
-                       , md_exports       = exports
-                       , md_complete_sigs = complete_sigs
+    return (ModDetails { md_types            = type_env'
+                       , md_insts            = insts'
+                       , md_fam_insts        = fam_insts
+                       , md_rules            = []
+                       , md_anns             = []
+                       , md_exports          = exports
+                       , md_complete_matches = complete_matches
                        })
   where
     dflags = hsc_dflags hsc_env
@@ -346,22 +346,22 @@ three places this is actioned:
 -}
 
 tidyProgram :: HscEnv -> ModGuts -> IO (CgGuts, ModDetails)
-tidyProgram hsc_env  (ModGuts { mg_module    = mod
-                              , mg_exports   = exports
-                              , mg_rdr_env   = rdr_env
-                              , mg_tcs       = tcs
-                              , mg_insts     = cls_insts
-                              , mg_fam_insts = fam_insts
-                              , mg_binds     = binds
-                              , mg_patsyns   = patsyns
-                              , mg_rules     = imp_rules
-                              , mg_anns      = anns
-                              , mg_complete_sigs = complete_sigs
-                              , mg_deps      = deps
-                              , mg_foreign   = foreign_stubs
-                              , mg_foreign_files = foreign_files
-                              , mg_hpc_info  = hpc_info
-                              , mg_modBreaks = modBreaks
+tidyProgram hsc_env  (ModGuts { mg_module           = mod
+                              , mg_exports          = exports
+                              , mg_rdr_env          = rdr_env
+                              , mg_tcs              = tcs
+                              , mg_insts            = cls_insts
+                              , mg_fam_insts        = fam_insts
+                              , mg_binds            = binds
+                              , mg_patsyns          = patsyns
+                              , mg_rules            = imp_rules
+                              , mg_anns             = anns
+                              , mg_complete_matches = complete_matches
+                              , mg_deps             = deps
+                              , mg_foreign          = foreign_stubs
+                              , mg_foreign_files    = foreign_files
+                              , mg_hpc_info         = hpc_info
+                              , mg_modBreaks        = modBreaks
                               })
 
   = Err.withTiming dflags
@@ -467,13 +467,13 @@ tidyProgram hsc_env  (ModGuts { mg_module    = mod
                            cg_modBreaks = modBreaks,
                            cg_spt_entries = spt_entries },
 
-                   ModDetails { md_types     = tidy_type_env,
-                                md_rules     = tidy_rules,
-                                md_insts     = tidy_cls_insts,
-                                md_fam_insts = fam_insts,
-                                md_exports   = exports,
-                                md_anns      = anns,      -- are already tidy
-                                md_complete_sigs = complete_sigs
+                   ModDetails { md_types            = tidy_type_env,
+                                md_rules            = tidy_rules,
+                                md_insts            = tidy_cls_insts,
+                                md_fam_insts        = fam_insts,
+                                md_exports          = exports,
+                                md_anns             = anns,      -- are already tidy
+                                md_complete_matches = complete_matches
                               })
         }
   where
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 52267070de..21749ea6aa 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -17,7 +17,7 @@ module GHC.IfaceToCore (
         typecheckIfacesForMerging,
         typecheckIfaceForInstantiate,
         tcIfaceDecl, tcIfaceInst, tcIfaceFamInst, tcIfaceRules,
-        tcIfaceAnnotations, tcIfaceCompleteSigs,
+        tcIfaceAnnotations, tcIfaceCompleteMatches,
         tcIfaceExpr,    -- Desired by HERMIT (#7683)
         tcIfaceGlobal,
         tcIfaceOneShot
@@ -67,6 +67,7 @@ import GHC.Types.Name.Set
 import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr )
 import GHC.Unit.Module
 import GHC.Types.Unique.FM
+import GHC.Types.Unique.DSet ( mkUniqDSet )
 import GHC.Types.Unique.Supply
 import GHC.Utils.Outputable
 import GHC.Data.Maybe
@@ -179,7 +180,7 @@ typecheckIface iface
         ; exports <- ifaceExportNames (mi_exports iface)
 
                 -- Complete Sigs
-        ; complete_sigs <- tcIfaceCompleteSigs (mi_complete_sigs iface)
+        ; complete_matches <- tcIfaceCompleteMatches (mi_complete_matches iface)
 
                 -- Finished
         ; traceIf (vcat [text "Finished typechecking interface for" <+> ppr (mi_module iface),
@@ -193,7 +194,7 @@ typecheckIface iface
                               , md_rules     = rules
                               , md_anns      = anns
                               , md_exports   = exports
-                              , md_complete_sigs = complete_sigs
+                              , md_complete_matches = complete_matches
                               }
     }
 
@@ -392,14 +393,14 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
         rules     <- tcIfaceRules ignore_prags (mi_rules iface)
         anns      <- tcIfaceAnnotations (mi_anns iface)
         exports   <- ifaceExportNames (mi_exports iface)
-        complete_sigs <- tcIfaceCompleteSigs (mi_complete_sigs iface)
+        complete_matches <- tcIfaceCompleteMatches (mi_complete_matches iface)
         return $ ModDetails { md_types     = type_env
                             , md_insts     = insts
                             , md_fam_insts = fam_insts
                             , md_rules     = rules
                             , md_anns      = anns
                             , md_exports   = exports
-                            , md_complete_sigs = complete_sigs
+                            , md_complete_matches = complete_matches
                             }
     return (global_type_env, details)
 
@@ -431,14 +432,14 @@ typecheckIfaceForInstantiate nsubst iface =
     rules     <- tcIfaceRules ignore_prags (mi_rules iface)
     anns      <- tcIfaceAnnotations (mi_anns iface)
     exports   <- ifaceExportNames (mi_exports iface)
-    complete_sigs <- tcIfaceCompleteSigs (mi_complete_sigs iface)
+    complete_matches <- tcIfaceCompleteMatches (mi_complete_matches iface)
     return $ ModDetails { md_types     = type_env
                         , md_insts     = insts
                         , md_fam_insts = fam_insts
                         , md_rules     = rules
                         , md_anns      = anns
                         , md_exports   = exports
-                        , md_complete_sigs = complete_sigs
+                        , md_complete_matches = complete_matches
                         }
 
 -- Note [Resolving never-exported Names]
@@ -1146,11 +1147,14 @@ tcIfaceAnnTarget (ModuleTarget mod) = do
 ************************************************************************
 -}
 
-tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
-tcIfaceCompleteSigs = mapM tcIfaceCompleteSig
+tcIfaceCompleteMatches :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
+tcIfaceCompleteMatches = mapM tcIfaceCompleteMatch
 
-tcIfaceCompleteSig :: IfaceCompleteMatch -> IfL CompleteMatch
-tcIfaceCompleteSig (IfaceCompleteMatch ms t) = return (CompleteMatch ms t)
+tcIfaceCompleteMatch :: IfaceCompleteMatch -> IfL CompleteMatch
+tcIfaceCompleteMatch (IfaceCompleteMatch ms) =
+  mkUniqDSet <$> mapM (forkM doc . tcIfaceConLike) ms
+  where
+    doc = text "COMPLETE sig" <+> ppr ms
 
 {-
 ************************************************************************
@@ -1759,7 +1763,13 @@ tcIfaceDataCon :: Name -> IfL DataCon
 tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
                          ; case thing of
                                 AConLike (RealDataCon dc) -> return dc
-                                _       -> pprPanic "tcIfaceExtDC" (ppr name$$ ppr thing) }
+                                _       -> pprPanic "tcIfaceDataCon" (ppr name$$ ppr thing) }
+
+tcIfaceConLike :: Name -> IfL ConLike
+tcIfaceConLike name = do { thing <- tcIfaceGlobal name
+                         ; case thing of
+                                AConLike cl -> return cl
+                                _           -> pprPanic "tcIfaceConLike" (ppr name$$ ppr thing) }
 
 tcIfaceExtId :: Name -> IfL Id
 tcIfaceExtId name = do { thing <- tcIfaceGlobal name
diff --git a/compiler/GHC/IfaceToCore.hs-boot b/compiler/GHC/IfaceToCore.hs-boot
index 91b538ef41..349c629835 100644
--- a/compiler/GHC/IfaceToCore.hs-boot
+++ b/compiler/GHC/IfaceToCore.hs-boot
@@ -11,9 +11,9 @@ import GHC.Core         ( CoreRule )
 import GHC.Driver.Types ( CompleteMatch )
 import GHC.Types.Annotations ( Annotation )
 
-tcIfaceDecl         :: Bool -> IfaceDecl -> IfL TyThing
-tcIfaceRules        :: Bool -> [IfaceRule] -> IfL [CoreRule]
-tcIfaceInst         :: IfaceClsInst -> IfL ClsInst
-tcIfaceFamInst      :: IfaceFamInst -> IfL FamInst
-tcIfaceAnnotations  :: [IfaceAnnotation] -> IfL [Annotation]
-tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
+tcIfaceDecl            :: Bool -> IfaceDecl -> IfL TyThing
+tcIfaceRules           :: Bool -> [IfaceRule] -> IfL [CoreRule]
+tcIfaceInst            :: IfaceClsInst -> IfL ClsInst
+tcIfaceFamInst         :: IfaceFamInst -> IfL FamInst
+tcIfaceAnnotations     :: [IfaceAnnotation] -> IfL [Annotation]
+tcIfaceCompleteMatches :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index d52b3dd1cd..af9073c87f 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -44,9 +44,8 @@ import GHC.Tc.Utils.TcMType
 import GHC.Core.Multiplicity
 import GHC.Core.FamInstEnv( normaliseType )
 import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
-import GHC.Core.TyCon
 import GHC.Tc.Utils.TcType
-import GHC.Core.Type (mkStrLitTy, tidyOpenType, splitTyConApp_maybe, mkCastTy)
+import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
 import GHC.Builtin.Types.Prim
 import GHC.Builtin.Types( mkBoxedTupleTy )
 import GHC.Types.Id
@@ -69,9 +68,9 @@ import GHC.Utils.Panic
 import GHC.Builtin.Names( ipClassName )
 import GHC.Tc.Validity (checkValidType)
 import GHC.Types.Unique.FM
+import GHC.Types.Unique.DSet
 import GHC.Types.Unique.Set
 import qualified GHC.LanguageExtensions as LangExt
-import GHC.Core.ConLike
 
 import Control.Monad
 import Data.Foldable (find)
@@ -197,112 +196,22 @@ tcTopBinds binds sigs
         -- The top level bindings are flattened into a giant
         -- implicitly-mutually-recursive LHsBinds
 
-
--- Note [Typechecking Complete Matches]
--- Much like when a user bundled a pattern synonym, the result types of
--- all the constructors in the match pragma must be consistent.
---
--- If we allowed pragmas with inconsistent types then it would be
--- impossible to ever match every constructor in the list and so
--- the pragma would be useless.
-
-
-
-
-
--- This is only used in `tcCompleteSig`. We fold over all the conlikes,
--- this accumulator keeps track of the first `ConLike` with a concrete
--- return type. After fixing the return type, all other constructors with
--- a fixed return type must agree with this.
---
--- The fields of `Fixed` cache the first conlike and its return type so
--- that we can compare all the other conlikes to it. The conlike is
--- stored for error messages.
---
--- `Nothing` in the case that the type is fixed by a type signature
-data CompleteSigType = AcceptAny | Fixed (Maybe ConLike) TyCon
-
 tcCompleteSigs  :: [LSig GhcRn] -> TcM [CompleteMatch]
 tcCompleteSigs sigs =
   let
-      doOne :: Sig GhcRn -> TcM (Maybe CompleteMatch)
-      doOne c@(CompleteMatchSig _ _ lns mtc)
-        = fmap Just $ do
-           addErrCtxt (text "In" <+> ppr c) $
-            case mtc of
-              Nothing -> infer_complete_match
-              Just tc -> check_complete_match tc
-        where
-
-          checkCLTypes acc = foldM checkCLType (acc, []) (unLoc lns)
-
-          infer_complete_match = do
-            (res, cls) <- checkCLTypes AcceptAny
-            case res of
-              AcceptAny -> failWithTc ambiguousError
-              Fixed _ tc  -> return $ mkMatch cls tc
-
-          check_complete_match tc_name = do
-            ty_con <- tcLookupLocatedTyCon tc_name
-            (_, cls) <- checkCLTypes (Fixed Nothing ty_con)
-            return $ mkMatch cls ty_con
-
-          mkMatch :: [ConLike] -> TyCon -> CompleteMatch
-          mkMatch cls ty_con = CompleteMatch {
-            -- foldM is a left-fold and will have accumulated the ConLikes in
-            -- the reverse order. foldrM would accumulate in the correct order,
-            -- but would type-check the last ConLike first, which might also be
-            -- confusing from the user's perspective. Hence reverse here.
-            completeMatchConLikes = reverse (map conLikeName cls),
-            completeMatchTyCon = tyConName ty_con
-            }
+      doOne :: LSig GhcRn -> TcM (Maybe CompleteMatch)
+      -- We don't need to "type-check" COMPLETE signatures anymore; if their
+      -- combinations are invalid it will be found so at match sites. Hence we
+      -- keep '_mtc' only for backwards compatibility.
+      doOne (L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) _mtc))
+        = fmap Just $ setSrcSpan loc $ addErrCtxt (text "In" <+> ppr c) $
+            mkUniqDSet <$> mapM (addLocM tcLookupConLike) ns
       doOne _ = return Nothing
 
-      ambiguousError :: SDoc
-      ambiguousError =
-        text "A type signature must be provided for a set of polymorphic"
-          <+> text "pattern synonyms."
-
-
-      -- See note [Typechecking Complete Matches]
-      checkCLType :: (CompleteSigType, [ConLike]) -> Located Name
-                  -> TcM (CompleteSigType, [ConLike])
-      checkCLType (cst, cs) n = do
-        cl <- addLocM tcLookupConLike n
-        let   (_,_,_,_,_,_, res_ty) = conLikeFullSig cl
-              res_ty_con = fst <$> splitTyConApp_maybe res_ty
-        case (cst, res_ty_con) of
-          (AcceptAny, Nothing) -> return (AcceptAny, cl:cs)
-          (AcceptAny, Just tc) -> return (Fixed (Just cl) tc, cl:cs)
-          (Fixed mfcl tc, Nothing)  -> return (Fixed mfcl tc, cl:cs)
-          (Fixed mfcl tc, Just tc') ->
-            if tc == tc'
-              then return (Fixed mfcl tc, cl:cs)
-              else case mfcl of
-                     Nothing ->
-                      addErrCtxt (text "In" <+> ppr cl) $
-                        failWithTc typeSigErrMsg
-                     Just cl -> failWithTc (errMsg cl)
-             where
-              typeSigErrMsg :: SDoc
-              typeSigErrMsg =
-                text "Couldn't match expected type"
-                      <+> quotes (ppr tc)
-                      <+> text "with"
-                      <+> quotes (ppr tc')
-
-              errMsg :: ConLike -> SDoc
-              errMsg fcl =
-                text "Cannot form a group of complete patterns from patterns"
-                  <+> quotes (ppr fcl) <+> text "and" <+> quotes (ppr cl)
-                  <+> text "as they match different type constructors"
-                  <+> parens (quotes (ppr tc)
-                               <+> text "resp."
-                               <+> quotes (ppr tc'))
   -- For some reason I haven't investigated further, the signatures come in
   -- backwards wrt. declaration order. So we reverse them here, because it makes
   -- a difference for incomplete match suggestions.
-  in  mapMaybeM (addLocM doOne) (reverse sigs) -- process in declaration order
+  in mapMaybeM doOne $ reverse sigs
 
 tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
 -- A hs-boot file has only one BindGroup, and it only has type
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index 0af8bbb2a4..3aea91fe7c 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -45,12 +45,11 @@ module GHC.Tc.Types(
         IdBindingInfo(..), ClosedTypeId, RhsNames,
         IsGroupClosed(..),
         SelfBootInfo(..),
-        pprTcTyThingCategory, pprPECategory, CompleteMatch(..),
+        pprTcTyThingCategory, pprPECategory, CompleteMatch,
 
         -- Desugaring types
         DsM, DsLclEnv(..), DsGblEnv(..),
-        DsMetaEnv, DsMetaVal(..), CompleteMatchMap,
-        mkCompleteMatchMap, extendCompleteMatchMap,
+        DsMetaEnv, DsMetaVal(..), CompleteMatches,
 
         -- Template Haskell
         ThStage(..), SpliceType(..), PendingStuff(..),
@@ -310,7 +309,7 @@ data DsGblEnv
         , ds_msgs    :: IORef Messages          -- Warning messages
         , ds_if_env  :: (IfGblEnv, IfLclEnv)    -- Used for looking up global,
                                                 -- possibly-imported things
-        , ds_complete_matches :: CompleteMatchMap
+        , ds_complete_matches :: CompleteMatches
            -- Additional complete pattern matches
         , ds_cc_st   :: IORef CostCentreState
            -- Tracking indices for cost centre annotations
@@ -602,7 +601,7 @@ data TcGblEnv
         tcg_static_wc :: TcRef WantedConstraints,
           -- ^ Wanted constraints of static forms.
         -- See Note [Constraints in static forms].
-        tcg_complete_matches :: [CompleteMatch],
+        tcg_complete_matches :: !CompleteMatches,
 
         -- ^ Tracking indices for cost centre annotations
         tcg_cc_st   :: TcRef CostCentreState
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index ea20808f98..04db590f4d 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -64,8 +64,8 @@ module GHC.Tc.Utils.Env(
         topIdLvl, isBrackStage,
 
         -- New Ids
-        newDFunName, newFamInstTyConName,
-        newFamInstAxiomName,
+        newDFunName,
+        newFamInstTyConName, newFamInstAxiomName,
         mkStableIdFromString, mkStableIdFromName,
         mkWrapperName
   ) where
diff --git a/docs/users_guide/exts/pragmas.rst b/docs/users_guide/exts/pragmas.rst
index 3c2e3ddb7d..1f6399fb7b 100644
--- a/docs/users_guide/exts/pragmas.rst
+++ b/docs/users_guide/exts/pragmas.rst
@@ -887,29 +887,6 @@ modules. ``COMPLETE`` pragmas should be thought of as asserting a
 universal truth about a set of patterns and as a result, should not be
 used to silence context specific incomplete match warnings.
 
-When specifying a ``COMPLETE`` pragma, the result types of all patterns must
-be consistent with each other. This is a sanity check as it would be impossible
-to match on all the patterns if the types were inconsistent.
-
-The result type must also be unambiguous. Usually this can be inferred but
-when all the pattern synonyms in a group are polymorphic in the constructor
-the user must provide a type signature. ::
-
-    class LL f where
-      go :: f a -> ()
-
-    instance LL [] where
-      go _ = ()
-
-    pattern T :: LL f => f a
-    pattern T <- (go -> ())
-
-    {-# COMPLETE T :: [] #-}
-
-    -- No warning
-    foo :: [a] -> Int
-    foo T = 5
-
 .. _overlap-pragma:
 
 ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig15.hs b/testsuite/tests/pmcheck/complete_sigs/T14422.hs
index 5936379aa7..be879f4b13 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig15.hs
+++ b/testsuite/tests/pmcheck/complete_sigs/T14422.hs
@@ -10,3 +10,6 @@ pattern P :: C f => f a
 pattern P <- (foo -> ())
 
 {-# COMPLETE P #-}
+
+f :: C f => f a -> ()
+f P = () -- A complete match
diff --git a/testsuite/tests/pmcheck/complete_sigs/T18277.hs b/testsuite/tests/pmcheck/complete_sigs/T18277.hs
new file mode 100644
index 0000000000..db09edf65a
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T18277.hs
@@ -0,0 +1,13 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+type List = []
+
+pattern DefinitelyAString :: String -> String
+pattern DefinitelyAString x = x
+{-# COMPLETE DefinitelyAString #-}
+
+f :: String -> String
+f (DefinitelyAString x) = x
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index bc4f39ac39..2728121160 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -1,7 +1,7 @@
 test('completesig01', normal, compile, [''])
 test('completesig02', normal, compile, [''])
 test('Completesig03', normal, multimod_compile, ['Completesig03', '-Wall'])
-test('completesig04', normal, compile_fail, [''])
+test('completesig04', normal, compile, ['-Wincomplete-patterns'])
 test('completesig05', normal, compile, [''])
 test('completesig06', normal, compile, [''])
 test('completesig07', normal, compile, [''])
@@ -12,7 +12,6 @@ test('completesig11', normal, compile, [''])
 test('completesig12', normal, compile, [''])
 test('completesig13', normal, compile, [''])
 test('completesig14', normal, compile, [''])
-test('completesig15', normal, compile_fail, [''])
 test('T13021', normal, compile, [''])
 test('T13363a', normal, compile, [''])
 test('T13363b', normal, compile, [''])
@@ -22,6 +21,8 @@ test('T13965', normal, compile, [''])
 test('T14059a', normal, compile, [''])
 test('T14059b', expect_broken('14059'), compile, [''])
 test('T14253', normal, compile, [''])
+test('T14422', normal, compile, [''])
 test('T14851', normal, compile, [''])
 test('T17149', normal, compile, [''])
 test('T17386', normal, compile, [''])
+test('T18277', normal, compile, [''])
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig04.hs b/testsuite/tests/pmcheck/complete_sigs/completesig04.hs
index dbe1110be1..d8f84cb71d 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig04.hs
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig04.hs
@@ -1,6 +1,12 @@
--- Test that a COMPLETE pragma over constructors of different types fails.
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+-- Test that a COMPLETE pragma over constructors of different types is a valid
+-- declaration, but that it's not suggested in any warning.
 module TyMismatch where
 
-data E = L | R
+data T = A | B | C
 
-{-# COMPLETE Just, L #-}
+{-# COMPLETE Just, A #-}
+
+f A = ()        -- should not suggest 'Just'
+
+g (Just _) = () -- should not suggest 'A'
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig04.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig04.stderr
index 21a6377ba3..a114d0199e 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig04.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig04.stderr
@@ -1,4 +1,11 @@
 
-completesig04.hs:6:1: error:
-    • Cannot form a group of complete patterns from patterns ‘Just’ and ‘L’ as they match different type constructors (‘Maybe’ resp. ‘E’)
-    • In {-# COMPLETE Just, L #-}
+completesig04.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’:
+        Patterns not matched:
+            B
+            C
+
+completesig04.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘g’: Patterns not matched: Nothing
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig15.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig15.stderr
deleted file mode 100644
index 3bff495ebe..0000000000
--- a/testsuite/tests/pmcheck/complete_sigs/completesig15.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-completesig15.hs:12:1: error:
-    • A type signature must be provided for a set of polymorphic pattern synonyms.
-    • In {-# COMPLETE P #-}
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index de0998ba29..e8938be163 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -88,7 +88,7 @@ test('T17112', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17207', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
-test('T17207b', expect_broken(17207), compile,
+test('T17207b', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17208', expect_broken(17208), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])