Don't zap to Any; error instead

This changes GHC's treatment of so-called Naughty Quantification
Candidates to issue errors, instead of zapping to Any.

Close #16775.

No new test cases, because existing ones cover this well.

compiler/basicTypes/OccName.hs

@@ -94,7 +94,7 @@ module OccName (
 
         -- * Tidying up
         TidyOccEnv, emptyTidyOccEnv, initTidyOccEnv,
-        tidyOccName, avoidClashesOccEnv,
+        tidyOccName, avoidClashesOccEnv, delTidyOccEnvList,
 
         -- FsEnv
         FastStringEnv, emptyFsEnv, lookupFsEnv, extendFsEnv, mkFsEnv
@@ -818,7 +818,7 @@ Every id contributes a type variable to the type signature, and all of them are
 
     (id,id,id) :: (a2 -> a2, a1 -> a1, a -> a)
 
-which is a bit unfortunate, as it unfairly renames only one of them. What we
+which is a bit unfortunate, as it unfairly renames only two of them. What we
 would like to see is
 
     (id,id,id) :: (a3 -> a3, a2 -> a2, a1 -> a1)
@@ -846,6 +846,9 @@ initTidyOccEnv = foldl' add emptyUFM
   where
     add env (OccName _ fs) = addToUFM env fs 1
 
+delTidyOccEnvList :: TidyOccEnv -> [FastString] -> TidyOccEnv
+delTidyOccEnvList = delListFromUFM
+
 -- see Note [Tidying multiple names at once]
 avoidClashesOccEnv :: TidyOccEnv -> [OccName] -> TidyOccEnv
 avoidClashesOccEnv env occs = go env emptyUFM occs

compiler/basicTypes/VarEnv.hs

@@ -71,13 +71,14 @@ module VarEnv (
 
         -- * TidyEnv and its operation
         TidyEnv,
-        emptyTidyEnv, mkEmptyTidyEnv
+        emptyTidyEnv, mkEmptyTidyEnv, delTidyEnvList
     ) where
 
 import GhcPrelude
 import qualified Data.IntMap.Strict as IntMap -- TODO: Move this to UniqFM
 
 import OccName
+import Name
 import Var
 import VarSet
 import UniqSet
@@ -424,6 +425,12 @@ emptyTidyEnv = (emptyTidyOccEnv, emptyVarEnv)
 mkEmptyTidyEnv :: TidyOccEnv -> TidyEnv
 mkEmptyTidyEnv occ_env = (occ_env, emptyVarEnv)
 
+delTidyEnvList :: TidyEnv -> [Var] -> TidyEnv
+delTidyEnvList (occ_env, var_env) vs = (occ_env', var_env')
+  where
+    occ_env' = occ_env `delTidyOccEnvList` map (occNameFS . getOccName) vs
+    var_env' = var_env `delVarEnvList` vs
+
 {-
 ************************************************************************
 *                                                                      *

compiler/typecheck/TcHsType.hs

@@ -1770,7 +1770,7 @@ the surrounding context, we must obey the following dictum:
   Every metavariable in a type must either be
     (A) generalized, or
     (B) promoted, or        See Note [Promotion in signatures]
-    (C) zapped to Any       See Note [Naughty quantification candidates] in TcMType
+    (C) a cause to error    See Note [Naughty quantification candidates] in TcMType
 
 The kindGeneralize functions do not require pre-zonking; they zonk as they
 go.

compiler/typecheck/TcMType.hs

@@ -1149,8 +1149,7 @@ So alpha is entirely unconstrained.
 
 What then should we do with alpha?  During generalization, every
 metavariable is either (A) promoted, (B) generalized, or (C) zapped
-(according again to Note [Recipe for checking a signature] in
-TcHsType).
+(according to Note [Recipe for checking a signature] in TcHsType).
 
  * We can't generalise it.
  * We can't promote it, because its kind prevents that
@@ -1158,11 +1157,14 @@ TcHsType).
    go into the typing environment (as the type of some let-bound
    variable, say), and then chaos erupts when we try to instantiate.
 
-So, we zap it, eagerly, to Any. We don't have to do this eager zapping
-in terms (say, in `length []`) because terms are never re-examined before
-the final zonk (which zaps any lingering metavariables to Any).
+Previously, we zapped it to Any. This worked, but it had the unfortunate
+effect of causing Any sometimes to appear in error messages. If this
+kind of signature happens, the user probably has made a mistake -- no
+one really wants Any in their types. So we now error. This must be
+a hard error (failure in the monad) to avoid other messages from mentioning
+Any.
 
-We do this eager zapping in candidateQTyVars, which always precedes
+We do this eager erroring in candidateQTyVars, which always precedes
 generalisation, because at that moment we have a clear picture of what
 skolems are in scope within the type itself (e.g. that 'forall arg').
 
@@ -1247,13 +1249,14 @@ partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
 -- See Note [Dependent type variables]
 candidateQTyVarsOfType :: TcType       -- not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty
+candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty
 
 -- | Like 'candidateQTyVarsOfType', but over a list of types
 -- The variables to quantify must have a TcLevel strictly greater than
 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
-candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys
+candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty)
+                                     mempty tys
 
 -- | Like 'candidateQTyVarsOfType', but consider every free variable
 -- to be dependent. This is appropriate when generalizing a *kind*,
@@ -1261,11 +1264,12 @@ candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempt
 -- to Type.)
 candidateQTyVarsOfKind :: TcKind       -- Not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty
+candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty
 
 candidateQTyVarsOfKinds :: [TcKind]    -- Not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys
+candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty)
+                                    mempty tys
 
 delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
 delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
@@ -1274,7 +1278,8 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
        , dv_cvs = cvs `delVarSetList`  vars }
 
 collect_cand_qtvs
-  :: Bool            -- True <=> consider every fv in Type to be dependent
+  :: TcType          -- original type that we started recurring into; for errors
+  -> Bool            -- True <=> consider every fv in Type to be dependent
   -> VarSet          -- Bound variables (locals only)
   -> CandidatesQTvs  -- Accumulating parameter
   -> Type            -- Not necessarily zonked
@@ -1284,14 +1289,14 @@ collect_cand_qtvs
 --   * Looks through meta-tyvars as it goes;
 --     no need to zonk in advance
 --
---   * Needs to be monadic anyway, because it does the zap-naughty
---     stuff; see Note [Naughty quantification candidates]
+--   * Needs to be monadic anyway, because it handles naughty
+--     quantification; see Note [Naughty quantification candidates]
 --
 --   * Returns fully-zonked CandidateQTvs, including their kinds
 --     so that subsequent dependency analysis (to build a well
 --     scoped telescope) works correctly
 
-collect_cand_qtvs is_dep bound dvs ty
+collect_cand_qtvs orig_ty is_dep bound dvs ty
   = go dvs ty
   where
     is_bound tv = tv `elemVarSet` bound
@@ -1304,8 +1309,8 @@ collect_cand_qtvs is_dep bound dvs ty
     go dv (FunTy _ arg res) = foldlM go dv [arg, res]
     go dv (LitTy {})        = return dv
     go dv (CastTy ty co)    = do dv1 <- go dv ty
-                                 collect_cand_qtvs_co bound dv1 co
-    go dv (CoercionTy co)   = collect_cand_qtvs_co bound dv co
+                                 collect_cand_qtvs_co orig_ty bound dv1 co
+    go dv (CoercionTy co)   = collect_cand_qtvs_co orig_ty bound dv co
 
     go dv (TyVarTy tv)
       | is_bound tv      = return dv
@@ -1315,8 +1320,8 @@ collect_cand_qtvs is_dep bound dvs ty
                                   Nothing     -> go_tv dv tv }
 
     go dv (ForAllTy (Bndr tv _) ty)
-      = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv)
-           ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty }
+      = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
+           ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
 
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
@@ -1334,25 +1339,23 @@ collect_cand_qtvs is_dep bound dvs ty
                  -- (#15795) and to make the naughty check
                  -- (which comes next) works correctly
 
+           ; let tv_kind_vars = tyCoVarsOfType tv_kind
            ; cur_lvl <- getTcLevel
            ; if |  tcTyVarLevel tv <= cur_lvl
                 -> return dv   -- this variable is from an outer context; skip
                                -- See Note [Use level numbers ofor quantification]
 
-                |  intersectsVarSet bound (tyCoVarsOfType tv_kind)
+                |  intersectsVarSet bound tv_kind_vars
                    -- the tyvar must not be from an outer context, but we have
                    -- already checked for this.
                    -- See Note [Naughty quantification candidates]
-                -> do { traceTc "Zapping naughty quantifier" $
+                -> do { traceTc "Naughty quantifier" $
                           vcat [ ppr tv <+> dcolon <+> ppr tv_kind
                                , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
-                               , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $
-                                                            tyCoVarsOfType tv_kind) ]
+                               , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet tv_kind_vars) ]
 
-                      ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
-
-                      -- See Note [Recurring into kinds for candidateQTyVars]
-                      ; collect_cand_qtvs True bound dv tv_kind }
+                      ; let escapees = intersectVarSet bound tv_kind_vars
+                      ; naughtyQuantification orig_ty tv escapees }
 
                 |  otherwise
                 -> do { let tv' = tv `setTyVarKind` tv_kind
@@ -1361,15 +1364,16 @@ collect_cand_qtvs is_dep bound dvs ty
                                 -- See Note [Order of accumulation]
 
                         -- See Note [Recurring into kinds for candidateQTyVars]
-                      ; collect_cand_qtvs True bound dv' tv_kind } }
+                      ; collect_cand_qtvs orig_ty True bound dv' tv_kind } }
 
-collect_cand_qtvs_co :: VarSet -- bound variables
+collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors
+                     -> VarSet -- bound variables
                      -> CandidatesQTvs -> Coercion
                      -> TcM CandidatesQTvs
-collect_cand_qtvs_co bound = go_co
+collect_cand_qtvs_co orig_ty bound = go_co
   where
-    go_co dv (Refl ty)             = collect_cand_qtvs True bound dv ty
-    go_co dv (GRefl _ ty mco)      = do dv1 <- collect_cand_qtvs True bound dv ty
+    go_co dv (Refl ty)             = collect_cand_qtvs orig_ty True bound dv ty
+    go_co dv (GRefl _ ty mco)      = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty
                                         go_mco dv1 mco
     go_co dv (TyConAppCo _ _ cos)  = foldlM go_co dv cos
     go_co dv (AppCo co1 co2)       = foldlM go_co dv [co1, co2]
@@ -1377,8 +1381,8 @@ collect_cand_qtvs_co bound = go_co
     go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
     go_co dv (AxiomRuleCo _ cos)   = foldlM go_co dv cos
     go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov
-                                        dv2 <- collect_cand_qtvs True bound dv1 t1
-                                        collect_cand_qtvs True bound dv2 t2
+                                        dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1
+                                        collect_cand_qtvs orig_ty True bound dv2 t2
     go_co dv (SymCo co)            = go_co dv co
     go_co dv (TransCo co1 co2)     = foldlM go_co dv [co1, co2]
     go_co dv (NthCo _ _ co)        = go_co dv co
@@ -1397,7 +1401,7 @@ collect_cand_qtvs_co bound = go_co
 
     go_co dv (ForAllCo tcv kind_co co)
       = do { dv1 <- go_co dv kind_co
-           ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co }
+           ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co }
 
     go_mco dv MRefl    = return dv
     go_mco dv (MCo co) = go_co dv co
@@ -1413,7 +1417,7 @@ collect_cand_qtvs_co bound = go_co
       | cv `elemVarSet` cvs = return dv
 
         -- See Note [Recurring into kinds for candidateQTyVars]
-      | otherwise           = collect_cand_qtvs True bound
+      | otherwise           = collect_cand_qtvs orig_ty True bound
                                     (dv { dv_cvs = cvs `extendVarSet` cv })
                                     (idType cv)
 
@@ -2317,8 +2321,8 @@ tidySigSkol env cx ty tv_prs
 %************************************************************************
 %*                                                                      *
              Levity polymorphism checks
-*                                                                      *
-************************************************************************
+*                                                                       *
+*************************************************************************
 
 See Note [Levity polymorphism checking] in DsMonad
 
@@ -2363,3 +2367,48 @@ formatLevPolyErr ty
   where
     (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
     tidy_ki             = tidyType tidy_env (tcTypeKind ty)
+
+{-
+%************************************************************************
+%*                                                                      *
+             Error messages
+*                                                                       *
+*************************************************************************
+
+-}
+
+-- See Note [Naughty quantification candidates]
+naughtyQuantification :: TcType   -- original type user wanted to quantify
+                      -> TcTyVar  -- naughty var
+                      -> TyVarSet -- skolems that would escape
+                      -> TcM a
+naughtyQuantification orig_ty tv escapees
+  = do { orig_ty1 <- zonkTcType orig_ty  -- in case it's not zonked
+
+       ; escapees' <- mapM zonkTcTyVarToTyVar $
+                      nonDetEltsUniqSet escapees
+                     -- we'll just be printing, so no harmful non-determinism
+
+       ; let fvs  = tyCoVarsOfTypeWellScoped orig_ty1
+             env0 = tidyFreeTyCoVars emptyTidyEnv fvs
+             env  = env0 `delTidyEnvList` escapees'
+                    -- this avoids gratuitous renaming of the escaped
+                    -- variables; very confusing to users!
+
+             orig_ty'   = tidyType env orig_ty1
+             ppr_tidied = pprTyVars . map (tidyTyCoVarOcc env)
+             doc = pprWithExplicitKindsWhen True $
+                   vcat [ sep [ text "Cannot generalise type; skolem" <> plural escapees'
+                              , quotes $ ppr_tidied escapees'
+                              , text "would escape" <+> itsOrTheir escapees' <+> text "scope"
+                              ]
+                        , sep [ text "if I tried to quantify"
+                              , ppr_tidied [tv]
+                              , text "in this type:"
+                              ]
+                        , nest 2 (pprTidiedType orig_ty')
+                        , text "(Indeed, I sometimes struggle even printing this correctly,"
+                        , text " due to its ill-scoped nature.)"
+                        ]
+
+       ; failWithTcM (env, doc) }

compiler/typecheck/TcPatSyn.hs

@@ -237,7 +237,7 @@ dependentArgErr (arg, bad_cos)
 ~~-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   data AST a = Sym [a]
-  class Prj s where { prj :: [a] -> Maybe (s a)
+  class Prj s where { prj :: [a] -> Maybe (s a) }
   pattern P x <= Sym (prj -> Just x)
 
 Here we get a matcher with this type
@@ -261,7 +261,7 @@ mentions the existentials.  We can conveniently do that by making the
    forall ex_tvs. arg_ty
 
 After that, Note [Naughty quantification candidates] in TcMType takes
-over, and zonks any such naughty variables to Any.
+over and errors.
 
 Note [Remove redundant provided dicts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/types/TyCoPpr.hs

@@ -5,7 +5,7 @@ module TyCoPpr
         PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
 
         -- * Pretty-printing types
-        pprType, pprParendType, pprPrecType, pprPrecTypeX,
+        pprType, pprParendType, pprTidiedType, pprPrecType, pprPrecTypeX,
         pprTypeApp, pprTCvBndr, pprTCvBndrs,
         pprSigmaType,
         pprTheta, pprParendTheta, pprForAll, pprUserForAll,
@@ -81,10 +81,13 @@ See Note [Precedence in types] in BasicTypes.
 -- See Note [Pretty printing via Iface syntax] in PprTyThing
 --------------------------------------------------------
 
-pprType, pprParendType :: Type -> SDoc
+pprType, pprParendType, pprTidiedType :: Type -> SDoc
 pprType       = pprPrecType topPrec
 pprParendType = pprPrecType appPrec
 
+-- already pre-tidied
+pprTidiedType = pprIfaceType . toIfaceTypeX emptyVarSet
+
 pprPrecType :: PprPrec -> Type -> SDoc
 pprPrecType = pprPrecTypeX emptyTidyEnv
 

compiler/types/TyCoTidy.hs

@@ -95,8 +95,8 @@ tidyTyCoVarBinders tidy_env tvbs
 tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
 -- ^ Add the free 'TyVar's to the env in tidy form,
 -- so that we can tidy the type they are free in
-tidyFreeTyCoVars (full_occ_env, var_env) tyvars
-  = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars)
+tidyFreeTyCoVars tidy_env tyvars
+  = fst (tidyOpenTyCoVars tidy_env tyvars)
 
 ---------------
 tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
@@ -232,5 +232,3 @@ tidyCo env@(_, subst) co
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = map (tidyCo env)
-
-

compiler/utils/Outputable.hs

@@ -34,7 +34,7 @@ module Outputable (
         sep, cat,
         fsep, fcat,
         hang, hangNotEmpty, punctuate, ppWhen, ppUnless,
-        speakNth, speakN, speakNOf, plural, isOrAre, doOrDoes,
+        speakNth, speakN, speakNOf, plural, isOrAre, doOrDoes, itsOrTheir,
         unicodeSyntax,
 
         coloured, keyword,
@@ -1160,6 +1160,15 @@ doOrDoes :: [a] -> SDoc
 doOrDoes [_] = text "does"
 doOrDoes _   = text "do"
 
+-- | Determines the form of possessive appropriate for the length of a list:
+--
+-- > itsOrTheir [x]   = text "its"
+-- > itsOrTheir [x,y] = text "their"
+-- > itsOrTheir []    = text "their"  -- probably avoid this
+itsOrTheir :: [a] -> SDoc
+itsOrTheir [_] = text "its"
+itsOrTheir _   = text "their"
+
 {-
 ************************************************************************
 *                                                                      *

docs/users_guide/8.12.1-notes.rst

@@ -18,6 +18,12 @@ Full details
 Language
 ~~~~~~~~
 
+* In obscure scenarios, GHC now rejects programs it previously accepted, but
+  with unhelpful types. For example, if (with ``-XPartialTypeSignatures``) you
+  were to write ``x :: forall (f :: forall a (b :: a -> Type). b _). f _``, GHC previously
+  would have accepted ``x``, but its type would have involved the mysterious ``Any``
+  internal type family. Now, GHC rejects, explaining the situation.
+
 Compiler
 ~~~~~~~~
 

testsuite/tests/dependent/should_compile/all.T

@@ -54,13 +54,9 @@ test('T15419', normal, compile, [''])
 test('T14066h', normal, compile, [''])
 test('T15666', normal, compile, [''])
 test('T15725', normal, compile, [''])
-test('T14880', normal, compile, [''])
-test('T14880-2', normal, compile, [''])
 test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
 test('InferDependency', normal, compile, [''])
 test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
-test('T15076', normal, compile, [''])
-test('T15076b', normal, compile, [''])
 test('T15076c', normal, compile, [''])
 test('T15829', normal, compile, [''])
 test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions'])

testsuite/tests/dependent/should_fail/T14880-2.stderr

+
+T14880-2.hs:12:9: error:
+    • Cannot generalise type; skolem ‘arg’ would escape its scope
+      if I tried to quantify (a0 :: arg) in this type:
+        forall arg. Proxy @{Proxy @{arg} a0 -> *} (Foo arg @a0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature: quux :: forall arg. Proxy (Foo arg) -> ()

testsuite/tests/dependent/should_fail/T14880.stderr

+
+T14880.hs:12:5: error:
+    • Cannot generalise type; skolem ‘arg’ would escape its scope
+      if I tried to quantify (a0 :: arg) in this type:
+        forall x arg.
+        ((Foo arg @a0 :: (Proxy @{arg} a0 -> *))
+         ~ (Foo arg @a0 :: (Proxy @{arg} a0 -> *))) =>
+        Bar x
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the definition of data constructor ‘MkBar’
+      In the data declaration for ‘Bar’

testsuite/tests/dependent/should_fail/T15076.stderr

+
+T15076.hs:10:8: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (f :: forall (x :: a). Proxy @{a} x -> *).
+        Proxy @{Proxy @{a} x0 -> *} (f @x0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type).
+               Proxy f -> ()

testsuite/tests/dependent/should_fail/T15076b.stderr

+
+T15076b.hs:8:8: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (f :: forall (x :: a). Proxy @{a} x -> *).
+        Proxy @{Proxy @{a} x0 -> *} (f @x0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type).
+               Proxy f -> ()

testsuite/tests/dependent/should_fail/T15825.stderr

 
-T15825.hs:14:31: error:
-    • Illegal type synonym family application ‘GHC.Types.Any
-                                                 @k’ in instance:
-        X (a @(GHC.Types.Any @k))
+T15825.hs:14:10: error:
+    • Cannot generalise type; skolem ‘k’ would escape its scope
+      if I tried to quantify (x0 :: k) in this type:
+        forall k (a :: C k). X (a @x0)
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
     • In the instance declaration for ‘X (a :: *)’

testsuite/tests/dependent/should_fail/all.T

@@ -60,3 +60,7 @@ test('T16418', normal, compile_fail, [''])
 test('T17541', normal, compile_fail, [''])
 test('T17541b', normal, compile_fail, [''])
 test('T17131', normal, compile_fail, [''])
+test('T14880', normal, compile_fail, [''])
+test('T14880-2', normal, compile_fail, [''])
+test('T15076', normal, compile_fail, [''])
+test('T15076b', normal, compile_fail, [''])