# 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).

###
`tc_hs_type`

functions

Two 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