Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Require building with GHC 9.10 #587

Merged
merged 7 commits into from
May 12, 2024
Merged

Require building with GHC 9.10 #587

merged 7 commits into from
May 12, 2024

Conversation

RyanGlScott
Copy link
Collaborator

@RyanGlScott RyanGlScott commented May 4, 2024

This is a collection of patches needed to make singletons, singletons-th, and singletons-base build with GHC 9.10 (and in the case of singletons-{th,base}, require them to build with GHC 9.10). The two most interesting commits (whose commit messages I have included below) are the ones involving changes to the arities of type families. GHC 9.10 no longer performs arity inference (see the commit messages below), so we need to explicitly use TypeAbstractions in more places to give promoted type families the correct arities.

This makes more progress towards #569.

singletons: Support building with GHC 9.10

Because GHC 9.10 no longer performs arity inference in type-level declarations (see
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst), we now must use TypeAbstractions in certain singletons definitions to make GHC 9.10 accept them.

One part of a fix for #566.

singletons-th: Adapt to GHC 9.10's lack of arity inference

GHC 9.10 no longer performs arity inference in type-level declarations (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst), and as it turns out, many of the promoted type families that singletons-th generates would have the wrong arity. For instance, singletons-th would promote this definition:

f :: Either a Bool
f = Right True

To this type family:

type F :: Either a Bool
type family F where
  F = Right True

With GHC 9.10 or later, however, GHC would conclude that F has arity 0, which means that it should not bind any arguments (visible or invisible). The type family equation for F, however, only works if F has arity 1! This is because the type family equation needs to bind an invisible @a argument:

  F @A = Right @A @Bool True

To ensure that type families like F have the expected arity, singletons-th now uses TypeAbstractions in more places to ensure that type family headers bind an appropriate number of type variables, which makes the type families' arities explicit. For instance, singletons-th now generates the following code for F:

type F :: Either a Bool
type family F @A where -- Note the @A here, which gives it arity 1
  F = Right True

For more details on how this is implemented, see the new Note [Generating type families with the correct arity] in Data.Singletons.TH.Promote.

A consequence of this change is that the average piece of singletons-th–generated code is much more likely to require TypeAbstractions than it did before. This explains why we now enable TypeAbstractions in almost every module in singletons-base.

Fixes #566.

This requires a more recent version of `haskell-ci` that supports GHC 9.10.1.
Another change that this more recent version of `haskell-ci` introduces is that
it drops support for pre-20.04 versions of Ubuntu, so we must also upgrade to a
more recent version of Ubuntu (I chose Ubuntu 22.04, or Jammy Jellyfish).

Unfortunately, `haskell-ci`'s GHCJS support no longer works with recent
versions of Ubuntu (see haskell-CI/haskell-ci#723),
so I had to remove the GHCJS configuration from the CI. This does not mean that
`singletons` is dropping JavaScript support, however, as we still plan to
support building the `singletons` library with GHC's JavaScript backend (the
modern successor to GHCJS).

There is currently no way to set up a GHC JavaScript backend CI job using
`haskell-ci`, and the amount of setup required to manually create one is such
that I'm putting it off for now. If someone asks for it, we can add one later.
Because GHC 9.10 no longer performs arity inference in type-level declarations
(see
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst),
we now must use `TypeAbstractions` in certain `singletons` definitions to make
GHC 9.10 accept them.

One part of a fix for #566.
GHC 9.10 includes `foldl'` as part of the `Prelude`, which makes some
`Data.Foldable` imports redundant. Let's remove them.
GHC 9.10 no longer performs arity inference in type-level declarations (see
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst),
and as it turns out, many of the promoted type families that `singletons-th`
generates would have the wrong arity. For instance, `singletons-th` would
promote this definition:

```hs
f :: Either a Bool
f = Right True
```

To this type family:

```hs
type F :: Either a Bool
type family F where
  F = Right True
```

With GHC 9.10 or later, however, GHC would conclude that `F` has arity 0, which
means that it should not bind any arguments (visible or invisible). The type
family equation for `F`, however, only works if `F` has arity 1! This is
because the type family equation needs to bind an invisible `@a` argument:

```hs
  F @A = Right @A @Bool True
```

To ensure that type families like `F` have the expected arity, `singletons-th`
now uses `TypeAbstractions` in more places to ensure that type family headers
bind an appropriate number of type variables, which makes the type families'
arities explicit. For instance, `singletons-th` now generates the following
code for `F`:

```hs
type F :: Either a Bool
type family F @A where -- Note the @A here, which gives it arity 1
  F = Right True
```

For more details on how this is implemented, see the new `Note [Generating type
families with the correct arity]` in `Data.Singletons.TH.Promote`.

A consequence of this change is that the average piece of
`singletons-th`–generated code is much more likely to require
`TypeAbstractions` than it did before. This explains why we now enable
`TypeAbstractions` in almost every module in `singletons-base`.

Fixes #566.
@RyanGlScott RyanGlScott marked this pull request as ready for review May 12, 2024 22:44
@RyanGlScott RyanGlScott merged commit a0dba46 into master May 12, 2024
24 checks passed
@RyanGlScott RyanGlScott deleted the ghc-9.10 branch May 12, 2024 22:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Adapt to arity inference changes in type-level declarations
2 participants