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

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import labels

Yes I agree.

Trac #11648 (closed) is highly relevant.

mentioned in commit 12794287

I see no reason not to merge for 8.6.

Trac metadata

Trac field	Value
Test case	- → polykinds/T11648b

added 1 deleted label

changed milestone to %8.8.1

These won't be addressed in GHC 8.6.

closed

changed milestone to %8.6.1

Actually, this is present in the GHC 8.6 branch, so it //did// make it in. Closing.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Pnormal label