Datatypes with CUSKs should quantify over unknown kinds
In the future, we will be able to give full kind signatures to datatype declarations. But in the present, we use CUSKs to write kind signatures.
data T (a :: Proxy k)
That has a CUSK, according to the CUSK rules. Yet we don't know the kind of
k. Currently, this definition is rejected, accusing the user of lying about having a complete kind. However, let's instead pretend the user had written
type T :: Proxy k -> Type data T a
After all, that's what the CUSK is shorthand for. In this case, it's clear that we should infer
T :: forall k1 (k :: k1). Proxy k -> Type, just the way we would do with a term-level type signature.
This turns out to be quite easy. See D4845.
This change allows strictly more programs to be accepted, and I think it falls under the threshold for requiring a proposal.