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