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:
-
kcInferDeclHeaderassigns an initial kind to a type constructor -
generaliseTcTyConzonks 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:
-
@-binders in constructor patterns -
@-binders in function parameters -
@-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 