Fix #13983 by creating a TyConFlavour type, and using it

An error message was referring to a type synonym as a datatype.
Annoyingly, learning that the TyCon over which the error message is
operating is actually a type synonym was previously impossible, since
that code only had access to a TcTyCon, which doesn't retain any
information about what sort of TyCon it is.

To rectify this, I created a new TyConFlavour datatype, intended to
capture roughly what sort of TyCon we're dealing with. I then performing
the necessary plumbing to ensure all TcTyCons have a TyConFlavour, and
propagated this information through to the relevant error message.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #13983

Differential Revision: https://phabricator.haskell.org/D3747

9 files changed, 161 insertions, 66 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 3766c6b114..045a0a1983 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1310,15 +1310,14 @@ tcWildCardBindersX new_wc wc_names thing_inside
 --
 -- This function does not do telescope checking.
 kcHsTyVarBndrs :: Name    -- ^ of the thing being checked
-               -> Bool    -- ^ True <=> the TyCon being kind-checked can be unsaturated
+               -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
                -> Bool    -- ^ True <=> the decl being checked has a CUSK
-               -> Bool    -- ^ True <=> the decl is an open type/data family
                -> Bool    -- ^ True <=> all the hsq_implicit are *kind* vars
                           -- (will give these kind * if -XNoTypeInType)
                -> LHsQTyVars GhcRn
                -> TcM (Kind, r)     -- ^ The result kind, possibly with other info
                -> TcM (TcTyCon, r)  -- ^ A suitably-kinded TcTyCon
-kcHsTyVarBndrs name unsat cusk open_fam all_kind_vars
+kcHsTyVarBndrs name flav cusk all_kind_vars
   (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
           , hsq_dependent = dep_names }) thing_inside
   | cusk
@@ -1353,12 +1352,12 @@ kcHsTyVarBndrs name unsat cusk open_fam all_kind_vars
                                  `unionVarSet` tyCoVarsOfType res_kind
              unmentioned_kvs   = filterOut (`elemVarSet` all_mentioned_tvs)
                                            scoped_kvs
-       ; reportFloatingKvs name all_tc_tvs unmentioned_kvs
+       ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
 
        ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
                             ++ tc_binders
              tycon = mkTcTyCon name final_binders res_kind
-                               unsat (scoped_kvs ++ tc_tvs)
+                               (scoped_kvs ++ tc_tvs) flav
                            -- the tvs contain the binders already
                            -- in scope from an enclosing class, but
                            -- re-adding tvs to the env't doesn't cause
@@ -1374,10 +1373,12 @@ kcHsTyVarBndrs name unsat cusk open_fam all_kind_vars
               bind_telescope hs_tvs thing_inside
        ; let   -- NB: Don't add scoped_kvs to tyConTyVars, because they
                -- must remain lined up with the binders
-             tycon = mkTcTyCon name binders res_kind unsat
-                               (scoped_kvs ++ binderVars binders)
+             tycon = mkTcTyCon name binders res_kind
+                               (scoped_kvs ++ binderVars binders) flav
        ; return (tycon, stuff) }
   where
+    open_fam = tcFlavourIsOpen flav
+
       -- if -XNoTypeInType and we know all the implicits are kind vars,
       -- just give the kind *. This prevents test
       -- dependent/should_fail/KindLevelsB from compiling, as it should
@@ -1741,7 +1742,7 @@ tcTyClTyVars tycon_name thing_inside
           -- See Note [Free-floating kind vars]
        ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
        ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
-       ; checkNoErrs $ reportFloatingKvs tycon_name
+       ; checkNoErrs $ reportFloatingKvs tycon_name (tyConFlavour tycon)
                                          zonked_scoped_tvs still_sig_tvs
 
           -- Add the *unzonked* tyvars to the env't, because those
@@ -2131,11 +2132,12 @@ funAppCtxt fun arg arg_no
        2 (quotes (ppr arg))
 
 -- See Note [Free-floating kind vars]
-reportFloatingKvs :: Name        -- of the tycon
-                  -> [TcTyVar]   -- all tyvars, not necessarily zonked
-                  -> [TcTyVar]   -- floating tyvars
+reportFloatingKvs :: Name         -- of the tycon
+                  -> TyConFlavour -- What sort of TyCon it is
+                  -> [TcTyVar]    -- all tyvars, not necessarily zonked
+                  -> [TcTyVar]    -- floating tyvars
                   -> TcM ()
-reportFloatingKvs tycon_name all_tvs bad_tvs
+reportFloatingKvs tycon_name flav all_tvs bad_tvs
   = unless (null bad_tvs) $  -- don't bother zonking if there's no error
     do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
        ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
@@ -2147,7 +2149,7 @@ reportFloatingKvs tycon_name all_tvs bad_tvs
     report typeintype tidy_all_tvs tidy_bad_tv
       = addErr $
         vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
-               text "is implicitly bound in datatype"
+               text "is implicitly bound in" <+> ppr flav
              , quotes (ppr tycon_name) <> comma <+>
                text "but does not appear as the kind of any"
              , text "of its type variables. Perhaps you meant"
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index d10d8474b5..0d0e16a346 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -950,7 +950,7 @@ tcConArgs :: ConLike -> [TcSigmaType]
 
 tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
-                  (arityErr "constructor" con_like con_arity no_of_args)
+                  (arityErr (text "constructor") con_like con_arity no_of_args)
         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
         ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys
                                               penv thing_inside
@@ -961,7 +961,7 @@ tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
 
 tcConArgs con_like arg_tys (InfixCon p1 p2) penv thing_inside
   = do  { checkTc (con_arity == 2)      -- Check correct arity
-                  (arityErr "constructor" con_like con_arity 2)
+                  (arityErr (text "constructor") con_like con_arity 2)
         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
         ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
                                               penv thing_inside
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index b0f39d358f..4e7c99cde8 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -369,6 +369,7 @@ kcTyClGroup decls
                  kc_binders  = tyConBinders tc
                  kc_res_kind = tyConResKind tc
                  kc_tyvars   = tyConTyVars tc
+                 kc_flav     = tyConFlavour tc
            ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
            ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
 
@@ -382,8 +383,8 @@ kcTyClGroup decls
                   , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)]
 
            ; return (mkTcTyCon name all_binders' kc_res_kind'
-                               (mightBeUnsaturatedTyCon tc)
-                               (tcTyConScopedTyVars tc)) }
+                               (tcTyConScopedTyVars tc)
+                               kc_flav) }
 
     generaliseTCD :: TcTypeEnv
                   -> LTyClDecl GhcRn -> TcM [TcTyCon]
@@ -482,21 +483,26 @@ getInitialKind :: TyClDecl GhcRn
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
   = do { let cusk = hsDeclHasCusk decl
        ; (tycon, inner_prs) <-
-           kcHsTyVarBndrs name True cusk False True ktvs $
+           kcHsTyVarBndrs name ClassFlavour cusk True ktvs $
            do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
               ; return (constraintKind, inner_prs) }
        ; return (extendEnvWithTcTyCon inner_prs tycon) }
 
 getInitialKind decl@(DataDecl { tcdLName = L _ name
                               , tcdTyVars = ktvs
-                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig } })
+                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
+                                                         , dd_ND = new_or_data } })
   = do  { (tycon, _) <-
-           kcHsTyVarBndrs name True (hsDeclHasCusk decl) False True ktvs $
+           kcHsTyVarBndrs name flav (hsDeclHasCusk decl) True ktvs $
            do { res_k <- case m_sig of
                            Just ksig -> tcLHsKindSig ksig
                            Nothing   -> return liftedTypeKind
               ; return (res_k, ()) }
         ; return (mkTcTyConEnv tycon) }
+  where
+    flav = case new_or_data of
+             NewType  -> NewtypeFlavour
+             DataType -> DataTypeFlavour
 
 getInitialKind (FamDecl { tcdFam = decl })
   = getFamDeclInitialKind Nothing decl
@@ -504,8 +510,9 @@ getInitialKind (FamDecl { tcdFam = decl })
 getInitialKind decl@(SynDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdRhs = rhs })
-  = do  { (tycon, _) <- kcHsTyVarBndrs name False (hsDeclHasCusk decl)
-                            False {- not open -} True ktvs $
+  = do  { (tycon, _) <- kcHsTyVarBndrs name TypeSynonymFlavour
+                            (hsDeclHasCusk decl)
+                            True ktvs $
             do  { res_k <- case kind_annotation rhs of
                             Nothing -> newMetaKindVar
                             Just ksig -> tcLHsKindSig ksig
@@ -534,12 +541,12 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                                , fdResultSig = L _ resultSig
                                                , fdInfo      = info })
   = do { (tycon, _) <-
-           kcHsTyVarBndrs name unsat cusk open True ktvs $
+           kcHsTyVarBndrs name flav cusk True ktvs $
            do { res_k <- case resultSig of
                       KindSig ki                        -> tcLHsKindSig ki
                       TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki
                       _ -- open type families have * return kind by default
-                        | open                     -> return liftedTypeKind
+                        | tcFlavourIsOpen flav     -> return liftedTypeKind
                         -- closed type families have their return kind inferred
                         -- by default
                         | otherwise                -> newMetaKindVar
@@ -547,10 +554,10 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
        ; return (mkTcTyConEnv tycon) }
   where
     cusk  = famDeclHasCusk mb_cusk decl
-    (open, unsat) = case info of
-      DataFamily         -> (True,  True)
-      OpenTypeFamily     -> (True,  False)
-      ClosedTypeFamily _ -> (False, False)
+    flav  = case info of
+      DataFamily         -> DataFamilyFlavour
+      OpenTypeFamily     -> OpenTypeFamilyFlavour
+      ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
 
 ------------------------------------------------------------------------
 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
@@ -616,8 +623,10 @@ kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
   = addErrCtxt (dataConCtxtName [name]) $
          -- the 'False' says that the existentials don't have a CUSK, as the
          -- concept doesn't really apply here. We just need to bring the variables
-         -- into scope.
-    do { _ <- kcHsTyVarBndrs (unLoc name) False False False False
+         -- into scope. (Similarly, the choice of PromotedDataConFlavour isn't
+         -- particularly important.)
+    do { _ <- kcHsTyVarBndrs (unLoc name) PromotedDataConFlavour
+                             False False
                              ((fromMaybe emptyLHsQTvs ex_tvs)) $
               do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
                  ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
@@ -3101,7 +3110,7 @@ addTyConCtxt tc
   = addErrCtxt ctxt
   where
     name = getName tc
-    flav = text (tyConFlavour tc)
+    flav = ppr (tyConFlavour tc)
     ctxt = hsep [ text "In the", flav
                 , text "declaration for", quotes (ppr name) ]
 
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 4c2d1693e4..4f7507745e 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -987,7 +987,7 @@ tyConArityErr :: TyCon -> [TcType] -> SDoc
 -- ignoring the /invisible/ arguments, which the user does not see.
 -- (e.g. Trac #10516)
 tyConArityErr tc tks
-  = arityErr (tyConFlavour tc) (tyConName tc)
+  = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
              tc_type_arity tc_type_args
   where
     vis_tks = filterOutInvisibleTypes tc tks
@@ -997,9 +997,9 @@ tyConArityErr tc tks
     tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
     tc_type_args  = length vis_tks
 
-arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
+arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
 arityErr what name n m
-  = hsep [ text "The" <+> text what, quotes (ppr name), text "should have",
+  = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
            n_arguments <> comma, text "but has been given",
            if m==0 then text "none" else int m]
     where
@@ -1281,7 +1281,7 @@ checkValidInstance ctxt hs_type ty
   = failWithTc (text "Instance head is not headed by a class")
 
   | isNothing mb_cls
-  = failWithTc (vcat [ text "Illegal instance for a" <+> text (tyConFlavour tc)
+  = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
                      , text "A class instance must be for a class" ])
 
   | not arity_ok
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 7b433fab9e..1be318d96a 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -13,7 +13,7 @@ module TyCon(
         TyCon, AlgTyConRhs(..), visibleDataCons,
         AlgTyConFlav(..), isNoParent,
         FamTyConFlav(..), Role(..), Injectivity(..),
-        RuntimeRepInfo(..),
+        RuntimeRepInfo(..), TyConFlavour(..),
 
         -- * TyConBinder
         TyConBinder, TyConBndrVis(..),
@@ -103,6 +103,9 @@ module TyCon(
         newTyConCo, newTyConCo_maybe,
         pprPromotionQuote, mkTyConKind,
 
+        -- ** Predicated on TyConFlavours
+        tcFlavourCanBeUnsaturated, tcFlavourIsOpen,
+
         -- * Runtime type representation
         TyConRepName, tyConRepName_maybe,
         mkPrelTyConRepName,
@@ -722,7 +725,6 @@ data TyCon
   | TcTyCon {
         tyConUnique :: Unique,
         tyConName   :: Name,
-        tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?
 
         -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyConBinder], -- ^ Full binders
@@ -731,8 +733,10 @@ data TyCon
         tyConKind    :: Kind,             -- ^ Kind of this TyCon
         tyConArity   :: Arity,            -- ^ Arity
 
-        tcTyConScopedTyVars :: [TyVar] -- ^ Scoped tyvars over the
-                                       -- tycon's body. See Note [TcTyCon]
+        tcTyConScopedTyVars :: [TyVar], -- ^ Scoped tyvars over the
+                                        -- tycon's body. See Note [TcTyCon]
+        tcTyConFlavour :: TyConFlavour
+                           -- ^ What sort of 'TyCon' this represents.
       }
 
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
@@ -1052,7 +1056,7 @@ so the coercion tycon CoT must have
 
 Note [TcTyCon]
 ~~~~~~~~~~~~~~
-TcTyCons are used for tow distinct purposes
+TcTyCons are used for two distinct purposes
 
 1.  When recovering from a type error in a type declaration,
     we want to put the erroneous TyCon in the environment in a
@@ -1456,19 +1460,19 @@ mkSumTyCon name binders res_kind arity tyvars cons parent
 mkTcTyCon :: Name
           -> [TyConBinder]
           -> Kind                -- ^ /result/ kind only
-          -> Bool                -- ^ Can this be unsaturated?
           -> [TyVar]             -- ^ Scoped type variables, see Note [TcTyCon]
+          -> TyConFlavour        -- ^ What sort of 'TyCon' this represents
           -> TyCon
-mkTcTyCon name binders res_kind unsat scoped_tvs
+mkTcTyCon name binders res_kind scoped_tvs flav
   = TcTyCon { tyConUnique  = getUnique name
             , tyConName    = name
             , tyConTyVars  = binderVars binders
             , tyConBinders = binders
             , tyConResKind = res_kind
             , tyConKind    = mkTyConKind binders res_kind
-            , tyConUnsat   = unsat
             , tyConArity   = length binders
-            , tcTyConScopedTyVars = scoped_tvs }
+            , tcTyConScopedTyVars = scoped_tvs
+            , tcTyConFlavour      = flav }
 
 -- | Create an unlifted primitive 'TyCon', such as @Int#@.
 mkPrimTyCon :: Name -> [TyConBinder]
@@ -1587,7 +1591,8 @@ makeRecoveryTyCon :: TyCon -> TyCon
 makeRecoveryTyCon tc
   = mkTcTyCon (tyConName tc)
               (tyConBinders tc) (tyConResKind tc)
-              (mightBeUnsaturatedTyCon tc) [{- no scoped vars -}]
+              [{- no scoped vars -}]
+              (tyConFlavour tc)
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
 isPrimTyCon :: TyCon -> Bool
@@ -1798,10 +1803,7 @@ isFamFreeTyCon _                                          = True
 -- type synonym, because you should probably have expanded it first
 -- But regardless, it's not decomposable
 mightBeUnsaturatedTyCon :: TyCon -> Bool
-mightBeUnsaturatedTyCon (SynonymTyCon {})                  = False
-mightBeUnsaturatedTyCon (FamilyTyCon  { famTcFlav = flav}) = isDataFamFlav flav
-mightBeUnsaturatedTyCon (TcTyCon { tyConUnsat = unsat })   = unsat
-mightBeUnsaturatedTyCon _other                             = True
+mightBeUnsaturatedTyCon = tcFlavourCanBeUnsaturated . tyConFlavour
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
@@ -2271,26 +2273,92 @@ instance Outputable TyCon where
   -- corresponding TyCon, so we add the quote to distinguish it here
   ppr tc = pprPromotionQuote tc <> ppr (tyConName tc)
 
-tyConFlavour :: TyCon -> String
+-- | Paints a picture of what a 'TyCon' represents, in broad strokes.
+-- This is used towards more informative error messages.
+data TyConFlavour
+  = ClassFlavour
+  | TupleFlavour Boxity
+  | SumFlavour
+  | DataTypeFlavour
+  | NewtypeFlavour
+  | AbstractTypeFlavour
+  | DataFamilyFlavour
+  | OpenTypeFamilyFlavour
+  | ClosedTypeFamilyFlavour
+  | TypeSynonymFlavour
+  | BuiltInTypeFlavour -- ^ e.g., the @(->)@ 'TyCon'.
+  | PromotedDataConFlavour
+  deriving Eq
+
+instance Outputable TyConFlavour where
+  ppr = text . go
+    where
+      go ClassFlavour = "class"
+      go (TupleFlavour boxed) | isBoxed boxed = "tuple"
+                              | otherwise     = "unboxed tuple"
+      go SumFlavour              = "unboxed sum"
+      go DataTypeFlavour         = "data type"
+      go NewtypeFlavour          = "newtype"
+      go AbstractTypeFlavour     = "abstract type"
+      go DataFamilyFlavour       = "data family"
+      go OpenTypeFamilyFlavour   = "type family"
+      go ClosedTypeFamilyFlavour = "type family"
+      go TypeSynonymFlavour      = "type synonym"
+      go BuiltInTypeFlavour      = "built-in type"
+      go PromotedDataConFlavour  = "promoted data constructor"
+
+tyConFlavour :: TyCon -> TyConFlavour
 tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
-  | ClassTyCon _ _ <- parent = "class"
+  | ClassTyCon _ _ <- parent = ClassFlavour
   | otherwise = case rhs of
                   TupleTyCon { tup_sort = sort }
-                     | isBoxed (tupleSortBoxity sort) -> "tuple"
-                     | otherwise                      -> "unboxed tuple"
-                  SumTyCon {}        -> "unboxed sum"
-                  DataTyCon {}       -> "data type"
-                  NewTyCon {}        -> "newtype"
-                  AbstractTyCon {}   -> "abstract type"
+                                     -> TupleFlavour (tupleSortBoxity sort)
+                  SumTyCon {}        -> SumFlavour
+                  DataTyCon {}       -> DataTypeFlavour
+                  NewTyCon {}        -> NewtypeFlavour
+                  AbstractTyCon {}   -> AbstractTypeFlavour
 tyConFlavour (FamilyTyCon { famTcFlav = flav })
-  | isDataFamFlav flav            = "data family"
-  | otherwise                     = "type family"
-tyConFlavour (SynonymTyCon {})    = "type synonym"
-tyConFlavour (FunTyCon {})        = "built-in type"
-tyConFlavour (PrimTyCon {})       = "built-in type"
-tyConFlavour (PromotedDataCon {}) = "promoted data constructor"
-tyConFlavour tc@(TcTyCon {})
-  = pprPanic "tyConFlavour sees a TcTyCon" (ppr tc)
+  = case flav of
+      DataFamilyTyCon{}            -> DataFamilyFlavour
+      OpenSynFamilyTyCon           -> OpenTypeFamilyFlavour
+      ClosedSynFamilyTyCon{}       -> ClosedTypeFamilyFlavour
+      AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour
+      BuiltInSynFamTyCon{}         -> ClosedTypeFamilyFlavour
+tyConFlavour (SynonymTyCon {})    = TypeSynonymFlavour
+tyConFlavour (FunTyCon {})        = BuiltInTypeFlavour
+tyConFlavour (PrimTyCon {})       = BuiltInTypeFlavour
+tyConFlavour (PromotedDataCon {}) = PromotedDataConFlavour
+tyConFlavour (TcTyCon { tcTyConFlavour = flav }) = flav
+
+-- | Can this flavour of 'TyCon' appear unsaturated?
+tcFlavourCanBeUnsaturated :: TyConFlavour -> Bool
+tcFlavourCanBeUnsaturated ClassFlavour            = True
+tcFlavourCanBeUnsaturated DataTypeFlavour         = True
+tcFlavourCanBeUnsaturated NewtypeFlavour          = True
+tcFlavourCanBeUnsaturated DataFamilyFlavour       = True
+tcFlavourCanBeUnsaturated TupleFlavour{}          = True
+tcFlavourCanBeUnsaturated SumFlavour              = True
+tcFlavourCanBeUnsaturated AbstractTypeFlavour     = True
+tcFlavourCanBeUnsaturated BuiltInTypeFlavour      = True
+tcFlavourCanBeUnsaturated PromotedDataConFlavour  = True
+tcFlavourCanBeUnsaturated TypeSynonymFlavour      = False
+tcFlavourCanBeUnsaturated OpenTypeFamilyFlavour   = False
+tcFlavourCanBeUnsaturated ClosedTypeFamilyFlavour = False
+
+-- | Is this flavour of 'TyCon' an open type family or a data family?
+tcFlavourIsOpen :: TyConFlavour -> Bool
+tcFlavourIsOpen DataFamilyFlavour       = True
+tcFlavourIsOpen OpenTypeFamilyFlavour   = True
+tcFlavourIsOpen ClosedTypeFamilyFlavour = False
+tcFlavourIsOpen ClassFlavour            = False
+tcFlavourIsOpen DataTypeFlavour         = False
+tcFlavourIsOpen NewtypeFlavour          = False
+tcFlavourIsOpen TupleFlavour{}          = False
+tcFlavourIsOpen SumFlavour              = False
+tcFlavourIsOpen AbstractTypeFlavour     = False
+tcFlavourIsOpen BuiltInTypeFlavour      = False
+tcFlavourIsOpen PromotedDataConFlavour  = False
+tcFlavourIsOpen TypeSynonymFlavour      = False
 
 pprPromotionQuote :: TyCon -> SDoc
 -- Promoted data constructors already have a tick in their OccName
diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr
index ad8a55b70a..c218cff153 100644
--- a/testsuite/tests/ghci/scripts/T7873.stderr
+++ b/testsuite/tests/ghci/scripts/T7873.stderr
@@ -1,6 +1,6 @@
 
 <interactive>:2:1: error:
-    Kind variable ‘k’ is implicitly bound in datatype
+    Kind variable ‘k’ is implicitly bound in data type
     ‘D1’, but does not appear as the kind of any
     of its type variables. Perhaps you meant
     to bind it explicitly somewhere?
diff --git a/testsuite/tests/typecheck/should_fail/T13983.hs b/testsuite/tests/typecheck/should_fail/T13983.hs
new file mode 100644
index 0000000000..b74a484397
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13983.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T13983 where
+
+import Data.Proxy
+
+type Wat = forall (a :: k). Proxy a
diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr
new file mode 100644
index 0000000000..65ce607961
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13983.stderr
@@ -0,0 +1,8 @@
+
+T13983.hs:7:1: error:
+    • Kind variable ‘k’ is implicitly bound in type synonym
+      ‘Wat’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+      Type variables with inferred kinds: (k :: *)
+    • In the type declaration for ‘Wat’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 2ac572f8c0..254e04b55d 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -445,3 +445,4 @@ test('T13640', normal, compile_fail, [''])
 test('T13677', normal, compile_fail, [''])
 test('T13821A', expect_broken(13821), run_command, ['$MAKE -s --no-print-directory T13821A'])
 test('T13821B', expect_broken(13821), backpack_typecheck_fail, [''])
+test('T13983', normal, compile_fail, [''])