Type families mistakingly report kind variables as unbound type variables

GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536 (closed)). However this also mistakingly catches kind variables that aren't present in the type family head.

Simplest test case:

{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a

As seen on 8.0.1-rc2 and 7.10.2:

../File.hs:3:23:
    Family instance purports to bind type variable ‘k1’
      but the real LHS (expanding synonyms) is: F (f a) = ...
    In the equations for closed type family ‘F’
    In the type family declaration for ‘F’

The culprit seems to be in exactTyCoVarsOfType, which doesn't grab kind variables from a type variable's kind, even though tyCoVarsOfType does.

Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned F are actually okay. (Are they?)

Trac metadata

Trac field	Value
Version	8.0.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture