GHC+DH Weekly Update #3, 2023-01-11

Hi all, I’m delighted to share another progress report on the implementation of dependent types in GHC.

This week I continued to work on @k-binders in type declarations, and I focused on two issues in particular: associated types and kind inference.

When a class has a standalone kind signature, its associated types use the same code path as CUSKs (specifically, the kcCheckDeclHeader_cusk function). So my initial plan to disregard CUSKs as a legacy feature didn’t pan out: I have to support them for the sake of associated types.

-- Associated type and data families with @-binders
type C :: forall k. k -> Constraint
class C (a :: j) where
  type F @j a :: j
  data D @j a :: j

What kinds do we assign to F and D? If we simply ignored the @ symbol, as if the user wrote type F j a :: j and data D j a :: j, then the existing code would infer the following kinds:

F :: forall j -> j -> j
D :: forall j -> j -> j

This is quite close to what we need, except that we want forall j. instead of forall j ->:

F :: forall j. j -> j
D :: forall j. j -> j

Turns out, this is not particularly hard to achieve. I started by modifying bindExplicitTKBndrs_Q_Skol to preserve the visibility flag instead of discarding it, and then I introduced a small helper to match on it:

mkExplicitTyConBinder (Bndr tv flag) =
  case flag of
    HsBndrRequired    -> mkRequiredTyConBinder mentioned_kv_set tv
    HsBndrInvisible{} -> mkNamedTyConBinder Specified tv

That’s about it. I’m very happy with how little code I had to change.

Kind inference turned out to be more tricky. There are two steps involved:

  1. kcInferDeclHeader assigns an initial kind to a type constructor
  2. generaliseTcTyCon zonks it and computes the final kind

The initial kind may contain metavariables, and it does not draw a distinction between k -> r and forall (a :: k) -> r, using the former representation for both. The final kind has no metavariables and uses different representations for dependent and non-dependent kind variables.

In between those two steps, kind inference happens. What I needed to figure out was how to pass visibility information between kcInferDeclHeader and generaliseTcTyCon. The data structure connecting them is the TcTyCon:

data TyCon = TyCon {
        tyConUnique  :: !Unique,
        tyConName    :: !Name,
        tyConBinders          :: [TyConBinder],
        tyConResKind          :: Kind,
        tyConHasClosedResKind :: Bool,
        tyConTyVars    :: [TyVar],
        tyConKind      :: Kind,
        tyConArity     :: Arity,
        tyConNullaryTy :: Type,
        tyConRoles :: [Role],
        tyConDetails :: !TyConDetails

data TyConDetails = TcTyCon {
        tctc_scoped_tvs :: [(Name,TcTyVar)],
        tctc_is_poly :: Bool,
        tctc_flavour :: TyConFlavour
  | ...  -- other constructors

And I didn’t know if I had to add more information to it or reuse the existing fields. Then I found this comment:

-- NB: spec_req_tvs = spec_tvs ++ req_tvs
--     And req_tvs is 1-1 with tyConTyVars
--     See Note [Scoped tyvars in a TcTyCon] in GHC.Core.TyCon

This one-to-one correspondence is exactly what I need because I can store visibility information in tyConBinders and then use zipWith to connect it with req_tvs. All of this took me some time to figure out, but in the end it works, and the code changes are minimal. The following GHCi session is now possible:

ghci> data T @k (a :: k) @j (b :: j)
ghci> :k T
T :: forall k. k -> forall j. j -> Type

Note how GHC inferred forall k. and forall j. from the corresponding binders in data T. At this point I have working kind checking and kind inference for @k-binders in type declarations. This is a good checkpoint.

The new feature is to be guarded by the TypeAbstractions flag, which I added separately in commit bc125775. The reason for adding the flag separately from the feature is that there are actually three major components to be included in the TypeAbstractions extension:

  1. @-binders in constructor patterns
  2. @-binders in function parameters
  3. @-binders in type declarations

This is all laid out in GHC Proposals #448 and #425. One of those components has been inconspicuously present since GHC 9.2, but it was guarded behind a combination of TypeApplications and ScopedTypeVariables instead of a dedicated language extension, so I figured that correcting this should be done in its own commit.

There are still other improvements pending, but I expect to start asking other GHC contributors to review my branch in the coming weeks.

I also decided to tackle a closely related issue #22478. My idea is to move the check for duplicate bindings from rnHsPatSigTypeBindingVars to collectPatsBinders. There is a nice synergy between this task and visible forall, which requires similar modifications to collectPatsBinders. I’ve made some progress locally, but haven’t pushed it yet.

Finally, I’d like to mention two patches by my colleague Rinat that have been merged upstream:

  • Commit b2857df4: Added a new warning about compatibility with RequiredTypeArguments
  • Commit 300bcc15: Parse qualified terms in type signatures

Both of those are steps towards dependent types, too.

And that’s it for this week. Let me know if you have any questions!

This work is funded by Serokell :purple_heart:


Thank you as always! Very exciting. You and Rinat seem to be taking massive strides!

1 Like