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.

However, consider

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.

Trac metadata

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