An initial attempt at type-directed COMPLETE pragmas.wip/T14422

Implement some suggestions from Sebastian Graf

Fix a test, add another

cmScrutineeType -> cmResultType, and change/add documentation

Simplify PmAltConSet to not include type information

31 files changed, 225 insertions, 129 deletions

diff --git a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
index 7516a56995..64e880b375 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
@@ -62,9 +62,8 @@ import GHC.Builtin.Types.Prim
 import GHC.Tc.Solver.Monad (InertSet, emptyInert)
 import GHC.Tc.Utils.TcType (isStringTy)
 import GHC.Types.CompleteMatch (CompleteMatch(..))
-import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
-                            , fractionalLitFromRational
-                            , FractionalExponentBase(..))
+import GHC.Types.SourceText (mkFractionalLit, FractionalLit, fractionalLitFromRational,
+  FractionalExponentBase(..), SourceText(..))
 import Numeric (fromRat)
 import Data.Foldable (find)
 import Data.Ratio
@@ -379,8 +378,8 @@ isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits
 -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
 -- the given 'PmAltCon' according to 'eqPmAltCon'.
 elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
-elemPmAltConSet (PmAltConLike cl) (PACS cls _   ) = elementOfUniqDSet cl cls
-elemPmAltConSet (PmAltLit lit)    (PACS _   lits) = elem lit lits
+elemPmAltConSet (PmAltConLike cl) (PACS cls _) = elementOfUniqDSet cl cls
+elemPmAltConSet (PmAltLit lit) (PACS _ lits) = elem lit lits
 
 extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
 extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index d3453fcd56..13865103b6 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1133,11 +1133,13 @@ repPhases (ActiveAfter _ i)  = do { MkC arg <- coreIntLit i
 repPhases _                  = dataCon allPhasesDataConName
 
 rep_complete_sig :: Located [Located Name]
-                 -> Maybe (Located Name)
+                 -> Maybe (HsPatSigType GhcRn)
                  -> SrcSpan
                  -> MetaM [(SrcSpan, Core (M TH.Dec))]
 rep_complete_sig (L _ cls) mty loc
-  = do { mty' <- repMaybe nameTyConName lookupLOcc mty
+  = do { qTyCon <- lift $ dsLookupTyCon qTyConName
+       ; typeTy <- lookupType typeTyConName
+       ; mty' <- repMaybeT (mkTyConApp qTyCon [typeTy]) (repLTy . hsPatSigType) mty
        ; cls' <- repList nameTyConName lookupLOcc cls
        ; sig <- repPragComplete cls' mty'
        ; return [(loc, sig)] }
@@ -2595,7 +2597,7 @@ repPragSpecInl (MkC nm) (MkC ty) (MkC inline) (MkC phases)
 repPragSpecInst :: Core (M TH.Type) -> MetaM (Core (M TH.Dec))
 repPragSpecInst (MkC ty) = rep2 pragSpecInstDName [ty]
 
-repPragComplete :: Core [TH.Name] -> Core (Maybe TH.Name) -> MetaM (Core (M TH.Dec))
+repPragComplete :: Core [TH.Name] -> Core (Maybe (M TH.Type)) -> MetaM (Core (M TH.Dec))
 repPragComplete (MkC cls) (MkC mty) = rep2 pragCompleteDName [cls, mty]
 
 repPragRule :: Core String -> Core (Maybe [(M (TH.TyVarBndr ()))])
@@ -2945,11 +2947,13 @@ coreStringLit s = do { z <- mkStringExpr s; return(MkC z) }
 
 ------------------- Maybe ------------------
 
+{- -- Presently unused.
 repMaybe :: Name -> (a -> MetaM (Core b))
                     -> Maybe a -> MetaM (Core (Maybe b))
 repMaybe tc_name f m = do
   t <- lookupType tc_name
   repMaybeT t f m
+-}
 
 repMaybeT :: Type -> (a -> MetaM (Core b))
                     -> Maybe a -> MetaM (Core (Maybe b))
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index 3fe14085a9..8f7482fa9e 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -1638,7 +1638,7 @@ instance HiePass p => ToHie (SigContext (Located (Sig (GhcPass p)))) where
         CompleteMatchSig _ _ (L ispan names) typ ->
           [ locOnly ispan
           , toHie $ map (C Use) names
-          , toHie $ fmap (C Use) typ
+          , toHie $ fmap (TS (ResolvedScopes [])) typ
           ]
 
 instance ToHie (TScoped (Located (HsSigType GhcRn))) where
diff --git a/compiler/GHC/Iface/Make.hs b/compiler/GHC/Iface/Make.hs
index 53f0032f28..5c06edbfd9 100644
--- a/compiler/GHC/Iface/Make.hs
+++ b/compiler/GHC/Iface/Make.hs
@@ -348,8 +348,8 @@ mkIface_ hsc_env
 -}
 
 mkIfaceCompleteMatch :: CompleteMatch -> IfaceCompleteMatch
-mkIfaceCompleteMatch (CompleteMatch cls mtc) =
-  IfaceCompleteMatch (map conLikeName (uniqDSetToList cls)) (toIfaceTyCon <$> mtc)
+mkIfaceCompleteMatch (CompleteMatch cls mty) =
+  IfaceCompleteMatch (map conLikeName (uniqDSetToList cls)) (fmap toIfaceType mty)
 
 
 {-
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index 21b4274cc7..baaa4c28a3 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -325,12 +325,12 @@ data IfaceAnnotation
 
 type IfaceAnnTarget = AnnTarget OccName
 
-data IfaceCompleteMatch = IfaceCompleteMatch [IfExtName] (Maybe IfaceTyCon)
+data IfaceCompleteMatch = IfaceCompleteMatch [IfExtName] (Maybe IfaceType)
 
 instance Outputable IfaceCompleteMatch where
-  ppr (IfaceCompleteMatch cls mtc) = text "COMPLETE" <> colon <+> ppr cls <+> case mtc of
+  ppr (IfaceCompleteMatch cls mty) = text "COMPLETE" <> colon <+> ppr cls <+> case mty of
     Nothing -> empty
-    Just tc -> dcolon <+> ppr tc
+    Just ty -> dcolon <+> ppr ty
 
 -- Here's a tricky case:
 --   * Compile with -O module A, and B which imports A.f
@@ -2491,7 +2491,7 @@ instance Binary IfaceTyConParent where
                 return $ IfDataInstance ax pr ty
 
 instance Binary IfaceCompleteMatch where
-  put_ bh (IfaceCompleteMatch cs mtc) = put_ bh cs >> put_ bh mtc
+  put_ bh (IfaceCompleteMatch cs mty) = put_ bh cs >> put_ bh mty
   get bh = IfaceCompleteMatch <$> get bh <*> get bh
 
 
@@ -2651,7 +2651,7 @@ instance NFData IfaceConAlt where
     IfaceLitAlt lit -> lit `seq` ()
 
 instance NFData IfaceCompleteMatch where
-  rnf (IfaceCompleteMatch f1 mtc) = rnf f1 `seq` rnf mtc
+  rnf (IfaceCompleteMatch f1 mty) = rnf f1 `seq` rnf mty
 
 instance NFData IfaceRule where
   rnf (IfaceRule f1 f2 f3 f4 f5 f6 f7 f8) =
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 76079ae8ff..99e89b0fd1 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1281,10 +1281,10 @@ tcIfaceCompleteMatches :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
 tcIfaceCompleteMatches = mapM tcIfaceCompleteMatch
 
 tcIfaceCompleteMatch :: IfaceCompleteMatch -> IfL CompleteMatch
-tcIfaceCompleteMatch (IfaceCompleteMatch ms mtc) = do
+tcIfaceCompleteMatch (IfaceCompleteMatch ms mty) = do
   conlikes <- mkUniqDSet <$> mapM (forkM doc . tcIfaceConLike) ms
-  mtc' <- traverse tcIfaceTyCon mtc
-  return (CompleteMatch conlikes mtc')
+  mty' <- traverse tcIfaceType mty
+  return (CompleteMatch conlikes mty')
   where
     doc = text "COMPLETE sig" <+> ppr ms
 
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index ff380f8c75..c8cf8c6c6a 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -1978,10 +1978,6 @@ opt_sig :: { ([AddAnn], Maybe (LHsType GhcPs)) }
         : {- empty -}                   { ([],Nothing) }
         | '::' ctype                    { ([mu AnnDcolon $1],Just $2) }
 
-opt_tyconsig :: { ([AddAnn], Maybe (Located RdrName)) }
-             : {- empty -}              { ([], Nothing) }
-             | '::' gtycon              { ([mu AnnDcolon $1], Just $2) }
-
 -- Like ktype, but for types that obey the forall-or-nothing rule.
 -- See Note [forall-or-nothing rule] in GHC.Hs.Type.
 sigktype :: { LHsSigType GhcPs }
@@ -1997,6 +1993,10 @@ sigktype :: { LHsSigType GhcPs }
 sigtype :: { LHsSigType GhcPs }
         : ctype                            { hsTypeToHsSigType $1 }
 
+opt_patsigtype :: { ([AddAnn], Maybe (HsPatSigType GhcPs)) }
+  : {- empty -}   { ([], Nothing) }
+  | '::' type     { ([mu AnnDcolon $1], Just (mkHsPatSigType $2)) }
+
 sig_vars :: { Located [Located RdrName] }    -- Returned in reversed order
          : sig_vars ',' var           {% addAnnotation (gl $ head $ unLoc $1)
                                                        AnnComma (gl $2)
@@ -2521,7 +2521,7 @@ sigdecl :: { LHsDecl GhcPs }
 
         | pattern_synonym_sig   { sLL $1 $> . SigD noExtField . unLoc $ $1 }
 
-        | '{-# COMPLETE' con_list opt_tyconsig  '#-}'
+        | '{-# COMPLETE' con_list opt_patsigtype '#-}'
                 {% let (dcolon, tc) = $3
                    in ams
                        (sLL $1 $>
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index fdcf89104f..385fc52ce8 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -1032,29 +1032,19 @@ renameSig ctxt sig@(SCCFunSig _ st v s)
 
 -- COMPLETE Sigs can refer to imported IDs which is why we use
 -- lookupLocatedOccRn rather than lookupSigOccRn
-renameSig _ctxt sig@(CompleteMatchSig _ s (L l bf) mty)
+renameSig _ctxt (CompleteMatchSig _ s (L l bf) mty)
   = do new_bf <- traverse lookupLocatedOccRn bf
-       new_mty  <- traverse lookupLocatedOccRn mty
-
-       this_mod <- fmap tcg_mod getGblEnv
-       unless (any (nameIsLocalOrFrom this_mod . unLoc) new_bf) $
-         -- Why 'any'? See Note [Orphan COMPLETE pragmas]
-         addErrCtxt (text "In" <+> ppr sig) $ failWithTc orphanError
-
+       let doc = GenericCtx (text "the scrutinee type signature of a COMPLETE pragma")
+       new_mty <- traverse (rnHsCompletePragType doc) mty
        return (CompleteMatchSig noExtField s (L l new_bf) new_mty, emptyFVs)
-  where
-    orphanError :: SDoc
-    orphanError =
-      text "Orphan COMPLETE pragmas not supported" $$
-      text "A COMPLETE pragma must mention at least one data constructor" $$
-      text "or pattern synonym defined in the same module."
 
 {-
 Note [Orphan COMPLETE pragmas]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We define a COMPLETE pragma to be a non-orphan if it includes at least
-one conlike defined in the current module. Why is this sufficient?
-Well if you have a pattern match
+one conlike defined in the current module, or if the specified type that
+it applies to is defined in the current module. Why is this sufficient?
+Well, with respect to the conlikes, if you have a pattern match
 
   case expr of
     P1 -> ...
@@ -1062,8 +1052,11 @@ Well if you have a pattern match
     P3 -> ...
 
 any COMPLETE pragma which mentions a conlike other than P1, P2 or P3
-will not be of any use in verifying that the pattern match is
-exhaustive. So as we have certainly read the interface files that
+(or which explicitly specifies a type other than the type being
+deconstructed) will not be of any use in verifying that the pattern
+match is exhaustive.
+
+So as we have certainly read the interface files that
 define P1, P2 and P3, we will have loaded all non-orphan COMPLETE
 pragmas that could be relevant to this pattern match.
 
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 8634d5939f..b0f239d6e3 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -13,6 +13,7 @@ module GHC.Rename.HsType (
         rnHsType, rnLHsType, rnLHsTypes, rnContext,
         rnHsKind, rnLHsKind, rnLHsTypeArgs,
         rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
+        rnHsCompletePragType,
         HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
         newTyVarNameRn,
         rnConDeclFields,
@@ -138,6 +139,25 @@ rnHsSigWcType doc (HsWC { hswc_body =
                       , sig_bndrs = outer_bndrs', sig_body = body_ty' }}
               , fvs) } }
 
+rnHsCompletePragType :: HsDocContext
+                     -> HsPatSigType GhcPs
+                     -> RnM (HsPatSigType GhcRn)
+-- Simplified version of rnHsPatSigType used for scrutinee types in COMPLETE pragmas.
+-- Doesn't check for any extensions.
+-- All type variables and wildcards are allowed but we don't keep track of the free type variables, since
+-- they never scope over anything further.
+rnHsCompletePragType ctx sig_ty
+  = do { let free_vars = extractHsTyRdrTyVars pat_sig_ty
+       ; (res, _) <- rnImplicitTvOccs Nothing free_vars $ \ imp_tvs ->
+            do { (nwcs, pat_sig_ty', fvs1) <- rnWcBody ctx [] pat_sig_ty
+               ; let sig_names = HsPSRn { hsps_nwcs = nwcs, hsps_imp_tvs = imp_tvs }
+                     sig_ty'   = HsPS { hsps_ext = sig_names, hsps_body = pat_sig_ty' }
+               ; return (sig_ty', fvs1) }
+       ; return res
+       }
+  where
+    pat_sig_ty = hsPatSigType sig_ty
+
 rnHsPatSigType :: HsPatSigTypeScoping
                -> HsDocContext
                -> HsPatSigType GhcPs
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 0ab561a0a7..4d4e1cc385 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE TypeFamilies        #-}
 
 {-
@@ -50,6 +49,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
 import GHC.Builtin.Types ( mkBoxedTupleTy )
 import GHC.Builtin.Types.Prim
+import GHC.Types.CompleteMatch
 import GHC.Types.SourceText
 import GHC.Types.Id
 import GHC.Types.Var as Var
@@ -66,7 +66,6 @@ import GHC.Data.Graph.Directed
 import GHC.Data.Maybe
 import GHC.Utils.Misc
 import GHC.Types.Basic
-import GHC.Types.CompleteMatch
 import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
 import GHC.Builtin.Names( ipClassName )
@@ -202,17 +201,27 @@ tcTopBinds binds sigs
 
 tcCompleteSigs  :: [LSig GhcRn] -> TcM [CompleteMatch]
 tcCompleteSigs sigs =
-  let
+  let orphanError :: SDoc
+      orphanError =
+        text "Orphan COMPLETE pragmas not supported" $$
+        text "A COMPLETE pragma must mention at least one data constructor" $$
+        text "or pattern synonym defined in the same module."
+
       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.
-      -- There it is also where we consider if the type of the pattern match is
-      -- compatible with the result type constructor 'mb_tc'.
-      doOne (L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) mb_tc_nm))
-        = fmap Just $ setSrcSpan loc $ addErrCtxt (text "In" <+> ppr c) $ do
-            cls   <- mkUniqDSet <$> mapM (addLocM tcLookupConLike) ns
-            mb_tc <- traverse @Maybe tcLookupLocatedTyCon mb_tc_nm
-            pure CompleteMatch { cmConLikes = cls, cmResultTyCon = mb_tc }
+      doOne (L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) mty))
+        = do this_mod <- fmap tcg_mod getGblEnv
+             mt <- forM mty $ \ty -> do
+               (_,_,t) <- tcHsPatSigType CompletePragCtxt HM_FamPat ty OpenKind
+               return t
+
+             fmap Just $ setSrcSpan loc $ addErrCtxt (text "In" <+> ppr c) $ do
+               -- Check if this COMPLETE pragma is an orphan.
+               unless (any (nameIsLocalOrFrom this_mod . unLoc) ns || any (nameSetAny (nameIsLocalOrFrom this_mod) . orphNamesOfType) mt) $
+                 -- Why 'any'? See Note [Orphan COMPLETE pragmas]
+                 failWithTc orphanError
+               -- Look up the ConLikes mentioned
+               conlikes <- mkUniqDSet <$> mapM (addLocM tcLookupConLike) ns
+               return (CompleteMatch { cmConLikes = conlikes, cmResultType = mt })
       doOne _ = return Nothing
 
   -- For some reason I haven't investigated further, the signatures come in
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 648bf5ce12..16a4a24467 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -109,6 +109,7 @@ data UserTypeCtxt
   | DataKindCtxt Name   -- The kind of a data/newtype (instance)
   | TySynKindCtxt Name  -- The kind of the RHS of a type synonym
   | TyFamResKindCtxt Name   -- The result kind of a type family
+  | CompletePragCtxt    -- The scrutinee type of a COMPLETE pragma
 
 {-
 -- Notes re TySynCtxt
@@ -150,6 +151,7 @@ pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type va
 pprUserTypeCtxt (DataKindCtxt n)  = text "the kind annotation on the declaration for" <+> quotes (ppr n)
 pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
 pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n)
+pprUserTypeCtxt CompletePragCtxt  = text "the scrutinee type of a COMPLETE pragma"
 
 isSigMaybe :: UserTypeCtxt -> Maybe Name
 isSigMaybe (FunSigCtxt n _) = Just n
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index f446b69634..c10e29fa80 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -377,6 +377,7 @@ checkValidType ctxt ty
                  DataKindCtxt _      -> rank1
                  TySynKindCtxt _     -> rank1
                  TyFamResKindCtxt _  -> rank1
+                 CompletePragCtxt -> rank1
 
                  _              -> panic "checkValidType"
                                           -- Can't happen; not used for *user* sigs
@@ -507,6 +508,7 @@ typeOrKindCtxt (SigmaCtxt {})       = OnlyTypeCtxt
 typeOrKindCtxt (DataTyCtxt {})      = OnlyTypeCtxt
 typeOrKindCtxt (DerivClauseCtxt {}) = OnlyTypeCtxt
 typeOrKindCtxt (ConArgCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (CompletePragCtxt {}) = OnlyTypeCtxt
   -- Although data constructors can be promoted with DataKinds, we always
   -- validity-check them as though they are the types of terms. We may need
   -- to revisit this decision if we ever allow visible dependent quantification
@@ -1376,6 +1378,7 @@ okIPCtxt (TyVarBndrKindCtxt {}) = False
 okIPCtxt (DataKindCtxt {})      = False
 okIPCtxt (TySynKindCtxt {})     = False
 okIPCtxt (TyFamResKindCtxt {})  = False
+okIPCtxt (CompletePragCtxt {})  = False
 
 {-
 Note [Kind polymorphic type classes]
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 12f65d36ca..4ae63d19c3 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -827,9 +827,9 @@ cvtPragmaD (LineP line file)
        }
 cvtPragmaD (CompleteP cls mty)
   = do { cls' <- noLoc <$> mapM cNameL cls
-       ; mty' <- traverse tconNameL mty
+       ; mty' <- traverse cvtType mty
        ; returnJustL $ Hs.SigD noExtField
-                   $ CompleteMatchSig noExtField NoSourceText cls' mty' }
+                   $ CompleteMatchSig noExtField NoSourceText cls' (fmap mkHsPatSigType mty') }
 
 dfltActivation :: TH.Inline -> Activation
 dfltActivation TH.NoInline = NeverActive
diff --git a/compiler/GHC/Types/CompleteMatch.hs b/compiler/GHC/Types/CompleteMatch.hs
index 43216eba12..9070082ac6 100644
--- a/compiler/GHC/Types/CompleteMatch.hs
+++ b/compiler/GHC/Types/CompleteMatch.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE TypeApplications #-}
-
 -- | COMPLETE signature
 module GHC.Types.CompleteMatch where
 
@@ -7,20 +5,22 @@ import GHC.Prelude
 import GHC.Core.TyCo.Rep
 import GHC.Types.Unique.DSet
 import GHC.Core.ConLike
-import GHC.Core.TyCon
-import GHC.Core.Type ( splitTyConApp_maybe )
 import GHC.Utils.Outputable
+import GHC.Core.Unify
+
+import Data.Maybe
 
 -- | A list of conlikes which represents a complete pattern match.
 -- These arise from @COMPLETE@ signatures.
 -- See also Note [Implementation of COMPLETE pragmas].
 data CompleteMatch = CompleteMatch
   { cmConLikes :: UniqDSet ConLike -- ^ The set of `ConLike` values
-  , cmResultTyCon :: Maybe TyCon   -- ^ The optional, concrete result TyCon the set applies to
+  , cmResultType :: Maybe Type -- ^ A type to be unified with the type of the scrutinee of a pattern match to determine if this pragma applies to the given match.
+                               -- It should be a type which is possibly the type of result of each of the constructors, though at present, we don't check this.
   }
 
 vanillaCompleteMatch :: UniqDSet ConLike -> CompleteMatch
-vanillaCompleteMatch cls = CompleteMatch { cmConLikes = cls, cmResultTyCon = Nothing }
+vanillaCompleteMatch cls = CompleteMatch { cmConLikes = cls, cmResultType = Nothing }
 
 instance Outputable CompleteMatch where
   ppr (CompleteMatch cls mty) = case mty of
@@ -30,11 +30,5 @@ instance Outputable CompleteMatch where
 type CompleteMatches = [CompleteMatch]
 
 completeMatchAppliesAtType :: Type -> CompleteMatch -> Bool
-completeMatchAppliesAtType ty cm = all @Maybe ty_matches (cmResultTyCon cm)
-  where
-    ty_matches sig_tc
-      | Just (tc, _arg_tys) <- splitTyConApp_maybe ty
-      , tc == sig_tc
-      = True
-      | otherwise
-      = False
+completeMatchAppliesAtType ty cm = all (isJust . (\t -> tcUnifyTyKi t ty)) (cmResultType cm)
+ -- NB: We're using all (from Foldable) on a Maybe here.
diff --git a/compiler/Language/Haskell/Syntax/Binds.hs b/compiler/Language/Haskell/Syntax/Binds.hs
index 6f7283be86..b2c7c4ab09 100644
--- a/compiler/Language/Haskell/Syntax/Binds.hs
+++ b/compiler/Language/Haskell/Syntax/Binds.hs
@@ -780,7 +780,7 @@ data Sig pass
   | CompleteMatchSig (XCompleteMatchSig pass)
                      SourceText
                      (XRec pass [LIdP pass])
-                     (Maybe (LIdP pass))
+                     (Maybe (HsPatSigType pass))
   | XSig !(XXSig pass)
 
 -- | Located Fixity Signature
diff --git a/docs/users_guide/exts/pragmas.rst b/docs/users_guide/exts/pragmas.rst
index fd0127f54a..83e35fc021 100644
--- a/docs/users_guide/exts/pragmas.rst
+++ b/docs/users_guide/exts/pragmas.rst
@@ -887,12 +887,12 @@ 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.
 
-It is also possible to restrict the types to which a ``COMPLETE`` pragma applies
-by putting a double colon ``::`` after the list of constructors, followed by a
-result type constructor, which will be used to restrict the cases in which the
-pragma applies. GHC will compare the annotated result type constructor with the
-type constructor in the head of the scrutinee type in a pattern match to see if
-the ``COMPLETE`` pragma is meant to apply to it.
+It is also possible to restrict the types to which a ``COMPLETE`` pragma
+applies by putting a double colon ``::`` after the list of constructors,
+followed by a result type, which will be used to restrict the cases
+in which the pragma applies. GHC will attempt to unify that result type
+with the type of the scrutinee in a pattern match to see if the
+``COMPLETE`` pragma is meant to apply to it.
 
 This is especially useful in cases that the constructors specified are
 polymorphic, e.g.::
@@ -923,8 +923,8 @@ polymorphic, e.g.::
       isCons [] = Nothing
       isCons (x:xs) = Just (x,xs)
 
-    {-# COMPLETE Empty :: Proxy #-}
-    {-# COMPLETE Empty, Cons :: [] #-}
+    {-# COMPLETE Empty :: Proxy a #-}
+    {-# COMPLETE Empty, Cons :: [a] #-}
 
     foo :: Proxy a -> Int
     foo Empty = 0
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
index 67017d4926..25b7062da8 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
@@ -513,8 +513,14 @@ pragAnnD target expr
 pragLineD :: Quote m => Int -> String -> m Dec
 pragLineD line file = pure $ PragmaD $ LineP line file
 
-pragCompleteD :: Quote m => [Name] -> Maybe Name -> m Dec
-pragCompleteD cls mty = pure $ PragmaD $ CompleteP cls mty
+pragCompleteD :: Quote m => [Name] -> Maybe (m Type) -> m Dec
+pragCompleteD cls mty =
+  case mty of
+    Nothing -> pure $ PragmaD $ CompleteP cls Nothing
+    Just ty ->
+      do
+        t <- ty
+        pure $ PragmaD $ CompleteP cls (Just t)
 
 dataInstD :: Quote m => m Cxt -> (Maybe [m (TyVarBndr ())]) -> m Type -> Maybe (m Kind) -> [m Con]
           -> [m DerivClause] -> m Dec
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index 6508c07a65..3dad480bc2 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -2355,7 +2355,7 @@ data Pragma = InlineP         Name Inline RuleMatch Phases
             | RuleP           String (Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases
             | AnnP            AnnTarget Exp
             | LineP           Int String
-            | CompleteP       [Name] (Maybe Name)
+            | CompleteP       [Name] (Maybe Type)
                 -- ^ @{ {\-\# COMPLETE C_1, ..., C_i [ :: T ] \#-} }@
         deriving( Show, Eq, Ord, Data, Generic )
 
diff --git a/libraries/template-haskell/tests/pragCompletePpr.hs b/libraries/template-haskell/tests/pragCompletePpr.hs
index cb06cdb10d..60fd477667 100644
--- a/libraries/template-haskell/tests/pragCompletePpr.hs
+++ b/libraries/template-haskell/tests/pragCompletePpr.hs
@@ -1,7 +1,7 @@
 module Main (main) where
 
 import Language.Haskell.TH.Ppr    (ppr)
-import Language.Haskell.TH.Syntax (Dec (PragmaD), Pragma (CompleteP), mkName)
+import Language.Haskell.TH.Syntax (Dec (PragmaD), Pragma (CompleteP), mkName, Type(ConT))
 
 main :: IO ()
-main = print $ ppr $ PragmaD $ CompleteP [mkName "Foo", mkName "Bar"] $ Just $ mkName "Bar"
+main = print $ ppr $ PragmaD $ CompleteP [mkName "Foo", mkName "Bar"] $ Just (ConT (mkName "Bar"))
diff --git a/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.hs b/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.hs
new file mode 100644
index 0000000000..da007177e5
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+import Data.Functor.Identity
+
+newtype App f x = App (f x)
+
+class WrappedIn s a | s -> a where
+  unwrap :: s -> a
+
+instance WrappedIn (App f a) (f a) where
+  unwrap (App fa) = fa
+
+pattern Unwrapped :: WrappedIn s a => a -> s
+pattern Unwrapped x <- (unwrap -> x)
+
+{-# COMPLETE Unwrapped :: App t #-}
+
+boom :: App Identity t -> Bool
+boom (Unwrapped (Identity _)) = True
+
+main :: IO ()
+main = print ":)"
diff --git a/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.stderr b/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.stderr
new file mode 100644
index 0000000000..324ec48a65
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/CompletePragmaKindError.stderr
@@ -0,0 +1,6 @@
+
+CompletePragmaKindError.hs:21:27: error:
+    • Expecting one more argument to ‘App t’
+      Expected a type, but ‘App t’ has kind ‘* -> *’
+    • In the type ‘App t’
+      In the scrutinee type of a COMPLETE pragma: App t
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14422.hs b/testsuite/tests/pmcheck/complete_sigs/T14422.hs
index eb0f728baa..be879f4b13 100644
--- a/testsuite/tests/pmcheck/complete_sigs/T14422.hs
+++ b/testsuite/tests/pmcheck/complete_sigs/T14422.hs
@@ -1,7 +1,7 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
-module T14422 where
+module Completesig15 where
 
 class C f where
   foo :: f a -> ()
@@ -13,33 +13,3 @@ pattern P <- (foo -> ())
 
 f :: C f => f a -> ()
 f P = () -- A complete match
-
--- But we also have to be able to constrain applicability of a COMPLETE sig.
--- Hence another example:
-
-class D f where
-  bar :: f a -> ()
-
-pattern Q :: D f => f a
-pattern Q <- (bar -> ())
-
-instance D [] where
-  bar _ = ()
-{-# COMPLETE Q :: [] #-}
-
-g :: D f => f a -> ()
-g Q = () -- Should warn! The sig shouldn't apply in a polymorphic context.
-
-h :: [a] -> ()
-h Q = () -- A complete match
-
--- What currently isn't possible (although, yet):
-class D f => E f where
-  -- Law: every match on 'Q' is COMPLETE
-
--- Commented out, because it's invalid syntax ATM.
--- {-# Q :: E f => f a #-}
-
-i :: E f => f a -> ()
-i Q = () -- Would be a complete match with GHC proposal #400
-
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14422.stderr b/testsuite/tests/pmcheck/complete_sigs/T14422.stderr
deleted file mode 100644
index 26a03573ae..0000000000
--- a/testsuite/tests/pmcheck/complete_sigs/T14422.stderr
+++ /dev/null
@@ -1,8 +0,0 @@
-
-T14422.hs:31:1: warning: [-Wincomplete-patterns (in -Wextra)]
-    Pattern match(es) are non-exhaustive
-    In an equation for ‘g’: Patterns of type ‘f a’ not matched: P
-
-T14422.hs:44:1: warning: [-Wincomplete-patterns (in -Wextra)]
-    Pattern match(es) are non-exhaustive
-    In an equation for ‘i’: Patterns of type ‘f a’ not matched: P
diff --git a/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.hs b/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.hs
new file mode 100644
index 0000000000..e88c686116
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module TypeDirectedComplete where
+
+data Proxy a = Proxy
+
+class IsEmpty a where
+  isEmpty :: a -> Bool
+
+class IsCons a where
+  type Elt a
+  isCons :: a -> Maybe (Elt a, a)
+
+pattern Empty :: IsEmpty a => a
+pattern Empty <- (isEmpty -> True)
+
+pattern Cons :: IsCons a => Elt a -> a -> a
+pattern Cons x xs <- (isCons -> Just (x,xs))
+
+instance IsEmpty (Proxy a) where
+  isEmpty Proxy = True
+
+instance IsEmpty [a] where
+  isEmpty = null
+
+instance IsCons [a] where
+  type Elt [a] = a
+  isCons [] = Nothing
+  isCons (x:xs) = Just (x,xs)
+
+{-# COMPLETE Empty :: Proxy a #-}
+{-# COMPLETE Empty, Cons :: [a] #-}
+
+foo :: Proxy a -> Int
+foo Empty = 0
+
+bar :: [a] -> Int
+bar Empty = 0
+bar (Cons _ _) = 1
+
+baz :: [a] -> Int
+baz Empty = 0
diff --git a/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.stderr b/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.stderr
new file mode 100644
index 0000000000..a711f179bf
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/TypeDirectedComplete.stderr
@@ -0,0 +1,5 @@
+
+TypeDirectedComplete.hs:45:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘baz’:
+        Patterns of type ‘[a]’ not matched: Cons _ _
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index 49ed3c62bc..5d0a51f0cf 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -28,3 +28,5 @@ test('T17386', normal, compile, [''])
 test('T18277', normal, compile, [''])
 test('T18960', normal, compile, [''])
 test('T18960b', normal, compile, [''])
+test('CompletePragmaKindError', normal, compile_fail, [''])
+test('TypeDirectedComplete', normal, compile, [''])
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig13.hs b/testsuite/tests/pmcheck/complete_sigs/completesig13.hs
index e545ef8d9b..8e922bdc32 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig13.hs
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig13.hs
@@ -1,8 +1,9 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wall #-}
-module Completesig13 where
+module Completesig11 where
 
 class LL f where
   go :: f a -> ()
@@ -13,7 +14,18 @@ instance LL [] where
 pattern T :: LL f => f a
 pattern T <- (go -> ())
 
-{-# COMPLETE T :: [] #-}
+{-# COMPLETE T :: [a] #-}
 
-foo :: [a] -> Int
+-- No warning should be generated here
+foo :: [t] -> Int
 foo T = 5
+
+data List a = Nil | Cons a (List a)
+
+instance LL List where
+  go _ = ()
+
+-- This should be warned about, since the COMPLETE pragma above only applies to
+-- the Prelude [] type, not List.
+bar :: List t -> Int
+bar T = 5
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig13.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig13.stderr
new file mode 100644
index 0000000000..e7e12f8394
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig13.stderr
@@ -0,0 +1,7 @@
+
+completesig13.hs:31:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘bar’:
+        Patterns of type ‘List t’ not matched:
+            Nil
+            Cons _ _
diff --git a/testsuite/tests/pmcheck/should_compile/T17112.hs b/testsuite/tests/pmcheck/should_compile/T17112.hs
index a6755f71fc..5668257e9b 100644
--- a/testsuite/tests/pmcheck/should_compile/T17112.hs
+++ b/testsuite/tests/pmcheck/should_compile/T17112.hs
@@ -23,7 +23,7 @@ instance WrappedIn (App f a) (f a) where
 
 pattern Unwrapped :: WrappedIn s a => a -> s
 pattern Unwrapped x <- (unwrap -> x)
-{-# COMPLETE Unwrapped :: App #-}
+{-# COMPLETE Unwrapped :: App f x #-}
 
 boom :: HideArg (App Identity) -> Bool
 boom (HideArg (Unwrapped (Identity _))) = True
diff --git a/testsuite/tests/pmcheck/should_compile/T17207b.hs b/testsuite/tests/pmcheck/should_compile/T17207b.hs
index 1649eea3ff..406011d672 100644
--- a/testsuite/tests/pmcheck/should_compile/T17207b.hs
+++ b/testsuite/tests/pmcheck/should_compile/T17207b.hs
@@ -14,7 +14,7 @@ pattern B <- (const False -> True)
 pattern C :: a
 pattern C <- (const True -> True)
 
-{-# COMPLETE B, C :: T #-}
+{-# COMPLETE B, C :: T t #-}
 
 f :: a :~: () -> T a -> ()
 f _    B = ()
diff --git a/testsuite/tests/th/T13098.hs b/testsuite/tests/th/T13098.hs
index e6a541cc55..21409197de 100644
--- a/testsuite/tests/th/T13098.hs
+++ b/testsuite/tests/th/T13098.hs
@@ -19,7 +19,7 @@ $([d| class LL f where
       pattern T2 :: LL f => f a
       pattern T2 <- (go -> ())
 
-      {-# COMPLETE T2 :: [] #-}
+      {-# COMPLETE T2 :: [a] #-}
 
       -- No warning
       foo :: [a] -> Int