GHC+DH Weekly Update #1, 2022-12-07

Hi all, it’s time for the first weekly update on the implementation of dependent types in GHC.

This week I mainly focused on #425 “Invisible binders in type declarations”. The proposal introduces @k-binders in type, data, newtype, class, type family, and data family declarations:

type KindOf :: forall k. k -> Type
type KindOf @k a = k
--          ↑
--       new syntax

I dusted off an old branch where I had already modified the AST in the appropriate way. The data type in GHC responsible for representing type variable binders is HsTyVarBndr:

data HsTyVarBndr flag pass
  = UserTyVar (XUserTyVar pass) flag (LIdP pass)
  | KindedTyVar (XKindedTyVar pass) flag (LIdP pass) (LHsKind pass)

In a data declaration such as data T k (a :: k) = ..., the k is represented as a UserTyVar because it has no kind annotation, whereas a :: k is represented as a KindedTyVar.

You can see that HsTyVarBndr is also parameterized by a flag. In type declarations, the flag is unused, so it is instantiated to (). In forall telescopes, the flag is instantiated to Specificity and is used to distinguish between forall a. and forall {a}. (if this looks unfamiliar, see #99 “Explicit specificity in type variable binders”).

This flag field looks like the most natural place to store information about the visibility of a binder. First, we need a new data type to represent the choice between k and @k:

data HsBndrVis pass
  = HsBndrRequired
      -- Binder for a visible (required) variable:
      --     type Dup a = (a, a)
      --             ^^^

  | HsBndrInvisible (LHsToken "@" pass)
      -- Binder for an invisible (specified) variable:
      --     type KindOf @k (a :: k) = k
      --                ^^^

And now we can use it as our flag instead of (). We got lucky that this type parameter was already there. Next, let us look at the parser. @-binders are already part of the grammar, but they are rejected by a later validation pass:

ghci> data T @k = MkT
<interactive>:1:9: error:
    Unexpected type application @k
    In the data declaration for ‘T’

The code responsible for this looks like this:

check (HsTypeArg _ ki@(L loc _)) =
  addFatalError $ mkPlainErrorMsgEnvelope (locA loc) $
    PsErrUnexpectedTypeAppInDecl ki pp_what (unLoc tc)

It is not difficult to make it produce a HsTyVarBndr instead of a parse error. This marks our first milestone: we can represent the new syntax in the AST and we can parse it from source.

Next up: Template Haskell support. At the moment, its AST is entirely separate from the one used by GHC, so we need to make the corresponding changes to it and update the conversion functions. Updating the TH AST is a bit of a headache, because if you get it wrong, you get mysterious errors when GHC tries to bootstrap itself. And since I’ve spent all my luck on the AST and the parser, this one just had to go wrong. In any case, I managed to debug it and all is well in the end.

The conversion functions in GHC.HsToCore.Quote posed a bit of a challenge. It took me a while to disentangle the relationship between addSimpleTyVarBinds, addHsTyVarBinds, addQTyVarBinds, and addTyClTyVarBinds, and I initially couldn’t figure out the correct way to add support for HsBndrVis to them. But after studying the code, I have come to the realization that addTyClTyVarBinds was actually misused in two places, and those happened to be the places that were problematic to update. I corrected this in a separate refactoring:

  • Commit 5d267d46: FreshOrReuse instead of addTyClTyVarBinds

The commit message explains it in more detail. With this refactoring in place, I managed to add TH support for invisible binders (mostly). There are still some issues around reification, but I decided to save them for later.

Then I decided to address the build failures I was getting in haddock. Since I added some new information to the types (namely, the HsBndrVis flag), Haddock did not know how to render it (i.e. convert it to HTML or LaTeX). When I began to update it, I spotted two other pre-existing issues that are not directly related to my changes but affect parts of the code that I was modifying. So I opened merge requests to fix those:

  • atSign has no unicode variant (!20)
  • LaTeX: fix printing of type variable bindings (!21)

One of those is a minor refactor, the other corrects a serious bug in the LaTeX backend. I suspect that not so many people use the LaTeX backend if such an egregious error was not reported before.

Anyway, with those fixes in place, I added support for invisible binders to Haddock and moved on to the most intriguing part: type checking. When it comes to type checking left-hand sides of type declarations, there are three independent code paths involved:

  • The kind inference case
  • The complete user-supplied kind case (CUSK)
  • The standalone kind signature case (SAKS)

Thanks to my prior experience with the implementation of StandaloneKindSignatures, I knew what to do in the SAKS case right off. In fact, I specified it right in the proposal text in pseudo-code: see the SAKS zipping algorithm. So I went ahead and implemented the zippable and skippable conditions in matchUpSigWithDecl.

The CUSK case is actually not specified in the proposal. Since CUSKs are a legacy feature, I thought I could simply avoid dealing with them by rejecting @k-binders. Then I thought that it would be, perhaps, a bit more elegant to say that @k-binders are not covered by the CUSK conditions, so we would fall back to the inference case. And then I realized that it might cause trouble in associated type families whose parent class has a SAKS, since we still rely on the CUSK code path to check them. Admittedly, this is something of an exotic edge case, but I would prefer to get it right, so I will need more time to think about it (and produce a compelling test case).

Finally, the kind inference case is a bit tricky, but doable. GHC is already capable of inferring forall-quantified kinds and preserving their order relative to other binders: it does so for VDQ in kinds. If you declare data T k (a :: k) j (b :: j), its inferred kind will be:

T :: forall k -> k -> forall j -> j -> Type

This is nice, because it means that we have the basic infrastructure in place. If we want to handle data T @k (a :: k) @j (b :: j), we could use the same inference algorithm but remember that k and j should be quantified with an invisible forall instead of VDQ:

T :: forall k. k -> forall j. j -> Type

However, I am yet to figure out a good place to store this information (my first instinct is to add it to TcTyVar, but that might have unforeseen and far-reaching implications).

Some other things I did while working on #425 were:

  • rebased my prototype onto type data TH updates
  • rewrote HsTypeArg to use LHsToken (!9486)
  • identified a potential bug in repNewtype (narrator: it was not a bug)
  • opened #22560 and submitted !9480

In parallel with all of that, I continued my work on #281 “Visible forall in types of terms”. The proposal extends the support of VDQ (forall a ->) from kinds to types:

-- Definition:
idv :: forall a -> a -> a
idv (type a) x = x :: a

-- Usage:
n = idv (type Double) 42

This is something I began to implement a few months back (see #22326, !9257), but it was blocked on the outcome of a discussion (#558) about the best way to accommodate this change in GHC Core. And this week I’ve finally come up with an approach that might provide a reasonable way forward, which I called specificity subsumption. The gist of it is:

  1. in GHC Core we would not draw a distinction between inferred, specified, and required binders
  2. in Haskell we would have a separate check to reject programs that abuse this notion

I described this idea in a comment. The next steps would be to formalize specificity subsumption in typing rules and to sketch out an implementation in GHC.

Inspired by getting unstuck on this issue, I rebased the prototype and fixed a bug in it. The bug concerned non-linear type variable bindings:

f :: forall (a :: Type) (b :: Type) -> ()
f (type t) (type t) = ()

This program should be rejected since it has conflicting bindings for t, but my prototype did not detect this. I fixed it by extending collectPatsBinders with a new mode in which it would also collect type variables.

Lastly, I also dedicated some time to bug fixes and refactorings unrelated to dependent types. I opened a ticket about a long-standing issue about processing Haddock comments after parsing (#22558), described how it can be fixed in three steps, and started to implement those steps in !9473, !9476, and !9477. The approach looks promising and the first merge request of the three has already been accepted.

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


This work is funded by Serokell :purple_heart:

25 Likes

What a great write up! Excellent job Vlad.

6 Likes

Is there a kind of “big picture” roadmap to dependent haskell? what will be next after binders and visible forall? can we checkout your branch and try out the new syntax?

2 Likes

Is there a kind of “big picture” roadmap to dependent haskell?

There is a design sketch in GHC Proposal #378 “Design for Dependent Types”, but no specific roadmap. When I am done with my current tasks, I will pick something else that brings us closer to the described design.

what will be next after binders and visible forall?

In the short term, I intend to work on some or all of the following:

  • #448 “Modern Scoped Type Variables”
  • #402 “Stable GADT constructor syntax”
  • #475 “Non-punning list and tuple syntax”
  • #12088 “Type/data family instances in kind checking”

In the long term, we are still missing promotion of term-level functions and a dependently-typed core language.

can we checkout your branch and try out the new syntax?

You are more than welcome to! If you find any issues, let me know and I will turn them into test cases. The branches are wip/int-index/emb-type and wip/int-index/decl-invis-binders.

9 Likes

For those waiting for the next weekly update that is due today, I’ve been mostly reading the Quick Look paper and prototyping an implementation of specificity subsumption, but I figured it’s not much for an entire report, so I’ll write one next week.

5 Likes