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