Skip to content

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 (closed), 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 printing HsType 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

  1. 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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information