Remove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc
Background
Currently, we carefully avoid HsType GhcTc
or HsDecl GhcTc
, by means of the NoGhcTc
type family:
| HsAppType (XAppTypeE p) -- After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p)) -- ^ Visible type application
The primary reason for this is that kind-checking and desugaring of types are intertwined. We mostly work with TcType
instead of HsType GhcTc
because it's more convenient in some places (e.g. in unifyKind
and unifyType
).
Motivation A
A better architecture would be to have similar pipelines for terms and types:
HsExpr GhcPs -> HsExpr GhcRn -> HsExpr GhcTc
HsType GhcPs -> HsType GhcRn -> HsType GhcTc
This would allow us to talk about e.g. HsDecl GhcTc
. For example, when discussing #12088, there was an idea of a refactoring that would separate tcTyClDecl
and zonking. But then we'd like the type of tcTyClDecl
to be:
tcTyClDecl :: LTyClDecl GhcRn -> TcM (LTyClDecl GhcTc)
And that's not currently possible.
Motivation B
This would facilitate fixing #15824, for instance, as we could use HsType GhcTc
as the input to GHC.Tc.Gen.Splice.reifyType
. This way, we would retain the HsOpTy
and HsAppTy
distinction.
Partial Solution
In order to address Motivation B, we would need to properly embed coercions into HsType GhcTc
and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following XXType
instance:
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
Then HsType GhcTc
would only ever use XHsType (HsTypeTc ty doc)
. The fields are as follows:
-
TcType
is the kind-checked, desugared type -
SDoc
is the result of pretty printingHsType GhcRn
, before parentheses and infix operators were discarded
This is sufficient to let us talk about HsType GhcTc
and HsDecl GhcTc
, and remove the NoGhcTc
type family.
Full Solution
The full solution would involve using HsType GhcTc
throughout the type checker, rewriting zonking and unification to work over HsType GhcTc
, and so on. It would address Motivation A, and also let us remove the notion of TcType
: the type checker would work with HsType GhcTc
, and Type
would be only used in Core. That would be a nice improvement, as we could remove TcTyVar
and AnonArgFlag
(maybe something else?) from the syntax of Core.
Completion
- The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.