Don't infer forall with an escaping kind

This ticket is really a subtask of #20686; I am creating a separate ticket since it's not about defaulting and in theory could be done separately.

Given this program

module M1 where

import GHC.Exts

f = f :: (_ :: TYPE (r s))

GHC fails:

M1.hs:5:1: error: [GHC-31147]
    • Quantified type's kind mentions quantified type variable
        type: ‘forall {k} {r :: k -> RuntimeRep} {s :: k}
                      {t :: TYPE (r s)}.
               t’
      where the body of the forall has this kind: ‘TYPE (r s)’

However, this failure happens too late: we have inferred a type for f that shouldn't exist in the first place. Quoting #23051 (comment 484810):

GHC is forming bad types, like forall f g (a :: TYPE (f g)). a, whose kind mentions free type variables. These types are errored upon in Validity.checkEscapingKind, but they shouldn't ever exist in the first place, as they violate the PKTI of Note [The Purely Kinded Type Invariant (PKTI)]. We mused on the call about using levels to ensure this property. I think this could work, but it's a bit indirect. Perhaps better (and simpler) would be just to instruct e.g. candidateQTyVarsOfTypes not to consider variables free in a type's kind as candidates for generalization. (The "e.g." is because there are several entry points to this algorithm; they'd all likely need to be updated. Note: entry points, not the recursive worker. This property is not recursive!) The candidate-gathering algorithm already tracks a set of bound variables not to consider as candidates, but these variables also are used to detect so-called "naughty" quantification, which is not what we're concerned about here. So we'd need a new set of variables-to-avoid. Once these variables are not quantified over, they will get promoted, and I think all will work smoothly. This is like Simon's idea (on the call) of adding the kind variables to the mono-tyvars, but covers both simplifyInfer and kindGeneralize, instead of just the former.

I think a better plan would be to promote any free meta-tyvars of the kind, before calling candidateQTyVarOfTypes. It already knows not to quantify over tyvars from an outer level.

As a result of this ticket, we should not form the bad type and remove the call checkEscapingKind in GHC.Tc.Gen.Bind; the error for the above program will be different.

Here are two other testcases that construct a forall with an escaping kind:

module M2 where

import GHC.Exts

f :: (_ :: TYPE r)
f = f

{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
module M3 where

import M3aux
h = $$g

{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
module M3aux where

import Data.Kind
import GHC.Exts
import Language.Haskell.TH (Code, Q)

g :: Code Q _
g = [||let f :: forall (r :: Type -> RuntimeRep) s (a :: TYPE (r s)). () -> a
           f = f
           in f () ||]

Relevant notes: Note [Inferred type with escaping kind], Note [Check for escaping result kind].