Although GHC rejects type family equations that have an oversaturated number of required arguments, it doesn't extend that treatment to oversatured visible kind arguments, such as in the following example:

type family F (x :: j) :: forall k. Either j k where
  F 5 @Symbol = Left 4

In this example, @Symbol is actually instantiating the k in the return kind! This should not be allowed (see #15740 (closed)), so this makes it so.

To catch oversaturated uses of VKA, we add an additional check to TcValidity.checkFamPatBinders that drops the first n type patterns in the equation (where n is the arity of the type family tycon), and if there are any types remaining, we know that they must be oversaturated VKAs, so reject. (See Note [Oversaturated type family equations] for a lengthier explanation.)

(Amusingly, implementing this check actually caught an oversaturated use of VKA in the T15793 test case, which was marked as should_compile!)

Fixes #16255 (closed).