Use bidirectional typechecking for types and type patterns

This ticket proposes to fix two separate issues.

See also !10725 (merged), #22478 (closed), #18986 (closed)

Higher rank kinds

The interaction of type patterns and higher-rank kinds is tricky. Consider

-- Example 1
data T where
  MkT :: forall (f :: forall k. k->Type). f Int -> f Bool -> T
g (MkT @f x y) = ...

Here I'd expect the existential f to be brought into scope with kind f :: forall k. k -> Type.

-- Example 2
type S :: (forall k. k -> Type) -> Type
h (Just @(S f) x) = ...

Here again we know f :: forall k. k -> Type.

It's all very similar to tcPat. We arrange to "push the expected type inwards".

We should do exactly this for types as well. That would remove the special cases described in Note [Type patterns: binders and unifiers] in !10725 (merged).

Two tc_hs_type functions

In GHC.Tc.Gen.HsType there are two functions

• Infer kind: tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
• Check kind: tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType

In a way that I don't quite understand, the data constructors of HsType are split between then, each taking some, and defering to the other for the other constructors.

This is hard to grok. And it's totally different to the way that expresions and patterns are handled; they have a single function, with an ExpType argument to distinguish inference and checking

Plan

I propose that we treat types the same way as we do patterns and expressions: one function does both inference and checking, using an ExpType argument to tell which.

For Pat and HsExpr we need a function for Pat and a function for Expr. For types, type patterns are still just HsType, so it is even possible we could use just one function for both type patterns and type expressions. But that's the cherry on the cake