Scoped type variables only appears non-injectively in declaration header [GHC-59738]

The disconnected type variables error applies when kind-checking the header of a type/class declaration that has a separate, standalone kind signature.

For this consider:

type S a = Type

type C :: forall k. S k -> Constraint
class C (a :: S kk) where
 op :: .. kk ..

Note that the class has a separate kind signature, so the elaborated decl should look like

class C @kk (a :: S kk) where ..

But how can we “connect up” the scoped variable kk with the skolem kind from the standalone kind signature for C? In general we do this by unifying the two. For example

type T k = (k,Type)
type W :: forall k. T k -> Type
data W (a :: (x,Type)) = ..

When we encounter (a :: (x,Type)) we unify the kind (x,Type) with the kind (T k) from the standalone kind signature. Of course, unification looks through synonyms so we end up with the mapping [x :-> k] that connects the scoped type variable x with the kind from the signature.

But in our earlier example this unification is ineffective, because S is a phantom synonym (and hence non-injective) that just discards its argument. So our answer to this issue is:

if matchUpSigWithDecl fails to connect kk with k, by unification, we give up and complain about a “disconnected” type variable.

The fix is easy: just add an explicit @kk parameter to the declaration, to bind kk explicitly, rather than binding it implicitly via unification.

More discussion can be found at ghc issue #24083.

This text was adapted from Simon Peyton Jones’ note on disconnected type variable, please refer to this note for more technical insight.