GHC+DH Weekly Update #6, 2023-06-07

After a long break, this is the sixth update on the implementation of dependent types in GHC.

Highlight: The MR that implements @k-binders has been merged.

  • Commit 4aea0a72: Invisible binders in type declarations

The feature will be available in GHC 9.8. I’ve talked about it in the previous reports, but as a reminder, it enables the following syntax if you turn on TypeAbstractions:

type D :: forall k j. k -> j -> Type
data D @k @j a b = ...
--     ↑  ↑
--   invisible binders

In order to make this happen, I prepared a head.hackage patchset (see !302) to adapt a bunch of packages to the breaking changes to template-haskell. This was the last requirement I had to fulfill before the feature could land.

@k-binders are a prerequisite for the following directions of work, which are finally unblocked:

  • Deprecating CUSKs
  • Removal of arity inference for type constructors

I intend to work on those next.

In other news, I’ve discarded my previous attempts at implementing specificity subsumption or a separate visibility check in favor of a much simpler approach of ignoring the visibility flag in eqType but taking it into account in tcEqType. See !10587 “Ignore forall visibility in eqType”. This is basically a one-line change, but the main difficulty is to justify this design decision. That’s where my failed attempts came in handy – I had developed enough understanding of the problem to write extensive documentation and a variety of tests.

Don’t hesitate to ask me any questions about this.


This work is funded by Serokell :purple_heart:

25 Likes

Such a massive undertaking! Huge congratulations :slight_smile:

4 Likes

After the first report, I’ve done various tasks, so let’s go over them one by one:

The first task was to implement the part of GHC proposal #448 Modern Scoped Type Variables about extension shuffling.

Short description: ScopedTypeVariables extension does three different things. Firstly, it enables pattern signatures:


not (a :: Bool) = Prelude.not a

    -- ↑ disallowed without ScopedTypeVariables

The second thing the extension does is add type variables from a type class and an instance head into the scope of its methods:


class C a where

  f :: a -> a

  f x = (x :: a) -- `a` scoped from the class head

-- and

instance C a => C (Identity a) where

  f = coerce @(a -> a) f

            -- ↑ `a` scoped from the instance head

And the third one is about scoping type variables from forall everywhere:


id :: forall a . a -> a

id x = (x :: a)

f = Left @a :: forall a . a -> Either a ()

-- and so on

With proposal #448 these would be three different extensions: PatternSignatures, MethodTypeVariables, and ExtendedForAllScope. ScopedTypeVariables will simply enable them all. I did this split up in !10385.

The proposal in the section I am describing also declares a new extension ImplicitForAll that allows you to control if you want to have implicit forall’s and a new warning - -Wpattern-signature-binds that warns about type variable binding in pattern signature, but currently, they are under discussion. I have a merge request with -Wpattern-signature-binds implemented, but I’m not sure that it will be merged into master: !10585.

Next, I did a couple of small documentation improvements: !10327 and !10366.

The first of them just describe ImplicitParams extension behavior more precisely. GHC must always use the most nested binding of the implicit variable:


f = let ?foo = 5 in let ?foo = 6 in ?foo -- `f` must be 6. If it isn't, then GHC has a bug

data D where

  MkD :: (?foo :: Int) -> D

g MkD MkD = ?foo -- here ?foo must come from the second matching

If GHC violates this behavior (I hope it will not anyway), you can point to the new section of the GHC User’s Guide in an issue description.

The second documentation improvement mentions nubOrd from the containers package as a better alternative to the nub function from the base in nub's haddock.

After that, I addressed issue #22558. Here GHC allows haddock comments, that should be rejected:


module

  -- | Bad comment for the module

  T17544_kw where

data Foo -- | Bad comment for MkFoo

  where MkFoo :: Foo

newtype Bar -- | Bad comment for MkBar

  where MkBar :: () -> Bar

class Cls a

    -- | Bad comment for clsmethod

  where

    clsmethod :: a

I reanimated two merge requests that in conjunction solve this issue: !9476 and !9477. The first of them adds tokens module, signature, data, newtype, class, where into Haskell AST and updates all the places that use updated constructors. The second one applies these tokens in GHC.Parser.PostProcess.Haddock to reject malformed comments. These merge requests a ready, but no one wants to review them (x1).

Then in discussion under my merge requests with extension shuffling was found an issue with -Wterm-variable-capture: #23434. This warning notifies you if you have an implicitly bound type variable that has the same name as a term-level variable, but it ignores the fact that the type variable may be bound in the type class head


k = 12

class C k a where

  type AT a :: k -> Type

            -- ↑ `k` bound in the class head, but

            -- `-Wterm-variable-capture` produces

            -- warning

I fixed this issue in the merge request !10548, but no one wants to review it (x2).

And at the end, I solved an old issue !16635. Here the problem is in a scoping distinction between term level and type level:


{-# LANGUAGE ScopedTypeVariables #-}

-- f :: [forall b . Either b ()]

f = [Right @a @() () :: forall a. Either a ()] -- works

type F = '[Right @a @() () :: forall a. Either a ()] -- doesn't work

               -- ↑ not in scope

The complication is that we can’t elaborate this type into Core. In term level GHC at desugaring phase inserts lambda with a type variable, so introduces binder for a


f = [(\@a -> Right @a @() ()) :: forall a . Either a ()]

But in types we can’t do the same, because we have no lambda in types


type F = '[(/\ a . Right @a @() ()) :: forall a. Either a ()]

         -- ↑ not in haskell :(

We want to unify term level and type level, but we can’t elaborate this type with the current GHC. The partial solution is to move the error from the renaming phase to the elaboration phase, and that is what I did in the merge request !10560. It is also ready for review, but no one wants to do that (x3).

And that’s all for this week! GHC team, please, review my patches.

10 Likes

do you think you can write “dependent haskell” in the title going forward? Because “DH” is too short to search

1 Like

I think I can but that’d make the title too long. Searching for “GHC+DH” works for me.

2 Likes

That seems fine to me, but … drawback is that someone has to know that trick to find the posts. (I didn’t, initially, so I had to ask. Now I do, but someone else won’t.)

Would “Dependent GHC” be short enough? Like this:

Dependent GHC weekly update #6, 2023-06-07

Also, is “weekly” necessary? Maybe it doesn’t have to say “weekly”, even if the folks working on DH are able and willing to provide weekly updates.

I’m not sure we need weekly updates anyway. I certainly don’t, but maybe others do. It’s just nice to know that progress is being made. (In my case, don’t know enough to understand all of the components of the project.)

(For comparison, there were periodic reports in discus.ocaml.org about progress toward the new multicore revision, which took years. I don’t think there was ever more than a monthly report, and I’m not sure that was always provided. I think it was good enough for most people who were interested to know that it was being worked on, and that there were challenges that the team was overcoming. Garbage collection had to be substantially reworked, for example, but we didn’t get detailed updates about changes in GC until it was done, as I recall. I may have missed some reports, though.)

I’m not an insider, so whatever others think will be fine with me.

3 Likes

I agree that “Glasgow Haskell Compiler + Dependent Haskell Weekly Update #n, YYYY-MM-DD” would be very long, if that’s what you’re thinking. What about just “dependent haskell, update #n”. After all, the date, the frequency of the update, and fact that the Haskell compiler in question is the GHC, seem like unnecessary data for a subject title.

But whatever, it’s not important. Name it whatever you like. Glad to see you’re back. Cheers.

1 Like

In this video from 2021 (starting at 6:35) by @rae, he references a document that he’s shared with @simonpj but that is not public. He has a section for current commits, a section called “the stack” of language change prerequisites that must be done before dependent types can be implemented, including

  • Kill Derived
  • m/kAppTy
  • Predicated not types
  • Homogeneous equality
  • TypeLike

Then he has a longer section of actual dependent haskell steps, called Road Map. He doesn’t showcase it in the video much, but you can see that the first few bullets are:

  • Rewrite only at top level
  • Inefficient flattening in FamInstEnv
  • Loose type maps
  • BoxedRep, then unlifted data types
  • Normalize type
  • Kill Derived
  • Use predicates, not types
  • TypeLike and friends
  • etc

Have you seen this document?

The commit you’re writing about today, about invisible binders in type declarations, and about forall visibility in eqType, do these correspond to any of the bullets in Richard’s and Simon’s roadmap checklist?

These weekly updates are good at saying what has happened recently. But if you want to know the current state of play (what is being worked on), there is a helpful DH current status page on the GHC wiki.

4 Likes