add proposal(s) / flesh out info about the following

A further alternative is to restrict the required information used for kind inference to the places that define types: type abbreviations, newtype and data declarations; this should be augmented with kind annotations.

Rationale: this permits a compiler not to check every single type annotation of a program to resolve kinds, but the kind annotations would enable the user to help out when necessary. The restriction to type-defining places is analogous to the way type ambiguity at value level is treated.