Tidying could cause ill-kinded types

I found (Trac #14175) that the tidying we do when reporting
type error messages could cause a well-kinded type to become
ill-kinded. Reason: we initialised the tidy-env with a
completely un-zonked TidyEnv accumulated in the TcLclEnv
as we come across lexical type-varialbe bindings.

Solution: zonk them.

But I ended up refactoring a bit:

* Get rid of tcl_tidy :: TidyEnv altogether

* Instead use tcl_bndrs :: TcBinderStack
  This used to contain only Ids, but now I've added those
  lexically scoped TyVars too.

* Change names:
     TcIdBinderStack -> TcBinderStack
     TcIdBinder      -> TcBinder
     extendTcIdBndrs -> extendTcBinderStack

* Now tcInitTidyEnv can grab those TyVars from the
  tcl_bndrs, zonk, and tidy them.

The only annoyance is that I had to add TcEnv.hs-boot, to
break the recursion between the zonking code and the
TrRnMonad functions like addErrTc that call tcInitTidyEnv.
Tiresome, but in fact that file existed already.

10 files changed, 127 insertions, 81 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 1f5a3cf671..24173eb574 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -408,7 +408,7 @@ tcValBinds top_lvl binds sigs thing_inside
 
                 -- Extend the envt right away with all the Ids
                 -- declared with complete type signatures
-                -- Do not extend the TcIdBinderStack; instead
+                -- Do not extend the TcBinderStack; instead
                 -- we extend it on a per-rhs basis in tcExtendForRhs
         ; tcExtendSigIds top_lvl poly_ids $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
@@ -702,7 +702,7 @@ tcPolyCheck prag_fn
 
        ; (ev_binds, (co_fn, matches'))
             <- checkConstraints skol_info skol_tvs ev_vars $
-               tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel]  $
+               tcExtendBinderStack [TcIdBndr mono_id NotTopLevel]  $
                tcExtendTyVarEnv2 tv_prs $
                setSrcSpan loc           $
                tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau)
@@ -1282,7 +1282,7 @@ tcMonoBinds is_rec sig_fn no_gen
             <- tcInferInst $ \ exp_ty ->
                   -- tcInferInst: see TcUnify,
                   -- Note [Deep instantiation of InferResult]
-               tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
+               tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
                   -- type of the thing whose rhs we are type checking
@@ -1470,7 +1470,7 @@ tcExtendTyVarEnvFromSig sig_inst thing_inside
     thing_inside
 
 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
--- Extend the TcIdBinderStack for the RHS of the binding, with
+-- Extend the TcBinderStack for the RHS of the binding, with
 -- the monomorphic Id.  That way, if we have, say
 --     f = \x -> blah
 -- and something goes wrong in 'blah', we get a "relevant binding"
@@ -1479,12 +1479,12 @@ tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
 --    f :: forall a. [a] -> [a]
 --    f x = True
 -- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
--- If we had the *polymorphic* version of f in the TcIdBinderStack, it
+-- If we had the *polymorphic* version of f in the TcBinderStack, it
 -- would not be reported as relevant, because its type is closed
 tcExtendIdBinderStackForRhs infos thing_inside
-  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
-                    | MBI { mbi_mono_id = mono_id } <- infos ]
-                    thing_inside
+  = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
+                        | MBI { mbi_mono_id = mono_id } <- infos ]
+                        thing_inside
     -- NotTopLevel: it's a monomorphic binding
 
 ---------------------
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 4a271345fb..087643deba 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -30,7 +30,7 @@ module TcEnv(
         tcExtendTyVarEnv, tcExtendTyVarEnv2,
         tcExtendLetEnv, tcExtendSigIds, tcExtendRecIds,
         tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
-        tcExtendIdBndrs, tcExtendLocalTypeEnv,
+        tcExtendBinderStack, tcExtendLocalTypeEnv,
         isTypeClosedLetBndr,
 
         tcLookup, tcLookupLocated, tcLookupLocalIds,
@@ -43,6 +43,9 @@ module TcEnv(
         getTypeSigNames,
         tcExtendRecEnv,         -- For knot-tying
 
+        -- Tidying
+        tcInitTidyEnv, tcInitOpenTidyEnv,
+
         -- Instances
         tcLookupInstance, tcGetInstEnvs,
 
@@ -85,6 +88,7 @@ import DataCon ( DataCon )
 import PatSyn  ( PatSyn )
 import ConLike
 import TyCon
+import Type
 import CoAxiom
 import Class
 import Name
@@ -398,23 +402,11 @@ tcExtendTyVarEnv2 binds thing_inside
   -- thus, no coercion variables
   = do { tc_extend_local_env NotTopLevel
                     [(name, ATyVar name tv) | (name, tv) <- binds] $
-         do { env <- getLclEnv
-            ; let env' = env { tcl_tidy = add_tidy_tvs (tcl_tidy env) }
-            ; setLclEnv env' thing_inside }}
+         tcExtendBinderStack tv_binds $
+         thing_inside }
   where
-    add_tidy_tvs env = foldl add env binds
-
-    -- We initialise the "tidy-env", used for tidying types before printing,
-    -- by building a reverse map from the in-scope type variables to the
-    -- OccName that the programmer originally used for them
-    add :: TidyEnv -> (Name, TcTyVar) -> TidyEnv
-    add (env,subst) (name, tyvar)
-        = ASSERT( isTyVar tyvar )
-          case tidyOccName env (nameOccName name) of
-            (env', occ') ->  (env', extendVarEnv subst tyvar tyvar')
-                where
-                  tyvar' = setTyVarName tyvar name'
-                  name'  = tidyNameOcc name occ'
+    tv_binds :: [TcBinder]
+    tv_binds = [TcTvBndr name tv | (name,tv) <- binds]
 
 isTypeClosedLetBndr :: Id -> Bool
 -- See Note [Bindings with closed types] in TcRnTypes
@@ -423,7 +415,7 @@ isTypeClosedLetBndr = noFreeVarsOfType . idType
 tcExtendRecIds :: [(Name, TcId)] -> TcM a -> TcM a
 -- Used for binding the recurive uses of Ids in a binding
 -- both top-level value bindings and and nested let/where-bindings
--- Does not extend the TcIdBinderStack
+-- Does not extend the TcBinderStack
 tcExtendRecIds pairs thing_inside
   = tc_extend_local_env NotTopLevel
           [ (name, ATcId { tct_id   = let_id
@@ -433,7 +425,7 @@ tcExtendRecIds pairs thing_inside
 
 tcExtendSigIds :: TopLevelFlag -> [TcId] -> TcM a -> TcM a
 -- Used for binding the Ids that have a complete user type signature
--- Does not extend the TcIdBinderStack
+-- Does not extend the TcBinderStack
 tcExtendSigIds top_lvl sig_ids thing_inside
   = tc_extend_local_env top_lvl
           [ (idName id, ATcId { tct_id   = id
@@ -447,10 +439,10 @@ tcExtendSigIds top_lvl sig_ids thing_inside
 tcExtendLetEnv :: TopLevelFlag -> TcSigFun -> IsGroupClosed
                   -> [TcId] -> TcM a -> TcM a
 -- Used for both top-level value bindings and and nested let/where-bindings
--- Adds to the TcIdBinderStack too
+-- Adds to the TcBinderStack too
 tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
                ids thing_inside
-  = tcExtendIdBndrs [TcIdBndr id top_lvl | id <- ids] $
+  = tcExtendBinderStack [TcIdBndr id top_lvl | id <- ids] $
     tc_extend_local_env top_lvl
           [ (idName id, ATcId { tct_id   = id
                               , tct_info = mk_tct_info id })
@@ -468,7 +460,7 @@ tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
 
 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
 -- For lambda-bound and case-bound Ids
--- Extends the the TcIdBinderStack as well
+-- Extends the the TcBinderStack as well
 tcExtendIdEnv ids thing_inside
   = tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
 
@@ -479,8 +471,8 @@ tcExtendIdEnv1 name id thing_inside
 
 tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
 tcExtendIdEnv2 names_w_ids thing_inside
-  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
-                    | (_,mono_id) <- names_w_ids ] $
+  = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
+                        | (_,mono_id) <- names_w_ids ] $
     tc_extend_local_env NotTopLevel
             [ (name, ATcId { tct_id = id
                            , tct_info    = NotLetBound })
@@ -560,15 +552,51 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
         --
         -- Nor must we generalise g over any kind variables free in r's kind
 
--------------------------------------------------------------
--- Extending the TcIdBinderStack, used only for error messages
 
-tcExtendIdBndrs :: [TcIdBinder] -> TcM a -> TcM a
-tcExtendIdBndrs bndrs thing_inside
-  = do { traceTc "tcExtendIdBndrs" (ppr bndrs)
+{- *********************************************************************
+*                                                                      *
+             The TcBinderStack
+*                                                                      *
+********************************************************************* -}
+
+tcExtendBinderStack :: [TcBinder] -> TcM a -> TcM a
+tcExtendBinderStack bndrs thing_inside
+  = do { traceTc "tcExtendBinderStack" (ppr bndrs)
        ; updLclEnv (\env -> env { tcl_bndrs = bndrs ++ tcl_bndrs env })
                    thing_inside }
 
+tcInitTidyEnv :: TcM TidyEnv
+-- We initialise the "tidy-env", used for tidying types before printing,
+-- by building a reverse map from the in-scope type variables to the
+-- OccName that the programmer originally used for them
+tcInitTidyEnv
+  = do  { lcl_env <- getLclEnv
+        ; go emptyTidyEnv (tcl_bndrs lcl_env) }
+  where
+    go (env, subst) []
+      = return (env, subst)
+    go (env, subst) (b : bs)
+      | TcTvBndr name tyvar <- b
+       = do { let (env', occ') = tidyOccName env (nameOccName name)
+                  name'  = tidyNameOcc name occ'
+                  tyvar1 = setTyVarName tyvar name'
+            ; tyvar2 <- zonkTcTyVarToTyVar tyvar1
+              -- Be sure to zonk here!  Tidying applies to zonked
+              -- types, so if we don't zonk we may create an
+              -- ill-kinded type (Trac #14175)
+            ; go (env', extendVarEnv subst tyvar tyvar2) bs }
+      | otherwise
+      = go (env, subst) bs
+
+-- | Get a 'TidyEnv' that includes mappings for all vars free in the given
+-- type. Useful when tidying open types.
+tcInitOpenTidyEnv :: [TyCoVar] -> TcM TidyEnv
+tcInitOpenTidyEnv tvs
+  = do { env1 <- tcInitTidyEnv
+       ; let env2 = tidyFreeTyCoVars env1 tvs
+       ; return env2 }
+
+
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcEnv.hs-boot b/compiler/typecheck/TcEnv.hs-boot
index 8cc90ae5a0..5e9bfe2039 100644
--- a/compiler/typecheck/TcEnv.hs-boot
+++ b/compiler/typecheck/TcEnv.hs-boot
@@ -1,7 +1,10 @@
-{-
->module TcEnv where
->import TcRnTypes
->import HsExtension ( GhcTcId, IdP )
->
->tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
--}
+module TcEnv where
+
+import TcRnTypes( TcM )
+import VarEnv( TidyEnv )
+
+-- Annoyingly, there's a recursion between tcInitTidyEnv
+-- (which does zonking and hence needs TcMType) and
+-- addErrTc etc which live in TcRnMonad.  Rats.
+tcInitTidyEnv :: TcM TidyEnv
+
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 85d5404588..7db611f85f 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -13,6 +13,7 @@ import TcRnTypes
 import TcRnMonad
 import TcMType
 import TcUnify( occCheckForErrors, OccCheckResult(..) )
+import TcEnv( tcInitTidyEnv )
 import TcType
 import RnUnbound ( unknownNameSuggestions )
 import Type
@@ -196,6 +197,7 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes
 
        ; traceTc "reportUnsolved (after zonking):" $
          vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
+              , text "Tidy env:" <+> ppr tidy_env
               , text "Wanted:" <+> ppr wanted ]
 
        ; warn_redundant <- woptM Opt_WarnRedundantConstraints
@@ -442,6 +444,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
                                        , text "Insols =" <+> ppr insols
                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)])
        ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
+       ; traceTc "rw2" (ppr tidy_cts)
 
          -- First deal with things that are utterly wrong
          -- Like Int ~ Bool (incl nullary TyCons)
@@ -1147,11 +1150,13 @@ validSubstitutions ct | isExprHoleCt ct =
     localsFirst elts = lcl ++ gbl
       where (lcl, gbl) = partition gre_lcl elts
 
-    getBndrOcc :: TcIdBinder -> OccName
-    getBndrOcc (TcIdBndr id _) = occName $ getName id
-    getBndrOcc (TcIdBndr_ExpType name _ _) = occName $ getName name
+    is_id_bind :: TcBinder -> Bool
+    is_id_bind (TcIdBndr {})         = True
+    is_id_bind (TcIdBndr_ExpType {}) = True
+    is_id_bind (TcTvBndr {})         = False
 
-    relBindSet =  mkOccSet $ map getBndrOcc $ tcl_bndrs hole_env
+    relBindSet = mkOccSet $ [ occName b | b <- tcl_bndrs hole_env
+                                        , is_id_bind b ]
 
     shouldBeSkipped :: GlobalRdrElt -> Bool
     shouldBeSkipped el = (occName $ gre_name el) `elemOccSet` relBindSet
@@ -2912,7 +2917,7 @@ relevantBindings want_filtering ctxt ct
 
     ---- fixes #12177
     ---- builds up a list of bindings whose OccName has not been seen before
-    remove_shadowing :: [TcIdBinder] -> [TcIdBinder]
+    remove_shadowing :: [TcBinder] -> [TcBinder]
     remove_shadowing bindings = reverse $ fst $ foldl
       (\(bindingAcc, seenNames) binding ->
         if (occName binding) `elemOccSet` seenNames -- if we've seen it
@@ -2922,13 +2927,14 @@ relevantBindings want_filtering ctxt ct
 
     go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
        -> Bool                          -- True <=> some filtered out due to lack of fuel
-       -> [TcIdBinder]
+       -> [TcBinder]
        -> TcM (TidyEnv, [SDoc], Bool)   -- The bool says if we filtered any out
                                         -- because of lack of fuel
     go _ tidy_env _ _ _ docs discards []
       = return (tidy_env, reverse docs, discards)
     go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
       = case tc_bndr of
+          TcTvBndr {} -> discard_it
           TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
           TcIdBndr_ExpType name et top_lvl ->
             do { mb_ty <- readExpType_maybe et
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 0416e36621..e5ecb3b138 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -85,7 +85,7 @@ module TcRnMonad(
   failIfTc, failIfTcM,
   warnIfFlag, warnIf, warnTc, warnTcM,
   addWarnTc, addWarnTcM, addWarn, addWarnAt, add_warn,
-  tcInitTidyEnv, tcInitOpenTidyEnv, mkErrInfo,
+  mkErrInfo,
 
   -- * Type constraints
   newTcEvBinds,
@@ -178,6 +178,8 @@ import Data.Set ( Set )
 import qualified Data.Set as Set
 
 import {-# SOURCE #-} TcSplice ( runRemoteModFinalizers )
+import {-# SOURCE #-} TcEnv    ( tcInitTidyEnv )
+
 import qualified Data.Map as Map
 
 {-
@@ -325,7 +327,6 @@ initTcWithGbl hsc_env gbl_env loc do_this
                 tcl_arrow_ctxt = NoArrowCtxt,
                 tcl_env        = emptyNameEnv,
                 tcl_bndrs      = [],
-                tcl_tidy       = emptyTidyEnv,
                 tcl_tyvars     = tvs_var,
                 tcl_lie        = lie_var,
                 tcl_tclvl      = topTcLevel
@@ -1299,19 +1300,6 @@ add_warn_at reason loc msg extra_info
                                     msg extra_info } ;
          reportWarning reason warn }
 
-tcInitTidyEnv :: TcM TidyEnv
-tcInitTidyEnv
-  = do  { lcl_env <- getLclEnv
-        ; return (tcl_tidy lcl_env) }
-
--- | Get a 'TidyEnv' that includes mappings for all vars free in the given
--- type. Useful when tidying open types.
-tcInitOpenTidyEnv :: [TyCoVar] -> TcM TidyEnv
-tcInitOpenTidyEnv tvs
-  = do { env1 <- tcInitTidyEnv
-       ; let env2 = tidyFreeTyCoVars env1 tvs
-       ; return env2 }
-
 
 {-
 -----------------------------------
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 0a76d23ad3..e718b4d68b 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -38,7 +38,7 @@ module TcRnTypes(
         WhereFrom(..), mkModDeps, modDepsElts,
 
         -- Typechecker types
-        TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
+        TcTypeEnv, TcBinderStack, TcBinder(..),
         TcTyThing(..), PromotionErr(..),
         IdBindingInfo(..), ClosedTypeId, RhsNames,
         IsGroupClosed(..),
@@ -828,10 +828,8 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_env  :: TcTypeEnv,    -- The local type environment:
                                   -- Ids and TyVars defined in this module
 
-        tcl_bndrs :: TcIdBinderStack,   -- Used for reporting relevant bindings
-
-        tcl_tidy :: TidyEnv,      -- Used for tidying types; contains all
-                                  -- in-scope type variables (but not term variables)
+        tcl_bndrs :: TcBinderStack,   -- Used for reporting relevant bindings,
+                                      -- and for tidying types
 
         tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
                         -- Namely, the in-scope TyVars bound in tcl_env,
@@ -885,34 +883,44 @@ type TcId        = Id
 type TcIdSet     = IdSet
 
 ---------------------------
--- The TcIdBinderStack
+-- The TcBinderStack
 ---------------------------
 
-type TcIdBinderStack = [TcIdBinder]
-   -- This is a stack of locally-bound ids, innermost on top
-   -- Used only in error reporting (relevantBindings in TcError)
+type TcBinderStack = [TcBinder]
+   -- This is a stack of locally-bound ids and tyvars,
+   --   innermost on top
+   -- Used only in error reporting (relevantBindings in TcError),
+   --   and in tidying
    -- We can't use the tcl_env type environment, because it doesn't
    --   keep track of the nesting order
 
-data TcIdBinder
+data TcBinder
   = TcIdBndr
        TcId
        TopLevelFlag    -- Tells whether the binding is syntactically top-level
                        -- (The monomorphic Ids for a recursive group count
                        --  as not-top-level for this purpose.)
+
   | TcIdBndr_ExpType  -- Variant that allows the type to be specified as
                       -- an ExpType
        Name
        ExpType
        TopLevelFlag
 
-instance Outputable TcIdBinder where
+  | TcTvBndr          -- e.g.   case x of P (y::a) -> blah
+       Name           -- We bind the lexical name "a" to the type of y,
+       TyVar          -- which might be an utterly different (perhaps
+                      -- existential) tyvar
+
+instance Outputable TcBinder where
    ppr (TcIdBndr id top_lvl)           = ppr id <> brackets (ppr top_lvl)
    ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl)
+   ppr (TcTvBndr name tv)              = ppr name <+> ppr tv
 
-instance HasOccName TcIdBinder where
-    occName (TcIdBndr id _) = (occName (idName id))
-    occName (TcIdBndr_ExpType name _ _) = (occName name)
+instance HasOccName TcBinder where
+    occName (TcIdBndr id _)             = occName (idName id)
+    occName (TcIdBndr_ExpType name _ _) = occName name
+    occName (TcTvBndr name _)           = occName name
 
 ---------------------------
 -- Template Haskell stages and levels
@@ -2934,7 +2942,7 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
   -- The TcLclEnv includes particularly
   --    source location:  tcl_loc   :: RealSrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
-  --    binder stack:     tcl_bndrs :: TcIdBinderStack
+  --    binder stack:     tcl_bndrs :: TcBinderStack
   --    level:            tcl_tclvl :: TcLevel
 
 mkKindLoc :: TcType -> TcType   -- original *types* being compared
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index fdff7e95aa..37f774047a 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -39,7 +39,7 @@ import TyCon
 -- others:
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
-import TcEnv       ( tcGetInstEnvs )
+import TcEnv       ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv )
 import FunDeps
 import InstEnv     ( InstMatch, lookupInstEnv )
 import FamInstEnv  ( isDominatedBy, injectiveBranches,
diff --git a/testsuite/tests/indexed-types/should_fail/T14175.hs b/testsuite/tests/indexed-types/should_fail/T14175.hs
new file mode 100644
index 0000000000..9d259fe704
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14175.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, TypeInType #-}
+
+module T14175 where
+
+import Data.Kind
+
+type family PComp (k :: j -> Type) (x :: k) :: ()
diff --git a/testsuite/tests/indexed-types/should_fail/T14175.stderr b/testsuite/tests/indexed-types/should_fail/T14175.stderr
new file mode 100644
index 0000000000..dbadbe1f46
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14175.stderr
@@ -0,0 +1,5 @@
+
+T14175.hs:7:42: error:
+    • Expecting one more argument to ‘k’
+      Expected a type, but ‘k’ has kind ‘j -> *’
+    • In the kind ‘k’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index ee4fccefb4..3af724d1b9 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -139,3 +139,4 @@ test('T13877', normal, compile_fail, [''])
 test('T13972', normal, compile_fail, [''])
 test('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile_fail, [''])
+test('T14175', normal, compile_fail, [''])