Note [Bidirectional type checking]

In types, as in terms, we use bidirectional type infefence.  The main workhorse
function looks like this:

    type ExpKind = ExpType
    data ExpType = Check TcSigmaKind | Infer ...(hole TcRhoType)...

    tcHsType :: TcTyMode -> HsType GhcRn -> ExpKind -> TcM TcType

* When the `ExpKind` argument is (Check ki), we /check/ that the type has
  kind `ki`
* When the `ExpKind` argument is (Infer hole), we /infer/ the kind of the
  type, and fill the hole with that kind