Too easy to trigger CUSK condition using TH

While trying to make singletons class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.

Consider this class:

$(promoteOnly [d|
  class Cls a  where
    fff :: Proxy a -> ()
  |])

The generated TH (slightly simplified by hand) looks like this:

type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm

data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ())

type instance Apply FffSym0 l_alvn = FffSym1 l_alvn

class PCls a_alve where
  type Fff (arg_alvl :: Proxy a_alve) :: ()

However, it fails to compile with the following error:

cusk.hs:25:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      a1627472612 :: k0
      l_alvn :: TyFun (Proxy a1627472612) ()

As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write

data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())

and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.

Looking at the module TcHsType in the GHC sources, I see that the error is reported by the kcHsTyVarBndrs function:

          -- If there are any meta-tvs left, the user has
          -- lied about having a CUSK. Error.
       ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
       ; when (not (null meta_tvs)) $
         report_non_cusk_tvs (qkvs ++ tc_tvs)

However, I don't see why we can't generalize over meta_tvs instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound.

Below I attach a self-contained example that demonstrates the issue and has no dependencies except base.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture