Note [Ambiguous kind vars]
We used to be concerned about ambiguous binders. Suppose we have the kind
S1 :: forall k -> * -> *
S2 :: forall k. * -> *
Here S1 is OK, because k is Required, and at a use of S1 we will
see (S1 *) or (S1 (*->*)) or whatever.
But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and
we have no way (ever) to figure out how 'k' should be instantiated.
For example if we see (S2 Int), that tells us nothing about k's
instantiation. (In this case we'll instantiate it to Any, but that
seems wrong.) This is really the same test as we make for ambiguous
type in term type signatures.
Now, it's impossible for a Specified variable not to occur
at all in the kind -- after all, it is Specified so it must have
occurred. (It /used/ to be possible; see tests T13983 and T7873. But
with the advent of the forall-or-nothing rule for kind variables,
those strange cases went away. See Note [forall-or-nothing rule] in
GHC.Hs.Type.)
But one might worry about
type v k = *
S3 :: forall k. V k -> *
which appears to mention 'k' but doesn't really. Or
S4 :: forall k. F k -> *
where F is a type function. But we simply don't check for
those cases of ambiguity, yet anyway. The worst that can happen
is ambiguity at the call sites.
Historical note: this test used to be called reportFloatingKvs. References 1
- forall-or-nothing rule Language.Haskell.Syntax.Type
Referenced by 1
- Bad TyCon telescopes GHC.Tc.Validity