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