This ticket proposes to fix two separate issues. See also !10725, #22478, #18986 ### 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. ### 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