Reject oversaturated VKAs in type family equations

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).